API REFERENCE/omnibias-core

omnibias.core.verified.jet

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

Module contract & mathematical conventions

Verified (interval) directional jets -- the rigorous twin of the float jets.

This mirrors the exact-derivative jet kernels of omnibias.jax.jet / omnibias.torch.jet (truncated-convolution Faà di Bruno composition) but propagates ~omnibias.core.verified.interval.Interval Taylor coefficients instead of floats. Because the structure is identical, a float jet and the midpoints of a verified jet agree to rounding; the verified version additionally certifies an enclosure of every directional derivative.

Conventions (identical to the float kernels)

• A *scalar jet* is list[Interval] of length N+1 holding Taylor coefficients a_k = f^(k)(0)/k! of a path parameter t.
• A *vector jet* is list[list[Interval]] of shape (N+1, D) (order-major), one inner list of components per Taylor order.
• jet_to_tower rescales coefficient a_k by k! to recover the directional derivative d^k/dt^k f.

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.

Module source ↗Source revision 9a2d73df0573Running reference examples →

CONSTANT

Jet

omnibias.core.verified.jet.JetSource ↗

Jet = list[Interval]

This exported constant is defined by the expression above. Its exact value and annotation come from the pinned source; use it with the module contract.

Read the implementation

Jet = list[Interval]

CONSTANT

VecJet

omnibias.core.verified.jet.VecJetSource ↗

VecJet = list[list[Interval]]

This exported constant is defined by the expression above. Its exact value and annotation come from the pinned source; use it with the module contract.

Read the implementation

VecJet = list[list[Interval]]

FUNCTION

affine_jet

omnibias.core.verified.affine_jetSource ↗

affine_jet(z_jet: Sequence[Sequence[Interval]], weight: Sequence[Sequence[IntervalLike]], bias: Sequence[IntervalLike] | None=None) -> VecJet

Push a vector jet through u = W z + b (acts per Taylor order).

Parameters

Name	Type & default	Contract
z_jetpositional-or-keyword	Sequence[Sequence[Interval]]Required	See the operation contract and implementation below.
weightpositional-or-keyword	Sequence[Sequence[IntervalLike]]Required	See the operation contract and implementation below.
biaspositional-or-keyword	Sequence[IntervalLike] | NoneDefault: None	See the operation contract and implementation below.

ReturnsVecJet

Explicit validation & failure cases

• When len(w_o) != d_in, raises ValueError('weight row width must match input dimension').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · screened poisson sign

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.

Full file, imports & fixtures ↗

def test_screened_poisson_sign() -> None:
    pde = screened_poisson(2, 2.0, 0.0)  # lap u - 4 u = -4 u  for affine
    x, y = 0.5, 0.5
    r = certified_interior_residual(_AFFINE, [(x, x), (y, y)], pde)
    assert r.lo <= -4.0 * _u_affine(x, y) <= r.hi

python -m pytest "packages/omnibias-core/tests/test_verified_pde_certificate.py::test_screened_poisson_sign" -q

Regression example · compose jet mv matches layer path

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.

Full file, imports & fixtures ↗

def test_compose_jet_mv_matches_layer_path() -> None:
    from omnibias.core.verified.jet import affine_jet
    from omnibias.core.verified.sigma import sigma_tower_interval

    w, b, name = [0.7, -0.3], 0.2, "sigmoid"
    order = 3
    box = [(0.0, 0.4), (-0.5, 0.1)]
    jet0 = identity_jet(box, order)
    u_jet = affine_jet(jet0, [list(w)], [b])
    tower = [
        [sigma_tower_interval(name, u_jet[0][0], order)[k]] for k in range(order + 1)
    ]
    composed = compose_jet_mv(u_jet, tower, 2, order)
    layer = layer_jet_mv(jet0, [list(w)], [b], name, 2, order)
    for g in range(len(composed)):
        assert composed[g][0].lo == layer[g][0].lo
        assert composed[g][0].hi == layer[g][0].hi

python -m pytest packages/omnibias-core/tests/test_verified_jet_mv.py -k test_compose_jet_mv_matches_layer_path -q

Read the implementation

