omnibias.sos.honesty

0.1.0a2AlphaPython >=3.10AGPL / commercial

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

import omnibias.sos.honesty

Module contract & mathematical conventions

Scope labels and tamper-evident sealing for SOS certificates.

An SOS proof is a genuine for all x statement -- but only about what it actually covers. This module records that scope honestly and seals a proved ~omnibias.sos.problem.SOSCertificate into a canonical, hash-sealed v1 positive_definite certificate (via omnibias.core.proof.certificate), so it can flow through the repo's schema / replay / Lean gates.

Every sealed certificate carries unproven_claim = False **by construction** -- there is no parameter, anywhere, that can set it True. The scope is one of:

global_polynomial -- p(x) >= 0 for all real x (a true universal statement about a polynomial);
finite_dim_system -- a bound holding for all data of a finite-dimensional system (e.g. a polynomial ODE);
galerkin_truncation -- a bound for a Galerkin-truncated PDE at a stated truncation_order -- explicitly **not** the continuum PDE and **not** a regularity / global-regularity statement.

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

FINITE_DIM_SYSTEM

omnibias.sos.FINITE_DIM_SYSTEMSource ↗

FINITE_DIM_SYSTEM = 'finite_dim_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 · no scope can emit unproven claim true

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_no_scope_can_emit_unproven_claim_true() -> None:
    # Every valid scope, and the default, must produce unproven_claim == False.
    for kind in (GLOBAL_POLYNOMIAL, FINITE_DIM_SYSTEM, GALERKIN_TRUNCATION):
        assert honesty_labels(SOSScope(kind))["unproven_claim"] is False

python -m pytest packages/omnibias-sos/tests/test_honesty_formal.py -k test_no_scope_can_emit_unproven_claim_true -q

Regression example · scope labels are honest

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_scope_labels_are_honest(scope: SOSScope, finite: bool) -> None:
    labels = honesty_labels(scope)
    assert labels["unproven_claim"] is False
    assert labels["finite_dimensional"] is finite
    cert = certify_sos(PD_POLY)
    sealed = seal_sos_certificate(cert, claim="bound", scope=scope)
    assert sealed["honesty"]["unproven_claim"] is False
    assert sealed["meta"]["sos"]["scope"] == scope.kind
    assert sealed["meta"]["sos"]["truncation_order"] == scope.truncation_order

python -m pytest packages/omnibias-sos/tests/test_honesty_formal.py -k test_scope_labels_are_honest -q

Read the implementation

FINITE_DIM_SYSTEM = "finite_dim_system"

Other public import paths

omnibias.sos.FINITE_DIM_SYSTEM
omnibias.sos.honesty.FINITE_DIM_SYSTEM

CONSTANT

GALERKIN_TRUNCATION

omnibias.sos.GALERKIN_TRUNCATIONSource ↗

GALERKIN_TRUNCATION = 'galerkin_truncation'

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 · no scope can emit unproven claim true

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_no_scope_can_emit_unproven_claim_true() -> None:
    # Every valid scope, and the default, must produce unproven_claim == False.
    for kind in (GLOBAL_POLYNOMIAL, FINITE_DIM_SYSTEM, GALERKIN_TRUNCATION):
        assert honesty_labels(SOSScope(kind))["unproven_claim"] is False

python -m pytest packages/omnibias-sos/tests/test_honesty_formal.py -k test_no_scope_can_emit_unproven_claim_true -q

Regression example · scope labels are honest

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_scope_labels_are_honest(scope: SOSScope, finite: bool) -> None:
    labels = honesty_labels(scope)
    assert labels["unproven_claim"] is False
    assert labels["finite_dimensional"] is finite
    cert = certify_sos(PD_POLY)
    sealed = seal_sos_certificate(cert, claim="bound", scope=scope)
    assert sealed["honesty"]["unproven_claim"] is False
    assert sealed["meta"]["sos"]["scope"] == scope.kind
    assert sealed["meta"]["sos"]["truncation_order"] == scope.truncation_order

python -m pytest packages/omnibias-sos/tests/test_honesty_formal.py -k test_scope_labels_are_honest -q

Read the implementation

GALERKIN_TRUNCATION = "galerkin_truncation"

Other public import paths

