API REFERENCE/omnibias-core

omnibias.core.verified.kantorovich

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

Module contract & mathematical conventions

Newton-Kantorovich / radii-polynomial existence certificates.

These are the standard workhorses of computer-assisted analysis: from an *approximate* zero x_bar of F and an approximate inverse A of the linearisation DF(x_bar), they prove a **true** zero exists in an explicit ball around x_bar -- and is unique there.

Two complementary, fully rigorous routes are provided:

• radii_polynomial_certificate -- the scalar *radii polynomial* p(r) = Z2 r^2 - (1 - Z0 - Z1) r + Y0. If some r gives p(r) < 0 and the contraction factor Z0 + Z1 + 2 Z2 r < 1 then the Newton-like operator is a self-map and contraction on B(x_bar, r) -- a unique zero exists there. The bounds Y0, Z0, Z1, Z2 are rigorous *upper* bounds; the certificate re-verifies the chosen radius in interval arithmetic.
• krawczyk_certificate -- the finite-dimensional **Krawczyk** test, which evaluates DF over the whole box and needs no separate Z2: if K(x_bar, X) subset int(X) and ||I - A DF(X)|| < 1 then F has a unique zero in X = B(x_bar, r).

newton_kantorovich_bounds computes (Y0, Z0, Z1, Z2) from F, its Jacobian, A and a caller-supplied Lipschitz bound on DF (explicit for polynomial maps), feeding the radii polynomial.

kantorovich_accept_step is the optimizer policy (theory 08-04): a Gauss–Newton or cubic trial is **legal** only when the radii polynomial returns a nonempty unique-zero ball. An empty ball is a valid reject, not a training failure. The sealed payload records continuum_pde_claim: false; the ball is of a finite residual map, never a continuum PDE solution. theorem_prover_verified is not asserted (sound-enclosure tier).

Shared formulas do not imply universal floating-point identity. Verify dtype, shape, derivative-order support, and the stated numerical assumptions for the path you use.

Module source ↗Source revision 9a2d73df0573Running reference examples →

CONSTANT

CONTINUUM_PDE_CLAIM_KEY

omnibias.core.verified.CONTINUUM_PDE_CLAIM_KEYSource ↗

CONTINUUM_PDE_CLAIM_KEY = 'continuum_pde_claim'

Honesty / payload key: the ball is never a continuum PDE existence claim.

Regression example · g2 never continuum

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_g2_never_continuum() -> None:
    func, jac, lip = polynomial_sqrt2_maps()
    decision = kantorovich_accept_step(
        func, jac, GOOD_A, [GOOD_TRIAL], lipschitz_df=lip, r_max=R_MAX
    )
    assert decision.certificate is not None
    sealed = decision.certificate.certificate
    assert verify_certificate_digest(sealed)
    payload = sealed["payload"]
    honesty = sealed["honesty"]
    assert payload[CONTINUUM_PDE_CLAIM_KEY] is False
    assert honesty[CONTINUUM_PDE_CLAIM_KEY] is False
    assert payload["finite_map"] is True
    claim = sealed["claim"]
    assert claim == FINITE_RESIDUAL_CLAIM
    assert "finite-dimensional" in claim
    assert "continuum PDE" in claim

python -m pytest packages/omnibias-core/tests/verified/test_kantorovich_accept.py -k test_g2_never_continuum -q

Read the implementation

CONTINUUM_PDE_CLAIM_KEY = "continuum_pde_claim"

Other public import paths

• omnibias.core.verified.CONTINUUM_PDE_CLAIM_KEY
• omnibias.core.verified.kantorovich.CONTINUUM_PDE_CLAIM_KEY

CONSTANT

FINITE_RESIDUAL_CLAIM

omnibias.core.verified.FINITE_RESIDUAL_CLAIMSource ↗

FINITE_RESIDUAL_CLAIM = 'unique zero of a finite-dimensional residual map F in B(theta_bar, r); not a continuum PDE solution'

Default claim for the optimizer accept/reject policy (theory 08-04).

Regression example · g2 never continuum

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_g2_never_continuum() -> None:
    func, jac, lip = polynomial_sqrt2_maps()
    decision = kantorovich_accept_step(
        func, jac, GOOD_A, [GOOD_TRIAL], lipschitz_df=lip, r_max=R_MAX
    )
    assert decision.certificate is not None
    sealed = decision.certificate.certificate
    assert verify_certificate_digest(sealed)
    payload = sealed["payload"]
    honesty = sealed["honesty"]
    assert payload[CONTINUUM_PDE_CLAIM_KEY] is False
    assert honesty[CONTINUUM_PDE_CLAIM_KEY] is False
    assert payload["finite_map"] is True
    claim = sealed["claim"]
    assert claim == FINITE_RESIDUAL_CLAIM
    assert "finite-dimensional" in claim
    assert "continuum PDE" in claim

python -m pytest packages/omnibias-core/tests/verified/test_kantorovich_accept.py -k test_g2_never_continuum -q

Read the implementation