def affine_jet(
    z_jet: Sequence[Sequence[Interval]],
    weight: Sequence[Sequence[IntervalLike]],
    bias: Sequence[IntervalLike] | None = None,
) -> VecJet:
    """Push a vector jet through ``u = W z + b`` (acts per Taylor order)."""
    np1 = len(z_jet)
    d_out = len(weight)
    d_in = len(z_jet[0]) if np1 else 0
    out: VecJet = []
    for k in range(np1):
        row: list[Interval] = []
        for o in range(d_out):
            w_o = weight[o]
            if len(w_o) != d_in:
                raise ValueError("weight row width must match input dimension")
            acc = _zero()
            for i in range(d_in):
                acc = acc + Interval.from_value(w_o[i]) * z_jet[k][i]
            if k == 0 and bias is not None:
                acc = acc + Interval.from_value(bias[o])
            row.append(acc)
        out.append(row)
    return out

Other public import paths

• omnibias.core.verified.affine_jet
• omnibias.core.verified.jet.affine_jet

FUNCTION

antiderivative_jet

omnibias.core.verified.antiderivative_jetSource ↗

antiderivative_jet(jet: Sequence[Interval], constant: IntervalLike=0.0) -> Jet

Taylor jet of the antiderivative F(t) = constant + \int_0^t f (term-by-term FTC).

With a_k = f^(k)(0)/k! the antiderivative's Taylor coefficients are A_0 = constant and A_m = a_{m-1}/m for m >= 1, so the jet lengthens by one order. This is the exact closed-form *integral tower* -- the two-sided partner of the derivative tower jet_to_tower -- valid to every order for any activation; the constant of integration is a free parameter (default 0).

Parameters

Name	Type & default	Contract
jetpositional-or-keyword	Sequence[Interval]Required	See the operation contract and implementation below.
constantpositional-or-keyword	IntervalLikeDefault: 0.0	See the operation contract and implementation below.

ReturnsJet

Executed regression · antiderivative jet constant and empty edges

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.

Full file, imports & fixtures ↗

def test_antiderivative_jet_constant_and_empty_edges() -> None:
    jet = [Interval.point(2.0), Interval.point(6.0), Interval.point(9.0)]
    anti = antiderivative_jet(jet, constant=Interval.point(-4.0))
    assert anti[0].lo == anti[0].hi == -4.0  # integration constant
    assert anti[1].lo <= 2.0 <= anti[1].hi  # A_1 = a_0 / 1
    assert anti[2].lo <= 3.0 <= anti[2].hi  # A_2 = a_1 / 2
    # a constant jet has no derivative information: derivative_jet yields length 0.
    assert derivative_jet([Interval.point(5.0)]) == []

python -m pytest "packages/omnibias-core/tests/verified/test_sigma_and_jet.py::test_antiderivative_jet_constant_and_empty_edges" -q

Regression example · antiderivative jet encloses mpmath and inverts

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.

Full file, imports & fixtures ↗

def test_antiderivative_jet_encloses_mpmath_and_inverts() -> None:
    """The verified integral tower of ``net(t) = tanh(a t + c)`` encloses the mpmath
    Taylor jet of its antiderivative, and ``derivative_jet`` inverts it (FTC part 1)."""
    a, c = 1.37, -0.42
    order = 6
    net = mlp_jet([0.0], [1.0], [([[a]], [c], "tanh")], order)
    series = [net[k][0] for k in range(len(net))]

    # Independent oracle: F(t) = (log cosh(a t + c) - log cosh c)/a, so F' = net, F(0)=0.
    def big_f(t: object) -> object:
        return (mpmath.log(mpmath.cosh(a * t + c)) - mpmath.log(mpmath.cosh(c))) / a

    with mpmath.workdps(50):
        taylor_f = mpmath.taylor(big_f, 0.0, order + 1)  # A_k, k = 0 .. order+1

    anti = antiderivative_jet(series)
    assert len(anti) == len(series) + 1
    for k in range(order + 2):
        assert anti[k].lo <= float(taylor_f[k]) <= anti[k].hi
        assert anti[k].width <= 1e-8 + 1e-8 * abs(float(taylor_f[k]))

    # FTC part 1: differentiating the antiderivative recovers the original jet.
    back = derivative_jet(anti)
    assert len(back) == len(series)
    for orig, got in zip(series, back, strict=True):
        assert got.lo <= orig.lo + 1e-12
        assert got.hi >= orig.hi - 1e-12
        assert got.width <= orig.width + 1e-12

