API REFERENCE/omnibias-core

omnibias.core.verified.linalg

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

Module contract & mathematical conventions

Verified dense linear algebra: a certified bound on ||A^{-1}||.

The radii-polynomial / Newton-Kantorovich machinery needs a *rigorous* upper bound on the norm of the inverse linearised operator. The classical tool is the **Neumann lemma**: if B approximates A^{-1} well enough that

\kappa := \| I - B A \| < 1,

then A is invertible and

\| A^{-1} \| \;\le\; \frac{\|B\|}{1 - \kappa}.

The approximate inverse B is produced by an ordinary floating-point solver (e.g. numpy.linalg.inv) by the *caller*; this module only needs A and B as nested float lists, so omnibias.core keeps its zero-dependency contract. The residual I - B A and both operator norms are evaluated in outward-rounded interval arithmetic, so the returned bound is theorem-grade.

Norms are the matrix infinity norm (max absolute row sum) and the matching vector sup norm.

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

FloatMatrix

omnibias.core.verified.linalg.FloatMatrixSource ↗

FloatMatrix = Sequence[Sequence[float]]

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

FloatMatrix = Sequence[Sequence[float]]

CONSTANT

IntervalMatrix

omnibias.core.verified.linalg.IntervalMatrixSource ↗

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

IntervalMatrix = list[list[Interval]]

CONSTANT

IntervalVector

omnibias.core.verified.linalg.IntervalVectorSource ↗

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

IntervalVector = list[Interval]

FUNCTION

identity_matrix

omnibias.core.verified.identity_matrixSource ↗

identity_matrix(n: int) -> IntervalMatrix

The module contract describes the context for this operation. Its signature, explicit validation, return expressions, and implementation are recorded below.

Parameters

Name	Type & default	Contract
npositional-or-keyword	intRequired	See the operation contract and implementation below.

ReturnsIntervalMatrix

Executed regression · certified damping zero when already conditioned

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_certified_damping_zero_when_already_conditioned() -> None:
    a = [[2.0, 0.0], [0.0, 3.0]]  # kappa = 1.5
    assert certified_damping(a, target_condition=10.0) == 0.0

python -m pytest "packages/omnibias-core/tests/verified/test_conditioning.py::test_certified_damping_zero_when_already_conditioned" -q

Read the implementation

def identity_matrix(n: int) -> IntervalMatrix:
    return [[Interval.point(1.0 if i == j else 0.0) for j in range(n)] for i in range(n)]

Other public import paths

• omnibias.core.verified.identity_matrix
• omnibias.core.verified.linalg.identity_matrix

FUNCTION

inf_norm_matrix

omnibias.core.verified.inf_norm_matrixSource ↗

inf_norm_matrix(a: IntervalMatrix) -> float

Rigorous upper bound on the infinity norm of any matrix in a.

Parameters

Name	Type & default	Contract
apositional-or-keyword	IntervalMatrixRequired	See the operation contract and implementation below.

Returnsfloat

Executed regression · inf norm matrix upper bound

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_inf_norm_matrix_upper_bound() -> None:
    a = to_interval_matrix([[1.0, -2.0], [3.0, 0.5]])
    assert inf_norm_matrix(a) >= 3.5  # row sums 3, 3.5

python -m pytest "packages/omnibias-core/tests/verified/test_numerics.py::test_inf_norm_matrix_upper_bound" -q

Read the implementation

def inf_norm_matrix(a: IntervalMatrix) -> float:
    """Rigorous upper bound on the infinity norm of any matrix in ``a``."""
    best = 0.0
    for row in a:
        row_sum = sum_intervals([x.abs() for x in row])
        best = max(best, row_sum.hi)
    return best

Related APIsomnibias.core.verified.sum_intervals↗

Other public import paths

• omnibias.core.verified.inf_norm_matrix
• omnibias.core.verified.linalg.inf_norm_matrix

FUNCTION

inf_norm_vector

omnibias.core.verified.inf_norm_vectorSource ↗

inf_norm_vector(x: Sequence[Interval]) -> float

Rigorous upper bound on max_i |x_i|.

