omnibias.core.verified.pde_certificate

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

Module contract & mathematical conventions

End-to-end wiring: trained network / spectral ansatz -> certified PDE residual.

This module is the *adaptor* that turns the verified primitives into a sealed ~omnibias.core.proof.certificate.Cert. It connects three pieces that already exist in omnibias.core.verified:

#. the **certified jet** (~omnibias.core.verified.jet_mv.certified_partials) -- rigorous enclosures of every mixed partial of a deep MLP over an input box; #. the **radii-polynomial / Newton-Kantorovich** closure (~omnibias.core.verified.kantorovich.radii_polynomial_certificate); #. the validated **Fourier algebra** (~omnibias.core.verified.fourier.ValidatedFourierSeries) for the spectral / nonlocal route.

Two complementary, fully-rigorous certificates are produced.

A-posteriori error bound (physical-space / trained MLP)

For a *linear, well-posed* boundary-value problem L u = f in Omega with u = g on dOmega and a rigorous **stability constant** pair (C_Omega, C_dOmega) such that

\|v\|_\infty \le C_\Omega\,\|L v\|_{\infty,\Omega} + C_{\partial\Omega}\,\|v\|_{\infty,\partial\Omega} \qquad \forall v,

applying the estimate to v = u_NN - u_true gives the certified bound

\|u_{NN} - u_{\text{true}}\|_\infty \le C_\Omega\,R_{\text{int}} + C_{\partial\Omega}\,R_{\text{bnd}},

where R_int = sup_Omega |L u_NN - f| and R_bnd = sup_{dOmega} |u_NN - g| are computed *rigorously* from the certified jet (box subdivision tightens both). The stability constants are the caller's proof obligation -- they are recorded in the certificate, not invented here.

Radii-polynomial existence (spectral / finite ansatz)

radii_polynomial_residual_certificate feeds a certified residual as the Newton-Kantorovich defect Y0 into the radii polynomial, proving a *true* solution exists in an explicit ball around the approximation when the contraction data (Z0, Z1, Z2) is supplied. spectral_residual_norm assembles the residual F(a) = L a + Q(a) - rhs of a band-limited Fourier ansatz with the validated algebra and returns its rigorous l1_nu norm -- the natural Y0 for a steady / self-similar spectral profile.

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

AdaptiveResidualDiagnostics

omnibias.core.verified.pde_certificate.AdaptiveResidualDiagnosticsSource ↗

class AdaptiveResidualDiagnostics

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.

Diagnostics from adaptive residual subdivision.

Parameters

Name	Type & default	Contract
`residual`dataclass field	`Interval`Required	See the operation contract and implementation below.
`residual_sup`dataclass field	`float`Required	See the operation contract and implementation below.
`splits`dataclass field	`tuple[int, ...]`Required	See the operation contract and implementation below.
`boxes`dataclass field	`int`Required	See the operation contract and implementation below.
`iterations`dataclass field	`int`Required	See the operation contract and implementation below.
`target`dataclass field	`float \| None`Required	See the operation contract and implementation below.
`reached_target`dataclass field	`bool`Required	See the operation contract and implementation below.
`max_box_width`dataclass field	`float`Required	See the operation contract and implementation below.

Fields & methods

residualfield

residual: Interval

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

View source ↗

residual_supfield

residual_sup: float

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

View source ↗

splitsfield

splits: tuple[int, ...]

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

View source ↗

boxesfield

boxes: int

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

View source ↗

iterationsfield

iterations: int

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

View source ↗

targetfield

target: float | None

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

View source ↗

reached_targetfield

reached_target: bool

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

View source ↗

max_box_widthfield

max_box_width: float

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

View source ↗

to_payloadmethod

to_payload(self) -> dict[str, object]

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

Returns: dict[str, object]

Method implementation

    def to_payload(self) -> dict[str, object]:
        return {
            "residual_enclosure": [self.residual.lo, self.residual.hi],
            "residual_sup": float(self.residual_sup),
            "splits": list(self.splits),
            "boxes": int(self.boxes),
            "iterations": int(self.iterations),
            "target": None if self.target is None else float(self.target),
            "reached_target": bool(self.reached_target),
            "max_box_width": float(self.max_box_width),
        }

View source ↗

Read the implementation

class AdaptiveResidualDiagnostics:
    """Diagnostics from adaptive residual subdivision."""

    residual: Interval
    residual_sup: float
    splits: tuple[int, ...]
    boxes: int
    iterations: int
    target: float | None
    reached_target: bool
    max_box_width: float

    def to_payload(self) -> dict[str, object]:
        return {
            "residual_enclosure": [self.residual.lo, self.residual.hi],
            "residual_sup": float(self.residual_sup),
            "splits": list(self.splits),
            "boxes": int(self.boxes),
            "iterations": int(self.iterations),
            "target": None if self.target is None else float(self.target),
            "reached_target": bool(self.reached_target),
            "max_box_width": float(self.max_box_width),
        }

CLASS

BoundaryFace

omnibias.core.verified.BoundaryFaceSource ↗

class BoundaryFace

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

One boundary patch: a (typically degenerate) box plus the target g.

Parameters

Name	Type & default	Contract
`box`dataclass field	`BoxLike`Required	See the operation contract and implementation below.
`target`dataclass field	`Coeff`Default: 0.0	See the operation contract and implementation below.

Regression example · boundary residual encloses face values

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_boundary_residual_encloses_face_values() -> None:
    # right edge x = 1, y in [-1, 1], target g = 0  ->  residual = u_NN on the face.
    face = BoundaryFace([(1.0, 1.0), (-1.0, 1.0)], 0.0)
    r = certified_boundary_residual(_AFFINE, [face], splits=4)
    for y in (-0.5, 0.0, 0.5):
        assert r.lo <= _u_affine(1.0, y) <= r.hi

python -m pytest packages/omnibias-core/tests/test_verified_pde_certificate.py -k test_boundary_residual_encloses_face_values -q

Regression example · aposteriori combines residuals

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_aposteriori_combines_residuals() -> None:
    net = _tanh_net()
    face = BoundaryFace([(1.0, 1.0), (-1.0, 1.0)], 0.0)
    ci, cb = 0.7, 1.3
    cert = aposteriori_error_certificate(
        net,
        _DOMAIN,
        laplace(2),
        boundary=[face],
        stability_interior=ci,
        stability_boundary=cb,
        splits=2,
        boundary_splits=3,
    )
    r_int = certified_interior_residual(net, _DOMAIN, laplace(2), splits=2).mag
    r_bnd = certified_boundary_residual(net, [face], splits=3).mag
    expected = (
        Interval.point(ci) * Interval.point(r_int)
        + Interval.point(cb) * Interval.point(r_bnd)
    ).hi
    assert cert.interior_residual == r_int
    assert cert.boundary_residual == r_bnd
    assert cert.error_bound == pytest.approx(expected, rel=1e-12, abs=1e-15)

python -m pytest packages/omnibias-core/tests/test_verified_pde_certificate.py -k test_aposteriori_combines_residuals -q

Fields & methods

boxfield

box: BoxLike

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

View source ↗

targetfield

target: Coeff = 0.0

Declared Coeff field on BoundaryFace. Default expression: 0.0.

View source ↗

Read the implementation

class BoundaryFace:
    """One boundary patch: a (typically degenerate) box plus the target ``g``."""

    box: BoxLike
    target: Coeff = 0.0

Other public import paths

omnibias.core.verified.BoundaryFace
omnibias.core.verified.pde_certificate.BoundaryFace

CONSTANT

CertifiedResidualCallback

omnibias.core.verified.pde_certificate.CertifiedResidualCallbackSource ↗

CertifiedResidualCallback = Callable[[Sequence[Interval], Mapping[MultiIndex, Sequence[Interval]]], IntervalLike]

Experimental nonlinear / custom residual callback. It receives the current sub-box and the certified partial dictionary produced for that box.

Read the implementation

CertifiedResidualCallback = Callable[
    [Sequence[Interval], Mapping[MultiIndex, Sequence[Interval]]], IntervalLike
]

CONSTANT

Coeff

omnibias.core.verified.CoeffSource ↗

Coeff = IntervalLike | Callable[[Sequence[Interval]], IntervalLike]

A PDE coefficient / source: a constant or a function of the (sub-)box.

Read the implementation

Coeff = IntervalLike | Callable[[Sequence[Interval]], IntervalLike]

Other public import paths

omnibias.core.verified.Coeff
omnibias.core.verified.pde_certificate.Coeff

CLASS

LinearPDE

omnibias.core.verified.LinearPDESource ↗

class LinearPDE

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 linear differential operator L u - f as a residual functional.

terms maps a multi-index alpha to its coefficient c_alpha (a constant or a box -> value callable for variable coefficients), encoding L u = sum_alpha c_alpha D^alpha u. source is f (constant or box -> value). residual evaluates a rigorous enclosure of L u(x) - f(x) over a box from a certified-partials dictionary.

Parameters

Name	Type & default	Contract
`terms`dataclass field	`Mapping[MultiIndex, Coeff]`Required	See the operation contract and implementation below.
`source`dataclass field	`Coeff`Default: 0.0	See the operation contract and implementation below.
`component`dataclass field	`int`Default: 0	See the operation contract and implementation below.

Executed regression · required order

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_required_order() -> None:
    assert laplace(2).required_order() == 2
    assert advection_diffusion(2, [1.0, 1.0], 0.5).required_order() == 2
    assert LinearPDE({}, source=3.0).required_order() == 0  # pure source

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

Fields & methods

termsfield

terms: Mapping[MultiIndex, Coeff]

Declared Mapping[MultiIndex, Coeff] field on LinearPDE. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

sourcefield

source: Coeff = 0.0

Declared Coeff field on LinearPDE. Default expression: 0.0.

View source ↗

componentfield

component: int = 0

Declared int field on LinearPDE. Default expression: 0.

View source ↗

required_ordermethod

required_order(self) -> int

Lowest jet order that contains every derivative the operator needs.

Returns: int

Executed regression · required order

Full file, imports & fixtures ↗

def test_required_order() -> None:
    assert laplace(2).required_order() == 2
    assert advection_diffusion(2, [1.0, 1.0], 0.5).required_order() == 2
    assert LinearPDE({}, source=3.0).required_order() == 0  # pure source

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

Method implementation

    def required_order(self) -> int:
        """Lowest jet order that contains every derivative the operator needs."""
        if not self.terms:
            return 0
        return max(sum(alpha) for alpha in self.terms)

View source ↗

residualmethod

