The polynomial X^(p^k) - X viewed inside the executable FpPoly p model.
Used to phrase the absolute (not modular) divisibility leg f ∣ X^(p^n) - X
underlying Rabin's test.
Equations
- Hex.Berlekamp.xPowSubX k = Hex.DensePoly.monomial (p ^ k) 1 - Hex.FpPoly.X
Instances For
The executable product ∏ c ∈ F_p, (X - c) over canonical residues.
Equations
- Hex.Berlekamp.primeFieldLinearProduct = List.foldl (fun (acc : Hex.FpPoly p) (c : Hex.ZMod64 p) => acc * (Hex.FpPoly.X - Hex.FpPoly.C c)) 1 (Hex.ZMod64.values p)
Instances For
Every field element contributes its linear factor to the canonical
prime-field product. This is the divisibility/root-coverage form used by
the subsequent X^p - X product-identity assembly.
The canonical product has one listed linear factor for each residue.
Not @[simp]: simp already closes it from ZMod64.values_length.
The zero-one CRT representative used to separate a coprime product
a * b: it is congruent to 0 modulo a and to 1 modulo b when
s * a + t * b = 1.
Equations
- Hex.Berlekamp.crtZeroOneCandidate a b s t = Hex.DensePoly.polyCRT a b 0 1 s t
Instances For
The zero-one CRT representative is congruent to 0 modulo the left factor.
The zero-one CRT representative is congruent to 1 modulo the right factor.
Monic reduction of the zero-one CRT representative modulo the left factor.
Monic reduction of the zero-one CRT representative modulo the right factor.
Remainder form of the zero residue modulo the left factor.
Remainder form of the one residue modulo the right factor.
The same zero-one CRT representative, using the executable xgcd coefficients.
Equations
Instances For
If the executable gcd is 1, xgcd supplies CRT-ready coefficients.
The xgcd-backed zero-one CRT representative is congruent to 0 on the left.
The xgcd-backed zero-one CRT representative is congruent to 1 on the right.
Remainder form of the xgcd-backed zero residue modulo the left factor.
Remainder form of the xgcd-backed one residue modulo the right factor.
The zero-one CRT representative is not congruent to a constant modulo
a * b when both factors have positive degree.
XGCD-backed specialization of crtZeroOneCandidate_not_congr_constant_mod_product.
Divisibility by f is equivalent to a zero canonical remainder.
linearPow has the same canonical remainder for bases with the same
canonical remainder.
Polynomial congruence modulo f is preserved by linearPow.
Polynomial congruence modulo f is preserved by subtraction.
Membership in the Frobenius fixed-kernel depends only on the residue class modulo the ambient polynomial.
This is the representative-reduction lemma needed by the Berlekamp CRT
construction: reducing a candidate modulo f preserves and reflects the
absolute divisibility condition f ∣ h^(p^k) - h.
Reduced zero-one CRT witness for a monic coprime product split. The witness is
Frobenius-fixed modulo a * b and is not congruent to any field constant
modulo that product.
Trivial case for deg f = 0: frobeniusDiffMod is already its own
canonical remainder modulo f. When deg f = 0 and f is monic, f
must have size 1 (since Monic 0 is impossible over a prime field), and
every polynomial mod a degree-0 monic divisor is 0; frobeniusDiffMod
is no exception, so both sides reduce to 0.
f divides the difference between the absolute polynomial X^(p^k) - X
and its modular form frobeniusDiffMod f hmonic k. This is the reduction fact
that makes the executable modular test equivalent to the absolute divisibility
leg, and it is reused by the Mathlib transport of Rabin's criterion.
f divides X^(p^k) - X (in the absolute sense) exactly when the
Berlekamp Frobenius remainder frobeniusDiffMod f hmonic k vanishes.
Identifies the absolute polynomial xPowSubX k with the modular Frobenius
remainder used by the executable rabinTest. The proof goes through
frobeniusDiffMod = (xPowSubX k) % f, which itself relies on
frobeniusXPowMod_eq_powMod for the absolute Frobenius identity.
The executable divisibility leg of Rabin's test is exactly the absolute
condition f ∣ X^(p^n) - X, where n = basisSize f.
This is the caller-facing form of
dvd_xPowSubX_iff_frobeniusDiffMod_isZero for code that consumes
rabinDividesTest without unfolding frobeniusDiffMod.
Boolean characterization of the executable Rabin test in theorem-facing
terms: positive degree, absolute divisibility by X^(p^n) - X, and all
maximal-proper-divisor gcd witnesses accepted.
A polynomial of positive degree is nonzero.
Used to discharge the f ≠ 0 leg of FpPoly.Irreducible and to show
that the factors a, b of f are individually nonzero.
Existence of a monic irreducible factor for any non-unit factor.
For a polynomial a : FpPoly p of positive degree appearing as a factor
of a monic polynomial f, there is a monic irreducible g ∣ a with
0 < deg g ≤ deg a. Standard descent on degree, with the monic-associate
rescaling needed when a itself is not monic.
The quotient class of X raised to p^k is represented by the executable
Frobenius remainder frobeniusXPowMod.
Rabin's degree-divisibility theorem in its FpPoly form (forward
direction).
If g is a monic irreducible polynomial of degree d > 0 over F_p and
g ∣ X^(p^n) - X, then d ∣ n. The standard proof works in the residue
field F_p[X]/(g) and shows that X has multiplicative order dividing
p^d - 1, forcing d ∣ n via the order of the Frobenius automorphism.
This is the deepest finite-field ingredient of Rabin's test soundness.
Rabin's degree-divisibility theorem in its FpPoly form (backward
direction).
A monic irreducible polynomial g of degree d > 0 over F_p divides
X^(p^d) - X. The standard proof builds the residue field
F_p[X]/(g) of order p^d and applies the Frobenius identity
α^(p^d) = α for every element of a finite field of order p^d.
xPowSubX d ∣ xPowSubX m whenever d ∣ m, lifting the geometric
divisibility X^(p^d-1) - 1 ∣ X^(p^m-1) - 1 (from p^d - 1 ∣ p^m - 1)
through the xPowSubX factorization.
Every positive proper divisor d of n is dominated by some maximal
proper divisor of n (with d dividing it).
Combinatorial fact about the proper-divisor lattice. Used in the
contrapositive proof to method an irreducible factor's degree d to a
divisor at which the gcd leg of rabinTest rules out divisibility.
A g that divides both f and xPowSubX k also divides the modular
Frobenius remainder frobeniusDiffMod f hmonic k.
Direct consequence of the absolute–modular Frobenius identity together
with the divMod_spec characterization of polynomial remainders.
A g that divides both f and the modular Frobenius remainder
frobeniusDiffMod f hmonic k also divides the absolute polynomial
xPowSubX k.
The converse companion to dvd_frobeniusDiffMod_of_dvd_dvd. Used by the
Mathlib reverse Rabin transport to lift an executable common divisor of f
and frobeniusDiffMod up to X^(p^k) - X, where it transports to a divisor
of frobeniusPolynomial p k.
A divisor of a unit polynomial is itself a unit polynomial.
Routine consequence of degree arithmetic: if g ∣ h and h has degree 0
with nonzero constant, then g also has degree 0 with nonzero constant.
The factor a of a nontrivial product a * b = f is nonzero.
A nonzero polynomial whose degree? is not some 0 has positive degree.
The degree of a factor a is strictly less than the degree of f whenever
the cofactor b has positive degree. The bound is phrased relative to
basisSize, as required by the Berlekamp and Rabin proofs.
The m-th maximal-proper-divisor witness of rabinTest: when the test
passes, every entry of rabinWitnesses is true, hence the gcd leg
holds at every maximal proper divisor.