Decidability of DifferentType (since equality in a finite field with decidable
equality is decidable).
The set of shifts δ ∈ F such that α + δ and β + δ are of different type
(in the sense of DifferentType). Used in Rabin's root-finding algorithm
(Algorithm 3.45 / Theorem 3.44).
Instances For
The map δ ↦ (α + δ)/(β + δ), used to put the different-type set in bijection
with the set of γ whose (q-1)/2-th power is -1.
Instances For
In a finite field F of odd characteristic, exactly (q-1)/2 elements satisfy
x^((q-1)/2) = -1 (the quadratic nonresidues), where q = |F|.
Theorem 3.44 (Rabin 1980): for any pair of distinct elements α, β ∈ F_q with
char F ≠ 2, the number of shifts δ such that α + δ and β + δ are of different
type equals (q-1)/2. Proved by exhibiting a bijection with the set of γ such that
γ^((q-1)/2) = -1.
Step 4b of Algorithm 3.45: compute gcd(g, (X + δ)^((q-1)/2) - 1), a candidate
nontrivial factor of g.
Instances For
Step 2 of Algorithm 3.45: compute gcd(f, X^q - X), the product of (X - α) over
all roots α ∈ F_q of f.
Instances For
Any root of berlekampRabinStep F g δ in F is also a root of g, because the
step output divides g.
Any root of berlekampRabinInit F f in F is a root of f.
Conversely, every root of f in F_q is a root of gcd(f, X^q - X), since
X^q - X vanishes on all of F_q by Fermat's little theorem.
If r is a root of berlekampRabinStep F g δ, then (r + δ)^((q-1)/2) = 1,
which means r + δ is a quadratic residue in F_q.
Read off the unique root from a monic linear polynomial g = X - r:
extractRoot g = -coeff 0 / leadingCoeff.
Instances For
Step 4c of Algorithm 3.45: replace g by whichever of h or g/h has lower
degree, provided h is a nontrivial proper factor.
Instances For
A single iteration of the inner loop in Algorithm 3.45: run berlekampRabinStep
with shift δ, then chooseFactor.
Instances For
The inner while-loop of Algorithm 3.45: iterate berlekampRabinIteration over a
supplied list of random shifts δ, stopping early once deg g ≤ 1.
Instances For
Algorithm 3.45 (Rabin 1980): given a monic polynomial f ∈ F_q[X], return some
root of f in F_q if one exists. Returns 0 if f(0) = 0; otherwise reduces to
the squarefree part g = gcd(f, X^q - X) containing exactly the roots, and iteratively
splits g using random shifts.
Instances For
For a monic linear polynomial g, extractRoot g is indeed a root of g.
If h ∣ g, then every root of chooseFactor F g h is also a root of g,
regardless of which branch (h, g/h, or g) is taken.
Inner loop of Yun's squarefree factorization (Algorithm 3.46): given v, w and a
fuel bound, repeatedly compute g_i = gcd(v_i, w_i - v_i') and refresh
v_{i+1} = v_i / g_i, w_{i+1} = (w_i - v_i') / g_i.
Instances For
Algorithm 3.46 (Yun): squarefree factorization of f ∈ F_q[X] (in characteristic
not dividing deg f). Returns a list [g_1, …, g_m] of squarefree pairwise coprime
polynomials with f = g_1 · g_2^2 · ⋯ · g_m^m.
Instances For
Reconstruct f from its squarefree factorization [g_1, …, g_m] as the product
∏_i g_i^i (with 1-based indexing).
Instances For
The correctness predicate for a squarefree factorization (output of
Algorithm 3.46): the list is nonempty, recovers f as ∏ g_i^i, each g_i is
squarefree, the factors are pairwise coprime, and the last factor is not 1.
- sqfree (g : Polynomial F) : g ∈ factors → Squarefree g
- coprime : List.Pairwise (fun (g h : Polynomial F) => IsCoprime g h) factors
Instances For
If g^2 ∣ f, then g divides gcd(f, f'). This is the easy direction used in
proving correctness of Yun's algorithm.
Characterization underlying Yun's algorithm: for an irreducible g (over a
perfect field), g^2 ∣ f iff g ∣ gcd(f, f'). The nontrivial direction uses
separability of irreducible polynomials over perfect fields.
Over a finite field (which is perfect), a polynomial is separable iff it is squarefree.
The initial gcd gcd(f, f') computed in Yun's algorithm divides f.
One probabilistic splitting step in equal-degree (Cantor-Zassenhaus) factorization
(Step 3 of Algorithm 3.47): try h₁ = gcd(g, u); if it is a proper factor, return it;
otherwise try h₂ = gcd(g, u^((q^j - 1)/2) - 1); otherwise return g.
Instances For
equalDegreeSplitStep F g u j always divides g, in each of the three branches.
Any root in F of equalDegreeSplitStep F g u j is a root of g, since the
output divides g.
The recursive splitting loop in equal-degree factorization (Step 3 of
Algorithm 3.47): given g of degree > j, repeatedly split using
equalDegreeSplitStep and recurse on both pieces, until each factor has degree j.
Instances For
Distinct-degree factorization step (Step 2 of Algorithm 3.47): compute
g_j = gcd(g, X^(q^j) - X), the product of irreducible factors of g of degree j,
and return the pair (g_j, g / g_j).
Instances For
Cantor-Zassenhaus factorization of a squarefree polynomial g (Steps 2–3 of
Algorithm 3.47): iterate distinctDegreeStep for j = 1, 2, …, then split each
g_j further using equalDegreeFactorLoop if needed.
Instances For
Instances For
Algorithm 3.47 (Cantor-Zassenhaus): compute the complete irreducible factorization
of a monic f ∈ F_q[X] as a list of pairs (p, i), where p is an irreducible
factor with multiplicity i. Uses Yun for the squarefree factorization and
factorSquarefree for each squarefree piece.
Instances For
Correctness predicate for the output of cantorZassenhausAlgorithm: the indexed
family factors : Fin n → F[X] consists of irreducibles, f = ∏ (factors i)^(mult i),
multiplicities are positive, and distinct indices give non-associated factors.
- irred (i : Fin n) : Irreducible (factors i)
- pairwise (i j : Fin n) : i ≠ j → ¬Associated (factors i) (factors j)
Instances For
The first component of distinctDegreeStep F g j, namely gcd(g, X^(q^j) - X),
divides g.