CoarseBinaryCorrectness.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EditApproximation.BinaryFraction.coarseBinaryEval_rep line 11

Source documentation

Every binary array cell equals the rational shared evaluator, including all pruning outcomes. The sole invariant is the explicitly constructed root denominator and the literal path's allowance denominator.

 theorem coarseBinaryEval_rep {B d : ℕ} {α : Type*} [DecidableEq α]
    (k q L D : ℕ) (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)
    (hroot : two.representation.den = coarseCommonDenominator 1 q L B D)
    (j : ℕ) (hdepth : j + d = D) (allowance : BinaryFraction) (start : ℕ)
    (ha : allowance.representation.den = two.representation.den)
    (hpath : allowance.value.den ∣ (L * B * q) ^ j) :
    CoarseArrayRep (coarseBinaryEval k q L frame two tree draws allowance start).1
      (coarseArrayEval k q (1 / L) frame tree draws allowance.value start).1 := by
…

Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseCommonDenominator, OAI.EditApproximation.BinaryFraction.CoarseArrayRep, OAI.EditApproximation.BinaryFraction.coarseBinaryEval, OAI.EditApproximation.coarseArrayEval