OAI/Combinatorics/LowSpaceSubsetSum/Search/GuardedDecision.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A uniform input-only finite decision core, including the exact fallback

The threshold is a single constant, independent of the input and of its polynomial bit-length promise. No solution or mean deficiency enters the program. The finite sampling law gives one-sided soundness and success probability at least two thirds.

  1. structure OAI.LowSpaceSubsetSum.DecisionThreshold line 22
  2. theorem OAI.LowSpaceSubsetSum.decisionThreshold_exists line 28
  3. def OAI.LowSpaceSubsetSum.decisionThreshold line 33

    Source documentation

    A fixed constant can be chosen once for the finite program.

    def decisionThreshold : DecisionThreshold := Classical.choice decisionThreshold_exists

    Mentions: OAI.LowSpaceSubsetSum.DecisionThreshold, OAI.LowSpaceSubsetSum.decisionThreshold_exists

  4. structure OAI.LowSpaceSubsetSum.DecisionCore line 35
  5. def OAI.LowSpaceSubsetSum.DecisionCore.acceptanceProbability line 43
  6. structure OAI.LowSpaceSubsetSum.CorrectDecisionCore line 50
  7. def OAI.LowSpaceSubsetSum.CorrectDecisionCore.ofLaw line 55
  8. def OAI.LowSpaceSubsetSum.mainDecision line 62
  9. def OAI.LowSpaceSubsetSum.fallbackDecision line 71
  10. def OAI.LowSpaceSubsetSum.guardedDecision line 84
  11. theorem OAI.LowSpaceSubsetSum.guardedDecision_sound line 91
  12. theorem OAI.LowSpaceSubsetSum.guardedDecision_probability line 96
  13. theorem OAI.LowSpaceSubsetSum.guardedDecision_rejects line 101