From d64f2e1a0405cddd5ddc5e75dea835a4ed64f266 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 11 Jul 2026 19:50:09 +0000 Subject: [PATCH] chore(real-roots-mathlib): Phase 2 review token and phase bumps Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01NUB5EStJpJ8CPqMkNw7Qjz --- .../HexRealRootsMathlib/Conformance.lean | 18 ++++++++++++++++++ libraries.yml | 2 +- ...hex-real-roots-mathlib.scaffolding-reviewed | 5 +++++ 3 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 status/hex-real-roots-mathlib.scaffolding-reviewed diff --git a/conformance/HexRealRootsMathlib/Conformance.lean b/conformance/HexRealRootsMathlib/Conformance.lean index b04cc0d3a..9ab5c5fda 100644 --- a/conformance/HexRealRootsMathlib/Conformance.lean +++ b/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: diff --git a/libraries.yml b/libraries.yml index 75c886192..5883ae632 100644 --- a/libraries.yml +++ b/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] diff --git a/status/hex-real-roots-mathlib.scaffolding-reviewed b/status/hex-real-roots-mathlib.scaffolding-reviewed new file mode 100644 index 000000000..fa920ebde --- /dev/null +++ b/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.