theorem Hex.Berlekamp.xPowSubX_one_eval_eq_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (c : ZMod64 p) : DensePoly.eval (xPowSubX 1) c = 0

Every prime-field residue is a root of xPowSubX 1: this is Fermat's little theorem packaged through the executable FpPoly evaluation.

theorem Hex.Berlekamp.primeFieldLinearFactor_dvd_xPowSubX_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (c : ZMod64 p) : primeFieldLinearFactor c ∣ xPowSubX 1

Each prime-field linear factor X - C c divides xPowSubX 1.

theorem Hex.Berlekamp.primeFieldLinearProduct_dvd_xPowSubX_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] : primeFieldLinearProduct ∣ xPowSubX 1

The canonical prime-field product divides xPowSubX 1.

theorem Hex.Berlekamp.primeFieldLinearProduct_size {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] : DensePoly.size primeFieldLinearProduct = p + 1

The canonical prime-field product has size p + 1.

theorem Hex.Berlekamp.primeFieldLinearProduct_ne_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] : primeFieldLinearProduct ≠ 0

The canonical prime-field product is nonzero.

theorem Hex.Berlekamp.primeFieldLinearProduct_monic {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] : DensePoly.Monic primeFieldLinearProduct

The canonical prime-field product is monic.

theorem Hex.Berlekamp.xPowSubX_one_size {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] : DensePoly.size (xPowSubX 1) = p + 1

xPowSubX 1 has size p + 1.

theorem Hex.Berlekamp.xPowSubX_one_monic {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] : DensePoly.Monic (xPowSubX 1)

xPowSubX 1 is monic.

theorem Hex.Berlekamp.primeFieldProduct_X_eq_xPowSubX {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] : List.foldl (fun (acc : FpPoly p) (c : ZMod64 p) => acc * (FpPoly.X - FpPoly.C c)) 1 (ZMod64.values p) = xPowSubX 1

The variable prime-field product identity: the canonical product over field constants equals xPowSubX 1.

theorem Hex.Berlekamp.compose_xPowSubX_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (w : FpPoly p) : DensePoly.compose (xPowSubX 1) w = w.linearPow p - w

Substituting w into xPowSubX 1 = X^p - X yields linearPow w p - w. This transport takes the variable identity primeFieldProduct_X_eq_xPowSubX to its witness-substituted form.

theorem Hex.Berlekamp.primeFieldProduct_witness_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (w : FpPoly p) : List.foldl (fun (acc : FpPoly p) (c : ZMod64 p) => acc * (w - FpPoly.C c)) 1 (ZMod64.values p) = w.linearPow p - w

Substituting an arbitrary witness into the prime-field product identity.

theorem Hex.Berlekamp.dvd_primeFieldProduct_witness_of_dvd_linearPow_sub_self {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f w : FpPoly p} (hdvd : f ∣ w.linearPow p - w) : f ∣ List.foldl (fun (acc : FpPoly p) (c : ZMod64 p) => acc * (w - FpPoly.C c)) 1 (ZMod64.values p)

Divisibility by w^p - w transports to the canonical witness product.

theorem Hex.Berlekamp.isUnitPolynomial_eq_false_of_pos_degree {p : Nat} [ZMod64.Bounds p] {g : FpPoly p} (hpos : 0 < DensePoly.natDegree g) : isUnitPolynomial g = false

A polynomial of positive degree is not the unit polynomial.

theorem Hex.Berlekamp.isUnitPolynomial_of_dvd_gcd_isUnit {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f q g : FpPoly p} (hgf : g ∣ f) (hgq : g ∣ q) (hgcd : isUnitPolynomial (DensePoly.gcd f q) = true) : isUnitPolynomial g = true

If gcd(f, q) is a unit polynomial and g divides both f and q, then g is itself a unit polynomial.

theorem Hex.Berlekamp.rabinTest_imp_irreducible {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (hrabin : rabinTest f hmonic = true) : f.Irreducible

Soundness of the executable Rabin test against the project-side FpPoly.Irreducible predicate.

The proof orchestrates the foundational lemmas above. The combinatorial shape (decomposing rabinTest, picking a monic irreducible factor of size strictly between 0 and n, handling through a maximal proper divisor, and contradicting the gcd leg) lives here. The heavy mathematical content (Rabin's degree theorem in both directions, finite-field factor existence, the absolute–modular Frobenius identity, and the xPowSubX divisibility chain) is delegated to the foundational lemmas above and in RabinCore.

theorem Hex.Berlekamp.checkIrreducibilityCertificate_imp_irreducible {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : IrreducibilityCertificate) (hcheck : checkIrreducibilityCertificate f hmonic cert = true) : f.Irreducible

Accepted executable irreducibility certificates imply project-side FpPoly.Irreducible, composing checkIrreducibilityCertificate_rabinTest with the Rabin soundness theorem above.

theorem Hex.Berlekamp.checkIrreducibilityCertificateLinear_imp_irreducible {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : IrreducibilityCertificate) (hcheck : checkIrreducibilityCertificateLinear f hmonic cert = true) : f.Irreducible

The kernel-reducible certificate checker also implies project-side FpPoly.Irreducible, composing the linear checker soundness theorem with Rabin soundness.

theorem Hex.Berlekamp.checkIrreducibilityCertificateLinearIncremental_imp_irreducible {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (cert : IrreducibilityCertificate) (hcheck : checkIrreducibilityCertificateLinearIncremental f hmonic cert = true) : f.Irreducible

The incremental kernel-reducible certificate checker also implies project-side FpPoly.Irreducible.