API REFERENCE/omnibias-core

omnibias.core.proof.obligations.rational_stencil

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.proof.obligations.rational_stencil

Module contract & mathematical conventions

Finite rational stencil obligations (theory 01-11).

The consistency conditions of a scale-free stencil are equalities of rationals

C_j = sum_{(i,p)} A_{i,p} c_i^{j-p} / (j-p)! = [j == q],

together with the reported leading moment C_N and (for a Birkhoff support) the Polya comparisons plus a nonzero confluent-Vandermonde determinant. Every quantity is a fraction of integers. Lean checks that finite algebra; it does not see a collapse, a Taylor remainder, or any statement quantified over a function class.

theorem_prover_verified is earned only by a genuine kernel lake build. This module never writes that flag into a certificate. mathlib_verified is a distinct tier and is never set here.

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

Obligation

omnibias.core.proof.ObligationSource ↗

class Obligation

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

A finite rational payload ready to seal. holds is Python algebra.

Parameters

Name	Type & default	Contract
kinddataclass field	strRequired	See the operation contract and implementation below.
payloaddataclass field	dict[str, Any]Required	See the operation contract and implementation below.
holdsdataclass field	boolRequired	See the operation contract and implementation below.
max_abs_intdataclass field	intRequired	See the operation contract and implementation below.

Regression example · seal report refuses obligation above integer cap

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_seal_report_refuses_obligation_above_integer_cap(
    monkeypatch: pytest.MonkeyPatch,
) -> None:
    """The CI-size cap must reject before constructing a certificate."""
    obligation = rational_stencil.Obligation(
        kind=PAYLOAD_STENCIL,
        payload={"type": PAYLOAD_STENCIL, "conditions": []},
        holds=True,
        max_abs_int=rational_stencil._INT_CAP + 1,
    )

    def should_not_run(**_kwargs: object) -> object:
        raise AssertionError("make_certificate must not run beyond _INT_CAP")

    monkeypatch.setattr(rational_stencil, "make_certificate", should_not_run)
    with pytest.raises(ValueError, match=r"integers exceed cap"):
        rational_stencil._seal_report(
            obligation,
            claim="oversized finite rational obligation",
            run_lean=False,
        )

python -m pytest packages/omnibias-core/tests/test_rational_stencil.py -k test_seal_report_refuses_obligation_above_integer_cap -q

Fields & methods

kindfield

kind: str

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

View source ↗

payloadfield

payload: dict[str, Any]

Declared dict[str, Any] field on Obligation. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

holdsfield

holds: bool

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

View source ↗

max_abs_intfield

max_abs_int: int

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

View source ↗

Read the implementation

class Obligation:
    """A finite rational payload ready to seal. ``holds`` is Python algebra."""

    kind: str
    payload: dict[str, Any]
    holds: bool
    max_abs_int: int

Other public import paths

• omnibias.core.proof.Obligation
• omnibias.core.proof.obligations.Obligation
• omnibias.core.proof.obligations.rational_stencil.Obligation

CONSTANT

PAYLOAD_POISEDNESS

omnibias.core.proof.obligations.PAYLOAD_POISEDNESSSource ↗

PAYLOAD_POISEDNESS = 'rational_poisedness'

This exported constant is defined by the expression above. Its exact value and annotation come from the pinned source; use it with the module contract.

Regression example · polya failure is not poised

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_polya_failure_is_not_poised() -> None:
    spec = MultiPackSpec.from_packs((PackSpec(order=2, mean=0.0),))
    obl = poisedness_obligation(spec)
    assert obl.holds is False
    assert obl.payload["type"] == PAYLOAD_POISEDNESS

python -m pytest packages/omnibias-core/tests/test_rational_stencil.py -k test_polya_failure_is_not_poised -q

Read the implementation

PAYLOAD_POISEDNESS = "rational_poisedness"

Other public import paths

• omnibias.core.proof.obligations.PAYLOAD_POISEDNESS
• omnibias.core.proof.obligations.rational_stencil.PAYLOAD_POISEDNESS

CONSTANT

PAYLOAD_STENCIL

omnibias.core.proof.obligations.PAYLOAD_STENCILSource ↗

PAYLOAD_STENCIL = 'rational_stencil_consistency'

This exported constant is defined by the expression above. Its exact value and annotation come from the pinned source; use it with the module contract.

Regression example · malformed stencil payload emits nothing

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_malformed_stencil_payload_emits_nothing() -> None:
    from omnibias.core.proof.certificate import make_certificate

    cert = make_certificate(
        claim="x",
        payload={"type": PAYLOAD_STENCIL, "conditions": []},
        honesty={},
    )
    assert generate_obligation(cert) is None

python -m pytest packages/omnibias-core/tests/test_rational_stencil.py -k test_malformed_stencil_payload_emits_nothing -q

Regression example · cannot forge theorem prover verified into seal

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_cannot_forge_theorem_prover_verified_into_seal() -> None:
    from omnibias.core.proof.certificate import make_certificate

    try:
        make_certificate(
            claim="forged",
            payload={"type": PAYLOAD_STENCIL, "conditions": []},
            honesty={"theorem_prover_verified": True},
        )
    except ValueError as exc:
        assert "theorem_prover_verified" in str(exc)
    else:
        raise AssertionError("forged formal flag must be refused")

python -m pytest packages/omnibias-core/tests/test_rational_stencil.py -k test_cannot_forge_theorem_prover_verified_into_seal -q

Read the implementation

PAYLOAD_STENCIL = "rational_stencil_consistency"

Other public import paths

• omnibias.core.proof.obligations.PAYLOAD_STENCIL
• omnibias.core.proof.obligations.rational_stencil.PAYLOAD_STENCIL

CLASS

RationalStencil

omnibias.core.proof.RationalStencilSource ↗

class RationalStencil

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.

Scale-free stencil A_{i,p} at nodes c_i (units of h).

leading_coeff is the reported C_N. Omit it to use the computed moment (self-check of the algebra, not of a foreign generator).

Parameters

Name	Type & default	Contract
nodesdataclass field	tuple[Fraction, ...]Required	See the operation contract and implementation below.
ordersdataclass field	tuple[tuple[int, ...], ...]Required	See the operation contract and implementation below.
weightsdataclass field	tuple[tuple[Fraction, ...], ...]Required	See the operation contract and implementation below.
target_orderdataclass field	intRequired	See the operation contract and implementation below.
leading_coeffdataclass field	Fraction | NoneDefault: None	See the operation contract and implementation below.
namedataclass field	strDefault: ''	See the operation contract and implementation below.

Executed regression · birkhoff spec moments

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

Full file, imports & fixtures ↗

