feat(univariate): Shoup and Las Vegas root-search backends by dhsorens · Pull Request #290 · Verified-zkEVM/CompPoly

dhsorens · 2026-08-07T14:40:44Z

Summary

Re-land of olympichek’s (Valerii Huhnin) univariate root-search work from #253 / #254 onto current main (module system, Lean/Mathlib 4.32).

Adds two LinearFactorProductSplitter backends for finite fields that do not admit a smooth multiplicative-subgroup schedule:

Shoup (Roots/Shoup/) — small-characteristic trace-coordinate splitting [vzGS92].
Las Vegas CZ (Roots/LasVegas/) — bounded randomized Cantor–Zassenhaus (odd-char and char-2 trace branches), explicit pure ProbeFamily randomness, deterministic fallback, soundness/completeness, and probability proofs.

This closes the documented root-finding gap (only SmoothSubgroup existed) without merging the stale PRs as-is.

Attribution

Original author: Valerii Huhnin (olympichek) — commit author and Authors: headers retained.
Maintainer port (module system, API drift fixes, Tower test integration, docs): Derek Sorensen (Co-authored-by).

What we deliberately did not land

The ~18k-line parallel Fields/Binary/GF2_{32,48,64,72} + Binary/Extension stack from feat(univariate): randomized Cantor-Zassenhaus root search #254. That duplicated Tower/BF128 architecture.
Char-2 coverage here uses ZMod 2 and binary-tower level 0 in tests (integration path for Tower). Named high-width Tower SmallPrimeTraceContext instances (32/64) and optional GF(2^{48})/GF(2^{72}) carriers remain follow-up (ROADMAP 🔄).

Idiom notes

Module system: module / public import / @[expose] public section (meta on tests).
Layout mirrors SmoothSubgroup/ (Basic + Correctness facades).
Contracts via existing FiniteFieldContext / LinearFactorProductSplitter.
Facades regenerated with ./scripts/update-lib.sh.
Wiki + ROADMAP updated in this PR.

Supersedes

feat(univariate): Cantor-Zassenhaus linear-factor splitter and root finder #252 (deterministic odd CZ wedge) — already closed.
feat(univariate): Shoup's trace splitter root search #253, feat(univariate): randomized Cantor-Zassenhaus root search #254 — re-landed here (auto-close on merge).

Closes #253
Closes #254

#255 (approximant/hybrid GS) is a separate re-land track (#291).

Test plan

github-actions · 2026-08-07T14:44:10Z

🤖 PR Summary

Adds two LinearFactorProductSplitter backends for finite fields that do not admit a smooth multiplicative-subgroup schedule: Shoup (small-characteristic trace-coordinate splitting) and Las Vegas CZ (bounded randomized Cantor–Zassenhaus with odd-char and char-2 trace branches, exhaustive enumeration fallback, and full probability proofs). All proofs are complete (no sorry or admit). The PR also includes documentation updates, tests over small fields, and the module-system plumbing to expose the new modules publicly.

Statistics

Metric	Count
📝 Files Changed	27
✅ Lines Added	10291
❌ Lines Removed	9

Lean Declarations

✏️ Added: 453 declaration(s)

CompPoly/Univariate/Roots/LasVegas/Basic.lean (25)

def cantorZassenhausEvenTraceAttemptWith {F : Type*}
def cantorZassenhausOddAttemptWith {F : Type*}
def isNontrivialProperChild {F : Type*} [Field F] [BEq F] [LawfulBEq F]
def lasVegasSplitCandidatesWith {F : Type*}
def lasVegasSplitCandidatesWithTrace {F : Type*}
def lasVegasSplitCandidatesWithTrace? {F : Type*}
def lasVegasSplitLinearFactorsWith {F : Type*}
def lasVegasSplitLinearFactorsWithTrace {F : Type*}
def lasVegasSplitLinearFactorsWithTrace? {F : Type*}
def lasVegasSplitLoopWith {F : Type*}
def lasVegasSplitterInput {F : Type*} [Field F]
def nontrivialProperChildren {F : Type*} [Field F] [BEq F] [LawfulBEq F]
def powModWith {F : Type*} [Field F] [BEq F] [LawfulBEq F]
def quotientAfterChild {F : Type*} [Field F] [BEq F] [LawfulBEq F]
def reduceModWith {F : Type*} [Field F] [BEq F] [LawfulBEq F]
def seededLinearProbeFamily {F : Type*} [Field F] [BEq F] [LawfulBEq F]
def tableProbeFamily {F : Type*} [Field F] [BEq F] [LawfulBEq F]
def traceBasisProbeFamily {F : Type*} [Field F] [BEq F] [LawfulBEq F]
def traceContextMatchesQ {F : Type*} [Field F] [BEq F] [LawfulBEq F]
def tracePowerSumPolynomialLoopWith {F : Type*}
def tracePowerSumPolynomialWith {F : Type*}
def tryEvenTraceSplitAttemptsWith {F : Type*}
def tryOddSplitAttemptsWith {F : Type*}
theorem lasVegasSplitLinearFactorsWithTrace_sound {F : Type*}
theorem lasVegasSplitLinearFactorsWith_sound {F : Type*}

CompPoly/Univariate/Roots/LasVegas/Correctness/Common.lean (75)

