OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedResidueLoop.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Tail-recursive residue enumeration with one shared budget

The loop keeps a residue counter and releases each completed bucket before starting its successor. The work accumulator avoids return frames.

  1. def OAI.LowSpaceSubsetSum.BudgetedResidueLoop.reference line 15
  2. def OAI.LowSpaceSubsetSum.BudgetedResidueLoop.loop line 19
  3. def OAI.LowSpaceSubsetSum.BudgetedResidueLoop.run line 33
  4. def OAI.LowSpaceSubsetSum.BudgetedResidueLoop.allowance line 36
  5. theorem OAI.LowSpaceSubsetSum.BudgetedResidueLoop.allowance_eq line 40
  6. theorem OAI.LowSpaceSubsetSum.BudgetedResidueLoop.loop_account line 55
  7. theorem OAI.LowSpaceSubsetSum.BudgetedResidueLoop.account line 116
  8. theorem OAI.LowSpaceSubsetSum.BudgetedResidueLoop.value line 121
  9. theorem OAI.LowSpaceSubsetSum.BudgetedResidueLoop.remaining line 150
  10. theorem OAI.LowSpaceSubsetSum.BudgetedResidueLoop.complete line 181