Extended Euclidean Algorithm for CPolynomial

xgcd p q returns a triple (r, s, t) with r = s * p + t * q. Early stop when r.natDegree < threshold. The default threshold = 0 makes r the Greatest Common Divisor of p and q.

For positive thresholds, xgcd_stopSpec characterizes the output: BezoutStopSpec packages the Bézout identity together with the residue/cofactor degree bounds at the stopping point, via the loop invariant BezoutDegreeInvariant.

def CompPoly.CPolynomial.xgcdAux {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (threshold n : ℕ) (r s t r' s' t' : CPolynomial R) : CPolynomial R × CPolynomial R × CPolynomial R

Extended euclidean algorithm on p, q.

Stops when r.natDegree < threshold, r = 0, or fuel n exhausted.

If threshold > 0 then xgcdAux need not compute the greatest common divisor.

Potential optimization: the raw long division behind r' / r already computes r' - (r' / r) * r but it's not exposed through CPolynomial R.

def CompPoly.CPolynomial.xgcd {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) (threshold : ℕ := 0) : CPolynomial R × CPolynomial R × CPolynomial R

Extended euclidean algorithm for (p, q).

Returns (r, s, t) with r = s * p + t * q.

With the default threshold = 0 returns the gcd of p and q. With threshold > 0 stops when r.natDegree < threshold.

If threshold > 0 then xgcdAux need not compute the greatest common divisor.

Bezout-identity correctness

def CompPoly.CPolynomial.Bezout {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R × CPolynomial R × CPolynomial R → Prop

Bezout predicate on a triple (r, s, t): r = s * p + t * q.

theorem CompPoly.CPolynomial.xgcdAux_bezout {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) (threshold n : ℕ) {r r' s t s' t' : CPolynomial R} (h : p.Bezout q (r, s, t)) (h' : p.Bezout q (r', s', t')) : p.Bezout q (xgcdAux threshold n r s t r' s' t')

xgcdAux preserves the Bezout identity.

theorem CompPoly.CPolynomial.xgcd_bezout {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) (threshold : ℕ) : p.Bezout q (p.xgcd q threshold)

The output of xgcd is a Bezout triple for (p, q).

xgcd correctness (threshold 0)

Correctness theorems for xgcd with the default threshold 0.

theorem CompPoly.CPolynomial.xgcdAux_toPoly_eq_gcd {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) (r r' s t s' t' : CPolynomial R) (hn : r.toPoly.degree < ↑n) : (xgcdAux 0 n r s t r' s' t').1.toPoly = EuclideanDomain.gcd r.toPoly r'.toPoly

The gcd component of CompPoly's xgcdAux at threshold 0 coincides with Mathlib's EuclideanDomain.gcd.

theorem CompPoly.CPolynomial.xgcd_toPoly_eq_gcd {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] [DecidableEq R] (p q : CPolynomial R) : (p.xgcd q).1.toPoly = EuclideanDomain.gcd p.toPoly q.toPoly

The gcd component of CompPoly's xgcd at threshold 0 coincides with Mathlib's EuclideanDomain.gcd.

theorem CompPoly.CPolynomial.xgcdAux_toPoly_eq_xgcdAux {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) (r s t r' s' t' : CPolynomial R) (hn : r.toPoly.degree < ↑n) : Prod.map (fun (x : CPolynomial R) => x.toPoly) (fun (x : CPolynomial R × CPolynomial R) => Prod.map (fun (x : CPolynomial R) => x.toPoly) (fun (x : CPolynomial R) => x.toPoly) x) (xgcdAux 0 n r s t r' s' t') = EuclideanDomain.xgcdAux r.toPoly s.toPoly t.toPoly r'.toPoly s'.toPoly t'.toPoly

CompPoly's xgcdAux at threshold 0 coincides with Mathlib's EuclideanDomain.xgcdAux.

theorem CompPoly.CPolynomial.xgcd_toPoly_eq_xgcd {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] [DecidableEq R] (p q : CPolynomial R) : Prod.map (fun (x : CPolynomial R) => x.toPoly) (fun (x : CPolynomial R) => x.toPoly) (p.xgcd q).2 = EuclideanDomain.xgcd p.toPoly q.toPoly

The Bezout component of CompPoly's xgcd coincides with Mathlib's EuclideanDomain.xgcd.

Normalized xgcd

def CompPoly.CPolynomial.normXgcd {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) (threshold : ℕ := 0) : CPolynomial R × CPolynomial R × CPolynomial R

CompPoly's xgcd p q scaled by the inverse leading coefficient of the gcd component, normalizing it to monic.

theorem CompPoly.CPolynomial.normXgcd_bezout {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) (threshold : ℕ) : p.Bezout q (p.normXgcd q threshold)

The normalized extended-gcd output satisfies the Bezout identity.

theorem CompPoly.CPolynomial.normXgcd_fst_toPoly {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] [DecidableEq R] (p q : CPolynomial R) : (p.normXgcd q).1.toPoly = normalize (EuclideanDomain.gcd p.toPoly q.toPoly)

The gcd component of CompPoly's normXgcd is the normalization of Mathlib's EuclideanDomain.gcd

theorem CompPoly.CPolynomial.monicNormalize_toPoly_eq_normalize {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] [DecidableEq R] (p : CPolynomial R) : p.monicNormalize.toPoly = normalize p.toPoly

Monic normalization of computable polynomials agrees with Mathlib normalization.

theorem CompPoly.CPolynomial.gcdMonic_toPoly_eq_normalize_gcd {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] [DecidableEq R] (p q : CPolynomial R) : (p.gcdMonic q).toPoly = normalize (EuclideanDomain.gcd p.toPoly q.toPoly)

The specialized monic gcd has the normalized Mathlib gcd as its toPoly image.

theorem CompPoly.CPolynomial.gcdMonic_eq_normXgcd_fst {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] [DecidableEq R] (p q : CPolynomial R) : p.gcdMonic q = (p.normXgcd q).1

The specialized monic gcd agrees with the gcd component of normalized extended gcd.

theorem CompPoly.CPolynomial.normXgcd_snd_toPoly {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] [DecidableEq R] (p q : CPolynomial R) : Prod.map (fun (x : CPolynomial R) => x.toPoly) (fun (x : CPolynomial R) => x.toPoly) (p.normXgcd q).2 = (EuclideanDomain.gcd p.toPoly q.toPoly).leadingCoeff⁻¹ • EuclideanDomain.xgcd p.toPoly q.toPoly

The Bezout component of normXgcd under toPoly is Mathlib's EuclideanDomain.xgcd scaled by the inverse leading coefficient of the gcd

theorem CompPoly.CPolynomial.normXgcd_fst_comm {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] [DecidableEq R] (p q : CPolynomial R) : (p.normXgcd q).1 = (q.normXgcd p).1

normXgcd is commutative for the gcd component

Stop specification for positive thresholds

BezoutDegreeInvariant is the invariant of the partial-EEA (xgcd) loop: each non-stop step preserves it (BezoutDegreeInvariant.step), and at the stopping threshold it yields the output specification BezoutStopSpec (xgcd_stopSpec).

This is the classical degree theory of the extended Euclidean algorithm — the row identity deg t + deg r' = deg g₀ and the complementary cofactor bound at the stop — i.e. the contract behind rational-function reconstruction and Reed-Solomon decoding.

structure CompPoly.BezoutDegreeInvariant {F : Type u_1} [Ring F] (g₀ g₁ : Polynomial F) (threshold : ℕ) (r s t r' s' t' : Polynomial F) : Prop

Loop invariant of one partial-EEA (xgcd) step.

• bez : r = s * g₀ + t * g₁
• bez' : r' = s' * g₀ + t' * g₁
• det : IsUnit (s' * t - s * t')
• degt : t'.degree < t.degree
• degr : r.degree < r'.degree
• thr : ↑threshold ≤ r'.degree

@[reducible, inline]

abbrev CompPoly.BezoutDegreeInvariantOf {F : Type u_1} [Ring F] (g₀ g₁ : CPolynomial F) (threshold : ℕ) (r s t r' s' t' : CPolynomial F) : Prop

BezoutDegreeInvariant on the toPoly images of a CPolynomial reference pair g₀, g₁ and the two state triples (r, s, t), (r', s', t').

theorem CompPoly.BezoutDegreeInvariant.degree_complement {F : Type u_1} [CommRing F] [NoZeroDivisors F] [Nontrivial F] {g₀ g₁ : Polynomial F} {threshold : ℕ} {r s t r' s' t' : Polynomial F} (h : BezoutDegreeInvariant g₀ g₁ threshold r s t r' s' t') : t.degree + r'.degree = g₀.degree

BezoutDegreeInvariant implies deg t + deg r' = deg g₀.

theorem CompPoly.BezoutDegreeInvariant.step {F : Type u_1} [Field F] {g₀ g₁ : Polynomial F} {threshold : ℕ} {r s t r' s' t' : Polynomial F} (h : BezoutDegreeInvariant g₀ g₁ threshold r s t r' s' t') (hr : r ≠ 0) (hstop : ¬r.natDegree < threshold) : BezoutDegreeInvariant g₀ g₁ threshold (r' - r' / r * r) (s' - r' / r * s) (t' - r' / r * t) r s t

A non-stop Euclidean step preserves the invariant.

structure CompPoly.BezoutStopSpec {F : Type u_1} [Semiring F] (g₀ g₁ : Polynomial F) (threshold : ℕ) (R S T : Polynomial F) : Prop

Stop spec of the partial EEA: R = S g₀ + T g₁, residue degree below threshold, and the cofactor T nonzero with complementary degree deg T + threshold ≤ deg g₀.

• bez : R = S * g₀ + T * g₁
• resDeg : R.natDegree < threshold
• cofDeg : T.degree + ↑threshold ≤ g₀.degree
• cofNe : T ≠ 0

@[reducible, inline]

abbrev CompPoly.BezoutStopSpecOf {F : Type u_1} [Semiring F] (g₀ g₁ : CPolynomial F) (threshold : ℕ) (result : CPolynomial F × CPolynomial F × CPolynomial F) : Prop

BezoutStopSpec on the toPoly images of a CPolynomial reference pair g₀, g₁ and result triple.

theorem CompPoly.xgcdAux_stopSpec_of_invariant {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (g₀ g₁ : CPolynomial F) (threshold : ℕ) (hthr : 1 ≤ threshold) (hg₀ : g₀.toPoly ≠ 0) (n : ℕ) (r s t r' s' t' : CPolynomial F) : BezoutDegreeInvariantOf g₀ g₁ threshold r s t r' s' t' → r.natDegree < n → BezoutStopSpecOf g₀ g₁ threshold (CPolynomial.xgcdAux threshold n r s t r' s' t')

BezoutDegreeInvariant implies xgcdAux's output satisfies the stop spec.

theorem CompPoly.xgcd_stopSpec {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (g₀ g₁ : CPolynomial F) (threshold : ℕ) (hdeg : g₁.degree < g₀.degree) (hthr : 1 ≤ threshold) (hthr' : ↑threshold ≤ g₀.degree) : BezoutStopSpecOf g₀ g₁ threshold (g₀.xgcd g₁ threshold)

xgcd's output satisfies the stop spec.