python -m pytest packages/omnibias-core/tests/verified/test_sigma_and_jet.py -k test_antiderivative_jet_encloses_mpmath_and_inverts -q

Read the implementation

def antiderivative_jet(jet: Sequence[Interval], constant: IntervalLike = 0.0) -> Jet:
    r"""Taylor jet of the antiderivative ``F(t) = constant + \int_0^t f`` (term-by-term FTC).

    With ``a_k = f^(k)(0)/k!`` the antiderivative's Taylor coefficients are
    ``A_0 = constant`` and ``A_m = a_{m-1}/m`` for ``m >= 1``, so the jet lengthens
    by one order.  This is the exact closed-form *integral tower* -- the two-sided
    partner of the derivative tower :func:`jet_to_tower` -- valid to every order for
    any activation; the constant of integration is a free parameter (default 0).
    """
    out: Jet = [Interval.from_value(constant)]
    out.extend(
        jet[m - 1] * Interval.from_rational(Fraction(1, m)) for m in range(1, len(jet) + 1)
    )
    return out

Other public import paths

• omnibias.core.verified.antiderivative_jet
• omnibias.core.verified.jet.antiderivative_jet

FUNCTION

compose_jet

omnibias.core.verified.compose_jetSource ↗

compose_jet(u_jet: Sequence[Interval], sigma_tower: Sequence[Interval]) -> Jet

Compose an activation onto a scalar jet: b(t) = sigma(u(t)).

sigma_tower[k] must enclose sigma^(k)(u_jet[0]). Identical algorithm to omnibias.jax.jet.compose_jet, evaluated in interval arithmetic.

Parameters

Name	Type & default	Contract
u_jetpositional-or-keyword	Sequence[Interval]Required	See the operation contract and implementation below.
sigma_towerpositional-or-keyword	Sequence[Interval]Required	See the operation contract and implementation below.

ReturnsJet

Explicit validation & failure cases

• When len(sigma_tower) != np1, raises ValueError(f'sigma_tower order {len(sigma_tower) - 1} must match jet order {np1 - 1}').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

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.

Full file, imports & fixtures ↗

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

Read the implementation

def compose_jet(u_jet: Sequence[Interval], sigma_tower: Sequence[Interval]) -> Jet:
    """Compose an activation onto a scalar jet: ``b(t) = sigma(u(t))``.

    ``sigma_tower[k]`` must enclose ``sigma^(k)(u_jet[0])``.  Identical algorithm
    to :func:`omnibias.jax.jet.compose_jet`, evaluated in interval arithmetic.
    """
    np1 = len(u_jet)
    if len(sigma_tower) != np1:
        raise ValueError(
            f"sigma_tower order {len(sigma_tower) - 1} must match jet order {np1 - 1}"
        )
    zero = _zero()
    w: Jet = [zero] + [u_jet[j] for j in range(1, np1)]
    p: Jet = [Interval.point(1.0)] + [zero for _ in range(np1 - 1)]
    result: Jet = [sigma_tower[0]] + [zero for _ in range(np1 - 1)]
    fact = 1
    for k in range(1, np1):
        fact *= k
        p = series_mul(p, w)
        dk = sigma_tower[k] * Interval.from_rational(Fraction(1, fact))
        for n in range(np1):
            result[n] = result[n] + dk * p[n]
    return result

Related APIsomnibias.core.verified.series_mul↗

Other public import paths

• omnibias.core.verified.compose_jet
• omnibias.core.verified.jet.compose_jet

FUNCTION

derivative_jet

omnibias.core.verified.derivative_jetSource ↗

derivative_jet(jet: Sequence[Interval]) -> Jet

Taylor jet of f' from the jet of f (differentiation; FTC inverse).

