def Hex.ZPoly.normalizeEval (q : ZPoly) : ZPoly

Remove zero roots and content from a candidate-evaluation eliminant.

Equations

• q.normalizeEval = q.removeX.primitivePart

def Hex.ZPoly.evalLowerDenom (q : ZPoly) : Nat

Denominator in the reciprocal-Cauchy lower bound |z| ≥ 1 / (1 + height q) for a nonzero root z of the normalized evaluation eliminant.

Equations

• q.evalLowerDenom = 1 + q.normalizeEval.coeffAbsMax

def Hex.Disambiguation.evalMajorant {A : Type} [Zero A] [DecidableEq A] (f : DensePoly A) (valueBound : A → Nat) (q : ZPoly) : Nat

Error-amplification majorant for Horner evaluation at a root of q, parameterized by an integer magnitude bound on coefficients so tower elements can reuse the same recurrence. The factor two on the root bound covers the |re| + |im| centre magnitude used by complex-ball multiplication; the three extra propagated-error units cover centre-radius conversion and the bilinear radius term.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PolyQuot.ratAbsCeil (q : Rat) : Nat

Ceiling of the absolute value of a rational, computed with integer arithmetic.

Equations

• Hex.PolyQuot.ratAbsCeil q = (q.num.natAbs + q.den - 1) / q.den

def Hex.PolyQuot.valueMajorant {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) : Nat

Integer magnitude majorant for a fixed-field coordinate evaluated at any root of its defining polynomial.

Equations

• a.valueMajorant = Array.foldr (fun (coeff : Rat) (acc : Nat) => acc * (2 ^ Hex.cauchyExp p + 1) + Hex.PolyQuot.ratAbsCeil coeff) 0 a.coeffs.toArray

def Hex.PolyQuot.evalMajorant {p : ZPoly} {x : SimpleRoot p} (f : DensePoly (PolyQuot p x)) (q : ZPoly) : Nat

Error-amplification majorant for Horner evaluation at a root of q.

The state tracks a value bound V and a coefficient of the common input error E. For (acc * y) + c, coefficient errors are at most one nominal unit. The update E' = 2*V + 2*B*E + 3*E + 1 covers root error, the |re| + |im| inflation in propagated accumulator error, their product, and coefficient error.

Equations

• Hex.PolyQuot.evalMajorant f q = Hex.Disambiguation.evalMajorant f Hex.PolyQuot.valueMajorant q

def Hex.evalDisambiguationLimit (q : ZPoly) (majorant : Nat) : Nat

The specified finite search endpoint ceilLog2(ceil(2 * (1 + height(q)) * C)) + 2. All inputs are integral, so the displayed ceiling is already exact.

Equations

• Hex.evalDisambiguationLimit q majorant = Hex.ceilLog2 (2 * q.evalLowerDenom * Nat.max 1 majorant) + 2

def Hex.evalRadiusSmall (q : ZPoly) (radius : Dyadic) : Bool

The evaluation radius is below one third of the reciprocal-Cauchy lower bound, written without division as 3 * D * radius < 1. The factor three is needed because Hex.DyadicComplexBall.excludesZero uses the centre's maximum coordinate, which can be a factor sqrt 2 below its Euclidean norm.

Equations

• Hex.evalRadiusSmall q radius = decide (↑(3 * q.evalLowerDenom) * radius < 1)

def Hex.evalDisambiguationPrec (q : ZPoly) (majorant : Nat) (evalAt : Nat → Option DyadicComplexBall) : Option Nat

Least precision in the finite prescribed range whose certified Horner ball has sufficiently small radius. A failed ball construction is skipped; the companion proves that the endpoint succeeds for the shipped evaluators.

Equations

• One or more equations did not get rendered due to their size.

def Hex.retainZero? (q : ZPoly) (majorant : Nat) (evalAt : Nat → Option DyadicComplexBall) : Option Bool

Decide whether a candidate evaluation can be zero. A zero eliminant is retained immediately. Otherwise evaluate at the first sufficiently small precision and retain exactly when the certified ball does not exclude zero.

Equations

• One or more equations did not get rendered due to their size.