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

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>

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

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>

* fix(roots): adapt Shoup and Las Vegas proofs to Lean 4.33.1

The rebase onto current main left the build failing on module-system exposure
and mathlib drift, not on any mathematical content. All 21 library modules and
3 test modules already carried `module`, `public import` and
`@[expose] public section`; the failures were downstream of main tightening
definition exposure.

- `import all` for the same-package implementation dependencies these proofs
  step through (`Univariate.Basic`, `Modular`, `Raw.Division`, `Raw.Modular`,
  `ToPoly.Core`). `natDegree`, `coeff`, `eval`, `monicNormalize`, `modByMonic`
  and the `Raw` modular kernels live in bare `public section`s, so their bodies
  are opaque downstream and `simp [natDegree]`, `unfold monicNormalize`,
  `change` into the `Raw` layer and `natDegree 0 = 0 := rfl` all stopped
  working. This is the pattern `docs/wiki/module-system.md` prescribes for
  exactly this case.
- Bridge `toPoly 0 = 0` with `toPoly_eq_zero_iff` rather than relying on
  definitional reduction.
- `letI`/`haveI` to `let`/`have` (26 sites) per the `haveILetI` style linter,
  and `Set.mem_setOf_eq` to `Set.mem_ofPred_eq` (32 sites) for the mathlib
  4.32 to 4.33 deprecation.
- Prove the two `ContainsAllFieldElements` obligations with plain `decide` over
  the whole quantifier, matching `tests/.../Roots/Enumeration.lean`. List
  membership decidability now wants `BEq`/`LawfulBEq`, which the previous
  `fin_cases`-then-`decide` shape could not synthesize.

A `natDegree_zero` characterization lemma in `Univariate/Basic.lean` would be
the tidier long-term fix for the last of those; left out to keep this change
inside the PR's own files.

Build, tests, lint, imports, docs integrity and `axiomsweep --check` all pass;
the sweep stays at 0 sorry and 0 non-standard axioms.

---------

Co-authored-by: Valerii Huhnin <olympichek1@gmail.com>