Skip to main content

omnibias.core.verified.transcend

0.5.0rc1Release candidatePython >=3.10Apache-2.0

Coefficient recurrences, activation contracts, jet algebra, and verified arithmetic shared by the numerical backends.

import omnibias.core.verified.transcend
Module 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 math libm and inflated by FALLBACK_ULPS representable steps in each direction. This is rigorous *provided* the libm error is below FALLBACK_ULPS ulp -- true for every mainstream correctly-rounded-ish libm (glibc bounds tanh/exp well under 2 ulp). backend_name reports "libm_fallback" on this path so a certificate can record it honestly. Certificate sealing that asserts unconditional soundness (or runs under certificate_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.

CONSTANT

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"
CONSTANT

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"
CONSTANT

BESSELI_SERIES_MAX_ARG​

omnibias.core.verified.transcend.BESSELI_SERIES_MAX_ARGSource ↗
BESSELI_SERIES_MAX_ARG: float = 600.0

Largest 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 -q
Regression 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 -q
Read the implementation
BESSELI_SERIES_MAX_ARG: float = 600.0
CONSTANT

BESSELI_SERIES_MAX_TERMS​

omnibias.core.verified.transcend.BESSELI_SERIES_MAX_TERMSSource ↗
BESSELI_SERIES_MAX_TERMS: int = 4096

Term 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 = 4096
CONSTANT

E_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-14
python -m pytest packages/omnibias-core/tests/verified/test_constants.py -k test_e_iv_encloses_math_e_tightly -q
Regression 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.hi
python -m pytest packages/omnibias-core/tests/verified/test_constants.py -k test_constants_are_nondegenerate_intervals -q
Read the implementation
E_IV = exp_iv(Interval.point(1.0))
Other public import paths
  • omnibias.core.verified.E_IV
  • omnibias.core.verified.transcend.E_IV
CONSTANT

FALLBACK_ULPS​

omnibias.core.verified.transcend.FALLBACK_ULPSSource ↗
FALLBACK_ULPS: int = 4

ulp inflation applied to each endpoint in the stdlib fallback.

Read the implementation
FALLBACK_ULPS: int = 4
CONSTANT

MPMATH_DPS​

omnibias.core.verified.transcend.MPMATH_DPSSource ↗
MPMATH_DPS: int = 60

high-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 -q
Read the implementation
MPMATH_DPS: int = 60
CONSTANT

PI_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-14
python -m pytest packages/omnibias-core/tests/verified/test_constants.py -k test_pi_iv_encloses_math_pi_tightly -q
Regression 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_IV
python -m pytest packages/omnibias-core/tests/verified/test_constants.py -k test_private_alias_is_public_constant -q
Read the implementation
PI_IV = Interval(_pred(math.pi), _succ(math.pi))
Other public import paths
  • omnibias.core.verified.PI_IV
  • omnibias.core.verified.transcend.PI_IV
FUNCTION

atan_iv​

omnibias.core.verified.atan_ivSource ↗
atan_iv(x: Interval) -> Interval

Guaranteed enclosure of atan(x) (monotone; clamped to (-pi/2, pi/2)).

Parameters

NameType & defaultContract
xpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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" -q
Read 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_iv
  • omnibias.core.verified.transcend.atan_iv
FUNCTION

atan_point​

omnibias.core.verified.atan_pointSource ↗
atan_point(x: float) -> Interval

Guaranteed enclosure of atan(x) at a scalar point x.

Parameters

NameType & defaultContract
xpositional-or-keywordfloatRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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/2
python -m pytest "packages/omnibias-core/tests/test_transcend_directed_soundness.py::test_atan_cap_does_not_cut_off_pi_over_two" -q
Read 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_point
  • omnibias.core.verified.transcend.atan_point
FUNCTION

backend_name​

omnibias.core.verified.backend_nameSource ↗
backend_name() -> str

"mpmath" when the high-precision backend is active, else "libm_fallback".

Returnsstr
Executed 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" -q
Regression 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 raise
python -m pytest packages/omnibias-core/tests/test_certificate_audit_regressions.py -k test_require_rigorous_backend_accepts_mpmath -q
Read 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_FALLBACK
Other public import paths
  • omnibias.core.verified.backend_name
  • omnibias.core.verified.transcend.backend_name
FUNCTION

besseli_iv​

omnibias.core.verified.besseli_ivSource ↗
besseli_iv(n: int, x: Interval) -> Interval

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 _besseli_series.

Parameters

NameType & defaultContract
npositional-or-keywordintRequiredSee the operation contract and implementation below.
xpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
ReturnsInterval
Explicit validation & failure cases
  • When type(n) is not int, raises ValueError('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]" -q
Regression 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 -q
Read 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_iv
  • omnibias.core.verified.transcend.besseli_iv
FUNCTION

besseli_point​

omnibias.core.verified.besseli_pointSource ↗
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.

Parameters

NameType & defaultContract
npositional-or-keywordintRequiredSee the operation contract and implementation below.
zpositional-or-keywordfloatRequiredSee the operation contract and implementation below.
ReturnsInterval
Explicit validation & failure cases
  • When type(n) is not int, raises ValueError('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" -q
Regression 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 -q
Read 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_point
  • omnibias.core.verified.transcend.besseli_point
FUNCTION

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.

ReturnsIterator[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" -q
Regression 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 -q
Read 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_mode
  • omnibias.core.verified.transcend.certificate_mode
FUNCTION

clear_libm_fallback_used​

omnibias.core.verified.clear_libm_fallback_usedSource ↗
clear_libm_fallback_used() -> None

Reset the libm_fallback_used sticky flag (tests / fresh certificate scopes).

ReturnsNone
Regression 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 -q
Regression 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 False
python -m pytest packages/omnibias-core/tests/verified/test_besseli.py -k test_the_series_fallback_is_unconditionally_rigorous -q
Read 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 = False
Other public import paths
  • omnibias.core.verified.clear_libm_fallback_used
  • omnibias.core.verified.transcend.clear_libm_fallback_used
FUNCTION

cos_iv​

omnibias.core.verified.cos_ivSource ↗
cos_iv(x: Interval) -> Interval

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 _PI_IV), so an interior extremum is never missed and the enclosure stays rigorous.

Parameters

NameType & defaultContract
xpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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" -q
Regression 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.hi
python -m pytest packages/omnibias-core/tests/verified/test_verified_trig.py -k test_cos_iv_contains_all_samples -q
Read 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_iv
  • omnibias.core.verified.transcend.cos_iv
FUNCTION

cos_point​

omnibias.core.verified.cos_pointSource ↗
cos_point(x: float) -> Interval

Guaranteed enclosure of cos(x) at a scalar point x.

Parameters

NameType & defaultContract
xpositional-or-keywordfloatRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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" -q
Regression 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)) < tol
python -m pytest packages/omnibias-core/tests/verified/test_spectral.py -k test_hilbert_mode_action_approx -q
Read 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_point
  • omnibias.core.verified.transcend.cos_point
FUNCTION

cosh_iv​

omnibias.core.verified.cosh_ivSource ↗
cosh_iv(x: Interval) -> Interval

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 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

NameType & defaultContract
xpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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 True
python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g2_jacobian_containment" -q
Read 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_iv
  • omnibias.core.verified.transcend.cosh_iv
FUNCTION

erf_iv​

omnibias.core.verified.erf_ivSource ↗
erf_iv(x: Interval) -> Interval

Guaranteed enclosure of erf(x) over x (monotone; clamped to [-1, 1]).

Parameters

NameType & defaultContract
xpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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" -q
Read 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_iv
  • omnibias.core.verified.transcend.erf_iv
FUNCTION

erf_point​

omnibias.core.verified.erf_pointSource ↗
erf_point(x: float) -> Interval

Guaranteed enclosure of erf(x) at a scalar point x.

Parameters

NameType & defaultContract
xpositional-or-keywordfloatRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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]" -q
Read 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_point
  • omnibias.core.verified.transcend.erf_point
