OAI/Combinatorics/EditApproximation/Binary/BinaryContinuationWork.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bit costs for the full numerical tail after its finite candidate lists have been prepared. Both Bellman minima, the online score minimum, and the final clipped decrement are executed by the counter being bounded.

  1. def OAI.EditApproximation.BinaryFraction.localContinuationInputBudget line 12
  2. def OAI.EditApproximation.BinaryFraction.localContinuationWordBudget line 15
  3. def OAI.EditApproximation.BinaryFraction.localContinuationBitBudget line 18
  4. theorem OAI.EditApproximation.BinaryFraction.localContinuationWithWork_bounds line 25