API REFERENCE/omnibias-core

omnibias.core.verified.radii_series

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_series

Module contract & mathematical conventions

One-sided radii-polynomial closure for a scalar quadratic fixed-point problem.

Existence gap this closes

omnibias.core.verified.radii_spectral glues the *two-sided* ~omnibias.core.verified.fourier.ValidatedFourierSeries Banach algebra, a symmetric bilinear form, and ~omnibias.core.verified.kantorovich.radii_polynomial_certificate into one Y0/Z0/Z1/Z2 pipeline for F(a) = ell*a + Q(a,a) - f = 0. No analogous pipeline existed for the *one-sided* ~omnibias.core.verified.sequence_space.ValidatedSeries (audited by grepping every radii_polynomial_certificate call site and reading ode.py, series.py, taylor_model.py, and pde_certificate.py -- the closest relative, pde_certificate.radii_polynomial_residual_certificate, is a thin wrapper that only *consumes* caller-precomputed (Y0,Z0,Z1,Z2) floats; it does not assemble them from a ValidatedSeries problem, so it is not a duplicate of what this module builds). This module is that minimal counterpart, scoped to the same shape radii_spectral uses:

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

posed in the weighted one-sided Banach algebra ~omnibias.core.verified.sequence_space.ValidatedSeries (ell^1_\nu over n >= 0). Here \ell is a **diagonal** symbol ell(n) (a per-coefficient scalar multiplier -- the one-sided analogue of radii_spectral's Fourier multiplier; a genuinely diagonal example in this monomial basis is the Euler/scaling generator c0 + c1\,(x\,d/dx), whose eigenvalue on x^n is c0 + c1 n), and the nonlinearity Q(a,a) := a * a is *exactly* ~omnibias.core.verified.sequence_space.ValidatedSeries.__mul__ -- the Banach-algebra convolution, not a caller-pluggable bilinear form -- so its bound C_Q = 1 is exact (||a*b||_nu <= ||a||_nu ||b||_nu, proved in omnibias.core.verified.sequence_space), not an estimate.

The Newton-Kantorovich operator and the split inverse

From an approximate zero a_bar (a length N+1 polynomial, coefficients 0..N) build an approximate inverse A of DF(a_bar) as a *split* operator with truncation N:

• on the finite block 0 <= n <= N: a numerical inverse A_N of the finite Jacobian block B_N (computed in floating point; rigor comes from *enclosing* every finite-input column exactly, never from trusting A_N itself);
• on the tail n > N: the exact diagonal inverse 1/ell(n), bounded by mu = sup_{n>N} |ell(n)|^{-1} (the caller's coercivity hypothesis, exactly omnibias.core.verified.banded.banded_tail_inverse_bound's diagonal s=0 special case -- see constant_tail_inverse_bound, which reuses it rather than re-deriving the same 1/d_min formula).

Writing DF(a_bar)h = ell*h + 2*(a_bar * h) (Q symmetric because convolution commutes) and T(a) = a - A F(a), the radii-polynomial bounds are, with ||A|| = max(||A_N||_op, mu) and C_Q = 1:

Y_0 &= \|A F(\bar a)\|_\nu, \\ Z_0 &= \max_{0 \le n \le N} \frac{\| e_n - A\,DF(\bar a)\,e_n \|_\nu}{\nu^{n}} \quad(\text{finite-input columns, computed exactly}),\\ Z_1 &= 2\,\|A\|\,\|\bar a\|_\nu \quad(\text{tail-input columns}),\\ Z_2 &= \|A\| \quad(\tfrac12\,\text{Lipschitz constant of } DF).

Because a_bar has only N+1 nonzero coefficients, embedding it (and every unit column e_n) as a *padded* ValidatedSeries of length 2N+1 (extra coefficients set to the exact point 0.0, zero tail) keeps every product computed by ValidatedSeries.__mul__ **exact**: the true convolution of two degree-<=N polynomials has degree <=2N, so it fits entirely inside the kept block at truncation L=2N and every "overflow" term ValidatedSeries.__mul__ folds into its tail is a literal sum of exact zeros. So F(a_bar) and every finite-input column DF(a_bar)e_n are exact (no analytic approximation); only the tail bounds Z_1, Z_2 (controlled by mu) are analytic estimates. 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* - a_bar||_nu <= r (unique in that ball).

What this does and does not cover

The linear part must be **diagonal** in the one-sided monomial basis (a per-coefficient scalar ell(n)); the nonlinearity is fixed to the algebra's own square a*a, not a general bilinear form. Both restrictions keep this a small, honestly-scoped instance of the same machinery radii_spectral provides for the two-sided Fourier case -- a **banded** (non-diagonal) linear part in either basis is out of scope here exactly as it is there (see omnibias.core.verified.banded for the tail-inverse-norm primitive a banded-capable successor of *either* pipeline would need).

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

SeriesProblem

omnibias.core.verified.SeriesProblemSource ↗

class SeriesProblem

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 one-sided problem F(a) = ell*a + a*a - f in ell^1_nu.

Parameters

Name	Type & default	Contract
truncdataclass field	intRequired	See the operation contract and implementation below.
nudataclass field	floatRequired	See the operation contract and implementation below.
linear_symboldataclass field	SymbolRequired	See the operation contract and implementation below.
tail_inverse_bounddataclass field	floatRequired	See the operation contract and implementation below.
forcingdataclass field	Sequence[IntervalLike] | 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/verified/test_radii_series.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 = series_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/verified/test_radii_series.py -k test_all_bounds_nonnegative -q

Fields & methods

truncfield

trunc: int

Declared int field on SeriesProblem. 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 = list(a_star)
    a_bar[-1] += 1e-3

    result = series_radii_certificate(problem, a_bar)
    assert result.proved
    assert result.radius is not None
    dist = _distance(a_star, a_bar, 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/verified/test_radii_series.py -k test_true_solution_lies_in_certified_ball -q

View source ↗

nufield

nu: float

Declared float field on SeriesProblem. 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 = series_radii_certificate(problem, a_star)
    ab_norm = _embed(a_star, 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/verified/test_radii_series.py -k test_z1_z2_match_their_closed_form -q

View source ↗

linear_symbolfield

linear_symbol: Symbol

Declared Symbol field on SeriesProblem. 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 SeriesProblem. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

forcingfield

forcing: Sequence[IntervalLike] | None = None

Declared Sequence[IntervalLike] | None field on SeriesProblem. 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.trunc < 1, raises ValueError('trunc N must be >= 1').
• When self.nu <= 0.0, raises ValueError('nu must be > 0 for the ell^1_nu algebra').
• When self.tail_inverse_bound < 0.0, raises ValueError('tail_inverse_bound mu must be non-negative').
• When self.forcing is not None and len(self.forcing) > self.work_trunc + 1, raises ValueError(f'forcing has {len(self.forcing)} coefficients, exceeding work_trunc+1={self.work_trunc + 1}').

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/verified/test_radii_series.py::test_manufactured_solution_is_an_exact_zero" -q

Method implementation

    def __post_init__(self) -> None:
        if self.trunc < 1:
            raise ValueError("trunc N must be >= 1")
        if self.nu <= 0.0:
            raise ValueError("nu must be > 0 for the ell^1_nu algebra")
        if self.tail_inverse_bound < 0.0:
            raise ValueError("tail_inverse_bound mu must be non-negative")
        if self.forcing is not None and len(self.forcing) > self.work_trunc + 1:
            raise ValueError(
                f"forcing has {len(self.forcing)} coefficients, exceeding "
                f"work_trunc+1={self.work_trunc + 1}"
            )

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/verified/test_radii_series.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 SeriesProblem:
    r"""A quadratic one-sided problem ``F(a) = ell*a + a*a - f`` in ``ell^1_nu``."""

    trunc: int
    nu: float
    linear_symbol: Symbol
    tail_inverse_bound: float
    forcing: Sequence[IntervalLike] | None = None

    def __post_init__(self) -> None:
        if self.trunc < 1:
            raise ValueError("trunc N must be >= 1")
        if self.nu <= 0.0:
            raise ValueError("nu must be > 0 for the ell^1_nu algebra")
        if self.tail_inverse_bound < 0.0:
            raise ValueError("tail_inverse_bound mu must be non-negative")
        if self.forcing is not None and len(self.forcing) > self.work_trunc + 1:
            raise ValueError(
                f"forcing has {len(self.forcing)} coefficients, exceeding "
                f"work_trunc+1={self.work_trunc + 1}"
            )

    @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.SeriesProblem
• omnibias.core.verified.radii_series.SeriesProblem

CLASS

SeriesRadiiResult

omnibias.core.verified.SeriesRadiiResultSource ↗

class SeriesRadiiResult

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 one-sided 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(lam=0.05)
    result = series_radii_certificate(problem, a_star)
    assert not result.proved
    assert result.certificate is None

python -m pytest "packages/omnibias-core/tests/verified/test_radii_series.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 = series_radii_certificate(problem, a_star)
    assert isinstance(result, SeriesRadiiResult)
    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/verified/test_radii_series.py -k test_exact_solution_proved -q

Fields & methods

y0field

y0: float

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

View source ↗

z0field

z0: float

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

View source ↗

z1field

z1: float

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

View source ↗

z2field

z2: float

Declared float field on SeriesRadiiResult. 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 SeriesRadiiResult. 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 SeriesRadiiResult. 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 SeriesRadiiResult. 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(lam=0.05)
    result = series_radii_certificate(problem, a_star)
    assert not result.proved
    assert result.certificate is None

python -m pytest "packages/omnibias-core/tests/verified/test_radii_series.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(lam=0.05)
    result = series_radii_certificate(problem, a_star)
    assert result.certificate is None
    assert result.radius is None
    assert result.z1 > 0.0
    assert result.a_op_norm > 0.0

python -m pytest "packages/omnibias-core/tests/verified/test_radii_series.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 SeriesRadiiResult:
    """Bounds and (optional) certificate from the one-sided 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.SeriesRadiiResult
• omnibias.core.verified.radii_series.SeriesRadiiResult

CONSTANT

Symbol

omnibias.core.verified.SeriesSymbolSource ↗

Symbol = Callable[[int], float]

A diagonal (per-coefficient scalar) linear symbol n -> ell(n).

Read the implementation

Symbol = Callable[[int], float]

Other public import paths

• omnibias.core.verified.SeriesSymbol
• omnibias.core.verified.radii_series.Symbol

FUNCTION

constant_symbol

omnibias.core.verified.constant_symbolSource ↗

constant_symbol(value: float) -> Symbol

The diagonal symbol ell(n) = value for every coefficient n (value*I).

Parameters

Name	Type & default	Contract
valuepositional-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/verified/test_radii_series.py::test_manufactured_solution_is_an_exact_zero" -q

Regression example · seriesproblem 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_seriesproblem_validation(kwargs: dict[str, object], match: str) -> None:
    base: dict[str, object] = dict(
        trunc=2,
        nu=1.05,
        linear_symbol=constant_symbol(4.0),
        tail_inverse_bound=0.25,
    )
    base.update(kwargs)
    with pytest.raises(ValueError, match=match):
        SeriesProblem(**base)  # type: ignore[arg-type]

python -m pytest packages/omnibias-core/tests/verified/test_radii_series.py -k test_seriesproblem_validation -q

Read the implementation

def constant_symbol(value: float) -> Symbol:
    r"""The diagonal symbol ``ell(n) = value`` for every coefficient ``n`` (``value*I``)."""

    def m(n: int) -> float:
        return value

    return m

Other public import paths

• omnibias.core.verified.constant_symbol
• omnibias.core.verified.radii_series.constant_symbol

FUNCTION

constant_tail_inverse_bound

omnibias.core.verified.constant_tail_inverse_boundSource ↗

constant_tail_inverse_bound(value: float) -> float

Sound mu = 1/|value| for the constant symbol ell(n) = value != 0.

Reuses omnibias.core.verified.banded.banded_tail_inverse_bound with a zero off-diagonal row sum: this problem's linear part is purely diagonal, so s = 0 and the general banded-operator bound specialises *exactly* to the classical 1/d_min formula (omnibias.core.verified.radii_spectral.laplacian_tail_inverse_bound is the same specialisation on the Fourier side) rather than re-deriving it.

Parameters

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

Returnsfloat

Executed regression · constant tail inverse bound requires nonzero

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_constant_tail_inverse_bound_requires_nonzero() -> None:
    with pytest.raises(ValueError, match="strictly positive"):
        constant_tail_inverse_bound(0.0)

python -m pytest "packages/omnibias-core/tests/verified/test_radii_series.py::test_constant_tail_inverse_bound_requires_nonzero" -q

Regression example · constant 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_constant_tail_inverse_bound_value() -> None:
    # mu = 1/|value|, value=4 -> 0.25, matching banded_tail_inverse_bound(4, 0).
    mu = constant_tail_inverse_bound(4.0)
    assert mu == pytest.approx(0.25, rel=1e-12)
    assert mu == banded_tail_inverse_bound(4.0, 0.0).hi

python -m pytest packages/omnibias-core/tests/verified/test_radii_series.py -k test_constant_tail_inverse_bound_value -q

Read the implementation

def constant_tail_inverse_bound(value: float) -> float:
    r"""Sound ``mu = 1/|value|`` for the constant symbol ``ell(n) = value != 0``.

    Reuses :func:`omnibias.core.verified.banded.banded_tail_inverse_bound` with a
    zero off-diagonal row sum: this problem's linear part is purely diagonal, so
    ``s = 0`` and the general banded-operator bound specialises *exactly* to the
    classical ``1/d_min`` formula
    (:func:`omnibias.core.verified.radii_spectral.laplacian_tail_inverse_bound`
    is the same specialisation on the Fourier side) rather than re-deriving it.
    """
    return banded_tail_inverse_bound(abs(value), 0.0).hi

Related APIsomnibias.core.verified.banded_tail_inverse_bound↗

Other public import paths

• omnibias.core.verified.constant_tail_inverse_bound
• omnibias.core.verified.radii_series.constant_tail_inverse_bound

FUNCTION

evaluate_residual

omnibias.core.verified.evaluate_series_residualSource ↗

evaluate_residual(problem: SeriesProblem, a_bar: Sequence[IntervalLike]) -> ValidatedSeries

The residual F(a_bar) = ell*a_bar + a_bar*a_bar - f (exact at L = 2N).

Parameters

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

ReturnsValidatedSeries

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/verified/test_radii_series.py::test_manufactured_solution_is_an_exact_zero" -q

Regression example · a bar longer than trunc plus one raises

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_a_bar_longer_than_trunc_plus_one_raises() -> None:
    problem, _ = _scalar_problem(trunc=2, a_star=[0.1, 0.05, 0.02])
    too_long = [0.1, 0.05, 0.02, 0.01]  # length 4 > trunc+1 = 3
    with pytest.raises(ValueError, match="trunc"):
        evaluate_residual(problem, too_long)
    with pytest.raises(ValueError, match="trunc"):
        series_radii_certificate(problem, too_long)

python -m pytest packages/omnibias-core/tests/verified/test_radii_series.py -k test_a_bar_longer_than_trunc_plus_one_raises -q

Read the implementation

def evaluate_residual(problem: SeriesProblem, a_bar: Sequence[IntervalLike]) -> ValidatedSeries:
    r"""The residual ``F(a_bar) = ell*a_bar + a_bar*a_bar - f`` (exact at ``L = 2N``)."""
    _validate_a_bar(problem, a_bar)
    ab = _embed(a_bar, problem.work_trunc, problem.nu)
    residual = _apply_diagonal_symbol(ab, problem.linear_symbol) + (ab * ab)
    if problem.forcing is not None:
        residual = residual + _embed(problem.forcing, problem.work_trunc, problem.nu).scale(-1.0)
    return residual

Other public import paths

• omnibias.core.verified.evaluate_series_residual
• omnibias.core.verified.radii_series.evaluate_residual

FUNCTION

series_radii_certificate

omnibias.core.verified.series_radii_certificateSource ↗

series_radii_certificate(problem: SeriesProblem, a_bar: Sequence[IntervalLike], *, r_max: float=float('inf')) -> SeriesRadiiResult

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

Returns a SeriesRadiiResult 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* - a_bar||_nu <= r (unique there). a_bar is the finite approximation (coefficients 0..N).

Parameters

Name	Type & default	Contract
problempositional-or-keyword	SeriesProblemRequired	See the operation contract and implementation below.
a_barpositional-or-keyword	Sequence[IntervalLike]Required	See the operation contract and implementation below.
r_maxkeyword-only	floatDefault: float('inf')	See the operation contract and implementation below.

ReturnsSeriesRadiiResult

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 = series_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/verified/test_radii_series.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(lam=0.05)
    result = series_radii_certificate(problem, a_star)
    assert not result.proved
    assert result.certificate is None

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

Read the implementation

def series_radii_certificate(
    problem: SeriesProblem,
    a_bar: Sequence[IntervalLike],
    *,
    r_max: float = float("inf"),
) -> SeriesRadiiResult:
    r"""Attempt a radii-polynomial existence proof for ``F(a) = 0`` near ``a_bar``.

    Returns a :class:`SeriesRadiiResult` 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* - a_bar||_nu <= r`` (unique there). ``a_bar``
    is the finite approximation (coefficients ``0..N``).
    """
    system = _assemble(problem, a_bar)
    inverse, df_cols, ab = system.inverse, system.df_cols, system.ab
    nu = problem.nu
    n = problem.trunc + 1
    c_q = 1.0  # exact Banach-algebra bound for Q(a,a) = a*a.

    # Z0 = max over finite input columns of || e_n - A DF(ab) e_n ||_nu / nu^n.
    z0 = Interval.point(0.0)
    for k in range(n):
        e_k = _unit(k, problem.work_trunc, nu)
        col = e_k + inverse.apply(df_cols[k]).scale(-1.0)
        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(ab_norm)).hi
    z2 = Interval.point(a_op).hi * c_q

    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 + a*a - f in B(a_bar, r) (one-sided ell^1_nu)",
    )
    return SeriesRadiiResult(y0, z0.hi, z1, z2, a_op, residual_norm, cert)

Related APIsomnibias.core.verified.Interval↗omnibias.core.verified.radii_polynomial_certificate↗omnibias.core.verified.SeriesRadiiResult↗omnibias.core.verified.evaluate_series_residual↗

Other public import paths

• omnibias.core.verified.series_radii_certificate
• omnibias.core.verified.radii_series.series_radii_certificate

← Package overviewRunnable learning examples →