omnibias.sos.GALERKIN_TRUNCATION
omnibias.sos.honesty.GALERKIN_TRUNCATION

CONSTANT

GLOBAL_POLYNOMIAL

omnibias.sos.GLOBAL_POLYNOMIALSource ↗

GLOBAL_POLYNOMIAL = 'global_polynomial'

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 · no scope can emit unproven claim true

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_no_scope_can_emit_unproven_claim_true() -> None:
    # Every valid scope, and the default, must produce unproven_claim == False.
    for kind in (GLOBAL_POLYNOMIAL, FINITE_DIM_SYSTEM, GALERKIN_TRUNCATION):
        assert honesty_labels(SOSScope(kind))["unproven_claim"] is False

python -m pytest packages/omnibias-sos/tests/test_honesty_formal.py -k test_no_scope_can_emit_unproven_claim_true -q

Regression example · scope labels are honest

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_scope_labels_are_honest(scope: SOSScope, finite: bool) -> None:
    labels = honesty_labels(scope)
    assert labels["unproven_claim"] is False
    assert labels["finite_dimensional"] is finite
    cert = certify_sos(PD_POLY)
    sealed = seal_sos_certificate(cert, claim="bound", scope=scope)
    assert sealed["honesty"]["unproven_claim"] is False
    assert sealed["meta"]["sos"]["scope"] == scope.kind
    assert sealed["meta"]["sos"]["truncation_order"] == scope.truncation_order

python -m pytest packages/omnibias-sos/tests/test_honesty_formal.py -k test_scope_labels_are_honest -q

Read the implementation

GLOBAL_POLYNOMIAL = "global_polynomial"

Other public import paths

omnibias.sos.GLOBAL_POLYNOMIAL
omnibias.sos.honesty.GLOBAL_POLYNOMIAL

CLASS

SOSScope

omnibias.sos.SOSScopeSource ↗

class SOSScope

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.

What an SOS / auxiliary-functional certificate actually claims.

kind must be one of GLOBAL_POLYNOMIAL, FINITE_DIM_SYSTEM, or GALERKIN_TRUNCATION. truncation_order records the Galerkin order (None outside a truncation); system is a free-text label.

Parameters

Name	Type & default	Contract
`kind`dataclass field	`str`Default: GLOBAL_POLYNOMIAL	See the operation contract and implementation below.
`truncation_order`dataclass field	`int \| None`Default: None	See the operation contract and implementation below.
`system`dataclass field	`str`Default: ''	See the operation contract and implementation below.

Executed regression · invalid scope rejected

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_invalid_scope_rejected() -> None:
    with pytest.raises(ValueError, match="scope kind"):
        SOSScope("unsupported_scope")

python -m pytest "packages/omnibias-sos/tests/test_honesty_formal.py::test_invalid_scope_rejected" -q

Regression example · no scope can emit unproven claim true

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_no_scope_can_emit_unproven_claim_true() -> None:
    # Every valid scope, and the default, must produce unproven_claim == False.
    for kind in (GLOBAL_POLYNOMIAL, FINITE_DIM_SYSTEM, GALERKIN_TRUNCATION):
        assert honesty_labels(SOSScope(kind))["unproven_claim"] is False

python -m pytest packages/omnibias-sos/tests/test_honesty_formal.py -k test_no_scope_can_emit_unproven_claim_true -q

Fields & methods

kindfield

kind: str = GLOBAL_POLYNOMIAL

Declared str field on SOSScope. Default expression: GLOBAL_POLYNOMIAL.

View source ↗

truncation_orderfield

truncation_order: int | None = None

Declared int | None field on SOSScope. Default expression: None.

View source ↗

systemfield

system: str = ''

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

View source ↗

__post_init__method

__post_init__(self) -> None

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

Returns: None

Validation & failure cases

When self.kind not in _VALID_SCOPES, raises ValueError(f'scope kind must be one of {sorted(_VALID_SCOPES)}, got {self.kind!r}').

Executed regression · invalid scope rejected

Full file, imports & fixtures ↗

def test_invalid_scope_rejected() -> None:
    with pytest.raises(ValueError, match="scope kind"):
        SOSScope("unsupported_scope")

python -m pytest "packages/omnibias-sos/tests/test_honesty_formal.py::test_invalid_scope_rejected" -q

