API REFERENCE/omnibias-core

omnibias.core.verified.lohner

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

Module contract & mathematical conventions

QR-Lohner validated flow: rigorous ODE integration without the wrapping blow-up.

Stepping a box through a rotation with plain interval arithmetic is a disaster: each step re-encloses a rotated box in an axis-aligned one, and the over-approximation compounds *exponentially* even though the true solution set stays bounded -- the **wrapping effect**. Lohner's trick is to carry the set in a co-moving orthonormal frame,

S_j = x_j \;\oplus\; Q_j\, r_j,

with x_j a point, Q_j an orthogonal matrix (refreshed by a QR factorisation each step) and r_j a small box. Because r_j lives in the rotating frame, the box does **not** grow under rotation.

The propagation needs the Jacobian of the time-h flow. This module encloses it with a rigorous **interval matrix exponential** of h * DF([Z]) over the step's a-priori enclosure [Z] (exact for linear systems, a sound C^1 bound for nonlinear ones), and reuses the validated Taylor step from omnibias.core.verified.ode for the centre.

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

JacobianEnclosure

omnibias.core.verified.JacobianEnclosureSource ↗

JacobianEnclosure = Callable[[Sequence[Interval]], IntervalMatrix]

A Jacobian enclosure: maps a box to an interval matrix bounding DF on it.

Read the implementation

JacobianEnclosure = Callable[[Sequence[Interval]], IntervalMatrix]

Other public import paths

• omnibias.core.verified.JacobianEnclosure
• omnibias.core.verified.lohner.JacobianEnclosure

CLASS

LohnerSet

omnibias.core.verified.LohnerSetSource ↗

class LohnerSet

Dataclass constructor fields; inherited fields, if any, are declared by the base class. A field(...) expression describes a default factory or field options, not a literal argument default.

A set center + Q r: point centre, orthogonal frame Q, box r.

Parameters

Name	Type & default	Contract
centerdataclass field	list[Interval]Required	See the operation contract and implementation below.
qdataclass field	list[list[float]]Required	See the operation contract and implementation below.
rdataclass field	list[Interval]Required	See the operation contract and implementation below.

Executed regression · g3 horizon extension

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_g3_horizon_extension() -> None:
    rows = horizon_report()
    assert len(rows) == 10
    assert all("ratio" in row for row in rows)
    wins = sum(1 for row in rows if row["win"])
    assert wins == 10, rows

python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -q

Regression example · lohner set roundtrip

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_lohner_set_roundtrip() -> None:
    box = [Interval(0.0, 2.0), Interval(-1.0, 1.0)]
    s = LohnerSet.from_box(box)
    out = s.to_box()
    for orig, got in zip(box, out, strict=True):
        assert got.lo <= orig.lo and orig.hi <= got.hi

python -m pytest packages/omnibias-core/tests/verified/test_lohner.py -k test_lohner_set_roundtrip -q

Fields & methods

centerfield

center: list[Interval]

Declared list[Interval] field on LohnerSet. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

qfield

q: list[list[float]]

Declared list[list[float]] field on LohnerSet. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

rfield

r: list[Interval]

Declared list[Interval] field on LohnerSet. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

from_boxmethod

from_box(cls, box: Sequence[IntervalLike]) -> LohnerSet

See the class contract above and the exact method implementation below.

Parameters

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

Returns: LohnerSet

Executed regression · g3 horizon extension

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_g3_horizon_extension() -> None:
    rows = horizon_report()
    assert len(rows) == 10
    assert all("ratio" in row for row in rows)
    wins = sum(1 for row in rows if row["win"])
    assert wins == 10, rows

python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -q

Method implementation

    def from_box(cls, box: Sequence[IntervalLike]) -> LohnerSet:
        ivs = [Interval.from_value(b) for b in box]
        n = len(ivs)
        center = [Interval.point(iv.mid) for iv in ivs]
        r = [iv - Interval.point(iv.mid) for iv in ivs]
        q = [[1.0 if i == j else 0.0 for j in range(n)] for i in range(n)]
        return cls(center, q, r)

