OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationPrefixSource.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Identifying every stored prefix field with its bounded history

The witness is the coupling's ideal history, but only after the concrete prefix has succeeded. The coupling agreement proof then identifies it with the returned bounded history; no backup is used by the execution.

  1. theorem OAI.LowSpaceSubsetSum.RepresentationPrefixArrays.source line 17