structure Hex.Berlekamp.SplitResult (p : Nat) [ZMod64.Bounds p] : Type

Result of one Berlekamp kernel-witness split search.

• splitConstant : ZMod64 p

  The field element whose kernel witness produced the split.

• factor : FpPoly p

  The first nontrivial factor found by the split.

• cofactor : FpPoly p

  The exact quotient by factor.

structure Hex.Berlekamp.Factorization (p : Nat) [ZMod64.Bounds p] : Type

Public result of executable Berlekamp factorization.

• input : FpPoly p

  The polynomial supplied to Berlekamp factorization.

• factors : List (FpPoly p)

  The returned monic irreducible factors, with repetition.

def Hex.Berlekamp.factorProduct {p : Nat} [ZMod64.Bounds p] (factors : List (FpPoly p)) : FpPoly p

Multiply a list of F_p[x] factors in stored order, starting from 1.

Equations

• Hex.Berlekamp.factorProduct factors = List.foldl (fun (acc factor : Hex.FpPoly p) => acc * factor) 1 factors

def Hex.Berlekamp.Factorization.product {p : Nat} [ZMod64.Bounds p] (result : Factorization p) : FpPoly p

Product of the factors returned by a Factorization.

Equations

• result.product = Hex.Berlekamp.factorProduct result.factors

@[simp]

theorem Hex.Berlekamp.factorProduct_nil {p : Nat} [ZMod64.Bounds p] : factorProduct [] = 1

Empty-list base case for factorProduct.

@[simp]

theorem Hex.Berlekamp.Factorization.product_def {p : Nat} [ZMod64.Bounds p] (result : Factorization p) : result.product = factorProduct result.factors

Unfold a Factorization's product to the factorProduct of its stored factors.

def Hex.Berlekamp.splitFactorAt {p : Nat} [ZMod64.Bounds p] (f witness : FpPoly p) (c : ZMod64 p) : FpPoly p

The gcd candidate attached to one field constant c.

Equations

• Hex.Berlekamp.splitFactorAt f witness c = Hex.DensePoly.gcd f (witness - Hex.FpPoly.C c)

def Hex.Berlekamp.splitFactorCached {p : Nat} [ZMod64.Bounds p] (f witness reduced : FpPoly p) (c : ZMod64 p) : FpPoly p

GCD candidate that resumes the reference Euclidean sequence from a cached witness remainder only when the current factor is positive-degree and strictly smaller than the original witness. This is exposed so the compiled profiler can exercise the production primitive directly; factorization clients should normally use kernelWitnessSplit?.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.Berlekamp.splitFactorCached_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f witness : FpPoly p) (c : ZMod64 p) : splitFactorCached f witness (witness % f) c = splitFactorAt f witness c

With the actual witness remainder cached, splitFactorCached is exactly the reference candidate, including its unnormalised executable representative.

def Hex.Berlekamp.kernelWitnessSplit? {p : Nat} [ZMod64.Bounds p] (f witness : FpPoly p) : Option (SplitResult p)

Search the Berlekamp split candidates gcd(f, h - c) over all constants c : F_p, returning the first nontrivial factorization found.

A witness w can only split f when w mod f is nonconstant: every candidate gcd(f, w - c) reduces to gcd(f, (w mod f) - c), which is f or a unit (never a proper factor) once w mod f is a field constant. The leading (witness % f).size ≤ 1 guard skips the whole p-wide constant sweep in that case; the dominant cost once a factor is already irreducible, since every kernel witness is then constant modulo it. The guard is value-preserving: kernelWitnessSplitAux_none_of_mod_size_le_one proves the skipped sweep would have returned none (over a field), so this agrees with the unguarded search at every input. When the current factor has positive degree and is strictly smaller than the original witness, the sweep also resumes each GCD from this cached remainder with the reference execution's remaining fuel; cachedSplitAux_eq proves the exact representative and result are unchanged over a prime modulus, which is the intended domain of this Berlekamp API. This cannot be an @[csimp] swap: the optimized aux has an extra cached-remainder argument and its equality proof needs PrimeModulus, so the reference aux instead remains intact behind an explicit equality.

