omnibias.convex.inequality
Differentiable LP and QP solver paths, barrier methods, KKT sensitivities, and scoped optimality evidence.
import omnibias.convex.inequalityModule contract & mathematical conventions
Linear inequality adapter (theory 09-30).
Propose via arrangement soft membership (temperature collapse). Check
slacks over Q. Emptiness only via vertex enum under
VERTEX_ENUM_MAX_*. InfeasibleProblemError is never DISPROVED.
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.
CLASS
LinearInequalityBackend
omnibias.convex.LinearInequalityBackendSource ↗class LinearInequalityBackendThe module contract describes the context for this operation. Its signature, explicit validation, return expressions, and implementation are recorded below.
Executed regression · linear 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.
def test_linear_three_verdicts() -> None:
register_inequality_backend(LinearInequalityBackend())
proved = InequalitySystem(
sort="linear",
existential=True,
data={"A": [["1"], ["-1"]], "b": ["1", "0"]},
)
disproved = InequalitySystem(
sort="linear",
existential=True,
data={"A": [["1"], ["-1"]], "b": ["-1", "-1"]},
)
high_a = []
high_b = []
for i in range(5):
pos = ["0"] * 5
neg = ["0"] * 5
pos[i] = "1"
neg[i] = "-1"
high_a.extend([pos, neg])
high_b.extend(["-1", "-1"])
blocked = InequalitySystem(
sort="linear",
existential=True,
data={"A": high_a, "b": high_b},
)
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-convex/tests/test_inequality_adapter.py::test_linear_three_verdicts" -qFields & methods
sortfield
sort: ClassVar[InequalitySort] = 'linear'Declared ClassVar[InequalitySort] field on LinearInequalityBackend. Default expression: 'linear'.
proposemethod
propose(self, system: InequalitySystem) -> ProposalSee 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 · linear 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.
def test_linear_three_verdicts() -> None:
register_inequality_backend(LinearInequalityBackend())
proved = InequalitySystem(
sort="linear",
existential=True,
data={"A": [["1"], ["-1"]], "b": ["1", "0"]},
)
disproved = InequalitySystem(
sort="linear",
existential=True,
data={"A": [["1"], ["-1"]], "b": ["-1", "-1"]},
)
high_a = []
high_b = []
for i in range(5):
pos = ["0"] * 5
neg = ["0"] * 5
pos[i] = "1"
neg[i] = "-1"
high_a.extend([pos, neg])
high_b.extend(["-1", "-1"])
blocked = InequalitySystem(
sort="linear",
existential=True,
data={"A": high_a, "b": high_b},
)
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-convex/tests/test_inequality_adapter.py::test_linear_three_verdicts" -qMethod implementation
def propose(self, system: InequalitySystem) -> Proposal:
a_mat = _matrix(system.data.get("A", ()))
b_vec = _vector(system.data.get("b", ()))
dim = len(a_mat[0]) if a_mat else 0
candidate = [0.0] * dim
poly = LearnedPolytope(
np.asarray([[float(v) for v in row] for row in a_mat], dtype=np.float64),
np.asarray([float(v) for v in b_vec], dtype=np.float64),
)
weight = float(soft_membership(poly, candidate, beta=8.0))
return Proposal(
method="soft_membership",
values=tuple(str(value) for value in candidate),
payload={"membership": weight, "beta": 8.0},
)rationalizemethod
rationalize(self, system: InequalitySystem, proposal: Proposal) -> RationalWitnessSee 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 · linear 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.
def test_linear_three_verdicts() -> None:
register_inequality_backend(LinearInequalityBackend())
proved = InequalitySystem(
sort="linear",
existential=True,
data={"A": [["1"], ["-1"]], "b": ["1", "0"]},
)
disproved = InequalitySystem(
sort="linear",
existential=True,
data={"A": [["1"], ["-1"]], "b": ["-1", "-1"]},
)
high_a = []
high_b = []
for i in range(5):
pos = ["0"] * 5
neg = ["0"] * 5
pos[i] = "1"
neg[i] = "-1"
high_a.extend([pos, neg])
high_b.extend(["-1", "-1"])
blocked = InequalitySystem(
sort="linear",
existential=True,
data={"A": high_a, "b": high_b},
)
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-convex/tests/test_inequality_adapter.py::test_linear_three_verdicts" -qMethod implementation
def rationalize(
self, system: InequalitySystem, proposal: Proposal
) -> RationalWitness:
values = tuple(
str(Fraction(item).limit_denominator(_FRAC_LIM)) for item in proposal.values
)
return RationalWitness(method="nearest_q", values=values, payload=dict(proposal.payload))checkmethod
check(self, system: InequalitySystem, witness: RationalWitness) -> ExactCheckSee 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 · linear 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.
def test_linear_three_verdicts() -> None:
register_inequality_backend(LinearInequalityBackend())
proved = InequalitySystem(
sort="linear",
existential=True,
data={"A": [["1"], ["-1"]], "b": ["1", "0"]},
)
disproved = InequalitySystem(
sort="linear",
existential=True,
data={"A": [["1"], ["-1"]], "b": ["-1", "-1"]},
)
high_a = []
high_b = []
for i in range(5):
pos = ["0"] * 5
neg = ["0"] * 5
pos[i] = "1"
neg[i] = "-1"
high_a.extend([pos, neg])
high_b.extend(["-1", "-1"])
blocked = InequalitySystem(
sort="linear",
existential=True,
data={"A": high_a, "b": high_b},
)
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-convex/tests/test_inequality_adapter.py::test_linear_three_verdicts" -qMethod implementation
def check(
self, system: InequalitySystem, witness: RationalWitness
) -> ExactCheck:
a_mat = _matrix(system.data.get("A", ()))
b_vec = _vector(system.data.get("b", ()))
x = tuple(_as_frac(item) for item in witness.values)
honesty = dict(honesty_payload())
honesty["new_lp_algorithm_claim"] = False
honesty["complete_solver"] = False
if len(x) != (len(a_mat[0]) if a_mat else 0):
return ExactCheck(
ok=False,
payload={
"role": "inconclusive",
"method": "dimension_mismatch",
"honesty": honesty,
"detail": "dimension_mismatch",
},
)
slacks = _slacks_q(a_mat, b_vec, x)
if all(s >= 0 for s in slacks):
return ExactCheck(
ok=True,
payload={
"role": "witness",
"method": "exact_slack",
"honesty": honesty,
"detail": "feasible_q",
"slacks": [str(s) for s in slacks],
},
)
dim = len(a_mat[0]) if a_mat else 0
n_ineq = len(a_mat)
if dim > VERTEX_ENUM_MAX_D or n_ineq > VERTEX_ENUM_MAX_N:
return ExactCheck(
ok=False,
payload={
"role": "inconclusive",
"method": "enum_refused",
"honesty": honesty,
"detail": "vertex_enum_refused",
},
)
poly = LearnedPolytope(
np.asarray([[float(v) for v in row] for row in a_mat], dtype=np.float64),
np.asarray([float(v) for v in b_vec], dtype=np.float64),
)
verts = enumerate_vertices(poly)
if verts.shape[0] == 0:
honesty["unsat_proof"] = True
return ExactCheck(
ok=False,
payload={
"role": "empty",
"method": "vertex_enum_empty",
"honesty": honesty,
"detail": "vertex_enum_empty",
"complete": True,
},
)
return ExactCheck(
ok=False,
payload={
"role": "inconclusive",
"method": "point_infeasible",
"honesty": honesty,
"detail": "proposed_point_infeasible",
},
)Read the implementation
class LinearInequalityBackend:
sort: ClassVar[InequalitySort] = "linear"
def propose(self, system: InequalitySystem) -> Proposal:
a_mat = _matrix(system.data.get("A", ()))
b_vec = _vector(system.data.get("b", ()))
dim = len(a_mat[0]) if a_mat else 0
candidate = [0.0] * dim
poly = LearnedPolytope(
np.asarray([[float(v) for v in row] for row in a_mat], dtype=np.float64),
np.asarray([float(v) for v in b_vec], dtype=np.float64),
)
weight = float(soft_membership(poly, candidate, beta=8.0))
return Proposal(
method="soft_membership",
values=tuple(str(value) for value in candidate),
payload={"membership": weight, "beta": 8.0},
)
def rationalize(
self, system: InequalitySystem, proposal: Proposal
) -> RationalWitness:
values = tuple(
str(Fraction(item).limit_denominator(_FRAC_LIM)) for item in proposal.values
)
return RationalWitness(method="nearest_q", values=values, payload=dict(proposal.payload))
def check(
self, system: InequalitySystem, witness: RationalWitness
) -> ExactCheck:
a_mat = _matrix(system.data.get("A", ()))
b_vec = _vector(system.data.get("b", ()))
x = tuple(_as_frac(item) for item in witness.values)
honesty = dict(honesty_payload())
honesty["new_lp_algorithm_claim"] = False
honesty["complete_solver"] = False
if len(x) != (len(a_mat[0]) if a_mat else 0):
return ExactCheck(
ok=False,
payload={
"role": "inconclusive",
"method": "dimension_mismatch",
"honesty": honesty,
"detail": "dimension_mismatch",
},
)
slacks = _slacks_q(a_mat, b_vec, x)
if all(s >= 0 for s in slacks):
return ExactCheck(
ok=True,
payload={
"role": "witness",
"method": "exact_slack",
"honesty": honesty,
"detail": "feasible_q",
"slacks": [str(s) for s in slacks],
},
)
dim = len(a_mat[0]) if a_mat else 0
n_ineq = len(a_mat)
if dim > VERTEX_ENUM_MAX_D or n_ineq > VERTEX_ENUM_MAX_N:
return ExactCheck(
ok=False,
payload={
"role": "inconclusive",
"method": "enum_refused",
"honesty": honesty,
"detail": "vertex_enum_refused",
},
)
poly = LearnedPolytope(
np.asarray([[float(v) for v in row] for row in a_mat], dtype=np.float64),
np.asarray([float(v) for v in b_vec], dtype=np.float64),
)
verts = enumerate_vertices(poly)
if verts.shape[0] == 0:
honesty["unsat_proof"] = True
return ExactCheck(
ok=False,
payload={
"role": "empty",
"method": "vertex_enum_empty",
"honesty": honesty,
"detail": "vertex_enum_empty",
"complete": True,
},
)
return ExactCheck(
ok=False,
payload={
"role": "inconclusive",
"method": "point_infeasible",
"honesty": honesty,
"detail": "proposed_point_infeasible",
},
)Other public import paths
omnibias.convex.LinearInequalityBackendomnibias.convex.inequality.LinearInequalityBackend