Universal certified arithmetic and root finding

Load Numerics and a certified real backend. Numerics only calls methods on the value; it does not know which plugin constructed it:

The provider always returns its structured work record. When its enclosure is certified, approximation is also a first-class CertifiedApproximation. Reaching maxWork therefore does not throw away completed work or invent digits: the status becomes :budgetExhausted, while the value retains the candidate, the exact enclosure reached so far, and requested/achieved precision metadata. .numerics.Approximation(result) extracts that value. Time and memory are cooperative provider limits; provider capability ceilings and requester limits combine by taking the smaller finite value. Depth remains available, but providers are better placed to define what one depth unit means.

When displayed after derived work it may use an interval spelling; bounded radix conversion such as (1/7).ToDecimalApproximation(5) instead produces the parseable prefix 0.14285?. By contrast, ... remains display-only truncation and never claims a certified enclosure.

The same request shape works with the Float provider:

The Float interval is the exact dyadic value stored by IEEE-754. It is not a certified enclosure of the ideal sine, so the result remains :approximate and carries :noErrorBoundForIntendedReal instead of claiming convergence.

Provider capabilities are data and can be inspected without backend-specific branches:

Relative accuracy, reuse, and generic algorithms

Absolute and relative accuracy can be requested together. Here one percent of a reference magnitude of ten is 1/10, which is tighter than 1/8; addition splits that target into two exact 1/20 operand budgets:

An immutable refinement history makes cache behavior inspectable. In this example the first result is already narrower than 1/100, so both later calls reuse it and retain the original proof record:

The generic algorithms keep their evidence boundary visible:

proved uses the Polynomial root-count protocol and is certified. assumed only observes an exact sign crossing and records continuity as a caller obligation. Likewise, finite adaptive samples are observations, and the one-dimensional optimizer requires the caller to justify its Lipschitz bound:

The three entry points make distinct requests. A provider may support only a subset; unsupported work is returned as a structured result rather than being silently treated as another operation:

Language Halo neighborhoods use this same Core contract directly:

Here epsilon requests enclosure width; it does not enlarge the target. An uncertified provider, including Float when interpreted as an intended real, produces a diagnostic undecided result rather than proving a relation.

Certified ranges for uncertain measurements

A RationalInterval supplied to a supported elementary function denotes every input in that closed interval. The multifunction returns a set-valued image; Range then proves one rational interval containing every output:

The endpoint tolerance controls numerical uncertainty in the outer bounds; it does not shrink the uncertainty in the measurement. Monotonicity, symmetry, Taylor/Lipschitz bounds, and certified trigonometric landmarks provide the proofs. Generic exact interval callbacks can use subdivision, including a callback that directly returns another supported interval image:

See [interval-ranges-tutorial.md](interval-ranges-tutorial.md) for measurement examples, pole/domain handling, hyperbolic and statistical ranges, and result interpretation. [range-certification.md](range-certification.md) describes the certified knowledge most useful for arbitrary user functions.

Arithmetic across real representations

Every refinable singleton-real provider advertises the same semantic contract: it denotes one real, returns certified rational enclosures, and can refine those enclosures arbitrarily. Finite balls are deliberately different: they denote a set, not a hidden singleton.

Arithmetic within one family retains that family. Exact Rationals are embedded as exact leaves, so adding one does not upgrade the result to another real type:

When two different certified families meet, their immutable refinement recipes are adapted to Oracle and the operation result is an Oracle. No eager decimal evaluation is needed; each adapter merely answers bounded enclosure requests using the source's existing refinement protocol:

Oracle conversion accepts only refinable singletons. .oracle.From therefore rejects a finite .ball(midpoint, radius). Use a nested ball recipe when the value is meant to identify one real.

Float is also outside implicit promotion. A Float is a stored binary32 or binary64 scalar, not a refinable certificate for an intended real, so both operands must be converted explicitly:

Expressions such as 1/2 + .float(1/3) and .ar.Sqrt2() + .float(1/3) are dispatch errors rather than silent conversions.

Weighted averaging for n-th roots

.numerics.NthRoot(q, n) creates a universal algorithm real. For a positive upper guess x, the partner q/x^(n-1) lies on the other side of the root. Their ordered pair is a certified enclosure, and the next upper guess is the weighted arithmetic-geometric step

