OAI/Combinatorics/LowSpaceSubsetSum/Search/StoppedDecisionRound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Repetition of the two actually stopped trial algorithms

Both branches use their shared-budget executions. No solution, mean deficiency test, or unbounded source computation chooses the runtime branch.

  1. def OAI.LowSpaceSubsetSum.StoppedDecision.compressionAccept line 19
  2. def OAI.LowSpaceSubsetSum.StoppedDecision.representationAccept line 22
  3. def OAI.LowSpaceSubsetSum.StoppedDecision.accept line 28
  4. theorem OAI.LowSpaceSubsetSum.StoppedDecision.sound line 33
  5. theorem OAI.LowSpaceSubsetSum.StoppedDecision.representation_probability line 44
  6. theorem OAI.LowSpaceSubsetSum.StoppedDecision.probability line 63
  7. theorem OAI.LowSpaceSubsetSum.StoppedDecision.repeated_sound line 99
  8. theorem OAI.LowSpaceSubsetSum.StoppedDecision.repeated_probability line 105