feat: isolation semantics and driver completeness

[kim-em]

This PR add HexRealRootsMathlib/Isolations.lean and HexRealRootsMathlib/Drivers.lean, the isolation-semantics and driver-completeness theorems of the hex-real-roots companion, all sorry-free. RealRootIsolation.exists_unique_root shows a certified isolation names exactly one real root of toPolyℝ p in its half-open interval; RealRootIsolations.isolates shows a complete run names every real root exactly once (injective root map plus the rootCount cardinality); refine1_isolates_same shows one bisection refinement preserves the isolated root and halves the width exactly, with the fallback branch unreachable; isolateSturm?_isSome and isolate?_isSome show the Sturm engine and the top-level driver succeed on nonzero squarefree input, via the worklist-drain induction sturmVisit_spec (an interval no wider than 2^(-sepPrec p) holds at most one root by sepPrec_separates', so the depth budget always suffices).

Three SPEC statements gain an explicit p ≠ 0 hypothesis (RealRootIsolations.isolates, isolateSturm?_isSome, isolate?_isSome): the SquareFreeRat p-only forms are unsound because SquareFreeRat 0 holds while all three fail at p = 0 (every real is a root of the zero polynomial, but complete forces zero isolations and the engine returns none). Same precedent as #8738/#8741/#8745. The nonzero-constant case is genuinely covered: the driver's degree? = some 0 branch certifies through the empty chain (rootCount = 0), and isolates is vacuous there, so downstream consumers (hex-rcf calling isolation on squareFreeCore output) need no degree case split. exists_unique_root keeps the SPEC signature verbatim by deriving positive degree from its count_one certificate (a Sturm count of 1 forces a nonempty chain).

One correctness question got resolved along the way: the engine's completeness check compares the sturmVisit totals seeded at ±rootBound p against rootCount p computed from ±∞ leading-coefficient variations, and one might worry a chain element (a remainder of (p, p'), whose roots rootBound p does not bound) could break the match. There is no gap: sturmVar_neg_pos_sub proves the ±rootBound variation difference equals rootCount p outright, because sturmCount_eq_card_roots is a statement about p's roots only — the chain elements' own zeros are already absorbed by Sturm's theorem, and Cauchy's bound puts all of p's roots inside (-R, R].

🤖 Prepared with Claude Code