refactor(real-roots-mathlib): use Mathlib list sign variations

[kim-em]

The Sturm development now uses List.signVariations from mathlib PR #43783. Bump Lean and Verso to v4.34.0 and Mathlib to 1cf325a0cf67aca2b04d76b5380ff6a9e410aefa, then synchronize the seven shared library/test modules with mathlib #43512 at 237738a03f8be551ca847d12f8a31d3a7ffe0e6c.

• Replace the duplicate Sturm counters and sign-congruence proofs with the shared list API, including the tactic's integer computation and generated proofs.

• Prove Hex.signVar agrees directly with List.signVariations, use its filter/map/congruence lemmas, and reduce the Descartes bridge to reversal invariance. The computational libraries remain Mathlib-free.

• Adapt the other Mathlib bridges to the bump: polynomial coefficients, power-series derivatives, product inequalities, norm_num, and explicit qualification of Hex's dyadic-to-real names where the new Mathlib name would shadow them.

• Refresh the full 392-input Hex factorization sweep and graph-isomorphism executable/tactic measurements for Lean v4.34.0, retaining timeouts and regenerating the published figures.

API migration

Use List.signVariations and its recursion/congruence lemmas in place of the removed Sturm.signVariations, Sturm.countSignChanges, and their helpers. signVar_eq_list gives the direct integer correspondence; signVar_eq remains the real-cast correspondence. HexRealRootsMathlib.signVariations_reverse now works for any linearly ordered type with zero.

Mathlib is pinned to a commit because the shared list API landed after the v4.34.0 release tag. The existing Hex dyadic conversion definitions and their simp behavior are retained, with explicit names where needed to distinguish them from Mathlib's new definitions.

Validation

• Full lake build, including the aggregate and Verso manual: 14,384 jobs, successful.
• CI's explicit library/benchmark/proof-probe targets (15,268 jobs) and conformance/fixture executable targets (14,413 jobs): successful.
• All HexRealRootsMathlib/*Tests.lean and HexRCF/*Tests.lean regression modules; matrix literal tests.
• Full lake build HexConformance: 13,695 jobs, successful. This also covers the interval experiment modules; remove four omega steps that are redundant after the new simplifications.
• check_sturm_sync.py: all seven modules match mathlib #43512.
• Axiom audit of the Sturm theorem, certificate cardinality, integer sign-variation correspondence, Descartes correspondence, and whole-line root count: only propext, Classical.choice, and Quot.sound.
• Factorization and graph-isomorphism source freshness, all figure-regeneration checks, and the graph per-node exponent check.
• Copyright, file-size, import-DAG, published trust-surface, release-manifest, manual-split, and whitespace checks.