theorem Hex.DensePoly.diagonal_eq_degree_bound {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (p q : DensePoly R) (n : Nat) : List.foldl (fun (acc : R) (i : Nat) => acc + p.diagonalMulCoeffTerm q n i) 0 (List.range p.size) = List.foldl (fun (acc : R) (i : Nat) => acc + p.diagonalMulCoeffTerm q n i) 0 (List.range (n + 1))

A polynomial multiplication diagonal may always be normalized to the canonical degree-sized range, independently of the left operand's support.

theorem Hex.DensePoly.coeff_polyOfSeries_mul {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] {n : Nat} (a b : TSeries R n) (i : Nat) (hi : i < n) : (polyOfSeries a * polyOfSeries b).coeff i = (a * b).coeff i

Polynomial conversion preserves every represented product coefficient.

def Hex.DensePoly.seriesMulUpTo {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) {n : Nat} (m : Nat) (a b : TSeries R n) : TSeries R n

Multiply two series through degree m - 1 with a polynomial multiplication plan.

Equations

• Hex.DensePoly.seriesMulUpTo plan m a b = Hex.TSeries.ofFn fun (i : Nat) => (Hex.DensePoly.mulLow plan m (Hex.DensePoly.polyOfSeries a) (Hex.DensePoly.polyOfSeries b)).coeff i

theorem Hex.DensePoly.seriesMulUpTo_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) {n : Nat} (m : Nat) (a b : TSeries R n) : seriesMulUpTo plan m a b = TSeries.mulUpTo m a b

Planned bounded series multiplication has exactly the established TSeries.mulUpTo semantics.

def Hex.DensePoly.reciprocalStep {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) {n : Nat} (g h : TSeries R n) (m : Nat) : TSeries R n

One Newton reciprocal update whose two bounded products both use the supplied multiplication plan.

Equations

• Hex.DensePoly.reciprocalStep plan g h m = Hex.DensePoly.seriesMulUpTo plan m h (Hex.TSeries.C (1 + 1) - Hex.DensePoly.seriesMulUpTo plan m g h)

theorem Hex.DensePoly.reciprocalStep_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) {n : Nat} (g h : TSeries R n) (m : Nat) : reciprocalStep plan g h m = g.invStep h m

A planned Newton update agrees exactly with the reference series update.

def Hex.DensePoly.reciprocalWith {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) {n : Nat} (g : TSeries R n) (u : R) : TSeries R n

Newton reciprocal at the full represented precision. Each doubling step uses plan.slice 0 k; no schoolbook TSeries product is executed by this definition.

Equations

• Hex.DensePoly.reciprocalWith plan g u = Hex.TSeries.newton (Hex.DensePoly.reciprocalStep plan g) (Hex.TSeries.C u) (Hex.TSeries.steps n)

theorem Hex.DensePoly.reciprocalWith_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) {n : Nat} (g : TSeries R n) (u : R) : reciprocalWith plan g u = g.invOfUnit u

The plan-driven reciprocal has the established truncated-series semantics. The inverse-witness hypothesis is intentionally not needed for algorithmic agreement; it is needed by the defining inverse equation below.

theorem Hex.DensePoly.reciprocalWith_mul {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) {n : Nat} (g : TSeries R n) (u : R) (hu : g.coeff 0 * u = 1) : g * reciprocalWith plan g u = 1

A planned reciprocal satisfies the multiplicative inverse equation when the supplied constant coefficient really is an inverse.