View source ↗

to_boxmethod

to_box(self) -> list[Interval]

Outward-rounded axis-aligned enclosure of the represented set.

Returns: list[Interval]

Executed regression · g3 horizon extension

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_g3_horizon_extension() -> None:
    rows = horizon_report()
    assert len(rows) == 10
    assert all("ratio" in row for row in rows)
    wins = sum(1 for row in rows if row["win"])
    assert wins == 10, rows

python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -q

Method implementation

    def to_box(self) -> list[Interval]:
        """Outward-rounded axis-aligned enclosure of the represented set."""
        qr = matvec(to_interval_matrix(self.q), self.r)
        return [self.center[i] + qr[i] for i in range(len(self.center))]

View source ↗

widthmethod

width(self) -> float

The widest component of the enclosing box (a wrapping diagnostic).

Returns: float

Executed regression · g3 horizon extension

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_g3_horizon_extension() -> None:
    rows = horizon_report()
    assert len(rows) == 10
    assert all("ratio" in row for row in rows)
    wins = sum(1 for row in rows if row["win"])
    assert wins == 10, rows

python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -q

Method implementation

    def width(self) -> float:
        """The widest component of the enclosing box (a wrapping diagnostic)."""
        return max(iv.width for iv in self.to_box())

View source ↗

Read the implementation

class LohnerSet:
    r"""A set ``center + Q r``: point centre, orthogonal frame ``Q``, box ``r``."""

    center: list[Interval]
    q: list[list[float]]
    r: list[Interval]

    @classmethod
    def from_box(cls, box: Sequence[IntervalLike]) -> LohnerSet:
        ivs = [Interval.from_value(b) for b in box]
        n = len(ivs)
        center = [Interval.point(iv.mid) for iv in ivs]
        r = [iv - Interval.point(iv.mid) for iv in ivs]
        q = [[1.0 if i == j else 0.0 for j in range(n)] for i in range(n)]
        return cls(center, q, r)

    def to_box(self) -> list[Interval]:
        """Outward-rounded axis-aligned enclosure of the represented set."""
        qr = matvec(to_interval_matrix(self.q), self.r)
        return [self.center[i] + qr[i] for i in range(len(self.center))]

    def width(self) -> float:
        """The widest component of the enclosing box (a wrapping diagnostic)."""
        return max(iv.width for iv in self.to_box())

Related APIsomnibias.core.verified.matvec↗omnibias.core.verified.to_interval_matrix↗

Other public import paths

• omnibias.core.verified.LohnerSet
• omnibias.core.verified.lohner.LohnerSet

FUNCTION

constant_jacobian

omnibias.core.verified.constant_jacobianSource ↗

constant_jacobian(a: Sequence[Sequence[float]]) -> JacobianEnclosure

Jacobian enclosure for a linear field (the constant matrix A).

Parameters

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

ReturnsJacobianEnclosure

Executed regression · g3 horizon extension

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_g3_horizon_extension() -> None:
    rows = horizon_report()
    assert len(rows) == 10
    assert all("ratio" in row for row in rows)
    wins = sum(1 for row in rows if row["win"])
    assert wins == 10, rows

python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -q

Regression example · rotation long time tightness

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_rotation_long_time_tightness() -> None:
    # Even over 20 revolutions the Lohner box width stays bounded (no blow-up).
    a = [[0.0, -1.0], [1.0, 0.0]]
    field = linear_field(a)
    jac = constant_jacobian(a)
    y0 = [Interval(1.0, 1.0), Interval(0.0, 0.0)]  # exact point start
    h = 2.0 * math.pi / 100.0
    final = lohner_flow(field, jac, y0, h, 100 * 20, order=16)
    assert final.width() < 1e-3

python -m pytest packages/omnibias-core/tests/verified/test_lohner.py -k test_rotation_long_time_tightness -q

Read the implementation

def constant_jacobian(a: Sequence[Sequence[float]]) -> JacobianEnclosure:
    """Jacobian enclosure for a linear field (the constant matrix ``A``)."""
    a_iv = to_interval_matrix(a)

    def jac(_box: Sequence[Interval]) -> IntervalMatrix:
        return [row[:] for row in a_iv]

    return jac