def test_birkhoff_spec_moments() -> None:
    st = birkhoff_spec_stencil()
    assert st.moment_sum(0) == 0
    assert st.moment_sum(1) == 1
    assert st.moment_sum(2) == 0
    assert st.computed_leading() == Fraction(5, 18)
    assert stencil_consistency_obligation(st).holds

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_birkhoff_spec_moments" -q

Fields & methods

nodesfield

nodes: tuple[Fraction, ...]

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

View source ↗

ordersfield

orders: tuple[tuple[int, ...], ...]

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

View source ↗

weightsfield

weights: tuple[tuple[Fraction, ...], ...]

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

View source ↗

target_orderfield

target_order: int

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

View source ↗

leading_coefffield

leading_coeff: Fraction | None = None

Declared Fraction | None field on RationalStencil. Default expression: None.

View source ↗

namefield

name: str = ''

Declared str field on RationalStencil. Default expression: ''.

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 not nodes, raises ValueError('RationalStencil requires at least one node').
• When len(set(nodes)) != len(nodes), raises ValueError('nodes must be distinct').
• When len(nodes) != len(orders), raises ValueError('nodes and orders must have the same length').
• When len(weights) != len(nodes), raises ValueError('weights must match nodes').
• When len(ords) != len(row), raises ValueError(f'weights[{i}] must match orders[{i}]').
• When q < 0, raises ValueError(f'target_order must be >= 0, got {q}').

Executed regression · birkhoff spec moments

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

Full file, imports & fixtures ↗

def test_birkhoff_spec_moments() -> None:
    st = birkhoff_spec_stencil()
    assert st.moment_sum(0) == 0
    assert st.moment_sum(1) == 1
    assert st.moment_sum(2) == 0
    assert st.computed_leading() == Fraction(5, 18)
    assert stencil_consistency_obligation(st).holds

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_birkhoff_spec_moments" -q

Method implementation

    def __post_init__(self) -> None:
        nodes = tuple(_as_frac(c) for c in self.nodes)
        if not nodes:
            raise ValueError("RationalStencil requires at least one node")
        if len(set(nodes)) != len(nodes):
            raise ValueError("nodes must be distinct")
        orders = _as_orders(self.orders)
        if len(nodes) != len(orders):
            raise ValueError("nodes and orders must have the same length")
        weights = tuple(tuple(_as_frac(a) for a in row) for row in self.weights)
        if len(weights) != len(nodes):
            raise ValueError("weights must match nodes")
        for i, (ords, row) in enumerate(zip(orders, weights, strict=True)):
            if len(ords) != len(row):
                raise ValueError(f"weights[{i}] must match orders[{i}]")
        q = int(self.target_order)
        if q < 0:
            raise ValueError(f"target_order must be >= 0, got {q}")
        lead = None if self.leading_coeff is None else _as_frac(self.leading_coeff)
        object.__setattr__(self, "nodes", nodes)
        object.__setattr__(self, "orders", orders)
        object.__setattr__(self, "weights", weights)
        object.__setattr__(self, "target_order", q)
        object.__setattr__(self, "leading_coeff", lead)
        object.__setattr__(self, "name", str(self.name))

View source ↗

n_conditionsproperty

n_conditions(self) -> int

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

Returns: int

Executed regression · birkhoff spec moments

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

Full file, imports & fixtures ↗

def test_birkhoff_spec_moments() -> None:
    st = birkhoff_spec_stencil()
    assert st.moment_sum(0) == 0
    assert st.moment_sum(1) == 1
    assert st.moment_sum(2) == 0
    assert st.computed_leading() == Fraction(5, 18)
    assert stencil_consistency_obligation(st).holds

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_birkhoff_spec_moments" -q

Method implementation

    def n_conditions(self) -> int:
        return sum(len(o) for o in self.orders)

View source ↗

pairsmethod

pairs(self) -> tuple[tuple[int, int], ...]

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

Returns: tuple[tuple[int, int], ...]

Executed regression · birkhoff spec moments

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

Full file, imports & fixtures ↗

def test_birkhoff_spec_moments() -> None:
    st = birkhoff_spec_stencil()
    assert st.moment_sum(0) == 0
    assert st.moment_sum(1) == 1
    assert st.moment_sum(2) == 0
    assert st.computed_leading() == Fraction(5, 18)
    assert stencil_consistency_obligation(st).holds

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_birkhoff_spec_moments" -q

Method implementation

    def pairs(self) -> tuple[tuple[int, int], ...]:
        out: list[tuple[int, int]] = []
        for i, ords in enumerate(self.orders):
            for p in ords:
                out.append((i, p))
        return tuple(out)

View source ↗

moment_summethod

moment_sum(self, j: int) -> Fraction

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

Parameters

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

Returns: Fraction

Executed regression · birkhoff spec moments

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

Full file, imports & fixtures ↗

def test_birkhoff_spec_moments() -> None:
    st = birkhoff_spec_stencil()
    assert st.moment_sum(0) == 0
    assert st.moment_sum(1) == 1
    assert st.moment_sum(2) == 0
    assert st.computed_leading() == Fraction(5, 18)
    assert stencil_consistency_obligation(st).holds

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_birkhoff_spec_moments" -q

Method implementation

    def moment_sum(self, j: int) -> Fraction:
        acc = Fraction(0)
        for (i, p), a in zip(self.pairs(), self.flat_weights(), strict=True):
            acc += a * _moment(self.nodes[i], j, p)
        return acc

View source ↗

flat_weightsmethod

flat_weights(self) -> tuple[Fraction, ...]

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

Returns: tuple[Fraction, ...]

Executed regression · birkhoff spec moments

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

Full file, imports & fixtures ↗

def test_birkhoff_spec_moments() -> None:
    st = birkhoff_spec_stencil()
    assert st.moment_sum(0) == 0
    assert st.moment_sum(1) == 1
    assert st.moment_sum(2) == 0
    assert st.computed_leading() == Fraction(5, 18)
    assert stencil_consistency_obligation(st).holds

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_birkhoff_spec_moments" -q

Method implementation

    def flat_weights(self) -> tuple[Fraction, ...]:
        return tuple(a for row in self.weights for a in row)

View source ↗

computed_leadingmethod

computed_leading(self) -> Fraction

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

Returns: Fraction

Executed regression · birkhoff spec moments

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

Full file, imports & fixtures ↗

def test_birkhoff_spec_moments() -> None:
    st = birkhoff_spec_stencil()
    assert st.moment_sum(0) == 0
    assert st.moment_sum(1) == 1
    assert st.moment_sum(2) == 0
    assert st.computed_leading() == Fraction(5, 18)
    assert stencil_consistency_obligation(st).holds

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_birkhoff_spec_moments" -q

