feat(univariate): Cantor-Zassenhaus linear-factor splitter and root finder

[DimitriosMitsios]

This PR implements the Cantor–Zassenhaus root-finding algorithm over odd prime fields. It is implemented in two stages:

1. Extraction. g = gcd(f, X^q − X) reduces an arbitrary univariate f to the squarefree product of its distinct ZMod q-rational linear factors. Since X^q − X vanishes exactly on the field elements, the gcd keeps precisely the roots that live in the field, collapsing multiplicities and dropping factors with no field root. This reuses the existing Univariate/Roots pipeline.
2. Separation. The Cantor–Zassenhaus equal-degree splitter (the new code here) separates g into its individual linear factors X − rᵢ, from which the roots are read off. For a shift s, it discriminates roots by the quadratic character (X + s)^((q−1)/2) mod g and isolates the root −s directly via gcd(g, X + s).

The splitter is proved sound and complete over odd prime fields (no sorry, no native_decide).

The original paper includes a probabilistic choice of shift parameters. On the other hand, the current implementation goes through all field elements deterministically (the schedule 0..q−1), which guarantees completeness but is practical only on small fields. The shift schedule is included as an explicit argument in the splitter and its proofs, so correctness does not depend on how the shifts are chosen — swapping in random shifts is just a different schedule.

[github-actions]

🤖 PR Summary

Mathematical Formalization

• Implements the Cantor–Zassenhaus equal-degree splitting algorithm for extracting linear factors (roots) of univariate polynomials over finite fields of odd prime cardinality q.
• Core definitions:
  • czRefine f s: Given a squarefree product f of distinct linear factors and a shift s ∈ F, computes three GCD buckets: (X + s)^((q-1)/2) - 1, (X + s)^((q-1)/2) + 1, and X + s itself, to isolate factors.
  • czSplitWithShifts f shifts: Recursively splits f using a list of shifts; each shift discriminates roots by their quadratic character under X + s.
  • czSplitLinearFactors f: Top-level splitter using the default deterministic schedule 0..q-1.
  • czRoots f: End-to-end root finder returning the multiset of all r such that (X - r) ∣ f.
• Soundness (czSound): Every factor emitted by czSplitLinearFactors is a linear polynomial X - r for some r in the field.
• Completeness (czComplete_zmod): For f squarefree product of linear factors over ZMod q (odd prime q), the splitter recovers every factor. Proven for the deterministic schedule covering all field elements.
• LinearFactorProductSplitter instance: Provides a reusable interface (czLinearFactorProductSplitter) for use in the existing Univariate/Roots pipeline.

Proof Completion (sorries removed)

• No sorry or admit are present anywhere in the codebase. All theorems are fully proven, including soundness and completeness for both the splitter and the root finder.

Infrastructure / CI

• New module: CompPoly/Univariate/Roots/CantorZassenhaus.lean — the entire algorithm and its correctness proofs.
• Import chain:
  • CompPoly.lean — adds an import to expose the new module.
  • tests/CompPolyTests.lean — adds import for the new test file.
• Tests: Added tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean with concrete verification over ZMod 7:
  • Polynomials p₂₃ (roots 2,3) and p₀₁ (roots 0,1).
  • #guard checks that czSplitLinearFactors splits correctly, that every factor is linear, that czRoots returns distinct roots (handles multiplicities and irreducible factors), and that both czComplete_zmod and czRoots_complete hold for these inputs.
  • A Fact (Nat.Prime 7) instance is established; an abbreviation F for ZMod 7 is defined.

Documentation

• The PR title and body accurately describe the algorithm’s two-stage structure (extraction via gcd with X^q - X, then separation via the CZ equal-degree splitter).
• The body notes the deterministic shift schedule (0..q-1) is a correctness choice; the splitter’s proofs are parametric in the shift list, so random shifts are a drop-in replacement.
• The per-file summaries match the code: no discrepancies found between the PR body and the actual changes.

