OAI/Combinatorics/LowSpaceSubsetSum/Storage/MixerCountCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Complete half-array and streamed mixer-count storage

Both half arrays stay live throughout the tournament count. The input domain is split once. No Cartesian list is constructed at any stage.

  1. def OAI.LowSpaceSubsetSum.MixerCountCells.run line 17
  2. theorem OAI.LowSpaceSubsetSum.MixerCountCells.run_value line 27
  3. theorem OAI.LowSpaceSubsetSum.MixerCountCells.run_cells line 32
  4. def OAI.LowSpaceSubsetSum.MixerCountCells.count line 68
  5. theorem OAI.LowSpaceSubsetSum.MixerCountCells.count_value line 73
  6. theorem OAI.LowSpaceSubsetSum.MixerCountCells.count_cells line 77