def Hex.DensePoly.leadingCoeff {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : R

The leading coefficient, or 0 for the zero polynomial.

Equations

• p.leadingCoeff = p.coeffs.getD (p.coeffs.size - 1) Zero.zero

@[simp]

theorem Hex.DensePoly.leadingCoeff_zero {R : Type u} [Zero R] [DecidableEq R] : leadingCoeff 0 = 0

The zero polynomial has leading coefficient 0. Registered as a simp normal form so callers reasoning about leadingCoeff discharge the zero case automatically.

@[instance_reducible]

instance Hex.DensePoly.instOne {R : Type u} [Zero R] [DecidableEq R] [One R] : One (DensePoly R)

The constant polynomial 1.

Equations

• Hex.DensePoly.instOne = { one := Hex.DensePoly.C 1 }

@[simp]

theorem Hex.DensePoly.leadingCoeff_C {R : Type u} [Zero R] [DecidableEq R] (c : R) : (C c).leadingCoeff = c

The leading coefficient of the constant polynomial C c is c itself, covering both c = 0 (the empty backing array) and c ≠ 0. The simp form lets callers read the leading coefficient off any constant.

@[simp]

theorem Hex.DensePoly.leadingCoeff_one {R : Type u} [Zero R] [DecidableEq R] [One R] : leadingCoeff 1 = 1

The constant polynomial 1 has leading coefficient 1, hence is monic. Specialises leadingCoeff_C and feeds the monicity facts about 1 that the division and gcd routines rely on.

theorem Hex.DensePoly.size_one {R : Type u} [Zero R] [DecidableEq R] [One R] (hone : 1 ≠ 0) : size 1 = 1

The constant polynomial 1 stores one coefficient when the coefficient ring's 1 is nonzero.

def Hex.DensePoly.Monic {R : Type u} [Zero R] [DecidableEq R] [One R] (p : DensePoly R) : Prop

A polynomial is monic when its leading coefficient is 1.

Equations

• p.Monic = (p.leadingCoeff = 1)

theorem Hex.DensePoly.leadingCoeff_eq_one_of_monic {R : Type u} [Zero R] [DecidableEq R] [One R] {p : DensePoly R} (hp : p.Monic) : p.leadingCoeff = 1

A monic polynomial has leading coefficient 1. Forwarding lemma so callers do not need to unfold Monic.

theorem Hex.DensePoly.monic_iff_leadingCoeff_eq_one {R : Type u} [Zero R] [DecidableEq R] [One R] {p : DensePoly R} : p.Monic ↔ p.leadingCoeff = 1

Characterization of Hex.DensePoly.Monic by the leading coefficient equation.

theorem Hex.DensePoly.leadingCoeff_eq_coeff_last {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) (_hpos : 0 < p.size) : p.leadingCoeff = p.coeff (p.size - 1)

For a nonzero normalized dense polynomial, leadingCoeff is the coefficient at the last stored index.

theorem Hex.DensePoly.leadingCoeff_ne_zero_of_pos_size {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) (hpos : 0 < p.size) : p.leadingCoeff ≠ Zero.zero

The leading coefficient of a nonzero normalized dense polynomial is nonzero.

def Hex.DensePoly.arrayDegreeAux {R : Type u} [Zero R] [DecidableEq R] (coeffs : Array R) : Nat → Option Nat

arrayDegreeAux coeffs fuel scans indices below fuel downward and returns the greatest index whose coefficient is nonzero, or none if every coefficient below fuel is zero.

Equations

• Hex.DensePoly.arrayDegreeAux coeffs 0 = none
• Hex.DensePoly.arrayDegreeAux coeffs fuel.succ = if coeffs.getD fuel Zero.zero = Zero.zero then Hex.DensePoly.arrayDegreeAux coeffs fuel else some fuel

def Hex.DensePoly.arrayDegree? {R : Type u} [Zero R] [DecidableEq R] (coeffs : Array R) : Option Nat

arrayDegree? coeffs is the highest index of a nonzero coefficient of coeffs, or none when every coefficient is zero, computed by scanning from coeffs.size downward.

Equations

• Hex.DensePoly.arrayDegree? coeffs = Hex.DensePoly.arrayDegreeAux coeffs coeffs.size

def Hex.DensePoly.subtractScaledShiftStep {R : Type u} [Zero R] [Sub R] [Mul R] (q : Array R) (shift : Nat) (coeff : R) (next : Array R) (j : Nat) : Array R

One coefficient of a long-division elimination step: subtract coeff * q[j] from position shift + j of next, the inner action folded by subtractScaledShift to wipe out the leading term of the current remainder.

Equations

• Hex.DensePoly.subtractScaledShiftStep q shift coeff next j = next.set! (shift + j) (next.getD (shift + j) Zero.zero - coeff * q.getD j Zero.zero)

def Hex.DensePoly.subtractScaledShift {R : Type u} [Zero R] [Sub R] [Mul R] (rem q : Array R) (shift : Nat) (coeff : R) : Array R

Subtract coeff times the divisor q shifted up by shift positions from the remainder rem, i.e. one full long-division step rem - coeff * xˢʰⁱᶠᵗ * q, realised by folding subtractScaledShiftStep over every index of q.

Equations

• Hex.DensePoly.subtractScaledShift rem q shift coeff = List.foldl (Hex.DensePoly.subtractScaledShiftStep q shift coeff) rem (List.range q.size)

def Hex.DensePoly.divModArrayAuxImpl {R : Type u} [Zero R] [DecidableEq R] [Sub R] [Mul R] (q : Array R) (qDegree : Nat) (scaleLead : R → R) (fuel : Nat) (quot rem : Array R) : Array R × Array R

Runtime implementation of divModArrayAux. Seeds the scan ceiling at rem.size, so the first iteration is identical to the reference's arrayDegree? rem; thereafter the ceiling tracks the working degree (see divModArrayAuxImplGo).

Equations

• Hex.DensePoly.divModArrayAuxImpl q qDegree scaleLead fuel quot rem = Hex.DensePoly.divModArrayAuxImplGo✝ q qDegree scaleLead fuel rem.size quot rem

noncomputable def Hex.DensePoly.divModArrayAux {R : Type u} [Zero R] [DecidableEq R] [Sub R] [Mul R] (q : Array R) (qDegree : Nat) (scaleLead : R → R) (fuel : Nat) (quot rem : Array R) : Array R × Array R

The fuel-bounded long-division loop: while the remainder's degree rd is at least the divisor degree qDegree, pick the quotient coefficient scaleLead (rem[rd]), record it in quot, eliminate the leading term via subtractScaledShift, and recurse, returning the final (quotient, remainder) pair. The compiled runtime uses the value-equal divModArrayAuxImpl (proved by divModArrayAux_eq_impl, registered @[csimp]), which tracks the working degree instead of rescanning.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.divModArrayAux q qDegree scaleLead 0 quot rem = (quot, rem)

@[csimp]

theorem Hex.DensePoly.divModArrayAux_eq_impl : @divModArrayAux = @divModArrayAuxImpl

Register the value-equal divModArrayAuxImpl as the compiled implementation of divModArrayAux. Unlike @[implemented_by], the @[csimp] swap is backed by the proof divModArrayAuxImpl_eq, so the runtime loop is verified equal to the specification.

def Hex.DensePoly.divModArray {R : Type u} [Zero R] [DecidableEq R] [Sub R] [Mul R] (p q : DensePoly R) (scaleLead : R → R) : DensePoly R × DensePoly R

Array-backed long division of dense polynomial p by q: returns (0, p) when q is zero, otherwise seeds a zero quotient and runs divModArrayAux with p.size fuel, packaging the resulting coefficient arrays back as DensePoly quotient and remainder.

Equations

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

def Hex.DensePoly.modArray {R : Type u} [Zero R] [DecidableEq R] [Sub R] [Mul R] (p q : DensePoly R) (scaleLead : R → R) : DensePoly R

Remainder-only array-backed long division. This mirrors divModArray but does not allocate the quotient array or update it during elimination.

Equations

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

theorem Hex.DensePoly.modArray_eq_divModArray_snd {R : Type u} [Zero R] [DecidableEq R] [Sub R] [Mul R] (p q : DensePoly R) (scaleLead : R → R) : p.modArray q scaleLead = (p.divModArray q scaleLead).snd

The remainder-only array implementation equals the remainder component of the verified quotient/remainder implementation.

theorem Hex.DensePoly.divModArray_scaleLead_congr {R : Type u} [Zero R] [DecidableEq R] [Sub R] [Mul R] (p q : DensePoly R) {scaleLead₁ scaleLead₂ : R → R} (hscale : ∀ (a : R), scaleLead₁ a = scaleLead₂ a) : p.divModArray q scaleLead₁ = p.divModArray q scaleLead₂

The array-backed long division result depends only on the pointwise values of the leading-coefficient scaling function.

theorem Hex.DensePoly.divModArray_remainder_degree_lt_of_pos_degree {R : Type u} [Zero R] [DecidableEq R] [Sub R] [Mul R] (p q : DensePoly R) (scaleLead : R → R) (hdegree : 0 < q.degree?.getD 0) (hcancel : ∀ (a : R), a - scaleLead a * q.leadingCoeff = Zero.zero) : (p.divModArray q scaleLead).snd.degree?.getD 0 < q.degree?.getD 0

For a positive-degree divisor and any scaling function that cancels the leading coefficient, the array-backed long-division loop returns a remainder strictly smaller in degree than the divisor.

def Hex.DensePoly.divModMonic {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (p q : DensePoly R) (_hmonic : q.Monic) : DensePoly R × DensePoly R

Divide by a monic polynomial. The remainder has degree below the divisor whenever the fuel is sufficient, which is the case for normalized dense polynomials.

Equations

• p.divModMonic q _hmonic = p.divModArray q id

def Hex.DensePoly.divMod {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) : DensePoly R × DensePoly R

Polynomial division with remainder over a field.

Equations

• p.divMod q = if p.degree?.getD 0 < q.degree?.getD 0 then (0, p) else p.divModArray q fun (coeff : R) => coeff / q.leadingCoeff

theorem Hex.DensePoly.divMod_remainder_degree_lt_of_pos_degree_of_cancel {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) (hdegree : 0 < q.degree?.getD 0) (hcancel : ∀ (a : R), a - a / q.leadingCoeff * q.leadingCoeff = Zero.zero) : (p.divMod q).snd.degree?.getD 0 < q.degree?.getD 0

For a positive-degree divisor, the field-style divMod returns a remainder strictly smaller in degree, given an explicit cancellation hypothesis for the coefficient ring. Concrete coefficient libraries discharge hcancel once and re-export this as the unconditional divMod_remainder_degree_lt_of_pos_degree via the DivModLaws instance.

theorem Hex.DensePoly.divMod_remainder_eq_zero_of_degree_zero_of_cancel {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) (hqsize : q.size = 1) (hcancel : ∀ (a : R), a - a / q.leadingCoeff * q.leadingCoeff = Zero.zero) : (p.divMod q).snd = 0

For a size-one (degree-zero, nonzero) divisor, the field-style divMod returns zero remainder, given an explicit cancellation hypothesis for the coefficient ring. Concrete coefficient libraries discharge hcancel once and re-export the result via the DivModLaws instance.

theorem Hex.DensePoly.divMod_remainder_eq_self_of_size_zero {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) (hqsize : q.size = 0) : (p.divMod q).snd = p

Dividing by a size-zero (zero) polynomial returns the dividend as remainder. The companion divMod_eq_zero_self_of_size_zero gives the full quotient-and-remainder pair.

theorem Hex.DensePoly.divMod_eq_zero_self_of_size_zero {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) (hqsize : q.size = 0) : p.divMod q = (0, p)

Dividing by a size-zero dense polynomial returns zero quotient and the original dividend as remainder.

def Hex.DensePoly.div {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) : DensePoly R

Quotient from polynomial long division over a field.

Equations

• p.div q = (p.divMod q).fst

def Hex.DensePoly.mod {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) : DensePoly R

Remainder from polynomial long division over a field.

Equations

• p.mod q = (p.divMod q).snd

def Hex.DensePoly.modImpl {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) : DensePoly R

Compiled remainder implementation that skips construction of the unused quotient. The public specification remains mod; the plain GCD's @[csimp] implementation uses this value-equal worker.

Equations

• p.modImpl q = if p.degree?.getD 0 < q.degree?.getD 0 then p else have qLead := q.leadingCoeff; p.modArray q fun (coeff : R) => coeff / qLead

def Hex.DensePoly.modByMonic {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (p q : DensePoly R) (hmonic : q.Monic) : DensePoly R

Remainder from long division by a monic polynomial over a commutative ring.

Equations

• p.modByMonic q hmonic = (p.divModMonic q hmonic).snd

@[instance_reducible]

instance Hex.DensePoly.instDivOfOneOfAddOfSubOfMul {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] : Div (DensePoly R)

The / notation on dense polynomials selects to DensePoly.div.

Equations

• Hex.DensePoly.instDivOfOneOfAddOfSubOfMul = { div := Hex.DensePoly.div }

@[instance_reducible]

instance Hex.DensePoly.instModOfOneOfAddOfSubOfMulOfDiv {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] : Mod (DensePoly R)

The % notation on dense polynomials selects to DensePoly.mod.

Equations

• Hex.DensePoly.instModOfOneOfAddOfSubOfMulOfDiv = { mod := Hex.DensePoly.mod }

@[instance_reducible]

instance Hex.DensePoly.instDvdOfAddOfMul {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] : Dvd (DensePoly R)

Commutative-ring divisibility for dense polynomials.

Equations

• Hex.DensePoly.instDvdOfAddOfMul = { dvd := fun (p q : Hex.DensePoly R) => ∃ (r : Hex.DensePoly R), q = p * r }

structure Hex.DensePoly.XGCDResult (R : Type u) [Zero R] [DecidableEq R] : Type u

Result package for polynomial extended gcd.

• gcd : DensePoly R

  Greatest common divisor returned by the extended Euclidean algorithm.

• left : DensePoly R

  Bezout coefficient multiplying the left input.

• right : DensePoly R

  Bezout coefficient multiplying the right input.

def Hex.DensePoly.xgcdAux {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (r₀ s₀ t₀ r₁ s₁ t₁ : DensePoly R) (fuel : Nat) : XGCDResult R

Tail-recursive extended Euclidean algorithm.

Equations

• One or more equations did not get rendered due to their size.
• r₀.xgcdAux s₀ t₀ r₁ s₁ t₁ 0 = { gcd := r₀, left := s₀, right := t₀ }

def Hex.DensePoly.xgcd {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) : XGCDResult R

Extended gcd over a field, returning the gcd together with Bezout coefficients.

Equations

• p.xgcd q = p.xgcdAux 1 0 q 0 1 (p.size + q.size + 1)

structure Hex.DensePoly.XGCDLeftResult (R : Type u) [Zero R] [DecidableEq R] : Type u

Result package for the one-sided extended Euclidean algorithm.

• gcd : DensePoly R

  Greatest common divisor returned by the Euclidean algorithm.

• left : DensePoly R

  Bezout coefficient multiplying the left input.

def Hex.DensePoly.xgcdLeftAux {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (r₀ s₀ r₁ s₁ : DensePoly R) (fuel : Nat) : XGCDLeftResult R

Tail-recursive extended Euclidean algorithm tracking only the coefficient of the left input. This avoids the second polynomial multiplication at every step when a consumer needs one inverse coefficient rather than both.

Equations

• r₀.xgcdLeftAux s₀ r₁ s₁ 0 = { gcd := r₀, left := s₀ }
• r₀.xgcdLeftAux s₀ r₁ s₁ fuel_1.succ = if _hr : r₁.isZero = true then { gcd := r₀, left := s₀ } else have qr := r₀.divMod r₁; r₁.xgcdLeftAux s₁ qr.snd (s₀ - qr.fst * s₁) fuel_1

def Hex.DensePoly.xgcdLeft {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) : XGCDLeftResult R

One-sided extended gcd, returning the gcd and only the Bezout coefficient multiplying the left input.

Equations

• p.xgcdLeft q = p.xgcdLeftAux 1 q 0 (p.size + q.size + 1)

theorem Hex.DensePoly.xgcdLeftAux_gcd_eq {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (r₀ s₀ t₀ r₁ s₁ t₁ : DensePoly R) (fuel : Nat) : (r₀.xgcdLeftAux s₀ r₁ s₁ fuel).gcd = (r₀.xgcdAux s₀ t₀ r₁ s₁ t₁ fuel).gcd

The one-sided and full extended algorithms return the same gcd.

theorem Hex.DensePoly.xgcdLeftAux_left_eq {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (r₀ s₀ t₀ r₁ s₁ t₁ : DensePoly R) (fuel : Nat) : (r₀.xgcdLeftAux s₀ r₁ s₁ fuel).left = (r₀.xgcdAux s₀ t₀ r₁ s₁ t₁ fuel).left

The one-sided algorithm returns the same left Bezout coefficient as the full extended algorithm.

theorem Hex.DensePoly.xgcdLeft_gcd_eq_xgcd {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) : (p.xgcdLeft q).gcd = (p.xgcd q).gcd

xgcdLeft returns the same gcd as xgcd.

theorem Hex.DensePoly.xgcdLeft_left_eq_xgcd {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) : (p.xgcdLeft q).left = (p.xgcd q).left

xgcdLeft returns the same left Bezout coefficient as xgcd.

def Hex.DensePoly.gcdAux {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (r₀ r₁ : DensePoly R) (fuel : Nat) : DensePoly R

Tail-recursive Euclidean gcd tracking only the remainder sequence, without the Bezout coefficients. xgcd/xgcdAux carry the Bezout accumulators s, t and update them with a polynomial multiplication (q * s₁, q * t₁) at every step on polynomials whose degree grows through the run; that is O(deg³) work and pure waste when only the gcd value is wanted (the common case: the square-free / separability test gcd(f, f') = 1). gcdAux keeps only the remainders and is O(deg²).

Equations

• r₀.gcdAux r₁ 0 = r₀
• r₀.gcdAux r₁ fuel_1.succ = if _hr : r₁.isZero = true then r₀ else r₁.gcdAux (r₀.divMod r₁).snd fuel_1

def Hex.DensePoly.gcdAuxImpl {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (r₀ r₁ : DensePoly R) (fuel : Nat) : DensePoly R

Runtime GCD loop using remainder-only long division. Its public specification remains gcdAux; the equality below supplies a proof-backed compiler replacement.

Equations

• r₀.gcdAuxImpl r₁ 0 = r₀
• r₀.gcdAuxImpl r₁ fuel_1.succ = if r₁.isZero = true then r₀ else r₁.gcdAuxImpl (r₀.modImpl r₁) fuel_1

@[csimp]

theorem Hex.DensePoly.gcdAux_eq_impl : @gcdAux = @gcdAuxImpl

Proof-backed compiled implementation of plain polynomial GCD that never constructs the discarded Euclidean quotient arrays.

theorem Hex.DensePoly.gcdAux_eq_xgcdAux_gcd {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (r₀ s₀ t₀ r₁ s₁ t₁ : DensePoly R) (fuel : Nat) : r₀.gcdAux r₁ fuel = (r₀.xgcdAux s₀ t₀ r₁ s₁ t₁ fuel).gcd

The plain remainder gcd agrees with the gcd component of the extended algorithm: XGCDResult.gcd never depends on the Bezout accumulators.

def Hex.DensePoly.gcd {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) : DensePoly R

Polynomial gcd over a field. Computed by the plain remainder sequence Hex.DensePoly.gcdAux, not the extended algorithm: the gcd value is independent of the Bezout coefficients, and computing them costs an extra polynomial multiplication per step (O(deg³) vs O(deg²)). Hex.DensePoly.xgcd stays available for callers that genuinely need Bezout coefficients.

Equations

• p.gcd q = p.gcdAux q (p.size + q.size + 1)

theorem Hex.DensePoly.gcd_eq_xgcd_gcd {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) : p.gcd q = (p.xgcd q).gcd

gcd equals the gcd component of xgcd; lets lemmas proved against the extended algorithm transfer to the plain gcd.

theorem Hex.DensePoly.xgcd_gcd_eq_gcd {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) : (p.xgcd q).gcd = p.gcd q

The gcd component returned by xgcd is the executable gcd.

@[simp]

theorem Hex.DensePoly.gcd_zero_zero {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] : gcd 0 0 = 0

The executable gcd of two zero dense polynomials is zero.

class Hex.DensePoly.DivModLaws (R : Type u) [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] : Prop

Law package for the executable dense-polynomial division operations.

The algorithms remain available for any coefficient type with the required operations, but theorems that use long-division invariants should require this class rather than claiming those invariants for arbitrary, potentially unlawful Div and Sub instances.

• divMod_spec (p q : DensePoly R) : let qr := p.divMod q; qr.fst * q + qr.snd = p
• divMod_remainder_degree_lt_of_pos_degree (p q : DensePoly R) : 0 < q.degree?.getD 0 → (p.divMod q).snd.degree?.getD 0 < q.degree?.getD 0
• divModMonic_eq_divMod_of_monic (p q : DensePoly R) (hq : q.Monic) : p.divModMonic q hq = p.divMod q
• mod_self_eq_zero (p : DensePoly R) : p % p = 0
• mod_eq_zero_of_dvd (p q : DensePoly R) : q ∣ p → p % q = 0
• mod_mod_of_not_pos_degree (p q : DensePoly R) : ¬0 < q.degree?.getD 0 → p % q % q = p % q
• mod_eq_mod_of_congr (p q m : DensePoly R) : m ∣ p - q → p % m = q % m
• mod_add_mod (p q m : DensePoly R) : (p + q) % m = (p % m + q % m) % m
• mod_mul_mod (p q m : DensePoly R) : p * q % m = p % m * (q % m) % m

class Hex.DensePoly.GcdLaws (R : Type u) [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] : Prop

Law package for the executable dense-polynomial gcd operations.

The generic algorithms are executable for any coefficient type with the required operations, but Euclidean gcd correctness is only true for lawful coefficient/division structures. Concrete coefficient libraries provide this package once they have proved the algorithmic invariants.

• gcd_dvd_left (p q : DensePoly R) : p.gcd q ∣ p
• gcd_dvd_right (p q : DensePoly R) : p.gcd q ∣ q
• dvd_gcd (d p q : DensePoly R) : d ∣ p → d ∣ q → d ∣ p.gcd q
• xgcd_bezout (p q : DensePoly R) : let r := p.xgcd q; r.left * p + r.right * q = r.gcd

theorem Hex.DensePoly.divMod_spec {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] [DivModLaws R] (p q : DensePoly R) : have qr := p.divMod q; qr.fst * q + qr.snd = p

The field-style quotient and remainder reconstruct the dividend.

theorem Hex.DensePoly.gcd_dvd_left {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] [GcdLaws R] (p q : DensePoly R) : p.gcd q ∣ p

The polynomial gcd divides the left argument.

theorem Hex.DensePoly.gcd_dvd_right {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] [GcdLaws R] (p q : DensePoly R) : p.gcd q ∣ q

The polynomial gcd divides the right argument.

theorem Hex.DensePoly.dvd_gcd {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] [GcdLaws R] (d p q : DensePoly R) : d ∣ p → d ∣ q → d ∣ p.gcd q

Every common divisor of p and q divides gcd p q.

theorem Hex.DensePoly.xgcd_bezout {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] [GcdLaws R] (p q : DensePoly R) : have r := p.xgcd q; r.left * p + r.right * q = r.gcd

Bezout identity: the extended-gcd coefficients reconstruct the gcd as left * p + right * q.

theorem Hex.DensePoly.modByMonic_eq_divModMonic {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (p q : DensePoly R) (hq : q.Monic) : p.modByMonic q hq = (p.divModMonic q hq).snd

modByMonic is definitionally the second component of divModMonic.

theorem Hex.DensePoly.modByMonic_zero {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] (q : DensePoly R) (hq : q.Monic) : modByMonic 0 q hq = 0

Zero has zero remainder under monic division.

theorem Hex.DensePoly.mod_eq_divMod {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) : p % q = (p.divMod q).snd

The % notation unfolds to the second component of divMod.

@[simp]

theorem Hex.DensePoly.zero_mod_eq_zero {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] (m : DensePoly S) : 0 % m = 0

Zero has zero remainder for the executable division algorithm.

theorem Hex.DensePoly.divMod_eq_zero_self_of_degree_lt {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) : p.degree?.getD 0 < q.degree?.getD 0 → p.divMod q = (0, p)

If the dividend already has degree strictly below the divisor, divMod short-circuits to (0, p) without entering the long-division loop.

theorem Hex.DensePoly.gcd_eq_aux_mod {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (f g : DensePoly R) (hf : f.isZero = false) (hsize : f.size < g.size) : f.gcd g = f.gcdAux (g % f) (f.size + g.size - 1)

When the nonzero left input is strictly smaller than the right input, resume gcd after its first two Euclidean steps. The explicit fuel is the fuel of the original execution after those steps, so this preserves its exact unnormalised remainder representative rather than merely an associate.

theorem Hex.DensePoly.divModArray_eq_zero_self_of_degree_lt {R : Type u} [Zero R] [DecidableEq R] [Sub R] [Mul R] (p q : DensePoly R) (scaleLead : R → R) (hdeg : p.degree?.getD 0 < q.degree?.getD 0) : p.divModArray q scaleLead = (0, p)

The array-backed long-division loop also short-circuits to (0, p) when the dividend already has degree below the divisor.

theorem Hex.DensePoly.divModMonic_eq_divMod_of_monic_of_scale {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) (hq : q.Monic) (hnot_lt : ¬p.degree?.getD 0 < q.degree?.getD 0) (hscale : ∀ (a : R), a / q.leadingCoeff = a) : p.divModMonic q hq = p.divMod q

If field-style coefficient division agrees pointwise with the monic scaling function, then the executable monic division path agrees with the general divMod path away from the early degree shortcut.

theorem Hex.DensePoly.divMod_remainder_degree_lt_of_pos_degree {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] [DivModLaws R] (p q : DensePoly R) : 0 < q.degree?.getD 0 → (p.divMod q).snd.degree?.getD 0 < q.degree?.getD 0

Division invariant: for positive-degree divisors, divMod returns a remainder whose degree is strictly smaller than the divisor degree.

theorem Hex.DensePoly.divModMonic_eq_divMod_of_monic {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] [DivModLaws R] (p q : DensePoly R) (hq : q.Monic) : p.divModMonic q hq = p.divMod q

Monic division agrees with field-style division when the divisor is monic. This is the implementation invariant relating the specialized divModMonic path to divMod.

theorem Hex.DensePoly.mod_eq_self_of_degree_lt {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (p q : DensePoly R) : p.degree?.getD 0 < q.degree?.getD 0 → p % q = p

A polynomial whose degree is already below the divisor is its own remainder.

theorem Hex.DensePoly.mod_mod_of_not_pos_degree {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] [DivModLaws R] (p q : DensePoly R) : ¬0 < q.degree?.getD 0 → p % q % q = p % q

Constant-degree divisors are an idempotent edge case for %.

theorem Hex.DensePoly.mod_degree_lt_of_pos_degree {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] [DivModLaws R] (p q : DensePoly R) : 0 < q.degree?.getD 0 → (p % q).degree?.getD 0 < q.degree?.getD 0

The computed remainder has degree below a positive-degree divisor.

theorem Hex.DensePoly.div_mul_add_mod {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] [DivModLaws R] (p q : DensePoly R) : p / q * q + p % q = p

Euclidean division identity: (p / q) * q + (p % q) = p.

@[simp]

theorem Hex.DensePoly.mod_eq_zero_of_dvd {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] [DivModLaws R] (p q : DensePoly R) : q ∣ p → p % q = 0

If q ∣ p, then p % q = 0.

theorem Hex.DensePoly.modByMonic_eq_mod {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] [DivModLaws R] (p q : DensePoly R) (hq : q.Monic) : p.modByMonic q hq = p % q

Monic division and the generic % notation agree when the divisor is monic.

@[simp]

theorem Hex.DensePoly.mod_mod {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] [DivModLaws R] (p q : DensePoly R) : p % q % q = p % q

The remainder modulo q is idempotent under % q.