diff --git a/CompPoly/Data/Polynomial/RabinCertificate.lean b/CompPoly/Data/Polynomial/RabinCertificate.lean index f5df9fdd..d5fe966f 100644 --- 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 index cf5ef709..eb429dfc 100644 --- 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 index bd5a293f..ea861c9a 100644 --- 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 index 2f1dbd3e..56f5e2d6 100644 --- 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

--f --lean --namespace `. 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 `copSteps`/`copRp`/… 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 + `copSteps`/`copRp`/… 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 index e83a2fc1..d1841d27 100644 --- 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