OAI/Combinatorics/LowSpaceSubsetSum/Storage/BudgetedStoppedCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Constant-retention execution of the stopped join loop

Only the current state survives an iteration. The peak accumulator records the temporary overlap between the old and returned state; no prior state is stored in a continuation frame.

  1. def OAI.LowSpaceSubsetSum.BudgetedStoppedCells.loop line 19
  2. theorem OAI.LowSpaceSubsetSum.BudgetedStoppedCells.loop_value line 38
  3. theorem OAI.LowSpaceSubsetSum.BudgetedStoppedCells.loop_cells line 57
  4. def OAI.LowSpaceSubsetSum.BudgetedStoppedCells.run line 88
  5. theorem OAI.LowSpaceSubsetSum.BudgetedStoppedCells.run_value line 91
  6. theorem OAI.LowSpaceSubsetSum.BudgetedStoppedCells.run_cells line 96