API REFERENCE/omnibias-core

omnibias.core.verified.eig

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

Module contract & mathematical conventions

Certified eigenvalue and spectral-gap enclosures -- the verified gap operator.

Three rigorous primitives that turn a (lattice transfer / Galerkin) matrix into a theorem-grade *spectral-gap* statement, all in outward-rounded interval arithmetic:

• rayleigh_quotient -- for a real symmetric A and test vector v, the quotient R(v) = vᵀAv / vᵀv obeys lambda_min <= R(v) <= lambda_max, so R(v).lo is a certified lower bound on the largest eigenvalue.
• symmetric_eigenvalue_residual_enclosure -- the symmetric residual (Bauer-Fike / Krylov-Bogoliubov) bound: with theta = R(v) and residual r = A v - theta v there is an eigenvalue of A within rho = ||r||_2 / ||v||_2 of theta; the returned interval encloses an actual eigenvalue.
• certified_perron_spectral_gap -- for an **entrywise-positive** matrix the Birkhoff-Hopf theorem bounds the subdominant eigenvalue ratio by the Hilbert projective contraction tau = (sqrt(kappa) - 1) / (sqrt(kappa) + 1) with kappa = max_{i,j,k,l} (a_ik a_jl) / (a_jk a_il). Hence |lambda_1| <= tau * lambda_0 and the (lattice-unit) mass gap obeys m a = -ln(lambda_1 / lambda_0) >= -ln(tau) > 0. The bound is *tight* for 2x2 positive matrices and conservative (an over-estimate of the ratio, hence a valid under-estimate of the gap) otherwise.

Every result is a **fixed-matrix** (fixed lattice spacing / finite volume) statement, never a continuum or asymptotic 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

BlockOperatorGapCertificate

omnibias.core.verified.BlockOperatorGapCertificateSource ↗

class BlockOperatorGapCertificate

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.

Finite-section + tail-defect coercivity bound for a self-adjoint operator.

For a self-adjoint operator S split by an orthogonal projection P (finite N-dimensional range) and Q = I - P into blocks

S = \begin{pmatrix} A & B \\ B^{\!*} & D \end{pmatrix},\qquad A = P S P,\ \ D = Q S Q,\ \ B = P S Q,

the Rayleigh quotient of any v = (p, q) obeys <Sv,v> >= a\|p\|^2 - 2b\|p\|\|q\| + d\|q\|^2 with a = \lambda_min(A), b >= \|B\|, d = \lambda_min(D); minimising the right-hand quadratic form over the unit circle gives the **certified** lower bound

\lambda_{\min}(S)\ \ge\ \tfrac12\Big[(a+d) - \sqrt{(a-d)^2 + 4b^2}\Big].

The finite gap a is computed here (Gershgorin) from the supplied finite block; the coupling bound b is supplied by the caller; the **tail gap d is an explicit hypothesis** -- it is *not* certified by this primitive (bounding the infinite tail is the hard analytic step). Coercivity (gap_lower > 0) holds iff a > 0 and d > threshold_tail_gap = b^2/a; that single scalar inequality is the isolated open obligation of a conditional coercivity / spectral-gap program (e.g. the linearised rescaled SQG operator in a weighted norm). This is a **fixed-finite-block** statement; it never claims the tail bound and never makes a continuum / blow-up / global-regularity claim.

Parameters

Name	Type & default	Contract
finite_dimdataclass field	intRequired	See the operation contract and implementation below.
finite_gap_lowerdataclass field	floatRequired	See the operation contract and implementation below.
coupling_norm_upperdataclass field	floatRequired	See the operation contract and implementation below.
tail_gap_lowerdataclass field	float | NoneRequired	See the operation contract and implementation below.
tail_is_hypothesisdataclass field	boolRequired	See the operation contract and implementation below.
gap_lowerdataclass field	float | NoneRequired	See the operation contract and implementation below.
coercivedataclass field	boolRequired	See the operation contract and implementation below.
threshold_tail_gapdataclass field	floatRequired	See the operation contract and implementation below.

Fields & methods

finite_dimfield

finite_dim: int

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

View source ↗

finite_gap_lowerfield

finite_gap_lower: float

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

View source ↗

coupling_norm_upperfield

coupling_norm_upper: float

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

View source ↗

tail_gap_lowerfield

tail_gap_lower: float | None

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

View source ↗

tail_is_hypothesisfield

tail_is_hypothesis: bool

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

View source ↗

gap_lowerfield

gap_lower: float | None

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

View source ↗

coercivefield

coercive: bool

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

View source ↗

threshold_tail_gapfield

threshold_tail_gap: float

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

View source ↗

Read the implementation

class BlockOperatorGapCertificate:
    r"""Finite-section + tail-defect coercivity bound for a self-adjoint operator.

    For a self-adjoint operator ``S`` split by an orthogonal projection ``P``
    (finite ``N``-dimensional range) and ``Q = I - P`` into blocks

    .. math::

        S = \begin{pmatrix} A & B \\ B^{\!*} & D \end{pmatrix},\qquad
        A = P S P,\ \ D = Q S Q,\ \ B = P S Q,

    the Rayleigh quotient of any ``v = (p, q)`` obeys
    ``<Sv,v> >= a\|p\|^2 - 2b\|p\|\|q\| + d\|q\|^2`` with ``a = \lambda_min(A)``,
    ``b >= \|B\|``, ``d = \lambda_min(D)``; minimising the right-hand quadratic form
    over the unit circle gives the **certified** lower bound

    .. math::

        \lambda_{\min}(S)\ \ge\
        \tfrac12\Big[(a+d) - \sqrt{(a-d)^2 + 4b^2}\Big].

    The finite gap ``a`` is computed here (Gershgorin) from the supplied finite
    block; the coupling bound ``b`` is supplied by the caller; the **tail gap
    ``d`` is an explicit hypothesis** -- it is *not* certified by this primitive
    (bounding the infinite tail is the hard analytic step).  Coercivity
    (``gap_lower > 0``) holds iff ``a > 0`` and ``d > threshold_tail_gap = b^2/a``;
    that single scalar inequality is the isolated open obligation of a conditional
    coercivity / spectral-gap program (e.g. the linearised rescaled SQG operator in
    a weighted norm).  This is a **fixed-finite-block** statement; it never claims
    the tail bound and never makes a continuum / blow-up / global-regularity claim.
    """

    finite_dim: int
    finite_gap_lower: float
    coupling_norm_upper: float
    tail_gap_lower: float | None
    tail_is_hypothesis: bool
    gap_lower: float | None
    coercive: bool
    threshold_tail_gap: float

