fix: Taylor-model coverage flag, endpoint-tight inequalities, and a non-terminating search

.github/workflows/ci.yml

@@ -537,8 +537,20 @@ jobs:
         # memory safety is hardest to get right. Nightly-only: this shard is
         # already off the PR critical path, so the extra build cost is free
         # where it would not be in Tier 1a.
+        #
+        # RUST_MIN_STACK for the same reason the `tsan` shard sets it, and it is
+        # load-bearing here too: the 2026-08-14 nightly — the first ASan run to
+        # see the parallel code — died with
+        # `AddressSanitizer: stack-overflow ... T1601`, on a rayon worker rather
+        # than the main thread. It is not corruption. `simplify::dispatch`'s
+        # stack governor refills at 512 KiB, ASan's instrumented frames are far
+        # fatter than the uninstrumented ones that margin was tuned for, and
+        # rayon workers start from a 2 MiB default rather than the main thread's
+        # 8 MiB. Raising the worker stack fixes it deterministically and it does
+        # not reproduce uninstrumented.
         env:
           LSAN_OPTIONS: detect_leaks=0
+          RUST_MIN_STACK: "33554432"
         run: |
           RUSTFLAGS="-Zsanitizer=address" \
           cargo +nightly test --workspace --lib --tests \

CHANGELOG.md

@@ -127,6 +127,55 @@ Both are detailed under *Behaviour changes to plan for*.
   this**: a root that never produces a sign change — a double root like
   `(x−1)²` on `[0, 2]`, or `(x²−1)²` on `[-2, 2]` — still answers
   `"undecided"`, because no witness pair exists and none is invented.
+- **`verified_sign` could hang on a rational constant with enough digits.**
+  `sin(x)·D − N·x ≥ 0` on `[0, 3/2]` took 0.05 s at `N/D = 636/1000`, 0.08 s at
+  nine digits, and **over 300 s at twelve** — three extra digits turned
+  milliseconds into a hang. The cause was neither exact rational arithmetic nor
+  repeated conversion but a **non-terminating loop** in the branch-and-bound:
+  a sub-box bisected down to the width floor was pushed back onto the active
+  list, immediately re-selected as the smallest key with nothing changed, and
+  the loop spun *without ever consuming its subdivision budget* — which is why
+  capping `max_subdivisions` at 64 did not help. It only triggered once `tol`
+  became unreachable, and `tol` is an **absolute** width: at `D = 10¹²` the
+  function is of order `10¹¹`, so the default `1e-9` asks for twenty digits and
+  the floor arrives first. Nine digits happened to converge just above the
+  floor, twelve just below. Boxes that reach the floor are now retired out of
+  the active list, their keys still folded into the final bound, so the search
+  always makes progress. Cost is now flat in the size of the constant: 0.33 s at
+  three digits through 0.47 s at sixteen.
+- **Inequalities that are tight at an endpoint no longer stay `"undecided"`.**
+  Cusa–Huygens, Mitrinović–Adamović, Wilker and Huygens were `"true"` on
+  `[0.1, 1.5]` but `"undecided"` on `[0.01, 1.5]` and at `x = 0` — precisely the
+  point that makes them worth stating. Two independent things were in the way.
+  First, `tol` was also the wrong *stopping rule* for a sign question: on
+  `[0.01, 1.5]` the true minimum of the Cusa–Huygens form is `1.7·10⁻¹³`, so the
+  search met the `1e-9` tolerance and stopped with an enclosure that still
+  straddled zero. `verified_sign` now re-runs the search with the sign itself as
+  the goal, refining while the running bound straddles zero instead of to an
+  absolute width. Second, where the margin genuinely *vanishes* no subdivision
+  can ever help, so the box is split: a collar `[a, a+δ]` at the endpoint is
+  handled by a truncated Taylor expansion there, and the rest by the usual
+  branch-and-bound. The two pieces are closed and share the join point `δ`, so
+  their union is the original box with no gap. All four are now `"true"` on
+  `[0, 1.5]`, as is Jordan's inequality stated exactly as
+  `10¹²·sin x − 636619772368·x ≥ 0`.
+  **The remainder is proven, not assumed.** Coefficients `c_k = g⁽ᵏ⁾(a)/k!` are
+  accepted as *zero* only when substitution followed by `simplify` lands on the
+  literal integer `0` — no numeric enclosure can prove a value is zero, and none
+  is asked to — cross-checked against ball arithmetic, and the tail is a
+  Lagrange remainder `|R(t)| ≤ t^m·sup|g⁽ᵐ⁾|/m!` whose sup is a rigorous
+  enclosure over the whole collar. Analyticity, which Taylor's theorem needs, is
+  certified by requiring every derivative `g … g⁽ᵐ⁾` to enclose successfully
+  there. With `c_0 … c_{j−1}` proven zero, `g(a+t) ≥ t^j·[c_j − T(δ)]` and
+  `t^j ≥ 0` finishes it. **Nothing was traded for the extra reach**: a margin
+  that vanishes in the *interior* — `(x − 7/10)²(x + 1)` on `[0, 3/2]` — is
+  still `"undecided"`, because the expansion does not apply there. A leading
+  coefficient proven *negative* now returns `"false"` rather than `"undecided"`,
+  which settles cases no sampling could see: `x³ − x²/1000` is negative only on
+  `(0, 1/1000)`, and each of the four inequalities reversed is refuted at the
+  same endpoint where the original is certified. A strict `"positive"` query is
+  `"false"` where the expression is proven to vanish exactly, so `x² > 0` on
+  `[0, 1]` is `"false"` while `x² ≥ 0` is `"true"`.
 - **`verified_integral` refused removable singularities.** Taylor-model
   quadrature raised `E-VALIDATED-003` on any sub-interval where the reciprocal's
   enclosure contained zero, which put `∫₀¹ ln(1+x)/x dx = π²/12` out of reach