((n - 1) x + q/x^(n-1)) / n.

Each iteration stores exact rational endpoints and discards its expression chain before beginning the next one. Trace entries expose this with actualized=1:

The radicand may itself be any certified real. Consequently the fourth root of two below consumes an algebraic-real provider, while adding a Cauchy real then uses the ordinary cross-family Oracle rule:

An even root of an enclosure that cannot certify a nonnegative radicand returns :unknown with :radicandSignNotCertified; it never chooses a complex or absolute-value interpretation silently.

Rational powers, exponential, and logarithm

Rational powers reuse the same universal root real:

Natural exponential and logarithm use certified rational series bounds. The optional second argument changes the base:

.Log2(x) and .Log10(x) are the corresponding base-selected conveniences. Every non-exact result remains an algorithm real: callers choose precision and work limits only when they ask to enclose or refine it.

Certified trigonometry in radians

Trigonometric functions are universal Numerics algorithms, not Float conversions. Pi() uses a certified Machin-formula enclosure. Sin and Cos use exact rational Taylor bounds, while the input may come from any certified real provider:

Tan, Sec, Csc, and Cot are arithmetic compositions of those universal reals. Their usual poles remain domain boundaries rather than being assigned a finite value.

The inverse functions use monotone endpoint bounds and return radians. Asin/Arcsin, Acos/Arccos, and Atan/Arctan are synonymous spellings:

An inverse-sine or inverse-cosine input that is not certified inside -1:1 returns :unknown with :inverseTrigDomainNotCertified. Numerics never silently selects a complex branch or a Float approximation.

Hyperbolic and special functions

The remaining scientific-calculator functions use the same refinement contract. They can be selected lexically and called without a plugin prefix:

Cbrt, Expm1, Log1p, Radians, and Degrees provide the familiar calculator conveniences. Hyperbolic reciprocal functions preserve their ordinary poles, while inverse hyperbolic functions inherit the certified root and logarithm domain checks.

Special functions publish their real-domain policy rather than silently crossing a branch: LogGamma and the Bessel Y/K families require positive arguments. Gamma continues between its explicit nonpositive-integer poles, and Zeta continues across the real line with its pole at 1 left unresolved. LambertW(x) is branch zero; LambertW(x,-1) is the lower real branch. Uncertified domains return structured :unknown results.

Geometry and the Gamma family

Hypot reuses universal arithmetic and roots. Atan2 accepts (y,x), keeps the quadrant decision certified, and uses the branch -Pi() < angle <= Pi(). The positive-real Gamma family shares the same bounded refinement contract:

Atan2(0,0) is undefined and therefore refines to structured :unknown evidence. Beta and the polygamma functions likewise report :unknown when their positive-real domains cannot be certified.

Compare Kantorovich with direct interval Newton

Kantorovich establishes an initial existence/uniqueness ball from pointwise Newton data, a derivative lower bound, and a derivative-Lipschitz or second-derivative bound. Direct interval Newton starts from a box and uses the complete first-derivative interval on that box. For x^2-2, both routes work:

The direct callback form records evidenceLevel=:assumed: its interval arithmetic and inclusion theorem are exact, but an arbitrary callback pair does not prove its own differentiability or derivative identity. Kantorovich checks its numeric bounds and condition, while retaining the same function/derivative identity assumption.

They also compose. Kantorovich can establish the initial ball; the public box operator can then show the contraction separately:

Interval Newton can prove absence as well as uniqueness. It fails closed when the derivative interval contains zero instead of dividing through it:

Every trace step materializes the input box, midpoint value, derivative enclosure, Newton image, intersection, and classification with bounded work.

Move from scalar Newton to a checked Krawczyk box

Krawczyk generalizes the enclosure idea to square systems. Unlike the callback form above, it accepts public Calculus expression graphs and a derivative collection whose Jacobian identities RiX checks independently.

Here strict Krawczyk inclusion proves a unique positive circle/diagonal intersection. A disjoint operator coordinate proves exclusion. A singular midpoint Jacobian remains :singularPreconditioner: that describes this algorithm's failure on the chosen box, not the absence of roots.

Request exact sign and root-count witnesses

The same witness schema covers exact scalars, polynomial evaluations, and bounded certified refinement. Root counts retain their complete Sturm evidence.