OAI/Combinatorics/LowSpaceSubsetSum/Search/PreparedDecision.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Counter-executed decision rounds and their fixed input guard

The repeated procedure uses stored preparation and interrupted trials. Its finite seed law includes the auxiliary coupling coordinates used in the success analysis.

  1. abbrev OAI.LowSpaceSubsetSum.PreparedDecision.Seed line 18
  2. def OAI.LowSpaceSubsetSum.PreparedDecision.run line 21
  3. def OAI.LowSpaceSubsetSum.PreparedDecision.law line 27
  4. theorem OAI.LowSpaceSubsetSum.PreparedDecision.sound line 30
  5. theorem OAI.LowSpaceSubsetSum.PreparedDecision.probability line 36
  6. theorem OAI.LowSpaceSubsetSum.PreparedDecision.work line 45
  7. def OAI.LowSpaceSubsetSum.PreparedDecision.core line 51
  8. def OAI.LowSpaceSubsetSum.PreparedDecision.guarded line 58
  9. theorem OAI.LowSpaceSubsetSum.PreparedDecision.guarded_sound line 65
  10. theorem OAI.LowSpaceSubsetSum.PreparedDecision.guarded_probability line 69