FINITE_RESIDUAL_CLAIM = (
    "unique zero of a finite-dimensional residual map F in B(theta_bar, r); "
    "not a continuum PDE solution"
)

Other public import paths

• omnibias.core.verified.FINITE_RESIDUAL_CLAIM
• omnibias.core.verified.kantorovich.FINITE_RESIDUAL_CLAIM

CLASS

KantorovichAccept

omnibias.core.verified.KantorovichAcceptSource ↗

class KantorovichAccept

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.

Optimizer policy: apply a trial step only if a unique-zero ball exists.

reason is "ball" on accept, "empty" when the radii polynomial has no admissible radius, and "bounds_failed" when the Newton-Kantorovich bounds cannot be assembled (singular / mismatched A, non-finite trial). Empty is a **valid** outcome: refuse the step, do not train through it.

Parameters

Name	Type & default	Contract
accepteddataclass field	boolRequired	See the operation contract and implementation below.
certificatedataclass field	RadiiCertificate | NoneRequired	See the operation contract and implementation below.
reasondataclass field	AcceptReasonRequired	See the operation contract and implementation below.

Fields & methods

acceptedfield

accepted: bool

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

View source ↗

reasonfield

reason: AcceptReason

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

View source ↗

Read the implementation

class KantorovichAccept:
    """Optimizer policy: apply a trial step only if a unique-zero ball exists.

    ``reason`` is ``"ball"`` on accept, ``"empty"`` when the radii polynomial
    has no admissible radius, and ``"bounds_failed"`` when the Newton-Kantorovich
    bounds cannot be assembled (singular / mismatched ``A``, non-finite trial).
    Empty is a **valid** outcome: refuse the step, do not train through it.
    """

    accepted: bool
    certificate: RadiiCertificate | None
    reason: AcceptReason

Other public import paths

• omnibias.core.verified.KantorovichAccept
• omnibias.core.verified.kantorovich.KantorovichAccept

CLASS

KrawczykCertificate

omnibias.core.verified.KrawczykCertificateSource ↗

class KrawczykCertificate

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 verified unique-zero box from the Krawczyk operator.

Parameters

Name	Type & default	Contract
radiusdataclass field	floatRequired	See the operation contract and implementation below.
kappadataclass field	floatRequired	See the operation contract and implementation below.
centerdataclass field	tuple[float, ...]Required	See the operation contract and implementation below.
enclosuredataclass field	tuple[tuple[float, float], ...]Required	See the operation contract and implementation below.
certificatedataclass field	CertRequired	See the operation contract and implementation below.

Fields & methods

radiusfield

radius: float

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

View source ↗

kappafield

kappa: float

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

View source ↗

centerfield

center: tuple[float, ...]

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

View source ↗

enclosurefield

enclosure: tuple[tuple[float, float], ...]

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

View source ↗

certificatefield

certificate: Cert

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

View source ↗

Read the implementation

class KrawczykCertificate:
    """A verified unique-zero box from the Krawczyk operator."""

    radius: float
    kappa: float
    center: tuple[float, ...]
    enclosure: tuple[tuple[float, float], ...]
    certificate: Cert

Other public import paths

• omnibias.core.verified.KrawczykCertificate
• omnibias.core.verified.kantorovich.KrawczykCertificate

CLASS

NKBounds

omnibias.core.verified.NKBoundsSource ↗

class NKBounds

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.

The Newton-Kantorovich bounds feeding the radii polynomial.

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.

Fields & methods

y0field

y0: float

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

View source ↗

z0field

z0: float

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

View source ↗

z1field

z1: float

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

View source ↗

z2field

z2: float

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

View source ↗

Read the implementation

class NKBounds:
    """The Newton-Kantorovich bounds feeding the radii polynomial."""

    y0: float
    z0: float
    z1: float
    z2: float

Other public import paths

• omnibias.core.verified.NKBounds
• omnibias.core.verified.kantorovich.NKBounds

CLASS

RadiiCertificate

omnibias.core.verified.RadiiCertificateSource ↗

class RadiiCertificate

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 verified existence radius from the radii polynomial.

Parameters

Name	Type & default	Contract
radiusdataclass field	floatRequired	See the operation contract and implementation below.
kappadataclass field	floatRequired	See the operation contract and implementation below.
p_valuedataclass field	floatRequired	See the operation contract and implementation below.
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.
r_intervaldataclass field	tuple[float, float]Required	See the operation contract and implementation below.
certificatedataclass field	CertRequired	See the operation contract and implementation below.

Fields & methods

radiusfield

radius: float

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

View source ↗

kappafield

kappa: float

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

View source ↗

p_valuefield

p_value: float

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

View source ↗

y0field

y0: float

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

View source ↗

z0field

z0: float

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

View source ↗

z1field

z1: float

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

View source ↗

z2field

z2: float

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

View source ↗

r_intervalfield

r_interval: tuple[float, float]

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

View source ↗

certificatefield

certificate: Cert

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

View source ↗

Read the implementation

