OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationOneCells.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Live cells of one buffered parent report

The completed tie buffer and saved cursor remain shared while replaying its records. A long group clones the saved tournament before replaying the suffix. Every return, including each budget failure, preserves the measured join-one result and has a bound independent of the suffix length.

  1. def OAI.LowSpaceSubsetSum.RepresentationOneCells.bufferRead line 18
  2. def OAI.LowSpaceSubsetSum.RepresentationOneCells.buffer line 21
  3. theorem OAI.LowSpaceSubsetSum.RepresentationOneCells.buffer_value line 28
  4. theorem OAI.LowSpaceSubsetSum.RepresentationOneCells.buffer_cells line 46
  5. def OAI.LowSpaceSubsetSum.RepresentationOneCells.run line 76
  6. theorem OAI.LowSpaceSubsetSum.RepresentationOneCells.run_value line 106
  7. theorem OAI.LowSpaceSubsetSum.RepresentationOneCells.run_cells line 140