OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorParameterCells.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Live scalar storage while preparing a separating family

The power and logarithm loops use scalar accumulators. The five binomial computations use the actual multiplicative loop, retaining four denominator states and the numerator. Input scalars and all four returned counts fit inside a constant number of cells.

  1. def OAI.LowSpaceSubsetSum.SeparatorParameterCells.powerLoop line 19
  2. theorem OAI.LowSpaceSubsetSum.SeparatorParameterCells.powerLoop_value line 23
  3. theorem OAI.LowSpaceSubsetSum.SeparatorParameterCells.powerLoop_cells line 29
  4. def OAI.LowSpaceSubsetSum.SeparatorParameterCells.logBits line 34
  5. theorem OAI.LowSpaceSubsetSum.SeparatorParameterCells.logBits_value line 39
  6. theorem OAI.LowSpaceSubsetSum.SeparatorParameterCells.logBits_cells line 43
  7. def OAI.LowSpaceSubsetSum.SeparatorParameterCells.sample line 50
  8. theorem OAI.LowSpaceSubsetSum.SeparatorParameterCells.sample_value line 54
  9. theorem OAI.LowSpaceSubsetSum.SeparatorParameterCells.sample_cells line 57
  10. def OAI.LowSpaceSubsetSum.SeparatorParameterCells.families line 62
  11. theorem OAI.LowSpaceSubsetSum.SeparatorParameterCells.families_value line 71
  12. theorem OAI.LowSpaceSubsetSum.SeparatorParameterCells.families_cells line 76
  13. def OAI.LowSpaceSubsetSum.SeparatorParameterCells.run line 85
  14. theorem OAI.LowSpaceSubsetSum.SeparatorParameterCells.run_value line 90
  15. theorem OAI.LowSpaceSubsetSum.SeparatorParameterCells.run_work line 93
  16. theorem OAI.LowSpaceSubsetSum.SeparatorParameterCells.run_cells line 97