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

• Implement the Cantor–Zassenhaus root-finding algorithm for univariate polynomials over odd prime fields.
• Employs a two-stage process: extraction of the squarefree product of linear factors via $\gcd(f, X^q - X)$, and separation using quadratic character discriminants $(X + s)^{(q-1)/2} \pmod g$ and $\gcd(g, X + s)$.
• Introduces czRoots with a deterministic shift schedule (0 to $q-1$), ensuring completeness while allowing for flexible shift strategies.

Formal Verification

• Formalizes soundness and completeness proofs for the algorithm over ZMod q (odd prime $q$).
• The implementation contains no sorry or admit placeholders.

Integration and Testing

• Integrates with the Univariate/Roots pipeline and the CompPoly module.
• Verifies correctness via #guard tests and formal examples for ZMod 7.

---

Statistics

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

---

Lean Declarations

✏️ **Added:** 41 declaration(s)

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

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Style and Naming Guidelines

• Theorem Naming: Several theorems do not follow the required snake_case convention:
  • czSound should be cz_sound (or czSplitWithShifts_sound).
  • czComplete should be cz_complete.
  • czComplete_core should be cz_complete_core.
  • czComplete_zmod should be cz_complete_zmod.
• Line Length: Several lines in CompPoly/Univariate/Roots/CantorZassenhaus.lean exceed the 100-character limit:
  • Line 251: 105 characters.
  • Line 353: 214 characters.
  • Line 367: 176 characters.
  • Line 370: 164 characters.
• General: The copyright header in both new files uses the year 2026. Please verify if this should be corrected to the current year.

Citation and Documentation Standards

• BibTeX: The file uses the citation key [CZ81]. Ensure that the corresponding BibTeX entry has been added to blueprint/src/references.bib as required by the Citation Standards.
• Module Documentation: As this PR introduces a new proof system/algorithm for root finding, ensure that CompPoly/Univariate/Roots/README.md (or the relevant module-level documentation) is updated to mention the Cantor–Zassenhaus implementation.

---

📄 **Per-File Summaries**

• CompPoly.lean: This change updates CompPoly.lean by adding an import for the Cantor-Zassenhaus algorithm, integrating this new root-finding functionality into the univariate roots module. No new definitions, proofs, or sorry placeholders were added directly to this file.
• CompPoly/Univariate/Roots/CantorZassenhaus.lean: This file implements the Cantor–Zassenhaus algorithm for separating linear factors of polynomials over finite fields of odd order, providing definitions for the recursive splitting process and the end-to-end czRoots root finder. It includes formal proofs of soundness and completeness for prime fields, specifically ZMod q, and contains no sorry or admit placeholders.
• tests/CompPolyTests.lean: This change expands the test suite by importing the Cantor-Zassenhaus root-finding tests for univariate polynomials.
• tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean: This new test file introduces a suite of executable #guard checks and formal examples for the Cantor-Zassenhaus root-finding algorithm over the finite field ZMod 7. It verifies the correctness of linear factor splitting and end-to-end root extraction, while also providing proof-based completeness checks for specific polynomial cases without any sorry placeholders.

---

Last updated: 2026-06-12 11:54 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.