OAI/Combinatorics/LowSpaceSubsetSum/Storage/CanonicalGuesses.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Direct interval encoding of the three representation guesses

The stored natural is the lower endpoint plus the accepted bounded range draw. This avoids enumerating a general finite type to decode a guess.

  1. abbrev OAI.LowSpaceSubsetSum.CanonicalGuesses.lower line 15
  2. abbrev OAI.LowSpaceSubsetSum.CanonicalGuesses.upper line 16
  3. def OAI.LowSpaceSubsetSum.CanonicalGuesses.width line 18
  4. theorem OAI.LowSpaceSubsetSum.CanonicalGuesses.endpoints line 20
  5. instance OAI.LowSpaceSubsetSum.CanonicalGuesses.widthNeZero line 24
  6. def OAI.LowSpaceSubsetSum.CanonicalGuesses.encode line 28
  7. def OAI.LowSpaceSubsetSum.CanonicalGuesses.encoding line 37
  8. instance OAI.LowSpaceSubsetSum.CanonicalGuesses.guessNonempty line 54
  9. def OAI.LowSpaceSubsetSum.CanonicalGuesses.coupling line 57
  10. theorem OAI.LowSpaceSubsetSum.CanonicalGuesses.coupling_uniform line 60
  11. theorem OAI.LowSpaceSubsetSum.CanonicalGuesses.coupling_failure line 64
  12. def OAI.LowSpaceSubsetSum.CanonicalGuesses.execution line 68
  13. theorem OAI.LowSpaceSubsetSum.CanonicalGuesses.execution_bounded line 71