OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionArrayCells.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Constructing compression arrays with an explicit live-cell trace

All seven compact lists are produced before the capacity test. Only its successful branch allocates the three raw lists and the two pair lists. The completed arrays are shared by subsequent residue passes.

  1. def OAI.LowSpaceSubsetSum.CompressionArrayCells.compactLists line 19
  2. theorem OAI.LowSpaceSubsetSum.CompressionArrayCells.compactLists_value line 25
  3. theorem OAI.LowSpaceSubsetSum.CompressionArrayCells.compact_length line 32
  4. theorem OAI.LowSpaceSubsetSum.CompressionArrayCells.compactLists_cells line 42
  5. def OAI.LowSpaceSubsetSum.CompressionArrayCells.assemble line 57
  6. theorem OAI.LowSpaceSubsetSum.CompressionArrayCells.assemble_value line 68
  7. theorem OAI.LowSpaceSubsetSum.CompressionArrayCells.assemble_cells line 72
  8. def OAI.LowSpaceSubsetSum.CompressionArrayCells.run line 104
  9. theorem OAI.LowSpaceSubsetSum.CompressionArrayCells.value line 119
  10. theorem OAI.LowSpaceSubsetSum.CompressionArrayCells.source_pair_bounds line 126
  11. theorem OAI.LowSpaceSubsetSum.CompressionArrayCells.cells line 151
  12. theorem OAI.LowSpaceSubsetSum.CompressionArrayCells.cells_scale line 213