def normStackReady {F : Type*} [Field F] [BEq F] [LawfulBEq F]
lemma mem_eraseDups_fold {α : Type*} [BEq α] [LawfulBEq α]
lemma mem_eraseDups_fold_of_mem {α : Type*} [BEq α] [LawfulBEq α]
lemma mem_eraseDups_of_mem {α : Type*} [BEq α] [LawfulBEq α]
lemma mem_of_mem_eraseDups {α : Type*} [BEq α] [LawfulBEq α]
noncomputable def normSplitWork {F : Type*} [Field F] [BEq F] [LawfulBEq F]
noncomputable def normStackWork {F : Type*} [Field F] [BEq F] [LawfulBEq F] :
noncomputable def splitWork {F : Type*} [Field F] [BEq F] [LawfulBEq F]
noncomputable def stackWork {F : Type*} [Field F] [BEq F] [LawfulBEq F] :
theorem child_ne_one_of_root {F : Type*}
theorem child_ne_zero_of_proper {F : Type*}
theorem child_quotient_natDegree_le_parent {F : Type*}
theorem child_size_le_fuel_of_proper_of_parent_size_le_succ {F : Type*}
theorem div_ne_zero_of_dvd_of_ne_zero {F : Type*}
theorem eq_of_monic_dvd_of_val_size_le {F : Type*}
theorem eq_of_monic_toPoly_dvd_of_natDegree_le {F : Type*}
theorem eq_of_not_proper_of_monic_dvd {F : Type*}
theorem eq_of_toPoly_eq {F : Type*}
theorem eval_monicNormalize_gcdMonic_eq_zero_iff {F : Type*}
theorem eval_powModWith_eq_pow {F : Type*}
theorem eval_reduceModWith_eq_self_of_root {F : Type*}
theorem finiteFieldRootProductWith_lasVegasSplitterInput {F : Type*}
theorem finiteFieldRootProduct_lasVegasSplitterInput {F : Type*}
theorem gcdMonic_ne_zero_left {F : Type*}
theorem left_proper_of_pair_filter_size_ge_two {F : Type*}
theorem middle_proper_of_triple_eraseDups_filter_size_ge_two_of_not_left {F : Type*}
theorem monicNormalize_size_le_self {F : Type*}
theorem monicNormalize_toPoly_degree_pos_of_proper {F : Type*}
theorem monicNormalize_toPoly_monic_of_ne_zero {F : Type*}
theorem monicNormalize_toPoly_natDegree_eq {F : Type*}
theorem monicNormalize_toPoly_natDegree_pos_of_proper {F : Type*}
theorem monicNormalize_zero {F : Type*}
theorem nontrivialProperChildren_mem_of_mem {F : Type*}
theorem normSplitWork_eq_splitWork {F : Type*}
theorem normSplitWork_pos_of_monicNormalize_ne_zero_ne_one {F : Type*}
theorem normSplitWork_pos_of_monic_ne_zero_ne_one {F : Type*}
theorem normSplitWork_pos_ready {F : Type*}
theorem normStackReady_append {F : Type*}
theorem normStackReady_tail {F : Type*}
theorem normStackWork_append {F : Type*}
theorem normStackWork_eq_stackWork {F : Type*}
theorem normStackWork_pos_of_mem {F : Type*}
theorem normStackWork_split_stack_le {F : Type*}
theorem normStackWork_tail_le_of_cons_le {F : Type*}
theorem polynomial_natDegree_le_of_degree_le {F : Type*} [Field F]
theorem proper_child_of_ne_zero_root_size_lt {F : Type*}
theorem proper_child_of_proper_intermediate {F : Type*}
theorem proper_of_mem_nontrivialProperChildren {F : Type*}
theorem quotientAfterChild_ne_zero_of_dvd {F : Type*}
theorem quotientAfterChild_root_of_not_child_root {F : Type*}
theorem quotientAfterChild_size_le_parent {F : Type*}
theorem quotientAfterChild_size_lt_parent_of_monicNormalize_proper {F : Type*}
theorem quotientAfterChild_toPoly_dvd_parent {F : Type*}
theorem quotientAfterChild_toPoly_monic_of_dvd {F : Type*}
theorem right_proper_of_pair_filter_size_ge_two {F : Type*}
theorem right_proper_of_triple_eraseDups_filter_size_ge_two_of_not_left {F : Type*}
theorem right_proper_of_triple_eraseDups_filter_size_ge_two_of_not_middle {F : Type*}
theorem splitWork_monicNormalize_eq {F : Type*}
theorem splitWork_pair_le_of_natDegree_sum_le {F : Type*}
theorem splitWork_pos_of_monic_ne_zero_ne_one {F : Type*}
theorem splitWork_pos_of_natDegree_pos {F : Type*}
theorem splitWork_triple_le_of_first_two_pos_natDegree_sum_le {F : Type*}
theorem splitWork_triple_le_of_natDegree_sum_le {F : Type*}
theorem split_child_or_quotient_root {F : Type*}
theorem stackWork_append {F : Type*}
theorem stackWork_eraseDups_fold_le {F : Type*}
theorem stackWork_eraseDups_le {F : Type*}
theorem stackWork_eraseDups_triple_dup_right_le {F : Type*}
theorem stackWork_push {F : Type*}
theorem third_proper_of_triple_filter_size_ge_two_of_not_left {F : Type*}
theorem toPoly_natDegree_pos_of_monic_ne_zero_ne_one {F : Type*}
theorem toPoly_ne_one_of_ne_one {F : Type*}
theorem val_size_eq_natDegree_add_one_of_ne_zero {F : Type*}
theorem val_size_le_of_toPoly_natDegree_le {F : Type*}
theorem val_size_lt_of_toPoly_degree_lt {F : Type*}

CompPoly/Univariate/Roots/LasVegas/Correctness/EvenTrace.lean (18)

