OAI/Combinatorics/LowSpaceSubsetSum/Storage/SamplerAttemptCells.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Bounded rejection from an explicit candidate array

The immutable array is counted once. A tail cursor and two counters replace the progressively shifted candidate function. The peak accumulator includes the current evaluator's scratch space on every visited candidate.

  1. def OAI.LowSpaceSubsetSum.SamplerAttemptCells.suffix line 16
  2. theorem OAI.LowSpaceSubsetSum.SamplerAttemptCells.suffix_zero line 19
  3. theorem OAI.LowSpaceSubsetSum.SamplerAttemptCells.suffix_succ line 23
  4. def OAI.LowSpaceSubsetSum.SamplerAttemptCells.runAcc line 31
  5. theorem OAI.LowSpaceSubsetSum.SamplerAttemptCells.runAcc_value line 42
  6. theorem OAI.LowSpaceSubsetSum.SamplerAttemptCells.runAcc_cells line 56
  7. def OAI.LowSpaceSubsetSum.SamplerAttemptCells.run line 72
  8. theorem OAI.LowSpaceSubsetSum.SamplerAttemptCells.run_value line 75
  9. theorem OAI.LowSpaceSubsetSum.SamplerAttemptCells.run_cells line 83
  10. def OAI.LowSpaceSubsetSum.SamplerAttemptCells.range line 89
  11. theorem OAI.LowSpaceSubsetSum.SamplerAttemptCells.range_value line 92
  12. theorem OAI.LowSpaceSubsetSum.SamplerAttemptCells.range_cells line 97
  13. def OAI.LowSpaceSubsetSum.SamplerAttemptCells.prime line 102
  14. theorem OAI.LowSpaceSubsetSum.SamplerAttemptCells.prime_value line 104
  15. theorem OAI.LowSpaceSubsetSum.SamplerAttemptCells.prime_cells line 110