OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionSampleArrays.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Executing compression sampling into stored input arrays

Only accepted range digits are materialized. The prime draw is skipped when the permutation sampler exhausts its allowance. Ideal backup values occur only in the refinement proof, never as a runtime choice.

  1. def OAI.LowSpaceSubsetSum.CompressionSampleArrays.prime line 19
  2. def OAI.LowSpaceSubsetSum.CompressionSampleArrays.run line 23
  3. theorem OAI.LowSpaceSubsetSum.CompressionSampleArrays.value line 34
  4. theorem OAI.LowSpaceSubsetSum.CompressionSampleArrays.complete line 61
  5. theorem OAI.LowSpaceSubsetSum.CompressionSampleArrays.work line 98