def Hex.NumberTower.Evaluation.evalElem? {T : NumberTower} (a : T.Elem) : Option AlgebraicRoot

Evaluate a fixed tower element in its chosen absolute embedding.

Equations

• Hex.NumberTower.Evaluation.evalElem? a = Hex.NumberTower.RawEvaluation.evalCoords? T.levels.toList (Hex.NumberTower.coeffs a)

def Hex.NumberTower.Evaluation.evalPoly? {T : NumberTower} (f : T.Poly) (candidate : AlgebraicRoot) : Option AlgebraicRoot

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

Equations

• Hex.NumberTower.Evaluation.evalPoly? f candidate = Hex.NumberTower.RawEvaluation.evalPoly? T.levels.toList (Array.map Hex.NumberTower.coeffs (Hex.DensePoly.toArray f)) candidate

def Hex.NumberTower.Evaluation.evalBall? {T : NumberTower} (f : T.Poly) (candidate : AlgebraicRoot) (prec : Nat) : Option DyadicComplexBall

Certified ball Horner evaluation at the tower's fixed embedding and one absolute candidate root. Each exact coefficient is refined far enough to supply the common 2^-prec input-error unit consumed by Hex.Disambiguation.evalMajorant.

Equations

• Hex.NumberTower.Evaluation.evalBall? f candidate prec = Hex.NumberTower.RawEvaluation.evalBall? T.levels.toList (Array.map Hex.NumberTower.coeffs (Hex.DensePoly.toArray f)) candidate prec

def Hex.NumberTower.Evaluation.vanishesAt? {T : NumberTower} (f : T.Poly) (candidate : AlgebraicRoot) : Option Bool

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

Equations

• Hex.NumberTower.Evaluation.vanishesAt? f candidate = Hex.NumberTower.RawEvaluation.vanishesAt? T.levels.toList (Array.map Hex.NumberTower.coeffs (Hex.DensePoly.toArray f)) candidate

def Hex.NumberTower.liftZPoly (T : NumberTower) (p : ZPoly) : T.Poly

Lift an integer polynomial coefficientwise to a tower polynomial.

Equations

• T.liftZPoly p = Hex.DensePoly.ofCoeffs (Array.map (fun (coefficient : Int) => T.ofRat ↑coefficient) (Hex.DensePoly.toArray p))

def Hex.NumberTower.selectFactor? (T : NumberTower) (candidate : AlgebraicRoot) (factors : Array (T.Poly × Nat)) : Option T.Poly

Retain the unique multiplicity-one irreducible factor that vanishes at the specified absolute root under the tower's fixed embedding.

Equations

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

def Hex.NumberTower.levelOfFactor {T : NumberTower} (candidate : AlgebraicRoot) (selected : T.Poly) : Level

Encode a selected monic relative factor as one raw extension level.

Equations

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

inductive Hex.NumberTower.Roots (T : NumberTower) : Type

Root data for a polynomial over a completed splitting tower.

• all {T : NumberTower} : T.Roots
• finite {T : NumberTower} (roots : Array (T.Elem × Nat)) : T.Roots

def Hex.NumberTower.Roots.finite? {T : NumberTower} : T.Roots → Option (Array (T.Elem × Nat))

The recorded roots with multiplicity, or none for the zero polynomial, every element being a root of that.

Equations

• (Hex.NumberTower.Roots.finite roots).finite? = some roots
• Hex.NumberTower.Roots.all.finite? = none

def Hex.NumberTower.Roots.toArray {T : NumberTower} (roots : T.Roots) : Array (T.Elem × Nat)

The recorded roots with multiplicity; the zero polynomial gives the empty array.

Equations

• roots.toArray = roots.finite?.getD #[]

@[simp]

theorem Hex.NumberTower.Roots.finite?_finite {T : NumberTower} (roots : Array (T.Elem × Nat)) : (finite roots).finite? = some roots

@[simp]

theorem Hex.NumberTower.Roots.finite?_all {T : NumberTower} : all.finite? = none

@[simp]

theorem Hex.NumberTower.Roots.toArray_finite {T : NumberTower} (roots : Array (T.Elem × Nat)) : (finite roots).toArray = roots

@[simp]

theorem Hex.NumberTower.Roots.toArray_all {T : NumberTower} : all.toArray = #[]

structure Hex.NumberTower.Splitting (T : NumberTower) (f : T.Poly) : Type

A checked extension together with all roots of the original polynomial in that extension.

• extension : T.Extension

  The extension over which the polynomial splits into linear factors.