@@ -372,6 +421,58 @@ Both are detailed under *Behaviour changes to plan for*.
 
 ### Added
 
+- **Validated-bounds coverage is queryable: `bounds_supported(expr)` and a
+  `taylor_model` bit in `capabilities()["primitives"]`.** The only
+  per-function coverage flag the agent contract exposed was `numeric_ball`,
+  and it is not the flag that governs `bound_on_box` / `verified_integral` /
+  `verified_no_roots` / `verified_sign`. Ball arithmetic is *pointwise*; a
+  Taylor model needs a rule with a rigorous Lagrange remainder, and ten
+  primitives have the first without the second — `erf`, `erfc`, `bessel_j0`,
+  `bessel_j1`, `digamma`, `lambert_w`, `acosh`, `asinh`, `floor`, `ceil`. So
+  `numeric_ball` said `True` for `bessel_j0` and every bound over a box died
+  on `E-VALIDATED-001`. The boundary was enforced correctly and could not be
+  found ahead of time, which is how a planning loop loses a whole designed
+  workload (Turán-type inequalities for Bessel functions, in the 2026-08-13
+  autoresearch run) to a route it could have ruled out for free.
+
+  `taylor_model` reports it per primitive — `True` for the elementary
+  fragment (`exp`, `log`, `sqrt`, `sin`, `cos`, `tan`, `asin`, `acos`,
+  `atan`, `sinh`, `cosh`, `tanh`, `abs`) and `False` for every special
+  function. `ak.bounds_supported(expr)` asks for a whole expression, without
+  running the bound: it is truthy when nothing in the expression will be
+  refused as unsupported, and carries `.blocker` (the evaluator's own
+  description of the first construct it has no rule for) and `.functions`
+  (every blocking function, so a substitution can be planned in one round
+  rather than found one at a time).
+
+  **Neither is a maintained list.** Both are derived by running the real
+  Taylor evaluator on a probe expression and asking whether it refuses with
+  `E-VALIDATED-001` — a second hand-written table is how `numeric_ball` came
+  to be read as coverage in the first place, and would have been a worse
+  outcome than no flag at all. `tests/test_taylor_model_coverage.py`
+  re-derives the bit the only other way there is, by calling `bound_on_box`
+  on every registered primitive, and fails if the two ever disagree.
+
+  `numeric_ball` itself is *accurate* and stays as it is: those ten
+  primitives really do have Arb ball arithmetic. It answers a different
+  question, and now says so next to a flag that answers this one. A `True`
+  from either means "not `E-VALIDATED-001`" — a covered function can still be
+  refused on a particular box for a domain violation (`E-VALIDATED-003`) or a
+  non-finite enclosure (`-004`), which no box-free predicate can rule out.
+
+  This is deliberately *not* folded into `certifiable`, which asks whether an
+  operation emits a **Lean** certificate and answers from the certificate
+  ledger. A rigorous enclosure is not a Lean proof term and the validated
+  subsystem has no ledger rows; one predicate returning `True` for two kinds
+  of evidence would be a worse contract than two predicates.
+
+  New in Rust: `alkahest_cas::{taylor_model_refusal, taylor_model_blockers,
+  taylor_model_supports, taylor_model_supports_call}` and
+  `Capabilities::TAYLOR_MODEL` (also a `taylor_model` column in
+  `CoverageReport::to_markdown`). `capabilities()["contract_version"]` stays
+  `3`: the row gained a key and lost none, which is the same additive rule
+  the `__all__` freeze check applies.
+
 - **Gröbner results can be read back — `GbPoly.to_expr`, iteration over a
   `GroebnerBasis`, and `expr_to_gbpoly`.** Everything that returned a basis
   returned a handle nobody could open. `GbPoly` exposed only `is_zero` and