Method implementation

    def computed_leading(self) -> Fraction:
        return self.moment_sum(self.n_conditions)

View source ↗

reported_leadingmethod

reported_leading(self) -> Fraction

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

Returns: Fraction

Executed regression · birkhoff spec moments

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

Full file, imports & fixtures ↗

def test_birkhoff_spec_moments() -> None:
    st = birkhoff_spec_stencil()
    assert st.moment_sum(0) == 0
    assert st.moment_sum(1) == 1
    assert st.moment_sum(2) == 0
    assert st.computed_leading() == Fraction(5, 18)
    assert stencil_consistency_obligation(st).holds

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_birkhoff_spec_moments" -q

Method implementation

    def reported_leading(self) -> Fraction:
        return self.leading_coeff if self.leading_coeff is not None else self.computed_leading()

View source ↗

with_flat_weightsmethod

with_flat_weights(self, flat: Sequence[Fraction | int | str]) -> RationalStencil

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

Parameters

Name	Type & default	Contract
flatpositional-or-keyword	Sequence[Fraction | int | str]Required	See the operation contract and implementation below.

Returns: RationalStencil

Validation & failure cases

• When len(seq) != self.n_conditions, raises ValueError('flat weight length mismatch').

Executed regression · corrupted weights fail python algebra

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_corrupted_weights_fail_python_algebra() -> None:
    bad = birkhoff_spec_stencil().corrupt_first_weight()
    obl = stencil_consistency_obligation(bad)
    assert obl.holds is False
    src = generate_obligation(
        seal_stencil_certificate(bad, run_lean=False).certificate
    )
    assert src is not None
    assert "allRatEq" in src

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_corrupted_weights_fail_python_algebra" -q

Method implementation

    def with_flat_weights(self, flat: Sequence[Fraction | int | str]) -> RationalStencil:
        seq = tuple(_as_frac(a) for a in flat)
        if len(seq) != self.n_conditions:
            raise ValueError("flat weight length mismatch")
        packed: list[tuple[Fraction, ...]] = []
        k = 0
        for ords in self.orders:
            n = len(ords)
            packed.append(seq[k : k + n])
            k += n
        return RationalStencil(
            self.nodes,
            self.orders,
            tuple(packed),
            self.target_order,
            leading_coeff=self.leading_coeff,
            name=self.name,
        )

View source ↗

corrupt_first_weightmethod

corrupt_first_weight(self, *, factor: Fraction | int=2) -> RationalStencil

Deliberately break consistency (G2 negative control).

Parameters

Name	Type & default	Contract
factorkeyword-only	Fraction | intDefault: 2	See the operation contract and implementation below.

Returns: RationalStencil

Validation & failure cases

• When not flat, raises ValueError('no weights to corrupt').

Executed regression · corrupted weights fail python algebra

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_corrupted_weights_fail_python_algebra() -> None:
    bad = birkhoff_spec_stencil().corrupt_first_weight()
    obl = stencil_consistency_obligation(bad)
    assert obl.holds is False
    src = generate_obligation(
        seal_stencil_certificate(bad, run_lean=False).certificate
    )
    assert src is not None
    assert "allRatEq" in src

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_corrupted_weights_fail_python_algebra" -q

Method implementation

    def corrupt_first_weight(self, *, factor: Fraction | int = 2) -> RationalStencil:
        """Deliberately break consistency (G2 negative control)."""
        flat = list(self.flat_weights())
        if not flat:
            raise ValueError("no weights to corrupt")
        flat[0] = flat[0] * _as_frac(factor)
        return self.with_flat_weights(flat)

View source ↗

Read the implementation

class RationalStencil:
    """Scale-free stencil ``A_{i,p}`` at nodes ``c_i`` (units of ``h``).

    ``leading_coeff`` is the reported ``C_N``. Omit it to use the computed
    moment (self-check of the algebra, not of a foreign generator).
    """

    nodes: tuple[Fraction, ...]
    orders: tuple[tuple[int, ...], ...]
    weights: tuple[tuple[Fraction, ...], ...]
    target_order: int
    leading_coeff: Fraction | None = None
    name: str = ""

    def __post_init__(self) -> None:
        nodes = tuple(_as_frac(c) for c in self.nodes)
        if not nodes:
            raise ValueError("RationalStencil requires at least one node")
        if len(set(nodes)) != len(nodes):
            raise ValueError("nodes must be distinct")
        orders = _as_orders(self.orders)
        if len(nodes) != len(orders):
            raise ValueError("nodes and orders must have the same length")
        weights = tuple(tuple(_as_frac(a) for a in row) for row in self.weights)
        if len(weights) != len(nodes):
            raise ValueError("weights must match nodes")
        for i, (ords, row) in enumerate(zip(orders, weights, strict=True)):
            if len(ords) != len(row):
                raise ValueError(f"weights[{i}] must match orders[{i}]")
        q = int(self.target_order)
        if q < 0:
            raise ValueError(f"target_order must be >= 0, got {q}")
        lead = None if self.leading_coeff is None else _as_frac(self.leading_coeff)
        object.__setattr__(self, "nodes", nodes)
        object.__setattr__(self, "orders", orders)
        object.__setattr__(self, "weights", weights)
        object.__setattr__(self, "target_order", q)
        object.__setattr__(self, "leading_coeff", lead)
        object.__setattr__(self, "name", str(self.name))

    @property
    def n_conditions(self) -> int:
        return sum(len(o) for o in self.orders)

    def pairs(self) -> tuple[tuple[int, int], ...]:
        out: list[tuple[int, int]] = []
        for i, ords in enumerate(self.orders):
            for p in ords:
                out.append((i, p))
        return tuple(out)

    def moment_sum(self, j: int) -> Fraction:
        acc = Fraction(0)
        for (i, p), a in zip(self.pairs(), self.flat_weights(), strict=True):
            acc += a * _moment(self.nodes[i], j, p)
        return acc

    def flat_weights(self) -> tuple[Fraction, ...]:
        return tuple(a for row in self.weights for a in row)

    def computed_leading(self) -> Fraction:
        return self.moment_sum(self.n_conditions)

    def reported_leading(self) -> Fraction:
        return self.leading_coeff if self.leading_coeff is not None else self.computed_leading()

    def with_flat_weights(self, flat: Sequence[Fraction | int | str]) -> RationalStencil:
        seq = tuple(_as_frac(a) for a in flat)
        if len(seq) != self.n_conditions:
            raise ValueError("flat weight length mismatch")
        packed: list[tuple[Fraction, ...]] = []
        k = 0
        for ords in self.orders:
            n = len(ords)
            packed.append(seq[k : k + n])
            k += n
        return RationalStencil(
            self.nodes,
            self.orders,
            tuple(packed),
            self.target_order,
            leading_coeff=self.leading_coeff,
            name=self.name,
        )

    def corrupt_first_weight(self, *, factor: Fraction | int = 2) -> RationalStencil:
        """Deliberately break consistency (G2 negative control)."""
        flat = list(self.flat_weights())
        if not flat:
            raise ValueError("no weights to corrupt")
        flat[0] = flat[0] * _as_frac(factor)
        return self.with_flat_weights(flat)

