OAI/Combinatorics/EditApproximation/Coarse/CoarseBinaryBitWork.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryEval_bitWork line 10

   Source documentation

   Actual Boolean work of the complete pruning-stopped evaluator. The hypotheses bound input registers and the common grid, not execution cost.

    theorem coarseBinaryEval_bitWork {B d : ℕ} {α : Type*} [DecidableEq α]
       (k q L N R D A : ℕ) (frame : List (Option α)) (two : BinaryFraction)
       (tree : CoarseSourceTree B α d) (draws : CoarseThresholdDraws B d)
       (hB : 0 < B) (hq : 0 < q) (hL : 0 < L) (htwo : two.value = 2)
       (htw : two.width ≤ A) (hd : Nat.size two.representation.den ≤ D)
       (hroot : two.representation.den = coarseCommonDenominator 1 q L B R)
       (hBbits : Nat.size B + 2 ≤ A) (hqbits : Nat.size q + 2 ≤ A)
       (hLbits : Nat.size L + 2 ≤ A) (hNbits : Nat.size N + 2 ≤ A)
       (hbound : Nat.size (coarseLevelMagnitude N k B R + 2) + 2 * D + 1 ≤ A)
       (j : ℕ) (hdepth : j + d = R) (allowance : BinaryFraction) (start : ℕ)
       (ha : CoarseGridCell two allowance k D A)
       (hpath : allowance.value.den ∣ (L * B * q) ^ j)
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseCommonDenominator, OAI.EditApproximation.BinaryFraction.coarseLevelMagnitude, OAI.EditApproximation.BinaryFraction.CoarseGridCell