feat(real-roots-mathlib): checked root counts and a simpler Sturm API

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

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

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

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,37 @@ 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 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 acc := acc * base
+      while k != 0 do
+        checkSystem "polynomial exponentiation"
+        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)
@@ -134,7 +146,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

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.
 

HexRCF/SturmReplay.lean

@@ -110,29 +110,17 @@ 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
 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
 

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