Other public import paths

• omnibias.core.proof.RationalStencil
• omnibias.core.proof.obligations.RationalStencil
• omnibias.core.proof.obligations.rational_stencil.RationalStencil

CLASS

RationalSupport

omnibias.core.proof.RationalSupportSource ↗

class RationalSupport

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.

Birkhoff support (nodes + per-node orders) for exact poisedness.

Parameters

Name	Type & default	Contract
nodesdataclass field	tuple[Fraction, ...]Required	See the operation contract and implementation below.
ordersdataclass field	tuple[tuple[int, ...], ...]Required	See the operation contract and implementation below.
namedataclass field	strDefault: ''	See the operation contract and implementation below.

Executed regression · polya failure is not poised

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_polya_failure_is_not_poised() -> None:
    spec = MultiPackSpec.from_packs((PackSpec(order=2, mean=0.0),))
    obl = poisedness_obligation(spec)
    assert obl.holds is False
    assert obl.payload["type"] == PAYLOAD_POISEDNESS

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_polya_failure_is_not_poised" -q

Fields & methods

nodesfield

nodes: tuple[Fraction, ...]

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

View source ↗

ordersfield

orders: tuple[tuple[int, ...], ...]

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

View source ↗

namefield

name: str = ''

Declared str field on RationalSupport. Default expression: ''.

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 not nodes, raises ValueError('RationalSupport requires at least one node').
• When len(set(nodes)) != len(nodes), raises ValueError('nodes must be distinct').
• When len(nodes) != len(orders), raises ValueError('nodes and orders must have the same length').

Executed regression · polya failure is not poised

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_polya_failure_is_not_poised() -> None:
    spec = MultiPackSpec.from_packs((PackSpec(order=2, mean=0.0),))
    obl = poisedness_obligation(spec)
    assert obl.holds is False
    assert obl.payload["type"] == PAYLOAD_POISEDNESS

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_polya_failure_is_not_poised" -q

Method implementation

    def __post_init__(self) -> None:
        nodes = tuple(_as_frac(c) for c in self.nodes)
        if not nodes:
            raise ValueError("RationalSupport requires at least one node")
        if len(set(nodes)) != len(nodes):
            raise ValueError("nodes must be distinct")
        orders = _as_orders(self.orders)
        if len(nodes) != len(orders):
            raise ValueError("nodes and orders must have the same length")
        object.__setattr__(self, "nodes", nodes)
        object.__setattr__(self, "orders", orders)
        object.__setattr__(self, "name", str(self.name))

View source ↗

n_conditionsproperty

n_conditions(self) -> int

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

Returns: int

Executed regression · polya failure is not poised

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_polya_failure_is_not_poised() -> None:
    spec = MultiPackSpec.from_packs((PackSpec(order=2, mean=0.0),))
    obl = poisedness_obligation(spec)
    assert obl.holds is False
    assert obl.payload["type"] == PAYLOAD_POISEDNESS

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_polya_failure_is_not_poised" -q

Method implementation

    def n_conditions(self) -> int:
        return sum(len(o) for o in self.orders)

View source ↗

pairsmethod

pairs(self) -> tuple[tuple[int, int], ...]

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

Returns: tuple[tuple[int, int], ...]

Executed regression · polya failure is not poised

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_polya_failure_is_not_poised() -> None:
    spec = MultiPackSpec.from_packs((PackSpec(order=2, mean=0.0),))
    obl = poisedness_obligation(spec)
    assert obl.holds is False
    assert obl.payload["type"] == PAYLOAD_POISEDNESS

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_polya_failure_is_not_poised" -q

Method implementation

    def pairs(self) -> tuple[tuple[int, int], ...]:
        out: list[tuple[int, int]] = []
        for i, ords in enumerate(self.orders):
            for p in ords:
                out.append((i, p))
        return tuple(out)

View source ↗

from_stencilmethod

from_stencil(cls, stencil: RationalStencil) -> RationalSupport

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

Parameters

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

Returns: RationalSupport

Executed regression · birkhoff poisedness det

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

Full file, imports & fixtures ↗

def test_birkhoff_poisedness_det() -> None:
    obl = poisedness_obligation(birkhoff_spec_stencil())
    assert obl.holds
    assert obl.payload["det"] == ["3", "2"]
    via_mp = poisedness_obligation(birkhoff_spec_multipack())
    assert via_mp.holds
    assert via_mp.payload["det"] == ["3", "2"]

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_birkhoff_poisedness_det" -q

Method implementation

    def from_stencil(cls, stencil: RationalStencil) -> RationalSupport:
        return cls(stencil.nodes, stencil.orders, name=stencil.name)

View source ↗

from_multipackmethod

from_multipack(cls, spec: MultiPackSpec, *, name: str='') -> RationalSupport

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

Parameters

Name	Type & default	Contract
specpositional-or-keyword	MultiPackSpecRequired	See the operation contract and implementation below.
namekeyword-only	strDefault: ''	See the operation contract and implementation below.

Returns: RationalSupport

Executed regression · polya failure is not poised

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_polya_failure_is_not_poised() -> None:
    spec = MultiPackSpec.from_packs((PackSpec(order=2, mean=0.0),))
    obl = poisedness_obligation(spec)
    assert obl.holds is False
    assert obl.payload["type"] == PAYLOAD_POISEDNESS

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_polya_failure_is_not_poised" -q

Method implementation

    def from_multipack(cls, spec: MultiPackSpec, *, name: str = "") -> RationalSupport:
        means = spec.distinct_means
        e = incidence_matrix(spec)
        nodes = tuple(_mean_to_fraction(m) for m in means)
        orders = tuple(tuple(j for j, flag in enumerate(row) if flag) for row in e)
        return cls(nodes, orders, name=name)

View source ↗

Read the implementation