private theorem cantorZassenhausEvenTraceAttemptWith_root {F : Type*}
private theorem eval_add_eq {F : Type*} [Field F] [BEq F] [LawfulBEq F]
private theorem eval_tracePowerSumPolynomialLoopWith {F : Type*}
private theorem tryEvenTraceSplitAttemptsWith_child_proper {F : Type*}
private theorem two_le_size_filter_pair {F : Type*}
theorem cantorZassenhausEvenTraceAttemptWith_child_dvd_input {F : Type*}
theorem cantorZassenhausEvenTraceAttemptWith_child_normSplitWork_pos {F : Type*}
theorem cantorZassenhausEvenTraceAttemptWith_child_proper {F : Type*}
theorem cantorZassenhausEvenTraceAttemptWith_probe_congr {F : Type*}
theorem cantorZassenhausEvenTraceAttemptWith_size_ge_two {F : Type*}
theorem cantorZassenhausEvenTraceAttemptWith_stackWork_le {F : Type*}
theorem cantorZassenhausEvenTraceAttemptWith_success_of_trace_separated {F : Type*}
theorem eval_tracePowerSumPolynomialWith_eq {F : Type*}
theorem tryEvenTraceSplitAttemptsWith_child_normSplitWork_pos {F : Type*}
theorem tryEvenTraceSplitAttemptsWith_eq_some_exists_attempt {F : Type*}
theorem tryEvenTraceSplitAttemptsWith_probe_congr {F : Type*}
theorem tryEvenTraceSplitAttemptsWith_root {F : Type*}
theorem tryEvenTraceSplitAttemptsWith_stackWork_le {F : Type*}

CompPoly/Univariate/Roots/LasVegas/Correctness/Loop.lean (12)

def lasVegasLinearFactorProductSplitterWith {F : Type*}
def lasVegasLinearFactorProductSplitterWithTrace {F : Type*}
private theorem lasVegasSplitLinearFactorsWithTrace?_complete {F : Type*}
private theorem lasVegasSplitLoopWith_complete_of_state {F : Type*}
private theorem lasVegasSplitLoopWith_fallback_complete {F : Type*}
private theorem lasVegasSplitLoopWith_mem_of_mem_out {F : Type*}
private theorem lasVegasSplitLoopWith_represented_mem_of_mem_out {F : Type*}
private theorem linearFactor_mem_enumeratedLinearFactors {F : Type*}
private theorem representedEnumeratedLinearFactors_complete {F : Type*}
theorem lasVegasSplitLinearFactorsWithTrace_complete {F : Type*}
theorem lasVegasSplitLinearFactorsWith_complete {F : Type*}
theorem rootProduct_satisfies_lasVegasSplitterInput {F : Type*}

CompPoly/Univariate/Roots/LasVegas/Correctness/Odd.lean (19)

private theorem cantorZassenhausOddAttemptWith_root {F : Type*}
private theorem cantorZassenhausOddAttemptWith_success_aux {F : Type*}
private theorem tryOddSplitAttemptsWith_child_proper {F : Type*}
private theorem two_le_length_of_mem_of_mem_of_ne {α : Type*} {l : List α} {u v : α}
private theorem two_le_size_eraseDups_of_mem_of_mem_of_ne {α : Type*} [BEq α] [LawfulBEq α]
theorem cantorZassenhausOddAttemptWith_child_dvd_input {F : Type*}
theorem cantorZassenhausOddAttemptWith_child_normSplitWork_pos {F : Type*}
theorem cantorZassenhausOddAttemptWith_child_proper {F : Type*}
theorem cantorZassenhausOddAttemptWith_ne_zero {F : Type*}
theorem cantorZassenhausOddAttemptWith_probe_congr {F : Type*}
theorem cantorZassenhausOddAttemptWith_root_preserved {F : Type*}
theorem cantorZassenhausOddAttemptWith_size_ge_two {F : Type*}
theorem cantorZassenhausOddAttemptWith_stackWork_le {F : Type*}
theorem cantorZassenhausOddAttemptWith_success_of_bucket_separated {F : Type*}
theorem tryOddSplitAttemptsWith_child_normSplitWork_pos {F : Type*}
theorem tryOddSplitAttemptsWith_eq_some_exists_attempt {F : Type*}
theorem tryOddSplitAttemptsWith_probe_congr {F : Type*}
theorem tryOddSplitAttemptsWith_root {F : Type*}
theorem tryOddSplitAttemptsWith_stackWork_le {F : Type*}

CompPoly/Univariate/Roots/LasVegas/OddBucket.lean (4)

def oddCZBucket {F : Type*} [MonoidWithZero F] [BEq F] [LawfulBEq F]

…and 303 more not listed.

sorry Tracking

No sorrys were added, removed, or affected.

Coverage Notes

AI file summarization partially analyzed 1 file(s) because their individual diffs exceeded the per-file size budget. Statistics and Lean signal tracking still cover the full PR.

Partially Analyzed Files

CompPoly/Univariate/Roots/Shoup/Correctness.lean (+1401/-0)

* Additional-instructions analysis was skipped because the full diff exceeded the analysis size budget, and partial results would be misleading.

📄 **Per-File Summaries**

