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

Polynomial irreducibility over F_p phrased as the absence of nontrivial factorizations inside the executable dense-polynomial model.

Equations

• f.Irreducible = (f ≠ 0 ∧ ∀ (a b : Hex.FpPoly p), a * b = f → Hex.DensePoly.degree? a = some 0 ∨ Hex.DensePoly.degree? b = some 0)

def Hex.FpPoly.ofCoeffs {p : Nat} [ZMod64.Bounds p] (coeffs : Array (ZMod64 p)) : FpPoly p

Build an FpPoly from raw coefficients, trimming trailing zero residues.

Equations

• Hex.FpPoly.ofCoeffs coeffs = Hex.DensePoly.ofCoeffs coeffs

def Hex.FpPoly.C {p : Nat} [ZMod64.Bounds p] (c : ZMod64 p) : FpPoly p

Constant polynomial in F_p[x].

Equations

• Hex.FpPoly.C c = Hex.DensePoly.C c

def Hex.FpPoly.X {p : Nat} [ZMod64.Bounds p] : FpPoly p

The polynomial indeterminate X.

Equations

• Hex.FpPoly.X = Hex.DensePoly.monomial 1 1

def Hex.FpPoly.modByMonic {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) (hmonic : DensePoly.Monic f) : FpPoly p

Reduction modulo a monic polynomial over F_p[x].

Equations

• f.modByMonic g hmonic = Hex.DensePoly.modByMonic g f hmonic

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

The zero polynomial evaluates to zero at every point.

@[simp]

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

A constant polynomial evaluates to its constant at every point. This is the base case from which the evaluation map's homomorphism laws are built.

@[simp]

