Kernel-checkable Rabin irreducibility certificates over prime fields

Rabin's test (CompPoly/Data/Polynomial/Rabin.lean) reduces irreducibility of a degree-d polynomial f over ZMod p to divisibility and coprimality conditions against X^(p^k) - X. Verifying those conditions requires computing X^(p^k) mod f — around d · log₂ p modular squarings — which is far beyond what decide can do on Polynomial values and which this repository's TCB policy forbids delegating to native_decide.

This file provides the reusable, degree-agnostic certificate infrastructure:

• Polynomials are represented as little-endian ℕ-coefficient lists (toPoly interprets them in (ZMod p)[X]), with schoolbook arithmetic (addNat, mulNat) by structural recursion, so every check reduces in the kernel via GMP-accelerated Nat operations.
• A certificate Step records a squaring (or multiply-by-X) together with the quotient and remainder of the division by f; checkStep verifies cur² = q·f + r (coefficientwise, mod p) and runChain folds a whole square-and-multiply chain, so an entire exponentiation certificate is one list literal checked by a single kernel reduction.
• runChain_sound lifts a checked chain to X^N % f = r % f in (ZMod p)[X]; the two Rabin conditions follow via dvd_X_pow_sub_X_of_runChain (trace) and isCoprime_X_pow_sub_X_of_runChain (coprimality, from a Bézout certificate on the reduced residue).
• irreducible_of_rabin_prime_degree packages Rabin's test for prime degree d, where the conditions collapse to a single trace and a single coprimality check; irreducible_of_rabin_prime_power does the same at d = ℓ ^ k, where the collapse is still sound; irreducible_of_rabin_two_prime_factors and irreducible_of_rabin_degree_six cover a degree with two distinct prime factors. All take the field size as a numeral q with Fintype.card F = q, the shape concrete extensions use.

Certificate data is produced by the untrusted generator scripts/gen_rabin_certificate.py; the kernel re-checks every step. Contrast CompPoly/Fields/Binary/BF128Ghash/, the bespoke GF(2¹²⁸) predecessor of this framework, which spells out each step as a separate lemma.

ℕ-level polynomial arithmetic

Little-endian coefficient lists. No coefficient is ever reduced during a product — entries stay below d² · p², comfortably inside GMP range — and comparisons reduce mod p at the end (eqModP), so no subtraction (and hence no truncation) occurs anywhere.

def CompPoly.RabinCert.addNat : List ℕ → List ℕ → List ℕ

Coefficientwise addition of little-endian coefficient lists.

def CompPoly.RabinCert.scaleNat (c : ℕ) (l : List ℕ) : List ℕ

Scale a coefficient list by a constant.

def CompPoly.RabinCert.mulNat : List ℕ → List ℕ → List ℕ

Schoolbook product of little-endian coefficient lists.

def CompPoly.RabinCert.eqModP (p : ℕ) : List ℕ → List ℕ → Bool

Coefficientwise equality modulo p, treating entries beyond a list's end as 0.

The specification bridge

noncomputable def CompPoly.RabinCert.toPoly (p : ℕ) : List ℕ → Polynomial (ZMod p)

Interpret a little-endian coefficient list in (ZMod p)[X], Horner-style. Specification only; certificate checking never evaluates it.

@[simp]

theorem CompPoly.RabinCert.toPoly_nil {p : ℕ} : toPoly p [] = 0

theorem CompPoly.RabinCert.toPoly_cons {p : ℕ} (c : ℕ) (cs : List ℕ) : toPoly p (c :: cs) = Polynomial.C ↑c + Polynomial.X * toPoly p cs

The defining Horner step of toPoly, as a rewrite rule: a head coefficient contributes a constant and the tail is multiplied by X.

@[simp]

theorem CompPoly.RabinCert.toPoly_X {p : ℕ} : toPoly p [0, 1] = Polynomial.X

@[simp]

theorem CompPoly.RabinCert.toPoly_one {p : ℕ} : toPoly p [1] = 1

theorem CompPoly.RabinCert.toPoly_addNat {p : ℕ} (a b : List ℕ) : toPoly p (addNat a b) = toPoly p a + toPoly p b

addNat denotes addition: the coefficientwise sum of two lists is the sum of the polynomials they denote. One of the three specification bridges that make the ℕ-list arithmetic usable as a certificate format.

theorem CompPoly.RabinCert.toPoly_scaleNat {p : ℕ} (c : ℕ) (l : List ℕ) : toPoly p (scaleNat c l) = Polynomial.C ↑c * toPoly p l

scaleNat denotes multiplication by a constant.

theorem CompPoly.RabinCert.toPoly_mulNat {p : ℕ} (a b : List ℕ) : toPoly p (mulNat a b) = toPoly p a * toPoly p b