Other public import paths

• omnibias.core.verified.BlockOperatorGapCertificate
• omnibias.core.verified.eig.BlockOperatorGapCertificate

CLASS

PerronGapCertificate

omnibias.core.verified.PerronGapCertificateSource ↗

class PerronGapCertificate

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.

Rigorous Birkhoff-Hopf spectral-gap data for an entrywise-positive matrix.

Parameters

Name	Type & default	Contract
dimensiondataclass field	intRequired	See the operation contract and implementation below.
min_entrydataclass field	floatRequired	See the operation contract and implementation below.
kappa_upperdataclass field	floatRequired	See the operation contract and implementation below.
subdominant_ratio_upperdataclass field	floatRequired	See the operation contract and implementation below.
spectral_gap_lowerdataclass field	floatRequired	See the operation contract and implementation below.
spectral_gap_lower_per_unitdataclass field	floatRequired	See the operation contract and implementation below.

Fields & methods

dimensionfield

dimension: int

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

View source ↗

min_entryfield

min_entry: float

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

View source ↗

kappa_upperfield

kappa_upper: float

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

View source ↗

subdominant_ratio_upperfield

subdominant_ratio_upper: float

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

View source ↗

spectral_gap_lowerfield

spectral_gap_lower: float

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

View source ↗

spectral_gap_lower_per_unitfield

spectral_gap_lower_per_unit: float

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

View source ↗

Read the implementation

class PerronGapCertificate:
    """Rigorous Birkhoff-Hopf spectral-gap data for an entrywise-positive matrix."""

    dimension: int
    min_entry: float
    kappa_upper: float
    subdominant_ratio_upper: float
    spectral_gap_lower: float
    spectral_gap_lower_per_unit: float

Other public import paths

• omnibias.core.verified.PerronGapCertificate
• omnibias.core.verified.eig.PerronGapCertificate

CLASS

SymmetricGapCertificate

omnibias.core.verified.SymmetricGapCertificateSource ↗

class SymmetricGapCertificate

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.

Rigorous spectral-gap data for a real *symmetric* matrix via power sums.

Tighter than PerronGapCertificate whenever the subdominant eigenvalue dominates the remaining spectral tail (e.g. heat-kernel transfer matrices, whose eigenvalues decay like e^{-t C2}).

Parameters

Name	Type & default	Contract
dimensiondataclass field	intRequired	See the operation contract and implementation below.
perron_lowerdataclass field	floatRequired	See the operation contract and implementation below.
subdominant_upperdataclass field	floatRequired	See the operation contract and implementation below.
subdominant_ratio_upperdataclass field	floatRequired	See the operation contract and implementation below.
spectral_gap_lowerdataclass field	floatRequired	See the operation contract and implementation below.
spectral_gap_lower_per_unitdataclass field	floatRequired	See the operation contract and implementation below.
partner_lowerdataclass field	floatDefault: 0.0	See the operation contract and implementation below.
partners_deflateddataclass field	intDefault: 0	See the operation contract and implementation below.
perron_upperdataclass field	floatDefault: inf	See the operation contract and implementation below.
subdominant_lowerdataclass field	floatDefault: 0.0	See the operation contract and implementation below.
spectral_gap_upperdataclass field	floatDefault: inf	See the operation contract and implementation below.
spectral_gap_upper_per_unitdataclass field	floatDefault: inf	See the operation contract and implementation below.

Fields & methods

dimensionfield

dimension: int

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

View source ↗

perron_lowerfield

perron_lower: float

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

View source ↗

subdominant_upperfield

subdominant_upper: float

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

View source ↗

subdominant_ratio_upperfield

subdominant_ratio_upper: float

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

View source ↗

spectral_gap_lowerfield

spectral_gap_lower: float

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

View source ↗

spectral_gap_lower_per_unitfield

spectral_gap_lower_per_unit: float

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

View source ↗

partner_lowerfield

partner_lower: float = 0.0

Declared float field on SymmetricGapCertificate. Default expression: 0.0.

View source ↗

partners_deflatedfield

partners_deflated: int = 0

number of partner eigenvalues whose certified lower bound was deflated

View source ↗

perron_upperfield

perron_upper: float = inf

Declared float field on SymmetricGapCertificate. Default expression: inf.

View source ↗

subdominant_lowerfield

subdominant_lower: float = 0.0

Declared float field on SymmetricGapCertificate. Default expression: 0.0.

View source ↗

spectral_gap_upperfield

spectral_gap_upper: float = inf

Declared float field on SymmetricGapCertificate. Default expression: inf.

View source ↗

spectral_gap_upper_per_unitfield

spectral_gap_upper_per_unit: float = inf

Declared float field on SymmetricGapCertificate. Default expression: inf.

View source ↗

Read the implementation

class SymmetricGapCertificate:
    """Rigorous spectral-gap data for a real *symmetric* matrix via power sums.

    Tighter than :class:`PerronGapCertificate` whenever the subdominant
    eigenvalue dominates the remaining spectral tail (e.g. heat-kernel transfer
    matrices, whose eigenvalues decay like ``e^{-t C2}``).
    """

    dimension: int
    perron_lower: float
    subdominant_upper: float
    subdominant_ratio_upper: float
    spectral_gap_lower: float
    spectral_gap_lower_per_unit: float
    partner_lower: float = 0.0
    # number of partner eigenvalues whose certified lower bound was deflated
    partners_deflated: int = 0
    perron_upper: float = inf
    subdominant_lower: float = 0.0
    spectral_gap_upper: float = inf
    spectral_gap_upper_per_unit: float = inf

Other public import paths

• omnibias.core.verified.SymmetricGapCertificate
• omnibias.core.verified.eig.SymmetricGapCertificate

FUNCTION

birkhoff_contraction_ratio

omnibias.core.verified.birkhoff_contraction_ratioSource ↗

birkhoff_contraction_ratio(matrix: Matrix) -> Interval

Enclosure of tau = (sqrt(kappa) - 1) / (sqrt(kappa) + 1) (in [0, 1)).

tau bounds the subdominant eigenvalue ratio: |lambda_1| <= tau lambda_0 for an entrywise-positive matrix. tau.hi is the certified upper bound.

Parameters

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