Equations

• Hex.Berlekamp.kernelWitnessSplit? f witness = if Hex.DensePoly.size (witness % f) ≤ 1 then none else Hex.Berlekamp.cachedSplitAux✝ f witness (witness % f) p 0

def Hex.Berlekamp.rootScanBudget {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : Bool

Budget for the residue scan of the root-extraction path. Two tests, both read off the degree and the field size alone, so the decision is deterministic and reads nothing about the coefficients of f.

deg f ≤ p is necessary: F_p has p elements, so a polynomial with deg f distinct roots in F_p cannot have degree above p. A scan of a higher-degree input can never succeed, so it is never started.

25 * p ≤ (deg f)^2 keeps the scan cheap against the work it would replace. The scan is one Horner evaluation per residue, p * deg f modular multiplications; the fixed-space matrix multiplies deg f polynomials modulo f, each product quadratic in the degree, so about (deg f)^3. The test therefore admits the scan only when it costs about a twenty-fifth of the matrix build alone. Measured on the diagnostic grid of issue #9157, an admitted-but-rejected scan costs between 0.8% and 2.3% of berlekampFactor, falling as the degree grows.

Together the two tests select 5 √p ≤ deg f ≤ p: a completely split image is a plausible thing to meet only when the degree is comparable to the field size.

Equations

• Hex.Berlekamp.rootScanBudget f = (decide (2 ≤ Hex.DensePoly.size f) && decide (Hex.DensePoly.size f ≤ p + 1) && decide (25 * p ≤ (Hex.DensePoly.size f - 1) * (Hex.DensePoly.size f - 1)))

def Hex.Berlekamp.rootFactorsOf {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (roots : List (ZMod64 p)) : Option (List (FpPoly p))

The length test of the root-extraction path: a list of roots accounts for all of f exactly when there are deg f of them, and then the monic linear factors it names are the complete factorization.

Equations

• Hex.Berlekamp.rootFactorsOf f roots = if roots.length + 1 = Hex.DensePoly.size f then some (List.map Hex.Berlekamp.primeFieldLinearFactor roots) else none

def Hex.Berlekamp.rootFactors? {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : Option (List (FpPoly p))

The root-extraction path: enumerate the roots of f in F_p and, when there are deg f of them, return the corresponding monic linear factors.

A squarefree f splits into distinct linear factors exactly when it has deg f roots in F_p, and the scan is its own certificate: the length test is what makes the result sound, so no separate complete-splitting test is computed and no Boolean is trusted unchecked. Hex.Berlekamp.eq_foldl_rootsIn_of_length turns the length test into the reconstruction ∏ (X - rᵢ) = f.

Returning none costs the scan; rootScanBudget bounds that cost.

Equations

• Hex.Berlekamp.rootFactors? f = if Hex.Berlekamp.rootScanBudget f = true then Hex.Berlekamp.rootFactorsOf f (Hex.Berlekamp.rootsIn f) else none

def Hex.Berlekamp.berlekampFactor {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) [ZMod64.PrimeModulus p] : Factorization p

Compute the Berlekamp factorization of a monic polynomial over F_p.

There is one selection point. When the residue scan is affordable and finds deg f roots, f is the product of the corresponding monic linear factors and those are returned directly. Otherwise the fixed-space kernel of Q_f - I is built and the input is fully split with the resulting kernel representatives. Both branches return factors whose product is f; the theorems below are proved for the two branches separately and stated only about berlekampFactor. The root-extraction branch emits monic linear factors; the kernel branch emits raw gcd leaves, monic only up to a unit, whose irreducibility comes from berlekampFactor_factors_irreducible on a square-free input.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.Berlekamp.berlekampFactor_factors_of_rootFactors_some {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) {fs : List (FpPoly p)} (h : rootFactors? f = some fs) : (berlekampFactor f hmonic).factors = fs

The root-extraction branch of berlekampFactor.

theorem Hex.Berlekamp.rootFactors?_some_spec {p : Nat} [ZMod64.Bounds p] {f : FpPoly p} {fs : List (FpPoly p)} (h : rootFactors? f = some fs) : 2 ≤ DensePoly.size f ∧ (rootsIn f).length + 1 = DensePoly.size f ∧ fs = List.map primeFieldLinearFactor (rootsIn f)

What a successful root extraction records: the input has positive degree, the scan found deg f roots, and the returned factors are their monic linear factors.

theorem Hex.Berlekamp.rootFactors?_eq_none_of_size_le_one {p : Nat} [ZMod64.Bounds p] {f : FpPoly p} (hsize : DensePoly.size f ≤ 1) : rootFactors? f = none

Root extraction never fires on a constant: the budget requires positive degree.

theorem Hex.Berlekamp.factorProduct_rootFactors {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {fs : List (FpPoly p)} (hmonic : DensePoly.Monic f) (h : rootFactors? f = some fs) : factorProduct fs = f

Reconstruction. The monic linear factors of the enumerated roots multiply back to f.

theorem Hex.Berlekamp.rootFactors_ne_nil {p : Nat} [ZMod64.Bounds p] {f : FpPoly p} {fs : List (FpPoly p)} (h : rootFactors? f = some fs) : fs ≠ []

The root-extraction branch emits one factor per root, and the budget forces f to have positive degree, so the result is never empty.

theorem Hex.Berlekamp.mem_rootFactors_size {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {fs : List (FpPoly p)} (h : rootFactors? f = some fs) (g : FpPoly p) : g ∈ fs → DensePoly.size g = 2

Every factor of the root-extraction branch is genuinely linear.

theorem Hex.Berlekamp.mem_rootFactors_pos_degree {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {fs : List (FpPoly p)} (h : rootFactors? f = some fs) (g : FpPoly p) : g ∈ fs → 0 < DensePoly.natDegree g

Every factor of the root-extraction branch has degree one, hence positive degree.

theorem Hex.Berlekamp.rootFactors_nodup {p : Nat} [ZMod64.Bounds p] {f : FpPoly p} {fs : List (FpPoly p)} (h : rootFactors? f = some fs) : fs.Nodup

The root-extraction branch returns distinct factors: distinct roots give distinct linear factors, and the residue scan lists each root once.

theorem Hex.Berlekamp.splitFactorAt_spec {p : Nat} [ZMod64.Bounds p] (f witness : FpPoly p) (c : ZMod64 p) : splitFactorAt f witness c = DensePoly.gcd f (witness - FpPoly.C c)

Definitional unfolding of splitFactorAt to its underlying gcd candidate.

theorem Hex.Berlekamp.kernelWitnessSplit_product_spec {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f witness : FpPoly p) (r : SplitResult p) (hsplit : kernelWitnessSplit? f witness = some r) : r.factor * r.cofactor = f

Any successful Berlekamp split records a factor and cofactor whose product is the original polynomial.

theorem Hex.Berlekamp.kernelWitnessSplit_nontrivial {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f witness : FpPoly p) (r : SplitResult p) (hsplit : kernelWitnessSplit? f witness = some r) : (!DensePoly.isZero r.factor) = true ∧ r.factor ≠ 1 ∧ r.factor ≠ f

Any successful Berlekamp split is nontrivial: the returned factor is neither 0, 1, nor the full input polynomial.

theorem Hex.Berlekamp.kernelWitnessSplit_size_lt {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f witness : FpPoly p) (r : SplitResult p) (hsplit : kernelWitnessSplit? f witness = some r) : DensePoly.size r.factor < DensePoly.size f

Any successful Berlekamp split returns a factor strictly smaller in size than the input. This is the strict-descent companion of kernelWitnessSplit_nontrivial and is what drives the Nodup invariant on the running factor list.

theorem Hex.Berlekamp.kernelWitnessSplit?_some_of_nontrivial_splitFactorAt {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f witness : FpPoly p) (c : ZMod64 p) (hnotZero : (!DensePoly.isZero (splitFactorAt f witness c)) = true) (hdegree : DensePoly.degree? (splitFactorAt f witness c) ≠ some 0) (hsize_lt : DensePoly.size (splitFactorAt f witness c) < DensePoly.size f) : ∃ (r : SplitResult p), kernelWitnessSplit? f witness = some r

Executable search reflection for one field constant: if the gcd candidate attached to c is nonzero, nonconstant, and strictly smaller in size than the input, then the guarded Berlekamp witness search succeeds. The guard cannot fire here: a genuine split means witness is nonconstant modulo f.

theorem Hex.Berlekamp.kernelWitnessSplit?_none_scale {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {c : ZMod64 p} (hc : c ≠ 0) (g witness : FpPoly p) (h : kernelWitnessSplit? g witness = none) : kernelWitnessSplit? (DensePoly.scale c g) witness = none

Transport of a failed Berlekamp split search across a unit scaling: if no kernel-witness split of g is found, none is found for scale c g either (c ≠ 0). Lets callers move a no-split fact from a raw factor to its monic associate.

theorem Hex.Berlekamp.factorProduct_cons {p : Nat} [ZMod64.Bounds p] (x : FpPoly p) (xs : List (FpPoly p)) : factorProduct (x :: xs) = x * factorProduct xs

Cons-expansion for factorProduct: pulling the head factor out of the running product. Useful for downstream proofs that reason about factorProduct without unfolding the underlying List.foldl.

theorem Hex.Berlekamp.factorProduct_append {p : Nat} [ZMod64.Bounds p] (xs ys : List (FpPoly p)) : factorProduct (xs ++ ys) = factorProduct xs * factorProduct ys

factorProduct distributes over list append.

theorem Hex.Berlekamp.factorProduct_berlekampFactor {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) : factorProduct (berlekampFactor f hmonic).factors = f

The Berlekamp factor list's product equals the input polynomial. Fully splitting preserves factorProduct without using square-freeness, so the product equality holds for every monic input.

theorem Hex.Berlekamp.prod_berlekampFactor {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) [ZMod64.PrimeModulus p] : (berlekampFactor f hmonic).product = f

The executable Berlekamp factorization preserves the input polynomial as the product of the returned factors for any monic input.

theorem Hex.Berlekamp.berlekampFactor_factors_ne_nil {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) [ZMod64.PrimeModulus p] : (berlekampFactor f hmonic).factors ≠ []

Executable Berlekamp factorization always retains at least one factor.

theorem Hex.Berlekamp.kernelWitnessSplit_factor_pos_degree {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f witness : FpPoly p) (r : SplitResult p) (hsplit : kernelWitnessSplit? f witness = some r) : 0 < DensePoly.natDegree r.factor

A successful kernel-witness split returns a factor of positive degree, so the recursive splitter always makes progress.

theorem Hex.Berlekamp.kernelWitnessSplit?_none_of_berlekampFactor_factors_length_le_one {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) [ZMod64.PrimeModulus p] (hsmall : (berlekampFactor f hmonic).factors.length ≤ 1) (w : FpPoly p) : w ∈ (fixedSpaceKernel f hmonic).toList → kernelWitnessSplit? f w = none

Structural lemma about berlekampFactor output: if its factors list has length at most one, then every fixed-space kernel witness yields kernelWitnessSplit? = none. This is the loop-tracing half of the parent Berlekamp completeness theorem; the algebraic half (no kernel-witness split forces irreducibility for square-free monic inputs) belongs to a separate Mathlib-free finite-field module.

theorem Hex.Berlekamp.mul_dvd_factorProduct_of_mem_of_ne {p : Nat} [ZMod64.Bounds p] {xs : List (FpPoly p)} (h_nodup : xs.Nodup) {a b : FpPoly p} (ha : a ∈ xs) (hb : b ∈ xs) (hab : a ≠ b) : a * b ∣ factorProduct xs

Two distinct elements of a Nodup list of FpPoly p have a product that divides the list's product.

theorem Hex.Berlekamp.berlekampFactor_factors_nodup_of_no_squared {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) [ZMod64.PrimeModulus p] (h_no_squared : ∀ (g : FpPoly p), g * g ∣ f → ¬0 < DensePoly.natDegree g) : (berlekampFactor f hmonic).factors.Nodup

Abstract form of berlekampFactor.factors.Nodup: when no positive-degree polynomial squares to a divisor of f, the executable Berlekamp factor list has no duplicates. The Mathlib-free squareness-implies-irreducibility chain discharges this hypothesis from gcd f f' = 1; see Hex.Berlekamp.berlekampFactor_factors_nodup in HexBerlekamp/RabinSoundness.lean.

theorem Hex.Berlekamp.berlekampFactor_factors_pairwise_coprime {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (h_no_squared : ∀ (g : FpPoly p), g * g ∣ f → ¬0 < DensePoly.natDegree g) : List.Pairwise (fun (a b : FpPoly p) => ∀ (d : FpPoly p), d ∣ a → d ∣ b → ¬0 < DensePoly.natDegree d) (berlekampFactor f hmonic).factors

Abstract pairwise-coprime form of berlekampFactor's output: when no positive-degree polynomial squares to a divisor of f, distinct factors in the returned list share no positive-degree common divisor. This strengthens berlekampFactor_factors_nodup_of_no_squared from "distinct values" to "no shared positive-degree divisor". The Mathlib-free squareness-implies- irreducibility chain discharges the no-squared hypothesis from gcd f f' = 1; see callers that pair this with isUnitPolynomial_of_squareFree_of_squared_dvd.

theorem Hex.Berlekamp.berlekampFactor_factors_pos_degree {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (hf_pos : 0 < DensePoly.natDegree f) (g : FpPoly p) : g ∈ (berlekampFactor f hmonic).factors → 0 < DensePoly.natDegree g

Abstract form of berlekampFactor's output factor-degree positivity: if the input polynomial has positive degree, then every factor in the executable Berlekamp factor list has positive degree. The squareness-free hypothesis needed by berlekampFactor_factors_nodup_of_no_squared is not needed here: positivity is preserved by every split regardless of square-freeness.

theorem Hex.Berlekamp.berlekampFactor_factors_eq_singleton_of_size_le_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (hsize : DensePoly.size f ≤ 1) : (berlekampFactor f hmonic).factors = [f]

For a monic input of size ≤ 1, the executable Berlekamp factor list is exactly the singleton [f]. A polynomial of size ≤ 1 has no positive-degree divisors, so it admits no kernel-witness split and fullySplit emits it as a leaf.

theorem Hex.Berlekamp.berlekampFactor_factors_ne_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (g : FpPoly p) : g ∈ (berlekampFactor f hmonic).factors → g ≠ 0

Every factor in the Berlekamp factor list is nonzero. Splits the positive- degree case (where every factor has positive degree via berlekampFactor_factors_pos_degree) from the size-≤-1 case (where the factor list is the singleton [f] and f is monic, hence nonzero).

theorem Hex.Berlekamp.kernelWitnessSplit?_none_of_berlekampFactor_factors {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (g : FpPoly p) : g ∈ (berlekampFactor f hmonic).factors → ∀ (w : FpPoly p), w ∈ (fixedSpaceKernel f hmonic).toList → kernelWitnessSplit? g w = none

Per-factor no-split. Every factor returned by the executable Berlekamp factorization of a monic input resists every fixed-space kernel-witness split. The f.size + 1 fuel always suffices to reach the witness-irreducible leaves.

theorem Hex.Berlekamp.berlekampFactor_factors_dvd {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (g : FpPoly p) : g ∈ (berlekampFactor f hmonic).factors → g ∣ f

Every factor returned by the executable Berlekamp factorization divides the input. Immediate from factorProduct_berlekampFactor.