Parameters

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

Returnsfloat

Executed regression · select keeps trial on accept

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_select_keeps_trial_on_accept() -> None:
    func, jac, lip = polynomial_sqrt2_maps()
    decision = kantorovich_accept_step(
        func, jac, GOOD_A, [GOOD_TRIAL], lipschitz_df=lip, r_max=R_MAX
    )
    chosen = select_accepted_params([0.25], [GOOD_TRIAL], decision)
    assert chosen == [GOOD_TRIAL]

python -m pytest "packages/omnibias-core/tests/verified/test_kantorovich_accept.py::test_select_keeps_trial_on_accept" -q

Read the implementation

def inf_norm_vector(x: Sequence[Interval]) -> float:
    """Rigorous upper bound on ``max_i |x_i|``."""
    return max((xi.abs().hi for xi in x), default=0.0)

Other public import paths

• omnibias.core.verified.inf_norm_vector
• omnibias.core.verified.linalg.inf_norm_vector

FUNCTION

interval_solve

omnibias.core.verified.interval_solveSource ↗

interval_solve(matrix: Sequence[Sequence[IntervalLike]], rhs: Sequence[IntervalLike], *, approximate_inverse: FloatMatrix | None=None, max_iter: int=8, symmetric: bool=False) -> IntervalVector

Enclose solutions of the interval linear system matrix * x = rhs.

For a general matrix box, this uses a Krawczyk fixed-point enclosure with a floating midpoint inverse as preconditioner. A contractive comparison iteration then sharpens its initial infinity-norm box componentwise. It raises ValueError rather than returning a non-rigorous answer if the required ||I - B A||_inf < 1 test fails.

Set symmetric=True to use the interval LDL^T path instead. That route needs sign-definite pivots and solves the factorized interval system by triangular substitution, avoiding a floating preconditioner.

Parameters

Name	Type & default	Contract
matrixpositional-or-keyword	Sequence[Sequence[IntervalLike]]Required	See the operation contract and implementation below.
rhspositional-or-keyword	Sequence[IntervalLike]Required	See the operation contract and implementation below.
approximate_inversekeyword-only	FloatMatrix | NoneDefault: None	See the operation contract and implementation below.
max_iterkeyword-only	intDefault: 8	See the operation contract and implementation below.
symmetrickeyword-only	boolDefault: False	See the operation contract and implementation below.

ReturnsIntervalVector

Explicit validation & failure cases

• When max_iter < 0, raises ValueError('max_iter must be non-negative').
• When len(f) != n, raises ValueError('right-hand side length must match matrix dimension').
• When solved is None, raises ValueError('symmetric interval LDLT factorization is inconclusive').
• When not all((isfinite(value) for row in midpoint for value in row)), raises ValueError('interval solve requires finite matrix endpoints').
• When preconditioner is None, raises ValueError('midpoint matrix is singular').
• When len(preconditioner) != n or any((len(row) != n for row in preconditioner)), raises ValueError('approximate inverse shape must match matrix').
• When not all((isfinite(value) for row in preconditioner for value in row)), raises ValueError('approximate inverse entries must be finite').
• When not all((isfinite(value) for value in center)), raises ValueError('interval solve produced a non-finite midpoint center').
• When not kappa < 1.0, raises ValueError('Krawczyk interval solve is inconclusive: ||I - B A||_inf must be < 1').

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

Executed regression · interval triangular solve and inconclusive inputs

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_interval_triangular_solve_and_inconclusive_inputs() -> None:
    lower = [
        [Interval.point(2.0), Interval.point(0.0)],
        [Interval.point(-1.0), Interval.point(3.0)],
    ]
    rhs = [Interval.point(4.0), Interval.point(5.0)]
    solution = interval_triangular_solve(lower, rhs, lower=True)
    assert solution[0].contains(2.0)
    assert solution[1].contains(7.0 / 3.0)

    upper = [
        [Interval.point(2.0), Interval.point(-1.0)],
        [Interval.point(0.0), Interval.point(3.0)],
    ]
    upper_solution = interval_triangular_solve(upper, rhs, lower=False)
    assert upper_solution[0].contains(17.0 / 6.0)
    assert upper_solution[1].contains(5.0 / 3.0)

    with pytest.raises(ValueError, match="singular|must be < 1"):
        interval_solve([[1.0, 1.0], [1.0, 1.0]], [1.0, 1.0])

