OAI/Combinatorics/LowSpaceSubsetSum/Storage/MixerPreparationCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Counting the three already stored mixer domains

The domain lists are retained throughout all three counts. Each count constructs only two half arrays and streams their sum tournament; the peak is independent of the number of emitted pairs. Domain construction is a separate preceding phase, whose returned lists are the explicit input here.

  1. def OAI.LowSpaceSubsetSum.MixerPreparationCells.source line 19
  2. def OAI.LowSpaceSubsetSum.MixerPreparationCells.run line 23
  3. theorem OAI.LowSpaceSubsetSum.MixerPreparationCells.run_value line 29
  4. theorem OAI.LowSpaceSubsetSum.MixerPreparationCells.scalar_bound line 37
  5. theorem OAI.LowSpaceSubsetSum.MixerPreparationCells.run_cells line 60
  6. theorem OAI.LowSpaceSubsetSum.MixerPreparationCells.counts_root line 77