residual(self, box: Sequence[Interval], partials: Mapping[MultiIndex, Sequence[Interval]]) -> Interval

Enclosure of L u - f over box from the certified partials.

Parameters

Name	Type & default	Contract
`box`positional-or-keyword	`Sequence[Interval]`Required	See the operation contract and implementation below.
`partials`positional-or-keyword	`Mapping[MultiIndex, Sequence[Interval]]`Required	See the operation contract and implementation below.

Returns: Interval

Executed regression · screened poisson sign

Full file, imports & fixtures ↗

def test_screened_poisson_sign() -> None:
    pde = screened_poisson(2, 2.0, 0.0)  # lap u - 4 u = -4 u  for affine
    x, y = 0.5, 0.5
    r = certified_interior_residual(_AFFINE, [(x, x), (y, y)], pde)
    assert r.lo <= -4.0 * _u_affine(x, y) <= r.hi

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

Method implementation

    def residual(
        self, box: Sequence[Interval], partials: Mapping[MultiIndex, Sequence[Interval]]
    ) -> Interval:
        """Enclosure of ``L u - f`` over ``box`` from the certified partials."""
        acc = Interval.point(0.0)
        for alpha, coeff in self.terms.items():
            row = partials[alpha]
            acc = acc + _eval_coeff(coeff, box) * row[self.component]
        return acc - _eval_coeff(self.source, box)

View source ↗

Read the implementation

class LinearPDE:
    r"""A linear differential operator ``L u - f`` as a residual functional.

    ``terms`` maps a multi-index ``alpha`` to its coefficient ``c_alpha`` (a
    constant or a ``box -> value`` callable for variable coefficients), encoding
    ``L u = sum_alpha c_alpha D^alpha u``.  ``source`` is ``f`` (constant or
    ``box -> value``).  :meth:`residual` evaluates a rigorous enclosure of
    ``L u(x) - f(x)`` over a box from a certified-partials dictionary.
    """

    terms: Mapping[MultiIndex, Coeff]
    source: Coeff = 0.0
    component: int = 0

    def required_order(self) -> int:
        """Lowest jet order that contains every derivative the operator needs."""
        if not self.terms:
            return 0
        return max(sum(alpha) for alpha in self.terms)

    def residual(
        self, box: Sequence[Interval], partials: Mapping[MultiIndex, Sequence[Interval]]
    ) -> Interval:
        """Enclosure of ``L u - f`` over ``box`` from the certified partials."""
        acc = Interval.point(0.0)
        for alpha, coeff in self.terms.items():
            row = partials[alpha]
            acc = acc + _eval_coeff(coeff, box) * row[self.component]
        return acc - _eval_coeff(self.source, box)

Other public import paths

omnibias.core.verified.LinearPDE
omnibias.core.verified.pde_certificate.LinearPDE

CLASS

PINNErrorCertificate

omnibias.core.verified.PINNErrorCertificateSource ↗

class PINNErrorCertificate

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 sealed a-posteriori sup-norm error bound for a trained network.

Parameters

Name	Type & default	Contract
`error_bound`dataclass field	`float`Required	See the operation contract and implementation below.
`interior_residual`dataclass field	`float`Required	See the operation contract and implementation below.
`boundary_residual`dataclass field	`float`Required	See the operation contract and implementation below.
`certificate`dataclass field	`Cert`Required	See the operation contract and implementation below.
`diagnostics`dataclass field	`AdaptiveResidualDiagnostics \| None`Default: None	See the operation contract and implementation below.

Fields & methods

error_boundfield

error_bound: float

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

View source ↗

interior_residualfield

interior_residual: float

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

View source ↗

boundary_residualfield

boundary_residual: float

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

View source ↗

certificatefield

certificate: Cert

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

View source ↗

diagnosticsfield

diagnostics: AdaptiveResidualDiagnostics | None = None

Declared AdaptiveResidualDiagnostics | None field on PINNErrorCertificate. Default expression: None.

View source ↗

Read the implementation

class PINNErrorCertificate:
    """A sealed a-posteriori sup-norm error bound for a trained network."""

    error_bound: float
    interior_residual: float
    boundary_residual: float
    certificate: Cert
    diagnostics: AdaptiveResidualDiagnostics | None = None

Other public import paths

omnibias.core.verified.PINNErrorCertificate
omnibias.core.verified.pde_certificate.PINNErrorCertificate

CLASS

StabilityEstimate

omnibias.core.verified.pde_certificate.StabilityEstimateSource ↗

class StabilityEstimate

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.

Provenance for the constants in the a-posteriori PDE estimate.

The constants remain mathematical proof obligations. This record prevents a certificate from carrying anonymous numbers by recording their source, assumptions, and whether they were supplied by the caller or a library helper.

Parameters

Name	Type & default	Contract
`interior`dataclass field	`float`Required	See the operation contract and implementation below.
`boundary`dataclass field	`float`Required	See the operation contract and implementation below.
`source`dataclass field	`str`Default: 'user_supplied'	See the operation contract and implementation below.
`pde_family`dataclass field	`str`Default: 'unspecified'	See the operation contract and implementation below.
`domain`dataclass field	`str`Default: 'unspecified'	See the operation contract and implementation below.
`assumptions`dataclass field	`tuple[str, ...]`Default: ()	See the operation contract and implementation below.
`library_provided`dataclass field	`bool`Default: False	See the operation contract and implementation below.

Executed regression · aposteriori negative stability raises

Full file, imports & fixtures ↗

def test_aposteriori_negative_stability_raises() -> None:
    with pytest.raises(ValueError):
        aposteriori_error_certificate(
            _AFFINE,
            _DOMAIN,
            laplace(2),
            stability_interior=-1.0,
            stability_boundary=1.0,
        )

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

Fields & methods

interiorfield

interior: float

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

View source ↗

boundaryfield

boundary: float

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

View source ↗

sourcefield

source: str = 'user_supplied'

Declared str field on StabilityEstimate. Default expression: 'user_supplied'.

View source ↗

pde_familyfield

pde_family: str = 'unspecified'

Declared str field on StabilityEstimate. Default expression: 'unspecified'.

View source ↗

domainfield

domain: str = 'unspecified'

Declared str field on StabilityEstimate. Default expression: 'unspecified'.

View source ↗

assumptionsfield

assumptions: tuple[str, ...] = ()

Declared tuple[str, ...] field on StabilityEstimate. Default expression: ().

View source ↗

library_providedfield

library_provided: bool = False

Declared bool field on StabilityEstimate. Default expression: False.

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.interior < 0.0 or self.boundary < 0.0, raises ValueError('stability constants must be non-negative').

Executed regression · aposteriori negative stability raises

Full file, imports & fixtures ↗

def test_aposteriori_negative_stability_raises() -> None:
    with pytest.raises(ValueError):
        aposteriori_error_certificate(
            _AFFINE,
            _DOMAIN,
            laplace(2),
            stability_interior=-1.0,
            stability_boundary=1.0,
        )

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

Method implementation

    def __post_init__(self) -> None:
        if self.interior < 0.0 or self.boundary < 0.0:
            raise ValueError("stability constants must be non-negative")

View source ↗

to_payloadmethod

to_payload(self) -> dict[str, object]

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

Returns: dict[str, object]

Executed regression · pinn schema rejects forged structural claim

Full file, imports & fixtures ↗

def test_pinn_schema_rejects_forged_structural_claim() -> None:
    cert = aposteriori_error_certificate(
        _AFFINE,
        _DOMAIN,
        laplace(2),
        stability_interior=1.0,
        stability_boundary=1.0,
        splits=2,
    ).certificate
    cert["payload"]["invariants"] = [{"kind": "divergence_free", "certified": True}]
    assert any("expression" in err for err in pinn_aposteriori_schema_errors(cert))

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

Method implementation

    def to_payload(self) -> dict[str, object]:
        return {
            "interior": float(self.interior),
            "boundary": float(self.boundary),
            "source": self.source,
            "pde_family": self.pde_family,
            "domain": self.domain,
            "assumptions": list(self.assumptions),
            "library_provided": bool(self.library_provided),
        }

View source ↗

Read the implementation

class StabilityEstimate:
    r"""Provenance for the constants in the a-posteriori PDE estimate.

    The constants remain mathematical proof obligations.  This record prevents a
    certificate from carrying anonymous numbers by recording their source,
    assumptions, and whether they were supplied by the caller or a library helper.
    """

    interior: float
    boundary: float
    source: str = "user_supplied"
    pde_family: str = "unspecified"
    domain: str = "unspecified"
    assumptions: tuple[str, ...] = ()
    library_provided: bool = False

    def __post_init__(self) -> None:
        if self.interior < 0.0 or self.boundary < 0.0:
            raise ValueError("stability constants must be non-negative")

    def to_payload(self) -> dict[str, object]:
        return {
            "interior": float(self.interior),
            "boundary": float(self.boundary),
            "source": self.source,
            "pde_family": self.pde_family,
            "domain": self.domain,
            "assumptions": list(self.assumptions),
            "library_provided": bool(self.library_provided),
        }

CLASS

StructuralInvariant

omnibias.core.verified.pde_certificate.StructuralInvariantSource ↗

class StructuralInvariant

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 structural identity recorded in a certificate payload.

Parameters

Name	Type & default	Contract
`kind`dataclass field	`str`Required	See the operation contract and implementation below.
`expression`dataclass field	`str`Required	See the operation contract and implementation below.
`certified`dataclass field	`bool`Default: True	See the operation contract and implementation below.
`assumptions`dataclass field	`tuple[str, ...]`Default: ()	See the operation contract and implementation below.
`method`dataclass field	`str`Default: 'structural_identity'	See the operation contract and implementation below.

Executed regression · aposteriori records stability invariants and formal margin

Full file, imports & fixtures ↗

def test_aposteriori_records_stability_invariants_and_formal_margin() -> None:
    stability = user_stability_estimate(
        0.5,
        1.0,
        source="maximum-principle fixture",
        pde_family="laplace",
        domain="unit-square",
        assumptions=("linear well-posed BVP",),
    )
    inv = structural_invariant(
        "streamfunction_2d",
        "u = d_y psi, v = -d_x psi => div u = 0",
        assumptions=("mixed partials commute",),
    )
    cert = aposteriori_error_certificate(
        _AFFINE,
        _DOMAIN,
        laplace(2),
        stability=stability,
        invariants=[inv],
        max_error=1e-6,
        splits=2,
    )
    payload = cert.certificate["payload"]
    assert payload["stability"]["source"] == "maximum-principle fixture"
    assert payload["invariants"][0]["kind"] == "streamfunction_2d"
    assert payload["finite_obligation"]["type"] == "error_bound_le_threshold"
    assert generate_obligation(cert.certificate) is not None

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

