the CAS enclosure layer computes proof-carrying rational enclosures of real constants and definite integrals

Identifier: F:cas-enclosure-layer-certified-real-number-enclosures
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.exact-rational-interval-arithmetic, cas.series-truncation-remainder-bounds-as-implemented: each certified head's remainder bound is this implementation's own derivation, re-checked by the verifier against the same formula rather than against an independent one, cas.krawczyk-operator-existence-and-uniqueness-as-implemented, oeis-decimal-expansions-as-published: the replication rows compare against published truncations, not against an independently re-derived expansion, cas.verifier-shares-the-crate-with-the-producer: the certificate checker re-derives every step from the recorded (head, inputs, order) and trusts no recorded number, but it lives in the same crate as the search that produced the certificate, so under ADR-0601 SS1 this is `cas-internal` evidence and NOT reconstruction through the one trust anchor (Kernel::add_declaration). That is why this fact is `computed` and not `proved`.

Recorded description

For each expression in the certified head set -- the field operations and integer powers (exact), sqrt, root_q, exp, ln, atan, sin, cos, pi, erf, Gamma, the Bessel functions J_n, Euler's gamma, the exponential and trigonometric integrals Si, Ci, Ei, li, Shi, Chi, the Fresnel integrals S and C, the inverse circular and hyperbolic functions, the symbolic power x^y, and definite integrals by certified quadrature -- `enclose` returns a closed interval with exact BigRational endpoints containing the true real value, of width at most 2^(-precision), together with one evidence Step per node of the expression tree recording (head, inputs, truncation order, remainder bound). `Enclosure::verify` re-derives every step from (head, inputs, order) alone and accepts only if all eight of its guards hold: step count, head match, input match, remainder not understated, order large enough for the claimed precision, containment, final width, and root output. Multivariate root enclosure additionally uses the Krawczyk operator K(X) = m - Y F(m) + (I - Y J(X))(X - m), where K(X) contained in the interior of X gives existence AND uniqueness of a zero in X. Outside the certified head set, past the series magnitude limit, or on a domain error, the layer DECLINES with a reason rather than returning an uncertified number.

Formal statement

{"contract":"f(X) contains { f(x) : x in X }","endpoint_arithmetic":"exact BigRational; no f64 below the interface","format":"axeyum-cas-enclosure-step-certificate","on_uncertified_input":"decline with a reason, never an uncertified number","root_enclosure":"Krawczyk K(X) = m - Y*F(m) + (I - Y*J(X))*(X - m)","verify_guards":["step-count","head-match","input-match","remainder-not-understated","order-sufficient","containment","final-width","root-output"],"version":1,"width_bound":"2^(-precision)"}

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

cas-enclosure-forgery-rejection-suite

Kind: witness-replay
Status: checked

Supports: that Enclosure::verify's eight guards each reject a certificate forged on exactly that axis, so the verifier is not a checker that cannot fail

Checker command

cargo test -p axeyum-cas --lib enclosure::tests

Evidence notes

62 tests. The forgery tests are the load-bearing half: a verifier that accepted a forged remainder bound would make every enclosure in this layer decorative.

cas-enclosure-published-value-replication

Kind: published-value-replication
Status: checked

Supports: that the certified enclosures bracket the published decimal expansions of the constants they name, so the layer computes the intended quantity and not merely a self-consistent one

Checker command

cargo test -p axeyum-cas --lib enclosure::tests

Evidence notes

A replication against a published expansion is an independence check on the SEMANTICS (does this compute pi?) that the forgery suite cannot give, since the forgery suite would pass equally on a layer that certified enclosures of the wrong constant.

cas-enclosure-decline-behaviour

Kind: witness-replay
Status: checked

Supports: that the layer declines rather than approximating when it leaves its certified set -- the property that makes a returned enclosure meaningful

Checker command

cargo test -p axeyum-cas --lib enclosure_special::tests

Evidence notes

30 tests, covering the Krawczyk system route and its declines (non-square system, singular Jacobian, multiple root).

cas-enclosure-certified-integral

Kind: witness-replay
Status: checked

Supports: that definite integrals are enclosed by quadrature whose certificate records the partition, so the bound is replayable rather than asserted

Checker command

cargo test -p axeyum-cas --lib enclosure_integral::tests

Evidence notes

44 tests.

Provenance

{
  "date": "2026-09-06",
  "established_by": "lane ledger-coverage (ADR-1674): registered from the existing axeyum-cas implementation and its own certificate verifiers; no new mathematics was produced by this lane",
  "source": "crates/axeyum-cas/src/enclosure.rs, enclosure_integral.rs, enclosure_special.rs (7,759 lines together)",
  "prior_art": [
    {
      "who": "R. E. Moore; and the modern rigorous-numerics tradition (Tucker, Rump)",
      "what": "interval arithmetic and validated numerics; the Krawczyk operator for verified root existence and uniqueness",
      "where": "Moore, Interval Analysis (1966); Krawczyk, Computing 4 (1969); Tucker, Validated Numerics (2011)",
      "attribution": "standard textbook attribution; this lane did not consult the primary sources"
    }
  ]
}