feat(real-roots-mathlib): checked root counts and a simpler Sturm API

[kim-em]

This is the Hex side of Mathlib #43512, where real_root_count removes the 61-line hand-written calculus argument for the real roots of X ^ 5 - 4 * X + 2, reducing the Abel–Ruffini archive file from 175 to 127 lines.

Add by real_root_count and the term form real_root_count p to HexRealRootsMathlib. They certify the number of distinct real roots of a closed, squarefree integer-coefficient polynomial over ℚ of positive degree. Hex proposes a signed remainder chain; ordinary Lean proofs check the polynomial identities, positive factors, derivative relation, and variation count.

example : Fintype.card ((X ^ 5 - 4 * X + 2 : ℚ[X]).rootSet ℝ) = 3 := by
  real_root_count

This carries the mathematical and elaborator improvements from Mathlib #43512 back into the Hex source of truth:

• Simplify the Sturm-chain predicate and proof helpers. State the counting theorems using natural-number addition, weaken squarefreeness to roots.Nodup, and permit equal interval endpoints.
• Add certificates over Mathlib polynomials, with separate chain-validity and separability theorems and a root-set cardinality theorem over any commutative coefficient ring with an algebra map into ℝ.
• Improve the shared polynomial parser with binary exponentiation, preserve expressions and local contexts during elaboration, reuse Hex.DensePoly.divMod, and add focused diagnostics and regression tests.
• Update executable-chain correspondence, literal certificates, and the real-closed-field replay clients to the simpler API. Existing root-isolation clients continue to compile.

scripts/check_sturm_sync.py /path/to/mathlib compares the five library modules and both test modules after translating module paths, namespaces, and documentation markup. The README documents the new entry point, and the release test target includes both new test modules. The companion copies can become re-exports once Hex's Mathlib pin contains the development.

Validation: full lake build; lake build HexReleaseTests, including root-count, Sturm endpoint, and existing isolation regression tests; release-manifest validation; the seven-module sync check; and git diff --check. The monorepo retains its pre-existing sorry warnings in unrelated multivariate libraries and line-length warnings in the manual; this change introduces none. The corresponding Mathlib theorem and certificate axiom audits report only propext, Classical.choice, and Quot.sound.

HexArith and HexModArith’s C build recipes set TMPDIR to the object directory for each compiler process. This supports Mathlib’s Landlock sandbox, which allows writes inside .lake but forbids /tmp, including when cc is a compiler wrapper. Release sync copies the selected recipes from the monorepo Lake file; its tests check preservation of the mirror skeleton, idempotence, and rejection of missing or ambiguous helpers. All three affected C objects were rebuilt under Landlock with /tmp unwritable. HexArith also drops two unused private bv_decide lemmas whose external solver had the same temporary-file problem; the general Newton/Hensel proof already establishes every refinement used by the public theorem.

The performance freshness checks now parse the Lake file by declaration and mechanically compare only the build configuration reachable from each measured executable. Regression tests ensure that changes to the nauty helpers or cactus target still invalidate graph-isomorphism measurements, while unrelated library and test targets do not. The full post-merge build completes successfully (11,223 jobs), and the factorization freshness, graph-isomorphism freshness, per-node fit, and committed-figure checks pass.