mulNat denotes multiplication: schoolbook convolution of the coefficient lists is the product of the polynomials they denote. Proved from toPoly_addNat and toPoly_scaleNat, following the same recursion mulNat uses.

theorem CompPoly.RabinCert.cast_eq_cast_of_mod_eq {p a b : ℕ} (h : a % p = b % p) : ↑a = ↑b

Two naturals equal mod p cast to the same element of ZMod p.

theorem CompPoly.RabinCert.toPoly_eq_zero_of_all_mod_eq_zero {p : ℕ} {l : List ℕ} : (l.all fun (x : ℕ) => x % p == 0) = true → toPoly p l = 0

A list whose every coefficient is 0 mod p denotes the zero polynomial. This is the base case behind toPoly_eq_of_eqModP, which is how a eqModP kernel check becomes an equation between polynomials.

theorem CompPoly.RabinCert.toPoly_eq_of_eqModP {p : ℕ} {a b : List ℕ} : eqModP p a b = true → toPoly p a = toPoly p b

Soundness of the coefficientwise checker: eqModP lists denote the same polynomial.

theorem CompPoly.RabinCert.verify_mulAdd {p : ℕ} {a b q fL r : List ℕ} (h : eqModP p (mulNat a b) (addNat (mulNat q fL) r) = true) : toPoly p a * toPoly p b = toPoly p q * toPoly p fL + toPoly p r

Lift a checked ℕ-level identity a·b ≡ q·f + r (mod p) to (ZMod p)[X].

Square-and-multiply chains

structure CompPoly.RabinCert.Step : Type

One step of a square-and-multiply chain modulo f: from the current residue cur, either square it (mulX = false) or multiply it by X (mulX = true), and divide by f to get quotient q and next residue r. The generator supplies q and r; the checker only has to confirm one polynomial identity per step.

• mulX : Bool

  true for a multiply-by-X step, false for a squaring step.

• q : List ℕ

  The quotient of the step's product by the modulus.

• r : List ℕ

  The remainder — the next residue in the chain.

def CompPoly.RabinCert.checkStep (p : ℕ) (fL cur : List ℕ) (s : Step) : Bool

Check one chain step: cur² = q·f + r (or X·cur = q·f + r), coefficientwise mod p.

def CompPoly.RabinCert.runChain (p : ℕ) (fL : List ℕ) : List ℕ → List Step → Option (List ℕ)

Fold a chain of steps from the residue cur, checking each; returns the final residue, or none if any check fails. One kernel reduction of runChain verifies a whole chain.

def CompPoly.RabinCert.chainExp : ℕ → List Step → ℕ

The exponent a chain computes: squaring doubles it, multiply-by-X adds one.

theorem CompPoly.RabinCert.step_sound {p : ℕ} [Fact (Nat.Prime p)] {fL cur : List ℕ} {f : Polynomial (ZMod p)} (hfL : toPoly p fL = f) (hf0 : f ≠ 0) {s : Step} {e : ℕ} (hcheck : checkStep p fL cur s = true) (hprev : Polynomial.X ^ e % f = toPoly p cur % f) : (Polynomial.X ^ bif s.mulX then e + 1 else 2 * e) % f = toPoly p s.r % f

Soundness of one chain step.

theorem CompPoly.RabinCert.runChain_sound {p : ℕ} [Fact (Nat.Prime p)] {fL : List ℕ} {f : Polynomial (ZMod p)} (hfL : toPoly p fL = f) (hf0 : f ≠ 0) (steps : List Step) (cur out : List ℕ) (e : ℕ) : runChain p fL cur steps = some out → Polynomial.X ^ e % f = toPoly p cur % f → Polynomial.X ^ chainExp e steps % f = toPoly p out % f

Soundness of a whole chain: a checked chain starting at the residue of X^e ends at the residue of X^(chainExp e steps).

theorem CompPoly.RabinCert.xpow_mod_of_runChain {p : ℕ} [Fact (Nat.Prime p)] {fL : List ℕ} {f : Polynomial (ZMod p)} (hfL : toPoly p fL = f) (hf0 : f ≠ 0) {steps : List Step} {out : List ℕ} {N : ℕ} (hrun : runChain p fL [0, 1] steps = some out) (hexp : chainExp 1 steps = N) : Polynomial.X ^ N % f = toPoly p out % f

A chain started at [0, 1] (the residue of X¹) computes X^N % f.

The two Rabin conditions from certificates

theorem CompPoly.RabinCert.dvd_sub_of_mod_eq {R : Type u_1} [EuclideanDomain R] {a b n : R} (h : a % n = b % n) : n ∣ a - b

Equal remainders mean the divisor divides the difference.