Related APIsomnibias.core.verified.to_interval_matrix↗

Other public import paths

• omnibias.core.verified.constant_jacobian
• omnibias.core.verified.lohner.constant_jacobian

FUNCTION

interval_matrix_exp

omnibias.core.verified.interval_matrix_expSource ↗

interval_matrix_exp(m: IntervalMatrix, order: int=12) -> IntervalMatrix

Rigorous enclosure of exp(M) for an interval matrix M.

Sums sum_{k=0}^{order} M^k / k! and adds an entrywise Lagrange remainder sum_{k>order} ||M||^k / k! (valid because |(M^k)_{ij}| <= ||M||_inf^k). Requires ||M||_inf < order + 2 for a convergent tail bound.

Parameters

Name	Type & default	Contract
mpositional-or-keyword	IntervalMatrixRequired	See the operation contract and implementation below.
orderpositional-or-keyword	intDefault: 12	See the operation contract and implementation below.

ReturnsIntervalMatrix

Explicit validation & failure cases

• When ratio >= 1.0, raises ValueError(f'||M||={norm!r} too large for order {order}; reduce the step size').

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

Executed regression · g3 horizon extension

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_g3_horizon_extension() -> None:
    rows = horizon_report()
    assert len(rows) == 10
    assert all("ratio" in row for row in rows)
    wins = sum(1 for row in rows if row["win"])
    assert wins == 10, rows

python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -q

Regression example · interval matrix exp rotation generator

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_interval_matrix_exp_rotation_generator() -> None:
    # exp([[0,-t],[t,0]]) = [[cos t, -sin t],[sin t, cos t]].
    t = 0.7
    m = [[Interval.point(0.0), Interval.point(-t)], [Interval.point(t), Interval.point(0.0)]]
    e = interval_matrix_exp(m, order=30)
    assert e[0][0].lo <= math.cos(t) <= e[0][0].hi
    assert e[1][0].lo <= math.sin(t) <= e[1][0].hi

python -m pytest packages/omnibias-core/tests/verified/test_lohner.py -k test_interval_matrix_exp_rotation_generator -q

Read the implementation

def interval_matrix_exp(m: IntervalMatrix, order: int = 12) -> IntervalMatrix:
    r"""Rigorous enclosure of ``exp(M)`` for an interval matrix ``M``.

    Sums ``sum_{k=0}^{order} M^k / k!`` and adds an entrywise Lagrange remainder
    ``sum_{k>order} ||M||^k / k!`` (valid because ``|(M^k)_{ij}| <= ||M||_inf^k``).
    Requires ``||M||_inf < order + 2`` for a convergent tail bound.
    """
    n = len(m)
    acc = identity_matrix(n)
    term = identity_matrix(n)  # M^0 / 0!
    for k in range(1, order + 1):
        term = _scale_matrix(matmul(term, m), Interval.from_rational(Fraction(1, k)))
        acc = _mat_add(acc, term)
    norm = inf_norm_matrix(m)
    ratio = norm / (order + 2)
    if ratio >= 1.0:
        raise ValueError(f"||M||={norm!r} too large for order {order}; reduce the step size")
    tail = (
        Interval.point(norm).pow_int(order + 1)
        / Interval.from_rational(factorial(order + 1))
        / (Interval.point(1.0) - Interval.point(ratio))
    )
    t = tail.hi
    rem = Interval(-t, t)
    return [[acc[i][j] + rem for j in range(n)] for i in range(n)]

Related APIsomnibias.core.verified.Interval↗omnibias.core.verified.identity_matrix↗omnibias.core.verified.inf_norm_matrix↗omnibias.core.verified.matmul↗

Other public import paths

• omnibias.core.verified.interval_matrix_exp
• omnibias.core.verified.lohner.interval_matrix_exp

FUNCTION

linear_field

omnibias.core.verified.linear_fieldSource ↗

linear_field(a: Sequence[Sequence[float]]) -> VectorField

