theorem Hex.FpPoly.compose_zero {p : Nat} [ZMod64.Bounds p] (q : FpPoly p) : DensePoly.compose 0 q = 0

Substituting any q into the zero polynomial gives 0.

@[simp]

theorem Hex.FpPoly.compose_C {p : Nat} [ZMod64.Bounds p] (c : ZMod64 p) (q : FpPoly p) : DensePoly.compose (C c) q = C c

Substituting q into a constant polynomial leaves the constant fixed.

@[simp]

theorem Hex.FpPoly.compose_X {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (q : FpPoly p) : DensePoly.compose X q = q

Substituting q into X returns q; X is the identity of composition.

theorem Hex.FpPoly.compose_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (q : FpPoly p) : DensePoly.compose 1 q = 1

Composing the constant polynomial 1 with any q yields 1: the multiplicative identity of FpPoly is fixed by substitution. This is the base case for composing an iterated product of linear factors (see compose_primeFieldLinearProduct).

theorem Hex.FpPoly.compose_eq_composeScalarCoeffList {p : Nat} [ZMod64.Bounds p] (f q : FpPoly p) : DensePoly.compose f q = DensePoly.composeScalarCoeffList (DensePoly.toList f) q

DensePoly.compose f q agrees with the iterative Horner form.

theorem Hex.FpPoly.C_add_eq {p : Nat} [ZMod64.Bounds p] (a b : ZMod64 p) : DensePoly.C (a + b) = DensePoly.C a + DensePoly.C b

The constant embedding C is additive: C (a + b) = C a + C b.

theorem Hex.FpPoly.C_sub_eq {p : Nat} [ZMod64.Bounds p] (a b : ZMod64 p) : DensePoly.C (a - b) = DensePoly.C a - DensePoly.C b

The constant embedding C turns a difference of scalars into a difference of constant polynomials. Used to push coefficient subtractions through products such as f * (X - C c).

theorem Hex.FpPoly.C_mul_C_eq {p : Nat} [ZMod64.Bounds p] (a b : ZMod64 p) : DensePoly.C (a * b) = DensePoly.C a * DensePoly.C b

The constant embedding C turns a product of scalars into a product of constant polynomials. Used to normalise constant coefficients when expanding products of linear factors.

theorem Hex.FpPoly.compose_monomial {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (w : FpPoly p) (k : Nat) (c : ZMod64 p) : (DensePoly.monomial k c).compose w = DensePoly.C c * w.linearPow k

Substituting w into a monomial gives the coefficient times a power of w.

This is the monomial case that Polynomial.induction_on' asks for on the Mathlib side, so it is what lets a Mathlib ring homomorphism be identified with the executable substitution.

theorem Hex.FpPoly.compose_linearPow_X {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (w : FpPoly p) (k : Nat) : DensePoly.compose (X.linearPow k) w = w.linearPow k

compose (linearPow X k) w = linearPow w k.

def Hex.FpPoly.composeCoeffPowerSumUpTo {p : Nat} [ZMod64.Bounds p] (coeff : Nat → ZMod64 p) : Nat → Nat → FpPoly p → FpPoly p

Recursive sum form of compose. The compose-power-sum Σ_{k=base}^{base+n-1} C(coeff k) · linearPow w k recursively builds up the polynomial substitution: each step adds a single C(coeff base) · linearPow w base term and recurses with base + 1. This shape is matched by Berlekamp's matrix-action sum after replacing linearPow w with the reduced powModMonic columns.

Equations

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

theorem Hex.FpPoly.composeCoeffPowerSumUpTo_eq {p : Nat} [ZMod64.Bounds p] (coeff : Nat → ZMod64 p) (n base : Nat) (w : FpPoly p) : composeCoeffPowerSumUpTo coeff n base w = DensePoly.composeCoeffPowerSumUpTo coeff n base w

The local FpPoly power-sum accumulator built from linearPow agrees with the shared DensePoly.composeCoeffPowerSumUpTo. Callers use this to transfer the explicit compose-as-sum characterization onto the DensePoly API that downstream files import.

theorem Hex.FpPoly.compose_eq_coeff_power_sum_upTo_bound {p : Nat} [ZMod64.Bounds p] (f w : FpPoly p) {bound : Nat} (hbound : DensePoly.size f ≤ bound) : DensePoly.compose f w = composeCoeffPowerSumUpTo (fun (i : Nat) => DensePoly.coeff f i) bound 0 w

compose f w equals composeCoeffPowerSumUpTo evaluated up to any upper bound that is at least f.size. Out-of-range coefficients of f vanish, so the recursion safely extends past f.size.

theorem Hex.FpPoly.compose_sub {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f h w : FpPoly p) : DensePoly.compose (f - h) w = DensePoly.compose f w - DensePoly.compose h w

compose distributes over subtraction.

theorem Hex.FpPoly.compose_add {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f h w : FpPoly p) : DensePoly.compose (f + h) w = DensePoly.compose f w + DensePoly.compose h w

Substitution is additive. Follows from Hex.FpPoly.compose_sub, since f + h = f - (0 - h) and substitution fixes zero.

theorem Hex.FpPoly.compose_sub_X {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (a w : FpPoly p) : (a - X).compose w = DensePoly.compose a w - w

Narrow specialisation needed by the witness-substitution caller: substituting w for X in a - X yields compose a w - w.

theorem Hex.FpPoly.compose_linearPow_X_sub_X {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (w : FpPoly p) (k : Nat) : (X.linearPow k - X).compose w = w.linearPow k - w

The linearPow X k - X substitution: substituting w for X in linearPow X k - X yields linearPow w k - w.

theorem Hex.FpPoly.compose_mul_X_sub_C {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (a : FpPoly p) (c : ZMod64 p) (w : FpPoly p) : (a * (X - C c)).compose w = DensePoly.compose a w * (w - C c)

Composition distributes over multiplication by a linear factor: substituting w into a * (X - C c) gives (compose a w) * (w - C c). This is the inductive step for composing an iterated product of linear factors ∏ (X - C cᵢ) (see compose_foldl_X_sub_C).

theorem Hex.FpPoly.compose_foldl_X_sub_C {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (xs : List (ZMod64 p)) (init w : FpPoly p) : (List.foldl (fun (acc : DensePoly (ZMod64 p)) (c : ZMod64 p) => acc * (X - C c)) init xs).compose w = List.foldl (fun (acc : DensePoly (ZMod64 p)) (c : ZMod64 p) => acc * (w - C c)) (DensePoly.compose init w) xs

Substituting w into a left-fold product of linear factors ∏ (X - C c) equals the same fold with each X replaced by w. The transport law underlying composition of the prime-field linear product.

theorem Hex.FpPoly.compose_primeFieldLinearProduct {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (w : FpPoly p) : (List.foldl (fun (acc : DensePoly (ZMod64 p)) (c : ZMod64 p) => acc * (X - C c)) 1 (ZMod64.values p)).compose w = List.foldl (fun (acc : DensePoly (ZMod64 p)) (c : ZMod64 p) => acc * (w - C c)) 1 (ZMod64.values p)

Specialisation to the canonical prime-field linear product starting from init = 1: substituting w into the variable form gives the witness form.

theorem Hex.FpPoly.linearPow_zero_of_pos {p : Nat} [ZMod64.Bounds p] (n : Nat) (hn : 0 < n) : linearPow 0 n = 0

A strictly positive power of the zero polynomial is zero. This discharges the vanishing-coefficient case when substituting into the compose power-sum form for the Frobenius identity.

@[simp]

theorem Hex.FpPoly.compose_X_right {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (w : FpPoly p) : DensePoly.compose w X = w

Substituting the polynomial indeterminate into w returns w.

Together with Hex.FpPoly.compose_X, this says that FpPoly.X is the two-sided identity for polynomial composition.

theorem Hex.FpPoly.compose_w_linearPow_X {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (w : FpPoly p) : DensePoly.compose w (X.linearPow p) = w.linearPow p

Compose-form Frobenius: substituting linearPow X p for X in w yields linearPow w p, over F_p. This is Freshman's dream packaged through the polynomial composition surface: viewed as w = ∑_i a_i X^i, the right-hand side equals ∑_i a_i X^(p·i).