FUNCTION

exp_iv​

omnibias.core.verified.exp_ivSource ↗
exp_iv(x: Interval) -> Interval

Guaranteed enclosure of exp(x) over the interval x.

Parameters

NameType & defaultContract
xpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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.hi
python -m pytest "packages/omnibias-core/tests/verified/test_hermite_basis.py::test_gaussian_weight_matches_exp" -q
Regression 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 -q
Read 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_iv
  • omnibias.core.verified.transcend.exp_iv
FUNCTION

gauss_cdf_iv​

omnibias.core.verified.gauss_cdf_ivSource ↗
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.

Parameters

NameType & defaultContract
xpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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 True
python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g2_jacobian_containment" -q
Regression 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 -q
Read 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_iv
  • omnibias.core.verified.transcend.gauss_cdf_iv
FUNCTION

gauss_cdf_point​

omnibias.core.verified.gauss_cdf_pointSource ↗
gauss_cdf_point(x: float) -> Interval

Guaranteed enclosure of the standard-normal CDF Phi(x) at a scalar point x.

Parameters

NameType & defaultContract
xpositional-or-keywordfloatRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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]" -q
Regression 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 -q
Read 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_point
  • omnibias.core.verified.transcend.gauss_cdf_point
FUNCTION

libm_fallback_used​