python -m pytest "packages/omnibias-core/tests/verified/test_linalg.py::test_interval_triangular_solve_and_inconclusive_inputs" -q

Regression example · interval solve krawczyk encloses grid and random systems

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_solve_krawczyk_encloses_grid_and_random_systems() -> None:
    """A Krawczyk comparison enclosure contains every sampled point-system solve."""
    matrix_lo = np.asarray([[3.8, -0.4], [0.1, 2.7]])
    matrix_hi = np.asarray([[4.2, -0.2], [0.3, 3.1]])
    rhs_lo = np.asarray([-1.2, 0.5])
    rhs_hi = np.asarray([-0.8, 0.9])
    matrix = [
        [Interval(float(matrix_lo[i, j]), float(matrix_hi[i, j])) for j in range(2)]
        for i in range(2)
    ]
    rhs = [Interval(float(rhs_lo[i]), float(rhs_hi[i])) for i in range(2)]
    solution = interval_solve(matrix, rhs, max_iter=12)

    # Dense deterministic samples.
    for matrix_fraction in np.linspace(0.0, 1.0, 17):
        matrix_sample = _sample(matrix_lo, matrix_hi, float(matrix_fraction))
        for rhs_fraction in np.linspace(0.0, 1.0, 17):
            rhs_sample = _sample(rhs_lo, rhs_hi, float(rhs_fraction))
            _assert_contains(solution, np.linalg.solve(matrix_sample, rhs_sample))

    # Independent random samples vary every entry separately.
    rng = np.random.default_rng(20260827)
    for _ in range(128):
        matrix_sample = rng.uniform(matrix_lo, matrix_hi)
        rhs_sample = rng.uniform(rhs_lo, rhs_hi)
        _assert_contains(solution, np.linalg.solve(matrix_sample, rhs_sample))

python -m pytest packages/omnibias-core/tests/verified/test_linalg.py -k test_interval_solve_krawczyk_encloses_grid_and_random_systems -q

Read the implementation