class RadiiCertificate:
    """A verified existence radius from the radii polynomial."""

    radius: float
    kappa: float
    p_value: float
    y0: float
    z0: float
    z1: float
    z2: float
    r_interval: tuple[float, float]
    certificate: Cert

Other public import paths

• omnibias.core.verified.RadiiCertificate
• omnibias.core.verified.kantorovich.RadiiCertificate

FUNCTION

certify_zero_radii

omnibias.core.verified.certify_zero_radiiSource ↗

certify_zero_radii(func: IntervalMap, jacobian: IntervalJac, x_bar: Sequence[float], a_inv: Sequence[Sequence[float]], *, lipschitz_df: float, r_max: float=math.inf) -> RadiiCertificate | None

End-to-end radii-polynomial existence proof for F(x) = 0.

Parameters

Name	Type & default	Contract
funcpositional-or-keyword	IntervalMapRequired	See the operation contract and implementation below.
jacobianpositional-or-keyword	IntervalJacRequired	See the operation contract and implementation below.
x_barpositional-or-keyword	Sequence[float]Required	See the operation contract and implementation below.
a_invpositional-or-keyword	Sequence[Sequence[float]]Required	See the operation contract and implementation below.
lipschitz_dfkeyword-only	floatRequired	See the operation contract and implementation below.
r_maxkeyword-only	floatDefault: math.inf	See the operation contract and implementation below.

ReturnsRadiiCertificate | None

Executed regression · 2d polynomial system radii polynomial

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_2d_polynomial_system_radii_polynomial() -> None:
    root = 1.0 / math.sqrt(2.0)

    def func(v: list[Interval]) -> list[Interval]:
        x, y = v
        return [x * x + y * y - Interval.point(1.0), x - y]

    def jac(v: list[Interval]) -> list[list[Interval]]:
        x, y = v
        two = Interval.point(2.0)
        return [[two * x, two * y], [Interval.point(1.0), Interval.point(-1.0)]]

    j = [[2 * root, 2 * root], [1.0, -1.0]]
    det = j[0][0] * j[1][1] - j[0][1] * j[1][0]
    a_inv = [[j[1][1] / det, -j[0][1] / det], [-j[1][0] / det, j[0][0] / det]]

    # DF is affine in (x,y): ||DF(u)-DF(v)||_inf <= 2||u-v||_inf, so Lipschitz = 2.
    cert = certify_zero_radii(func, jac, [root, root], a_inv, lipschitz_df=2.0)
    assert cert is not None
    assert cert.kappa < 1.0

python -m pytest "packages/omnibias-core/tests/verified/test_kantorovich.py::test_2d_polynomial_system_radii_polynomial" -q

Regression example · radii polynomial synthetic existence

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_radii_polynomial_synthetic_existence() -> None:
    # Y0 small, contraction slack large -> existence with a tiny radius.
    cert = radii_polynomial_certificate(y0=1e-3, z0=0.1, z1=0.0, z2=0.5)
    assert cert is not None
    assert cert.kappa < 1.0
    assert cert.p_value < 0.0
    assert cert.radius > 0.0
    assert verify_certificate_digest(cert.certificate)

python -m pytest packages/omnibias-core/tests/verified/test_kantorovich.py -k test_radii_polynomial_synthetic_existence -q

Read the implementation

def certify_zero_radii(
    func: IntervalMap,
    jacobian: IntervalJac,
    x_bar: Sequence[float],
    a_inv: Sequence[Sequence[float]],
    *,
    lipschitz_df: float,
    r_max: float = math.inf,
) -> RadiiCertificate | None:
    """End-to-end radii-polynomial existence proof for ``F(x) = 0``."""
    bounds = newton_kantorovich_bounds(
        func, jacobian, x_bar, a_inv, lipschitz_df=lipschitz_df
    )
    return radii_polynomial_certificate(
        bounds.y0, bounds.z0, bounds.z1, bounds.z2, r_max=r_max
    )

Related APIsomnibias.core.verified.newton_kantorovich_bounds↗omnibias.core.verified.radii_polynomial_certificate↗

Other public import paths

• omnibias.core.verified.certify_zero_radii
• omnibias.core.verified.kantorovich.certify_zero_radii

FUNCTION

kantorovich_accept_step

omnibias.core.verified.kantorovich_accept_stepSource ↗

kantorovich_accept_step(func: IntervalMap, jacobian: IntervalJac, a_inv: Sequence[Sequence[float]], trial_params: Sequence[float], *, lipschitz_df: float, r_max: float, claim: str=FINITE_RESIDUAL_CLAIM) -> KantorovichAccept

Accept a trial point iff it sits in a nonempty unique-zero ball of F.

Assembles newton_kantorovich_bounds and consults radii_polynomial_certificate. The sealed payload always records continuum_pde_claim: false; theorem_prover_verified is never asserted (sound-enclosure tier). Does not apply the step -- callers keep or discard trial_params from KantorovichAccept.accepted.

Parameters