Method implementation

    def __post_init__(self) -> None:
        if self.kind not in _VALID_SCOPES:
            raise ValueError(f"scope kind must be one of {sorted(_VALID_SCOPES)}, got {self.kind!r}")

View source ↗

finite_dimensionalproperty

finite_dimensional(self) -> bool

True for finite-dimensional / Galerkin scopes (not the global polynomial).

Returns: bool

Executed regression · no scope can emit unproven claim true

Full file, imports & fixtures ↗

def test_no_scope_can_emit_unproven_claim_true() -> None:
    # Every valid scope, and the default, must produce unproven_claim == False.
    for kind in (GLOBAL_POLYNOMIAL, FINITE_DIM_SYSTEM, GALERKIN_TRUNCATION):
        assert honesty_labels(SOSScope(kind))["unproven_claim"] is False

python -m pytest "packages/omnibias-sos/tests/test_honesty_formal.py::test_no_scope_can_emit_unproven_claim_true" -q

Method implementation

    def finite_dimensional(self) -> bool:
        """``True`` for finite-dimensional / Galerkin scopes (not the global polynomial)."""
        return self.kind != GLOBAL_POLYNOMIAL

View source ↗

Read the implementation

class SOSScope:
    """What an SOS / auxiliary-functional certificate actually claims.

    ``kind`` must be one of :data:`GLOBAL_POLYNOMIAL`, :data:`FINITE_DIM_SYSTEM`,
    or :data:`GALERKIN_TRUNCATION`.  ``truncation_order`` records the Galerkin
    order (``None`` outside a truncation); ``system`` is a free-text label.
    """

    kind: str = GLOBAL_POLYNOMIAL
    truncation_order: int | None = None
    system: str = ""

    def __post_init__(self) -> None:
        if self.kind not in _VALID_SCOPES:
            raise ValueError(f"scope kind must be one of {sorted(_VALID_SCOPES)}, got {self.kind!r}")

    @property
    def finite_dimensional(self) -> bool:
        """``True`` for finite-dimensional / Galerkin scopes (not the global polynomial)."""
        return self.kind != GLOBAL_POLYNOMIAL

Other public import paths

omnibias.sos.SOSScope
omnibias.sos.honesty.SOSScope

FUNCTION

honesty_labels

omnibias.sos.honesty_labelsSource ↗

honesty_labels(scope: SOSScope) -> dict[str, bool]

The boolean honesty flags for scope; unproven_claim is always False.

None of these can be flipped by any caller-supplied value -- soundness of the scope labelling does not depend on trust in the caller.

Parameters

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

Returnsdict[str, bool]

Executed regression · no scope can emit unproven claim true

Full file, imports & fixtures ↗

def test_no_scope_can_emit_unproven_claim_true() -> None:
    # Every valid scope, and the default, must produce unproven_claim == False.
    for kind in (GLOBAL_POLYNOMIAL, FINITE_DIM_SYSTEM, GALERKIN_TRUNCATION):
        assert honesty_labels(SOSScope(kind))["unproven_claim"] is False

python -m pytest "packages/omnibias-sos/tests/test_honesty_formal.py::test_no_scope_can_emit_unproven_claim_true" -q

Regression example · scope labels are honest

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_scope_labels_are_honest(scope: SOSScope, finite: bool) -> None:
    labels = honesty_labels(scope)
    assert labels["unproven_claim"] is False
    assert labels["finite_dimensional"] is finite
    cert = certify_sos(PD_POLY)
    sealed = seal_sos_certificate(cert, claim="bound", scope=scope)
    assert sealed["honesty"]["unproven_claim"] is False
    assert sealed["meta"]["sos"]["scope"] == scope.kind
    assert sealed["meta"]["sos"]["truncation_order"] == scope.truncation_order

python -m pytest packages/omnibias-sos/tests/test_honesty_formal.py -k test_scope_labels_are_honest -q

Read the implementation

def honesty_labels(scope: SOSScope) -> dict[str, bool]:
    """The boolean honesty flags for ``scope``; ``unproven_claim`` is always ``False``.

    None of these can be flipped by any caller-supplied value -- soundness of the
    scope labelling does not depend on trust in the caller.
    """
    return {
        "unproven_claim": False,
        "continuum_pde_claim": False,
        "regularity_claim": False,
        "finite_dimensional": scope.finite_dimensional,
    }

