OAI/Combinatorics/LowSpaceSubsetSum/Streams/MeasuredLog2.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A bounded tail-recursive binary logarithm

This is the integer operation needed to turn measured mixer counts into prime widths. Each iteration divides by two and updates two counters.

  1. def OAI.LowSpaceSubsetSum.MeasuredLog2.loop line 13
  2. theorem OAI.LowSpaceSubsetSum.MeasuredLog2.loop_value line 19
  3. theorem OAI.LowSpaceSubsetSum.MeasuredLog2.loop_work line 35
  4. def OAI.LowSpaceSubsetSum.MeasuredLog2.run line 45
  5. theorem OAI.LowSpaceSubsetSum.MeasuredLog2.run_value line 47
  6. theorem OAI.LowSpaceSubsetSum.MeasuredLog2.run_work line 55