The autonomous linear vector field y' = A y as a VectorField.

Parameters

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

ReturnsVectorField

Executed regression · g3 horizon extension

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_g3_horizon_extension() -> None:
    rows = horizon_report()
    assert len(rows) == 10
    assert all("ratio" in row for row in rows)
    wins = sum(1 for row in rows if row["win"])
    assert wins == 10, rows

python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -q

Regression example · rotation long time tightness

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_rotation_long_time_tightness() -> None:
    # Even over 20 revolutions the Lohner box width stays bounded (no blow-up).
    a = [[0.0, -1.0], [1.0, 0.0]]
    field = linear_field(a)
    jac = constant_jacobian(a)
    y0 = [Interval(1.0, 1.0), Interval(0.0, 0.0)]  # exact point start
    h = 2.0 * math.pi / 100.0
    final = lohner_flow(field, jac, y0, h, 100 * 20, order=16)
    assert final.width() < 1e-3

python -m pytest packages/omnibias-core/tests/verified/test_lohner.py -k test_rotation_long_time_tightness -q

Read the implementation

def linear_field(a: Sequence[Sequence[float]]) -> VectorField:
    """The autonomous linear vector field ``y' = A y`` as a :data:`VectorField`."""
    a_iv = to_interval_matrix(a)

    def field(series: list[TaylorSeries]) -> list[TaylorSeries]:
        order = series[0].order
        out: list[TaylorSeries] = []
        for i in range(len(a_iv)):
            acc = TaylorSeries.constant(0.0, order)
            for j in range(len(a_iv)):
                acc = acc + series[j] * a_iv[i][j]
            out.append(acc)
        return out

    return field

Related APIsomnibias.core.verified.to_interval_matrix↗

Other public import paths

• omnibias.core.verified.linear_field
• omnibias.core.verified.lohner.linear_field

FUNCTION

lohner_flow

omnibias.core.verified.lohner_flowSource ↗

lohner_flow(field: VectorField, jac: JacobianEnclosure, y0: Sequence[IntervalLike], h: float, n_steps: int, order: int=12) -> LohnerSet

Integrate y' = field(y) for n_steps QR-Lohner steps; return the final set.

Parameters

Name	Type & default	Contract
fieldpositional-or-keyword	VectorFieldRequired	See the operation contract and implementation below.
jacpositional-or-keyword	JacobianEnclosureRequired	See the operation contract and implementation below.
y0positional-or-keyword	Sequence[IntervalLike]Required	See the operation contract and implementation below.
hpositional-or-keyword	floatRequired	See the operation contract and implementation below.
n_stepspositional-or-keyword	intRequired	See the operation contract and implementation below.
orderpositional-or-keyword	intDefault: 12	See the operation contract and implementation below.

ReturnsLohnerSet

Executed regression · g3 horizon extension

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_g3_horizon_extension() -> None:
    rows = horizon_report()
    assert len(rows) == 10
    assert all("ratio" in row for row in rows)
    wins = sum(1 for row in rows if row["win"])
    assert wins == 10, rows

python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -q

Regression example · rotation long time tightness

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_rotation_long_time_tightness() -> None:
    # Even over 20 revolutions the Lohner box width stays bounded (no blow-up).
    a = [[0.0, -1.0], [1.0, 0.0]]
    field = linear_field(a)
    jac = constant_jacobian(a)
    y0 = [Interval(1.0, 1.0), Interval(0.0, 0.0)]  # exact point start
    h = 2.0 * math.pi / 100.0
    final = lohner_flow(field, jac, y0, h, 100 * 20, order=16)
    assert final.width() < 1e-3

python -m pytest packages/omnibias-core/tests/verified/test_lohner.py -k test_rotation_long_time_tightness -q

Read the implementation

def lohner_flow(
    field: VectorField,
    jac: JacobianEnclosure,
    y0: Sequence[IntervalLike],
    h: float,
    n_steps: int,
    order: int = 12,
) -> LohnerSet:
    """Integrate ``y' = field(y)`` for ``n_steps`` QR-Lohner steps; return the final set."""
    state = LohnerSet.from_box(y0)
    for _ in range(n_steps):
        state = lohner_step(field, jac, state, h, order)
    return state