ReturnsInterval

Executed regression · birkhoff diameter and ratio enclosures

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_birkhoff_diameter_and_ratio_enclosures() -> None:
    kappa = birkhoff_projective_diameter(A2)
    assert kappa.lo <= 4.0 <= kappa.hi
    tau = birkhoff_contraction_ratio(A2)
    assert tau.lo <= (1.0 / 3.0) <= tau.hi

python -m pytest "packages/omnibias-core/tests/verified/test_eig.py::test_birkhoff_diameter_and_ratio_enclosures" -q

Read the implementation

def birkhoff_contraction_ratio(matrix: Matrix) -> Interval:
    r"""Enclosure of ``tau = (sqrt(kappa) - 1) / (sqrt(kappa) + 1)`` (in ``[0, 1)``).

    ``tau`` bounds the subdominant eigenvalue ratio: ``|lambda_1| <= tau lambda_0``
    for an entrywise-positive matrix.  ``tau.hi`` is the certified upper bound.
    """
    kappa = birkhoff_projective_diameter(matrix)
    root = kappa.sqrt()
    return (root - Interval.point(1.0)) * (root + Interval.point(1.0)).reciprocal()

Related APIsomnibias.core.verified.birkhoff_projective_diameter↗

Other public import paths

• omnibias.core.verified.birkhoff_contraction_ratio
• omnibias.core.verified.eig.birkhoff_contraction_ratio

FUNCTION

birkhoff_projective_diameter

omnibias.core.verified.birkhoff_projective_diameterSource ↗

birkhoff_projective_diameter(matrix: Matrix) -> Interval

Enclosure of kappa = max_{i,j,k,l} (a_ik a_jl) / (a_jk a_il) (>= 1).

Uses the column factorization kappa = max_{k,l} m(k,l) m(l,k) with m(k,l) = max_i a_ik / a_il (O(n^3)). Each ratio is enclosed; the maxima are taken endpoint-wise so the returned interval encloses the true kappa.

Parameters

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

ReturnsInterval

Executed regression · birkhoff diameter and ratio enclosures

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_birkhoff_diameter_and_ratio_enclosures() -> None:
    kappa = birkhoff_projective_diameter(A2)
    assert kappa.lo <= 4.0 <= kappa.hi
    tau = birkhoff_contraction_ratio(A2)
    assert tau.lo <= (1.0 / 3.0) <= tau.hi

python -m pytest "packages/omnibias-core/tests/verified/test_eig.py::test_birkhoff_diameter_and_ratio_enclosures" -q

Read the implementation

def birkhoff_projective_diameter(matrix: Matrix) -> Interval:
    r"""Enclosure of ``kappa = max_{i,j,k,l} (a_ik a_jl) / (a_jk a_il)`` (``>= 1``).

    Uses the column factorization ``kappa = max_{k,l} m(k,l) m(l,k)`` with
    ``m(k,l) = max_i a_ik / a_il`` (``O(n^3)``).  Each ratio is enclosed; the
    maxima are taken endpoint-wise so the returned interval encloses the true
    ``kappa``.
    """
    a = _positive_matrix(matrix)
    n = len(a)

    def m(k: int, ell: int) -> Interval:
        ratios = [a[i][k] * a[i][ell].reciprocal() for i in range(n)]
        return Interval(max(r.lo for r in ratios), max(r.hi for r in ratios))

    products = [m(k, ell) * m(ell, k) for k in range(n) for ell in range(n)]
    return Interval(max(p.lo for p in products), max(p.hi for p in products))

Related APIsomnibias.core.verified.Interval↗

Other public import paths

• omnibias.core.verified.birkhoff_projective_diameter
• omnibias.core.verified.eig.birkhoff_projective_diameter

FUNCTION

certified_block_operator_gap

omnibias.core.verified.certified_block_operator_gapSource ↗

certified_block_operator_gap(finite_block: Matrix, *, coupling_norm_upper: float, tail_gap_lower: float | None=None) -> BlockOperatorGapCertificate

Conditional coercivity gap of a self-adjoint block operator (finite + tail).

Computes a rigorous lower bound on the finite block's smallest eigenvalue a = \lambda_min(A) (Gershgorin) and combines it with a coupling bound b >= \|B\| (coupling_norm_upper) and an **assumed** tail gap d <= \lambda_min(D) (tail_gap_lower) via

\lambda_{\min}(S) \ge \tfrac12[(a+d) - \sqrt{(a-d)^2 + 4b^2}].

All endpoints are outward rounded so the returned gap_lower is a genuine lower bound *given* the hypothesis d. When tail_gap_lower is None only threshold_tail_gap = b^2/a is reported: the minimal tail gap for which coercivity would follow -- i.e. the single inequality a conditional program must still close. tail_is_hypothesis is always True: this primitive does not prove the tail bound.

Parameters

finite_block: The N x N (numerically) symmetric finite section A = P S P. coupling_norm_upper: A certified upper bound b >= \|B\| on the finite-to-tail coupling. tail_gap_lower: An assumed lower bound d <= \lambda_min(D) on the tail block. Left None to report only the threshold the tail must clear.

Parameters

Name	Type & default	Contract
finite_blockpositional-or-keyword	MatrixRequired	The N x N (numerically) symmetric finite section A = P S P.
coupling_norm_upperkeyword-only	floatRequired	A certified upper bound b >= \|B\| on the finite-to-tail coupling.
tail_gap_lowerkeyword-only	float | NoneDefault: None	An assumed lower bound d <= \lambda_min(D) on the tail block. Left None to report only the threshold the tail must clear.

ReturnsBlockOperatorGapCertificate

Explicit validation & failure cases

• When b < 0.0, raises ValueError('coupling_norm_upper must be >= 0').

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

Executed regression · block gap rejects negative coupling

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_block_gap_rejects_negative_coupling() -> None:
    with pytest.raises(ValueError):
        certified_block_operator_gap([[1.0]], coupling_norm_upper=-0.1)

python -m pytest "packages/omnibias-core/tests/verified/test_eig.py::test_block_gap_rejects_negative_coupling" -q

Regression example · perron gap respects lattice spacing

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_perron_gap_respects_lattice_spacing() -> None:
    a = 0.25
    cert = certified_perron_spectral_gap(A2, lattice_spacing=a)
    assert cert.spectral_gap_lower_per_unit == pytest.approx(
        cert.spectral_gap_lower / a, rel=1e-12
    )

