theorem Hex.DensePoly.size_le_of_coeff_zero_above {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] {p : DensePoly R} {n : Nat} (hzero : ∀ (i : Nat), n ≤ i → p.coeff i = 0) : p.size ≤ n

A polynomial whose coefficients vanish from n onward has size at most n.

theorem Hex.DensePoly.size_add_le_max {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (p q : DensePoly R) : (p + q).size ≤ max p.size q.size

Addition cannot increase size beyond the larger operand.

theorem Hex.DensePoly.size_sub_le_max {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (p q : DensePoly R) : (p - q).size ≤ max p.size q.size

Subtraction cannot increase size beyond the larger operand.

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

A proof-carrying implementation of full, square, and clipped dense polynomial multiplication. slice lo len a b stores coefficients beginning at degree lo, shifted down to degree zero.

• mul : DensePoly R → DensePoly R → DensePoly R

  A complete normalized product.

• square : DensePoly R → DensePoly R

  A specialized square.

• slice : Nat → Nat → DensePoly R → DensePoly R → DensePoly R

  len coefficients beginning at product degree lo, shifted down.

• mul_eq (a b : DensePoly R) : self.mul a b = a * b

  Full multiplication agrees with the reference product.

• square_eq (a : DensePoly R) : self.square a = a * a

  Squaring agrees with the reference product.

• coeff_slice (lo len : Nat) (a b : DensePoly R) (i : Nat) : (self.slice lo len a b).coeff i = if i < len then (a * b).coeff (lo + i) else 0

  The slice contains exactly the selected product coefficients.

noncomputable def Hex.DensePoly.schoolbookSlice {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (lo len : Nat) (a b : DensePoly R) : DensePoly R

Kernel-facing clipped schoolbook product. The definition is phrased by the semantic product so its coefficient law is immediate; compiled code uses schoolbookSliceImpl, which evaluates the requested schoolbook coefficient folds directly and never materializes the full product.

Equations

• Hex.DensePoly.schoolbookSlice lo len a b = Hex.DensePoly.ofList (List.map (fun (i : Nat) => (a * b).coeff (lo + i)) (List.range len))

theorem Hex.DensePoly.coeff_schoolbookSlice {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (lo len : Nat) (a b : DensePoly R) (i : Nat) : (schoolbookSlice lo len a b).coeff i = if i < len then (a * b).coeff (lo + i) else 0

Coefficient law for a clipped schoolbook product.

def Hex.DensePoly.schoolbookCoeff {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (a b : DensePoly R) (d : Nat) : R

Fold one product diagonal. The left operand is the loop driver; callers put the shorter operand there. Indices outside the valid convolution diagonal perform no coefficient operation.

Equations

• a.schoolbookCoeff b d = List.foldl (fun (acc : R) (i : Nat) => if d < i then acc else if d - i < b.size then acc + a.coeff i * b.coeff (d - i) else acc) 0 (List.range a.size)

theorem Hex.DensePoly.schoolbookCoeff_eq_mulCoeffSum {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (a b : DensePoly R) (d : Nat) : a.schoolbookCoeff b d = a.mulCoeffSum b d

The direct diagonal kernel agrees with the schoolbook product fold.

def Hex.DensePoly.schoolbookSliceImpl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (lo len : Nat) (a b : DensePoly R) : DensePoly R

Allocation-conscious runtime implementation of schoolbookSlice. Requests beyond the product support are discarded before entering the coefficient folds, and the shorter operand drives each diagonal fold.

Equations

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

theorem Hex.DensePoly.schoolbookSlice_eq_impl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (lo len : Nat) (a b : DensePoly R) : schoolbookSlice lo len a b = schoolbookSliceImpl lo len a b

The bounded coefficient-fold implementation agrees with the semantic clipped product.

@[csimp]

theorem Hex.DensePoly.schoolbookSlice_csimp : @schoolbookSlice = @schoolbookSliceImpl

Compiled clipped schoolbook products use direct coefficient folds.

def Hex.DensePoly.schoolbookPlan {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] : MulPlan R

The reference plan backed by the existing allocation-conscious schoolbook multiplication.

Equations

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

@[inline]

def Hex.DensePoly.mulWith {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (a b : DensePoly R) : DensePoly R

Multiply using an explicit plan.

Equations

• Hex.DensePoly.mulWith plan a b = plan.mul a b

@[inline]

def Hex.DensePoly.squareWith {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (a : DensePoly R) : DensePoly R

Square using an explicit plan.

Equations

• Hex.DensePoly.squareWith plan a = plan.square a

@[inline]

def Hex.DensePoly.mulLow {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (len : Nat) (a b : DensePoly R) : DensePoly R

Keep the first len coefficients of a planned product.

Equations

• Hex.DensePoly.mulLow plan len a b = plan.slice 0 len a b

@[inline]

def Hex.DensePoly.mulSlice {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (lo len : Nat) (a b : DensePoly R) : DensePoly R

Keep len coefficients beginning at product degree lo.

Equations

• Hex.DensePoly.mulSlice plan lo len a b = plan.slice lo len a b

@[inline]

def Hex.DensePoly.mulMiddle {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (a b : DensePoly R) (_hsize : b.size ≤ a.size) (_hpos : 0 < b.size) : DensePoly R

The standard middle product for operands of sizes m ≥ n > 0. The result contains product degrees n - 1 through m - 1, shifted down.

Equations

• Hex.DensePoly.mulMiddle plan a b _hsize _hpos = plan.slice (b.size - 1) (a.size - b.size + 1) a b

def Hex.DensePoly.mulMiddleChecked {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (a b : DensePoly R) : DensePoly R

Checked middle product. Operands are ordered by size; an empty operand has zero middle product.

Equations

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

theorem Hex.DensePoly.mulWith_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (a b : DensePoly R) : mulWith plan a b = a * b

Planned multiplication has the existing dense-polynomial semantics.

theorem Hex.DensePoly.squareWith_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (a : DensePoly R) : squareWith plan a = a * a

Planned squaring has the existing dense-polynomial semantics.

theorem Hex.DensePoly.coeff_mulLow {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (len i : Nat) (a b : DensePoly R) : (mulLow plan len a b).coeff i = if i < len then (a * b).coeff i else 0

Coefficient law for a planned low product.

theorem Hex.DensePoly.coeff_mulSlice {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (lo len i : Nat) (a b : DensePoly R) : (mulSlice plan lo len a b).coeff i = if i < len then (a * b).coeff (lo + i) else 0

Coefficient law for an arbitrary planned slice.

theorem Hex.DensePoly.coeff_mulMiddle {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (a b : DensePoly R) (hsize : b.size ≤ a.size) (hpos : 0 < b.size) (i : Nat) : (mulMiddle plan a b hsize hpos).coeff i = if i < a.size - b.size + 1 then (a * b).coeff (b.size - 1 + i) else 0

Coefficient law for the standard proof-taking middle product.