From d2bf4bbfed7858aa93944a4995b7f5e0f03addb1 Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Tue, 9 Jun 2026 16:51:48 +0300
Subject: [PATCH 01/18] =?UTF-8?q?feat(univariate):=20Cantor=E2=80=93Zassen?=
 =?UTF-8?q?haus=20linear-factor=20splitter=20(algorithm=20+=20soundness)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add an executable Cantor–Zassenhaus equal-degree (degree-one) splitter for
field-root products over odd-cardinality finite fields, plugging into the
`Univariate/Roots` `LinearFactorProductSplitter` interface alongside the
smooth-subgroup splitter (PR #244).

- czRefine / czSplitWithShifts / czSplitLinearFactors: executable algorithm.
- czSound: every emitted factor is linear (proved).
- czShift_eq_linearFactor: the shift bucket `X + s` is `linearFactor (-s)`,
  the first link of completeness (prime-field isolation, no QR needed).
- czLinearFactorProductSplitterOf: adapter taking `complete` as a parameter.

Completeness (prime fields) is in progress on this branch.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 CompPoly.lean                                 |   1 +
 .../Univariate/Roots/CantorZassenhaus.lean    | 176 ++++++++++++++++++
 2 files changed, 177 insertions(+)
 create mode 100644 CompPoly/Univariate/Roots/CantorZassenhaus.lean

diff --git a/CompPoly.lean b/CompPoly.lean
index 867fadc3..7a7f63d0 100644
--- a/CompPoly.lean
+++ b/CompPoly.lean
@@ -177,6 +177,7 @@ import CompPoly.Univariate.Raw.Ops
 import CompPoly.Univariate.Raw.Proofs
 import CompPoly.Univariate.Roots
 import CompPoly.Univariate.Roots.Backend
+import CompPoly.Univariate.Roots.CantorZassenhaus
 import CompPoly.Univariate.Roots.Context
 import CompPoly.Univariate.Roots.Correctness
 import CompPoly.Univariate.Roots.Enumeration
diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
new file mode 100644
index 00000000..16d97aa6
--- /dev/null
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -0,0 +1,176 @@
+/-
+Copyright (c) 2026 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dimitrios Mitsios
+-/
+
+import CompPoly.Univariate.Roots.Splitter
+
+/-!
+# Cantor–Zassenhaus Linear-Factor Splitting
+
+Executable equal-degree (degree-one) splitter for field-root products over a
+finite field of odd cardinality `q`, following the Cantor–Zassenhaus
+root-finding method [CZ81]. It plugs into the shared
+`LinearFactorProductSplitter` interface alongside the smooth-subgroup splitter.
+
+The generic root pipeline first reduces to a squarefree product of linear
+factors `p = ∏ (X - rᵢ)` via `gcd(f, X^q - X)` (see `Roots.RootProduct`); this
+module only performs the *separation* of those linear factors.
+
+## Method
+
+For a shift `s : F`, with `w = (X + s)^((q-1)/2) mod p`:
+
+* `gcd(p, X + s)` isolates the root `r = -s` (if present);
+* `gcd(p, w - 1)` collects roots `r` with `r + s` a nonzero square;
+* `gcd(p, w + 1)` collects roots `r` with `r + s` a non-square.
+
+Iterating over a sequence of shifts separates all roots: for any two distinct
+roots, some shift sends them to different quadratic-residue classes. The split
+is correct for *every* shift; the shift sequence only governs termination, so no
+probabilistic reasoning enters correctness. See `czSound` (proved here) and the
+`complete` obligation, supplied to `czLinearFactorProductSplitterOf`.
+
+## References
+
+* [Cantor, D. G., and Zassenhaus, H., *A new algorithm for factoring
+    polynomials over finite fields*][CZ81]
+-/
+
+namespace CompPoly
+
+namespace CPolynomial
+
+namespace Roots
+
+namespace FiniteField
+
+variable {F : Type*} [Field F] [BEq F] [LawfulBEq F]
+
+/-- `(X + s)^exponent mod modulus`, lifted back to canonical polynomials.
+The Cantor–Zassenhaus discriminating power, generalising `xPowModWith` to the
+shifted base `X + s`. -/
+def shiftedPowModWith (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
+    (modulus : CPolynomial F) (s : F) (exponent : Nat) : CPolynomial F :=
+  CPolynomial.ofArray
+    (CPolynomial.Raw.powModWith M D modulus.val
+      (CPolynomial.X + CPolynomial.C s).val exponent)
+
+/-- One Cantor–Zassenhaus refinement against shift `s`: returns the three
+sub-factors `(gcd(p, X+s), gcd(p, w-1), gcd(p, w+1))` where `w` is the shifted
+discriminating power. Their product is `p` (for squarefree `p` of odd `q`). -/
+def czRefine (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
+    (q : Nat) (s : F) (p : CPolynomial F) :
+    CPolynomial F × CPolynomial F × CPolynomial F :=
+  let w := shiftedPowModWith M D p s ((q - 1) / 2)
+  let gZero := CPolynomial.monicNormalize (CPolynomial.gcdMonic p (CPolynomial.X + CPolynomial.C s))
+  let gRes := CPolynomial.monicNormalize (CPolynomial.gcdMonic p (w - 1))
+  let gNon := CPolynomial.monicNormalize (CPolynomial.gcdMonic p (w + 1))
+  (gZero, gRes, gNon)
+
+/-- The shift bucket `X + s` is exactly the monic linear factor with root `-s`.
+First step of the completeness argument: at shift `s = -a` the `gcd(p, X + s)`
+bucket isolates the root `a` directly, with no quadratic-residue reasoning. The
+residue buckets `w ± 1` are needed only for fields whose elements are not all
+reached by the prime-subfield shift schedule (extension fields). -/
+theorem czShift_eq_linearFactor (s : F) :
+    (CPolynomial.X + CPolynomial.C s : CPolynomial F) = CPolynomial.linearFactor (-s) := by
+  rw [CPolynomial.linearFactor, neg_neg, add_comm]
+
+/-- Cantor–Zassenhaus separation driven by an explicit shift schedule
+(structural recursion on the schedule).
+
+Emits a factor only when it is recognised as a represented linear factor, so the
+output is linear by construction (`czSound`). When the schedule is exhausted on a
+still-composite factor, that factor is dropped (defensive): completeness is
+therefore conditional on the schedule separating all roots, which is the content
+of the `complete` obligation. -/
+def czSplitWithShifts (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
+    (q : Nat) : List F → CPolynomial F → Array (CPolynomial F)
+  | [], p =>
+      let p := CPolynomial.monicNormalize p
+      if isRepresentedLinearFactor p then #[p] else #[]
+  | s :: rest, p =>
+      let p := CPolynomial.monicNormalize p
+      if p == 0 || p == 1 then
+        #[]
+      else if isRepresentedLinearFactor p then
+        #[p]
+      else
+        let (gZero, gRes, gNon) := czRefine M D q s p
+        czSplitWithShifts M D q rest gZero ++
+          czSplitWithShifts M D q rest gRes ++
+            czSplitWithShifts M D q rest gNon
+
+/-- Default shift schedule: `0, 1, …, (count - 1)` cast into `F`. -/
+def czDefaultShifts (count : Nat) : List F :=
+  (List.range count).map (fun i => (Nat.cast i : F))
+
+/-- Cantor–Zassenhaus linear-factor splitting with naive polynomial arithmetic
+contexts and the default shift schedule of length `q`. -/
+def czSplitLinearFactors (q : Nat) (p : CPolynomial F) : Array (CPolynomial F) :=
+  czSplitWithShifts CPolynomial.Raw.MulContext.naive CPolynomial.Raw.ModContext.naive
+    q (czDefaultShifts q) p
+
+/-- Soundness: every factor emitted by the CZ schedule is a linear factor. -/
+theorem czSound (q : Nat) (shifts : List F) (p factor : CPolynomial F)
+    (h : factor ∈ (czSplitWithShifts CPolynomial.Raw.MulContext.naive
+      CPolynomial.Raw.ModContext.naive q shifts p).toList) :
+    IsLinearFactor factor := by
+  induction shifts generalizing p with
+  | nil =>
+      rw [czSplitWithShifts] at h
+      split at h
+      · rename_i hlin
+        have hfp : factor = CPolynomial.monicNormalize p := by simpa using h
+        subst hfp
+        exact isRepresentedLinearFactor_sound hlin
+      · simp at h
+  | cons s rest ih =>
+      rw [czSplitWithShifts] at h
+      split at h
+      · simp at h
+      · split at h
+        · rename_i hlin
+          have hfp : factor = CPolynomial.monicNormalize p := by simpa using h
+          subst hfp
+          exact isRepresentedLinearFactor_sound hlin
+        · simp only [czRefine, Array.toList_append, List.mem_append] at h
+          rcases h with (h | h) | h
+          · exact ih _ h
+          · exact ih _ h
+          · exact ih _ h
+
+/-- Build a `LinearFactorProductSplitter` from the Cantor–Zassenhaus algorithm.
+
+`sound` is discharged by `czSound`. `complete` is left as a parameter: it is the
+statement that, under `validInput`, the supplied shift schedule (here the default
+of length `q`) separates every root into its own linear factor. The proof rests
+on the quadratic-residue separation lemma (for distinct roots some shift splits
+them) and termination of the schedule — no probabilistic argument. -/
+def czLinearFactorProductSplitterOf
+    (validInput : Nat → CPolynomial F → Prop)
+    (complete :
+      ∀ q p a,
+        validInput q p →
+          p ≠ 0 →
+            CPolynomial.eval a p = 0 →
+              ∃ factor,
+                factor ∈ (czSplitLinearFactors q p).toList ∧
+                  IsLinearRootFactorCandidate factor a) :
+    LinearFactorProductSplitter F where
+  splitLinearFactors := czSplitLinearFactors
+  validInput := validInput
+  sound := by
+    intro q p factor h
+    exact czSound q (czDefaultShifts q) p factor h
+  complete := complete
+
+end FiniteField
+
+end Roots
+
+end CPolynomial
+
+end CompPoly

From 7ecc4a94bd0f603bc52769cf08ddd64a28cc24b9 Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Tue, 9 Jun 2026 16:59:55 +0300
Subject: [PATCH 02/18] feat(univariate): CZ shifted modexp evaluation
 (eval_shiftedPowModWith)

Analytic core of the quadratic-residue routing: at a root a of p,
shiftedPowModWith M D p s k evaluates to (a+s)^k, wrapping the framework's
raw_eval_powModWith_eq_pow. Plus eval_X_add_C.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .../Univariate/Roots/CantorZassenhaus.lean    | 23 +++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index 16d97aa6..2f06e8ce 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -5,6 +5,7 @@ Authors: Dimitrios Mitsios
 -/
 
 import CompPoly.Univariate.Roots.Splitter
+import CompPoly.Univariate.Roots.Correctness
 
 /-!
 # Cantor–Zassenhaus Linear-Factor Splitting
@@ -78,6 +79,28 @@ theorem czShift_eq_linearFactor (s : F) :
     (CPolynomial.X + CPolynomial.C s : CPolynomial F) = CPolynomial.linearFactor (-s) := by
   rw [CPolynomial.linearFactor, neg_neg, add_comm]
 
+/-- Evaluating the shift base `X + s` at `a` gives `a + s`. -/
+theorem eval_X_add_C (a s : F) :
+    CPolynomial.eval a (CPolynomial.X + CPolynomial.C s) = a + s := by
+  rw [CPolynomial.eval_toPoly, CPolynomial.toPoly_add, CPolynomial.X_toPoly,
+    CPolynomial.C_toPoly, Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C]
+
+/-- At a root `a` of `p`, the shifted discriminating power evaluates as
+`(a + s)^k`. This is the analytic core of the quadratic-residue routing:
+`w(a) = (a + s)^((q-1)/2)`. Wraps `raw_eval_powModWith_eq_pow`. -/
+theorem eval_shiftedPowModWith (M : CPolynomial.Raw.MulContext F)
+    (D : CPolynomial.Raw.ModContext F) (p : CPolynomial F) (s a : F) (k : Nat)
+    (hp : CPolynomial.eval a p = 0) :
+    CPolynomial.eval a (shiftedPowModWith M D p s k) = (a + s) ^ k := by
+  have hmod : (p.val : CPolynomial.Raw F).eval a = 0 := hp
+  unfold shiftedPowModWith
+  show CPolynomial.Raw.eval a
+      (CPolynomial.Raw.powModWith M D p.val (CPolynomial.X + CPolynomial.C s).val k).trim =
+      (a + s) ^ k
+  rw [CPolynomial.Raw.eval_trim_eq_eval, raw_eval_powModWith_eq_pow M D hmod k]
+  change CPolynomial.eval a (CPolynomial.X + CPolynomial.C s) ^ k = (a + s) ^ k
+  rw [eval_X_add_C]
+
 /-- Cantor–Zassenhaus separation driven by an explicit shift schedule
 (structural recursion on the schedule).
 

From da2a05515604639717b013cf36d3f5016c7dfba0 Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Tue, 9 Jun 2026 19:39:59 +0300
Subject: [PATCH 03/18] feat(univariate): CZ quadratic-residue routing lemma

czRefine_root_in_residue_bucket: for odd q and a+s != 0, a root a of p lands
in one of the residue buckets gRes/gNon. Uses Fermat (a^q=a) to show the
discriminating power (a+s)^((q-1)/2) squares to 1, hence is +/-1 at a.
Adds eval_add helper and czRefine projection lemmas.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .../Univariate/Roots/CantorZassenhaus.lean    | 64 +++++++++++++++++++
 1 file changed, 64 insertions(+)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index 2f06e8ce..4985a272 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -101,6 +101,70 @@ theorem eval_shiftedPowModWith (M : CPolynomial.Raw.MulContext F)
   change CPolynomial.eval a (CPolynomial.X + CPolynomial.C s) ^ k = (a + s) ^ k
   rw [eval_X_add_C]
 
+/-- Evaluation is additive (the library provides `eval_sub` but not `eval_add`). -/
+theorem eval_add (a : F) (p₁ p₂ : CPolynomial F) :
+    CPolynomial.eval a (p₁ + p₂) = CPolynomial.eval a p₁ + CPolynomial.eval a p₂ := by
+  rw [CPolynomial.eval_toPoly, CPolynomial.toPoly_add, Polynomial.eval_add,
+    ← CPolynomial.eval_toPoly, ← CPolynomial.eval_toPoly]
+
+/-- The quotient bucket of `czRefine` is `gcd(p, X + s)`, normalized. -/
+theorem czRefine_fst (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
+    (q : Nat) (s : F) (p : CPolynomial F) :
+    (czRefine M D q s p).1 =
+      CPolynomial.monicNormalize (CPolynomial.gcdMonic p (CPolynomial.X + CPolynomial.C s)) :=
+  rfl
+
+/-- The quadratic-residue bucket of `czRefine` is `gcd(p, w - 1)`, normalized. -/
+theorem czRefine_snd_fst (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
+    (q : Nat) (s : F) (p : CPolynomial F) :
+    (czRefine M D q s p).2.1 =
+      CPolynomial.monicNormalize
+        (CPolynomial.gcdMonic p (shiftedPowModWith M D p s ((q - 1) / 2) - 1)) :=
+  rfl
+
+/-- The non-residue bucket of `czRefine` is `gcd(p, w + 1)`, normalized. -/
+theorem czRefine_snd_snd (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
+    (q : Nat) (s : F) (p : CPolynomial F) :
+    (czRefine M D q s p).2.2 =
+      CPolynomial.monicNormalize
+        (CPolynomial.gcdMonic p (shiftedPowModWith M D p s ((q - 1) / 2) + 1)) :=
+  rfl
+
+/-- Quadratic-residue routing: for `q` odd and `a + s ≠ 0`, a root `a` of `p` is a
+root of one of the two residue buckets `gRes`/`gNon`. Uses Fermat (`a^q = a`) so
+that `((a+s)^((q-1)/2))² = 1`, hence the discriminating power is `±1` at `a`. -/
+theorem czRefine_root_in_residue_bucket
+    (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
+    (q : Nat) (hodd : Odd q) (hfrob : ∀ x : F, x ^ q = x)
+    (s a : F) (p : CPolynomial F)
+    (hp : CPolynomial.eval a p = 0) (hsa : a + s ≠ 0) :
+    CPolynomial.eval a (czRefine M D q s p).2.1 = 0 ∨
+      CPolynomial.eval a (czRefine M D q s p).2.2 = 0 := by
+  obtain ⟨m, hm⟩ := hodd
+  have hwa : CPolynomial.eval a (shiftedPowModWith M D p s ((q - 1) / 2))
+      = (a + s) ^ ((q - 1) / 2) :=
+    eval_shiftedPowModWith M D p s a ((q - 1) / 2) hp
+  have hpow : (a + s) ^ (q - 1) = 1 := by
+    have h := hfrob (a + s)
+    have hq : q = (q - 1) + 1 := by omega
+    rw [hq, pow_succ] at h
+    have hcancel : (a + s) ^ (q - 1) * (a + s) = 1 * (a + s) := by simpa using h
+    exact mul_right_cancel₀ hsa hcancel
+  have ht2 : CPolynomial.eval a (shiftedPowModWith M D p s ((q - 1) / 2))
+      * CPolynomial.eval a (shiftedPowModWith M D p s ((q - 1) / 2)) = 1 := by
+    rw [hwa, ← pow_add]
+    have hsum : (q - 1) / 2 + (q - 1) / 2 = q - 1 := by omega
+    rw [hsum, hpow]
+  rcases mul_self_eq_one_iff.mp ht2 with ht | ht
+  · left
+    rw [czRefine_snd_fst]
+    refine monicNormalize_root_of_root (gcdMonic_root_of_left_right hp ?_)
+    rw [eval_sub, eval_one, ht]; ring
+  · right
+    rw [czRefine_snd_snd]
+    refine monicNormalize_root_of_root (gcdMonic_root_of_left_right hp ?_)
+    rw [eval_add, eval_one, ht]; ring
+
 /-- Cantor–Zassenhaus separation driven by an explicit shift schedule
 (structural recursion on the schedule).
 

From 30a889aee863a3acbf4f4c91b2757712ef5f0715 Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Tue, 9 Jun 2026 19:46:10 +0300
Subject: [PATCH 04/18] feat(univariate): CZ root-isolation lemma (gcd with
 linear factor)

gcdMonic_linearFactor_of_root: at a root a of p, gcdMonic p (linearFactor a)
= linearFactor a, via toPoly + normalize_eq_normalize + Monic.normalize_eq_self.
This makes the s=-a quotient bucket of czRefine isolate the root. Adds
linearFactor_toPoly.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .../Univariate/Roots/CantorZassenhaus.lean    | 31 +++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index 4985a272..3d64326b 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -165,6 +165,37 @@ theorem czRefine_root_in_residue_bucket
     refine monicNormalize_root_of_root (gcdMonic_root_of_left_right hp ?_)
     rw [eval_add, eval_one, ht]; ring
 
+/-- `linearFactor a` maps to the Mathlib monic linear polynomial `X - C a`. -/
+theorem linearFactor_toPoly (a : F) :
+    (CPolynomial.linearFactor a).toPoly = (Polynomial.X - Polynomial.C a) := by
+  rw [CPolynomial.linearFactor, CPolynomial.toPoly_add, CPolynomial.C_toPoly,
+    CPolynomial.X_toPoly, Polynomial.C_neg]
+  ring
+
+/-- Isolation: at a root `a` of `p`, the monic gcd of `p` with the linear factor
+`X - a` is exactly that linear factor. This makes the `s = -a` quotient bucket of
+`czRefine` equal to `linearFactor a`, isolating the root. -/
+theorem gcdMonic_linearFactor_of_root {p : CPolynomial F} {a : F}
+    (hroot : CPolynomial.eval a p = 0) :
+    CPolynomial.gcdMonic p (CPolynomial.linearFactor a) = CPolynomial.linearFactor a := by
+  classical
+  have hisroot : p.toPoly.IsRoot a := by
+    rw [Polynomial.IsRoot.def, ← CPolynomial.eval_toPoly]; exact hroot
+  have hdvd : (Polynomial.X - Polynomial.C a) ∣ p.toPoly :=
+    Polynomial.dvd_iff_isRoot.mpr hisroot
+  have hg1 : EuclideanDomain.gcd p.toPoly (Polynomial.X - Polynomial.C a) ∣
+      (Polynomial.X - Polynomial.C a) := EuclideanDomain.gcd_dvd_right _ _
+  have hg2 : (Polynomial.X - Polynomial.C a) ∣
+      EuclideanDomain.gcd p.toPoly (Polynomial.X - Polynomial.C a) :=
+    EuclideanDomain.dvd_gcd hdvd dvd_rfl
+  have htoPoly : (CPolynomial.gcdMonic p (CPolynomial.linearFactor a)).toPoly =
+      (CPolynomial.linearFactor a).toPoly := by
+    rw [CPolynomial.gcdMonic_toPoly_eq_normalize_gcd, linearFactor_toPoly,
+      normalize_eq_normalize hg1 hg2, (Polynomial.monic_X_sub_C a).normalize_eq_self]
+  apply CPolynomial.eq_iff_coeff.mpr
+  intro i
+  rw [CPolynomial.coeff_toPoly, CPolynomial.coeff_toPoly, htoPoly]
+
 /-- Cantor–Zassenhaus separation driven by an explicit shift schedule
 (structural recursion on the schedule).
 

From d6286caadd626c3923ab143f0a945ec21006e7c4 Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Tue, 9 Jun 2026 19:48:58 +0300
Subject: [PATCH 05/18] feat(univariate): CZ monicNormalize_linearFactor

monicNormalize fixes the monic linear factor X - a, completing the s=-a
isolation chain (gZero = linearFactor a).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 CompPoly/Univariate/Roots/CantorZassenhaus.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index 3d64326b..fed07802 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -196,6 +196,18 @@ theorem gcdMonic_linearFactor_of_root {p : CPolynomial F} {a : F}
   intro i
   rw [CPolynomial.coeff_toPoly, CPolynomial.coeff_toPoly, htoPoly]
 
+/-- `monicNormalize` fixes the already-monic linear factor `X - a`. -/
+theorem monicNormalize_linearFactor (a : F) :
+    CPolynomial.monicNormalize (CPolynomial.linearFactor a) = CPolynomial.linearFactor a := by
+  classical
+  have htoPoly : (CPolynomial.monicNormalize (CPolynomial.linearFactor a)).toPoly =
+      (CPolynomial.linearFactor a).toPoly := by
+    rw [CPolynomial.monicNormalize_toPoly_eq_normalize, linearFactor_toPoly,
+      (Polynomial.monic_X_sub_C a).normalize_eq_self]
+  apply CPolynomial.eq_iff_coeff.mpr
+  intro i
+  rw [CPolynomial.coeff_toPoly, CPolynomial.coeff_toPoly, htoPoly]
+
 /-- Cantor–Zassenhaus separation driven by an explicit shift schedule
 (structural recursion on the schedule).
 

From ebd6b2951a0a8f7ee42272644d43709f9c176d2c Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Tue, 9 Jun 2026 19:53:11 +0300
Subject: [PATCH 06/18] feat(univariate): CZ base emit lemma +
 represented-factor helpers

czSplit_emits: a normalized represented linear factor with root a is emitted
as a candidate. Plus represented_coeff_one_ne_zero, represented_zero_one_eq_false.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .../Univariate/Roots/CantorZassenhaus.lean    | 32 +++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index fed07802..e35b258e 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -272,6 +272,38 @@ theorem czSound (q : Nat) (shifts : List F) (p factor : CPolynomial F)
           · exact ih _ h
           · exact ih _ h
 
+/-- A represented linear factor has nonzero degree-one coefficient. -/
+theorem represented_coeff_one_ne_zero {q : CPolynomial F}
+    (hq : isRepresentedLinearFactor q = true) : CPolynomial.coeff q 1 ≠ 0 := by
+  intro h
+  rw [isRepresentedLinearFactor, h] at hq
+  simp at hq
+
+/-- A represented linear factor is neither `0` nor `1`. -/
+theorem represented_zero_one_eq_false {q : CPolynomial F}
+    (hq : isRepresentedLinearFactor q = true) : (q == 0 || q == 1) = false := by
+  have hc := represented_coeff_one_ne_zero hq
+  have h0 : q ≠ 0 := by intro h; exact hc (by rw [h]; exact CPolynomial.coeff_zero 1)
+  have h1 : q ≠ 1 := by intro h; apply hc; rw [h]; rfl
+  simp [h0, h1]
+
+/-- Base case of completeness: if the (normalized) input is already a represented
+linear factor with root `a`, the schedule emits it as a root factor candidate. -/
+theorem czSplit_emits (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
+    (q : Nat) (a : F) (shifts : List F) (p : CPolynomial F)
+    (hlin : isRepresentedLinearFactor (CPolynomial.monicNormalize p) = true)
+    (hroot : CPolynomial.eval a p = 0) :
+    ∃ factor, factor ∈ (czSplitWithShifts M D q shifts p).toList ∧
+      IsLinearRootFactorCandidate factor a := by
+  refine ⟨CPolynomial.monicNormalize p, ?_, ?_⟩
+  · cases shifts with
+    | nil => rw [czSplitWithShifts, if_pos hlin]; simp
+    | cons s rest =>
+        rw [czSplitWithShifts,
+          if_neg (by rw [represented_zero_one_eq_false hlin]; simp), if_pos hlin]
+        simp
+  · exact representedLinearFactor_candidate_of_root hlin (monicNormalize_root_of_root hroot)
+
 /-- Build a `LinearFactorProductSplitter` from the Cantor–Zassenhaus algorithm.
 
 `sound` is discharged by `czSound`. `complete` is left as a parameter: it is the

From 9b53c299e9090e138ff8d5a33ae07d47766442ac Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Tue, 9 Jun 2026 19:56:11 +0300
Subject: [PATCH 07/18] feat(univariate): CZ completeness over prime fields
 (czComplete)

czComplete_core: the recursion finds a root factor candidate for every root a
(q odd, schedule reaches -a). Root preserved into a residue bucket at each
non-isolating shift (QR routing), isolated at s=-a via the X+s bucket.
czComplete: top-level completeness given prime-field schedule coverage.
Adds eval_linearFactor_self and czSplitWithShifts_cons_else.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .../Univariate/Roots/CantorZassenhaus.lean    | 93 +++++++++++++++++++
 1 file changed, 93 insertions(+)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index e35b258e..ddcf13da 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -304,6 +304,99 @@ theorem czSplit_emits (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.Mo
         simp
   · exact representedLinearFactor_candidate_of_root hlin (monicNormalize_root_of_root hroot)
 
+/-- A linear factor vanishes at its own root. -/
+theorem eval_linearFactor_self (a : F) :
+    CPolynomial.eval a (CPolynomial.linearFactor a) = 0 := by
+  rw [CPolynomial.eval_toPoly, linearFactor_toPoly]; simp
+
+/-- Unfolding the non-leaf cons step into its three bucket recursions. -/
+theorem czSplitWithShifts_cons_else (M : CPolynomial.Raw.MulContext F)
+    (D : CPolynomial.Raw.ModContext F) (q : Nat) (s : F) (rest : List F) (p : CPolynomial F)
+    (h01 : (CPolynomial.monicNormalize p == 0 || CPolynomial.monicNormalize p == 1) = false)
+    (hlin : isRepresentedLinearFactor (CPolynomial.monicNormalize p) = false) :
+    czSplitWithShifts M D q (s :: rest) p =
+      czSplitWithShifts M D q rest (czRefine M D q s (CPolynomial.monicNormalize p)).1 ++
+        czSplitWithShifts M D q rest (czRefine M D q s (CPolynomial.monicNormalize p)).2.1 ++
+        czSplitWithShifts M D q rest (czRefine M D q s (CPolynomial.monicNormalize p)).2.2 := by
+  rw [czSplitWithShifts, if_neg (by rw [h01]; simp), if_neg (by rw [hlin]; simp)]
+
+/-- Completeness core: for `q` odd over a field where the schedule reaches `-a`,
+the Cantor–Zassenhaus recursion finds a root factor candidate for every root `a`.
+The recursion preserves the root into a residue bucket at each non-isolating
+shift, and isolates it at shift `s = -a` via the `X + s` quotient bucket. -/
+theorem czComplete_core (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
+    (q : Nat) (hodd : Odd q) (hfrob : ∀ x : F, x ^ q = x) (a : F) :
+    ∀ (shifts : List F) (p : CPolynomial F),
+      CPolynomial.eval a p = 0 → p ≠ 0 → (-a) ∈ shifts →
+      ∃ factor, factor ∈ (czSplitWithShifts M D q shifts p).toList ∧
+        IsLinearRootFactorCandidate factor a := by
+  intro shifts
+  induction shifts with
+  | nil => intro p _ _ hmem; simp at hmem
+  | cons s rest ih =>
+      intro p hroot hpne hmem
+      by_cases hlin : isRepresentedLinearFactor (CPolynomial.monicNormalize p) = true
+      · exact czSplit_emits M D q a (s :: rest) p hlin hroot
+      · have hlinf : isRepresentedLinearFactor (CPolynomial.monicNormalize p) = false := by
+          simpa using hlin
+        have hp' : CPolynomial.eval a (CPolynomial.monicNormalize p) = 0 :=
+          monicNormalize_root_of_root hroot
+        have hp'ne : CPolynomial.monicNormalize p ≠ 0 := monicNormalize_ne_zero_of_ne_zero hpne
+        have hne1 : CPolynomial.monicNormalize p ≠ 1 := by
+          intro h; rw [h, eval_one] at hp'; exact one_ne_zero hp'
+        have h01 : (CPolynomial.monicNormalize p == 0 || CPolynomial.monicNormalize p == 1)
+            = false := by simp [hp'ne, hne1]
+        rw [czSplitWithShifts_cons_else M D q s rest p h01 hlinf]
+        by_cases hsa : a + s = 0
+        · have hgz : (czRefine M D q s (CPolynomial.monicNormalize p)).1 =
+              CPolynomial.linearFactor a := by
+            rw [czRefine_fst]
+            have hxs : (CPolynomial.X + CPolynomial.C s) = CPolynomial.linearFactor a := by
+              rw [czShift_eq_linearFactor]; congr 1; linear_combination -hsa
+            rw [hxs, gcdMonic_linearFactor_of_root hp', monicNormalize_linearFactor]
+          obtain ⟨factor, hfmem, hfcand⟩ :=
+            czSplit_emits M D q a rest (CPolynomial.linearFactor a)
+              (by rw [monicNormalize_linearFactor]; exact linearFactor_isRepresentedLinearFactor a)
+              (eval_linearFactor_self a)
+          refine ⟨factor, ?_, hfcand⟩
+          rw [hgz]
+          simp only [Array.toList_append, List.mem_append]
+          exact Or.inl (Or.inl hfmem)
+        · have hmemrest : (-a) ∈ rest := by
+            rcases List.mem_cons.mp hmem with h | h
+            · exact absurd (by linear_combination -h : a + s = 0) hsa
+            · exact h
+          rcases czRefine_root_in_residue_bucket M D q hodd hfrob s a
+            (CPolynomial.monicNormalize p) hp' hsa with hr | hr
+          · obtain ⟨factor, hfmem, hfcand⟩ :=
+              ih (czRefine M D q s (CPolynomial.monicNormalize p)).2.1 hr
+                (by rw [czRefine_snd_fst]
+                    exact monicNormalize_ne_zero_of_ne_zero (gcdMonic_ne_zero_of_left hp'ne))
+                hmemrest
+            refine ⟨factor, ?_, hfcand⟩
+            simp only [Array.toList_append, List.mem_append]
+            exact Or.inl (Or.inr hfmem)
+          · obtain ⟨factor, hfmem, hfcand⟩ :=
+              ih (czRefine M D q s (CPolynomial.monicNormalize p)).2.2 hr
+                (by rw [czRefine_snd_snd]
+                    exact monicNormalize_ne_zero_of_ne_zero (gcdMonic_ne_zero_of_left hp'ne))
+                hmemrest
+            refine ⟨factor, ?_, hfcand⟩
+            simp only [Array.toList_append, List.mem_append]
+            exact Or.inr hfmem
+
+/-- Completeness of the Cantor–Zassenhaus splitter over a prime field of odd
+cardinality `q`: the hypothesis `hcover` (the shift schedule `0..q-1` reaches
+every field element) holds for `F = ZMod q`. -/
+theorem czComplete (q : Nat) (hodd : Odd q) (hfrob : ∀ x : F, x ^ q = x)
+    (hcover : ∀ x : F, x ∈ czDefaultShifts q)
+    (p : CPolynomial F) (a : F) (hpne : p ≠ 0) (hroot : CPolynomial.eval a p = 0) :
+    ∃ factor, factor ∈ (czSplitLinearFactors q p).toList ∧
+      IsLinearRootFactorCandidate factor a := by
+  rw [czSplitLinearFactors]
+  exact czComplete_core CPolynomial.Raw.MulContext.naive CPolynomial.Raw.ModContext.naive q
+    hodd hfrob a (czDefaultShifts q) p hroot hpne (hcover (-a))
+
 /-- Build a `LinearFactorProductSplitter` from the Cantor–Zassenhaus algorithm.
 
 `sound` is discharged by `czSound`. `complete` is left as a parameter: it is the

From 0b02ae8a411ededced15a840b47899df457450dc Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Tue, 9 Jun 2026 19:57:06 +0300
Subject: [PATCH 08/18] feat(univariate): package CZ splitter
 (czLinearFactorProductSplitter)

Concrete LinearFactorProductSplitter from Cantor-Zassenhaus, with validInput
recording odd q, Frobenius, and prime-field schedule coverage. Completeness
discharged by czComplete. The CZ splitter is now sound and complete over odd
prime fields, with no sorry/native_decide.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 CompPoly/Univariate/Roots/CantorZassenhaus.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index ddcf13da..73d12f78 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -422,6 +422,18 @@ def czLinearFactorProductSplitterOf
     exact czSound q (czDefaultShifts q) p factor h
   complete := complete
 
+/-- The Cantor–Zassenhaus splitter packaged as a `LinearFactorProductSplitter`.
+`validInput q p` records the facts the completeness proof needs: `q` odd, the
+Frobenius identity `x^q = x`, and that the shift schedule `0..q-1` reaches every
+element of `F` (all three hold for a prime field `F = ZMod q` of odd order). -/
+def czLinearFactorProductSplitter : LinearFactorProductSplitter F :=
+  czLinearFactorProductSplitterOf
+    (fun q _ => Odd q ∧ (∀ x : F, x ^ q = x) ∧ (∀ x : F, x ∈ czDefaultShifts q))
+    (by
+      intro q p a hvalid hpne hroot
+      obtain ⟨hodd, hfrob, hcover⟩ := hvalid
+      exact czComplete q hodd hfrob hcover p a hpne hroot)
+
 end FiniteField
 
 end Roots

From 8d0fc9dafb9c8d7dbcecb25dfbc0026c389a763f Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Tue, 9 Jun 2026 20:35:51 +0300
Subject: [PATCH 09/18] feat(univariate): CZ completeness over ZMod prime
 fields (czComplete_zmod)

Discharges czComplete's validInput for ZMod q (odd prime) via ZMod.pow_card and
schedule coverage (zmod_mem_czDefaultShifts). Covers KoalaBear/BabyBear.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .../Univariate/Roots/CantorZassenhaus.lean    | 21 +++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index 73d12f78..786bb3d2 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -6,6 +6,7 @@ Authors: Dimitrios Mitsios
 
 import CompPoly.Univariate.Roots.Splitter
 import CompPoly.Univariate.Roots.Correctness
+import Mathlib.FieldTheory.Finite.Basic
 
 /-!
 # Cantor–Zassenhaus Linear-Factor Splitting
@@ -422,6 +423,26 @@ def czLinearFactorProductSplitterOf
     exact czSound q (czDefaultShifts q) p factor h
   complete := complete
 
+/-- Over the prime field `ZMod q` the schedule `0..q-1` reaches every element,
+since every `x` equals `↑x.val` with `x.val < q`. -/
+theorem zmod_mem_czDefaultShifts (q : Nat) [Fact (Nat.Prime q)] (x : ZMod q) :
+    x ∈ czDefaultShifts q := by
+  haveI : NeZero q := ⟨(Fact.out : Nat.Prime q).pos.ne'⟩
+  rw [czDefaultShifts, List.mem_map]
+  exact ⟨x.val, List.mem_range.mpr (ZMod.val_lt x), ZMod.natCast_zmod_val x⟩
+
+/-- Completeness over a prime field `ZMod q` of odd order: every root of a nonzero
+polynomial is found by `czSplitLinearFactors`. Discharges the `validInput` facts
+of `czComplete` from `ZMod.pow_card` (Frobenius) and `zmod_mem_czDefaultShifts`
+(coverage). Applies to KoalaBear and BabyBear. -/
+theorem czComplete_zmod (q : Nat) [Fact (Nat.Prime q)] (hodd : Odd q)
+    (p : CPolynomial (ZMod q)) (a : ZMod q) (hpne : p ≠ 0)
+    (hroot : CPolynomial.eval a p = 0) :
+    ∃ factor, factor ∈ (czSplitLinearFactors q p).toList ∧
+      IsLinearRootFactorCandidate factor a :=
+  czComplete q hodd (fun x => ZMod.pow_card x) (fun x => zmod_mem_czDefaultShifts q x)
+    p a hpne hroot
+
 /-- The Cantor–Zassenhaus splitter packaged as a `LinearFactorProductSplitter`.
 `validInput q p` records the facts the completeness proof needs: `q` odd, the
 Frobenius identity `x^q = x`, and that the shift schedule `0..q-1` reaches every

From f5a0fc7143d33e03d959029e384407b26e6773ca Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Tue, 9 Jun 2026 20:38:16 +0300
Subject: [PATCH 10/18] test(univariate): Cantor-Zassenhaus splitter regression
 tests over ZMod 7

#guard checks that czSplitLinearFactors splits (X-2)(X-3) and X(X-1) into
linear factors (including root 0), all factors linear, plus a czComplete_zmod
instantiation.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 tests/CompPolyTests.lean                      |  1 +
 .../Univariate/Roots/CantorZassenhaus.lean    | 61 +++++++++++++++++++
 2 files changed, 62 insertions(+)
 create mode 100644 tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean

diff --git a/tests/CompPolyTests.lean b/tests/CompPolyTests.lean
index b8ee14f5..a401a744 100644
--- a/tests/CompPolyTests.lean
+++ b/tests/CompPolyTests.lean
@@ -37,6 +37,7 @@ import CompPolyTests.Univariate.NTT.FastMul
 import CompPolyTests.Univariate.NTT.Forward
 import CompPolyTests.Univariate.NTT.Inverse
 import CompPolyTests.Univariate.Raw
+import CompPolyTests.Univariate.Roots.CantorZassenhaus
 import CompPolyTests.Univariate.Roots.Enumeration
 import CompPolyTests.Univariate.Roots.FiniteField
 import CompPolyTests.Univariate.ToPoly
diff --git a/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean b/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean
new file mode 100644
index 00000000..76f006ae
--- /dev/null
+++ b/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean
@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dimitrios Mitsios
+-/
+import CompPoly.Univariate.Roots.CantorZassenhaus
+import Mathlib.Data.ZMod.Basic
+import Mathlib.Algebra.Field.ZMod
+
+/-!
+# Tests: Cantor–Zassenhaus linear-factor splitter
+
+Executable `#guard` checks over the small prime field `ZMod 7`, where the default
+shift schedule `0..6` is cheap. The splitter takes a squarefree product of linear
+factors and returns its individual linear factors.
+-/
+
+open CompPoly
+open CompPoly.CPolynomial.Roots.FiniteField
+
+namespace CompPolyTests
+namespace CantorZassenhausTest
+
+instance : Fact (Nat.Prime 7) := ⟨by decide⟩
+
+abbrev F : Type := ZMod 7
+
+/-! ### Splitting `(X - 2)(X - 3)` into its two linear factors. -/
+
+private def p₂₃ : CPolynomial F :=
+  (CPolynomial.X - CPolynomial.C 2) * (CPolynomial.X - CPolynomial.C 3)
+
+#guard (czSplitLinearFactors 7 p₂₃).size == 2
+#guard (czSplitLinearFactors 7 p₂₃).contains (CPolynomial.linearFactor (2 : F))
+#guard (czSplitLinearFactors 7 p₂₃).contains (CPolynomial.linearFactor (3 : F))
+
+/-! ### A factor with root `0` is also found (`X(X - 1) = X² - X`). -/
+
+private def p₀₁ : CPolynomial F := CPolynomial.X ^ 2 - CPolynomial.X
+
+#guard (czSplitLinearFactors 7 p₀₁).size == 2
+#guard (czSplitLinearFactors 7 p₀₁).contains (CPolynomial.linearFactor (0 : F))
+#guard (czSplitLinearFactors 7 p₀₁).contains (CPolynomial.linearFactor (1 : F))
+
+/-! ### Every emitted factor is linear (soundness, on a concrete input). -/
+
+#guard (czSplitLinearFactors 7 p₂₃).all (fun f => isRepresentedLinearFactor f)
+
+/-! ### Completeness is provable for any root (theorem-level check).
+
+The polynomial-level hypotheses are kept abstract: `decide` does not kernel-reduce
+`CPolynomial`/`ZMod` equalities, so `p ≠ 0` and `eval a p = 0` are taken as
+arguments. The point is that `czComplete_zmod` composes for `ZMod 7`. -/
+
+example (a : F) (hpne : p₂₃ ≠ 0) (h : CPolynomial.eval a p₂₃ = 0) :
+    ∃ factor, factor ∈ (czSplitLinearFactors 7 p₂₃).toList ∧
+      IsLinearRootFactorCandidate factor a :=
+  czComplete_zmod 7 (by decide) p₂₃ a hpne h
+
+end CantorZassenhausTest
+end CompPolyTests

From fcb16ce04dd66ab13be7a01f94fba8589d483836 Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Tue, 9 Jun 2026 20:40:37 +0300
Subject: [PATCH 11/18] docs(univariate): refine CZ docstrings (concise,
 completeness proved)

Update module doc to state soundness/completeness are proved over odd prime
fields and note the schedule-length efficiency caveat; trim over-explanation
and an em-dash connective.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .../Univariate/Roots/CantorZassenhaus.lean    | 34 ++++++++-----------
 1 file changed, 15 insertions(+), 19 deletions(-)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index 786bb3d2..3ee35089 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -28,11 +28,15 @@ For a shift `s : F`, with `w = (X + s)^((q-1)/2) mod p`:
 * `gcd(p, w - 1)` collects roots `r` with `r + s` a nonzero square;
 * `gcd(p, w + 1)` collects roots `r` with `r + s` a non-square.
 
-Iterating over a sequence of shifts separates all roots: for any two distinct
-roots, some shift sends them to different quadratic-residue classes. The split
-is correct for *every* shift; the shift sequence only governs termination, so no
-probabilistic reasoning enters correctness. See `czSound` (proved here) and the
-`complete` obligation, supplied to `czLinearFactorProductSplitterOf`.
+The split is correct for every shift, so no probabilistic reasoning enters
+correctness; the schedule only governs termination. Over a prime field the
+default schedule `0..q-1` reaches every element, and the root `a` is isolated at
+shift `s = -a` by the `gcd(p, X + s)` bucket. Soundness (`czSound`) and
+completeness over odd prime fields (`czComplete`, `czComplete_zmod`) are proved.
+
+The default schedule has length `q`, suitable for small fields. Efficient use on
+large fields needs a short schedule, whose completeness relies on quadratic-residue
+separation of distinct roots.
 
 ## References
 
@@ -71,11 +75,8 @@ def czRefine (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext
   let gNon := CPolynomial.monicNormalize (CPolynomial.gcdMonic p (w + 1))
   (gZero, gRes, gNon)
 
-/-- The shift bucket `X + s` is exactly the monic linear factor with root `-s`.
-First step of the completeness argument: at shift `s = -a` the `gcd(p, X + s)`
-bucket isolates the root `a` directly, with no quadratic-residue reasoning. The
-residue buckets `w ± 1` are needed only for fields whose elements are not all
-reached by the prime-subfield shift schedule (extension fields). -/
+/-- The shift bucket `X + s` is the monic linear factor with root `-s`. At shift
+`s = -a` this isolates the root `a` directly, without quadratic-residue reasoning. -/
 theorem czShift_eq_linearFactor (s : F) :
     (CPolynomial.X + CPolynomial.C s : CPolynomial F) = CPolynomial.linearFactor (-s) := by
   rw [CPolynomial.linearFactor, neg_neg, add_comm]
@@ -87,8 +88,7 @@ theorem eval_X_add_C (a s : F) :
     CPolynomial.C_toPoly, Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C]
 
 /-- At a root `a` of `p`, the shifted discriminating power evaluates as
-`(a + s)^k`. This is the analytic core of the quadratic-residue routing:
-`w(a) = (a + s)^((q-1)/2)`. Wraps `raw_eval_powModWith_eq_pow`. -/
+`(a + s)^k`. With `k = (q-1)/2` this is the value routed on by the residue buckets. -/
 theorem eval_shiftedPowModWith (M : CPolynomial.Raw.MulContext F)
     (D : CPolynomial.Raw.ModContext F) (p : CPolynomial F) (s a : F) (k : Nat)
     (hp : CPolynomial.eval a p = 0) :
@@ -398,13 +398,9 @@ theorem czComplete (q : Nat) (hodd : Odd q) (hfrob : ∀ x : F, x ^ q = x)
   exact czComplete_core CPolynomial.Raw.MulContext.naive CPolynomial.Raw.ModContext.naive q
     hodd hfrob a (czDefaultShifts q) p hroot hpne (hcover (-a))
 
-/-- Build a `LinearFactorProductSplitter` from the Cantor–Zassenhaus algorithm.
-
-`sound` is discharged by `czSound`. `complete` is left as a parameter: it is the
-statement that, under `validInput`, the supplied shift schedule (here the default
-of length `q`) separates every root into its own linear factor. The proof rests
-on the quadratic-residue separation lemma (for distinct roots some shift splits
-them) and termination of the schedule — no probabilistic argument. -/
+/-- Build a `LinearFactorProductSplitter` from the algorithm, taking `validInput`
+and `complete` as parameters. `sound` is discharged by `czSound`. The packaged
+`czLinearFactorProductSplitter` supplies `complete` from `czComplete`. -/
 def czLinearFactorProductSplitterOf
     (validInput : Nat → CPolynomial F → Prop)
     (complete :

From 25be967d4b0a8e49d4c6b67eb71a81f0e3cbe16f Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Wed, 10 Jun 2026 15:32:06 +0300
Subject: [PATCH 12/18] refactor(univariate): flatten CZ completeness
 statements via HasRootFactor

Introduce HasRootFactor abbreviation for the repeated
'exists a linear root factor candidate' conclusion, removing the deeply nested
existential from czComplete/_core/_zmod, czSplit_emits, and the splitter builder
parameter. Add HasRootFactor.append_left/right to collapse the three membership
lifts in czComplete_core to one line each.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .../Univariate/Roots/CantorZassenhaus.lean    | 75 +++++++++----------
 1 file changed, 37 insertions(+), 38 deletions(-)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index 3ee35089..96ed57cb 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -54,6 +54,24 @@ namespace FiniteField
 
 variable {F : Type*} [Field F] [BEq F] [LawfulBEq F]
 
+/-- The splitter output contains a linear root factor candidate for `a`. -/
+abbrev HasRootFactor (out : Array (CPolynomial F)) (a : F) : Prop :=
+  ∃ factor, factor ∈ out.toList ∧ IsLinearRootFactorCandidate factor a
+
+omit [BEq F] [LawfulBEq F] in
+/-- A candidate in the left part survives appending on the right. -/
+theorem HasRootFactor.append_left {A B : Array (CPolynomial F)} {a : F}
+    (h : HasRootFactor A a) : HasRootFactor (A ++ B) a := by
+  obtain ⟨f, hf, hc⟩ := h
+  exact ⟨f, by simp only [Array.toList_append, List.mem_append]; exact Or.inl hf, hc⟩
+
+omit [BEq F] [LawfulBEq F] in
+/-- A candidate in the right part survives appending on the left. -/
+theorem HasRootFactor.append_right {A B : Array (CPolynomial F)} {a : F}
+    (h : HasRootFactor B a) : HasRootFactor (A ++ B) a := by
+  obtain ⟨f, hf, hc⟩ := h
+  exact ⟨f, by simp only [Array.toList_append, List.mem_append]; exact Or.inr hf, hc⟩
+
 /-- `(X + s)^exponent mod modulus`, lifted back to canonical polynomials.
 The Cantor–Zassenhaus discriminating power, generalising `xPowModWith` to the
 shifted base `X + s`. -/
@@ -294,8 +312,7 @@ theorem czSplit_emits (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.Mo
     (q : Nat) (a : F) (shifts : List F) (p : CPolynomial F)
     (hlin : isRepresentedLinearFactor (CPolynomial.monicNormalize p) = true)
     (hroot : CPolynomial.eval a p = 0) :
-    ∃ factor, factor ∈ (czSplitWithShifts M D q shifts p).toList ∧
-      IsLinearRootFactorCandidate factor a := by
+    HasRootFactor (czSplitWithShifts M D q shifts p) a := by
   refine ⟨CPolynomial.monicNormalize p, ?_, ?_⟩
   · cases shifts with
     | nil => rw [czSplitWithShifts, if_pos hlin]; simp
@@ -329,8 +346,7 @@ theorem czComplete_core (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.
     (q : Nat) (hodd : Odd q) (hfrob : ∀ x : F, x ^ q = x) (a : F) :
     ∀ (shifts : List F) (p : CPolynomial F),
       CPolynomial.eval a p = 0 → p ≠ 0 → (-a) ∈ shifts →
-      ∃ factor, factor ∈ (czSplitWithShifts M D q shifts p).toList ∧
-        IsLinearRootFactorCandidate factor a := by
+      HasRootFactor (czSplitWithShifts M D q shifts p) a := by
   intro shifts
   induction shifts with
   | nil => intro p _ _ hmem; simp at hmem
@@ -355,36 +371,26 @@ theorem czComplete_core (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.
             have hxs : (CPolynomial.X + CPolynomial.C s) = CPolynomial.linearFactor a := by
               rw [czShift_eq_linearFactor]; congr 1; linear_combination -hsa
             rw [hxs, gcdMonic_linearFactor_of_root hp', monicNormalize_linearFactor]
-          obtain ⟨factor, hfmem, hfcand⟩ :=
-            czSplit_emits M D q a rest (CPolynomial.linearFactor a)
-              (by rw [monicNormalize_linearFactor]; exact linearFactor_isRepresentedLinearFactor a)
-              (eval_linearFactor_self a)
-          refine ⟨factor, ?_, hfcand⟩
           rw [hgz]
-          simp only [Array.toList_append, List.mem_append]
-          exact Or.inl (Or.inl hfmem)
+          exact HasRootFactor.append_left (HasRootFactor.append_left
+            (czSplit_emits M D q a rest (CPolynomial.linearFactor a)
+              (by rw [monicNormalize_linearFactor]; exact linearFactor_isRepresentedLinearFactor a)
+              (eval_linearFactor_self a)))
         · have hmemrest : (-a) ∈ rest := by
             rcases List.mem_cons.mp hmem with h | h
             · exact absurd (by linear_combination -h : a + s = 0) hsa
             · exact h
+          have hbucket : ∀ b : CPolynomial F, CPolynomial.monicNormalize
+              (CPolynomial.gcdMonic (CPolynomial.monicNormalize p) b) ≠ 0 := fun b =>
+            monicNormalize_ne_zero_of_ne_zero (gcdMonic_ne_zero_of_left hp'ne)
           rcases czRefine_root_in_residue_bucket M D q hodd hfrob s a
             (CPolynomial.monicNormalize p) hp' hsa with hr | hr
-          · obtain ⟨factor, hfmem, hfcand⟩ :=
-              ih (czRefine M D q s (CPolynomial.monicNormalize p)).2.1 hr
-                (by rw [czRefine_snd_fst]
-                    exact monicNormalize_ne_zero_of_ne_zero (gcdMonic_ne_zero_of_left hp'ne))
-                hmemrest
-            refine ⟨factor, ?_, hfcand⟩
-            simp only [Array.toList_append, List.mem_append]
-            exact Or.inl (Or.inr hfmem)
-          · obtain ⟨factor, hfmem, hfcand⟩ :=
-              ih (czRefine M D q s (CPolynomial.monicNormalize p)).2.2 hr
-                (by rw [czRefine_snd_snd]
-                    exact monicNormalize_ne_zero_of_ne_zero (gcdMonic_ne_zero_of_left hp'ne))
-                hmemrest
-            refine ⟨factor, ?_, hfcand⟩
-            simp only [Array.toList_append, List.mem_append]
-            exact Or.inr hfmem
+          · exact HasRootFactor.append_left (HasRootFactor.append_right
+              (ih (czRefine M D q s (CPolynomial.monicNormalize p)).2.1 hr
+                (by rw [czRefine_snd_fst]; exact hbucket _) hmemrest))
+          · exact HasRootFactor.append_right
+              (ih (czRefine M D q s (CPolynomial.monicNormalize p)).2.2 hr
+                (by rw [czRefine_snd_snd]; exact hbucket _) hmemrest)
 
 /-- Completeness of the Cantor–Zassenhaus splitter over a prime field of odd
 cardinality `q`: the hypothesis `hcover` (the shift schedule `0..q-1` reaches
@@ -392,8 +398,7 @@ every field element) holds for `F = ZMod q`. -/
 theorem czComplete (q : Nat) (hodd : Odd q) (hfrob : ∀ x : F, x ^ q = x)
     (hcover : ∀ x : F, x ∈ czDefaultShifts q)
     (p : CPolynomial F) (a : F) (hpne : p ≠ 0) (hroot : CPolynomial.eval a p = 0) :
-    ∃ factor, factor ∈ (czSplitLinearFactors q p).toList ∧
-      IsLinearRootFactorCandidate factor a := by
+    HasRootFactor (czSplitLinearFactors q p) a := by
   rw [czSplitLinearFactors]
   exact czComplete_core CPolynomial.Raw.MulContext.naive CPolynomial.Raw.ModContext.naive q
     hodd hfrob a (czDefaultShifts q) p hroot hpne (hcover (-a))
@@ -404,13 +409,8 @@ and `complete` as parameters. `sound` is discharged by `czSound`. The packaged
 def czLinearFactorProductSplitterOf
     (validInput : Nat → CPolynomial F → Prop)
     (complete :
-      ∀ q p a,
-        validInput q p →
-          p ≠ 0 →
-            CPolynomial.eval a p = 0 →
-              ∃ factor,
-                factor ∈ (czSplitLinearFactors q p).toList ∧
-                  IsLinearRootFactorCandidate factor a) :
+      ∀ q p a, validInput q p → p ≠ 0 → CPolynomial.eval a p = 0 →
+        HasRootFactor (czSplitLinearFactors q p) a) :
     LinearFactorProductSplitter F where
   splitLinearFactors := czSplitLinearFactors
   validInput := validInput
@@ -434,8 +434,7 @@ of `czComplete` from `ZMod.pow_card` (Frobenius) and `zmod_mem_czDefaultShifts`
 theorem czComplete_zmod (q : Nat) [Fact (Nat.Prime q)] (hodd : Odd q)
     (p : CPolynomial (ZMod q)) (a : ZMod q) (hpne : p ≠ 0)
     (hroot : CPolynomial.eval a p = 0) :
-    ∃ factor, factor ∈ (czSplitLinearFactors q p).toList ∧
-      IsLinearRootFactorCandidate factor a :=
+    HasRootFactor (czSplitLinearFactors q p) a :=
   czComplete q hodd (fun x => ZMod.pow_card x) (fun x => zmod_mem_czDefaultShifts q x)
     p a hpne hroot
 

From 6768320fe85b34e3665d77eebd01a70f9e4a04a8 Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Wed, 10 Jun 2026 18:48:19 +0300
Subject: [PATCH 13/18] chore(univariate): author name Dimitris in CZ files

---
 CompPoly/Univariate/Roots/CantorZassenhaus.lean            | 2 +-
 tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index 96ed57cb..45815843 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 CompPoly Contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Dimitrios Mitsios
+Authors: Dimitris Mitsios
 -/
 
 import CompPoly.Univariate.Roots.Splitter
diff --git a/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean b/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean
index 76f006ae..5ac41987 100644
--- a/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean
+++ b/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 CompPoly. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Dimitrios Mitsios
+Authors: Dimitris Mitsios
 -/
 import CompPoly.Univariate.Roots.CantorZassenhaus
 import Mathlib.Data.ZMod.Basic

From 2f1f85e6434eda53439ed90eafef6da8d296b852 Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Wed, 10 Jun 2026 19:11:35 +0300
Subject: [PATCH 14/18] feat(univariate): end-to-end CZ root finder czRoots
 over ZMod q

Wire the Cantor-Zassenhaus splitter into the framework root pipeline
(rootsInFiniteField): czFiniteFieldContext for ZMod q plus czRoots, with
czRoots_sound/czRoots_complete derived from the orchestrator's correctness and
the splitter's validInput facts. Finds the distinct field roots of an arbitrary
univariate f (stage 1 gcd(f, X^q - X) + CZ split). Tests over ZMod 7 incl.
multiplicity collapse and a rootless irreducible.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .../Univariate/Roots/CantorZassenhaus.lean    | 27 +++++++++++++++++++
 .../Univariate/Roots/CantorZassenhaus.lean    | 22 +++++++++++++++
 2 files changed, 49 insertions(+)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index 45815843..92f512df 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -450,6 +450,33 @@ def czLinearFactorProductSplitter : LinearFactorProductSplitter F :=
       obtain ⟨hodd, hfrob, hcover⟩ := hvalid
       exact czComplete q hodd hfrob hcover p a hpne hroot)
 
+/-- Finite-field context for the prime field `ZMod q` of odd order. -/
+def czFiniteFieldContext (q : Nat) [Fact (Nat.Prime q)] : FiniteFieldContext (ZMod q) :=
+  haveI : NeZero q := ⟨(Fact.out : Nat.Prime q).pos.ne'⟩
+  { q := q
+    finite := inferInstance
+    card_eq := by rw [Nat.card_eq_fintype_card, ZMod.card]
+    frobenius_fixed := fun a => ZMod.pow_card a }
+
+/-- End-to-end root finder over `ZMod q`: stage 1 extracts the distinct field
+roots as `gcd(f, X^q - X)`, then the Cantor–Zassenhaus splitter separates them.
+Returns the set of roots in `ZMod q` of an arbitrary univariate `f`. -/
+def czRoots (q : Nat) [Fact (Nat.Prime q)] (f : CPolynomial (ZMod q)) : Array (ZMod q) :=
+  rootsInFiniteField (czFiniteFieldContext q) czLinearFactorProductSplitter f
+
+/-- Soundness: every element of `czRoots` is a root of `f`. -/
+theorem czRoots_sound (q : Nat) [Fact (Nat.Prime q)] {f : CPolynomial (ZMod q)} {a : ZMod q}
+    (h : a ∈ (czRoots q f).toList) : CPolynomial.eval a f = 0 :=
+  rootsInFiniteField_sound (czFiniteFieldContext q) czLinearFactorProductSplitter h
+
+/-- Completeness: for odd `q`, every root of a nonzero `f` is found by `czRoots`. -/
+theorem czRoots_complete (q : Nat) [Fact (Nat.Prime q)] (hodd : Odd q)
+    {f : CPolynomial (ZMod q)} {a : ZMod q} (hf : f ≠ 0) (hroot : CPolynomial.eval a f = 0) :
+    a ∈ (czRoots q f).toList :=
+  rootsInFiniteField_complete (czFiniteFieldContext q) czLinearFactorProductSplitter
+    (by intro p _; exact ⟨hodd, fun x => ZMod.pow_card x, fun x => zmod_mem_czDefaultShifts q x⟩)
+    hf hroot
+
 end FiniteField
 
 end Roots
diff --git a/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean b/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean
index 5ac41987..4f6dcace 100644
--- a/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean
+++ b/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean
@@ -57,5 +57,27 @@ example (a : F) (hpne : p₂₃ ≠ 0) (h : CPolynomial.eval a p₂₃ = 0) :
       IsLinearRootFactorCandidate factor a :=
   czComplete_zmod 7 (by decide) p₂₃ a hpne h
 
+/-! ### End-to-end root finding on a general `f` (`czRoots`).
+
+`czRoots` runs stage 1 (`gcd(f, X^7 - X)`) then the CZ splitter, returning the
+distinct field roots of an arbitrary `f`. Multiplicities collapse and factors with
+no `ZMod 7` root are filtered. -/
+
+-- `(X - 2)² (X - 3)`: roots `{2, 3}`, the double root counted once.
+private def fMult : CPolynomial F :=
+  (CPolynomial.X - CPolynomial.C 2) ^ 2 * (CPolynomial.X - CPolynomial.C 3)
+
+#guard (czRoots 7 fMult).size == 2
+#guard (czRoots 7 fMult).contains 2
+#guard (czRoots 7 fMult).contains 3
+
+-- `X² + 1` is irreducible over `ZMod 7` (`-1` is a non-residue), so no roots.
+#guard (czRoots 7 (CPolynomial.X ^ 2 + 1)).size == 0
+
+-- Completeness of the end-to-end finder.
+example (a : F) (hf : fMult ≠ 0) (h : CPolynomial.eval a fMult = 0) :
+    a ∈ (czRoots 7 fMult).toList :=
+  czRoots_complete 7 (by decide) hf h
+
 end CantorZassenhausTest
 end CompPolyTests

From 48d466bc16d87f33d12b7cd5cdd793752d00dd17 Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Thu, 11 Jun 2026 14:57:45 +0300
Subject: [PATCH 15/18] docs(univariate): tighten CZ docstrings to
 state-what-not-how

Trim proof sketches and usage motivation from 11 declaration docstrings
(shiftedPowModWith, czShift_eq_linearFactor, eval_shiftedPowModWith, eval_add,
czRefine_root_in_residue_bucket, gcdMonic_linearFactor_of_root, czSplitWithShifts,
czComplete_core, zmod_mem_czDefaultShifts, czComplete_zmod); drop inaccurate
'odd order' from czFiniteFieldContext.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .../Univariate/Roots/CantorZassenhaus.lean    | 49 +++++++------------
 1 file changed, 17 insertions(+), 32 deletions(-)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index 92f512df..5b217841 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -72,9 +72,7 @@ theorem HasRootFactor.append_right {A B : Array (CPolynomial F)} {a : F}
   obtain ⟨f, hf, hc⟩ := h
   exact ⟨f, by simp only [Array.toList_append, List.mem_append]; exact Or.inr hf, hc⟩
 
-/-- `(X + s)^exponent mod modulus`, lifted back to canonical polynomials.
-The Cantor–Zassenhaus discriminating power, generalising `xPowModWith` to the
-shifted base `X + s`. -/
+/-- `(X + s)^exponent mod modulus`, the shifted discriminating power of the method. -/
 def shiftedPowModWith (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
     (modulus : CPolynomial F) (s : F) (exponent : Nat) : CPolynomial F :=
   CPolynomial.ofArray
@@ -93,8 +91,7 @@ def czRefine (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext
   let gNon := CPolynomial.monicNormalize (CPolynomial.gcdMonic p (w + 1))
   (gZero, gRes, gNon)
 
-/-- The shift bucket `X + s` is the monic linear factor with root `-s`. At shift
-`s = -a` this isolates the root `a` directly, without quadratic-residue reasoning. -/
+/-- The shift base `X + s` equals the monic linear factor with root `-s`. -/
 theorem czShift_eq_linearFactor (s : F) :
     (CPolynomial.X + CPolynomial.C s : CPolynomial F) = CPolynomial.linearFactor (-s) := by
   rw [CPolynomial.linearFactor, neg_neg, add_comm]
@@ -105,8 +102,7 @@ theorem eval_X_add_C (a s : F) :
   rw [CPolynomial.eval_toPoly, CPolynomial.toPoly_add, CPolynomial.X_toPoly,
     CPolynomial.C_toPoly, Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C]
 
-/-- At a root `a` of `p`, the shifted discriminating power evaluates as
-`(a + s)^k`. With `k = (q-1)/2` this is the value routed on by the residue buckets. -/
+/-- At a root `a` of `p`, the shifted discriminating power evaluates to `(a + s)^k`. -/
 theorem eval_shiftedPowModWith (M : CPolynomial.Raw.MulContext F)
     (D : CPolynomial.Raw.ModContext F) (p : CPolynomial F) (s a : F) (k : Nat)
     (hp : CPolynomial.eval a p = 0) :
@@ -120,7 +116,7 @@ theorem eval_shiftedPowModWith (M : CPolynomial.Raw.MulContext F)
   change CPolynomial.eval a (CPolynomial.X + CPolynomial.C s) ^ k = (a + s) ^ k
   rw [eval_X_add_C]
 
-/-- Evaluation is additive (the library provides `eval_sub` but not `eval_add`). -/
+/-- Evaluation is additive. -/
 theorem eval_add (a : F) (p₁ p₂ : CPolynomial F) :
     CPolynomial.eval a (p₁ + p₂) = CPolynomial.eval a p₁ + CPolynomial.eval a p₂ := by
   rw [CPolynomial.eval_toPoly, CPolynomial.toPoly_add, Polynomial.eval_add,
@@ -149,9 +145,8 @@ theorem czRefine_snd_snd (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw
         (CPolynomial.gcdMonic p (shiftedPowModWith M D p s ((q - 1) / 2) + 1)) :=
   rfl
 
-/-- Quadratic-residue routing: for `q` odd and `a + s ≠ 0`, a root `a` of `p` is a
-root of one of the two residue buckets `gRes`/`gNon`. Uses Fermat (`a^q = a`) so
-that `((a+s)^((q-1)/2))² = 1`, hence the discriminating power is `±1` at `a`. -/
+/-- Quadratic-residue routing: for odd `q` and `a + s ≠ 0`, a root `a` of `p` is a
+root of one of the two residue buckets `gRes`/`gNon`. -/
 theorem czRefine_root_in_residue_bucket
     (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
     (q : Nat) (hodd : Odd q) (hfrob : ∀ x : F, x ^ q = x)
@@ -191,9 +186,8 @@ theorem linearFactor_toPoly (a : F) :
     CPolynomial.X_toPoly, Polynomial.C_neg]
   ring
 
-/-- Isolation: at a root `a` of `p`, the monic gcd of `p` with the linear factor
-`X - a` is exactly that linear factor. This makes the `s = -a` quotient bucket of
-`czRefine` equal to `linearFactor a`, isolating the root. -/
+/-- At a root `a` of `p`, the monic gcd of `p` with `linearFactor a` equals
+`linearFactor a`. -/
 theorem gcdMonic_linearFactor_of_root {p : CPolynomial F} {a : F}
     (hroot : CPolynomial.eval a p = 0) :
     CPolynomial.gcdMonic p (CPolynomial.linearFactor a) = CPolynomial.linearFactor a := by
@@ -227,14 +221,10 @@ theorem monicNormalize_linearFactor (a : F) :
   intro i
   rw [CPolynomial.coeff_toPoly, CPolynomial.coeff_toPoly, htoPoly]
 
-/-- Cantor–Zassenhaus separation driven by an explicit shift schedule
-(structural recursion on the schedule).
-
-Emits a factor only when it is recognised as a represented linear factor, so the
-output is linear by construction (`czSound`). When the schedule is exhausted on a
-still-composite factor, that factor is dropped (defensive): completeness is
-therefore conditional on the schedule separating all roots, which is the content
-of the `complete` obligation. -/
+/-- Cantor–Zassenhaus separation along a shift schedule. A factor is emitted once
+it is a represented linear factor; a still-composite factor with the schedule
+exhausted is dropped, so completeness is conditional on the schedule separating
+all roots. -/
 def czSplitWithShifts (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
     (q : Nat) : List F → CPolynomial F → Array (CPolynomial F)
   | [], p =>
@@ -338,10 +328,8 @@ theorem czSplitWithShifts_cons_else (M : CPolynomial.Raw.MulContext F)
         czSplitWithShifts M D q rest (czRefine M D q s (CPolynomial.monicNormalize p)).2.2 := by
   rw [czSplitWithShifts, if_neg (by rw [h01]; simp), if_neg (by rw [hlin]; simp)]
 
-/-- Completeness core: for `q` odd over a field where the schedule reaches `-a`,
-the Cantor–Zassenhaus recursion finds a root factor candidate for every root `a`.
-The recursion preserves the root into a residue bucket at each non-isolating
-shift, and isolates it at shift `s = -a` via the `X + s` quotient bucket. -/
+/-- Completeness core: for odd `q` over a field whose schedule reaches `-a`, the
+recursion finds a root factor candidate for every root `a`. -/
 theorem czComplete_core (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
     (q : Nat) (hodd : Odd q) (hfrob : ∀ x : F, x ^ q = x) (a : F) :
     ∀ (shifts : List F) (p : CPolynomial F),
@@ -419,8 +407,7 @@ def czLinearFactorProductSplitterOf
     exact czSound q (czDefaultShifts q) p factor h
   complete := complete
 
-/-- Over the prime field `ZMod q` the schedule `0..q-1` reaches every element,
-since every `x` equals `↑x.val` with `x.val < q`. -/
+/-- Over the prime field `ZMod q` the schedule `0..q-1` reaches every element. -/
 theorem zmod_mem_czDefaultShifts (q : Nat) [Fact (Nat.Prime q)] (x : ZMod q) :
     x ∈ czDefaultShifts q := by
   haveI : NeZero q := ⟨(Fact.out : Nat.Prime q).pos.ne'⟩
@@ -428,9 +415,7 @@ theorem zmod_mem_czDefaultShifts (q : Nat) [Fact (Nat.Prime q)] (x : ZMod q) :
   exact ⟨x.val, List.mem_range.mpr (ZMod.val_lt x), ZMod.natCast_zmod_val x⟩
 
 /-- Completeness over a prime field `ZMod q` of odd order: every root of a nonzero
-polynomial is found by `czSplitLinearFactors`. Discharges the `validInput` facts
-of `czComplete` from `ZMod.pow_card` (Frobenius) and `zmod_mem_czDefaultShifts`
-(coverage). Applies to KoalaBear and BabyBear. -/
+`f` is found by `czSplitLinearFactors`. Applies to KoalaBear and BabyBear. -/
 theorem czComplete_zmod (q : Nat) [Fact (Nat.Prime q)] (hodd : Odd q)
     (p : CPolynomial (ZMod q)) (a : ZMod q) (hpne : p ≠ 0)
     (hroot : CPolynomial.eval a p = 0) :
@@ -450,7 +435,7 @@ def czLinearFactorProductSplitter : LinearFactorProductSplitter F :=
       obtain ⟨hodd, hfrob, hcover⟩ := hvalid
       exact czComplete q hodd hfrob hcover p a hpne hroot)
 
-/-- Finite-field context for the prime field `ZMod q` of odd order. -/
+/-- Finite-field context for the prime field `ZMod q`. -/
 def czFiniteFieldContext (q : Nat) [Fact (Nat.Prime q)] : FiniteFieldContext (ZMod q) :=
   haveI : NeZero q := ⟨(Fact.out : Nat.Prime q).pos.ne'⟩
   { q := q

From f76678442fda3db7184df6b7890844cb14d9054b Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Thu, 11 Jun 2026 15:04:00 +0300
Subject: [PATCH 16/18] docs(test): tighten CZ test section comments

Trim the 'why abstract hypotheses' and 'stage 1 then splitter' how-detail from
two section headers.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .../Univariate/Roots/CantorZassenhaus.lean           | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean b/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean
index 4f6dcace..24fae567 100644
--- a/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean
+++ b/tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean
@@ -46,11 +46,10 @@ private def p₀₁ : CPolynomial F := CPolynomial.X ^ 2 - CPolynomial.X
 
 #guard (czSplitLinearFactors 7 p₂₃).all (fun f => isRepresentedLinearFactor f)
 
-/-! ### Completeness is provable for any root (theorem-level check).
+/-! ### Completeness is provable for any root.
 
-The polynomial-level hypotheses are kept abstract: `decide` does not kernel-reduce
-`CPolynomial`/`ZMod` equalities, so `p ≠ 0` and `eval a p = 0` are taken as
-arguments. The point is that `czComplete_zmod` composes for `ZMod 7`. -/
+`decide` does not kernel-reduce `CPolynomial`/`ZMod` equalities, so `p ≠ 0` and
+`eval a p = 0` are passed as hypotheses. -/
 
 example (a : F) (hpne : p₂₃ ≠ 0) (h : CPolynomial.eval a p₂₃ = 0) :
     ∃ factor, factor ∈ (czSplitLinearFactors 7 p₂₃).toList ∧
@@ -59,9 +58,8 @@ example (a : F) (hpne : p₂₃ ≠ 0) (h : CPolynomial.eval a p₂₃ = 0) :
 
 /-! ### End-to-end root finding on a general `f` (`czRoots`).
 
-`czRoots` runs stage 1 (`gcd(f, X^7 - X)`) then the CZ splitter, returning the
-distinct field roots of an arbitrary `f`. Multiplicities collapse and factors with
-no `ZMod 7` root are filtered. -/
+Returns the distinct `ZMod 7` roots of an arbitrary `f`: multiplicities collapse
+and factors with no `ZMod 7` root are dropped. -/
 
 -- `(X - 2)² (X - 3)`: roots `{2, 3}`, the double root counted once.
 private def fMult : CPolynomial F :=

From 657149192566c9e9e89202e3d621fc4aabcaa7d3 Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Thu, 11 Jun 2026 15:18:22 +0300
Subject: [PATCH 17/18] docs(univariate): clarify short-schedule completeness
 is future work

Reword the module-doc efficiency note so the fast large-field (short/random
schedule) variant and its QR-separation completeness are clearly marked as
unimplemented future work, not an existing guarantee.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 CompPoly/Univariate/Roots/CantorZassenhaus.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index 5b217841..f9963f48 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -34,9 +34,10 @@ default schedule `0..q-1` reaches every element, and the root `a` is isolated at
 shift `s = -a` by the `gcd(p, X + s)` bucket. Soundness (`czSound`) and
 completeness over odd prime fields (`czComplete`, `czComplete_zmod`) are proved.
 
-The default schedule has length `q`, suitable for small fields. Efficient use on
-large fields needs a short schedule, whose completeness relies on quadratic-residue
-separation of distinct roots.
+The default schedule has length `q`, so it is practical only on small fields. A
+fast large-field variant would use a short (e.g. random) schedule; proving its
+completeness needs the quadratic-residue separation argument and is left as future
+work.
 
 ## References
 

From 667dc3750a9013449aefac7ad132c76eedbfc6c8 Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Fri, 12 Jun 2026 13:31:56 +0300
Subject: [PATCH 18/18] =?UTF-8?q?style(univariate):=20use=20maps-to=20arro?=
 =?UTF-8?q?w=20(fun=20x=20=E2=86=A6)=20in=20CZ=20lambdas?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Per the style guide and matching the neighboring SmoothSubgroup code.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 CompPoly/Univariate/Roots/CantorZassenhaus.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/CompPoly/Univariate/Roots/CantorZassenhaus.lean b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
index f9963f48..04d84c7d 100644
--- a/CompPoly/Univariate/Roots/CantorZassenhaus.lean
+++ b/CompPoly/Univariate/Roots/CantorZassenhaus.lean
@@ -245,7 +245,7 @@ def czSplitWithShifts (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.Mo
 
 /-- Default shift schedule: `0, 1, …, (count - 1)` cast into `F`. -/
 def czDefaultShifts (count : Nat) : List F :=
-  (List.range count).map (fun i => (Nat.cast i : F))
+  (List.range count).map (fun i ↦ (Nat.cast i : F))
 
 /-- Cantor–Zassenhaus linear-factor splitting with naive polynomial arithmetic
 contexts and the default shift schedule of length `q`. -/
@@ -370,7 +370,7 @@ theorem czComplete_core (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.
             · exact absurd (by linear_combination -h : a + s = 0) hsa
             · exact h
           have hbucket : ∀ b : CPolynomial F, CPolynomial.monicNormalize
-              (CPolynomial.gcdMonic (CPolynomial.monicNormalize p) b) ≠ 0 := fun b =>
+              (CPolynomial.gcdMonic (CPolynomial.monicNormalize p) b) ≠ 0 := fun b ↦
             monicNormalize_ne_zero_of_ne_zero (gcdMonic_ne_zero_of_left hp'ne)
           rcases czRefine_root_in_residue_bucket M D q hodd hfrob s a
             (CPolynomial.monicNormalize p) hp' hsa with hr | hr
@@ -421,7 +421,7 @@ theorem czComplete_zmod (q : Nat) [Fact (Nat.Prime q)] (hodd : Odd q)
     (p : CPolynomial (ZMod q)) (a : ZMod q) (hpne : p ≠ 0)
     (hroot : CPolynomial.eval a p = 0) :
     HasRootFactor (czSplitLinearFactors q p) a :=
-  czComplete q hodd (fun x => ZMod.pow_card x) (fun x => zmod_mem_czDefaultShifts q x)
+  czComplete q hodd (fun x ↦ ZMod.pow_card x) (fun x ↦ zmod_mem_czDefaultShifts q x)
     p a hpne hroot
 
 /-- The Cantor–Zassenhaus splitter packaged as a `LinearFactorProductSplitter`.
@@ -430,7 +430,7 @@ Frobenius identity `x^q = x`, and that the shift schedule `0..q-1` reaches every
 element of `F` (all three hold for a prime field `F = ZMod q` of odd order). -/
 def czLinearFactorProductSplitter : LinearFactorProductSplitter F :=
   czLinearFactorProductSplitterOf
-    (fun q _ => Odd q ∧ (∀ x : F, x ^ q = x) ∧ (∀ x : F, x ∈ czDefaultShifts q))
+    (fun q _ ↦ Odd q ∧ (∀ x : F, x ^ q = x) ∧ (∀ x : F, x ∈ czDefaultShifts q))
     (by
       intro q p a hvalid hpne hroot
       obtain ⟨hodd, hfrob, hcover⟩ := hvalid
@@ -442,7 +442,7 @@ def czFiniteFieldContext (q : Nat) [Fact (Nat.Prime q)] : FiniteFieldContext (ZM
   { q := q
     finite := inferInstance
     card_eq := by rw [Nat.card_eq_fintype_card, ZMod.card]
-    frobenius_fixed := fun a => ZMod.pow_card a }
+    frobenius_fixed := fun a ↦ ZMod.pow_card a }
 
 /-- End-to-end root finder over `ZMod q`: stage 1 extracts the distinct field
 roots as `gcd(f, X^q - X)`, then the Cantor–Zassenhaus splitter separates them.
@@ -460,7 +460,7 @@ theorem czRoots_complete (q : Nat) [Fact (Nat.Prime q)] (hodd : Odd q)
     {f : CPolynomial (ZMod q)} {a : ZMod q} (hf : f ≠ 0) (hroot : CPolynomial.eval a f = 0) :
     a ∈ (czRoots q f).toList :=
   rootsInFiniteField_complete (czFiniteFieldContext q) czLinearFactorProductSplitter
-    (by intro p _; exact ⟨hodd, fun x => ZMod.pow_card x, fun x => zmod_mem_czDefaultShifts q x⟩)
+    (by intro p _; exact ⟨hodd, fun x ↦ ZMod.pow_card x, fun x ↦ zmod_mem_czDefaultShifts q x⟩)
     hf hroot
 
 end FiniteField