@[implicit_reducible]

def Hex.instCommRingZPoly_hexNumberFieldMathlib_1 : CommRing ZPoly

Proof-local Mathlib CommRing view of ZPoly, assembled from the executable library's verified Lean.Grind.CommRing instance.

Equations

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

theorem Hex.instIsDomainZPoly_hexNumberFieldMathlib_1 : IsDomain ZPoly

Proof-local domain structure on ZPoly, transported from Polynomial Int.

def Hex.RootSet.Contains (roots : RootSet) (z : ℂ) : Prop

Semantic membership in a root set. Every complex number belongs to the root set of the zero polynomial.

Equations

• Hex.RootSet.all.Contains z = True
• (Hex.RootSet.finite entries).Contains z = ∃ entry ∈ entries.toList, entry.root.toComplex = z

noncomputable def Hex.RootSet.multiplicityOf (roots : RootSet) (z : ℂ) : ℕ

The recorded multiplicity of a complex value, or zero when it is absent. The .all case also returns zero, matching Mathlib's convention for Polynomial.rootMultiplicity of the zero polynomial.

Equations

• One or more equations did not get rendered due to their size.
• Hex.RootSet.all.multiplicityOf z = 0

def Hex.RootSet.totalMultiplicity : RootSet → ℕ

Sum of the multiplicities in a finite root set.

Equations

• Hex.RootSet.all.totalMultiplicity = 0
• (Hex.RootSet.finite entries).totalMultiplicity = Array.foldl (fun (total : ℕ) (entry : Hex.RootCount) => total + entry.multiplicity) 0 entries

def Hex.RootSet.Positive : RootSet → Prop

Every stored entry has positive multiplicity.

Equations

• Hex.RootSet.all.Positive = True
• (Hex.RootSet.finite entries).Positive = ∀ entry ∈ entries.toList, 0 < entry.multiplicity

def Hex.RootSet.NoDuplicates : RootSet → Prop

A finite root set contains no two entries with the same semantic value.

Equations

• Hex.RootSet.all.NoDuplicates = True
• (Hex.RootSet.finite entries).NoDuplicates = List.Pairwise (fun (a b : Hex.RootCount) => a.root.toComplex ≠ b.root.toComplex) entries.toList

def Hex.RootSet.Ordered : RootSet → Prop

Finite root entries occur in the executable canonical order.

Equations

• Hex.RootSet.all.Ordered = True
• (Hex.RootSet.finite entries).Ordered = List.Pairwise (fun (a b : Hex.RootCount) => Hex.PolyQuot.Roots.rootLe a b = true) entries.toList

theorem Hex.PolyQuot.Roots.sameValue?_sound (a b : AlgebraicRoot) {same : Bool} (h : sameValue? a b = some same) : same = true ↔ a.toComplex = b.toComplex

A successful lazy-root comparison decides equality of represented complex values.

theorem Hex.PolyQuot.Roots.sameValue?_isSome (a b : AlgebraicRoot) : (sameValue? a b).isSome = true

Lazy-root comparison always succeeds, exactifying only when distinct enclosing polynomials have a nonconstant gcd.