Related APIsomnibias.core.verified.lohner_step↗

Other public import paths

• omnibias.core.verified.lohner_flow
• omnibias.core.verified.lohner.lohner_flow

FUNCTION

lohner_step

omnibias.core.verified.lohner_stepSource ↗

lohner_step(field: VectorField, jac: JacobianEnclosure, state: LohnerSet, h: float, order: int) -> LohnerSet

One QR-Lohner step of size h for y' = field(y) with Jacobian jac.

Parameters

Name	Type & default	Contract
fieldpositional-or-keyword	VectorFieldRequired	See the operation contract and implementation below.
jacpositional-or-keyword	JacobianEnclosureRequired	See the operation contract and implementation below.
statepositional-or-keyword	LohnerSetRequired	See the operation contract and implementation below.
hpositional-or-keyword	floatRequired	See the operation contract and implementation below.
orderpositional-or-keyword	intRequired	See the operation contract and implementation below.

ReturnsLohnerSet

Executed regression · g3 horizon extension

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_g3_horizon_extension() -> None:
    rows = horizon_report()
    assert len(rows) == 10
    assert all("ratio" in row for row in rows)
    wins = sum(1 for row in rows if row["win"])
    assert wins == 10, rows

python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -q

Regression example · g6 lohner flow bit unchanged

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_g6_lohner_flow_bit_unchanged() -> None:
    snap_a = lohner_regression_snapshot()
    snap_b = lohner_regression_snapshot()
    assert snap_a == snap_b
    a = [[0.0, -1.0], [1.0, 0.0]]
    field = linear_field(a)
    jac = constant_jacobian(a)
    y0 = [Interval(0.999, 1.001), Interval(-0.001, 0.001)]
    classic = lohner_flow(field, jac, y0, 0.05, 20, order=12)
    # The jet wrapper must reproduce the same step as lohner_step.
    state = LohnerSet.from_box(y0)
    jet_state, budget = lohner_step_jet(state, field, jac, order=12, h=0.05)
    plain = lohner_step(field, jac, state, 0.05, 12)
    for left, right in zip(jet_state.to_box(), plain.to_box(), strict=True):
        assert left.lo == right.lo and left.hi == right.hi
    assert isinstance(budget, WidthBudget)
    wrap = naive_vs_lohner_wrapping()
    assert wrap["naive"] > wrap["lohner"]
    # Existing path still encloses the rotation centre.
    box = classic.to_box()
    assert box[0].lo <= math.cos(1.0) <= box[0].hi

python -m pytest packages/omnibias-core/tests/verified/test_jet_flow.py -k test_g6_lohner_flow_bit_unchanged -q

Read the implementation

def lohner_step(
    field: VectorField,
    jac: JacobianEnclosure,
    state: LohnerSet,
    h: float,
    order: int,
) -> LohnerSet:
    """One QR-Lohner step of size ``h`` for ``y' = field(y)`` with Jacobian ``jac``."""
    n = len(state.center)
    box = state.to_box()
    z_encl = _apriori_enclosure(field, box, h)
    # Centre: validated Taylor flow; keep the point, push its spread into the box.
    c_next = _step(field, state.center, h, order)
    xc = [Interval.point(iv.mid) for iv in c_next]
    z_rem = [c_next[i] - xc[i] for i in range(n)]
    # Variational Jacobian of the step, enclosed via the interval matrix exp.
    j_step = interval_matrix_exp(_scale_matrix(jac(z_encl), h), order=max(order, 8))
    b = matmul(j_step, to_interval_matrix(state.q))
    q_new = qr_gram_schmidt(_midpoint(b))
    q_new_t = to_interval_matrix(_transpose_float(q_new))
    r_lin = matvec(matmul(q_new_t, b), state.r)
    r_rem = matvec(q_new_t, z_rem)
    r_new = [r_lin[i] + r_rem[i] for i in range(n)]
    return LohnerSet(xc, q_new, r_new)

