OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionWeightCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Live storage of compression's compact weight lists

Raw subset masks and their weights use the concrete list generator. The sorted list is compacted by adjacent comparisons, retaining its existing linear work counter and accounting for each recursive return frame.

  1. def OAI.LowSpaceSubsetSum.CompressionWeightCells.tail line 16
  2. theorem OAI.LowSpaceSubsetSum.CompressionWeightCells.tail_value line 26
  3. theorem OAI.LowSpaceSubsetSum.CompressionWeightCells.tail_cells line 34
  4. def OAI.LowSpaceSubsetSum.CompressionWeightCells.dedup line 44
  5. theorem OAI.LowSpaceSubsetSum.CompressionWeightCells.dedup_value line 48
  6. theorem OAI.LowSpaceSubsetSum.CompressionWeightCells.dedup_cells line 53
  7. def OAI.LowSpaceSubsetSum.CompressionWeightCells.compact line 61
  8. theorem OAI.LowSpaceSubsetSum.CompressionWeightCells.compact_value line 69
  9. theorem OAI.LowSpaceSubsetSum.CompressionWeightCells.compact_cells line 74