python -m pytest packages/omnibias-core/tests/verified/test_eig.py -k test_perron_gap_respects_lattice_spacing -q

Read the implementation

def certified_block_operator_gap(
    finite_block: Matrix,
    *,
    coupling_norm_upper: float,
    tail_gap_lower: float | None = None,
) -> BlockOperatorGapCertificate:
    r"""Conditional coercivity gap of a self-adjoint block operator (finite + tail).

    Computes a rigorous lower bound on the finite block's smallest eigenvalue
    ``a = \lambda_min(A)`` (Gershgorin) and combines it with a coupling bound
    ``b >= \|B\|`` (``coupling_norm_upper``) and an **assumed** tail gap
    ``d <= \lambda_min(D)`` (``tail_gap_lower``) via

    .. math::
        \lambda_{\min}(S) \ge \tfrac12[(a+d) - \sqrt{(a-d)^2 + 4b^2}].

    All endpoints are outward rounded so the returned ``gap_lower`` is a genuine
    lower bound *given* the hypothesis ``d``.  When ``tail_gap_lower`` is ``None``
    only ``threshold_tail_gap = b^2/a`` is reported: the minimal tail gap for which
    coercivity would follow -- i.e. the single inequality a conditional program must
    still close.  ``tail_is_hypothesis`` is always ``True``: this primitive does not
    prove the tail bound.

    Parameters
    ----------
    finite_block:
        The ``N x N`` (numerically) symmetric finite section ``A = P S P``.
    coupling_norm_upper:
        A certified upper bound ``b >= \|B\|`` on the finite-to-tail coupling.
    tail_gap_lower:
        An assumed lower bound ``d <= \lambda_min(D)`` on the tail block.  Left
        ``None`` to report only the threshold the tail must clear.
    """
    a_mat = _to_matrix(finite_block)
    b = float(coupling_norm_upper)
    if b < 0.0:
        raise ValueError("coupling_norm_upper must be >= 0")
    a = _gershgorin_eig_lower(a_mat)
    a_iv = Interval.point(a)
    b_iv = Interval.point(b)
    if a > 0.0:
        threshold = (b_iv * b_iv * a_iv.reciprocal()).hi
    else:
        threshold = inf
    gap_lower: float | None = None
    coercive = False
    if tail_gap_lower is not None:
        d = float(tail_gap_lower)
        d_iv = Interval.point(d)
        # radicand (a-d)^2 + 4 b^2; clamp the lower endpoint against rounding.
        radicand = (a_iv - d_iv).pow_int(2) + Interval.point(4.0) * b_iv * b_iv
        radicand = Interval(max(radicand.lo, 0.0), max(radicand.hi, 0.0))
        root = radicand.sqrt()
        # lower bound on gamma uses (a+d) low and root.hi (the worst case).
        gamma = (a_iv + d_iv - root) * Interval.point(0.5)
        gap_lower = float(gamma.lo)
        coercive = bool(gamma.lo > 0.0)
    return BlockOperatorGapCertificate(
        finite_dim=len(a_mat),
        finite_gap_lower=float(a),
        coupling_norm_upper=b,
        tail_gap_lower=(float(tail_gap_lower) if tail_gap_lower is not None else None),
        tail_is_hypothesis=True,
        gap_lower=gap_lower,
        coercive=coercive,
        threshold_tail_gap=float(threshold),
    )

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

Other public import paths

• omnibias.core.verified.certified_block_operator_gap
• omnibias.core.verified.eig.certified_block_operator_gap

FUNCTION

certified_perron_spectral_gap

omnibias.core.verified.certified_perron_spectral_gapSource ↗

certified_perron_spectral_gap(matrix: Matrix, *, lattice_spacing: float=1.0) -> PerronGapCertificate

Certified subdominant-ratio and mass-gap lower bound for a positive matrix.

Returns tau with |lambda_1| <= tau lambda_0 and the lattice-unit gap lower bound m a >= -ln(tau) (plus -ln(tau) / a for spacing a). The matrix must be entrywise positive. A rank-one positive matrix has tau = 0 and the gap is reported as inf.

Parameters

Name	Type & default	Contract
matrixpositional-or-keyword	MatrixRequired	See the operation contract and implementation below.
lattice_spacingkeyword-only	floatDefault: 1.0	See the operation contract and implementation below.

ReturnsPerronGapCertificate

Explicit validation & failure cases

• When lattice_spacing <= 0.0, raises ValueError(f'lattice_spacing must be > 0, got {lattice_spacing!r}').

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

Executed regression · perron gap respects lattice spacing

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_perron_gap_respects_lattice_spacing() -> None:
    a = 0.25
    cert = certified_perron_spectral_gap(A2, lattice_spacing=a)
    assert cert.spectral_gap_lower_per_unit == pytest.approx(
        cert.spectral_gap_lower / a, rel=1e-12
    )

python -m pytest "packages/omnibias-core/tests/verified/test_eig.py::test_perron_gap_respects_lattice_spacing" -q

Regression example · perron gap tight for second 2x2

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_perron_gap_tight_for_second_2x2() -> None:
    cert = certified_perron_spectral_gap(B2)  # ratio 1/2, gap ln 2
    assert cert.subdominant_ratio_upper >= 0.5 - 1e-12
    assert cert.spectral_gap_lower <= math.log(2.0) + 1e-12
    assert cert.spectral_gap_lower >= math.log(2.0) - 1e-6

python -m pytest packages/omnibias-core/tests/verified/test_eig.py -k test_perron_gap_tight_for_second_2x2 -q

Read the implementation