Related APIsomnibias.core.verified.matmul↗omnibias.core.verified.matvec↗omnibias.core.verified.to_interval_matrix↗omnibias.core.verified.LohnerSet↗omnibias.core.verified.interval_matrix_exp↗omnibias.core.verified.qr_gram_schmidt↗

Other public import paths

• omnibias.core.verified.lohner_step
• omnibias.core.verified.lohner.lohner_step

FUNCTION

naive_interval_flow

omnibias.core.verified.naive_interval_flowSource ↗

naive_interval_flow(a: Sequence[Sequence[float]], y0: Sequence[IntervalLike], h: float, n_steps: int, order: int=12) -> list[Interval]

Plain interval stepping of a *linear* flow -- the wrapping-prone baseline.

Parameters

Name	Type & default	Contract
apositional-or-keyword	Sequence[Sequence[float]]Required	See the operation contract and implementation below.
y0positional-or-keyword	Sequence[IntervalLike]Required	See the operation contract and implementation below.
hpositional-or-keyword	floatRequired	See the operation contract and implementation below.
n_stepspositional-or-keyword	intRequired	See the operation contract and implementation below.
orderpositional-or-keyword	intDefault: 12	See the operation contract and implementation below.

Returnslist[Interval]

Executed regression · g6 lohner flow bit unchanged

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_g6_lohner_flow_bit_unchanged() -> None:
    snap_a = lohner_regression_snapshot()
    snap_b = lohner_regression_snapshot()
    assert snap_a == snap_b
    a = [[0.0, -1.0], [1.0, 0.0]]
    field = linear_field(a)
    jac = constant_jacobian(a)
    y0 = [Interval(0.999, 1.001), Interval(-0.001, 0.001)]
    classic = lohner_flow(field, jac, y0, 0.05, 20, order=12)
    # The jet wrapper must reproduce the same step as lohner_step.
    state = LohnerSet.from_box(y0)
    jet_state, budget = lohner_step_jet(state, field, jac, order=12, h=0.05)
    plain = lohner_step(field, jac, state, 0.05, 12)
    for left, right in zip(jet_state.to_box(), plain.to_box(), strict=True):
        assert left.lo == right.lo and left.hi == right.hi
    assert isinstance(budget, WidthBudget)
    wrap = naive_vs_lohner_wrapping()
    assert wrap["naive"] > wrap["lohner"]
    # Existing path still encloses the rotation centre.
    box = classic.to_box()
    assert box[0].lo <= math.cos(1.0) <= box[0].hi

python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g6_lohner_flow_bit_unchanged" -q

Regression example · rotation wrapping is controlled

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_rotation_wrapping_is_controlled() -> None:
    # y' = A y, A a pure rotation generator: the true |y| is conserved, so the
    # enclosure of a small initial box should stay small for many revolutions.
    a = [[0.0, -1.0], [1.0, 0.0]]
    field = linear_field(a)
    jac = constant_jacobian(a)
    y0 = [Interval(0.999, 1.001), Interval(-0.001, 0.001)]

    h = 2.0 * math.pi / 200.0
    steps = 200 * 6  # six full revolutions
    final = lohner_flow(field, jac, y0, h, steps, order=14)
    naive = naive_interval_flow(a, y0, h, steps, order=14)

    # True solution of the centre after `steps` is rotation by total angle ~ 6*2pi.
    angle = h * steps
    true_x = math.cos(angle) * 1.0 - math.sin(angle) * 0.0
    true_y = math.sin(angle) * 1.0 + math.cos(angle) * 0.0
    box = final.to_box()
    assert box[0].lo <= true_x <= box[0].hi
    assert box[1].lo <= true_y <= box[1].hi

    # Wrapping control: Lohner stays tight; naive interval stepping blows up.
    assert final.width() < 0.05
    assert naive[0].width > 10.0 * final.width()

python -m pytest packages/omnibias-core/tests/verified/test_lohner.py -k test_rotation_wrapping_is_controlled -q

Read the implementation

