API REFERENCE/omnibias-core

omnibias.core.proof.realization_algebra_replay

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

Module contract & mathematical conventions

Generic finite replay of algebraic witnesses, Laurent paths and box trees.

Sturm chain arithmetic is checked, while Sturm's theorem connecting variation counts to real roots is an explicit mathematical dependency. Likewise the finite box computation does not formalize the general real interval theorem.

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 →

FUNCTION

algebraic_realization_replay_certificate

omnibias.core.proof.realization_algebra_replay.algebraic_realization_replay_certificateSource ↗

algebraic_realization_replay_certificate(source: PolynomialRealizationMap, witness: AlgebraicRealizationWitness) -> Cert

Substitute algebraic parameters and verify divisibility by their primitive.

A reducible primitive for which equality holds only at its selected root is unsupported by this finite divisibility family; refine the primitive first.

Parameters

Name	Type & default	Contract
sourcepositional-or-keyword	PolynomialRealizationMapRequired	See the operation contract and implementation below.
witnesspositional-or-keyword	AlgebraicRealizationWitnessRequired	See the operation contract and implementation below.

ReturnsCert

Explicit validation & failure cases

• When not witness.verify(source), raises ValueError('invalid algebraic realization witness').
• When remainder, raises NotImplementedError('refine reducible primitive: selected-root equality is not polynomial divisibility').

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

Executed regression · resealed arithmetic tampering is not hidden by source seal

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_resealed_arithmetic_tampering_is_not_hidden_by_source_seal(index):
    false = deepcopy(_examples()[index])
    p, s = false["payload"], false["payload"]["source"]
    if index <= 1:
        s["chain"][1][0] = [999, 1]
    elif index == 2:
        p["quotients"][0] = [[999, 1]]
    elif index == 3:
        s["parameters"][0] = [[-1, [1, 1]]]
    else:
        p["tree"]["midpoint"] = [2, 1]
    p["source_digest"] = source_digest(s)
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is not None

python -m pytest "packages/omnibias-core/tests/proof/test_realization_algebra_replay.py::test_resealed_arithmetic_tampering_is_not_hidden_by_source_seal[0]" -q

Read the implementation

def algebraic_realization_replay_certificate(
    source: PolynomialRealizationMap, witness: AlgebraicRealizationWitness
) -> Cert:
    """Substitute algebraic parameters and verify divisibility by their primitive.

    A reducible primitive for which equality holds only at its selected root is
    unsupported by this finite divisibility family; refine the primitive first.
    """
    if not witness.verify(source):
        raise ValueError("invalid algebraic realization witness")
    primitive = trim(witness.field.polynomial)
    parameters = tuple(p.coefficients for p in witness.parameters)
    quotients = []
    for p, target in zip(source.polynomials, witness.target, strict=True):
        quotient, remainder = divide(add(_compose(p, parameters), (-target,)), primitive)
        if remainder:
            raise NotImplementedError(
                "refine reducible primitive: selected-root equality is not polynomial divisibility"
            )
        quotients.append(quotient)
    return _seal(
        "algebraic_substitution",
        {
            "fingerprint": source.fingerprint,
            "root": _sturm(witness.field),
            "polynomials": [p.to_payload() for p in source.polynomials],
            "parameters": [[_q(x) for x in p] for p in parameters],
            "target": [_q(x) for x in witness.target],
        },
        quotients=[[_q(x) for x in p] for p in quotients],
    )

FUNCTION

laurent_closure_replay_certificate

omnibias.core.proof.realization_algebra_replay.laurent_closure_replay_certificateSource ↗

laurent_closure_replay_certificate(source: PolynomialRealizationMap, witness: LaurentClosureWitness, *, radius: Rational | None=None) -> Cert

Replay cancellation of every pole, target coefficients and tail budgets.

Parameters

Name	Type & default	Contract
sourcepositional-or-keyword	PolynomialRealizationMapRequired	See the operation contract and implementation below.
witnesspositional-or-keyword	LaurentClosureWitnessRequired	See the operation contract and implementation below.
radiuskeyword-only	Rational | NoneDefault: None	See the operation contract and implementation below.

ReturnsCert

Explicit validation & failure cases

• When not witness.verify(source), raises ValueError('invalid Laurent closure witness').

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

Executed regression · resealed arithmetic tampering is not hidden by source seal

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_resealed_arithmetic_tampering_is_not_hidden_by_source_seal(index):
    false = deepcopy(_examples()[index])
    p, s = false["payload"], false["payload"]["source"]
    if index <= 1:
        s["chain"][1][0] = [999, 1]
    elif index == 2:
        p["quotients"][0] = [[999, 1]]
    elif index == 3:
        s["parameters"][0] = [[-1, [1, 1]]]
    else:
        p["tree"]["midpoint"] = [2, 1]
    p["source_digest"] = source_digest(s)
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is not None

