Algebraic half of Berlekamp completeness for square-free inputs.
For a monic square-free f ∈ F_p[x], if every fixed-space kernel witness fails
to produce a Berlekamp split (kernelWitnessSplit? f w = none), then f is
irreducible.
The proof goes by contradiction: a nontrivial factorization f = a₀ * b₀
yields a monic irreducible factor g ∣ a₀ and a monic cofactor b' = f / g
of positive degree. The reduced CRT zero-one witness from
exists_reduced_crtZeroOne_kernelWitness_of_squareFree_monic_split produces
a polynomial h of size ≤ basisSize f with f ∣ linearPow h p - h and
h nonconstant modulo f. The fixed-space iff
(isFixedSpaceKernelPolynomial_iff_dvd_linearPow_sub_self) makes h an
algebraic kernel polynomial; the spanning lemma
fixedSpaceKernelPolynomial_coeffVector_complete decomposes its coefficient
vector as a linear combination of basis polynomials. Because h is not a
constant, at least one basis polynomial w must be nonconstant; the iff in
the matrix→algebraic direction (fixedSpaceKernel_sound) and
dvd_primeFieldProduct_witness_of_dvd_linearPow_sub_self lift w to a
witness of f ∣ Π_c (w − C c). The executable split surface
exists_kernelWitnessSplit?_some_of_witnessProduct_dvd_of_pos_degree then
produces kernelWitnessSplit? f w = some _, contradicting hno_split.
Divisor-generalized Berlekamp completeness. For a monic square-free f and
a monic divisor g ∣ f, if no fixed-space kernel witness of f admits a
Berlekamp split of g, then g is irreducible. This is the per-factor
soundness obligation of berlekampFactor, which splits every returned factor
with f's single shared kernel. The case f = g recovers
irreducible_of_no_kernelWitnessSplit_squareFree.
The proof assumes a nontrivial factorization g = a₀ * b₀, extracts a monic
irreducible factor g₁ ∣ a₀ with monic cofactor c₀ = g / g₁, builds a
g-kernel CRT witness hh nonconstant mod g, lifts it to an f-kernel
witness H nonconstant mod g (exists_fKernel_witness_nonconst_mod_g), moves
the nonconstancy to an f-basis polynomial w (exists_basis_nonconst_mod_g),
and feeds w to the executable split surface to contradict hno_split.
Non-monic divisor-generalized Berlekamp completeness. Drops the monicity
requirement on the divisor g of irreducible_of_no_kernelWitnessSplit_squareFree_of_dvd
to bare nonzeroness. The factors returned by berlekampFactor are raw gcd
outputs and so are only monic up to a unit; this is the form the executable
completeness theorem consumes. Positive-degree divisors are normalized to their monic
associate scale (leadingCoeff g)⁻¹ g, to which the monic theorem applies after
transporting the no-split fact via kernelWitnessSplit?_none_scale; a nonzero
constant divisor is irreducible directly.
Executable Berlekamp factor irreducibility. Every factor returned by
berlekampFactor on a monic square-free input is irreducible. Assembles the
per-factor postconditions of the splitting loop; each factor is nonzero
(berlekampFactor_factors_ne_zero), divides f
(berlekampFactor_factors_dvd), and admits no kernel-witness split
(kernelWitnessSplit?_none_of_berlekampFactor_factors); and feeds them to the
non-monic divisor completeness theorem.
For a monic square-free f whose executable Berlekamp factorization returns
at most one factor, f is irreducible. Composes the structural loop lemma
kernelWitnessSplit?_none_of_berlekampFactor_factors_length_le_one with the
algebraic completeness theorem
irreducible_of_no_kernelWitnessSplit_squareFree.
The executable Berlekamp factor list of a square-free monic input has no
duplicates. Composes the abstract loop invariant
Hex.Berlekamp.berlekampFactor_factors_nodup_of_no_squared
(HexBerlekamp/Factor.lean) with the squareness-implies-isUnitPolynomial
result Hex.Berlekamp.isUnitPolynomial_of_squareFree_of_squared_dvd.