API REFERENCE/omnibias-sos

omnibias.sos.inequality

0.1.0a2AlphaPython >=3.10AGPL / commercial

Sum-of-squares constructions, polynomial positivity checks, and rigorous validation of proposed Gram matrices.

import omnibias.sos.inequality

Module contract & mathematical conventions

Polynomial inequality adapter (theory 09-30).

Reuses Observation.poly_terms encoding. Universal positivity goes through certify_sos; a failed SDP is BLOCKED. A rational point with p < 0 is a counterexample. Soft RMSE is never an ExactCheck.

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

PolynomialInequalityBackend

omnibias.sos.PolynomialInequalityBackendSource ↗

class PolynomialInequalityBackend

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

Executed regression · polynomial three verdicts

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_polynomial_three_verdicts() -> None:
    register_inequality_backend(PolynomialInequalityBackend())
    proved = InequalitySystem(
        sort="polynomial",
        existential=False,
        data={"poly_n_vars": 1, "poly_terms": [[[0], "1"]]},
    )
    disproved = InequalitySystem(
        sort="polynomial",
        existential=False,
        data={"poly_n_vars": 1, "poly_terms": [[[0], "-1"]]},
    )
    blocked = InequalitySystem(
        sort="polynomial",
        existential=False,
        data={"poly_n_vars": 2, "poly_terms": [[[2, 0], "1"], [[0, 2], "1"]]},
    )
    assert run_inequality_pipeline(proved)[0] == "PROVED"
    assert run_inequality_pipeline(disproved)[0] == "DISPROVED"
    assert run_inequality_pipeline(blocked)[0] == "BLOCKED"

python -m pytest "packages/omnibias-sos/tests/test_inequality_adapter.py::test_polynomial_three_verdicts" -q

Fields & methods

sortfield

sort: ClassVar[InequalitySort] = 'polynomial'

Declared ClassVar[InequalitySort] field on PolynomialInequalityBackend. Default expression: 'polynomial'.

View source ↗

proposemethod

propose(self, system: InequalitySystem) -> Proposal

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

Parameters

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

Returns: Proposal

Executed regression · polynomial three verdicts

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_polynomial_three_verdicts() -> None:
    register_inequality_backend(PolynomialInequalityBackend())
    proved = InequalitySystem(
        sort="polynomial",
        existential=False,
        data={"poly_n_vars": 1, "poly_terms": [[[0], "1"]]},
    )
    disproved = InequalitySystem(
        sort="polynomial",
        existential=False,
        data={"poly_n_vars": 1, "poly_terms": [[[0], "-1"]]},
    )
    blocked = InequalitySystem(
        sort="polynomial",
        existential=False,
        data={"poly_n_vars": 2, "poly_terms": [[[2, 0], "1"], [[0, 2], "1"]]},
    )
    assert run_inequality_pipeline(proved)[0] == "PROVED"
    assert run_inequality_pipeline(disproved)[0] == "DISPROVED"
    assert run_inequality_pipeline(blocked)[0] == "BLOCKED"

python -m pytest "packages/omnibias-sos/tests/test_inequality_adapter.py::test_polynomial_three_verdicts" -q

Method implementation

    def propose(self, system: InequalitySystem) -> Proposal:
        n_vars = int(system.data.get("poly_n_vars", 1))
        origin = tuple("0" for _ in range(max(n_vars, 1)))
        return Proposal(method="origin", values=origin, payload={"sdp": True})

View source ↗

rationalizemethod

rationalize(self, system: InequalitySystem, proposal: Proposal) -> RationalWitness

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

Parameters

Name	Type & default	Contract
systempositional-or-keyword	InequalitySystemRequired	See the operation contract and implementation below.
proposalpositional-or-keyword	ProposalRequired	See the operation contract and implementation below.

Returns: RationalWitness

