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

[kim-em]

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.