OAI/Combinatorics/LowSpaceSubsetSum/Storage/PartitionArrayExecution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Sequential materialization of the three balanced partition arrays

The stored output consists only of labels in sorted mixer order. Every component executes the bounded permutation sampler, and a failed component stops the remaining draws. The source colorings appear only in refinement.

  1. abbrev OAI.LowSpaceSubsetSum.PartitionArrayExecution.Labels line 17
  2. def OAI.LowSpaceSubsetSum.PartitionArrayExecution.encode line 20
  3. theorem OAI.LowSpaceSubsetSum.PartitionArrayExecution.component_value line 24
  4. def OAI.LowSpaceSubsetSum.PartitionArrayExecution.coupling line 45
  5. def OAI.LowSpaceSubsetSum.PartitionArrayExecution.execution line 50
  6. def OAI.LowSpaceSubsetSum.PartitionArrayExecution.run line 54
  7. theorem OAI.LowSpaceSubsetSum.PartitionArrayExecution.value line 66
  8. theorem OAI.LowSpaceSubsetSum.PartitionArrayExecution.component_work line 106
  9. theorem OAI.LowSpaceSubsetSum.PartitionArrayExecution.work line 115