omnibias.core.proof.inequality

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

Module contract & mathematical conventions

Unified inequality engine (theory 09-30).

A front door, not a new solver and not a complexity-class claim. Owning packages register backends at import; this module never imports them. The optimizer proposes; an exact Q / GF(2) / enclosure / tiny enum proves. A float residual 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 →

CONSTANT

CheckRole

omnibias.core.proof.inequality.CheckRoleSource ↗

CheckRole = Literal['witness', 'empty', 'positivity', 'counterexample', 'inconclusive']

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.

Read the implementation

CheckRole = Literal[
    "witness",
    "empty",
    "positivity",
    "counterexample",
    "inconclusive",
]

CONSTANT

INEQUALITY_KIND

omnibias.core.proof.INEQUALITY_KINDSource ↗

INEQUALITY_KIND = 'inequality_system'

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 · missing backend is blocked

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_missing_backend_is_blocked() -> None:
    _reset_inequality_backends_for_tests()
    system = InequalitySystem(sort="linear", existential=True, data={})
    status, payload, honesty = run_inequality_pipeline(system)
    assert status == "BLOCKED"
    assert payload["detail"] == "backend_unavailable"
    attempt = prove_inequality(
        Conjecture("missing", INEQUALITY_KIND, system.as_dict())
    )
    assert attempt.status == "BLOCKED"

python -m pytest packages/omnibias-core/tests/test_inequality_protocol.py -k test_missing_backend_is_blocked -q

Read the implementation

INEQUALITY_KIND = "inequality_system"

Other public import paths

omnibias.core.proof.INEQUALITY_KIND
omnibias.core.proof.inequality.INEQUALITY_KIND

CLASS

InequalityBackend

omnibias.core.proof.InequalityBackendSource ↗

class InequalityBackend(Protocol)

Owning-package adapter. check must be exact / enclosure / tiny enum.

Fields & methods

sortproperty

sort(self) -> InequalitySort

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

Returns: InequalitySort

Method implementation

    def sort(self) -> InequalitySort: ...

View source ↗

proposemethod

propose(self, system: InequalitySystem) -> Proposal

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

Parameters

Name	Type & default	Contract
`system`positional-or-keyword	`InequalitySystem`Required	See the operation contract and implementation below.

Returns: Proposal

Method implementation

    def propose(self, system: InequalitySystem) -> Proposal: ...

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
`system`positional-or-keyword	`InequalitySystem`Required	See the operation contract and implementation below.
`proposal`positional-or-keyword	`Proposal`Required	See the operation contract and implementation below.

Returns: RationalWitness

Method implementation

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

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
`system`positional-or-keyword	`InequalitySystem`Required	See the operation contract and implementation below.
`witness`positional-or-keyword	`RationalWitness`Required	See the operation contract and implementation below.

Returns: ExactCheck

Method implementation

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

View source ↗

Read the implementation

class InequalityBackend(Protocol):
    """Owning-package adapter. ``check`` must be exact / enclosure / tiny enum."""

    @property
    def sort(self) -> InequalitySort: ...

    def propose(self, system: InequalitySystem) -> Proposal: ...

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

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

Other public import paths

omnibias.core.proof.InequalityBackend
omnibias.core.proof.inequality.InequalityBackend

CONSTANT

InequalitySort

omnibias.core.proof.InequalitySortSource ↗

InequalitySort = Literal['linear', 'polynomial', 'boolean', 'csp']

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.

Read the implementation

InequalitySort = Literal["linear", "polynomial", "boolean", "csp"]

Other public import paths

omnibias.core.proof.InequalitySort
omnibias.core.proof.inequality.InequalitySort

CLASS

InequalitySystem

omnibias.core.proof.InequalitySystemSource ↗

class InequalitySystem

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.

JSON-able inequality payload. data is sort-specific.

Parameters

Name	Type & default	Contract
`sort`dataclass field	`InequalitySort`Required	See the operation contract and implementation below.
`existential`dataclass field	`bool`Required	See the operation contract and implementation below.
`data`dataclass field	`Mapping[str, Any]`Required	See the operation contract and implementation below.
`name`dataclass field	`str`Default: ''	See the operation contract and implementation below.

Executed regression · unknown sort raises

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_unknown_sort_raises() -> None:
    with pytest.raises(ValueError, match="unknown inequality sort"):
        InequalitySystem.from_mapping({"sort": "cad", "data": {}})

