OAI/Combinatorics/LowSpaceSubsetSum/Storage/PartitionLabelExecution.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Stored labels from an actual bounded mixer permutation

For each sorted mixer position, the accepted permutation rank determines its consecutive block label by integer division. Only the resulting label array is retained after the temporary permutation has been scanned.

  1. abbrev OAI.LowSpaceSubsetSum.PartitionLabelExecution.size line 18
  2. def OAI.LowSpaceSubsetSum.PartitionLabelExecution.run line 21
  3. theorem OAI.LowSpaceSubsetSum.PartitionLabelExecution.value line 31
  4. theorem OAI.LowSpaceSubsetSum.PartitionLabelExecution.label_source line 50
  5. theorem OAI.LowSpaceSubsetSum.PartitionLabelExecution.source_value line 58
  6. theorem OAI.LowSpaceSubsetSum.PartitionLabelExecution.complete line 71
  7. theorem OAI.LowSpaceSubsetSum.PartitionLabelExecution.work line 94