OAI/Combinatorics/EditApproximation/Binary/BinarySeedMedianWork.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The natural seed cache stores a trimmed result, so repeated median passes do not accumulate leading zero words. The trimming scan is charged.

  1. theorem OAI.EditApproximation.BinaryFraction.seedMedianWithWork_value line 15
  2. theorem OAI.EditApproximation.BinaryFraction.seedMedianWithWork_length line 20
  3. def OAI.EditApproximation.BinaryFraction.seedMedianBitBudget line 25
  4. theorem OAI.EditApproximation.BinaryFraction.seedMedianWithWork_cost line 27