def Hex.GF2nPoly.evalCoeffList {f : GF2Poly} {hirr : f.Irreducible} : List (GF2nPoly f hirr) → GF2nPoly f hirr → GF2nPoly f hirr

Evaluate a low-to-high quotient-coefficient list at a quotient point.

The list [c₀, c₁, ...] denotes c₀ + β * (c₁ + β * (...)). This proof-facing evaluator is separate from executable packed polynomial evaluation; it is used by quotient-field root-count arguments.

Equations

• Hex.GF2nPoly.evalCoeffList [] x✝ = 0
• Hex.GF2nPoly.evalCoeffList (c :: cs) x✝ = c + x✝ * Hex.GF2nPoly.evalCoeffList cs x✝

@[simp]

theorem Hex.GF2nPoly.evalCoeffList_nil {f : GF2Poly} {hirr : f.Irreducible} (β : GF2nPoly f hirr) : evalCoeffList [] β = 0

Evaluating the empty coefficient list yields 0.

@[simp]

theorem Hex.GF2nPoly.evalCoeffList_cons {f : GF2Poly} {hirr : f.Irreducible} (c : GF2nPoly f hirr) (cs : List (GF2nPoly f hirr)) (β : GF2nPoly f hirr) : evalCoeffList (c :: cs) β = c + β * evalCoeffList cs β

Horner recursion equation: evaluating c :: cs at β peels off the head coefficient c and folds the tail through one more multiplication by β.

def Hex.GF2nPoly.Internal.dividedDifferenceCoeffs {f : GF2Poly} {hirr : f.Irreducible} : List (GF2nPoly f hirr) → GF2nPoly f hirr → List (GF2nPoly f hirr)

Internal root-count helper: synthetic quotient coefficients for the divided difference of cs at the base point α.

If P is represented by cs, this list represents the quotient (P(T) + P(α)) / (T + α) in characteristic two. Its length is one less than the input list, which is the measure used by root-count induction.

Equations

• Hex.GF2nPoly.Internal.dividedDifferenceCoeffs [] x✝ = []
• Hex.GF2nPoly.Internal.dividedDifferenceCoeffs [head] x✝ = []
• Hex.GF2nPoly.Internal.dividedDifferenceCoeffs (head :: c :: cs) x✝ = Hex.GF2nPoly.evalCoeffList (c :: cs) x✝ :: Hex.GF2nPoly.Internal.dividedDifferenceCoeffs (c :: cs) x✝

@[simp]

theorem Hex.GF2nPoly.Internal.dividedDifferenceCoeffs_nil {f : GF2Poly} {hirr : f.Irreducible} (α : GF2nPoly f hirr) : dividedDifferenceCoeffs [] α = []

The divided-difference coefficient list of the zero polynomial is empty.

@[simp]

theorem Hex.GF2nPoly.Internal.dividedDifferenceCoeffs_singleton {f : GF2Poly} {hirr : f.Irreducible} (c α : GF2nPoly f hirr) : dividedDifferenceCoeffs [c] α = []

A constant coefficient list has no divided-difference coefficients.

@[simp]

theorem Hex.GF2nPoly.Internal.dividedDifferenceCoeffs_cons_cons {f : GF2Poly} {hirr : f.Irreducible} (c d : GF2nPoly f hirr) (cs : List (GF2nPoly f hirr)) (α : GF2nPoly f hirr) : dividedDifferenceCoeffs (c :: d :: cs) α = evalCoeffList (d :: cs) α :: dividedDifferenceCoeffs (d :: cs) α

Divided differences peel the tail polynomial evaluated at the base point.

@[simp]

theorem Hex.GF2nPoly.Internal.dividedDifferenceCoeffs_length {f : GF2Poly} {hirr : f.Irreducible} (cs : List (GF2nPoly f hirr)) (α : GF2nPoly f hirr) : (dividedDifferenceCoeffs cs α).length = cs.length - 1

The synthetic divided-difference coefficient list has one fewer entry.