• roots : self.extension.tower.Roots

  All roots of the input polynomial in the extended tower.

def Hex.NumberTower.mapPoly {T U : NumberTower} (embed : T.Elem → U.Elem) (f : T.Poly) : U.Poly

Map polynomial coefficients through an explicitly supplied tower embedding.

Equations

• Hex.NumberTower.mapPoly embed f = Hex.DensePoly.ofCoeffs (Array.map embed (Hex.DensePoly.toArray f))

def Hex.NumberTower.Extension.identity (T : NumberTower) : T.Extension

The identity extension, used when no generator needs to be adjoined.

Equations

• Hex.NumberTower.Extension.identity T = { tower := T, embed := id, gen := 0, root := Hex.AlgebraicNumber.zero.toRoot }

@[instance_reducible]

instance Hex.NumberTower.instInhabitedExtension (T : NumberTower) : Inhabited T.Extension

The identity extension is the default, so (adjoin? T r).get! unwraps an adjunction that adjoin?_isSome shows never fails.

Equations

• T.instInhabitedExtension = { default := Hex.NumberTower.Extension.identity T }

def Hex.NumberTower.Extension.trans {T : NumberTower} (outer : T.Extension) (inner : outer.tower.Extension) : T.Extension

Compose dependent tower extensions while retaining the most recently adjoined generator.

Equations

• outer.trans inner = { tower := inner.tower, embed := fun (a : T.Elem) => inner.embed (outer.embed a), gen := inner.gen, root := inner.root }

theorem Hex.NumberTower.Extension.trans_tower {T : NumberTower} (outer : T.Extension) (inner : outer.tower.Extension) : (outer.trans inner).tower = inner.tower

The carrier of a composed extension is the carrier of its inner step.

theorem Hex.NumberTower.Extension.trans_embed {T : NumberTower} (outer : T.Extension) (inner : outer.tower.Extension) (a : T.Elem) : (outer.trans inner).embed a = inner.embed (outer.embed a)

A composed extension embeds by applying the outer and then inner map.

theorem Hex.NumberTower.Splitting.trans_eq {T : NumberTower} {f : T.Poly} (outer : T.Extension) (inner : outer.tower.Splitting (mapPoly outer.embed f)) : { extension := outer.trans inner.extension, roots := inner.roots } = { extension := { tower := inner.extension.tower, embed := fun (a : T.Elem) => inner.extension.embed (outer.embed a), gen := inner.extension.gen, root := inner.extension.root }, roots := inner.roots }

Whole-record normal form for pulling an inner splitting back through an extension. Stating the equality at this level keeps the dependent root carrier aligned while clients reason about the explicit composite.

def Hex.NumberTower.adjoin? (T : NumberTower) (candidate : AlgebraicRoot) : Option T.Extension

Adjoin the specified absolute algebraic root. A selected linear factor produces the identity extension; a nonlinear factor is admitted only through Hex.NumberTower.Internal.extend?, which reruns structural, relative-irreducibility, and fixed- embedding checks before constructing the new carrier index.

Equations

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

def Hex.NumberTower.factorEliminant {T : NumberTower} (f : T.Poly) : ZPoly

Squarefree primitive integer eliminant obtained by taking the selected factor's norm through every tower level.

Equations

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

def Hex.NumberTower.retainRoots? {T : NumberTower} (f : T.Poly) : List AlgebraicRoot → Option (List AlgebraicRoot)

Retain exactly the absolute candidates at which the relative factor vanishes, preserving isolation order.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.retainRoots? f [] = some []

def Hex.NumberTower.factorRoot? {T : NumberTower} (f : T.Poly) : Option AlgebraicRoot

Isolate the absolute eliminant and retain the first root that zeros the relative factor under the current fixed embedding.

Equations

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

def Hex.NumberTower.linearRoots? {T : NumberTower} (factors : Array (T.Poly × Nat)) : Option (Array (T.Elem × Nat))

Recover all roots once a checked factorization is entirely linear.

Equations

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

def Hex.NumberTower.splitAux {T : NumberTower} (f : T.Poly) (fuel : Nat) : Option (T.Splitting f)

Fuel-bounded split/refactor loop. Each recursive call works over the local tower and composes its checked extension on return, retaining the intermediate embedding needed by proof-facing consumers. Every successful nonlinear iteration consumes one fuel unit and must strictly increase the tower dimension.

Equations

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

def Hex.NumberTower.split? {T : NumberTower} (f : T.Poly) : Option (T.Splitting f)

Construct an extension in which the input polynomial splits into linear factors, retaining multiplicities from checked factorization.

Equations

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