theorem Hex.NumberTower.Evaluation.evalElem?_sound (T : NumberTower) (a : T.Elem) {root : AlgebraicRoot} (h : evalElem? a = some root) : root.toComplex = T.toComplex a

Successful executable evaluation of tower coordinates preserves their fixed complex value.

theorem Hex.NumberTower.Evaluation.evalElem?_isSome (T : NumberTower) (a : T.Elem) : (evalElem? a).isSome = true

Coordinate evaluation succeeds for every validated tower element.

theorem Hex.NumberTower.Evaluation.evalPoly?_sound (T : NumberTower) (f : T.Poly) (candidate result : AlgebraicRoot) (h : evalPoly? f candidate = some result) : result.toComplex = Polynomial.eval candidate.toComplex (T.toPolynomial f)

Successful exact tower-polynomial evaluation agrees with semantic polynomial evaluation.

theorem Hex.NumberTower.Evaluation.vanishesAt?_isSome (T : NumberTower) (f : T.Poly) (candidate : AlgebraicRoot) : (vanishesAt? f candidate).isSome = true

The bounded zero test returns a Boolean for every public tower polynomial.

theorem Hex.NumberTower.Evaluation.vanishesAt?_eq_some_true_iff (T : NumberTower) (f : T.Poly) (candidate : AlgebraicRoot) : vanishesAt? f candidate = some true ↔ Polynomial.eval candidate.toComplex (T.toPolynomial f) = 0

The total public zero test returns true exactly at a semantic root.

def Hex.NumberTower.Extension.evalPoly {T : NumberTower} (E : T.Extension) (f : T.Poly) (a : E.tower.Elem) : E.tower.Elem

Evaluate a base-tower polynomial at an extension element after embedding its coefficients.

Equations

• E.evalPoly f a = Array.foldr (fun (coefficient : T.Elem) (value : E.tower.Elem) => E.embed coefficient + a * value) 0 (Hex.DensePoly.toArray f)

def Hex.NumberTower.Extension.Generated {T : NumberTower} (E : T.Extension) : Prop

Every element of the result is generated by the old tower and the distinguished generator.

Equations

• E.Generated = ∀ (b : E.tower.Elem), ∃ (f : T.Poly), E.evalPoly f E.gen = b

def Hex.NumberTower.Extension.AlreadyContains (T : NumberTower) (candidate : AlgebraicRoot) : Prop

The candidate value was already present in the old fixed embedding.

Equations

• Hex.NumberTower.Extension.AlreadyContains T candidate = ∃ (a : T.Elem), T.toComplex a = candidate.toComplex

def Hex.NumberTower.Extension.Sound {T : NumberTower} (candidate : AlgebraicRoot) (E : T.Extension) : Prop

Mathematical meaning of a checked adjoining result.

Equations

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

theorem Hex.NumberTower.toPolynomial_liftZPoly (T : NumberTower) (p : ZPoly) : T.toPolynomial (T.liftZPoly p) = HexRootsMathlib.toPolyℂ p

Lifting an integer polynomial into a tower preserves its complex coefficient polynomial.

theorem Hex.NumberTower.factor_fsts_pairwise {T : NumberTower} {f : T.Poly} (r : T.Factorization f) (hsound : r.Sound) : List.Pairwise (fun (a b : T.Poly × ℕ) => a.1 ≠ b.1) r.factors.toList

Strict canonical factor ordering makes the public factor polynomials pairwise distinct.

theorem Hex.NumberTower.selectFactor?_sound (T : NumberTower) (candidate : AlgebraicRoot) (factors : Array (T.Poly × ℕ)) {selected : T.Poly} (hirreducible : ∀ entry ∈ factors.toList, T.PolynomialIrreducible entry.1) (h : T.selectFactor? candidate factors = some selected) : T.PolynomialIrreducible selected ∧ Polynomial.eval candidate.toComplex (T.toPolynomial selected) = 0

A selected relative factor is irreducible and vanishes at the requested absolute candidate under the fixed embedding.

theorem Hex.NumberTower.Extension.toComplex_evalPoly {T : NumberTower} (E : T.Extension) (hpreserves : E.PreservesEmbedding) (hgenerator : E.GeneratorValue) (f : T.Poly) : E.tower.toComplex (E.evalPoly f E.gen) = Polynomial.eval E.root.toComplex (T.toPolynomial f)

Horner evaluation in a checked extension agrees with ordinary semantic evaluation at its distinguished root.

theorem Hex.NumberTower.adjoin?_sound (T : NumberTower) (candidate : AlgebraicRoot) {E : T.Extension} (h : T.adjoin? candidate = some E) : Extension.Sound candidate E

Every returned adjoining payload satisfies the fixed-embedding, generation, and identity-extension contracts.

theorem Hex.NumberTower.adjoin?_isSome (T : NumberTower) (candidate : AlgebraicRoot) : (T.adjoin? candidate).isSome = true

Factor selection and evaluation disambiguation always produce the checked extension containing the requested algebraic root.