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

The linear factor corresponding to a prime-field residue.

Equations

• Hex.Berlekamp.primeFieldLinearFactor c = Hex.FpPoly.X - Hex.FpPoly.C c

theorem Hex.Berlekamp.primeFieldLinearFactor_coeff_one {p : Nat} [ZMod64.Bounds p] (c : ZMod64 p) : DensePoly.coeff (primeFieldLinearFactor c) 1 = 1

The listed prime-field linear factors are genuinely degree-one candidates.

theorem Hex.Berlekamp.primeFieldLinearFactor_ne_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (c : ZMod64 p) : primeFieldLinearFactor c ≠ 0

No listed prime-field linear factor is the zero polynomial.

theorem Hex.Berlekamp.primeFieldLinearFactor_size {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (c : ZMod64 p) : DensePoly.size (primeFieldLinearFactor c) = 2

Each prime-field linear factor has size 2 (it is genuinely degree 1).

theorem Hex.Berlekamp.primeFieldLinearFactor_monic {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (c : ZMod64 p) : DensePoly.Monic (primeFieldLinearFactor c)

Each prime-field linear factor is monic.

theorem Hex.Berlekamp.primeFieldLinearFactor_degree {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (c : ZMod64 p) : DensePoly.natDegree (primeFieldLinearFactor c) = 1

Each prime-field linear factor has degree exactly one.

theorem Hex.Berlekamp.primeFieldLinearFactor_injective {p : Nat} [ZMod64.Bounds p] {c d : ZMod64 p} (h : primeFieldLinearFactor c = primeFieldLinearFactor d) : c = d

Distinct residues give distinct linear factors.

theorem Hex.Berlekamp.primeFieldLinearFactor_distinct_common_dvd_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {c d : ZMod64 p} (hcd : c ≠ d) (e : FpPoly p) (hec : e ∣ primeFieldLinearFactor c) (hed : e ∣ primeFieldLinearFactor d) : e ∣ 1

Distinct prime-field linear factors are coprime: any common divisor is a unit.

theorem Hex.Berlekamp.foldl_primeFieldLinearFactor_dvd {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (xs : List (ZMod64 p)) (acc : FpPoly p) : xs.Nodup → acc ∣ f → (∀ (c : ZMod64 p), c ∈ xs → primeFieldLinearFactor c ∣ f) → (∀ (c : ZMod64 p), c ∈ xs → ∀ (e : FpPoly p), e ∣ acc → e ∣ primeFieldLinearFactor c → e ∣ 1) → List.foldl (fun (acc : FpPoly p) (c : ZMod64 p) => acc * (FpPoly.X - FpPoly.C c)) acc xs ∣ f

Foldl-shape divisibility: if every linear factor in xs divides f, the cumulative (acc * ∏ (X - C cᵢ)) divides f as long as acc is coprime with each new linear factor.

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

The constant polynomial 1 over a prime modulus is nonzero.

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

The constant polynomial 1 over a prime modulus has size 1.

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

The constant polynomial 1 over a prime modulus is monic.

theorem Hex.Berlekamp.foldl_size_and_monic {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (xs : List (ZMod64 p)) (acc : FpPoly p) : acc ≠ 0 → DensePoly.Monic acc → List.foldl (fun (acc : FpPoly p) (c : ZMod64 p) => acc * (FpPoly.X - FpPoly.C c)) acc xs ≠ 0 ∧ (List.foldl (fun (acc : DensePoly (ZMod64 p)) (c : ZMod64 p) => acc * (FpPoly.X - FpPoly.C c)) acc xs).Monic ∧ DensePoly.size (List.foldl (fun (acc : FpPoly p) (c : ZMod64 p) => acc * (FpPoly.X - FpPoly.C c)) acc xs) = DensePoly.size acc + xs.length

Foldl induction: size grows by one for each linear factor multiplied in.

def Hex.Berlekamp.rootsBelow {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : Nat → List (ZMod64 p) → List (ZMod64 p)

The roots of f among the residues ofNat p k for k < n, listed in increasing k and consed onto acc.

Counting down and consing keeps the loop tail-recursive and allocates only the roots it keeps, so the scan holds deg f residues rather than the whole of F_p. Filtering ZMod64.values p instead would allocate p residues, and the budget in Hex.Berlekamp.rootScanBudget only bounds the scan against the kernel computation it replaces, not in the absolute.

Equations

• Hex.Berlekamp.rootsBelow f 0 x✝ = x✝
• Hex.Berlekamp.rootsBelow f n.succ x✝ = Hex.Berlekamp.rootsBelow f n (if Hex.DensePoly.evalImpl f (Hex.ZMod64.ofNat p n) = 0 then Hex.ZMod64.ofNat p n :: x✝ else x✝)

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

The roots of f in F_p, listed in canonical residue order.

One Horner evaluation per residue, so p * f.size modular multiplications. Callers gate the scan on the field size; see Hex.Berlekamp.rootScanBudget.

Equations

• Hex.Berlekamp.rootsIn f = Hex.Berlekamp.rootsBelow f p []

theorem Hex.Berlekamp.rootsIn_eq_filter {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : rootsIn f = List.filter (fun (c : ZMod64 p) => decide (DensePoly.evalImpl f c = 0)) (ZMod64.values p)

The scan enumerates exactly the vanishing residues of the canonical residue list: the loop is the filter, without materializing the list.

theorem Hex.Berlekamp.mem_rootsIn_iff {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (c : ZMod64 p) : c ∈ rootsIn f ↔ DensePoly.eval f c = 0

Membership in rootsIn is exactly vanishing of the evaluation.

theorem Hex.Berlekamp.rootsIn_nodup {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : (rootsIn f).Nodup

The root list has no duplicates: it enumerates the duplicate-free residue list.

theorem Hex.Berlekamp.nodup_map_primeFieldLinearFactor {p : Nat} [ZMod64.Bounds p] {xs : List (ZMod64 p)} (h : xs.Nodup) : (List.map primeFieldLinearFactor xs).Nodup

Distinct residues give a duplicate-free list of monic linear factors.

theorem Hex.Berlekamp.primeFieldLinearFactor_dvd_of_mem_rootsIn {p : Nat} [ZMod64.Bounds p] {f : FpPoly p} {c : ZMod64 p} (hc : c ∈ rootsIn f) : primeFieldLinearFactor c ∣ f

Every listed root contributes its monic linear factor as a divisor of f.

theorem Hex.Berlekamp.eq_of_dvd_of_monic_of_size_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {a f : FpPoly p} (hdvd : a ∣ f) (ha : DensePoly.Monic a) (hf : DensePoly.Monic f) (hf_ne : f ≠ 0) (hsize : DensePoly.size a = DensePoly.size f) : a = f

A monic divisor of a monic polynomial of the same size is that polynomial.

theorem Hex.Berlekamp.eq_foldl_rootsIn_of_length {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hmonic : DensePoly.Monic f) (hlen : (rootsIn f).length + 1 = DensePoly.size f) : List.foldl (fun (acc : FpPoly p) (c : ZMod64 p) => acc * primeFieldLinearFactor c) 1 (rootsIn f) = f

Reconstruction from roots. When the residue scan finds deg f distinct roots of a monic f, the corresponding monic linear factors multiply back to f: their product divides f (pairwise coprime divisors), is monic, and has the same size, so it is f itself.