noncomputable def Hex.DensePoly.scale {R : Type u} [Zero R] [DecidableEq R] [Mul R] (c : R) (p : DensePoly R) : DensePoly R

Multiply every coefficient by c.

Kernel-facing specification: one map over the reference coefficient list. Compiled code uses Hex.DensePoly.scaleImpl, the value-equal Array.map pass selected by Hex.DensePoly.scale_eq_impl.

Equations

• Hex.DensePoly.scale c p = Hex.DensePoly.ofList (List.map (fun (a : R) => c * a) p.toList)

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

Runtime implementation of scale: one Array.map pass over the stored coefficients (value-equal to scale by scale_eq_impl, registered @[csimp]).

Equations

• Hex.DensePoly.scaleImpl c p = Hex.DensePoly.ofCoeffs (Array.map (fun (a : R) => c * a) p.toArray)

theorem Hex.DensePoly.scale_eq_scaleImpl {R : Type u} [Zero R] [DecidableEq R] [Mul R] (c : R) (p : DensePoly R) : scale c p = scaleImpl c p

The reference scale and the Array.map runtime pass compute the same polynomial.

theorem Hex.DensePoly.size_scaleImpl_le {R : Type u} [Zero R] [DecidableEq R] [Mul R] (c : R) (p : DensePoly R) : (scaleImpl c p).size ≤ p.size

Coefficientwise scaling cannot increase the stored polynomial size.

@[csimp]

theorem Hex.DensePoly.scale_eq_impl : @scale = @scaleImpl

Register the Array.map pass as the compiled implementation of scale.

noncomputable def Hex.DensePoly.shift {R : Type u} [Zero R] [DecidableEq R] (n : Nat) (p : DensePoly R) : DensePoly R

Multiply by x^n.

Kernel-facing specification: one replicate-append of the reference coefficient list. Compiled code uses Hex.DensePoly.shiftImpl, the value-equal Array.append implementation selected by Hex.DensePoly.shift_eq_impl.

Equations

• Hex.DensePoly.shift n p = if p.isZero = true then 0 else Hex.DensePoly.ofList (List.replicate n Zero.zero ++ p.toList)

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

Runtime implementation of shift: one Array append with no intermediate list (value-equal to shift by shift_eq_impl, registered @[csimp]).

Equations

• Hex.DensePoly.shiftImpl n p = if p.isZero = true then 0 else Hex.DensePoly.ofCoeffs (Array.replicate n Zero.zero ++ p.toArray)

theorem Hex.DensePoly.shift_eq_shiftImpl {R : Type u} [Zero R] [DecidableEq R] (n : Nat) (p : DensePoly R) : shift n p = shiftImpl n p

The reference shift and the Array append compute the same polynomial.

@[csimp]

theorem Hex.DensePoly.shift_eq_impl : @shift = @shiftImpl

Register the Array append as the compiled implementation of shift.

theorem Hex.DensePoly.coeff_scale {R : Type u} [Zero R] [DecidableEq R] [Mul R] (c : R) (p : DensePoly R) (n : Nat) (hzero : c * Zero.zero = Zero.zero) : (scale c p).coeff n = c * p.coeff n

Coefficient law for scalar multiplication. The explicit zero law records the fact that scaling a missing coefficient still gives the default coefficient 0.

@[simp]

theorem Hex.DensePoly.scale_zero_right {R : Type u} [Zero R] [DecidableEq R] [Mul R] (c : R) : scale c 0 = 0

Scaling the zero polynomial yields the zero polynomial: scale c 0 = 0. A simp/grind normal form, so callers need no c * 0 = 0 hypothesis to discharge the scaled-zero case.

@[simp]