CompPoly.lean: This diff adds 21 new public import directives to CompPoly.lean, exposing two major new modules: LasVegas and Shoup, each with several submodules. The LasVegas imports span Basic, Correctness (with submodules Common, EvenTrace, Loop, Odd), OddBucket, and Probability (including Basic, EvenTrace, OddBuckets, OddTrial, Recursive, Repeated, Uniform). The Shoup imports cover Basic, Correctness, and FrobeniusLinear. These imports make the definitions, theorems, and structures from these new subfiles available to downstream consumers of the CompPoly top-level module.
CompPoly/Univariate/Roots.lean: Made the CompPoly/Univariate/Roots module publicly re-export two newly added submodules: CompPoly.Univariate.Roots.LasVegas and CompPoly.Univariate.Roots.Shoup. This expands the public API of the module to include the definitions and theorems provided by those submodules.
CompPoly/Univariate/Roots/LasVegas.lean: Added a new file CompPoly/Univariate/Roots/LasVegas.lean that publicly re-exports CompPoly.Univariate.Roots.LasVegas.Basic and CompPoly.Univariate.Roots.LasVegas.Correctness. The file introduces an @[expose] public section to serve as the module's public interface, providing an entry point for bounded Las Vegas finite-field root splitting with exhaustive enumeration fallback.
CompPoly/Univariate/Roots/LasVegas/Basic.lean: This file adds the complete Las Vegas linear-factor splitting module for finite-field root products. It introduces the ProbeFamily structure and three concrete probe families (seededLinearProbeFamily, tableProbeFamily, traceBasisProbeFamily), the LasVegasConfig configuration structure, and the lasVegasSplitterInput predicate. The core splitting algorithm is implemented through cantorZassenhausOddAttemptWith (odd-field Cantor-Zassenhaus), cantorZassenhausEvenTraceAttemptWith (characteristic-two trace-based splitting using tracePowerSumPolynomialWith), tryOddSplitAttemptsWith, tryEvenTraceSplitAttemptsWith, and lasVegasSplitLoopWith, which orchestrates splitting with enumeration fallback. Public entry points include lasVegasSplitCandidatesWith, lasVegasSplitLinearFactorsWith, and their trace-aware counterparts, plus two soundness theorems (lasVegasSplitLinearFactorsWith_sound, lasVegasSplitLinearFactorsWithTrace_sound) that delegate to representedLinearFactorsOnly_sound. No sorry or admit are present.
CompPoly/Univariate/Roots/LasVegas/Correctness.lean: Created a new file CompPoly/Univariate/Roots/LasVegas/Correctness.lean as a collector module that publicly exports CompPoly.Univariate.Roots.LasVegas.Correctness.Loop and introduces an @[expose] public section to surface the correctness API for the bounded Las Vegas splitter. No new theorems, definitions, or sorries are added — the file purely re-exports an existing module and declares an exposure annotation for the public section. This provides the entry point for the correctness surface of the Las Vegas splitting algorithm.
CompPoly/Univariate/Roots/LasVegas/Correctness/Common.lean: This new file adds shared correctness lemmas for the Las Vegas splitter over finite fields. It introduces root-preservation theorems (eval_reduceModWith_eq_self_of_root, eval_powModWith_eq_pow), establishes that the finiteFieldRootProduct functions satisfy the lasVegasSplitterInput predicate, and defines work measures (splitWork, stackWork, normSplitWork, normStackWork) with accompanying lemmas for termination/induction. It also provides a battery of lemmas about nontrivialProperChildren/isNontrivialProperChild, quotientAfterChild, monic normalization, size bounds, and GCD evaluation, all of which are used by the correctness proofs of the Las Vegas splitter.
CompPoly/Univariate/Roots/LasVegas/Correctness/EvenTrace.lean: This file adds a new module CompPoly/Univariate/Roots/LasVegas/Correctness/EvenTrace.lean containing 12 theorems and lemmas that establish correctness properties for the even-trace split attempt (cantorZassenhausEvenTraceAttemptWith) and its retry loop (tryEvenTraceSplitAttemptsWith) in the Las Vegas factorization algorithm. The theorems prove that when these routines succeed, each resulting child polynomial is a nontrivial proper divisor of the monic-normalized input (cantorZassenhausEvenTraceAttemptWith_child_proper, tryEvenTraceSplitAttemptsWith_child_proper), divides the input polynomial (cantorZassenhausEvenTraceAttemptWith_child_dvd_input), has positive norm-split work (cantorZassenhausEvenTraceAttemptWith_child_normSplitWork_pos, tryEvenTraceSplitAttemptsWith_child_normSplitWork_pos), and that the overall stack work bound is preserved (cantorZassenhausEvenTraceAttemptWith_stackWork_le, tryEvenTraceSplitAttemptsWith_stackWork_le). A root-preservation lemma (cantorZassenhausEvenTraceAttemptWith_root, tryEvenTraceSplitAttemptsWith_root) ensures any root of the input remains a root of at least one child. Two _probe_congr theorems show that the attempt and retry loop depend only on the actual probe values drawn, not on the probe family. A critical cantorZassenhausEvenTraceAttemptWith_success_of_trace_separated theorem proves that if a probe's trace power sum separates two distinct roots (one zero, one nonzero), then the even-trace split attempt succeeds in producing a nontrivial factorization. The file also includes a private lemma eval_tracePowerSumPolynomialLoopWith and the public theorem cantorZassenhausEvenTraceAttemptWith_size_ge_two and eval_tracePowerSumPolynomialWith_eq. The diff is entirely new code with no sorry or admit statements.
CompPoly/Univariate/Roots/LasVegas/Correctness/Loop.lean: This new file provides the completeness surface for the Las Vegas polynomial splitting loop, proving that any root found in the input polynomial is represented in the output factor list. Key additions include:

representedEnumeratedLinearFactors_complete: shows that for any root a of p, the linear factor X - a is among the represented linear factors of the enumerated list.
linearFactor_mem_enumeratedLinearFactors: directly places X - a in the enumerated linear factors.
lasVegasSplitLoopWith_mem_of_mem_out and lasVegasSplitLoopWith_represented_mem_of_mem_out: monotonicity lemmas stating that factors already in the output array remain in the loop's result, and if they are represented linear factors, they appear in the represented-only filtered output.
lasVegasSplitLoopWith_fallback_complete: handles the fallback case by applying the enumeration to g when g has a root a.
lasVegasSplitLoopWith_complete_of_state: the main inductive completeness lemma for the loop, using a fuel-based induction and assuming work/ready conditions on the stack, to produce a represented linear factor candidate.
lasVegasSplitLinearFactorsWithTrace?_complete, lasVegasSplitLinearFactorsWith_complete, and lasVegasSplitLinearFactorsWithTrace_complete: public completeness theorems for the top-level splitter functions.
lasVegasLinearFactorProductSplitterWith and lasVegasLinearFactorProductSplitterWithTrace: structure instances packaging these splitters as LinearFactorProductSplitter values, wiring up soundness and completeness proofs.
rootProduct_satisfies_lasVegasSplitterInput: a convenience theorem confirming that a root product satisfies the splitter's input precondition.