With a_k = f^(k)(0)/k! the derivative's Taylor coefficients are (f')^(k)(0)/k! = (k+1)\,a_{k+1}, so the jet shortens by one order. This is the exact inverse of antiderivative_jet (derivative_jet(antiderivative_jet(a)) == a), the differentiation half of the Fundamental Theorem of Calculus in the jet register.

Parameters

Name	Type & default	Contract
jetpositional-or-keyword	Sequence[Interval]Required	See the operation contract and implementation below.

ReturnsJet

Executed regression · antiderivative jet constant and empty edges

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.

Full file, imports & fixtures ↗

def test_antiderivative_jet_constant_and_empty_edges() -> None:
    jet = [Interval.point(2.0), Interval.point(6.0), Interval.point(9.0)]
    anti = antiderivative_jet(jet, constant=Interval.point(-4.0))
    assert anti[0].lo == anti[0].hi == -4.0  # integration constant
    assert anti[1].lo <= 2.0 <= anti[1].hi  # A_1 = a_0 / 1
    assert anti[2].lo <= 3.0 <= anti[2].hi  # A_2 = a_1 / 2
    # a constant jet has no derivative information: derivative_jet yields length 0.
    assert derivative_jet([Interval.point(5.0)]) == []

python -m pytest "packages/omnibias-core/tests/verified/test_sigma_and_jet.py::test_antiderivative_jet_constant_and_empty_edges" -q

Regression example · antiderivative jet encloses mpmath and inverts

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.

Full file, imports & fixtures ↗

def test_antiderivative_jet_encloses_mpmath_and_inverts() -> None:
    """The verified integral tower of ``net(t) = tanh(a t + c)`` encloses the mpmath
    Taylor jet of its antiderivative, and ``derivative_jet`` inverts it (FTC part 1)."""
    a, c = 1.37, -0.42
    order = 6
    net = mlp_jet([0.0], [1.0], [([[a]], [c], "tanh")], order)
    series = [net[k][0] for k in range(len(net))]

    # Independent oracle: F(t) = (log cosh(a t + c) - log cosh c)/a, so F' = net, F(0)=0.
    def big_f(t: object) -> object:
        return (mpmath.log(mpmath.cosh(a * t + c)) - mpmath.log(mpmath.cosh(c))) / a

    with mpmath.workdps(50):
        taylor_f = mpmath.taylor(big_f, 0.0, order + 1)  # A_k, k = 0 .. order+1

    anti = antiderivative_jet(series)
    assert len(anti) == len(series) + 1
    for k in range(order + 2):
        assert anti[k].lo <= float(taylor_f[k]) <= anti[k].hi
        assert anti[k].width <= 1e-8 + 1e-8 * abs(float(taylor_f[k]))

    # FTC part 1: differentiating the antiderivative recovers the original jet.
    back = derivative_jet(anti)
    assert len(back) == len(series)
    for orig, got in zip(series, back, strict=True):
        assert got.lo <= orig.lo + 1e-12
        assert got.hi >= orig.hi - 1e-12
        assert got.width <= orig.width + 1e-12

python -m pytest packages/omnibias-core/tests/verified/test_sigma_and_jet.py -k test_antiderivative_jet_encloses_mpmath_and_inverts -q

Read the implementation

def derivative_jet(jet: Sequence[Interval]) -> Jet:
    r"""Taylor jet of ``f'`` from the jet of ``f`` (differentiation; FTC inverse).

    With ``a_k = f^(k)(0)/k!`` the derivative's Taylor coefficients are
    ``(f')^(k)(0)/k! = (k+1)\,a_{k+1}``, so the jet shortens by one order.  This is
    the exact inverse of :func:`antiderivative_jet`
    (``derivative_jet(antiderivative_jet(a)) == a``), the differentiation half of
    the Fundamental Theorem of Calculus in the jet register.
    """
    return [jet[k + 1] * Interval.from_rational(k + 1) for k in range(len(jet) - 1)]

Other public import paths

• omnibias.core.verified.derivative_jet
• omnibias.core.verified.jet.derivative_jet

