OAI/Combinatorics/LowSpaceSubsetSum/Search/StoppedGuardedDecision.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The fixed guard with both stopped trial algorithms

The finite decision law uses only completed watchdog executions and the exact fallback.

  1. def OAI.LowSpaceSubsetSum.StoppedDecision.main line 18
  2. def OAI.LowSpaceSubsetSum.StoppedDecision.guarded line 27
  3. theorem OAI.LowSpaceSubsetSum.StoppedDecision.guarded_sound line 34
  4. theorem OAI.LowSpaceSubsetSum.StoppedDecision.guarded_probability line 38
  5. theorem OAI.LowSpaceSubsetSum.StoppedDecision.guarded_rejects line 42