def Hex.GF2nPoly.Internal.dividedDifference {f : GF2Poly} {hirr : f.Irreducible} (cs : List (GF2nPoly f hirr)) (α β : GF2nPoly f hirr) : GF2nPoly f hirr

Internal root-count helper: evaluate the divided difference of a quotient-coefficient polynomial between the base point α and target point β.

Equations

• Hex.GF2nPoly.Internal.dividedDifference cs α β = Hex.GF2nPoly.evalCoeffList (Hex.GF2nPoly.Internal.dividedDifferenceCoeffs cs α) β

@[simp]

theorem Hex.GF2nPoly.Internal.dividedDifference_nil {f : GF2Poly} {hirr : f.Irreducible} (α β : GF2nPoly f hirr) : dividedDifference [] α β = 0

The divided difference of an empty coefficient list is zero.

@[simp]

theorem Hex.GF2nPoly.Internal.dividedDifference_cons {f : GF2Poly} {hirr : f.Irreducible} (c d : GF2nPoly f hirr) (cs : List (GF2nPoly f hirr)) (α β : GF2nPoly f hirr) : dividedDifference (c :: d :: cs) α β = evalCoeffList (d :: cs) α + β * dividedDifference (d :: cs) α β

The divided difference of a nonconstant list satisfies the synthetic recurrence used by the root-count induction.

theorem Hex.GF2nPoly.Internal.evalCoeffList_add_evalCoeffList_eq_add_mul_dividedDifference {f : GF2Poly} {hirr : f.Irreducible} (cs : List (GF2nPoly f hirr)) (α β : GF2nPoly f hirr) : evalCoeffList cs β + evalCoeffList cs α = (β + α) * dividedDifference cs α β

The quotient-coefficient divided difference satisfies P(β) + P(α) = (β + α) * DD(P, α, β).

This is the characteristic-two orientation of the usual P(β) - P(α) = (β - α) * Q(β) identity, and is the API consumed by the root-count induction.

theorem Hex.GF2nPoly.frobeniusIter_mul {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) (k : Nat) : (a * b).frobeniusIter k = a.frobeniusIter k * b.frobeniusIter k

Iterated Frobenius preserves multiplication in the packed quotient.

theorem Hex.GF2nPoly.frobeniusIter_add_eq {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) (k : Nat) : (a + b).frobeniusIter k = a.frobeniusIter k + b.frobeniusIter k

Iterated Frobenius preserves addition in the packed quotient.

@[simp]

theorem Hex.GF2nPoly.frobeniusIter_zero_eq {f : GF2Poly} {hirr : f.Irreducible} (k : Nat) : frobeniusIter 0 k = 0

Zero is fixed by every iterated Frobenius.

theorem Hex.GF2nPoly.frobeniusIter_fixed_add {f : GF2Poly} {hirr : f.Irreducible} {a b : GF2nPoly f hirr} {k : Nat} (ha : a.frobeniusIter k = a) (hb : b.frobeniusIter k = b) : (a + b).frobeniusIter k = a + b

Fixed packed quotient elements are closed under addition for a shared Frobenius iterate.

theorem Hex.GF2nPoly.frobeniusIter_fixed_mul {f : GF2Poly} {hirr : f.Irreducible} {a b : GF2nPoly f hirr} {k : Nat} (ha : a.frobeniusIter k = a) (hb : b.frobeniusIter k = b) : (a * b).frobeniusIter k = a * b

Fixed packed quotient elements are closed under multiplication for a shared Frobenius iterate.

@[simp]

theorem Hex.GF2nPoly.frobeniusIter_one_eq {f : GF2Poly} {hirr : f.Irreducible} (k : Nat) : frobeniusIter 1 k = 1

One is fixed by every iterated Frobenius.

@[simp]

theorem Hex.GF2nPoly.reducePoly_monomial_zero {f : GF2Poly} {hirr : f.Irreducible} : reducePoly (GF2Poly.monomial 0) = 1

Reducing the constant-one monomial gives the quotient one.