omnibias.core.verified.libm_fallback_usedSource ↗
libm_fallback_used() -> bool

True if the libm fallback has produced at least one enclosure this process.

Returnsbool
Executed 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" -q
Regression 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 False
python -m pytest packages/omnibias-core/tests/verified/test_besseli.py -k test_the_series_fallback_is_unconditionally_rigorous -q
Read the implementation
def libm_fallback_used() -> bool:
    """``True`` if the libm fallback has produced at least one enclosure this process."""
    return _LIBM_FALLBACK_USED
Other public import paths
  • omnibias.core.verified.libm_fallback_used
  • omnibias.core.verified.transcend.libm_fallback_used
FUNCTION

ln_iv​

omnibias.core.verified.ln_ivSource ↗
ln_iv(x: Interval) -> Interval

Guaranteed enclosure of ln(x) over x (monotone; requires x.lo > 0).

Parameters

NameType & defaultContract
xpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
ReturnsInterval
Explicit validation & failure cases
  • When x.lo <= 0.0, raises ValueError('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.hi
python -m pytest "packages/omnibias-core/tests/verified/test_riesz.py::test_potential_matches_mpmath" -q
Regression 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 -q
Read 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_iv
  • omnibias.core.verified.transcend.ln_iv
FUNCTION

ln_point​

omnibias.core.verified.ln_pointSource ↗
ln_point(x: float) -> Interval

Guaranteed enclosure of ln(x) at a scalar point x > 0.

Parameters

NameType & defaultContract
xpositional-or-keywordfloatRequiredSee the operation contract and implementation below.
ReturnsInterval
Explicit validation & failure cases
  • When x <= 0.0, raises ValueError('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_point
  • omnibias.core.verified.transcend.ln_point
FUNCTION

require_rigorous_backend​

omnibias.core.verified.require_rigorous_backendSource ↗
require_rigorous_backend() -> None

Raise 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.

ReturnsNone
Explicit validation & failure cases
  • When backend_name() != BACKEND_MPMATH, raises RuntimeError(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" -q
Regression 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 raise
python -m pytest packages/omnibias-core/tests/test_certificate_audit_regressions.py -k test_require_rigorous_backend_accepts_mpmath -q
Read 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_backend
  • omnibias.core.verified.transcend.require_rigorous_backend
FUNCTION

sech_iv​

omnibias.core.verified.sech_ivSource ↗
sech_iv(x: Interval) -> Interval

Guaranteed enclosure of sech(x) = 1 / cosh(x) over x (clamped to (0, 1]).

Parameters

NameType & defaultContract
xpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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 True
python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g2_jacobian_containment" -q
Read 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_iv
  • omnibias.core.verified.transcend.sech_iv
FUNCTION

set_strict_backend​

omnibias.core.verified.set_strict_backendSource ↗
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 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

NameType & defaultContract
enabledpositional-or-keywordboolRequiredSee the operation contract and implementation below.
Returnsbool
Regression 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 prev
python -m pytest packages/omnibias-core/tests/test_certificate_audit_regressions.py -k test_strict_backend_toggle_roundtrips -q
Regression 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 = current
python -m pytest packages/omnibias-core/tests/verified/test_besseli.py -k test_it_increases_with_the_argument_on_the_positive_axis -q
Read 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 previous
Other public import paths
  • omnibias.core.verified.set_strict_backend
  • omnibias.core.verified.transcend.set_strict_backend
FUNCTION

sigmoid_iv​

omnibias.core.verified.sigmoid_ivSource ↗
sigmoid_iv(x: Interval) -> Interval

Guaranteed enclosure of sigmoid(x) (clamped to the true range [0, 1]).

Parameters

NameType & defaultContract
xpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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.1
python -m pytest "packages/omnibias-core/tests/verified/test_tm_neuron.py::test_g2_non_vacuous" -q
Regression 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 -q
Read 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_iv
  • omnibias.core.verified.transcend.sigmoid_iv
FUNCTION

sin_iv​

omnibias.core.verified.sin_ivSource ↗
sin_iv(x: Interval) -> Interval

Guaranteed 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

NameType & defaultContract
xpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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" -q
Regression 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.hi
python -m pytest packages/omnibias-core/tests/verified/test_verified_trig.py -k test_sin_iv_contains_all_samples -q
Read 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_iv
  • omnibias.core.verified.transcend.sin_iv
FUNCTION

sin_point​

omnibias.core.verified.sin_pointSource ↗
sin_point(x: float) -> Interval

Guaranteed enclosure of sin(x) at a scalar point x.

Parameters

NameType & defaultContract
xpositional-or-keywordfloatRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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" -q
Regression 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)) < tol
python -m pytest packages/omnibias-core/tests/verified/test_spectral.py -k test_hilbert_mode_action_approx -q
Read 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_point
  • omnibias.core.verified.transcend.sin_point
FUNCTION

sinh_iv​

omnibias.core.verified.sinh_ivSource ↗
sinh_iv(x: Interval) -> Interval

Guaranteed 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

NameType & defaultContract
xpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
ReturnsInterval
Read 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_iv
  • omnibias.core.verified.transcend.sinh_iv
FUNCTION

softplus_iv​

omnibias.core.verified.softplus_ivSource ↗
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).