def interval_solve(
    matrix: Sequence[Sequence[IntervalLike]],
    rhs: Sequence[IntervalLike],
    *,
    approximate_inverse: FloatMatrix | None = None,
    max_iter: int = 8,
    symmetric: bool = False,
) -> IntervalVector:
    r"""Enclose solutions of the interval linear system ``matrix * x = rhs``.

    For a general matrix box, this uses a Krawczyk fixed-point enclosure with a
    floating midpoint inverse as preconditioner.  A contractive comparison
    iteration then sharpens its initial infinity-norm box componentwise.  It
    raises :class:`ValueError` rather than returning a non-rigorous answer if
    the required ``||I - B A||_inf < 1`` test fails.

    Set ``symmetric=True`` to use the interval ``LDL^T`` path instead.  That
    route needs sign-definite pivots and solves the factorized interval system
    by triangular substitution, avoiding a floating preconditioner.
    """
    if max_iter < 0:
        raise ValueError("max_iter must be non-negative")
    a = _square_interval_matrix(matrix)
    n = len(a)
    f = [Interval.from_value(value) for value in rhs]
    if len(f) != n:
        raise ValueError("right-hand side length must match matrix dimension")

    if symmetric:
        solved = _symmetric_ldlt_solve(a, f)
        if solved is None:
            raise ValueError("symmetric interval LDLT factorization is inconclusive")
        return solved

    midpoint = [[entry.mid for entry in row] for row in a]
    if not all(isfinite(value) for row in midpoint for value in row):
        raise ValueError("interval solve requires finite matrix endpoints")
    if approximate_inverse is None:
        preconditioner = _float_inverse(midpoint)
        if preconditioner is None:
            raise ValueError("midpoint matrix is singular")
    else:
        preconditioner = [
            [float(value) for value in row] for row in approximate_inverse
        ]
        if len(preconditioner) != n or any(len(row) != n for row in preconditioner):
            raise ValueError("approximate inverse shape must match matrix")
        if not all(isfinite(value) for row in preconditioner for value in row):
            raise ValueError("approximate inverse entries must be finite")

    f_mid = [entry.mid for entry in f]
    center = [
        fsum(preconditioner[i][j] * f_mid[j] for j in range(n))
        for i in range(n)
    ]
    if not all(isfinite(value) for value in center):
        raise ValueError("interval solve produced a non-finite midpoint center")
    b = to_interval_matrix(preconditioner)
    center_iv = [Interval.point(value) for value in center]
    residual = _interval_vector_sub(f, matvec(a, center_iv))
    correction = matvec(b, residual)
    contraction = mat_sub(identity_matrix(n), matmul(b, a))
    kappa = inf_norm_matrix(contraction)
    if not kappa < 1.0:
        raise ValueError(
            "Krawczyk interval solve is inconclusive: ||I - B A||_inf must be < 1"
        )

    one_minus_kappa = Interval.point(1.0) - Interval.point(kappa)
    global_radius = (
        Interval.point(inf_norm_vector(correction)) * one_minus_kappa.reciprocal()
    ).hi
    radii = [global_radius for _ in range(n)]
    for _ in range(max_iter):
        next_radii: list[float] = []
        for i in range(n):
            bound = correction[i].abs()
            for j in range(n):
                bound = bound + contraction[i][j].abs() * Interval.point(radii[j])
            next_radii.append(min(radii[i], bound.hi))
        radii = next_radii

    enclosure = [
        Interval.point(center[i]) + Interval(-radii[i], radii[i]) for i in range(n)
    ]
    for _ in range(max_iter):
        delta = _interval_vector_sub(enclosure, center_iv)
        image_delta = matvec(contraction, delta)
        image = [
            center_iv[i] + correction[i] + image_delta[i] for i in range(n)
        ]
        try:
            next_enclosure = [
                enclosure[i].intersect(image[i]) for i in range(n)
            ]
        except ValueError:
            break
        if next_enclosure == enclosure:
            break
        enclosure = next_enclosure
    return enclosure

Related APIsomnibias.core.verified.Interval↗omnibias.core.verified.identity_matrix↗omnibias.core.verified.inf_norm_matrix↗omnibias.core.verified.inf_norm_vector↗omnibias.core.verified.mat_sub↗omnibias.core.verified.matmul↗omnibias.core.verified.matvec↗omnibias.core.verified.to_interval_matrix↗

Other public import paths

• omnibias.core.verified.interval_solve
• omnibias.core.verified.linalg.interval_solve

FUNCTION

interval_triangular_solve

omnibias.core.verified.interval_triangular_solveSource ↗

interval_triangular_solve(matrix: Sequence[Sequence[IntervalLike]], rhs: Sequence[IntervalLike], *, lower: bool, unit_diagonal: bool=False) -> IntervalVector

Solve an interval triangular system by forward or backward substitution.

The result encloses the solution of every point system represented by matrix and rhs. Every diagonal interval must exclude zero unless unit_diagonal=True. Only the declared triangular half of matrix is used, so callers can supply a full matrix without copying it.

Parameters

Name	Type & default	Contract
matrixpositional-or-keyword	Sequence[Sequence[IntervalLike]]Required	See the operation contract and implementation below.
rhspositional-or-keyword	Sequence[IntervalLike]Required	See the operation contract and implementation below.
lowerkeyword-only	boolRequired	See the operation contract and implementation below.
unit_diagonalkeyword-only	boolDefault: False	See the operation contract and implementation below.

ReturnsIntervalVector

Explicit validation & failure cases

• When n == 0 or any((len(row) != n for row in a)), raises ValueError('triangular solve requires a non-empty square matrix').
• When len(b) != n, raises ValueError('right-hand side length must match matrix dimension').

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

