noncomputable def Hex.PolyQuot.Roots.toPolynomialMap {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Semiring K] (embedding : PolyQuot p x →+* K) (f : DensePoly (PolyQuot p x)) : Polynomial K

Interpret an executable fixed-field polynomial after a field embedding.

Equations

• Hex.PolyQuot.Roots.toPolynomialMap embedding f = Polynomial.map embedding (HexPolyMathlib.toPolynomial f)

theorem Hex.PolyQuot.Roots.toPolynomialMap_eq_map {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Semiring K] (embedding : PolyQuot p x →+* K) (f : DensePoly (PolyQuot p x)) : toPolynomialMap embedding f = Polynomial.map embedding (HexPolyMathlib.toPolynomial f)

Unfolding rule for the polynomial interpretation used by the Yun proofs.

theorem Hex.PolyQuot.Roots.toPolynomial_derivative {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) : HexPolyMathlib.toPolynomial (derivative f) = Polynomial.derivative (HexPolyMathlib.toPolynomial f)

The executable fixed-field derivative agrees with the Mathlib derivative after dense-polynomial transport.

theorem Hex.PolyQuot.Roots.rootMultiplicity_gcd {K : Type u_1} [Field K] [DecidableEq K] (f g : Polynomial K) (hf : f ≠ 0) (hg : g ≠ 0) (z : K) : Polynomial.rootMultiplicity z (EuclideanDomain.gcd f g) = min (Polynomial.rootMultiplicity z f) (Polynomial.rootMultiplicity z g)

The multiplicity of a root of a polynomial gcd is the minimum of its multiplicities in the two nonzero inputs.

theorem Hex.PolyQuot.Roots.rootMultiplicity_of_mul_eq {K : Type u_1} [Field K] (quotient divisor dividend : Polynomial K) (hdividend : dividend ≠ 0) (hreconstruct : quotient * divisor = dividend) (z : K) : Polynomial.rootMultiplicity z quotient = Polynomial.rootMultiplicity z dividend - Polynomial.rootMultiplicity z divisor

Root multiplicity subtracts across an exact polynomial quotient.

theorem Hex.PolyQuot.Roots.rootMultiplicity_le_natDegree {K : Type u_1} [Field K] (f : Polynomial K) (hf : f ≠ 0) (z : K) : Polynomial.rootMultiplicity z f ≤ f.natDegree

A root's multiplicity is bounded by the degree of a nonzero polynomial.

theorem Hex.PolyQuot.Roots.rootMultiplicity_div {K : Type u_1} [Field K] [DecidableEq K] (dividend divisor : DensePoly K) (hdivisor : divisor ∣ dividend) (hdividend : HexPolyMathlib.toPolynomial dividend ≠ 0) (z : K) : Polynomial.rootMultiplicity z (HexPolyMathlib.toPolynomial (dividend / divisor)) = Polynomial.rootMultiplicity z (HexPolyMathlib.toPolynomial dividend) - Polynomial.rootMultiplicity z (HexPolyMathlib.toPolynomial divisor)

Executable field division subtracts root multiplicities when the divisor is known to divide the nonzero dividend.