Parameters

NameType & defaultContract
xpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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 True
python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g2_jacobian_containment" -q
Read 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_iv
  • omnibias.core.verified.transcend.softplus_iv
FUNCTION

strict_backend​

omnibias.core.verified.strict_backendSource ↗
strict_backend() -> bool

True when strict (mpmath-only) transcendental mode is active.

Returnsbool
Executed 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" -q
Regression 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 prev
python -m pytest packages/omnibias-core/tests/test_certificate_audit_regressions.py -k test_strict_backend_toggle_roundtrips -q
Read the implementation
def strict_backend() -> bool:
    """``True`` when strict (mpmath-only) transcendental mode is active."""
    return _STRICT_BACKEND
Other public import paths
  • omnibias.core.verified.strict_backend
  • omnibias.core.verified.transcend.strict_backend
FUNCTION

tanh_iv​

omnibias.core.verified.tanh_ivSource ↗
tanh_iv(x: Interval) -> Interval

Guaranteed enclosure of tanh(x) (clamped to the true range [-1, 1]).

Parameters

NameType & defaultContract
xpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
ReturnsInterval
Executed 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 False
python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_coefficient_arithmetic_chooses_interval" -q
Regression 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 -q
Read 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_iv
  • omnibias.core.verified.transcend.tanh_iv