No sorry or admit are present.

CompPoly/Univariate/Roots/LasVegas/Correctness/Odd.lean: This file introduces the correctness lemmas for the odd-characteristic Cantor-Zassenhaus split step. It adds the private theorem cantorZassenhausOddAttemptWith_root, which already existed, and then provides three new results: cantorZassenhausOddAttemptWith_probe_congr (the odd attempt depends only on the probe drawn, not on the probe family), a private cantorZassenhausOddAttemptWith_success_aux (core technical lemma handling the case where two roots fall into different Euler buckets), and the main public theorem cantorZassenhausOddAttemptWith_success_of_bucket_separated (if a probe's oddCZBucket separates two distinct roots of g, then the attempt succeeds, producing some children). No sorry or admit are present.
CompPoly/Univariate/Roots/LasVegas/OddBucket.lean: Adds the OddCZBucket inductive type (constructors zero, square, nonsquare) and the oddCZBucket function that classifies a field element x by checking x == 0 and x ^ ((q-1)/2) == 1. Three accompanying theorems (oddCZBucket_eq_zero_iff, oddCZBucket_eq_square_iff, oddCZBucket_eq_nonsquare_iff) provide equivalences characterizing when each bucket is hit. The file is intentionally kept free of PMF and measure-theory imports so it can be shared by both the deterministic correctness and the probability surfaces of the odd-field Cantor‑Zassenhaus splitting.
CompPoly/Univariate/Roots/LasVegas/Probability.lean: Added CompPoly/Univariate/Roots/LasVegas/Probability.lean as a public import facade for seven probability-theory modules: Basic (event probabilities, uniform enumeration models), Uniform (uniform field-element and probe distributions), OddBuckets (Euler criterion bridge), OddTrial (Cantor–Zassenhaus half-success theorem), EvenTrace (trace-fiber counting and half-success), Repeated (repeated-trial geometric bounds), and Recursive (recursive fallback binomial-tail bound). This file is purely structural and contains no theorems or sorries; it re-exports the submodules that model the idealized uniform probe distributions underpinning the deterministic, executable root splitter.
CompPoly/Univariate/Roots/LasVegas/Probability/Basic.lean: Adds probability-side vocabulary for the Las Vegas root splitter: UniformFieldEnumeration (injective enumeration with size equal to q) and OddUniformFieldModel (q odd and equal to field cardinality), TrialResult inductive type with IsSuccess, children, and allFailed predicates, and noncomputable eventProbability, trialSuccessProbability. Also adds three theorems: trialFailureProbability_eq_failed_mass (failure probability equals PMF mass of failed outcome), trialSuccessProbability_add_failed_mass (success probability plus failed mass sum to 1), and trialFailureProbability_le_half_of_success (failure probability ≤ 1/2 when success probability ≥ 1/2). No sorry or admit appear.
CompPoly/Univariate/Roots/LasVegas/Probability/EvenTrace.lean: This new file EvenTrace.lean adds the probability analysis for the characteristic-two trace splitting branch of the Las Vegas root-finding algorithm. It defines tracePowerSum_mul_self (showing trace power sums are idempotent over binary fields), tracePowerSum_eq_zero_or_one (trace power sums only take values 0 or 1), traceFiberPoly (a polynomial whose roots form a trace fiber) with its evaluation and nat-degree properties, and card_tracePowerSum_fiber_le (each trace fiber has at most half the field). The file then proves tracePowerSum_pair_separated_probability_ge_half (two independent uniform field values land in different trace fibers with probability ≥ 1/2), defines the EvenTraceUniformFieldModel structure capturing the required field/context constraints, and defines evenTraceTrialPMF (one trace split trial under uniform probes). Three main success theorems follow: evenTraceTrial_success_probability_ge_half_of_two_le and evenTraceTrial_success_probability_ge_half (each trial succeeds with probability ≥ 1/2 given appropriate hypotheses), and repeatedEvenTraceTrialsPMF with fallbackAfterEvenTraceAttemptsProbability for modeling repeated trials. The lemma fallbackAfterEvenTraceAttemptsProbability_succ gives a recurrence for fallback probability, and fallbackAfterEvenTraceAttempts_probability_le_geometric along with _of_uniformProbe show fallback probability is bounded by (2⁻¹)^attempts. Finally, tryEvenTraceSplitAttemptsWith_uniformTable_none_le_geometric bridges to the executable retry loop, proving that exhausting all attempts has probability at most `(2⁻¹)^attempts.
CompPoly/Univariate/Roots/LasVegas/Probability/OddBuckets.lean: This new file OddBuckets.lean collects theorems about the deterministic Euler bucket classifier oddCZBucket for odd finite fields. It adds three private helper lemmas: two_le_q_of_card_eq (shows 2 ≤ q from the field cardinality), ringChar_ne_two_of_odd_card (the ring characteristic is not 2 when the order is odd), and pow_half_eq_one_or_neg_one (for a nonzero x, x^((q-1)/2) is either 1 or -1). The file then proves the public theorems oddCZBucket_eq_square_iff_isSquare and oddCZBucket_eq_nonsquare_iff_pow_eq_neg_one, which relate memberships in the square and nonsquare buckets to being a nonzero square and to the power equaling -1, respectively. It also proves card_oddCZBucket_zero (the zero bucket contains exactly one element) and the theorems card_oddCZBucket_square and card_oddCZBucket_nonsquare (each of the square and nonsquare buckets has size (q-1)/2). Finally, it proves oddCZBucket_pair_separated_probability_ge_half, which uses a uniform-pair separation lemma to show that two independent uniform field elements land in different Euler buckets with probability at least 1/2. No sorry or admit are present in the diff.
CompPoly/Univariate/Roots/LasVegas/Probability/OddTrial.lean: This new file introduces the probability framework for a single odd-field Cantor-Zassenhaus trial under uniform probes. It defines the probability-facing root-product model RootProductProbabilityInput (nonzero, splits over X^q - X, squarefree, roots-card = degree) and the trial PMF oddSplitTrialPMF, together with the validity theorem oddSplitTrialPMF_support_success_valid. The half‑success model OddSplitTrialHalfSuccessModel is established by the central result oddSplitTrial_success_probability_ge_half_of_two_le (and corollaries _linear and _half), showing that for a squarefree finite‑field root product with HasTwoDistinctRoots and odd field cardinality, uniform probes yield success probability at least 1/2; adapter theorems finiteFieldRootProductWith_rootProductProbabilityInput and rootProductProbabilityInput_of_lasVegasSplitterInput connect the concrete runtime root‑product construction to this model.
CompPoly/Univariate/Roots/LasVegas/Probability/Recursive.lean: This new file formalizes the recursive fallback analysis for the Las Vegas splitting algorithm. It defines the binomial-tail bound binomialFallbackTail and the model predicate RecursiveFallbackProbabilityModel, then builds the multi-factor splitting process recursiveSplitProcessPMF that records which factors fall back to enumeration. The key theorem recursiveSplitProcessPMF_fallback_probability_le_binomialTail proves that the fallback probability is bounded by the binomial tail under the assumptions that each per-factor trial succeeds with probability at least 1/2 and successful splits satisfy IsSplitStep. The file then instantiates this framework for the odd-characteristic branch (recursiveOddSplitProcessPMF), the even-trace branch (recursiveEvenTraceSplitProcessPMF), and the full Las Vegas backend (lasVegasRecursiveSplitProcessPMF), culminating in the headline theorem finiteFieldRootProductWith_lasVegas_fallback_probability_le_binomialTail. It also includes supporting lemmas relating trial outcome support to IsSplitStep for each branch, and the LasVegasUniformFieldModel inductive type that packages the required field cardinality and characteristic case.
CompPoly/Univariate/Roots/LasVegas/Probability/Repeated.lean: This new file introduces repeatedOddSplitTrialsPMF, fallbackAfterOddAttemptsProbability, and a family of theorems establishing that, when each odd-field trial succeeds with probability at least 1/2, the probability of reaching fallback after attempts trials is at most 2⁻ᵃᵗᵗᵉᵐᵖᵗˢ. It then connects this bound to the executable tryOddSplitAttemptsWith via tryOddSplitAttemptsWith_uniformTable_none_le_geometric and generalizes to the table‑driven recursors recursiveSplitWithTables, recursiveOddSplitWithTables, and lasVegasSplitWithTables. The main results (recursiveSplitWithTables_fallback_probability_le_binomialTail and lasVegasSplitWithTables_fallback_probability_le_binomialTail) prove that the deterministic Las Vegas backend, supplied with one independently sampled uniform probe table per processed factor, reaches exhaustive enumeration fallback with probability at most the binomial tail 2⁻ᵃᵗᵗᵉᵐᵖᵗˢ * ∑ⱼ₌₀ᵈ⁻² C(attempts, j) for any finite field (odd or binary with trace metadata). No sorry or admit appear in the diff.
CompPoly/Univariate/Roots/LasVegas/Probability/Uniform.lean: This new file Uniform.lean defines a hierarchy of uniform probability distributions for the Las Vegas root-finding project. It introduces uniformFieldIndexPMF and uniformFieldElementPMF for sampling field elements via a lazy enumeration, uniformCoefficientArrayPMF for generating independent uniform coefficient arrays of arbitrary length, and uniformProbePMF as the pushforward of coefficient arrays to CPolynomial via CPolynomial.ofArray. The file proves that under a UniformFieldEnumeration, every field element has probability 1/q (uniformFieldElementPMF_apply), that uniform probes have degree below the coefficient count (uniformProbePMF_support_natDegree_lt), and the central pair-evaluation uniformity result (uniformProbePMF_eval_pair_apply): for any a ≠ b and coefficientCount ≥ 2, the probability that a probe evaluates to a prescribed pair (x, y) is q⁻¹ * q⁻¹. This theorem is extended to uniformProbePMF_map_eval_pair, showing the evaluation pair map pushes forward to two independent uniform field elements. Finally, uniformPair_separated_probability_ge_half_of_fiber_card_le gives a lower bound on the probability that a classifier separates two independent uniform field values, under a fiber-cardinality condition. All definitions are noncomputable and the file contains no sorry or admit.
CompPoly/Univariate/Roots/Shoup.lean: This new file serves as the public-facing module for the Shoup-style small-characteristic root splitter, exposing the three submodules: CompPoly.Univariate.Roots.Shoup.Basic, CompPoly.Univariate.Roots.Shoup.Correctness, and CompPoly.Univariate.Roots.Shoup.FrobeniusLinear. It uses the @[expose] attribute and a public section to make all declarations from those submodules available to consumers, providing a clean entry point for the Shoup trace splitting API.
CompPoly/Univariate/Roots/Shoup/Basic.lean: Summary unavailable — AI generation failed.
CompPoly/Univariate/Roots/Shoup/Correctness.lean: This file provides the correctness surface for the Shoup-style trace-splitting algorithm. It adds and proves several key theorems: eval_shoupModularXPowerWith_eq_pow and eval_traceCoordinatePolynomialWith relate evaluations of modular power and trace-coordinate polynomials to field arithmetic; smallPrimeTraceContext_charP derives the field's characteristic; traceValue_sub and traceValue_mul_sub_eq_zero_of_eq establish additivity and zero-trace properties for the trace value; and eq_of_traceValue_eq_on_basis shows that matching traces on a separating basis forces equality of field elements. The file then proves the core algorithmic lemmas shoup_gcdBucket_root and shoup_gcdBucket_root_iff connecting Gcd buckets with root-preservation and the trace-bucket condition. A series of private theorems (shoupRefineBaseConstants_root, shoupRefineBaseConstants_dvd, shoupRefineFactorWith_root, shoupRefineFactorsWith_root, shoupRefineBasisWith_root, and corresponding *_dvd and *_rootsAgreeOn variants) establish the correctness of the refinement loop over constants, factors, and the basis. The top-level theorems shoupSplitCandidatesWith_root, shoupSplitCandidatesWith_dvd_input, shoupSplitCandidatesWith_root_unique, and shoupSplitCandidatesWith_valid_factor_represented guarantee that the candidate set covers every root, divides the input polynomial, has unique roots, and outputs represented linear factors. Finally, shoupSplitLinearFactorsWith_complete and the construction of shoupLinearFactorProductSplitterWith and shoupLinearFactorProductSplitter adapt these results to the generic LinearFactorProductSplitter interface, and finiteFieldRootProductWith_dvd_frobenius proves that the root product divides the Frobenius polynomial via a modular-Gcd bridge. No sorry or admit statements appear in the diff.
CompPoly/Univariate/Roots/Shoup/FrobeniusLinear.lean: This new file introduces theorem isRepresentedLinearFactor_of_dvd_frobenius_unique_root, which establishes that a nonzero factor of X^q - X over GF(q) with exactly one root in the field is necessarily a represented nonconstant linear factor. This result serves as the field-theoretic bridge for the Shoup trace splitter.
ROADMAP.md: The ROADMAP.md file was updated to mark two previously in-progress items as completed and to add one new future work item. Specifically, the in-progress status indicator for "Splitting strategies for fields with no smooth refinement schedule" was replaced with a completed checkmark, and two new bullet points were added under that item to confirm the implementation of Shoup-style small-characteristic trace splitting (Roots/Shoup/) and a bounded Las Vegas Cantor–Zassenhaus (Roots/LasVegas/) with odd-char and char-2 trace branches and probability proofs. Additionally, a new in-progress future work item was added for "Named high-width binary-tower SmallPrimeTraceContext instances (32/64) and optional GF(2^{48})/GF(2^{72}) carriers for production char-2 benches".
docs/wiki/coding-theory.md: This documentation update expands the coding-theory.md wiki entry to cover two new root-finding backends (Shoup/ and LasVegas/) alongside the existing SmoothSubgroup/ backend, each with a description of the algorithm and a table explaining when to use which backend. It adds concrete coverage details for ZMod odd primes, ZMod 2, and binary-tower level 0, notes that larger Tower levels for char-2 Shoup contexts are not yet packaged, and adds references for the von zur Gathen–Shoup paper and the Cantor–Zassenhaus algorithm. The file also updates the
tests/CompPolyTests.lean: Two new public imports have been added to the module: CompPolyTests.Univariate.Roots.LasVegas and CompPolyTests.Univariate.Roots.Shoup. These imports expose new test files covering Las Vegas and Shoup algorithms for univariate polynomial roots, expanding the test coverage in the CompPolyTests suite.
tests/CompPolyTests/Univariate/Roots/LasVegas.lean: Added tests/CompPolyTests/Univariate/Roots/LasVegas.lean, a new test file providing deterministic probe coverage for the Las Vegas univariate root-finding algorithm over finite fields of characteristic 5, 11, and 2. The file defines field contexts (f5Ctx, f11TraceCtx, f2TraceCtx), enumerations, probe families (xProbe, constantOneProbe, failThenXProbe, duplicateQuotientProbe, etc.), and splitter configurations (lvSplitter, lvTraceSplitter, lvNoTraceSplitter) and exercises them via #guard assertions on immediate splitting, fallback behavior, repeated roots, public root extraction, and trace-based splitting for characteristic two.
tests/CompPolyTests/Univariate/Roots/Shoup.lean: This new test file adds executable coverage for the Shoup-based rootsInFiniteField algorithm over two fields of cardinality 2: F2 = ZMod 2 and BT0 (the degree‑1 concrete binary tower). For each field it constructs a SmallPrimeTraceContext, derives a LinearFactorProductSplitter via shoupLinearFactorProductSplitter, and then tests root extraction on polynomials representing no roots, all roots, repeated roots, partial roots, and a zero‑only root. Each test uses #guard to assert the expected root set (e.g., allRootsOut contains both 0 and 1 and has size 2). The file also includes the theorem bt0_card establishing that Nat.card BT0 = 2 via the concrete tower’s fieldFintypeCard. No sorry or admit appear.

Last updated: 2026-08-10 19:44 UTC.

dhsorens · 2026-08-07T14:50:05Z

Stack child: #291 (approximant + hybrid GS interpolation) targets this branch.

github-actions · 2026-08-07T14:51:49Z

Build Timing Report

Commit: 527a505
Message: Merge 11b1e3b into a6adbd9
Ref: re-land/roots-shoup-lasvegas
Comparison baseline: 04f5d8a from the previous successful PR update.
Measured on ubuntu-latest with /usr/bin/time -p.
Commands: library build (warm) lake build.
Clean build was skipped (warm/incremental CI; no toolchain or lake-manifest change). Runs automatically when lean-toolchain or lake-manifest.json changes, or via Actions → Lean Action CI → Run workflow with clean_build.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	296.73	-	-	-
Library build (warm)	1.34	7.38	+6.04	exit 1
Test path	35.13	-	-	-

Incremental Rebuild Signal

Warm-only run: default CI reuses cached oleans and rebuilds dirty modules only. No same-job clean:warm ratio.

Slowest Current Build Files (warm library build)

Showing 3 slowest current targets from the warm library build log, with comparison against the baseline clean build log when available.

Current (s)	Baseline (s)	Delta (s)	Path
1.90	3.70	-1.80	`CompPoly/Univariate/Roots/Shoup/Basic.lean`
1.60	2.50	-0.90	`CompPoly/Univariate/Roots/LasVegas/Basic.lean`
0.77	1.60	-0.83	`CompPoly/Univariate/Roots/LasVegas/OddBucket.lean`

The approximant/hybrid stack elaborated 70 declarations with overlapping instance parameters. `main` and #290 are warning-free, so this was a regression against a clean baseline and against docs/wiki/typeclass-minimization.md. Two distinct causes: - 63x `[Field F]` with a redundant `[Nontrivial F]`, from eight `variable` lines carrying both. Removed the redundant binder and the matching entries in the dependent `omit ... in` lines. - 7x `[Field F]` with a redundant `[Zero F]`, on declarations sitting inside a `variable ... [Field F]` scope. This is the harmful case: Lean reports the two can infer conflicting `Zero F`, an instance diamond. Removed `[Zero F]` from the six `ModularEquation` accessors and from `pmBasisFuel`. The `[Zero F]` on the `ModularEquation` and `AdaptiveSolveState` structures is kept: those rebind `F` themselves, do not overlap, and are correct typeclass minimization. No signature is weakened. Every affected declaration already carried `[Field F]` through the enclosing `variable`, so the removed binders were duplicates rather than assumptions. Verified: lake build (0 warnings, 0 errors), lake test, lint-style, update-lib/check-imports, check-docs-integrity.

Re-land olympichek's Shoup trace splitter and bounded Las Vegas Cantor–Zassenhaus stack from #253/#254 onto current main (module system, Lean 4.32). Both implement LinearFactorProductSplitter for fields without a smooth multiplicative-subgroup schedule. - Roots/Shoup: small-char trace coordinates [vzGS92] with correctness - Roots/LasVegas: odd CZ + char-2 trace branches, ProbeFamily, probability - Tests on ZMod 2/5/11 and binary-tower level 0 (Tower integration path) - Docs/ROADMAP: close the non-smooth splitter gap; note high-width Tower SmallPrimeTraceContext instances as follow-up Port fixes for open-friendly CPolynomial APIs and module-system proof adjustments. No parallel Binary/Extension field stack in this PR. Co-authored-by: Derek Sorensen <d@dhsorens.com>

Re-land olympichek's approximant-basis and hybrid Guruswami-Sudan interpolation backends from #255 onto the roots re-land stack (#290). - PolynomialMatrix.Approximant: PM-Basis, modular key equations, partial linearization, with soundness/completeness - GS ApproximantBasis + Hybrid (budgeted Lee fallback) as GSInterpContext - WitnessDivisibility quasi-linear multiplicity check - Named KoalaBear contexts in Implementations; matrix ops/Strassen helpers - Module-system port; shortened ApproximantBasis leaf paths for lint - Docs/ROADMAP: four interpolation backends documented Co-authored-by: Derek Sorensen <d@dhsorens.com>

The approximant/hybrid stack elaborated 70 declarations with overlapping instance parameters. `main` and #290 are warning-free, so this was a regression against a clean baseline and against docs/wiki/typeclass-minimization.md. Two distinct causes: - 63x `[Field F]` with a redundant `[Nontrivial F]`, from eight `variable` lines carrying both. Removed the redundant binder and the matching entries in the dependent `omit ... in` lines. - 7x `[Field F]` with a redundant `[Zero F]`, on declarations sitting inside a `variable ... [Field F]` scope. This is the harmful case: Lean reports the two can infer conflicting `Zero F`, an instance diamond. Removed `[Zero F]` from the six `ModularEquation` accessors and from `pmBasisFuel`. The `[Zero F]` on the `ModularEquation` and `AdaptiveSolveState` structures is kept: those rebind `F` themselves, do not overlap, and are correct typeclass minimization. No signature is weakened. Every affected declaration already carried `[Field F]` through the enclosing `variable`, so the removed binders were duplicates rather than assumptions. Verified: lake build (0 warnings, 0 errors), lake test, lint-style, update-lib/check-imports, check-docs-integrity.

This was referenced Aug 7, 2026

feat(univariate): Shoup's trace splitter root search #253

Open

feat(univariate): randomized Cantor-Zassenhaus root search #254

Open

dhsorens mentioned this pull request Aug 7, 2026

feat(bivariate): approximant-basis and hybrid GS interpolation #291

Open

5 tasks

dhsorens mentioned this pull request Aug 7, 2026

feat(bivariate): approximant-basis and hybrid interpolation for GS decoder #255

Open

dhsorens force-pushed the re-land/roots-shoup-lasvegas branch from 04f5d8a to 11b1e3b Compare August 10, 2026 19:41

Navigation Menu

Uh oh!

feat(univariate): Shoup and Las Vegas root-search backends - #290

feat(univariate): Shoup and Las Vegas root-search backends#290
dhsorens wants to merge 1 commit into
mainfrom
re-land/roots-shoup-lasvegas

dhsorens commented Aug 7, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Aug 7, 2026 •

edited

Loading

Uh oh!

dhsorens commented Aug 7, 2026

Uh oh!

github-actions Bot commented Aug 7, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

dhsorens commented Aug 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Attribution

What we deliberately did not land

Idiom notes

Supersedes

Test plan

Uh oh!

github-actions Bot commented Aug 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

dhsorens commented Aug 7, 2026

Uh oh!

github-actions Bot commented Aug 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Build Timing Report

Incremental Rebuild Signal

Slowest Current Build Files (warm library build)

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

dhsorens commented Aug 7, 2026 •

edited

Loading

github-actions Bot commented Aug 7, 2026 •

edited

Loading

github-actions Bot commented Aug 7, 2026 •

edited

Loading