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 root-finding algorithm for univariate polynomials over odd prime fields ($ZMod q$).
• Extracts distinct linear factors via $\gcd(f, X^q - X)$ and separates them using quadratic characters $(X + s)^{(q-1)/2} \pmod g$.
• Isolates roots directly via $\gcd(g, X + s)$.
• Employs a deterministic shift schedule ($0$ to $q-1$) for completeness on small fields, structured to support future probabilistic extensions.

Proof Status

• Fully formalized with no sorry or admit placeholders.
• Provides soundness and completeness proofs for the equal-degree splitter and the czRoots function.

Integration & Testing

• Integrates logic into the Univariate/Roots pipeline and updates CompPoly.lean to expose the new functionality.
• Includes a test suite in tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean with executable #guard checks and formal verification for ZMod 7 instances.

---

Statistics

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

---

Lean Declarations

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

• theorem represented_coeff_one_ne_zero {q : CPolynomial F} in CompPoly/Univariate/Roots/CantorZassenhaus.lean
• theorem HasRootFactor.append_left {A B : Array (CPolynomial F)} {a : F} 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 czRoots_complete (q : Nat) [Fact (Nat.Prime q)] (hodd : Odd q) in CompPoly/Univariate/Roots/CantorZassenhaus.lean
• theorem eval_add (a : F) (p₁ p₂ : CPolynomial F) : in CompPoly/Univariate/Roots/CantorZassenhaus.lean
• private def fMult : CPolynomial F in tests/CompPolyTests/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
• theorem eval_shiftedPowModWith (M : CPolynomial.Raw.MulContext F) in CompPoly/Univariate/Roots/CantorZassenhaus.lean
• theorem linearFactor_toPoly (a : F) : in CompPoly/Univariate/Roots/CantorZassenhaus.lean
• example (a : F) (hf : fMult ≠ 0) (h : CPolynomial.eval a fMult = 0) : in tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean
• abbrev F : Type 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
• theorem czRefine_fst (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext 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
• theorem HasRootFactor.append_right {A B : Array (CPolynomial F)} {a : F} in CompPoly/Univariate/Roots/CantorZassenhaus.lean
• theorem monicNormalize_linearFactor (a : F) : in CompPoly/Univariate/Roots/CantorZassenhaus.lean
• def czFiniteFieldContext (q : Nat) [Fact (Nat.Prime q)] : FiniteFieldContext (ZMod q) in CompPoly/Univariate/Roots/CantorZassenhaus.lean
• theorem czShift_eq_linearFactor (s : 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 zmod_mem_czDefaultShifts (q : Nat) [Fact (Nat.Prime q)] (x : ZMod q) : in CompPoly/Univariate/Roots/CantorZassenhaus.lean
• private def p₀₁ : CPolynomial F in tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean
• def czLinearFactorProductSplitterOf 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 czLinearFactorProductSplitter : LinearFactorProductSplitter 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 czSplitLinearFactors (q : Nat) (p : CPolynomial F) : Array (CPolynomial F) in CompPoly/Univariate/Roots/CantorZassenhaus.lean
• theorem czRefine_root_in_residue_bucket in CompPoly/Univariate/Roots/CantorZassenhaus.lean
• theorem eval_linearFactor_self (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
• private def p₂₃ : CPolynomial F in tests/CompPolyTests/Univariate/Roots/CantorZassenhaus.lean
• theorem represented_zero_one_eq_false {q : CPolynomial F} 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 czSound (q : Nat) (shifts : List F) (p factor : CPolynomial F) 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
• theorem czRoots_sound (q : Nat) [Fact (Nat.Prime q)] {f : CPolynomial (ZMod q)} {a : ZMod q} in CompPoly/Univariate/Roots/CantorZassenhaus.lean
• theorem eval_X_add_C (a s : 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

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Naming Guidelines and Style Violations

• Theorem Naming: Several theorems violate the snake_case requirement for theorems and proofs. Most names use camelCase or a hybrid style:
  • czSound, czComplete, czComplete_core, czComplete_zmod, czRoots_sound, czRoots_complete should be in snake_case (e.g., cz_sound, cz_complete).
  • Theorems referencing camelCase definitions like czRefine_fst, linearFactor_toPoly, and monicNormalize_linearFactor should ideally use snake_case throughout (e.g., linear_factor_to_poly).
• Naming Conventions (Props): HasRootFactor is an abbrev for a Prop. While not a class, naming for Prop-valued terms usually follows snake_case or UpperCamelCase (if a class). Standardizing this to IsLinearRootFactor or similar may be more consistent with IsLinearFactor.
• Formatting (Empty Lines): There are empty lines inside multiple proof blocks, which violates the guideline "Avoid empty lines inside definitions or proofs." Examples include:
  • czComplete_core: Empty lines between have statements and by_cases branches.
  • czSound: Empty lines between induction cases.
• File Headers: The copyright year is listed as 2026 in both new files, which is inconsistent with the provided template and current date.
• Citation Format: In the module docstring for CantorZassenhaus.lean, the reference for [CZ81] includes "D. G." as the first initial. The instructions request [Author Last Name, First Initial, *Title*][citation_key] (e.g., [Cantor, D., and Zassenhaus, H., ...]).

Progress Against Roadmap

• Active Formalizations: This PR implements the Cantor–Zassenhaus algorithm, a known goal for root-finding over finite fields. It correctly plugs into the existing LinearFactorProductSplitter interface.
• Blueprints: For a significant contribution like CZ, the instructions recommend a blueprint. Ensure that the corresponding blueprint/src/references.bib has been updated with the [CZ81] BibTeX entry as per the citation standards.

Suggestions for Improvement

• Theorem Suffixes: For czRefine_fst, czRefine_snd_fst, and czRefine_snd_snd, consider using more descriptive names such as czRefine_zero_factor, czRefine_res_factor, and czRefine_nonres_factor to better reflect the mathematical roles (zero, residue, non-residue).

---

📄 **Per-File Summaries**

• CompPoly.lean: The update adds an import for the Cantor-Zassenhaus algorithm to the CompPoly.lean file, extending the library's univariate polynomial root-finding functionality.
• 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-27 06:38 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.