Name	Type & default	Contract
funcpositional-or-keyword	IntervalMapRequired	See the operation contract and implementation below.
jacobianpositional-or-keyword	IntervalJacRequired	See the operation contract and implementation below.
a_invpositional-or-keyword	Sequence[Sequence[float]]Required	See the operation contract and implementation below.
trial_paramspositional-or-keyword	Sequence[float]Required	See the operation contract and implementation below.
lipschitz_dfkeyword-only	floatRequired	See the operation contract and implementation below.
r_maxkeyword-only	floatRequired	See the operation contract and implementation below.
claimkeyword-only	strDefault: FINITE_RESIDUAL_CLAIM	See the operation contract and implementation below.

ReturnsKantorovichAccept

Explicit validation & failure cases

• When r_max <= 0.0, raises ValueError(f'r_max must be > 0, got {r_max}').
• When float(lipschitz_df) < 0.0, raises ValueError(f'lipschitz_df must be >= 0, got {lipschitz_df}').

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

Executed regression · r max must be positive

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_r_max_must_be_positive() -> None:
    func, jac, lip = polynomial_sqrt2_maps()
    with pytest.raises(ValueError, match="r_max"):
        kantorovich_accept_step(
            func, jac, GOOD_A, [GOOD_TRIAL], lipschitz_df=lip, r_max=0.0
        )

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

Regression example · nonfinite trial is bounds failed

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_nonfinite_trial_is_bounds_failed() -> None:
    func, jac, lip = polynomial_sqrt2_maps()
    decision = kantorovich_accept_step(
        func, jac, GOOD_A, [math.nan], lipschitz_df=lip, r_max=R_MAX
    )
    assert decision.reason == "bounds_failed"

python -m pytest packages/omnibias-core/tests/verified/test_kantorovich_accept.py -k test_nonfinite_trial_is_bounds_failed -q

Read the implementation

def kantorovich_accept_step(
    func: IntervalMap,
    jacobian: IntervalJac,
    a_inv: Sequence[Sequence[float]],
    trial_params: Sequence[float],
    *,
    lipschitz_df: float,
    r_max: float,
    claim: str = FINITE_RESIDUAL_CLAIM,
) -> KantorovichAccept:
    """Accept a trial point iff it sits in a nonempty unique-zero ball of ``F``.

    Assembles :func:`newton_kantorovich_bounds` and consults
    :func:`radii_polynomial_certificate`.  The sealed payload always records
    ``continuum_pde_claim: false``; ``theorem_prover_verified`` is never
    asserted (sound-enclosure tier).  Does not apply the step -- callers keep
    or discard ``trial_params`` from :attr:`KantorovichAccept.accepted`.
    """
    if r_max <= 0.0:
        raise ValueError(f"r_max must be > 0, got {r_max}")
    if float(lipschitz_df) < 0.0:
        raise ValueError(f"lipschitz_df must be >= 0, got {lipschitz_df}")
    trial = [float(v) for v in trial_params]
    if not trial or not all(math.isfinite(v) for v in trial):
        return KantorovichAccept(False, None, "bounds_failed")
    try:
        a_rows = [[float(c) for c in row] for row in a_inv]
        if len(a_rows) != len(trial) or any(len(row) != len(trial) for row in a_rows):
            return KantorovichAccept(False, None, "bounds_failed")
        if not all(math.isfinite(c) for row in a_rows for c in row):
            return KantorovichAccept(False, None, "bounds_failed")
        bounds = newton_kantorovich_bounds(
            func, jacobian, trial, a_rows, lipschitz_df=float(lipschitz_df)
        )
    except (ValueError, ZeroDivisionError, ArithmeticError):
        return KantorovichAccept(False, None, "bounds_failed")
    cert = radii_polynomial_certificate(
        bounds.y0,
        bounds.z0,
        bounds.z1,
        bounds.z2,
        r_max=float(r_max),
        claim=claim,
        honesty={"unproven_claim": False, CONTINUUM_PDE_CLAIM_KEY: False},
        payload_extra={CONTINUUM_PDE_CLAIM_KEY: False, "finite_map": True},
    )
    if cert is None:
        return KantorovichAccept(False, None, "empty")
    return KantorovichAccept(True, cert, "ball")

Related APIsomnibias.core.verified.KantorovichAccept↗omnibias.core.verified.newton_kantorovich_bounds↗omnibias.core.verified.radii_polynomial_certificate↗

Other public import paths

• omnibias.core.verified.kantorovich_accept_step
• omnibias.core.verified.kantorovich.kantorovich_accept_step

FUNCTION

krawczyk_certificate

omnibias.core.verified.krawczyk_certificateSource ↗

krawczyk_certificate(func: IntervalMap, jacobian: IntervalJac, x_bar: Sequence[float], a_inv: Sequence[Sequence[float]], r: float) -> KrawczykCertificate | None

Krawczyk unique-zero test on the box B(x_bar, r) (rigorous).

Returns a certificate iff K(x_bar, X) subset int(X) and ||I - A DF(X)||_inf < 1 -- a unique zero of F then lies in X.

Parameters