python -m pytest "packages/omnibias-core/tests/test_inequality_protocol.py::test_unknown_sort_raises" -q

Regression example · missing backend is blocked

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_missing_backend_is_blocked() -> None:
    _reset_inequality_backends_for_tests()
    system = InequalitySystem(sort="linear", existential=True, data={})
    status, payload, honesty = run_inequality_pipeline(system)
    assert status == "BLOCKED"
    assert payload["detail"] == "backend_unavailable"
    attempt = prove_inequality(
        Conjecture("missing", INEQUALITY_KIND, system.as_dict())
    )
    assert attempt.status == "BLOCKED"

python -m pytest packages/omnibias-core/tests/test_inequality_protocol.py -k test_missing_backend_is_blocked -q

Fields & methods

sortfield

sort: InequalitySort

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

View source ↗

existentialfield

existential: bool

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

View source ↗

datafield

data: Mapping[str, Any]

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

View source ↗

namefield

name: str = ''

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

View source ↗

as_dictmethod

as_dict(self) -> dict[str, Any]

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

Returns: dict[str, Any]

Executed regression · missing backend is blocked

Full file, imports & fixtures ↗

def test_missing_backend_is_blocked() -> None:
    _reset_inequality_backends_for_tests()
    system = InequalitySystem(sort="linear", existential=True, data={})
    status, payload, honesty = run_inequality_pipeline(system)
    assert status == "BLOCKED"
    assert payload["detail"] == "backend_unavailable"
    attempt = prove_inequality(
        Conjecture("missing", INEQUALITY_KIND, system.as_dict())
    )
    assert attempt.status == "BLOCKED"

python -m pytest "packages/omnibias-core/tests/test_inequality_protocol.py::test_missing_backend_is_blocked" -q

Method implementation

    def as_dict(self) -> dict[str, Any]:
        return {
            "sort": self.sort,
            "existential": self.existential,
            "data": dict(self.data),
            "name": self.name,
        }

View source ↗

from_mappingmethod

from_mapping(cls, raw: Mapping[str, Any]) -> InequalitySystem

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

Parameters

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

Returns: InequalitySystem

Validation & failure cases

When sort not in _SORTS, raises ValueError(f'unknown inequality sort {sort!r}').
When not isinstance(data_raw, Mapping), raises ValueError('inequality data must be a mapping').

Executed regression · unknown sort raises

Full file, imports & fixtures ↗

def test_unknown_sort_raises() -> None:
    with pytest.raises(ValueError, match="unknown inequality sort"):
        InequalitySystem.from_mapping({"sort": "cad", "data": {}})

python -m pytest "packages/omnibias-core/tests/test_inequality_protocol.py::test_unknown_sort_raises" -q

Method implementation

    def from_mapping(cls, raw: Mapping[str, Any]) -> InequalitySystem:
        sort = str(raw.get("sort", ""))
        if sort not in _SORTS:
            raise ValueError(f"unknown inequality sort {sort!r}")
        data_raw = raw.get("data", {})
        if not isinstance(data_raw, Mapping):
            raise ValueError("inequality data must be a mapping")
        return cls(
            sort=cast(InequalitySort, sort),
            existential=bool(raw.get("existential", True)),
            data=dict(data_raw),
            name=str(raw.get("name", "")),
        )

View source ↗

Read the implementation

class InequalitySystem:
    """JSON-able inequality payload. ``data`` is sort-specific."""

    sort: InequalitySort
    existential: bool
    data: Mapping[str, Any]
    name: str = ""

    def as_dict(self) -> dict[str, Any]:
        return {
            "sort": self.sort,
            "existential": self.existential,
            "data": dict(self.data),
            "name": self.name,
        }

    @classmethod
    def from_mapping(cls, raw: Mapping[str, Any]) -> InequalitySystem:
        sort = str(raw.get("sort", ""))
        if sort not in _SORTS:
            raise ValueError(f"unknown inequality sort {sort!r}")
        data_raw = raw.get("data", {})
        if not isinstance(data_raw, Mapping):
            raise ValueError("inequality data must be a mapping")
        return cls(
            sort=cast(InequalitySort, sort),
            existential=bool(raw.get("existential", True)),
            data=dict(data_raw),
            name=str(raw.get("name", "")),
        )

Other public import paths

omnibias.core.proof.InequalitySystem
omnibias.core.proof.inequality.InequalitySystem

CLASS

