omnibias.core.verified.transcend
Coefficient recurrences, activation contracts, jet algebra, and verified arithmetic shared by the numerical backends.
import omnibias.core.verified.transcendModule contract & mathematical conventions
Rigorous interval enclosures of the transcendental base functions.
The interval *algebra* in omnibias.core.verified.interval is exact up to
outward directed rounding, but it cannot by itself bound a transcendental such
as \tanh. This module supplies guaranteed enclosures of exp,
tanh and sigmoid at interval arguments.
Two backends, selected automatically:
- **mpmath (preferred).** Elementary functions use its directed interval context. Composites retain intervals throughout. Error-function tails use explicit positive-series or integration-by-parts remainder bounds; Bessel I uses a positive series. Already enclosed endpoints are rounded outward to binary64, including gradual underflow. A high-precision point value and an assumed extra ulp are not used as an enclosure proof.
- **stdlib fallback.** Without mpmath the value is taken from the platform
mathlibm and inflated byFALLBACK_ULPSrepresentable steps in each direction. This is rigorous *provided* the libm error is belowFALLBACK_ULPSulp -- true for every mainstream correctly-rounded-ish libm (glibc boundstanh/expwell under 2 ulp).backend_namereports"libm_fallback"on this path so a certificate can record it honestly. Certificate sealing that asserts unconditional soundness (or runs undercertificate_mode/set_strict_backend) *refuses* this path rather than silently accepting a conditional enclosure.
mpmath is intentionally an *optional* dependency: it is imported lazily via
importlib so omnibias.core keeps its zero-dependency contract and
the strict type gate never tries to resolve an un-stubbed module.
besseli_iv is the one exception to the second bullet. Its mpmath-free
path is a truncated all-positive series with a geometric tail bound, not a
libm reading, so it is *unconditionally* rigorous: it neither trips
libm_fallback_used nor is refused by strict_backend.
Shared formulas do not imply universal floating-point identity. Verify dtype, shape, derivative-order support, and the stated numerical assumptions for the path you use.
BACKEND_LIBM_FALLBACK
omnibias.core.verified.transcend.BACKEND_LIBM_FALLBACKSource ↗BACKEND_LIBM_FALLBACK: str = 'libm_fallback'Stamp value recorded when the conditionally-rigorous stdlib path is active.
Named libm_fallback (not bare libm) so a sealed certificate cannot be
misread as claiming a fully verified libm.
Read the implementation
BACKEND_LIBM_FALLBACK: str = "libm_fallback"BACKEND_MPMATH
omnibias.core.verified.transcend.BACKEND_MPMATHSource ↗BACKEND_MPMATH: str = 'mpmath'Stamp value recorded when the high-precision backend is active.
Read the implementation
BACKEND_MPMATH: str = "mpmath"BESSELI_SERIES_MAX_ARG
omnibias.core.verified.transcend.BESSELI_SERIES_MAX_ARGSource ↗BESSELI_SERIES_MAX_ARG: float = 600.0Largest argument the mpmath-free besseli_iv series accepts. I_n(z)
grows like e^z, so beyond roughly z = 709 the individual series terms
overflow a double and the "enclosure" would degenerate to [inf, inf] -- an
*unsound* bound. Refusing early is the only honest option; the same explicit series cap is applied with mpmath installed.
Regression example · bessel refuses the unproved overflow region even with mpmath
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_bessel_refuses_the_unproved_overflow_region_even_with_mpmath() -> None:
with tr.certificate_mode(), pytest.raises(ValueError, match="overflow"):
tr.besseli_point(0, tr.BESSELI_SERIES_MAX_ARG+1)python -m pytest packages/omnibias-core/tests/test_transcend_directed_soundness.py -k test_bessel_refuses_the_unproved_overflow_region_even_with_mpmath -qRegression example · the series refuses an argument it cannot bound soundly
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_the_series_refuses_an_argument_it_cannot_bound_soundly(
monkeypatch: pytest.MonkeyPatch,
) -> None:
"""Beyond the cap the terms overflow, so refusing beats returning ``[inf, inf]``."""
with _without_mpmath(monkeypatch), pytest.raises(ValueError, match="overflow"):
besseli_point(0, BESSELI_SERIES_MAX_ARG + 1.0)python -m pytest packages/omnibias-core/tests/verified/test_besseli.py -k test_the_series_refuses_an_argument_it_cannot_bound_soundly -qRead the implementation
BESSELI_SERIES_MAX_ARG: float = 600.0BESSELI_SERIES_MAX_TERMS
omnibias.core.verified.transcend.BESSELI_SERIES_MAX_TERMSSource ↗BESSELI_SERIES_MAX_TERMS: int = 4096Term budget for the mpmath-free besseli_iv series. Convergence needs
roughly z / 2 terms before the ratio test bites, so this is ample for every
argument BESSELI_SERIES_MAX_ARG admits.
Read the implementation
BESSELI_SERIES_MAX_TERMS: int = 4096E_IV
omnibias.core.verified.E_IVSource ↗E_IV = exp_iv(Interval.point(1.0))A rigorous enclosure of Euler's number e = exp(1) via exp_iv. It
uses the active transcendental backend (mpmath when present, else the
ulp-inflated libm fallback), so it is exactly as rigorous as any other
exp_iv call -- the public constant that Euler-Maclaurin / asymptotic
enclosures compose with (alongside PI_IV).
Regression example · e iv encloses math e tightly
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_e_iv_encloses_math_e_tightly() -> None:
assert E_IV.lo <= math.e <= E_IV.hi
assert E_IV.width < 1e-14python -m pytest packages/omnibias-core/tests/verified/test_constants.py -k test_e_iv_encloses_math_e_tightly -qRegression example · constants are nondegenerate intervals
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_constants_are_nondegenerate_intervals() -> None:
assert isinstance(PI_IV, Interval)
assert isinstance(E_IV, Interval)
assert PI_IV.lo < PI_IV.hi
assert E_IV.lo < E_IV.hipython -m pytest packages/omnibias-core/tests/verified/test_constants.py -k test_constants_are_nondegenerate_intervals -qRead the implementation
E_IV = exp_iv(Interval.point(1.0))Other public import paths
omnibias.core.verified.E_IVomnibias.core.verified.transcend.E_IV
FALLBACK_ULPS
omnibias.core.verified.transcend.FALLBACK_ULPSSource ↗FALLBACK_ULPS: int = 4ulp inflation applied to each endpoint in the stdlib fallback.
Read the implementation
FALLBACK_ULPS: int = 4MPMATH_DPS
omnibias.core.verified.transcend.MPMATH_DPSSource ↗MPMATH_DPS: int = 60high-precision working decimal digits for the mpmath backend.
Regression example · private context reuse does not share caller or thread precision
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_private_context_reuse_does_not_share_caller_or_thread_precision() -> None:
from concurrent.futures import ThreadPoolExecutor
from threading import Barrier
context = tr._iv_context(mp)
assert tr._iv_context(mp) is context
old = mp.iv.dps
try:
mp.iv.dps = 3
assert tr._iv_context(mp).dps == tr.MPMATH_DPS
finally:
mp.iv.dps = old
barrier = Barrier(2)
def thread_context() -> int:
local = tr._iv_context(mp)
barrier.wait(timeout=5)
return id(local)
with ThreadPoolExecutor(max_workers=2) as executor:
first, second = executor.submit(thread_context), executor.submit(thread_context)
assert first.result() != second.result()python -m pytest packages/omnibias-core/tests/test_transcend_directed_soundness.py -k test_private_context_reuse_does_not_share_caller_or_thread_precision -qRead the implementation
MPMATH_DPS: int = 60PI_IV
omnibias.core.verified.PI_IVSource ↗PI_IV = Interval(_pred(math.pi), _succ(math.pi))A rigorous double bracket of pi. math.pi is the nearest double to the
true pi (within half a ulp), so widening it one representable step in each
direction provably straddles pi with margin. Kept as plain stdlib (no
mpmath dependency) because soundness needs only a *valid* enclosure -- a wider
bracket merely makes the extremum test below conservatively report an extremum
slightly more often, which only ever widens the result to the exact +/-1. This
is the public constant Euler-Maclaurin / zeta / asymptotic enclosures compose
with; _PI_IV is retained as a private alias for the trig extremum tests.
Regression example · pi iv encloses math pi tightly
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_pi_iv_encloses_math_pi_tightly() -> None:
assert PI_IV.lo <= math.pi <= PI_IV.hi
assert PI_IV.width < 1e-14python -m pytest packages/omnibias-core/tests/verified/test_constants.py -k test_pi_iv_encloses_math_pi_tightly -qRegression example · private alias is public constant
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_private_alias_is_public_constant() -> None:
# Trig extremum tests still reach pi via the retained private alias.
assert _PI_IV is PI_IVpython -m pytest packages/omnibias-core/tests/verified/test_constants.py -k test_private_alias_is_public_constant -qRead the implementation
PI_IV = Interval(_pred(math.pi), _succ(math.pi))Other public import paths
omnibias.core.verified.PI_IVomnibias.core.verified.transcend.PI_IV
atan_iv
omnibias.core.verified.atan_ivSource ↗atan_iv(x: Interval) -> IntervalGuaranteed enclosure of atan(x) (monotone; clamped to (-pi/2, pi/2)).
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
IntervalExecuted regression · hardy pair encloses random sample
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_hardy_pair_encloses_random_sample() -> None:
rng = random.Random(17)
for _ in range(40):
y = rng.uniform(-8.0, 8.0)
a = rng.uniform(0.2, 3.0)
alpha = rng.uniform(0.51, 1.2)
p, q = hardy_pair(y, a, alpha)
assert p.contains(_true_p(y, a, alpha))
assert q.contains(_true_q(y, a, alpha))python -m pytest "packages/omnibias-core/tests/verified/test_hardy_line.py::test_hardy_pair_encloses_random_sample" -qRead the implementation
def atan_iv(x: Interval) -> Interval:
"""Guaranteed enclosure of ``atan(x)`` (monotone; clamped to ``(-pi/2, pi/2)``)."""
lo, hi = _monotone_increasing("atan", x)
return Interval(max(lo, -_HALF_PI_HI), min(hi, _HALF_PI_HI))Other public import paths
omnibias.core.verified.atan_ivomnibias.core.verified.transcend.atan_iv
atan_point
omnibias.core.verified.atan_pointSource ↗atan_point(x: float) -> IntervalGuaranteed enclosure of atan(x) at a scalar point x.
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
IntervalExecuted regression · atan cap does not cut off pi over two
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_atan_cap_does_not_cut_off_pi_over_two() -> None:
with tr.certificate_mode(), mp.workdps(140):
for x in (1e20, 1e100, 1e300):
assert _contains(tr.atan_point(x), mp.atan(mp.mpf(x)))
assert _contains(tr.atan_point(-x), mp.atan(-mp.mpf(x)))
assert tr.atan_point(1e100).hi > math.pi/2python -m pytest "packages/omnibias-core/tests/test_transcend_directed_soundness.py::test_atan_cap_does_not_cut_off_pi_over_two" -qRead the implementation
def atan_point(x: float) -> Interval:
"""Guaranteed enclosure of ``atan(x)`` at a scalar point ``x``."""
lo, hi = _enclose_point("atan", x)
return Interval(max(lo, -_HALF_PI_HI), min(hi, _HALF_PI_HI))Other public import paths
omnibias.core.verified.atan_pointomnibias.core.verified.transcend.atan_point
backend_name
omnibias.core.verified.backend_nameSource ↗backend_name() -> str"mpmath" when the high-precision backend is active, else "libm_fallback".
strExecuted regression · honesty defaults to no unproven claim
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_honesty_defaults_to_no_unproven_claim() -> None:
cert = make_certificate(claim="benign", payload={"type": "interval"})
assert cert["honesty"] == {"unproven_claim": False}python -m pytest "packages/omnibias-core/tests/test_certificate.py::test_honesty_defaults_to_no_unproven_claim" -qRegression example · require rigorous backend accepts mpmath
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_require_rigorous_backend_accepts_mpmath(monkeypatch: pytest.MonkeyPatch) -> None:
monkeypatch.setattr(transcend, "_mpmath", lambda: object())
assert transcend.backend_name() == "mpmath"
transcend.require_rigorous_backend() # must not raisepython -m pytest packages/omnibias-core/tests/test_certificate_audit_regressions.py -k test_require_rigorous_backend_accepts_mpmath -qRead the implementation
def backend_name() -> str:
"""``"mpmath"`` when the high-precision backend is active, else ``"libm_fallback"``."""
return BACKEND_MPMATH if _mpmath() is not None else BACKEND_LIBM_FALLBACKOther public import paths
omnibias.core.verified.backend_nameomnibias.core.verified.transcend.backend_name
besseli_iv
omnibias.core.verified.besseli_ivSource ↗besseli_iv(n: int, x: Interval) -> IntervalGuaranteed enclosure of the modified Bessel function I_n over x.
I_n is the eigenvalue-generating function of the Wilson lattice transfer
matrix, whose character expansion has I_n ratios as coefficients.
The order is an integer and negative orders fold through I_{-n} = I_n.
Bounding the *range* uses the parity of the function rather than raw endpoint
values, which would be unsound for even orders:
- odd
n--I_nis odd and strictly increasing on the whole real line (I_n' = (I_{n-1} + I_{n+1}) / 2 > 0), so the endpoints do bound it; - even
n--I_nis *even* with its minimum atz = 0, so an interval straddling zero attains its lower bound in the interior, not at an endpoint, and its upper bound at whichever endpoint is farther from zero.
Enclosures always use the unconditionally rigorous ascending series in _besseli_series.
Parameters
| Name | Type & default | Contract |
|---|---|---|
npositional-or-keyword | intRequired | See the operation contract and implementation below. |
xpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
IntervalExplicit validation & failure cases
- When
type(n) is not int, raisesValueError('Bessel order must be an exact integer').
These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.
Executed regression · enclosure contains a dense grid
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_enclosure_contains_a_dense_grid(order: int, lo: float, hi: float) -> None:
out = besseli_iv(order, Interval(lo, hi))
for z in _grid(lo, hi):
value = _true(order, z)
assert out.lo <= value <= out.hi, f"I_{order}({z}) = {value} escaped {out}"python -m pytest "packages/omnibias-core/tests/verified/test_besseli.py::test_enclosure_contains_a_dense_grid[-0.5-4.0-0]" -qRegression example · bessel does not round a different order into a certificate
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_bessel_does_not_round_a_different_order_into_a_certificate(order: object) -> None:
with pytest.raises(ValueError, match="exact integer"):
tr.besseli_point(order, 1)
with pytest.raises(ValueError, match="exact integer"):
tr.besseli_iv(order, Interval(1, 2))python -m pytest packages/omnibias-core/tests/test_transcend_directed_soundness.py -k test_bessel_does_not_round_a_different_order_into_a_certificate -qRead the implementation
def besseli_iv(n: int, x: Interval) -> Interval:
r"""Guaranteed enclosure of the modified Bessel function ``I_n`` over ``x``.
``I_n`` is the eigenvalue-generating function of the Wilson lattice transfer
matrix, whose character expansion has ``I_n`` ratios as coefficients.
The order is an integer and negative orders fold through ``I_{-n} = I_n``.
Bounding the *range* uses the parity of the function rather than raw endpoint
values, which would be unsound for even orders:
* odd ``n`` -- ``I_n`` is odd and strictly increasing on the whole real line
(``I_n' = (I_{n-1} + I_{n+1}) / 2 > 0``), so the endpoints do bound it;
* even ``n`` -- ``I_n`` is *even* with its minimum at ``z = 0``, so an
interval straddling zero attains its lower bound in the interior, not at an
endpoint, and its upper bound at whichever endpoint is farther from zero.
Enclosures always use the unconditionally rigorous ascending series in :func:`_besseli_series`.
"""
if type(n) is not int:
raise ValueError("Bessel order must be an exact integer")
order = abs(n)
if order % 2 == 1:
return Interval(
_besseli_point_signed(order, x.lo).lo,
_besseli_point_signed(order, x.hi).hi,
)
lo_mag, hi_mag = abs(x.lo), abs(x.hi)
nearest = 0.0 if x.contains_zero() else min(lo_mag, hi_mag)
farthest = max(lo_mag, hi_mag)
return Interval(
max(_besseli_nonneg_point(order, nearest).lo, 0.0),
_besseli_nonneg_point(order, farthest).hi,
)Other public import paths
omnibias.core.verified.besseli_ivomnibias.core.verified.transcend.besseli_iv
besseli_point
omnibias.core.verified.besseli_pointSource ↗besseli_point(n: int, z: float) -> IntervalGuaranteed enclosure of the modified Bessel function I_n(z) at a scalar.
The order must be an integer; negative orders are folded through the exact
identity I_{-n} = I_n.
Parameters
| Name | Type & default | Contract |
|---|---|---|
npositional-or-keyword | intRequired | See the operation contract and implementation below. |
zpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
IntervalExplicit validation & failure cases
- When
type(n) is not int, raisesValueError('Bessel order must be an exact integer').
These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.
Executed regression · a negative order folds onto the positive one
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_a_negative_order_folds_onto_the_positive_one() -> None:
for order in (1, 2, 5):
for z in (0.3, 2.2):
assert besseli_point(-order, z) == besseli_point(order, z)python -m pytest "packages/omnibias-core/tests/verified/test_besseli.py::test_a_negative_order_folds_onto_the_positive_one" -qRegression example · the enclosure is tight not merely sound
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_the_enclosure_is_tight_not_merely_sound(order: int, z: float) -> None:
out = besseli_point(order, z)
value = _true(order, z)
assert out.width <= 1e-12 * max(abs(value), 1.0)python -m pytest packages/omnibias-core/tests/verified/test_besseli.py -k test_the_enclosure_is_tight_not_merely_sound -qRead the implementation
def besseli_point(n: int, z: float) -> Interval:
"""Guaranteed enclosure of the modified Bessel function ``I_n(z)`` at a scalar.
The order must be an integer; negative orders are folded through the exact
identity ``I_{-n} = I_n``.
"""
if type(n) is not int:
raise ValueError("Bessel order must be an exact integer")
return _besseli_point_signed(abs(n), z)Other public import paths
omnibias.core.verified.besseli_pointomnibias.core.verified.transcend.besseli_point
certificate_mode
omnibias.core.verified.certificate_modeSource ↗certificate_mode() -> Iterator[None]Context that makes the rigorous (mpmath) backend mandatory.
Enter this (or call set_strict_backend True) before computing any
transcendental enclosure that will feed a sealed certificate. Inside the
context the libm fallback raises, and make_certificate refuses to
seal unless backend_name is BACKEND_MPMATH.
Iterator[None]Executed regression · bessel refuses the unproved overflow region even with mpmath
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_bessel_refuses_the_unproved_overflow_region_even_with_mpmath() -> None:
with tr.certificate_mode(), pytest.raises(ValueError, match="overflow"):
tr.besseli_point(0, tr.BESSELI_SERIES_MAX_ARG+1)python -m pytest "packages/omnibias-core/tests/test_transcend_directed_soundness.py::test_bessel_refuses_the_unproved_overflow_region_even_with_mpmath" -qRegression example · erf and cdf series and remainder bounds
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_erf_and_cdf_series_and_remainder_bounds(x: float) -> None:
with tr.certificate_mode(), mp.workdps(150):
z = mp.mpf(x)
assert _contains(tr.erf_point(x), mp.erf(z))
assert _contains(tr.gauss_cdf_point(x), mp.erfc(-z/mp.sqrt(2))/2)python -m pytest packages/omnibias-core/tests/test_transcend_directed_soundness.py -k test_erf_and_cdf_series_and_remainder_bounds -qRead the implementation
def certificate_mode() -> Iterator[None]:
"""Context that makes the rigorous (mpmath) backend mandatory.
Enter this (or call :func:`set_strict_backend` ``True``) before computing any
transcendental enclosure that will feed a sealed certificate. Inside the
context the libm fallback raises, and :func:`make_certificate` refuses to
seal unless :func:`backend_name` is :data:`BACKEND_MPMATH`.
"""
require_rigorous_backend()
previous = set_strict_backend(True)
clear_libm_fallback_used()
try:
yield
finally:
set_strict_backend(previous)Other public import paths
omnibias.core.verified.certificate_modeomnibias.core.verified.transcend.certificate_mode
clear_libm_fallback_used
omnibias.core.verified.clear_libm_fallback_usedSource ↗clear_libm_fallback_used() -> NoneReset the libm_fallback_used sticky flag (tests / fresh certificate scopes).
NoneRegression example · pure rational interval does not acquire a libm stamp
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_pure_rational_interval_does_not_acquire_a_libm_stamp(
monkeypatch: pytest.MonkeyPatch,
) -> None:
"""No evaluated transcendental is distinct from a conditional fallback."""
from omnibias.core.verified import transcend
monkeypatch.setattr(transcend, "_mpmath", lambda: None)
transcend.clear_libm_fallback_used()
cert = make_certificate(claim="rational only", payload={"type": "interval"})
assert certificate_transcend_backend(cert) == NO_TRANSCENDENTAL_BACKEND
assert certificate_is_unconditional(cert)python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_pure_rational_interval_does_not_acquire_a_libm_stamp -qRegression example · the series fallback is unconditionally rigorous
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_the_series_fallback_is_unconditionally_rigorous(
monkeypatch: pytest.MonkeyPatch,
) -> None:
"""It reads no libm value, so it neither trips the flag nor strict mode.
This is the property that separates it from ``_enclose_point``: there is no
"assume libm is accurate to 4 ulp" premise to record, so a certificate built
on it stays unconditional and strict mode has nothing to refuse.
"""
transcend.clear_libm_fallback_used()
previous = set_strict_backend(True)
try:
with _without_mpmath(monkeypatch):
out = besseli_point(0, 1.5)
finally:
set_strict_backend(previous)
assert out.contains(_true(0, 1.5))
assert libm_fallback_used() is Falsepython -m pytest packages/omnibias-core/tests/verified/test_besseli.py -k test_the_series_fallback_is_unconditionally_rigorous -qRead the implementation
def clear_libm_fallback_used() -> None:
"""Reset the :func:`libm_fallback_used` sticky flag (tests / fresh certificate scopes)."""
global _LIBM_FALLBACK_USED
_LIBM_FALLBACK_USED = FalseOther public import paths
omnibias.core.verified.clear_libm_fallback_usedomnibias.core.verified.transcend.clear_libm_fallback_used
cos_iv
omnibias.core.verified.cos_ivSource ↗cos_iv(x: Interval) -> IntervalGuaranteed enclosure of cos over the (possibly wide) interval x.
cos is **not monotone**, so endpoint values alone do not bound it. Its
maxima (cos = +1) sit at *even* multiples of pi and its minima
(cos = -1) at *odd* multiples; away from those it is monotone. The range
is therefore the hull of the two endpoint brackets, widened to +1 / -1
whenever an even / odd multiple of pi lies in x. Membership is tested
on an outward enclosure of x / pi (via _PI_IV), so an interior
extremum is never missed and the enclosure stays rigorous.
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
IntervalExecuted regression · clenshaw curtis encloses sin
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_clenshaw_curtis_encloses_sin(self) -> None:
enc = clenshaw_curtis_integral(_sin_iv, 0.0, math.pi, n=8, deriv_np1_bound=Interval(-1.0, 1.0))
assert enc.contains(2.0)python -m pytest "packages/omnibias-core/tests/verified/test_quadrature_rules.py::TestCertifiedRulesEncloseExact::test_clenshaw_curtis_encloses_sin" -qRegression example · cos iv contains all samples
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_cos_iv_contains_all_samples(lo: float, hi: float) -> None:
enc = cos_iv(Interval(lo, hi))
assert -1.0 <= enc.lo <= enc.hi <= 1.0
for x in _samples(lo, hi):
assert enc.lo <= math.cos(x) <= enc.hipython -m pytest packages/omnibias-core/tests/verified/test_verified_trig.py -k test_cos_iv_contains_all_samples -qRead the implementation
def cos_iv(x: Interval) -> Interval:
r"""Guaranteed enclosure of ``cos`` over the (possibly wide) interval ``x``.
``cos`` is **not monotone**, so endpoint values alone do not bound it. Its
maxima (``cos = +1``) sit at *even* multiples of ``pi`` and its minima
(``cos = -1``) at *odd* multiples; away from those it is monotone. The range
is therefore the hull of the two endpoint brackets, widened to ``+1`` / ``-1``
whenever an even / odd multiple of ``pi`` lies in ``x``. Membership is tested
on an outward enclosure of ``x / pi`` (via :data:`_PI_IV`), so an interior
extremum is never missed and the enclosure stays rigorous.
"""
ca = cos_point(x.lo)
cb = cos_point(x.hi)
lo = min(ca.lo, cb.lo)
hi = max(ca.hi, cb.hi)
lo_over = (Interval.point(x.lo) / _PI_IV).lo # lower bound on x.lo / pi
hi_over = (Interval.point(x.hi) / _PI_IV).hi # upper bound on x.hi / pi
if _has_integer_with_residue(lo_over, hi_over, 0, 2): # even multiple -> max +1
hi = 1.0
if _has_integer_with_residue(lo_over, hi_over, 1, 2): # odd multiple -> min -1
lo = -1.0
return Interval(max(lo, -1.0), min(hi, 1.0))Other public import paths
omnibias.core.verified.cos_ivomnibias.core.verified.transcend.cos_iv
cos_point
omnibias.core.verified.cos_pointSource ↗cos_point(x: float) -> IntervalGuaranteed enclosure of cos(x) at a scalar point x.
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
IntervalExecuted regression · clenshaw curtis encloses sin
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_clenshaw_curtis_encloses_sin(self) -> None:
enc = clenshaw_curtis_integral(_sin_iv, 0.0, math.pi, n=8, deriv_np1_bound=Interval(-1.0, 1.0))
assert enc.contains(2.0)python -m pytest "packages/omnibias-core/tests/verified/test_quadrature_rules.py::TestCertifiedRulesEncloseExact::test_clenshaw_curtis_encloses_sin" -qRegression example · hilbert mode action approx
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_hilbert_mode_action_approx(n: int) -> None:
"""Sanity: H cos(kx)~sin(kx), H sin(kx)~-cos(kx) to O(n*ulp)."""
nodes = uniform_nodes(n)
hmat = hilbert_circulant(n)
tol = 50 * n * 2.3e-16
for k in range(1, n // 2):
hc = matvec(hmat, [cos_point(k * x) for x in nodes])
hs = matvec(hmat, [sin_point(k * x) for x in nodes])
for j, x in enumerate(nodes):
assert abs(hc[j].mid - math.sin(k * x)) < tol
assert abs(hs[j].mid + math.cos(k * x)) < tolpython -m pytest packages/omnibias-core/tests/verified/test_spectral.py -k test_hilbert_mode_action_approx -qRead the implementation
def cos_point(x: float) -> Interval:
"""Guaranteed enclosure of ``cos(x)`` at a scalar point ``x``."""
lo, hi = _enclose_point("cos", x)
return Interval(max(lo, -1.0), min(hi, 1.0))Other public import paths
omnibias.core.verified.cos_pointomnibias.core.verified.transcend.cos_point
cosh_iv
omnibias.core.verified.cosh_ivSource ↗cosh_iv(x: Interval) -> IntervalGuaranteed enclosure of cosh(x) = (e^x + e^{-x}) / 2 over x.
cosh is **not monotone** (it is even, with its minimum 1 at 0), so
an endpoint-only bound would be unsound. Composing the two monotone
exp_iv enclosures instead is rigorous for *any* interval -- including
one that straddles zero -- because the sum of two positive enclosures encloses
e^t + e^{-t} for every t in x. The result stays strictly positive
(cosh >= 1), so sech_iv may take its reciprocal safely.
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
IntervalExecuted regression · g2 jacobian containment
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g2_jacobian_containment() -> None:
report = jacobian_containment_report(n_boxes=1000, seed=3)
assert report["fields"] == 10
assert report["checked"] == 10000
assert report["misses"] == 0
assert report["containment"] is Truepython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g2_jacobian_containment" -qRead the implementation
def cosh_iv(x: Interval) -> Interval:
r"""Guaranteed enclosure of ``cosh(x) = (e^x + e^{-x}) / 2`` over ``x``.
``cosh`` is **not monotone** (it is even, with its minimum ``1`` at ``0``), so
an endpoint-only bound would be unsound. Composing the two monotone
:func:`exp_iv` enclosures instead is rigorous for *any* interval -- including
one that straddles zero -- because the sum of two positive enclosures encloses
``e^t + e^{-t}`` for every ``t`` in ``x``. The result stays strictly positive
(``cosh >= 1``), so :func:`sech_iv` may take its reciprocal safely.
"""
return (exp_iv(x) + exp_iv(-x)) * Interval.point(0.5)Other public import paths
omnibias.core.verified.cosh_ivomnibias.core.verified.transcend.cosh_iv
erf_iv
omnibias.core.verified.erf_ivSource ↗erf_iv(x: Interval) -> IntervalGuaranteed enclosure of erf(x) over x (monotone; clamped to [-1, 1]).
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
IntervalExecuted regression · erf cdf monotone interval contains dense and random
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_erf_cdf_monotone_interval_contains_dense_and_random() -> None:
rng = random.Random(43)
with tr.certificate_mode(), mp.workdps(120):
for lo, hi in ((-20., -12.), (-9., -7.), (-2., 2.), (7., 9.)):
erf_box, cdf_box = tr.erf_iv(Interval(lo, hi)), tr.gauss_cdf_iv(Interval(lo, hi))
nodes = [lo+(hi-lo)*i/80 for i in range(81)]
nodes += [rng.uniform(lo, hi) for _ in range(40)]
for x in nodes:
z = mp.mpf(x)
assert _contains(erf_box, mp.erf(z))
assert _contains(cdf_box, mp.erfc(-z/mp.sqrt(2))/2)python -m pytest "packages/omnibias-core/tests/test_transcend_directed_soundness.py::test_erf_cdf_monotone_interval_contains_dense_and_random" -qRead the implementation
def erf_iv(x: Interval) -> Interval:
"""Guaranteed enclosure of ``erf(x)`` over ``x`` (monotone; clamped to ``[-1, 1]``)."""
lo, hi = _monotone_increasing("erf", x)
return Interval(max(lo, -1.0), min(hi, 1.0))Other public import paths
omnibias.core.verified.erf_ivomnibias.core.verified.transcend.erf_iv
erf_point
omnibias.core.verified.erf_pointSource ↗erf_point(x: float) -> IntervalGuaranteed enclosure of erf(x) at a scalar point x.
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
IntervalExecuted regression · erf and cdf series and remainder bounds
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_erf_and_cdf_series_and_remainder_bounds(x: float) -> None:
with tr.certificate_mode(), mp.workdps(150):
z = mp.mpf(x)
assert _contains(tr.erf_point(x), mp.erf(z))
assert _contains(tr.gauss_cdf_point(x), mp.erfc(-z/mp.sqrt(2))/2)python -m pytest "packages/omnibias-core/tests/test_transcend_directed_soundness.py::test_erf_and_cdf_series_and_remainder_bounds[-0.1]" -qRead the implementation
def erf_point(x: float) -> Interval:
"""Guaranteed enclosure of ``erf(x)`` at a scalar point ``x``."""
lo, hi = _enclose_point("erf", x)
return Interval(max(lo, -1.0), min(hi, 1.0))Other public import paths
omnibias.core.verified.erf_pointomnibias.core.verified.transcend.erf_point
exp_iv
omnibias.core.verified.exp_ivSource ↗exp_iv(x: Interval) -> IntervalGuaranteed enclosure of exp(x) over the interval x.
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
IntervalExecuted regression · gaussian weight matches exp
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_gaussian_weight_matches_exp() -> None:
for x in (-1.5, 0.0, 0.7, 3.0):
w = gaussian_weight(x)
ref = math.exp(-0.5 * x * x)
assert w.lo <= ref <= w.hipython -m pytest "packages/omnibias-core/tests/verified/test_hermite_basis.py::test_gaussian_weight_matches_exp" -qRegression example · exp iv supersets oracle on grid
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_exp_iv_supersets_oracle_on_grid() -> None:
xs = [i / 8.0 for i in range(-80, 81)]
for x in xs:
assert_superset(exp_iv(Interval.point(x)), oracle_exp(x), name=f"exp@{x}")python -m pytest tests/test_oracles.py -k test_exp_iv_supersets_oracle_on_grid -qRead the implementation
def exp_iv(x: Interval) -> Interval:
"""Guaranteed enclosure of ``exp(x)`` over the interval ``x``."""
lo, hi = _monotone_increasing("exp", x)
return Interval(lo, hi)Other public import paths
omnibias.core.verified.exp_ivomnibias.core.verified.transcend.exp_iv
gauss_cdf_iv
omnibias.core.verified.gauss_cdf_ivSource ↗gauss_cdf_iv(x: Interval) -> IntervalGuaranteed enclosure of the standard-normal CDF Phi (monotone; clamped to [0, 1]).
Phi(x) = 1/2 (1 + erf(x / sqrt 2)) is strictly increasing, so the enclosure
is built from the lower endpoint at x.lo and the upper endpoint at x.hi.
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
IntervalExecuted regression · g2 jacobian containment
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g2_jacobian_containment() -> None:
report = jacobian_containment_report(n_boxes=1000, seed=3)
assert report["fields"] == 10
assert report["checked"] == 10000
assert report["misses"] == 0
assert report["containment"] is Truepython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g2_jacobian_containment" -qRegression example · erf cdf monotone interval contains dense and random
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_erf_cdf_monotone_interval_contains_dense_and_random() -> None:
rng = random.Random(43)
with tr.certificate_mode(), mp.workdps(120):
for lo, hi in ((-20., -12.), (-9., -7.), (-2., 2.), (7., 9.)):
erf_box, cdf_box = tr.erf_iv(Interval(lo, hi)), tr.gauss_cdf_iv(Interval(lo, hi))
nodes = [lo+(hi-lo)*i/80 for i in range(81)]
nodes += [rng.uniform(lo, hi) for _ in range(40)]
for x in nodes:
z = mp.mpf(x)
assert _contains(erf_box, mp.erf(z))
assert _contains(cdf_box, mp.erfc(-z/mp.sqrt(2))/2)python -m pytest packages/omnibias-core/tests/test_transcend_directed_soundness.py -k test_erf_cdf_monotone_interval_contains_dense_and_random -qRead the implementation
def gauss_cdf_iv(x: Interval) -> Interval:
"""Guaranteed enclosure of the standard-normal CDF ``Phi`` (monotone; clamped to ``[0, 1]``).
``Phi(x) = 1/2 (1 + erf(x / sqrt 2))`` is strictly increasing, so the enclosure
is built from the lower endpoint at ``x.lo`` and the upper endpoint at ``x.hi``.
"""
lo, hi = _monotone_increasing("gauss_cdf", x)
return Interval(max(lo, 0.0), min(hi, 1.0))Other public import paths
omnibias.core.verified.gauss_cdf_ivomnibias.core.verified.transcend.gauss_cdf_iv
gauss_cdf_point
omnibias.core.verified.gauss_cdf_pointSource ↗gauss_cdf_point(x: float) -> IntervalGuaranteed enclosure of the standard-normal CDF Phi(x) at a scalar point x.
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
IntervalExecuted regression · erf and cdf series and remainder bounds
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_erf_and_cdf_series_and_remainder_bounds(x: float) -> None:
with tr.certificate_mode(), mp.workdps(150):
z = mp.mpf(x)
assert _contains(tr.erf_point(x), mp.erf(z))
assert _contains(tr.gauss_cdf_point(x), mp.erfc(-z/mp.sqrt(2))/2)python -m pytest "packages/omnibias-core/tests/test_transcend_directed_soundness.py::test_erf_and_cdf_series_and_remainder_bounds[-0.1]" -qRegression example · gaussian tail cancellation counterexample is fixed
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_gaussian_tail_cancellation_counterexample_is_fixed() -> None:
with tr.certificate_mode(), mp.workdps(140):
value = mp.erfc(mp.mpf(20)/mp.sqrt(2))/2
box = tr.gauss_cdf_point(-20.0)
assert _contains(box, value)
assert box.lo > 0
assert box.width < 1e-103
# The previous mp point 1+erf path returned [0, minimum-subnormal].
assert value > mp.mpf(math.ulp(0.0))python -m pytest packages/omnibias-core/tests/test_transcend_directed_soundness.py -k test_gaussian_tail_cancellation_counterexample_is_fixed -qRead the implementation
def gauss_cdf_point(x: float) -> Interval:
"""Guaranteed enclosure of the standard-normal CDF ``Phi(x)`` at a scalar point ``x``."""
lo, hi = _enclose_point("gauss_cdf", x)
return Interval(max(lo, 0.0), min(hi, 1.0))Other public import paths
omnibias.core.verified.gauss_cdf_pointomnibias.core.verified.transcend.gauss_cdf_point
libm_fallback_used
omnibias.core.verified.libm_fallback_usedSource ↗libm_fallback_used() -> boolTrue if the libm fallback has produced at least one enclosure this process.
boolExecuted regression · honesty defaults to no unproven claim
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_honesty_defaults_to_no_unproven_claim() -> None:
cert = make_certificate(claim="benign", payload={"type": "interval"})
assert cert["honesty"] == {"unproven_claim": False}python -m pytest "packages/omnibias-core/tests/test_certificate.py::test_honesty_defaults_to_no_unproven_claim" -qRegression example · the series fallback is unconditionally rigorous
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_the_series_fallback_is_unconditionally_rigorous(
monkeypatch: pytest.MonkeyPatch,
) -> None:
"""It reads no libm value, so it neither trips the flag nor strict mode.
This is the property that separates it from ``_enclose_point``: there is no
"assume libm is accurate to 4 ulp" premise to record, so a certificate built
on it stays unconditional and strict mode has nothing to refuse.
"""
transcend.clear_libm_fallback_used()
previous = set_strict_backend(True)
try:
with _without_mpmath(monkeypatch):
out = besseli_point(0, 1.5)
finally:
set_strict_backend(previous)
assert out.contains(_true(0, 1.5))
assert libm_fallback_used() is Falsepython -m pytest packages/omnibias-core/tests/verified/test_besseli.py -k test_the_series_fallback_is_unconditionally_rigorous -qRead the implementation
def libm_fallback_used() -> bool:
"""``True`` if the libm fallback has produced at least one enclosure this process."""
return _LIBM_FALLBACK_USEDOther public import paths
omnibias.core.verified.libm_fallback_usedomnibias.core.verified.transcend.libm_fallback_used
ln_iv
omnibias.core.verified.ln_ivSource ↗ln_iv(x: Interval) -> IntervalGuaranteed enclosure of ln(x) over x (monotone; requires x.lo > 0).
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
IntervalExplicit validation & failure cases
- When
x.lo <= 0.0, raisesValueError('ln_iv requires a strictly positive interval').
These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.
Executed regression · potential matches mpmath
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_potential_matches_mpmath() -> None:
for x, y in _PTS:
enc = newtonian_potential(x, y, _A)
assert enc.lo <= float(_N(x, y, _A)) <= enc.hipython -m pytest "packages/omnibias-core/tests/verified/test_riesz.py::test_potential_matches_mpmath" -qRegression example · strict mode refuses libm fallback
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_strict_mode_refuses_libm_fallback(monkeypatch: pytest.MonkeyPatch) -> None:
# Simulate mpmath being unavailable so the libm fallback path is taken.
monkeypatch.setattr(transcend, "_mpmath", lambda: None)
assert transcend.backend_name() == "libm_fallback"
with pytest.raises(RuntimeError):
transcend.require_rigorous_backend()
prev = transcend.set_strict_backend(True)
try:
with pytest.raises(RuntimeError):
transcend.exp_iv(Interval.point(0.5))
with pytest.raises(RuntimeError):
transcend.ln_iv(Interval(0.5, 2.0))
finally:
transcend.set_strict_backend(prev)
# With strict off the (conditionally rigorous) libm fallback still encloses.
transcend.clear_libm_fallback_used()
enc = transcend.exp_iv(Interval.point(0.0))
assert enc.lo <= 1.0 <= enc.hi
assert transcend.libm_fallback_used()python -m pytest packages/omnibias-core/tests/test_certificate_audit_regressions.py -k test_strict_mode_refuses_libm_fallback -qRead the implementation
def ln_iv(x: Interval) -> Interval:
"""Guaranteed enclosure of ``ln(x)`` over ``x`` (monotone; requires ``x.lo > 0``)."""
if x.lo <= 0.0:
raise ValueError("ln_iv requires a strictly positive interval")
lo, hi = _monotone_increasing("log", x)
return Interval(lo, hi)Other public import paths
omnibias.core.verified.ln_ivomnibias.core.verified.transcend.ln_iv
ln_point
omnibias.core.verified.ln_pointSource ↗ln_point(x: float) -> IntervalGuaranteed enclosure of ln(x) at a scalar point x > 0.
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
IntervalExplicit validation & failure cases
- When
x <= 0.0, raisesValueError('ln_point requires x > 0').
These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.
Read the implementation
def ln_point(x: float) -> Interval:
"""Guaranteed enclosure of ``ln(x)`` at a scalar point ``x > 0``."""
if x <= 0.0:
raise ValueError("ln_point requires x > 0")
lo, hi = _enclose_point("log", x)
return Interval(lo, hi)Other public import paths
omnibias.core.verified.ln_pointomnibias.core.verified.transcend.ln_point
require_rigorous_backend
omnibias.core.verified.require_rigorous_backendSource ↗require_rigorous_backend() -> NoneRaise RuntimeError unless the rigorous (mpmath) backend is active.
The stdlib libm fallback is only *conditionally* rigorous -- it assumes the
platform math error is below FALLBACK_ULPS ulp, which the language
does **not** guarantee. Call this before asserting that a certificate whose
proof chain touches a transcendental (spectral gaps via ln_iv, Hilbert
kernels, ...) is unconditionally sound. make_certificate also calls
this automatically under certificate_mode / strict mode / an
unconditional_transcendentals honesty claim.
NoneExplicit validation & failure cases
- When
backend_name() != BACKEND_MPMATH, raisesRuntimeError(f'rigorous transcendental backend (mpmath) required but unavailable: the libm fallback is only conditionally rigorous (assumes < {FALLBACK_ULPS} ulp libm error). Install mpmath to seal an unconditionally rigorous certificate.').
These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.
Executed regression · bessel refuses the unproved overflow region even with mpmath
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_bessel_refuses_the_unproved_overflow_region_even_with_mpmath() -> None:
with tr.certificate_mode(), pytest.raises(ValueError, match="overflow"):
tr.besseli_point(0, tr.BESSELI_SERIES_MAX_ARG+1)python -m pytest "packages/omnibias-core/tests/test_transcend_directed_soundness.py::test_bessel_refuses_the_unproved_overflow_region_even_with_mpmath" -qRegression example · require rigorous backend accepts mpmath
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_require_rigorous_backend_accepts_mpmath(monkeypatch: pytest.MonkeyPatch) -> None:
monkeypatch.setattr(transcend, "_mpmath", lambda: object())
assert transcend.backend_name() == "mpmath"
transcend.require_rigorous_backend() # must not raisepython -m pytest packages/omnibias-core/tests/test_certificate_audit_regressions.py -k test_require_rigorous_backend_accepts_mpmath -qRead the implementation
def require_rigorous_backend() -> None:
"""Raise :class:`RuntimeError` unless the rigorous (mpmath) backend is active.
The stdlib ``libm`` fallback is only *conditionally* rigorous -- it assumes the
platform ``math`` error is below :data:`FALLBACK_ULPS` ulp, which the language
does **not** guarantee. Call this before asserting that a certificate whose
proof chain touches a transcendental (spectral gaps via :func:`ln_iv`, Hilbert
kernels, ...) is unconditionally sound. :func:`make_certificate` also calls
this automatically under :func:`certificate_mode` / strict mode / an
``unconditional_transcendentals`` honesty claim.
"""
if backend_name() != BACKEND_MPMATH:
raise RuntimeError(
"rigorous transcendental backend (mpmath) required but unavailable: "
f"the libm fallback is only conditionally rigorous (assumes < "
f"{FALLBACK_ULPS} ulp libm error). Install mpmath to seal an "
"unconditionally rigorous certificate."
)Other public import paths
omnibias.core.verified.require_rigorous_backendomnibias.core.verified.transcend.require_rigorous_backend
sech_iv
omnibias.core.verified.sech_ivSource ↗sech_iv(x: Interval) -> IntervalGuaranteed enclosure of sech(x) = 1 / cosh(x) over x (clamped to (0, 1]).
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
IntervalExecuted regression · g2 jacobian containment
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g2_jacobian_containment() -> None:
report = jacobian_containment_report(n_boxes=1000, seed=3)
assert report["fields"] == 10
assert report["checked"] == 10000
assert report["misses"] == 0
assert report["containment"] is Truepython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g2_jacobian_containment" -qRead the implementation
def sech_iv(x: Interval) -> Interval:
r"""Guaranteed enclosure of ``sech(x) = 1 / cosh(x)`` over ``x`` (clamped to ``(0, 1]``)."""
out = cosh_iv(x).reciprocal()
return Interval(max(out.lo, 0.0), min(out.hi, 1.0))Other public import paths
omnibias.core.verified.sech_ivomnibias.core.verified.transcend.sech_iv
set_strict_backend
omnibias.core.verified.set_strict_backendSource ↗set_strict_backend(enabled: bool) -> boolEnable/disable strict (mpmath-only) mode; returns the previous setting.
In strict mode any transcendental evaluation that would fall back to the
platform libm raises RuntimeError instead of returning a
*conditionally*-rigorous bracket. Use it to guarantee a produced enclosure is
unconditionally sound (e.g. before sealing a spectral-gap certificate).
Parameters
| Name | Type & default | Contract |
|---|---|---|
enabledpositional-or-keyword | boolRequired | See the operation contract and implementation below. |
boolRegression example · strict backend toggle roundtrips
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_strict_backend_toggle_roundtrips() -> None:
prev = transcend.set_strict_backend(True)
try:
assert transcend.strict_backend() is True
finally:
restored = transcend.set_strict_backend(prev)
assert restored is True
assert transcend.strict_backend() is prevpython -m pytest packages/omnibias-core/tests/test_certificate_audit_regressions.py -k test_strict_backend_toggle_roundtrips -qRegression example · it increases with the argument on the positive axis
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_it_increases_with_the_argument_on_the_positive_axis(order: int) -> None:
"""Strict separation, so a merely-wide enclosure cannot pass by overlapping."""
previous = besseli_point(order, 0.0)
for z in (0.25, 0.5, 1.0, 2.0, 4.0, 7.0):
current = besseli_point(order, z)
assert current.lo > previous.hi, f"I_{order} did not increase at z={z}"
previous = currentpython -m pytest packages/omnibias-core/tests/verified/test_besseli.py -k test_it_increases_with_the_argument_on_the_positive_axis -qRead the implementation
def set_strict_backend(enabled: bool) -> bool:
"""Enable/disable strict (mpmath-only) mode; returns the previous setting.
In strict mode any transcendental evaluation that would fall back to the
platform ``libm`` raises :class:`RuntimeError` instead of returning a
*conditionally*-rigorous bracket. Use it to guarantee a produced enclosure is
unconditionally sound (e.g. before sealing a spectral-gap certificate).
"""
global _STRICT_BACKEND
previous = _STRICT_BACKEND
_STRICT_BACKEND = bool(enabled)
return previousOther public import paths
omnibias.core.verified.set_strict_backendomnibias.core.verified.transcend.set_strict_backend
sigmoid_iv
omnibias.core.verified.sigmoid_ivSource ↗sigmoid_iv(x: Interval) -> IntervalGuaranteed enclosure of sigmoid(x) (clamped to the true range [0, 1]).
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
IntervalExecuted regression · g2 non vacuous
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g2_non_vacuous() -> None:
ex = worked_example()
assert float(ex["remainder_width"]) < 0.1
assert ex["vacuous"] is False
assert float(ex["width"]) < 0.1python -m pytest "packages/omnibias-core/tests/verified/test_tm_neuron.py::test_g2_non_vacuous" -qRegression example · tanh sigmoid iv superset oracle random
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_tanh_sigmoid_iv_superset_oracle_random() -> None:
rng = random.Random(0)
for _ in range(500):
x = rng.uniform(-12.0, 12.0)
assert_superset(tanh_iv(Interval.point(x)), oracle_tanh(x), name=f"tanh@{x}")
assert_superset(sigmoid_iv(Interval.point(x)), oracle_sigmoid(x), name=f"sigmoid@{x}")python -m pytest tests/test_oracles.py -k test_tanh_sigmoid_iv_superset_oracle_random -qRead the implementation
def sigmoid_iv(x: Interval) -> Interval:
"""Guaranteed enclosure of ``sigmoid(x)`` (clamped to the true range ``[0, 1]``)."""
lo, hi = _monotone_increasing("sigmoid", x)
return Interval(max(lo, 0.0), min(hi, 1.0))Other public import paths
omnibias.core.verified.sigmoid_ivomnibias.core.verified.transcend.sigmoid_iv
sin_iv
omnibias.core.verified.sin_ivSource ↗sin_iv(x: Interval) -> IntervalGuaranteed enclosure of sin over the (possibly wide) interval x.
The twin of cos_iv: sin extrema sit at *odd* multiples of
pi/2 -- writing such a point as m * pi/2 the maxima (sin = +1) are
the m == 1 (mod 4) cases and the minima (sin = -1) the
m == 3 (mod 4) cases. Membership is tested on an outward enclosure of
2 x / pi.
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
IntervalExecuted regression · clenshaw curtis encloses sin
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_clenshaw_curtis_encloses_sin(self) -> None:
enc = clenshaw_curtis_integral(_sin_iv, 0.0, math.pi, n=8, deriv_np1_bound=Interval(-1.0, 1.0))
assert enc.contains(2.0)python -m pytest "packages/omnibias-core/tests/verified/test_quadrature_rules.py::TestCertifiedRulesEncloseExact::test_clenshaw_curtis_encloses_sin" -qRegression example · sin iv contains all samples
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_sin_iv_contains_all_samples(lo: float, hi: float) -> None:
enc = sin_iv(Interval(lo, hi))
assert -1.0 <= enc.lo <= enc.hi <= 1.0
for x in _samples(lo, hi):
assert enc.lo <= math.sin(x) <= enc.hipython -m pytest packages/omnibias-core/tests/verified/test_verified_trig.py -k test_sin_iv_contains_all_samples -qRead the implementation
def sin_iv(x: Interval) -> Interval:
r"""Guaranteed enclosure of ``sin`` over the (possibly wide) interval ``x``.
The twin of :func:`cos_iv`: ``sin`` extrema sit at *odd* multiples of
``pi/2`` -- writing such a point as ``m * pi/2`` the maxima (``sin = +1``) are
the ``m == 1 (mod 4)`` cases and the minima (``sin = -1``) the
``m == 3 (mod 4)`` cases. Membership is tested on an outward enclosure of
``2 x / pi``.
"""
sa = sin_point(x.lo)
sb = sin_point(x.hi)
lo = min(sa.lo, sb.lo)
hi = max(sa.hi, sb.hi)
lo_over = (Interval.point(x.lo) * 2 / _PI_IV).lo # lower bound on 2 x.lo / pi
hi_over = (Interval.point(x.hi) * 2 / _PI_IV).hi # upper bound on 2 x.hi / pi
if _has_integer_with_residue(lo_over, hi_over, 1, 4): # -> max +1
hi = 1.0
if _has_integer_with_residue(lo_over, hi_over, 3, 4): # -> min -1
lo = -1.0
return Interval(max(lo, -1.0), min(hi, 1.0))Other public import paths
omnibias.core.verified.sin_ivomnibias.core.verified.transcend.sin_iv
sin_point
omnibias.core.verified.sin_pointSource ↗sin_point(x: float) -> IntervalGuaranteed enclosure of sin(x) at a scalar point x.
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
IntervalExecuted regression · clenshaw curtis encloses sin
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_clenshaw_curtis_encloses_sin(self) -> None:
enc = clenshaw_curtis_integral(_sin_iv, 0.0, math.pi, n=8, deriv_np1_bound=Interval(-1.0, 1.0))
assert enc.contains(2.0)python -m pytest "packages/omnibias-core/tests/verified/test_quadrature_rules.py::TestCertifiedRulesEncloseExact::test_clenshaw_curtis_encloses_sin" -qRegression example · hilbert mode action approx
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_hilbert_mode_action_approx(n: int) -> None:
"""Sanity: H cos(kx)~sin(kx), H sin(kx)~-cos(kx) to O(n*ulp)."""
nodes = uniform_nodes(n)
hmat = hilbert_circulant(n)
tol = 50 * n * 2.3e-16
for k in range(1, n // 2):
hc = matvec(hmat, [cos_point(k * x) for x in nodes])
hs = matvec(hmat, [sin_point(k * x) for x in nodes])
for j, x in enumerate(nodes):
assert abs(hc[j].mid - math.sin(k * x)) < tol
assert abs(hs[j].mid + math.cos(k * x)) < tolpython -m pytest packages/omnibias-core/tests/verified/test_spectral.py -k test_hilbert_mode_action_approx -qRead the implementation
def sin_point(x: float) -> Interval:
"""Guaranteed enclosure of ``sin(x)`` at a scalar point ``x``."""
lo, hi = _enclose_point("sin", x)
return Interval(max(lo, -1.0), min(hi, 1.0))Other public import paths
omnibias.core.verified.sin_pointomnibias.core.verified.transcend.sin_point
sinh_iv
omnibias.core.verified.sinh_ivSource ↗sinh_iv(x: Interval) -> IntervalGuaranteed enclosure of sinh(x) = (e^x - e^{-x}) / 2 over x.
sinh is odd and strictly increasing, so composing the two monotone
exp_iv enclosures is rigorous on any interval, including one that
straddles zero.
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
IntervalRead the implementation
def sinh_iv(x: Interval) -> Interval:
r"""Guaranteed enclosure of ``sinh(x) = (e^x - e^{-x}) / 2`` over ``x``.
``sinh`` is odd and strictly increasing, so composing the two monotone
:func:`exp_iv` enclosures is rigorous on any interval, including one that
straddles zero.
"""
return (exp_iv(x) - exp_iv(-x)) * Interval.point(0.5)Other public import paths
omnibias.core.verified.sinh_ivomnibias.core.verified.transcend.sinh_iv
softplus_iv
omnibias.core.verified.softplus_ivSource ↗softplus_iv(x: Interval) -> IntervalGuaranteed enclosure of softplus(x) = ln(1 + exp(x)) over x.
softplus is strictly increasing and positive, so the enclosure is built
from the lower endpoint at x.lo and the upper endpoint at x.hi and
clamped to the true range (0, inf).
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
IntervalExecuted regression · g2 jacobian containment
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g2_jacobian_containment() -> None:
report = jacobian_containment_report(n_boxes=1000, seed=3)
assert report["fields"] == 10
assert report["checked"] == 10000
assert report["misses"] == 0
assert report["containment"] is Truepython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g2_jacobian_containment" -qRead the implementation
def softplus_iv(x: Interval) -> Interval:
"""Guaranteed enclosure of ``softplus(x) = ln(1 + exp(x))`` over ``x``.
``softplus`` is strictly increasing and positive, so the enclosure is built
from the lower endpoint at ``x.lo`` and the upper endpoint at ``x.hi`` and
clamped to the true range ``(0, inf)``.
"""
lo = _softplus_point(x.lo).lo
hi = _softplus_point(x.hi).hi
return Interval(max(lo, 0.0), hi)Other public import paths
omnibias.core.verified.softplus_ivomnibias.core.verified.transcend.softplus_iv
strict_backend
omnibias.core.verified.strict_backendSource ↗strict_backend() -> boolTrue when strict (mpmath-only) transcendental mode is active.
boolExecuted regression · honesty defaults to no unproven claim
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_honesty_defaults_to_no_unproven_claim() -> None:
cert = make_certificate(claim="benign", payload={"type": "interval"})
assert cert["honesty"] == {"unproven_claim": False}python -m pytest "packages/omnibias-core/tests/test_certificate.py::test_honesty_defaults_to_no_unproven_claim" -qRegression example · strict backend toggle roundtrips
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_strict_backend_toggle_roundtrips() -> None:
prev = transcend.set_strict_backend(True)
try:
assert transcend.strict_backend() is True
finally:
restored = transcend.set_strict_backend(prev)
assert restored is True
assert transcend.strict_backend() is prevpython -m pytest packages/omnibias-core/tests/test_certificate_audit_regressions.py -k test_strict_backend_toggle_roundtrips -qRead the implementation
def strict_backend() -> bool:
"""``True`` when strict (mpmath-only) transcendental mode is active."""
return _STRICT_BACKENDOther public import paths
omnibias.core.verified.strict_backendomnibias.core.verified.transcend.strict_backend
tanh_iv
omnibias.core.verified.tanh_ivSource ↗tanh_iv(x: Interval) -> IntervalGuaranteed enclosure of tanh(x) (clamped to the true range [-1, 1]).
Parameters
| Name | Type & default | Contract |
|---|---|---|
xpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
IntervalExecuted regression · coefficient arithmetic chooses interval
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_coefficient_arithmetic_chooses_interval() -> None:
report = coefficient_arithmetic_report()
assert report["choice"] == "interval"
assert report["tm_required"] is Falsepython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_coefficient_arithmetic_chooses_interval" -qRegression example · tanh sigmoid iv superset oracle random
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_tanh_sigmoid_iv_superset_oracle_random() -> None:
rng = random.Random(0)
for _ in range(500):
x = rng.uniform(-12.0, 12.0)
assert_superset(tanh_iv(Interval.point(x)), oracle_tanh(x), name=f"tanh@{x}")
assert_superset(sigmoid_iv(Interval.point(x)), oracle_sigmoid(x), name=f"sigmoid@{x}")python -m pytest tests/test_oracles.py -k test_tanh_sigmoid_iv_superset_oracle_random -qRead the implementation
def tanh_iv(x: Interval) -> Interval:
"""Guaranteed enclosure of ``tanh(x)`` (clamped to the true range ``[-1, 1]``)."""
lo, hi = _monotone_increasing("tanh", x)
return Interval(max(lo, -1.0), min(hi, 1.0))Other public import paths
omnibias.core.verified.tanh_ivomnibias.core.verified.transcend.tanh_iv