def Hex.NumberTower.RawEvaluation.evalCoords? (levels : List Level) : Array Rat → Option AlgebraicRoot

Evaluate raw mixed-radix coordinates at the absolute roots stored by a top-first level list.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.RawEvaluation.evalCoords? [] x✝ = do let value ← Hex.AlgebraicPoly.Common.rational? (x✝.getD 0 0) some value.toRoot

def Hex.NumberTower.RawEvaluation.evalPoly? (levels : List Level) (f : Array (Array Rat)) (candidate : AlgebraicRoot) : Option AlgebraicRoot

Exact lazy Horner evaluation of a raw tower polynomial at an absolute candidate root.

Equations

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

def Hex.NumberTower.RawEvaluation.coordsMajorant (levels : List Level) : Array Rat → Nat

Integer magnitude majorant for raw coordinates under every embedding of the stored level polynomials.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.RawEvaluation.coordsMajorant [] x✝ = Hex.PolyQuot.ratAbsCeil (x✝.getD 0 0)

def Hex.NumberTower.RawEvaluation.evalBall? (levels : List Level) (f : Array (Array Rat)) (candidate : AlgebraicRoot) (prec : Nat) : Option DyadicComplexBall

Certified ball Horner evaluation for raw tower coefficients.

Equations

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

def Hex.NumberTower.RawEvaluation.vanishesAt? (levels : List Level) (f : Array (Array Rat)) (candidate : AlgebraicRoot) : Option Bool

Decide at the prescribed finite precision endpoint whether a raw tower polynomial vanishes at an absolute candidate root.

Equations

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