Fields & methods

kindfield

kind: str

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

View source ↗

expressionfield

expression: str

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

View source ↗

certifiedfield

certified: bool = True

Declared bool field on StructuralInvariant. Default expression: True.

View source ↗

assumptionsfield

assumptions: tuple[str, ...] = ()

Declared tuple[str, ...] field on StructuralInvariant. Default expression: ().

View source ↗

methodfield

method: str = 'structural_identity'

Declared str field on StructuralInvariant. Default expression: 'structural_identity'.

View source ↗

to_payloadmethod

to_payload(self) -> dict[str, object]

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

Returns: dict[str, object]

Executed regression · aposteriori records stability invariants and formal margin

Full file, imports & fixtures ↗

def test_aposteriori_records_stability_invariants_and_formal_margin() -> None:
    stability = user_stability_estimate(
        0.5,
        1.0,
        source="maximum-principle fixture",
        pde_family="laplace",
        domain="unit-square",
        assumptions=("linear well-posed BVP",),
    )
    inv = structural_invariant(
        "streamfunction_2d",
        "u = d_y psi, v = -d_x psi => div u = 0",
        assumptions=("mixed partials commute",),
    )
    cert = aposteriori_error_certificate(
        _AFFINE,
        _DOMAIN,
        laplace(2),
        stability=stability,
        invariants=[inv],
        max_error=1e-6,
        splits=2,
    )
    payload = cert.certificate["payload"]
    assert payload["stability"]["source"] == "maximum-principle fixture"
    assert payload["invariants"][0]["kind"] == "streamfunction_2d"
    assert payload["finite_obligation"]["type"] == "error_bound_le_threshold"
    assert generate_obligation(cert.certificate) is not None

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

Method implementation

    def to_payload(self) -> dict[str, object]:
        return {
            "kind": self.kind,
            "expression": self.expression,
            "certified": bool(self.certified),
            "assumptions": list(self.assumptions),
            "method": self.method,
        }

View source ↗

Read the implementation

class StructuralInvariant:
    """A structural identity recorded in a certificate payload."""

    kind: str
    expression: str
    certified: bool = True
    assumptions: tuple[str, ...] = ()
    method: str = "structural_identity"

    def to_payload(self) -> dict[str, object]:
        return {
            "kind": self.kind,
            "expression": self.expression,
            "certified": bool(self.certified),
            "assumptions": list(self.assumptions),
            "method": self.method,
        }

FUNCTION

adaptive_certified_interior_residual

omnibias.core.verified.pde_certificate.adaptive_certified_interior_residualSource ↗

adaptive_certified_interior_residual(layers: Sequence[Layer], domain: BoxLike, pde: LinearPDE, *, target: float | None=None, initial_splits: int | Sequence[int]=1, max_splits: int=16) -> AdaptiveResidualDiagnostics

Refine uniform subdivisions until a residual target or split budget is hit.

Parameters

Name	Type & default	Contract
`layers`positional-or-keyword	`Sequence[Layer]`Required	See the operation contract and implementation below.
`domain`positional-or-keyword	`BoxLike`Required	See the operation contract and implementation below.
`pde`positional-or-keyword	`LinearPDE`Required	See the operation contract and implementation below.
`target`keyword-only	`float \| None`Default: None	See the operation contract and implementation below.
`initial_splits`keyword-only	`int \| Sequence[int]`Default: 1	See the operation contract and implementation below.
`max_splits`keyword-only	`int`Default: 16	See the operation contract and implementation below.

ReturnsAdaptiveResidualDiagnostics

Explicit validation & failure cases

When max_splits < 1, raises ValueError('max_splits must be >= 1').
When any((s > max_splits for s in splits)), raises ValueError('initial_splits cannot exceed max_splits').
When tgt is not None and tgt < 0.0, raises ValueError('target must be non-negative').

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

Executed regression · adaptive residual diagnostics reaches target

Full file, imports & fixtures ↗

def test_adaptive_residual_diagnostics_reaches_target() -> None:
    diag = adaptive_certified_interior_residual(
        _AFFINE, _DOMAIN, laplace(2), target=1e-9, initial_splits=1, max_splits=4
    )
    assert diag.reached_target is True
    assert diag.residual_sup < 1e-9
    assert diag.boxes == 1

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

Read the implementation

def adaptive_certified_interior_residual(
    layers: Sequence[Layer],
    domain: BoxLike,
    pde: LinearPDE,
    *,
    target: float | None = None,
    initial_splits: int | Sequence[int] = 1,
    max_splits: int = 16,
) -> AdaptiveResidualDiagnostics:
    """Refine uniform subdivisions until a residual target or split budget is hit."""
    box = _promote(domain)
    dim = len(box)
    splits = _normalize_splits(initial_splits, dim)
    if max_splits < 1:
        raise ValueError("max_splits must be >= 1")
    if any(s > max_splits for s in splits):
        raise ValueError("initial_splits cannot exceed max_splits")
    tgt = None if target is None else float(target)
    if tgt is not None and tgt < 0.0:
        raise ValueError("target must be non-negative")

    iterations = 0
    while True:
        iterations += 1
        residual = certified_interior_residual(layers, box, pde, splits=splits)
        reached = tgt is not None and residual.mag <= tgt
        saturated = all(s >= max_splits for s in splits)
        if reached or saturated or tgt is None:
            boxes = 1
            for s in splits:
                boxes *= s
            widths = _box_widths(box)
            max_width = max((w / s for w, s in zip(widths, splits, strict=True)), default=0.0)
            return AdaptiveResidualDiagnostics(
                residual=residual,
                residual_sup=residual.mag,
                splits=tuple(splits),
                boxes=boxes,
                iterations=iterations,
                target=tgt,
                reached_target=reached,
                max_box_width=max_width,
            )
        splits = [min(max_splits, s * 2) for s in splits]

FUNCTION

advection_diffusion

omnibias.core.verified.advection_diffusionSource ↗

advection_diffusion(dim: int, velocity: Sequence[float], diffusivity: float, source: Coeff=0.0, *, component: int=0) -> LinearPDE

The steady advection-diffusion residual b . grad u - nu Delta u - f.

Parameters

Name	Type & default	Contract
`dim`positional-or-keyword	`int`Required	See the operation contract and implementation below.
`velocity`positional-or-keyword	`Sequence[float]`Required	See the operation contract and implementation below.
`diffusivity`positional-or-keyword	`float`Required	See the operation contract and implementation below.
`source`positional-or-keyword	`Coeff`Default: 0.0	See the operation contract and implementation below.
`component`keyword-only	`int`Default: 0	See the operation contract and implementation below.

ReturnsLinearPDE

Explicit validation & failure cases

When len(velocity) != dim, raises ValueError(f'velocity must have {dim} components, got {len(velocity)}').

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

Executed regression · advection diffusion velocity length

Full file, imports & fixtures ↗

def test_advection_diffusion_velocity_length() -> None:
    with pytest.raises(ValueError):
        advection_diffusion(2, [1.0], 0.5)

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

Regression example · required order

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_required_order() -> None:
    assert laplace(2).required_order() == 2
    assert advection_diffusion(2, [1.0, 1.0], 0.5).required_order() == 2
    assert LinearPDE({}, source=3.0).required_order() == 0  # pure source

python -m pytest packages/omnibias-core/tests/test_verified_pde_certificate.py -k test_required_order -q

Read the implementation

def advection_diffusion(
    dim: int,
    velocity: Sequence[float],
    diffusivity: float,
    source: Coeff = 0.0,
    *,
    component: int = 0,
) -> LinearPDE:
    r"""The steady advection-diffusion residual ``b . grad u - nu Delta u - f``."""
    if len(velocity) != dim:
        raise ValueError(f"velocity must have {dim} components, got {len(velocity)}")
    terms: dict[MultiIndex, Coeff] = {}
    for i in range(dim):
        terms[_unit(i, dim)] = float(velocity[i])
        terms[_double(i, dim)] = -float(diffusivity)
    return LinearPDE(terms, source, component)

Other public import paths

omnibias.core.verified.advection_diffusion
omnibias.core.verified.pde_certificate.advection_diffusion

FUNCTION

aposteriori_error_certificate

omnibias.core.verified.aposteriori_error_certificateSource ↗

aposteriori_error_certificate(layers: Sequence[Layer], domain: BoxLike, pde: LinearPDE, *, boundary: Sequence[BoundaryFace]=(), stability: StabilityEstimate | None=None, stability_interior: float | None=None, stability_boundary: float | None=None, invariants: Sequence[StructuralInvariant]=(), model_metadata: Mapping[str, object] | None=None, max_error: float | None=None, diagnostics: AdaptiveResidualDiagnostics | None=None, splits: int | Sequence[int]=1, boundary_splits: int | Sequence[int]=1) -> PINNErrorCertificate

Certified a-posteriori bound ||u_NN - u_true||_inf <= C_O R_int + C_b R_bnd.

Pass a provenance-carrying stability record, or explicitly provide both stability_interior (C_Omega) and stability_boundary (C_{partial Omega}). They must be rigorous constants for the linear, well-posed BVP pde; silent 1.0 defaults are deliberately refused. Both residuals are computed rigorously from the certified jet, so the resulting bound is a true upper bound on the network's error only under the recorded stability assumptions.

Parameters

Name	Type & default	Contract
`layers`positional-or-keyword	`Sequence[Layer]`Required	See the operation contract and implementation below.
`domain`positional-or-keyword	`BoxLike`Required	See the operation contract and implementation below.
`pde`positional-or-keyword	`LinearPDE`Required	See the operation contract and implementation below.
`boundary`keyword-only	`Sequence[BoundaryFace]`Default: ()	See the operation contract and implementation below.
`stability`keyword-only	`StabilityEstimate \| None`Default: None	See the operation contract and implementation below.
`stability_interior`keyword-only	`float \| None`Default: None	See the operation contract and implementation below.
`stability_boundary`keyword-only	`float \| None`Default: None	See the operation contract and implementation below.
`invariants`keyword-only	`Sequence[StructuralInvariant]`Default: ()	See the operation contract and implementation below.
`model_metadata`keyword-only	`Mapping[str, object] \| None`Default: None	See the operation contract and implementation below.
`max_error`keyword-only	`float \| None`Default: None	See the operation contract and implementation below.
`diagnostics`keyword-only	`AdaptiveResidualDiagnostics \| None`Default: None	See the operation contract and implementation below.
`splits`keyword-only	`int \| Sequence[int]`Default: 1	See the operation contract and implementation below.
`boundary_splits`keyword-only	`int \| Sequence[int]`Default: 1	See the operation contract and implementation below.

