OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionFromPermutationCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Live compression storage from an actual stored permutation

Domain and weight construction are performed only after their prepaid guards pass. The resulting arrays are shared across all residue passes.

  1. def OAI.LowSpaceSubsetSum.CompressionFromPermutationCells.finish line 18
  2. theorem OAI.LowSpaceSubsetSum.CompressionFromPermutationCells.finish_value line 34
  3. theorem OAI.LowSpaceSubsetSum.CompressionFromPermutationCells.output_source line 46
  4. theorem OAI.LowSpaceSubsetSum.CompressionFromPermutationCells.output_lengths line 58
  5. theorem OAI.LowSpaceSubsetSum.CompressionFromPermutationCells.scale_step line 71
  6. theorem OAI.LowSpaceSubsetSum.CompressionFromPermutationCells.finish_cells line 77
  7. def OAI.LowSpaceSubsetSum.CompressionFromPermutationCells.run line 122
  8. theorem OAI.LowSpaceSubsetSum.CompressionFromPermutationCells.value line 130
  9. theorem OAI.LowSpaceSubsetSum.CompressionFromPermutationCells.cells line 137