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

[olympichek]

Overview

This PR adds Shoup's deterministic univariate root-search algorithm in addition to the current smooth-subgroup algorithm.

This PR includes:

• The Shoup root-search backend and its Frobenius-linear helper layer.
• Correctness proofs showing that the Shoup backend satisfies the same finite-field root-search contract as the smooth backend.
• Shared binary-field carrier infrastructure for $\mathrm{GF}(2^{32})$, $\mathrm{GF}(2^{48})$, $\mathrm{GF}(2^{64})$, and $\mathrm{GF}(2^{72})$.
• Binary-field root contexts and tests that can be reused by later root-search backends.
• Documentation updates for the new binary-field modules.
• Univariate root tests and binary-field regression tests for the new concrete field contexts.
• Benchmarks comparing Shoup and smooth-subgroup algorithms on $\mathrm{GF}(2^{32})$, $\mathrm{GF}(2^{48})$, $\mathrm{GF}(2^{64})$, and $\mathrm{GF}(2^{72})$

[dhsorens]

Maintainer re-land in progress. The original author is no longer available; we are porting this work onto current main (module system, Lean 4.32, Tower/Binary integration rather than a parallel GF2_* stack).

Bookkeeping: #254 is the roots source of truth (it already contains Shoup + more). We will not merge this PR as-is. When the re-land PR merges, this PR will be closed as superseded. Attribution to Valerii Huhnin (olympichek) is retained on ported modules.

[dhsorens]

Re-land PR opened: #290 (includes Shoup from this PR as part of the #254 stack). This PR can close as superseded when #290 merges.