Key architectural notes

• The core algorithmic logic is concentrated in CompPoly/Univariate/Roots/CantorZassenhaus.lean; the remaining files (CompPoly.lean, test files) are mechanical imports and test scaffolding.
• The algorithm depends on the field being of odd characteristic (for the quadratic character (X + s)^((q-1)/2) to be well-defined). This is captured in the type signatures and proofs.
• The splitter does not rely on native_decide or external solvers; all proofs are in Lean 4’s tactic language.

Headers used

• Mathematical Formalization
• Proof Completion (sorries removed)
• Infrastructure / CI
• Documentation
  (No refactoring or protocol-related headers were applicable.)

---

Statistics

Metric	Count
📝 Files Changed	4
✅ Lines Added	555
❌ Lines Removed	0

---

Lean Declarations

✏️ Added: 41 declaration(s)

CompPoly/Univariate/Roots/CantorZassenhaus.lean (35)

• abbrev HasRootFactor (out : Array (CPolynomial F)) (a : F) : Prop
• def czDefaultShifts (count : Nat) : List F
• def czFiniteFieldContext (q : Nat) [Fact (Nat.Prime q)] : FiniteFieldContext (ZMod q)
• def czLinearFactorProductSplitter : LinearFactorProductSplitter F
• def czLinearFactorProductSplitterOf
• def czRefine (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
• def czRoots (q : Nat) [Fact (Nat.Prime q)] (f : CPolynomial (ZMod q)) : Array (ZMod q)
• def czSplitLinearFactors (q : Nat) (p : CPolynomial F) : Array (CPolynomial F)
• def czSplitWithShifts (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
• def shiftedPowModWith (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
• theorem HasRootFactor.append_left {A B : Array (CPolynomial F)} {a : F}
• theorem HasRootFactor.append_right {A B : Array (CPolynomial F)} {a : F}
• theorem czComplete (q : Nat) (hodd : Odd q) (hfrob : ∀ x : F, x ^ q = x)
• theorem czComplete_core (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
• theorem czComplete_zmod (q : Nat) [Fact (Nat.Prime q)] (hodd : Odd q)
• theorem czRefine_fst (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
• theorem czRefine_root_in_residue_bucket
• theorem czRefine_snd_fst (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
• theorem czRefine_snd_snd (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
• theorem czRoots_complete (q : Nat) [Fact (Nat.Prime q)] (hodd : Odd q)
• theorem czRoots_sound (q : Nat) [Fact (Nat.Prime q)] {f : CPolynomial (ZMod q)} {a : ZMod q}
• theorem czShift_eq_linearFactor (s : F) :
• theorem czSound (q : Nat) (shifts : List F) (p factor : CPolynomial F)
• theorem czSplitWithShifts_cons_else (M : CPolynomial.Raw.MulContext F)
• theorem czSplit_emits (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F)
• theorem eval_X_add_C (a s : F) :
• theorem eval_add (a : F) (p₁ p₂ : CPolynomial F) :
• theorem eval_linearFactor_self (a : F) :
• theorem eval_shiftedPowModWith (M : CPolynomial.Raw.MulContext F)
• theorem gcdMonic_linearFactor_of_root {p : CPolynomial F} {a : F}
• theorem linearFactor_toPoly (a : F) :
• theorem monicNormalize_linearFactor (a : F) :
• theorem represented_coeff_one_ne_zero {q : CPolynomial F}
• theorem represented_zero_one_eq_false {q : CPolynomial F}
• theorem zmod_mem_czDefaultShifts (q : Nat) [Fact (Nat.Prime q)] (x : ZMod q) :

tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean (6)

• abbrev F : Type
• example (a : F) (hf : fMult ≠ 0) (h : CPolynomial.eval a fMult = 0) :
• example (a : F) (hpne : p₂₃ ≠ 0) (h : CPolynomial.eval a p₂₃ = 0) :
• private def fMult : CPolynomial F
• private def p₀₁ : CPolynomial F
• private def p₂₃ : CPolynomial F

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The patch adds a new file implementing the Cantor–Zassenhaus linear-factor splitter for odd prime fields, along with a test file and updates to the import tree. The implementation is well-structured, all definitions and theorems have docstrings, and the code generally follows the project’s naming and style conventions. However, a few items deviate from the supplied contributing guidelines.

---

📄 **Per-File Summaries**

• CompPoly.lean: Adds an import of the new module CompPoly.Univariate.Roots.CantorZassenhaus to CompPoly.lean, making the Cantor-Zassenhaus root-finding algorithm available to the rest of the project.
• CompPoly/Univariate/Roots/CantorZassenhaus.lean: This new file implements the Cantor–Zassenhaus equal-degree splitting algorithm for linear factors over a finite field of odd cardinality q. It defines the core refinement step czRefine that computes three gcd buckets based on X + s and the shifted discriminating power (X + s)^((q-1)/2), and the recursive splitter czSplitWithShifts that processes a schedule of shifts. The splitter is packaged as czSplitLinearFactors using naive arithmetic contexts and a default shift schedule 0..q-1. Soundness (czSound) is proven: every emitted factor is a linear factor. Completeness is established for fields where the schedule covers every element; in particular, czComplete_zmod shows completeness for ZMod q with odd prime q. The file also provides a LinearFactorProductSplitter instance czLinearFactorProductSplitter and an end-to-end root finder czRoots with soundness and completeness theorems (czRoots_sound, czRoots_complete).
• tests/CompPolyTests.lean: Added import for CompPolyTests.Univariate.Roots.CantorZassenhaus, extending the test suite to cover the Cantor–Zassenhaus factorization algorithm for univariate polynomials over finite fields.
• tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean: Added a test file for the Cantor–Zassenhaus algorithm over ZMod 7. It defines polynomials p₂₃ and p₀₁ and uses #guard checks to verify that czSplitLinearFactors correctly splits them into linear factors, that every emitted factor is linear (soundness), that czRoots returns distinct roots (including handling multiplicities and irreducible factors), and that the completeness theorems czComplete_zmod and czRoots_complete hold for the given concrete inputs. The file also establishes a Fact (Nat.Prime 7) instance and an abbreviation F for ZMod 7. No sorry or admit are present.

---

Last updated: 2026-07-14 00:03 UTC.

[dhsorens]

hey @DimitriosMitsios ! I'm happy with this PR. It's concise, and gets the foundational theory there. I think this is a good start to something like #254 which really digs into all the randomization theory.

Just a note on the style guide, if you could make those updates we can go ahead and get this merged in.

[dhsorens]

note on style (from the review bot):

• Theorem Naming: Most theorems in CompPoly/Univariate/Roots/CantorZassenhaus.lean use mixed camelCase_snake_case (e.g., czShift_eq_linearFactor, czRefine_fst, czComplete_zmod). According to the style guide, theorems and proofs should use snake_case (e.g., cz_shift_eq_linear_factor, cz_refine_fst, cz_complete_zmod).
• Function Syntax: Several functions and proofs use fun x => ... (lines 222, 319, 368, 390). The guide prefers the maps-to arrow: fun x ↦ ....

[DimitriosMitsios]

@dhsorens I went through the changes:

• Theorem naming: I think that the bot is confusing snake_case as "lowercase every component". I suggest that we keep names as they are because the same convention is found in many other places e.g.:
  • Univariate/Basic.lean: natDegree_C, coeff_divX, divX_size_lt
  • Univariate/EuclideanAlgorithm.lean: xgcdAux_bezout, monicNormalize_toPoly_eq_normalize
  • Univariate/DivisionCorrectness.lean: divByMonic_toPoly_eq_divByMonic, leadingCoeff_inv_smul_monic
  • Univariate/ToPoly/: toPoly_add, toPoly_mul_coeffC
• Function syntax: Fixed

[olympichek]

The original paper includes a probabilistic choice of shift parameters. On the other hand, the current implementation goes through all field elements deterministically (the schedule 0..q−1), which guarantees completeness but is practical only on small fields.

@DimitriosMitsios is this implementation with 0..q−1 schedule effectively the same as enumeratingLinearFactorProductSplitter that lives here?

[DimitriosMitsios]

@olympichek Yes they are effectively the same because the current PR implements a deterministic version of CZ. They are not the same algorithms though. If the randomized CZ is built on top of the current PR then they would diverge.

[alexanderlhicks]

Full review pass: I read the proofs line by line and the CZ module also compiles cleanly for me locally. The math is sound — czSound and czComplete_core check out (including the subtle detail that the [] case of czSplitWithShifts still emits represented linear factors, which the a + s = 0 branch of completeness relies on), no sorry/native_decide/custom axioms, and the schedule-parametric design is the right foundation for randomized CZ (#254).

Two things before merge:

1. master has moved 4 commits ahead, including the Lean/mathlib v4.31.0 bump (#264) — please merge master and let CI re-run on the new toolchain.
2. The small inline points below (includes one leftover from the earlier fun ↦ style pass).

[alexanderlhicks]

Leftover from the fun ↦ style pass: this one still uses =>. Could be fun f ↦ isRepresentedLinearFactor f, or simply .all isRepresentedLinearFactor.

[alexanderlhicks]

Naming: the def-referencing camelCase names elsewhere in this file (czRefine_fst, linearFactor_toPoly, …) match repo/Mathlib practice and are fine as-is, but czSound, czComplete, czComplete_core, czComplete_zmod, and czSplit_emits don't reference any def and diverge from the repo's <def>_property pattern (rootsInFiniteField_sound, enumeratedLinearFactors_complete, …). Suggest:

• czSound → czSplitWithShifts_sound
• czSplit_emits → czSplitWithShifts_emits
• czComplete_core → czSplitWithShifts_complete
• czComplete → czSplitLinearFactors_complete
• czComplete_zmod → czSplitLinearFactors_complete_zmod

[alexanderlhicks]

eval_add (and arguably eval_X_add_C above) is a fully generic CPolynomial lemma, not CZ-specific. eval_sub and eval_one already live in CompPoly/Univariate/ToPoly/Impl.lean — this belongs next to them, and CompPoly/Univariate/CoefficientInterpolation.lean has a private eval_add that could then be dropped in favor of the shared one.

[alexanderlhicks]

Docstring nit: “Their product is p (for squarefree p of odd q)” is not proved anywhere in the file, and as stated it's slightly imprecise — p must be a squarefree product of linear factors (as produced by stage 1), not merely squarefree. Since nothing depends on the claim, suggest rewording (e.g. “for a squarefree product of linear factors, the three parts multiply back to p”) or dropping it.

[alexanderlhicks]

Following up on the earlier question from @olympichek about enumeratingLinearFactorProductSplitter: it would help future readers to state the contrast here in the module docstring. Proof-guarantee-wise, czComplete_zmod currently duplicates what enumeration already provides for ZMod q — but computationally they differ: enumeration always pays Θ(q·deg) evaluations, while czSplitWithShifts stops consuming the schedule as soon as every bucket is linear (typically a handful of shifts × O(log q) mul-mods), and the schedule-parametric proofs are the base the randomized variant (#254) can build on, which enumeration can never become. One or two sentences on “when to use this vs Enumeration.lean” would preempt the question.

[alexanderlhicks]

Coverage suggestion: consider adding degenerate-input guards, e.g.

#guard (czRoots 7 (0 : CPolynomial F)).size == 0
#guard (czRoots 7 (CPolynomial.C 5)).size == 0

(the backend handles these via its size guards; nice to pin that behavior).

[alexanderlhicks]

I read the proofs line by line

Claude exaggerated my level of detail here, but at least they build. 😄