def certified_perron_spectral_gap(
    matrix: Matrix, *, lattice_spacing: float = 1.0
) -> PerronGapCertificate:
    r"""Certified subdominant-ratio and mass-gap lower bound for a positive matrix.

    Returns ``tau`` with ``|lambda_1| <= tau lambda_0`` and the lattice-unit gap
    lower bound ``m a >= -ln(tau)`` (plus ``-ln(tau) / a`` for spacing ``a``).  The
    matrix must be entrywise positive.  A rank-one positive matrix has ``tau = 0``
    and the gap is reported as ``inf``.
    """
    a = _positive_matrix(matrix)
    if lattice_spacing <= 0.0:
        raise ValueError(f"lattice_spacing must be > 0, got {lattice_spacing!r}")
    n = len(a)
    min_entry = min(x.lo for row in a for x in row)
    kappa = birkhoff_projective_diameter(a)
    root = kappa.sqrt()
    tau = (root - Interval.point(1.0)) * (root + Interval.point(1.0)).reciprocal()
    tau_upper = max(tau.hi, 0.0)
    if tau_upper <= 0.0:
        gap_lower = inf
    else:
        # m a >= -ln(tau): -ln is decreasing, so a guaranteed lower bound on the
        # gap is -(upper bound of ln(tau_upper)).
        gap_lower = max(-ln_iv(Interval.point(tau_upper)).hi, 0.0)
    gap_per_unit = inf if gap_lower == inf else gap_lower / lattice_spacing
    return PerronGapCertificate(
        dimension=n,
        min_entry=float(min_entry),
        kappa_upper=float(kappa.hi),
        subdominant_ratio_upper=float(tau_upper),
        spectral_gap_lower=float(gap_lower),
        spectral_gap_lower_per_unit=float(gap_per_unit),
    )

Related APIsomnibias.core.verified.PerronGapCertificate↗omnibias.core.verified.birkhoff_projective_diameter↗omnibias.core.verified.ln_iv↗

Other public import paths

• omnibias.core.verified.certified_perron_spectral_gap
• omnibias.core.verified.eig.certified_perron_spectral_gap

FUNCTION

certified_symmetric_spectral_gap

omnibias.core.verified.certified_symmetric_spectral_gapSource ↗

certified_symmetric_spectral_gap(matrix: Matrix, perron_vector: Vector, *, subdominant_vectors: Sequence[Vector] | None=None, lattice_spacing: float=1.0) -> SymmetricGapCertificate

Certified subdominant-ratio / mass-gap for a real **symmetric** matrix.

A must be (numerically) symmetric so that its eigenvalues are real. Given an approximate dominant eigenvector perron_vector the certificate combines two rigorous facts:

• a lower bound lambda_0 >= max(R(x), min_i (A x)_i / x_i) from the Rayleigh quotient and -- when x > 0 and A is positive -- Collatz-Wielandt;
• the power-sum / Schur inequality lambda_1**2 <= trace(A**2) - lambda_0**2 - sum_{i>=2} lambda_i**2 for the second-largest eigenvalue, since sum_i lambda_i**2 = trace(A**2) = sum_ij a_ij**2.

Hence |lambda_1| / lambda_0 <= ratio and the lattice-unit gap obeys m a >= -ln(ratio). Unlike Birkhoff-Hopf this is *tight* whenever the subdominant eigenvalue dominates the remaining tail, recovering nearly the full gap for rapidly decaying spectra. It is still a **fixed-matrix** statement (fixed spacing / finite dimension), never a continuum claim.