Executed regression · polynomial three verdicts

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_polynomial_three_verdicts() -> None:
    register_inequality_backend(PolynomialInequalityBackend())
    proved = InequalitySystem(
        sort="polynomial",
        existential=False,
        data={"poly_n_vars": 1, "poly_terms": [[[0], "1"]]},
    )
    disproved = InequalitySystem(
        sort="polynomial",
        existential=False,
        data={"poly_n_vars": 1, "poly_terms": [[[0], "-1"]]},
    )
    blocked = InequalitySystem(
        sort="polynomial",
        existential=False,
        data={"poly_n_vars": 2, "poly_terms": [[[2, 0], "1"], [[0, 2], "1"]]},
    )
    assert run_inequality_pipeline(proved)[0] == "PROVED"
    assert run_inequality_pipeline(disproved)[0] == "DISPROVED"
    assert run_inequality_pipeline(blocked)[0] == "BLOCKED"

python -m pytest "packages/omnibias-sos/tests/test_inequality_adapter.py::test_polynomial_three_verdicts" -q

Method implementation

    def rationalize(
        self, system: InequalitySystem, proposal: Proposal
    ) -> RationalWitness:
        values = tuple(str(_as_frac(item)) for item in proposal.values)
        return RationalWitness(method="nearest_q", values=values)

View source ↗

checkmethod

check(self, system: InequalitySystem, witness: RationalWitness) -> ExactCheck

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

Parameters

Name	Type & default	Contract
systempositional-or-keyword	InequalitySystemRequired	See the operation contract and implementation below.
witnesspositional-or-keyword	RationalWitnessRequired	See the operation contract and implementation below.

Returns: ExactCheck

Executed regression · polynomial three verdicts

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_polynomial_three_verdicts() -> None:
    register_inequality_backend(PolynomialInequalityBackend())
    proved = InequalitySystem(
        sort="polynomial",
        existential=False,
        data={"poly_n_vars": 1, "poly_terms": [[[0], "1"]]},
    )
    disproved = InequalitySystem(
        sort="polynomial",
        existential=False,
        data={"poly_n_vars": 1, "poly_terms": [[[0], "-1"]]},
    )
    blocked = InequalitySystem(
        sort="polynomial",
        existential=False,
        data={"poly_n_vars": 2, "poly_terms": [[[2, 0], "1"], [[0, 2], "1"]]},
    )
    assert run_inequality_pipeline(proved)[0] == "PROVED"
    assert run_inequality_pipeline(disproved)[0] == "DISPROVED"
    assert run_inequality_pipeline(blocked)[0] == "BLOCKED"

python -m pytest "packages/omnibias-sos/tests/test_inequality_adapter.py::test_polynomial_three_verdicts" -q

Method implementation

    def check(
        self, system: InequalitySystem, witness: RationalWitness
    ) -> ExactCheck:
        n_vars = int(system.data.get("poly_n_vars", 1))
        terms = _parse_terms(system.data.get("poly_terms", ()))
        point = tuple(_as_frac(item) for item in witness.values) or (Fraction(0),) * n_vars
        if len(point) < n_vars:
            point = point + (Fraction(0),) * (n_vars - len(point))
        value = _eval_q(terms, point[:n_vars])
        honesty = dict(honesty_labels(SOSScope(kind=GLOBAL_POLYNOMIAL)))
        honesty["complete_solver"] = False
        if not system.existential and value < 0:
            return ExactCheck(
                ok=True,
                payload={
                    "role": "counterexample",
                    "method": "eval_q",
                    "honesty": honesty,
                    "detail": f"p<0 at {tuple(str(v) for v in point)}",
                    "value": str(value),
                },
            )
        if system.existential:
            constraints = system.data.get("poly_constraints", ())
            ok = True
            if isinstance(constraints, Sequence) and constraints:
                for raw in constraints:
                    c_terms = _parse_terms(raw)
                    if _eval_q(c_terms, point[:n_vars]) < 0:
                        ok = False
                        break
            return ExactCheck(
                ok=ok,
                payload={
                    "role": "witness" if ok else "inconclusive",
                    "method": "eval_q",
                    "honesty": honesty,
                    "detail": "feasible_point" if ok else "point_violates_g",
                },
            )
        poly = _to_polynomial(n_vars, terms)
        cert = certify_sos(poly)
        if cert.certified:
            return ExactCheck(
                ok=True,
                payload={
                    "role": "positivity",
                    "method": "certify_sos",
                    "honesty": honesty,
                    "detail": "sos_certified",
                },
            )
        return ExactCheck(
            ok=False,
            payload={
                "role": "inconclusive",
                "method": "certify_sos",
                "honesty": honesty,
                "detail": str(cert.detail or "sos_inconclusive"),
            },
        )