def naive_interval_flow(
    a: Sequence[Sequence[float]],
    y0: Sequence[IntervalLike],
    h: float,
    n_steps: int,
    order: int = 12,
) -> list[Interval]:
    """Plain interval stepping of a *linear* flow -- the wrapping-prone baseline."""
    j_step = interval_matrix_exp(_scale_matrix(to_interval_matrix(a), h), order=max(order, 8))
    box = [Interval.from_value(v) for v in y0]
    for _ in range(n_steps):
        box = matvec(j_step, box)
    return box

Related APIsomnibias.core.verified.matvec↗omnibias.core.verified.to_interval_matrix↗omnibias.core.verified.interval_matrix_exp↗

Other public import paths

• omnibias.core.verified.naive_interval_flow
• omnibias.core.verified.lohner.naive_interval_flow

FUNCTION

qr_gram_schmidt

omnibias.core.verified.qr_gram_schmidtSource ↗

qr_gram_schmidt(a: Sequence[Sequence[float]]) -> list[list[float]]

Orthonormal Q (as Q[i][j]) from modified Gram-Schmidt on a's columns.

Falls back to the identity for a (numerically) rank-deficient input so the Lohner step always has a valid frame.

Rigour caveat (recorded assumption, **not** a discharged theorem): Q is computed in plain float and is orthonormal only to working precision. The QR-Lohner step uses Qᵀ in place of the true inverse Q⁻¹ (see lohner_step), which is exact only for a perfectly orthogonal Q. The residual non-orthogonality ||QᵀQ - I|| (~1e-15 for modified Gram-Schmidt) is **assumed negligible** here and is *not* separately interval-bounded. A fully rigorous implementation would either enclose Q⁻¹ by verified Gaussian elimination or inflate the box r by a certified bound on that defect; long nonlinear integrations should be treated with that caveat in mind.

Parameters

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

Returnslist[list[float]]

Executed regression · g3 horizon extension

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_g3_horizon_extension() -> None:
    rows = horizon_report()
    assert len(rows) == 10
    assert all("ratio" in row for row in rows)
    wins = sum(1 for row in rows if row["win"])
    assert wins == 10, rows

python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -q

Read the implementation

def qr_gram_schmidt(a: Sequence[Sequence[float]]) -> list[list[float]]:
    """Orthonormal ``Q`` (as ``Q[i][j]``) from modified Gram-Schmidt on ``a``'s columns.

    Falls back to the identity for a (numerically) rank-deficient input so the
    Lohner step always has a valid frame.

    Rigour caveat (recorded assumption, **not** a discharged theorem): ``Q`` is
    computed in plain ``float`` and is orthonormal only to working precision. The
    QR-Lohner step uses ``Qᵀ`` in place of the true inverse ``Q⁻¹`` (see
    :func:`lohner_step`), which is exact only for a perfectly orthogonal ``Q``. The
    residual non-orthogonality ``||QᵀQ - I||`` (~1e-15 for modified Gram-Schmidt)
    is **assumed negligible** here and is *not* separately interval-bounded. A
    fully rigorous implementation would either enclose ``Q⁻¹`` by verified Gaussian
    elimination or inflate the box ``r`` by a certified bound on that defect; long
    nonlinear integrations should be treated with that caveat in mind.
    """
    n = len(a)
    cols = [[float(a[i][j]) for i in range(n)] for j in range(n)]
    q_cols: list[list[float]] = []
    for j in range(n):
        v = cols[j][:]
        for q in q_cols:
            dot = sum(q[i] * v[i] for i in range(n))
            v = [v[i] - dot * q[i] for i in range(n)]
        norm = sqrt(sum(vi * vi for vi in v))
        if norm < 1e-12:
            return [[1.0 if i == j else 0.0 for j in range(n)] for i in range(n)]
        q_cols.append([vi / norm for vi in v])
    return [[q_cols[j][i] for j in range(n)] for i in range(n)]

Other public import paths

• omnibias.core.verified.qr_gram_schmidt
• omnibias.core.verified.lohner.qr_gram_schmidt

← Package overviewRunnable learning examples →