class RationalSupport:
    """Birkhoff support (nodes + per-node orders) for exact poisedness."""

    nodes: tuple[Fraction, ...]
    orders: tuple[tuple[int, ...], ...]
    name: str = ""

    def __post_init__(self) -> None:
        nodes = tuple(_as_frac(c) for c in self.nodes)
        if not nodes:
            raise ValueError("RationalSupport requires at least one node")
        if len(set(nodes)) != len(nodes):
            raise ValueError("nodes must be distinct")
        orders = _as_orders(self.orders)
        if len(nodes) != len(orders):
            raise ValueError("nodes and orders must have the same length")
        object.__setattr__(self, "nodes", nodes)
        object.__setattr__(self, "orders", orders)
        object.__setattr__(self, "name", str(self.name))

    @property
    def n_conditions(self) -> int:
        return sum(len(o) for o in self.orders)

    def pairs(self) -> tuple[tuple[int, int], ...]:
        out: list[tuple[int, int]] = []
        for i, ords in enumerate(self.orders):
            for p in ords:
                out.append((i, p))
        return tuple(out)

    @classmethod
    def from_stencil(cls, stencil: RationalStencil) -> RationalSupport:
        return cls(stencil.nodes, stencil.orders, name=stencil.name)

    @classmethod
    def from_multipack(cls, spec: MultiPackSpec, *, name: str = "") -> RationalSupport:
        means = spec.distinct_means
        e = incidence_matrix(spec)
        nodes = tuple(_mean_to_fraction(m) for m in means)
        orders = tuple(tuple(j for j, flag in enumerate(row) if flag) for row in e)
        return cls(nodes, orders, name=name)

Related APIsomnibias.core.incidence_matrix↗

Other public import paths

• omnibias.core.proof.RationalSupport
• omnibias.core.proof.obligations.RationalSupport
• omnibias.core.proof.obligations.rational_stencil.RationalSupport

CLASS

StencilCertificateReport

omnibias.core.proof.StencilCertificateReportSource ↗

class StencilCertificateReport

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.

Sealed certificate plus the kernel / Mathlib flags for this spec.

mathlib_verified is always False: this path never touches the Mathlib-backed project.

Parameters

Name	Type & default	Contract
certificatedataclass field	dict[str, Any]Required	See the operation contract and implementation below.
obligationdataclass field	ObligationRequired	See the operation contract and implementation below.
theorem_prover_verifieddataclass field	boolRequired	See the operation contract and implementation below.
mathlib_verifieddataclass field	boolRequired	See the operation contract and implementation below.
leandataclass field	LeanCheckResult | NoneRequired	See the operation contract and implementation below.
wall_secondsdataclass field	float | NoneRequired	See the operation contract and implementation below.

Fields & methods

certificatefield

certificate: dict[str, Any]

Declared dict[str, Any] field on StencilCertificateReport. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

obligationfield

obligation: Obligation

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

View source ↗

theorem_prover_verifiedfield

theorem_prover_verified: bool

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

View source ↗

mathlib_verifiedfield

mathlib_verified: bool

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

View source ↗

leanfield

lean: LeanCheckResult | None

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

View source ↗

wall_secondsfield

wall_seconds: float | None

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

View source ↗

Read the implementation

class StencilCertificateReport:
    """Sealed certificate plus the kernel / Mathlib flags for this spec.

    ``mathlib_verified`` is always ``False``: this path never touches the
    Mathlib-backed project.
    """

    certificate: dict[str, Any]
    obligation: Obligation
    theorem_prover_verified: bool
    mathlib_verified: bool
    lean: LeanCheckResult | None
    wall_seconds: float | None

Other public import paths

• omnibias.core.proof.StencilCertificateReport
• omnibias.core.proof.obligations.StencilCertificateReport
• omnibias.core.proof.obligations.rational_stencil.StencilCertificateReport

FUNCTION

birkhoff_spec_multipack

omnibias.core.proof.obligations.rational_stencil.birkhoff_spec_multipackSource ↗

birkhoff_spec_multipack() -> MultiPackSpec

The module contract describes the context for this operation. Its signature, explicit validation, return expressions, and implementation are recorded below.

ReturnsMultiPackSpec

Executed regression · birkhoff poisedness det

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

Full file, imports & fixtures ↗

def test_birkhoff_poisedness_det() -> None:
    obl = poisedness_obligation(birkhoff_spec_stencil())
    assert obl.holds
    assert obl.payload["det"] == ["3", "2"]
    via_mp = poisedness_obligation(birkhoff_spec_multipack())
    assert via_mp.holds
    assert via_mp.payload["det"] == ["3", "2"]

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_birkhoff_poisedness_det" -q

Read the implementation

def birkhoff_spec_multipack() -> MultiPackSpec:
    return MultiPackSpec.from_packs(
        (
            PackSpec(order=0, mean=-1.0),
            PackSpec(order=0, mean=0.0),
            PackSpec(order=1, mean=1.0),
        )
    )

Related APIsomnibias.core.PackSpec↗

FUNCTION

birkhoff_spec_stencil

omnibias.core.proof.obligations.rational_stencil.birkhoff_spec_stencilSource ↗

birkhoff_spec_stencil() -> RationalStencil

Worked example from spec 01-11 / 01-04.

ReturnsRationalStencil

Executed regression · birkhoff spec moments

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

Full file, imports & fixtures ↗

def test_birkhoff_spec_moments() -> None:
    st = birkhoff_spec_stencil()
    assert st.moment_sum(0) == 0
    assert st.moment_sum(1) == 1
    assert st.moment_sum(2) == 0
    assert st.computed_leading() == Fraction(5, 18)
    assert stencil_consistency_obligation(st).holds

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_birkhoff_spec_moments" -q

Regression example · birkhoff poisedness det

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_birkhoff_poisedness_det() -> None:
    obl = poisedness_obligation(birkhoff_spec_stencil())
    assert obl.holds
    assert obl.payload["det"] == ["3", "2"]
    via_mp = poisedness_obligation(birkhoff_spec_multipack())
    assert via_mp.holds
    assert via_mp.payload["det"] == ["3", "2"]

python -m pytest packages/omnibias-core/tests/test_rational_stencil.py -k test_birkhoff_poisedness_det -q

Read the implementation

def birkhoff_spec_stencil() -> RationalStencil:
    """Worked example from spec 01-11 / 01-04."""
    for st in curated_rational_stencils():
        if st.name == "birkhoff_spec":
            return st
    raise RuntimeError("birkhoff_spec missing from curated set")

Related APIsomnibias.core.proof.curated_rational_stencils↗

FUNCTION

birkhoff_spec_support

omnibias.core.proof.obligations.rational_stencil.birkhoff_spec_supportSource ↗

birkhoff_spec_support() -> RationalSupport

The module contract describes the context for this operation. Its signature, explicit validation, return expressions, and implementation are recorded below.

ReturnsRationalSupport

Read the implementation

def birkhoff_spec_support() -> RationalSupport:
    return RationalSupport.from_stencil(birkhoff_spec_stencil())

