API REFERENCE/omnibias-core

omnibias.core.verified.eig_operator

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

Module contract & mathematical conventions

Certified eigenvalue **lower** bounds at the bottom of the spectrum.

omnibias.core.verified.eig certifies the *top* of the spectrum (Rayleigh quotients, Perron / power-sum gaps for transfer matrices). This module does the genuinely hard direction -- rigorous **lower** bounds on the lowest eigenvalues of a self-adjoint operator bounded below -- via the classical **Temple -> Lehmann-Maehly -> Goerisch** ladder, plus the finite-section machinery that turns a truncated (Galerkin) problem into a statement about the true operator.

The cast (all in outward-rounded interval arithmetic):

• temple_lower_bound -- Temple's inequality, the one-vector base case: with Rayleigh quotient theta = <Au,u>/<u,u>, second moment eta = ||Au||^2/<u,u> and an a-priori rho <= lambda_2,

.. math:: \lambda_1 \ge \theta - \frac{\eta - \theta^2}{\rho - \theta}.

• interval_ldlt_inertia -- certified inertia of a symmetric interval matrix by an interval LDL^T factorisation (every pivot sign-definite => Sylvester's law fixes the inertia of the whole matrix box).
• count_eigenvalues_below -- the number of generalized eigenvalues of the pencil (a, M) below t equals the negative inertia of a - t M (M SPD); the rigorous spectral counter that drives the bisection.
• generalized_eigenvalue_enclosure -- enclose the i-th smallest generalized eigenvalue of a symmetric-definite pencil by inertia bisection.
• lehmann_maehly_lower_bounds -- the Lehmann-Maehly-Goerisch theorem: with a = A_1 - rho A_0 and M = A_2 - 2 rho A_1 + rho^2 A_0 (the Gram matrices A_0=<w_i,w_j>, A_1=<Aw_i,w_j>, A_2=<Aw_i,Aw_j>), the negative generalized eigenvalues tau_1<=...<=tau_p<0 give lambda_{N-i+1} >= rho + 1/tau_i where N is the (a-priori) number of eigenvalues at or below rho. Goerisch's choice A_2=<Aw_i,Aw_j> computed with the *exact* operator captures the discarded-subspace tail, so the bound is valid for the true (possibly infinite-dimensional) operator, not just the finite section.
• operator_comparison_bounds -- Weyl monotonicity a-priori brackets for H = H_0 + V from a known base spectrum and min V <= V <= max V; this is how one obtains the a-priori rho (a certified lower bound on lambda_{N+1}) that the Lehmann labelling requires.
• certified_spectral_gap -- combine a Rayleigh-Ritz **upper** bound on lambda_1 with the Lehmann **lower** bound on lambda_2 into a certified positive gap lambda_2 - lambda_1.

Every statement is a **fixed-operator** result; nothing here makes a continuum or limit claim.

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 →

CLASS

EigenvalueLowerBound

omnibias.core.verified.EigenvalueLowerBoundSource ↗

class EigenvalueLowerBound

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.

One certified lambda_index >= lower_bound from the Lehmann pencil.

Parameters

Name	Type & default	Contract
indexdataclass field	intRequired	See the operation contract and implementation below.
lower_bounddataclass field	floatRequired	See the operation contract and implementation below.
tau_upperdataclass field	floatRequired	See the operation contract and implementation below.
rhodataclass field	floatRequired	See the operation contract and implementation below.

Fields & methods

indexfield

index: int

Declared int field on EigenvalueLowerBound. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

lower_boundfield

lower_bound: float

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

View source ↗

tau_upperfield

tau_upper: float

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

View source ↗

rhofield

rho: float

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

View source ↗

Read the implementation

class EigenvalueLowerBound:
    """One certified ``lambda_index >= lower_bound`` from the Lehmann pencil."""

    index: int
    lower_bound: float
    tau_upper: float
    rho: float

Other public import paths

• omnibias.core.verified.EigenvalueLowerBound
• omnibias.core.verified.eig_operator.EigenvalueLowerBound

CLASS

Inertia

omnibias.core.verified.InertiaSource ↗

class Inertia

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.

Certified signature of a symmetric interval matrix (counts must sum to n).

Parameters

Name	Type & default	Contract
negativedataclass field	intRequired	See the operation contract and implementation below.
positivedataclass field	intRequired	See the operation contract and implementation below.
pivotsdataclass field	tuple[float, ...]Required	See the operation contract and implementation below.

Fields & methods

negativefield

negative: int

Declared int field on Inertia. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

positivefield

positive: int

Declared int field on Inertia. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

pivotsfield

pivots: tuple[float, ...]

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

View source ↗

Read the implementation

class Inertia:
    """Certified signature of a symmetric interval matrix (counts must sum to ``n``)."""

    negative: int
    positive: int
    pivots: tuple[float, ...]

Other public import paths

• omnibias.core.verified.Inertia
• omnibias.core.verified.eig_operator.Inertia

CLASS

LehmannCertificate

omnibias.core.verified.LehmannCertificateSource ↗

class LehmannCertificate

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.

Lehmann-Maehly-Goerisch certified lower bounds for the lowest eigenvalues.

Parameters

Name	Type & default	Contract
rhodataclass field	floatRequired	See the operation contract and implementation below.
n_belowdataclass field	intRequired	See the operation contract and implementation below.
negativesdataclass field	intRequired	See the operation contract and implementation below.
m_positive_definitedataclass field	boolRequired	See the operation contract and implementation below.
inertia_certifieddataclass field	boolRequired	See the operation contract and implementation below.
boundsdataclass field	tuple[EigenvalueLowerBound, ...]Required	See the operation contract and implementation below.

Fields & methods

rhofield

rho: float

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

View source ↗

n_belowfield

n_below: int

Declared int field on LehmannCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

negativesfield

negatives: int

Declared int field on LehmannCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

m_positive_definitefield

m_positive_definite: bool

Declared bool field on LehmannCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

inertia_certifiedfield

inertia_certified: bool

Declared bool field on LehmannCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

boundsfield

bounds: tuple[EigenvalueLowerBound, ...]

Declared tuple[EigenvalueLowerBound, ...] field on LehmannCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

Read the implementation

class LehmannCertificate:
    """Lehmann-Maehly-Goerisch certified lower bounds for the lowest eigenvalues."""

    rho: float
    n_below: int
    negatives: int
    m_positive_definite: bool
    inertia_certified: bool
    bounds: tuple[EigenvalueLowerBound, ...]

Other public import paths

• omnibias.core.verified.LehmannCertificate
• omnibias.core.verified.eig_operator.LehmannCertificate

CLASS

SpectralGapCertificate

omnibias.core.verified.SpectralGapCertificateSource ↗

class SpectralGapCertificate

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.

Certified lambda_2 - lambda_1 for the bottom of a self-adjoint spectrum.

Parameters

Name	Type & default	Contract
lambda1_upperdataclass field	floatRequired	See the operation contract and implementation below.
lambda2_lowerdataclass field	floatRequired	See the operation contract and implementation below.
gap_lowerdataclass field	floatRequired	See the operation contract and implementation below.
rhodataclass field	floatRequired	See the operation contract and implementation below.
certifieddataclass field	boolRequired	See the operation contract and implementation below.

Fields & methods

lambda1_upperfield

lambda1_upper: float

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

View source ↗

lambda2_lowerfield

lambda2_lower: float

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

View source ↗

gap_lowerfield

gap_lower: float

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

View source ↗

rhofield

rho: float

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

View source ↗

certifiedfield

certified: bool

Declared bool field on SpectralGapCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

Read the implementation

class SpectralGapCertificate:
    """Certified ``lambda_2 - lambda_1`` for the bottom of a self-adjoint spectrum."""

    lambda1_upper: float
    lambda2_lower: float
    gap_lower: float
    rho: float
    certified: bool

Other public import paths

• omnibias.core.verified.SpectralGapCertificate
• omnibias.core.verified.eig_operator.SpectralGapCertificate

FUNCTION

certified_spectral_gap

omnibias.core.verified.certified_spectral_gapSource ↗

certified_spectral_gap(a0: Matrix, a1: Matrix, a2: Matrix, rho: float, lambda1_upper: float) -> SpectralGapCertificate

Certified positive gap lambda_2 - lambda_1 from a Ritz upper + Lehmann lower bound.

lambda1_upper is any rigorous upper bound on lambda_1 (e.g. a Rayleigh-Ritz value); the Lehmann lower bound on lambda_2 is computed from the pencil with n_below = 2. gap_lower = lambda2_lower - lambda1_upper is a certified lower bound on the true gap (<= lambda_2 - lambda_1); certified is True only when it is positive.

Parameters

Name	Type & default	Contract
a0positional-or-keyword	MatrixRequired	See the operation contract and implementation below.
a1positional-or-keyword	MatrixRequired	See the operation contract and implementation below.
a2positional-or-keyword	MatrixRequired	See the operation contract and implementation below.
rhopositional-or-keyword	floatRequired	See the operation contract and implementation below.
lambda1_upperpositional-or-keyword	floatRequired	See the operation contract and implementation below.

ReturnsSpectralGapCertificate

Executed regression · certified spectral gap schrodinger

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_spectral_gap_schrodinger() -> None:
    n = 40

    def potential(x: float) -> float:
        return 25.0 * (x - 0.5) ** 2

    a, _ = _schrodinger(n, potential)
    evals = _eigvals_sym(a)
    _, modes = _laplacian_modes(n)
    trial = [modes[0], modes[1]]
    a0, a1, a2 = _gram_matrices(a, trial)
    rho = 0.5 * (evals[1] + evals[2])
    # Rigorous upper bound on lambda_1 from the ground-mode Rayleigh quotient.
    lam1_up = ritz_upper_bound(a, modes[0]).hi
    assert lam1_up >= evals[0] - 1e-9
    cert = certified_spectral_gap(a0, a1, a2, rho, lam1_up)
    assert cert.certified
    true_gap = evals[1] - evals[0]
    assert 0.0 < cert.gap_lower <= true_gap + 1e-9
    assert cert.gap_lower > 0.5 * true_gap  # meaningfully tight

python -m pytest "packages/omnibias-core/tests/verified/test_eig_operator.py::test_certified_spectral_gap_schrodinger" -q

Regression example · lehmann reports failure without crashing

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_lehmann_reports_failure_without_crashing() -> None:
    # rho far below the spectrum -> no negative pencil eigenvalues -> empty bounds.
    a = [[2.0, 0.0], [0.0, 3.0]]
    cols = [[1.0, 0.0], [0.0, 1.0]]
    a0, a1, a2 = _gram_matrices(a, cols)
    cert = lehmann_maehly_lower_bounds(a0, a1, a2, rho=-10.0, n_below=0)
    assert cert.negatives == 0
    assert cert.bounds == ()

python -m pytest packages/omnibias-core/tests/verified/test_eig_operator.py -k test_lehmann_reports_failure_without_crashing -q

Read the implementation

def certified_spectral_gap(
    a0: Matrix,
    a1: Matrix,
    a2: Matrix,
    rho: float,
    lambda1_upper: float,
) -> SpectralGapCertificate:
    r"""Certified positive gap ``lambda_2 - lambda_1`` from a Ritz upper + Lehmann lower bound.

    ``lambda1_upper`` is any rigorous upper bound on ``lambda_1`` (e.g. a
    Rayleigh-Ritz value); the Lehmann lower bound on ``lambda_2`` is computed from
    the pencil with ``n_below = 2``.  ``gap_lower = lambda2_lower - lambda1_upper``
    is a certified lower bound on the true gap (``<= lambda_2 - lambda_1``);
    ``certified`` is ``True`` only when it is positive.
    """
    cert = lehmann_maehly_lower_bounds(a0, a1, a2, rho, n_below=2)
    lam2 = next((b.lower_bound for b in cert.bounds if b.index == 2), None)
    lam1_up = float(lambda1_upper)
    if lam2 is None:
        return SpectralGapCertificate(lam1_up, -inf, -inf, float(rho), False)
    gap = (Interval.point(lam2) - Interval.point(lam1_up)).lo
    return SpectralGapCertificate(lam1_up, lam2, gap, float(rho), gap > 0.0)

Related APIsomnibias.core.verified.SpectralGapCertificate↗omnibias.core.verified.lehmann_maehly_lower_bounds↗

Other public import paths

• omnibias.core.verified.certified_spectral_gap
• omnibias.core.verified.eig_operator.certified_spectral_gap

FUNCTION

count_eigenvalues_below

omnibias.core.verified.count_eigenvalues_belowSource ↗

count_eigenvalues_below(a: Matrix, m: Matrix, t: float) -> int | None

Number of generalized eigenvalues of (a, m) strictly below t.

For symmetric a and SPD m the matrix a - t m is congruent to diag(tau_i - t), so its negative inertia counts #{tau_i < t}. Returns None when the count cannot be certified (a pivot straddles 0, i.e. t is essentially on the spectrum).

Parameters

Name	Type & default	Contract
apositional-or-keyword	MatrixRequired	See the operation contract and implementation below.
mpositional-or-keyword	MatrixRequired	See the operation contract and implementation below.
tpositional-or-keyword	floatRequired	See the operation contract and implementation below.

Returnsint | None

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 · count eigenvalues below standard

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_count_eigenvalues_below_standard() -> None:
    a = [[2.0, 1.0, 0.0], [1.0, 2.0, 1.0], [0.0, 1.0, 2.0]]
    ident = [[1.0 if i == j else 0.0 for j in range(3)] for i in range(3)]
    evals = _eigvals_sym(a)
    for t in (-1.0, evals[0] + 1e-6, 0.5 * (evals[0] + evals[1]), evals[2] + 1.0):
        expected = sum(1 for e in evals if e < t)
        assert count_eigenvalues_below(a, ident, t) == expected

python -m pytest packages/omnibias-core/tests/verified/test_eig_operator.py -k test_count_eigenvalues_below_standard -q

Read the implementation

def count_eigenvalues_below(a: Matrix, m: Matrix, t: float) -> int | None:
    r"""Number of generalized eigenvalues of ``(a, m)`` strictly below ``t``.

    For symmetric ``a`` and SPD ``m`` the matrix ``a - t m`` is congruent to
    ``diag(tau_i - t)``, so its negative inertia counts ``#{tau_i < t}``.  Returns
    ``None`` when the count cannot be certified (a pivot straddles ``0``, i.e.
    ``t`` is essentially on the spectrum).
    """
    ai = _to_sym_matrix(a)
    mi = _to_sym_matrix(m)
    inertia = interval_ldlt_inertia(_pencil_shift(ai, mi, t))
    return None if inertia is None else inertia.negative

Related APIsomnibias.core.verified.interval_ldlt_inertia↗

Other public import paths

• omnibias.core.verified.count_eigenvalues_below
• omnibias.core.verified.eig_operator.count_eigenvalues_below

FUNCTION

generalized_eigenvalue_enclosure

omnibias.core.verified.generalized_eigenvalue_enclosureSource ↗

generalized_eigenvalue_enclosure(a: Matrix, m: Matrix, index: int, *, bracket: tuple[float, float] | None=None, iters: int=200) -> Interval

Enclose the index-th smallest (1-based) generalized eigenvalue of (a, m).

m must be certified SPD. Two inertia bisections (one for each endpoint) sandwich tau_index: the lower endpoint is the greatest certified t with count_below(t) < index and the upper endpoint the least certified t with count_below(t) >= index. Rigorous for any symmetric-definite pencil.

Parameters

Name	Type & default	Contract
apositional-or-keyword	MatrixRequired	See the operation contract and implementation below.
mpositional-or-keyword	MatrixRequired	See the operation contract and implementation below.
indexpositional-or-keyword	intRequired	See the operation contract and implementation below.
bracketkeyword-only	tuple[float, float] | NoneDefault: None	See the operation contract and implementation below.
iterskeyword-only	intDefault: 200	See the operation contract and implementation below.

ReturnsInterval

Explicit validation & failure cases

• When not 1 <= index <= n, raises ValueError(f'index must be in 1..{n}, got {index}').
• When not is_positive_definite(mi), raises ValueError('right matrix m must be certified positive definite').

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

Regression example · generalized eigenvalue enclosure rejects indefinite m

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_generalized_eigenvalue_enclosure_rejects_indefinite_m() -> None:
    a = [[1.0, 0.0], [0.0, 1.0]]
    m = [[1.0, 2.0], [2.0, 1.0]]  # indefinite
    with pytest.raises(ValueError, match="positive definite"):
        generalized_eigenvalue_enclosure(a, m, 1)

python -m pytest packages/omnibias-core/tests/verified/test_eig_operator.py -k test_generalized_eigenvalue_enclosure_rejects_indefinite_m -q

Read the implementation

def generalized_eigenvalue_enclosure(
    a: Matrix, m: Matrix, index: int, *, bracket: tuple[float, float] | None = None, iters: int = 200
) -> Interval:
    r"""Enclose the ``index``-th smallest (1-based) generalized eigenvalue of ``(a, m)``.

    ``m`` must be certified SPD.  Two inertia bisections (one for each endpoint)
    sandwich ``tau_index``: the lower endpoint is the greatest certified ``t`` with
    ``count_below(t) < index`` and the upper endpoint the least certified ``t``
    with ``count_below(t) >= index``.  Rigorous for any symmetric-definite pencil.
    """
    ai = _to_sym_matrix(a)
    mi = _to_sym_matrix(m)
    n = len(ai)
    if not 1 <= index <= n:
        raise ValueError(f"index must be in 1..{n}, got {index}")
    if not is_positive_definite(mi):
        raise ValueError("right matrix m must be certified positive definite")
    if bracket is None:
        b = _spectral_bracket(ai, mi)
        lo0, hi0 = -b, b
    else:
        lo0, hi0 = bracket
    return Interval(
        _bisect_endpoint(ai, mi, index, lo0, hi0, iters, want_upper=False),
        _bisect_endpoint(ai, mi, index, lo0, hi0, iters, want_upper=True),
    )

Related APIsomnibias.core.verified.is_positive_definite↗omnibias.core.verified.Interval↗

Other public import paths

• omnibias.core.verified.generalized_eigenvalue_enclosure
• omnibias.core.verified.eig_operator.generalized_eigenvalue_enclosure

FUNCTION

interval_ldlt_factor

omnibias.core.verified.interval_ldlt_factorSource ↗

interval_ldlt_factor(matrix: Matrix) -> tuple[tuple[tuple[Interval, ...], ...], tuple[Interval, ...]] | None

Return the interval unit-lower L and diagonal D of LDL^T.

The factorization is available only when every interval pivot excludes zero. Each returned entry encloses the corresponding factor of every point matrix in the input box. It therefore composes with interval triangular solves to enclose solutions of symmetric linear systems.

Parameters

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

Returnstuple[tuple[tuple[Interval, ...], ...], tuple[Interval, ...]] | None

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 solve symmetric ldlt 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_symmetric_ldlt_encloses_grid_and_random_systems() -> None:
    """The exposed LDLT factors and triangular route enclose an SPD matrix box."""
    diagonal_lo = np.asarray([3.8, 2.9])
    diagonal_hi = np.asarray([4.2, 3.3])
    off_lo, off_hi = -0.3, -0.1
    rhs_lo = np.asarray([-1.0, 0.4])
    rhs_hi = np.asarray([-0.6, 0.8])
    matrix = [
        [Interval(float(diagonal_lo[0]), float(diagonal_hi[0])), Interval(off_lo, off_hi)],
        [Interval(off_lo, off_hi), Interval(float(diagonal_lo[1]), float(diagonal_hi[1]))],
    ]
    rhs = [Interval(float(rhs_lo[i]), float(rhs_hi[i])) for i in range(2)]
    factor = interval_ldlt_factor(matrix)
    assert factor is not None
    lower, diagonal = factor
    assert all(lower[i][i] == Interval.point(1.0) for i in range(2))
    assert all(not pivot.contains_zero() for pivot in diagonal)
    solution = interval_solve(matrix, rhs, symmetric=True)

    for fraction in np.linspace(0.0, 1.0, 17):
        diagonal_sample = _sample(diagonal_lo, diagonal_hi, float(fraction))
        rhs_sample = _sample(rhs_lo, rhs_hi, float(1.0 - fraction))
        matrix_sample = np.asarray(
            [
                [diagonal_sample[0], off_lo + fraction * (off_hi - off_lo)],
                [off_lo + fraction * (off_hi - off_lo), diagonal_sample[1]],
            ]
        )
        _assert_contains(solution, np.linalg.solve(matrix_sample, rhs_sample))

    rng = np.random.default_rng(20260827)
    for _ in range(128):
        diagonal_sample = rng.uniform(diagonal_lo, diagonal_hi)
        off_diagonal = rng.uniform(off_lo, off_hi)
        matrix_sample = np.asarray(
            [[diagonal_sample[0], off_diagonal], [off_diagonal, diagonal_sample[1]]]
        )
        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_symmetric_ldlt_encloses_grid_and_random_systems -q

Read the implementation

def interval_ldlt_factor(
    matrix: Matrix,
) -> tuple[tuple[tuple[Interval, ...], ...], tuple[Interval, ...]] | None:
    r"""Return the interval unit-lower ``L`` and diagonal ``D`` of ``LDL^T``.

    The factorization is available only when every interval pivot excludes zero.
    Each returned entry encloses the corresponding factor of every point matrix
    in the input box.  It therefore composes with interval triangular solves to
    enclose solutions of symmetric linear systems.
    """
    factor = _ldlt_pivots(_to_sym_matrix(matrix))
    if factor is None:
        return None
    lower, diagonal = factor
    return tuple(tuple(row) for row in lower), tuple(diagonal)

Other public import paths

• omnibias.core.verified.interval_ldlt_factor
• omnibias.core.verified.eig_operator.interval_ldlt_factor

FUNCTION

interval_ldlt_inertia

omnibias.core.verified.interval_ldlt_inertiaSource ↗

interval_ldlt_inertia(matrix: Matrix) -> Inertia | None

Certified inertia of a symmetric interval matrix via interval LDL^T.

Returns None when a pivot interval straddles 0 (the sign -- hence the inertia -- cannot be certified for the whole matrix box; t is too close to an eigenvalue). Otherwise every point matrix in the box shares the returned inertia, because each interval pivot contains the corresponding exact pivot (inclusion-isotone arithmetic) and S = L D L^T is a congruence (Sylvester's law of inertia).

Parameters

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

ReturnsInertia | None

Executed regression · is positive definite

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_is_positive_definite() -> None:
    assert is_positive_definite([[2.0, 1.0], [1.0, 2.0]])
    assert not is_positive_definite([[1.0, 2.0], [2.0, 1.0]])

python -m pytest "packages/omnibias-core/tests/verified/test_eig_operator.py::test_is_positive_definite" -q

Regression example · inertia returns none when 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_inertia_returns_none_when_singular() -> None:
    # eigenvalue exactly 0 -> a pivot straddles 0 -> cannot certify the sign.
    assert interval_ldlt_inertia([[1.0, 1.0], [1.0, 1.0]]) is None

python -m pytest packages/omnibias-core/tests/verified/test_eig_operator.py -k test_inertia_returns_none_when_singular -q

Read the implementation

def interval_ldlt_inertia(matrix: Matrix) -> Inertia | None:
    r"""Certified inertia of a symmetric interval matrix via interval ``LDL^T``.

    Returns ``None`` when a pivot interval straddles ``0`` (the sign -- hence the
    inertia -- cannot be certified for the whole matrix box; ``t`` is too close to
    an eigenvalue).  Otherwise every point matrix in the box shares the returned
    inertia, because each interval pivot contains the corresponding exact pivot
    (inclusion-isotone arithmetic) and ``S = L D L^T`` is a congruence
    (Sylvester's law of inertia).
    """
    factor = _ldlt_pivots(_to_sym_matrix(matrix))
    if factor is None:
        return None
    _, d = factor
    neg = sum(1 for dj in d if dj.hi < 0.0)
    return Inertia(negative=neg, positive=len(d) - neg, pivots=tuple(x.mid for x in d))

Related APIsomnibias.core.verified.Inertia↗

Other public import paths

• omnibias.core.verified.interval_ldlt_inertia
• omnibias.core.verified.eig_operator.interval_ldlt_inertia

FUNCTION

interval_ldlt_pivots

omnibias.core.verified.interval_ldlt_pivotsSource ↗

interval_ldlt_pivots(matrix: Matrix) -> tuple[Interval, ...] | None

Certified interval LDL^T pivots of a symmetric interval matrix (or None).

The finer-grained companion of interval_ldlt_inertia: instead of only the *counts* of positive / negative pivots it returns each pivot **interval** D_jj in order. A matrix box is certified positive definite exactly when the result is not None and every returned pivot has .lo > 0 -- the full inertia vector that the Lean kernel's allPivotsPos obligation re-checks (lifting the positive-definiteness claim above its single scalar eig_min shadow). Returns None when a pivot straddles 0.

Parameters

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

Returnstuple[Interval, ...] | None

Executed regression · is sos helper agrees

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_is_sos_helper_agrees() -> None:
    assert is_sos(X * X - X * Y + Y * Y + ONE)
    assert not is_sos(Polynomial(2, {(4, 2): 1.0, (2, 4): 1.0, (2, 2): -3.0, (0, 0): 1.0}))

python -m pytest "packages/omnibias-sos/tests/test_certify.py::test_is_sos_helper_agrees" -q

Regression example · record ldlt diagonal trace is independent of eig operator

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_record_ldlt_diagonal_trace_is_independent_of_eig_operator() -> None:
    """Calling the instrumented recorder never touches, imports as a side
    effect, or otherwise perturbs ``eig_operator`` -- an uninstrumented call
    before and after recording returns the identical result."""
    before = interval_ldlt_pivots(_SPD_2X2)
    record_ldlt_diagonal_trace(_SPD_2X2)
    after = interval_ldlt_pivots(_SPD_2X2)
    assert before == after

python -m pytest packages/omnibias-core/tests/test_replay.py -k test_record_ldlt_diagonal_trace_is_independent_of_eig_operator -q

Read the implementation

def interval_ldlt_pivots(matrix: Matrix) -> tuple[Interval, ...] | None:
    r"""Certified interval ``LDL^T`` pivots of a symmetric interval matrix (or ``None``).

    The finer-grained companion of :func:`interval_ldlt_inertia`: instead of only
    the *counts* of positive / negative pivots it returns each pivot **interval**
    ``D_jj`` in order.  A matrix box is certified positive definite exactly when the
    result is not ``None`` and every returned pivot has ``.lo > 0`` -- the full
    inertia vector that the Lean kernel's ``allPivotsPos`` obligation re-checks
    (lifting the positive-definiteness claim above its single scalar ``eig_min``
    shadow).  Returns ``None`` when a pivot straddles ``0``.
    """
    factor = _ldlt_pivots(_to_sym_matrix(matrix))
    return None if factor is None else tuple(factor[1])

Other public import paths

• omnibias.core.verified.interval_ldlt_pivots
• omnibias.core.verified.eig_operator.interval_ldlt_pivots

FUNCTION

is_positive_definite

omnibias.core.verified.is_positive_definiteSource ↗

is_positive_definite(matrix: Matrix) -> bool

True iff a symmetric interval matrix is *certified* positive definite.

Parameters

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

Returnsbool

Executed regression · is positive definite

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_is_positive_definite() -> None:
    assert is_positive_definite([[2.0, 1.0], [1.0, 2.0]])
    assert not is_positive_definite([[1.0, 2.0], [2.0, 1.0]])

python -m pytest "packages/omnibias-core/tests/verified/test_eig_operator.py::test_is_positive_definite" -q

Regression example · generalized eigenvalue enclosure pencil

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_generalized_eigenvalue_enclosure_pencil() -> None:
    a = [[3.0, 0.5, 0.1], [0.5, 2.0, 0.3], [0.1, 0.3, 1.0]]
    m = [[2.0, 0.2, 0.0], [0.2, 1.5, 0.1], [0.0, 0.1, 1.0]]
    assert is_positive_definite(m)
    taus = _gen_eigvals(a, m)
    for idx in (1, 2, 3):
        enc = generalized_eigenvalue_enclosure(a, m, idx)
        assert enc.lo <= taus[idx - 1] <= enc.hi

python -m pytest packages/omnibias-core/tests/verified/test_eig_operator.py -k test_generalized_eigenvalue_enclosure_pencil -q

Read the implementation

def is_positive_definite(matrix: Matrix) -> bool:
    """``True`` iff a symmetric interval matrix is *certified* positive definite."""
    inertia = interval_ldlt_inertia(matrix)
    return inertia is not None and inertia.negative == 0

Related APIsomnibias.core.verified.interval_ldlt_inertia↗

Other public import paths

• omnibias.core.verified.is_positive_definite
• omnibias.core.verified.eig_operator.is_positive_definite

FUNCTION

lehmann_maehly_lower_bounds

omnibias.core.verified.lehmann_maehly_lower_boundsSource ↗

lehmann_maehly_lower_bounds(a0: Matrix, a1: Matrix, a2: Matrix, rho: float, *, n_below: int) -> LehmannCertificate

Certified lower bounds on the lowest eigenvalues (Lehmann-Maehly-Goerisch).

Parameters

a0, a1, a2: The Gram matrices A_0=<w_i,w_j>, A_1=<Aw_i,w_j>, A_2=<Aw_i,Aw_j> over the trial vectors w_i (A_2 evaluated with the *exact* operator -- Goerisch -- so the discarded-subspace tail is included). rho: An a-priori value with lambda_{n_below} <= rho <= lambda_{n_below+1} (typically from operator_comparison_bounds). The *labelling* of the bounds relies on this hypothesis; the inequalities themselves are certified. n_below: N: the number of eigenvalues at or below rho.

Returns a LehmannCertificate; bounds[k] carries lambda_{N-k+1} >= rho + 1/tau_{k+1}. Empty bounds (with the flags showing why) when M is not certified SPD or the pencil's inertia cannot be certified.

Parameters

Name	Type & default	Contract
a0positional-or-keyword	MatrixRequired	The Gram matrices A_0=<w_i,w_j>, A_1=<Aw_i,w_j>, A_2=<Aw_i,Aw_j> over the trial vectors w_i (A_2 evaluated with the *exact* operator -- Goerisch -- so the discarded-subspace tail is included).
a1positional-or-keyword	MatrixRequired	See the operation contract and implementation below.
a2positional-or-keyword	MatrixRequired	See the operation contract and implementation below.
rhopositional-or-keyword	floatRequired	An a-priori value with lambda_{n_below} <= rho <= lambda_{n_below+1} (typically from operator_comparison_bounds). The *labelling* of the bounds relies on this hypothesis; the inequalities themselves are certified.
n_belowkeyword-only	intRequired	N: the number of eigenvalues at or below rho.

ReturnsLehmannCertificate

Executed regression · lehmann reports failure without crashing

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_lehmann_reports_failure_without_crashing() -> None:
    # rho far below the spectrum -> no negative pencil eigenvalues -> empty bounds.
    a = [[2.0, 0.0], [0.0, 3.0]]
    cols = [[1.0, 0.0], [0.0, 1.0]]
    a0, a1, a2 = _gram_matrices(a, cols)
    cert = lehmann_maehly_lower_bounds(a0, a1, a2, rho=-10.0, n_below=0)
    assert cert.negatives == 0
    assert cert.bounds == ()

python -m pytest "packages/omnibias-core/tests/verified/test_eig_operator.py::test_lehmann_reports_failure_without_crashing" -q

Regression example · lehmann exact on full space

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_lehmann_exact_on_full_space() -> None:
    # Full trial space (W = I): A0=I, A1=A, A2=A^2 -> Lehmann recovers eigenvalues.
    a = [[2.0, -1.0, 0.0], [-1.0, 2.0, -1.0], [0.0, -1.0, 2.0]]
    evals = _eigvals_sym(a)
    cols = [[1.0 if i == j else 0.0 for i in range(3)] for j in range(3)]
    a0, a1, a2 = _gram_matrices(a, cols)
    rho = evals[2] + 1.0  # above all 3 eigenvalues -> N = 3 below rho
    cert = lehmann_maehly_lower_bounds(a0, a1, a2, rho, n_below=3)
    assert cert.m_positive_definite and cert.inertia_certified
    assert cert.negatives == 3
    by_index = {b.index: b.lower_bound for b in cert.bounds}
    for k in (1, 2, 3):
        assert by_index[k] <= evals[k - 1] + 1e-9
        assert abs(by_index[k] - evals[k - 1]) < 1e-6

python -m pytest packages/omnibias-core/tests/verified/test_eig_operator.py -k test_lehmann_exact_on_full_space -q

Read the implementation

def lehmann_maehly_lower_bounds(
    a0: Matrix, a1: Matrix, a2: Matrix, rho: float, *, n_below: int
) -> LehmannCertificate:
    r"""Certified lower bounds on the lowest eigenvalues (Lehmann-Maehly-Goerisch).

    Parameters
    ----------
    a0, a1, a2:
        The Gram matrices ``A_0=<w_i,w_j>``, ``A_1=<Aw_i,w_j>``,
        ``A_2=<Aw_i,Aw_j>`` over the trial vectors ``w_i`` (``A_2`` evaluated with
        the *exact* operator -- Goerisch -- so the discarded-subspace tail is
        included).
    rho:
        An a-priori value with ``lambda_{n_below} <= rho <= lambda_{n_below+1}``
        (typically from :func:`operator_comparison_bounds`).  The *labelling* of
        the bounds relies on this hypothesis; the inequalities themselves are
        certified.
    n_below:
        ``N``: the number of eigenvalues at or below ``rho``.

    Returns a :class:`LehmannCertificate`; ``bounds[k]`` carries
    ``lambda_{N-k+1} >= rho + 1/tau_{k+1}``.  Empty ``bounds`` (with the flags
    showing why) when ``M`` is not certified SPD or the pencil's inertia cannot be
    certified.
    """
    a0i, a1i, a2i = (to_interval_matrix(x) for x in (a0, a1, a2))
    rho_f = float(rho)
    a, m = _lehmann_matrices(a0i, a1i, a2i, rho_f)
    pd = is_positive_definite(m)
    inertia = interval_ldlt_inertia(a)
    if not pd or inertia is None:
        return LehmannCertificate(rho_f, int(n_below), 0, pd, inertia is not None, ())
    p = inertia.negative
    rho_iv = Interval.point(rho_f)
    bracket = (-_spectral_bracket(a, m), 0.0)
    bounds: list[EigenvalueLowerBound] = []
    for i in range(1, p + 1):
        tau_hi = _bisect_endpoint(a, m, i, bracket[0], bracket[1], 200, want_upper=True)
        if tau_hi >= 0.0:
            continue
        sigma = rho_iv + Interval.point(tau_hi).reciprocal()
        idx = n_below - i + 1
        if idx < 1:
            continue
        bounds.append(
            EigenvalueLowerBound(index=idx, lower_bound=sigma.lo, tau_upper=tau_hi, rho=rho_f)
        )
    bounds.sort(key=lambda b: b.index)
    return LehmannCertificate(rho_f, int(n_below), p, True, True, tuple(bounds))

Related APIsomnibias.core.verified.EigenvalueLowerBound↗omnibias.core.verified.LehmannCertificate↗omnibias.core.verified.interval_ldlt_inertia↗omnibias.core.verified.is_positive_definite↗omnibias.core.verified.to_interval_matrix↗

Other public import paths

• omnibias.core.verified.lehmann_maehly_lower_bounds
• omnibias.core.verified.eig_operator.lehmann_maehly_lower_bounds

FUNCTION

operator_comparison_bounds

omnibias.core.verified.operator_comparison_boundsSource ↗

operator_comparison_bounds(base_eigenvalues: Sequence[float], perturbation_lower: float, perturbation_upper: float) -> list[Interval]

Weyl monotonicity brackets for H = H_0 + V, min V <= V <= max V.

For self-adjoint H_0 with eigenvalues mu_k and a bounded symmetric perturbation V with min V <= V <= max V (as forms), Weyl's inequality gives mu_k + min V <= lambda_k(H) <= mu_k + max V. Each returned interval rigorously brackets lambda_k; used to place the Lehmann rho in a certified spectral gap.

Parameters

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

Returnslist[Interval]

Executed regression · operator comparison brackets contain truth

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_operator_comparison_brackets_contain_truth() -> None:
    n = 30

    def potential(x: float) -> float:
        return 12.0 * math.sin(math.pi * x)  # 0 <= V <= 12

    a, _ = _schrodinger(n, potential)
    base, _ = _laplacian_modes(n)
    evals = _eigvals_sym(a)
    brackets = operator_comparison_bounds(base, perturbation_lower=0.0, perturbation_upper=12.0)
    for k in range(n):
        assert brackets[k].lo <= evals[k] <= brackets[k].hi

python -m pytest "packages/omnibias-core/tests/verified/test_eig_operator.py::test_operator_comparison_brackets_contain_truth" -q

Read the implementation

def operator_comparison_bounds(
    base_eigenvalues: Sequence[float],
    perturbation_lower: float,
    perturbation_upper: float,
) -> list[Interval]:
    r"""Weyl monotonicity brackets for ``H = H_0 + V``, ``min V <= V <= max V``.

    For self-adjoint ``H_0`` with eigenvalues ``mu_k`` and a bounded symmetric
    perturbation ``V`` with ``min V <= V <= max V`` (as forms), Weyl's inequality
    gives ``mu_k + min V <= lambda_k(H) <= mu_k + max V``.  Each returned interval
    rigorously brackets ``lambda_k``; used to place the Lehmann ``rho`` in a
    certified spectral gap.
    """
    lo = Interval.point(float(perturbation_lower))
    hi = Interval.point(float(perturbation_upper))
    out: list[Interval] = []
    for mu in base_eigenvalues:
        mu_iv = Interval.point(float(mu))
        out.append(Interval((mu_iv + lo).lo, (mu_iv + hi).hi))
    return out

Related APIsomnibias.core.verified.Interval↗

Other public import paths

• omnibias.core.verified.operator_comparison_bounds
• omnibias.core.verified.eig_operator.operator_comparison_bounds

FUNCTION

ritz_upper_bound

omnibias.core.verified.ritz_upper_boundSource ↗

ritz_upper_bound(matrix: Matrix, vector: Vector) -> Interval

Rayleigh-quotient **upper** bound on lambda_1 (.hi is the bound).

Any Rayleigh quotient R(v) = v^T A v / v^T v satisfies R(v) >= lambda_1, so the upper endpoint of its enclosure is a certified upper bound on the smallest eigenvalue.

Parameters

Name	Type & default	Contract
matrixpositional-or-keyword	MatrixRequired	See the operation contract and implementation below.
vectorpositional-or-keyword	VectorRequired	See the operation contract and implementation below.

ReturnsInterval

Explicit validation & failure cases

• When len(v) != len(a), raises ValueError('vector length must match matrix dimension').
• When vv.lo <= 0.0, raises ValueError('vector must be nonzero').

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

Executed regression · certified spectral gap schrodinger

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_spectral_gap_schrodinger() -> None:
    n = 40

    def potential(x: float) -> float:
        return 25.0 * (x - 0.5) ** 2

    a, _ = _schrodinger(n, potential)
    evals = _eigvals_sym(a)
    _, modes = _laplacian_modes(n)
    trial = [modes[0], modes[1]]
    a0, a1, a2 = _gram_matrices(a, trial)
    rho = 0.5 * (evals[1] + evals[2])
    # Rigorous upper bound on lambda_1 from the ground-mode Rayleigh quotient.
    lam1_up = ritz_upper_bound(a, modes[0]).hi
    assert lam1_up >= evals[0] - 1e-9
    cert = certified_spectral_gap(a0, a1, a2, rho, lam1_up)
    assert cert.certified
    true_gap = evals[1] - evals[0]
    assert 0.0 < cert.gap_lower <= true_gap + 1e-9
    assert cert.gap_lower > 0.5 * true_gap  # meaningfully tight

python -m pytest "packages/omnibias-core/tests/verified/test_eig_operator.py::test_certified_spectral_gap_schrodinger" -q

Read the implementation

def ritz_upper_bound(matrix: Matrix, vector: Vector) -> Interval:
    r"""Rayleigh-quotient **upper** bound on ``lambda_1`` (``.hi`` is the bound).

    Any Rayleigh quotient ``R(v) = v^T A v / v^T v`` satisfies ``R(v) >= lambda_1``,
    so the upper endpoint of its enclosure is a certified upper bound on the
    smallest eigenvalue.
    """
    a = _to_sym_matrix(matrix)
    v = [Interval.from_value(x) for x in vector]
    if len(v) != len(a):
        raise ValueError("vector length must match matrix dimension")
    vv = _dot(v, v)
    if vv.lo <= 0.0:
        raise ValueError("vector must be nonzero")
    return _dot(v, _matvec_sym(a, v)) * vv.reciprocal()

Other public import paths

• omnibias.core.verified.ritz_upper_bound
• omnibias.core.verified.eig_operator.ritz_upper_bound

FUNCTION

temple_lower_bound

omnibias.core.verified.temple_lower_boundSource ↗

temple_lower_bound(rayleigh: IntervalLike, second_moment: IntervalLike, rho: float) -> Interval

Temple's lower bound on lambda_1 (its .lo is the certified bound).

rayleigh is theta = <Au,u>/<u,u> (so theta >= lambda_1), second_moment is eta = ||Au||^2/<u,u> (so eta >= theta^2), and rho must satisfy theta < rho <= lambda_2. Returns the enclosure of theta - (eta - theta^2)/(rho - theta); its lower endpoint underestimates the true Temple value, hence lambda_1.

Parameters

Name	Type & default	Contract
rayleighpositional-or-keyword	IntervalLikeRequired	See the operation contract and implementation below.
second_momentpositional-or-keyword	IntervalLikeRequired	See the operation contract and implementation below.
rhopositional-or-keyword	floatRequired	See the operation contract and implementation below.

ReturnsInterval

Explicit validation & failure cases

• When theta.hi >= rho_f, raises ValueError('Temple requires the Rayleigh quotient strictly below rho').

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

Executed regression · temple requires rayleigh below rho

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_temple_requires_rayleigh_below_rho() -> None:
    a = [[1.0, 0.0], [0.0, 5.0]]
    # vector biased to the large eigenvalue -> Rayleigh quotient above rho.
    with pytest.raises(ValueError, match="strictly below rho"):
        temple_lower_bound_vector(a, [0.1, 1.0], rho=2.0)

python -m pytest "packages/omnibias-core/tests/verified/test_eig_operator.py::test_temple_requires_rayleigh_below_rho" -q

Read the implementation

def temple_lower_bound(
    rayleigh: IntervalLike, second_moment: IntervalLike, rho: float
) -> Interval:
    r"""Temple's lower bound on ``lambda_1`` (its ``.lo`` is the certified bound).

    ``rayleigh`` is ``theta = <Au,u>/<u,u>`` (so ``theta >= lambda_1``),
    ``second_moment`` is ``eta = ||Au||^2/<u,u>`` (so ``eta >= theta^2``), and
    ``rho`` must satisfy ``theta < rho <= lambda_2``.  Returns the enclosure of
    ``theta - (eta - theta^2)/(rho - theta)``; its lower endpoint underestimates
    the true Temple value, hence ``lambda_1``.
    """
    theta = Interval.from_value(rayleigh)
    eta = Interval.from_value(second_moment)
    rho_f = float(rho)
    if theta.hi >= rho_f:
        raise ValueError("Temple requires the Rayleigh quotient strictly below rho")
    denom = Interval.point(rho_f) - theta  # > 0
    variance = eta - theta * theta  # >= 0
    return theta - variance * denom.reciprocal()

Other public import paths

• omnibias.core.verified.temple_lower_bound
• omnibias.core.verified.eig_operator.temple_lower_bound

FUNCTION

temple_lower_bound_vector

omnibias.core.verified.temple_lower_bound_vectorSource ↗

temple_lower_bound_vector(matrix: Matrix, vector: Vector, rho: float) -> Interval

Temple's bound from an explicit matrix A and (approx ground-state) vector.

Parameters

Name	Type & default	Contract
matrixpositional-or-keyword	MatrixRequired	See the operation contract and implementation below.
vectorpositional-or-keyword	VectorRequired	See the operation contract and implementation below.
rhopositional-or-keyword	floatRequired	See the operation contract and implementation below.

ReturnsInterval

Explicit validation & failure cases

• When len(v) != len(a), raises ValueError('vector length must match matrix dimension').
• When vv.lo <= 0.0, raises ValueError('vector must be nonzero').

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

Executed regression · temple requires rayleigh below rho

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_temple_requires_rayleigh_below_rho() -> None:
    a = [[1.0, 0.0], [0.0, 5.0]]
    # vector biased to the large eigenvalue -> Rayleigh quotient above rho.
    with pytest.raises(ValueError, match="strictly below rho"):
        temple_lower_bound_vector(a, [0.1, 1.0], rho=2.0)

python -m pytest "packages/omnibias-core/tests/verified/test_eig_operator.py::test_temple_requires_rayleigh_below_rho" -q

Regression example · temple recovers lambda1 tightly

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_temple_recovers_lambda1_tightly() -> None:
    a = [[2.0, -1.0, 0.0], [-1.0, 2.0, -1.0], [0.0, -1.0, 2.0]]
    evals = _eigvals_sym(a)
    lam1, lam2 = evals[0], evals[1]
    # Approximate ground eigenvector (smooth sine mode); rho strictly below lambda_2.
    u = [math.sin(i * math.pi / 4) for i in range(1, 4)]
    rho = 0.5 * (lam1 + lam2)
    bound = temple_lower_bound_vector(a, u, rho)
    assert bound.lo <= lam1 + 1e-12  # rigorous lower bound
    assert lam1 - bound.lo < 1e-2  # and tight

python -m pytest packages/omnibias-core/tests/verified/test_eig_operator.py -k test_temple_recovers_lambda1_tightly -q

Read the implementation

def temple_lower_bound_vector(matrix: Matrix, vector: Vector, rho: float) -> Interval:
    """Temple's bound from an explicit matrix ``A`` and (approx ground-state) vector."""
    a = _to_sym_matrix(matrix)
    v = [Interval.from_value(x) for x in vector]
    if len(v) != len(a):
        raise ValueError("vector length must match matrix dimension")
    vv = _dot(v, v)
    if vv.lo <= 0.0:
        raise ValueError("vector must be nonzero")
    inv = vv.reciprocal()
    av = _matvec_sym(a, v)
    theta = _dot(v, av) * inv
    eta = _dot(av, av) * inv
    return temple_lower_bound(theta, eta, rho)

Related APIsomnibias.core.verified.temple_lower_bound↗

Other public import paths

• omnibias.core.verified.temple_lower_bound_vector
• omnibias.core.verified.eig_operator.temple_lower_bound_vector

← Package overviewRunnable learning examples →