OAI/Combinatorics/LowSpaceSubsetSum/Storage/PartitionLabelCells.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Live candidate, permutation, and balanced-label arrays

Only the accepted label vector survives a component. During construction the digits, temporary permutation, and label vector are all counted. The sequential family retains earlier label vectors while later draws run.

  1. def OAI.LowSpaceSubsetSum.PartitionLabelCells.run line 18
  2. theorem OAI.LowSpaceSubsetSum.PartitionLabelCells.run_value line 31
  3. theorem OAI.LowSpaceSubsetSum.PartitionLabelCells.run_cells line 37
  4. theorem OAI.LowSpaceSubsetSum.PartitionLabelCells.size_eq line 45
  5. def OAI.LowSpaceSubsetSum.PartitionLabelCells.family line 49
  6. theorem OAI.LowSpaceSubsetSum.PartitionLabelCells.family_value line 63
  7. theorem OAI.LowSpaceSubsetSum.PartitionLabelCells.family_cells line 78