Related APIsomnibias.core.proof.obligations.rational_stencil.birkhoff_spec_stencil↗

FUNCTION

curated_rational_stencils

omnibias.core.proof.curated_rational_stencilsSource ↗

curated_rational_stencils() -> tuple[RationalStencil, ...]

Uniform, irregular, and Birkhoff fixtures (more than 20).

Returnstuple[RationalStencil, ...]

Executed regression · birkhoff spec moments

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

Full file, imports & fixtures ↗

def test_birkhoff_spec_moments() -> None:
    st = birkhoff_spec_stencil()
    assert st.moment_sum(0) == 0
    assert st.moment_sum(1) == 1
    assert st.moment_sum(2) == 0
    assert st.computed_leading() == Fraction(5, 18)
    assert stencil_consistency_obligation(st).holds

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_birkhoff_spec_moments" -q

Regression example · curated set is consistent and large

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_curated_set_is_consistent_and_large() -> None:
    stencils = curated_rational_stencils()
    assert len(stencils) >= 20
    names = [s.name for s in stencils]
    assert len(names) == len(set(names))
    for st in stencils:
        obl = stencil_consistency_obligation(st)
        assert obl.holds, st.name
        assert obl.kind == PAYLOAD_STENCIL
        n = st.n_conditions
        for j in range(n):
            rhs = Fraction(1) if j == st.target_order else Fraction(0)
            assert st.moment_sum(j) == rhs, (st.name, j)

python -m pytest packages/omnibias-core/tests/test_rational_stencil.py -k test_curated_set_is_consistent_and_large -q

Read the implementation

def curated_rational_stencils() -> tuple[RationalStencil, ...]:
    """Uniform, irregular, and Birkhoff fixtures (more than 20)."""
    return (
        _value_only("fwd1_2", (0, 1), (-1, 1), 1),
        _value_only("bwd1_2", (-1, 0), (-1, 1), 1),
        _value_only("ctr1_2", (-1, 1), (Fraction(-1, 2), Fraction(1, 2)), 1),
        _value_only("fwd1_3", (0, 1, 2), (Fraction(-3, 2), 2, Fraction(-1, 2)), 1),
        _value_only("bwd1_3", (-2, -1, 0), (Fraction(1, 2), -2, Fraction(3, 2)), 1),
        _value_only("ctr2_3", (-1, 0, 1), (1, -2, 1), 2),
        _value_only("fwd2_3", (0, 1, 2), (1, -2, 1), 2),
        _value_only("bwd2_3", (-2, -1, 0), (1, -2, 1), 2),
        _value_only(
            "ctr1_4",
            (-2, -1, 1, 2),
            (Fraction(1, 12), Fraction(-2, 3), Fraction(2, 3), Fraction(-1, 12)),
            1,
        ),
        _value_only(
            "fwd1_4",
            (0, 1, 2, 3),
            (Fraction(-11, 6), 3, Fraction(-3, 2), Fraction(1, 3)),
            1,
        ),
        _value_only(
            "ctr2_5",
            (-2, -1, 0, 1, 2),
            (Fraction(-1, 12), Fraction(4, 3), Fraction(-5, 2), Fraction(4, 3), Fraction(-1, 12)),
            2,
        ),
        _value_only("ctr4_5", (-2, -1, 0, 1, 2), (1, -4, 6, -4, 1), 4),
        _value_only("fwd3_4", (0, 1, 2, 3), (-1, 3, -3, 1), 3),
        _value_only("interp2", (-1, 1), (Fraction(1, 2), Fraction(1, 2)), 0),
        _value_only("interp3", (-1, 0, 1), (0, 1, 0), 0),
        RationalStencil(
            (Fraction(-1), Fraction(0), Fraction(1)),
            ((0,), (0,), (1,)),
            ((Fraction(-2, 3),), (Fraction(2, 3),), (Fraction(1, 3),)),
            1,
            leading_coeff=Fraction(5, 18),
            name="birkhoff_spec",
        ),
        _value_only(
            "irr_half",
            (Fraction(-1, 2), 0, 1),
            (Fraction(-4, 3), 1, Fraction(1, 3)),
            1,
        ),
        _value_only(
            "irr_spread",
            (-2, -1, 1, 3),
            (Fraction(1, 15), Fraction(-5, 8), Fraction(7, 12), Fraction(-1, 40)),
            1,
        ),
        RationalStencil(
            (Fraction(-1), Fraction(1)),
            ((0,), (0, 1)),
            ((Fraction(-1, 2),), (Fraction(1, 2), Fraction(0))),
            1,
            name="birk_right",
        ),
        _value_only(
            "fwd1_5",
            (0, 1, 2, 3, 4),
            (Fraction(-25, 12), 4, -3, Fraction(4, 3), Fraction(-1, 4)),
            1,
        ),
        _value_only("ctr3_4", (-2, -1, 1, 2), (Fraction(-1, 2), 1, -1, Fraction(1, 2)), 3),
        RationalStencil(
            (Fraction(0), Fraction(1)),
            ((0, 1), (0,)),
            ((Fraction(0), Fraction(1)), (Fraction(0),)),
            1,
            name="hermite_q1",
        ),
    )

Related APIsomnibias.core.proof.RationalStencil↗

Other public import paths

• omnibias.core.proof.curated_rational_stencils
• omnibias.core.proof.obligations.curated_rational_stencils
• omnibias.core.proof.obligations.rational_stencil.curated_rational_stencils

FUNCTION

digest_is_valid

omnibias.core.proof.obligations.rational_stencil.digest_is_validSource ↗

digest_is_valid(cert: Mapping[str, Any]) -> bool

The module contract describes the context for this operation. Its signature, explicit validation, return expressions, and implementation are recorded below.

Parameters

Name	Type & default	Contract
certpositional-or-keyword	Mapping[str, Any]Required	See the operation contract and implementation below.

Returnsbool

Read the implementation

def digest_is_valid(cert: Mapping[str, Any]) -> bool:
    return verify_certificate_digest(cert)

Related APIsomnibias.core.proof.verify_certificate_digest↗

FUNCTION

honesty_payload

omnibias.core.proof.obligations.honesty_payloadSource ↗

honesty_payload() -> dict[str, bool]

Sealed honesty for the smoke artifact. Not a Lean pass.

Returnsdict[str, bool]

Executed regression · g5 tier separation

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_g5_tier_separation() -> None:
    st_report = seal_stencil_certificate(birkhoff_spec_stencil(), run_lean=True)
    po_report = seal_poisedness_certificate(birkhoff_spec_stencil(), run_lean=True)
    assert st_report.mathlib_verified is False
    assert po_report.mathlib_verified is False
    honesty = honesty_payload()
    assert honesty["mathlib_path_used"] is False
    assert honesty["collapse_limit_in_lean"] is False

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_g5_tier_separation" -q