python -m pytest "packages/omnibias-core/tests/proof/test_realization_algebra_replay.py::test_resealed_arithmetic_tampering_is_not_hidden_by_source_seal[0]" -q

Read the implementation

def laurent_closure_replay_certificate(
    source: PolynomialRealizationMap,
    witness: LaurentClosureWitness,
    *,
    radius: Rational | None = None,
) -> Cert:
    """Replay cancellation of every pole, target coefficients and tail budgets."""
    if not witness.verify(source):
        raise ValueError("invalid Laurent closure witness")
    rho = witness.radius if radius is None else rational(radius)
    errors = witness.coefficient_error_bounds(source, rho)
    return _seal(
        "laurent_cancellation",
        {
            "fingerprint": source.fingerprint,
            "polynomials": [p.to_payload() for p in source.polynomials],
            "parameters": [[[k, _q(c)] for k, c in p.terms] for p in witness.parameters],
            "target": [_q(x) for x in witness.target],
            "radius": _q(rho),
        },
        errors=[_q(x) for x in errors],
    )

Related APIsomnibias.core.realization.polynomial.rational↗

FUNCTION

moment_identity_replay_certificate

omnibias.core.proof.realization_algebra_replay.moment_identity_replay_certificateSource ↗

moment_identity_replay_certificate(offsets: Sequence[Rational], coefficients: Sequence[Rational], *, center: Rational, expected_moments: Sequence[Rational]) -> Cert

Replay normalized collision moments from every original rational operand.

Parameters

Name	Type & default	Contract
offsetspositional-or-keyword	Sequence[Rational]Required	See the operation contract and implementation below.
coefficientspositional-or-keyword	Sequence[Rational]Required	See the operation contract and implementation below.
centerkeyword-only	RationalRequired	See the operation contract and implementation below.
expected_momentskeyword-only	Sequence[Rational]Required	See the operation contract and implementation below.

ReturnsCert

Explicit validation & failure cases

• When not n or len(coefficients) != n or (not expected_moments), raises ValueError('nonempty matching offsets/coefficients and moments required').

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

Executed regression · moment identity embeds original offsets weights and center

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_moment_identity_embeds_original_offsets_weights_and_center():
    certificate = moment_identity_replay_certificate(
        (1, -1), (2, 3), center=0, expected_moments=(5, -1, Q(5, 2), -Q(1, 6), Q(5, 24))
    )
    assert verify_replay_certificate(certificate)
    assert len(certificate["payload"]["point"]) == 5
    false = deepcopy(certificate)
    false["payload"]["point"][0] = [3, 1]
    assert not verify_replay_certificate(seal_certificate(false))
    with pytest.raises(ValueError):
        moment_identity_replay_certificate((1, -1), (2, 3), center=0, expected_moments=(5, 0))

python -m pytest "packages/omnibias-core/tests/proof/test_realization_algebra_replay.py::test_moment_identity_embeds_original_offsets_weights_and_center" -q

Regression example · actual kernel algebra build when toolchain available

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_actual_kernel_algebra_build_when_toolchain_available(certificate):
    from omnibias.core.proof.lean_check import check_certificate, lean_check_available

    if not lean_check_available():
        pytest.skip("Lean toolchain unavailable")
    assert check_certificate(certificate).verified

python -m pytest packages/omnibias-core/tests/proof/test_realization_algebra_replay.py -k test_actual_kernel_algebra_build_when_toolchain_available -q

Read the implementation

def moment_identity_replay_certificate(
    offsets: Sequence[Rational],
    coefficients: Sequence[Rational],
    *,
    center: Rational,
    expected_moments: Sequence[Rational],
) -> Cert:
    """Replay normalized collision moments from every original rational operand."""
    from math import factorial

    from omnibias.core.proof.realization_replay import polynomial_evaluation_certificate

    n = len(offsets)
    if not n or len(coefficients) != n or not expected_moments:
        raise ValueError("nonempty matching offsets/coefficients and moments required")
    point = tuple(map(rational, coefficients)) + tuple(map(rational, offsets)) + (rational(center),)
    variables = tuple(SparsePolynomial.variable(2 * n + 1, i) for i in range(2 * n + 1))
    polys = []
    for order in range(len(expected_moments)):
        value = SparsePolynomial.constant(2 * n + 1, 0)
        for i in range(n):
            value = value + variables[i] * (variables[n + i] - variables[-1]) ** order * Fraction(
                1, factorial(order)
            )
        polys.append(value)
    return polynomial_evaluation_certificate(polys, point, expected_moments)