FUNCTION

jet_to_tower

omnibias.core.verified.jet_to_towerSource ↗

jet_to_tower(jet: Sequence[Interval]) -> Jet

Rescale a scalar jet a_k by k! to the derivative tower.

Parameters

Name	Type & default	Contract
jetpositional-or-keyword	Sequence[Interval]Required	See the operation contract and implementation below.

ReturnsJet

Executed regression · jet to tower roundtrip

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.

Full file, imports & fixtures ↗

def test_jet_to_tower_roundtrip() -> None:
    jet = mlp_jet([0.2], [1.0], [([[1.0]], [0.0], "tanh")], 4)
    series = [jet[k][0] for k in range(len(jet))]
    tower = jet_to_tower(series)
    # tower[1] = tanh'(0.2) = 1 - tanh(0.2)^2
    t = math.tanh(0.2)
    assert tower[1].lo <= 1 - t * t <= tower[1].hi

python -m pytest "packages/omnibias-core/tests/verified/test_sigma_and_jet.py::test_jet_to_tower_roundtrip" -q

Regression example · sech tower encloses 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.

Full file, imports & fixtures ↗

def test_sech_tower_encloses_mpmath(z0: float) -> None:
    """The ``sech`` tower encloses the true derivatives tightly at a point."""
    order = 6
    with mpmath.workdps(50):
        taylor = mpmath.taylor(lambda z: mpmath.sech(z), z0, order)  # a_k = f^(k)/k!
        tower_true = [taylor[k] * math.factorial(k) for k in range(order + 1)]

    tower = sigma_tower_interval("sech", Interval.point(z0), order)
    for k in range(order + 1):
        assert tower[k].lo <= float(tower_true[k]) <= tower[k].hi
        assert tower[k].width <= 1e-8 + 1e-8 * abs(float(tower_true[k]))

python -m pytest packages/omnibias-core/tests/verified/test_sigma_and_jet.py -k test_sech_tower_encloses_mpmath -q

Read the implementation

def jet_to_tower(jet: Sequence[Interval]) -> Jet:
    """Rescale a scalar jet ``a_k`` by ``k!`` to the derivative tower."""
    return [jet[k] * Interval.from_rational(factorial(k)) for k in range(len(jet))]

Other public import paths

• omnibias.core.verified.jet_to_tower
• omnibias.core.verified.jet.jet_to_tower

FUNCTION

layer_jet

omnibias.core.verified.layer_jetSource ↗

layer_jet(z_jet: Sequence[Sequence[Interval]], weight: Sequence[Sequence[IntervalLike]], bias: Sequence[IntervalLike] | None, name: str) -> VecJet

Push a vector jet through one sigma(W z + b) layer (interval).

Parameters

Name	Type & default	Contract
z_jetpositional-or-keyword	Sequence[Sequence[Interval]]Required	See the operation contract and implementation below.
weightpositional-or-keyword	Sequence[Sequence[IntervalLike]]Required	See the operation contract and implementation below.
biaspositional-or-keyword	Sequence[IntervalLike] | NoneRequired	See the operation contract and implementation below.
namepositional-or-keyword	strRequired	See the operation contract and implementation below.

ReturnsVecJet

Executed regression · jet to tower roundtrip

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.

Full file, imports & fixtures ↗

def test_jet_to_tower_roundtrip() -> None:
    jet = mlp_jet([0.2], [1.0], [([[1.0]], [0.0], "tanh")], 4)
    series = [jet[k][0] for k in range(len(jet))]
    tower = jet_to_tower(series)
    # tower[1] = tanh'(0.2) = 1 - tanh(0.2)^2
    t = math.tanh(0.2)
    assert tower[1].lo <= 1 - t * t <= tower[1].hi

python -m pytest "packages/omnibias-core/tests/verified/test_sigma_and_jet.py::test_jet_to_tower_roundtrip" -q

Read the implementation