ReturnsPINNErrorCertificate

Explicit validation & failure cases

When not isinstance(stability, StabilityEstimate), raises TypeError('stability must be a StabilityEstimate').
When stability_interior is not None or stability_boundary is not None, raises ValueError('pass either stability or both stability_interior and stability_boundary, not both').
When stability_interior is None or stability_boundary is None, raises ValueError('a-posteriori PDE certification requires stability=StabilityEstimate or both stability_interior and stability_boundary').
When max_error < 0.0, raises ValueError('max_error must be non-negative').

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

Executed regression · aposteriori requires explicit stability

Full file, imports & fixtures ↗

def test_aposteriori_requires_explicit_stability() -> None:
    with pytest.raises(ValueError, match="requires stability"):
        aposteriori_error_certificate(_AFFINE, _DOMAIN, laplace(2))

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

Regression example · aposteriori negative stability 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_aposteriori_negative_stability_raises() -> None:
    with pytest.raises(ValueError):
        aposteriori_error_certificate(
            _AFFINE,
            _DOMAIN,
            laplace(2),
            stability_interior=-1.0,
            stability_boundary=1.0,
        )

python -m pytest packages/omnibias-core/tests/test_verified_pde_certificate.py -k test_aposteriori_negative_stability_raises -q

Read the implementation

def aposteriori_error_certificate(
    layers: Sequence[Layer],
    domain: BoxLike,
    pde: LinearPDE,
    *,
    boundary: Sequence[BoundaryFace] = (),
    stability: StabilityEstimate | None = None,
    stability_interior: float | None = None,
    stability_boundary: float | None = None,
    invariants: Sequence[StructuralInvariant] = (),
    model_metadata: Mapping[str, object] | None = None,
    max_error: float | None = None,
    diagnostics: AdaptiveResidualDiagnostics | None = None,
    splits: int | Sequence[int] = 1,
    boundary_splits: int | Sequence[int] = 1,
) -> PINNErrorCertificate:
    r"""Certified a-posteriori bound ``||u_NN - u_true||_inf <= C_O R_int + C_b R_bnd``.

    Pass a provenance-carrying ``stability`` record, or explicitly provide both
    ``stability_interior`` (``C_Omega``) and ``stability_boundary``
    (``C_{partial Omega}``). They must be rigorous constants for the linear,
    well-posed BVP ``pde``; silent ``1.0`` defaults are deliberately refused.
    Both residuals are computed rigorously from the certified jet, so the
    resulting bound is a true upper bound on the network's error only under the
    recorded stability assumptions.
    """
    if stability is not None:
        if not isinstance(stability, StabilityEstimate):
            raise TypeError("stability must be a StabilityEstimate")
        if stability_interior is not None or stability_boundary is not None:
            raise ValueError(
                "pass either stability or both stability_interior and "
                "stability_boundary, not both"
            )
        estimate = stability
    else:
        if stability_interior is None or stability_boundary is None:
            raise ValueError(
                "a-posteriori PDE certification requires stability=StabilityEstimate "
                "or both stability_interior and stability_boundary"
            )
        estimate = user_stability_estimate(
            stability_interior,
            stability_boundary,
            source="explicit_arguments",
            pde_family="linear",
            domain="caller_supplied",
        )
    if diagnostics is not None:
        r_int = diagnostics.residual
    else:
        r_int = certified_interior_residual(layers, domain, pde, splits=splits)
    r_bnd = certified_boundary_residual(
        layers, boundary, component=pde.component, splits=boundary_splits
    )
    r_int_sup = r_int.mag
    r_bnd_sup = r_bnd.mag
    err = (
        Interval.point(estimate.interior) * Interval.point(r_int_sup)
        + Interval.point(estimate.boundary) * Interval.point(r_bnd_sup)
    )
    from omnibias.core.proof.certificate import make_certificate

    payload: dict[str, object] = {
        "type": "pinn_aposteriori_error",
        "error_bound": err.hi,
        "interior_residual_sup": r_int_sup,
        "boundary_residual_sup": r_bnd_sup,
        "stability_interior": float(estimate.interior),
        "stability_boundary": float(estimate.boundary),
        "stability": estimate.to_payload(),
        "interior_enclosure": [r_int.lo, r_int.hi],
        "boundary_enclosure": [r_bnd.lo, r_bnd.hi],
        "pde_order": pde.required_order(),
        "n_boundary_faces": len(boundary),
        "invariants": [inv.to_payload() for inv in invariants],
    }
    if model_metadata is not None:
        payload["model"] = _as_payload_value(model_metadata)
    if diagnostics is not None:
        payload["adaptive_diagnostics"] = diagnostics.to_payload()
    if max_error is not None:
        if max_error < 0.0:
            raise ValueError("max_error must be non-negative")
        margin = Interval.point(float(max_error)) - err
        payload["finite_obligation"] = {
            "type": "error_bound_le_threshold",
            "threshold": float(max_error),
            "margin": [margin.lo, margin.hi],
            "note": (
                "Lean can only check this finite numerical inequality; it does "
                "not formalize the analytic PDE stability theorem."
            ),
        }

    cert = make_certificate(
        claim=(
            "a-posteriori sup-norm error bound "
            "||u_NN - u_true||_inf <= C_Omega * R_interior + C_boundary * R_boundary"
        ),
        payload=payload,
        honesty={
            "unproven_claim": False,
            "continuum_claim": False,
            "interval_verified": True,
            "pde_stability_user_obligation": not estimate.library_provided,
        },
    )
    return PINNErrorCertificate(err.hi, r_int_sup, r_bnd_sup, cert, diagnostics)

Other public import paths

omnibias.core.verified.aposteriori_error_certificate
omnibias.core.verified.pde_certificate.aposteriori_error_certificate

FUNCTION

certified_boundary_residual

omnibias.core.verified.certified_boundary_residualSource ↗

certified_boundary_residual(layers: Sequence[Layer], faces: Sequence[BoundaryFace], *, component: int=0, splits: int | Sequence[int]=1) -> Interval

Rigorous enclosure of { u_NN(x) - g(x) : x in dOmega } over the faces.

Reads the order-0 value row of the certified jet on each (subdivided) face; certified_boundary_residual(...).mag is a certified sup-norm bound on the boundary mismatch.

Parameters

Name	Type & default	Contract
`layers`positional-or-keyword	`Sequence[Layer]`Required	See the operation contract and implementation below.
`faces`positional-or-keyword	`Sequence[BoundaryFace]`Required	See the operation contract and implementation below.
`component`keyword-only	`int`Default: 0	See the operation contract and implementation below.
`splits`keyword-only	`int \| Sequence[int]`Default: 1	See the operation contract and implementation below.

ReturnsInterval

Executed regression · boundary residual empty is zero

Full file, imports & fixtures ↗

def test_boundary_residual_empty_is_zero() -> None:
    assert certified_boundary_residual(_AFFINE, []).mag < 1e-300

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

Regression example · boundary residual encloses face values

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_boundary_residual_encloses_face_values() -> None:
    # right edge x = 1, y in [-1, 1], target g = 0  ->  residual = u_NN on the face.
    face = BoundaryFace([(1.0, 1.0), (-1.0, 1.0)], 0.0)
    r = certified_boundary_residual(_AFFINE, [face], splits=4)
    for y in (-0.5, 0.0, 0.5):
        assert r.lo <= _u_affine(1.0, y) <= r.hi

python -m pytest packages/omnibias-core/tests/test_verified_pde_certificate.py -k test_boundary_residual_encloses_face_values -q

Read the implementation

def certified_boundary_residual(
    layers: Sequence[Layer],
    faces: Sequence[BoundaryFace],
    *,
    component: int = 0,
    splits: int | Sequence[int] = 1,
) -> Interval:
    r"""Rigorous enclosure of ``{ u_NN(x) - g(x) : x in dOmega }`` over the faces.

    Reads the order-0 value row of the certified jet on each (subdivided) face;
    ``certified_boundary_residual(...).mag`` is a certified sup-norm bound on the
    boundary mismatch.
    """
    if not faces:
        return Interval.point(0.0)
    pieces: list[Interval] = []
    for face in faces:
        fbox = _promote(face.box)
        per = _normalize_splits(splits, len(fbox))
        for sub in _grid(fbox, per):
            value = certified_partials(sub, layers, 0)[(0,) * len(fbox)][component]
            pieces.append(value - _eval_coeff(face.target, sub))
    return hull(list(pieces))

Other public import paths

omnibias.core.verified.certified_boundary_residual
omnibias.core.verified.pde_certificate.certified_boundary_residual

FUNCTION

certified_custom_residual

omnibias.core.verified.pde_certificate.certified_custom_residualSource ↗

certified_custom_residual(layers: Sequence[Layer], domain: BoxLike, residual: CertifiedResidualCallback, *, order: int, splits: int | Sequence[int]=1) -> Interval

Rigorous enclosure of a user-supplied certified residual callback.

This is the v1 extension point for semilinear / nonlinear PDE terms. The callback must be inclusion-isotonic in the interval inputs it receives; the helper supplies certified partials through order on every sub-box and returns the hull of the callback values. General nonlinear PDE soundness is therefore the callback author's obligation.

Parameters

Name	Type & default	Contract
`layers`positional-or-keyword	`Sequence[Layer]`Required	See the operation contract and implementation below.
`domain`positional-or-keyword	`BoxLike`Required	See the operation contract and implementation below.
`residual`positional-or-keyword	`CertifiedResidualCallback`Required	See the operation contract and implementation below.
`order`keyword-only	`int`Required	See the operation contract and implementation below.
`splits`keyword-only	`int \| Sequence[int]`Default: 1	See the operation contract and implementation below.

ReturnsInterval

Explicit validation & failure cases

When order < 0, raises ValueError('order must be non-negative').

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

Executed regression · custom and quadratic residual hooks

Full file, imports & fixtures ↗

def test_custom_and_quadratic_residual_hooks() -> None:
    def residual(box, partials):
        return partials[(0,) * len(box)][0]

    r = certified_custom_residual(_AFFINE, [(0.5, 0.5), (0.25, 0.25)], residual, order=0)
    assert r.lo <= _u_affine(0.5, 0.25) <= r.hi

    q = certified_quadratic_reaction_residual(
        _AFFINE, [(0.0, 0.0), (0.0, 0.0)], laplace(2), coefficient=2.0
    )
    assert q.lo <= 2.0 * (_u_affine(0.0, 0.0) ** 2) <= q.hi

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

