omnibias.sos.formal
Sum-of-squares constructions, polynomial positivity checks, and rigorous validation of proposed Gram matrices.
import omnibias.sos.formalModule contract & mathematical conventions
Hand a sealed SOS certificate to the Lean kernel.
An SOS proof reduces to a *finite, rational* fact: the interval LDL^T pivots
of the Gram matrix are all positive. That is exactly the obligation the repo's
Mathlib-free kernel already proves -- so this module writes **no Lean**. It
forwards the sealed positive_definite certificate to
omnibias.core.proof.lean_check.check_certificate, which emits the
allPivotsPos [...] = true obligation (matrix_positive_definite_certified)
and runs lake build.
theorem_prover_verified is earned **only** by a genuine lake pass; with no
toolchain present the check degrades gracefully (available=False,
verified=False) and never raises.
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.
is_theorem_prover_verified
omnibias.sos.is_theorem_prover_verifiedSource ↗is_theorem_prover_verified(sealed_certificate: Mapping[str, Any], *, timeout: float=600.0) -> boolTrue iff the Lean kernel accepts the certificate's PD obligation.
Parameters
| Name | Type & default | Contract |
|---|---|---|
sealed_certificatepositional-or-keyword | Mapping[str, Any]Required | See the operation contract and implementation below. |
timeoutkeyword-only | floatDefault: 600.0 | See the operation contract and implementation below. |
boolRegression example · lean check degrades gracefully
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_lean_check_degrades_gracefully() -> None:
_cert, sealed = _sealed()
result = lean_check_sos(sealed)
if not lean_available():
assert result.available is False
assert result.verified is False
assert not is_theorem_prover_verified(sealed)
else: # pragma: no cover - only when a Lean toolchain is installed
assert result.available is Truepython -m pytest packages/omnibias-sos/tests/test_honesty_formal.py -k test_lean_check_degrades_gracefully -qRead the implementation
def is_theorem_prover_verified(
sealed_certificate: Mapping[str, Any], *, timeout: float = 600.0
) -> bool:
"""``True`` iff the Lean kernel accepts the certificate's PD obligation."""
return bool(lean_check_sos(sealed_certificate, timeout=timeout).verified)Other public import paths
omnibias.sos.is_theorem_prover_verifiedomnibias.sos.formal.is_theorem_prover_verified
lean_available
omnibias.sos.lean_availableSource ↗lean_available() -> boolTrue iff a lake executable and the verified-kernel checkout are present.
boolExecuted regression · lean check degrades gracefully
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_lean_check_degrades_gracefully() -> None:
_cert, sealed = _sealed()
result = lean_check_sos(sealed)
if not lean_available():
assert result.available is False
assert result.verified is False
assert not is_theorem_prover_verified(sealed)
else: # pragma: no cover - only when a Lean toolchain is installed
assert result.available is Truepython -m pytest "packages/omnibias-sos/tests/test_honesty_formal.py::test_lean_check_degrades_gracefully" -qRead the implementation
def lean_available() -> bool:
"""``True`` iff a ``lake`` executable and the verified-kernel checkout are present."""
return bool(lean_check_available())Other public import paths
omnibias.sos.lean_availableomnibias.sos.formal.lean_available
lean_check_sos
omnibias.sos.lean_check_sosSource ↗lean_check_sos(sealed_certificate: Mapping[str, Any], *, timeout: float=600.0) -> LeanCheckResultKernel-check a sealed SOS certificate's allPivotsPos obligation.
Returns a ~omnibias.core.proof.lean_check.LeanCheckResult;
verified is True only on a genuine lake pass, available is
False when no Lean toolchain / kernel checkout is present.
Parameters
| Name | Type & default | Contract |
|---|---|---|
sealed_certificatepositional-or-keyword | Mapping[str, Any]Required | See the operation contract and implementation below. |
timeoutkeyword-only | floatDefault: 600.0 | See the operation contract and implementation below. |
LeanCheckResultExecuted regression · lean check degrades gracefully
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_lean_check_degrades_gracefully() -> None:
_cert, sealed = _sealed()
result = lean_check_sos(sealed)
if not lean_available():
assert result.available is False
assert result.verified is False
assert not is_theorem_prover_verified(sealed)
else: # pragma: no cover - only when a Lean toolchain is installed
assert result.available is Truepython -m pytest "packages/omnibias-sos/tests/test_honesty_formal.py::test_lean_check_degrades_gracefully" -qRegression example · tamper evidence blocks lean
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_tamper_evidence_blocks_lean() -> None:
_cert, sealed = _sealed()
tampered = dict(sealed)
tampered["payload"] = dict(sealed["payload"])
pivots = [dict(p) for p in sealed["payload"]["pivots"]]
pivots[0]["lo"] = (0.5).hex() # forge a "better" margin
tampered["payload"]["pivots"] = pivots
assert not verify_certificate_digest(tampered)
result = lean_check_sos(tampered)
assert result.verified is False
assert "digest" in result.detail.lower()python -m pytest packages/omnibias-sos/tests/test_honesty_formal.py -k test_tamper_evidence_blocks_lean -qRead the implementation
def lean_check_sos(
sealed_certificate: Mapping[str, Any], *, timeout: float = 600.0
) -> LeanCheckResult:
r"""Kernel-check a sealed SOS certificate's ``allPivotsPos`` obligation.
Returns a :class:`~omnibias.core.proof.lean_check.LeanCheckResult`;
``verified`` is ``True`` only on a genuine ``lake`` pass, ``available`` is
``False`` when no Lean toolchain / kernel checkout is present.
"""
return check_certificate(sealed_certificate, timeout=timeout)Other public import paths
omnibias.sos.lean_check_sosomnibias.sos.formal.lean_check_sos