Executed regression · result is the dataclass type

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_result_is_the_dataclass_type() -> None:
    cert = certified_invariant_subspace(A_DEGENERATE, [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0]])
    assert isinstance(cert, InvariantSubspaceCertificate)
    assert cert.dimension == 3
    assert cert.cluster_size == 2

python -m pytest "packages/omnibias-core/tests/verified/test_invariant_subspace.py::test_result_is_the_dataclass_type" -q

Regression example · interval triangular solve and inconclusive inputs

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_triangular_solve_and_inconclusive_inputs() -> None:
    lower = [
        [Interval.point(2.0), Interval.point(0.0)],
        [Interval.point(-1.0), Interval.point(3.0)],
    ]
    rhs = [Interval.point(4.0), Interval.point(5.0)]
    solution = interval_triangular_solve(lower, rhs, lower=True)
    assert solution[0].contains(2.0)
    assert solution[1].contains(7.0 / 3.0)

    upper = [
        [Interval.point(2.0), Interval.point(-1.0)],
        [Interval.point(0.0), Interval.point(3.0)],
    ]
    upper_solution = interval_triangular_solve(upper, rhs, lower=False)
    assert upper_solution[0].contains(17.0 / 6.0)
    assert upper_solution[1].contains(5.0 / 3.0)

    with pytest.raises(ValueError, match="singular|must be < 1"):
        interval_solve([[1.0, 1.0], [1.0, 1.0]], [1.0, 1.0])

python -m pytest packages/omnibias-core/tests/verified/test_linalg.py -k test_interval_triangular_solve_and_inconclusive_inputs -q

Read the implementation

def interval_triangular_solve(
    matrix: Sequence[Sequence[IntervalLike]],
    rhs: Sequence[IntervalLike],
    *,
    lower: bool,
    unit_diagonal: bool = False,
) -> IntervalVector:
    r"""Solve an interval triangular system by forward or backward substitution.

    The result encloses the solution of every point system represented by
    ``matrix`` and ``rhs``.  Every diagonal interval must exclude zero unless
    ``unit_diagonal=True``.  Only the declared triangular half of ``matrix`` is
    used, so callers can supply a full matrix without copying it.
    """
    a = to_interval_matrix(matrix)
    n = len(a)
    if n == 0 or any(len(row) != n for row in a):
        raise ValueError("triangular solve requires a non-empty square matrix")
    b = [Interval.from_value(value) for value in rhs]
    if len(b) != n:
        raise ValueError("right-hand side length must match matrix dimension")

    solution = [Interval.point(0.0) for _ in range(n)]
    indices = range(n) if lower else range(n - 1, -1, -1)
    for i in indices:
        numerator = b[i]
        known = range(i) if lower else range(i + 1, n)
        for j in known:
            numerator = numerator - a[i][j] * solution[j]
        solution[i] = numerator if unit_diagonal else numerator / a[i][i]
    return solution

Related APIsomnibias.core.verified.to_interval_matrix↗

Other public import paths

• omnibias.core.verified.interval_triangular_solve
• omnibias.core.verified.linalg.interval_triangular_solve

FUNCTION

mat_sub

omnibias.core.verified.mat_subSource ↗

mat_sub(a: IntervalMatrix, b: IntervalMatrix) -> IntervalMatrix

The module contract describes the context for this operation. Its signature, explicit validation, return expressions, and implementation are recorded below.

Parameters

Name	Type & default	Contract
apositional-or-keyword	IntervalMatrixRequired	See the operation contract and implementation below.
bpositional-or-keyword	IntervalMatrixRequired	See the operation contract and implementation below.

ReturnsIntervalMatrix

Executed regression · certified damping zero when already conditioned

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_certified_damping_zero_when_already_conditioned() -> None:
    a = [[2.0, 0.0], [0.0, 3.0]]  # kappa = 1.5
    assert certified_damping(a, target_condition=10.0) == 0.0

python -m pytest "packages/omnibias-core/tests/verified/test_conditioning.py::test_certified_damping_zero_when_already_conditioned" -q

Read the implementation

def mat_sub(a: IntervalMatrix, b: IntervalMatrix) -> IntervalMatrix:
    return [[a[i][j] - b[i][j] for j in range(len(a[i]))] for i in range(len(a))]

