API REFERENCE/omnibias-core

omnibias.core.verified.radii_spectral

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

Module contract & mathematical conventions

Infinite-dimensional radii-polynomial closure for a *quadratic* spectral problem.

This is the capstone of the spectral route: a **computer-assisted existence proof** for a periodic solution of

F(a) = \ell\,a + Q(a, a) - f = 0,

posed in the weighted Banach algebra ~omnibias.core.verified.fourier.ValidatedFourierSeries (\ell^1_\nu over Z^d). Here \ell is a **diagonal** Fourier multiplier \ell(k) (the dominant linear part), Q a bounded **symmetric bilinear** form (a convolution, optionally dressed with Riesz / derivative multipliers -- the SQG advection Q(a,a) = R^\perp a \cdot \nabla a fits), and f a forcing. Steady states of 2-D Euler / SQG-type models and semilinear elliptic problems all have this shape.

The Newton-Kantorovich operator and the split inverse

From an approximate zero \bar a (a finite trigonometric polynomial supported on \|k\|_\infty \le N) we build an approximate inverse A of DF(\bar a) as a *split* operator with truncation N:

• on the finite block \|k\|_\infty \le N: a numerical inverse A_N of the finite Jacobian block B_N = P_N DF(\bar a) P_N (computed in floating point; the rigor comes from *enclosing* I - A_N B_N, never from trusting A_N);
• on the tail \|k\|_\infty > N: the exact diagonal inverse 1/\ell(k), bounded by \mu = \sup_{\|k\|_\infty > N} |\ell(k)|^{-1} (the caller's coercivity hypothesis).

Writing DF(\bar a)h = \ell h + 2 Q(\bar a, h) (symmetric Q) and T(a) = a - A F(a) (so a fixed point of T is a zero of F), the standard radii-polynomial bounds are, with \|A\| = \max(\|A_N\|_{op}, \mu) and C_Q the bilinear bound \|Q(u,v)\| \le C_Q \|u\|\,\|v\|:

Y_0 &= \|A F(\bar a)\|_\nu, \\ Z_0 &= \max_{\|k\|_\infty \le N} \frac{\| e_k - A\,DF(\bar a)\,e_k \|_\nu}{\nu^{\|k\|_1}} \quad(\text{finite-input columns, computed exactly}),\\ Z_1 &= 2\,\|A\|\,C_Q\,\|\bar a\|_\nu \quad(\text{tail-input columns: } \|A\,2Q(\bar a, e_k)\| \le \|A\|\,2C_Q\|\bar a\|\,\nu^{\|k\|_1}),\\ Z_2 &= \|A\|\,C_Q \quad(\tfrac12\,\text{Lipschitz of } DF:\ \|DF(a)-DF(b)\| \le 2C_Q\|a-b\|).

Because \bar a is finite, F(\bar a) and every finite-input column DF(\bar a)e_k = \ell(k)e_k + 2\,\bar a * e_k are supported on \|k\|_\infty \le 2N; working at the internal truncation L = 2N keeps them *exact* (zero tail), so Y_0 and Z_0 are computed with no analytic approximation -- the only analytic estimates are the tail bounds Z_1, Z_2 (controlled by \mu and C_Q). Feeding (Y_0, Z_0, Z_1, Z_2) to ~omnibias.core.verified.kantorovich.radii_polynomial_certificate yields, when a contracting radius r exists, a **true** zero a^\* of F with \|a^\* - \bar a\|_\nu \le r (unique in that ball).

What this does and does not cover

The linear part is either **diagonal** (a Fourier multiplier ell) or **banded**: a BandedLinearPart couples each mode k to a *finite* set of neighbours k + d (e.g. the d = \pm 1 couplings a multiplication-by-cos(x) term produces, the toy stand-in this module uses for the *self-similar* scaling operator \alpha + \beta\,x\cdot\nabla of a finite-time-singularity ansatz -- x\cdot\nabla is genuinely non-diagonal because multiplication by x couples neighbouring Fourier modes). The tail piece of the split inverse (see below) needs a scalar bound mu; for a diagonal symbol that is the exact 1/ell(k) supremum (laplacian_tail_inverse_bound), and for a banded linear part it is tail_inverse_bound_from_banded, built from omnibias.core.verified.banded.banded_tail_inverse_bound via the nu-weighted row/column-sum bound banded_row_sum_bound_nu (see that function's docstring for exactly which operator norm this certifies). Either way mu plugs into the *same* SpectralProblem.tail_inverse_bound field and the *same* Z1/Z2 formulas below -- the banded case only changes how the finite-input columns DF(\bar a)e_k are built and how the split inverse treats modes outside the numerically-inverted block \|k\|_\infty \le N (exactly per-mode for a diagonal symbol; folded into one aggregate mu-scaled magnitude for a banded one, since a non-diagonal tail has no elementary per-mode inverse -- see BandedLinearPart and _SplitInverse.apply).

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

BandedLinearPart

omnibias.core.verified.BandedLinearPartSource ↗

class BandedLinearPart

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

A finite-bandwidth linear part ell(k) e_k + sum_{d} c_d(k) e_{k+d}.

Generalises SpectralProblem.linear_symbol from a diagonal-only Fourier multiplier to a **banded** (non-diagonal) operator that couples each mode k to a finite set of neighbours k + d. This is a strict *alternative* value for linear_symbol -- every existing diagonal call site (a plain Symbol callable) keeps working unchanged; only a caller that explicitly constructs a BandedLinearPart opts into the banded code path.

diagonal is the diagonal part ell, with the identical contract as the plain Symbol this field replaces. couplings maps each nonzero offset d (a Wavevector) to a symbol c_d, so mode k receives the extra contribution c_d(k) * a[k + d] for every d -- e.g. couplings = {(1,): c, (-1,): c} is the pair of nearest-neighbour couplings multiplication by cos(x) produces in a 1-D Fourier basis. See constant_coefficient_band for the common translation-invariant (k-independent c_d) case.

Parameters

Name	Type & default	Contract
diagonaldataclass field	SymbolRequired	See the operation contract and implementation below.
couplingsdataclass field	Mapping[Wavevector, Symbol]Required	See the operation contract and implementation below.

Executed regression · banded manufactured solution proved

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_banded_manufactured_solution_proved() -> None:
    from omnibias.core.verified.radii_spectral import (
        _apply_finite_linear,
        constant_coefficient_band,
        tail_inverse_bound_from_banded,
    )

    dim = 1
    nu = 1.05
    trunc = 4
    coupling = 0.05
    a_star = {(0,): 0.1, (1,): 0.05, (-1,): 0.05, (2,): 0.02, (-2,): 0.02}
    diagonal = laplacian_symbol(4.0, 1.0)
    band = constant_coefficient_band(diagonal, {(1,): coupling, (-1,): coupling})
    mu = tail_inverse_bound_from_banded(
        4.0 + (trunc + 1) ** 2, {(1,): coupling, (-1,): coupling}, nu
    )
    quad = _convolution()
    ab = _embed(a_star, dim, 2 * trunc, nu)
    forcing_series = _apply_finite_linear(ab, band, nu) + quad(ab, ab)  # type: ignore[operator]
    problem = SpectralProblem(
        dim=dim,
        trunc=trunc,
        nu=nu,
        linear_symbol=band,
        tail_inverse_bound=mu,
        quadratic=quad,  # type: ignore[arg-type]
        quadratic_norm=1.0,
        forcing={k: v for k, v in forcing_series.coeffs.items()},
    )
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-10
    result = quadratic_radii_certificate(problem, a_star)
    assert result.proved
    assert result.y0 < 1e-10
    assert result.radius is not None and result.radius > 0.0

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_banded_manufactured_solution_proved" -q

Fields & methods

diagonalfield

diagonal: Symbol

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

View source ↗

couplingsfield

couplings: Mapping[Wavevector, Symbol]

Declared Mapping[Wavevector, Symbol] field on BandedLinearPart. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

__post_init__method

__post_init__(self) -> None

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

Returns: None

Validation & failure cases

• When all((di == 0 for di in d)), raises ValueError('couplings must not include the zero offset; use `diagonal`').

Executed regression · banded manufactured solution proved

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_banded_manufactured_solution_proved() -> None:
    from omnibias.core.verified.radii_spectral import (
        _apply_finite_linear,
        constant_coefficient_band,
        tail_inverse_bound_from_banded,
    )

    dim = 1
    nu = 1.05
    trunc = 4
    coupling = 0.05
    a_star = {(0,): 0.1, (1,): 0.05, (-1,): 0.05, (2,): 0.02, (-2,): 0.02}
    diagonal = laplacian_symbol(4.0, 1.0)
    band = constant_coefficient_band(diagonal, {(1,): coupling, (-1,): coupling})
    mu = tail_inverse_bound_from_banded(
        4.0 + (trunc + 1) ** 2, {(1,): coupling, (-1,): coupling}, nu
    )
    quad = _convolution()
    ab = _embed(a_star, dim, 2 * trunc, nu)
    forcing_series = _apply_finite_linear(ab, band, nu) + quad(ab, ab)  # type: ignore[operator]
    problem = SpectralProblem(
        dim=dim,
        trunc=trunc,
        nu=nu,
        linear_symbol=band,
        tail_inverse_bound=mu,
        quadratic=quad,  # type: ignore[arg-type]
        quadratic_norm=1.0,
        forcing={k: v for k, v in forcing_series.coeffs.items()},
    )
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-10
    result = quadratic_radii_certificate(problem, a_star)
    assert result.proved
    assert result.y0 < 1e-10
    assert result.radius is not None and result.radius > 0.0

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_banded_manufactured_solution_proved" -q

Method implementation

    def __post_init__(self) -> None:
        for d in self.couplings:
            if all(di == 0 for di in d):
                raise ValueError("couplings must not include the zero offset; use `diagonal`")

View source ↗

bandwidthproperty

bandwidth(self) -> int

The sup-norm radius of the coupling offsets (0 if purely diagonal).

Returns: int

Method implementation

    def bandwidth(self) -> int:
        """The sup-norm radius of the coupling offsets (``0`` if purely diagonal)."""
        if not self.couplings:
            return 0
        return max(max(abs(di) for di in d) for d in self.couplings)

View source ↗

Read the implementation

class BandedLinearPart:
    r"""A finite-bandwidth linear part ``ell(k) e_k + sum_{d} c_d(k) e_{k+d}``.

    Generalises :attr:`SpectralProblem.linear_symbol` from a diagonal-only
    Fourier multiplier to a **banded** (non-diagonal) operator that couples
    each mode ``k`` to a finite set of neighbours ``k + d``.  This is a strict
    *alternative* value for ``linear_symbol`` -- every existing diagonal call
    site (a plain :data:`Symbol` callable) keeps working unchanged; only a
    caller that explicitly constructs a ``BandedLinearPart`` opts into the
    banded code path.

    ``diagonal`` is the diagonal part ``ell``, with the identical contract as
    the plain :data:`Symbol` this field replaces.  ``couplings`` maps each
    nonzero offset ``d`` (a :data:`Wavevector`) to a symbol ``c_d``, so mode
    ``k`` receives the extra contribution ``c_d(k) * a[k + d]`` for every
    ``d`` -- e.g. ``couplings = {(1,): c, (-1,): c}`` is the pair of
    nearest-neighbour couplings multiplication by ``cos(x)`` produces in a 1-D
    Fourier basis.  See :func:`constant_coefficient_band` for the common
    translation-invariant (``k``-independent ``c_d``) case.
    """

    diagonal: Symbol
    couplings: Mapping[Wavevector, Symbol]

    def __post_init__(self) -> None:
        for d in self.couplings:
            if all(di == 0 for di in d):
                raise ValueError("couplings must not include the zero offset; use `diagonal`")

    @property
    def bandwidth(self) -> int:
        """The sup-norm radius of the coupling offsets (``0`` if purely diagonal)."""
        if not self.couplings:
            return 0
        return max(max(abs(di) for di in d) for d in self.couplings)

Other public import paths

• omnibias.core.verified.BandedLinearPart
• omnibias.core.verified.radii_spectral.BandedLinearPart

CONSTANT

Bilinear

omnibias.core.verified.BilinearSource ↗

Bilinear = Callable[[ValidatedFourierSeries, ValidatedFourierSeries], ValidatedFourierSeries]

A symmetric bounded bilinear form on the Fourier algebra.

Read the implementation

Bilinear = Callable[[ValidatedFourierSeries, ValidatedFourierSeries], ValidatedFourierSeries]

Other public import paths

• omnibias.core.verified.Bilinear
• omnibias.core.verified.radii_spectral.Bilinear

CLASS

SpectralProblem

omnibias.core.verified.SpectralProblemSource ↗

class SpectralProblem

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

A quadratic spectral problem F(a) = ell*a + Q(a,a) - f in l1_nu.

Parameters

Name	Type & default	Contract
dimdataclass field	intRequired	See the operation contract and implementation below.
truncdataclass field	intRequired	See the operation contract and implementation below.
nudataclass field	floatRequired	See the operation contract and implementation below.
linear_symboldataclass field	Symbol | BandedLinearPartRequired	See the operation contract and implementation below.
tail_inverse_bounddataclass field	floatRequired	See the operation contract and implementation below.
quadraticdataclass field	BilinearRequired	See the operation contract and implementation below.
quadratic_normdataclass field	floatRequired	See the operation contract and implementation below.
forcingdataclass field	Mapping[Wavevector, ComplexLike] | NoneDefault: None	See the operation contract and implementation below.

Executed regression · manufactured solution is an exact zero

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_manufactured_solution_is_an_exact_zero() -> None:
    problem, a_star = _scalar_problem()
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-12

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_manufactured_solution_is_an_exact_zero" -q

Regression example · all bounds nonnegative

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_all_bounds_nonnegative() -> None:
    problem, a_star = _scalar_problem()
    r = quadratic_radii_certificate(problem, a_star)
    assert min(r.y0, r.z0, r.z1, r.z2, r.a_op_norm, r.residual_norm) >= 0.0

python -m pytest packages/omnibias-core/tests/test_verified_radii_spectral.py -k test_all_bounds_nonnegative -q

Fields & methods

dimfield

dim: int

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

Regression example · z1 z2 match their closed form

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_z1_z2_match_their_closed_form() -> None:
    problem, a_star = _scalar_problem()
    result = quadratic_radii_certificate(problem, a_star)
    ab_norm = _embed(a_star, problem.dim, problem.work_trunc, problem.nu).norm().hi
    # Z1 = 2 ||A|| C_Q ||a||,  Z2 = ||A|| C_Q   (C_Q = 1 here).
    assert result.z1 == pytest.approx(2.0 * result.a_op_norm * ab_norm, rel=1e-9)
    assert result.z2 == pytest.approx(result.a_op_norm, rel=1e-9)

python -m pytest packages/omnibias-core/tests/test_verified_radii_spectral.py -k test_z1_z2_match_their_closed_form -q

View source ↗

truncfield

trunc: int

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

Regression example · true solution lies in certified ball

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_true_solution_lies_in_certified_ball() -> None:
    # Certify at a *perturbed* approximation; the genuine zero a* must be captured.
    problem, a_star = _scalar_problem()
    a_bar = dict(a_star)
    a_bar[(3,)] = a_bar.get((3,), 0.0) + 1e-3
    a_bar[(-3,)] = a_bar.get((-3,), 0.0) + 1e-3

    result = quadratic_radii_certificate(problem, a_bar)
    assert result.proved
    assert result.radius is not None
    dist = _distance(a_star, a_bar, problem.dim, problem.trunc, problem.nu)
    assert dist > 0.0  # genuinely perturbed
    assert dist <= result.radius  # the true zero is inside the unique-solution ball

python -m pytest packages/omnibias-core/tests/test_verified_radii_spectral.py -k test_true_solution_lies_in_certified_ball -q

View source ↗

nufield

nu: float

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

Regression example · z1 z2 match their closed form

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_z1_z2_match_their_closed_form() -> None:
    problem, a_star = _scalar_problem()
    result = quadratic_radii_certificate(problem, a_star)
    ab_norm = _embed(a_star, problem.dim, problem.work_trunc, problem.nu).norm().hi
    # Z1 = 2 ||A|| C_Q ||a||,  Z2 = ||A|| C_Q   (C_Q = 1 here).
    assert result.z1 == pytest.approx(2.0 * result.a_op_norm * ab_norm, rel=1e-9)
    assert result.z2 == pytest.approx(result.a_op_norm, rel=1e-9)

python -m pytest packages/omnibias-core/tests/test_verified_radii_spectral.py -k test_z1_z2_match_their_closed_form -q

View source ↗

linear_symbolfield

linear_symbol: Symbol | BandedLinearPart

Declared Symbol | BandedLinearPart field on SpectralProblem. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

tail_inverse_boundfield

tail_inverse_bound: float

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

View source ↗

quadraticfield

quadratic: Bilinear

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

View source ↗

quadratic_normfield

quadratic_norm: float

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

View source ↗

forcingfield

forcing: Mapping[Wavevector, ComplexLike] | None = None

Declared Mapping[Wavevector, ComplexLike] | None field on SpectralProblem. Default expression: None.

View source ↗

__post_init__method

__post_init__(self) -> None

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

Returns: None

Validation & failure cases

• When self.dim < 1, raises ValueError('dim must be >= 1').
• When self.trunc < 1, raises ValueError('trunc N must be >= 1').
• When self.nu < 1.0, raises ValueError('nu must be >= 1 for the l1_nu algebra').
• When self.tail_inverse_bound < 0.0, raises ValueError('tail_inverse_bound mu must be non-negative').
• When self.quadratic_norm < 0.0, raises ValueError('quadratic_norm C_Q must be non-negative').

Executed regression · manufactured solution is an exact zero

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_manufactured_solution_is_an_exact_zero() -> None:
    problem, a_star = _scalar_problem()
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-12

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_manufactured_solution_is_an_exact_zero" -q

Method implementation

    def __post_init__(self) -> None:
        if self.dim < 1:
            raise ValueError("dim must be >= 1")
        if self.trunc < 1:
            raise ValueError("trunc N must be >= 1")
        if self.nu < 1.0:
            raise ValueError("nu must be >= 1 for the l1_nu algebra")
        if self.tail_inverse_bound < 0.0:
            raise ValueError("tail_inverse_bound mu must be non-negative")
        if self.quadratic_norm < 0.0:
            raise ValueError("quadratic_norm C_Q must be non-negative")

View source ↗

work_truncproperty

work_trunc(self) -> int

Internal truncation L = 2N at which residual / columns are exact.

Returns: int

Executed regression · manufactured solution is an exact zero

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_manufactured_solution_is_an_exact_zero() -> None:
    problem, a_star = _scalar_problem()
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-12

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_manufactured_solution_is_an_exact_zero" -q

Method implementation

    def work_trunc(self) -> int:
        """Internal truncation ``L = 2N`` at which residual / columns are exact."""
        return 2 * self.trunc

View source ↗

Read the implementation

class SpectralProblem:
    r"""A quadratic spectral problem ``F(a) = ell*a + Q(a,a) - f`` in ``l1_nu``."""

    dim: int
    trunc: int
    nu: float
    linear_symbol: Symbol | BandedLinearPart
    tail_inverse_bound: float
    quadratic: Bilinear
    quadratic_norm: float
    forcing: Mapping[Wavevector, ComplexLike] | None = None

    def __post_init__(self) -> None:
        if self.dim < 1:
            raise ValueError("dim must be >= 1")
        if self.trunc < 1:
            raise ValueError("trunc N must be >= 1")
        if self.nu < 1.0:
            raise ValueError("nu must be >= 1 for the l1_nu algebra")
        if self.tail_inverse_bound < 0.0:
            raise ValueError("tail_inverse_bound mu must be non-negative")
        if self.quadratic_norm < 0.0:
            raise ValueError("quadratic_norm C_Q must be non-negative")

    @property
    def work_trunc(self) -> int:
        """Internal truncation ``L = 2N`` at which residual / columns are exact."""
        return 2 * self.trunc

Other public import paths

• omnibias.core.verified.SpectralProblem
• omnibias.core.verified.radii_spectral.SpectralProblem

CLASS

SpectralRadiiResult

omnibias.core.verified.SpectralRadiiResultSource ↗

class SpectralRadiiResult

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.

Bounds and (optional) certificate from the spectral radii-polynomial closure.

Parameters

Name	Type & default	Contract
y0dataclass field	floatRequired	See the operation contract and implementation below.
z0dataclass field	floatRequired	See the operation contract and implementation below.
z1dataclass field	floatRequired	See the operation contract and implementation below.
z2dataclass field	floatRequired	See the operation contract and implementation below.
a_op_normdataclass field	floatRequired	See the operation contract and implementation below.
residual_normdataclass field	floatRequired	See the operation contract and implementation below.
certificatedataclass field	RadiiCertificate | NoneRequired	See the operation contract and implementation below.

Executed regression · non coercive symbol is not proved

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_non_coercive_symbol_is_not_proved() -> None:
    # Weak linear part -> large mu / Z1 > 1 -> no contraction.
    problem, a_star = _scalar_problem(c0=0.05, c2=0.01)
    result = quadratic_radii_certificate(problem, a_star)
    assert not result.proved
    assert result.certificate is None

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_non_coercive_symbol_is_not_proved" -q

Regression example · exact solution proved

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_exact_solution_proved() -> None:
    problem, a_star = _scalar_problem()
    result = quadratic_radii_certificate(problem, a_star)
    assert isinstance(result, SpectralRadiiResult)
    assert result.proved
    assert result.certificate is not None
    assert result.y0 < 1e-12  # exact defect
    assert result.z0 < 1.0  # finite-block inverse is good
    assert result.radius is not None and result.radius > 0.0

python -m pytest packages/omnibias-core/tests/test_verified_radii_spectral.py -k test_exact_solution_proved -q

Fields & methods

y0field

y0: float

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

View source ↗

z0field

z0: float

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

View source ↗

z1field

z1: float

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

View source ↗

z2field

z2: float

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

View source ↗

a_op_normfield

a_op_norm: float

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

View source ↗

residual_normfield

residual_norm: float

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

View source ↗

certificatefield

certificate: RadiiCertificate | None

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

View source ↗

provedproperty

proved(self) -> bool

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

Returns: bool

Executed regression · non coercive symbol is not proved

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_non_coercive_symbol_is_not_proved() -> None:
    # Weak linear part -> large mu / Z1 > 1 -> no contraction.
    problem, a_star = _scalar_problem(c0=0.05, c2=0.01)
    result = quadratic_radii_certificate(problem, a_star)
    assert not result.proved
    assert result.certificate is None

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_non_coercive_symbol_is_not_proved" -q

Method implementation

    def proved(self) -> bool:
        return self.certificate is not None

View source ↗

radiusproperty

radius(self) -> float | None

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

Returns: float | None

Executed regression · unproved result still reports bounds

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_unproved_result_still_reports_bounds() -> None:
    problem, a_star = _scalar_problem(c0=0.05, c2=0.01)
    result = quadratic_radii_certificate(problem, a_star)
    assert result.certificate is None
    assert result.radius is None
    # bounds are still computed and inspectable
    assert result.z1 > 0.0
    assert result.a_op_norm > 0.0

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_unproved_result_still_reports_bounds" -q

Method implementation

    def radius(self) -> float | None:
        return None if self.certificate is None else self.certificate.radius

View source ↗

Read the implementation

class SpectralRadiiResult:
    """Bounds and (optional) certificate from the spectral radii-polynomial closure."""

    y0: float
    z0: float
    z1: float
    z2: float
    a_op_norm: float
    residual_norm: float
    certificate: RadiiCertificate | None

    @property
    def proved(self) -> bool:
        return self.certificate is not None

    @property
    def radius(self) -> float | None:
        return None if self.certificate is None else self.certificate.radius

Other public import paths

• omnibias.core.verified.SpectralRadiiResult
• omnibias.core.verified.radii_spectral.SpectralRadiiResult

FUNCTION

banded_row_sum_bound_nu

omnibias.core.verified.banded_row_sum_bound_nuSource ↗

banded_row_sum_bound_nu(coupling_bounds: Mapping[Wavevector, float], nu: float) -> float

The ell^1_nu-consistent off-diagonal row/column-sum bound for a banded tail.

coupling_bounds maps each nonzero offset d to a rigorous upper bound on |c_d(k)|, uniform over every tail row k (a translation-invariant, or merely uniformly-bounded, coupling). Returns

s = \sum_d \texttt{coupling\_bounds}[d] \cdot \nu^{\|d\|_1}

(outward rounded), the off_diagonal_row_sum_upper that omnibias.core.verified.banded.banded_tail_inverse_bound consumes when it is fed *this* quantity rather than a raw (unweighted) row sum.

Why this is the right quantity for ell^1_nu (not just ell^infty)

omnibias.core.verified.banded's docstring is explicit that its bound certifies the operator norm induced by the *unweighted* sup norm, and documents two honest options for a caller who instead needs the weighted ell^1_nu operator norm radii_spectral actually uses (a *column*-sum criterion): reformulate everything in sup-norm, or recompute the row/column sum in the nu-weighted quantity. This function takes the second option. For a fixed output column index j (i.e. the input coefficient at wavevector j), the weighted contribution to every row k with k + d = j is |c_d(k)|\,\nu^{\|k\|_1} for k = j - d; since \|j - d\|_1 \le \|j\|_1 + \|d\|_1 (triangle inequality) and \nu \ge 1 (so \nu^{(\cdot)} is non-decreasing),

\nu^{\|j - d\|_1} \le \nu^{\|j\|_1}\,\nu^{\|d\|_1},

so (1/\nu^{\|j\|_1}) \sum_d |c_d(j-d)|\,\nu^{\|j-d\|_1} \le \sum_d |c_d(j-d)|\,\nu^{\|d\|_1} \le \sum_d \texttt{coupling\_bounds}[d] \,\nu^{\|d\|_1} = s, uniformly in j -- exactly the weighted column-sum bound the ell^1_nu operator norm needs. This requires only a per-offset magnitude bound uniform over k, not literal translation invariance.

Parameters

Name	Type & default	Contract
coupling_boundspositional-or-keyword	Mapping[Wavevector, float]Required	See the operation contract and implementation below.
nupositional-or-keyword	floatRequired	See the operation contract and implementation below.

Returnsfloat

Explicit validation & failure cases

• When nu < 1.0, raises ValueError('nu must be >= 1 for the l1_nu algebra').
• When all((di == 0 for di in d)), raises ValueError('coupling_bounds must not include the zero offset').
• When b < 0.0, raises ValueError(f'coupling bound for offset {d!r} must be non-negative, got {b!r}').

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

Executed regression · banded tail inverse uses banded primitive

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_banded_tail_inverse_uses_banded_primitive() -> None:
    from omnibias.core.verified.radii_spectral import tail_inverse_bound_from_banded

    mu = tail_inverse_bound_from_banded(5.0, {(1,): 0.5, (-1,): 0.5}, 1.05)
    assert mu > 0.0
    assert mu < 1.0

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_banded_tail_inverse_uses_banded_primitive" -q

Read the implementation

def banded_row_sum_bound_nu(coupling_bounds: Mapping[Wavevector, float], nu: float) -> float:
    r"""The ``ell^1_nu``-consistent off-diagonal row/column-sum bound for a banded tail.

    ``coupling_bounds`` maps each nonzero offset ``d`` to a rigorous upper
    bound on ``|c_d(k)|``, uniform over every tail row ``k`` (a
    translation-invariant, or merely uniformly-bounded, coupling).  Returns

    .. math::

        s = \sum_d \texttt{coupling\_bounds}[d] \cdot \nu^{\|d\|_1}

    (outward rounded), the ``off_diagonal_row_sum_upper`` that
    :func:`omnibias.core.verified.banded.banded_tail_inverse_bound` consumes
    when it is fed *this* quantity rather than a raw (unweighted) row sum.

    Why this is the right quantity for ``ell^1_nu`` (not just ``ell^infty``)
    --------------------------------------------------------------------------
    :mod:`omnibias.core.verified.banded`'s docstring is explicit that its bound
    certifies the operator norm induced by the *unweighted* sup norm, and
    documents two honest options for a caller who instead needs the weighted
    ``ell^1_nu`` operator norm :mod:`radii_spectral` actually uses (a
    *column*-sum criterion): reformulate everything in sup-norm, or recompute
    the row/column sum in the ``nu``-weighted quantity.  This function takes
    the second option.  For a fixed output column index ``j`` (i.e. the
    input coefficient at wavevector ``j``), the weighted contribution to every
    row ``k`` with ``k + d = j`` is ``|c_d(k)|\,\nu^{\|k\|_1}`` for
    ``k = j - d``; since ``\|j - d\|_1 \le \|j\|_1 + \|d\|_1`` (triangle
    inequality) and ``\nu \ge 1`` (so ``\nu^{(\cdot)}`` is non-decreasing),

    .. math::

        \nu^{\|j - d\|_1} \le \nu^{\|j\|_1}\,\nu^{\|d\|_1},

    so ``(1/\nu^{\|j\|_1}) \sum_d |c_d(j-d)|\,\nu^{\|j-d\|_1}
    \le \sum_d |c_d(j-d)|\,\nu^{\|d\|_1} \le \sum_d \texttt{coupling\_bounds}[d]
    \,\nu^{\|d\|_1} = s``, uniformly in ``j`` -- exactly the weighted
    column-sum bound the ``ell^1_nu`` operator norm needs.  This requires only
    a per-offset magnitude bound uniform over ``k``, not literal translation
    invariance.
    """
    if nu < 1.0:
        raise ValueError("nu must be >= 1 for the l1_nu algebra")
    terms = []
    for d, bound in coupling_bounds.items():
        if all(di == 0 for di in d):
            raise ValueError("coupling_bounds must not include the zero offset")
        b = float(bound)
        if b < 0.0:
            raise ValueError(f"coupling bound for offset {d!r} must be non-negative, got {b!r}")
        weight = Interval.point(float(nu)).pow_int(sum(abs(di) for di in d))
        terms.append(Interval.point(b) * weight)
    if not terms:
        return 0.0
    return sum_intervals(terms).hi

Related APIsomnibias.core.verified.sum_intervals↗

Other public import paths

• omnibias.core.verified.banded_row_sum_bound_nu
• omnibias.core.verified.radii_spectral.banded_row_sum_bound_nu

FUNCTION

constant_coefficient_band

omnibias.core.verified.constant_coefficient_bandSource ↗

constant_coefficient_band(diagonal: Symbol, coupling_constants: Mapping[Wavevector, ComplexLike]) -> BandedLinearPart

Convenience BandedLinearPart for *translation-invariant* couplings.

coupling_constants maps each nonzero offset d to a **constant** (k-independent) complex coupling coefficient c_d -- the common case where the off-diagonal part comes from convolution with a fixed finite kernel (e.g. multiplication by a fixed trigonometric polynomial such as cos(x), which couples d = \pm 1 with the constant coefficient 1/2).

Parameters

Name	Type & default	Contract
diagonalpositional-or-keyword	SymbolRequired	See the operation contract and implementation below.
coupling_constantspositional-or-keyword	Mapping[Wavevector, ComplexLike]Required	See the operation contract and implementation below.

ReturnsBandedLinearPart

Executed regression · banded manufactured solution proved

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_banded_manufactured_solution_proved() -> None:
    from omnibias.core.verified.radii_spectral import (
        _apply_finite_linear,
        constant_coefficient_band,
        tail_inverse_bound_from_banded,
    )

    dim = 1
    nu = 1.05
    trunc = 4
    coupling = 0.05
    a_star = {(0,): 0.1, (1,): 0.05, (-1,): 0.05, (2,): 0.02, (-2,): 0.02}
    diagonal = laplacian_symbol(4.0, 1.0)
    band = constant_coefficient_band(diagonal, {(1,): coupling, (-1,): coupling})
    mu = tail_inverse_bound_from_banded(
        4.0 + (trunc + 1) ** 2, {(1,): coupling, (-1,): coupling}, nu
    )
    quad = _convolution()
    ab = _embed(a_star, dim, 2 * trunc, nu)
    forcing_series = _apply_finite_linear(ab, band, nu) + quad(ab, ab)  # type: ignore[operator]
    problem = SpectralProblem(
        dim=dim,
        trunc=trunc,
        nu=nu,
        linear_symbol=band,
        tail_inverse_bound=mu,
        quadratic=quad,  # type: ignore[arg-type]
        quadratic_norm=1.0,
        forcing={k: v for k, v in forcing_series.coeffs.items()},
    )
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-10
    result = quadratic_radii_certificate(problem, a_star)
    assert result.proved
    assert result.y0 < 1e-10
    assert result.radius is not None and result.radius > 0.0

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_banded_manufactured_solution_proved" -q

Read the implementation

def constant_coefficient_band(
    diagonal: Symbol, coupling_constants: Mapping[Wavevector, ComplexLike]
) -> BandedLinearPart:
    r"""Convenience :class:`BandedLinearPart` for *translation-invariant* couplings.

    ``coupling_constants`` maps each nonzero offset ``d`` to a **constant**
    (``k``-independent) complex coupling coefficient ``c_d`` -- the common case
    where the off-diagonal part comes from convolution with a fixed finite
    kernel (e.g. multiplication by a fixed trigonometric polynomial such as
    ``cos(x)``, which couples ``d = \pm 1`` with the constant coefficient
    ``1/2``).
    """
    # The factory binds each constant separately, preserving one closure per offset.
    def constant_symbol(value: ComplexLike) -> Symbol:
        coefficient = ComplexInterval.from_value(value)

        def evaluate(_wavevector: Wavevector) -> ComplexInterval:
            return coefficient

        return evaluate

    couplings: dict[Wavevector, Symbol] = {
        tuple(d): constant_symbol(value)
        for d, value in coupling_constants.items()
    }
    return BandedLinearPart(diagonal, couplings)

Related APIsomnibias.core.verified.BandedLinearPart↗

Other public import paths

• omnibias.core.verified.constant_coefficient_band
• omnibias.core.verified.radii_spectral.constant_coefficient_band

FUNCTION

evaluate_residual

omnibias.core.verified.evaluate_residualSource ↗

evaluate_residual(problem: SpectralProblem, a_bar: Mapping[Wavevector, ComplexLike]) -> ValidatedFourierSeries

The residual F(\bar a) = ell*\bar a + Q(\bar a, \bar a) - f (exact at L = 2N).

Parameters

Name	Type & default	Contract
problempositional-or-keyword	SpectralProblemRequired	See the operation contract and implementation below.
a_barpositional-or-keyword	Mapping[Wavevector, ComplexLike]Required	See the operation contract and implementation below.

ReturnsValidatedFourierSeries

Executed regression · manufactured solution is an exact zero

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_manufactured_solution_is_an_exact_zero() -> None:
    problem, a_star = _scalar_problem()
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-12

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_manufactured_solution_is_an_exact_zero" -q

Regression example · riesz dressed symmetric quadratic proof

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_riesz_dressed_symmetric_quadratic_proof() -> None:
    # Symmetric, bounded dressed nonlinearity Q(u,v) = 1/2 (R0 u * v + R0 v * u).
    dim, trunc, nu = 1, 4, 1.05
    c0, c2 = 4.0, 1.0
    symbol = laplacian_symbol(c0, c2)
    mu = laplacian_tail_inverse_bound(dim, trunc, c0, c2)

    def quad(u: ValidatedFourierSeries, v: ValidatedFourierSeries) -> ValidatedFourierSeries:
        return (u.riesz(0) * v + v.riesz(0) * u).scale(0.5)

    a_star = {(0,): 0.0, (1,): 0.05, (-1,): 0.05, (2,): 0.02, (-2,): 0.02}
    forcing = _forcing_for(a_star, dim, trunc, nu, symbol, quad)
    problem = SpectralProblem(
        dim, trunc, nu, symbol, mu, quad, 1.0, forcing  # type: ignore[arg-type]
    )
    assert evaluate_residual(problem, a_star).norm().hi < 1e-12
    result = quadratic_radii_certificate(problem, a_star)
    assert result.proved

python -m pytest packages/omnibias-core/tests/test_verified_radii_spectral.py -k test_riesz_dressed_symmetric_quadratic_proof -q

Read the implementation

def evaluate_residual(
    problem: SpectralProblem, a_bar: Mapping[Wavevector, ComplexLike]
) -> ValidatedFourierSeries:
    r"""The residual ``F(\bar a) = ell*\bar a + Q(\bar a, \bar a) - f`` (exact at ``L = 2N``)."""
    ab = _embed(a_bar, problem.dim, problem.work_trunc, problem.nu)
    residual = _apply_finite_linear(ab, problem.linear_symbol, problem.nu) + problem.quadratic(
        ab, ab
    )
    if problem.forcing is not None:
        residual = residual - _embed(
            problem.forcing, problem.dim, problem.work_trunc, problem.nu
        )
    return residual

Other public import paths

• omnibias.core.verified.evaluate_residual
• omnibias.core.verified.radii_spectral.evaluate_residual

FUNCTION

laplacian_symbol

omnibias.core.verified.laplacian_symbolSource ↗

laplacian_symbol(c0: float, c2: float) -> Symbol

The real diagonal symbol ell(k) = c0 + c2 |k|^2 (a screened Laplacian).

Parameters

Name	Type & default	Contract
c0positional-or-keyword	floatRequired	See the operation contract and implementation below.
c2positional-or-keyword	floatRequired	See the operation contract and implementation below.

ReturnsSymbol

Executed regression · manufactured solution is an exact zero

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_manufactured_solution_is_an_exact_zero() -> None:
    problem, a_star = _scalar_problem()
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-12

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_manufactured_solution_is_an_exact_zero" -q

Regression example · spectralproblem validation

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_spectralproblem_validation(kwargs: dict[str, object], match: str) -> None:
    base = dict(
        dim=1,
        trunc=2,
        nu=1.05,
        linear_symbol=laplacian_symbol(1.0, 1.0),
        tail_inverse_bound=0.1,
        quadratic=_convolution(),
        quadratic_norm=1.0,
    )
    base.update(kwargs)
    with pytest.raises(ValueError, match=match):
        SpectralProblem(**base)  # type: ignore[arg-type]

python -m pytest packages/omnibias-core/tests/test_verified_radii_spectral.py -k test_spectralproblem_validation -q

Read the implementation

def laplacian_symbol(c0: float, c2: float) -> Symbol:
    r"""The real diagonal symbol ``ell(k) = c0 + c2 |k|^2`` (a screened Laplacian)."""

    def m(k: Wavevector) -> ComplexInterval:
        ksq = sum(ki * ki for ki in k)
        return ComplexInterval(
            Interval.from_value(c0) + Interval.from_value(c2) * Interval.from_rational(ksq),
            Interval.point(0.0),
        )

    return m

Related APIsomnibias.core.verified.ComplexInterval↗

Other public import paths

• omnibias.core.verified.laplacian_symbol
• omnibias.core.verified.radii_spectral.laplacian_symbol

FUNCTION

laplacian_tail_inverse_bound

omnibias.core.verified.laplacian_tail_inverse_boundSource ↗

laplacian_tail_inverse_bound(dim: int, trunc: int, c0: float, c2: float) -> float

Sound mu = sup_{||k||inf > N} 1/(c0 + c2 |k|^2) for the screened Laplacian.

On the tail max_i |k_i| >= N + 1 so |k|^2 >= (N + 1)^2; with c0, c2 >= 0 and c0 + c2 (N+1)^2 > 0 the supremum is 1/(c0 + c2 (N+1)^2) (outward rounded).

Parameters

Name	Type & default	Contract
dimpositional-or-keyword	intRequired	See the operation contract and implementation below.
truncpositional-or-keyword	intRequired	See the operation contract and implementation below.
c0positional-or-keyword	floatRequired	See the operation contract and implementation below.
c2positional-or-keyword	floatRequired	See the operation contract and implementation below.

Returnsfloat

Explicit validation & failure cases

• When c0 < 0.0 or c2 < 0.0, raises ValueError('c0 and c2 must be non-negative for a coercive symbol').
• When denom.lo <= 0.0, raises ValueError('symbol is not coercive on the tail (c0 + c2 (N+1)^2 must be > 0)').

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

Executed regression · manufactured solution is an exact zero

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_manufactured_solution_is_an_exact_zero() -> None:
    problem, a_star = _scalar_problem()
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-12

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_manufactured_solution_is_an_exact_zero" -q

Regression example · laplacian tail inverse bound value

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_laplacian_tail_inverse_bound_value() -> None:
    # mu = 1/(c0 + c2 (N+1)^2), N=4 -> 1/(4 + 25) = 1/29.
    mu = laplacian_tail_inverse_bound(1, 4, 4.0, 1.0)
    assert mu == pytest.approx(1.0 / 29.0, rel=1e-12)
    assert mu >= 1.0 / 29.0  # outward rounded upper bound

python -m pytest packages/omnibias-core/tests/test_verified_radii_spectral.py -k test_laplacian_tail_inverse_bound_value -q

Read the implementation

def laplacian_tail_inverse_bound(dim: int, trunc: int, c0: float, c2: float) -> float:
    r"""Sound ``mu = sup_{||k||inf > N} 1/(c0 + c2 |k|^2)`` for the screened Laplacian.

    On the tail ``max_i |k_i| >= N + 1`` so ``|k|^2 >= (N + 1)^2``; with ``c0, c2 >= 0``
    and ``c0 + c2 (N+1)^2 > 0`` the supremum is ``1/(c0 + c2 (N+1)^2)`` (outward rounded).
    """
    if c0 < 0.0 or c2 < 0.0:
        raise ValueError("c0 and c2 must be non-negative for a coercive symbol")
    denom = Interval.from_value(c0) + Interval.from_value(c2) * Interval.from_rational(
        (trunc + 1) ** 2
    )
    if denom.lo <= 0.0:
        raise ValueError("symbol is not coercive on the tail (c0 + c2 (N+1)^2 must be > 0)")
    return (Interval.point(1.0) / denom).hi

Other public import paths

• omnibias.core.verified.laplacian_tail_inverse_bound
• omnibias.core.verified.radii_spectral.laplacian_tail_inverse_bound

FUNCTION

quadratic_radii_certificate

omnibias.core.verified.quadratic_radii_certificateSource ↗

quadratic_radii_certificate(problem: SpectralProblem, a_bar: Mapping[Wavevector, ComplexLike], *, r_max: float=float('inf')) -> SpectralRadiiResult

Attempt a radii-polynomial existence proof for F(a)=0 near \bar a.

Returns a SpectralRadiiResult carrying the rigorous bounds (Y0, Z0, Z1, Z2) and, when a contracting radius exists, a sealed ~omnibias.core.verified.kantorovich.RadiiCertificate proving a *true* zero a^* of F with \|a^* - \bar a\|_\nu \le r (unique there). a_bar is the finite approximation (coefficients on \|k\|_\infty \le N).

Parameters

Name	Type & default	Contract
problempositional-or-keyword	SpectralProblemRequired	See the operation contract and implementation below.
a_barpositional-or-keyword	Mapping[Wavevector, ComplexLike]Required	See the operation contract and implementation below.
r_maxkeyword-only	floatDefault: float('inf')	See the operation contract and implementation below.

ReturnsSpectralRadiiResult

Executed regression · all bounds nonnegative

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_all_bounds_nonnegative() -> None:
    problem, a_star = _scalar_problem()
    r = quadratic_radii_certificate(problem, a_star)
    assert min(r.y0, r.z0, r.z1, r.z2, r.a_op_norm, r.residual_norm) >= 0.0

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_all_bounds_nonnegative" -q

Regression example · non coercive symbol is not proved

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_non_coercive_symbol_is_not_proved() -> None:
    # Weak linear part -> large mu / Z1 > 1 -> no contraction.
    problem, a_star = _scalar_problem(c0=0.05, c2=0.01)
    result = quadratic_radii_certificate(problem, a_star)
    assert not result.proved
    assert result.certificate is None

python -m pytest packages/omnibias-core/tests/test_verified_radii_spectral.py -k test_non_coercive_symbol_is_not_proved -q

Read the implementation

def quadratic_radii_certificate(
    problem: SpectralProblem,
    a_bar: Mapping[Wavevector, ComplexLike],
    *,
    r_max: float = float("inf"),
) -> SpectralRadiiResult:
    r"""Attempt a radii-polynomial existence proof for ``F(a)=0`` near ``\bar a``.

    Returns a :class:`SpectralRadiiResult` carrying the rigorous bounds
    ``(Y0, Z0, Z1, Z2)`` and, when a contracting radius exists, a sealed
    :class:`~omnibias.core.verified.kantorovich.RadiiCertificate` proving a *true*
    zero ``a^*`` of ``F`` with ``\|a^* - \bar a\|_\nu \le r`` (unique there).
    ``a_bar`` is the finite approximation (coefficients on ``\|k\|_\infty \le N``).
    """
    system = _assemble(problem, a_bar)
    inverse, modes, df_cols, ab = system.inverse, system.modes, system.df_cols, system.ab
    nu, c_q = problem.nu, problem.quadratic_norm

    # Z0 = max over finite input columns of || e_k - A DF(ab) e_k ||_nu / nu^|k|.
    z0 = Interval.point(0.0)
    for jk, k in enumerate(modes):
        e_k = _embed({k: 1.0}, problem.dim, problem.work_trunc, nu)
        col = e_k - inverse.apply(df_cols[jk])
        colsum = col.norm() / _weight(nu, k)
        z0 = Interval(max(z0.lo, colsum.lo), max(z0.hi, colsum.hi))

    a_op = inverse.op_norm()
    ab_norm = ab.norm().hi
    z1 = (Interval.point(2.0) * Interval.point(a_op) * Interval.point(c_q) * Interval.point(ab_norm)).hi
    z2 = (Interval.point(a_op) * Interval.point(c_q)).hi

    residual = evaluate_residual(problem, a_bar)
    y0 = inverse.apply(residual).norm().hi
    residual_norm = residual.norm().hi

    cert = radii_polynomial_certificate(
        y0,
        z0.hi,
        z1,
        z2,
        r_max=r_max,
        claim="unique zero a* of F(a)=ell a + Q(a,a) - f in B(a_bar, r) (l1_nu)",
    )
    return SpectralRadiiResult(y0, z0.hi, z1, z2, a_op, residual_norm, cert)

Related APIsomnibias.core.verified.Interval↗omnibias.core.verified.radii_polynomial_certificate↗omnibias.core.verified.SpectralRadiiResult↗omnibias.core.verified.evaluate_residual↗

Other public import paths

• omnibias.core.verified.quadratic_radii_certificate
• omnibias.core.verified.radii_spectral.quadratic_radii_certificate

FUNCTION

tail_inverse_bound_from_banded

omnibias.core.verified.tail_inverse_bound_from_bandedSource ↗

tail_inverse_bound_from_banded(diag_lower: float, coupling_bounds: Mapping[Wavevector, float], nu: float) -> float

mu for SpectralProblem.tail_inverse_bound from a banded tail.

The banded-linear-part generalisation of laplacian_tail_inverse_bound: combines banded_row_sum_bound_nu (the ell^1_nu-consistent off-diagonal sum) with omnibias.core.verified.banded.banded_tail_inverse_bound (the Gershgorin / Neumann-series closed form) to produce the scalar tail operator-norm bound that plugs directly into the existing SpectralProblem(tail_inverse_bound=mu, ...) / _SplitInverse machinery -- unchanged from how a diagonal symbol's mu is used.

diag_lower is the caller's coercivity hypothesis inf_{\|k\|_\infty > N} |ell(k)| \ge \texttt{diag\_lower} > 0 (the same proof obligation laplacian_tail_inverse_bound discharges for the screened Laplacian, generalised to whatever diagonal part the caller's BandedLinearPart uses). coupling_bounds/nu are as in banded_row_sum_bound_nu. Raises ValueError (propagated from ~omnibias.core.verified.banded.banded_tail_inverse_bound) when the resulting row-wise diagonal-dominance margin is not certifiably positive -- never fabricates a bound.

Parameters

Name	Type & default	Contract
diag_lowerpositional-or-keyword	floatRequired	See the operation contract and implementation below.
coupling_boundspositional-or-keyword	Mapping[Wavevector, float]Required	See the operation contract and implementation below.
nupositional-or-keyword	floatRequired	See the operation contract and implementation below.

Returnsfloat

Executed regression · banded tail inverse uses banded primitive

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_banded_tail_inverse_uses_banded_primitive() -> None:
    from omnibias.core.verified.radii_spectral import tail_inverse_bound_from_banded

    mu = tail_inverse_bound_from_banded(5.0, {(1,): 0.5, (-1,): 0.5}, 1.05)
    assert mu > 0.0
    assert mu < 1.0

python -m pytest "packages/omnibias-core/tests/test_verified_radii_spectral.py::test_banded_tail_inverse_uses_banded_primitive" -q

Regression example · laplacian tail inverse bound value

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_laplacian_tail_inverse_bound_value() -> None:
    # mu = 1/(c0 + c2 (N+1)^2), N=4 -> 1/(4 + 25) = 1/29.
    mu = laplacian_tail_inverse_bound(1, 4, 4.0, 1.0)
    assert mu == pytest.approx(1.0 / 29.0, rel=1e-12)
    assert mu >= 1.0 / 29.0  # outward rounded upper bound

python -m pytest packages/omnibias-core/tests/test_verified_radii_spectral.py -k test_laplacian_tail_inverse_bound_value -q

Read the implementation

def tail_inverse_bound_from_banded(
    diag_lower: float, coupling_bounds: Mapping[Wavevector, float], nu: float
) -> float:
    r"""``mu`` for :attr:`SpectralProblem.tail_inverse_bound` from a banded tail.

    The banded-linear-part generalisation of :func:`laplacian_tail_inverse_bound`:
    combines :func:`banded_row_sum_bound_nu` (the ``ell^1_nu``-consistent
    off-diagonal sum) with
    :func:`omnibias.core.verified.banded.banded_tail_inverse_bound` (the
    Gershgorin / Neumann-series closed form) to produce the scalar tail
    operator-norm bound that plugs directly into the existing
    ``SpectralProblem(tail_inverse_bound=mu, ...)`` / ``_SplitInverse``
    machinery -- unchanged from how a diagonal symbol's ``mu`` is used.

    ``diag_lower`` is the caller's coercivity hypothesis
    ``inf_{\|k\|_\infty > N} |ell(k)| \ge \texttt{diag\_lower} > 0`` (the same
    proof obligation :func:`laplacian_tail_inverse_bound` discharges for the
    screened Laplacian, generalised to whatever diagonal part the caller's
    :class:`BandedLinearPart` uses).  ``coupling_bounds``/``nu`` are as in
    :func:`banded_row_sum_bound_nu`.  Raises :class:`ValueError` (propagated
    from :func:`~omnibias.core.verified.banded.banded_tail_inverse_bound`)
    when the resulting row-wise diagonal-dominance margin is not certifiably
    positive -- never fabricates a bound.
    """
    s = banded_row_sum_bound_nu(coupling_bounds, nu)
    return banded_tail_inverse_bound(diag_lower, s).hi

Related APIsomnibias.core.verified.banded_tail_inverse_bound↗omnibias.core.verified.banded_row_sum_bound_nu↗

Other public import paths

• omnibias.core.verified.tail_inverse_bound_from_banded
• omnibias.core.verified.radii_spectral.tail_inverse_bound_from_banded

← Package overviewRunnable learning examples →