theorem Hex.GF2nPoly.frobeniusIter_reducePoly_monomial_eq_self_of_X_fixed {f : GF2Poly} {hirr : f.Irreducible} {k : Nat} (hX : X.frobeniusIter k = X) (n : Nat) : (reducePoly (GF2Poly.monomial n)).frobeniusIter k = reducePoly (GF2Poly.monomial n)

If the quotient class of X is fixed by a Frobenius iterate, then every monomial quotient class is fixed by the same iterate.

theorem Hex.GF2nPoly.frobeniusIter_reducePoly_ofBoolListFrom_eq_self_of_X_fixed {f : GF2Poly} {hirr : f.Irreducible} {k : Nat} (hX : X.frobeniusIter k = X) (start : Nat) (bs : List Bool) : (reducePoly (GF2Poly.Internal.ofBoolListFrom start bs)).frobeniusIter k = reducePoly (GF2Poly.Internal.ofBoolListFrom start bs)

If the quotient class of X is fixed by a Frobenius iterate, then any Boolean coefficient list starting at an arbitrary monomial degree is fixed.

theorem Hex.GF2nPoly.frobeniusIter_boolListExpression_eq_self_of_X_fixed {f : GF2Poly} {hirr : f.Irreducible} {k : Nat} (hX : X.frobeniusIter k = X) (bs : List Bool) : (boolListExpression bs).frobeniusIter k = boolListExpression bs

If the quotient class of X is fixed by a Frobenius iterate, then every Boolean coefficient expression generated from X is fixed.

theorem Hex.GF2nPoly.frobeniusIter_eq_self_of_X_fixed {f : GF2Poly} {hirr : f.Irreducible} {k : Nat} (hX : X.frobeniusIter k = X) (a : GF2nPoly f hirr) : a.frobeniusIter k = a

If the quotient class of X is fixed by a Frobenius iterate, then every packed quotient-field element is fixed by the same iterate.

theorem Hex.GF2nPoly.inv_mul_cancel {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) (ha : a ≠ 0) : a⁻¹ * a = 1

The inverse cancels on the left for nonzero quotient elements.

