Verified-zkEVM · alexanderlhicks · Aug 18, 2026 · Aug 18, 2026
diff --git a/CompPoly/Data/Polynomial/RabinCertificate.lean b/CompPoly/Data/Polynomial/RabinCertificate.lean
@@ -32,7 +32,9 @@ This file provides the reusable, degree-agnostic *certificate* infrastructure:
   `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.
+  conditions collapse to a single trace and a single coprimality check. The `_of_card` variants
+  of the packaged forms take the field size as a numeral `q` with `Fintype.card F = q`; that is
+  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
@@ -389,37 +391,46 @@ theorem irreducible_of_rabin_degree_six {F : Type*} [Field F] [Fintype F] {f : F
   irreducible_of_rabin_two_prime_factors h_deg (by norm_num) primeFactors_six h_trace
     (by simpa using h_cop₃) (by simpa using h_cop₂)
 
-/-- Explicit-cardinality form of the prime-degree Rabin test.
-
-Identical content to `irreducible_of_rabin_prime_degree`, but the field size is
-a caller-supplied numeral `q` (with `Fintype.card F = q`) rather than
-`Fintype.card F` itself. This lets a caller state the trace and coprimality
-certificates with `q` a concrete literal. That matters for **re-checking**: a
-kernel replay of the resulting proof from an empty environment then never has to
-reduce `Fintype.card F` (for a `ZMod p` field, an enumeration of ~`p` elements)
-to reconcile it with the literal through a rewrite cast. `q` stays universally
-quantified here, so this declaration itself carries no concrete large numeral,
-and the two forms are definitionally equal, so nothing is weakened. -/
+/-! ### Explicit-cardinality forms
+
+The wrappers above state their conditions at `Fintype.card F`. Concrete extensions instead define
+their field as `ZMod fieldSize` and generate certificates already stated in terms of the numeral
+(`chainExp 1 steps = fieldSize ^ d`), so the `_of_card` forms below take the field size as a
+caller-supplied `q` with `hcard : Fintype.card F = q`. Same shape as
+`irreducible_X_pow_four_sub_C_of_card` in `CompPoly/Fields/Extension/Binomial.lean`.
+-/
+
+/--
+**Rabin's test for prime degree, with the cardinality abstracted into a numeral `q`.**
+
+Identical content to `irreducible_of_rabin_prime_degree`, with the field size supplied as `q` and
+`hcard : Fintype.card F = q` rather than read off as `Fintype.card F`. Each Rabin condition is then
+discharged by applying its certificate directly, rather than first casting the goal with
+`rw [hcard]`. Supply `hcard` as `ZMod.card _`.
+
+Nothing is weakened: instantiating at `q := Fintype.card F` with `rfl` recovers
+`irreducible_of_rabin_prime_degree` verbatim, and `CompPolyTests.RabinCertificate` pins that
+instantiation as a regression test.
+-/
 theorem irreducible_of_rabin_prime_degree_of_card {F : Type*} [Field F] [Fintype F]
-    {f : F[X]} {d : ℕ} (q : ℕ) (hq : Fintype.card F = q)
+    {f : F[X]} {d q : ℕ} (hcard : Fintype.card F = q)
     (hd : d.Prime) (h_deg : f.natDegree = d)
     (h_trace : f ∣ X ^ (q ^ d) - X)
     (h_cop : IsCoprime f (X ^ q - X)) :
     Irreducible f := by
-  subst hq
+  subst hcard
   exact irreducible_of_rabin_prime_degree hd h_deg h_trace h_cop
 
-/-- Explicit-cardinality form of the degree-6 Rabin test. See
-`irreducible_of_rabin_prime_degree_of_card` for why the numeral form matters for
-re-checking; the same reasoning applies here at composite degree 6. -/
+/-- **Rabin's test at degree 6, with the cardinality abstracted into a numeral `q`.** See
+`irreducible_of_rabin_prime_degree_of_card`; the same reasoning applies at composite degree 6. -/
 theorem irreducible_of_rabin_degree_six_of_card {F : Type*} [Field F] [Fintype F]
-    {f : F[X]} (q : ℕ) (hq : Fintype.card F = q)
+    {f : F[X]} {q : ℕ} (hcard : Fintype.card F = q)
     (h_deg : f.natDegree = 6)
     (h_trace : f ∣ X ^ (q ^ 6) - X)
     (h_cop₃ : IsCoprime f (X ^ (q ^ 3) - X))
     (h_cop₂ : IsCoprime f (X ^ (q ^ 2) - X)) :
     Irreducible f := by
-  subst hq
+  subst hcard
   exact irreducible_of_rabin_degree_six h_deg h_trace h_cop₃ h_cop₂
 
 end CompPoly.RabinCert
diff --git a/CompPoly/Fields/KoalaBear/Ext5/QuinticIrreducible.lean b/CompPoly/Fields/KoalaBear/Ext5/QuinticIrreducible.lean
@@ -14,10 +14,10 @@ public import Mathlib.Tactic.NormNum.Prime
 # Irreducibility of `X^5 + X^2 - 1` over KoalaBear
 
 The quintic `X^5 + X^2 - 1` is irreducible over `KoalaBear.Field`, proved by Rabin's test at
-prime degree (`CompPoly.RabinCert.irreducible_of_rabin_prime_degree`). No degree-5 *binomial*
-does the job: `gcd(5, p - 1) = 1`, so `x ↦ x^5` is a bijection on KoalaBear and every `X^5 - W`
-has a root. This non-binomial quintic is the defining polynomial of the degree-5 extension in
-`CompPoly/Fields/KoalaBear/Ext5.lean`.
+prime degree (`CompPoly.RabinCert.irreducible_of_rabin_prime_degree_of_card`). No degree-5
+*binomial* does the job: `gcd(5, p - 1) = 1`, so `x ↦ x^5` is a bijection on KoalaBear and every
+`X^5 - W` has a root. This non-binomial quintic is the defining polynomial of the degree-5
+extension in `CompPoly/Fields/KoalaBear/Ext5.lean`.
 
 The two Rabin conditions — `f ∣ X^(p^5) - X` and `IsCoprime f (X^p - X)` — are discharged by
 kernel-checked certificates from `CompPoly/Fields/KoalaBear/Ext5/QuinticCertData.lean`
@@ -110,8 +110,7 @@ theorem quintic_bezout_check :
 kernel-checked certificates for both conditions. -/
 theorem quinticPoly_irreducible : Irreducible quinticPoly := by
   have hcard : Fintype.card Field = fieldSize := ZMod.card _
-  refine irreducible_of_rabin_prime_degree_of_card fieldSize hcard (by norm_num)
-    quinticPoly_natDegree ?_ ?_
+  refine irreducible_of_rabin_prime_degree_of_card hcard (by norm_num) quinticPoly_natDegree ?_ ?_
   · exact dvd_X_pow_sub_X_of_runChain toPoly_quinticL quinticPoly_ne_zero
       quintic_trace_chain quintic_trace_exp
   · exact isCoprime_X_pow_sub_X_of_runChain toPoly_quinticL quinticPoly_ne_zero

diff --git a/CompPoly/Fields/KoalaBear/Ext6/SexticIrreducible.lean b/CompPoly/Fields/KoalaBear/Ext6/SexticIrreducible.lean
@@ -138,7 +138,7 @@ theorem sextic_cop2_bezout_check :
 factors, with kernel-checked certificates for all three conditions. -/
 theorem sexticPoly_irreducible : Irreducible sexticPoly := by
   have hcard : Fintype.card Field = fieldSize := ZMod.card _
-  refine irreducible_of_rabin_degree_six_of_card fieldSize hcard sexticPoly_natDegree ?_ ?_ ?_
+  refine irreducible_of_rabin_degree_six_of_card hcard sexticPoly_natDegree ?_ ?_ ?_
   · exact dvd_X_pow_sub_X_of_runChain toPoly_sexticL sexticPoly_ne_zero
       sextic_trace_chain sextic_trace_exp
   · exact isCoprime_X_pow_sub_X_of_runChain toPoly_sexticL sexticPoly_ne_zero

diff --git a/docs/wiki/field-extensions.md b/docs/wiki/field-extensions.md
@@ -50,7 +50,7 @@ makes a cheap Frobenius and a norm-based inverse possible. See "Choosing a gener
 | Rabin's test, general | [`../../CompPoly/Data/Polynomial/Rabin.lean`](../../CompPoly/Data/Polynomial/Rabin.lean) | `irreducible_of_rabin`, `irreducible_iff_rabin` for any degree over any finite field |
 | Factor-degree bound | [`../../CompPoly/ToMathlib/Polynomial/Irreducible.lean`](../../CompPoly/ToMathlib/Polynomial/Irreducible.lean) | `exists_factor_natDegree_le_of_reducible` |
 | Binomial criterion | [`../../CompPoly/Fields/Extension/Binomial.lean`](../../CompPoly/Fields/Extension/Binomial.lean) | the collapse to base-field exponentiations; `irreducible_X_pow_four_sub_C_iff` |
-| Rabin certificates | [`../../CompPoly/Data/Polynomial/RabinCertificate.lean`](../../CompPoly/Data/Polynomial/RabinCertificate.lean) | kernel-checked chains for non-binomial moduli; `runChain_sound`, `irreducible_of_rabin_prime_degree`, `irreducible_of_rabin_two_prime_factors`, `irreducible_of_rabin_degree_six` |
+| Rabin certificates | [`../../CompPoly/Data/Polynomial/RabinCertificate.lean`](../../CompPoly/Data/Polynomial/RabinCertificate.lean) | kernel-checked chains for non-binomial moduli; `runChain_sound`, `irreducible_of_rabin_prime_degree`, `irreducible_of_rabin_two_prime_factors`, `irreducible_of_rabin_degree_six`, and the `_of_card` forms concrete callers use |
 | Carrier and ring ops | [`../../CompPoly/Fields/Extension/Defs.lean`](../../CompPoly/Fields/Extension/Defs.lean) | `ExtensionParams`, `BinomialParams` (+ `toExtensionParams`), `Ext P`, `Ext.shiftReduce`, `Ext.monomialMod`, `Ext.mul` (spec), `Ext.red` + `Ext.mulTbl` (compiled, via `@[csimp]`) |
 | Bridge and `CommRing` | [`../../CompPoly/Fields/Extension/Bridge.lean`](../../CompPoly/Fields/Extension/Bridge.lean) | `toQuot`, `toQuot_shiftReduce`, `toQuot_mul`, `instCommRing` |
 | Bijectivity and `Field` | [`../../CompPoly/Fields/Extension/Field.lean`](../../CompPoly/Fields/Extension/Field.lean) | `ringEquivQuot`, `card_ext`, `inv`, `instField` |
@@ -144,6 +144,15 @@ over `d.primeFactors`; the packaged forms are:
 | `6` | `irreducible_of_rabin_degree_six` | plus `IsCoprime f (X^(q^3) - X)` and `IsCoprime f (X^(q^2) - X)` |
 | two prime factors | `irreducible_of_rabin_two_prime_factors` | as above, `Nat.primeFactors d = {ℓ₁, ℓ₂}` supplied by the caller |
 
+Each of the first two also has an `_of_card` form (`irreducible_of_rabin_prime_degree_of_card`,
+`irreducible_of_rabin_degree_six_of_card`) taking the field size as a numeral `q` with
+`hcard : Fintype.card F = q`, supplied as `ZMod.card _`. Concrete extensions use those: their
+generated certificates are already stated in terms of `fieldSize`, so the conditions apply
+directly instead of needing a `rw [hcard]` cast per condition. This mirrors
+`irreducible_X_pow_four_sub_C_of_card` on the binomial side. The two forms are inter-derivable —
+instantiating at `q := Fintype.card F` with `rfl` recovers the plain one — and
+`tests/CompPolyTests/Data/Polynomial/RabinCertificate.lean` pins that round trip.
+
 Concretely, over KoalaBear `(X^3 + X + 4)(X^3 + X - 4)` divides `X^(p^6) - X` and is coprime to
 `X^p - X`, so it satisfies the prime-degree conditions verbatim while being visibly reducible;
 only the `q^3` check rejects it. `Nat.primeFactors 6 = {2, 3}` cannot be closed by `decide`
@@ -212,11 +221,14 @@ That is about 60 lines.
 2. Generate the certificate module:
    `python3 scripts/gen_rabin_certificate.py --p <p> --f <coeffs> --lean <path> --namespace <NS>`.
 3. Write the irreducibility wrapper: `toPoly p fL = f`, `natDegree`, `f ≠ 0`, then the
-   chain/Bézout `rfl` checks and the assembly through `irreducible_of_rabin_prime_degree`
-   (prime `d`, see `KoalaBear/Ext5/QuinticIrreducible.lean`) or
-   `irreducible_of_rabin_degree_six` / `irreducible_of_rabin_two_prime_factors` (composite `d`,
-   see `KoalaBear/Ext6/SexticIrreducible.lean`). At composite `d` there is one chain plus Bézout
-   block per prime factor, named `cop<m>Steps`/`cop<m>Rp`/… for `m = d / ℓ`.
+   chain/Bézout `rfl` checks and the assembly through
+   `irreducible_of_rabin_prime_degree_of_card` (prime `d`, see
+   `KoalaBear/Ext5/QuinticIrreducible.lean`) or `irreducible_of_rabin_degree_six_of_card`
+   (composite `d`, see `KoalaBear/Ext6/SexticIrreducible.lean`), passing
+   `hcard : Fintype.card Field = fieldSize := ZMod.card _`. At a composite `d` with no `_of_card`
+   form yet, use `irreducible_of_rabin_two_prime_factors` and cast each condition with
+   `rw [hcard]`. At composite `d` there is one chain plus Bézout block per prime factor, named
+   `cop<m>Steps`/`cop<m>Rp`/… for `m = d / ℓ`.
 4. Write the `ExtensionParams` (lower coefficients of `f`, little-endian) and prove
    `...Params.poly = f`; register the `Fact` and define the `abbrev` — see
    `KoalaBear/Ext5.lean` (supporting cert/proof files under `KoalaBear/Ext5/`).

diff --git a/tests/CompPolyTests/Data/Polynomial/RabinCertificate.lean b/tests/CompPolyTests/Data/Polynomial/RabinCertificate.lean
@@ -272,4 +272,35 @@ theorem not_isCoprime : ¬ IsCoprime fRed ((X : (ZMod P)[X]) ^ (P ^ 3) - X) := b
 
 end ReducibleSextic
 
+/-! ### The `_of_card` forms are equivalent to the plain ones
+
+`irreducible_of_rabin_prime_degree_of_card` and `irreducible_of_rabin_degree_six_of_card` state
+their conditions at a caller-supplied numeral `q` with `hcard : Fintype.card F = q`, which is the
+shape concrete extensions use. Their docstrings claim nothing is weakened; the two theorems below
+are that claim, machine-checked. Instantiating at `q := Fintype.card F` with `rfl` has to recover
+the plain form *verbatim*, so a future edit cannot silently add a hypothesis or shift an exponent.
+The opposite direction is the `_of_card` proof body itself, checked whenever the library builds.
+-/
+
+namespace OfCardRoundTrip
+
+/-- `irreducible_of_rabin_prime_degree_of_card` recovers `irreducible_of_rabin_prime_degree`. -/
+theorem prime_degree_recovered {F : Type*} [Field F] [Fintype F] {f : F[X]} {d : ℕ}
+    (hd : d.Prime) (h_deg : f.natDegree = d)
+    (h_trace : f ∣ X ^ (Fintype.card F ^ d) - X)
+    (h_cop : IsCoprime f (X ^ Fintype.card F - X)) :
+    Irreducible f :=
+  irreducible_of_rabin_prime_degree_of_card rfl hd h_deg h_trace h_cop
+
+/-- `irreducible_of_rabin_degree_six_of_card` recovers `irreducible_of_rabin_degree_six`. -/
+theorem degree_six_recovered {F : Type*} [Field F] [Fintype F] {f : F[X]}
+    (h_deg : f.natDegree = 6)
+    (h_trace : f ∣ X ^ (Fintype.card F ^ 6) - X)
+    (h_cop₃ : IsCoprime f (X ^ (Fintype.card F ^ 3) - X))
+    (h_cop₂ : IsCoprime f (X ^ (Fintype.card F ^ 2) - X)) :
+    Irreducible f :=
+  irreducible_of_rabin_degree_six_of_card rfl h_deg h_trace h_cop₃ h_cop₂
+
+end OfCardRoundTrip
+
 end CompPolyTests.RabinCertificate