OAI/Combinatorics/LowSpaceSubsetSum/Search/DecisionRound.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Input-only rounds and the mean-deficiency dichotomy

Each round samples and runs compression followed by representation. The analysis chooses which trial supplies its success probability; the program does not compute mean deficiency. The runtime target is always the original target, and sampler exhaustion rejects only that trial.

  1. theorem OAI.LowSpaceSubsetSum.roundLogBudget line 26
  2. abbrev OAI.LowSpaceSubsetSum.RoundOutcome line 33
  3. def OAI.LowSpaceSubsetSum.roundLaw line 37
  4. def OAI.LowSpaceSubsetSum.roundCompressionAccept line 41
  5. def OAI.LowSpaceSubsetSum.roundRepresentationAccept line 45
  6. def OAI.LowSpaceSubsetSum.roundAccept line 51
  7. theorem OAI.LowSpaceSubsetSum.input_representation_acceptance line 56
  8. theorem OAI.LowSpaceSubsetSum.roundAccept_sound line 75
  9. theorem OAI.LowSpaceSubsetSum.round_acceptance_probability line 88
  10. theorem OAI.LowSpaceSubsetSum.repeated_round_sound line 122
  11. theorem OAI.LowSpaceSubsetSum.repeated_round_probability line 128