Proposal

omnibias.core.proof.ProposalSource ↗

class Proposal

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.

Float / soft proposal. skipped is allowed (Boolean exact path).

Parameters

Name	Type & default	Contract
`method`dataclass field	`str`Required	See the operation contract and implementation below.
`values`dataclass field	`tuple[str, ...]`Default: ()	See the operation contract and implementation below.
`payload`dataclass field	`Mapping[str, Any]`Default: field(default_factory=dict)	See the operation contract and implementation below.
`skipped`dataclass field	`bool`Default: False	See the operation contract and implementation below.

Regression example · soft residual cannot become exact check

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_soft_residual_cannot_become_exact_check() -> None:
    _reset_inequality_backends_for_tests()

    class _Soft:
        sort = "boolean"

        def propose(self, system: InequalitySystem) -> Proposal:
            return Proposal(method="soft", skipped=True)

        def rationalize(
            self, system: InequalitySystem, proposal: Proposal
        ) -> RationalWitness:
            return RationalWitness(method="none")

        def check(
            self, system: InequalitySystem, witness: RationalWitness
        ) -> ExactCheck:
            return ExactCheck(
                ok=True,
                payload={
                    "role": "witness",
                    "soft_residual_is_exact_check": True,
                },
            )

    register_inequality_backend(_Soft())
    with pytest.raises(ValueError, match="soft residual"):
        run_inequality_pipeline(
            InequalitySystem(sort="boolean", existential=True, data={})
        )
    _reset_inequality_backends_for_tests()

python -m pytest packages/omnibias-core/tests/test_inequality_protocol.py -k test_soft_residual_cannot_become_exact_check -q

Fields & methods

methodfield

method: str

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

View source ↗

valuesfield

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

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

View source ↗

payloadfield

payload: Mapping[str, Any] = field(default_factory=dict)

Declared Mapping[str, Any] field on Proposal. Default expression: field(default_factory=dict).

View source ↗

skippedfield

skipped: bool = False

Declared bool field on Proposal. Default expression: False.

View source ↗

Read the implementation

class Proposal:
    """Float / soft proposal. ``skipped`` is allowed (Boolean exact path)."""

    method: str
    values: tuple[str, ...] = ()
    payload: Mapping[str, Any] = field(default_factory=dict)
    skipped: bool = False

Other public import paths

omnibias.core.proof.Proposal
omnibias.core.proof.inequality.Proposal

CLASS

RationalWitness

omnibias.core.proof.RationalWitnessSource ↗

class RationalWitness

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.

Rationalized proposal. Values are fraction strings or discrete indices.

Parameters

Name	Type & default	Contract
`method`dataclass field	`str`Required	See the operation contract and implementation below.
`values`dataclass field	`tuple[str, ...]`Default: ()	See the operation contract and implementation below.
`payload`dataclass field	`Mapping[str, Any]`Default: field(default_factory=dict)	See the operation contract and implementation below.

Regression example · soft residual cannot become exact check

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_soft_residual_cannot_become_exact_check() -> None:
    _reset_inequality_backends_for_tests()

    class _Soft:
        sort = "boolean"

        def propose(self, system: InequalitySystem) -> Proposal:
            return Proposal(method="soft", skipped=True)

        def rationalize(
            self, system: InequalitySystem, proposal: Proposal
        ) -> RationalWitness:
            return RationalWitness(method="none")

        def check(
            self, system: InequalitySystem, witness: RationalWitness
        ) -> ExactCheck:
            return ExactCheck(
                ok=True,
                payload={
                    "role": "witness",
                    "soft_residual_is_exact_check": True,
                },
            )

    register_inequality_backend(_Soft())
    with pytest.raises(ValueError, match="soft residual"):
        run_inequality_pipeline(
            InequalitySystem(sort="boolean", existential=True, data={})
        )
    _reset_inequality_backends_for_tests()

python -m pytest packages/omnibias-core/tests/test_inequality_protocol.py -k test_soft_residual_cannot_become_exact_check -q

Fields & methods

methodfield

method: str

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

View source ↗

valuesfield

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

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

View source ↗

payloadfield

payload: Mapping[str, Any] = field(default_factory=dict)

Declared Mapping[str, Any] field on RationalWitness. Default expression: field(default_factory=dict).

View source ↗

Read the implementation

