Irreducibility of binomials X^d - W over a finite field #
Applying Rabin's test (CompPoly/Data/Polynomial/Rabin.lean) to a binomial defining
polynomial collapses both conditions into single exponentiations in the base field.
The reason is that X^d ≡ W, so whenever d ∣ N - 1, writing k = (N-1)/d,
X^N - X = X * (X^(d*k) - 1) and X^(d*k) ≡ W^k (mod X^d - W).
Hence X^d - W divides X^N - X exactly when W^k = 1, and is coprime to it exactly when
W^k ≠ 1: the residue is then X * C (W^k - 1), a unit multiple of X, and X does not
divide X^d - W because W ≠ 0.
Instantiating at N = q^d and N = q^(d/ℓ) turns Rabin's test into
irreducible_X_pow_sub_C_iff, whose conditions are two base-field exponentiations. Contrast
the ~2100 lines of hand-generated BitVec step certificates in
CompPoly/Fields/Binary/BF128Ghash/XPowTwoPow{Mod,Gcd}Certificate.lean, which is what the
same test costs when the defining polynomial is not a binomial.
Main statements #
Polynomial.X_pow_sub_C_dvd_X_pow_sub_X/Polynomial.isCoprime_X_pow_sub_C_X_pow_sub_X: the two collapsed Rabin conditions, and their converses.Polynomial.irreducible_X_pow_sub_C_iff: the criterion for generald.Polynomial.irreducible_X_pow_four_sub_C: thed = 4corollary, which dischargesNat.primeFactorsinternally. This is the degree used by BabyBear, KoalaBear and Hachi extension fields.
Both take the field size as a numeral q together with Fintype.card F = q, as everything in
the Rabin layer does; pass rfl if you have no numeral.
References #
- [Rabin80] Michael O. Rabin, Probabilistic Algorithms in Finite Fields, SIAM Journal on Computing 9(2), 1980.
- [LN97] Rudolf Lidl and Harald Niederreiter, Finite Fields, 2nd ed., Theorem 3.75.
Reducing powers of X modulo a binomial #
The two collapsed Rabin conditions #
Rabin condition 2, collapsed. If d ∣ N - 1, W ≠ 0 and W ^ ((N-1)/d) ≠ 1, then
X^d - C W is coprime to X^N - X.
Modulo X^d - C W the polynomial X^N - X reduces to X * C (W^k - 1), a unit multiple of
X, and X is coprime to X^d - C W by not_X_dvd_X_pow_sub_C.
The irreducibility criterion #
Each statement takes the field size as a numeral q with hcard : Fintype.card F = q, matching
Polynomial.irreducible_of_rabin; a concrete field supplies ZMod.card _ and a caller with no
numeral passes rfl. The section comment in CompPoly/Data/Polynomial/Rabin.lean says why.
Irreducibility criterion for binomials.
Over a finite field with q elements, X^d - W is irreducible if and only if
W^((q^d - 1)/d) = 1 and W^((q^(d/ℓ) - 1)/d) ≠ 1 for every prime ℓ ∣ d.
The divisibility side conditions h_top and h_mid hold in every case of interest — for
d = 4 and q ≡ 1 mod 4, for instance — and are decidable arithmetic facts about q and d.
The mpr direction of irreducible_X_pow_sub_C_iff, as a standalone lemma.
Irreducibility criterion for quartic binomials.
X^4 - W is irreducible over a finite field with q elements exactly when
W^((q^4 - 1)/4) = 1 and W^((q^2 - 1)/4) ≠ 1.
This is the shape used by the BabyBear, KoalaBear and Hachi degree-4 extensions. It differs
from irreducible_X_pow_sub_C_iff only in discharging Nat.primeFactors 4 = {2} internally,
so callers never touch Nat.primeFactors.
Being an iff, a failed check proves reducibility rather than merely failing to prove
irreducibility.
Concrete fields are defined as ZMod fieldSize where fieldSize is an expression such as
2 ^ 31 - 2 ^ 24 + 1, and the hypotheses are stated at the numeral q, which is what lets a
caller discharge them with norm_num and reduce_mod_char. reduce_mod_char still needs to see
the type as ZMod <numeral>, so the two exponentiation goals are usually preceded by a show;
see CompPoly/Fields/KoalaBear/Ext4.lean for the idiom.
Alias of Polynomial.irreducible_X_pow_four_sub_C_iff.
Irreducibility criterion for quartic binomials.
X^4 - W is irreducible over a finite field with q elements exactly when
W^((q^4 - 1)/4) = 1 and W^((q^2 - 1)/4) ≠ 1.
This is the shape used by the BabyBear, KoalaBear and Hachi degree-4 extensions. It differs
from irreducible_X_pow_sub_C_iff only in discharging Nat.primeFactors 4 = {2} internally,
so callers never touch Nat.primeFactors.
Being an iff, a failed check proves reducibility rather than merely failing to prove
irreducibility.
Concrete fields are defined as ZMod fieldSize where fieldSize is an expression such as
2 ^ 31 - 2 ^ 24 + 1, and the hypotheses are stated at the numeral q, which is what lets a
caller discharge them with norm_num and reduce_mod_char. reduce_mod_char still needs to see
the type as ZMod <numeral>, so the two exponentiation goals are usually preceded by a show;
see CompPoly/Fields/KoalaBear/Ext4.lean for the idiom.
The mpr direction of irreducible_X_pow_four_sub_C_iff, as a standalone lemma.
Alias of Polynomial.irreducible_X_pow_four_sub_C.
The mpr direction of irreducible_X_pow_four_sub_C_iff, as a standalone lemma.