theorem Hex.FpPoly.eval_X {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (x : ZMod64 p) : DensePoly.eval X x = x

The variable X evaluates to the evaluation point. The companion base case to eval_C for reasoning about the evaluation map.

@[simp]

theorem Hex.FpPoly.eval_monomial {p : Nat} [ZMod64.Bounds p] (n : Nat) (c x : ZMod64 p) : (DensePoly.monomial n c).eval x = c * x ^ n

Evaluating a monomial gives the coefficient times the corresponding power.

@[simp]

theorem Hex.FpPoly.coeff_C {p : Nat} [ZMod64.Bounds p] (c : ZMod64 p) (n : Nat) : DensePoly.coeff (C c) n = if n = 0 then c else 0

Coefficients of the constant polynomial wrapper are constant at degree zero and zero elsewhere.

theorem Hex.FpPoly.coeff_X_zero {p : Nat} [ZMod64.Bounds p] : DensePoly.coeff X 0 = 0

The degree-zero coefficient of the indeterminate wrapper is zero.

theorem Hex.FpPoly.coeff_X_one {p : Nat} [ZMod64.Bounds p] : DensePoly.coeff X 1 = 1

The degree-one coefficient of the indeterminate wrapper is one.

@[simp]

theorem Hex.FpPoly.coeff_X {p : Nat} [ZMod64.Bounds p] (n : Nat) : DensePoly.coeff X n = if n = 1 then 1 else 0

Coefficients of the indeterminate wrapper are one at degree one and zero elsewhere.

theorem Hex.FpPoly.eval_shift_scale_row {p : Nat} [ZMod64.Bounds p] (i : Nat) (c : ZMod64 p) (f : FpPoly p) (x : ZMod64 p) : (DensePoly.shift i (DensePoly.scale c f)).eval x = c * x ^ i * DensePoly.eval f x

Evaluating the monomial row c · Xⁱ · f at x multiplies the value of f by c * xⁱ. This isolates one term of a product so that eval_mul and related multiplicative laws can be assembled row by row.

@[simp]

theorem Hex.FpPoly.eval_add {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 additive: the value of a sum is the sum of the values. One half of the statement that evaluation at a point is a ring homomorphism.

@[simp]

theorem Hex.FpPoly.eval_sub {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 respects subtraction. Lets callers push an evaluation through a difference of polynomials, for example when checking that two polynomials agree at a point.

@[simp]

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

Evaluation respects additive inverses.

@[simp]

theorem Hex.FpPoly.add_zero {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : f + 0 = f

0 is a right identity for addition. Part of the commutative-ring structure on FpPoly p.

@[simp]

theorem Hex.FpPoly.zero_add {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : 0 + f = f

0 is a left identity for addition. Part of the commutative-ring structure on FpPoly p.

theorem Hex.FpPoly.add_comm {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) : f + g = g + f

Polynomial addition is commutative. Part of the commutative-ring structure on FpPoly p that downstream algebra relies on.

theorem Hex.FpPoly.add_assoc {p : Nat} [ZMod64.Bounds p] (f g h : FpPoly p) : f + g + h = f + (g + h)

Polynomial addition is associative, letting callers regroup sums freely. Part of the commutative-ring structure on FpPoly p.

@[simp]

theorem Hex.FpPoly.neg_zero {p : Nat} [ZMod64.Bounds p] : -0 = 0

Negating 0 gives 0.

@[simp]

theorem Hex.FpPoly.add_left_neg {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : -f + f = 0

The negation is a left additive inverse: -f + f = 0.

@[simp]

theorem Hex.FpPoly.add_right_neg {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : f + -f = 0

The negation is a right additive inverse: f + -f = 0.

@[simp]

theorem Hex.FpPoly.sub_zero {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : f - 0 = f

Subtracting 0 leaves a polynomial unchanged.

@[simp]

theorem Hex.FpPoly.zero_sub {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : 0 - f = -f

Subtracting a polynomial from 0 yields its negation.

@[simp]

theorem Hex.FpPoly.sub_self {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : f - f = 0

A polynomial minus itself is 0.

theorem Hex.FpPoly.sub_eq_add_neg {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) : f - g = f + -g

Subtraction unfolds to adding the negation. Rewrites subtraction in terms of the additive operations, so results proved for + transfer to -.

@[simp]

theorem Hex.FpPoly.zero_mul {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : 0 * f = 0

0 is a left absorbing element for multiplication.

@[simp]

theorem Hex.FpPoly.mul_zero {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : f * 0 = 0

0 is a right absorbing element for multiplication.

@[simp]

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

1 is a left identity for multiplication.

@[simp]

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

1 is a right identity for multiplication.

def Hex.FpPoly.mulCoeffTerm {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) (n i : Nat) : ZMod64 p

The ith schoolbook contribution to coefficient n of f * g. Ordinary FpPoly multiplication callers should use coeff_mul, not this definition.

Equations

• f.mulCoeffTerm g n i = if n < i then 0 else Hex.DensePoly.coeff f i * Hex.DensePoly.coeff g (n - i)

def Hex.FpPoly.mulCoeffSum {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) (n : Nat) : ZMod64 p

The executable schoolbook coefficient sum matching FpPoly multiplication. Ordinary FpPoly multiplication callers should use coeff_mul, not this definition.

Equations

• f.mulCoeffSum g n = List.foldl (fun (acc : Hex.ZMod64 p) (i : Nat) => acc + f.mulCoeffTerm g n i) 0 (List.range (Hex.DensePoly.size f))

theorem Hex.FpPoly.coeff_mul {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) (n : Nat) : DensePoly.coeff (f * g) n = f.mulCoeffSum g n

The n-th coefficient of a product is the convolution sum Hex.FpPoly.mulCoeffSum. This is the coefficient-level specification of the executable multiplication, the entry point for proving every higher multiplicative law.

theorem Hex.FpPoly.mul_comm {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) : f * g = g * f

Polynomial multiplication is commutative. Part of the commutative-ring structure on FpPoly p, and lets callers swap factors to match a lemma's expected orientation.

theorem Hex.FpPoly.coeff_mul_shift_scale_one {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (c : ZMod64 p) (i n : Nat) : DensePoly.coeff (f * DensePoly.shift i (DensePoly.scale c 1)) n = if i ≤ n then DensePoly.coeff f (n - i) * c else 0

Multiplying f by the scaled monomial c · Xⁱ shifts each coefficient up by i and scales it by c. Gives a closed form for the coefficients produced when a polynomial is multiplied by a single monomial term.

theorem Hex.FpPoly.left_distrib {p : Nat} [ZMod64.Bounds p] (f g h : FpPoly p) : f * (g + h) = f * g + f * h

Multiplication distributes over addition on the left. Part of the commutative-ring structure on FpPoly p.

theorem Hex.FpPoly.right_distrib {p : Nat} [ZMod64.Bounds p] (f g h : FpPoly p) : (f + g) * h = f * h + g * h

Multiplication distributes over addition on the right. Part of the commutative-ring structure on FpPoly p.

theorem Hex.FpPoly.mul_assoc {p : Nat} [ZMod64.Bounds p] (f g h : FpPoly p) : f * g * h = f * (g * h)

Polynomial multiplication is associative, letting callers regroup products freely. Part of the commutative-ring structure on FpPoly p.

instance Hex.FpPoly.instAssociativeMul {p : Nat} [ZMod64.Bounds p] : Std.Associative fun (x1 x2 : FpPoly p) => x1 * x2

FpPoly p is a multiplicative monoid for Std, so the shared List.foldl_mul_* algebra and the standard List.foldl_assoc apply to fold-products of FpPoly.

instance Hex.FpPoly.instLawfulIdentityMul {p : Nat} [ZMod64.Bounds p] : Std.LawfulIdentity (fun (x1 x2 : FpPoly p) => x1 * x2) 1