chore: HexRealRootsMathlib scaffolding review and phase bumps

[kim-em]

This PR records the Phase 2 skeptical review of HexRealRootsMathlib and advances its phase counter to 3. A reviewer agent distinct from the authors read every file of the library against SPEC/Libraries/hex-real-roots-mathlib.md and confirmed every SPEC theorem is present with faithful, non-vacuous content across SturmChainDefs, SturmTheorem, ChainCorrespond, Separation, Isolations, Drivers, and SimpleRealRoot, with the single SPEC-sanctioned sorry (isolateDescartes?_isSome, deferred behind the Obreshkoff two-circle theorem) verified to be the only one. The review confirms the documented hypothesis adjustments are sound: p ≠ 0 shapes where SquareFreeRat alone is vacuous, the primitivePart head on the chain correspondence, and the 1 ≤ degree hypotheses retained on the count correspondences. #print axioms is clean of sorryAx on isolate?_isSome, sepPrec_separates', Sturm.sturm_half_open, and overlaps_iff_same_root, each depending only on propext, Classical.choice, and Quot.sound.

The Phase 3 conformance module already exists at conformance/HexRealRootsMathlib/Conformance.lean and is reached by the HexConformance globs; its oracle is the proven correspondence theorems themselves, in always mode. This PR brings its docstring into literal compliance with the per-library module contract by adding the explicit Covered operations, Covered properties, and Covered edge cases lists, then bumps libraries.yml done_through from 1 to 3, records the status/hex-real-roots-mathlib.scaffolding-reviewed attestation, and leaves lake build HexRealRootsMathlib HexConformance green with check_dag and check_phase4 passing.

🤖 Prepared with Claude Code