OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionArrayBuild.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Building the compression trial's stored arrays

All seven compact lists are materialized once. Their capacity test precedes raw-list and pair-list construction. The resulting arrays are shared by all residue passes.

  1. def OAI.LowSpaceSubsetSum.CompressionArrayBuild.pairSums line 18
  2. theorem OAI.LowSpaceSubsetSum.CompressionArrayBuild.pairSums_value line 24
  3. theorem OAI.LowSpaceSubsetSum.CompressionArrayBuild.pairSums_work line 29
  4. theorem OAI.LowSpaceSubsetSum.CompressionArrayBuild.pairSums_work_le line 35
  5. structure OAI.LowSpaceSubsetSum.CompressionArrayBuild.Blocks line 40
  6. def OAI.LowSpaceSubsetSum.CompressionArrayBuild.compactLists line 45
  7. def OAI.LowSpaceSubsetSum.CompressionArrayBuild.passed line 48
  8. def OAI.LowSpaceSubsetSum.CompressionArrayBuild.assemble line 51
  9. def OAI.LowSpaceSubsetSum.CompressionArrayBuild.run line 60
  10. def OAI.LowSpaceSubsetSum.CompressionArrayBuild.source line 72
  11. theorem OAI.LowSpaceSubsetSum.CompressionArrayBuild.compactLists_source line 76
  12. theorem OAI.LowSpaceSubsetSum.CompressionArrayBuild.passed_source line 80
  13. theorem OAI.LowSpaceSubsetSum.CompressionArrayBuild.assemble_source line 85
  14. theorem OAI.LowSpaceSubsetSum.CompressionArrayBuild.run_source line 96