OAI/Combinatorics/EditApproximation/Binary/BinaryPhysicalContinuationWork.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual endpoint distances and connection words supply all representation premises of the two Bellman scans and final refinement update.

  1. def OAI.EditApproximation.BinaryFraction.physicalContinuationInputBudget line 12
  2. def OAI.EditApproximation.BinaryFraction.physicalContinuationBitBudget line 15
  3. theorem OAI.EditApproximation.BinaryFraction.endpointDistance_uniform line 20

    Also declared: OAI/Combinatorics/EditApproximation/Binary/BinaryLocalWarmupWork.lean:34 (same declaration text).

  4. theorem OAI.EditApproximation.BinaryFraction.physicalContinuationWithWork_bounds line 30