theorem CompPoly.RabinCert.dvd_X_pow_sub_X_of_runChain {p : ℕ} [Fact (Nat.Prime p)] {fL : List ℕ} {f : Polynomial (ZMod p)} (hfL : toPoly p fL = f) (hf0 : f ≠ 0) {steps : List Step} {N : ℕ} (hrun : runChain p fL [0, 1] steps = some [0, 1]) (hexp : chainExp 1 steps = N) : f ∣ Polynomial.X ^ N - Polynomial.X

The trace condition from a chain. A checked chain for X^N ending back at [0, 1] (the residue X) proves f ∣ X^N - X.

theorem CompPoly.RabinCert.isCoprime_X_pow_sub_X_of_runChain {p : ℕ} [Fact (Nat.Prime p)] {fL : List ℕ} {f : Polynomial (ZMod p)} (hfL : toPoly p fL = f) (hf0 : f ≠ 0) {steps : List Step} {rp w u v : List ℕ} {N : ℕ} (hrun : runChain p fL [0, 1] steps = some rp) (hexp : chainExp 1 steps = N) (hw : eqModP p rp (addNat w [0, 1]) = true) (hbez : eqModP p (addNat (mulNat u fL) (mulNat v w)) [1] = true) : IsCoprime f (Polynomial.X ^ N - Polynomial.X)

The coprimality condition from a chain plus a Bézout certificate.

The chain reduces X^N to a residue rp; writing rp = w + X (checked by eqModP), we have X^N - X ≡ w (mod f), so a Bézout identity u·f + v·w = 1 (again checked by eqModP) witnesses IsCoprime f (X^N - X).

Packaging Rabin's test at a concrete degree

Polynomial.irreducible_of_rabin already quantifies the coprimality condition over d.primeFactors. The wrappers below discharge that quantifier for the shapes of d that concrete extensions use, so a caller supplies one coprimality proof per prime factor and nothing else. Each takes the field size as a numeral q with hcard : Fintype.card F = q, exactly as Polynomial.irreducible_of_rabin does — supply ZMod.card _ at a concrete field, or rfl to read the conditions at Fintype.card F. The section comment in CompPoly/Data/Polynomial/Rabin.lean records why that is the only shape these statements have.

Note that irreducible_of_rabin_prime_degree does not apply at composite d, and its collapsed condition is not merely inconvenient but unsound there: a product of equal-degree factors divides X^(q^d) - X and is coprime to X^q - X, so it would pass. irreducible_of_rabin_prime_power is the collapse that is sound at d = ℓ ^ k.

theorem CompPoly.RabinCert.irreducible_of_rabin_prime_degree {F : Type u_1} [Field F] [Fintype F] {f : Polynomial F} {d q : ℕ} (hcard : Fintype.card F = q) (hd : Nat.Prime d) (h_deg : f.natDegree = d) (h_trace : f ∣ Polynomial.X ^ q ^ d - Polynomial.X) (h_cop : IsCoprime f (Polynomial.X ^ q - Polynomial.X)) : Irreducible f

Rabin's test for prime degree. For f of prime degree d over a finite field with q elements, the per-prime-factor conditions collapse to a single coprimality check at exponent q: f is irreducible provided f ∣ X^(q^d) - X and IsCoprime f (X^q - X).

@[deprecated CompPoly.RabinCert.irreducible_of_rabin_prime_degree (since := "2026-09-18")]

theorem CompPoly.RabinCert.irreducible_of_rabin_prime_degree_of_card {F : Type u_1} [Field F] [Fintype F] {f : Polynomial F} {d q : ℕ} (hcard : Fintype.card F = q) (hd : Nat.Prime d) (h_deg : f.natDegree = d) (h_trace : f ∣ Polynomial.X ^ q ^ d - Polynomial.X) (h_cop : IsCoprime f (Polynomial.X ^ q - Polynomial.X)) : Irreducible f

Alias of CompPoly.RabinCert.irreducible_of_rabin_prime_degree.

---

Rabin's test for prime degree. For f of prime degree d over a finite field with q elements, the per-prime-factor conditions collapse to a single coprimality check at exponent q: f is irreducible provided f ∣ X^(q^d) - X and IsCoprime f (X^q - X).

theorem CompPoly.RabinCert.irreducible_of_rabin_prime_power {F : Type u_1} [Field F] [Fintype F] {f : Polynomial F} {d ℓ k q : ℕ} (hcard : Fintype.card F = q) (hℓ : Nat.Prime ℓ) (hk : k ≠ 0) (hd_eq : d = ℓ ^ k) (h_deg : f.natDegree = d) (h_trace : f ∣ Polynomial.X ^ q ^ d - Polynomial.X) (h_cop : IsCoprime f (Polynomial.X ^ q ^ (d / ℓ) - Polynomial.X)) : Irreducible f

