OAI/Combinatorics/LowSpaceSubsetSum/Word/WordFinalDecision.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

One input-only algorithm with counted preprocessing and fallback

Finite word tables represent fresh independent draws. Only the entries read by the sequential generators are consumed; reused draws are in their counted retained candidate buffers. The input descriptor is computed before the guard.

  1. abbrev OAI.LowSpaceSubsetSum.WordFinalDecision.Words line 20
  2. def OAI.LowSpaceSubsetSum.WordFinalDecision.run line 22
  3. theorem OAI.LowSpaceSubsetSum.WordFinalDecision.sound line 32
  4. theorem OAI.LowSpaceSubsetSum.WordFinalDecision.probability line 39
  5. theorem OAI.LowSpaceSubsetSum.WordFinalDecision.rejects line 59
  6. theorem OAI.LowSpaceSubsetSum.WordFinalDecision.overhead line 64
  7. theorem OAI.LowSpaceSubsetSum.WordFinalDecision.main_bounds line 73
  8. theorem OAI.LowSpaceSubsetSum.WordFinalDecision.work_fits line 93
  9. theorem OAI.LowSpaceSubsetSum.WordFinalDecision.cells_fits line 104