OAI/Combinatorics/LowSpaceSubsetSum/Storage/PermutationDigitsExecution.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Reading bounded permutation choices into stored digits

The recursive execution stops after a failed range draw and never evaluates the ideal backup permutation. Accepted digits materialize the exact bounded sampler output by the integer-digit array construction.

  1. def OAI.LowSpaceSubsetSum.PermutationDigitsExecution.run line 18
  2. theorem OAI.LowSpaceSubsetSum.PermutationDigitsExecution.value line 29
  3. theorem OAI.LowSpaceSubsetSum.PermutationDigitsExecution.counts line 50
  4. def OAI.LowSpaceSubsetSum.PermutationDigitsExecution.materialize line 68
  5. theorem OAI.LowSpaceSubsetSum.PermutationDigitsExecution.materialize_work line 77
  6. theorem OAI.LowSpaceSubsetSum.PermutationDigitsExecution.materialize_value line 84