subdominant_vectors optionally supplies approximate eigenvectors for the partners v_1 ~ lambda_1, v_2 ~ lambda_2, ... below the dominant mode. When m >= 2 are given, a *chain* of nested frames [perron, v_1, ..., v_k] (k = 2 .. m) each yields a Courant-Fischer lower bound ell_k <= lambda_k (_partner_eigenvalue_lower), and because the lambda_k are distinct power-sum terms sum_k ell_k**2 <= sum_{i>=2} lambda_i**2. Subtracting the whole chain, lambda_1**2 <= trace(A**2) - lambda_0**2 - sum_k ell_k**2, drives the bound toward the exact lambda_1 as more partners are supplied. Deflating a single partner removes the sqrt(multiplicity) inflation of a doubly-degenerate subdominant (the +/- n U(1) modes, the (p, q) <-> (q, p) SU(3) pairs); deflating the chain additionally tames a **slowly-decaying tail** (e.g. the Wilson transfer matrix, whose Bessel eigenvalues I_n decay far slower than a heat kernel's e^{-t C2}). Including the dominant direction in every frame is what makes ell_k a valid lambda_k (not lambda_{k-1}) bound; the chain is rigorous for *any* test vectors (each ell_k >= 0, and 0 whenever positivity or frame full-rank cannot be certified) and never weakens the certificate. partners_deflated reports how many chain terms were certified positive; partner_lower is ell_2 (the first partner).

When at least one subdominant_vectors entry is given the certificate also reports a rigorous **upper** bound on the gap, bracketing m a in [spectral_gap_lower, spectral_gap_upper]: lambda_0 is bounded above by min(sqrt(trace(A**2)), max-Gershgorin-row) and the subdominant lambda_1 below by the smallest Ritz value of the 2-frame [perron, v_2] (Cauchy interlacing: mu_min(V^T A V, V^T V) <= lambda_1), so ratio >= lambda_1_lower / lambda_0_upper and m a <= -ln(that). The bracket collapsing onto a point certifies the gap essentially exactly (a fixed-matrix statement -- it does *not* address the continuum / uniform limit).

A non-positive certified Perron lower bound raises ValueError; a ratio >= 1 (no separation certifiable) yields spectral_gap_lower == 0.0.

Parameters

Name	Type & default	Contract
matrixpositional-or-keyword	MatrixRequired	See the operation contract and implementation below.
perron_vectorpositional-or-keyword	VectorRequired	See the operation contract and implementation below.
subdominant_vectorskeyword-only	Sequence[Vector] | NoneDefault: None	See the operation contract and implementation below.
lattice_spacingkeyword-only	floatDefault: 1.0	See the operation contract and implementation below.

ReturnsSymmetricGapCertificate

Explicit validation & failure cases

• When lattice_spacing <= 0.0, raises ValueError(f'lattice_spacing must be > 0, got {lattice_spacing!r}').
• When perron_lo <= 0.0, raises ValueError('could not certify a positive Perron lower bound').

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

Executed regression · symmetric gap invalid spacing raises

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_symmetric_gap_invalid_spacing_raises() -> None:
    with pytest.raises(ValueError):
        certified_symmetric_spectral_gap(A2, [1.0, 1.0], lattice_spacing=0.0)

python -m pytest "packages/omnibias-core/tests/verified/test_eig.py::test_symmetric_gap_invalid_spacing_raises" -q

Regression example · symmetric gap respects lattice spacing

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_symmetric_gap_respects_lattice_spacing() -> None:
    a = 0.25
    cert = certified_symmetric_spectral_gap(A2, [1.0, 1.0], lattice_spacing=a)
    assert cert.spectral_gap_lower_per_unit == pytest.approx(
        cert.spectral_gap_lower / a, rel=1e-12
    )

python -m pytest packages/omnibias-core/tests/verified/test_eig.py -k test_symmetric_gap_respects_lattice_spacing -q

Read the implementation

def certified_symmetric_spectral_gap(
    matrix: Matrix,
    perron_vector: Vector,
    *,
    subdominant_vectors: Sequence[Vector] | None = None,
    lattice_spacing: float = 1.0,
) -> SymmetricGapCertificate:
    r"""Certified subdominant-ratio / mass-gap for a real **symmetric** matrix.

    ``A`` must be (numerically) symmetric so that its eigenvalues are real.  Given
    an approximate dominant eigenvector ``perron_vector`` the certificate combines
    two rigorous facts:

    * a lower bound ``lambda_0 >= max(R(x), min_i (A x)_i / x_i)`` from the
      Rayleigh quotient and -- when ``x > 0`` and ``A`` is positive --
      Collatz-Wielandt;
    * the power-sum / Schur inequality
      ``lambda_1**2 <= trace(A**2) - lambda_0**2 - sum_{i>=2} lambda_i**2`` for the
      second-largest eigenvalue, since ``sum_i lambda_i**2 = trace(A**2) =
      sum_ij a_ij**2``.

    Hence ``|lambda_1| / lambda_0 <= ratio`` and the lattice-unit gap obeys
    ``m a >= -ln(ratio)``.  Unlike Birkhoff-Hopf this is *tight* whenever the
    subdominant eigenvalue dominates the remaining tail, recovering nearly the
    full gap for rapidly decaying spectra.  It is still a **fixed-matrix**
    statement (fixed spacing / finite dimension), never a continuum claim.

    ``subdominant_vectors`` optionally supplies approximate eigenvectors for the
    partners ``v_1 ~ lambda_1, v_2 ~ lambda_2, ...`` below the dominant mode.  When
    ``m >= 2`` are given, a *chain* of nested frames ``[perron, v_1, ..., v_k]``
    (``k = 2 .. m``) each yields a Courant-Fischer lower bound
    ``ell_k <= lambda_k`` (:func:`_partner_eigenvalue_lower`), and because the
    ``lambda_k`` are distinct power-sum terms ``sum_k ell_k**2 <= sum_{i>=2}
    lambda_i**2``.  Subtracting the whole chain,
    ``lambda_1**2 <= trace(A**2) - lambda_0**2 - sum_k ell_k**2``, drives the bound
    toward the exact ``lambda_1`` as more partners are supplied.  Deflating a single
    partner removes the ``sqrt(multiplicity)`` inflation of a doubly-degenerate
    subdominant (the ``+/- n`` U(1) modes, the ``(p, q) <-> (q, p)`` SU(3) pairs);
    deflating the chain additionally tames a **slowly-decaying tail** (e.g. the
    Wilson transfer matrix, whose Bessel eigenvalues ``I_n`` decay far slower than a
    heat kernel's ``e^{-t C2}``).  Including the dominant direction in every frame is
    what makes ``ell_k`` a valid ``lambda_k`` (not ``lambda_{k-1}``) bound; the chain
    is rigorous for *any* test vectors (each ``ell_k >= 0``, and ``0`` whenever
    positivity or frame full-rank cannot be certified) and never weakens the
    certificate.  ``partners_deflated`` reports how many chain terms were certified
    positive; ``partner_lower`` is ``ell_2`` (the first partner).

    When at least one ``subdominant_vectors`` entry is given the certificate also
    reports a rigorous **upper** bound on the gap, bracketing ``m a`` in
    ``[spectral_gap_lower, spectral_gap_upper]``: ``lambda_0`` is bounded above by
    ``min(sqrt(trace(A**2)), max-Gershgorin-row)`` and the subdominant ``lambda_1``
    below by the smallest Ritz value of the ``2``-frame ``[perron, v_2]``
    (Cauchy interlacing: ``mu_min(V^T A V, V^T V) <= lambda_1``), so
    ``ratio >= lambda_1_lower / lambda_0_upper`` and ``m a <= -ln(that)``.  The
    bracket collapsing onto a point certifies the gap essentially exactly (a
    fixed-matrix statement -- it does *not* address the continuum / uniform limit).

    A non-positive certified Perron lower bound raises ``ValueError``; a ratio
    ``>= 1`` (no separation certifiable) yields ``spectral_gap_lower == 0.0``.
    """
    a = _to_matrix(matrix)
    if lattice_spacing <= 0.0:
        raise ValueError(f"lattice_spacing must be > 0, got {lattice_spacing!r}")
    n = len(a)
    perron_lo = rayleigh_quotient(a, perron_vector).lo
    try:
        perron_lo = max(perron_lo, collatz_wielandt_perron_bounds(a, perron_vector).lo)
    except ValueError:
        # Non-positive matrix or non-positive test vector: keep the Rayleigh bound.
        pass
    if perron_lo <= 0.0:
        raise ValueError("could not certify a positive Perron lower bound")
    perron_lo_iv = Interval.point(perron_lo)
    fro = _frobenius_norm_sq(a)
    # Deflate a *chain* of certified lower bounds on the subdominant's partners.
    # Each nested frame [perron, v_1, ..., v_k] (k = 2 .. m) yields a Courant-Fischer
    # lower bound ell_k <= lambda_k (0-indexed), and since the lambda_k are distinct
    # power-sum terms, sum_k ell_k^2 <= sum_{i>=2} lambda_i^2.  Subtracting the whole
    # chain tightens lambda_1^2 <= trace(A^2) - lambda_0^2 - sum_k ell_k^2 toward the
    # exact value -- crucial for slowly-decaying spectra (e.g. the Wilson transfer
    # matrix, whose Bessel eigenvalues I_n decay far slower than the heat kernel's
    # e^{-t C2}, so a single partner leaves a large polluting tail).  Rigorous for
    # arbitrary inputs: ell_k >= 0, and 0 whenever positivity / frame full-rank
    # cannot be certified, so the tail is never over-deflated.
    partner_lo = 0.0
    partners_deflated = 0
    partner_sq = Interval.point(0.0)
    if subdominant_vectors is not None and len(subdominant_vectors) >= 2:
        subs = [list(v) for v in subdominant_vectors]
        pv = list(perron_vector)
        for k in range(2, len(subs) + 1):
            ell = _partner_eigenvalue_lower(a, [pv, *subs[:k]])
            partner_sq = partner_sq + _square(Interval.point(ell))
            if ell > 0.0:
                partners_deflated += 1
                if k == 2:
                    partner_lo = ell
    # lambda_1^2 <= trace(A^2) - lambda_0^2 - sum_k ell_k^2: upper-bound trace(A^2),
    # lower-bound lambda_0^2 and each ell_k^2; interval subtraction keeps tail.hi an
    # upper bound (subtracting the rounded-down squares only enlarges it).
    tail = fro - _square(perron_lo_iv) - partner_sq
    sub_hi = max(tail.hi, 0.0)
    sub_upper = Interval(sub_hi, sub_hi).sqrt().hi
    ratio = Interval.point(sub_upper) * perron_lo_iv.reciprocal()
    ratio_upper = max(ratio.hi, 0.0)  # honest: > 1 means no certifiable separation
    if 0.0 < ratio_upper < 1.0:
        gap_lower = max(-ln_iv(Interval.point(ratio_upper)).hi, 0.0)
    else:
        # ratio_upper >= 1: no certifiable separation.  ratio_upper == 0: the tail
        # collapsed to numerical zero, indistinguishable from rounding.  Either way
        # the conservative (never-over-claim) gap lower bound is 0.
        gap_lower = 0.0
    # Two-sided bracket: upper bound on lambda_0 (lambda_0^2 <= tr(A^2); Gershgorin
    # row bound) and -- given a subdominant direction -- a lower bound on lambda_1
    # (smallest Ritz value of the 2-frame [perron, v_2]) give an upper gap bound.
    fro_hi = max(fro.hi, 0.0)
    perron_up = min(Interval(fro_hi, fro_hi).sqrt().hi, _gershgorin_eig_upper(a))
    sub_lo = 0.0
    if subdominant_vectors is not None and len(subdominant_vectors) >= 1:
        sub_lo = _partner_eigenvalue_lower(
            a, [list(perron_vector), list(subdominant_vectors[0])]
        )
    gap_upper = inf
    if sub_lo > 0.0 and perron_up > 0.0:
        ratio_lo = (Interval.point(sub_lo) * Interval.point(perron_up).reciprocal()).lo
        if 0.0 < ratio_lo < 1.0:
            gap_upper = max(-ln_iv(Interval.point(ratio_lo)).lo, gap_lower)
    gap_upper_per_unit = gap_upper / lattice_spacing if gap_upper != inf else inf
    return SymmetricGapCertificate(
        dimension=n,
        perron_lower=float(perron_lo),
        subdominant_upper=float(sub_upper),
        subdominant_ratio_upper=float(ratio_upper),
        spectral_gap_lower=float(gap_lower),
        spectral_gap_lower_per_unit=float(gap_lower / lattice_spacing),
        partner_lower=float(partner_lo),
        partners_deflated=int(partners_deflated),
        perron_upper=float(perron_up),
        subdominant_lower=float(sub_lo),
        spectral_gap_upper=float(gap_upper),
        spectral_gap_upper_per_unit=float(gap_upper_per_unit),
    )

Related APIsomnibias.core.verified.SymmetricGapCertificate↗omnibias.core.verified.collatz_wielandt_perron_bounds↗omnibias.core.verified.rayleigh_quotient↗omnibias.core.verified.Interval↗omnibias.core.verified.ln_iv↗

Other public import paths

• omnibias.core.verified.certified_symmetric_spectral_gap
• omnibias.core.verified.eig.certified_symmetric_spectral_gap

FUNCTION

collatz_wielandt_perron_bounds

omnibias.core.verified.collatz_wielandt_perron_boundsSource ↗

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

Collatz-Wielandt enclosure of the Perron root of a positive matrix.

For an entrywise-positive A and a strictly positive test vector x the Perron-Frobenius / Collatz-Wielandt inequalities give min_i (A x)_i / x_i <= lambda_0 <= max_i (A x)_i / x_i. The returned interval [min_i ratio, max_i ratio] brackets the dominant eigenvalue and is tight as x approaches the Perron vector. lo is therefore a certified lower bound on lambda_0.

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 x.lo <= 0.0, raises ValueError('Collatz-Wielandt requires a strictly positive vector').

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

Executed regression · collatz wielandt non perron vector still brackets

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_collatz_wielandt_non_perron_vector_still_brackets() -> None:
    # any positive vector brackets the Perron root between row-scaled extremes.
    enc = collatz_wielandt_perron_bounds(A2, [1.0, 2.0])
    assert enc.lo <= 3.0 <= enc.hi

python -m pytest "packages/omnibias-core/tests/verified/test_eig.py::test_collatz_wielandt_non_perron_vector_still_brackets" -q

Regression example · residual enclosure zero for exact eigenvector

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_residual_enclosure_zero_for_exact_eigenvector() -> None:
    enc = symmetric_eigenvalue_residual_enclosure(A2, [1.0, 1.0])
    assert enc.lo <= 3.0 <= enc.hi
    assert enc.width < 1e-9  # residual ~ 0 -> tight bracket on the eigenvalue

python -m pytest packages/omnibias-core/tests/verified/test_eig.py -k test_residual_enclosure_zero_for_exact_eigenvector -q

Read the implementation

def collatz_wielandt_perron_bounds(matrix: Matrix, vector: Vector) -> Interval:
    r"""Collatz-Wielandt enclosure of the Perron root of a positive matrix.

    For an entrywise-positive ``A`` and a strictly positive test vector ``x`` the
    Perron-Frobenius / Collatz-Wielandt inequalities give
    ``min_i (A x)_i / x_i <= lambda_0 <= max_i (A x)_i / x_i``.  The returned
    interval ``[min_i ratio, max_i ratio]`` brackets the dominant eigenvalue and
    is tight as ``x`` approaches the Perron vector.  ``lo`` is therefore a
    certified lower bound on ``lambda_0``.
    """
    a = _positive_matrix(matrix)
    v = [Interval.from_value(x) for x in vector]
    if len(v) != len(a):
        raise ValueError("vector length must match matrix dimension")
    for x in v:
        if x.lo <= 0.0:
            raise ValueError("Collatz-Wielandt requires a strictly positive vector")
    av = _matvec(a, v)
    ratios = [av[i] * v[i].reciprocal() for i in range(len(v))]
    return Interval(min(r.lo for r in ratios), max(r.hi for r in ratios))

Related APIsomnibias.core.verified.Interval↗

Other public import paths

• omnibias.core.verified.collatz_wielandt_perron_bounds
• omnibias.core.verified.eig.collatz_wielandt_perron_bounds

FUNCTION

rayleigh_quotient

omnibias.core.verified.rayleigh_quotientSource ↗

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

Enclosure of the Rayleigh quotient R(v) = vᵀAv / vᵀv.

For real symmetric A this satisfies lambda_min <= R(v) <= lambda_max, so R(v).lo is a certified lower bound on the largest eigenvalue and R(v).hi an upper bound on the smallest.

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 denom.lo <= 0.0, raises ValueError('vector must be nonzero (vᵀv must exclude 0)').

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

Executed regression · residual enclosure zero for exact eigenvector

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_residual_enclosure_zero_for_exact_eigenvector() -> None:
    enc = symmetric_eigenvalue_residual_enclosure(A2, [1.0, 1.0])
    assert enc.lo <= 3.0 <= enc.hi
    assert enc.width < 1e-9  # residual ~ 0 -> tight bracket on the eigenvalue

python -m pytest "packages/omnibias-core/tests/verified/test_eig.py::test_residual_enclosure_zero_for_exact_eigenvector" -q

Regression example · rayleigh quotient matches analytic

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_rayleigh_quotient_matches_analytic(n: int) -> None:
    lap = _ring_laplacian(n)
    for k in range(1, n // 2):
        v = _cos_mode(n, k)
        lam = 2.0 - 2.0 * math.cos(2.0 * math.pi * k / n)
        rq = rayleigh_quotient(lap, v)
        assert rq.lo <= lam <= rq.hi

python -m pytest packages/omnibias-graph/tests/test_verified_ring.py -k test_rayleigh_quotient_matches_analytic -q

Read the implementation

def rayleigh_quotient(matrix: Matrix, vector: Vector) -> Interval:
    r"""Enclosure of the Rayleigh quotient ``R(v) = vᵀAv / vᵀv``.

    For real symmetric ``A`` this satisfies ``lambda_min <= R(v) <= lambda_max``,
    so ``R(v).lo`` is a certified lower bound on the largest eigenvalue and
    ``R(v).hi`` an upper bound on the smallest.
    """
    a = _to_matrix(matrix)
    v = [Interval.from_value(x) for x in vector]
    if len(v) != len(a):
        raise ValueError("vector length must match matrix dimension")
    denom = _norm_sq(v)
    if denom.lo <= 0.0:
        raise ValueError("vector must be nonzero (vᵀv must exclude 0)")
    num = _dot(v, _matvec(a, v))
    return num * denom.reciprocal()

Other public import paths

• omnibias.core.verified.rayleigh_quotient
• omnibias.core.verified.eig.rayleigh_quotient

FUNCTION

symmetric_eigenvalue_residual_enclosure

omnibias.core.verified.symmetric_eigenvalue_residual_enclosureSource ↗

symmetric_eigenvalue_residual_enclosure(matrix: Matrix, vector: Vector, *, value: IntervalLike | None=None) -> Interval

Interval guaranteed to contain an eigenvalue of the symmetric matrix A.

With theta the Rayleigh quotient (or the supplied value) and residual r = A v - theta v, the symmetric residual theorem gives an eigenvalue of A within rho = ||r||_2 / ||v||_2 of theta. The returned interval is theta + [-rho, rho] (outward rounded). A is assumed symmetric; the enclosure is only meaningful in that case.

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.
valuekeyword-only	IntervalLike | NoneDefault: None	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 v2.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 · residual enclosure zero for exact eigenvector

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_residual_enclosure_zero_for_exact_eigenvector() -> None:
    enc = symmetric_eigenvalue_residual_enclosure(A2, [1.0, 1.0])
    assert enc.lo <= 3.0 <= enc.hi
    assert enc.width < 1e-9  # residual ~ 0 -> tight bracket on the eigenvalue

python -m pytest "packages/omnibias-core/tests/verified/test_eig.py::test_residual_enclosure_zero_for_exact_eigenvector" -q

Regression example · residual enclosure brackets eigenvalue for test vector

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_residual_enclosure_brackets_eigenvalue_for_test_vector() -> None:
    # v = e0 is not an eigenvector: theta = 2, residual norm 1 -> [1, 3].
    enc = symmetric_eigenvalue_residual_enclosure(A2, [1.0, 0.0])
    assert enc.lo <= 1.0 and enc.hi >= 3.0  # contains the true eigenvalues 1 and 3

python -m pytest packages/omnibias-core/tests/verified/test_eig.py -k test_residual_enclosure_brackets_eigenvalue_for_test_vector -q

Read the implementation

def symmetric_eigenvalue_residual_enclosure(
    matrix: Matrix, vector: Vector, *, value: IntervalLike | None = None
) -> Interval:
    r"""Interval guaranteed to contain an eigenvalue of the symmetric matrix ``A``.

    With ``theta`` the Rayleigh quotient (or the supplied ``value``) and residual
    ``r = A v - theta v``, the symmetric residual theorem gives an eigenvalue of
    ``A`` within ``rho = ||r||_2 / ||v||_2`` of ``theta``.  The returned interval
    is ``theta + [-rho, rho]`` (outward rounded).  ``A`` is assumed symmetric; the
    enclosure is only meaningful in that case.
    """
    a = _to_matrix(matrix)
    v = [Interval.from_value(x) for x in vector]
    if len(v) != len(a):
        raise ValueError("vector length must match matrix dimension")
    theta = Interval.from_value(value) if value is not None else rayleigh_quotient(a, v)
    av = _matvec(a, v)
    resid = [av[i] - theta * v[i] for i in range(len(v))]
    v2 = _norm_sq(v)
    if v2.lo <= 0.0:
        raise ValueError("vector must be nonzero")
    # The true radicand ||r||^2 / ||v||^2 is >= 0; outward rounding can push the
    # lower endpoint a denormal below 0, so clamp before the (lo >= 0) sqrt.
    radicand = _norm_sq(resid) * v2.reciprocal()
    rho_hi = Interval(max(radicand.lo, 0.0), max(radicand.hi, 0.0)).sqrt().hi
    return theta + Interval(-rho_hi, rho_hi)

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

Other public import paths

• omnibias.core.verified.symmetric_eigenvalue_residual_enclosure
• omnibias.core.verified.eig.symmetric_eigenvalue_residual_enclosure

← Package overviewRunnable learning examples →