OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionSampleCells.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Live storage for the bounded compression sample

The accepted digits are materialized once. The prime candidate tuple is retained, but not searched, when the digit sampler fails. Ideal backup values remain proof data and do not select an execution branch.

  1. def OAI.LowSpaceSubsetSum.CompressionSampleCells.run line 18
  2. theorem OAI.LowSpaceSubsetSum.CompressionSampleCells.value line 31
  3. theorem OAI.LowSpaceSubsetSum.CompressionSampleCells.cells line 37
  4. theorem OAI.LowSpaceSubsetSum.CompressionSampleCells.cells_scale line 47