def layer_jet(
    z_jet: Sequence[Sequence[Interval]],
    weight: Sequence[Sequence[IntervalLike]],
    bias: Sequence[IntervalLike] | None,
    name: str,
) -> VecJet:
    """Push a vector jet through one ``sigma(W z + b)`` layer (interval)."""
    u_jet = affine_jet(z_jet, weight, bias)
    np1 = len(u_jet)
    order = np1 - 1
    width = len(u_jet[0]) if np1 else 0
    out: VecJet = [[_zero() for _ in range(width)] for _ in range(np1)]
    for o in range(width):
        u_series = [u_jet[k][o] for k in range(np1)]
        tower = sigma_tower_interval(name, u_series[0], order)
        composed = compose_jet(u_series, list(tower))
        for k in range(np1):
            out[k][o] = composed[k]
    return out

Related APIsomnibias.core.verified.affine_jet↗omnibias.core.verified.compose_jet↗omnibias.core.verified.sigma_tower_interval↗

Other public import paths

• omnibias.core.verified.layer_jet
• omnibias.core.verified.jet.layer_jet

FUNCTION

lhopital_ratio_iv

omnibias.core.verified.lhopital_ratio_ivSource ↗

lhopital_ratio_iv(num_jet: Sequence[Interval], den_jet: Sequence[Interval], order: int=1) -> Interval

Verified L'Hopital limit num_jet[order] / den_jet[order] (enclosure).

Interval twin of omnibias.jax.jet.lhopital_ratio: given rigorous enclosures of the Taylor coefficients of a 0/0 numerator and denominator that both vanish to order order - 1, returns an Interval enclosing the limit of the ratio. Raises ZeroDivisionError (via Interval.reciprocal) when the leading denominator enclosure straddles zero -- i.e. the limit is not certified finite at this truncation order.

Parameters

Name	Type & default	Contract
num_jetpositional-or-keyword	Sequence[Interval]Required	See the operation contract and implementation below.
den_jetpositional-or-keyword	Sequence[Interval]Required	See the operation contract and implementation below.
orderpositional-or-keyword	intDefault: 1	See the operation contract and implementation below.

ReturnsInterval

Explicit validation & failure cases

• When order < 0, raises ValueError(f'order must be >= 0, got {order}').
• When order > max_order, raises ValueError(f'order {order} exceeds available jet order {max_order}').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · order out of range raises

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.

Full file, imports & fixtures ↗

def test_order_out_of_range_raises() -> None:
    num = [Interval.point(0.0), Interval.point(1.0)]
    den = [Interval.point(0.0), Interval.point(1.0)]
    with pytest.raises(ValueError, match="exceeds available jet order"):
        lhopital_ratio_iv(num, den, order=5)

python -m pytest "packages/omnibias-core/tests/verified/test_limit_iv.py::test_order_out_of_range_raises" -q

Regression example · enclosure contains float backend result

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.

Full file, imports & fixtures ↗

def test_enclosure_contains_float_backend_result() -> None:
    # A non-trivial ratio with rounding: 2.5 / -0.5 = -5.0.
    num = _point_jet([Fraction(0), Fraction(5, 2)])
    den = _point_jet([Fraction(0), Fraction(-1, 2)])
    enclosure = lhopital_ratio_iv(num, den, order=1)
    assert enclosure.contains(-5.0)

python -m pytest packages/omnibias-core/tests/verified/test_limit_iv.py -k test_enclosure_contains_float_backend_result -q

Read the implementation

def lhopital_ratio_iv(
    num_jet: Sequence[Interval], den_jet: Sequence[Interval], order: int = 1
) -> Interval:
    r"""Verified L'Hopital limit ``num_jet[order] / den_jet[order]`` (enclosure).

    Interval twin of :func:`omnibias.jax.jet.lhopital_ratio`: given rigorous
    enclosures of the Taylor coefficients of a ``0/0`` numerator and denominator
    that both vanish to order ``order - 1``, returns an :class:`Interval`
    enclosing the limit of the ratio. Raises :class:`ZeroDivisionError` (via
    :meth:`Interval.reciprocal`) when the leading denominator enclosure straddles
    zero -- i.e. the limit is not certified finite at this truncation order.
    """
    if order < 0:
        raise ValueError(f"order must be >= 0, got {order}")
    max_order = min(len(num_jet), len(den_jet)) - 1
    if order > max_order:
        raise ValueError(f"order {order} exceeds available jet order {max_order}")
    return num_jet[order] / den_jet[order]