Other public import paths

omnibias.sos.honesty_labels
omnibias.sos.honesty.honesty_labels

FUNCTION

seal_sos_certificate

omnibias.sos.seal_sos_certificateSource ↗

seal_sos_certificate(certificate: SOSCertificate, *, claim: str, scope: SOSScope | None=None, meta: Mapping[str, Any] | None=None) -> Cert

Seal a **proved** SOS certificate into a v1 positive_definite certificate.

The interval LDL^T pivots become the certificate payload the Lean bridge turns into the allPivotsPos obligation. Raises ValueError on an inconclusive certificate -- there is nothing sound to seal.

Parameters

Name	Type & default	Contract
`certificate`positional-or-keyword	`SOSCertificate`Required	See the operation contract and implementation below.
`claim`keyword-only	`str`Required	See the operation contract and implementation below.
`scope`keyword-only	`SOSScope \| None`Default: None	See the operation contract and implementation below.
`meta`keyword-only	`Mapping[str, Any] \| None`Default: None	See the operation contract and implementation below.

ReturnsCert

Explicit validation & failure cases

When not certificate.certified, raises ValueError('cannot seal an inconclusive SOS certificate (no proof to record)').

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

Executed regression · cannot seal inconclusive

Full file, imports & fixtures ↗

def test_cannot_seal_inconclusive() -> None:
    motzkin = Polynomial(2, {(4, 2): 1.0, (2, 4): 1.0, (2, 2): -3.0, (0, 0): 1.0})
    cert = certify_sos(motzkin)
    assert not cert.certified
    with pytest.raises(ValueError, match="inconclusive"):
        seal_sos_certificate(cert, claim="should not seal")

python -m pytest "packages/omnibias-sos/tests/test_honesty_formal.py::test_cannot_seal_inconclusive" -q

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

Full file, imports & fixtures ↗

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 True

python -m pytest packages/omnibias-sos/tests/test_honesty_formal.py -k test_lean_check_degrades_gracefully -q

Read the implementation

def seal_sos_certificate(
    certificate: SOSCertificate,
    *,
    claim: str,
    scope: SOSScope | None = None,
    meta: Mapping[str, Any] | None = None,
) -> Cert:
    r"""Seal a **proved** SOS certificate into a v1 ``positive_definite`` certificate.

    The interval ``LDL^T`` pivots become the certificate payload the Lean bridge
    turns into the ``allPivotsPos`` obligation.  Raises :class:`ValueError` on an
    inconclusive certificate -- there is nothing sound to seal.
    """
    if not certificate.certified:
        raise ValueError("cannot seal an inconclusive SOS certificate (no proof to record)")
    if scope is None:
        scope = SOSScope(GLOBAL_POLYNOMIAL)

    pivots = [Interval(lo, hi) for lo, hi in certificate.pivots]
    sealed_meta: dict[str, Any] = {
        "generator": "omnibias-sos",
        "sos": {
            "scope": scope.kind,
            "truncation_order": scope.truncation_order,
            "system": scope.system,
            "n_vars": certificate.n_vars,
            "basis_size": len(certificate.basis),
            "pd_margin": certificate.pd_margin,
            "gram": [list(row) for row in certificate.gram] if certificate.gram else None,
        },
    }
    if meta is not None:
        sealed_meta.update(meta)

    return positive_definite_certificate(
        claim,
        pivots,
        honesty=honesty_labels(scope),
        meta=sealed_meta,
    )

Other public import paths

omnibias.sos.seal_sos_certificate
omnibias.sos.honesty.seal_sos_certificate

← Package overview Runnable learning examples →

omnibias.sos.honesty

FINITE_DIM_SYSTEM​

GALERKIN_TRUNCATION​

GLOBAL_POLYNOMIAL​

SOSScope​

Parameters

Fields & methods

honesty_labels​

Parameters

seal_sos_certificate​

Parameters

FINITE_DIM_SYSTEM

GALERKIN_TRUNCATION

GLOBAL_POLYNOMIAL

SOSScope

honesty_labels

seal_sos_certificate