theorem Hex.DensePoly.coeff_scale_semiring {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (c : S) (p : DensePoly S) (n : Nat) : (scale c p).coeff n = c * p.coeff n

Semiring-specialized coefficient law for scalar multiplication, registered as a normalizing rewrite because the required c * 0 = 0 law is available from the semiring structure.

theorem Hex.DensePoly.scale_scale {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (a b : S) (p : DensePoly S) : scale a (scale b p) = scale (a * b) p

Scaling twice multiplies the two scalars.

@[simp]

theorem Hex.DensePoly.scale_zero_left_semiring {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (p : DensePoly S) : scale 0 p = 0

Semiring-specialized left zero law for scalar multiplication.

@[simp]

theorem Hex.DensePoly.coeff_shift {R : Type u} [Zero R] [DecidableEq R] (n : Nat) (p : DensePoly R) (k : Nat) : (shift n p).coeff k = if k < n then Zero.zero else p.coeff (k - n)

Coefficient law for shifting by x^n: coefficients below n are zero and later coefficients are read from the original polynomial with the index shifted down.

@[simp]

theorem Hex.DensePoly.shift_zero_right {R : Type u} [Zero R] [DecidableEq R] (n : Nat) : shift n 0 = 0

Shifting the zero polynomial by any power leaves it zero: shift n 0 = 0. A simp/grind normal form for the degenerate input to shift.

@[simp]

theorem Hex.DensePoly.shift_zero_left {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : shift 0 p = p

Shifting by x^0 is the identity: shift 0 p = p. A simp/grind normal form so a trivial shift drops out of multiplication and division proofs.

theorem Hex.DensePoly.coeff_shift_scale {R : Type u} [Zero R] [DecidableEq R] [Mul R] (i : Nat) (c : R) (p : DensePoly R) (k : Nat) (hzero : c * Zero.zero = Zero.zero) : (shift i (scale c p)).coeff k = if k < i then Zero.zero else c * p.coeff (k - i)

Combined coefficient law for a scaled shift. The zero-law hypothesis is the only algebraic fact needed to normalize coefficients that are outside the support.

@[simp]

theorem Hex.DensePoly.coeff_shift_scale_semiring {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (i : Nat) (c : S) (p : DensePoly S) (k : Nat) : (shift i (scale c p)).coeff k = if k < i then Zero.zero else c * p.coeff (k - i)

Semiring-specialized coefficient law for a scaled shift, registered as a normalizing rewrite for the common algebraic setting.

theorem Hex.DensePoly.toList_getD_eq_coeff {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) (n : Nat) : p.toList.getD n Zero.zero = p.coeff n

Reading the reference coefficient list with default zero agrees with DensePoly.coeff.

@[simp]

theorem Hex.DensePoly.coeff_zero {R : Type u} [Zero R] [DecidableEq R] (n : Nat) : coeff 0 n = 0

The zero polynomial has coefficient 0 at every index.

def Hex.DensePoly.zipPad {R : Type u} [Zero R] (f : R → R → R) : List R → List R → List R

Zip two coefficient lists with f, padding the shorter list with literal Zero.zero arguments: overhang entries become f p Zero.zero / f Zero.zero q rather than being passed through, so every output entry is literally f (xs.getD i) (ys.getD i); the value the Array.ofFn runtime impls reproduce with no algebraic laws on R.

Equations

• Hex.DensePoly.zipPad f [] x✝ = List.map (fun (y : R) => f Zero.zero y) x✝
• Hex.DensePoly.zipPad f (x_2 :: xs) [] = f x_2 Zero.zero :: Hex.DensePoly.zipPad f xs []
• Hex.DensePoly.zipPad f (x_2 :: xs) (y :: ys) = f x_2 y :: Hex.DensePoly.zipPad f xs ys

noncomputable def Hex.DensePoly.add {R : Type u} [Zero R] [DecidableEq R] [Add R] (p q : DensePoly R) : DensePoly R

Add two dense polynomials coefficientwise.

Kernel-facing specification: a single padded walk of the two coefficient lists. Compiled code uses Hex.DensePoly.addImpl, the value-equal, one-allocation Array.ofFn loop selected by Hex.DensePoly.add_eq_impl.

Equations

• p.add q = Hex.DensePoly.ofCoeffs (Hex.DensePoly.zipPad (fun (x1 x2 : R) => x1 + x2) p.toList q.toList).toArray

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

Runtime implementation of add: one Array.ofFn allocation over the padded index range (value-equal to add by add_eq_impl, registered @[csimp]).

Equations

• p.addImpl q = Hex.DensePoly.ofCoeffs (Array.ofFn fun (i : Fin (max p.size q.size)) => p.coeff ↑i + q.coeff ↑i)

theorem Hex.DensePoly.add_eq_addImpl {R : Type u} [Zero R] [DecidableEq R] [Add R] (p q : DensePoly R) : p.add q = p.addImpl q

The reference add and the Array.ofFn runtime loop compute the same polynomial: each output coefficient is literally p.coeff i + q.coeff i on both sides, so no algebraic laws on R are needed.

@[csimp]

theorem Hex.DensePoly.add_eq_impl : @add = @addImpl

Register the Array.ofFn loop as the compiled implementation of add.

@[instance_reducible]

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

Equations

• Hex.DensePoly.instAdd = { add := Hex.DensePoly.add }

noncomputable def Hex.DensePoly.sub {R : Type u} [Zero R] [DecidableEq R] [Sub R] (p q : DensePoly R) : DensePoly R

Subtract two dense polynomials coefficientwise.

Like Hex.DensePoly.add, this is a kernel-reduction-friendly specification. Compiled code uses Hex.DensePoly.subImpl, the value-equal Array.ofFn loop selected by Hex.DensePoly.sub_eq_impl.

Equations

• p.sub q = Hex.DensePoly.ofCoeffs (Hex.DensePoly.zipPad (fun (x1 x2 : R) => x1 - x2) p.toList q.toList).toArray

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

Runtime implementation of sub (value-equal to sub by sub_eq_impl, registered @[csimp]).

Equations

• p.subImpl q = Hex.DensePoly.ofCoeffs (Array.ofFn fun (i : Fin (max p.size q.size)) => p.coeff ↑i - q.coeff ↑i)

theorem Hex.DensePoly.sub_eq_subImpl {R : Type u} [Zero R] [DecidableEq R] [Sub R] (p q : DensePoly R) : p.sub q = p.subImpl q

The reference sub and the Array.ofFn runtime loop compute the same polynomial.

@[csimp]

theorem Hex.DensePoly.sub_eq_impl : @sub = @subImpl

Register the Array.ofFn loop as the compiled implementation of sub.

@[instance_reducible]

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

Equations

• Hex.DensePoly.instSub = { sub := Hex.DensePoly.sub }

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

Coefficientwise additive inverse, expressed through executable subtraction.

Kernel-facing specification (one Hex.DensePoly.sub against the zero polynomial); compiled code uses Hex.DensePoly.negImpl, the value-equal Array.map pass selected by Hex.DensePoly.neg_eq_impl.

Equations

• p.neg = 0 - p

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

Runtime implementation of neg: one Array.map pass over the stored coefficients (value-equal to neg by neg_eq_impl, registered @[csimp]).

Equations

• p.negImpl = Hex.DensePoly.ofCoeffs (Array.map (fun (a : R) => Zero.zero - a) p.toArray)

theorem Hex.DensePoly.neg_eq_negImpl {R : Type u} [Zero R] [DecidableEq R] [Sub R] (p : DensePoly R) : p.neg = p.negImpl

The reference neg and the Array.map runtime pass compute the same polynomial: each coefficient is literally Zero.zero - p.coeff i on both sides.

@[csimp]

theorem Hex.DensePoly.neg_eq_impl : @neg = @negImpl

Register the Array.map pass as the compiled implementation of neg.

@[instance_reducible]

instance Hex.DensePoly.instNegOfSub {R : Type u} [Zero R] [DecidableEq R] [Sub R] : Neg (DensePoly R)

Equations

• Hex.DensePoly.instNegOfSub = { neg := Hex.DensePoly.neg }

class Hex.DensePoly.AddZeroLaw (S : Type u) [Zero S] [Add S] : Prop

Compatibility law for caller-facing Zero/Add instances used by semiring wrappers.

• add_zero_zero : Zero.zero + Zero.zero = Zero.zero

instance Hex.DensePoly.addZeroLaw_of_semiring {S : Type u} [Lean.Grind.Semiring S] : AddZeroLaw S

Semiring structures provide the zero-addition compatibility law used by coefficient lemmas.

class Hex.DensePoly.SubZeroLaw (S : Type u) [Zero S] [Sub S] : Prop

Compatibility law for caller-facing Zero/Sub instances used by ring wrappers.

• sub_zero_zero : Zero.zero - Zero.zero = Zero.zero

instance Hex.DensePoly.subZeroLaw_of_ring {S : Type u} [Lean.Grind.Ring S] : SubZeroLaw S

Ring structures provide the zero-subtraction compatibility law used by coefficient lemmas.

class Hex.DensePoly.ZeroSubNegLaw (S : Type u) [Zero S] [Sub S] [Neg S] : Prop

Compatibility law for caller-facing Zero/Sub/Neg instances used by negation wrappers.

• zero_sub_eq_neg (a : S) : Zero.zero - a = -a

instance Hex.DensePoly.zeroSubNegLaw_of_ring {S : Type u} [Lean.Grind.Ring S] : ZeroSubNegLaw S

Ring structures provide the zero-subtraction negation law used by coefficient lemmas.

def Hex.DensePoly.mulRow {R : Type u} [Add R] [Mul R] (c : R) : List R → List R → List R

One row of the schoolbook convolution: add c times each entry of qs into the corresponding entry of acc, dropping contributions past the end of acc (matching the dropped out-of-bounds Array.set! writes of mulImpl).

Equations

• Hex.DensePoly.mulRow c x✝ [] = x✝
• Hex.DensePoly.mulRow c [] (head :: tail) = []
• Hex.DensePoly.mulRow c (a :: acc) (q :: qs) = (a + c * q) :: Hex.DensePoly.mulRow c acc qs

def Hex.DensePoly.mulRows {R : Type u} [Add R] [Mul R] (qs : List R) : List R → List R → List R

All rows of the schoolbook convolution: for each coefficient of ps in ascending-degree order, add its scaled copy of qs into the accumulator at the matching offset. The accumulator entry at the current offset is final once its row is applied, so each step emits one finished coefficient and recurses on the tail. Additions reach each accumulator entry in exactly the order of the Array-based mulImpl loop, which is what makes mul_eq_impl provable without any algebraic laws on R.

Equations

• Hex.DensePoly.mulRows qs [] x✝ = x✝
• Hex.DensePoly.mulRows qs (x_2 :: xs) [] = []
• Hex.DensePoly.mulRows [] (x_2 :: xs) (y :: ys) = y :: Hex.DensePoly.mulRows [] xs ys
• Hex.DensePoly.mulRows (q :: qs') (x_2 :: xs) (y :: ys) = (y + x_2 * q) :: Hex.DensePoly.mulRows (q :: qs') xs (Hex.DensePoly.mulRow x_2 ys qs')

noncomputable def Hex.DensePoly.mul {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p q : DensePoly R) : DensePoly R

Schoolbook dense polynomial multiplication by direct coefficient convolution.

This definition is the kernel-reduction-friendly specification: the accumulator is a plain list walked head-first, so reducing a concrete product costs one cons-step per (i, j) coefficient pair instead of an O(size) list traversal per Array access. Compiled code instead runs the in-place Array loop Hex.DensePoly.mulImpl, selected by Hex.DensePoly.mul_eq_impl.

Equations

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

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

Runtime implementation of mul: the same schoolbook convolution computed by in-place Array writes (value-equal to mul by mul_eq_impl, registered @[csimp]).

The inner j-loop reads the loop-invariant coefficient p.coeff i from a single let-bound value (pi) instead of re-projecting it on every (i, j) step, so the compiled inner loop performs one bounds-checked coefficient read per i rather than per (i, j). The let is a zeta reduction away from the bare convolution, so it does not change the value, the coeff_mul characterization, or any proof.

Equations

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

def Hex.DensePoly.mulCoeffStep {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p q : DensePoly R) (n i : Nat) (acc : R) (j : Nat) : R

One inner schoolbook multiplication step, projected to coefficient n.

Equations

• p.mulCoeffStep q n i acc j = if i + j = n then acc + p.coeff i * q.coeff j else acc

def Hex.DensePoly.mulCoeffSum {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p q : DensePoly R) (n : Nat) : R

The schoolbook coefficient fold matching the executable multiplication loop order.

Equations

• p.mulCoeffSum q n = List.foldl (fun (acc : R) (i : Nat) => List.foldl (p.mulCoeffStep q n i) acc (List.range q.size)) Zero.zero (List.range p.size)

theorem Hex.DensePoly.mulCoeffSum_eq_singleFold {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p q : DensePoly R) (n : Nat) : p.mulCoeffSum q n = List.foldl (fun (c : R) (i : Nat) => if i ≤ n ∧ n - i < q.size then c + p.coeff i * q.coeff (n - i) else c) Zero.zero (List.range p.size)

mulCoeffSum collapsed to a single fold over the row index i, each row contributing p.coeff i * q.coeff (n - i) when i ≤ n and n - i is in range (closed form from foldl_mulCoeffStep_range). Public so lazy-reduction convolution kernels can relate their per-coefficient Nat sums to the reference product coefficient.

theorem Hex.DensePoly.mul_eq_mulImpl {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p q : DensePoly R) : p.mul q = p.mulImpl q

The specification mul and the Array-loop mulImpl compute the same polynomial: both sides perform the same coefficient additions in the same order, so no algebraic laws on R are needed.

@[csimp]

theorem Hex.DensePoly.mul_eq_impl : @mul = @mulImpl

Register the Array-loop mulImpl as the compiled implementation of mul. As with trimTrailingZeros_eq_impl, the @[csimp] swap is backed by a proof, so the runtime loop is verified equal to the kernel-facing specification.

@[instance_reducible]

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

Equations

• Hex.DensePoly.instMulOfAdd = { mul := Hex.DensePoly.mul }

theorem Hex.DensePoly.coeff_mul {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p q : DensePoly R) (n : Nat) : (p * q).coeff n = p.mulCoeffSum q n

Characterising coefficient law for multiplication: each coefficient of p * q is computed by the same nested schoolbook fold as the executable multiplication loop.

theorem Hex.DensePoly.size_mul_le {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p q : DensePoly R) : (p * q).size ≤ p.size + q.size - 1

A product stores at most p.size + q.size - 1 coefficients.

def Hex.DensePoly.evalCoeffList {R : Type u} [Zero R] [Add R] [Mul R] : List R → R → R

List-level Horner evaluation, reading coefficients from low to high degree. The body of the eval specification.

Equations

• Hex.DensePoly.evalCoeffList [] x✝ = Zero.zero
• Hex.DensePoly.evalCoeffList (c :: cs) x✝ = Hex.DensePoly.evalCoeffList cs x✝ * x✝ + c

noncomputable def Hex.DensePoly.eval {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p : DensePoly R) (x : R) : R

Evaluate a polynomial using Horner's method.

Kernel-facing specification: one cons walk of the coefficient list, highest degree innermost. Compiled code uses Hex.DensePoly.evalImpl, the value-equal downward Array.foldr loop with no intermediate list or reverse allocation, selected by Hex.DensePoly.eval_eq_impl.

Equations

• p.eval x = Hex.DensePoly.evalCoeffList p.toList x

def Hex.DensePoly.evalImpl {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p : DensePoly R) (x : R) : R

Runtime implementation of eval: a downward Array.foldr Horner loop over the stored coefficients, with no intermediate coefficient-list or reverse allocation (value-equal to eval by eval_eq_impl, registered @[csimp]).

Equations

• p.evalImpl x = Array.foldr (fun (coeff acc : R) => acc * x + coeff) Zero.zero p.toArray

theorem Hex.DensePoly.eval_eq_evalImpl {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p : DensePoly R) (x : R) : p.eval x = p.evalImpl x

The reference eval and the Array.foldr runtime loop compute the same value.

@[csimp]

theorem Hex.DensePoly.eval_eq_impl : @eval = @evalImpl

Register the Array.foldr loop as the compiled implementation of eval.

def Hex.DensePoly.composeCoeffList {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] : List R → DensePoly R → DensePoly R

List-level Horner composition, reading coefficients from low to high degree and preserving the acc * q + C c step orientation (for generic R this differs from composeScalarCoeffList's C c + q * acc).

Equations

• Hex.DensePoly.composeCoeffList [] x✝ = 0
• Hex.DensePoly.composeCoeffList (c :: cs) x✝ = Hex.DensePoly.composeCoeffList cs x✝ * x✝ + Hex.DensePoly.C c

noncomputable def Hex.DensePoly.compose {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p q : DensePoly R) : DensePoly R

Compose polynomials using Horner's method.

Kernel-facing specification: one cons walk of the coefficient list. Compiled code uses Hex.DensePoly.composeImpl, the value-equal downward Array.foldr loop selected by Hex.DensePoly.compose_eq_impl.

Equations

• p.compose q = Hex.DensePoly.composeCoeffList p.toList q

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

Runtime implementation of compose: a downward Array.foldr Horner loop (value-equal to compose by compose_eq_impl, registered @[csimp]).

Equations

• p.composeImpl q = Array.foldr (fun (coeff : R) (acc : Hex.DensePoly R) => acc * q + Hex.DensePoly.C coeff) 0 p.toArray

theorem Hex.DensePoly.compose_eq_composeImpl {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p q : DensePoly R) : p.compose q = p.composeImpl q

The reference compose and the Array.foldr runtime loop compute the same polynomial.

@[csimp]

theorem Hex.DensePoly.compose_eq_impl : @compose = @composeImpl

Register the Array.foldr loop as the compiled implementation of compose.

@[simp]

theorem Hex.DensePoly.compose_zero_left {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (q : DensePoly R) : compose 0 q = 0

Left-composition by the zero polynomial is zero.

theorem Hex.DensePoly.compose_C {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (c : R) (q : DensePoly R) (hzero_add : Zero.zero + c = c) : (C c).compose q = C c

Composition of a constant polynomial. The explicit zero-addition law is needed because the generic Add/Mul/Zero interfaces do not provide algebraic simplification rules.

@[simp]

theorem Hex.DensePoly.compose_C_semiring {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (c : S) (q : DensePoly S) : (C c).compose q = C c

Semiring-specialized composition law for constants. This packages the zero-addition law needed by the generic compose_C.

def Hex.DensePoly.composeScalarCoeffList {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] : List R → DensePoly R → DensePoly R

List-level Horner form for composition, reading coefficients from low to high degree.

Equations

• Hex.DensePoly.composeScalarCoeffList [] x✝ = 0
• Hex.DensePoly.composeScalarCoeffList (c :: cs) x✝ = Hex.DensePoly.C c + x✝ * Hex.DensePoly.composeScalarCoeffList cs x✝

theorem Hex.DensePoly.compose_eq_composeScalarCoeffList_of_step {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p q : DensePoly R) (hstep : ∀ (acc : DensePoly R) (c : R), acc * q + C c = C c + q * acc) : p.compose q = composeScalarCoeffList p.toList q

DensePoly.compose agrees with the list-level Horner form over the stored coefficients when the caller supplies the algebraic step that commutes a Horner tail past q.

def Hex.DensePoly.composePower {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Mul R] (q : DensePoly R) : Nat → DensePoly R

Iterated polynomial power used by the compose power-sum characterisation.

Equations

• q.composePower 0 = Hex.DensePoly.C 1
• q.composePower n.succ = q * q.composePower n

def Hex.DensePoly.composeCoeffPowerSumFrom {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Mul R] : List R → Nat → DensePoly R → DensePoly R

List-backed power-sum form for composition, starting at a coefficient base index.

Equations

• Hex.DensePoly.composeCoeffPowerSumFrom [] x✝¹ x✝ = 0
• Hex.DensePoly.composeCoeffPowerSumFrom (c :: cs) x✝¹ x✝ = Hex.DensePoly.C c * x✝.composePower x✝¹ + Hex.DensePoly.composeCoeffPowerSumFrom cs (x✝¹ + 1) x✝

def Hex.DensePoly.composeCoeffPowerSumUpTo {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Mul R] (coeff : Nat → R) : Nat → Nat → DensePoly R → DensePoly R

Coefficient-indexed bounded power-sum form for composition.

Equations

• Hex.DensePoly.composeCoeffPowerSumUpTo coeff 0 x✝¹ x✝ = 0
• Hex.DensePoly.composeCoeffPowerSumUpTo coeff n.succ x✝¹ x✝ = Hex.DensePoly.C (coeff x✝¹) * x✝.composePower x✝¹ + Hex.DensePoly.composeCoeffPowerSumUpTo coeff n (x✝¹ + 1) x✝

theorem Hex.DensePoly.composeCoeffPowerSumFrom_range_eq_upTo {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Mul R] (coeff : Nat → R) (q : DensePoly R) (n base : Nat) : composeCoeffPowerSumFrom (List.map (fun (i : Nat) => coeff (base + i)) (List.range n)) base q = composeCoeffPowerSumUpTo coeff n base q

composeCoeffPowerSumFrom over a consecutive range is the bounded coefficient-indexed power sum.

theorem Hex.DensePoly.toList_eq_coeff_range {R : Type u} [Zero R] [DecidableEq R] (p : DensePoly R) : p.toList = List.map (fun (i : Nat) => p.coeff i) (List.range p.size)

The reference coefficient list is the range of coefficient reads over p.size.

def Hex.DensePoly.derivList {R : Type u} [NatCast R] [Mul R] : Nat → List R → List R

Index-carrying derivative walk: entry j of derivList i cs is ((i + j + 1 : Nat) : R) * cs[j]. Applied at i = 0 to the coefficient tail, it produces the formal-derivative coefficients in one cons walk.

Equations

• Hex.DensePoly.derivList x✝ [] = []
• Hex.DensePoly.derivList x✝ (c :: cs) = ↑(x✝ + 1) * c :: Hex.DensePoly.derivList (x✝ + 1) cs

noncomputable def Hex.DensePoly.derivative {R : Type u} [Zero R] [DecidableEq R] [NatCast R] [Mul R] (p : DensePoly R) : DensePoly R

Formal derivative. The coefficient of x^i becomes (i + 1) * a_(i+1).

Kernel-facing specification: one cons walk of the coefficient tail. Compiled code uses Hex.DensePoly.derivativeImpl, the value-equal Array.ofFn loop selected by Hex.DensePoly.derivative_eq_impl.

Equations

• p.derivative = Hex.DensePoly.ofCoeffs (Hex.DensePoly.derivList 0 (List.drop 1 p.toList)).toArray

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

Runtime implementation of derivative: one Array.ofFn allocation (value-equal to derivative by derivative_eq_impl, registered @[csimp]).

Equations

• p.derivativeImpl = Hex.DensePoly.ofCoeffs (Array.ofFn fun (i : Fin (p.size - 1)) => ↑(↑i + 1) * p.coeff (↑i + 1))

theorem Hex.DensePoly.derivative_eq_derivativeImpl {R : Type u} [Zero R] [DecidableEq R] [NatCast R] [Mul R] (p : DensePoly R) : p.derivative = p.derivativeImpl

The reference derivative and the Array.ofFn runtime loop compute the same polynomial.

@[csimp]

theorem Hex.DensePoly.derivative_eq_impl : @derivative = @derivativeImpl

Register the Array.ofFn loop as the compiled implementation of derivative.

theorem Hex.DensePoly.size_derivative_le {R : Type u} [Zero R] [DecidableEq R] [NatCast R] [Mul R] (p : DensePoly R) : p.derivative.size ≤ p.size - 1

The derivative stores at most one fewer coefficient than its input.

theorem Hex.DensePoly.coeff_add {R : Type u} [Zero R] [DecidableEq R] [Add R] (p q : DensePoly R) (n : Nat) (hzero : Zero.zero + Zero.zero = Zero.zero) : (p + q).coeff n = p.coeff n + q.coeff n

Coefficient law for addition. The explicit zero law is needed because the generic Add/Zero interface does not imply 0 + 0 = 0.

@[simp]

theorem Hex.DensePoly.coeff_add_semiring {S : Type u} [Zero S] [Add S] [Lean.Grind.Semiring S] [DecidableEq S] (p q : DensePoly S) (n : Nat) (hzero : AddZeroLaw S := by infer_instance) : (p + q).coeff n = p.coeff n + q.coeff n

Semiring-specialized coefficient law for addition.

theorem Hex.DensePoly.scale_add {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (a : S) (p q : DensePoly S) : scale a (p + q) = scale a p + scale a q

Scaling distributes over polynomial addition.

theorem Hex.DensePoly.coeff_sub {R : Type u} [Zero R] [DecidableEq R] [Sub R] (p q : DensePoly R) (n : Nat) (hzero : Zero.zero - Zero.zero = Zero.zero) : (p - q).coeff n = p.coeff n - q.coeff n

Coefficient law for subtraction. The explicit zero law is needed because the generic Sub/Zero interface does not imply 0 - 0 = 0.

@[simp]

theorem Hex.DensePoly.coeff_sub_ring {S : Type u} [Zero S] [Sub S] [Lean.Grind.Ring S] [DecidableEq S] (p q : DensePoly S) (n : Nat) (hzero : SubZeroLaw S := by infer_instance) : (p - q).coeff n = p.coeff n - q.coeff n

Ring-specialized coefficient law for subtraction.

theorem Hex.DensePoly.coeff_neg {R : Type u} [Zero R] [DecidableEq R] [Sub R] (p : DensePoly R) (n : Nat) (hzero : Zero.zero - Zero.zero = Zero.zero) : (-p).coeff n = 0 - p.coeff n

Coefficient law for negation, expressed through subtraction from zero. The explicit zero law is inherited from the generic subtraction coefficient theorem.

@[simp]

theorem Hex.DensePoly.coeff_neg_ring {S : Type u} [Zero S] [Sub S] [Neg S] [Lean.Grind.Ring S] [DecidableEq S] (p : DensePoly S) (n : Nat) (hsub : SubZeroLaw S := by infer_instance) (hneg : ZeroSubNegLaw S := by infer_instance) : (-p).coeff n = -p.coeff n

Ring-specialized coefficient law for negation.

@[simp]

theorem Hex.DensePoly.add_zero_semiring {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (p : DensePoly S) : p + 0 = p

Semiring-specialized right zero law for dense polynomial addition.

@[simp]

theorem Hex.DensePoly.zero_add_semiring {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (p : DensePoly S) : 0 + p = p

Semiring-specialized left zero law for dense polynomial addition.

@[simp]

theorem Hex.DensePoly.sub_zero_ring {S : Type u} [Lean.Grind.Ring S] [DecidableEq S] (p : DensePoly S) : p - 0 = p

Ring-specialized right zero law for dense polynomial subtraction.

@[simp]

theorem Hex.DensePoly.zero_sub_ring {S : Type u} [Lean.Grind.Ring S] [DecidableEq S] (p : DensePoly S) : 0 - p = -p

Ring-specialized left zero law for dense polynomial subtraction.

@[simp]

theorem Hex.DensePoly.neg_zero_ring {S : Type u} [Lean.Grind.Ring S] [DecidableEq S] : -0 = 0

Ring-specialized negation of the zero dense polynomial.

@[simp]

theorem Hex.DensePoly.eval_zero {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (x : R) : eval 0 x = 0

Horner evaluation sends the zero dense polynomial to 0.

theorem Hex.DensePoly.eval_add {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p q : DensePoly R) (x : R) (hzero_add : Zero.zero + Zero.zero = Zero.zero) (hzero_horner : Zero.zero * x + Zero.zero = Zero.zero) (hstep : ∀ (a b c d : R), (a + b) * x + (c + d) = a * x + c + (b * x + d)) : (p + q).eval x = p.eval x + q.eval x

Evaluation law for addition. The explicit laws package the zero-preservation and one-step Horner distributivity needed by the generic Add/Mul interface.

@[simp]

theorem Hex.DensePoly.eval_add_semiring {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (p q : DensePoly S) (x : S) : (p + q).eval x = p.eval x + q.eval x

Semiring-specialized evaluation law for addition.

theorem Hex.DensePoly.eval_sub {R : Type u} [Zero R] [DecidableEq R] [Sub R] [Add R] [Mul R] (p q : DensePoly R) (x : R) (hzero_sub : Zero.zero - Zero.zero = Zero.zero) (hzero_horner : Zero.zero * x + Zero.zero = Zero.zero) (hstep : ∀ (a b c d : R), (a - b) * x + (c - d) = a * x + c - (b * x + d)) : (p - q).eval x = p.eval x - q.eval x

Evaluation law for subtraction. The explicit laws package the zero-preservation and one-step Horner distributivity needed by the generic Sub/Mul interface.

@[simp]

theorem Hex.DensePoly.eval_sub_ring {S : Type u} [Lean.Grind.Ring S] [DecidableEq S] (p q : DensePoly S) (x : S) : (p - q).eval x = p.eval x - q.eval x

Ring-specialized evaluation law for subtraction.

theorem Hex.DensePoly.eval_neg {R : Type u} [Zero R] [DecidableEq R] [Sub R] [Add R] [Mul R] (p : DensePoly R) (x : R) (hzero_sub : Zero.zero - Zero.zero = Zero.zero) (hzero_horner : Zero.zero * x + Zero.zero = Zero.zero) (hstep : ∀ (a b c d : R), (a - b) * x + (c - d) = a * x + c - (b * x + d)) : (-p).eval x = Zero.zero - p.eval x

Evaluation law for negation, expressed through subtraction from zero.

@[simp]

theorem Hex.DensePoly.eval_neg_ring {S : Type u} [Lean.Grind.Ring S] [DecidableEq S] (p : DensePoly S) (x : S) (hneg : ZeroSubNegLaw S := by infer_instance) : (-p).eval x = -p.eval x

Ring-specialized evaluation law for negation.

theorem Hex.DensePoly.eval_C {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (c x : R) (hzero_mul : Zero.zero * x = Zero.zero) (hzero_add : Zero.zero + c = c) : (C c).eval x = c

Evaluation of a constant polynomial. The explicit zero laws are needed because the generic Add/Mul/Zero interfaces do not provide algebraic simplification rules.

@[simp]

theorem Hex.DensePoly.eval_C_semiring {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (c x : S) : (C c).eval x = c

Semiring-specialized evaluation law for constants. This packages the zero-multiplication and zero-addition laws needed by the generic eval_C.

@[simp]

theorem Hex.DensePoly.eval_monomial_semiring {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (n : Nat) (c x : S) : (monomial n c).eval x = c * x ^ n

Semiring-specialized evaluation law for monomials.

@[simp]

theorem Hex.DensePoly.derivative_zero {R : Type u} [Zero R] [DecidableEq R] [NatCast R] [Mul R] : derivative 0 = 0

The formal derivative of the zero polynomial is zero.

theorem Hex.DensePoly.coeff_derivative {R : Type u} [Zero R] [DecidableEq R] [NatCast R] [Mul R] (p : DensePoly R) (n : Nat) (hzero : ↑(n + 1) * Zero.zero = Zero.zero) : p.derivative.coeff n = ↑(n + 1) * p.coeff (n + 1)

Characterising coefficient law for the formal derivative: the coefficient of x^n in derivative p is (n + 1) * p.coeff (n + 1). The explicit zero law ((n + 1 : Nat) : R) * 0 = 0 is needed because the generic NatCast/Mul/Zero interface does not guarantee it, mirroring the hypothesis on Hex.DensePoly.coeff_scale.

@[simp]

theorem Hex.DensePoly.coeff_derivative_semiring {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (p : DensePoly S) (n : Nat) : p.derivative.coeff n = ↑(n + 1) * p.coeff (n + 1)

Semiring-specialized coefficient law for the formal derivative, registered as a normalizing rewrite because semirings provide the required a * 0 = 0 law.

@[simp]

theorem Hex.DensePoly.derivative_C_semiring {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (c : S) : (C c).derivative = 0

The formal derivative of a constant polynomial is zero over a semiring.

@[simp]

theorem Hex.DensePoly.derivative_monomial_zero_semiring {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (c : S) : (monomial 0 c).derivative = 0

The formal derivative of a degree-zero monomial is zero over a semiring.

theorem Hex.DensePoly.derivative_monomial_succ_semiring {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (n : Nat) (c : S) : (monomial (n + 1) c).derivative = monomial n (↑(n + 1) * c)

The formal derivative of c * x^(n + 1) is (n + 1) * c * x^n over a semiring.