View source ↗

Read the implementation

class PolynomialInequalityBackend:
    sort: ClassVar[InequalitySort] = "polynomial"

    def propose(self, system: InequalitySystem) -> Proposal:
        n_vars = int(system.data.get("poly_n_vars", 1))
        origin = tuple("0" for _ in range(max(n_vars, 1)))
        return Proposal(method="origin", values=origin, payload={"sdp": True})

    def rationalize(
        self, system: InequalitySystem, proposal: Proposal
    ) -> RationalWitness:
        values = tuple(str(_as_frac(item)) for item in proposal.values)
        return RationalWitness(method="nearest_q", values=values)

    def check(
        self, system: InequalitySystem, witness: RationalWitness
    ) -> ExactCheck:
        n_vars = int(system.data.get("poly_n_vars", 1))
        terms = _parse_terms(system.data.get("poly_terms", ()))
        point = tuple(_as_frac(item) for item in witness.values) or (Fraction(0),) * n_vars
        if len(point) < n_vars:
            point = point + (Fraction(0),) * (n_vars - len(point))
        value = _eval_q(terms, point[:n_vars])
        honesty = dict(honesty_labels(SOSScope(kind=GLOBAL_POLYNOMIAL)))
        honesty["complete_solver"] = False
        if not system.existential and value < 0:
            return ExactCheck(
                ok=True,
                payload={
                    "role": "counterexample",
                    "method": "eval_q",
                    "honesty": honesty,
                    "detail": f"p<0 at {tuple(str(v) for v in point)}",
                    "value": str(value),
                },
            )
        if system.existential:
            constraints = system.data.get("poly_constraints", ())
            ok = True
            if isinstance(constraints, Sequence) and constraints:
                for raw in constraints:
                    c_terms = _parse_terms(raw)
                    if _eval_q(c_terms, point[:n_vars]) < 0:
                        ok = False
                        break
            return ExactCheck(
                ok=ok,
                payload={
                    "role": "witness" if ok else "inconclusive",
                    "method": "eval_q",
                    "honesty": honesty,
                    "detail": "feasible_point" if ok else "point_violates_g",
                },
            )
        poly = _to_polynomial(n_vars, terms)
        cert = certify_sos(poly)
        if cert.certified:
            return ExactCheck(
                ok=True,
                payload={
                    "role": "positivity",
                    "method": "certify_sos",
                    "honesty": honesty,
                    "detail": "sos_certified",
                },
            )
        return ExactCheck(
            ok=False,
            payload={
                "role": "inconclusive",
                "method": "certify_sos",
                "honesty": honesty,
                "detail": str(cert.detail or "sos_inconclusive"),
            },
        )

Related APIsomnibias.core.proof.ExactCheck↗omnibias.core.proof.Proposal↗omnibias.core.proof.RationalWitness↗omnibias.sos.certify_sos↗omnibias.sos.SOSScope↗omnibias.sos.honesty_labels↗

Other public import paths

• omnibias.sos.PolynomialInequalityBackend
• omnibias.sos.inequality.PolynomialInequalityBackend

← Package overviewRunnable learning examples →