class RationalWitness:
    """Rationalized proposal. Values are fraction strings or discrete indices."""

    method: str
    values: tuple[str, ...] = ()
    payload: Mapping[str, Any] = field(default_factory=dict)

Other public import paths

omnibias.core.proof.RationalWitness
omnibias.core.proof.inequality.RationalWitness

FUNCTION

build_inequality_machine

omnibias.core.proof.build_inequality_machineSource ↗

build_inequality_machine() -> ProofMachine

ProofMachine with the inequality kind. Loads owning backends.

ReturnsProofMachine

Read the implementation

def build_inequality_machine() -> ProofMachine:
    """ProofMachine with the inequality kind. Loads owning backends."""

    from omnibias.core.proof import ProofMachine

    load_inequality_stack()
    return ProofMachine().register(inequality_prover())

Other public import paths

omnibias.core.proof.build_inequality_machine
omnibias.core.proof.inequality.build_inequality_machine

FUNCTION

default_inequality_honesty

omnibias.core.proof.default_inequality_honestySource ↗

default_inequality_honesty() -> dict[str, bool]

Engine-level honesty. Backends may raise complete_solver on a cube.

Returnsdict[str, bool]

Executed regression · honesty defaults forbid parent claims

Full file, imports & fixtures ↗

def test_honesty_defaults_forbid_parent_claims() -> None:
    honesty = default_inequality_honesty()
    assert honesty["complete_solver"] is False
    assert honesty["new_lp_algorithm_claim"] is False
    assert honesty["unsat_from_float_infeasible"] is False
    assert honesty["soft_residual_is_exact_check"] is False

python -m pytest "packages/omnibias-core/tests/test_inequality_protocol.py::test_honesty_defaults_forbid_parent_claims" -q

Regression example · missing backend is blocked

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_missing_backend_is_blocked() -> None:
    _reset_inequality_backends_for_tests()
    system = InequalitySystem(sort="linear", existential=True, data={})
    status, payload, honesty = run_inequality_pipeline(system)
    assert status == "BLOCKED"
    assert payload["detail"] == "backend_unavailable"
    attempt = prove_inequality(
        Conjecture("missing", INEQUALITY_KIND, system.as_dict())
    )
    assert attempt.status == "BLOCKED"

python -m pytest packages/omnibias-core/tests/test_inequality_protocol.py -k test_missing_backend_is_blocked -q

Read the implementation

def default_inequality_honesty() -> dict[str, bool]:
    """Engine-level honesty. Backends may raise ``complete_solver`` on a cube."""

    return {
        "complete_solver": False,
        "unsat_proof": False,
        "new_lp_algorithm_claim": False,
        "unsat_from_float_infeasible": False,
        "soft_residual_is_exact_check": False,
        **_PARENT_FLAGS,
    }

Other public import paths

omnibias.core.proof.default_inequality_honesty
omnibias.core.proof.inequality.default_inequality_honesty

FUNCTION

inequality_backend

omnibias.core.proof.inequality_backendSource ↗

inequality_backend(sort: str) -> InequalityBackend | None

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
`sort`positional-or-keyword	`str`Required	See the operation contract and implementation below.

ReturnsInequalityBackend | None

Read the implementation

def inequality_backend(sort: str) -> InequalityBackend | None:
    return _BACKENDS.get(sort)

Other public import paths

omnibias.core.proof.inequality_backend
omnibias.core.proof.inequality.inequality_backend

FUNCTION

inequality_prover

omnibias.core.proof.inequality_proverSource ↗

inequality_prover() -> FunctionProver

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

ReturnsFunctionProver

Read the implementation

def inequality_prover() -> FunctionProver:
    from omnibias.core.proof import FunctionProver

    return FunctionProver(
        name="inequality_system",
        kinds=frozenset({INEQUALITY_KIND}),
        prove_fn=prove_inequality,
        schema_fn=inequality_schema_errors,
        replay_fn=replay_inequality,
    )

Other public import paths

omnibias.core.proof.inequality_prover
omnibias.core.proof.inequality.inequality_prover

FUNCTION

inequality_schema_errors

omnibias.core.proof.inequality.inequality_schema_errorsSource ↗

inequality_schema_errors(certificate: Certificate) -> list[str]

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
`certificate`positional-or-keyword	`Certificate`Required	See the operation contract and implementation below.

Returnslist[str]

Read the implementation

