theorem Hex.AlgebraicNumber.toRoot_toComplex (a : AlgebraicNumber) : a.toRoot.toComplex = a.toComplex

Forgetting minimality preserves the selected complex value.

theorem Hex.AlgebraicNumber.ofNormalized?_isSome (p : ZPoly) (prim : p.Primitive) (pos_lc : 0 < DensePoly.leadingCoeff p) (pos_degree : 0 < DensePoly.natDegree p) (checked : p.CheckedIrreducible) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) : (ofNormalized? p prim pos_lc pos_degree checked squarefree rep).isSome = true

Canonicalization of an already normalized polynomial is total.

theorem Hex.AlgebraicRoot.exactFactor?_sound (a : AlgebraicRoot) (q : ZPoly) (hq : ∀ (z : ℂ), (HexRootsMathlib.toPolyℂ q).IsRoot z → (HexRootsMathlib.toPolyℂ a.p).IsRoot z) {b : AlgebraicNumber} (h : a.exactFactor? q = some b) : b.toComplex = a.toComplex

Trying a factor is semantically sound whenever every root of that factor is a root of the enclosing polynomial.

theorem Hex.AlgebraicRoot.exactFactor?_isSome (a : AlgebraicRoot) (q : ZPoly) (hprim : q.content = 1) (hpos : 0 < DensePoly.leadingCoeff q) (hdegree : 0 < DensePoly.natDegree q) (hirred : q.isIrreducible = true) (hsimple : HasOnlySimpleRoots q) (hroot : (HexRootsMathlib.toPolyℂ q).IsRoot a.toComplex) : (a.exactFactor? q).isSome = true

A normalized irreducible factor containing the selected root always survives isolation, refinement, and canonicalization.

theorem Hex.AlgebraicRoot.exact?_sound (a : AlgebraicRoot) {b : AlgebraicNumber} (h : a.exact? = some b) : b.toComplex = a.toComplex

Every successful exactification denotes the original selected root.

theorem Hex.AlgebraicRoot.exact?_isSome (a : AlgebraicRoot) : a.exact?.isSome = true

Factor selection and isolation always find the canonical representative.

theorem Hex.AlgebraicRoot.exact_toComplex (a : AlgebraicRoot) : a.exact.toComplex = a.toComplex

The total canonicalization wrapper preserves the represented value.

theorem Hex.PolyQuot.root_eq_of_meetsBall {q : ZPoly} (hq : q ≠ 0) (r : RefinedIsolation q) {z : ℂ} (hz : (HexRootsMathlib.toPolyℂ q).IsRoot z) {b : DyadicComplexBall} (hzmem : z ∈ b.set) (hbradius : b.realRadius ≤ 2 ^ (-↑(mahlerPrec q))) (hmeet : (↑r).square.meetsBall b = true) : r.root = z

A sufficiently small certified ball can meet a refined isolation only at the root it contains.

theorem Hex.PolyQuot.toAlgebraicNumber?_sound {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) {b : AlgebraicNumber} (hb : a.toAlgebraicNumber? rep h = some b) : b.toComplex = a.toComplex rep h

Successful conversion out of fixed coordinates preserves their value at the selected embedding.

theorem Hex.PolyQuot.toAlgebraicNumber?_isSome {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : (a.toAlgebraicNumber? rep h).isSome = true

The minimal-polynomial and isolation search for fixed coordinates always finds a canonical representative.

theorem Hex.PolyQuot.toAlgebraicNumber_toComplex {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : (a.toAlgebraicNumber rep h).toComplex = a.toComplex rep h

The total fixed-presentation conversion preserves the selected complex value.