theorem Hex.FpPoly.scale_add {p : Nat} [ZMod64.Bounds p] (c : ZMod64 p) (f g : FpPoly p) : DensePoly.scale c (f + g) = DensePoly.scale c f + DensePoly.scale c g

Scalar scaling distributes over polynomial addition. Lets callers move a scalar across a sum, for example when normalizing a linear combination.

theorem Hex.FpPoly.scale_mul_left {p : Nat} [ZMod64.Bounds p] (c : ZMod64 p) (f g : FpPoly p) : DensePoly.scale c (f * g) = DensePoly.scale c f * g

Scaling a product equals scaling its left factor. With mul_comm this lets a scalar be absorbed into either factor of a product.

theorem Hex.FpPoly.scale_one_poly {p : Nat} [ZMod64.Bounds p] (c : ZMod64 p) : DensePoly.scale c 1 = DensePoly.C c

Scaling the unit polynomial by c yields the constant polynomial C c. Identifies the scalar action on 1 with the constant embedding.

theorem Hex.FpPoly.C_mul_eq_scale {p : Nat} [ZMod64.Bounds p] (c : ZMod64 p) (f : FpPoly p) : DensePoly.C c * f = DensePoly.scale c f

Multiplying by a constant polynomial coincides with scalar scaling. Lets callers convert between the C c * f and scale c f representations so the scale-specific lemmas apply to constant multiplications.

theorem Hex.FpPoly.eval_C_mul {p : Nat} [ZMod64.Bounds p] (c : ZMod64 p) (f : FpPoly p) (x : ZMod64 p) : (DensePoly.C c * f).eval x = c * DensePoly.eval f x

Evaluating C c * f at x multiplies the value of f by the scalar c. The constant-multiplication special case of eval_mul.

@[simp]

theorem Hex.FpPoly.eval_one {p : Nat} [ZMod64.Bounds p] (x : ZMod64 p) : DensePoly.eval 1 x = 1

Evaluating the constant polynomial 1 at any point gives 1.

@[simp]

theorem Hex.FpPoly.eval_mul {p : Nat} [ZMod64.Bounds p] (f h : FpPoly p) (x : ZMod64 p) : DensePoly.eval (f * h) x = DensePoly.eval f x * DensePoly.eval h x

Evaluation is multiplicative: the value of a product is the product of the values. Together with eval_add this is the ring-homomorphism property of evaluation, used wherever a root or factorization is checked pointwise.

theorem Hex.FpPoly.scale_scale {p : Nat} [ZMod64.Bounds p] (c d : ZMod64 p) (f : FpPoly p) : DensePoly.scale c (DensePoly.scale d f) = DensePoly.scale (c * d) f

Two successive scalings compose into a single scaling by the product of the scalars. Lets callers collapse a chain of scalar adjustments into one.

