OAI/Combinatorics/LowSpaceSubsetSum/Storage/MeasuredSortCells.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Live cells of measured mergesort

Recursive merge retains a bounded frame per emitted item. Mergesort retains its split lists and the completed left result during the right recursion. The trace counts list nodes and bounded record payloads explicitly.

  1. def OAI.LowSpaceSubsetSum.MeasuredSortCells.merge line 16
  2. theorem OAI.LowSpaceSubsetSum.MeasuredSortCells.merge_value line 31
  3. theorem OAI.LowSpaceSubsetSum.MeasuredSortCells.merge_cells line 42
  4. def OAI.LowSpaceSubsetSum.MeasuredSortCells.run line 62
  5. theorem OAI.LowSpaceSubsetSum.MeasuredSortCells.run_value line 76
  6. theorem OAI.LowSpaceSubsetSum.MeasuredSortCells.run_length line 88
  7. theorem OAI.LowSpaceSubsetSum.MeasuredSortCells.run_cells line 92