OAI/Combinatorics/LowSpaceSubsetSum/Compression/SampledCompressionCells.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Every-outcome storage of the executed sampled compression trial

The trace includes the bounded candidate tuples, materialized permutation, all guarded array construction, and the complete stopped residue scan. The first projection preserves both the Boolean result and its work count.

  1. def OAI.LowSpaceSubsetSum.SampledCompressionCells.retained line 20

    Source documentation

    Retained candidate words, input indices, permutation and scalar fields.

    def retained (n : ℕ) := 32*(n+1)^4+256
  2. def OAI.LowSpaceSubsetSum.SampledCompressionCells.run line 22
  3. theorem OAI.LowSpaceSubsetSum.SampledCompressionCells.value line 33
  4. theorem OAI.LowSpaceSubsetSum.SampledCompressionCells.retained_bound line 40
  5. theorem OAI.LowSpaceSubsetSum.SampledCompressionCells.cells line 55