theorem Hex.GF2nPoly.mul_ne_zero_of_ne_zero {f : GF2Poly} {hirr : f.Irreducible} {a b : GF2nPoly f hirr} (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0

The product of two nonzero packed quotient elements is nonzero.

theorem Hex.GF2nPoly.mul_left_injective {f : GF2Poly} {hirr : f.Irreducible} {a : GF2nPoly f hirr} (ha : a ≠ 0) {b₁ b₂ : GF2nPoly f hirr} (heq : a * b₁ = a * b₂) : b₁ = b₂

Left multiplication by a nonzero packed quotient element is injective.

def Hex.GF2nPoly.Internal.coeffListTopNonzero {f : GF2Poly} {hirr : f.Irreducible} : List (GF2nPoly f hirr) → Prop

The highest coefficient in a low-to-high quotient coefficient list is nonzero.

This predicate gives the syntactic degree bound consumed by the root-count theorem: a list satisfying it represents a polynomial of degree strictly below the list length, with actual degree exactly length - 1.

Equations

• Hex.GF2nPoly.Internal.coeffListTopNonzero x✝ = ∃ (c : Hex.GF2nPoly f hirr), x✝.getLast? = some c ∧ c ≠ 0

def Hex.GF2nPoly.Internal.rootsOfCoeffList {f : GF2Poly} {hirr : f.Irreducible} (cs : List (GF2nPoly f hirr)) : List (GF2nPoly f hirr)

Internal root-count helper: roots of a quotient-coefficient polynomial inside the canonical quotient enumeration.

Equations

• Hex.GF2nPoly.Internal.rootsOfCoeffList cs = List.filter (fun (β : Hex.GF2nPoly f hirr) => decide (Hex.GF2nPoly.evalCoeffList cs β = 0)) Hex.GF2nPoly.elements

@[simp]

theorem Hex.GF2nPoly.Internal.mem_rootsOfCoeffList {f : GF2Poly} {hirr : f.Irreducible} (cs : List (GF2nPoly f hirr)) (β : GF2nPoly f hirr) : β ∈ rootsOfCoeffList cs ↔ evalCoeffList cs β = 0

Membership in the computed root list is exactly vanishing of the coefficient-list polynomial at that quotient element.

theorem Hex.GF2nPoly.Internal.rootsOfCoeffList_nodup {f : GF2Poly} {hirr : f.Irreducible} (cs : List (GF2nPoly f hirr)) : (rootsOfCoeffList cs).Nodup

The quotient-coefficient root list has no duplicate roots.

theorem Hex.GF2nPoly.Internal.rootsOfCoeffList_length_le_degree {f : GF2Poly} {hirr : f.Irreducible} (cs : List (GF2nPoly f hirr)) (htop : coeffListTopNonzero cs) : (rootsOfCoeffList cs).length ≤ cs.length - 1

A nonzero quotient-coefficient polynomial has at most its degree many roots in the duplicate-free packed quotient enumeration.

The coefficient list is low-to-high, and coeffListTopNonzero cs says the highest listed coefficient is nonzero, so the degree bound is cs.length - 1.

theorem Hex.GF2nPoly.Internal.evalCoeffList_rootsIn_elements_length_le_degree {f : GF2Poly} {hirr : f.Irreducible} (cs : List (GF2nPoly f hirr)) (htop : coeffListTopNonzero cs) : (List.filter (fun (β : GF2nPoly f hirr) => decide (evalCoeffList cs β = 0)) elements).length ≤ cs.length - 1

Direct root-count bound for the canonical elements filter form used by callers.

theorem Hex.GF2nPoly.nonzeroElements_map_mul_left_perm {f : GF2Poly} {hirr : f.Irreducible} {a : GF2nPoly f hirr} (ha : a ≠ 0) : (List.map (fun (b : GF2nPoly f hirr) => a * b) nonzeroElements).Perm nonzeroElements

Multiplication by a nonzero packed quotient element permutes the nonzero enumeration. The list of nonzero elements multiplied on the left by a is a permutation of the original nonzero list.

def Hex.GF2nPoly.Internal.linearPow {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : Nat → GF2nPoly f hirr

Internal proof-facing linear natural powers in the packed quotient field. This variant has simple recursion equations; executable exponentiation remains the Pow instance above.

Equations

• Hex.GF2nPoly.Internal.linearPow a 0 = 1
• Hex.GF2nPoly.Internal.linearPow a n.succ = Hex.GF2nPoly.Internal.linearPow a n * a

@[simp]

theorem Hex.GF2nPoly.Internal.linearPow_zero {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : linearPow a 0 = 1

Base case of proof-facing linear exponentiation: the zeroth power is 1.

@[simp]

theorem Hex.GF2nPoly.Internal.linearPow_succ {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) (n : Nat) : linearPow a (n + 1) = linearPow a n * a

Recursion equation for proof-facing linear exponentiation: each successor power multiplies the previous power by one more factor of a.

theorem Hex.GF2nPoly.Internal.linearPow_add {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) (m n : Nat) : linearPow a (m + n) = linearPow a m * linearPow a n

Linear quotient powers turn addition of exponents into multiplication.

theorem Hex.GF2nPoly.Internal.linearPow_double {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) (n : Nat) : linearPow (a * a) n = linearPow a (2 * n)

Doubling an exponent squares the base, in the linear reference form.

theorem Hex.GF2nPoly.Internal.linearPow_double_add_one {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) (n : Nat) : a * linearPow (a * a) n = linearPow a (2 * n + 1)

The odd-exponent companion of Hex.GF2nPoly.Internal.linearPow_double.

theorem Hex.GF2nPoly.Internal.pow_go_eq_acc_mul_linearPow {f : GF2Poly} {hirr : f.Irreducible} (acc base : GF2nPoly f hirr) (k : Nat) : pow.go acc base k = acc * linearPow base k

The executable square-and-multiply accumulator computes acc * base ^ k.

This is the invariant that ties the fast Pow instance to the linear reference: the loop halves the exponent and squares the base, so the accumulator carries exactly the factors already consumed.

theorem Hex.GF2nPoly.Internal.pow_eq_linearPow {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) (n : Nat) : a ^ n = linearPow a n

The executable square-and-multiply power agrees with the linear reference.

theorem Hex.GF2nPoly.Internal.linearPow_mul {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) (n : Nat) : linearPow (a * b) n = linearPow a n * linearPow b n

Linear powers of a product factor in the commutative packed quotient.

theorem Hex.GF2nPoly.Internal.frobeniusIter_eq_linearPow_two_pow {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) (k : Nat) : a.frobeniusIter k = linearPow a (2 ^ k)

Iterated Frobenius squaring agrees with linear powering by 2^k.

def Hex.GF2nPoly.frobeniusFixedCoeffList {f : GF2Poly} {hirr : f.Irreducible} (k : Nat) : List (GF2nPoly f hirr)

Coefficients for the characteristic-two polynomial T^(2^k) + T.

For 0 < k, the list is low-to-high with nonzero coefficients exactly at degrees 1 and 2^k. The k = 0 list intentionally evaluates to zero, matching T + T; root-count callers use the positive-k theorem below.

Equations

• Hex.GF2nPoly.frobeniusFixedCoeffList k = if k = 0 then [0] else 0 :: 1 :: (List.replicate (2 ^ k - 2) 0 ++ [1])

theorem Hex.GF2nPoly.frobeniusIter_fixed_elements_length_le_two_pow {f : GF2Poly} {hirr : f.Irreducible} (hf_pos : 0 < f.natDegree) {k : Nat} (hk : 0 < k) : (List.filter (fun (β : GF2nPoly f hirr) => decide (β.frobeniusIter k = β)) elements).length ≤ 2 ^ k

At most 2^k packed quotient elements are fixed by the k-fold Frobenius when 0 < k.

This is the root-count specialization for T^(2^k) + T, stated directly against the canonical duplicate-free elements enumeration so downstream Rabin arguments can combine it with elements_card.

theorem Hex.GF2nPoly.frobeniusIter_universal_fixed_degree_le {f : GF2Poly} {hirr : f.Irreducible} (hf_pos : 0 < f.natDegree) {k : Nat} (hk : 0 < k) (hfixed : ∀ (β : GF2nPoly f hirr), β.frobeniusIter k = β) : f.natDegree ≤ k

If every packed quotient element is fixed by a positive Frobenius iterate, then the iterate is at least the modulus degree.

This is the downstream cardinality form of the fixed-root bound: otherwise all 2^f.natDegree quotient elements would be roots of T^(2^k) + T, whose packed root-count bound is only 2^k.

theorem Hex.GF2nPoly.not_forall_frobeniusIter_eq_self_of_pos_lt_degree {f : GF2Poly} {hirr : f.Irreducible} (hf_pos : 0 < f.natDegree) {r : Nat} (hr_pos : 0 < r) (hr_lt : r < f.natDegree) : ¬∀ (β : GF2nPoly f hirr), β.frobeniusIter r = β

For a positive iterate below the packed quotient degree, not every quotient element can be fixed by Frobenius.

This contrapositive is the form Rabin soundness uses after reducing an exponent modulo the irreducible factor degree.

theorem Hex.GF2nPoly.exists_frobeniusIter_ne_self_of_pos_lt_degree {f : GF2Poly} {hirr : f.Irreducible} (hf_pos : 0 < f.natDegree) {r : Nat} (hr_pos : 0 < r) (hr_lt : r < f.natDegree) : ∃ (β : GF2nPoly f hirr), β.frobeniusIter r ≠ β

A positive iterate below the quotient degree has some non-fixed element.

theorem Hex.GF2nPoly.frobeniusIter_X_ne_self_of_pos_lt_degree {f : GF2Poly} {hirr : f.Irreducible} (hf_pos : 0 < f.natDegree) {r : Nat} (hr_pos : 0 < r) (hr_lt : r < f.natDegree) : X.frobeniusIter r ≠ X

For a positive iterate below the quotient degree, the quotient class of X cannot be fixed by Frobenius.

If X were fixed, the existing quotient-generation theorem would make every element fixed, contradicting the fixed-point cardinality bound.

def Hex.GF2nPoly.Internal.listProd {f : GF2Poly} {hirr : f.Irreducible} (xs : List (GF2nPoly f hirr)) : GF2nPoly f hirr

Internal proof-facing product of a list of packed quotient elements (right fold), used with the canonical nonzero quotient enumeration.

Equations

• Hex.GF2nPoly.Internal.listProd xs = List.foldr (fun (x1 x2 : Hex.GF2nPoly f hirr) => x1 * x2) 1 xs

@[simp]

theorem Hex.GF2nPoly.Internal.listProd_nil {f : GF2Poly} {hirr : f.Irreducible} : listProd [] = 1

The right-folded product of the empty quotient-element list is one.

@[simp]

theorem Hex.GF2nPoly.Internal.listProd_cons {f : GF2Poly} {hirr : f.Irreducible} (x : GF2nPoly f hirr) (xs : List (GF2nPoly f hirr)) : listProd (x :: xs) = x * listProd xs

The right-folded product of a cons multiplies the head by the tail product.

theorem Hex.GF2nPoly.Internal.listProd_perm {f : GF2Poly} {hirr : f.Irreducible} {xs ys : List (GF2nPoly f hirr)} (h : xs.Perm ys) : listProd xs = listProd ys

The list product is invariant under List.Perm.

theorem Hex.GF2nPoly.Internal.listProd_map_mul_left {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) (xs : List (GF2nPoly f hirr)) : listProd (List.map (fun (b : GF2nPoly f hirr) => a * b) xs) = linearPow a xs.length * listProd xs

Mapping a list by left-multiplication factors out as a linear power of the multiplier times the original list product.

theorem Hex.GF2nPoly.Internal.listProd_ne_zero {f : GF2Poly} {hirr : f.Irreducible} (hf_pos : 0 < f.natDegree) {xs : List (GF2nPoly f hirr)} (hxs : ∀ (x : GF2nPoly f hirr), x ∈ xs → x ≠ 0) : listProd xs ≠ 0

The product of a list of nonzero packed quotient elements is nonzero.

theorem Hex.GF2nPoly.Internal.linearPow_pred_card_eq_one_of_ne_zero {f : GF2Poly} {hirr : f.Irreducible} (hf_pos : 0 < f.natDegree) {a : GF2nPoly f hirr} (ha : a ≠ 0) : linearPow a (2 ^ f.natDegree - 1) = 1

Finite-field exponent theorem for the packed quotient: every nonzero quotient element raised to the number of nonzero representatives is 1.

theorem Hex.GF2nPoly.frobeniusIter_degree_eq_self {f : GF2Poly} {hirr : f.Irreducible} (hf_pos : 0 < f.natDegree) (a : GF2nPoly f hirr) : a.frobeniusIter f.natDegree = a

Every packed quotient element is fixed by the degree-cardinality Frobenius iterate.

theorem Hex.GF2nPoly.frobeniusIter_add_mul_degree_eq {f : GF2Poly} {hirr : f.Irreducible} (hf_pos : 0 < f.natDegree) (a : GF2nPoly f hirr) (m q : Nat) : a.frobeniusIter (m + f.natDegree * q) = a.frobeniusIter m

Adding any multiple of the modulus degree to a Frobenius iterate does not change the result.

theorem Hex.GF2nPoly.frobeniusIter_mod_degree_eq_of_fixed {f : GF2Poly} {hirr : f.Irreducible} (hf_pos : 0 < f.natDegree) {a : GF2nPoly f hirr} {n : Nat} (hfixed : a.frobeniusIter n = a) : a.frobeniusIter (n % f.natDegree) = a

If a quotient element is fixed by the n-fold Frobenius, it is also fixed by the remainder of n modulo the modulus degree.