Read the implementation

def honesty_payload() -> dict[str, bool]:
    """Sealed honesty for the smoke artifact. Not a Lean pass."""
    return {
        "unproven_claim": False,
        "collapse_limit_in_lean": False,
        "taylor_theorem_in_lean": False,
        "function_class_in_lean": False,
        "mathlib_path_used": False,
    }

Other public import paths

• omnibias.core.proof.obligations.honesty_payload
• omnibias.core.proof.obligations.rational_stencil.honesty_payload

FUNCTION

payload_max_abs_int

omnibias.core.proof.obligations.rational_stencil.payload_max_abs_intSource ↗

payload_max_abs_int(payload: Mapping[str, Any]) -> int

Largest absolute integer appearing in a sealed stencil / poisedness payload.

Parameters

Name	Type & default	Contract
payloadpositional-or-keyword	Mapping[str, Any]Required	See the operation contract and implementation below.

Returnsint

Read the implementation

def payload_max_abs_int(payload: Mapping[str, Any]) -> int:
    """Largest absolute integer appearing in a sealed stencil / poisedness payload."""
    acc = 1
    conditions = payload.get("conditions")
    if isinstance(conditions, Sequence) and not isinstance(conditions, str | bytes):
        for row in conditions:
            if not isinstance(row, Mapping):
                continue
            for key in ("lhs", "rhs"):
                pair = row.get(key)
                if (
                    isinstance(pair, Sequence)
                    and not isinstance(pair, str | bytes)
                    and len(pair) == 2
                ):
                    acc = max(acc, abs(int(pair[0])), abs(int(pair[1])))
    for key in ("leading_coeff", "leading_lhs", "det"):
        pair = payload.get(key)
        if (
            isinstance(pair, Sequence)
            and not isinstance(pair, str | bytes)
            and len(pair) == 2
        ):
            acc = max(acc, abs(int(pair[0])), abs(int(pair[1])))
    return acc

FUNCTION

poisedness_obligation

omnibias.core.proof.poisedness_obligationSource ↗

poisedness_obligation(spec: RationalSupport | RationalStencil | MultiPackSpec) -> Obligation

Polya inequalities plus a nonzero confluent Vandermonde determinant.

Parameters

Name	Type & default	Contract
specpositional-or-keyword	RationalSupport | RationalStencil | MultiPackSpecRequired	See the operation contract and implementation below.

ReturnsObligation

Explicit validation & failure cases

• When n == 0, raises ValueError('poisedness requires at least one incidence pair').

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

Executed regression · polya failure is not poised

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_polya_failure_is_not_poised() -> None:
    spec = MultiPackSpec.from_packs((PackSpec(order=2, mean=0.0),))
    obl = poisedness_obligation(spec)
    assert obl.holds is False
    assert obl.payload["type"] == PAYLOAD_POISEDNESS

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_polya_failure_is_not_poised" -q

Regression example · birkhoff poisedness det

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_birkhoff_poisedness_det() -> None:
    obl = poisedness_obligation(birkhoff_spec_stencil())
    assert obl.holds
    assert obl.payload["det"] == ["3", "2"]
    via_mp = poisedness_obligation(birkhoff_spec_multipack())
    assert via_mp.holds
    assert via_mp.payload["det"] == ["3", "2"]

python -m pytest packages/omnibias-core/tests/test_rational_stencil.py -k test_birkhoff_poisedness_det -q

Read the implementation

def poisedness_obligation(
    spec: RationalSupport | RationalStencil | MultiPackSpec,
) -> Obligation:
    """Polya inequalities plus a nonzero confluent Vandermonde determinant."""
    if isinstance(spec, MultiPackSpec):
        support = RationalSupport.from_multipack(spec)
    elif isinstance(spec, RationalStencil):
        support = RationalSupport.from_stencil(spec)
    else:
        support = spec
    n = support.n_conditions
    if n == 0:
        raise ValueError("poisedness requires at least one incidence pair")
    mat = _vandermonde(support.nodes, support.pairs(), n)
    det = _det_over_q(mat)
    polya = _polya_pairs(support)
    polya_ok = all(have >= need for have, need in polya)
    holds = polya_ok and det != 0
    payload: dict[str, Any] = {
        "type": PAYLOAD_POISEDNESS,
        "kind": PAYLOAD_POISEDNESS,
        "nodes": [_rat_pair(c) for c in support.nodes],
        "orders": [list(o) for o in support.orders],
        "polya": [{"j": j, "have": have, "need": need} for j, (have, need) in enumerate(polya)],
        "det": _rat_pair(det),
        "name": support.name,
    }
    max_abs = max(
        abs(det.numerator),
        abs(det.denominator),
        *(max(abs(h), abs(n_)) for h, n_ in polya),
        1,
    )
    return Obligation(PAYLOAD_POISEDNESS, payload, holds, max_abs)

Related APIsomnibias.core.proof.Obligation↗

Other public import paths

• omnibias.core.proof.poisedness_obligation
• omnibias.core.proof.obligations.poisedness_obligation
• omnibias.core.proof.obligations.rational_stencil.poisedness_obligation

FUNCTION

seal_poisedness_certificate

omnibias.core.proof.seal_poisedness_certificateSource ↗

seal_poisedness_certificate(spec: RationalSupport | RationalStencil | MultiPackSpec, *, run_lean: bool=True) -> StencilCertificateReport

Seal Polya + nonzero-det poisedness. Same honesty rules as the stencil seal.

Parameters

Name	Type & default	Contract
specpositional-or-keyword	RationalSupport | RationalStencil | MultiPackSpecRequired	See the operation contract and implementation below.
run_leankeyword-only	boolDefault: True	See the operation contract and implementation below.

ReturnsStencilCertificateReport

Executed regression · generate poisedness obligation shape

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_generate_poisedness_obligation_shape() -> None:
    cert = seal_poisedness_certificate(birkhoff_spec_stencil(), run_lean=False).certificate
    src = generate_obligation(cert)
    assert src is not None
    assert "allIntGe" in src
    assert "ratNez" in src
    assert "limit" not in src.lower()

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_generate_poisedness_obligation_shape" -q

Regression example · g5 tier separation

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_g5_tier_separation() -> None:
    st_report = seal_stencil_certificate(birkhoff_spec_stencil(), run_lean=True)
    po_report = seal_poisedness_certificate(birkhoff_spec_stencil(), run_lean=True)
    assert st_report.mathlib_verified is False
    assert po_report.mathlib_verified is False
    honesty = honesty_payload()
    assert honesty["mathlib_path_used"] is False
    assert honesty["collapse_limit_in_lean"] is False

