def Hex.DensePoly.reversePrefix {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] {n : Nat} (k : Nat) (a : TSeries R n) : DensePoly R

Reverse the first k coefficients of a represented series back into a normalized polynomial. The explicit bound is independent of any trailing zeros removed by polynomial normalization.

Equations

• Hex.DensePoly.reversePrefix k a = Hex.DensePoly.ofList (List.map (fun (i : Nat) => a.coeff (k - 1 - i)) (List.range k))

theorem Hex.DensePoly.coeff_reversePrefix {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] {n : Nat} (k : Nat) (a : TSeries R n) (i : Nat) : (reversePrefix k a).coeff i = if i < k then a.coeff (k - 1 - i) else 0

Coefficient law for fixed-bound reverse conversion.

theorem Hex.DensePoly.coeff_reversePrefix_mul {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] {n : Nat} (a : TSeries R n) (q : DensePoly R) (k t : Nat) (hk : k ≤ n) (ht : t < k) (hq : 0 < q.size) : (reversePrefix k a * q).coeff (k + q.size - 2 - t) = (q.reverseSeries n * a).coeff t

Reversing a k-coefficient series prefix converts its product's high coefficients into the corresponding low series convolution.

def Hex.DensePoly.quotientLength {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (p q : DensePoly R) : Nat

Number of quotient coefficients required for division of p by q. It is zero for the zero divisor and for a divisor larger than the dividend.

Equations

• p.quotientLength q = if (decide (q.size = 0) || decide (p.size < q.size)) = true then 0 else p.size - q.size + 1

theorem Hex.DensePoly.quotientLength_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (p q : DensePoly R) : p.quotientLength q = if (decide (q.size = 0) || decide (p.size < q.size)) = true then 0 else p.size - q.size + 1

Expansion of the quotient-length guard.

structure Hex.DensePoly.DivPlan (R : Type u) [DecidableEq R] [Lean.Grind.CommRing R] : Type u

A reusable divisor with a reciprocal cached to a fixed capacity.

• mul : MulPlan R

  Multiplication plan used by Newton division.

• divisor : DensePoly R

  Nonzero divisor represented by this plan.

• capacity : Nat

  Maximum quotient precision supported by the cached reciprocal.

• unitInv : R

  Inverse of the reversed divisor's constant coefficient.

• reciprocal : TSeries R self.capacity

  Cached reciprocal of the reversed divisor.

• divisor_ne : self.divisor ≠ 0

  The divisor is nonzero.

• unitInv_spec : 0 < self.capacity → (self.divisor.reverseSeries self.capacity).coeff 0 * self.unitInv = 1

  At positive precision, the supplied inverse is a unit witness.

• reciprocal_spec : self.reciprocal = (self.divisor.reverseSeries self.capacity).invOfUnit self.unitInv

  The cached reciprocal agrees with series inversion.

def Hex.DensePoly.DivPlan.ofMonic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (mul : MulPlan R) (q : DensePoly R) (hq : q.Monic) (hqne : q ≠ 0) (capacity : Nat) : DivPlan R

Build a cached plan for a nonzero monic divisor.

Equations

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

@[simp]

theorem Hex.DensePoly.DivPlan.divisor_ofMonic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (mul : MulPlan R) (q : DensePoly R) (hq : q.Monic) (hqne : q ≠ 0) (capacity : Nat) : (ofMonic mul q hq hqne capacity).divisor = q

A monic division plan retains its supplied divisor.

@[simp]

theorem Hex.DensePoly.DivPlan.mul_ofMonic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (mul : MulPlan R) (q : DensePoly R) (hq : q.Monic) (hqne : q ≠ 0) (capacity : Nat) : (ofMonic mul q hq hqne capacity).mul = mul

A monic division plan retains its supplied multiplication plan.

@[simp]

theorem Hex.DensePoly.DivPlan.capacity_ofMonic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (mul : MulPlan R) (q : DensePoly R) (hq : q.Monic) (hqne : q ≠ 0) (capacity : Nat) : (ofMonic mul q hq hqne capacity).capacity = capacity

A monic division plan retains its supplied capacity.

def Hex.DensePoly.DivPlan.ofNonzero {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (mul : MulPlan F) (q : DensePoly F) (hqne : q ≠ 0) (capacity : Nat) : DivPlan F

Build a cached plan for an arbitrary nonzero divisor over a field.

Equations

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

@[simp]

theorem Hex.DensePoly.DivPlan.divisor_ofNonzero {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (mul : MulPlan F) (q : DensePoly F) (hqne : q ≠ 0) (capacity : Nat) : (ofNonzero mul q hqne capacity).divisor = q

A field division plan retains its supplied divisor.

@[simp]

theorem Hex.DensePoly.DivPlan.mul_ofNonzero {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (mul : MulPlan F) (q : DensePoly F) (hqne : q ≠ 0) (capacity : Nat) : (ofNonzero mul q hqne capacity).mul = mul

A field division plan retains its supplied multiplication plan.

@[simp]

theorem Hex.DensePoly.DivPlan.capacity_ofNonzero {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (mul : MulPlan F) (q : DensePoly F) (hqne : q ≠ 0) (capacity : Nat) : (ofNonzero mul q hqne capacity).capacity = capacity

A field division plan retains its supplied capacity.

def Hex.DensePoly.DivPlan.quotient {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : DivPlan R) (p : DensePoly R) (_hcap : p.quotientLength plan.divisor ≤ plan.capacity) : DensePoly R

Quotient obtained from a cached reversed reciprocal.

Equations

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

theorem Hex.DensePoly.DivPlan.coeff_quotient_mul_high {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : DivPlan R) (p : DensePoly R) (hcap : p.quotientLength plan.divisor ≤ plan.capacity) (t : Nat) (ht : t < p.quotientLength plan.divisor) : (plan.quotient p hcap * plan.divisor).coeff (p.size - 1 - t) = p.coeff (p.size - 1 - t)

The reciprocal quotient cancels every coefficient in the high window of the dividend. The index t counts down from the leading coefficient.

theorem Hex.DensePoly.DivPlan.size_quotient_le {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : DivPlan R) (p : DensePoly R) (hcap : p.quotientLength plan.divisor ≤ plan.capacity) : (plan.quotient p hcap).size ≤ p.quotientLength plan.divisor

The normalized reciprocal quotient has no more than the requested number of coefficients.

theorem Hex.DensePoly.DivPlan.remainder_size_le {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : DivPlan R) (p : DensePoly R) (hcap : p.quotientLength plan.divisor ≤ plan.capacity) : (p - mulWith plan.mul (plan.quotient p hcap) plan.divisor).size ≤ plan.divisor.size - 1

Subtracting the reciprocal quotient product leaves fewer coefficients than the divisor. This is the executable division algorithm's termination law.

theorem Hex.DensePoly.DivPlan.remainder_degree_lt {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : DivPlan R) (p : DensePoly R) (hcap : p.quotientLength plan.divisor ≤ plan.capacity) (hdeg : 0 < plan.divisor.natDegree) : (p - mulWith plan.mul (plan.quotient p hcap) plan.divisor).natDegree < plan.divisor.natDegree

The cached division remainder has degree strictly below every positive-degree divisor.

def Hex.DensePoly.DivPlan.divMod {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : DivPlan R) (p : DensePoly R) (hcap : p.quotientLength plan.divisor ≤ plan.capacity) : DensePoly R × DensePoly R

Divide using a cached reciprocal. The proof ensures the cached precision covers the requested quotient; it is erased from executable code.

Equations

• plan.divMod p hcap = (plan.quotient p hcap, p - Hex.DensePoly.mulWith plan.mul (plan.quotient p hcap) plan.divisor)

theorem Hex.DensePoly.DivPlan.divMod_eq_divMod {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] [Div R] (plan : DivPlan R) (p : DensePoly R) (hcap : p.quotientLength plan.divisor ≤ plan.capacity) (hcancel : ∀ (a : R), a - a / plan.divisor.leadingCoeff * plan.divisor.leadingCoeff = 0) (hexact : ∀ (a : R), a * plan.divisor.leadingCoeff / plan.divisor.leadingCoeff = a) (h_top_ne : ∀ (a : R), a ≠ 0 → a * plan.divisor.leadingCoeff ≠ 0) : plan.divMod p hcap = p.divMod plan.divisor

Cached reciprocal division agrees with the established long-division result whenever coefficient division satisfies the laws needed by that result. The size-one divisor case is handled as an exact product rather than being hidden by the default-zero degree convention.

def Hex.DensePoly.DivPlan.mod {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : DivPlan R) (p : DensePoly R) (hcap : p.quotientLength plan.divisor ≤ plan.capacity) : DensePoly R

Remainder-only cached division.

Equations

• plan.mod p hcap = (plan.divMod p hcap).snd

theorem Hex.DensePoly.DivPlan.mod_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : DivPlan R) (p : DensePoly R) (hcap : p.quotientLength plan.divisor ≤ plan.capacity) : plan.mod p hcap = p - mulWith plan.mul (plan.quotient p hcap) plan.divisor

Reconstruction form of the cached remainder.

theorem Hex.DensePoly.DivPlan.size_mod_le {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : DivPlan R) (p : DensePoly R) (hcap : p.quotientLength plan.divisor ≤ plan.capacity) : (plan.mod p hcap).size ≤ plan.divisor.size - 1

A cached remainder has fewer coefficients than its divisor.

theorem Hex.DensePoly.DivPlan.eval_mod {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : DivPlan R) (p : DensePoly R) (hcap : p.quotientLength plan.divisor ≤ plan.capacity) (a : R) (hzero : plan.divisor.eval a = 0) : (plan.mod p hcap).eval a = p.eval a

Taking a cached remainder preserves evaluation at every zero of the divisor.

def Hex.DensePoly.divModMonicWith {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (mul : MulPlan R) (p q : DensePoly R) (hq : q.Monic) : DensePoly R × DensePoly R

One-shot reciprocal division by a monic polynomial.

Equations

• Hex.DensePoly.divModMonicWith mul p q hq = if hqne : q = 0 then (0, p) else let k := p.quotientLength q; let plan := Hex.DensePoly.DivPlan.ofMonic mul q hq hqne k; plan.divMod p ⋯

theorem Hex.DensePoly.divModMonicWith_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (mul : MulPlan R) (p q : DensePoly R) (hq : q.Monic) : divModMonicWith mul p q hq = p.divModMonic q hq

One-shot monic reciprocal division agrees with the existing specialized monic long-division operation.

def Hex.DensePoly.divModNewton {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (mul : MulPlan F) (p q : DensePoly F) : DensePoly F × DensePoly F

One-shot reciprocal division over a field.

Equations

• Hex.DensePoly.divModNewton mul p q = if hqne : q = 0 then (0, p) else let k := p.quotientLength q; let plan := Hex.DensePoly.DivPlan.ofNonzero mul q hqne k; plan.divMod p ⋯

theorem Hex.DensePoly.divModNewton_eq {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (mul : MulPlan F) (p q : DensePoly F) : divModNewton mul p q = p.divMod q

One-shot field reciprocal division is extensionally the existing verified long-division operation.

theorem Hex.DensePoly.divModNewton_size_lt {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (p q : DensePoly F) (hq : q ≠ 0) : (divModNewton plan p q).snd.size < q.size

Fast field division leaves fewer stored coefficients than its nonzero divisor.

def Hex.DensePoly.divModWith {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (mul : MulPlan F) (p q : DensePoly F) : DensePoly F × DensePoly F

Kernel-visible reference division. Compiled code uses the proved short-operand/Newton dispatch with the supplied multiplication plan.

Equations

• Hex.DensePoly.divModWith mul p q = p.divMod q

theorem Hex.DensePoly.divModWith_eq {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (mul : MulPlan F) (p q : DensePoly F) : divModWith mul p q = p.divMod q

Planned division has the exact reference quotient and remainder.

theorem Hex.DensePoly.divModWith_size_lt {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) (p q : DensePoly F) (hq : q ≠ 0) : (divModWith plan p q).snd.size < q.size

Planned division retains the strict reference remainder bound.

def Hex.DensePoly.divisionCutoff : Nat

Maximum short operand length for direct one-shot polynomial division.

Equations

• Hex.DensePoly.divisionCutoff = 8

def Hex.DensePoly.divModWithImpl {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (mul : MulPlan F) (p q : DensePoly F) : DensePoly F × DensePoly F

Short divisors and short quotients use array long division. Its work is linear in the long operand when either length is bounded; building a full Newton reciprocal in that regime would introduce unnecessary dense products.

Equations

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

@[csimp]

theorem Hex.DensePoly.divModWith_csimp : @divModWith = @divModWithImpl

The short-operand division dispatch preserves both quotient and remainder.