Name	Type & default	Contract
funcpositional-or-keyword	IntervalMapRequired	See the operation contract and implementation below.
jacobianpositional-or-keyword	IntervalJacRequired	See the operation contract and implementation below.
x_barpositional-or-keyword	Sequence[float]Required	See the operation contract and implementation below.
a_invpositional-or-keyword	Sequence[Sequence[float]]Required	See the operation contract and implementation below.
rpositional-or-keyword	floatRequired	See the operation contract and implementation below.

ReturnsKrawczykCertificate | None

Explicit validation & failure cases

• When r <= 0.0, raises ValueError('box radius r must be positive').

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

Executed regression · g4 orbit recovery

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_g4_orbit_recovery() -> None:
    rows = orbit_recovery_report()
    assert len(rows) == 3
    assert all(row["recovered"] for row in rows), rows
    for row in rows:
        assert row["jet_enclosure"] is not None
        lo, hi = row["jet_enclosure"][0]
        assert hi >= lo

python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g4_orbit_recovery" -q

Regression example · dottie via krawczyk

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_dottie_via_krawczyk() -> None:
    # F(x) = x - cos(x); F'(x) = 1 + sin(x); A = 1/F'(x_bar).
    x_bar = DOTTIE
    a = 1.0 / (1.0 + math.sin(x_bar))

    def func(xs: list[Interval]) -> list[Interval]:
        return [xs[0] - _cos_iv(xs[0])]

    def jac(xs: list[Interval]) -> list[list[Interval]]:
        return [[Interval.point(1.0) + _sin_iv(xs[0])]]

    cert = krawczyk_certificate(func, jac, [x_bar], [[a]], r=1e-3)
    assert cert is not None
    assert cert.kappa < 1.0
    lo, hi = cert.enclosure[0]
    assert lo <= DOTTIE <= hi  # the true root is inside the certified box

python -m pytest packages/omnibias-core/tests/verified/test_kantorovich.py -k test_dottie_via_krawczyk -q

Read the implementation

def krawczyk_certificate(
    func: IntervalMap,
    jacobian: IntervalJac,
    x_bar: Sequence[float],
    a_inv: Sequence[Sequence[float]],
    r: float,
) -> KrawczykCertificate | None:
    r"""Krawczyk unique-zero test on the box ``B(x_bar, r)`` (rigorous).

    Returns a certificate iff ``K(x_bar, X) subset int(X)`` and
    ``||I - A DF(X)||_inf < 1`` -- a unique zero of ``F`` then lies in ``X``.
    """
    n = len(x_bar)
    if r <= 0.0:
        raise ValueError("box radius r must be positive")
    box = [Interval(x_bar[i] - r, x_bar[i] + r) for i in range(n)]
    a_iv = to_interval_matrix(a_inv)
    fx = [Interval.from_value(v) for v in func([Interval.point(v) for v in x_bar])]
    a_fx = matvec(a_iv, fx)
    j_box = to_interval_matrix([[Interval.from_value(v) for v in row] for row in jacobian(box)])
    m = mat_sub(identity_matrix(n), matmul(a_iv, j_box))  # I - A DF(X)
    diff = [box[i] - Interval.point(x_bar[i]) for i in range(n)]
    m_diff = matvec(m, diff)
    k = [Interval.point(x_bar[i]) - a_fx[i] + m_diff[i] for i in range(n)]
    kappa = inf_norm_matrix(m)
    inside = all(box[i].lo < k[i].lo and k[i].hi < box[i].hi for i in range(n))
    if kappa < 1.0 and inside:
        from omnibias.core.proof.certificate import make_certificate

        enclosure = tuple((k[i].lo, k[i].hi) for i in range(n))
        cert = make_certificate(
            claim="unique zero of F in the Krawczyk box",
            payload={
                "type": "krawczyk",
                "radius": r,
                "kappa": kappa,
                "center": list(x_bar),
                "enclosure": [[lo, hi] for lo, hi in enclosure],
            },
        )
        return KrawczykCertificate(r, kappa, tuple(x_bar), enclosure, cert)
    return None

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

Other public import paths

• omnibias.core.verified.krawczyk_certificate
• omnibias.core.verified.kantorovich.krawczyk_certificate

FUNCTION

krawczyk_search

omnibias.core.verified.krawczyk_searchSource ↗

krawczyk_search(func: IntervalMap, jacobian: IntervalJac, x_bar: Sequence[float], a_inv: Sequence[Sequence[float]], *, radii: Sequence[float]) -> KrawczykCertificate | None

Try krawczyk_certificate over radii (ascending), return the first hit.

Parameters

Name	Type & default	Contract
funcpositional-or-keyword	IntervalMapRequired	See the operation contract and implementation below.
jacobianpositional-or-keyword	IntervalJacRequired	See the operation contract and implementation below.
x_barpositional-or-keyword	Sequence[float]Required	See the operation contract and implementation below.
a_invpositional-or-keyword	Sequence[Sequence[float]]Required	See the operation contract and implementation below.
radiikeyword-only	Sequence[float]Required	See the operation contract and implementation below.

ReturnsKrawczykCertificate | None

Read the implementation