python -m pytest packages/omnibias-core/tests/test_rational_stencil.py -k test_g5_tier_separation -q

Read the implementation

def seal_poisedness_certificate(
    spec: RationalSupport | RationalStencil | MultiPackSpec,
    *,
    run_lean: bool = True,
) -> StencilCertificateReport:
    """Seal Polya + nonzero-det poisedness. Same honesty rules as the stencil seal."""
    obligation = poisedness_obligation(spec)
    return _seal_report(
        obligation,
        claim="Birkhoff support is poised over the rationals",
        run_lean=run_lean,
    )

Related APIsomnibias.core.proof.poisedness_obligation↗

Other public import paths

• omnibias.core.proof.seal_poisedness_certificate
• omnibias.core.proof.obligations.seal_poisedness_certificate
• omnibias.core.proof.obligations.rational_stencil.seal_poisedness_certificate

FUNCTION

seal_stencil_certificate

omnibias.core.proof.seal_stencil_certificateSource ↗

seal_stencil_certificate(stencil: RationalStencil, *, run_lean: bool=True) -> StencilCertificateReport

Seal the v1 certificate and optionally drive the Lean kernel.

theorem_prover_verified is set only on a genuine kernel pass. mathlib_verified stays False.

Parameters

Name	Type & default	Contract
stencilpositional-or-keyword	RationalStencilRequired	See the operation contract and implementation below.
run_leankeyword-only	boolDefault: True	See the operation contract and implementation below.

ReturnsStencilCertificateReport

Executed regression · corrupted weights fail python algebra

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_corrupted_weights_fail_python_algebra() -> None:
    bad = birkhoff_spec_stencil().corrupt_first_weight()
    obl = stencil_consistency_obligation(bad)
    assert obl.holds is False
    src = generate_obligation(
        seal_stencil_certificate(bad, run_lean=False).certificate
    )
    assert src is not None
    assert "allRatEq" in src

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_corrupted_weights_fail_python_algebra" -q

Regression example · g5 tier separation

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_g5_tier_separation() -> None:
    st_report = seal_stencil_certificate(birkhoff_spec_stencil(), run_lean=True)
    po_report = seal_poisedness_certificate(birkhoff_spec_stencil(), run_lean=True)
    assert st_report.mathlib_verified is False
    assert po_report.mathlib_verified is False
    honesty = honesty_payload()
    assert honesty["mathlib_path_used"] is False
    assert honesty["collapse_limit_in_lean"] is False

python -m pytest packages/omnibias-core/tests/test_rational_stencil.py -k test_g5_tier_separation -q

Read the implementation

def seal_stencil_certificate(
    stencil: RationalStencil,
    *,
    run_lean: bool = True,
) -> StencilCertificateReport:
    """Seal the v1 certificate and optionally drive the Lean kernel.

    ``theorem_prover_verified`` is set only on a genuine kernel pass.
    ``mathlib_verified`` stays ``False``.
    """
    obligation = stencil_consistency_obligation(stencil)
    return _seal_report(
        obligation,
        claim="stencil consistency conditions are rational identities",
        run_lean=run_lean,
    )

Related APIsomnibias.core.proof.stencil_consistency_obligation↗

Other public import paths

• omnibias.core.proof.seal_stencil_certificate
• omnibias.core.proof.obligations.seal_stencil_certificate
• omnibias.core.proof.obligations.rational_stencil.seal_stencil_certificate

FUNCTION

stencil_consistency_obligation

omnibias.core.proof.stencil_consistency_obligationSource ↗

stencil_consistency_obligation(stencil: RationalStencil) -> Obligation

Finite conjunction of C_0 .. C_{N-1} plus the reported C_N.

Parameters

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

ReturnsObligation

Executed regression · birkhoff spec moments

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

Full file, imports & fixtures ↗

def test_birkhoff_spec_moments() -> None:
    st = birkhoff_spec_stencil()
    assert st.moment_sum(0) == 0
    assert st.moment_sum(1) == 1
    assert st.moment_sum(2) == 0
    assert st.computed_leading() == Fraction(5, 18)
    assert stencil_consistency_obligation(st).holds

python -m pytest "packages/omnibias-core/tests/test_rational_stencil.py::test_birkhoff_spec_moments" -q

Regression example · polya failure is not poised

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_polya_failure_is_not_poised() -> None:
    spec = MultiPackSpec.from_packs((PackSpec(order=2, mean=0.0),))
    obl = poisedness_obligation(spec)
    assert obl.holds is False
    assert obl.payload["type"] == PAYLOAD_POISEDNESS

python -m pytest packages/omnibias-core/tests/test_rational_stencil.py -k test_polya_failure_is_not_poised -q

Read the implementation

def stencil_consistency_obligation(stencil: RationalStencil) -> Obligation:
    """Finite conjunction of ``C_0 .. C_{N-1}`` plus the reported ``C_N``."""
    n = stencil.n_conditions
    q = stencil.target_order
    conditions: list[dict[str, Any]] = []
    holds = True
    rat_pairs: list[list[str]] = []
    for j in range(n):
        lhs = stencil.moment_sum(j)
        rhs = Fraction(1) if j == q else Fraction(0)
        if lhs != rhs:
            holds = False
        conditions.append({"j": j, "lhs": _rat_pair(lhs), "rhs": _rat_pair(rhs)})
        rat_pairs.extend([_rat_pair(lhs), _rat_pair(rhs)])
    lead_lhs = stencil.computed_leading()
    lead_rhs = stencil.reported_leading()
    if lead_lhs != lead_rhs:
        holds = False
    rat_pairs.extend([_rat_pair(lead_lhs), _rat_pair(lead_rhs)])
    payload: dict[str, Any] = {
        "type": PAYLOAD_STENCIL,
        "kind": PAYLOAD_STENCIL,
        "nodes": [_rat_pair(c) for c in stencil.nodes],
        "orders": [list(o) for o in stencil.orders],
        "weights": [[_rat_pair(a) for a in row] for row in stencil.weights],
        "target_order": q,
        "conditions": conditions,
        "leading_coeff": _rat_pair(lead_rhs),
        "leading_lhs": _rat_pair(lead_lhs),
        "name": stencil.name,
    }
    return Obligation(PAYLOAD_STENCIL, payload, holds, _max_abs_from_pairs(rat_pairs))

Related APIsomnibias.core.proof.Obligation↗

Other public import paths

• omnibias.core.proof.stencil_consistency_obligation
• omnibias.core.proof.obligations.stencil_consistency_obligation
• omnibias.core.proof.obligations.rational_stencil.stencil_consistency_obligation

← Package overviewRunnable learning examples →