Other public import paths

• omnibias.core.verified.lhopital_ratio_iv
• omnibias.core.verified.jet.lhopital_ratio_iv

FUNCTION

mlp_jet

omnibias.core.verified.mlp_jetSource ↗

mlp_jet(x0: Sequence[IntervalLike], v: Sequence[IntervalLike], layers: Sequence[tuple[Sequence[Sequence[IntervalLike]], Sequence[IntervalLike] | None, str | None]], order: int) -> VecJet

Exact directional interval jet of a deep MLP along x(t) = x0 + t v.

Each layer is (W, b, name); name=None is a pure affine readout.

Parameters

Name	Type & default	Contract
x0positional-or-keyword	Sequence[IntervalLike]Required	See the operation contract and implementation below.
vpositional-or-keyword	Sequence[IntervalLike]Required	See the operation contract and implementation below.
layerspositional-or-keyword	Sequence[tuple[Sequence[Sequence[IntervalLike]], Sequence[IntervalLike] | None, str | None]]Required	See the operation contract and implementation below.
orderpositional-or-keyword	intRequired	See the operation contract and implementation below.

ReturnsVecJet

Executed regression · jet to tower roundtrip

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.

Full file, imports & fixtures ↗

def test_jet_to_tower_roundtrip() -> None:
    jet = mlp_jet([0.2], [1.0], [([[1.0]], [0.0], "tanh")], 4)
    series = [jet[k][0] for k in range(len(jet))]
    tower = jet_to_tower(series)
    # tower[1] = tanh'(0.2) = 1 - tanh(0.2)^2
    t = math.tanh(0.2)
    assert tower[1].lo <= 1 - t * t <= tower[1].hi

python -m pytest "packages/omnibias-core/tests/verified/test_sigma_and_jet.py::test_jet_to_tower_roundtrip" -q

Regression example · antiderivative jet constant and empty edges

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.

Full file, imports & fixtures ↗

def test_antiderivative_jet_constant_and_empty_edges() -> None:
    jet = [Interval.point(2.0), Interval.point(6.0), Interval.point(9.0)]
    anti = antiderivative_jet(jet, constant=Interval.point(-4.0))
    assert anti[0].lo == anti[0].hi == -4.0  # integration constant
    assert anti[1].lo <= 2.0 <= anti[1].hi  # A_1 = a_0 / 1
    assert anti[2].lo <= 3.0 <= anti[2].hi  # A_2 = a_1 / 2
    # a constant jet has no derivative information: derivative_jet yields length 0.
    assert derivative_jet([Interval.point(5.0)]) == []

python -m pytest packages/omnibias-core/tests/verified/test_sigma_and_jet.py -k test_antiderivative_jet_constant_and_empty_edges -q

Read the implementation

def mlp_jet(
    x0: Sequence[IntervalLike],
    v: Sequence[IntervalLike],
    layers: Sequence[
        tuple[Sequence[Sequence[IntervalLike]], Sequence[IntervalLike] | None, str | None]
    ],
    order: int,
) -> VecJet:
    """Exact directional interval jet of a deep MLP along ``x(t) = x0 + t v``.

    Each layer is ``(W, b, name)``; ``name=None`` is a pure affine readout.
    """
    jet = path_jet(x0, v, order)
    for weight, bias, name in layers:
        jet = affine_jet(jet, weight, bias) if name is None else layer_jet(jet, weight, bias, name)
    return jet

Related APIsomnibias.core.verified.affine_jet↗omnibias.core.verified.layer_jet↗omnibias.core.verified.path_jet↗

Other public import paths

• omnibias.core.verified.mlp_jet
• omnibias.core.verified.jet.mlp_jet

FUNCTION

path_jet

omnibias.core.verified.path_jetSource ↗

path_jet(x0: Sequence[IntervalLike], v: Sequence[IntervalLike], order: int) -> VecJet

Vector input jet for the line x(t) = x0 + t v truncated at order.