def inequality_schema_errors(certificate: Certificate) -> list[str]:
    errors = list(schema_errors_v1(certificate))
    payload = certificate.get("payload")
    if not isinstance(payload, Mapping):
        errors.append("payload missing")
        return errors
    if "role" not in payload:
        errors.append("payload.role missing")
    return errors

FUNCTION

list_inequality_backends

omnibias.core.proof.list_inequality_backendsSource ↗

list_inequality_backends() -> tuple[str, ...]

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

Returnstuple[str, ...]

Read the implementation

def list_inequality_backends() -> tuple[str, ...]:
    return tuple(sorted(_BACKENDS))

Other public import paths

omnibias.core.proof.list_inequality_backends
omnibias.core.proof.inequality.list_inequality_backends

FUNCTION

load_inequality_stack

omnibias.core.proof.load_inequality_stackSource ↗

load_inequality_stack() -> tuple[str, ...]

Import owning adapters so they register. Core stays clean.

Returnstuple[str, ...]

Read the implementation

def load_inequality_stack() -> tuple[str, ...]:
    """Import owning adapters so they register. Core stays clean."""

    import importlib

    loaded: list[str] = []
    for name in _STACK_MODULES:
        try:
            module = importlib.import_module(name)
        except ImportError:
            continue
        register = getattr(module, "_register", None)
        if callable(register):
            register()
        loaded.append(name)
    return tuple(loaded)

Other public import paths

omnibias.core.proof.load_inequality_stack
omnibias.core.proof.inequality.load_inequality_stack

FUNCTION

locked_catalog

omnibias.core.proof.locked_catalogSource ↗

locked_catalog() -> tuple[dict[str, Any], ...]

Twelve locked instances: three per sort, expected statuses published.

Returnstuple[dict[str, Any], ...]

Executed regression · locked catalog has twelve

Full file, imports & fixtures ↗

def test_locked_catalog_has_twelve() -> None:
    rows = locked_catalog()
    assert len(rows) == 12
    sorts = {str(row["sort"]) for row in rows}
    assert sorts == {"linear", "polynomial", "boolean", "csp"}
    expected = {str(row["expected"]) for row in rows}
    assert expected == {"PROVED", "DISPROVED", "BLOCKED"}

python -m pytest "packages/omnibias-core/tests/test_inequality_protocol.py::test_locked_catalog_has_twelve" -q

Read the implementation

def locked_catalog() -> tuple[dict[str, Any], ...]:
    """Twelve locked instances: three per sort, expected statuses published."""

    high_a = []
    high_b = []
    for i in range(5):
        row_pos = ["0"] * 5
        row_neg = ["0"] * 5
        row_pos[i] = "1"
        row_neg[i] = "-1"
        high_a.append(row_pos)
        high_a.append(row_neg)
        high_b.extend(["-1", "-1"])
    return (
        {
            "name": "linear_box_sat",
            "sort": "linear",
            "existential": True,
            "expected": "PROVED",
            "data": {"A": [["1"], ["-1"]], "b": ["1", "0"]},
        },
        {
            "name": "linear_empty_enum",
            "sort": "linear",
            "existential": True,
            "expected": "DISPROVED",
            "data": {"A": [["1"], ["-1"]], "b": ["-1", "-1"]},
        },
        {
            "name": "linear_highdim_blocked",
            "sort": "linear",
            "existential": True,
            "expected": "BLOCKED",
            "data": {"A": high_a, "b": high_b},
        },
        {
            "name": "poly_constant_one",
            "sort": "polynomial",
            "existential": False,
            "expected": "PROVED",
            "data": {
                "poly_n_vars": 1,
                "poly_terms": [[[0], "1"]],
            },
        },
        {
            "name": "poly_constant_neg",
            "sort": "polynomial",
            "existential": False,
            "expected": "DISPROVED",
            "data": {
                "poly_n_vars": 1,
                "poly_terms": [[[0], "-1"]],
            },
        },
        {
            "name": "poly_x2_y2_blocked",
            "sort": "polynomial",
            "existential": False,
            "expected": "BLOCKED",
            "data": {
                "poly_n_vars": 2,
                "poly_terms": [[[2, 0], "1"], [[0, 2], "1"]],
            },
        },
        {
            "name": "boolean_and_sat",
            "sort": "boolean",
            "existential": True,
            "expected": "PROVED",
            "data": {"tables": [[0, 0, 0, 1]]},
        },
        {
            "name": "boolean_x_not_x_unsat",
            "sort": "boolean",
            "existential": True,
            "expected": "DISPROVED",
            "data": {"tables": [[1, 1]]},
        },
        {
            "name": "boolean_budget_zero",
            "sort": "boolean",
            "existential": True,
            "expected": "BLOCKED",
            "data": {"tables": [[0, 0, 0, 1]], "budget": 0},
        },
        {
            "name": "csp_two_var_sat",
            "sort": "csp",
            "existential": True,
            "expected": "PROVED",
            "data": {
                "variables": [
                    {"name": "x0", "domain": ["a", "b"]},
                    {"name": "x1", "domain": ["a", "b"]},
                ],
                "relations": [{"scope": [0, 1], "allowed": [[0, 0], [1, 1]]}],
                "oracle": False,
            },
        },
        {
            "name": "csp_empty_unsat",
            "sort": "csp",
            "existential": True,
            "expected": "DISPROVED",
            "data": {
                "variables": [
                    {"name": "x0", "domain": ["a", "b"]},
                    {"name": "x1", "domain": ["a", "b"]},
                ],
                "relations": [{"scope": [0, 1], "allowed": []}],
                "oracle": True,
            },
        },
        {
            "name": "csp_anneal_blocked",
            "sort": "csp",
            "existential": True,
            "expected": "BLOCKED",
            "data": {
                "variables": [
                    {"name": "x0", "domain": ["a", "b"]},
                    {"name": "x1", "domain": ["a", "b"]},
                ],
                "relations": [{"scope": [0, 1], "allowed": []}],
                "oracle": False,
            },
        },
    )