alkahest-core/src/holonomic/zeilberger.rs

@@ -806,11 +806,23 @@ mod tests {
             .expect("Franel must be decided at the default bounds");
         let elapsed = start.elapsed();
         println!("franel: order {} in {:?}", result.value.order, elapsed);
-        assert!(
-            elapsed < std::time::Duration::from_secs(10),
-            "Franel took {elapsed:?} at the default bounds — the exact Q(n)(k) \
-             post-processing has regressed to the coefficient blowup it used to have"
-        );
+        // The wall-clock guard is meaningful only in an uninstrumented release
+        // build. Under a sanitizer it is not: the nightly `lsan` shard runs a
+        // debug build with LeakSanitizer, where the whole lib suite takes ~23
+        // minutes and this test breached a 10 s bound while the thing it guards
+        // — the Z[n][k] gcd — was perfectly healthy. A timing assertion that
+        // fails for the instrumentation rather than the regression is a flaky
+        // test, so it is skipped there; the correctness assertions below always
+        // run, in every configuration.
+        // `debug_assertions` is the discriminator: every sanitizer shard builds
+        // in debug, and the release run this guard is written for does not.
+        if !cfg!(debug_assertions) {
+            assert!(
+                elapsed < std::time::Duration::from_secs(10),
+                "Franel took {elapsed:?} at the default bounds — the exact Q(n)(k) \
+                 post-processing has regressed to the coefficient blowup it used to have"
+            );
+        }
 
         let r = &result.value;
         assert_eq!(r.order, 2, "Σ_k C(n,k)³ satisfies an order-2 recurrence");

alkahest-core/src/lib.rs

@@ -222,7 +222,10 @@ pub use number_theory::{
     discrete_log, factorint, isprime, jacobi_symbol, nextprime, nthroot_mod, totient,
     NumberTheoryError, QuadraticDirichlet,
 };
-pub use primitive::{Capabilities, CoverageReport, CoverageRow, Primitive, PrimitiveRegistry};
+pub use primitive::{
+    taylor_model_blockers, taylor_model_refusal, taylor_model_supports, taylor_model_supports_call,
+    Capabilities, CoverageReport, CoverageRow, Primitive, PrimitiveRegistry,
+};
 #[cfg(feature = "groebner")]
 pub use solver::{
     diophantine, expr_to_gbpoly, extract_regular_chain_from_basis, gbpoly_to_expr,
@@ -310,7 +313,10 @@ pub mod stable {
         ResultantError, RootInterval, SparseGcdError, SparseInterpError, UniPoly,
         UniPolyFactorModP, UniPolyFactorization,
     };
-    pub use crate::primitive::{Primitive, PrimitiveRegistry};
+    pub use crate::primitive::{
+        taylor_model_blockers, taylor_model_refusal, taylor_model_supports,
+        taylor_model_supports_call, Primitive, PrimitiveRegistry,
+    };
     pub use crate::real::{
         cad_lift, cad_project, decide, decide_expr, routh_hurwitz, CadError, QeResult, RouthHurwitz,
     };

alkahest-core/src/primitive/mod.rs

@@ -50,6 +50,12 @@ use crate::kernel::{ExprId, ExprPool};
 use std::collections::HashMap;
 use std::fmt;
 
+pub mod taylor_support;
+
+pub use taylor_support::{
+    taylor_model_blockers, taylor_model_refusal, taylor_model_supports, taylor_model_supports_call,
+};
+
 // ---------------------------------------------------------------------------
 // Capability flags
 // ---------------------------------------------------------------------------
@@ -65,6 +71,18 @@ bitflags::bitflags! {
         const NUMERIC_BALL  = 1 << 4;
         const LOWER_LLVM    = 1 << 5;
         const LEAN_THEOREM  = 1 << 6;
+        /// The validated-bounds subsystem ([`crate::validated`]) has a
+        /// rigorous Taylor-model rule for this primitive, so
+        /// `bound_on_box` / `verified_integral` / `verified_no_roots` /
+        /// `verified_sign` will not refuse it with `E-VALIDATED-001`.
+        ///
+        /// **This is not implied by `NUMERIC_BALL`, and does not imply it.**
+        /// Pointwise ball arithmetic and a Taylor model with a rigorous
+        /// remainder are different pieces of work: `erf`, `bessel_j0`,
+        /// `digamma`, `floor`, … have the former and not the latter. The bit
+        /// is derived by running the evaluator (see
+        /// [`taylor_support`]), never from a list.
+        const TAYLOR_MODEL  = 1 << 7;
     }
 }
 
@@ -78,6 +96,7 @@ impl fmt::Display for Capabilities {
             (Capabilities::NUMERIC_BALL, "numeric_ball"),
             (Capabilities::LOWER_LLVM, "lower_llvm"),
             (Capabilities::LEAN_THEOREM, "lean"),
+            (Capabilities::TAYLOR_MODEL, "taylor_model"),
         ];
         let present: Vec<&str> = names
             .iter()
@@ -182,8 +201,8 @@ pub struct CoverageReport {
 impl CoverageReport {
     /// Render as a Markdown table (suitable for CI PR comments or docs).
     pub fn to_markdown(&self) -> String {
-        let header = "| Primitive | simplify | diff_fwd | diff_rev | numeric_f64 | numeric_ball | lower_llvm | lean |\n\
-                      |---|---|---|---|---|---|---|---|";
+        let header = "| Primitive | simplify | diff_fwd | diff_rev | numeric_f64 | numeric_ball | lower_llvm | lean | taylor_model |\n\
+                      |---|---|---|---|---|---|---|---|---|";
         let rows: Vec<String> = self
             .rows
             .iter()
@@ -196,7 +215,7 @@ impl CoverageReport {
                     }
                 };
                 format!(
-                    "| {} | {} | {} | {} | {} | {} | {} | {} |",
+                    "| {} | {} | {} | {} | {} | {} | {} | {} | {} |",
                     r.name,
                     tick(Capabilities::SIMPLIFY),
                     tick(Capabilities::DIFF_FORWARD),
@@ -205,6 +224,7 @@ impl CoverageReport {
                     tick(Capabilities::NUMERIC_BALL),
                     tick(Capabilities::LOWER_LLVM),
                     tick(Capabilities::LEAN_THEOREM),
+                    tick(Capabilities::TAYLOR_MODEL),
                 )
             })
             .collect();
@@ -261,7 +281,7 @@ impl PrimitiveRegistry {
     pub fn capabilities(&self, name: &str) -> Capabilities {
         self.map
             .get(name)
-            .map(|e| e.caps)
+            .map(|e| with_taylor_model(name, e.caps))
             .unwrap_or(Capabilities::empty())
     }
 
@@ -273,7 +293,7 @@ impl PrimitiveRegistry {
             .iter()
             .map(|(name, e)| CoverageRow {
                 name: name.to_string(),
-                caps: e.caps,
+                caps: with_taylor_model(name, e.caps),
             })
             .collect();
         rows.sort_by(|a, b| a.name.cmp(&b.name));
@@ -372,7 +392,9 @@ impl PrimitiveRegistry {
 
     /// Iterate over all registered (name, capabilities) pairs.
     pub fn iter(&self) -> impl Iterator<Item = (&str, Capabilities)> {
-        self.map.iter().map(|(k, e)| (*k, e.caps))
+        self.map
+            .iter()
+            .map(|(k, e)| (*k, with_taylor_model(k, e.caps)))
     }
 }
 
@@ -453,9 +475,35 @@ fn probe_caps(p: &dyn Primitive) -> Capabilities {
     if p.lean_theorem().is_some() {
         caps |= Capabilities::LEAN_THEOREM;
     }
+    // NB: `TAYLOR_MODEL` is deliberately *not* probed here — see
+    // `with_taylor_model`. Probing it at registration cost every caller that
+    // builds a registry, which `default_registry()` does on hot paths.
     caps
 }
 
+/// Add [`Capabilities::TAYLOR_MODEL`] to a primitive's stored capabilities.
+///
+/// This bit is resolved when the capabilities are *read*, not when the
+/// primitive is registered. It is not a slot on the `Primitive` trait: the
+/// validated-bounds subsystem keeps its own per-function rules in
+/// `validated::taylor`, and a primitive cannot self-report whether one exists
+/// without that claim being able to drift — so the answer comes from asking
+/// the evaluator (memoised, see `taylor_support`).
+///
+/// Asking it at registration time made `PrimitiveRegistry::register` pay a
+/// probe per primitive, and `default_registry()` is rebuilt on hot paths such
+/// as `diff` and `series` — it cost `series(sin x, 12)` roughly 30% steady
+/// state and ~4 ms on the first construction in a process. Reading is rare
+/// (`capabilities()`, `bounds_supported`, the coverage report), so the cost
+/// belongs here.
+fn with_taylor_model(name: &str, caps: Capabilities) -> Capabilities {
+    if taylor_support::taylor_model_supports(name) {
+        caps | Capabilities::TAYLOR_MODEL
+    } else {
+        caps
+    }
+}
+
 // ---------------------------------------------------------------------------
 // Built-in primitives
 // ---------------------------------------------------------------------------