Other public import paths

• omnibias.core.verified.mat_sub
• omnibias.core.verified.linalg.mat_sub

FUNCTION

matmul

omnibias.core.verified.matmulSource ↗

matmul(a: IntervalMatrix, b: IntervalMatrix) -> IntervalMatrix

The module contract describes the context for this operation. Its signature, explicit validation, return expressions, and implementation are recorded below.

Parameters

Name	Type & default	Contract
apositional-or-keyword	IntervalMatrixRequired	See the operation contract and implementation below.
bpositional-or-keyword	IntervalMatrixRequired	See the operation contract and implementation below.

ReturnsIntervalMatrix

Explicit validation & failure cases

• When a and len(a[0]) != k, raises ValueError('inner dimensions do not match').

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

Executed regression · certified damping zero when already conditioned

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_certified_damping_zero_when_already_conditioned() -> None:
    a = [[2.0, 0.0], [0.0, 3.0]]  # kappa = 1.5
    assert certified_damping(a, target_condition=10.0) == 0.0

python -m pytest "packages/omnibias-core/tests/verified/test_conditioning.py::test_certified_damping_zero_when_already_conditioned" -q

Read the implementation

def matmul(a: IntervalMatrix, b: IntervalMatrix) -> IntervalMatrix:
    n, k, m = len(a), len(b), len(b[0]) if b else 0
    if a and len(a[0]) != k:
        raise ValueError("inner dimensions do not match")
    out: IntervalMatrix = []
    for i in range(n):
        row: list[Interval] = []
        for j in range(m):
            acc = Interval.point(0.0)
            for p in range(k):
                acc = acc + a[i][p] * b[p][j]
            row.append(acc)
        out.append(row)
    return out

Other public import paths

• omnibias.core.verified.matmul
• omnibias.core.verified.linalg.matmul

FUNCTION

matvec

omnibias.core.verified.matvecSource ↗

matvec(a: IntervalMatrix, x: Sequence[Interval]) -> list[Interval]

The module contract describes the context for this operation. Its signature, explicit validation, return expressions, and implementation are recorded below.

Parameters

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

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

Regression example · hilbert kills 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.

Full file, imports & fixtures ↗

def test_hilbert_kills_constant() -> None:
    n = 16
    hmat = hilbert_circulant(n)
    ones = [Interval.point(1.0) for _ in range(n)]
    out = matvec(hmat, ones)
    for v in out:
        assert v.contains(0.0)
        assert abs(v.lo) < 1e-12 and abs(v.hi) < 1e-12

python -m pytest packages/omnibias-core/tests/verified/test_spectral.py -k test_hilbert_kills_constant -q

Read the implementation

def matvec(a: IntervalMatrix, x: Sequence[Interval]) -> list[Interval]:
    out: list[Interval] = []
    for row in a:
        acc = Interval.point(0.0)
        for aij, xj in zip(row, x, strict=True):
            acc = acc + aij * xj
        out.append(acc)
    return out

Other public import paths

• omnibias.core.verified.matvec
• omnibias.core.verified.linalg.matvec

FUNCTION

neumann_inverse_norm_bound

omnibias.core.verified.neumann_inverse_norm_boundSource ↗

neumann_inverse_norm_bound(a: FloatMatrix, b: FloatMatrix) -> dict[str, float | bool]

Certify ||A^{-1}||_inf <= ||B||/(1 - ||I - B A||) if kappa < 1.

Parameters

a The (float) matrix whose inverse norm is sought. b A floating-point approximate inverse of a (e.g. numpy.linalg.inv).

Returns

dict[str, float | bool] kappa (a rigorous upper bound on ||I - BA||), norm_b, inverse_norm_bound, and a certified flag.

Parameters

Name	Type & default	Contract
apositional-or-keyword	FloatMatrixRequired	The (float) matrix whose inverse norm is sought.
bpositional-or-keyword	FloatMatrixRequired	A floating-point approximate inverse of a (e.g. numpy.linalg.inv).

Returnsdict[str, float | bool]