Other public import paths

omnibias.core.proof.locked_catalog
omnibias.core.proof.inequality.locked_catalog

FUNCTION

prove_inequality

omnibias.core.proof.prove_inequalitySource ↗

prove_inequality(conjecture: Conjecture) -> ProofAttempt

Dispatch inequality_system conjectures.

Parameters

Name	Type & default	Contract
`conjecture`positional-or-keyword	`Conjecture`Required	See the operation contract and implementation below.

ReturnsProofAttempt

Executed regression · missing backend is blocked

Full file, imports & fixtures ↗

def test_missing_backend_is_blocked() -> None:
    _reset_inequality_backends_for_tests()
    system = InequalitySystem(sort="linear", existential=True, data={})
    status, payload, honesty = run_inequality_pipeline(system)
    assert status == "BLOCKED"
    assert payload["detail"] == "backend_unavailable"
    attempt = prove_inequality(
        Conjecture("missing", INEQUALITY_KIND, system.as_dict())
    )
    assert attempt.status == "BLOCKED"

python -m pytest "packages/omnibias-core/tests/test_inequality_protocol.py::test_missing_backend_is_blocked" -q

Read the implementation

def prove_inequality(conjecture: Conjecture) -> ProofAttempt:
    """Dispatch ``inequality_system`` conjectures."""

    raw = dict(conjecture.data)
    if "sort" not in raw and "system" in raw and isinstance(raw["system"], Mapping):
        raw = dict(raw["system"])
    try:
        system = InequalitySystem.from_mapping(raw)
    except ValueError as exc:
        return _seal_attempt(
            "BLOCKED",
            {"role": "inconclusive", "detail": str(exc), "pipeline": []},
            default_inequality_honesty(),
            str(exc),
        )
    if not system.name:
        system = InequalitySystem(
            sort=system.sort,
            existential=system.existential,
            data=system.data,
            name=conjecture.name,
        )
    status, payload, honesty = run_inequality_pipeline(system)
    return _seal_attempt(status, payload, honesty, str(payload.get("detail", "")))

Other public import paths

omnibias.core.proof.prove_inequality
omnibias.core.proof.inequality.prove_inequality

FUNCTION

register_inequality_backend

omnibias.core.proof.register_inequality_backendSource ↗

register_inequality_backend(backend: InequalityBackend) -> None

Parameters

Name	Type & default	Contract
`backend`positional-or-keyword	`InequalityBackend`Required	See the operation contract and implementation below.

ReturnsNone

Explicit validation & failure cases

When type(existing) is not type(backend), raises ValueError(f'inequality backend collision for {backend.sort!r}').

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

Executed regression · boolean three verdicts

Full file, imports & fixtures ↗