theorem Hex.PolyQuot.Roots.evalBall?_isSome {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (candidate : AlgebraicRoot) (prec : ℕ) : (evalBall? f rep h candidate prec).isSome = true

Certified ball Horner evaluation always reaches its requested precision.

theorem Hex.PolyQuot.Roots.componentRoots?_isSome {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (multiplicity : ℕ) (hMultiplicity : 0 < multiplicity) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (hprim : (normEliminant f).squareFreeCore.content = 1) (hpos : 0 < DensePoly.leadingCoeff (normEliminant f).squareFreeCore) (hdegree : 0 < DensePoly.natDegree (normEliminant f).squareFreeCore) (hsimple : HasOnlySimpleRoots (normEliminant f).squareFreeCore) : (componentRoots? f multiplicity hMultiplicity rep h).isSome = true

Once the norm eliminant passes its normalization checks, component root isolation, refinement, exact evaluation, and bounded disambiguation are total.

theorem Hex.PolyQuot.Roots.componentRoots?_total {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (multiplicity : ℕ) (hMultiplicity : 0 < multiplicity) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (hnorm : normEliminant f ≠ 0) (hdegree : 0 < DensePoly.natDegree (normEliminant f).squareFreeCore) : (componentRoots? f multiplicity hMultiplicity rep h).isSome = true

A nonzero norm eliminant with positive-degree square-free core supplies all normalization witnesses required by the component driver.

theorem Hex.PolyQuot.Roots.mergeRoot_isSome (roots : Array RootCount) (candidate : RootCount) : (mergeRoot roots candidate).isSome = true

Merging a root through a complete semantic scan cannot fail.

theorem Hex.PolyQuot.Roots.mergeRoots_isSome (roots candidates : Array RootCount) : (Array.foldlM mergeRoot roots candidates).isSome = true

Folding semantic root merging over a finite candidate array cannot fail.

theorem Hex.PolyQuot.Roots.yun_positive {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (component : DensePoly (PolyQuot p x) × ℕ) (hcomponent : component ∈ (yun f).toList) : 0 < component.1.natDegree ∧ 0 < component.2

Every component emitted by the executable Yun loop has positive degree and positive multiplicity.

theorem Hex.PolyQuot.Roots.coeffDen_dvd {p : ZPoly} {x : SimpleRoot p} (f : DensePoly (PolyQuot p x)) (i j : ℕ) : ((f.coeff i).coeffs.coeff j).den ∣ commonDen f

Every stored rational coordinate denominator divides the executable common denominator, including zero-extended coefficient reads.

theorem Hex.PolyQuot.Roots.commonDen_pos {p : ZPoly} {x : SimpleRoot p} (f : DensePoly (PolyQuot p x)) : 0 < commonDen f

The executable common denominator is positive.

theorem Hex.PolyQuot.Roots.clearRat_cast (den : ℕ) (q : ℚ) (hden : q.den ∣ den) : ↑(clearRat den q) = ↑den * ↑q

Clearing a rational coordinate against a divisible denominator has the expected value after embedding into ℂ.

theorem Hex.PolyQuot.Roots.coeff_clearedOuter {p : ZPoly} {x : SimpleRoot p} (f : DensePoly (PolyQuot p x)) {i j : ℕ} (hi : i < f.size) (hj : j < DensePoly.natDegree p) : DensePoly.coeff ((clearedOuter f).coeff j) i = clearRat (commonDen f) ((f.coeff i).coeffs.coeff j)

The rectangular coefficient array used for the bivariate lift stores the cleared coordinate at the corresponding outer and polynomial indices.

noncomputable def Hex.PolyQuot.toPolynomialAt {p : ZPoly} {x : SimpleRoot p} (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : Polynomial ℂ

Interpret a fixed-field dense polynomial at the selected embedding.

Equations

• Hex.PolyQuot.toPolynomialAt f rep h = Array.foldr (fun (a : Hex.PolyQuot p x) (value : Polynomial ℂ) => Polynomial.C (a.toComplex rep h) + Polynomial.X * value) 0 f.toArray

theorem Hex.PolyQuot.coeff_toPolynomialAt {p : ZPoly} {x : SimpleRoot p} (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (n : ℕ) : (toPolynomialAt f rep h).coeff n = (f.coeff n).toComplex rep h

Semantic coefficients agree with fixed-coordinate evaluation.

theorem Hex.PolyQuot.toPolynomialAt_eq_map {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : toPolynomialAt f rep h = Polynomial.map (embedding rep h) (HexPolyMathlib.toPolynomial f)

Fixed-field Horner interpretation is polynomial coefficient mapping by the selected complex embedding.

theorem Hex.PolyQuot.poly_isZero_iff {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : f.isZero = true ↔ toPolynomialAt f rep h = 0

Fixed-field executable zero detection agrees with semantic polynomial zero.

theorem Hex.PolyQuot.natDegree_toPolynomialAt {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (_hf : (!f.isZero) = true) : (toPolynomialAt f rep h).natDegree = f.natDegree

A nonzero fixed-field polynomial has the expected semantic degree.

theorem Hex.PolyQuot.Roots.clearedOuter_eval {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (t : ℂ) (hf : 0 < f.size) : Polynomial.eval rep.root (Polynomial.map ((Polynomial.eval₂RingHom (Int.castRingHom ℂ) t).comp HexPolyMathlib.equiv.toRingHom) (HexPolyMathlib.toPolynomial (clearedOuter f))) = ↑(commonDen f) * Polynomial.eval t (toPolynomialAt f rep h)

The integer bivariate lift specializes at the selected generator to the fixed-field polynomial, scaled by its positive common denominator.

theorem Hex.PolyQuot.Roots.normEliminant_isRoot {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (t : ℂ) (hf : (!f.isZero) = true) (hroot : Polynomial.eval t (toPolynomialAt f rep h) = 0) : Polynomial.eval t (HexRootsMathlib.toPolyℂ (normEliminant f)) = 0

Every root at the selected fixed-field embedding is a root of the integer norm eliminant.

theorem Hex.PolyQuot.Roots.normEliminant_ne_zero {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (hf : (!f.isZero) = true) : normEliminant f ≠ 0

The integer norm eliminant of a nonzero fixed-field polynomial is nonzero.

theorem Hex.PolyQuot.Roots.evalEliminant_isRoot {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (e : ZPoly) {z : ℂ} (hf : 0 < f.size) (he : 1 < DensePoly.size e) (hz : (HexRootsMathlib.toPolyℂ e).IsRoot z) : (HexRootsMathlib.toPolyℂ (evalEliminant f e)).IsRoot (Polynomial.eval z (toPolynomialAt f rep h))

The evaluation eliminant vanishes at the evaluation of the fixed-field polynomial at any root of the candidate eliminant and the selected embedding.

theorem Hex.PolyQuot.Roots.evalEliminant_ne_zero {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (e : ZPoly) (hf : (!f.isZero) = true) (he : 1 < DensePoly.size e) : evalEliminant f e ≠ 0

The evaluation eliminant of a nonzero fixed-field polynomial and a positive-degree candidate eliminant is nonzero.

theorem Hex.PolyQuot.Roots.size_pos_of_core_degree {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (hdegree : 0 < DensePoly.natDegree (normEliminant f).squareFreeCore) : 0 < f.size

A positive-degree square-free norm-eliminant core forces the component itself to be nonzero.

theorem Hex.PolyQuot.Roots.componentRoots?_total_of_degree {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (multiplicity : ℕ) (hMultiplicity : 0 < multiplicity) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (hdegree : 0 < f.natDegree) : (componentRoots? f multiplicity hMultiplicity rep h).isSome = true

Every positive-degree fixed-field component satisfies the normalization conditions needed by the component root driver.

theorem Hex.PolyQuot.Roots.evalBall?_sound {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (candidate : AlgebraicRoot) (prec : ℕ) {ball : DyadicComplexBall} (hrun : evalBall? f rep h candidate prec = some ball) : Polynomial.eval candidate.toComplex (toPolynomialAt f rep h) ∈ ball.set

Certified ball Horner evaluation encloses exact evaluation at the selected embedding and candidate root.

theorem Hex.PolyQuot.Roots.retainZero?_correct {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (candidate : AlgebraicRoot) (hf : 0 < f.size) {keep : Bool} (hkeep : retainZero? (evalEliminant f candidate.p) (evalMajorant f candidate.p) (evalBall? f rep h candidate) = some keep) : keep = true ↔ Polynomial.eval candidate.toComplex (toPolynomialAt f rep h) = 0

Bounded disambiguation against the shared double-resultant evaluation eliminant retains precisely the candidates at which the fixed-field polynomial vanishes.

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

The fixed-field root driver always produces a checked root set.

theorem Hex.PolyQuot.roots?_eq_roots {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : roots? f rep h = some (roots f rep h)

The total fixed-field root API is exactly the output of its now-proved total checked driver.

theorem Hex.PolyQuot.roots_all_iff {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : roots f rep h = RootSet.all ↔ toPolynomialAt f rep h = 0

The fixed-field driver returns .all exactly for the zero polynomial.