Executed regression · certified damping zero when already conditioned

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_certified_damping_zero_when_already_conditioned() -> None:
    a = [[2.0, 0.0], [0.0, 3.0]]  # kappa = 1.5
    assert certified_damping(a, target_condition=10.0) == 0.0

python -m pytest "packages/omnibias-core/tests/verified/test_conditioning.py::test_certified_damping_zero_when_already_conditioned" -q

Regression example · neumann fails for singular

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_neumann_fails_for_singular() -> None:
    a = [[1.0, 1.0], [1.0, 1.0]]  # singular
    b = [[1.0, 0.0], [0.0, 1.0]]
    rep = neumann_inverse_norm_bound(a, b)
    assert rep["certified"] is False
    assert rep["inverse_norm_bound"] == float("inf")

python -m pytest packages/omnibias-core/tests/verified/test_numerics.py -k test_neumann_fails_for_singular -q

Read the implementation

def neumann_inverse_norm_bound(a: FloatMatrix, b: FloatMatrix) -> dict[str, float | bool]:
    """Certify ``||A^{-1}||_inf <= ||B||/(1 - ||I - B A||)`` if ``kappa < 1``.

    Parameters
    ----------
    a
        The (float) matrix whose inverse norm is sought.
    b
        A floating-point approximate inverse of ``a`` (e.g. ``numpy.linalg.inv``).

    Returns
    -------
    dict[str, float | bool]
        ``kappa`` (a rigorous upper bound on ``||I - BA||``), ``norm_b``,
        ``inverse_norm_bound``, and a ``certified`` flag.
    """
    n = len(a)
    a_iv = to_interval_matrix(a)
    b_iv = to_interval_matrix(b)
    residual = mat_sub(identity_matrix(n), matmul(b_iv, a_iv))
    kappa = inf_norm_matrix(residual)
    norm_b = inf_norm_matrix(b_iv)
    certified = kappa < 1.0
    if certified:
        one_minus = Interval(1.0, 1.0) - Interval.point(kappa)  # lower-bounds 1 - kappa
        bound = (Interval.point(norm_b) * one_minus.reciprocal()).hi
    else:
        bound = float("inf")
    return {
        "kappa": kappa,
        "norm_b": norm_b,
        "inverse_norm_bound": bound,
        "certified": certified,
    }

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

Other public import paths

• omnibias.core.verified.neumann_inverse_norm_bound
• omnibias.core.verified.linalg.neumann_inverse_norm_bound

FUNCTION

to_interval_matrix

omnibias.core.verified.to_interval_matrixSource ↗

to_interval_matrix(a: Sequence[Sequence[IntervalLike]]) -> IntervalMatrix

The module contract describes the context for this operation. Its signature, explicit validation, return expressions, and implementation are recorded below.

Parameters

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

ReturnsIntervalMatrix

Executed regression · inf norm matrix upper bound

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_inf_norm_matrix_upper_bound() -> None:
    a = to_interval_matrix([[1.0, -2.0], [3.0, 0.5]])
    assert inf_norm_matrix(a) >= 3.5  # row sums 3, 3.5

python -m pytest "packages/omnibias-core/tests/verified/test_numerics.py::test_inf_norm_matrix_upper_bound" -q

Regression example · neumann fails for singular

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_neumann_fails_for_singular() -> None:
    a = [[1.0, 1.0], [1.0, 1.0]]  # singular
    b = [[1.0, 0.0], [0.0, 1.0]]
    rep = neumann_inverse_norm_bound(a, b)
    assert rep["certified"] is False
    assert rep["inverse_norm_bound"] == float("inf")

python -m pytest packages/omnibias-core/tests/verified/test_numerics.py -k test_neumann_fails_for_singular -q

Read the implementation

def to_interval_matrix(a: Sequence[Sequence[IntervalLike]]) -> IntervalMatrix:
    return [[Interval.from_value(x) for x in row] for row in a]

Other public import paths

• omnibias.core.verified.to_interval_matrix
• omnibias.core.verified.linalg.to_interval_matrix

← Package overviewRunnable learning examples →