From 5561ec6bf066e96aa20c949d36bd5c84c867e597 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 7 Sep 2026 08:48:04 +0000 Subject: [PATCH 1/8] feat(real-roots-mathlib): checked root counts and a simpler Sturm API --- HexPolyZMathlib/PolyParse.lean | 44 +- HexRCF/SPEC/hex-rcf.md | 4 +- HexRCF/SturmReplay.lean | 20 +- HexRealRootsMathlib.lean | 6 + HexRealRootsMathlib/ChainCorrespond.lean | 107 ++--- HexRealRootsMathlib/LiteralChain.lean | 36 +- HexRealRootsMathlib/README.md | 27 ++ HexRealRootsMathlib/RealRootCount.lean | 170 +++++++ HexRealRootsMathlib/RealRootCountTests.lean | 73 +++ .../SPEC/hex-real-roots-mathlib.md | 30 +- HexRealRootsMathlib/SturmCertificate.lean | 190 ++++++++ HexRealRootsMathlib/SturmChainDefs.lean | 188 +++----- HexRealRootsMathlib/SturmTests.lean | 38 ++ HexRealRootsMathlib/SturmTheorem.lean | 444 ++++++++---------- lakefile.lean | 2 + scripts/check_sturm_sync.py | 55 +++ scripts/release/released.yml | 2 +- 17 files changed, 932 insertions(+), 504 deletions(-) create mode 100644 HexRealRootsMathlib/RealRootCount.lean create mode 100644 HexRealRootsMathlib/RealRootCountTests.lean create mode 100644 HexRealRootsMathlib/SturmCertificate.lean create mode 100644 HexRealRootsMathlib/SturmTests.lean create mode 100644 scripts/check_sturm_sync.py diff --git a/HexPolyZMathlib/PolyParse.lean b/HexPolyZMathlib/PolyParse.lean index 9f181abae2..e623d7d8a5 100644 --- a/HexPolyZMathlib/PolyParse.lean +++ b/HexPolyZMathlib/PolyParse.lean @@ -7,16 +7,15 @@ Authors: Kim Morrison module public meta import HexPolyZ.IntegerPolynomial -public import HexPolyZMathlib.PolynomialEquivalence -public import Lean - -public section +public import Mathlib.Algebra.Polynomial.Basic +public import Mathlib.Data.Rat.Defs +public meta import Mathlib.Lean.Expr.Basic /-! +# Interpreting closed polynomial expressions + Elaboration-time interpretation of closed `Polynomial R` expressions as -executable `Hex.ZPoly` values, shared by the `isolate_roots` elaborator -(`HexRealRootsMathlib`) and the `factor_poly`/`irreducibility` `Polynomial ℤ` -extension (`HexBerlekampZassenhausMathlib`). +executable `Hex.ZPoly` values. The interpreter matches the structural heads `X / C / numerals / + / - / * / neg / ^ (Nat literal)` on the *raw* term (a `whnf` would unfold @@ -25,6 +24,8 @@ match) and unfolds named definitions one delta step at a time under a fuel guard. Every entry point takes the calling tactic's name for error messages. -/ +public section + namespace HexPolyZMathlib.PolyParse open Lean Meta @@ -96,26 +97,35 @@ meta def evalCoeff (tactic : String) (isRat : Bool) (e : Expr) : MetaM Int := do /-- Recursive interpreter from a `Polynomial R` expression over `X / C / numerals (OfNat) / + / - / * / ^ (Nat) / neg`, with named local defs unfolded one delta step at a time under a fuel guard, to a `Hex.ZPoly` value. -`isRat` selects the `ℚ`-style non-integer rejection. -/ +`isRat` permits evaluating closed rational coefficients, provided they are integers. +`fuel` bounds successive unfolding of named definitions. `onUnfold` records their +names so that callers can unfold the same definitions when checking the result. -/ meta partial def parsePoly (tactic : String) (isRat : Bool) (fuel : Nat) - (e : Expr) : MetaM Hex.ZPoly := do + (e : Expr) (onUnfold : Name → MetaM Unit := fun _ => pure ()) : MetaM Hex.ZPoly := do + match e with + | .mdata _ body => return ← parsePoly tactic isRat fuel body onUnfold + | .letE _ _ value body _ => + return ← parsePoly tactic isRat fuel (body.instantiate1 value) onUnfold + | _ => pure () -- Match structural heads on the *raw* term first: `whnf` would unfold -- `Polynomial.C`/`X`/numerals into their `Finsupp` normal form and defeat the -- match. Only if no structural head applies do we unfold once (a named local -- def) under the fuel guard. match e.getAppFnArgs with | (``HAdd.hAdd, #[_, _, _, _, a, b]) => - return (← parsePoly tactic isRat fuel a) + (← parsePoly tactic isRat fuel b) + return (← parsePoly tactic isRat fuel a onUnfold) + (← parsePoly tactic isRat fuel b onUnfold) | (``HSub.hSub, #[_, _, _, _, a, b]) => - return (← parsePoly tactic isRat fuel a) - (← parsePoly tactic isRat fuel b) + return (← parsePoly tactic isRat fuel a onUnfold) - (← parsePoly tactic isRat fuel b onUnfold) | (``HMul.hMul, #[_, _, _, _, a, b]) => - return (← parsePoly tactic isRat fuel a) * (← parsePoly tactic isRat fuel b) - | (``Neg.neg, #[_, _, a]) => return - (← parsePoly tactic isRat fuel a) + return (← parsePoly tactic isRat fuel a onUnfold) * (← parsePoly tactic isRat fuel b onUnfold) + | (``Neg.neg, #[_, _, a]) => return - (← parsePoly tactic isRat fuel a onUnfold) | (``HPow.hPow, #[_, _, _, _, a, n]) => do - let base ← parsePoly tactic isRat fuel a + let base ← parsePoly tactic isRat fuel a onUnfold let k ← getNat tactic n let mut acc : Hex.ZPoly := Hex.DensePoly.C 1 - for _ in [0:k] do acc := acc * base + for _ in [0:k] do + checkSystem "polynomial exponentiation" + acc := acc * base return acc | (``Polynomial.X, _) => return Hex.DensePoly.ofCoeffs #[(0 : Int), 1] | (``Polynomial.C, #[_, _, c]) => return Hex.DensePoly.C (← evalCoeff tactic isRat c) @@ -134,7 +144,9 @@ meta partial def parsePoly (tactic : String) (isRat : Bool) (fuel : Nat) throwError "{tactic}: unsupported polynomial syntax{indentExpr e}" else match ← unfoldDefinition? e with - | some e' => parsePoly tactic isRat (fuel - 1) e' + | some e' => + if let some name := e.getAppFn.constName? then onUnfold name + parsePoly tactic isRat (fuel - 1) e' onUnfold | none => throwError "{tactic}: unsupported polynomial syntax{indentExpr e}" end HexPolyZMathlib.PolyParse diff --git a/HexRCF/SPEC/hex-rcf.md b/HexRCF/SPEC/hex-rcf.md index bcbf02fdcf..298858916f 100644 --- a/HexRCF/SPEC/hex-rcf.md +++ b/HexRCF/SPEC/hex-rcf.md @@ -226,7 +226,7 @@ proved equivalences. which must be `0` or `1`. Count `0` means the root is greater than `e`. Count `1` means the root is at most `e`; exact evaluation of `P(e)` distinguishes equality from strict inequality. - `Sturm.sturm_half_open` has no endpoint-nonroot premise, so this is + `Sturm.IsSturmChain.sturm_Ioc` has no endpoint-nonroot premise, so this is valid even when the dyadic lower endpoint `l` is itself a root. 6. **Build cells.** With `k` isolations `I₀ < … < Iₖ₋₁` (roots @@ -416,7 +416,7 @@ literal cast chain satisfies `Sturm.IsSturmChain`; in particular `f` is squarefree. Its interval count is the variation difference of this literal chain, not a call to `ZPoly.sturmCount f`, and its total count is the corresponding `−∞/+∞` difference. The proof factors through -`Sturm.sturm_half_open` and `Sturm.sturm_line`. Constants are handled +`Sturm.IsSturmChain.sturm_Ioc` and `Sturm.IsSturmChain.sturm`. Constants are handled separately because the interval-count theorem requires positive degree. diff --git a/HexRCF/SturmReplay.lean b/HexRCF/SturmReplay.lean index 757b538f2d..bed3bf28c5 100644 --- a/HexRCF/SturmReplay.lean +++ b/HexRCF/SturmReplay.lean @@ -110,14 +110,8 @@ theorem count_eq_card_roots {f : ZPoly} {cert : SturmReplay} cert.count I = (HexRealRootsMathlib.Literal.rootsIn (HexRealRootsMathlib.toPolyℝ f) I).card := by - obtain ⟨s₁, rest, _hchain, _hrep, hnz, _hdegrees, _hpos, _hderiv, _hcount⟩ := - check_sound h - unfold count - apply HexRealRootsMathlib.literalCount_eq_card_roots f cert.chain - · intro hf - exact hnz f (by simp) (HexRealRootsMathlib.toPolyℝ_eq_zero_iff.mp hf) - · exact squarefree_of_check h - · exact isChain_of_check h + exact HexRealRootsMathlib.literalCount_eq_card_roots f cert.chain + (squarefree_of_check h) (isChain_of_check h) I /-- The literal infinite-endpoint variation drop of an accepted replay counts exactly all real roots of its head. This acts directly on the certificate @@ -125,14 +119,8 @@ array. -/ theorem total_eq_card_roots {f : ZPoly} {cert : SturmReplay} (h : cert.check f = true) : cert.total = (HexRealRootsMathlib.toPolyℝ f).roots.card := by - obtain ⟨s₁, rest, _hchain, _hrep, hnz, _hdegrees, _hpos, _hderiv, _hcount⟩ := - check_sound h - unfold total - apply HexRealRootsMathlib.literalRootCount_eq_card_roots f cert.chain - · intro hf - exact hnz f (by simp) (HexRealRootsMathlib.toPolyℝ_eq_zero_iff.mp hf) - · exact squarefree_of_check h - · exact isChain_of_check h + exact HexRealRootsMathlib.literalRootCount_eq_card_roots f cert.chain + (squarefree_of_check h) (isChain_of_check h) end SturmReplay diff --git a/HexRealRootsMathlib.lean b/HexRealRootsMathlib.lean index 82f4fdc515..53afeadb72 100644 --- a/HexRealRootsMathlib.lean +++ b/HexRealRootsMathlib.lean @@ -8,6 +8,8 @@ module public import HexRealRootsMathlib.SturmChainDefs public import HexRealRootsMathlib.SturmTheorem +public import HexRealRootsMathlib.SturmCertificate +public import HexRealRootsMathlib.RealRootCount public import HexRealRootsMathlib.Hadamard public import HexRealRootsMathlib.Discr public import HexRealRootsMathlib.Separation @@ -38,6 +40,10 @@ The Sturm development includes the zero-skipping sign-variation count {name}`Sturm.IsSturmChain`, and the counting and line forms of Sturm's theorem over `Polynomial ℝ`, independently of the executable `HexRealRoots` types. +`SturmCertificate` assembles root-count certificates from identities between +Mathlib polynomials. `RealRootCount` uses them to provide `by real_root_count` +and the term form `real_root_count p`, with Hex supplying the candidate chain. + The executable correspondence builds on these results: `ChainCorrespond` connects {name}`Hex.ZPoly.sturmChain`, {name}`Hex.ZPoly.sturmCount`, and diff --git a/HexRealRootsMathlib/ChainCorrespond.lean b/HexRealRootsMathlib/ChainCorrespond.lean index 777dc22370..47390f1e60 100644 --- a/HexRealRootsMathlib/ChainCorrespond.lean +++ b/HexRealRootsMathlib/ChainCorrespond.lean @@ -46,7 +46,7 @@ Every downstream consumer supplies a nonzero (indeed positive-degree) input. namespace HexRealRootsMathlib -open Polynomial HexPolyZMathlib +open Polynomial HexPolyZMathlib Filter Topology noncomputable section @@ -992,23 +992,13 @@ private theorem chainList_last_unit : `C c₀ · a = Q · b − C k · c'` (with `k ≠ 0`) transports `IsCoprime b c'` *back* to `IsCoprime a b`: solving the relation for `c'` and substituting into a Bezout combination for `(b, c')` yields one for `(a, b)`. -/ -theorem coprime_step_rev {a b c' : Polynomial ℝ} {c₀ k : ℝ} {Q : Polynomial ℝ} - (hk : k ≠ 0) - (hrel : Polynomial.C c₀ * a = Q * b - Polynomial.C k * c') - (h : IsCoprime b c') : IsCoprime a b := by - obtain ⟨u, v, huv⟩ := h - have hCk : Polynomial.C k⁻¹ * Polynomial.C k = 1 := by - rw [← Polynomial.C_mul, inv_mul_cancel₀ hk, Polynomial.C_1] - have hc' : c' = Polynomial.C k⁻¹ * (Q * b - Polynomial.C c₀ * a) := by - have hkc' : Polynomial.C k * c' = Q * b - Polynomial.C c₀ * a := by rw [hrel]; ring - calc c' = Polynomial.C k⁻¹ * (Polynomial.C k * c') := by rw [← mul_assoc, hCk, one_mul] - _ = Polynomial.C k⁻¹ * (Q * b - Polynomial.C c₀ * a) := by rw [hkc'] - refine ⟨-(v * Polynomial.C k⁻¹ * Polynomial.C c₀), u + v * Polynomial.C k⁻¹ * Q, ?_⟩ - calc -(v * Polynomial.C k⁻¹ * Polynomial.C c₀) * a - + (u + v * Polynomial.C k⁻¹ * Q) * b - = u * b + v * (Polynomial.C k⁻¹ * (Q * b - Polynomial.C c₀ * a)) := by ring - _ = u * b + v * c' := by rw [← hc'] - _ = 1 := huv +theorem coprime_step_rev {p q r : ℝ[X]} {a b : ℝ} {d : ℝ[X]} + (hb : b ≠ 0) (hid : C a * p = d * q - C b * r) (h : IsCoprime q r) : + IsCoprime p q := by + apply IsCoprime.of_mul_left_right (x := C a) + rw [hid, IsCoprime.mul_sub_right_left_iff, + isCoprime_mul_unit_left_left (isUnit_C.mpr (isUnit_iff_ne_zero.mpr hb))] + exact h.symm /-- **A terminal-constant chain has coprime seeds.** If the last element of `prev :: cur :: chainList fuel prev cur` is a unit of `ℝ[X]` (its real cast), then @@ -1073,41 +1063,21 @@ negative on a punctured left neighbourhood of `r` and positive on a punctured right neighbourhood: the difference quotient tends to the positive derivative, so it is eventually positive, and the sign of `f x = slope · (x − r)` follows the sign of `x − r`. -/ -private theorem eventually_flank_of_deriv_pos {f : Polynomial ℝ} {r : ℝ} - (h0 : f.eval r = 0) (hd : 0 < f.derivative.eval r) : - (∀ᶠ x in nhdsWithin r (Set.Iio r), f.eval x < 0) ∧ - (∀ᶠ x in nhdsWithin r (Set.Ioi r), 0 < f.eval x) := by - have hder : HasDerivAt (fun y => f.eval y) (f.derivative.eval r) r := - f.hasDerivAt r - have hslope : Filter.Tendsto (slope (fun y => f.eval y) r) (nhdsWithin r {r}ᶜ) - (nhds (f.derivative.eval r)) := hasDerivAt_iff_tendsto_slope.mp hder - have hpos : ∀ᶠ x in nhdsWithin r {r}ᶜ, slope (fun y => f.eval y) r x ∈ Set.Ioi 0 := - hslope (Ioi_mem_nhds hd) +private theorem sign_near_root {p : ℝ[X]} {r : ℝ} + (hr : p.eval r = 0) (hd : 0 < p.derivative.eval r) : + (∀ᶠ x in 𝓝[<] r, p.eval x < 0) ∧ (∀ᶠ x in 𝓝[>] r, 0 < p.eval x) := by + obtain ⟨hl, hu⟩ := hasDerivAt_iff_tendsto_slope_left_right.mp (p.hasDerivAt r) constructor - · have hmono : nhdsWithin r (Set.Iio r) ≤ nhdsWithin r {r}ᶜ := - nhdsWithin_mono r (fun x hx => ne_of_lt hx) - filter_upwards [hpos.filter_mono hmono, self_mem_nhdsWithin] with x hx hxr - have hx' : 0 < (f.eval x - f.eval r) / (x - r) := by - have := Set.mem_Ioi.mp hx - rwa [slope_def_field] at this - rw [h0, sub_zero] at hx' - have hxr' : x - r < 0 := sub_neg.mpr (Set.mem_Iio.mp hxr) - have h2 : f.eval x = f.eval x / (x - r) * (x - r) := - (div_mul_cancel₀ _ (ne_of_lt hxr')).symm - rw [h2] - exact mul_neg_of_pos_of_neg hx' hxr' - · have hmono : nhdsWithin r (Set.Ioi r) ≤ nhdsWithin r {r}ᶜ := - nhdsWithin_mono r (fun x hx => (ne_of_lt (Set.mem_Ioi.mp hx)).symm) - filter_upwards [hpos.filter_mono hmono, self_mem_nhdsWithin] with x hx hxr - have hx' : 0 < (f.eval x - f.eval r) / (x - r) := by - have := Set.mem_Ioi.mp hx - rwa [slope_def_field] at this - rw [h0, sub_zero] at hx' - have hxr' : 0 < x - r := sub_pos.mpr (Set.mem_Ioi.mp hxr) - have h2 : f.eval x = f.eval x / (x - r) * (x - r) := - (div_mul_cancel₀ _ (ne_of_gt hxr')).symm - rw [h2] - exact mul_pos hx' hxr' + · filter_upwards [hl.eventually_const_lt hd, self_mem_nhdsWithin] with x hx hxr + simp only [slope_def_field, hr, sub_zero] at hx + rcases div_pos_iff.mp hx with ⟨_, h⟩ | ⟨h, _⟩ + · exact False.elim ((sub_neg.mpr hxr).not_gt h) + · exact h + · filter_upwards [hu.eventually_const_lt hd, self_mem_nhdsWithin] with x hx hxr + simp only [slope_def_field, hr, sub_zero] at hx + rcases div_pos_iff.mp hx with ⟨h, _⟩ | ⟨_, h⟩ + · exact h + · exact False.elim ((sub_pos.mpr hxr).not_gt h) /-- **The head-pair flank.** If `s₀` vanishes at `r`, `s₁` does not, and `s₀' = C γ · s₁` with `γ > 0` (the executable seeds: the primitive parts of @@ -1118,7 +1088,7 @@ theorem flank_of_key {s₀ s₁ : Polynomial ℝ} {γ : ℝ} (hγ : 0 < γ) {r : ℝ} (h0 : s₀.eval r = 0) (h1 : s₁.eval r ≠ 0) : (∀ᶠ x in nhdsWithin r (Set.Iio r), (s₀ * s₁).eval x < 0) ∧ (∀ᶠ x in nhdsWithin r (Set.Ioi r), 0 < (s₀ * s₁).eval x) := by - apply eventually_flank_of_deriv_pos + apply sign_near_root · rw [Polynomial.eval_mul, h0, zero_mul] · rw [Polynomial.derivative_mul, Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_mul, h0, zero_mul, add_zero, hkey, Polynomial.eval_mul, @@ -1130,12 +1100,8 @@ theorem flank_of_key {s₀ s₁ : Polynomial ℝ} {γ : ℝ} (hγ : 0 < γ) /-- Coprime polynomials never vanish together. -/ theorem eval_ne_zero_of_isCoprime {a b : Polynomial ℝ} (h : IsCoprime a b) {x : ℝ} (ha : a.eval x = 0) : b.eval x ≠ 0 := by - obtain ⟨u, v, huv⟩ := h - intro hb - have h2 := congrArg (Polynomial.eval x) huv - rw [Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_mul, ha, hb, - mul_zero, mul_zero, add_zero, Polynomial.eval_one] at h2 - exact zero_ne_one h2 + have hc := h.map (evalRingHom x) + simpa [ha, isCoprime_zero_left, isUnit_iff_ne_zero] using hc /-- Unpack an indexed read of the mapped chain into a read of the executable chain. -/ @@ -1166,8 +1132,8 @@ private theorem isSturmChain_of_seeds (s₀ s₁ : Hex.ZPoly) (fuel : ℕ) (γ : ℝ) (hγ : 0 < γ) (hkey : Polynomial.derivative (toPolyℝ s₀) = Polynomial.C γ * toPolyℝ s₁) : Sturm.IsSturmChain (toPolyℝ s₀) ((s₀ :: s₁ :: chainList fuel s₀ s₁).map toPolyℝ) := by - refine { nonempty := by simp, head := rfl, root_flank := ?_, nonzero_mem := ?_, - consec_coprime := ?_, interior_alternates := ?_, last_no_root := ?_ } + refine { head := rfl, root_flank := ?_, nonzero_mem := ?_, + interior_alternates := ?_, last_no_root := ?_ } · -- root_flank intro r hr have hs₁r : (toPolyℝ s₁).eval r ≠ 0 := eval_ne_zero_of_isCoprime hcop hr @@ -1178,12 +1144,6 @@ private theorem isSturmChain_of_seeds (s₀ s₁ : Hex.ZPoly) (fuel : ℕ) rw [List.mem_map] at hq obtain ⟨z, hz, rfl⟩ := hq exact fun hh => chainList_nonzero fuel s₀ s₁ hs₀ hs₁ z hz (toPolyℝ_eq_zero_iff.mp hh) - · -- consec_coprime - intro i x a b ha hb hax - obtain ⟨za, hza, rfl⟩ := getElem?_map_toPolyℝ ha - obtain ⟨zb, hzb, rfl⟩ := getElem?_map_toPolyℝ hb - exact eval_ne_zero_of_isCoprime - (chainList_pairs_coprime fuel s₀ s₁ hs₁ hcop i za zb hza hzb) hax · -- interior_alternates intro i x a b c ha hb hc hbx obtain ⟨za, hza, rfl⟩ := getElem?_map_toPolyℝ ha @@ -1453,15 +1413,15 @@ theorem sturmCount_eq_card_roots (p : Hex.ZPoly) (hp : 1 ≤ p.natDegree) simp only [Hex.DensePoly.degree?_zero_getD] at hp omega have hchain := sturmChain_isSturmChain p hp hsq - have hs₀0 : toPolyℝ (Hex.ZPoly.primitivePart p) ≠ 0 := - fun hh => primitivePart_ne_zero hp0 (toPolyℝ_eq_zero_iff.mp hh) have hsf := squarefree_toPolyℝ_primitivePart p hp0 hsq have hab : Dyadic.toReal I.lower < Dyadic.toReal I.upper := toReal_lt_toReal I.lt - have hkey := Sturm.sturm_half_open hs₀0 hsf hchain hab + have hkey := hchain.sturm_Ioc (Polynomial.nodup_roots + (PerfectField.separable_iff_squarefree.mpr hsf)) hab.le show (Hex.sturmVarAt (Hex.ZPoly.sturmChain p) I.lower : Int) - Hex.sturmVarAt (Hex.ZPoly.sturmChain p) I.upper = _ rw [sturmVarAt_eq, sturmVarAt_eq, roots_toPolyℝ_eq_primitivePart p hp0] - exact hkey + simp only [Set.mem_Ioc] at hkey + omega /-- Casting an integer's sign to `ℝ` preserves `SignType.sign`. -/ private theorem sign_intCast_sign (n : Int) : @@ -1518,10 +1478,9 @@ theorem rootCount_eq_card_roots (p : Hex.ZPoly) (hp : 1 ≤ p.natDegree) simp only [Hex.DensePoly.degree?_zero_getD] at hp omega have hchain := sturmChain_isSturmChain p hp hsq - have hs₀0 : toPolyℝ (Hex.ZPoly.primitivePart p) ≠ 0 := - fun hh => primitivePart_ne_zero hp0 (toPolyℝ_eq_zero_iff.mp hh) have hsf := squarefree_toPolyℝ_primitivePart p hp0 hsq - have hkey := Sturm.sturm_line hs₀0 hsf hchain + have hkey := hchain.sturm (Polynomial.nodup_roots + (PerfectField.separable_iff_squarefree.mpr hsf)) rw [← roots_toPolyℝ_eq_primitivePart p hp0] at hkey show Hex.sturmVarNegInf (Hex.ZPoly.sturmChain p) - Hex.sturmVarPosInf (Hex.ZPoly.sturmChain p) = _ diff --git a/HexRealRootsMathlib/LiteralChain.lean b/HexRealRootsMathlib/LiteralChain.lean index de9cb261b9..8ce9cb8787 100644 --- a/HexRealRootsMathlib/LiteralChain.lean +++ b/HexRealRootsMathlib/LiteralChain.lean @@ -141,17 +141,14 @@ theorem isChain_of_replay {f s₁ : Polynomial ℝ} {rest : List (Polynomial ℝ (hderiv : Polynomial.derivative f = Polynomial.C δ * s₁) : IsSturmChain f (f :: s₁ :: rest) := by have hcop : IsCoprime f s₁ := hrep.first_coprime - refine { nonempty := by simp, head := rfl, root_flank := ?_, nonzero_mem := hnz, - consec_coprime := ?_, interior_alternates := ?_, last_no_root := ?_ } + refine { head := rfl, root_flank := ?_, nonzero_mem := hnz, + interior_alternates := ?_, last_no_root := ?_ } · intro r hr have hs₁r : s₁.eval r ≠ 0 := HexRealRootsMathlib.eval_ne_zero_of_isCoprime hcop hr obtain ⟨hleft, hright⟩ := HexRealRootsMathlib.flank_of_key hδ hderiv hr hs₁r exact ⟨s₁, rfl, hs₁r, hleft, hright⟩ - · intro i x a b ha hb hax - exact HexRealRootsMathlib.eval_ne_zero_of_isCoprime - (hrep.pair_coprime i a b ha hb) hax · intro i x a b c ha hb hc hbx obtain ⟨left, quotient, right, hleft, hright, hrel⟩ := hrep.triple i a b c ha hb hc @@ -306,7 +303,7 @@ end Literal half-open dyadic interval. This reads the supplied chain directly and never calls the executable chain builder. -/ theorem literalCount_eq_card_roots (p : Hex.ZPoly) (chain : Array Hex.ZPoly) - (hp : toPolyℝ p ≠ 0) (hsf : Squarefree (toPolyℝ p)) + (hsf : Squarefree (toPolyℝ p)) (hchain : Sturm.IsSturmChain (toPolyℝ p) (chain.toList.map toPolyℝ)) (I : Hex.DyadicInterval) : (Hex.sturmVarAt chain I.lower : Int) - Hex.sturmVarAt chain I.upper = @@ -314,23 +311,28 @@ theorem literalCount_eq_card_roots (p : Hex.ZPoly) (chain : Array Hex.ZPoly) classical rw [sturmVarAt_eq, sturmVarAt_eq] rw [Literal.rootsIn] - have h := Sturm.sturm_half_open hp hsf hchain (toReal_lt_toReal I.lt) - rw [h] - norm_cast - apply congrArg Multiset.card - apply Multiset.filter_congr - intro x _hx - rfl + have h := hchain.sturm_Ioc (Polynomial.nodup_roots + (PerfectField.separable_iff_squarefree.mpr hsf)) (toReal_lt_toReal I.lt).le + have hf : (toPolyℝ p).roots.filter (Literal.InInterval I) = + (toPolyℝ p).roots.filter (fun r => r ∈ Set.Ioc + (Dyadic.toReal I.lower) (Dyadic.toReal I.upper)) := by + apply Multiset.filter_congr + intro x _ + rfl + rw [hf] + omega /-- A literal chain's variation drop at infinity is the exact total number of real roots. -/ theorem literalRootCount_eq_card_roots (p : Hex.ZPoly) (chain : Array Hex.ZPoly) - (hp : toPolyℝ p ≠ 0) (hsf : Squarefree (toPolyℝ p)) + (hsf : Squarefree (toPolyℝ p)) (hchain : Sturm.IsSturmChain (toPolyℝ p) (chain.toList.map toPolyℝ)) : (Hex.sturmVarNegInf chain : Int) - Hex.sturmVarPosInf chain = (toPolyℝ p).roots.card := by rw [sturmVarNegInf_eq, sturmVarPosInf_eq] - exact Sturm.sturm_line hp hsf hchain + have h := hchain.sturm (Polynomial.nodup_roots + (PerfectField.separable_iff_squarefree.mpr hsf)) + omega /-- A checked integer replay gives the exact literal count on an interval. @@ -346,8 +348,6 @@ theorem ZReplay.count_eq_card_roots {f s₁ : Hex.ZPoly} {rest : List Hex.ZPoly} Hex.sturmVarAt (f :: s₁ :: rest).toArray I.upper = (Literal.rootsIn (toPolyℝ f) I).card := by apply literalCount_eq_card_roots f (f :: s₁ :: rest).toArray - · intro hf - exact hnz f (by simp) (toPolyℝ_eq_zero_iff.mp hf) · exact hrep.squarefree δ hδ hderiv · simpa using hrep.isChain hnz δ hδ hderiv @@ -361,8 +361,6 @@ theorem ZReplay.total_eq_card_roots {f s₁ : Hex.ZPoly} {rest : List Hex.ZPoly} Hex.sturmVarPosInf (f :: s₁ :: rest).toArray = (toPolyℝ f).roots.card := by apply literalRootCount_eq_card_roots f (f :: s₁ :: rest).toArray - · intro hf - exact hnz f (by simp) (toPolyℝ_eq_zero_iff.mp hf) · exact hrep.squarefree δ hδ hderiv · simpa using hrep.isChain hnz δ hδ hderiv diff --git a/HexRealRootsMathlib/README.md b/HexRealRootsMathlib/README.md index d95edb14d7..25bef8e2cf 100644 --- a/HexRealRootsMathlib/README.md +++ b/HexRealRootsMathlib/README.md @@ -33,6 +33,33 @@ example : roots.intervals = #v[((0 : ℚ), (2 : ℚ)), ((2 : ℚ), (4 : ℚ))] := rfl ``` +# Root counts + +For a closed squarefree polynomial over `ℚ` with integer coefficients and positive +degree, `real_root_count` proves the exact number of distinct real roots: + +```lean +import HexRealRootsMathlib.RealRootCount + +open Polynomial + +example : Fintype.card ((X ^ 5 - 4 * X + 2 : ℚ[X]).rootSet ℝ) = 3 := by + real_root_count +``` + +The term form `real_root_count (X ^ 5 - 4 * X + 2 : ℚ[X])` is also available. +Hex proposes a signed remainder chain. Polynomial identities, positive scalar +factors, and sign variations are checked in Lean. A nonzero constant at the end +of the chain certifies separability as well as the root count. + +The general Sturm theorems use only Mathlib types. `Sturm.IsSturmChain.sturm_Ioc` +counts roots on `(a, b]`, including equal endpoints, and `Sturm.IsSturmChain.sturm` +counts roots on the real line. Their hypothesis is that the multiset of real +roots has no duplicates. + +The corresponding Mathlib sources can be checked with +`python3 scripts/check_sturm_sync.py /path/to/mathlib` from `hex-dev`. + # Functionality The input may be a closed `Hex.ZPoly` or a closed integer-coefficient diff --git a/HexRealRootsMathlib/RealRootCount.lean b/HexRealRootsMathlib/RealRootCount.lean new file mode 100644 index 0000000000..3e1ea28901 --- /dev/null +++ b/HexRealRootsMathlib/RealRootCount.lean @@ -0,0 +1,170 @@ +/- +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 HexRealRootsMathlib.SturmCertificate +public import Mathlib.Tactic.ComputeDegree +public import Mathlib.Tactic.NormNum +public import HexPolyZMathlib.PolyParse +public meta import HexPolyZMathlib.PolyParse +public meta import HexRealRoots.Chain +public meta import HexPoly.Euclid.DivGcd + +/-! +# Certified real root counts + +`by real_root_count` proves a goal `Fintype.card (p.rootSet ℝ) = n`. +The term form `real_root_count (p : ℚ[X])` proves `Fintype.card (p.rootSet ℝ) = n` for a closed, +squarefree polynomial of positive degree with integer coefficients. Hex proposes +a signed remainder chain; `ring`, `compute_degree`, and `norm_num` check its +identities, nonvanishing, and signs. No correctness assumption about the generator +or its polynomial representation enters the proof. +-/ + +public meta section + +namespace HexRealRootsMathlib.RealRootCount + +open Lean Meta Elab Term + +private def intTerm (z : Int) : TermElabM (TSyntax `term) := do + let n := Syntax.mkNumLit (toString z.natAbs) + if z < 0 then `(-$n) else `($n) + +private def polyTerm (cs : Array Int) : TermElabM (TSyntax `term) := do + let mut sum : Option (TSyntax `term) := none + for i in [:cs.size] do + if cs[i]! != 0 then + let c ← intTerm cs[i]! + let k := Syntax.mkNumLit (toString i) + let monomial ← if i == 0 then `(($c : Polynomial ℝ)) + else `(($c : Polynomial ℝ) * Polynomial.X ^ $k) + sum ← match sum with + | none => pure (some monomial) + | some t => some <$> `($t + $monomial) + return sum.getD (← `((0 : Polynomial ℝ))) + +/-- Coefficients of `C left * p = quotient * q - C right * r`. -/ +private structure RemainderIdentity where + left : Int + quotient : Array Int + right : Int + +/-- Divide over `ℚ`, then clear denominators to obtain an integer identity. +The generated proof checks both the identity and positivity of the two factors. -/ +private def remainderIdentity (p q r : Array Int) : RemainderIdentity := Id.run do + let toRat := Hex.DensePoly.ofCoeffs ∘ Array.map (fun (c : Int) => (c : Rat)) + let (quotient, remainder) := Hex.DensePoly.divMod (toRat p) (toRat q) + let right := -remainder.coeff (r.size - 1) / (r.back! : Rat) + let left := quotient.coeffs.foldl (fun n c => n.lcm c.den) right.den + return ⟨left, quotient.coeffs.map (fun c => (c * (left : Rat)).num), + (right * (left : Rat)).num⟩ + +private def variations (xs : Array Int) : Nat := Id.run do + let mut last := 0 + let mut n := 0 + for x in xs do + if x != 0 then + if last * x < 0 then n := n + 1 + last := x + return n + +private def emit (pStx : TSyntax `term) (p : Hex.ZPoly) + (unfolds : Array (TSyntax ``Parser.Tactic.simpLemma)) : TermElabM (TSyntax `term) := do + let _ : Inhabited Hex.ZPoly := ⟨Hex.DensePoly.C 0⟩ + if p.isZero then + throwError "real_root_count: expected a nonzero polynomial" + if p.size == 1 then + throwError "real_root_count: expected a polynomial of positive degree" + let polys := Hex.ZPoly.sturmChain p + if polys.size < 2 || polys.back!.size != 1 then + throwError "real_root_count: expected a squarefree polynomial" + -- The generator removes positive content from its first entry. Use the original + -- polynomial here, so the final transport only checks coefficient arithmetic. + let cs := (polys.set! 0 p).map (·.coeffs) + let ps ← cs.mapM polyTerm + let mut facts : Array (TSyntax `tactic) := #[] + let mut nonzeros : Array (TSyntax `term) := #[] + -- Record degree, leading coefficient, and nonvanishing once per entry. + for i in [:ps.size] do + let t := ps[i]! + let d := Syntax.mkNumLit (toString (cs[i]!.size - 1)) + let c ← intTerm cs[i]!.back! + let hd := mkIdent (← mkFreshUserName `degree) + let hc := mkIdent (← mkFreshUserName `coeff) + let hl := mkIdent (← mkFreshUserName `leadingCoeff) + let hn := mkIdent (← mkFreshUserName `nonzero) + facts := facts.push (← `(tactic| have $hd : ($t).natDegree = $d := by compute_degree!)) + facts := facts.push (← `(tactic| have $hc : ($t).coeff $d = $c := by compute_degree!)) + facts := facts.push (← `(tactic| have $hl : ($t).leadingCoeff = $c := by + rw [Polynomial.leadingCoeff, $hd:term]; exact $hc)) + facts := facts.push (← `(tactic| have $hn : $t ≠ 0 := by + apply Polynomial.leadingCoeff_ne_zero.mp + rw [$hl:term] + norm_num)) + nonzeros := nonzeros.push (← `($hn)) + let m := ps.size + let c ← intTerm cs.back!.back! + let mut cert ← `(show Sturm.RemainderChain [$(ps[m - 2]!), $(ps[m - 1]!)] from by + convert Sturm.RemainderChain.pair $(nonzeros[m - 2]!) + (show ($c : ℝ) ≠ 0 by norm_num) using 1 <;> norm_num) + for k in [:m - 2] do + let i := m - 3 - k + let identity := remainderIdentity cs[i]! cs[i + 1]! cs[i + 2]! + let a ← intTerm identity.left + let b ← intTerm identity.right + let d ← polyTerm identity.quotient + cert ← `(Sturm.RemainderChain.cons (d := $d) $cert $(nonzeros[i]!) + (show (0 : ℝ) < $a by norm_num) (show (0 : ℝ) < $b by norm_num) + (by norm_num [map_ofNat] <;> ring)) + let a ← intTerm ((p.coeff (p.size - 1) * (p.size - 1 : Nat)) / cs[1]!.back!) + let pos := variations (cs.map Array.back!) + let neg := variations (cs.map fun c => c.back! * (-1) ^ (c.size - 1)) + let n := Syntax.mkNumLit (toString (neg - pos)) + `(by + $facts:tactic* + exact Sturm.RemainderChain.card_rootSet (f := $pStx) (n := $n) $cert + (show (0 : ℝ) < $a by norm_num) + (by simp [Polynomial.derivative_add, Polynomial.derivative_mul, + Polynomial.derivative_pow, map_ofNat] <;> ring) + (by norm_num [map_ofNat, $unfolds,*] <;> ring) + (by simp only [Sturm.sturmVarNegInf, Sturm.sturmVarPosInf, + List.map_cons, List.map_nil, *] + norm_num [Sturm.signVariations, Sturm.countSignChanges])) + +/-- Compute and certify the number of distinct real roots of a closed squarefree +integer-coefficient polynomial over `ℚ` of positive degree. -/ +elab "real_root_count " pStx:term : term <= expectedType? => withRef pStx do + let pTy ← elabType (← `(Polynomial ℚ)) + let e ← elabTermEnsuringType pStx pTy + synthesizeSyntheticMVarsNoPostponing + let e ← instantiateMVars e + if e.hasFVar || e.hasExprMVar then + throwError "real_root_count: expected a closed polynomial" + let names ← IO.mkRef (#[] : Array Name) + let p ← HexPolyZMathlib.PolyParse.parsePoly "real_root_count" true 16 e + (fun n => names.modify (fun ns => if ns.contains n then ns else ns.push n)) + let unfolds ← (← names.get).mapM fun n => `(Parser.Tactic.simpLemma| $(mkIdent n):term) + elabTermEnsuringType (← emit pStx p unfolds) expectedType? + +/-- Prove a goal `Fintype.card (p.rootSet ℝ) = n` by a checked Sturm chain. +The polynomial must be closed, squarefree, of positive degree, and have integer coefficients. -/ +elab "real_root_count" : tactic => do + let goal ← Tactic.getMainGoal + let target ← instantiateMVars (← goal.getType) + let some (_, lhs, _) := target.eq? | + throwError "real_root_count: expected a goal `Fintype.card (p.rootSet ℝ) = n`" + unless lhs.isAppOf ``Fintype.card do + throwError "real_root_count: expected a goal `Fintype.card (p.rootSet ℝ) = n`" + let some roots := lhs.getAppArgs[0]!.find? (·.isAppOf ``Polynomial.rootSet) | + throwError "real_root_count: expected a goal `Fintype.card (p.rootSet ℝ) = n`" + let p ← PrettyPrinter.delab roots.getAppArgs[2]! + let proof ← elabTermEnsuringType (← `(real_root_count $p)) (some target) + goal.assign proof + Tactic.replaceMainGoal [] + +end HexRealRootsMathlib.RealRootCount diff --git a/HexRealRootsMathlib/RealRootCountTests.lean b/HexRealRootsMathlib/RealRootCountTests.lean new file mode 100644 index 0000000000..1fcc58d315 --- /dev/null +++ b/HexRealRootsMathlib/RealRootCountTests.lean @@ -0,0 +1,73 @@ +import HexRealRootsMathlib.RealRootCount + +open Polynomial + +example : Fintype.card ((X ^ 5 - 4 * X + 2 : ℚ[X]).rootSet ℝ) = 3 := + real_root_count (X ^ 5 - 4 * X + 2 : ℚ[X]) + +example : Fintype.card ((X ^ 4 + X + 1 : ℚ[X]).rootSet ℝ) = 0 := + real_root_count (X ^ 4 + X + 1 : ℚ[X]) + +example : Fintype.card ((-2 * X ^ 3 + 8 * X : ℚ[X]).rootSet ℝ) = 3 := + real_root_count (-2 * X ^ 3 + 8 * X : ℚ[X]) + +example : Fintype.card ((6 * X - 3 : ℚ[X]).rootSet ℝ) = 1 := + real_root_count (6 * X - 3 : ℚ[X]) + +noncomputable def testPolynomial : ℚ[X] := X ^ 3 - 2 + +example : Fintype.card (testPolynomial.rootSet ℝ) = 1 := + real_root_count testPolynomial + +noncomputable def nestedPolynomial : ℚ[X] := testPolynomial * (X ^ 2 + 1) + +example : Fintype.card (nestedPolynomial.rootSet ℝ) = 1 := + real_root_count nestedPolynomial + +example : Fintype.card ((X ^ 2 - C 3 : ℚ[X]).rootSet ℝ) = 2 := + real_root_count (X ^ 2 - C 3 : ℚ[X]) + +example : Fintype.card ((X ^ 3 - 2 : ℚ[X]).rootSet ℝ) = 1 := + real_root_count (let p : ℚ[X] := X ^ 3; p - 2) + +example : Fintype.card ((X ^ 6 - 1000000 : ℚ[X]).rootSet ℝ) = 2 := + real_root_count (X ^ 6 - 1000000 : ℚ[X]) + +/-- error: real_root_count: expected a squarefree polynomial -/ +#guard_msgs in +example := real_root_count ((X - 1) ^ 2 : ℚ[X]) + +/-- error: real_root_count: expected a nonzero polynomial -/ +#guard_msgs in +example := real_root_count (0 : ℚ[X]) + +/-- error: real_root_count: expected a polynomial of positive degree -/ +#guard_msgs in +example := real_root_count (2 : ℚ[X]) + +/-- +error: real_root_count: non-integer coefficient + 1 / 2 +-/ +#guard_msgs in +example := real_root_count (X + C (1 / 2) : ℚ[X]) + +/-- error: real_root_count: expected a closed polynomial -/ +#guard_msgs in +example (p : ℚ[X]) := real_root_count p + +-- A valid certificate must still prove the count requested by the caller. +example : True := by + fail_if_success have : Fintype.card ((X ^ 2 - 1 : ℚ[X]).rootSet ℝ) = 1 := + real_root_count (X ^ 2 - 1 : ℚ[X]) + trivial + +example : Fintype.card ((X ^ 5 - 4 * X + 2 : ℚ[X]).rootSet ℝ) = 3 := by + real_root_count + +example : Fintype.card (nestedPolynomial.rootSet ℝ) = 1 := by + real_root_count + +/-- error: real_root_count: expected a goal `Fintype.card (p.rootSet ℝ) = n` -/ +#guard_msgs in +example : True := by real_root_count diff --git a/HexRealRootsMathlib/SPEC/hex-real-roots-mathlib.md b/HexRealRootsMathlib/SPEC/hex-real-roots-mathlib.md index fcb850e55a..f92699241c 100644 --- a/HexRealRootsMathlib/SPEC/hex-real-roots-mathlib.md +++ b/HexRealRootsMathlib/SPEC/hex-real-roots-mathlib.md @@ -162,8 +162,8 @@ derivative flanks, and exclusion of a common zero. The finite-point bridge `sturmVarAt_eq` and the infinity bridges `sturmVarNegInf_eq` / `sturmVarPosInf_eq` are public for an arbitrary -literal `Array ZPoly`. Together with `Sturm.sturm_half_open` and -`Sturm.sturm_line`, they turn literal executable variation reads into +literal `Array ZPoly`. Together with `Sturm.IsSturmChain.sturm_Ioc` and +`Sturm.IsSturmChain.sturm`, they turn literal executable variation reads into root counts without calling `ZPoly.sturmCount` or `ZPoly.rootCount`. The `ZReplay.count_eq_card_roots` and `ZReplay.total_eq_card_roots` corollaries perform the list-to-array alignment and compose replay, squarefreeness, and @@ -584,12 +584,38 @@ Status and boundaries: against `Polynomial ℝ`/`ℂ` with no `HexRealRoots` dependence, ready as a Mathlib contribution in its own right. +## Root-count certificates over Mathlib polynomials + +`SturmCertificate` checks signed remainder identities over `Polynomial ℝ`. +`Sturm.RemainderChain.pair` terminates a certificate at a nonzero constant; +`Sturm.RemainderChain.cons` prepends a positive scaled remainder identity. +The derivative relation gives `RemainderChain.isSturmChain` and +`RemainderChain.separable` separately. `RemainderChain.card_rootSet` works for +any coefficient ring equipped with an algebra map into `ℝ`. + +`RealRootCount` provides the tactic `by real_root_count` and the term elaborator +`real_root_count p`. Both accept closed squarefree integer-coefficient +polynomials over `ℚ` of positive degree. The generator and rational division +run at elaboration time; the emitted proof checks polynomial identities, +nonvanishing, positivity, and the natural-number variation count. + +The generic Sturm statements, certificate checker, polynomial parser, and +root-count elaborator agree with their Mathlib counterparts after module-path, +parser-namespace, and documentation-markup translation. Run +`python3 scripts/check_sturm_sync.py /path/to/mathlib` to check that agreement. +Once the pinned Mathlib release contains the development, these companion +modules can re-export the corresponding Mathlib modules. + ## File organisation ``` HexRealRootsMathlib/ SturmChainDefs.lean -- IsSturmChain, sturmVar over Polynomial ℝ SturmTheorem.lean -- the counting theorem and the line form + SturmCertificate.lean -- certificates over Mathlib polynomials + RealRootCount.lean -- checked root-count tactic and term elaborator + SturmTests.lean -- endpoint conventions and constant chains + RealRootCountTests.lean -- root counts and elaborator diagnostics ChainCorrespond.lean -- executable-chain correspondence and the shared recurrence/cast helpers; sturmCount_eq_card_roots; compatibility aliases for HexPolyZMathlib.Squarefree diff --git a/HexRealRootsMathlib/SturmCertificate.lean b/HexRealRootsMathlib/SturmCertificate.lean new file mode 100644 index 0000000000..13133ee0bd --- /dev/null +++ b/HexRealRootsMathlib/SturmCertificate.lean @@ -0,0 +1,190 @@ +/- +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 HexRealRootsMathlib.SturmTheorem +public import Mathlib.FieldTheory.Separable +public import Mathlib.Analysis.Calculus.Deriv.Polynomial +public import Mathlib.Analysis.Calculus.Deriv.Slope +public import Mathlib.Tactic.Ring + +/-! +# Algebraic certificates for Sturm chains + +A signed remainder chain ending in a nonzero constant certifies a real root count. +The certificate consists of polynomial identities and positive scalar factors; +its correctness is independent of how the chain was found. + +## Main results + +* `Sturm.RemainderChain.pair` and `Sturm.RemainderChain.cons` build certificates. +* `Sturm.RemainderChain.isSturmChain` verifies the derivative relation. +* `Sturm.RemainderChain.separable` proves that the first entry is separable. +* `Sturm.RemainderChain.card_rootSet` counts the distinct real roots. +-/ + +public section + +noncomputable section + +open Polynomial Filter Topology + +namespace Sturm + +private theorem coprime_of_remainder {p q r : ℝ[X]} {a b : ℝ} {d : ℝ[X]} + (hb : b ≠ 0) (hid : C a * p = d * q - C b * r) (h : IsCoprime q r) : + IsCoprime p q := by + apply IsCoprime.of_mul_left_right (x := C a) + rw [hid, IsCoprime.mul_sub_right_left_iff, + isCoprime_mul_unit_left_left (isUnit_C.mpr (isUnit_iff_ne_zero.mpr hb))] + exact h.symm + +private theorem sign_near_root {p : ℝ[X]} {r : ℝ} + (hr : p.eval r = 0) (hd : 0 < p.derivative.eval r) : + (∀ᶠ x in 𝓝[<] r, p.eval x < 0) ∧ (∀ᶠ x in 𝓝[>] r, 0 < p.eval x) := by + obtain ⟨hl, hu⟩ := hasDerivAt_iff_tendsto_slope_left_right.mp (p.hasDerivAt r) + constructor + · filter_upwards [hl.eventually_const_lt hd, self_mem_nhdsWithin] with x hx hxr + simp only [slope_def_field, hr, sub_zero] at hx + rcases div_pos_iff.mp hx with ⟨_, h⟩ | ⟨h, _⟩ + · exact False.elim ((sub_neg.mpr hxr).not_gt h) + · exact h + · filter_upwards [hu.eventually_const_lt hd, self_mem_nhdsWithin] with x hx hxr + simp only [slope_def_field, hr, sub_zero] at hx + rcases div_pos_iff.mp hx with ⟨h, _⟩ | ⟨_, h⟩ + · exact h + · exact False.elim ((sub_pos.mpr hxr).not_gt h) + +/-- The product of the first two entries changes from negative to positive +at a root of the first entry. -/ +private theorem mul_sign_near_root {s₀ s₁ : Polynomial ℝ} {γ : ℝ} (hγ : 0 < γ) + (hkey : Polynomial.derivative s₀ = Polynomial.C γ * s₁) + {r : ℝ} (h0 : s₀.eval r = 0) (h1 : s₁.eval r ≠ 0) : + (∀ᶠ x in nhdsWithin r (Set.Iio r), (s₀ * s₁).eval x < 0) ∧ + (∀ᶠ x in nhdsWithin r (Set.Ioi r), 0 < (s₀ * s₁).eval x) := by + apply sign_near_root + · rw [Polynomial.eval_mul, h0, zero_mul] + · rw [Polynomial.derivative_mul, Polynomial.eval_add, Polynomial.eval_mul, + Polynomial.eval_mul, h0, zero_mul, add_zero, hkey, Polynomial.eval_mul, + Polynomial.eval_C, mul_assoc] + exact mul_pos hγ (mul_self_pos.mpr h1) + +/-- Coprime polynomials never vanish together. -/ +private theorem eval_ne_zero_of_isCoprime {a b : Polynomial ℝ} (h : IsCoprime a b) + {x : ℝ} (ha : a.eval x = 0) : b.eval x ≠ 0 := by + have hc := h.map (evalRingHom x) + simpa [ha, isCoprime_zero_left, isUnit_iff_ne_zero] using hc + +/-- The algebraic conditions on a signed remainder chain, before checking its seeds. -/ +structure RemainderChain (chain : List ℝ[X]) : Prop where + /-- Every entry is a nonzero polynomial. -/ + nonzero_mem : ∀ p ∈ chain, p ≠ 0 + /-- Consecutive entries are coprime. -/ + coprime : ∀ i a b, chain[i]? = some a → chain[i + 1]? = some b → IsCoprime a b + /-- Neighbors of a vanishing interior entry have opposite signs. -/ + interior_alternates : ∀ i x a b c, chain[i]? = some a → chain[i + 1]? = some b → + chain[i + 2]? = some c → b.eval x = 0 → + a.eval x ≠ 0 ∧ c.eval x ≠ 0 ∧ a.eval x * c.eval x < 0 + /-- The last entry has no real roots. -/ + last_no_root : ∀ p, chain.getLast? = some p → ∀ x, p.eval x ≠ 0 + +/-- Terminate a certificate at a nonzero constant. -/ +theorem RemainderChain.pair {p : ℝ[X]} {c : ℝ} (hp : p ≠ 0) (hc : c ≠ 0) : + RemainderChain [p, C c] where + nonzero_mem := by simp_all + coprime := by + intro i a b ha hb + cases i with + | zero => + simp only [List.getElem?_cons_zero, Option.some.injEq] at ha + subst a + simp only [Nat.zero_add, List.getElem?_cons_succ, List.getElem?_cons_zero, + Option.some.injEq] at hb + subst b + refine ⟨0, C c⁻¹, ?_⟩ + simp [← C_mul, hc] + | succ i => cases i <;> simp at hb + interior_alternates := by + intro i x a b d ha hb hd + cases i <;> simp at hd + last_no_root := by simp_all + +/-- Prepend a positive multiple of a signed remainder identity. -/ +theorem RemainderChain.cons {p q r : ℝ[X]} {tail : List ℝ[X]} {a b : ℝ} + {d : ℝ[X]} (h : RemainderChain (q :: r :: tail)) (hp : p ≠ 0) + (ha : 0 < a) (hb : 0 < b) (hid : C a * p = d * q - C b * r) : + RemainderChain (p :: q :: r :: tail) where + nonzero_mem := by simpa only [List.mem_cons, forall_eq_or_imp] using And.intro hp h.nonzero_mem + coprime := by + intro i u v hu hv + cases i with + | zero => + simp only [List.getElem?_cons_zero, Option.some.injEq] at hu + simp only [Nat.zero_add, List.getElem?_cons_succ, List.getElem?_cons_zero, + Option.some.injEq] at hv + subst u; subst v + exact coprime_of_remainder (ne_of_gt hb) hid (h.coprime 0 q r rfl rfl) + | succ i => exact h.coprime i u v hu hv + interior_alternates := by + intro i x u v w hu hv hw hv0 + cases i with + | zero => + simp only [List.getElem?_cons_zero, Option.some.injEq] at hu + simp only [Nat.zero_add, List.getElem?_cons_succ, List.getElem?_cons_zero, + Option.some.injEq] at hv hw + subst u; subst v; subst w + have hr := eval_ne_zero_of_isCoprime (h.coprime 0 q r rfl rfl) hv0 + have he := congrArg (Polynomial.eval x) hid + simp only [eval_mul, eval_C, eval_sub, hv0, mul_zero, zero_sub] at he + have hpr : p.eval x * r.eval x < 0 := by + have hs : 0 < r.eval x * r.eval x := mul_self_pos.mpr hr + apply (mul_lt_mul_iff_right₀ ha).mp + calc a * (p.eval x * r.eval x) = -(b * (r.eval x * r.eval x)) := by + rw [← mul_assoc, he] + ring + _ < a * 0 := by simpa using neg_neg_of_pos (mul_pos hb hs) + exact ⟨fun hz => by simp [hz] at hpr, hr, hpr⟩ + | succ i => exact h.interior_alternates i x u v w hu hv hw hv0 + last_no_root := by simpa using h.last_no_root + +/-- A remainder chain starting with a positive multiple of the derivative is a Sturm chain. -/ +theorem RemainderChain.isSturmChain {p q : ℝ[X]} {tail : List ℝ[X]} {a : ℝ} + (h : RemainderChain (p :: q :: tail)) (ha : 0 < a) + (hd : derivative p = C a * q) : IsSturmChain p (p :: q :: tail) where + head := rfl + root_flank := by + intro x hx + have hq := eval_ne_zero_of_isCoprime (h.coprime 0 p q rfl rfl) hx + exact ⟨q, rfl, hq, mul_sign_near_root ha hd hx hq⟩ + nonzero_mem := h.nonzero_mem + interior_alternates := h.interior_alternates + last_no_root := h.last_no_root + +/-- A remainder chain whose second entry is a nonzero multiple of the derivative +certifies separability. -/ +theorem RemainderChain.separable {p q : ℝ[X]} {tail : List ℝ[X]} {a : ℝ} + (h : RemainderChain (p :: q :: tail)) (ha : a ≠ 0) + (hd : derivative p = C a * q) : p.Separable := by + rw [separable_def, hd, isCoprime_mul_unit_left_right + (isUnit_C.mpr (isUnit_iff_ne_zero.mpr ha))] + exact h.coprime 0 p q rfl rfl + +/-- Convert the variation count of a checked chain to the number of distinct real roots. -/ +theorem RemainderChain.card_rootSet {R : Type*} [CommRing R] [Algebra R ℝ] + {f : R[X]} {p q : ℝ[X]} {tail : List ℝ[X]} + {a : ℝ} {n : ℕ} (h : RemainderChain (p :: q :: tail)) (ha : 0 < a) + (hd : derivative p = C a * q) (hf : f.map (algebraMap R ℝ) = p) + (hn : sturmVarPosInf (p :: q :: tail) + n = sturmVarNegInf (p :: q :: tail)) : + Fintype.card (f.rootSet ℝ) = n := by + classical + have hs := h.separable (ne_of_gt ha) hd + have hc := (h.isSturmChain ha hd).sturm (Polynomial.nodup_roots hs) + simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe, aroots_def, hf] + rw [Multiset.toFinset_card_of_nodup (Polynomial.nodup_roots hs)] + omega + +end Sturm diff --git a/HexRealRootsMathlib/SturmChainDefs.lean b/HexRealRootsMathlib/SturmChainDefs.lean index c0f8670613..47fe43cd8b 100644 --- a/HexRealRootsMathlib/SturmChainDefs.lean +++ b/HexRealRootsMathlib/SturmChainDefs.lean @@ -6,24 +6,32 @@ Authors: Kim Morrison module -public import Mathlib - -public section +public import Mathlib.Data.Sign.Basic +public import Mathlib.Algebra.Polynomial.Eval.Defs +public import Mathlib.Algebra.Polynomial.Degree.Defs +public import Mathlib.Topology.Instances.Real.Lemmas /-! -Definitions supporting Sturm's theorem over `Polynomial ℝ`. +# Sturm chains and sign variations + +The number of sign variations in a list is the number of adjacent opposite signs +remaining after zero entries are removed. For example, `[1, 0, -1]` has one +sign variation. -This module defines the zero-skipping sign-variation count `Sturm.sturmVar` -of a chain of real polynomials at a point, and the predicate -`Sturm.IsSturmChain` capturing the sign axioms that the root-counting -argument uses. Nothing here refers to any `HexRealRoots` executable type; the -definitions are stated directly over `Polynomial ℝ`. +`Sturm.sturmVar` applies this count to the evaluations of a list of real +polynomials. `Sturm.IsSturmChain` records the local sign conditions used in +Sturm's theorem. The chain need not be produced by Euclidean division. -The zero-skipping convention: the variation count of a sign pattern such as -`(+, 0, −)` is `1`. Concretely we drop the zero evaluations and count the -adjacent pairs of opposite sign among what remains. +## Main definitions + +* `Sturm.signVariations`: sign variations with zero entries removed. +* `Sturm.sturmVar`: sign variations of polynomial evaluations at a real point. +* `Sturm.sturmVarPosInf` and `Sturm.sturmVarNegInf`: sign variations at infinity. +* `Sturm.IsSturmChain`: the local sign conditions for a generalized Sturm chain. -/ +public section + open Filter Topology namespace Sturm @@ -56,14 +64,11 @@ noncomputable def signVariations (l : List ℝ) : ℕ := @[simp] theorem signVariations_nil : signVariations [] = 0 := rfl /-- Prepending a zero entry does not change the sign variations. -/ -theorem signVariations_cons_zero (l : List ℝ) : +@[simp] theorem signVariations_cons_zero (l : List ℝ) : signVariations (0 :: l) = signVariations l := by simp [signVariations] -/-- Prepending a nonzero entry `a` to a list whose first surviving entry has -the same sign as `a` (or which becomes empty after dropping zeros) is -governed by `countSignChanges`; this unfolding lemma exposes the recursion to -downstream local-sign arguments. -/ +/-- A nonzero first entry survives removal of zero entries. -/ theorem signVariations_cons_ne (a : ℝ) (l : List ℝ) (ha : a ≠ 0) : signVariations (a :: l) = countSignChanges (a :: l.filter (fun v => decide (v ≠ 0))) := by @@ -98,13 +103,11 @@ theorem countSignChanges_congr {l₁ l₂ : List ℝ} rw [countSignChanges_cons_cons, countSignChanges_cons_cons] have hiff : (a * c < 0) ↔ (b * d < 0) := by rw [← sign_eq_neg_one_iff, ← sign_eq_neg_one_iff, sign_mul, sign_mul, hab, hcd] - by_cases hc : a * c < 0 - · rw [ite_eq_left hc, ite_eq_left (hiff.mp hc), ih] - · rw [ite_eq_right hc, ite_eq_right (fun h => hc (hiff.mpr h)), ih] + simp only [hiff, ih] /-- Dropping the zero entries commutes with a pointwise sign-equal correspondence: the filtered lists remain pointwise sign-equal. -/ -theorem filter_ne_zero_congr {l₁ l₂ : List ℝ} +private theorem filter_ne_zero_congr {l₁ l₂ : List ℝ} (h : List.Forall₂ (fun u v => SignType.sign u = SignType.sign v) l₁ l₂) : List.Forall₂ (fun u v => SignType.sign u = SignType.sign v) (l₁.filter (fun v => decide (v ≠ 0))) (l₂.filter (fun v => decide (v ≠ 0))) := by @@ -114,18 +117,9 @@ theorem filter_ne_zero_congr {l₁ l₂ : List ℝ} have hzero : (a = 0) ↔ (b = 0) := by rw [← sign_eq_zero_iff (a := a), ← sign_eq_zero_iff (a := b), hab] by_cases ha : a = 0 - · have hb : b = 0 := hzero.mp ha - have e1 : (a :: l₁').filter (fun v => decide (v ≠ 0)) - = l₁'.filter (fun v => decide (v ≠ 0)) := by rw [List.filter_cons]; simp [ha] - have e2 : (b :: l₂').filter (fun v => decide (v ≠ 0)) - = l₂'.filter (fun v => decide (v ≠ 0)) := by rw [List.filter_cons]; simp [hb] - rw [e1, e2]; exact ih - · have hb : b ≠ 0 := fun h => ha (hzero.mpr h) - have e1 : (a :: l₁').filter (fun v => decide (v ≠ 0)) - = a :: l₁'.filter (fun v => decide (v ≠ 0)) := by rw [List.filter_cons]; simp [ha] - have e2 : (b :: l₂').filter (fun v => decide (v ≠ 0)) - = b :: l₂'.filter (fun v => decide (v ≠ 0)) := by rw [List.filter_cons]; simp [hb] - rw [e1, e2]; exact List.Forall₂.cons hab ih + · simpa [ha, hzero.mp ha] using ih + · simpa [ha, mt hzero.mpr ha] using + List.Forall₂.cons (R := fun u v : ℝ => SignType.sign u = SignType.sign v) hab ih /-- `signVariations` reads only the signs of the entries: two real lists whose entries are pointwise sign-equal have equal sign variations. -/ @@ -158,7 +152,7 @@ private theorem sign_mul_eq_neg_one {a b : ℝ} : /-- Prepending a nonzero entry `a` adds one variation exactly when its sign is opposite the sign of the next surviving entry. -/ -theorem signVariations_cons_pos {a : ℝ} (l : List ℝ) (ha : a ≠ 0) : +theorem signVariations_cons {a : ℝ} (l : List ℝ) (ha : a ≠ 0) : signVariations (a :: l) = (firstSign l).elim 0 (fun t => if SignType.sign a * t = -1 then 1 else 0) + signVariations l := by @@ -176,86 +170,32 @@ theorem signVariations_cons_pos {a : ℝ} (l : List ℝ) (ha : a ≠ 0) : ← signVariations_cons_ne b l' hb] simp only [Option.elim_some] congr 1 - by_cases hlt : a * b < 0 - · rw [ite_eq_left hlt, ite_eq_left (sign_mul_eq_neg_one.mpr hlt)] - · rw [ite_eq_right hlt, ite_eq_right (fun h => hlt (sign_mul_eq_neg_one.mp h))] - -/-- A local sign-pattern relation between two real lists: they agree entry by -entry except that a nonzero entry flanked by two opposite-sign neighbours may -collapse to `0`. Such a collapse is variation-neutral, so `signVariations` and -the leading sign are preserved (`SVRel.signVariations_eq`). -/ -inductive SVRel : List ℝ → List ℝ → Prop - | nil : SVRel [] [] - | same {x y : ℝ} {l m : List ℝ} (hx : x ≠ 0) (hy : y ≠ 0) - (hs : SignType.sign x = SignType.sign y) (h : SVRel l m) : - SVRel (x :: l) (y :: m) - | collapse {x X x' : ℝ} {l m : List ℝ} {y y' : ℝ} - (hx : x ≠ 0) (hX : X ≠ 0) (hy' : y' ≠ 0) - (hsx : SignType.sign x = SignType.sign x') - (hsy : SignType.sign y = SignType.sign y') - (hopp : SignType.sign x * SignType.sign y = -1) - (h : SVRel (y :: l) (y' :: m)) : - SVRel (x :: X :: y :: l) (x' :: 0 :: y' :: m) - -private theorem svrel_flank_arith (u v w : SignType) (huw : u * w = -1) (hv : v ≠ 0) : - (if u * v = -1 then (1 : ℕ) else 0) + (if v * w = -1 then 1 else 0) = 1 := by - revert huw hv; revert u v w; decide - -/-- The core combinatorial fact: an `SVRel`-related pair of lists has equal -sign variations and equal leading sign. -/ -theorem SVRel.signVariations_eq {L M : List ℝ} (h : SVRel L M) : - signVariations L = signVariations M ∧ firstSign L = firstSign M := by - induction h with - | nil => exact ⟨rfl, rfl⟩ - | @same x y l m hx hy hs h ih => - refine ⟨?_, ?_⟩ - · rw [signVariations_cons_pos l hx, signVariations_cons_pos m hy, ih.1, ih.2, hs] - · rw [firstSign_cons_ne l hx, firstSign_cons_ne m hy, hs] - | @collapse x X x' l m y y' hx hX hy' hsx hsy hopp h ih => - have hy : y ≠ 0 := by - intro hy0; rw [hy0, sign_zero, mul_zero] at hopp; exact absurd hopp (by decide) - have hx' : x' ≠ 0 := by - intro hx0; rw [hx0, sign_zero] at hsx; exact hx (sign_eq_zero_iff.mp hsx) - refine ⟨?_, ?_⟩ - · -- signVariations L - rw [signVariations_cons_pos (X :: y :: l) hx, - firstSign_cons_ne (y :: l) hX, signVariations_cons_pos (y :: l) hX, - firstSign_cons_ne l hy] - rw [signVariations_cons_pos (0 :: y' :: m) hx', - firstSign_cons_zero (y' :: m) rfl, firstSign_cons_ne m hy', - signVariations_cons_zero] - simp only [Option.elim_some] - rw [← add_assoc, ih.1] - congr 1 - rw [← hsx, ← hsy, ite_eq_left hopp] - exact svrel_flank_arith _ _ _ hopp (fun h => hX (sign_eq_zero_iff.mp h)) - · rw [firstSign_cons_ne (X :: y :: l) hx, firstSign_cons_ne (0 :: y' :: m) hx', hsx] - -/-- A generalised Sturm chain for `p`: the sign axioms that the counting -argument actually uses, packaged as explicit fields. The chain is stored as -a plain `List (Polynomial ℝ)` and elements are addressed by index through -{name}`getElem?`, so no length lower bound is baked in (a nonzero constant `p` has -the one-element chain `[p]`). - -The fields are: - -* `nonempty` / `head` — the chain is nonempty and its head is `p`; -* `root_flank` — at every real root `r` of `p` there is a second element - `q` (`chain[1] = q`), nonzero at `r`, with `p * q` negative on a punctured - left neighbourhood of `r` and positive on a punctured right neighbourhood. - Phrasing the second element existentially forbids the degenerate witness in - which `p` has a root but the chain has no derivative-like second entry; -* `nonzero_mem` — no chain element is the zero polynomial, so each element - has finitely many zeros and the counting theorem's telescope over the - chain's zeros is finite; -* `consec_coprime` — consecutive elements never vanish at a common point; -* `interior_alternates` — when an interior element (one with both neighbours - present) vanishes at a point, both neighbours are nonzero there and have - opposite signs, so the local pattern is `(±, 0, ∓)`; -* `last_no_root` — the last element has no real zero. -/ + simp only [sign_mul_eq_neg_one] + +/-- Sign variations of the chain at `+∞`: the sign of each element there is the +sign of its leading coefficient, so this is the zero-skipping variation count +of the leading coefficients. The zero polynomial contributes leading +coefficient `0`, which the zero-skipping convention drops. -/ +@[expose] +noncomputable def sturmVarPosInf (chain : List (Polynomial ℝ)) : ℕ := + signVariations (chain.map Polynomial.leadingCoeff) + +/-- Sign variations of the chain at `−∞`: the sign of an element there is the +sign of its leading coefficient times `(-1) ^ degree`, so this is the +zero-skipping variation count of `leadingCoeff · (-1) ^ natDegree`. -/ +@[expose] +noncomputable def sturmVarNegInf (chain : List (Polynomial ℝ)) : ℕ := + signVariations (chain.map (fun q => q.leadingCoeff * (-1) ^ q.natDegree)) + +/-- A generalized Sturm chain for a real polynomial. + +At a root of the first polynomial, the product of the first two entries changes +from negative to positive. At a root of an interior entry, its neighbors have +opposite signs. The last entry has no real roots, and every entry is nonzero. + +These conditions allow the one-element chain of a nonzero constant polynomial. +-/ structure IsSturmChain (p : Polynomial ℝ) (chain : List (Polynomial ℝ)) : Prop where - /-- The chain is nonempty. -/ - nonempty : chain ≠ [] /-- The head of the chain is `p`. -/ head : chain.head? = some p /-- At every real root `r` of `p`, the chain has a second element `q`, @@ -267,9 +207,6 @@ structure IsSturmChain (p : Polynomial ℝ) (chain : List (Polynomial ℝ)) : Pr (∀ᶠ x in 𝓝[>] r, 0 < (p * q).eval x) /-- No chain element is the zero polynomial. -/ nonzero_mem : ∀ q ∈ chain, q ≠ 0 - /-- Consecutive elements have no common real zero. -/ - consec_coprime : ∀ (i : ℕ) (x : ℝ) (a b : Polynomial ℝ), - chain[i]? = some a → chain[i + 1]? = some b → a.eval x = 0 → b.eval x ≠ 0 /-- Whenever the interior element `b = chain[i+1]` vanishes at `x`, its two neighbours `a = chain[i]` and `c = chain[i+2]` are nonzero there and have opposite signs. -/ @@ -279,4 +216,23 @@ structure IsSturmChain (p : Polynomial ℝ) (chain : List (Polynomial ℝ)) : Pr /-- The last element of the chain has no real zero. -/ last_no_root : ∀ q : Polynomial ℝ, chain.getLast? = some q → ∀ x : ℝ, q.eval x ≠ 0 +namespace IsSturmChain + +variable {p : Polynomial ℝ} {chain : List (Polynomial ℝ)} + +/-- A Sturm chain is nonempty. -/ +theorem nonempty (h : IsSturmChain p chain) : chain ≠ [] := by + rintro rfl + simpa using h.head + +/-- The polynomial counted by a Sturm chain is its first entry. -/ +theorem head_mem (h : IsSturmChain p chain) : p ∈ chain := + List.mem_of_head? h.head + +/-- A polynomial admitting a Sturm chain is nonzero. -/ +theorem ne_zero (h : IsSturmChain p chain) : p ≠ 0 := + h.nonzero_mem p h.head_mem + +end IsSturmChain + end Sturm diff --git a/HexRealRootsMathlib/SturmTests.lean b/HexRealRootsMathlib/SturmTests.lean new file mode 100644 index 0000000000..13e0e5c7dc --- /dev/null +++ b/HexRealRootsMathlib/SturmTests.lean @@ -0,0 +1,38 @@ +import HexRealRootsMathlib.SturmCertificate +import Mathlib.Tactic.NormNum + +open Polynomial Sturm + +private theorem linearChain : IsSturmChain (X : ℝ[X]) [X, 1] := by + have h : RemainderChain [(X : ℝ[X]), 1] := by + simpa using RemainderChain.pair X_ne_zero (one_ne_zero : (1 : ℝ) ≠ 0) + exact h.isSturmChain (a := 1) (by norm_num) (by simp) + +-- A root at the right endpoint is counted. +example : ((X : ℝ[X]).roots.filter (fun r => r ∈ Set.Ioc (-1) 0)).card = 1 := by + simpa [sturmVar, signVariations, countSignChanges] using + linearChain.sturm_Ioc (by simp) (show (-1 : ℝ) ≤ 0 by norm_num) + +-- A root at the left endpoint is excluded. +example : ((X : ℝ[X]).roots.filter (fun r => r ∈ Set.Ioc 0 1)).card = 0 := by + convert linearChain.sturm_Ioc (by simp) (show (0 : ℝ) ≤ 1 by norm_num) using 1 <;> + norm_num [sturmVar, signVariations, countSignChanges] + +-- Equal endpoints are permitted, including when that endpoint is a root. +example : ((X : ℝ[X]).roots.filter (fun r => r ∈ Set.Ioc 0 0)).card = 0 := by + convert linearChain.sturm_Ioc (by simp) (le_refl (0 : ℝ)) using 1 <;> + norm_num [sturmVar, signVariations, countSignChanges] + +-- The single-entry chain of a nonzero constant is a valid Sturm chain. +private theorem constantChain : IsSturmChain (1 : ℝ[X]) [1] where + head := rfl + root_flank := by simp [Polynomial.IsRoot] + nonzero_mem := by simp + interior_alternates := by + intro i x a b c ha hb hc + cases i <;> simp at hc + last_no_root := by simp + +example : (1 : ℝ[X]).roots.card = 0 := by + convert constantChain.sturm (by simp) using 1 <;> + norm_num [sturmVarNegInf, sturmVarPosInf, signVariations, countSignChanges] diff --git a/HexRealRootsMathlib/SturmTheorem.lean b/HexRealRootsMathlib/SturmTheorem.lean index 3d4ac00147..b54f042eed 100644 --- a/HexRealRootsMathlib/SturmTheorem.lean +++ b/HexRealRootsMathlib/SturmTheorem.lean @@ -7,53 +7,90 @@ Authors: Kim Morrison module public import HexRealRootsMathlib.SturmChainDefs - -public section +public import Mathlib.Analysis.Polynomial.Order /-! -Sturm's theorem over `Polynomial ℝ`, proved as a five-step chain. Everything -here is a slice over `Polynomial ℝ` with no `HexRealRoots` -dependence. - -The three local lemmas (`sturmVar_const_of_no_zero`, `sturmVar_interior_cross`, -`sturmVar_root_cross`) describe the behaviour of `Sturm.sturmVar` across the -finitely many zeros of the chain elements. The two global results -(`sturm_half_open`, `sturm_line`) are the telescoping consequences: the number -of real roots of `p` in a half-open interval `(a, b]` is the drop in -`sturmVar` from `a` to `b`, and the total number of real roots is the drop -from `−∞` to `+∞`. - -The half-open form telescopes the three local lemmas over the finitely many -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 -degree parities (helpers `eval_sign_pos_inf` / `eval_sign_neg_inf`). +# Sturm's theorem + +For a real polynomial with no repeated real roots admitting a Sturm chain, the number of roots +in `(a, b]` is the decrease in sign variations from `a` to `b`. Evaluating the +signs at infinity gives the total number of real roots. + +## Main results + +* `Sturm.IsSturmChain.sturm_Ioc`: the root count on a half-open interval. +* `Sturm.IsSturmChain.sturm`: the root count on the real line. + +The proof first establishes local constancy away from chain zeros. Crossing an +interior entry's zero preserves the variation count; crossing a root of the +first entry decreases it by one. The value at a root equals the value just to +its right, accounting for the half-open interval convention. Induction over the +finite set of chain zeros then gives the interval theorem. + +## References + +* Basu, Pollack and Roy, *Algorithms in Real Algebraic Geometry*, second edition, + [§2.2.2](https://doi.org/10.1007/3-540-33099-2). -/ +public section + open Filter Topology namespace Sturm -/-- Sign variations of the chain at `+∞`: the sign of each element there is the -sign of its leading coefficient, so this is the zero-skipping variation count -of the leading coefficients. The zero polynomial contributes leading -coefficient `0`, which the zero-skipping convention drops. -/ -@[expose] -noncomputable def sturmVarPosInf (chain : List (Polynomial ℝ)) : ℕ := - signVariations (chain.map Polynomial.leadingCoeff) - -/-- Sign variations of the chain at `−∞`: the sign of an element there is the -sign of its leading coefficient times `(-1) ^ degree`, so this is the -zero-skipping variation count of `leadingCoeff · (-1) ^ natDegree`. -/ -@[expose] -noncomputable def sturmVarNegInf (chain : List (Polynomial ℝ)) : ℕ := - signVariations (chain.map (fun q => q.leadingCoeff * (-1) ^ q.natDegree)) - -/-- **Sign persistence.** A polynomial with no zero on `[a, b]` keeps a constant -sign there: its evaluation signs at the two endpoints agree. If they differed, -the two endpoint values would straddle `0` and the intermediate value theorem -would supply an interior zero. -/ +/-- A local sign-pattern relation between two real lists: they agree entry by +entry except that a nonzero entry flanked by two opposite-sign neighbours may +collapse to `0`. Such a collapse is variation-neutral, so `signVariations` and +the leading sign are preserved (`SignRelation.signVariations_eq`). -/ +private inductive SignRelation : List ℝ → List ℝ → Prop + | nil : SignRelation [] [] + | same {x y : ℝ} {l m : List ℝ} (hx : x ≠ 0) (hy : y ≠ 0) + (hs : SignType.sign x = SignType.sign y) (h : SignRelation l m) : + SignRelation (x :: l) (y :: m) + | collapse {x X x' : ℝ} {l m : List ℝ} {y y' : ℝ} + (hx : x ≠ 0) (hX : X ≠ 0) (hy' : y' ≠ 0) + (hsx : SignType.sign x = SignType.sign x') + (hsy : SignType.sign y = SignType.sign y') + (hopp : SignType.sign x * SignType.sign y = -1) + (h : SignRelation (y :: l) (y' :: m)) : + SignRelation (x :: X :: y :: l) (x' :: 0 :: y' :: m) + +private theorem sign_changes_of_opposite (u v w : SignType) (huw : u * w = -1) (hv : v ≠ 0) : + (if u * v = -1 then (1 : ℕ) else 0) + (if v * w = -1 then 1 else 0) = 1 := by + revert huw hv; revert u v w; decide + +/-- Lists related by `SignRelation` have equal sign variations and equal leading signs. -/ +private theorem SignRelation.signVariations_eq {L M : List ℝ} (h : SignRelation L M) : + signVariations L = signVariations M ∧ firstSign L = firstSign M := by + induction h with + | nil => exact ⟨rfl, rfl⟩ + | @same x y l m hx hy hs h ih => + refine ⟨?_, ?_⟩ + · rw [signVariations_cons l hx, signVariations_cons m hy, ih.1, ih.2, hs] + · rw [firstSign_cons_ne l hx, firstSign_cons_ne m hy, hs] + | @collapse x X x' l m y y' hx hX hy' hsx hsy hopp h ih => + have hy : y ≠ 0 := by + intro hy0; rw [hy0, sign_zero, mul_zero] at hopp; exact absurd hopp (by decide) + have hx' : x' ≠ 0 := by + intro hx0; rw [hx0, sign_zero] at hsx; exact hx (sign_eq_zero_iff.mp hsx) + refine ⟨?_, ?_⟩ + · -- signVariations L + rw [signVariations_cons (X :: y :: l) hx, + firstSign_cons_ne (y :: l) hX, signVariations_cons (y :: l) hX, + firstSign_cons_ne l hy] + rw [signVariations_cons (0 :: y' :: m) hx', + firstSign_cons_zero (y' :: m) rfl, firstSign_cons_ne m hy', + signVariations_cons_zero] + simp only [Option.elim_some] + rw [← add_assoc, ih.1] + congr 1 + rw [← hsx, ← hsy, ite_eq_left hopp] + exact sign_changes_of_opposite _ _ _ hopp (fun h => hX (sign_eq_zero_iff.mp h)) + · rw [firstSign_cons_ne (X :: y :: l) hx, firstSign_cons_ne (0 :: y' :: m) hx', hsx] + + +/-- A real polynomial with no roots on an interval has equal signs at its endpoints. -/ theorem eval_sign_eq_of_no_zero {q : Polynomial ℝ} {a b : ℝ} (hab : a ≤ b) (hz : ∀ x ∈ Set.Icc a b, q.eval x ≠ 0) : SignType.sign (q.eval a) = SignType.sign (q.eval b) := by @@ -76,7 +113,7 @@ theorem eval_sign_eq_of_no_zero {q : Polynomial ℝ} {a b : ℝ} (hab : a ≤ b) · rw [sign_pos h1, sign_pos h2] · rw [sign_neg h1, sign_neg h2] -/-- Build the sign-pattern relation `SVRel` between the evaluations of a +/-- Build the sign-pattern relation `SignRelation` between the evaluations of a polynomial list at a "generic" point `a` (where every element is nonzero) and a "special" point `r` (where some interior elements may vanish). The hypotheses are exactly what an `IsSturmChain` supplies restricted to the relevant interval: @@ -84,7 +121,7 @@ every element is nonzero at `a`; the head and last elements are nonzero at `r`; whenever an interior element vanishes at `r` its neighbours are nonzero there with opposite signs; and every element nonzero at `r` has the same sign at `a` and `r`. -/ -private theorem buildSVRel (a r : ℝ) : +private theorem signRelation_eval (a r : ℝ) : ∀ (cs : List (Polynomial ℝ)), (∀ q ∈ cs, q.eval a ≠ 0) → (∀ q, cs.head? = some q → q.eval r ≠ 0) → @@ -93,11 +130,11 @@ private theorem buildSVRel (a r : ℝ) : cs[i + 2]? = some q2 → q1.eval r = 0 → q0.eval r ≠ 0 ∧ q2.eval r ≠ 0 ∧ q0.eval r * q2.eval r < 0) → (∀ q ∈ cs, q.eval r ≠ 0 → SignType.sign (q.eval a) = SignType.sign (q.eval r)) → - SVRel (cs.map (Polynomial.eval a)) (cs.map (Polynomial.eval r)) - | [], _, _, _, _, _ => SVRel.nil + SignRelation (cs.map (Polynomial.eval a)) (cs.map (Polynomial.eval r)) + | [], _, _, _, _, _ => SignRelation.nil | [q0], hne0, hfront, _, _, hsame => by have hr : q0.eval r ≠ 0 := hfront q0 rfl - exact SVRel.same (hne0 q0 (by simp)) hr (hsame q0 (by simp) hr) SVRel.nil + exact SignRelation.same (hne0 q0 (by simp)) hr (hsame q0 (by simp) hr) SignRelation.nil | q0 :: q1 :: rest, hne0, hfront, hlast, halt, hsame => by have hr0 : q0.eval r ≠ 0 := hfront q0 rfl have ha0 : q0.eval a ≠ 0 := hne0 q0 (by simp) @@ -130,10 +167,10 @@ private theorem buildSVRel (a r : ℝ) : have hsame' : ∀ q ∈ q2 :: rest', q.eval r ≠ 0 → SignType.sign (q.eval a) = SignType.sign (q.eval r) := fun q hq => hsame q (List.mem_cons_of_mem _ (List.mem_cons_of_mem _ hq)) - have IH := buildSVRel a r (q2 :: rest') hne0' hfront' hlast' halt' hsame' + have IH := signRelation_eval a r (q2 :: rest') hne0' hfront' hlast' halt' hsame' simp only [List.map_cons] at IH ⊢ rw [hq1] - exact SVRel.collapse ha0 (hne0 q1 (by simp)) hn2 hsx hsy hoppA IH + exact SignRelation.collapse ha0 (hne0 q1 (by simp)) hn2 hsx hsy hoppA IH · have hne0' : ∀ q ∈ q1 :: rest, q.eval a ≠ 0 := fun q hq => hne0 q (List.mem_cons_of_mem _ hq) have hfront' : ∀ q, (q1 :: rest).head? = some q → q.eval r ≠ 0 := by @@ -152,44 +189,25 @@ private theorem buildSVRel (a r : ℝ) : have hsame' : ∀ q ∈ q1 :: rest, q.eval r ≠ 0 → SignType.sign (q.eval a) = SignType.sign (q.eval r) := fun q hq => hsame q (List.mem_cons_of_mem _ hq) - have IH := buildSVRel a r (q1 :: rest) hne0' hfront' hlast' halt' hsame' + have IH := signRelation_eval a r (q1 :: rest) hne0' hfront' hlast' halt' hsame' simp only [List.map_cons] at IH ⊢ - exact SVRel.same ha0 hr0 (hsame q0 (by simp) hr0) IH + exact SignRelation.same ha0 hr0 (hsame q0 (by simp) hr0) IH variable {p : Polynomial ℝ} {chain : List (Polynomial ℝ)} -/-- **Local constancy.** On a closed interval `[a, b]` containing no zero of -any chain element, `sturmVar` takes the same value at the two endpoints. - -Proof sketch: each element keeps a constant nonzero sign across -`[a, b]` by continuity of polynomial evaluation ({name}`Polynomial.continuous_aeval`) -and the intermediate value theorem ({name}`intermediate_value_Icc`): a sign change -would force a zero. The list of evaluation signs is therefore the same at `a` -and `b`, so `signVariations` — which depends only on those signs — agrees. -/ -theorem sturmVar_const_of_no_zero (_hchain : IsSturmChain p chain) +/-- Sign variations are constant on an interval containing no zero of any chain entry. -/ +theorem sturmVar_const_of_no_zero (a b : ℝ) (hab : a ≤ b) (hz : ∀ q ∈ chain, ∀ x ∈ Set.Icc a b, q.eval x ≠ 0) : sturmVar chain a = sturmVar chain b := by - show signVariations (chain.map (Polynomial.eval a)) + change signVariations (chain.map (Polynomial.eval a)) = signVariations (chain.map (Polynomial.eval b)) apply signVariations_congr rw [List.forall₂_map_left_iff, List.forall₂_map_right_iff, List.forall₂_same] intro q hq exact eval_sign_eq_of_no_zero hab (fun x hx => hz q hq x hx) -/-- **Interior-element crossing preserves `sturmVar`.** If `r` is not a root of -`p` and the only chain zeros in `[a, b]` occur at `r` (necessarily zeros of -interior elements), then `sturmVar` is unchanged from `a` to `b`. - -Proof sketch: away from `r` local constancy applies on `[a, r]` -and `[r, b]`. At `r` the vanishing interior elements sit between neighbours of -opposite sign (`IsSturmChain.interior_alternates`), so each contributes exactly -one variation both immediately before and immediately after `r` regardless of -the sign it passes through, and the head pair (involving `p`, nonzero near `r`) -is unaffected. Hence the count at `a`, at `r`, and at `b` coincide. The value -at `r` itself is part of the statement because the global theorem places no -restriction on its endpoints, so a telescoping step may need the count exactly -at an interior-element zero. -/ +/-- Crossing a zero of an interior entry preserves the variation count. -/ theorem sturmVar_interior_cross (hchain : IsSturmChain p chain) (r : ℝ) (hpr : ¬ p.IsRoot r) (a b : ℝ) (har : a < r) (hrb : r < b) (hz : ∀ q ∈ chain, ∀ x ∈ Set.Icc a b, x ≠ r → q.eval x ≠ 0) : @@ -206,17 +224,17 @@ theorem sturmVar_interior_cross (hchain : IsSturmChain p chain) (r : ℝ) q0.eval r ≠ 0 ∧ q2.eval r ≠ 0 ∧ q0.eval r * q2.eval r < 0 := fun i q0 q1 q2 h0 h1 h2 hz => hchain.interior_alternates i r q0 q1 q2 h0 h1 h2 hz constructor - · show signVariations (chain.map (Polynomial.eval a)) + · change signVariations (chain.map (Polynomial.eval a)) = signVariations (chain.map (Polynomial.eval r)) - refine (buildSVRel a r chain (fun q hq => hz q hq a ⟨le_refl a, hab⟩ (ne_of_lt har)) + refine (signRelation_eval a r chain (fun q hq => hz q hq a ⟨le_refl a, hab⟩ (ne_of_lt har)) hfront hlast halt (fun q hq hqr => ?_)).signVariations_eq.1 exact eval_sign_eq_of_no_zero har.le (fun x hx => by by_cases hxr : x = r · rw [hxr]; exact hqr · exact hz q hq x ⟨hx.1, hx.2.trans hrb.le⟩ hxr) - · show signVariations (chain.map (Polynomial.eval r)) + · change signVariations (chain.map (Polynomial.eval r)) = signVariations (chain.map (Polynomial.eval b)) - refine ((buildSVRel b r chain + refine ((signRelation_eval b r chain (fun q hq => hz q hq b ⟨hab, le_refl b⟩ (ne_of_lt hrb).symm) hfront hlast halt (fun q hq hqr => ?_)).signVariations_eq.1).symm exact (eval_sign_eq_of_no_zero hrb.le (fun x hx => by @@ -224,26 +242,14 @@ theorem sturmVar_interior_cross (hchain : IsSturmChain p chain) (r : ℝ) · rw [hxr]; exact hqr · exact hz q hq x ⟨har.le.trans hx.1, hx.2⟩ hxr)).symm -/-- **Simple-zero crossing of `p` drops `sturmVar` by one, registering at `r`.** -If `r` is a (simple, by squarefreeness) root of `p` and the only chain zeros in -`[a, b]` occur at `r`, then `sturmVar` at `a` exceeds the value at `b` by -exactly one, and the drop has already registered at `r`: the value at `r` -equals the value at `b`. - -Proof sketch: the head pair `(p, q)` with `q = chain[1]` has -`p * q < 0` just left of `r` and `p * q > 0` just right (`root_flank`), so this -pair contributes one variation for `x < r` and none for `x ≥ r`; with the -zero-skipping convention the zero of `p` at `r` is dropped, so the change -registers at `r` itself. All interior crossings at `r` are variation-neutral by -step 2, and away from `r` `sturmVar` is locally constant by step 1. The -half-open registration is the one design-sensitive point: it is what makes the -executable half-open counts match with no endpoint hypotheses. -/ -theorem sturmVar_root_cross (_hp : p ≠ 0) (_hsf : Squarefree p) - (hchain : IsSturmChain p chain) (r : ℝ) (hr : p.IsRoot r) +/-- Crossing a root of the first entry decreases the variation count by one. +The count at the root equals the count just to its right. -/ +theorem sturmVar_root_cross (hchain : IsSturmChain p chain) (r : ℝ) (hr : p.IsRoot r) (a b : ℝ) (har : a < r) (hrb : r < b) - (hz : ∀ q ∈ chain, ∀ x ∈ Set.Icc a b, x ≠ r → q.eval x ≠ 0) - (hpz : ∀ x ∈ Set.Icc a b, x ≠ r → ¬ p.IsRoot x) : + (hz : ∀ q ∈ chain, ∀ x ∈ Set.Icc a b, x ≠ r → q.eval x ≠ 0) : sturmVar chain a = sturmVar chain b + 1 ∧ sturmVar chain r = sturmVar chain b := by + have hpz : ∀ x ∈ Set.Icc a b, x ≠ r → ¬ p.IsRoot x := + fun x hx hxr => hz p hchain.head_mem x hx hxr have hab : a ≤ b := (har.trans hrb).le obtain ⟨q, hq1, hqr, hflL, hflR⟩ := hchain.root_flank r hr -- Split the chain into its head `p` and second element `q`. @@ -317,37 +323,35 @@ theorem sturmVar_root_cross (_hp : p ≠ 0) (_hsf : Squarefree p) · exact hz s (List.mem_cons_of_mem _ hs) x ⟨har.le.trans hx.1, hx.2⟩ hxr)).symm -- The tail's `sturmVar` is the same at `a`, `r`, `b` (interior-crossing). have hEqA : sturmVar (q :: tail) a = sturmVar (q :: tail) r := - (buildSVRel a r (q :: tail) + (signRelation_eval a r (q :: tail) (fun s hs => hz s (List.mem_cons_of_mem _ hs) a ⟨le_refl a, hab⟩ (ne_of_lt har)) hfront_rest hlast_rest halt_rest hsame_a).signVariations_eq.1 have hEqB : sturmVar (q :: tail) b = sturmVar (q :: tail) r := - (buildSVRel b r (q :: tail) + (signRelation_eval b r (q :: tail) (fun s hs => hz s (List.mem_cons_of_mem _ hs) b ⟨hab, le_refl b⟩ (ne_of_lt hrb).symm) hfront_rest hlast_rest halt_rest hsame_b).signVariations_eq.1 -- Head-pair bookkeeping at each point. have hSVa : sturmVar (p :: q :: tail) a = 1 + sturmVar (q :: tail) a := by - show signVariations (p.eval a :: (q :: tail).map (Polynomial.eval a)) + change signVariations (p.eval a :: (q :: tail).map (Polynomial.eval a)) = 1 + signVariations ((q :: tail).map (Polynomial.eval a)) - rw [signVariations_cons_pos _ hpa] + rw [signVariations_cons _ hpa] simp only [List.map_cons] rw [firstSign_cons_ne _ hqa, Option.elim_some, ite_eq_left hsignA] have hSVb : sturmVar (p :: q :: tail) b = sturmVar (q :: tail) b := by - show signVariations (p.eval b :: (q :: tail).map (Polynomial.eval b)) + change signVariations (p.eval b :: (q :: tail).map (Polynomial.eval b)) = signVariations ((q :: tail).map (Polynomial.eval b)) - rw [signVariations_cons_pos _ hpb] + rw [signVariations_cons _ hpb] simp only [List.map_cons] rw [firstSign_cons_ne _ hqb, Option.elim_some, ite_eq_right hsignB, zero_add] have hSVr : sturmVar (p :: q :: tail) r = sturmVar (q :: tail) r := by - show signVariations (p.eval r :: (q :: tail).map (Polynomial.eval r)) + change signVariations (p.eval r :: (q :: tail).map (Polynomial.eval r)) = signVariations ((q :: tail).map (Polynomial.eval r)) rw [hpr0]; exact signVariations_cons_zero _ refine ⟨?_, ?_⟩ · rw [hSVa, hSVb, hEqA, hEqB]; omega · rw [hSVr, hSVb]; exact hEqB.symm -/-- The finite set of real points at which some element of `chain` vanishes. -Every chain element is nonzero (`IsSturmChain.nonzero_mem`), so each contributes -finitely many zeros; their union is the telescope's set of break points. -/ +/-- The union of the real root sets of the chain entries. -/ noncomputable def chainZeros (cs : List (Polynomial ℝ)) : Finset ℝ := cs.toFinset.biUnion (fun q => q.roots.toFinset) @@ -355,76 +359,36 @@ noncomputable def chainZeros (cs : List (Polynomial ℝ)) : Finset ℝ := element vanishes there (using that every chain element is nonzero). -/ theorem mem_chainZeros {cs : List (Polynomial ℝ)} (hne : ∀ q ∈ cs, q ≠ 0) {x : ℝ} : x ∈ chainZeros cs ↔ ∃ q ∈ cs, q.eval x = 0 := by - unfold chainZeros - simp only [Finset.mem_biUnion, List.mem_toFinset, Multiset.mem_toFinset] - constructor - · rintro ⟨q, hq, hx⟩ - exact ⟨q, hq, (Polynomial.mem_roots (hne q hq)).mp hx⟩ - · rintro ⟨q, hq, hx⟩ - exact ⟨q, hq, (Polynomial.mem_roots (hne q hq)).mpr hx⟩ - -/-- 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_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 - have hUne : U.Nonempty := ⟨lo, Finset.mem_insert_self _ _⟩ - have hmax_lt : U.max' hUne < z := by - rw [Finset.max'_lt_iff] - intro u hu - rw [hU, Finset.mem_insert] at hu - rcases hu with h | h - · rw [h]; exact hlo - · exact (Finset.mem_filter.mp h).2 - refine ⟨(U.max' hUne + z) / 2, ?_, ?_, ?_⟩ - · have : lo ≤ U.max' hUne := Finset.le_max' U lo (Finset.mem_insert_self _ _) - linarith - · linarith - · intro x hx hxz - have : x ≤ U.max' hUne := - Finset.le_max' U x (Finset.mem_insert.mpr (Or.inr (Finset.mem_filter.mpr ⟨hx, hxz⟩))) - linarith - -/-- 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_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 - have hUne : U.Nonempty := ⟨hi, Finset.mem_insert_self _ _⟩ - have hlt_min : z < U.min' hUne := by - rw [Finset.lt_min'_iff] - intro u hu - rw [hU, Finset.mem_insert] at hu - rcases hu with h | h - · rw [h]; exact hhi - · exact (Finset.mem_filter.mp h).2 - refine ⟨(z + U.min' hUne) / 2, ?_, ?_, ?_⟩ - · linarith - · have : U.min' hUne ≤ hi := Finset.min'_le U hi (Finset.mem_insert_self _ _) - linarith - · intro x hx hxz - have : U.min' hUne ≤ x := - Finset.min'_le U x (Finset.mem_insert.mpr (Or.inr (Finset.mem_filter.mpr ⟨hx, hxz⟩))) - linarith - -/-- The head `p` of a Sturm chain is a member of the chain. -/ -theorem chain_head_mem (hchain : IsSturmChain p chain) : p ∈ chain := by - cases chain with - | nil => exact absurd hchain.head (by simp) - | cons hd tl => - have hhd : hd = p := by simpa using hchain.head - rw [← hhd]; exact List.mem_cons_self - -/-- **Right registration.** If no chain element vanishes anywhere in the -half-open interval `(z, c]` (with `z ≤ c`), then `sturmVar` agrees at `z` and -`c`, even if `z` itself is a chain zero: the value at a break point equals the -value immediately to its right. -/ -theorem sturmVar_eq_right (hp : p ≠ 0) (hsf : Squarefree p) - (hchain : IsSturmChain p chain) {z c : ℝ} (hzc : z ≤ c) + simp only [chainZeros, Finset.mem_biUnion, List.mem_toFinset, Multiset.mem_toFinset] + exact exists_congr fun q => and_congr_right fun hq => Polynomial.mem_roots (hne q hq) + +/-- Choose a point between `lo` and `z` above every element of `S` below `z`. -/ +private theorem exists_left_gap (S : Finset ℝ) (z lo : ℝ) (hlo : lo < z) : + ∃ a, lo < a ∧ a < z ∧ ∀ x ∈ S, x < z → x < a := by + have h : ∀ᶠ a in 𝓝[<] z, ∀ x ∈ S, x < z → x < a := by + rw [S.eventually_all] + intro x _ + by_cases hx : x < z + · exact ((eventually_gt_nhds hx).filter_mono nhdsWithin_le_nhds).mono fun _ ha _ => ha + · simp [hx] + obtain ⟨a, ha, hla, haz⟩ := (h.and (Ioo_mem_nhdsLT hlo)).exists + exact ⟨a, hla, haz, ha⟩ + +/-- Choose a point between `z` and `hi` below every element of `S` above `z`. -/ +private theorem exists_right_gap (S : Finset ℝ) (z hi : ℝ) (hhi : z < hi) : + ∃ b, z < b ∧ b < hi ∧ ∀ x ∈ S, z < x → b < x := by + have h : ∀ᶠ b in 𝓝[>] z, ∀ x ∈ S, z < x → b < x := by + rw [S.eventually_all] + intro x _ + by_cases hx : z < x + · exact ((eventually_lt_nhds hx).filter_mono nhdsWithin_le_nhds).mono fun _ hb _ => hb + · simp [hx] + obtain ⟨b, hb, hzb, hbh⟩ := (h.and (Ioo_mem_nhdsGT hhi)).exists + exact ⟨b, hzb, hbh, hb⟩ + +/-- The variation count agrees with its value immediately to the right, +including at zeros of chain entries. -/ +theorem sturmVar_eq_right (hchain : IsSturmChain p chain) {z c : ℝ} (hzc : z ≤ c) (hclear : ∀ x, z < x → x ≤ c → x ∉ chainZeros chain) : sturmVar chain z = sturmVar chain c := by rcases eq_or_lt_of_le hzc with rfl | hlt @@ -440,15 +404,7 @@ theorem sturmVar_eq_right (hp : p ≠ 0) (hsf : Squarefree p) · exact hxz heq · exact hclear x hgt' hx.2 hxZ by_cases hroot : p.IsRoot z - · 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, 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 - · exact hclear x hgt' hx.2 hxZ - exact (sturmVar_root_cross hp hsf hchain z hroot a₀ c ha₀z hlt hz_ex hpz).2 + · exact (sturmVar_root_cross hchain z hroot a₀ c ha₀z hlt hz_ex).2 · exact (sturmVar_interior_cross hchain z hroot a₀ c ha₀z hlt hz_ex).2 · have hz_all : ∀ q ∈ chain, ∀ x ∈ Set.Icc z c, q.eval x ≠ 0 := by intro q hq x hx hqx @@ -456,7 +412,7 @@ theorem sturmVar_eq_right (hp : p ≠ 0) (hsf : Squarefree p) rcases eq_or_lt_of_le hx.1 with heq | hgt · exact hzZ (by rw [heq]; exact hxZ) · exact hclear x hgt hx.2 hxZ - exact sturmVar_const_of_no_zero hchain z c hzc hz_all + exact sturmVar_const_of_no_zero z c hzc hz_all /-- 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]`. -/ @@ -484,30 +440,21 @@ private theorem card_filter_Ioc_split (s : Multiset ℝ) {a a' b : ℝ} (h1 : a · exact Or.inr ⟨hx, h'⟩ rw [← Multiset.card_add, Multiset.filter_add_filter, hand, Multiset.add_zero, hor] -/-- **Sturm's theorem, half-open form.** For `p ≠ 0` squarefree with a -generalised Sturm chain, the drop in `sturmVar` from `a` to `b` equals the -number of real roots of `p` in the half-open interval `(a, b]`, counted as the -cardinality of the corresponding filtered submultiset of `p.roots`. - -Proof sketch: telescope the preceding lemmas over the finitely many zeros of -the chain elements in `(a, b]`. Zeros of interior elements are variation-neutral -(step 2); each root of `p` drops the count by exactly one and registers at the -root under the half-open convention (step 3); between consecutive chain zeros -`sturmVar` is constant (step 1). The signed total is therefore the number of -roots of `p` in `(a, b]`. -/ -theorem sturm_half_open (hp : p ≠ 0) (hsf : Squarefree p) - (hchain : IsSturmChain p chain) {a b : ℝ} (hab : a < b) : - (sturmVar chain a : ℤ) - sturmVar chain b = - (p.roots.filter (fun r => a < r ∧ r ≤ b)).card := by +/-- **Sturm's theorem** on a half-open interval. + +The decrease in sign variations from `a` to `b` counts the roots in `(a, b]`. +The hypothesis on `p.roots` ensures each real root has multiplicity one. -/ +theorem IsSturmChain.sturm_Ioc (hchain : IsSturmChain p chain) (hnod : p.roots.Nodup) + {a b : ℝ} (hab : a ≤ b) : + sturmVar chain b + (p.roots.filter (fun r => r ∈ Set.Ioc a b)).card = + sturmVar chain a := by classical have hne := hchain.nonzero_mem - have hnod : p.roots.Nodup := - Polynomial.nodup_roots (PerfectField.separable_iff_squarefree.mpr hsf) suffices H : ∀ n : ℕ, ∀ a b : ℝ, a ≤ b → ((chainZeros chain).filter (fun x => a < x ∧ x ≤ b)).card = n → - (sturmVar chain a : ℤ) - sturmVar chain b = - (p.roots.filter (fun r => a < r ∧ r ≤ b)).card by - exact H _ a b hab.le rfl + sturmVar chain b + (p.roots.filter (fun r => a < r ∧ r ≤ b)).card = + sturmVar chain a by + simpa only [Set.mem_Ioc] using H _ a b hab rfl intro n induction n using Nat.strong_induction_on with | _ n ih => @@ -520,11 +467,13 @@ theorem sturm_half_open (hp : p ≠ 0) (hsf : Squarefree p) have hxF : x ∈ F := by rw [hF, Finset.mem_filter]; exact ⟨hxZ, hx1, hx2⟩ rw [hemp] at hxF; exact absurd hxF (Finset.notMem_empty x) have heqv : sturmVar chain a = sturmVar chain b := - sturmVar_eq_right hp hsf hchain hab hclear + sturmVar_eq_right hchain hab hclear 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, chain_head_mem hchain, (Polynomial.mem_roots hp).mp hx⟩) + exact hclear x h1 h2 + ((mem_chainZeros hne).mpr + ⟨p, hchain.head_mem, (Polynomial.mem_roots hchain.ne_zero).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 @@ -551,11 +500,9 @@ theorem sturm_half_open (hp : p ≠ 0) (hsf : Squarefree p) · exact absurd (ha'gap x hxZ hlt') (not_lt.mpr hx.1) · 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 (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 + apply sturmVar_eq_right hchain hzb intro x hx1 hx2 hxZ have hxF : x ∈ F := by rw [hF, Finset.mem_filter]; exact ⟨hxZ, lt_trans haz hx1, hx2⟩ exact absurd (hzmax x hxF) (not_le.mpr hx1) @@ -569,19 +516,14 @@ theorem sturm_half_open (hp : p ≠ 0) (hsf : Squarefree p) rw [← hcard] exact Finset.card_lt_card ((Finset.ssubset_iff_of_subset hsub).mpr ⟨z, hzmem, hznotin⟩) have IHres := ih _ hlt_card a a' ha_a'.le rfl - have hsplitZ : ((p.roots.filter (fun r => a < r ∧ r ≤ b)).card : ℤ) - = ((p.roots.filter (fun r => a < r ∧ r ≤ a')).card : ℤ) - + ((p.roots.filter (fun r => a' < r ∧ r ≤ b)).card : ℤ) := by - exact_mod_cast card_filter_Ioc_split p.roots ha_a'.le (le_trans ha'z.le hzb) + have hsplit := card_filter_Ioc_split p.roots ha_a'.le (ha'z.le.trans hzb) by_cases hzroot : p.IsRoot z · obtain ⟨hcrossL, hcrossR⟩ := - sturmVar_root_cross hp hsf hchain z hzroot a' b' ha'z hzb' hz_ex hpz - have ha'bZ : (sturmVar chain a' : ℤ) = sturmVar chain b + 1 := by - have : sturmVar chain a' = sturmVar chain b + 1 := by - rw [hcrossL, ← hcrossR, hzeqb] - exact_mod_cast this - have hRZ : ((p.roots.filter (fun r => a' < r ∧ r ≤ b)).card : ℤ) = 1 := by - have hzrootmem : z ∈ p.roots := (Polynomial.mem_roots hp).mpr hzroot + sturmVar_root_cross hchain z hzroot a' b' ha'z hzb' hz_ex + have ha'b : sturmVar chain a' = sturmVar chain b + 1 := by + rw [hcrossL, ← hcrossR, hzeqb] + have hRZ : (p.roots.filter (fun r => a' < r ∧ r ≤ b)).card = 1 := by + have hzrootmem : z ∈ p.roots := (Polynomial.mem_roots hchain.ne_zero).mpr hzroot have hfeq : p.roots.filter (fun r => a' < r ∧ r ≤ b) = p.roots.filter (fun r => r = z) := by apply Multiset.filter_congr @@ -589,27 +531,27 @@ theorem sturm_half_open (hp : p ≠ 0) (hsf : Squarefree p) constructor · rintro ⟨h1, h2⟩ exact honly x h1 h2 - ((mem_chainZeros hne).mpr ⟨p, chain_head_mem hchain, (Polynomial.mem_roots hp).mp hx⟩) + ((mem_chainZeros hne).mpr + ⟨p, hchain.head_mem, (Polynomial.mem_roots hchain.ne_zero).mp hx⟩) · rintro rfl; exact ⟨ha'z, hzb⟩ rw [hfeq, Multiset.filter_eq', Multiset.card_replicate, Multiset.count_eq_one_of_mem hnod hzrootmem] - rfl - linarith [hsplitZ, hRZ, ha'bZ, IHres] + omega · obtain ⟨hcrossL, _⟩ := sturmVar_interior_cross hchain z hzroot a' b' ha'z hzb' hz_ex - have ha'bZ : (sturmVar chain a' : ℤ) = sturmVar chain b := by - have : sturmVar chain a' = sturmVar chain b := by rw [hcrossL, hzeqb] - exact_mod_cast this - have hRZ : ((p.roots.filter (fun r => a' < r ∧ r ≤ b)).card : ℤ) = 0 := by + have ha'b : sturmVar chain a' = sturmVar chain b := by + rw [hcrossL, hzeqb] + have hRZ : (p.roots.filter (fun r => a' < r ∧ r ≤ b)).card = 0 := by have hfeq : p.roots.filter (fun r => a' < r ∧ r ≤ b) = 0 := by rw [Multiset.filter_eq_nil] rintro x hx ⟨h1, h2⟩ have hxz : x = z := honly x h1 h2 - ((mem_chainZeros hne).mpr ⟨p, chain_head_mem hchain, (Polynomial.mem_roots hp).mp hx⟩) + ((mem_chainZeros hne).mpr + ⟨p, hchain.head_mem, (Polynomial.mem_roots hchain.ne_zero).mp hx⟩) rw [hxz] at hx - exact hzroot ((Polynomial.mem_roots hp).mp hx) + exact hzroot ((Polynomial.mem_roots hchain.ne_zero).mp hx) rw [hfeq]; rfl - linarith [hsplitZ, hRZ, ha'bZ, IHres] + omega /-- **Sign at `+∞`.** Past all its real roots, a nonzero real polynomial has the sign of its leading coefficient. -/ @@ -646,32 +588,18 @@ theorem eval_sign_neg_inf {q : Polynomial ℝ} (hq : q ≠ 0) {x : ℝ} rw [heval, hlcr] at hsign exact hsign -/-- **Sturm's theorem, line form.** For `p ≠ 0` squarefree with a generalised -Sturm chain, the total number of real roots of `p` equals the drop in `sturmVar` -from `−∞` to `+∞`. - -Proof sketch: take `a` below and `b` above every real root -(e.g. beyond a Cauchy bound). Then `sturmVar chain a = sturmVarNegInf chain` and -`sturmVar chain b = sturmVarPosInf chain`, because each chain element has -constant sign past its largest real zero equal to its sign at the corresponding -infinity, and `(a, b]` contains every real root. Apply `sturm_half_open`; the -filtered multiset is all of `p.roots`. -/ -theorem sturm_line (hp : p ≠ 0) (hsf : Squarefree p) - (hchain : IsSturmChain p chain) : - (sturmVarNegInf chain : ℤ) - sturmVarPosInf chain = p.roots.card := by +/-- **Sturm's theorem** on the real line: the decrease in sign variations from +`-∞` to `+∞` counts all real roots. -/ +theorem IsSturmChain.sturm (hchain : IsSturmChain p chain) (hnod : p.roots.Nodup) : + sturmVarPosInf chain + p.roots.card = sturmVarNegInf chain := by classical have hne := hchain.nonzero_mem -- A bound `M > 0` strictly beyond every chain zero (hence every root of every element). obtain ⟨M, hMpos, hM⟩ : ∃ M : ℝ, 0 < M ∧ ∀ x ∈ chainZeros chain, |x| < M := by - set B := insert (0 : ℝ) ((chainZeros chain).image (fun x => |x|)) with hB - have hBne : B.Nonempty := ⟨0, Finset.mem_insert_self _ _⟩ - refine ⟨B.max' hBne + 1, ?_, ?_⟩ - · have : (0 : ℝ) ≤ B.max' hBne := Finset.le_max' B 0 (Finset.mem_insert_self _ _) - linarith - · intro x hx - have : |x| ≤ B.max' hBne := - Finset.le_max' B |x| (Finset.mem_insert.mpr (Or.inr (Finset.mem_image.mpr ⟨x, hx, rfl⟩))) - linarith + have h : ∀ᶠ M : ℝ in atTop, ∀ x ∈ chainZeros chain, |x| < M := by + rw [Finset.eventually_all] + exact fun x _ => eventually_gt_atTop |x| + exact ((eventually_gt_atTop 0).and h).exists -- Sign of each element at `±M` is its sign at the corresponding infinity. have hpos : ∀ q ∈ chain, SignType.sign (q.eval M) = SignType.sign q.leadingCoeff := by intro q hq @@ -688,26 +616,26 @@ theorem sturm_line (hp : p ≠ 0) (hsf : Squarefree p) have hya := hM y hyz; rw [abs_lt] at hya; exact hya.1 -- Hence `sturmVar` at `±M` equals the `±∞` counts. have hMposEq : sturmVar chain M = sturmVarPosInf chain := by - show signVariations (chain.map (Polynomial.eval M)) + change signVariations (chain.map (Polynomial.eval M)) = signVariations (chain.map Polynomial.leadingCoeff) apply signVariations_congr rw [List.forall₂_map_left_iff, List.forall₂_map_right_iff, List.forall₂_same] exact hpos have hMnegEq : sturmVar chain (-M) = sturmVarNegInf chain := by - show signVariations (chain.map (Polynomial.eval (-M))) + change signVariations (chain.map (Polynomial.eval (-M))) = signVariations (chain.map (fun q => q.leadingCoeff * (-1) ^ q.natDegree)) apply signVariations_congr rw [List.forall₂_map_left_iff, List.forall₂_map_right_iff, List.forall₂_same] exact hneg -- Apply the half-open form on `(-M, M]`, which catches every root. - have hkey := sturm_half_open hp hsf hchain (a := -M) (b := M) (by linarith) - have hfilter : p.roots.filter (fun r => -M < r ∧ r ≤ M) = p.roots := by + have hkey := hchain.sturm_Ioc hnod (a := -M) (b := M) (by linarith) + have hfilter : p.roots.filter (fun r => r ∈ Set.Ioc (-M) M) = p.roots := by 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, chain_head_mem hchain, hroot⟩ + have hroot : p.eval r = 0 := (Polynomial.mem_roots hchain.ne_zero).mp hr + have hrz : r ∈ chainZeros chain := (mem_chainZeros hne).mpr ⟨p, hchain.head_mem, hroot⟩ have hra := hM r hrz; rw [abs_lt] at hra exact ⟨hra.1, hra.2.le⟩ - rw [← hMnegEq, ← hMposEq, hkey, hfilter] + simpa only [hMnegEq, hMposEq, hfilter] using hkey end Sturm diff --git a/lakefile.lean b/lakefile.lean index 1244ad61a1..4116768af5 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -893,6 +893,8 @@ lean_lib HexReleaseTests where `HexRealRoots.ReplayTest, `HexRealRootsMathlib.IsolateRootsTests, `HexRealRootsMathlib.IsolateRootsElabTests, + `HexRealRootsMathlib.SturmTests, + `HexRealRootsMathlib.RealRootCountTests, `HexRootsMathlib.Examples, `HexMvPoly.KernelTests, `HexSparsePoly.KernelTests, diff --git a/scripts/check_sturm_sync.py b/scripts/check_sturm_sync.py new file mode 100644 index 0000000000..3d33d62736 --- /dev/null +++ b/scripts/check_sturm_sync.py @@ -0,0 +1,55 @@ +#!/usr/bin/env python3 +"""Check that the Sturm development agrees with a Mathlib checkout. + +Usage: python3 scripts/check_sturm_sync.py /path/to/mathlib +Module paths, the parser namespace, and Verso name markup may differ. +""" + +import argparse +import difflib +import re +from pathlib import Path + +MODULES = { + "HexRealRootsMathlib.SturmChainDefs": "Mathlib.Analysis.Polynomial.Sturm.Defs", + "HexRealRootsMathlib.SturmTheorem": "Mathlib.Analysis.Polynomial.Sturm.Basic", + "HexRealRootsMathlib.SturmCertificate": "Mathlib.Analysis.Polynomial.Sturm.Certificate", + "HexPolyZMathlib.PolyParse": "Mathlib.Tactic.RealRootCount.Parse", + "HexRealRootsMathlib.RealRootCount": "Mathlib.Tactic.RealRootCount", + "HexRealRootsMathlib.RealRootCountTests": "MathlibTest.RealRootCount", + "HexRealRootsMathlib.SturmTests": "MathlibTest.Sturm", +} + + +# Mathlib master has moved the Sign modules since Hex's pinned Mathlib release. +RENAMES = MODULES | {"Mathlib.Data.Sign.Basic": "Mathlib.Basic.Sign.Basic"} + + +def mathlib_text(text: str) -> str: + for source, target in sorted(RENAMES.items(), key=lambda item: -len(item[0])): + text = text.replace(source, target) + return re.sub(r"\{name\}(`[^`]+`)", r"\1", text) + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("mathlib", type=Path) + args = parser.parse_args() + root = Path(__file__).resolve().parent.parent + different = False + for source, target in MODULES.items(): + src = root / (source.replace(".", "/") + ".lean") + dst = args.mathlib / (target.replace(".", "/") + ".lean") + expected = mathlib_text(src.read_text()).splitlines(keepends=True) + actual = dst.read_text().splitlines(keepends=True) + diff = list(difflib.unified_diff(expected, actual, fromfile=str(src), tofile=str(dst))) + if diff: + different = True + print("".join(diff), end="") + if different: + raise SystemExit(1) + print(f"All {len(MODULES)} Sturm library and test modules agree with Mathlib.") + + +if __name__ == "__main__": + main() diff --git a/scripts/release/released.yml b/scripts/release/released.yml index d983d7a0b7..3c53d9407c 100644 --- a/scripts/release/released.yml +++ b/scripts/release/released.yml @@ -270,7 +270,7 @@ repos: - repo: leanprover/hex-real-roots-mathlib lib: HexRealRootsMathlib - test_modules: [HexRealRootsMathlib.IsolateRootsTests, HexRealRootsMathlib.IsolateRootsElabTests] + test_modules: [HexRealRootsMathlib.IsolateRootsTests, HexRealRootsMathlib.IsolateRootsElabTests, HexRealRootsMathlib.SturmTests, HexRealRootsMathlib.RealRootCountTests] umbrella: true spec: hex-real-roots-mathlib pins: [hex-basic, hex-arith, hex-poly, hex-mod-arith, hex-poly-z, hex-poly-fp, hex-hensel, hex-poly-mathlib, hex-mod-arith-mathlib, hex-poly-z-mathlib, hex-real-roots] From c5353cdd6673f2e44d5657e55d892bcdef90f6a9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 7 Sep 2026 12:29:31 +0000 Subject: [PATCH 2/8] test(real-roots-mathlib): add required source headers --- HexRealRootsMathlib/RealRootCountTests.lean | 6 ++++++ HexRealRootsMathlib/SturmTests.lean | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/HexRealRootsMathlib/RealRootCountTests.lean b/HexRealRootsMathlib/RealRootCountTests.lean index 1fcc58d315..c7341ae9b3 100644 --- a/HexRealRootsMathlib/RealRootCountTests.lean +++ b/HexRealRootsMathlib/RealRootCountTests.lean @@ -1,3 +1,9 @@ +/- +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.RealRootCount open Polynomial diff --git a/HexRealRootsMathlib/SturmTests.lean b/HexRealRootsMathlib/SturmTests.lean index 13e0e5c7dc..7e597a3fad 100644 --- a/HexRealRootsMathlib/SturmTests.lean +++ b/HexRealRootsMathlib/SturmTests.lean @@ -1,3 +1,9 @@ +/- +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.SturmCertificate import Mathlib.Tactic.NormNum From 9e5c13e5f4e032368f58eea3d3a20d2e2995294c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 7 Sep 2026 12:39:42 +0000 Subject: [PATCH 3/8] fix(build): keep FFI compiler temporary files in the build directory --- lakefile.lean | 18 +++++++- scripts/release/check_released_manifest.py | 12 +++++ scripts/release/released.yml | 4 ++ scripts/release/sync_released.py | 46 +++++++++++++++++++ scripts/release/test_sync_released.py | 53 ++++++++++++++++++++++ 5 files changed, 131 insertions(+), 2 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 4116768af5..7e6d1e44ca 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -37,7 +37,14 @@ private def zmod64MulOTarget (pkg : Package) : FetchM (Job FilePath) := do let srcTarget ← inputTextFile <| pkg.dir / "HexModArith" / "ffi" / "zmod64_mul.c" buildFileAfterDep oFile srcTarget fun srcFile => do let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC", "-O3"] - compileO oFile srcFile flags + -- Mathlib's sandbox permits writes in the build directory, but not /tmp. + -- Set TMPDIR for this compiler process only, including compiler wrappers. + createParentDirs oFile + proc { + cmd := "cc" + args := #["-c", "-o", oFile.toString, srcFile.toString] ++ flags + env := #[("TMPDIR", some (← IO.FS.realPath (oFile.parent.getD ".")).toString)] + } extern_lib hexgf2ffi (pkg) := do let name := nameToStaticLib "hexgf2ffi" @@ -50,7 +57,14 @@ private def hexArithOTarget (pkg : Package) (src : String) : FetchM (Job FilePat let srcTarget ← inputTextFile <| pkg.dir / "HexArith" / "ffi" / src buildFileAfterDep oFile srcTarget fun srcFile => do let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC", "-O3"] - compileO oFile srcFile flags + -- Mathlib's sandbox permits writes in the build directory, but not /tmp. + -- Set TMPDIR for this compiler process only, including compiler wrappers. + createParentDirs oFile + proc { + cmd := "cc" + args := #["-c", "-o", oFile.toString, srcFile.toString] ++ flags + env := #[("TMPDIR", some (← IO.FS.realPath (oFile.parent.getD ".")).toString)] + } extern_lib hexarithffi (pkg) := do let name := nameToStaticLib "hexarithffi" diff --git a/scripts/release/check_released_manifest.py b/scripts/release/check_released_manifest.py index 5e8d36a2b7..041497e38f 100644 --- a/scripts/release/check_released_manifest.py +++ b/scripts/release/check_released_manifest.py @@ -20,6 +20,7 @@ MANIFEST, SKELETON, keep_paths, + lake_declaration, managed_paths, released_ci_workflows, source_build_settings, @@ -492,6 +493,17 @@ def main() -> int: fail(f"duplicate released library {lib}") library_names.add(lib) check_build_settings(entry) + helpers = entry.get("lake_declarations", []) + if (not isinstance(helpers, list) + or not all(isinstance(name, str) for name in helpers) + or len(helpers) != len(set(helpers)) + or (helpers and entry.get("lakefile") != "lean")): + fail(f"{repo}: lake_declarations requires unique names and a Lean Lake file") + for name in helpers: + try: + lake_declaration((REPO_ROOT / "lakefile.lean").read_text(), name) + except RuntimeError as exc: + fail(f"{repo}: {exc}") test_modules = entry.get("test_modules", []) if ( not isinstance(test_modules, list) diff --git a/scripts/release/released.yml b/scripts/release/released.yml index 3c53d9407c..a53e1fb0f1 100644 --- a/scripts/release/released.yml +++ b/scripts/release/released.yml @@ -59,6 +59,8 @@ # skeleton must build separately from the curated public umbrella. # `executables` maps an unmanaged released executable name to its mathematical # root module. The sync refuses to publish when the skeleton is stale. +# `lake_declarations` lists build helper declarations copied from the monorepo +# Lake file into the corresponding declarations in a Lean mirror skeleton. # `pins` lists the upstream repos whose git rev is rewritten in this repo's root # lakefile (matched by their github URL); `lakefile` is that file's format. # The mirror's `lean_lib` build settings are deliberately *not* recorded here: @@ -112,6 +114,7 @@ repos: spec: hex-arith pins: [] lakefile: lean + lake_declarations: [hexArithOTarget] - repo: leanprover/hex-primality component: Certified primality @@ -152,6 +155,7 @@ repos: spec: hex-mod-arith pins: [hex-arith] lakefile: lean + lake_declarations: [zmod64MulOTarget] - repo: leanprover/hex-poly-mathlib lib: HexPolyMathlib diff --git a/scripts/release/sync_released.py b/scripts/release/sync_released.py index 58ff0d4f0e..1e3bd64b7d 100755 --- a/scripts/release/sync_released.py +++ b/scripts/release/sync_released.py @@ -764,6 +764,50 @@ def rewrite_lib_settings(entry: dict, clone: Path) -> list[str]: return notes +def lake_declaration(text: str, name: str) -> tuple[int, int]: + """Locate an unindented build helper and its indented body. + + Managed helpers use ordinary `def` declarations without attributes. Refuse + missing or ambiguous declarations rather than modifying the wrong recipe. + """ + if not re.fullmatch(r"[A-Za-z_][A-Za-z0-9_']*", name): + raise RuntimeError(f"invalid Lake build helper name: {name!r}") + matches = list(re.finditer( + r"(?m)^(?:private |public )?def " + re.escape(name) + r"(?=\s|\()[^\n]*\n", + text, + )) + if len(matches) != 1: + raise RuntimeError(f"expected one Lake build helper {name}, found {len(matches)}") + start = matches[0].start() + end = _block_end(text, matches[0].end()) + return start, end + + +def rewrite_lake_declarations(entry: dict, clone: Path) -> list[str]: + """Copy selected C build recipes from the source-of-truth Lake file.""" + names = entry.get("lake_declarations", []) + if not names: + return [] + if (entry.get("lakefile") != "lean" or not isinstance(names, list) + or not all(isinstance(name, str) for name in names) + or len(names) != len(set(names))): + raise RuntimeError("lake_declarations requires a Lean Lake file and unique helper names") + source = LAKEFILE.read_text(encoding="utf-8") + path = clone / "lakefile.lean" + text = path.read_text(encoding="utf-8") + notes = [] + for name in names: + src_start, src_end = lake_declaration(source, name) + dst_start, dst_end = lake_declaration(text, name) + definition = source[src_start:src_end].rstrip() + "\n\n" + if text[dst_start:dst_end] != definition: + text = text[:dst_start] + definition + text[dst_end:] + notes.append(f" build helper {name} (lakefile.lean)") + if notes: + path.write_text(text, encoding="utf-8") + return notes + + def validate_skeleton(entry: dict, clone: Path) -> None: """Check the unmanaged Lake file carries every release build root. @@ -1383,6 +1427,8 @@ def sync_repo(entry: dict, source_sha: str, token: str | None, dry_run: bool, print(line) for line in rewrite_lib_settings(entry, clone): print(line) + for line in rewrite_lake_declarations(entry, clone): + print(line) for line in rewrite_toolchains(clone): print(line) for line in rewrite_external_pins(clone, pins): diff --git a/scripts/release/test_sync_released.py b/scripts/release/test_sync_released.py index 554647c1b8..a9acdbf19f 100644 --- a/scripts/release/test_sync_released.py +++ b/scripts/release/test_sync_released.py @@ -724,6 +724,59 @@ def publish(entry, _source_sha, _token, _dry_run, synced, self.assertEqual(advanced["downstream"], "new-downstream") +class LakeDeclarationTests(unittest.TestCase): + def setUp(self) -> None: + self.temporary = tempfile.TemporaryDirectory() + self.addCleanup(self.temporary.cleanup) + self.root = Path(self.temporary.name) + self.source = self.root / "source.lean" + self.clone = self.root / "clone" + self.clone.mkdir() + self.target = self.clone / "lakefile.lean" + self.entry = {"lakefile": "lean", "lake_declarations": ["compileTarget"]} + self.definition = ( + "private def compileTarget (pkg : Package) : FetchM (Job FilePath) := do\n" + " let flags := #[\"-pipe\"]\n" + " compileO output source flags\n\n" + ) + self.source.write_text("import Lake\n\n" + self.definition + "lean_lib Other\n") + self.original = ( + "import Lake\n\n" + "private def compileTarget (pkg : Package) : FetchM (Job FilePath) := do\n" + " compileO output source #[]\n\n" + "@[default_target]\nlean_lib Consumer where\n precompileModules := true\n" + ) + self.target.write_text(self.original) + + def rewrite(self) -> list[str]: + with patch.object(sync_released, "LAKEFILE", self.source): + return sync_released.rewrite_lake_declarations(self.entry, self.clone) + + def test_copies_recipe_preserving_skeleton_and_is_idempotent(self) -> None: + self.assertEqual(len(self.rewrite()), 1) + self.assertEqual(self.target.read_text(), + "import Lake\n\n" + self.definition + + "@[default_target]\nlean_lib Consumer where\n precompileModules := true\n") + self.assertEqual(self.rewrite(), []) + + def test_missing_helper_does_not_write_partial_result(self) -> None: + self.entry["lake_declarations"].append("missing") + with self.assertRaisesRegex(RuntimeError, "expected one Lake build helper missing"): + self.rewrite() + self.assertEqual(self.target.read_text(), self.original) + + def test_duplicate_declarations_are_rejected(self) -> None: + self.source.write_text(self.definition * 2) + with self.assertRaisesRegex(RuntimeError, "found 2"): + self.rewrite() + self.assertEqual(self.target.read_text(), self.original) + + def test_toml_target_is_rejected(self) -> None: + self.entry["lakefile"] = "toml" + with self.assertRaisesRegex(RuntimeError, "requires a Lean Lake file"): + self.rewrite() + + class LibBuildSettingTests(unittest.TestCase): """The mirror's `lean_lib` must be built the way hex-dev builds it. From 7b79a786034f60ae87023443ae2cc86beef55c25 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 7 Sep 2026 12:40:47 +0000 Subject: [PATCH 4/8] docs(build): describe sandbox-compatible FFI compilation --- HexArith/SPEC/hex-arith.md | 10 +++++++--- HexModArith/SPEC/hex-mod-arith.md | 8 ++++++++ 2 files changed, 15 insertions(+), 3 deletions(-) diff --git a/HexArith/SPEC/hex-arith.md b/HexArith/SPEC/hex-arith.md index 67e6daeee6..2dc0c20ed1 100644 --- a/HexArith/SPEC/hex-arith.md +++ b/HexArith/SPEC/hex-arith.md @@ -251,9 +251,13 @@ The C extern bodies live in `HexArith/ffi/wide_arith.c`: The C source is wired into `lakefile.lean` via an `extern_lib` block (paralleling `extern_lib hexgf2ffi` for HexGF2's CLMUL). The -block compiles the `.c` sources to `.o` via `compileO` (with -`-I (← getLeanIncludeDir).toString -fPIC`), bundles them into a -static library via `buildStaticLib`, and Lake links that library +block compiles the `.c` sources to `.o` with `cc`, Lean’s include +directory, `-fPIC`, and `-O3`. Each compiler process receives the +object directory as `TMPDIR`, so temporary files remain inside +`.lake/build` even when a downstream sandbox forbids writes to `/tmp`. +The release sync copies this recipe from the monorepo Lake file. +The block bundles the objects into a static library via `buildStaticLib`, +and Lake links that library into anything depending on `lean_lib HexArith`. The same `extern_lib` block carries `mpz_gcdext.c` (see "Extern contract: `mpz_gcdext`" below). Putting `.c` paths in `moreLinkArgs` (or in diff --git a/HexModArith/SPEC/hex-mod-arith.md b/HexModArith/SPEC/hex-mod-arith.md index 7f8723b5fc..f71d8d8a8f 100644 --- a/HexModArith/SPEC/hex-mod-arith.md +++ b/HexModArith/SPEC/hex-mod-arith.md @@ -6,6 +6,14 @@ representative in `[0, p)`); Barrett and Montgomery from `hex-arith` provide opt-in *operations* on `ZMod64` for hot loops, not parallel types. +## Native build + +The `hexmodarithffi` Lake target compiles `zmod64_mul.c` with `cc`, Lean’s +include directory, `-fPIC`, and `-O3`. It sets `TMPDIR` to the object directory +for that compiler process, keeping temporary files inside `.lake/build` when +a downstream sandbox forbids writes to `/tmp`. The release sync copies the +recipe from the monorepo Lake file. + ## Bounds typeclass and type ```lean From be961d3e75c63eeeb7215d933395662d10e4f340 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 7 Sep 2026 12:41:28 +0000 Subject: [PATCH 5/8] refactor(real-roots-mathlib): simplify proofs and preserve elaboration context --- HexPolyZMathlib/PolyParse.lean | 10 ++++--- HexRealRootsMathlib/ChainCorrespond.lean | 10 +++---- HexRealRootsMathlib/RealRootCount.lean | 11 ++++---- HexRealRootsMathlib/RealRootCountTests.lean | 25 ++++++++++++++++++ HexRealRootsMathlib/SturmCertificate.lean | 10 +++---- HexRealRootsMathlib/SturmChainDefs.lean | 3 +++ HexRealRootsMathlib/SturmTheorem.lean | 29 ++++++++------------- 7 files changed, 59 insertions(+), 39 deletions(-) diff --git a/HexPolyZMathlib/PolyParse.lean b/HexPolyZMathlib/PolyParse.lean index e623d7d8a5..2bd195d987 100644 --- a/HexPolyZMathlib/PolyParse.lean +++ b/HexPolyZMathlib/PolyParse.lean @@ -120,12 +120,14 @@ meta partial def parsePoly (tactic : String) (isRat : Bool) (fuel : Nat) return (← parsePoly tactic isRat fuel a onUnfold) * (← parsePoly tactic isRat fuel b onUnfold) | (``Neg.neg, #[_, _, a]) => return - (← parsePoly tactic isRat fuel a onUnfold) | (``HPow.hPow, #[_, _, _, _, a, n]) => do - let base ← parsePoly tactic isRat fuel a onUnfold - let k ← getNat tactic n + let mut base ← parsePoly tactic isRat fuel a onUnfold + let mut k ← getNat tactic n let mut acc : Hex.ZPoly := Hex.DensePoly.C 1 - for _ in [0:k] do + while k != 0 do checkSystem "polynomial exponentiation" - acc := acc * base + if k % 2 == 1 then acc := acc * base + k := k / 2 + if k != 0 then base := base * base return acc | (``Polynomial.X, _) => return Hex.DensePoly.ofCoeffs #[(0 : Int), 1] | (``Polynomial.C, #[_, _, c]) => return Hex.DensePoly.C (← evalCoeff tactic isRat c) diff --git a/HexRealRootsMathlib/ChainCorrespond.lean b/HexRealRootsMathlib/ChainCorrespond.lean index 47390f1e60..8e29110971 100644 --- a/HexRealRootsMathlib/ChainCorrespond.lean +++ b/HexRealRootsMathlib/ChainCorrespond.lean @@ -1070,14 +1070,12 @@ private theorem sign_near_root {p : ℝ[X]} {r : ℝ} constructor · filter_upwards [hl.eventually_const_lt hd, self_mem_nhdsWithin] with x hx hxr simp only [slope_def_field, hr, sub_zero] at hx - rcases div_pos_iff.mp hx with ⟨_, h⟩ | ⟨h, _⟩ - · exact False.elim ((sub_neg.mpr hxr).not_gt h) - · exact h + have hneg : x - r < 0 := sub_neg.mpr hxr + simpa only [div_pos_iff, hneg.not_gt, hneg, + and_false, and_true, false_or] using hx · filter_upwards [hu.eventually_const_lt hd, self_mem_nhdsWithin] with x hx hxr simp only [slope_def_field, hr, sub_zero] at hx - rcases div_pos_iff.mp hx with ⟨h, _⟩ | ⟨_, h⟩ - · exact h - · exact False.elim ((sub_pos.mpr hxr).not_gt h) + exact (div_pos_iff_of_pos_right (sub_pos.mpr hxr)).mp hx /-- **The head-pair flank.** If `s₀` vanishes at `r`, `s₁` does not, and `s₀' = C γ · s₁` with `γ > 0` (the executable seeds: the primitive parts of diff --git a/HexRealRootsMathlib/RealRootCount.lean b/HexRealRootsMathlib/RealRootCount.lean index 3e1ea28901..83b3aa96a9 100644 --- a/HexRealRootsMathlib/RealRootCount.lean +++ b/HexRealRootsMathlib/RealRootCount.lean @@ -22,7 +22,8 @@ The term form `real_root_count (p : ℚ[X])` proves `Fintype.card (p.rootSet ℝ squarefree polynomial of positive degree with integer coefficients. Hex proposes a signed remainder chain; `ring`, `compute_degree`, and `norm_num` check its identities, nonvanishing, and signs. No correctness assumption about the generator -or its polynomial representation enters the proof. +or its polynomial representation enters the proof. Named definitions and closed local +`let` bindings are supported. -/ public meta section @@ -142,18 +143,18 @@ elab "real_root_count " pStx:term : term <= expectedType? => withRef pStx do let pTy ← elabType (← `(Polynomial ℚ)) let e ← elabTermEnsuringType pStx pTy synthesizeSyntheticMVarsNoPostponing - let e ← instantiateMVars e + let e ← zetaReduce (← instantiateMVars e) if e.hasFVar || e.hasExprMVar then throwError "real_root_count: expected a closed polynomial" let names ← IO.mkRef (#[] : Array Name) let p ← HexPolyZMathlib.PolyParse.parsePoly "real_root_count" true 16 e (fun n => names.modify (fun ns => if ns.contains n then ns else ns.push n)) let unfolds ← (← names.get).mapM fun n => `(Parser.Tactic.simpLemma| $(mkIdent n):term) - elabTermEnsuringType (← emit pStx p unfolds) expectedType? + elabTermEnsuringType (← emit (← exprToSyntax e) p unfolds) expectedType? /-- Prove a goal `Fintype.card (p.rootSet ℝ) = n` by a checked Sturm chain. The polynomial must be closed, squarefree, of positive degree, and have integer coefficients. -/ -elab "real_root_count" : tactic => do +elab "real_root_count" : tactic => Tactic.withMainContext do let goal ← Tactic.getMainGoal let target ← instantiateMVars (← goal.getType) let some (_, lhs, _) := target.eq? | @@ -162,7 +163,7 @@ elab "real_root_count" : tactic => do throwError "real_root_count: expected a goal `Fintype.card (p.rootSet ℝ) = n`" let some roots := lhs.getAppArgs[0]!.find? (·.isAppOf ``Polynomial.rootSet) | throwError "real_root_count: expected a goal `Fintype.card (p.rootSet ℝ) = n`" - let p ← PrettyPrinter.delab roots.getAppArgs[2]! + let p ← exprToSyntax roots.getAppArgs[2]! let proof ← elabTermEnsuringType (← `(real_root_count $p)) (some target) goal.assign proof Tactic.replaceMainGoal [] diff --git a/HexRealRootsMathlib/RealRootCountTests.lean b/HexRealRootsMathlib/RealRootCountTests.lean index c7341ae9b3..defeff3bdd 100644 --- a/HexRealRootsMathlib/RealRootCountTests.lean +++ b/HexRealRootsMathlib/RealRootCountTests.lean @@ -77,3 +77,28 @@ example : Fintype.card (nestedPolynomial.rootSet ℝ) = 1 := by /-- error: real_root_count: expected a goal `Fintype.card (p.rootSet ℝ) = n` -/ #guard_msgs in example : True := by real_root_count + +-- Closed local definitions are accepted, in both the term and tactic forms. +example : True := by + let p : ℚ[X] := X ^ 3 - 2 + have : Fintype.card (p.rootSet ℝ) = 1 := real_root_count p + trivial + +example : True := by + let p : ℚ[X] := X ^ 3 - 2 + have : Fintype.card (p.rootSet ℝ) = 1 := by real_root_count + trivial + +-- Solving the first goal preserves the remaining goals and their local context. +example (n : ℕ) : Fintype.card ((X : ℚ[X]).rootSet ℝ) = 1 ∧ n = n := by + constructor + · real_root_count + · rfl + +-- Exponentiation covers the zero, even, and odd cases, including large exponents +-- when the base is constant. +example : Fintype.card ((X + (1 : ℚ[X]) ^ 10000).rootSet ℝ) = 1 := by + real_root_count + +example : Fintype.card ((X + (X ^ 2 + 1) ^ 0 : ℚ[X]).rootSet ℝ) = 1 := by + real_root_count diff --git a/HexRealRootsMathlib/SturmCertificate.lean b/HexRealRootsMathlib/SturmCertificate.lean index 13133ee0bd..143c0359bf 100644 --- a/HexRealRootsMathlib/SturmCertificate.lean +++ b/HexRealRootsMathlib/SturmCertificate.lean @@ -50,14 +50,12 @@ private theorem sign_near_root {p : ℝ[X]} {r : ℝ} constructor · filter_upwards [hl.eventually_const_lt hd, self_mem_nhdsWithin] with x hx hxr simp only [slope_def_field, hr, sub_zero] at hx - rcases div_pos_iff.mp hx with ⟨_, h⟩ | ⟨h, _⟩ - · exact False.elim ((sub_neg.mpr hxr).not_gt h) - · exact h + have hneg : x - r < 0 := sub_neg.mpr hxr + simpa only [div_pos_iff, hneg.not_gt, hneg, + and_false, and_true, false_or] using hx · filter_upwards [hu.eventually_const_lt hd, self_mem_nhdsWithin] with x hx hxr simp only [slope_def_field, hr, sub_zero] at hx - rcases div_pos_iff.mp hx with ⟨h, _⟩ | ⟨_, h⟩ - · exact h - · exact False.elim ((sub_pos.mpr hxr).not_gt h) + exact (div_pos_iff_of_pos_right (sub_pos.mpr hxr)).mp hx /-- The product of the first two entries changes from negative to positive at a root of the first entry. -/ diff --git a/HexRealRootsMathlib/SturmChainDefs.lean b/HexRealRootsMathlib/SturmChainDefs.lean index 47fe43cd8b..cc38eba261 100644 --- a/HexRealRootsMathlib/SturmChainDefs.lean +++ b/HexRealRootsMathlib/SturmChainDefs.lean @@ -63,6 +63,9 @@ noncomputable def signVariations (l : List ℝ) : ℕ := @[simp] theorem signVariations_nil : signVariations [] = 0 := rfl +@[simp] theorem signVariations_singleton (a : ℝ) : signVariations [a] = 0 := by + by_cases ha : a = 0 <;> simp [signVariations, ha] + /-- Prepending a zero entry does not change the sign variations. -/ @[simp] theorem signVariations_cons_zero (l : List ℝ) : signVariations (0 :: l) = signVariations l := by diff --git a/HexRealRootsMathlib/SturmTheorem.lean b/HexRealRootsMathlib/SturmTheorem.lean index b54f042eed..7bf8416ce3 100644 --- a/HexRealRootsMathlib/SturmTheorem.lean +++ b/HexRealRootsMathlib/SturmTheorem.lean @@ -421,24 +421,17 @@ private theorem card_filter_Ioc_split (s : Multiset ℝ) {a a' b : ℝ} (h1 : a = (s.filter (fun r => a < r ∧ r ≤ a')).card + (s.filter (fun r => a' < r ∧ r ≤ b)).card := by classical - have hand : s.filter (fun r => (a < r ∧ r ≤ a') ∧ (a' < r ∧ r ≤ b)) = 0 := by - rw [Multiset.filter_eq_nil] - rintro x _ ⟨⟨_, hxa'⟩, ha'x, _⟩ - exact absurd ha'x (not_lt.mpr hxa') - have hor : s.filter (fun r => (a < r ∧ r ≤ a') ∨ (a' < r ∧ r ≤ b)) - = s.filter (fun r => a < r ∧ r ≤ b) := by - apply Multiset.filter_congr - intro x _ - constructor - · rintro (⟨h, h'⟩ | ⟨h, h'⟩) - · exact ⟨h, le_trans h' h2⟩ - · exact ⟨lt_of_le_of_lt h1 h, h'⟩ - · rintro ⟨h, h'⟩ - rcases lt_trichotomy x a' with hx | hx | hx - · exact Or.inl ⟨h, hx.le⟩ - · exact Or.inl ⟨h, hx.le⟩ - · exact Or.inr ⟨hx, h'⟩ - rw [← Multiset.card_add, Multiset.filter_add_filter, hand, Multiset.add_zero, hor] + rw [← Multiset.card_add, ← Multiset.filter_add_not (fun r => r ≤ a') + (s.filter (fun r => a < r ∧ r ≤ b)), Multiset.filter_filter, Multiset.filter_filter] + congr 2 <;> apply Multiset.filter_congr <;> intro x _ <;> constructor + · rintro ⟨h, hax, hxb⟩ + exact ⟨hax, h⟩ + · rintro ⟨hax, hxa⟩ + exact ⟨hxa, hax, hxa.trans h2⟩ + · rintro ⟨h, hax, hxb⟩ + exact ⟨lt_of_not_ge h, hxb⟩ + · rintro ⟨hax, hxb⟩ + exact ⟨hax.not_ge, h1.trans_lt hax, hxb⟩ /-- **Sturm's theorem** on a half-open interval. From de84d55e0707d7f9a456425b5603d3858a2d9efd Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 7 Sep 2026 12:48:50 +0000 Subject: [PATCH 6/8] test(build): record runtime-neutral compiler environment change --- .../lakefile-lean-a56a63e3-7e6d1e44.json | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 scripts/bench/proof_only_runtime_exemptions/lakefile-lean-a56a63e3-7e6d1e44.json diff --git a/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-a56a63e3-7e6d1e44.json b/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-a56a63e3-7e6d1e44.json new file mode 100644 index 0000000000..1fd9a35629 --- /dev/null +++ b/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-a56a63e3-7e6d1e44.json @@ -0,0 +1,6 @@ +{ + "path": "lakefile.lean", + "baseline_blob": "a56a63e3b99c2af2c1b477347d0b3a5bec8d9b51", + "current_blob": "7e6d1e44cae8e18889a99350b2cfd55d20606efb", + "reason": "The HexArith and HexModArith compiler recipes retain the same cc executable, source paths, object paths, include directory, -fPIC and -O3 flags, and static linking. They only set TMPDIR to the object directory for the compiler process so Mathlib can build inside its existing sandbox. Rebuilding wide_arith.o, mpz_gcdext.o and zmod64_mul.o produced byte-for-byte identical objects. The other changes register independent rational-function, graph-isomorphism, conformance and test targets (including Sturm tests); none changes hexbz_factor_service or its runtime dependency graph." +} From b9fbaa62f1d4325b38e34be9f5ac445a03215a48 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 7 Sep 2026 21:48:47 +0000 Subject: [PATCH 7/8] fix(arith): remove sandbox-incompatible dead proofs --- HexArith/Montgomery/InvNat.lean | 18 ------------------ 1 file changed, 18 deletions(-) diff --git a/HexArith/Montgomery/InvNat.lean b/HexArith/Montgomery/InvNat.lean index 46192ec785..8d9fbf0bf2 100644 --- a/HexArith/Montgomery/InvNat.lean +++ b/HexArith/Montgomery/InvNat.lean @@ -5,8 +5,6 @@ Authors: Kim Morrison -/ module -public meta import Std.Tactic.BVDecide - public import HexArith.Montgomery.RedcNat public section @@ -24,22 +22,6 @@ resulting modular-inverse properties. def montPosInvStep (p x : UInt64) : UInt64 := x * (2 - p * x) -/-- The executable wrapping Newton step lifts a 3-bit inverse to 6 bits. -/ -private theorem montPosInvStep_mod_3_to_6 (p x : UInt64) - (hx : p * x % 8 = 1) : - p * montPosInvStep p x % 64 = 1 := by - unfold montPosInvStep - bv_decide (config := { timeout := 120 }) - -set_option maxHeartbeats 1000000 in -/-- The executable wrapping Newton step lifts a 6-bit inverse to 12 bits. -The bit-vector decision procedure needs this theorem-local elaboration budget. -/ -private theorem montPosInvStep_mod_6_to_12 (p x : UInt64) - (hx : p * x % 64 = 1) : - p * montPosInvStep p x % 4096 = 1 := by - unfold montPosInvStep - bv_decide (config := { timeout := 120 }) - /-- Every power of two up to `2^64` divides the `UInt64` modulus `2^64`. -/ private theorem two_pow_dvd_uint64_word {t : Nat} (ht : t ≤ 64) : 2 ^ t ∣ UInt64.word := by From 75e0717b2bff6eb13d90721e243350c8d25758d9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 7 Sep 2026 22:11:36 +0000 Subject: [PATCH 8/8] test(bench): scope build configuration freshness --- scripts/bench/check_factor_sweep_freshness.py | 40 ++---------- .../bench/check_graphiso_sweep_freshness.py | 65 ++++++++++++++++--- scripts/bench/graphiso_pernode_fit.py | 8 +-- ...tgomery-invnat-lean-46192ec7-8d9fbf0b.json | 6 ++ ...n => lakefile-lean-a56a63e3-c4319f88.json} | 4 +- scripts/bench/sweep_freshness.py | 43 ++++++++++-- .../test_check_factor_sweep_freshness.py | 15 ++++- scripts/bench/test_sweep_freshness.py | 46 +++++++++++++ 8 files changed, 168 insertions(+), 59 deletions(-) create mode 100644 scripts/bench/proof_only_runtime_exemptions/hexarith-montgomery-invnat-lean-46192ec7-8d9fbf0b.json rename scripts/bench/proof_only_runtime_exemptions/{lakefile-lean-a56a63e3-7e6d1e44.json => lakefile-lean-a56a63e3-c4319f88.json} (63%) diff --git a/scripts/bench/check_factor_sweep_freshness.py b/scripts/bench/check_factor_sweep_freshness.py index d9b67c1684..b5dd9d1ffa 100755 --- a/scripts/bench/check_factor_sweep_freshness.py +++ b/scripts/bench/check_factor_sweep_freshness.py @@ -25,7 +25,6 @@ import hashlib import json from pathlib import Path -import re import subprocess import sys @@ -40,42 +39,9 @@ LAKEFILE = "lakefile.lean" -# Lines that begin a top-level Lake declaration. Anything before one of these -# (comments, docstrings, `@[default_target]`) belongs to the declaration that -# follows it. -LAKE_DECL = re.compile( - r"^(package|require|lean_lib|lean_exe|extern_lib|target|script" - r"|input_file|module_facet|library_facet|package_facet)\s+(\S+)") - - -def lakefile_blocks(text: str) -> dict[str, str]: - """Split a lakefile into top-level declaration blocks, keyed by decl name.""" - blocks: dict[str, str] = {} - key: str | None = None - pending: list[str] = [] - current: list[str] = [] - for line in text.splitlines(): - match = LAKE_DECL.match(line) - if match: - if key is not None: - blocks[key] = "\n".join(current).rstrip() - key = f"{match.group(1)} {match.group(2)}" - current = pending + [line] - pending = [] - elif key is None: - pending.append(line) - elif line.strip() == "" or line.startswith((" ", "\t")): - current.append(line) - else: - # A bare top-level line (comment, attribute, `open ...`) starts a - # run that attaches to whatever declaration comes next. - pending.append(line) - if key is not None: - blocks[key] = "\n".join(current).rstrip() - return blocks - FACTOR_SERVICE_EXE = "hexbz_factor_service" +FACTOR_BUILD_DEFS = {"hexArithOTarget", "zmod64MulOTarget"} def factorization_blocks(text: str) -> dict[str, str]: @@ -88,7 +54,7 @@ def factorization_blocks(text: str) -> dict[str, str]: """ libs = set(freshness.FACTOR_LIBRARIES) relevant = {} - for name, body in lakefile_blocks(text).items(): + for name, body in freshness.lakefile_blocks(text).items(): kind, _, decl = name.partition(" ") if kind in ("package", "require"): relevant[name] = body @@ -96,6 +62,8 @@ def factorization_blocks(text: str) -> dict[str, str]: relevant[name] = body elif kind == "lean_lib" and decl in libs: relevant[name] = body + elif kind == "def" and decl in FACTOR_BUILD_DEFS: + relevant[name] = body return relevant diff --git a/scripts/bench/check_graphiso_sweep_freshness.py b/scripts/bench/check_graphiso_sweep_freshness.py index d3f70bffa5..f871ccc153 100644 --- a/scripts/bench/check_graphiso_sweep_freshness.py +++ b/scripts/bench/check_graphiso_sweep_freshness.py @@ -18,13 +18,11 @@ sources and headers are tracked. The set and the shared mechanism are declared in ``scripts/bench/sweep_freshness.py``. -The family declares no exemption channel, so any difference has to be -re-measured, with one exception the check verifies for itself: a ``.lean`` -path whose two blobs are equal once their comments are removed -(``lean_comment_only``). Prose under the library tree is edited often -enough, and cannot move a curve, that making every docstring cost a sweep -would either stop the prose being written or make regeneration routine -enough to stop meaning anything. +The family declares no exemption channel, so any runtime-relevant difference +has to be re-measured. The check itself verifies two exceptions: a ``.lean`` +path whose two blobs are equal once their comments are removed, and a lakefile +edit outside the declarations that build the cactus executable. Neither relies +on a persistent assertion that can go stale. """ from __future__ import annotations @@ -42,6 +40,56 @@ RESULTS = freshness.RESULTS SWEEP_RE = re.compile(r"^hexgraphiso-cactus-([0-9a-f]{12})-[^.]+\.jsonl$") +LAKEFILE = "lakefile.lean" + +GRAPHISO_LIBRARIES = {"Hex", "HexBasic", "HexGraph", "HexGraphIso"} +GRAPHISO_EXECUTABLE = "hexgraphiso_cactus" +GRAPHISO_EXTERN_LIBRARY = "hexnautyffi" +GRAPHISO_BUILD_DEFS = {"nautyVendorOTarget", "nautyCanonOTarget"} + + +def graphiso_blocks(text: str) -> dict[str, str]: + """The lakefile declarations that can affect the cactus executable.""" + relevant = {} + for name, body in freshness.lakefile_blocks(text).items(): + kind, _, declaration = name.partition(" ") + if kind in ("package", "require"): + relevant[name] = body + elif kind == "lean_lib" and declaration in GRAPHISO_LIBRARIES: + relevant[name] = body + elif kind == "lean_exe" and declaration == GRAPHISO_EXECUTABLE: + relevant[name] = body + elif kind == "extern_lib" and declaration == GRAPHISO_EXTERN_LIBRARY: + relevant[name] = body + elif kind == "def" and declaration in GRAPHISO_BUILD_DEFS: + relevant[name] = body + return relevant + + +def lakefile_texts_differ(before: str, after: str) -> bool: + """Whether a lakefile edit changes the cactus executable's build.""" + old_blocks = graphiso_blocks(before) + new_blocks = graphiso_blocks(after) + if set(old_blocks) != set(new_blocks): + return True + return any(new_blocks[name] != body for name, body in old_blocks.items()) + + +def build_only_lakefile_edit(difference: freshness.Difference) -> bool: + """A lakefile transition outside the cactus executable's build graph.""" + if difference.path != LAKEFILE: + return False + if difference.baseline is None or difference.current is None: + return False + return not lakefile_texts_differ( + freshness.blob_text(difference.baseline), + freshness.blob_text(difference.current)) + + +def runtime_neutral_edit(difference: freshness.Difference) -> bool: + """A source edit mechanically known not to change either cactus curve.""" + return (freshness.lean_comment_only(difference) + or build_only_lakefile_edit(difference)) def observations() -> tuple[list[freshness.Observation], list[str]]: @@ -71,8 +119,7 @@ def observations() -> tuple[list[freshness.Observation], list[str]]: def main() -> int: found, errors = observations() - verdict = freshness.assess(FAMILY, found, - allow=freshness.lean_comment_only) + verdict = freshness.assess(FAMILY, found, allow=runtime_neutral_edit) errors.extend(verdict.errors) errors.extend(freshness.missing_figures(FAMILY)) diff --git a/scripts/bench/graphiso_pernode_fit.py b/scripts/bench/graphiso_pernode_fit.py index 8cfea37da9..b7301c1293 100644 --- a/scripts/bench/graphiso_pernode_fit.py +++ b/scripts/bench/graphiso_pernode_fit.py @@ -112,13 +112,13 @@ def current_sweep() -> Path: A sweep recorded at the current fingerprint wins. Otherwise the same verdict as `check_graphiso_sweep_freshness.py` applies: when the source differs from the newest recorded sweep only in paths the - freshness check exempts (a `.lean` file whose comments alone changed), - that sweep still measures this source and the fit reads it. + freshness check verifies as runtime-neutral, that sweep still measures + this source and the fit reads it. """ from scripts.bench import check_graphiso_sweep_freshness as check found, errors = check.observations() - verdict = freshness.assess(freshness.GRAPHISO, found, - allow=freshness.lean_comment_only) + verdict = freshness.assess( + freshness.GRAPHISO, found, allow=check.runtime_neutral_edit) covering = verdict.matched or (verdict.baseline if verdict.fresh else None) if errors or covering is None: sys.exit(f"no recorded sweep covers the current source " diff --git a/scripts/bench/proof_only_runtime_exemptions/hexarith-montgomery-invnat-lean-46192ec7-8d9fbf0b.json b/scripts/bench/proof_only_runtime_exemptions/hexarith-montgomery-invnat-lean-46192ec7-8d9fbf0b.json new file mode 100644 index 0000000000..dc8e94a273 --- /dev/null +++ b/scripts/bench/proof_only_runtime_exemptions/hexarith-montgomery-invnat-lean-46192ec7-8d9fbf0b.json @@ -0,0 +1,6 @@ +{ + "path": "HexArith/Montgomery/InvNat.lean", + "baseline_blob": "46192ec785ce77951aca7bbcee2932fc7a599fdf", + "current_blob": "8d9fbf0bf282af9fdc45c8bc64c8c5a32a66633d", + "reason": "Deletes two unused private bv_decide lemmas and their tactic import. The executable definitions, public theorems and every dependency of hexbz_factor_service are unchanged." +} diff --git a/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-a56a63e3-7e6d1e44.json b/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-a56a63e3-c4319f88.json similarity index 63% rename from scripts/bench/proof_only_runtime_exemptions/lakefile-lean-a56a63e3-7e6d1e44.json rename to scripts/bench/proof_only_runtime_exemptions/lakefile-lean-a56a63e3-c4319f88.json index 1fd9a35629..a3ab498976 100644 --- a/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-a56a63e3-7e6d1e44.json +++ b/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-a56a63e3-c4319f88.json @@ -1,6 +1,6 @@ { "path": "lakefile.lean", "baseline_blob": "a56a63e3b99c2af2c1b477347d0b3a5bec8d9b51", - "current_blob": "7e6d1e44cae8e18889a99350b2cfd55d20606efb", - "reason": "The HexArith and HexModArith compiler recipes retain the same cc executable, source paths, object paths, include directory, -fPIC and -O3 flags, and static linking. They only set TMPDIR to the object directory for the compiler process so Mathlib can build inside its existing sandbox. Rebuilding wide_arith.o, mpz_gcdext.o and zmod64_mul.o produced byte-for-byte identical objects. The other changes register independent rational-function, graph-isomorphism, conformance and test targets (including Sturm tests); none changes hexbz_factor_service or its runtime dependency graph." + "current_blob": "c4319f886f102a35fad0b9d3e82a836658968a2a", + "reason": "The HexArith and HexModArith compiler recipes retain the same cc executable, source paths, object paths, include directory, -fPIC and -O3 flags, and static linking. They only set TMPDIR to the object directory for the compiler process so Mathlib can build inside its existing sandbox. Rebuilding wide_arith.o, mpz_gcdext.o and zmod64_mul.o produced byte-for-byte identical objects. The remaining changes since the measurement register independent libraries, conformance drivers and test targets; none changes hexbz_factor_service or its runtime dependency graph." } diff --git a/scripts/bench/sweep_freshness.py b/scripts/bench/sweep_freshness.py index c77abd038c..a7a223770d 100644 --- a/scripts/bench/sweep_freshness.py +++ b/scripts/bench/sweep_freshness.py @@ -39,11 +39,10 @@ A family may also pass ``assess`` an ``allow`` rule, which differs from an exemption in what it costs to trust. An exemption is an assertion a -reviewer has to weigh; a rule decides from the two blobs themselves. -``lean_comment_only`` is the one such rule today: it reads both versions -of a ``.lean`` path and accepts the difference when they are equal with -their comments removed. Editing a docstring therefore does not force a -sweep, and no file records a claim that could go stale. +reviewer has to weigh; a rule decides from the two blobs themselves. The +rules read both versions to recognize comment-only Lean edits and lakefile +edits outside a measured executable's declarations. No file records a +claim that could go stale. """ from __future__ import annotations @@ -52,6 +51,7 @@ import hashlib import json from pathlib import Path +import re import subprocess import sys @@ -62,6 +62,39 @@ MANIFEST_SUFFIX = ".manifest" FINGERPRINT_DIGITS = 12 +# Lines that begin a top-level Lake declaration. Text between declarations +# belongs to the declaration that follows it, including attributes and helper +# definitions used by that declaration. +LAKE_DECL = re.compile( + r"^(?:(?:private|protected|public)\s+)?" + r"(package|require|lean_lib|lean_exe|extern_lib|target|script|def" + r"|input_file|module_facet|library_facet|package_facet)\s+(\S+)") + + +def lakefile_blocks(text: str) -> dict[str, str]: + """Split a lakefile into top-level declaration blocks, keyed by name.""" + blocks: dict[str, str] = {} + key: str | None = None + pending: list[str] = [] + current: list[str] = [] + for line in text.splitlines(): + match = LAKE_DECL.match(line) + if match: + if key is not None: + blocks[key] = "\n".join(current).rstrip() + key = f"{match.group(1)} {match.group(2)}" + current = pending + [line] + pending = [] + elif key is None: + pending.append(line) + elif line.strip() == "" or line.startswith((" ", "\t")): + current.append(line) + else: + pending.append(line) + if key is not None: + blocks[key] = "\n".join(current).rstrip() + return blocks + def git(*args: str) -> str: # `core.quotePath=false` so a non-ASCII path is listed under the name diff --git a/scripts/bench/test_check_factor_sweep_freshness.py b/scripts/bench/test_check_factor_sweep_freshness.py index be93a4c639..3681667315 100644 --- a/scripts/bench/test_check_factor_sweep_freshness.py +++ b/scripts/bench/test_check_factor_sweep_freshness.py @@ -7,6 +7,7 @@ from pathlib import Path from scripts.bench import check_factor_sweep_freshness as guard +from scripts.bench import sweep_freshness as freshness BASE = """\ @@ -21,6 +22,8 @@ lean_lib HexPoly where srcDir := "." +private def hexArithOTarget := "cc" + lean_exe hexbz_factor_service where srcDir := "bench" root := `HexBench.FactorService @@ -29,21 +32,22 @@ class LakefileBlocks(unittest.TestCase): def test_splits_top_level_declarations(self): - blocks = guard.lakefile_blocks(BASE) + blocks = freshness.lakefile_blocks(BASE) self.assertIn("package hex", blocks) self.assertIn("lean_lib HexPoly", blocks) + self.assertIn("def hexArithOTarget", blocks) self.assertIn("lean_exe hexbz_factor_service", blocks) self.assertIn('require "leanprover-community"', blocks) def test_indented_body_stays_with_its_declaration(self): - blocks = guard.lakefile_blocks(BASE) + blocks = freshness.lakefile_blocks(BASE) self.assertIn('root := `HexBench.FactorService', blocks["lean_exe hexbz_factor_service"]) self.assertNotIn("srcDir", blocks["package hex"]) def test_leading_comment_attaches_to_the_following_declaration(self): text = BASE + '\n-- a note\nlean_lib HexNew where\n srcDir := "."\n' - blocks = guard.lakefile_blocks(text) + blocks = freshness.lakefile_blocks(text) self.assertIn("-- a note", blocks["lean_lib HexNew"]) @@ -91,6 +95,11 @@ def test_editing_a_factorization_library_is_a_runtime_change(self): 'lean_lib HexPoly where\n srcDir := "src"') self.assertTrue(guard.lakefile_texts_differ(BASE, after)) + def test_editing_a_factorization_build_helper_is_a_runtime_change(self): + after = BASE.replace('hexArithOTarget := "cc"', + 'hexArithOTarget := "clang"') + self.assertTrue(guard.lakefile_texts_differ(BASE, after)) + class Observations(unittest.TestCase): """Binding a committed report to the source fingerprint it was taken at.""" diff --git a/scripts/bench/test_sweep_freshness.py b/scripts/bench/test_sweep_freshness.py index 55aeeefe1a..fed378684f 100644 --- a/scripts/bench/test_sweep_freshness.py +++ b/scripts/bench/test_sweep_freshness.py @@ -11,6 +11,7 @@ import unittest.mock from pathlib import Path +from scripts.bench import check_graphiso_sweep_freshness as graphiso_guard from scripts.bench import sweep_freshness as freshness @@ -51,6 +52,51 @@ def test_staging_pathspec_keeps_the_globs_and_the_exclusions(self): ":!Lib/SPEC", ":!Lib/README.md"]) +class GraphIsoLakefile(unittest.TestCase): + BASE = """\ +import Lake +open Lake DSL + +package hex where + leanOptions := #[] + +require "leanprover-community" / "batteries" @ git "main" + +lean_lib Hex where + +lean_lib HexBasic where + +lean_lib HexGraph where + +lean_lib HexGraphIso where + +private def nautyVendorOTarget (pkg : Package) := pkg.dir + +extern_lib hexnautyffi (pkg) := do + pure (pkg.dir, #[]) + +lean_exe hexgraphiso_cactus where + srcDir := "bench" + root := `HexGraphIso.Cactus +""" + + def test_unrelated_target_does_not_change_cactus_build(self): + after = self.BASE + "\nlean_lib HexInterval where\n" + self.assertFalse( + graphiso_guard.lakefile_texts_differ(self.BASE, after)) + + def test_cactus_executable_change_is_relevant(self): + after = self.BASE.replace("HexGraphIso.Cactus", "HexGraphIso.CactusV2") + self.assertTrue( + graphiso_guard.lakefile_texts_differ(self.BASE, after)) + + def test_nauty_build_helper_change_is_relevant(self): + after = self.BASE.replace( + "pkg.dir\n\nextern_lib", "pkg.buildDir\n\nextern_lib") + self.assertTrue( + graphiso_guard.lakefile_texts_differ(self.BASE, after)) + + class Differences(unittest.TestCase): BASE = listing(("a.lean", "1" * 40), ("b.lean", "2" * 40))