OAI/Combinatorics/EditApproximation/Binary/BinaryLocalGuardWork.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Every local eligibility test is charged at the bit level, including its rational divisions and the construction of its two thresholds.

  1. def OAI.EditApproximation.BinaryFraction.localEligibilityBitBudget line 12
  2. theorem OAI.EditApproximation.BinaryFraction.centerEligibilityWithWork_cost line 16
  3. theorem OAI.EditApproximation.BinaryFraction.refinementScaleGuardWithWork_cost line 50