Related APIsomnibias.core.realization.polynomial.rational↗

FUNCTION

polynomial_box_replay_certificate

omnibias.core.proof.realization_algebra_replay.polynomial_box_replay_certificateSource ↗

polynomial_box_replay_certificate(polynomials: Sequence[SparsePolynomial], box: Sequence[Sequence[Rational]], tree: Mapping[str, Any]) -> Cert

Replay a finite binary cover and an excluded polynomial at every leaf.

Tree format is {equation, enclosure} or {axis, midpoint, left, right}; all numeric leaves use rational [numerator, denominator] pairs.

Parameters

Name	Type & default	Contract
polynomialspositional-or-keyword	Sequence[SparsePolynomial]Required	See the operation contract and implementation below.
boxpositional-or-keyword	Sequence[Sequence[Rational]]Required	See the operation contract and implementation below.
treepositional-or-keyword	Mapping[str, Any]Required	See the operation contract and implementation below.

ReturnsCert

Explicit validation & failure cases

• When not polynomials or any((p.nvars != len(bounds) for p in polynomials)), raises ValueError('polynomial box dimensions differ').
• When not verify_algebra_replay(certificate), raises ValueError('invalid polynomial exclusion tree').

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

Executed regression · resealed arithmetic tampering is not hidden by source seal

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_resealed_arithmetic_tampering_is_not_hidden_by_source_seal(index):
    false = deepcopy(_examples()[index])
    p, s = false["payload"], false["payload"]["source"]
    if index <= 1:
        s["chain"][1][0] = [999, 1]
    elif index == 2:
        p["quotients"][0] = [[999, 1]]
    elif index == 3:
        s["parameters"][0] = [[-1, [1, 1]]]
    else:
        p["tree"]["midpoint"] = [2, 1]
    p["source_digest"] = source_digest(s)
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is not None

python -m pytest "packages/omnibias-core/tests/proof/test_realization_algebra_replay.py::test_resealed_arithmetic_tampering_is_not_hidden_by_source_seal[0]" -q

Read the implementation

def polynomial_box_replay_certificate(
    polynomials: Sequence[SparsePolynomial],
    box: Sequence[Sequence[Rational]],
    tree: Mapping[str, Any],
) -> Cert:
    """Replay a finite binary cover and an excluded polynomial at every leaf.

    Tree format is ``{equation, enclosure}`` or ``{axis, midpoint, left, right}``;
    all numeric leaves use rational ``[numerator, denominator]`` pairs.
    """
    bounds = tuple(_interval(x) for x in box)
    if not polynomials or any(p.nvars != len(bounds) for p in polynomials):
        raise ValueError("polynomial box dimensions differ")
    certificate = _seal(
        "polynomial_box",
        {
            "polynomials": [p.to_payload() for p in polynomials],
            "box": [_iv_payload(x) for x in bounds],
        },
        tree=dict(tree),
    )
    if not verify_algebra_replay(certificate):
        raise ValueError("invalid polynomial exclusion tree")
    return certificate

FUNCTION

sturm_isolation_replay_certificate

omnibias.core.proof.realization_algebra_replay.sturm_isolation_replay_certificateSource ↗

sturm_isolation_replay_certificate(field: RealAlgebraicField) -> Cert

Replay derivative, Euclidean Sturm chain, endpoints and variation counts.

Parameters

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

ReturnsCert

Executed regression · resealed arithmetic tampering is not hidden by source seal

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_resealed_arithmetic_tampering_is_not_hidden_by_source_seal(index):
    false = deepcopy(_examples()[index])
    p, s = false["payload"], false["payload"]["source"]
    if index <= 1:
        s["chain"][1][0] = [999, 1]
    elif index == 2:
        p["quotients"][0] = [[999, 1]]
    elif index == 3:
        s["parameters"][0] = [[-1, [1, 1]]]
    else:
        p["tree"]["midpoint"] = [2, 1]
    p["source_digest"] = source_digest(s)
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is not None

python -m pytest "packages/omnibias-core/tests/proof/test_realization_algebra_replay.py::test_resealed_arithmetic_tampering_is_not_hidden_by_source_seal[0]" -q

Read the implementation

def sturm_isolation_replay_certificate(field: RealAlgebraicField) -> Cert:
    """Replay derivative, Euclidean Sturm chain, endpoints and variation counts."""
    return _seal("sturm_arithmetic", _sturm(field))

← Package overviewRunnable learning examples →