OAI/Combinatorics/LowSpaceSubsetSum/Storage/MixerParameterCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Constant-state integer mixer parameter preparation

The logarithm is evaluated by its actual bounded division loop. Sorting three counts and building the seven scalar parameter fields retain only fixed-size vectors. The input counts are shared throughout.

  1. def OAI.LowSpaceSubsetSum.MixerParameterCells.logLoop line 16
  2. theorem OAI.LowSpaceSubsetSum.MixerParameterCells.logLoop_value line 22
  3. theorem OAI.LowSpaceSubsetSum.MixerParameterCells.logLoop_cells line 30
  4. def OAI.LowSpaceSubsetSum.MixerParameterCells.low line 40
  5. theorem OAI.LowSpaceSubsetSum.MixerParameterCells.low_value line 44
  6. theorem OAI.LowSpaceSubsetSum.MixerParameterCells.low_cells line 48
  7. def OAI.LowSpaceSubsetSum.MixerParameterCells.run line 54
  8. theorem OAI.LowSpaceSubsetSum.MixerParameterCells.run_value line 63
  9. theorem OAI.LowSpaceSubsetSum.MixerParameterCells.run_cells line 74