Rabin's test for a prime-power degree, such as d = 8, 64 or 128.

d = ℓ ^ k has the single prime factor ℓ, so — exactly as at prime degree — the caller supplies the trace condition plus one coprimality certificate, here at exponent q ^ (d / ℓ). Unlike irreducible_of_rabin_prime_degree this is sound at composite d: the check at d / ℓ rules out every proper divisor of d, because every proper divisor of ℓ ^ k divides ℓ ^ (k - 1).

d is kept separate from ℓ ^ k and tied to it by hd_eq so that the conditions read at the caller's numeral (q ^ 64, not q ^ 2 ^ 6); supply hd_eq as by norm_num. This is the shape the characteristic-two moduli use — Aes.modulus at d = 8 and BF64.basePoly at d = 64.

theorem CompPoly.RabinCert.irreducible_of_rabin_two_prime_factors {F : Type u_1} [Field F] [Fintype F] {f : Polynomial F} {d ℓ₁ ℓ₂ q : ℕ} (hcard : Fintype.card F = q) (h_deg : f.natDegree = d) (h_pos : 0 < d) (h_factors : d.primeFactors = {ℓ₁, ℓ₂}) (h_trace : f ∣ Polynomial.X ^ q ^ d - Polynomial.X) (h_cop₁ : IsCoprime f (Polynomial.X ^ q ^ (d / ℓ₁) - Polynomial.X)) (h_cop₂ : IsCoprime f (Polynomial.X ^ q ^ (d / ℓ₂) - Polynomial.X)) : Irreducible f

Rabin's test for a degree with exactly two prime factors, such as d = 6.

The caller supplies the trace condition plus one coprimality certificate per prime factor, at exponents q^(d/ℓ₁) and q^(d/ℓ₂). The hypothesis h_factors is by decide at a concrete degree — for d = 6 it is (6 : ℕ).primeFactors = {2, 3}, giving checks at q^3 and q^2.

Both checks are needed. Dropping the q^3 one admits a product of two irreducible cubics; dropping the q^2 one admits a product of three irreducible quadratics.

theorem CompPoly.RabinCert.irreducible_of_rabin_degree_six {F : Type u_1} [Field F] [Fintype F] {f : Polynomial F} {q : ℕ} (hcard : Fintype.card F = q) (h_deg : f.natDegree = 6) (h_trace : f ∣ Polynomial.X ^ q ^ 6 - Polynomial.X) (h_cop₃ : IsCoprime f (Polynomial.X ^ q ^ 3 - Polynomial.X)) (h_cop₂ : IsCoprime f (Polynomial.X ^ q ^ 2 - Polynomial.X)) : Irreducible f

Rabin's test at degree 6. f of degree 6 over a finite field with q elements is irreducible provided f ∣ X^(q^6) - X, IsCoprime f (X^(q^3) - X), and IsCoprime f (X^(q^2) - X).

This is the shape used by the KoalaBear degree-6 extension. It differs from irreducible_of_rabin_two_prime_factors only in discharging Nat.primeFactors 6 = {2, 3} internally, so callers never touch Nat.primeFactors.

The q^3 check is what rules out a product of two irreducible cubics, and the q^2 check a product of three irreducible quadratics; the trace condition alone permits both.

@[deprecated CompPoly.RabinCert.irreducible_of_rabin_degree_six (since := "2026-09-18")]

theorem CompPoly.RabinCert.irreducible_of_rabin_degree_six_of_card {F : Type u_1} [Field F] [Fintype F] {f : Polynomial F} {q : ℕ} (hcard : Fintype.card F = q) (h_deg : f.natDegree = 6) (h_trace : f ∣ Polynomial.X ^ q ^ 6 - Polynomial.X) (h_cop₃ : IsCoprime f (Polynomial.X ^ q ^ 3 - Polynomial.X)) (h_cop₂ : IsCoprime f (Polynomial.X ^ q ^ 2 - Polynomial.X)) : Irreducible f

Alias of CompPoly.RabinCert.irreducible_of_rabin_degree_six.

---

Rabin's test at degree 6. f of degree 6 over a finite field with q elements is irreducible provided f ∣ X^(q^6) - X, IsCoprime f (X^(q^3) - X), and IsCoprime f (X^(q^2) - X).

This is the shape used by the KoalaBear degree-6 extension. It differs from irreducible_of_rabin_two_prime_factors only in discharging Nat.primeFactors 6 = {2, 3} internally, so callers never touch Nat.primeFactors.

The q^3 check is what rules out a product of two irreducible cubics, and the q^2 check a product of three irreducible quadratics; the trace condition alone permits both.