theorem Hex.FpPoly.scale_one_left {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : DensePoly.scale 1 f = f

Scaling by 1 leaves the polynomial unchanged. The identity law of the scalar action, needed to recognize a trivial scaling as a no-op.

theorem Hex.FpPoly.scale_size_le {p : Nat} [ZMod64.Bounds p] (c : ZMod64 p) (f : FpPoly p) : (DensePoly.scale c f).size ≤ DensePoly.size f

Scaling never increases the coefficient-array size. The unconditional size bound, valid even when c = 0 collapses leading coefficients to zero.

theorem Hex.FpPoly.scale_size_eq_of_ne_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {c : ZMod64 p} (hc : c ≠ 0) (f : FpPoly p) : (DensePoly.scale c f).size = DensePoly.size f

Scaling by a nonzero scalar preserves the coefficient-array size: over a field the top coefficient cannot be cancelled. Callers use this to know that a unit scaling preserves degree.

theorem Hex.FpPoly.scale_degree?_eq_of_ne_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {c : ZMod64 p} (hc : c ≠ 0) (f : FpPoly p) : (DensePoly.scale c f).degree? = DensePoly.degree? f

Scaling by a nonzero scalar preserves the optional degree. The degree-level counterpart of scale_size_eq_of_ne_zero, used when reasoning in terms of degree? rather than size.

theorem Hex.FpPoly.scale_degree?_getD_eq_of_ne_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {c : ZMod64 p} (hc : c ≠ 0) (f : FpPoly p) : (DensePoly.scale c f).natDegree = DensePoly.natDegree f

Nonzero scaling preserves the degree in the natDegree form callers commonly carry, sparing them an Option unfolding at each use site.

theorem Hex.FpPoly.leadingCoeff_eq_coeff_pred {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (_hpos : 0 < DensePoly.size f) : DensePoly.leadingCoeff f = DensePoly.coeff f (DensePoly.size f - 1)

For a nonempty polynomial the leading coefficient is the coefficient at the top index size - 1. Gives callers a concrete index for the leading coefficient when they need to compute or rewrite it.

theorem Hex.FpPoly.leadingCoeff_ne_zero_of_pos_degree {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hpos : 0 < DensePoly.natDegree f) : DensePoly.leadingCoeff f ≠ 0

A polynomial of positive degree has a nonzero leading coefficient. The nondegeneracy fact that justifies inverting the leading coefficient during monic normalization.

theorem Hex.FpPoly.leadingCoeff_scale_of_ne_zero_of_pos_degree {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {c : ZMod64 p} (hc : c ≠ 0) (f : FpPoly p) (hpos : 0 < DensePoly.natDegree f) : (DensePoly.scale c f).leadingCoeff = c * DensePoly.leadingCoeff f

For a nonzero scalar and a positive-degree polynomial the leading coefficient scales by c. Lets callers track how the leading coefficient moves under a unit scaling, the key step in computing a monic-normalizing scalar.

theorem Hex.FpPoly.leadingCoeff_scale_of_ne_zero_of_nonzero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {c : ZMod64 p} (hc : c ≠ 0) (f : FpPoly p) (hfsize : DensePoly.size f ≠ 0) : (DensePoly.scale c f).leadingCoeff = c * DensePoly.leadingCoeff f

The same leading-coefficient scaling law as leadingCoeff_scale_of_ne_zero_of_pos_degree, stated from the weaker nonempty hypothesis f.size ≠ 0 so it applies to constants as well as higher-degree polynomials.

theorem Hex.FpPoly.scale_inv_leadingCoeff_monic {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hpos : 0 < DensePoly.natDegree f) : (DensePoly.scale (DensePoly.leadingCoeff f)⁻¹ f).Monic

Scaling a positive-degree polynomial by the inverse of its leading coefficient produces a monic polynomial. This is the monic-normalization step that puts a polynomial into the canonical leading-1 form.

theorem Hex.FpPoly.irreducible_scale_iff_of_ne_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {c : ZMod64 p} (hc : c ≠ 0) (f : FpPoly p) : Irreducible (DensePoly.scale c f) ↔ f.Irreducible

Scaling by a nonzero (hence unit) scalar preserves irreducibility in both directions. Lets callers normalize a polynomial to monic form without changing whether it is irreducible.

theorem Hex.FpPoly.irreducible_scale_of_ne_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {c : ZMod64 p} (hc : c ≠ 0) {f : FpPoly p} (hf : f.Irreducible) : Irreducible (DensePoly.scale c f)

Forward direction of irreducible_scale_iff_of_ne_zero: a nonzero scaling of an irreducible polynomial is irreducible. The convenient form when the hypothesis is irreducibility of the unscaled polynomial.

theorem Hex.FpPoly.irreducible_of_scale_of_ne_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {c : ZMod64 p} (hc : c ≠ 0) {f : FpPoly p} (hf : Irreducible (DensePoly.scale c f)) : f.Irreducible

Reverse direction of irreducible_scale_iff_of_ne_zero: if a nonzero scaling is irreducible then so is the unscaled polynomial. Lets callers transfer irreducibility back from a normalized representative.

theorem Hex.FpPoly.dvd_scale_of_dvd {p : Nat} [ZMod64.Bounds p] {c : ZMod64 p} {f g : FpPoly p} (hfg : f ∣ g) : DensePoly.scale c f ∣ DensePoly.scale c g

Divisibility is preserved when both sides are scaled by the same scalar. Holds for any c, so callers can scale a divisibility relation without a nonzero hypothesis.

theorem Hex.FpPoly.dvd_of_scale_dvd {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {c : ZMod64 p} (hc : c ≠ 0) {f g : FpPoly p} (hfg : DensePoly.scale c f ∣ DensePoly.scale c g) : f ∣ g

Converse of dvd_scale_of_dvd for a nonzero scalar: a divisibility between equally scaled polynomials reflects back to the originals. Lets callers strip a common unit scaling from both sides of a divisibility.

theorem Hex.FpPoly.dvd_scale_self_of_ne_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {c : ZMod64 p} (hc : c ≠ 0) (f : FpPoly p) : DensePoly.scale c f ∣ f

A nonzero scaling of f divides f itself: scaling by a unit produces an associate. Lets callers treat a unit-scaled polynomial and the original as mutually divisible.

theorem Hex.FpPoly.degree?_mul_eq_add_degree? {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (a b : FpPoly p) (ha : a ≠ 0) (hb : b ≠ 0) : DensePoly.natDegree (a * b) = DensePoly.natDegree a + DensePoly.natDegree b

Over a prime modulus, the degree of a product of nonzero polynomials in FpPoly p equals the sum of the degrees. This is the no-zero-divisors identity expressed at the level of natDegree.

theorem Hex.FpPoly.size_pos_of_ne_zero {p : Nat} [ZMod64.Bounds p] {f : FpPoly p} (hf : f ≠ 0) : 0 < DensePoly.size f

An FpPoly p polynomial is nonzero exactly when its stored coefficient array is nonempty.

theorem Hex.FpPoly.size_mul_eq_add_sub_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (a b : FpPoly p) (ha : a ≠ 0) (hb : b ≠ 0) : DensePoly.size (a * b) = DensePoly.size a + DensePoly.size b - 1

Over a prime modulus, the executable size of a product of two nonzero polynomials in FpPoly p is the sum of their sizes minus one. This is the no-zero-divisors identity at the level of DensePoly.size.

theorem Hex.FpPoly.mul_ne_zero_of_ne_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {a b : FpPoly p} (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0

Over a prime modulus, multiplying two nonzero polynomials in FpPoly p gives a nonzero polynomial: prime-field polynomials form an integral domain.

theorem Hex.FpPoly.leadingCoeff_mul {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (a b : FpPoly p) (ha : a ≠ 0) (hb : b ≠ 0) : DensePoly.leadingCoeff (a * b) = DensePoly.leadingCoeff a * DensePoly.leadingCoeff b

Leading coefficient of a product equals the product of leading coefficients on nonzero FpPoly p factors: the top-coefficient lemma coeff_mul_at_top plus the size identity size_mul_eq_add_sub_one give this directly.

theorem Hex.FpPoly.mul_right_cancel_of_ne_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {a b c : FpPoly p} (hc : c ≠ 0) (h : a * c = b * c) : a = b

Right cancellation for multiplication by a nonzero FpPoly p polynomial.

theorem Hex.FpPoly.size_le_of_dvd_of_ne_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {a b : FpPoly p} (hab : a ∣ b) (hb : b ≠ 0) : DensePoly.size a ≤ DensePoly.size b

Over a prime modulus, divisibility implies a size bound: if a ∣ b and b ≠ 0, then a.size ≤ b.size. The standard polynomial fact that a divisor has degree at most the degree of the dividend, expressed at the level of DensePoly.size.

theorem Hex.FpPoly.size_div_add_size_eq_size_add_one_of_dvd {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {c d : FpPoly p} (hdc : d ∣ c) (hc : c ≠ 0) : DensePoly.size (c / d) + DensePoly.size d = DensePoly.size c + 1

Over a prime modulus, when d divides a nonzero polynomial c, the executable sizes satisfy (c / d).size + d.size = c.size + 1. This is degree-additivity for exact division translated to the size indexing.

theorem Hex.FpPoly.size_div_lt_of_size_gcd_pos {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (c w : FpPoly p) (hgcd_pos : 1 < (DensePoly.gcd c w).size) (hc : DensePoly.isZero c = false) : DensePoly.size (c / DensePoly.gcd c w) < DensePoly.size c

Specialised quotient-size strict decrease: if gcd c w is nonconstant (size ≥ 2) and c ≠ 0, then c / gcd c w has strictly smaller size than c. This is the size-strict descent step that powers Yun-style square-free decomposition termination.

theorem Hex.FpPoly.eq_one_of_monic_dvd_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g : FpPoly p} (hmonic : DensePoly.Monic g) (hdiv : g ∣ 1) : g = 1

A monic finite-field polynomial that divides the unit polynomial is the unit polynomial.

theorem Hex.FpPoly.gcd_eq_one_of_monic_of_common_dvd_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (a b : FpPoly p) (hmonic : (DensePoly.gcd a b).Monic) (hcommon : ∀ (d : FpPoly p), d ∣ a → d ∣ b → d ∣ 1) : DensePoly.gcd a b = 1

Turn the executable gcd into the equality gcd a b = 1 once the gcd is known monic and every common divisor of a and b divides 1.

theorem Hex.FpPoly.dvd_of_dvd_mul_of_common_dvd_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {g c h : FpPoly p} (hdvd : g ∣ c * h) (hcoprime : ∀ (d : FpPoly p), d ∣ c → d ∣ g → d ∣ 1) : g ∣ h

Bezout-style coprime cancellation for FpPoly p. If g ∣ c * h and every common divisor of c and g divides the unit polynomial 1, then g ∣ h.

The proof uses the extended Euclidean algorithm DensePoly.xgcd: from the Bezout identity r.left * c + r.right * g = DensePoly.gcd c g and the fact that DensePoly.gcd c g ∣ 1 (via the coprime hypothesis), one concludes that g divides h.

theorem Hex.FpPoly.coeff_monomial_mul {p : Nat} [ZMod64.Bounds p] (k : Nat) (c : ZMod64 p) (g : FpPoly p) (n : Nat) : (DensePoly.monomial k c * g).coeff n = if n < k then 0 else c * DensePoly.coeff g (n - k)

Coefficient of monomial k c * g at degree n: zero below k, c · g[n-k] above.

theorem Hex.FpPoly.X_sub_C_dvd_of_eval_eq_zero {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (c : ZMod64 p) (hroot : DensePoly.eval f c = 0) : X - C c ∣ f

If c is a scalar root of f, then the linear factor X - C c divides f.

theorem Hex.FpPoly.monomial_mul_monomial {p : Nat} [ZMod64.Bounds p] (m n : Nat) : DensePoly.monomial m 1 * DensePoly.monomial n 1 = DensePoly.monomial (m + n) 1

Multiplying two monic monomials adds their exponents.

theorem Hex.FpPoly.monomial_zero_one_eq_one {p : Nat} [ZMod64.Bounds p] : DensePoly.monomial 0 1 = 1

The constant 1 polynomial agrees with the zero-degree monic monomial.

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

Linear polynomial exponentiation by repeated right-multiplication. This is the building block for the geometric-series identity used by the xPowSubX divisibility chain.

Equations

• f.linearPow 0 = 1
• f.linearPow n.succ = f.linearPow n * f

@[simp]

theorem Hex.FpPoly.linearPow_zero {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : f.linearPow 0 = 1

The zeroth power is the multiplicative identity 1. Base case pairing with linearPow_succ.

@[simp]

theorem Hex.FpPoly.linearPow_succ {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (n : Nat) : f.linearPow (n + 1) = f.linearPow n * f

Successor exponents append one right multiplication by the base.

theorem Hex.FpPoly.linearPow_succ_left {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (n : Nat) : f.linearPow (n + 1) = f * f.linearPow n

Successor exponents may also be read as one left multiplication by the base.

theorem Hex.FpPoly.linearPow_one {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : f.linearPow 1 = f

The first linearPow of a polynomial is the polynomial itself.

theorem Hex.FpPoly.linearPow_add {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (m n : Nat) : f.linearPow (m + n) = f.linearPow m * f.linearPow n

linearPow turns exponent addition into polynomial multiplication.

theorem Hex.FpPoly.linearPow_iterate_mul {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (m n : Nat) : (f.linearPow m).linearPow n = f.linearPow (m * n)

Iterated linearPow multiplies exponents.

theorem Hex.FpPoly.eval_linearPow {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (n : Nat) (x : ZMod64 p) : DensePoly.eval (f.linearPow n) x = DensePoly.eval f x ^ n

Scalar evaluation distributes over linearPow: eval (f^n) x = (eval f x)^n.

theorem Hex.FpPoly.linearPow_monomial {p : Nat} [ZMod64.Bounds p] (k n : Nat) : linearPow (DensePoly.monomial k 1) n = DensePoly.monomial (k * n) 1

linearPow (monomial k 1) n = monomial (k * n) 1.

theorem Hex.FpPoly.linearPow_monomial_one {p : Nat} [ZMod64.Bounds p] (n : Nat) : linearPow (DensePoly.monomial 1 1) n = DensePoly.monomial n 1

linearPow (monomial 1 1) n = monomial n 1.

theorem Hex.FpPoly.linearPow_X {p : Nat} [ZMod64.Bounds p] (n : Nat) : X.linearPow n = DensePoly.monomial n 1

linearPow X n is the degree-n monomial.

theorem Hex.FpPoly.linearPow_C {p : Nat} [ZMod64.Bounds p] (c : ZMod64 p) (n : Nat) : (C c).linearPow n = C (c ^ n)

linearPow of a constant polynomial stays constant.

theorem Hex.FpPoly.sub_one_dvd_linearPow_sub_one {p : Nat} [ZMod64.Bounds p] (Y : FpPoly p) (j : Nat) : Y - 1 ∣ Y.linearPow j - 1

Geometric-series divisibility: Y - 1 ∣ Y^j - 1.

theorem Hex.FpPoly.monomial_sub_one_dvd_of_dvd {p : Nat} [ZMod64.Bounds p] {k l : Nat} (hdvd : k ∣ l) : DensePoly.monomial k 1 - 1 ∣ DensePoly.monomial l 1 - 1

Geometric-series divisibility for monomials: when k ∣ l, (monomial k 1 - 1) ∣ (monomial l 1 - 1).