def krawczyk_search(
    func: IntervalMap,
    jacobian: IntervalJac,
    x_bar: Sequence[float],
    a_inv: Sequence[Sequence[float]],
    *,
    radii: Sequence[float],
) -> KrawczykCertificate | None:
    """Try :func:`krawczyk_certificate` over ``radii`` (ascending), return the first hit."""
    for r in radii:
        cert = krawczyk_certificate(func, jacobian, x_bar, a_inv, r)
        if cert is not None:
            return cert
    return None

Related APIsomnibias.core.verified.krawczyk_certificate↗

Other public import paths

• omnibias.core.verified.krawczyk_search
• omnibias.core.verified.kantorovich.krawczyk_search

FUNCTION

newton_kantorovich_bounds

omnibias.core.verified.newton_kantorovich_boundsSource ↗

newton_kantorovich_bounds(func: IntervalMap, jacobian: IntervalJac, x_bar: Sequence[float], a_inv: Sequence[Sequence[float]], *, lipschitz_df: float) -> NKBounds

Compute (Y0, Z0, Z1, Z2) for the radii polynomial.

lipschitz_df is a rigorous bound on ||DF(x) - DF(y)||_inf per unit ||x - y||_inf over the region of interest (explicit for polynomial maps). Z2 = ||A||_inf * lipschitz_df; Z1 = 0 (the linearisation we invert is DF(x_bar) itself, whose enclosure folds into Z0).

Parameters

Name	Type & default	Contract
funcpositional-or-keyword	IntervalMapRequired	See the operation contract and implementation below.
jacobianpositional-or-keyword	IntervalJacRequired	See the operation contract and implementation below.
x_barpositional-or-keyword	Sequence[float]Required	See the operation contract and implementation below.
a_invpositional-or-keyword	Sequence[Sequence[float]]Required	See the operation contract and implementation below.
lipschitz_dfkeyword-only	floatRequired	See the operation contract and implementation below.

ReturnsNKBounds

Executed regression · select keeps trial on accept

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

Full file, imports & fixtures ↗

def test_select_keeps_trial_on_accept() -> None:
    func, jac, lip = polynomial_sqrt2_maps()
    decision = kantorovich_accept_step(
        func, jac, GOOD_A, [GOOD_TRIAL], lipschitz_df=lip, r_max=R_MAX
    )
    chosen = select_accepted_params([0.25], [GOOD_TRIAL], decision)
    assert chosen == [GOOD_TRIAL]

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

Regression example · dottie via radii polynomial

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_dottie_via_radii_polynomial() -> None:
    # Hand-derived rigorous bounds: |F''(x)| = |cos x| <= 1 everywhere, so the
    # Lipschitz constant of F' is 1 and Z2 = ||A|| * 1.
    x_bar = DOTTIE
    a = 1.0 / (1.0 + math.sin(x_bar))

    def func(xs: list[Interval]) -> list[Interval]:
        return [xs[0] - _cos_iv(xs[0])]

    def jac(xs: list[Interval]) -> list[list[Interval]]:
        return [[Interval.point(1.0) + _sin_iv(xs[0])]]

    bounds = newton_kantorovich_bounds(func, jac, [x_bar], [[a]], lipschitz_df=1.0)
    assert bounds.y0 < 1e-6  # x_bar is an excellent approximation
    cert = radii_polynomial_certificate(bounds.y0, bounds.z0, bounds.z1, bounds.z2)
    assert cert is not None
    # The unique root lies within radius of x_bar; check it brackets Dottie.
    assert abs(DOTTIE - x_bar) <= cert.radius

python -m pytest packages/omnibias-core/tests/verified/test_kantorovich.py -k test_dottie_via_radii_polynomial -q

Read the implementation

def newton_kantorovich_bounds(
    func: IntervalMap,
    jacobian: IntervalJac,
    x_bar: Sequence[float],
    a_inv: Sequence[Sequence[float]],
    *,
    lipschitz_df: float,
) -> NKBounds:
    r"""Compute ``(Y0, Z0, Z1, Z2)`` for the radii polynomial.

    ``lipschitz_df`` is a rigorous bound on ``||DF(x) - DF(y)||_inf`` per unit
    ``||x - y||_inf`` over the region of interest (explicit for polynomial maps).
    ``Z2 = ||A||_inf * lipschitz_df``; ``Z1 = 0`` (the linearisation we invert is
    ``DF(x_bar)`` itself, whose enclosure folds into ``Z0``).
    """
    n = len(x_bar)
    a_iv = to_interval_matrix(a_inv)
    center = [Interval.point(v) for v in x_bar]
    fx = [Interval.from_value(v) for v in func(center)]
    y0 = inf_norm_vector(matvec(a_iv, fx))
    jc = to_interval_matrix([[Interval.from_value(v) for v in row] for row in jacobian(center)])
    z0 = inf_norm_matrix(mat_sub(identity_matrix(n), matmul(a_iv, jc)))
    z2 = Interval.point(inf_norm_matrix(a_iv)) * Interval.point(float(lipschitz_df))
    return NKBounds(y0=y0, z0=z0, z1=0.0, z2=z2.hi)

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

