OAI/Combinatorics/LowSpaceSubsetSum/Storage/CanonicalMixerCells.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Complete canonical mixer preparation with shared domains

The three interval domains are built from the stored permutation, retained while their half-array tournaments are counted, and passed directly to the integer parameter stage. Every returned value and work counter agrees with the input-only preparation used by the trial.

  1. def OAI.LowSpaceSubsetSum.CanonicalMixerCells.run line 21
  2. theorem OAI.LowSpaceSubsetSum.CanonicalMixerCells.run_value line 30
  3. theorem OAI.LowSpaceSubsetSum.CanonicalMixerCells.scalar_bound line 44
  4. theorem OAI.LowSpaceSubsetSum.CanonicalMixerCells.run_cells line 70
  5. def OAI.LowSpaceSubsetSum.CanonicalMixerCells.prepare line 95
  6. theorem OAI.LowSpaceSubsetSum.CanonicalMixerCells.prepare_value line 101
  7. theorem OAI.LowSpaceSubsetSum.CanonicalMixerCells.parameters_bound line 106
  8. theorem OAI.LowSpaceSubsetSum.CanonicalMixerCells.prepare_cells line 124
  9. theorem OAI.LowSpaceSubsetSum.CanonicalMixerCells.half_capacity line 132
  10. theorem OAI.LowSpaceSubsetSum.CanonicalMixerCells.prepare_cells_capacity line 139