def test_boolean_three_verdicts() -> None:
    register_inequality_backend(BooleanInequalityBackend())
    proved = InequalitySystem(
        sort="boolean",
        existential=True,
        data={"tables": [[0, 0, 0, 1]]},
    )
    disproved = InequalitySystem(
        sort="boolean",
        existential=True,
        data={"tables": [[1, 1]]},
    )
    blocked = InequalitySystem(
        sort="boolean",
        existential=True,
        data={"tables": [[0, 0, 0, 1]], "budget": 0},
    )
    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-boolean/tests/test_inequality_adapter.py::test_boolean_three_verdicts" -q

Regression example · polynomial three verdicts

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 -k test_polynomial_three_verdicts -q

Read the implementation

def register_inequality_backend(backend: InequalityBackend) -> None:
    """Register ``backend`` for its ``sort``. Same object is idempotent."""

    existing = _BACKENDS.get(backend.sort)
    if existing is not None and existing is not backend:
        if type(existing) is not type(backend):
            raise ValueError(f"inequality backend collision for {backend.sort!r}")
    _BACKENDS[backend.sort] = backend

Other public import paths

omnibias.core.proof.register_inequality_backend
omnibias.core.proof.inequality.register_inequality_backend

FUNCTION

replay_inequality

omnibias.core.proof.replay_inequalitySource ↗

replay_inequality(certificate: Certificate) -> bool | None

Re-run check on the sealed witness. Does not re-propose.

Parameters

Name	Type & default	Contract
`certificate`positional-or-keyword	`Certificate`Required	See the operation contract and implementation below.

Returnsbool | None

Read the implementation

def replay_inequality(certificate: Certificate) -> bool | None:
    """Re-run ``check`` on the sealed witness. Does not re-propose."""

    payload = certificate.get("payload")
    if not isinstance(payload, Mapping):
        return False
    system_raw = payload.get("system")
    if not isinstance(system_raw, Mapping):
        return False
    try:
        system = InequalitySystem.from_mapping(system_raw)
    except ValueError:
        return False
    backend = _BACKENDS.get(system.sort)
    if backend is None:
        return str(payload.get("detail", "")) == "backend_unavailable"
    witness = RationalWitness(
        method=str(payload.get("rationalize_method", "")),
        values=tuple(str(item) for item in payload.get("witness", ())),
        payload={},
    )
    checked = backend.check(system, witness)
    extra = checked.payload
    role = str(extra.get("role", "inconclusive"))
    status = _status_from_check(existential=system.existential, role=role)
    return role == str(payload.get("role", "")) and status == str(
        payload.get("status", status)
    )

Other public import paths

omnibias.core.proof.replay_inequality
omnibias.core.proof.inequality.replay_inequality

FUNCTION

run_inequality_pipeline

omnibias.core.proof.run_inequality_pipelineSource ↗

run_inequality_pipeline(system: InequalitySystem) -> tuple[VerdictStatus, dict[str, Any], dict[str, bool]]

Propose → rationalize → check. Returns (status, payload, honesty).

Parameters

Name	Type & default	Contract
`system`positional-or-keyword	`InequalitySystem`Required	See the operation contract and implementation below.

Returnstuple[VerdictStatus, dict[str, Any], dict[str, bool]]

Explicit validation & failure cases

When extra.get('soft_residual_is_exact_check'), raises ValueError('soft residual cannot become an ExactCheck').

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

Executed regression · missing backend is blocked

Full file, imports & fixtures ↗

def test_missing_backend_is_blocked() -> None:
    _reset_inequality_backends_for_tests()
    system = InequalitySystem(sort="linear", existential=True, data={})
    status, payload, honesty = run_inequality_pipeline(system)
    assert status == "BLOCKED"
    assert payload["detail"] == "backend_unavailable"
    attempt = prove_inequality(
        Conjecture("missing", INEQUALITY_KIND, system.as_dict())
    )
    assert attempt.status == "BLOCKED"

python -m pytest "packages/omnibias-core/tests/test_inequality_protocol.py::test_missing_backend_is_blocked" -q

Regression example · boolean three verdicts

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_boolean_three_verdicts() -> None:
    register_inequality_backend(BooleanInequalityBackend())
    proved = InequalitySystem(
        sort="boolean",
        existential=True,
        data={"tables": [[0, 0, 0, 1]]},
    )
    disproved = InequalitySystem(
        sort="boolean",
        existential=True,
        data={"tables": [[1, 1]]},
    )
    blocked = InequalitySystem(
        sort="boolean",
        existential=True,
        data={"tables": [[0, 0, 0, 1]], "budget": 0},
    )
    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-boolean/tests/test_inequality_adapter.py -k test_boolean_three_verdicts -q

