OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationGroupCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A concrete tie-group execution retaining its shared buffer

The trace includes the incoming pair of readers and dictionary, the completed buffer, lookahead scratch, optional snapshot, and the actual outer replay. Only the result state survives after this call returns.

  1. abbrev OAI.LowSpaceSubsetSum.RepresentationGroupCells.Left line 17
  2. abbrev OAI.LowSpaceSubsetSum.RepresentationGroupCells.Right line 20
  3. def OAI.LowSpaceSubsetSum.RepresentationGroupCells.run line 23
  4. theorem OAI.LowSpaceSubsetSum.RepresentationGroupCells.run_value line 56
  5. theorem OAI.LowSpaceSubsetSum.RepresentationGroupCells.peak_scale line 95
  6. theorem OAI.LowSpaceSubsetSum.RepresentationGroupCells.run_cells line 103