From a93e231f4d820d90ca12cf794649fcd9c6480857 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 11 Jul 2026 19:28:13 +0000 Subject: [PATCH 1/2] feat: root identity, the deferred two-circle statement, and companion conformance MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add HexRealRootsMathlib/SimpleRealRoot.lean (theRoot, overlaps_iff_same_root, SimpleRealRoot.toReal/toReal_isRoot/toReal_injective, sameRoot_iff), HexRealRootsMathlib/TwoCircle.lean (the deferred isolateDescartes?_isSome behind the Obreshkoff two-circle prerequisite — the library's one intentional sorry), and conformance/HexRealRootsMathlib/Conformance.lean (the companion conformance module). Rename the M5 Sturm helpers, bump HexRealRootsMathlib done_through to 1, and wire the two new files into the umbrella. See progress/2026-07-11T19-27-49Z-real-roots-s8-wrapup.md. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01NUB5EStJpJ8CPqMkNw7Qjz --- HexRealRootsMathlib.lean | 24 +- HexRealRootsMathlib/SimpleRealRoot.lean | 270 ++++++++++++++++++ HexRealRootsMathlib/SturmTheorem.lean | 28 +- HexRealRootsMathlib/TwoCircle.lean | 84 ++++++ .../HexRealRootsMathlib/Conformance.lean | 198 +++++++++++++ lakefile.lean | 2 +- libraries.yml | 2 +- ...26-07-11T19-27-49Z-real-roots-s8-wrapup.md | 39 +++ 8 files changed, 622 insertions(+), 25 deletions(-) create mode 100644 HexRealRootsMathlib/SimpleRealRoot.lean create mode 100644 HexRealRootsMathlib/TwoCircle.lean create mode 100644 conformance/HexRealRootsMathlib/Conformance.lean create mode 100644 progress/2026-07-11T19-27-49Z-real-roots-s8-wrapup.md diff --git a/HexRealRootsMathlib.lean b/HexRealRootsMathlib.lean index 8ff199538..50cba80d8 100644 --- a/HexRealRootsMathlib.lean +++ b/HexRealRootsMathlib.lean @@ -14,6 +14,8 @@ public import HexRealRootsMathlib.Separation public import HexRealRootsMathlib.ChainCorrespond public import HexRealRootsMathlib.Isolations public import HexRealRootsMathlib.Drivers +public import HexRealRootsMathlib.SimpleRealRoot +public import HexRealRootsMathlib.TwoCircle public section @@ -21,14 +23,18 @@ public section The `HexRealRootsMathlib` library is the Mathlib companion for the executable real-root isolation library `HexRealRoots`. -This umbrella currently exposes only the **self-contained Sturm slice**: the -zero-skipping sign-variation count `Sturm.sturmVar`, the generalised-chain -predicate `Sturm.IsSturmChain`, and the five-step statement of Sturm's theorem -over `Polynomial ℝ`. The slice is deliberately free of any `HexRealRoots` -dependence, so it can be contributed to Mathlib (which does not yet have -Sturm's theorem) once exercised here. +The **self-contained Sturm slice** — the zero-skipping sign-variation count +`Sturm.sturmVar`, the generalised-chain predicate `Sturm.IsSturmChain`, and the +counting/line forms of Sturm's theorem over `Polynomial ℝ` — is deliberately +free of any `HexRealRoots` dependence, so it can be contributed to Mathlib +(which does not yet have Sturm's theorem) once exercised here. -The executable-correspondence files — connecting `Hex.sturmChain`, -`Hex.sturmCount`, and the isolation drivers to this abstract development, and -the isolation-soundness and driver-completeness theorems — arrive in later PRs. +The executable-correspondence and consequence files build on it: +`ChainCorrespond` connects `Hex.sturmChain`, `Hex.sturmCount`, and `Hex.rootCount` +to the abstract development; `Separation`/`Discr`/`Hadamard` supply the Mahler +separation bound; `Isolations` and `Drivers` prove isolation soundness, run +completeness, driver completeness, and refinement; `SimpleRealRoot` proves the +root-identity theorems (overlap classes are the real roots); and `TwoCircle` +states the single deferred theorem — Descartes-engine termination — behind its +Obreshkoff two-circle prerequisite, the one intentional `sorry` in the library. -/ diff --git a/HexRealRootsMathlib/SimpleRealRoot.lean b/HexRealRootsMathlib/SimpleRealRoot.lean new file mode 100644 index 000000000..84153bab8 --- /dev/null +++ b/HexRealRootsMathlib/SimpleRealRoot.lean @@ -0,0 +1,270 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +module + +public import Mathlib +public import HexRealRootsMathlib.Isolations +public import HexRealRoots.SimpleRealRoot +-- `import all` on `Separation` so `Dyadic.toReal` unfolds in the dyadic-order +-- helpers below, on `Basic` so `DensePoly.degree?_zero_getD` is available when +-- deriving `p ≠ 0` from an isolation's `count_one`, and on `SimpleRealRoot` so +-- the non-`@[expose]` bodies of `SimpleRealRoot` (a `Quot`) and `SimpleRealRoot. +-- mk` unfold — `Quot.lift`/`Quot.ind`/`Quot.sound` need `SimpleRealRoot p` +-- reducible to `Quot Overlaps` here. +import all HexRealRootsMathlib.Separation +import all HexRealRoots.Basic +import all HexRealRoots.SimpleRealRoot + +public section + +/-! +# Root identity: `Overlaps` classes are exactly the real roots + +The executable layer (`HexRealRoots.SimpleRealRoot`) defines `SimpleRealRoot p` +as the `Quot` of `RefinedRealIsolation p` by interval overlap, taking the +quotient with `Quot` (which needs no equivalence proof) because the argument +that `Overlaps` is an equivalence is semantic. This module supplies that +argument: + +* `overlaps_iff_same_root`: two refined isolations overlap iff they name the + same real root. Both intervals have width `≤ 2^{−sepPrec p}`, which is below + `sep(p)/4` (`sepPrec_separates'`); an overlap places a point within + `sep(p)/2` of both roots, forcing them to coincide, and conversely two + isolations of the same root both contain it, so they overlap. +* `SimpleRealRoot.toReal`: the well-defined real value of a root identity, + lifting `theRoot` through the quotient by the forward direction. +* `SimpleRealRoot.toReal_isRoot`, `SimpleRealRoot.toReal_injective`: the lift + lands on genuine roots and is injective (distinct classes name distinct + roots, the backward direction via `Quot.sound`). +* `sameRoot_iff`: the executable boolean `sameRoot` decides equality in + `SimpleRealRoot p`. + +`theRoot hp iso` is the unique real root delivered by +`RealRootIsolation.exists_unique_root` for the isolation underlying `iso`. + +## SPEC signature note + +The SPEC states these with only `SquareFreeRat p`, and that is exactly what +they carry here — no separate `p ≠ 0` hypothesis. Unlike `RealRootIsolations. +isolates` or `isolateSturm?_isSome` (which have no isolation on hand and so +must assume `p ≠ 0`), every theorem here is handed a `RefinedRealIsolation`, +whose underlying `RealRootIsolation` carries `count_one`; that forces positive +degree (`degree_pos_of_count_one`), hence `p ≠ 0`. So the nonzero fact is +derived internally and the statements match the SPEC verbatim. +-/ + +namespace HexRealRootsMathlib + +open Polynomial + +noncomputable section + +variable {p : Hex.ZPoly} + +/-! ### Dyadic-order helpers (real values) -/ + +/-- Dyadic `≤` transfers to the real values. -/ +private theorem toReal_le_toReal {a b : Dyadic} (h : a ≤ b) : + Dyadic.toReal a ≤ Dyadic.toReal b := by + have h2 : a.toRat ≤ b.toRat := Dyadic.toRat_le_toRat_iff.mpr h + unfold Dyadic.toReal; exact_mod_cast h2 + +/-- Failing dyadic `≤` gives the reverse inequality on the real values (the +core `Dyadic` order need not be a `LinearOrder`, so this routes through the +total order on `ℚ` via `toRat`). -/ +private theorem toReal_le_of_not_le {a b : Dyadic} (h : ¬ a ≤ b) : + Dyadic.toReal b ≤ Dyadic.toReal a := by + have h1 : ¬ (a.toRat ≤ b.toRat) := fun hh => h (Dyadic.toRat_le_toRat_iff.mp hh) + have h2 : b.toRat ≤ a.toRat := (not_le.mp h1).le + unfold Dyadic.toReal; exact_mod_cast h2 + +/-- Dyadic `<` coincides with the order of the real values. -/ +private theorem toReal_lt_toReal_iff {a b : Dyadic} : + Dyadic.toReal a < Dyadic.toReal b ↔ a < b := by + unfold Dyadic.toReal + rw [Rat.cast_lt, Dyadic.toRat_lt_toRat_iff] + +/-- `Dyadic.toReal` is subtractive. -/ +private theorem toReal_sub (a b : Dyadic) : + Dyadic.toReal (a - b) = Dyadic.toReal a - Dyadic.toReal b := by + unfold Dyadic.toReal; rw [Dyadic.toRat_sub]; push_cast; ring + +/-- A real root of the real cast is a complex root of the complex cast. -/ +private theorem isRoot_toPolyℂ {r : ℝ} (hr : (toPolyℝ p).IsRoot r) : + (toPolyℂ p).IsRoot (r : ℂ) := by + have hcomp : (algebraMap ℝ ℂ).comp (Int.castRingHom ℝ) = Int.castRingHom ℂ := + RingHom.ext_int _ _ + have hmap : toPolyℂ p = (toPolyℝ p).map (algebraMap ℝ ℂ) := by + show (HexPolyZMathlib.toPolynomial p).map (Int.castRingHom ℂ) + = ((HexPolyZMathlib.toPolynomial p).map (Int.castRingHom ℝ)).map (algebraMap ℝ ℂ) + rw [Polynomial.map_map, hcomp] + rw [hmap] + have h2 : Polynomial.IsRoot ((toPolyℝ p).map (algebraMap ℝ ℂ)) (algebraMap ℝ ℂ r) := hr.map + simpa using h2 + +/-! ### The root of a refined isolation -/ + +/-- The unique real root isolated by a refined isolation, delivered by +`RealRootIsolation.exists_unique_root` for the underlying `RealRootIsolation`. -/ +noncomputable def theRoot (hp : Hex.ZPoly.SquareFreeRat p) + (iso : Hex.RefinedRealIsolation p) : ℝ := + (RealRootIsolation.exists_unique_root hp iso.1).choose + +/-- `theRoot` is a root of `toPolyℝ p`. -/ +theorem theRoot_isRoot (hp : Hex.ZPoly.SquareFreeRat p) (iso : Hex.RefinedRealIsolation p) : + (toPolyℝ p).IsRoot (theRoot hp iso) := + (RealRootIsolation.exists_unique_root hp iso.1).choose_spec.1.1 + +/-- `theRoot` lies strictly above the isolation's lower endpoint. -/ +theorem theRoot_lt (hp : Hex.ZPoly.SquareFreeRat p) (iso : Hex.RefinedRealIsolation p) : + Dyadic.toReal iso.1.interval.lower < theRoot hp iso := + (RealRootIsolation.exists_unique_root hp iso.1).choose_spec.1.2.1 + +/-- `theRoot` lies at or below the isolation's upper endpoint. -/ +theorem theRoot_le (hp : Hex.ZPoly.SquareFreeRat p) (iso : Hex.RefinedRealIsolation p) : + theRoot hp iso ≤ Dyadic.toReal iso.1.interval.upper := + (RealRootIsolation.exists_unique_root hp iso.1).choose_spec.1.2.2 + +/-- The width of a refined isolation, on the real values, is at most +`2^{−sepPrec p}` (the defining property of `RefinedRealIsolation`). -/ +private theorem refined_width (i : Hex.RefinedRealIsolation p) : + Dyadic.toReal i.1.interval.upper - Dyadic.toReal i.1.interval.lower + ≤ (2 : ℝ) ^ (-(Hex.sepPrec p : ℤ)) := by + have h := toReal_le_toReal i.2 + rw [toReal_sub, toReal_twoPow] at h + exact h + +/-! ### `Overlaps` as a real-interval intersection -/ + +/-- `Overlaps` unfolds to a genuine intersection of the half-open real +intervals: `max lower < min upper`. -/ +private theorem overlaps_iff_real (i₁ i₂ : Hex.RefinedRealIsolation p) : + Hex.Overlaps i₁ i₂ ↔ + max (Dyadic.toReal i₁.1.interval.lower) (Dyadic.toReal i₂.1.interval.lower) + < min (Dyadic.toReal i₁.1.interval.upper) (Dyadic.toReal i₂.1.interval.upper) := by + have hmax : max (Dyadic.toReal i₁.1.interval.lower) (Dyadic.toReal i₂.1.interval.lower) + = Dyadic.toReal (if i₁.1.interval.lower ≤ i₂.1.interval.lower + then i₂.1.interval.lower else i₁.1.interval.lower) := by + by_cases h : i₁.1.interval.lower ≤ i₂.1.interval.lower + · rw [if_pos h, max_eq_right (toReal_le_toReal h)] + · rw [if_neg h, max_eq_left (toReal_le_of_not_le h)] + have hmin : min (Dyadic.toReal i₁.1.interval.upper) (Dyadic.toReal i₂.1.interval.upper) + = Dyadic.toReal (if i₁.1.interval.upper ≤ i₂.1.interval.upper + then i₁.1.interval.upper else i₂.1.interval.upper) := by + by_cases h : i₁.1.interval.upper ≤ i₂.1.interval.upper + · rw [if_pos h, min_eq_left (toReal_le_toReal h)] + · rw [if_neg h, min_eq_right (toReal_le_of_not_le h)] + rw [hmax, hmin, toReal_lt_toReal_iff] + exact Iff.rfl + +/-! ### Overlap iff same root -/ + +/-- **`Overlaps` classes are the real roots.** Two refined isolations of `p` +overlap iff they name the same real root of `toPolyℝ p`. + +Forward: both widths are `≤ 2^{−sepPrec p}`, below `sep(p)/4`; an overlap point +sits within one width of each root, so the two roots are less than +`4 · 2^{−sepPrec p}` apart, and `sepPrec_separates'` forces them equal. +Backward: a common root lies in both half-open intervals, so `max lower` (below +the root) is under `min upper` (at or above it). -/ +theorem overlaps_iff_same_root (hp : Hex.ZPoly.SquareFreeRat p) + (i₁ i₂ : Hex.RefinedRealIsolation p) : + Hex.Overlaps i₁ i₂ ↔ theRoot hp i₁ = theRoot hp i₂ := by + constructor + · intro hov + -- `p ≠ 0` is derivable from either isolation's `count_one`. + have hp0 : p ≠ 0 := by + have hdeg := degree_pos_of_count_one i₁.1 + intro hh + rw [hh] at hdeg + simp only [Hex.DensePoly.degree?_zero_getD] at hdeg + omega + by_contra hne + have h1l := theRoot_lt hp i₁ + have h1u := theRoot_le hp i₁ + have h2l := theRoot_lt hp i₂ + have h2u := theRoot_le hp i₂ + have hw1 := refined_width i₁ + have hw2 := refined_width i₂ + have hovr := (overlaps_iff_real i₁ i₂).mp hov + -- `b` is a point common to both intervals: below every upper, above the max lower. + set b := min (Dyadic.toReal i₁.1.interval.upper) (Dyadic.toReal i₂.1.interval.upper) + with hbdef + have hbu1 : b ≤ Dyadic.toReal i₁.1.interval.upper := min_le_left _ _ + have hbu2 : b ≤ Dyadic.toReal i₂.1.interval.upper := min_le_right _ _ + have hbl1 : Dyadic.toReal i₁.1.interval.lower < b := + lt_of_le_of_lt (le_max_left _ _) hovr + have hbl2 : Dyadic.toReal i₂.1.interval.lower < b := + lt_of_le_of_lt (le_max_right _ _) hovr + have hwpos : (0 : ℝ) < (2 : ℝ) ^ (-(Hex.sepPrec p : ℤ)) := by positivity + -- Both roots sit within one width of `b`, so within `2·2^{−sepPrec}` of each other. + have hbound : |theRoot hp i₁ - theRoot hp i₂| < 2 * (2 : ℝ) ^ (-(Hex.sepPrec p : ℤ)) := by + rw [abs_lt] + exact ⟨by linarith, by linarith⟩ + -- Separation forbids two distinct roots being that close. + have hsep := sepPrec_separates' p hp0 hp (theRoot hp i₁ : ℂ) (theRoot hp i₂ : ℂ) + (isRoot_toPolyℂ (theRoot_isRoot hp i₁)) (isRoot_toPolyℂ (theRoot_isRoot hp i₂)) + (fun h => hne (by exact_mod_cast h)) + have hnorm : ‖(theRoot hp i₁ : ℂ) - (theRoot hp i₂ : ℂ)‖ + = |theRoot hp i₁ - theRoot hp i₂| := by + rw [← Complex.ofReal_sub, Complex.norm_real, Real.norm_eq_abs] + rw [hnorm] at hsep + linarith + · intro hsame + rw [overlaps_iff_real] + have h1l := theRoot_lt hp i₁ + have h1u := theRoot_le hp i₁ + have h2l := theRoot_lt hp i₂ + have h2u := theRoot_le hp i₂ + rw [hsame] at h1l h1u + exact lt_of_lt_of_le (max_lt h1l h2l) (le_min h1u h2u) + +/-! ### The quotient `SimpleRealRoot p` -/ + +/-- The real value of a root identity: `theRoot` lifted through the overlap +quotient. Well-defined by the forward direction of `overlaps_iff_same_root`. -/ +noncomputable def _root_.Hex.SimpleRealRoot.toReal (hp : Hex.ZPoly.SquareFreeRat p) : + Hex.SimpleRealRoot p → ℝ := + Quot.lift (theRoot hp) (fun _ _ hab => (overlaps_iff_same_root hp _ _).mp hab) + +/-- The lifted value is a genuine root of `toPolyℝ p`. -/ +theorem _root_.Hex.SimpleRealRoot.toReal_isRoot (hp : Hex.ZPoly.SquareFreeRat p) + (s : Hex.SimpleRealRoot p) : (toPolyℝ p).IsRoot (s.toReal hp) := by + induction s using Quot.ind with + | _ i => exact theRoot_isRoot hp i + +/-- Distinct root identities name distinct reals: `toReal` is injective. The +backward direction of `overlaps_iff_same_root` produces the `Overlaps` witness +that `Quot.sound` needs. -/ +theorem _root_.Hex.SimpleRealRoot.toReal_injective (hp : Hex.ZPoly.SquareFreeRat p) : + Function.Injective (Hex.SimpleRealRoot.toReal (p := p) hp) := by + intro s₁ s₂ h + induction s₁ using Quot.ind with + | _ i₁ => + induction s₂ using Quot.ind with + | _ i₂ => + have hEq : theRoot hp i₁ = theRoot hp i₂ := h + exact Quot.sound ((overlaps_iff_same_root hp i₁ i₂).mpr hEq) + +/-- **`sameRoot` decides equality in `SimpleRealRoot p`.** The executable +boolean overlap test on refined isolations is `true` exactly when they are the +same element of the quotient. -/ +theorem sameRoot_iff (hp : Hex.ZPoly.SquareFreeRat p) (i₁ i₂ : Hex.RefinedRealIsolation p) : + Hex.RefinedRealIsolation.sameRoot i₁ i₂ = true ↔ + Hex.SimpleRealRoot.mk i₁ = Hex.SimpleRealRoot.mk i₂ := by + simp only [Hex.RefinedRealIsolation.sameRoot, decide_eq_true_iff] + constructor + · intro hov + exact Quot.sound hov + · intro heq + have hEq : theRoot hp i₁ = theRoot hp i₂ := + congrArg (Hex.SimpleRealRoot.toReal hp) heq + exact (overlaps_iff_same_root hp i₁ i₂).mpr hEq + +end + +end HexRealRootsMathlib diff --git a/HexRealRootsMathlib/SturmTheorem.lean b/HexRealRootsMathlib/SturmTheorem.lean index 525778b22..4f1de98b8 100644 --- a/HexRealRootsMathlib/SturmTheorem.lean +++ b/HexRealRootsMathlib/SturmTheorem.lean @@ -24,7 +24,7 @@ of real roots of `p` in a half-open interval `(a, b]` is the drop in from `−∞` to `+∞`. The half-open form telescopes the three local lemmas over the finitely many -chain zeros in `(a, b]` (helpers `chainZeros`, `exists_gap_lt`/`exists_gap_gt`, +chain zeros in `(a, b]` (helpers `chainZeros`, `exists_left_gap`/`exists_right_gap`, `sturmVar_eq_right`, `card_filter_Ioc_split`). The line form evaluates the chain just beyond every root at `±M` and reads the `±∞` variation counts `Sturm.sturmVarNegInf` / `Sturm.sturmVarPosInf` off the leading coefficients and @@ -366,7 +366,7 @@ theorem mem_chainZeros {cs : List (Polynomial ℝ)} (hne : ∀ q ∈ cs, q ≠ 0 /-- A gap point just below `z` and above `lo`, lying above every element of the finite set `S` that is below `z`. Used to manufacture the artificial left neighbour a crossing lemma needs at a break point. -/ -theorem exists_gap_lt (S : Finset ℝ) (z lo : ℝ) (hlo : lo < z) : +theorem exists_left_gap (S : Finset ℝ) (z lo : ℝ) (hlo : lo < z) : ∃ a₀, lo < a₀ ∧ a₀ < z ∧ ∀ x ∈ S, x < z → x < a₀ := by classical set U : Finset ℝ := insert lo (S.filter (fun x => x < z)) with hU @@ -390,7 +390,7 @@ theorem exists_gap_lt (S : Finset ℝ) (z lo : ℝ) (hlo : lo < z) : /-- A gap point just above `z` and below `hi`, lying below every element of the finite set `S` that is above `z`. Used to manufacture the artificial right neighbour a crossing lemma needs at a break point. -/ -theorem exists_gap_gt (S : Finset ℝ) (z hi : ℝ) (hhi : z < hi) : +theorem exists_right_gap (S : Finset ℝ) (z hi : ℝ) (hhi : z < hi) : ∃ b₀, z < b₀ ∧ b₀ < hi ∧ ∀ x ∈ S, z < x → b₀ < x := by classical set U : Finset ℝ := insert hi (S.filter (fun x => z < x)) with hU @@ -412,7 +412,7 @@ theorem exists_gap_gt (S : Finset ℝ) (z hi : ℝ) (hhi : z < hi) : linarith /-- The head `p` of a Sturm chain is a member of the chain. -/ -theorem head_mem (hchain : IsSturmChain p chain) : p ∈ chain := by +theorem chain_head_mem (hchain : IsSturmChain p chain) : p ∈ chain := by cases chain with | nil => exact absurd hchain.head (by simp) | cons hd tl => @@ -431,7 +431,7 @@ theorem sturmVar_eq_right (hp : p ≠ 0) (hsf : Squarefree p) · rfl have hne := hchain.nonzero_mem by_cases hzZ : z ∈ chainZeros chain - · obtain ⟨a₀, _, ha₀z, ha₀gap⟩ := exists_gap_lt (chainZeros chain) z (z - 1) (by linarith) + · obtain ⟨a₀, _, ha₀z, ha₀gap⟩ := exists_left_gap (chainZeros chain) z (z - 1) (by linarith) have hz_ex : ∀ q ∈ chain, ∀ x ∈ Set.Icc a₀ c, x ≠ z → q.eval x ≠ 0 := by intro q hq x hx hxz hqx have hxZ : x ∈ chainZeros chain := (mem_chainZeros hne).mpr ⟨q, hq, hqx⟩ @@ -443,7 +443,7 @@ theorem sturmVar_eq_right (hp : p ≠ 0) (hsf : Squarefree p) · have hpz : ∀ x ∈ Set.Icc a₀ c, x ≠ z → ¬ p.IsRoot x := by intro x hx hxz hpr have hxZ : x ∈ chainZeros chain := - (mem_chainZeros hne).mpr ⟨p, head_mem hchain, hpr⟩ + (mem_chainZeros hne).mpr ⟨p, chain_head_mem hchain, hpr⟩ rcases lt_trichotomy x z with hlt' | heq | hgt' · exact absurd (ha₀gap x hxZ hlt') (not_lt.mpr hx.1) · exact hxz heq @@ -460,7 +460,7 @@ theorem sturmVar_eq_right (hp : p ≠ 0) (hsf : Squarefree p) /-- Splitting a half-open interval count: for `a ≤ a' ≤ b`, the number of multiset entries in `(a, b]` is the sum of those in `(a, a']` and `(a', b]`. -/ -theorem card_filter_Ioc_split (s : Multiset ℝ) {a a' b : ℝ} (h1 : a ≤ a') (h2 : a' ≤ b) : +private theorem card_filter_Ioc_split (s : Multiset ℝ) {a a' b : ℝ} (h1 : a ≤ a') (h2 : a' ≤ b) : (s.filter (fun r => a < r ∧ r ≤ b)).card = (s.filter (fun r => a < r ∧ r ≤ a')).card + (s.filter (fun r => a' < r ∧ r ≤ b)).card := by @@ -524,7 +524,7 @@ theorem sturm_half_open (hp : p ≠ 0) (hsf : Squarefree p) have hroots0 : p.roots.filter (fun r => a < r ∧ r ≤ b) = 0 := by rw [Multiset.filter_eq_nil] rintro x hx ⟨h1, h2⟩ - exact hclear x h1 h2 ((mem_chainZeros hne).mpr ⟨p, head_mem hchain, (Polynomial.mem_roots hp).mp hx⟩) + exact hclear x h1 h2 ((mem_chainZeros hne).mpr ⟨p, chain_head_mem hchain, (Polynomial.mem_roots hp).mp hx⟩) rw [heqv, hroots0]; simp · -- Peel off the largest break point `z` in `(a, b]`. have hFne : F.Nonempty := Finset.nonempty_iff_ne_empty.mpr hemp @@ -533,8 +533,8 @@ theorem sturm_half_open (hp : p ≠ 0) (hsf : Squarefree p) have hzmax : ∀ x ∈ F, x ≤ z := fun x hx => F.le_max' x hx obtain ⟨hzS, haz, hzb⟩ : z ∈ chainZeros chain ∧ a < z ∧ z ≤ b := by have h := hzmem; rw [hF, Finset.mem_filter] at h; exact ⟨h.1, h.2.1, h.2.2⟩ - obtain ⟨a', ha_a', ha'z, ha'gap⟩ := exists_gap_lt (chainZeros chain) z a haz - obtain ⟨b', hzb', _, hb'gap⟩ := exists_gap_gt (chainZeros chain) z (z + 1) (by linarith) + obtain ⟨a', ha_a', ha'z, ha'gap⟩ := exists_left_gap (chainZeros chain) z a haz + obtain ⟨b', hzb', _, hb'gap⟩ := exists_right_gap (chainZeros chain) z (z + 1) (by linarith) -- Only break point in `(a', b]` is `z`. have honly : ∀ x, a' < x → x ≤ b → x ∈ chainZeros chain → x = z := by intro x hx1 hx2 hxZ @@ -552,7 +552,7 @@ theorem sturm_half_open (hp : p ≠ 0) (hsf : Squarefree p) · exact hxz heq · exact absurd (hb'gap x hxZ hgt') (not_lt.mpr hx.2) have hpz : ∀ x ∈ Set.Icc a' b', x ≠ z → ¬ p.IsRoot x := fun x hx hxz hpr => - hz_ex p (head_mem hchain) x hx hxz hpr + hz_ex p (chain_head_mem hchain) x hx hxz hpr -- Right registration: `sturmVar z = sturmVar b`. have hzeqb : sturmVar chain z = sturmVar chain b := by apply sturmVar_eq_right hp hsf hchain hzb @@ -589,7 +589,7 @@ theorem sturm_half_open (hp : p ≠ 0) (hsf : Squarefree p) constructor · rintro ⟨h1, h2⟩ exact honly x h1 h2 - ((mem_chainZeros hne).mpr ⟨p, head_mem hchain, (Polynomial.mem_roots hp).mp hx⟩) + ((mem_chainZeros hne).mpr ⟨p, chain_head_mem hchain, (Polynomial.mem_roots hp).mp hx⟩) · rintro rfl; exact ⟨ha'z, hzb⟩ rw [hfeq, Multiset.filter_eq', Multiset.card_replicate, Multiset.count_eq_one_of_mem hnod hzrootmem] @@ -605,7 +605,7 @@ theorem sturm_half_open (hp : p ≠ 0) (hsf : Squarefree p) rw [Multiset.filter_eq_nil] rintro x hx ⟨h1, h2⟩ have hxz : x = z := honly x h1 h2 - ((mem_chainZeros hne).mpr ⟨p, head_mem hchain, (Polynomial.mem_roots hp).mp hx⟩) + ((mem_chainZeros hne).mpr ⟨p, chain_head_mem hchain, (Polynomial.mem_roots hp).mp hx⟩) rw [hxz] at hx exact hzroot ((Polynomial.mem_roots hp).mp hx) rw [hfeq]; rfl @@ -705,7 +705,7 @@ theorem sturm_line (hp : p ≠ 0) (hsf : Squarefree p) rw [Multiset.filter_eq_self] intro r hr have hroot : p.eval r = 0 := (Polynomial.mem_roots hp).mp hr - have hrz : r ∈ chainZeros chain := (mem_chainZeros hne).mpr ⟨p, head_mem hchain, hroot⟩ + have hrz : r ∈ chainZeros chain := (mem_chainZeros hne).mpr ⟨p, chain_head_mem hchain, hroot⟩ have hra := hM r hrz; rw [abs_lt] at hra exact ⟨hra.1, hra.2.le⟩ rw [← hMnegEq, ← hMposEq, hkey, hfilter] diff --git a/HexRealRootsMathlib/TwoCircle.lean b/HexRealRootsMathlib/TwoCircle.lean new file mode 100644 index 000000000..6d81209f6 --- /dev/null +++ b/HexRealRootsMathlib/TwoCircle.lean @@ -0,0 +1,84 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +module + +public import Mathlib +public import HexRealRoots.IsolateDescartes + +public section + +/-! +# Deferred: Descartes engine termination (the two-circle theorem) + +This module states the one deferred theorem of `HexRealRootsMathlib` and names +its prerequisite. It is the **only intentional `sorry` in the library** — every +other theorem (isolation soundness, run completeness, driver completeness for +the Sturm engine, refinement, and root identity) is complete without it. + +`isolateDescartes?_isSome` says the *Descartes* engine alone never falls back to +`none` on nonzero square-free input. The Sturm engine's termination +(`isolateSturm?_isSome`) and hence the top-level driver (`isolate?_isSome`) are +already proven, so nothing downstream — including hex-rcf's decision procedure — +waits on this statement. Its value is to retire the Sturm fallback from the +trusted runtime story. + +## Prerequisite: the Obreshkoff two-circle theorem + +For an interval `(a, b)`, the variation count of the Möbius-transformed +polynomial is at least the number of roots in the one-circle region (the open +disc with diameter `(a, b)`) and at most the number of roots in the two-circle +region (the union of the two discs through `a` and `b` whose centres lie at +`(a+b)/2 ± i·(b−a)/(2√3)`), counted with multiplicity. Consequences: a short +interval far from all roots has count `0`, and a short interval whose two-circle +region contains one simple real root has count `1`, so at `isolationDepth p` the +Descartes worklist drains and every candidate certifies. + +Unlike the Sturm termination argument, the Descartes variation counts are also +disturbed by nearby *non-real* roots, which is exactly why this statement needs +the two-circle theorem rather than the real-gap separation bound. + +## Status and boundaries (from the SPEC) + +- The two-circle theorem has no formalisation in any proof assistant that we + know of. The classical proof (Obreschkoff 1963; modern treatment in + Krandick-Mehlhorn 2006 and Eigenwillig 2008) is an induction on multiplying in + linear and conjugate-quadratic factors, with sector inequalities on + coefficient sequences. Elementary but long, and the effort is genuinely + uncertain. +- **Nothing else waits for it.** `isolate?_isSome`, all soundness theorems, and + hex-rcf's decision procedure are complete without it. +- Like the Sturm slice, it should be developed against `Polynomial ℝ` (and `ℂ` + for the regions) with no `HexRealRoots` dependence, as a Mathlib contribution + in its own right. + +## Conformance-deletion obligation + +The PR that discharges this `sorry` **must delete the Descartes stand-in +assertions** in `conformance/HexRealRoots/Conformance.lean` in the same change. +Those assertions — `(isolateDescartes? p).isSome` and +`endpoints (isolateDescartes? p) = endpoints (isolate? p)` per fixture — are the +SPEC-mandated executable stand-in for this theorem (see +[hex-real-roots.md](../SPEC/Libraries/hex-real-roots.md) §"Conformance +fixtures" and the deletion note in that conformance module). Once the theorem +carries the claim, the stand-in is redundant and is retired. +-/ + +namespace HexRealRootsMathlib + +/-- **The Descartes engine succeeds on nonzero square-free input (deferred).** +`isolateDescartes? p ≠ none` for nonzero `p` passing the executable +`SquareFreeRat` test. + +Deferred pending the Obreshkoff two-circle theorem (see the module docstring): +at `isolationDepth p` the Descartes worklist drains because each short interval's +Möbius variation count is pinned to the number of roots in its two-circle +region, which is `0` far from the roots and `1` around a single simple real +root. This is the sole intentional `sorry` in `HexRealRootsMathlib`. -/ +theorem isolateDescartes?_isSome (p : Hex.ZPoly) (hp0 : p ≠ 0) + (hp : Hex.ZPoly.SquareFreeRat p) : (Hex.isolateDescartes? p).isSome := sorry + +end HexRealRootsMathlib diff --git a/conformance/HexRealRootsMathlib/Conformance.lean b/conformance/HexRealRootsMathlib/Conformance.lean new file mode 100644 index 000000000..b04cc0d3a --- /dev/null +++ b/conformance/HexRealRootsMathlib/Conformance.lean @@ -0,0 +1,198 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +import HexRealRootsMathlib.ChainCorrespond +import HexRealRootsMathlib.Isolations + +/-! +Companion conformance checks for `HexRealRootsMathlib`. + +Oracle: core uses the **proven correspondence theorems** as the algebraic +oracle. `rootCount_eq_card_roots` (and `squareFreeRat_iff` feeding its +square-free hypothesis) is the bridge that ties the executable, computable +`Hex.rootCount` to the noncomputable Mathlib `(toPolyℝ p).roots.card`. There is +no external oracle profile: the two sides are pinned independently — the +executable side by `#guard` (native evaluation) and the Mathlib side by a +hand-derived root-multiset computation proven as a theorem — and the correspond- +ence theorem certifies they agree. +Mode: always for core. + +Because Mathlib root counts are noncomputable, the checks are **theorems**, not +`#guard`s of the root multiset. For each committed fixture: + +* `toPolyℝ_` identifies the real cast of the executable polynomial with + an explicit `Polynomial ℝ` (mechanical `coeff` comparison). +* `card_` computes `(toPolyℝ ).roots.card` from that explicit + polynomial by an independent Mathlib factorisation (the hand-derived count). +* `#guard Hex.rootCount = N` confirms the executable engine computes + the same `N` at runtime. + +This module certifies that the **theorem layer** connects — that the +correspondence theorems instantiate and transport concrete counts — rather than +re-running the executable oracle (which is `HexRealRoots.Conformance`'s job). +The `x − 5` fixture carries the full formal tie: `rootCount_x_sub_5` derives +`Hex.rootCount = 1` from `rootCount_eq_card_roots` and the independent +`card_linear`, so the executable value (also `#guard`ed) is pinned by the +theorem, not just by evaluation. The higher-degree fixtures certify each side +independently against the same hand-derived count; their full ties would need a +square-free proof of each rational cast, which the linear demonstrator already +exhibits end to end. +-/ + +namespace HexRealRootsMathlib +namespace Conformance + +open Polynomial + +/-! ### Committed fixtures. + +Stored in ascending-degree coefficient order; the factored form and real roots +are named so the Mathlib-side counts are hand-derivable. -/ + +/-- `x − 5`; single real root `5`. -/ +private def linear : Hex.ZPoly := Hex.DensePoly.ofCoeffs #[(-5 : Int), 1] +/-- `x² − 1 = (x − 1)(x + 1)`; real roots `±1`. -/ +private def quadPair : Hex.ZPoly := Hex.DensePoly.ofCoeffs #[(-1 : Int), 0, 1] +/-- `x² + 1`; no real roots. -/ +private def quadNone : Hex.ZPoly := Hex.DensePoly.ofCoeffs #[(1 : Int), 0, 1] +/-- `x³ − x = x(x − 1)(x + 1)`; real roots `−1, 0, 1`. -/ +private def cubicTriple : Hex.ZPoly := Hex.DensePoly.ofCoeffs #[(0 : Int), -1, 0, 1] +/-- The nonzero constant `7`; no roots (degree `0`, below the correspondence +theorem's positive-degree hypothesis). -/ +private def const7 : Hex.ZPoly := Hex.DensePoly.ofCoeffs #[(7 : Int)] + +/-! ### Real casts: the executable polynomial as an explicit `Polynomial ℝ`. -/ + +private theorem toPolyℝ_linear : toPolyℝ linear = X - C 5 := by + apply Polynomial.ext; intro n + rw [coeff_toPolyℝ] + simp only [linear, Hex.DensePoly.coeff_ofCoeffs, coeff_sub, coeff_X, coeff_C] + match n with + | 0 => norm_num [Array.getD] + | 1 => norm_num [Array.getD] + | (k + 2) => norm_num [Array.getD]; omega + +private theorem toPolyℝ_quadPair : toPolyℝ quadPair = X ^ 2 - C 1 := by + apply Polynomial.ext; intro n + rw [coeff_toPolyℝ] + simp only [quadPair, Hex.DensePoly.coeff_ofCoeffs, coeff_sub, coeff_X_pow, coeff_C] + match n with + | 0 => norm_num [Array.getD] + | 1 => norm_num [Array.getD] + | 2 => norm_num [Array.getD] + | (k + 3) => norm_num [Array.getD]; omega + +private theorem toPolyℝ_quadNone : toPolyℝ quadNone = X ^ 2 + C 1 := by + apply Polynomial.ext; intro n + rw [coeff_toPolyℝ] + simp only [quadNone, Hex.DensePoly.coeff_ofCoeffs, coeff_add, coeff_X_pow, coeff_C] + match n with + | 0 => norm_num [Array.getD] + | 1 => norm_num [Array.getD] + | 2 => norm_num [Array.getD] + | (k + 3) => norm_num [Array.getD]; omega + +private theorem toPolyℝ_cubicTriple : toPolyℝ cubicTriple = X ^ 3 - X := by + apply Polynomial.ext; intro n + rw [coeff_toPolyℝ] + simp only [cubicTriple, Hex.DensePoly.coeff_ofCoeffs, coeff_sub, coeff_X_pow, coeff_X] + match n with + | 0 => norm_num [Array.getD] + | 1 => norm_num [Array.getD] + | 2 => norm_num [Array.getD] + | 3 => norm_num [Array.getD] + | (k + 4) => norm_num [Array.getD]; omega + +private theorem toPolyℝ_const7 : toPolyℝ const7 = C 7 := by + apply Polynomial.ext; intro n + rw [coeff_toPolyℝ] + simp only [const7, Hex.DensePoly.coeff_ofCoeffs, coeff_C] + match n with + | 0 => norm_num [Array.getD] + | (k + 1) => norm_num [Array.getD] + +/-! ### Mathlib-side root counts (hand-derived by factorisation). -/ + +private theorem card_linear : (toPolyℝ linear).roots.card = 1 := by + rw [toPolyℝ_linear, roots_X_sub_C]; simp + +private theorem card_quadPair : (toPolyℝ quadPair).roots.card = 2 := by + rw [toPolyℝ_quadPair, + show (X ^ 2 - C 1 : ℝ[X]) = (X - C 1) * (X + C 1) by + have h : (X - C (1 : ℝ)) * (X + C 1) = X ^ 2 - C 1 * C 1 := by ring + rw [h, ← map_mul, mul_one]] + rw [roots_mul (by + apply mul_ne_zero <;> intro h <;> simpa using congrArg (Polynomial.eval 0) h)] + rw [roots_X_sub_C, show (X + C (1 : ℝ)) = X - C (-1) by rw [map_neg]; ring, roots_X_sub_C] + simp + +private theorem card_quadNone : (toPolyℝ quadNone).roots.card = 0 := by + rw [toPolyℝ_quadNone, Multiset.card_eq_zero] + by_contra hne0 + obtain ⟨x, hx⟩ := Multiset.exists_mem_of_ne_zero hne0 + have hne : (X ^ 2 + C (1 : ℝ)) ≠ 0 := by + intro h; simpa using congrArg (Polynomial.eval 0) h + have hroot := (Polynomial.mem_roots hne).mp hx + simp only [Polynomial.IsRoot, eval_add, eval_pow, eval_X, eval_C] at hroot + nlinarith [sq_nonneg x] + +private theorem card_cubicTriple : (toPolyℝ cubicTriple).roots.card = 3 := by + rw [toPolyℝ_cubicTriple, + show (X ^ 3 - X : ℝ[X]) = X * (X - C 1) * (X + C 1) by + have h : X * (X - C (1 : ℝ)) * (X + C 1) = X ^ 3 - X * (C 1 * C 1) := by ring + rw [h, ← map_mul, mul_one, map_one, mul_one]] + have h1 : (X * (X - C 1) * (X + C 1) : ℝ[X]) ≠ 0 := by + apply mul_ne_zero + · apply mul_ne_zero + · exact X_ne_zero + · intro h; simpa using congrArg (Polynomial.eval 0) h + · intro h; simpa using congrArg (Polynomial.eval 0) h + rw [roots_mul h1, roots_mul (by + apply mul_ne_zero + · exact X_ne_zero + · intro h; simpa using congrArg (Polynomial.eval 0) h)] + rw [roots_X, roots_X_sub_C, show (X + C (1 : ℝ)) = X - C (-1) by rw [map_neg]; ring, + roots_X_sub_C] + simp + +private theorem card_const7 : (toPolyℝ const7).roots.card = 0 := by + rw [toPolyℝ_const7, roots_C]; simp + +/-! ### Executable root counts agree with the Mathlib counts (runtime). -/ + +#guard Hex.rootCount linear = 1 +#guard Hex.rootCount quadPair = 2 +#guard Hex.rootCount quadNone = 0 +#guard Hex.rootCount cubicTriple = 3 +#guard Hex.rootCount const7 = 0 + +/-! ### The full formal tie on the linear fixture. + +`rootCount_eq_card_roots` needs a `SquareFreeRat` witness; for `x − 5` it comes +from `squareFreeRat_iff` and the irreducibility of the linear rational cast. +Chained with `card_linear`, the correspondence theorem pins the executable +`Hex.rootCount` to `1` as a theorem — the same value the `#guard` above +evaluates. -/ + +private theorem toPolyℚ_linear : toPolyℚ linear = X - C 5 := by + apply Polynomial.ext; intro n + rw [Polynomial.coeff_map, HexPolyZMathlib.coeff_toPolynomial] + simp only [linear, Hex.DensePoly.coeff_ofCoeffs, coeff_sub, coeff_X, coeff_C] + match n with + | 0 => norm_num [Array.getD] + | 1 => norm_num [Array.getD] + | (k + 2) => norm_num [Array.getD]; omega + +private theorem squareFreeRat_linear : Hex.ZPoly.SquareFreeRat linear := by + rw [squareFreeRat_iff linear (by decide)] + rw [toPolyℚ_linear] + exact (irreducible_X_sub_C (5 : ℚ)).squarefree + +private theorem rootCount_x_sub_5 : Hex.rootCount linear = 1 := by + rw [rootCount_eq_card_roots linear (by decide) squareFreeRat_linear, card_linear] + +end Conformance +end HexRealRootsMathlib diff --git a/lakefile.lean b/lakefile.lean index d97c5b736..f0f41f903 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -205,7 +205,7 @@ lean_lib HexGF2BenchSupport where -- `*_emit_fixtures` exes below, carrying `srcDir := "conformance"`. lean_lib HexConformance where srcDir := "conformance" - globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexLLL.Conformance, `HexMatrix.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRealRoots.Conformance, `HexRoots.Conformance] + globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexLLL.Conformance, `HexMatrix.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexRoots.Conformance] lean_exe hexrowreduce_emit_fixtures where srcDir := "conformance" diff --git a/libraries.yml b/libraries.yml index 16fd49d3d..4d3cd8c93 100644 --- a/libraries.yml +++ b/libraries.yml @@ -502,7 +502,7 @@ libraries: HexRealRootsMathlib: deps: [HexRealRoots, HexPolyZMathlib] mathlib: true - done_through: 0 + done_through: 1 status: active HexRCF: deps: [HexRealRoots, HexRealRootsMathlib, HexPolyZ, HexPolyZMathlib] diff --git a/progress/2026-07-11T19-27-49Z-real-roots-s8-wrapup.md b/progress/2026-07-11T19-27-49Z-real-roots-s8-wrapup.md new file mode 100644 index 000000000..b3ed47dc1 --- /dev/null +++ b/progress/2026-07-11T19-27-49Z-real-roots-s8-wrapup.md @@ -0,0 +1,39 @@ +# HexRealRootsMathlib S8 wrap-up: root identity, deferred two-circle, companion conformance + +## Accomplished + +- `HexRealRootsMathlib/SimpleRealRoot.lean`: `theRoot`, `overlaps_iff_same_root`, + `SimpleRealRoot.toReal`/`toReal_isRoot`/`toReal_injective`, `sameRoot_iff`. + The forward direction of `overlaps_iff_same_root` is the separation argument + (both widths `≤ 2^{−sepPrec}`, `sepPrec_separates'`); the backward direction is + the common-root interval containment. Signatures match the SPEC verbatim: `p ≠ 0` + is derived internally from the isolation's `count_one` (`degree_pos_of_count_one`), + so no `hp0` hypothesis is needed (unlike the driver theorems). +- `HexRealRootsMathlib/TwoCircle.lean`: states `isolateDescartes?_isSome` with the + full deferred-theorem docstring (Obreshkoff two-circle prerequisite, nothing + depends on it, conformance-deletion obligation). The one intentional `sorry`. +- `conformance/HexRealRootsMathlib/Conformance.lean` (plain file, module + `HexRealRootsMathlib.Conformance`): cast equalities + independent Mathlib + root-card theorems + `#guard`ed executable `rootCount`, plus the full formal tie + on `x − 5` (`rootCount_eq_card_roots` instantiated via `squareFreeRat_iff` + + irreducibility). Added to the `HexConformance` globs; `conformance_targets.py + --check` passes. +- M5 renames in `SturmTheorem.lean`: `exists_gap_lt/gt` → `exists_left_gap/right_gap`, + `head_mem` → `chain_head_mem`, `card_filter_Ioc_split` made `private`. +- `libraries.yml`: `HexRealRootsMathlib` `done_through` 0 → 1. +- Umbrella imports the two new files; docstring refreshed. `check_dag`, + `check_phase4`, `conformance_targets --check` all green. + +## Current frontier + +`lake build HexRealRootsMathlib HexConformance` completes (9065 jobs); the only +`sorry` warning in the whole library is `TwoCircle.isolateDescartes?_isSome`. + +## Next step + +Phase-2 review pass for `HexRealRootsMathlib`, and eventually discharging the +two-circle theorem (which then deletes the conformance Descartes stand-ins). + +## Blockers + +None. From a056402825d0fe435168da28d1368b701b2bce8a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 11 Jul 2026 19:31:54 +0000 Subject: [PATCH 2/2] doc(real-roots-mathlib): p != 0 in the deferred theorem's SPEC signature SquareFreeRat 0 holds vacuously, so the nonzero hypothesis is required; matches the driver-completeness precedent. Per Codex review of #8753. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01NUB5EStJpJ8CPqMkNw7Qjz --- SPEC/Libraries/hex-real-roots-mathlib.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/SPEC/Libraries/hex-real-roots-mathlib.md b/SPEC/Libraries/hex-real-roots-mathlib.md index cb875b33d..962bf88f3 100644 --- a/SPEC/Libraries/hex-real-roots-mathlib.md +++ b/SPEC/Libraries/hex-real-roots-mathlib.md @@ -239,8 +239,8 @@ theorem sameRoot_iff (hp) (i₁ i₂) : ## Deferred: Descartes engine termination ```lean -theorem isolateDescartes?_isSome (p : ZPoly) (hp : SquareFreeRat p) : - (Hex.isolateDescartes? p).isSome +theorem isolateDescartes?_isSome (p : ZPoly) (hp0 : p ≠ 0) + (hp : SquareFreeRat p) : (Hex.isolateDescartes? p).isSome ``` Prerequisite: the **Obreshkoff two-circle theorem**. For an interval