chore: HexRealRootsMathlib scaffolding review and phase bumps

conformance/HexRealRootsMathlib/Conformance.lean

@@ -20,6 +20,24 @@ hand-derived root-multiset computation proven as a theorem — and the correspon
 ence theorem certifies they agree.
 Mode: always for core.
 
+Covered operations:
+* `Hex.rootCount`, the executable real-root count, tied to the noncomputable
+  Mathlib count `(toPolyℝ p).roots.card` by `rootCount_eq_card_roots`.
+
+Covered properties:
+* `rootCount p = (toPolyℝ p).roots.card`, the root-count correspondence,
+  instantiated per fixture (executable side `#guard`ed, Mathlib side proven as a
+  theorem from an independent factorisation).
+* the full formal tie on `x - 5`: `Hex.rootCount = 1` derived through
+  `rootCount_eq_card_roots` and `squareFreeRat_iff`, not read off evaluation.
+
+Covered edge cases:
+* degree-0 nonzero constant (`const7 = 7`), below the correspondence theorem's
+  positive-degree hypothesis: no roots, executable count `0`.
+* a polynomial with no real roots (`quadNone = x^2 + 1`): count `0`.
+* a polynomial with several distinct real roots (`cubicTriple = x^3 - x`):
+  count `3`.
+
 Because Mathlib root counts are noncomputable, the checks are **theorems**, not
 `#guard`s of the root multiset. For each committed fixture:
 

libraries.yml

@@ -523,7 +523,7 @@ libraries:
   HexRealRootsMathlib:
     deps: [HexRealRoots, HexPolyZMathlib]
     mathlib: true
-    done_through: 1
+    done_through: 3
     status: active
   HexRCF:
     deps: [HexRealRoots, HexRealRootsMathlib, HexPolyZ, HexPolyZMathlib]

status/hex-real-roots-mathlib.scaffolding-reviewed

@@ -0,0 +1,5 @@
+Reviewer-agent Phase 2 skeptical review of HexRealRootsMathlib, read against SPEC/Libraries/hex-real-roots-mathlib.md by an agent distinct from the authors. Every file was read (SturmChainDefs, SturmTheorem, Hadamard, Discr, Separation, ChainCorrespond, Isolations, Drivers, SimpleRealRoot, TwoCircle, the umbrella, and the conformance module). Every SPEC theorem is present with faithful, non-vacuous content: IsSturmChain / sturmVar (SturmChainDefs), sturm_half_open / sturm_line (SturmTheorem), sturmChain_isSturmChain / sturmVarAt_eq / squareFreeRat_iff / sturmCount_eq_card_roots / rootCount_eq_card_roots / sepPrec_separates' (ChainCorrespond), rootBound_bounds_roots / sepPrec_separates (Separation), exists_unique_root / RealRootIsolations.isolates (Isolations), refine1_isolates_same / isolateSturm?_isSome / isolate?_isSome (Drivers), overlaps_iff_same_root / SimpleRealRoot.toReal / toReal_isRoot / toReal_injective / sameRoot_iff (SimpleRealRoot), and the deferred isolateDescartes?_isSome (TwoCircle).
+
+Flagged hypothesis adjustments, each documented in the relevant docstring and sound: (1) p ≠ 0 shapes added where SquareFreeRat alone is unsound because SquareFreeRat 0 holds vacuously while the driver returns none / complete forces zero isolations (isolate?_isSome, isolateSturm?_isSome, RealRootIsolations.isolates, sepPrec_separates'); (2) the executable chain head is primitivePart p, so sturmChain_isSturmChain is stated at toPolyℝ (primitivePart p) rather than toPolyℝ p, the SPEC form being unsatisfiable as written, with identical roots and hence unchanged counting consequences; (3) 1 ≤ degree retained on the correspondence theorems (sturmChain_isSturmChain, sturmCount_eq_card_roots, rootCount_eq_card_roots) since the primitive-part chain requires positive degree.
+
+The single intentional sorry is isolateDescartes?_isSome in TwoCircle.lean, the SPEC-sanctioned Descartes-termination deferral behind the Obreshkoff two-circle prerequisite; verified to be the only sorry in the library. #print axioms is clean of sorryAx on isolate?_isSome, sepPrec_separates', Sturm.sturm_half_open, and overlaps_iff_same_root (each depends only on propext / Classical.choice / Quot.sound); isolateDescartes?_isSome carries sorryAx as expected. No axioms, no native_decide, no data-level placeholders, no wrong-shape scaffolds, no meta-commentary progress notes. Downstream API hex-rcf cites (isolate?_isSome, sturmChain_isSturmChain, sturmCount_eq_card_roots, RealRootIsolations.isolates) is present. lake build HexRealRootsMathlib HexConformance is green.