Read the implementation

def certified_custom_residual(
    layers: Sequence[Layer],
    domain: BoxLike,
    residual: CertifiedResidualCallback,
    *,
    order: int,
    splits: int | Sequence[int] = 1,
) -> Interval:
    r"""Rigorous enclosure of a user-supplied certified residual callback.

    This is the v1 extension point for semilinear / nonlinear PDE terms.  The
    callback must be inclusion-isotonic in the interval inputs it receives; the
    helper supplies certified partials through ``order`` on every sub-box and
    returns the hull of the callback values.  General nonlinear PDE soundness is
    therefore the callback author's obligation.
    """
    if order < 0:
        raise ValueError("order must be non-negative")
    box = _promote(domain)
    dim = len(box)
    per = _normalize_splits(splits, dim)
    pieces = [
        Interval.from_value(residual(sub, certified_partials(sub, layers, order)))
        for sub in _grid(box, per)
    ]
    return hull(list(pieces))

FUNCTION

certified_interior_residual

omnibias.core.verified.certified_interior_residualSource ↗

certified_interior_residual(layers: Sequence[Layer], domain: BoxLike, pde: LinearPDE, *, splits: int | Sequence[int]=1) -> Interval

Rigorous enclosure of { L u_NN(x) - f(x) : x in domain }.

u_NN is the MLP described by layers (the ~omnibias.core.verified.jet_mv.Layer format). The enclosure is the hull over a splits grid of sub-boxes; certified_interior_residual(...) .mag is a certified sup-norm bound on the interior PDE residual.

Parameters

Name	Type & default	Contract
`layers`positional-or-keyword	`Sequence[Layer]`Required	See the operation contract and implementation below.
`domain`positional-or-keyword	`BoxLike`Required	See the operation contract and implementation below.
`pde`positional-or-keyword	`LinearPDE`Required	See the operation contract and implementation below.
`splits`keyword-only	`int \| Sequence[int]`Default: 1	See the operation contract and implementation below.

ReturnsInterval

Executed regression · screened poisson sign

Full file, imports & fixtures ↗

def test_screened_poisson_sign() -> None:
    pde = screened_poisson(2, 2.0, 0.0)  # lap u - 4 u = -4 u  for affine
    x, y = 0.5, 0.5
    r = certified_interior_residual(_AFFINE, [(x, x), (y, y)], pde)
    assert r.lo <= -4.0 * _u_affine(x, y) <= r.hi

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

Regression example · subdivision tightens

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_subdivision_tightens() -> None:
    net = _tanh_net()
    pde = laplace(2)
    coarse = certified_interior_residual(net, _DOMAIN, pde, splits=1)
    fine = certified_interior_residual(net, _DOMAIN, pde, splits=6)
    assert fine.mag <= coarse.mag + 1e-12

python -m pytest packages/omnibias-core/tests/test_verified_pde_certificate.py -k test_subdivision_tightens -q

Read the implementation

def certified_interior_residual(
    layers: Sequence[Layer],
    domain: BoxLike,
    pde: LinearPDE,
    *,
    splits: int | Sequence[int] = 1,
) -> Interval:
    r"""Rigorous enclosure of ``{ L u_NN(x) - f(x) : x in domain }``.

    ``u_NN`` is the MLP described by ``layers`` (the
    :data:`~omnibias.core.verified.jet_mv.Layer` format).  The enclosure is the
    hull over a ``splits`` grid of sub-boxes; ``certified_interior_residual(...)
    .mag`` is a certified sup-norm bound on the interior PDE residual.
    """
    box = _promote(domain)
    dim = len(box)
    order = pde.required_order()
    per = _normalize_splits(splits, dim)
    pieces = [
        pde.residual(sub, certified_partials(sub, layers, order))
        for sub in _grid(box, per)
    ]
    return hull(list(pieces))

Other public import paths

omnibias.core.verified.certified_interior_residual
omnibias.core.verified.pde_certificate.certified_interior_residual

FUNCTION

certified_quadratic_reaction_residual

omnibias.core.verified.pde_certificate.certified_quadratic_reaction_residualSource ↗

certified_quadratic_reaction_residual(layers: Sequence[Layer], domain: BoxLike, pde: LinearPDE, *, coefficient: Coeff=1.0, splits: int | Sequence[int]=1) -> Interval

Experimental enclosure of L u - f + c u^2 for scalar semilinear PDEs.

Parameters

Name	Type & default	Contract
`layers`positional-or-keyword	`Sequence[Layer]`Required	See the operation contract and implementation below.
`domain`positional-or-keyword	`BoxLike`Required	See the operation contract and implementation below.
`pde`positional-or-keyword	`LinearPDE`Required	See the operation contract and implementation below.
`coefficient`keyword-only	`Coeff`Default: 1.0	See the operation contract and implementation below.
`splits`keyword-only	`int \| Sequence[int]`Default: 1	See the operation contract and implementation below.

ReturnsInterval

Executed regression · custom and quadratic residual hooks

Full file, imports & fixtures ↗

def test_custom_and_quadratic_residual_hooks() -> None:
    def residual(box, partials):
        return partials[(0,) * len(box)][0]

    r = certified_custom_residual(_AFFINE, [(0.5, 0.5), (0.25, 0.25)], residual, order=0)
    assert r.lo <= _u_affine(0.5, 0.25) <= r.hi

    q = certified_quadratic_reaction_residual(
        _AFFINE, [(0.0, 0.0), (0.0, 0.0)], laplace(2), coefficient=2.0
    )
    assert q.lo <= 2.0 * (_u_affine(0.0, 0.0) ** 2) <= q.hi

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

Read the implementation

def certified_quadratic_reaction_residual(
    layers: Sequence[Layer],
    domain: BoxLike,
    pde: LinearPDE,
    *,
    coefficient: Coeff = 1.0,
    splits: int | Sequence[int] = 1,
) -> Interval:
    r"""Experimental enclosure of ``L u - f + c u^2`` for scalar semilinear PDEs."""

    def residual(
        box: Sequence[Interval], partials: Mapping[MultiIndex, Sequence[Interval]]
    ) -> Interval:
        value = partials[(0,) * len(box)][pde.component]
        return pde.residual(box, partials) + _eval_coeff(coefficient, box) * value * value

    return certified_custom_residual(
        layers, domain, residual, order=pde.required_order(), splits=splits
    )

FUNCTION

certified_streamfunction_divergence

omnibias.core.verified.pde_certificate.certified_streamfunction_divergenceSource ↗

certified_streamfunction_divergence(layers: Sequence[Layer], domain: BoxLike, *, splits: int | Sequence[int]=1) -> Interval

Rigorous enclosure of \nabla\cdot(\nabla^\perp\psi) over the box.

For a scalar streamfunction \psi the induced velocity u = (\psi_y, -\psi_x) is divergence free identically; the divergence \psi_{xy} - \psi_{yx} is recomputed naively in interval arithmetic, so the returned enclosure always contains 0 and .mag is a certified bound on the (structurally zero) incompressibility defect that tightens to 0 as splits grows. This is the numerical cross-check of the structural cage, not its proof (the proof is equality of mixed partials).

Parameters

Name	Type & default	Contract
`layers`positional-or-keyword	`Sequence[Layer]`Required	See the operation contract and implementation below.
`domain`positional-or-keyword	`BoxLike`Required	See the operation contract and implementation below.
`splits`keyword-only	`int \| Sequence[int]`Default: 1	See the operation contract and implementation below.

ReturnsInterval

Read the implementation

def certified_streamfunction_divergence(
    layers: Sequence[Layer],
    domain: BoxLike,
    *,
    splits: int | Sequence[int] = 1,
) -> Interval:
    r"""Rigorous enclosure of ``\nabla\cdot(\nabla^\perp\psi)`` over the box.

    For a scalar streamfunction ``\psi`` the induced velocity ``u = (\psi_y,
    -\psi_x)`` is divergence free identically; the divergence
    ``\psi_{xy} - \psi_{yx}`` is recomputed naively in interval arithmetic, so the
    returned enclosure always contains ``0`` and ``.mag`` is a certified bound on
    the (structurally zero) incompressibility defect that tightens to ``0`` as
    ``splits`` grows.  This is the numerical cross-check of the structural cage,
    not its proof (the proof is equality of mixed partials).
    """

    def residual(
        box: Sequence[Interval], partials: Mapping[MultiIndex, Sequence[Interval]]
    ) -> Interval:
        cross = partials[(1, 1)][0]
        return cross - cross

    return certified_custom_residual(layers, domain, residual, order=2, splits=splits)

FUNCTION

certified_vorticity_transport_residual

omnibias.core.verified.pde_certificate.certified_vorticity_transport_residualSource ↗

certified_vorticity_transport_residual(layers: Sequence[Layer], domain: BoxLike, *, viscosity: float=0.0, forcing: Coeff=0.0, splits: int | Sequence[int]=1) -> Interval

Rigorous enclosure of the steady 2-D vorticity-transport residual.

The streamfunction \psi (an MLP in Layer format, scalar output) induces u = (\psi_y, -\psi_x) and vorticity \omega = -\Delta\psi. The residual of the steady viscous vorticity-transport equation

R = (u\cdot\nabla)\omega - \nu\,\Delta\omega - f_\omega

is assembled from the certified partials of \psi (up to order 3 for the Euler advection \nu=0, order 4 when the viscous term is included):

u\cdot\nabla\omega = \psi_y\,\bigl[-(\psi_{xxx}+\psi_{xyy})\bigr]
\psi_x\,\bigl[-(\psi_{xxy}+\psi_{yyy})\bigr],\qquad \Delta\omega = -(\psi_{xxxx}+2\psi_{xxyy}+\psi_{yyyy}).