Parameters

Name	Type & default	Contract
x0positional-or-keyword	Sequence[IntervalLike]Required	See the operation contract and implementation below.
vpositional-or-keyword	Sequence[IntervalLike]Required	See the operation contract and implementation below.
orderpositional-or-keyword	intRequired	See the operation contract and implementation below.

ReturnsVecJet

Explicit validation & failure cases

• When order < 0, raises ValueError(f'order must be >= 0, got {order}').
• When len(v) != d, raises ValueError('x0 and v must have the same dimension').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · jet to tower roundtrip

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.

Full file, imports & fixtures ↗

def test_jet_to_tower_roundtrip() -> None:
    jet = mlp_jet([0.2], [1.0], [([[1.0]], [0.0], "tanh")], 4)
    series = [jet[k][0] for k in range(len(jet))]
    tower = jet_to_tower(series)
    # tower[1] = tanh'(0.2) = 1 - tanh(0.2)^2
    t = math.tanh(0.2)
    assert tower[1].lo <= 1 - t * t <= tower[1].hi

python -m pytest "packages/omnibias-core/tests/verified/test_sigma_and_jet.py::test_jet_to_tower_roundtrip" -q

Read the implementation

def path_jet(
    x0: Sequence[IntervalLike], v: Sequence[IntervalLike], order: int
) -> VecJet:
    """Vector input jet for the line ``x(t) = x0 + t v`` truncated at ``order``."""
    if order < 0:
        raise ValueError(f"order must be >= 0, got {order}")
    d = len(x0)
    if len(v) != d:
        raise ValueError("x0 and v must have the same dimension")
    rows: VecJet = [[Interval.from_value(x0[i]) for i in range(d)]]
    if order >= 1:
        rows.append([Interval.from_value(v[i]) for i in range(d)])
    for _ in range(order - 1):
        rows.append([_zero() for _ in range(d)])
    return rows[: order + 1]

Other public import paths

• omnibias.core.verified.path_jet
• omnibias.core.verified.jet.path_jet

FUNCTION

series_mul

omnibias.core.verified.series_mulSource ↗

series_mul(a: Sequence[Interval], b: Sequence[Interval]) -> Jet

Truncated Cauchy product of two equal-length interval series.

Parameters

Name	Type & default	Contract
apositional-or-keyword	Sequence[Interval]Required	See the operation contract and implementation below.
bpositional-or-keyword	Sequence[Interval]Required	See the operation contract and implementation below.

ReturnsJet

Explicit validation & failure cases

• When len(b) != np1, raises ValueError(f'series length mismatch: {len(a)} vs {len(b)}').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

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.

Full file, imports & fixtures ↗

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

Read the implementation

def series_mul(a: Sequence[Interval], b: Sequence[Interval]) -> Jet:
    """Truncated Cauchy product of two equal-length interval series."""
    np1 = len(a)
    if len(b) != np1:
        raise ValueError(f"series length mismatch: {len(a)} vs {len(b)}")
    out: Jet = []
    for n in range(np1):
        acc = _zero()
        for i in range(n + 1):
            acc = acc + a[i] * b[n - i]
        out.append(acc)
    return out

Other public import paths

• omnibias.core.verified.series_mul
• omnibias.core.verified.jet.series_mul

FUNCTION

tower_to_jet

omnibias.core.verified.tower_to_jetSource ↗

tower_to_jet(tower: Sequence[Interval]) -> Jet

Rescale a derivative tower by 1/k! to the Taylor jet.

Parameters

Name	Type & default	Contract
towerpositional-or-keyword	Sequence[Interval]Required	See the operation contract and implementation below.

ReturnsJet

Read the implementation

def tower_to_jet(tower: Sequence[Interval]) -> Jet:
    """Rescale a derivative tower by ``1/k!`` to the Taylor jet."""
    return [
        tower[k] * Interval.from_rational(Fraction(1, factorial(k)))
        for k in range(len(tower))
    ]

Other public import paths

• omnibias.core.verified.tower_to_jet
• omnibias.core.verified.jet.tower_to_jet

← Package overviewRunnable learning examples →