OAI/Combinatorics/EditApproximation/Binary/BinaryUnskippedGuardWork.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

All post-construction band guards, including rounded wide membership and the child imbalance scan, have explicit Boolean arithmetic costs.

  1. def OAI.EditApproximation.BinaryFraction.unskippedGuardInputBudget line 12
  2. def OAI.EditApproximation.BinaryFraction.unskippedGuardBitBudget line 16
  3. theorem OAI.EditApproximation.BinaryFraction.unskippedGuardWithWork_cost line 26