Other public import paths

• omnibias.core.verified.newton_kantorovich_bounds
• omnibias.core.verified.kantorovich.newton_kantorovich_bounds

FUNCTION

polynomial_sqrt2_maps

omnibias.core.verified.polynomial_sqrt2_mapsSource ↗

polynomial_sqrt2_maps() -> tuple[IntervalMap, IntervalJac, float]

Worked example F(x) = x^2 - 2 with Lipschitz constant Lip(DF) = 2.

F''(x) = 2 constantly, so ||DF(x) - DF(y)||_inf = 2 |x - y|.

Returnstuple[IntervalMap, IntervalJac, float]

Executed regression · r max must be positive

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_r_max_must_be_positive() -> None:
    func, jac, lip = polynomial_sqrt2_maps()
    with pytest.raises(ValueError, match="r_max"):
        kantorovich_accept_step(
            func, jac, GOOD_A, [GOOD_TRIAL], lipschitz_df=lip, r_max=0.0
        )

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

Regression example · nonfinite trial is bounds failed

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_nonfinite_trial_is_bounds_failed() -> None:
    func, jac, lip = polynomial_sqrt2_maps()
    decision = kantorovich_accept_step(
        func, jac, GOOD_A, [math.nan], lipschitz_df=lip, r_max=R_MAX
    )
    assert decision.reason == "bounds_failed"

python -m pytest packages/omnibias-core/tests/verified/test_kantorovich_accept.py -k test_nonfinite_trial_is_bounds_failed -q

Read the implementation

def polynomial_sqrt2_maps() -> tuple[IntervalMap, IntervalJac, float]:
    """Worked example ``F(x) = x^2 - 2`` with Lipschitz constant ``Lip(DF) = 2``.

    ``F''(x) = 2`` constantly, so ``||DF(x) - DF(y)||_inf = 2 |x - y|``.
    """

    two = Interval.point(2.0)

    def func(xs: list[Interval]) -> list[Interval]:
        x = xs[0]
        return [x * x - two]

    def jacobian(xs: list[Interval]) -> list[list[Interval]]:
        return [[two * xs[0]]]

    return func, jacobian, 2.0

Other public import paths

• omnibias.core.verified.polynomial_sqrt2_maps
• omnibias.core.verified.kantorovich.polynomial_sqrt2_maps

FUNCTION

radii_polynomial_certificate

omnibias.core.verified.radii_polynomial_certificateSource ↗

radii_polynomial_certificate(y0: float, z0: float, z1: float, z2: float, *, r_max: float=math.inf, claim: str='unique zero in closed ball B(x_bar, r)', honesty: Mapping[str, bool] | None=None, payload_extra: Mapping[str, Any] | None=None) -> RadiiCertificate | None

Verify the radii polynomial and return an existence certificate, or None.

y0, z0, z1, z2 must be rigorous **upper** bounds. Returns None when no admissible radius exists (no contraction, or the discriminant is non-positive).

Parameters

Name	Type & default	Contract
y0positional-or-keyword	floatRequired	See the operation contract and implementation below.
z0positional-or-keyword	floatRequired	See the operation contract and implementation below.
z1positional-or-keyword	floatRequired	See the operation contract and implementation below.
z2positional-or-keyword	floatRequired	See the operation contract and implementation below.
r_maxkeyword-only	floatDefault: math.inf	See the operation contract and implementation below.
claimkeyword-only	strDefault: 'unique zero in closed ball B(x_bar, r)'	See the operation contract and implementation below.
honestykeyword-only	Mapping[str, bool] | NoneDefault: None	See the operation contract and implementation below.
payload_extrakeyword-only	Mapping[str, Any] | NoneDefault: None	See the operation contract and implementation below.

ReturnsRadiiCertificate | None

Explicit validation & failure cases

• When min(y0, z0, z1, z2) < 0.0, raises ValueError('radii-polynomial bounds must be non-negative').

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

Executed regression · radii bridge no contraction returns none

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_radii_bridge_no_contraction_returns_none() -> None:
    # huge defect -> discriminant negative -> no certificate.
    assert radii_polynomial_residual_certificate(10.0, 0.1, 0.0, 0.5) is None

python -m pytest "packages/omnibias-core/tests/test_verified_pde_certificate.py::test_radii_bridge_no_contraction_returns_none" -q

Regression example · radii polynomial no contraction returns none

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_radii_polynomial_no_contraction_returns_none() -> None:
    # Z0 + Z1 >= 1: no contraction possible.
    assert radii_polynomial_certificate(y0=0.1, z0=0.9, z1=0.2, z2=0.5) is None
    # Discriminant negative: Y0 too large for the available slack.
    assert radii_polynomial_certificate(y0=10.0, z0=0.0, z1=0.0, z2=1.0) is None

python -m pytest packages/omnibias-core/tests/verified/test_kantorovich.py -k test_radii_polynomial_no_contraction_returns_none -q

Read the implementation

