theorem Hex.NumberTower.Norm.iterated_isRoot_toRat (T : NumberTower) (f : T.Poly) (z : ℂ) (hroot : (T.toPolynomial f).IsRoot z) : (Polynomial.map (algebraMap ℚ ℂ) (HexPolyMathlib.toPolynomial (Factor.toRatPoly (iterated T.levels.toList (Array.map coeffs (DensePoly.toArray f)))))).IsRoot z

Every root in the fixed tower embedding remains a root of the absolute iterated norm.

theorem Hex.NumberTower.factorRoot?_sound (T : NumberTower) (f : T.Poly) {candidate : AlgebraicRoot} (h : factorRoot? f = some candidate) : Polynomial.eval candidate.toComplex (T.toPolynomial f) = 0

A root returned by the absolute eliminant filter is a root of the input tower polynomial in the fixed embedding.

theorem Hex.NumberTower.factorRoot?_isSome (T : NumberTower) (f : T.Poly) (hdegreeF : 0 < DensePoly.natDegree f) : (factorRoot? f).isSome = true

Every positive-degree tower polynomial supplies an absolute root through its iterated-norm eliminant.

def Hex.NumberTower.Roots.linearProduct {T : NumberTower} : T.Roots → T.Poly

Product of the recorded monic linear factors. The .all case denotes the zero polynomial.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.Roots.all.linearProduct = 0

def Hex.NumberTower.Roots.Positive {T : NumberTower} : T.Roots → Prop

Every finite root entry has positive multiplicity.

Equations

• Hex.NumberTower.Roots.all.Positive = True
• (Hex.NumberTower.Roots.finite roots).Positive = ∀ entry ∈ roots.toList, 0 < entry.2

def Hex.NumberTower.Roots.NoDuplicates {T : NumberTower} : T.Roots → Prop

A finite root array contains no duplicate tower values.

Equations

• Hex.NumberTower.Roots.all.NoDuplicates = True
• (Hex.NumberTower.Roots.finite roots).NoDuplicates = List.Pairwise (fun (a b : T.Elem × ℕ) => a.1 ≠ b.1) roots.toList

def Hex.NumberTower.Roots.Contains {T : NumberTower} (roots : T.Roots) (entry : T.Elem × ℕ) : Prop

Membership in a finite root result. The all-roots result has no finite entries to enumerate.

Equations

• Hex.NumberTower.Roots.all.Contains entry = False
• (Hex.NumberTower.Roots.finite roots_1).Contains entry = (entry ∈ roots_1.toList)

def Hex.NumberTower.Splitting.reconstruct {T : NumberTower} {f : T.Poly} (S : T.Splitting f) : S.extension.tower.Poly

Reconstruct the mapped input from its leading coefficient and returned monic linear factors.

Equations

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

inductive Hex.NumberTower.Splitting.GeneratedBy {T : NumberTower} {f : T.Poly} (S : T.Splitting f) : S.extension.tower.Elem → Prop

Closure of the embedded base and returned roots under field operations.

• base {T : NumberTower} {f : T.Poly} {S : T.Splitting f} (a : T.Elem) : S.GeneratedBy (S.extension.embed a)
• root {T : NumberTower} {f : T.Poly} {S : T.Splitting f} (entry : S.extension.tower.Elem × ℕ) (h : S.roots.Contains entry) : S.GeneratedBy entry.1
• add {T : NumberTower} {f : T.Poly} {S : T.Splitting f} {a b : S.extension.tower.Elem} : S.GeneratedBy a → S.GeneratedBy b → S.GeneratedBy (a + b)
• neg {T : NumberTower} {f : T.Poly} {S : T.Splitting f} {a : S.extension.tower.Elem} : S.GeneratedBy a → S.GeneratedBy (-a)
• mul {T : NumberTower} {f : T.Poly} {S : T.Splitting f} {a b : S.extension.tower.Elem} : S.GeneratedBy a → S.GeneratedBy b → S.GeneratedBy (a * b)
• inv {T : NumberTower} {f : T.Poly} {S : T.Splitting f} {a : S.extension.tower.Elem} : S.GeneratedBy a → S.GeneratedBy a⁻¹

def Hex.NumberTower.Splitting.Sound {T : NumberTower} {f : T.Poly} (S : T.Splitting f) : Prop

Mathematical meaning of a checked splitting result.

Equations

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

theorem Hex.NumberTower.split?_sound (T : NumberTower) (f : T.Poly) {S : T.Splitting f} (h : split? f = some S) : S.Sound

Every returned split payload reconstructs the input and generates the result extension from the listed roots.

theorem Hex.NumberTower.split?_isSome (T : NumberTower) (f : T.Poly) : (split? f).isSome = true

The bounded split/refactor loop succeeds for every tower polynomial.