Read the implementation

def run_inequality_pipeline(
    system: InequalitySystem,
) -> tuple[VerdictStatus, dict[str, Any], dict[str, bool]]:
    """Propose → rationalize → check. Returns ``(status, payload, honesty)``."""

    backend = _BACKENDS.get(system.sort)
    if backend is None:
        payload: dict[str, Any] = {
            "sort": system.sort,
            "existential": system.existential,
            "role": "inconclusive",
            "status": "BLOCKED",
            "detail": "backend_unavailable",
            "pipeline": [],
            "system": system.as_dict(),
        }
        return "BLOCKED", payload, default_inequality_honesty()
    proposal = backend.propose(system)
    witness = backend.rationalize(system, proposal)
    checked = backend.check(system, witness)
    extra = checked.payload
    role = str(extra.get("role", "inconclusive"))
    if extra.get("soft_residual_is_exact_check"):
        raise ValueError("soft residual cannot become an ExactCheck")
    pipeline: list[str] = []
    if not proposal.skipped:
        pipeline.append("propose")
    pipeline.extend(["rationalize", "check"])
    status = _status_from_check(existential=system.existential, role=role)
    payload = {
        "sort": system.sort,
        "existential": system.existential,
        "role": role,
        "status": status,
        "ok": checked.ok,
        "pipeline": pipeline,
        "propose_method": proposal.method,
        "rationalize_method": witness.method,
        "check_method": str(extra.get("method", "")),
        "witness": list(witness.values),
        "system": system.as_dict(),
        "detail": str(extra.get("detail", "")),
    }
    honesty_raw = extra.get("honesty")
    honesty_extra: dict[str, Any] = (
        dict(honesty_raw) if isinstance(honesty_raw, Mapping) else {}
    )
    honesty = _merge_honesty(honesty_extra)
    if role == "empty":
        honesty["unsat_proof"] = True
    return status, payload, honesty

Other public import paths

omnibias.core.proof.run_inequality_pipeline
omnibias.core.proof.inequality.run_inequality_pipeline

FUNCTION

solve_inequality

omnibias.core.proof.solve_inequalitySource ↗

solve_inequality(system: InequalitySystem, *, replay: bool=True) -> Verdict

Convenience: one system through build_inequality_machine.

Parameters

Name	Type & default	Contract
`system`positional-or-keyword	`InequalitySystem`Required	See the operation contract and implementation below.
`replay`keyword-only	`bool`Default: True	See the operation contract and implementation below.

ReturnsVerdict

Read the implementation

def solve_inequality(system: InequalitySystem, *, replay: bool = True) -> Verdict:
    """Convenience: one system through :func:`build_inequality_machine`."""

    from omnibias.core.proof import Conjecture

    machine = build_inequality_machine()
    return machine.evaluate(
        Conjecture(
            name=system.name or system.sort,
            kind=INEQUALITY_KIND,
            data=system.as_dict(),
        ),
        replay=replay,
    )

Other public import paths

omnibias.core.proof.solve_inequality
omnibias.core.proof.inequality.solve_inequality

← Package overview Runnable learning examples →

omnibias.core.proof.inequality

CheckRole​

INEQUALITY_KIND​

InequalityBackend​

Fields & methods

Parameters

Parameters

Parameters

InequalitySort​

InequalitySystem​

Parameters

Fields & methods

Parameters

Proposal​

Parameters

Fields & methods

RationalWitness​

Parameters

Fields & methods

build_inequality_machine​

default_inequality_honesty​

inequality_backend​

Parameters

inequality_prover​

inequality_schema_errors​

Parameters

list_inequality_backends​

load_inequality_stack​

locked_catalog​

prove_inequality​

Parameters

register_inequality_backend​

Parameters

replay_inequality​

Parameters

run_inequality_pipeline​

Parameters

solve_inequality​

Parameters

CheckRole

INEQUALITY_KIND

InequalityBackend

InequalitySort

InequalitySystem

Proposal

RationalWitness

build_inequality_machine

default_inequality_honesty

inequality_backend

inequality_prover

inequality_schema_errors

list_inequality_backends

load_inequality_stack

locked_catalog

prove_inequality

register_inequality_backend

replay_inequality

run_inequality_pipeline

solve_inequality