def radii_polynomial_certificate(
    y0: float,
    z0: float,
    z1: float,
    z2: float,
    *,
    r_max: float = math.inf,
    claim: str = "unique zero in closed ball B(x_bar, r)",
    honesty: Mapping[str, bool] | None = None,
    payload_extra: Mapping[str, Any] | None = None,
) -> RadiiCertificate | None:
    r"""Verify the radii polynomial and return an existence certificate, or ``None``.

    ``y0, z0, z1, z2`` must be rigorous **upper** bounds.  Returns ``None`` when no
    admissible radius exists (no contraction, or the discriminant is non-positive).
    """
    y0, z0, z1, z2 = float(y0), float(z0), float(z1), float(z2)
    if min(y0, z0, z1, z2) < 0.0:
        raise ValueError("radii-polynomial bounds must be non-negative")
    slack = 1.0 - z0 - z1
    if slack <= 0.0:
        return None

    if z2 == 0.0:
        r_lo = y0 / slack
        r_hi = r_max
        candidates = [r_lo * (1.0 + t) for t in (1e-6, 1e-3, 1e-2, 0.1, 0.5, 1.0)]
    else:
        disc = slack * slack - 4.0 * z2 * y0
        if disc <= 0.0:
            return None
        s = math.sqrt(disc)
        r_lo = (slack - s) / (2.0 * z2)
        r_hi = (slack + s) / (2.0 * z2)
        vertex = slack / (2.0 * z2)
        candidates = [r_lo + frac * (vertex - r_lo) for frac in (0.25, 0.5, 0.1, 0.75, 0.9)]

    from omnibias.core.proof.certificate import make_certificate

    yi, z0i, z1i, z2i = (Interval.point(v) for v in (y0, z0, z1, z2))
    two = Interval.point(2.0)
    for r0 in candidates:
        if not (r0 > 0.0 and r0 <= r_max):
            continue
        ri = Interval.point(r0)
        p = yi + (z0i + z1i) * ri + z2i * ri * ri - ri
        kappa = z0i + z1i + two * z2i * ri
        if p.hi < 0.0 and kappa.hi < 1.0:
            payload: dict[str, Any] = {
                "type": "radii_polynomial",
                "radius": r0,
                "kappa": kappa.hi,
                "p_value": p.hi,
                "Y0": y0,
                "Z0": z0,
                "Z1": z1,
                "Z2": z2,
            }
            if payload_extra:
                payload.update(dict(payload_extra))
            cert = make_certificate(
                claim=claim,
                payload=payload,
                honesty=honesty,
            )
            return RadiiCertificate(r0, kappa.hi, p.hi, y0, z0, z1, z2, (r_lo, r_hi), cert)
    return None

Related APIsomnibias.core.verified.RadiiCertificate↗

Other public import paths

• omnibias.core.verified.radii_polynomial_certificate
• omnibias.core.verified.kantorovich.radii_polynomial_certificate

FUNCTION

select_accepted_params

omnibias.core.verified.select_accepted_paramsSource ↗

select_accepted_params(current: Sequence[float], trial: Sequence[float], decision: KantorovichAccept) -> list[float]

Return trial on a unique-zero ball, otherwise keep current.

Parameters

Name	Type & default	Contract
currentpositional-or-keyword	Sequence[float]Required	See the operation contract and implementation below.
trialpositional-or-keyword	Sequence[float]Required	See the operation contract and implementation below.
decisionpositional-or-keyword	KantorovichAcceptRequired	See the operation contract and implementation below.

Returnslist[float]

Executed regression · select keeps trial on accept

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

Full file, imports & fixtures ↗

def test_select_keeps_trial_on_accept() -> None:
    func, jac, lip = polynomial_sqrt2_maps()
    decision = kantorovich_accept_step(
        func, jac, GOOD_A, [GOOD_TRIAL], lipschitz_df=lip, r_max=R_MAX
    )
    chosen = select_accepted_params([0.25], [GOOD_TRIAL], decision)
    assert chosen == [GOOD_TRIAL]

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

Regression example · g1 reject named far point

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_g1_reject_named_far_point() -> None:
    func, jac, lip = polynomial_sqrt2_maps()
    decision = kantorovich_accept_step(
        func, jac, GOOD_A, [FAR_TRIAL], lipschitz_df=lip, r_max=R_MAX
    )
    assert decision.accepted is False
    assert decision.reason == "empty"
    assert decision.certificate is None
    kept = select_accepted_params([0.0], [FAR_TRIAL], decision)
    assert kept == [0.0]

python -m pytest packages/omnibias-core/tests/verified/test_kantorovich_accept.py -k test_g1_reject_named_far_point -q

Read the implementation

def select_accepted_params(
    current: Sequence[float],
    trial: Sequence[float],
    decision: KantorovichAccept,
) -> list[float]:
    """Return ``trial`` on a unique-zero ball, otherwise keep ``current``."""
    chosen = trial if decision.accepted else current
    return [float(v) for v in chosen]

Other public import paths

• omnibias.core.verified.select_accepted_params
• omnibias.core.verified.kantorovich.select_accepted_params

← Package overviewRunnable learning examples →