theorem Hex.PolyQuot.Roots.rootMultiplicity_monic {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (hf : HexPolyMathlib.toPolynomial f ≠ 0) (z : PolyQuot p x) : Polynomial.rootMultiplicity z (HexPolyMathlib.toPolynomial (monic f)) = Polynomial.rootMultiplicity z (HexPolyMathlib.toPolynomial f)

Monic normalization changes a nonzero polynomial only by a nonzero constant factor, so it preserves every root multiplicity.

theorem Hex.PolyQuot.Roots.toPolynomial_monic_associated {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (hf : HexPolyMathlib.toPolynomial f ≠ 0) : Associated (HexPolyMathlib.toPolynomial (monic f)) (HexPolyMathlib.toPolynomial f)

Monic normalization is associated to its nonzero input.

theorem Hex.PolyQuot.Roots.rootMultiplicity_associated {K : Type u_1} [Field K] [DecidableEq K] {f g : Polynomial K} (h : Associated f g) (z : K) : Polynomial.rootMultiplicity z f = Polynomial.rootMultiplicity z g

Associated polynomials have the same root multiplicity.

theorem Hex.PolyQuot.Roots.rootMultiplicity_monicGcd {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f g : DensePoly (PolyQuot p x)) (hf : HexPolyMathlib.toPolynomial f ≠ 0) (hg : HexPolyMathlib.toPolynomial g ≠ 0) (z : PolyQuot p x) : Polynomial.rootMultiplicity z (HexPolyMathlib.toPolynomial (monic (f.gcd g))) = min (Polynomial.rootMultiplicity z (HexPolyMathlib.toPolynomial f)) (Polynomial.rootMultiplicity z (HexPolyMathlib.toPolynomial g))

The executable monic gcd realizes the pointwise minimum of root multiplicities.

theorem Hex.PolyQuot.Roots.monicGcd_dvd {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f g : DensePoly (PolyQuot p x)) (hf : HexPolyMathlib.toPolynomial f ≠ 0) : monic (f.gcd g) ∣ f ∧ monic (f.gcd g) ∣ g

The executable monic gcd divides each nonzero input.

theorem Hex.PolyQuot.Roots.toPolynomial_div_ne_zero {K : Type u_1} [Field K] [DecidableEq K] (dividend divisor : DensePoly K) (hdivisor : divisor ∣ dividend) (hdividend : HexPolyMathlib.toPolynomial dividend ≠ 0) : HexPolyMathlib.toPolynomial (dividend / divisor) ≠ 0

An exact quotient of a nonzero executable polynomial is nonzero.

theorem Hex.PolyQuot.Roots.toPolynomial_monic_ne_zero {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (hf : HexPolyMathlib.toPolynomial f ≠ 0) : HexPolyMathlib.toPolynomial (monic f) ≠ 0

Monic normalization of a nonzero executable polynomial remains nonzero.

theorem Hex.PolyQuot.Roots.rootMultiplicity_monicDiv {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (dividend divisor : DensePoly (PolyQuot p x)) (hdivisor : divisor ∣ dividend) (hdividend : HexPolyMathlib.toPolynomial dividend ≠ 0) (z : PolyQuot p x) : Polynomial.rootMultiplicity z (HexPolyMathlib.toPolynomial (monic (dividend / divisor))) = Polynomial.rootMultiplicity z (HexPolyMathlib.toPolynomial dividend) - Polynomial.rootMultiplicity z (HexPolyMathlib.toPolynomial divisor)

A monic exact quotient subtracts the divisor's root multiplicity.

theorem Hex.PolyQuot.Roots.map_monic_associated {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] (embedding : PolyQuot p x →+* K) (f : DensePoly (PolyQuot p x)) (hf : toPolynomialMap embedding f ≠ 0) : Associated (toPolynomialMap embedding (monic f)) (toPolynomialMap embedding f)

Monic normalization remains associated after any field embedding.

theorem Hex.PolyQuot.Roots.rootMultiplicity_map_monic {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] [DecidableEq K] (embedding : PolyQuot p x →+* K) (f : DensePoly (PolyQuot p x)) (hf : toPolynomialMap embedding f ≠ 0) (z : K) : Polynomial.rootMultiplicity z (toPolynomialMap embedding (monic f)) = Polynomial.rootMultiplicity z (toPolynomialMap embedding f)

Monic normalization preserves root multiplicity after any field embedding.

theorem Hex.PolyQuot.Roots.rootMultiplicity_map_monicGcd {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] [DecidableEq K] (embedding : PolyQuot p x →+* K) (f g : DensePoly (PolyQuot p x)) (hf : toPolynomialMap embedding f ≠ 0) (hg : toPolynomialMap embedding g ≠ 0) (z : K) : Polynomial.rootMultiplicity z (toPolynomialMap embedding (monic (f.gcd g))) = min (Polynomial.rootMultiplicity z (toPolynomialMap embedding f)) (Polynomial.rootMultiplicity z (toPolynomialMap embedding g))

The executable monic gcd realizes the pointwise minimum of root multiplicities after any field embedding.

theorem Hex.PolyQuot.Roots.map_monicGcd_ne_zero {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] (embedding : PolyQuot p x →+* K) (f g : DensePoly (PolyQuot p x)) (hf : toPolynomialMap embedding f ≠ 0) : toPolynomialMap embedding (monic (f.gcd g)) ≠ 0

The monic gcd of two polynomials that remain nonzero after a field embedding also remains nonzero.

theorem Hex.PolyQuot.Roots.map_derivative {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] (embedding : PolyQuot p x →+* K) (f : DensePoly (PolyQuot p x)) : toPolynomialMap embedding (derivative f) = Polynomial.derivative (toPolynomialMap embedding f)

The executable derivative commutes with every field embedding.

theorem Hex.PolyQuot.Roots.map_div_mul {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] (embedding : PolyQuot p x →+* K) (dividend divisor : DensePoly (PolyQuot p x)) (hdivisor : divisor ∣ dividend) : toPolynomialMap embedding (dividend / divisor) * toPolynomialMap embedding divisor = toPolynomialMap embedding dividend

Exact executable division remains an exact factorization after a field embedding.

theorem Hex.PolyQuot.Roots.map_div_ne_zero {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] (embedding : PolyQuot p x →+* K) (dividend divisor : DensePoly (PolyQuot p x)) (hdivisor : divisor ∣ dividend) (hdividend : toPolynomialMap embedding dividend ≠ 0) : toPolynomialMap embedding (dividend / divisor) ≠ 0

An exact quotient of a polynomial that stays nonzero after embedding also stays nonzero.

theorem Hex.PolyQuot.Roots.rootMultiplicity_map_div {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] (embedding : PolyQuot p x →+* K) (dividend divisor : DensePoly (PolyQuot p x)) (hdivisor : divisor ∣ dividend) (hdividend : toPolynomialMap embedding dividend ≠ 0) (z : K) : Polynomial.rootMultiplicity z (toPolynomialMap embedding (dividend / divisor)) = Polynomial.rootMultiplicity z (toPolynomialMap embedding dividend) - Polynomial.rootMultiplicity z (toPolynomialMap embedding divisor)

Exact executable division subtracts root multiplicities after a field embedding.

theorem Hex.PolyQuot.Roots.rootMultiplicity_map_monicDiv {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] [DecidableEq K] (embedding : PolyQuot p x →+* K) (dividend divisor : DensePoly (PolyQuot p x)) (hdivisor : divisor ∣ dividend) (hdividend : toPolynomialMap embedding dividend ≠ 0) (z : K) : Polynomial.rootMultiplicity z (toPolynomialMap embedding (monic (dividend / divisor))) = Polynomial.rootMultiplicity z (toPolynomialMap embedding dividend) - Polynomial.rootMultiplicity z (toPolynomialMap embedding divisor)

A monic exact quotient subtracts root multiplicities after a field embedding.

theorem Hex.PolyQuot.Roots.map_monicDiv_ne_zero {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] (embedding : PolyQuot p x →+* K) (dividend divisor : DensePoly (PolyQuot p x)) (hdivisor : divisor ∣ dividend) (hdividend : toPolynomialMap embedding dividend ≠ 0) : toPolynomialMap embedding (monic (dividend / divisor)) ≠ 0

A monic exact quotient remains nonzero after a field embedding.

structure Hex.PolyQuot.Roots.YunInvariant {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] (embedding : PolyQuot p x →+* K) (z : K) (r k : ℕ) (w repeated : DensePoly (PolyQuot p x)) : Prop

Pointwise semantic invariant of the Yun loop at multiplicity index k. The first polynomial contains the root once exactly while k ≤ r; the repeated part contains the remaining r - k copies.

• w_ne : toPolynomialMap embedding w ≠ 0

  The current squarefree-product accumulator is nonzero.

• repeated_ne : toPolynomialMap embedding repeated ≠ 0

  The current repeated part is nonzero.

• w_multiplicity : Polynomial.rootMultiplicity z (toPolynomialMap embedding w) = if k ≤ r then 1 else 0

  The accumulator contains z exactly once while copies remain.

• repeated_multiplicity : Polynomial.rootMultiplicity z (toPolynomialMap embedding repeated) = r - k

  The repeated part contains the remaining r - k copies of z.

theorem Hex.PolyQuot.Roots.YunInvariant.step {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] [DecidableEq K] (embedding : PolyQuot p x →+* K) (z : K) (r k : ℕ) (w repeated : DensePoly (PolyQuot p x)) (invariant : YunInvariant embedding z r k w repeated) : have shared := monic (w.gcd repeated); have nextRepeated := monic (repeated / shared); YunInvariant embedding z r (k + 1) shared nextRepeated

One executable Yun step advances the pointwise loop invariant.

theorem Hex.PolyQuot.Roots.YunInvariant.component {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] [DecidableEq K] (embedding : PolyQuot p x →+* K) (z : K) (r k : ℕ) (w repeated : DensePoly (PolyQuot p x)) (invariant : YunInvariant embedding z r k w repeated) : have shared := monic (w.gcd repeated); have component := monic (w / shared); Polynomial.rootMultiplicity z (toPolynomialMap embedding component) = if k = r then 1 else 0

The component produced at a Yun step contains the root exactly when the current index is its original multiplicity.

theorem Hex.PolyQuot.Roots.YunInvariant.init {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] [CharZero K] [DecidableEq K] (embedding : PolyQuot p x →+* K) (f : DensePoly (PolyQuot p x)) (hf : toPolynomialMap embedding f ≠ 0) (hdegree : (toPolynomialMap embedding f).natDegree ≠ 0) (z : K) : have normalized := monic f; have repeated := monic (normalized.gcd (derivative normalized)); have distinct := monic (normalized / repeated); YunInvariant embedding z (Polynomial.rootMultiplicity z (toPolynomialMap embedding f)) 1 distinct repeated

The normalized derivative/gcd prelude establishes the Yun invariant at multiplicity index one.

theorem Hex.PolyQuot.Roots.degree_pos_of_map_root {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] (embedding : PolyQuot p x →+* K) (f : DensePoly (PolyQuot p x)) (hf : toPolynomialMap embedding f ≠ 0) {z : K} (hroot : (toPolynomialMap embedding f).IsRoot z) : 0 < f.natDegree

A nonzero embedded polynomial with a root has positive executable degree.

theorem Hex.PolyQuot.Roots.yun_sound {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] [CharZero K] [DecidableEq K] (embedding : PolyQuot p x →+* K) (f : DensePoly (PolyQuot p x)) (hf : toPolynomialMap embedding f ≠ 0) (hdegree : 0 < f.natDegree) (z : K) (entry : DensePoly (PolyQuot p x) × ℕ) (hentry : entry ∈ (yun f).toList) (hroot : (toPolynomialMap embedding entry.1).IsRoot z) : entry.2 = Polynomial.rootMultiplicity z (toPolynomialMap embedding f)

Every root of an emitted Yun component is a root of the input with the component's stored multiplicity.

theorem Hex.PolyQuot.Roots.yun_complete {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] {K : Type u_1} [Field K] [CharZero K] [DecidableEq K] (embedding : PolyQuot p x →+* K) (f : DensePoly (PolyQuot p x)) (hf : toPolynomialMap embedding f ≠ 0) (hdegree : 0 < f.natDegree) (z : K) (hroot : (toPolynomialMap embedding f).IsRoot z) : ∃ entry ∈ (yun f).toList, (toPolynomialMap embedding entry.1).IsRoot z ∧ entry.2 = Polynomial.rootMultiplicity z (toPolynomialMap embedding f)

Every root of a positive-degree input occurs in an emitted Yun component at its exact multiplicity.