OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetDecisionRound.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Acceptance specification with the full-core budget

The finite-law specification accepts only outcomes whose trial succeeds within the full-core budget. The interrupting execution refines this Boolean acceptance predicate.

  1. def OAI.LowSpaceSubsetSum.RepresentationData.budgetedTrial line 23
  2. theorem OAI.LowSpaceSubsetSum.RepresentationData.budgetedTrial_iff line 29
  3. def OAI.LowSpaceSubsetSum.BudgetDecision.representationAccept line 48
  4. def OAI.LowSpaceSubsetSum.BudgetDecision.accept line 54
  5. theorem OAI.LowSpaceSubsetSum.BudgetDecision.input_representation_acceptance line 59
  6. theorem OAI.LowSpaceSubsetSum.BudgetDecision.sound line 79
  7. theorem OAI.LowSpaceSubsetSum.BudgetDecision.acceptance_probability line 92
  8. theorem OAI.LowSpaceSubsetSum.BudgetDecision.repeated_sound line 126
  9. theorem OAI.LowSpaceSubsetSum.BudgetDecision.repeated_probability line 132