The result encloses { R(x) : x in domain } for *every* point of the box, so .mag is a certified sup-norm bound on the residual. forcing is the target vorticity forcing f_\omega (a constant or a rigorous box -> enclosure callback -- its soundness is the caller's obligation, like a source term). viscosity is \nu; with \nu = 0 and forcing = 0 this is the exact steady-Euler residual.

Parameters

Name	Type & default	Contract
`layers`positional-or-keyword	`Sequence[Layer]`Required	See the operation contract and implementation below.
`domain`positional-or-keyword	`BoxLike`Required	See the operation contract and implementation below.
`viscosity`keyword-only	`float`Default: 0.0	See the operation contract and implementation below.
`forcing`keyword-only	`Coeff`Default: 0.0	See the operation contract and implementation below.
`splits`keyword-only	`int \| Sequence[int]`Default: 1	See the operation contract and implementation below.

ReturnsInterval

Explicit validation & failure cases

When viscosity < 0.0, raises ValueError('viscosity must be non-negative').

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

Read the implementation

def certified_vorticity_transport_residual(
    layers: Sequence[Layer],
    domain: BoxLike,
    *,
    viscosity: float = 0.0,
    forcing: Coeff = 0.0,
    splits: int | Sequence[int] = 1,
) -> Interval:
    r"""Rigorous enclosure of the steady 2-D vorticity-transport residual.

    The streamfunction ``\psi`` (an MLP in :data:`Layer` format, scalar output)
    induces ``u = (\psi_y, -\psi_x)`` and vorticity ``\omega = -\Delta\psi``.  The
    residual of the steady viscous vorticity-transport equation

    .. math::

        R = (u\cdot\nabla)\omega - \nu\,\Delta\omega - f_\omega

    is assembled from the certified partials of ``\psi`` (up to order 3 for the
    Euler advection ``\nu=0``, order 4 when the viscous term is included):

    .. math::

        u\cdot\nabla\omega
          = \psi_y\,\bigl[-(\psi_{xxx}+\psi_{xyy})\bigr]
          - \psi_x\,\bigl[-(\psi_{xxy}+\psi_{yyy})\bigr],\qquad
        \Delta\omega = -(\psi_{xxxx}+2\psi_{xxyy}+\psi_{yyyy}).

    The result encloses ``{ R(x) : x in domain }`` for *every* point of the box,
    so ``.mag`` is a certified sup-norm bound on the residual.  ``forcing`` is the
    target vorticity forcing ``f_\omega`` (a constant or a rigorous
    ``box -> enclosure`` callback -- its soundness is the caller's obligation, like
    a source term).  ``viscosity`` is ``\nu``; with ``\nu = 0`` and ``forcing = 0``
    this is the exact steady-Euler residual.
    """
    if viscosity < 0.0:
        raise ValueError("viscosity must be non-negative")
    order = 4 if viscosity != 0.0 else 3
    nu = Interval.point(float(viscosity))
    two = Interval.point(2.0)

    def residual(
        box: Sequence[Interval], partials: Mapping[MultiIndex, Sequence[Interval]]
    ) -> Interval:
        def d(alpha: MultiIndex) -> Interval:
            return partials[alpha][0]

        u1 = d((0, 1))  # psi_y  = u_x
        u2 = _neg(d((1, 0)))  # -psi_x = u_y
        dx_omega = _neg(d((3, 0)) + d((1, 2)))  # d_x omega
        dy_omega = _neg(d((2, 1)) + d((0, 3)))  # d_y omega
        res = u1 * dx_omega + u2 * dy_omega
        if viscosity != 0.0:
            lap_omega = _neg(d((4, 0)) + two * d((2, 2)) + d((0, 4)))
            res = res - nu * lap_omega
        return res - _eval_coeff(forcing, box)

    return certified_custom_residual(layers, domain, residual, order=order, splits=splits)

FUNCTION

helmholtz

omnibias.core.verified.helmholtzSource ↗

helmholtz(dim: int, wavenumber: float, source: Coeff=0.0, *, component: int=0) -> LinearPDE

The Helmholtz residual Delta u + k^2 u - f.

Parameters

Name	Type & default	Contract
`dim`positional-or-keyword	`int`Required	See the operation contract and implementation below.
`wavenumber`positional-or-keyword	`float`Required	See the operation contract and implementation below.
`source`positional-or-keyword	`Coeff`Default: 0.0	See the operation contract and implementation below.
`component`keyword-only	`int`Default: 0	See the operation contract and implementation below.

ReturnsLinearPDE

Executed regression · affine helmholtz encloses pointwise value

Full file, imports & fixtures ↗

def test_affine_helmholtz_encloses_pointwise_value() -> None:
    pde = helmholtz(2, 1.0, 0.0)  # lap u + u - 0 = u  (affine lap = 0)
    for x, y in [(0.3, -0.2), (-0.7, 0.5), (1.0, 1.0)]:
        r = certified_interior_residual(_AFFINE, [(x, x), (y, y)], pde)
        assert r.lo <= _u_affine(x, y) <= r.hi

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

Read the implementation

def helmholtz(
    dim: int, wavenumber: float, source: Coeff = 0.0, *, component: int = 0
) -> LinearPDE:
    r"""The Helmholtz residual ``Delta u + k^2 u - f``."""
    terms: dict[MultiIndex, Coeff] = {_double(i, dim): 1.0 for i in range(dim)}
    terms[(0,) * dim] = float(wavenumber) ** 2
    return LinearPDE(terms, source, component)

Other public import paths

omnibias.core.verified.helmholtz
omnibias.core.verified.pde_certificate.helmholtz

FUNCTION

laplace

omnibias.core.verified.laplaceSource ↗

laplace(dim: int, *, component: int=0) -> LinearPDE

The Laplace operator residual Delta u (harmonic when zero).

Parameters

Name	Type & default	Contract
`dim`positional-or-keyword	`int`Required	See the operation contract and implementation below.
`component`keyword-only	`int`Default: 0	See the operation contract and implementation below.

ReturnsLinearPDE

Executed regression · aposteriori requires explicit stability

Full file, imports & fixtures ↗

def test_aposteriori_requires_explicit_stability() -> None:
    with pytest.raises(ValueError, match="requires stability"):
        aposteriori_error_certificate(_AFFINE, _DOMAIN, laplace(2))

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

Regression example · required order

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_required_order() -> None:
    assert laplace(2).required_order() == 2
    assert advection_diffusion(2, [1.0, 1.0], 0.5).required_order() == 2
    assert LinearPDE({}, source=3.0).required_order() == 0  # pure source

python -m pytest packages/omnibias-core/tests/test_verified_pde_certificate.py -k test_required_order -q

Read the implementation

def laplace(dim: int, *, component: int = 0) -> LinearPDE:
    r"""The Laplace operator residual ``Delta u`` (harmonic when zero)."""
    return LinearPDE({_double(i, dim): 1.0 for i in range(dim)}, 0.0, component)

Other public import paths

omnibias.core.verified.laplace
omnibias.core.verified.pde_certificate.laplace

FUNCTION

pinn_aposteriori_schema_errors

omnibias.core.verified.pde_certificate.pinn_aposteriori_schema_errorsSource ↗

pinn_aposteriori_schema_errors(cert: Mapping[str, object]) -> list[str]

Validate the v1 pinn_aposteriori_error certificate payload.

Parameters

Name	Type & default	Contract
`cert`positional-or-keyword	`Mapping[str, object]`Required	See the operation contract and implementation below.

Returnslist[str]

Executed regression · pinn schema rejects forged structural claim

Full file, imports & fixtures ↗

def test_pinn_schema_rejects_forged_structural_claim() -> None:
    cert = aposteriori_error_certificate(
        _AFFINE,
        _DOMAIN,
        laplace(2),
        stability_interior=1.0,
        stability_boundary=1.0,
        splits=2,
    ).certificate
    cert["payload"]["invariants"] = [{"kind": "divergence_free", "certified": True}]
    assert any("expression" in err for err in pinn_aposteriori_schema_errors(cert))

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

Regression example · aposteriori exact solution has tiny error

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_aposteriori_exact_solution_has_tiny_error() -> None:
    # affine net is harmonic; no boundary term -> error bound ~ 0.
    cert = aposteriori_error_certificate(
        _AFFINE,
        _DOMAIN,
        laplace(2),
        stability_interior=0.5,
        stability_boundary=1.0,
        splits=2,
    )
    assert cert.error_bound < 1e-9
    assert cert.boundary_residual < 1e-300  # no boundary faces supplied
    assert verify_certificate_digest(cert.certificate)
    assert cert.certificate["payload"]["type"] == "pinn_aposteriori_error"
    assert pinn_aposteriori_schema_errors(cert.certificate) == []
    assert replay_pinn_aposteriori_certificate(cert.certificate)

python -m pytest packages/omnibias-core/tests/test_verified_pde_certificate.py -k test_aposteriori_exact_solution_has_tiny_error -q

Read the implementation

def pinn_aposteriori_schema_errors(cert: Mapping[str, object]) -> list[str]:
    """Validate the v1 ``pinn_aposteriori_error`` certificate payload."""
    from omnibias.core.proof.certificate import schema_errors_v1

    errors = schema_errors_v1(cert)
    payload = cert.get("payload")
    if not isinstance(payload, Mapping):
        return errors + ["payload must be a mapping"]
    if payload.get("type") != "pinn_aposteriori_error":
        errors.append("payload.type must be 'pinn_aposteriori_error'")

    required = (
        "error_bound",
        "interior_residual_sup",
        "boundary_residual_sup",
        "stability",
        "interior_enclosure",
        "boundary_enclosure",
        "pde_order",
        "n_boundary_faces",
    )
    for key in required:
        if key not in payload:
            errors.append(f"payload missing required field {key!r}")

    for key in ("error_bound", "interior_residual_sup", "boundary_residual_sup"):
        try:
            if float(payload.get(key, -1.0)) < 0.0:
                errors.append(f"payload.{key} must be non-negative")
        except (TypeError, ValueError):
            errors.append(f"payload.{key} must be numeric")

    stability = payload.get("stability")
    if not isinstance(stability, Mapping):
        errors.append("payload.stability must be a mapping with provenance")
    else:
        for key in ("interior", "boundary", "source", "pde_family", "domain"):
            if key not in stability:
                errors.append(f"payload.stability missing {key!r}")
        for key in ("interior", "boundary"):
            try:
                if float(stability.get(key, -1.0)) < 0.0:
                    errors.append(f"payload.stability.{key} must be non-negative")
            except (TypeError, ValueError):
                errors.append(f"payload.stability.{key} must be numeric")

    invariants = payload.get("invariants", [])
    if not isinstance(invariants, Sequence) or isinstance(invariants, str | bytes):
        errors.append("payload.invariants must be a sequence")
    else:
        for idx, inv in enumerate(invariants):
            if not isinstance(inv, Mapping):
                errors.append(f"payload.invariants[{idx}] must be a mapping")
                continue
            if inv.get("certified") and not inv.get("expression"):
                errors.append(f"payload.invariants[{idx}] certified invariant needs expression")

    finite = payload.get("finite_obligation")
    if finite is not None:
        if not isinstance(finite, Mapping):
            errors.append("payload.finite_obligation must be a mapping")
        elif finite.get("type") != "error_bound_le_threshold":
            errors.append("payload.finite_obligation.type must be 'error_bound_le_threshold'")
        elif "margin" not in finite:
            errors.append("payload.finite_obligation missing 'margin'")

    honesty = cert.get("honesty", {})
    if isinstance(honesty, Mapping) and bool(honesty.get("unproven_claim", False)):
        errors.append("honesty.unproven_claim must be False")
    return errors

FUNCTION

poisson

omnibias.core.verified.poissonSource ↗

poisson(dim: int, source: Coeff, *, component: int=0) -> LinearPDE

The Poisson residual Delta u - f.

Parameters

Name	Type & default	Contract
`dim`positional-or-keyword	`int`Required	See the operation contract and implementation below.
`source`positional-or-keyword	`Coeff`Required	See the operation contract and implementation below.
`component`keyword-only	`int`Default: 0	See the operation contract and implementation below.

ReturnsLinearPDE

Executed regression · affine laplacian and poisson are zero

Full file, imports & fixtures ↗

def test_affine_laplacian_and_poisson_are_zero() -> None:
    assert certified_interior_residual(_AFFINE, _DOMAIN, laplace(2), splits=2).mag < 1e-9
    assert (
        certified_interior_residual(_AFFINE, _DOMAIN, poisson(2, 0.0), splits=2).mag
        < 1e-9
    )

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

Read the implementation

def poisson(dim: int, source: Coeff, *, component: int = 0) -> LinearPDE:
    r"""The Poisson residual ``Delta u - f``."""
    return LinearPDE({_double(i, dim): 1.0 for i in range(dim)}, source, component)

Other public import paths

omnibias.core.verified.poisson
omnibias.core.verified.pde_certificate.poisson

FUNCTION

radii_polynomial_residual_certificate

omnibias.core.verified.radii_polynomial_residual_certificateSource ↗

radii_polynomial_residual_certificate(residual_sup: float, z0: float, z1: float, z2: float, *, a_norm: float=1.0, r_max: float=float('inf'), claim: str='unique zero in closed ball B(x_bar, r)') -> RadiiCertificate | None

Radii-polynomial existence from a certified residual as the NK defect.

The Newton-Kantorovich defect is Y0 = ||A F(x_bar)|| <= ||A|| * residual_sup (a_norm = ||A||, the approximate-inverse operator norm). residual_sup is any rigorous bound on the residual norm -- e.g. from certified_interior_residual (its .mag) or spectral_residual_norm (its .hi). (Z0, Z1, Z2) are the contraction bounds of the linearisation (the caller's obligation); the result is None when no contracting radius exists.

Parameters

Name	Type & default	Contract
`residual_sup`positional-or-keyword	`float`Required	See the operation contract and implementation below.
`z0`positional-or-keyword	`float`Required	See the operation contract and implementation below.
`z1`positional-or-keyword	`float`Required	See the operation contract and implementation below.
`z2`positional-or-keyword	`float`Required	See the operation contract and implementation below.
`a_norm`keyword-only	`float`Default: 1.0	See the operation contract and implementation below.
`r_max`keyword-only	`float`Default: float('inf')	See the operation contract and implementation below.
`claim`keyword-only	`str`Default: 'unique zero in closed ball B(x_bar, r)'	See the operation contract and implementation below.

ReturnsRadiiCertificate | None

Explicit validation & failure cases

When residual_sup < 0.0 or a_norm < 0.0, raises ValueError('residual_sup and a_norm 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

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 bridge negative inputs raise

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_negative_inputs_raise() -> None:
    with pytest.raises(ValueError):
        radii_polynomial_residual_certificate(-1.0, 0.1, 0.0, 0.5)
    with pytest.raises(ValueError):
        radii_polynomial_residual_certificate(1e-4, 0.1, 0.0, 0.5, a_norm=-1.0)

python -m pytest packages/omnibias-core/tests/test_verified_pde_certificate.py -k test_radii_bridge_negative_inputs_raise -q

Read the implementation

def radii_polynomial_residual_certificate(
    residual_sup: float,
    z0: float,
    z1: float,
    z2: float,
    *,
    a_norm: float = 1.0,
    r_max: float = float("inf"),
    claim: str = "unique zero in closed ball B(x_bar, r)",
) -> RadiiCertificate | None:
    r"""Radii-polynomial existence from a certified residual as the NK defect.

    The Newton-Kantorovich defect is ``Y0 = ||A F(x_bar)|| <= ||A|| * residual_sup``
    (``a_norm = ||A||``, the approximate-inverse operator norm).  ``residual_sup``
    is any rigorous bound on the residual norm -- e.g. from
    :func:`certified_interior_residual` (its ``.mag``) or
    :func:`spectral_residual_norm` (its ``.hi``).  ``(Z0, Z1, Z2)`` are the
    contraction bounds of the linearisation (the caller's obligation); the result
    is ``None`` when no contracting radius exists.
    """
    if residual_sup < 0.0 or a_norm < 0.0:
        raise ValueError("residual_sup and a_norm must be non-negative")
    y0 = (Interval.point(float(a_norm)) * Interval.point(float(residual_sup))).hi
    return radii_polynomial_certificate(y0, z0, z1, z2, r_max=r_max, claim=claim)

Other public import paths

omnibias.core.verified.radii_polynomial_residual_certificate
omnibias.core.verified.pde_certificate.radii_polynomial_residual_certificate

FUNCTION

replay_pinn_aposteriori_certificate

omnibias.core.verified.pde_certificate.replay_pinn_aposteriori_certificateSource ↗

replay_pinn_aposteriori_certificate(cert: Mapping[str, object]) -> bool

Independent arithmetic replay of the sealed a-posteriori error formula.

Parameters

Name	Type & default	Contract
`cert`positional-or-keyword	`Mapping[str, object]`Required	See the operation contract and implementation below.

Returnsbool

Executed regression · aposteriori exact solution has tiny error

Full file, imports & fixtures ↗

def test_aposteriori_exact_solution_has_tiny_error() -> None:
    # affine net is harmonic; no boundary term -> error bound ~ 0.
    cert = aposteriori_error_certificate(
        _AFFINE,
        _DOMAIN,
        laplace(2),
        stability_interior=0.5,
        stability_boundary=1.0,
        splits=2,
    )
    assert cert.error_bound < 1e-9
    assert cert.boundary_residual < 1e-300  # no boundary faces supplied
    assert verify_certificate_digest(cert.certificate)
    assert cert.certificate["payload"]["type"] == "pinn_aposteriori_error"
    assert pinn_aposteriori_schema_errors(cert.certificate) == []
    assert replay_pinn_aposteriori_certificate(cert.certificate)

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

Read the implementation

def replay_pinn_aposteriori_certificate(cert: Mapping[str, object]) -> bool:
    """Independent arithmetic replay of the sealed a-posteriori error formula."""
    if pinn_aposteriori_schema_errors(cert):
        return False
    payload = cert["payload"]
    assert isinstance(payload, Mapping)
    stability = payload["stability"]
    assert isinstance(stability, Mapping)
    expected = (
        Interval.point(float(stability["interior"]))
        * Interval.point(float(payload["interior_residual_sup"]))
        + Interval.point(float(stability["boundary"]))
        * Interval.point(float(payload["boundary_residual_sup"]))
    ).hi
    return abs(expected - float(payload["error_bound"])) <= max(1e-12, 1e-12 * abs(expected))

FUNCTION

screened_poisson

omnibias.core.verified.screened_poissonSource ↗

screened_poisson(dim: int, kappa: float, source: Coeff=0.0, *, component: int=0) -> LinearPDE

The screened-Poisson / modified-Helmholtz residual Delta u - kappa^2 u - f.

Parameters

Name	Type & default	Contract
`dim`positional-or-keyword	`int`Required	See the operation contract and implementation below.
`kappa`positional-or-keyword	`float`Required	See the operation contract and implementation below.
`source`positional-or-keyword	`Coeff`Default: 0.0	See the operation contract and implementation below.
`component`keyword-only	`int`Default: 0	See the operation contract and implementation below.

ReturnsLinearPDE

Executed regression · screened poisson sign

Full file, imports & fixtures ↗

def test_screened_poisson_sign() -> None:
    pde = screened_poisson(2, 2.0, 0.0)  # lap u - 4 u = -4 u  for affine
    x, y = 0.5, 0.5
    r = certified_interior_residual(_AFFINE, [(x, x), (y, y)], pde)
    assert r.lo <= -4.0 * _u_affine(x, y) <= r.hi

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

Read the implementation

def screened_poisson(
    dim: int, kappa: float, source: Coeff = 0.0, *, component: int = 0
) -> LinearPDE:
    r"""The screened-Poisson / modified-Helmholtz residual ``Delta u - kappa^2 u - f``."""
    terms: dict[MultiIndex, Coeff] = {_double(i, dim): 1.0 for i in range(dim)}
    terms[(0,) * dim] = -(float(kappa) ** 2)
    return LinearPDE(terms, source, component)

Other public import paths

omnibias.core.verified.screened_poisson
omnibias.core.verified.pde_certificate.screened_poisson

FUNCTION

spectral_residual_norm

omnibias.core.verified.spectral_residual_normSource ↗

spectral_residual_norm(ansatz: ValidatedFourierSeries, linear_symbol: Symbol, linear_tail_factor: float, *, quadratic: Callable[[ValidatedFourierSeries], ValidatedFourierSeries] | None=None, rhs: ValidatedFourierSeries | None=None) -> Interval

Rigorous l1_nu norm of the residual F(a) = L a + Q(a) - rhs.

L is the diagonal Fourier multiplier linear_symbol (with linear_tail_factor a sound bound on sup_{|k|>N}|symbol(k)|); Q is an optional quadratic term built from the validated algebra (e.g. lambda a: a * a for u^2, or a Riesz/convolution advection); rhs is the forcing. The returned interval's .hi is the natural Y0 for radii_polynomial_residual_certificate.

Parameters

Name	Type & default	Contract
`ansatz`positional-or-keyword	`ValidatedFourierSeries`Required	See the operation contract and implementation below.
`linear_symbol`positional-or-keyword	`Symbol`Required	See the operation contract and implementation below.
`linear_tail_factor`positional-or-keyword	`float`Required	See the operation contract and implementation below.
`quadratic`keyword-only	`Callable[[ValidatedFourierSeries], ValidatedFourierSeries] \| None`Default: None	See the operation contract and implementation below.
`rhs`keyword-only	`ValidatedFourierSeries \| None`Default: None	See the operation contract and implementation below.

ReturnsInterval

Executed regression · spectral feeds radii bridge

Full file, imports & fixtures ↗

def test_spectral_feeds_radii_bridge() -> None:
    dim, n, nu = 1, 3, 1.0
    a = VFS.from_coeffs({(1,): 1e-3, (-1,): 1e-3}, dim, n, nu)
    res = spectral_residual_norm(a, _zero_symbol, 0.0, quadratic=lambda s: s * s)
    cert = radii_polynomial_residual_certificate(res.hi, 0.1, 0.0, 0.5)
    assert cert is not None
    assert math.isfinite(cert.radius)

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

Regression example · spectral quadratic matches hand computation

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_spectral_quadratic_matches_hand_computation() -> None:
    # a(x) = 2 cos x ; (a*a) has coeffs {-2:1, 0:2, 2:1}; L = 0, no rhs.
    dim, n, nu = 1, 4, 1.0
    a = VFS.from_coeffs({(1,): 1.0, (-1,): 1.0}, dim, n, nu)
    res = spectral_residual_norm(a, _zero_symbol, 0.0, quadratic=lambda s: s * s)
    assert res.hi == pytest.approx(4.0, abs=1e-12)  # 1 + 2 + 1, nu = 1

python -m pytest packages/omnibias-core/tests/test_verified_pde_certificate.py -k test_spectral_quadratic_matches_hand_computation -q

Read the implementation

def spectral_residual_norm(
    ansatz: ValidatedFourierSeries,
    linear_symbol: Symbol,
    linear_tail_factor: float,
    *,
    quadratic: Callable[[ValidatedFourierSeries], ValidatedFourierSeries] | None = None,
    rhs: ValidatedFourierSeries | None = None,
) -> Interval:
    r"""Rigorous ``l1_nu`` norm of the residual ``F(a) = L a + Q(a) - rhs``.

    ``L`` is the diagonal Fourier multiplier ``linear_symbol`` (with
    ``linear_tail_factor`` a sound bound on ``sup_{|k|>N}|symbol(k)|``); ``Q`` is
    an optional quadratic term built from the validated algebra (e.g.
    ``lambda a: a * a`` for ``u^2``, or a Riesz/convolution advection); ``rhs`` is
    the forcing.  The returned interval's ``.hi`` is the natural ``Y0`` for
    :func:`radii_polynomial_residual_certificate`.
    """
    residual = ansatz.apply_multiplier(linear_symbol, linear_tail_factor)
    if quadratic is not None:
        residual = residual + quadratic(ansatz)
    if rhs is not None:
        residual = residual - rhs
    return residual.norm()

Other public import paths

omnibias.core.verified.spectral_residual_norm
omnibias.core.verified.pde_certificate.spectral_residual_norm

FUNCTION

structural_invariant

omnibias.core.verified.pde_certificate.structural_invariantSource ↗

structural_invariant(kind: str, expression: str, *, assumptions: Sequence[str]=(), certified: bool=True, method: str='structural_identity') -> StructuralInvariant

Create a serialisable record for an invariant enforced by construction.

Parameters

Name	Type & default	Contract
`kind`positional-or-keyword	`str`Required	See the operation contract and implementation below.
`expression`positional-or-keyword	`str`Required	See the operation contract and implementation below.
`assumptions`keyword-only	`Sequence[str]`Default: ()	See the operation contract and implementation below.
`certified`keyword-only	`bool`Default: True	See the operation contract and implementation below.
`method`keyword-only	`str`Default: 'structural_identity'	See the operation contract and implementation below.

ReturnsStructuralInvariant

Explicit validation & failure cases

When not kind, raises ValueError('invariant kind must be non-empty').
When certified and (not expression), raises ValueError('certified structural invariants need an expression').

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

Executed regression · aposteriori records stability invariants and formal margin

Full file, imports & fixtures ↗

def test_aposteriori_records_stability_invariants_and_formal_margin() -> None:
    stability = user_stability_estimate(
        0.5,
        1.0,
        source="maximum-principle fixture",
        pde_family="laplace",
        domain="unit-square",
        assumptions=("linear well-posed BVP",),
    )
    inv = structural_invariant(
        "streamfunction_2d",
        "u = d_y psi, v = -d_x psi => div u = 0",
        assumptions=("mixed partials commute",),
    )
    cert = aposteriori_error_certificate(
        _AFFINE,
        _DOMAIN,
        laplace(2),
        stability=stability,
        invariants=[inv],
        max_error=1e-6,
        splits=2,
    )
    payload = cert.certificate["payload"]
    assert payload["stability"]["source"] == "maximum-principle fixture"
    assert payload["invariants"][0]["kind"] == "streamfunction_2d"
    assert payload["finite_obligation"]["type"] == "error_bound_le_threshold"
    assert generate_obligation(cert.certificate) is not None

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

Read the implementation

def structural_invariant(
    kind: str,
    expression: str,
    *,
    assumptions: Sequence[str] = (),
    certified: bool = True,
    method: str = "structural_identity",
) -> StructuralInvariant:
    """Create a serialisable record for an invariant enforced by construction."""
    if not kind:
        raise ValueError("invariant kind must be non-empty")
    if certified and not expression:
        raise ValueError("certified structural invariants need an expression")
    return StructuralInvariant(
        kind=str(kind),
        expression=str(expression),
        certified=bool(certified),
        assumptions=tuple(str(a) for a in assumptions),
        method=str(method),
    )

FUNCTION

user_stability_estimate

omnibias.core.verified.pde_certificate.user_stability_estimateSource ↗

user_stability_estimate(interior: float, boundary: float, *, source: str='user_supplied', pde_family: str='unspecified', domain: str='unspecified', assumptions: Sequence[str]=()) -> StabilityEstimate

Build an explicit user-supplied stability estimate record.

Parameters

Name	Type & default	Contract
`interior`positional-or-keyword	`float`Required	See the operation contract and implementation below.
`boundary`positional-or-keyword	`float`Required	See the operation contract and implementation below.
`source`keyword-only	`str`Default: 'user_supplied'	See the operation contract and implementation below.
`pde_family`keyword-only	`str`Default: 'unspecified'	See the operation contract and implementation below.
`domain`keyword-only	`str`Default: 'unspecified'	See the operation contract and implementation below.
`assumptions`keyword-only	`Sequence[str]`Default: ()	See the operation contract and implementation below.

ReturnsStabilityEstimate

Executed regression · aposteriori negative stability raises

Full file, imports & fixtures ↗

def test_aposteriori_negative_stability_raises() -> None:
    with pytest.raises(ValueError):
        aposteriori_error_certificate(
            _AFFINE,
            _DOMAIN,
            laplace(2),
            stability_interior=-1.0,
            stability_boundary=1.0,
        )

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

Regression example · aposteriori records stability invariants and formal margin

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_aposteriori_records_stability_invariants_and_formal_margin() -> None:
    stability = user_stability_estimate(
        0.5,
        1.0,
        source="maximum-principle fixture",
        pde_family="laplace",
        domain="unit-square",
        assumptions=("linear well-posed BVP",),
    )
    inv = structural_invariant(
        "streamfunction_2d",
        "u = d_y psi, v = -d_x psi => div u = 0",
        assumptions=("mixed partials commute",),
    )
    cert = aposteriori_error_certificate(
        _AFFINE,
        _DOMAIN,
        laplace(2),
        stability=stability,
        invariants=[inv],
        max_error=1e-6,
        splits=2,
    )
    payload = cert.certificate["payload"]
    assert payload["stability"]["source"] == "maximum-principle fixture"
    assert payload["invariants"][0]["kind"] == "streamfunction_2d"
    assert payload["finite_obligation"]["type"] == "error_bound_le_threshold"
    assert generate_obligation(cert.certificate) is not None

python -m pytest packages/omnibias-core/tests/test_verified_pde_certificate.py -k test_aposteriori_records_stability_invariants_and_formal_margin -q

Read the implementation

def user_stability_estimate(
    interior: float,
    boundary: float,
    *,
    source: str = "user_supplied",
    pde_family: str = "unspecified",
    domain: str = "unspecified",
    assumptions: Sequence[str] = (),
) -> StabilityEstimate:
    """Build an explicit user-supplied stability estimate record."""
    return StabilityEstimate(
        float(interior),
        float(boundary),
        source=source,
        pde_family=pde_family,
        domain=domain,
        assumptions=tuple(str(a) for a in assumptions),
        library_provided=False,
    )

← Package overview Runnable learning examples →

omnibias.core.verified.pde_certificate

AdaptiveResidualDiagnostics​

Parameters

Fields & methods

BoundaryFace​

Parameters

Fields & methods

CertifiedResidualCallback​

Coeff​

LinearPDE​

Parameters

Fields & methods

Parameters

PINNErrorCertificate​

Parameters

Fields & methods

StabilityEstimate​

Parameters

Fields & methods

StructuralInvariant​

Parameters

Fields & methods

adaptive_certified_interior_residual​

Parameters

advection_diffusion​

Parameters

aposteriori_error_certificate​

Parameters

certified_boundary_residual​

Parameters

certified_custom_residual​

Parameters

certified_interior_residual​

Parameters

certified_quadratic_reaction_residual​

Parameters

certified_streamfunction_divergence​

Parameters

certified_vorticity_transport_residual​

Parameters

helmholtz​

Parameters

laplace​

Parameters

pinn_aposteriori_schema_errors​

Parameters

poisson​

Parameters

radii_polynomial_residual_certificate​

Parameters

replay_pinn_aposteriori_certificate​

Parameters

screened_poisson​

Parameters

spectral_residual_norm​

Parameters

structural_invariant​

Parameters

user_stability_estimate​

Parameters

AdaptiveResidualDiagnostics

BoundaryFace

CertifiedResidualCallback

Coeff

LinearPDE

PINNErrorCertificate

StabilityEstimate

StructuralInvariant

adaptive_certified_interior_residual

advection_diffusion

aposteriori_error_certificate

certified_boundary_residual

certified_custom_residual

certified_interior_residual

certified_quadratic_reaction_residual

certified_streamfunction_divergence

certified_vorticity_transport_residual

helmholtz

laplace

pinn_aposteriori_schema_errors

poisson

radii_polynomial_residual_certificate

replay_pinn_aposteriori_certificate

screened_poisson

spectral_residual_norm

structural_invariant

user_stability_estimate