omnibias.sos.positivstellensatz

0.1.0a2AlphaPython >=3.10AGPL / commercial

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

import omnibias.sos.positivstellensatz

Module contract & mathematical conventions

Constrained positivity by a certified Putinar representation.

To prove p(x) >= 0 for all x in the semialgebraic set S = {x : g_1(x) >= 0, ..., g_k(x) >= 0} it suffices to exhibit an identity

p = s_0 + s_1 g_1 + ... + s_k g_k

with every s_i a sum of squares (Putinar's Positivstellensatz, fixed degree): on S each s_i g_i >= 0 and s_0 >= 0, so p >= 0.

The SDP proposes the SOS multipliers s_i (one PSD Gram block each, packed into one block-diagonal Gram with the cross blocks pinned to zero). The **proof** is again rigorous: the float blocks are rounded and the *joint* coefficient identity is projected exactly onto the rationals (a Gram entry now feeds several monomials, so this uses the general ~omnibias.sos.rounding.project_coefficients_exact rather than the disjoint-group shortcut), then every block is certified positive definite by interval LDL^T. Anything short of that is inconclusive.

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

PositivstellensatzCertificate

omnibias.sos.PositivstellensatzCertificateSource ↗

class PositivstellensatzCertificate

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.

Result of a constrained-positivity attempt via a Putinar representation.

Parameters

Name	Type & default	Contract
`status`dataclass field	`str`Required	See the operation contract and implementation below.
`n_vars`dataclass field	`int`Required	See the operation contract and implementation below.
`multipliers`dataclass field	`tuple[SOSMultiplier, ...]`Required	See the operation contract and implementation below.
`pivots`dataclass field	`tuple[tuple[float, float], ...]`Required	See the operation contract and implementation below.
`pd_margin`dataclass field	`float`Required	See the operation contract and implementation below.
`detail`dataclass field	`str`Required	See the operation contract and implementation below.

Executed regression · false statement is inconclusive

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_false_statement_is_inconclusive() -> None:
    # x - 5 <= -4 on [-1, 1]; must never be "proved".
    cert = certify_nonneg_on_set(X1 - 5.0 * ONE1, [ONE1 - X1 * X1])
    assert cert.status == "inconclusive"
    assert not cert.certified

python -m pytest "packages/omnibias-sos/tests/test_positivstellensatz.py::test_false_statement_is_inconclusive" -q

Fields & methods

statusfield

status: str

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

View source ↗

n_varsfield

n_vars: int

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

View source ↗

multipliersfield

multipliers: tuple[SOSMultiplier, ...]

Declared tuple[SOSMultiplier, ...] field on PositivstellensatzCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

pivotsfield

pivots: tuple[tuple[float, float], ...]

Declared tuple[tuple[float, float], ...] field on PositivstellensatzCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

pd_marginfield

pd_margin: float

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

View source ↗

detailfield

detail: str

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

View source ↗

certifiedproperty

certified(self) -> bool

Whether this is a sound proof of positivity on the constraint set.

Returns: bool

Executed regression · false statement is inconclusive

Full file, imports & fixtures ↗

def test_false_statement_is_inconclusive() -> None:
    # x - 5 <= -4 on [-1, 1]; must never be "proved".
    cert = certify_nonneg_on_set(X1 - 5.0 * ONE1, [ONE1 - X1 * X1])
    assert cert.status == "inconclusive"
    assert not cert.certified

python -m pytest "packages/omnibias-sos/tests/test_positivstellensatz.py::test_false_statement_is_inconclusive" -q

Method implementation

    def certified(self) -> bool:
        """Whether this is a sound proof of positivity on the constraint set."""
        return self.status == "proved"

View source ↗

Read the implementation

class PositivstellensatzCertificate:
    """Result of a constrained-positivity attempt via a Putinar representation."""

    status: str
    n_vars: int
    multipliers: tuple[SOSMultiplier, ...]
    pivots: tuple[tuple[float, float], ...]
    pd_margin: float
    detail: str

    @property
    def certified(self) -> bool:
        """Whether this is a sound proof of positivity on the constraint set."""
        return self.status == "proved"

Other public import paths

omnibias.sos.PositivstellensatzCertificate
omnibias.sos.positivstellensatz.PositivstellensatzCertificate

CLASS

SOSMultiplier

omnibias.sos.SOSMultiplierSource ↗

class SOSMultiplier

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.

One certified-SOS multiplier s_i in a Putinar representation.

Parameters

Name	Type & default	Contract
`constraint_index`dataclass field	`int`Required	See the operation contract and implementation below.
`basis`dataclass field	`tuple[Exponent, ...]`Required	See the operation contract and implementation below.
`gram`dataclass field	`tuple[tuple[str, ...], ...]`Required	See the operation contract and implementation below.

Fields & methods

constraint_indexfield

constraint_index: int

-1 for the free term s_0; otherwise the index of the constraint g_i.

View source ↗

basisfield

basis: tuple[Exponent, ...]

Declared tuple[Exponent, ...] field on SOSMultiplier. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

gramfield

gram: tuple[tuple[str, ...], ...]

Exact rational Gram of s_i (as strings).

View source ↗

Read the implementation

class SOSMultiplier:
    """One certified-SOS multiplier ``s_i`` in a Putinar representation."""

    constraint_index: int
    """``-1`` for the free term ``s_0``; otherwise the index of the constraint ``g_i``."""
    basis: tuple[Exponent, ...]
    gram: tuple[tuple[str, ...], ...]
    """Exact rational Gram of ``s_i`` (as strings)."""

Other public import paths

omnibias.sos.SOSMultiplier
omnibias.sos.positivstellensatz.SOSMultiplier

FUNCTION

certify_nonneg_on_set

omnibias.sos.certify_nonneg_on_setSource ↗

certify_nonneg_on_set(polynomial: Polynomial, constraints: Sequence[Polynomial], *, half_degree: int | None=None, denominators: Sequence[int]=DEFAULT_DENOMINATORS) -> PositivstellensatzCertificate

Certify polynomial >= 0 on {g_i >= 0} via a Putinar representation.

Parameters

polynomial: The polynomial to certify nonnegative on the constraint set. constraints: The polynomials g_i defining S = {x : g_i(x) >= 0}. half_degree: Relaxation half-degree omega (the free multiplier s_0 uses a basis up to omega; each s_i up to omega - ceil(deg g_i / 2)). Defaults to ceil(max deg / 2).

Returns

PositivstellensatzCertificate status == "proved" carries the exact rational SOS multipliers and their certified interval LDL^T pivots; status == "inconclusive" otherwise.

Parameters

Name	Type & default	Contract
`polynomial`positional-or-keyword	`Polynomial`Required	The polynomial to certify nonnegative on the constraint set.
`constraints`positional-or-keyword	`Sequence[Polynomial]`Required	The polynomials `g_i` defining `S = {x : g_i(x) >= 0}`.
`half_degree`keyword-only	`int \| None`Default: None	Relaxation half-degree `omega` (the free multiplier `s_0` uses a basis up to `omega`; each `s_i` up to `omega - ceil(deg g_i / 2)`). Defaults to `ceil(max deg / 2)`.
`denominators`keyword-only	`Sequence[int]`Default: DEFAULT_DENOMINATORS	See the operation contract and implementation below.

ReturnsPositivstellensatzCertificate

Executed regression · false statement is inconclusive

Full file, imports & fixtures ↗

def test_false_statement_is_inconclusive() -> None:
    # x - 5 <= -4 on [-1, 1]; must never be "proved".
    cert = certify_nonneg_on_set(X1 - 5.0 * ONE1, [ONE1 - X1 * X1])
    assert cert.status == "inconclusive"
    assert not cert.certified

python -m pytest "packages/omnibias-sos/tests/test_positivstellensatz.py::test_false_statement_is_inconclusive" -q

Regression example · interval constraint is proved and exact

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_interval_constraint_is_proved_and_exact() -> None:
    p = 2.0 * ONE1 - X1 * X1
    gs = [ONE1 - X1 * X1]  # [-1, 1]
    cert = certify_nonneg_on_set(p, gs)
    assert cert.certified
    assert _identity_holds(cert, p, gs)
    assert _min_in_set(p, gs) >= -1e-9
    assert is_nonneg_on_set(p, gs)

python -m pytest packages/omnibias-sos/tests/test_positivstellensatz.py -k test_interval_constraint_is_proved_and_exact -q

Read the implementation

def certify_nonneg_on_set(
    polynomial: Polynomial,
    constraints: Sequence[Polynomial],
    *,
    half_degree: int | None = None,
    denominators: Sequence[int] = DEFAULT_DENOMINATORS,
) -> PositivstellensatzCertificate:
    r"""Certify ``polynomial >= 0`` on ``{g_i >= 0}`` via a Putinar representation.

    Parameters
    ----------
    polynomial:
        The polynomial to certify nonnegative on the constraint set.
    constraints:
        The polynomials ``g_i`` defining ``S = {x : g_i(x) >= 0}``.
    half_degree:
        Relaxation half-degree ``omega`` (the free multiplier ``s_0`` uses a basis
        up to ``omega``; each ``s_i`` up to ``omega - ceil(deg g_i / 2)``).
        Defaults to ``ceil(max deg / 2)``.

    Returns
    -------
    PositivstellensatzCertificate
        ``status == "proved"`` carries the exact rational SOS multipliers and their
        certified interval ``LDL^T`` pivots; ``status == "inconclusive"`` otherwise.
    """
    n = polynomial.n_vars
    constraints = list(constraints)
    extended = [Polynomial.constant(1.0, n), *constraints]  # s_0 multiplies g_0 := 1
    _omega, bases = _default_bases(polynomial, constraints, half_degree)

    sizes = [len(b) for b in bases]
    offsets = [0]
    for size in sizes:
        offsets.append(offsets[-1] + size)
    total = offsets[-1]
    svec_idx = _svec_indices(total)
    svec_dim = _svec_dim(total)

    var_column: dict[tuple[int, int, int], int] = {}
    n_vars_lin = 0
    for block, basis in enumerate(bases):
        for r in range(len(basis)):
            for s in range(r, len(basis)):
                var_column[(block, r, s)] = n_vars_lin
                n_vars_lin += 1

    # Product monomials that can appear, plus every monomial of p (an unrepresentable
    # p-monomial then forces an all-zero == nonzero row, i.e. an honest infeasibility).
    alphas: set[Exponent] = set(polynomial.support)
    for block, basis in enumerate(bases):
        for r in range(len(basis)):
            for s in range(r, len(basis)):
                base_rs = tuple(basis[r][t] + basis[s][t] for t in range(n))
                for term in extended[block].support:
                    alphas.add(tuple(base_rs[t] + term[t] for t in range(n)))
    alpha_list = sorted(alphas)

    float_rows: list[list[float]] = []
    float_rhs: list[float] = []
    rational_rows: list[list[Fraction]] = []
    for alpha in alpha_list:
        srow = [0.0] * svec_dim
        rrow = [Fraction(0)] * n_vars_lin
        for block, basis in enumerate(bases):
            multiplier = extended[block]
            for r in range(len(basis)):
                for s in range(r, len(basis)):
                    needed = tuple(alpha[t] - basis[r][t] - basis[s][t] for t in range(n))
                    if any(v < 0 for v in needed):
                        continue
                    coeff = multiplier.coefficient(needed)
                    if coeff == 0.0:
                        continue
                    gr, gs = offsets[block] + r, offsets[block] + s
                    if r == s:
                        srow[svec_idx[(gr, gr)]] += coeff
                        rrow[var_column[(block, r, s)]] += Fraction(coeff)
                    else:
                        srow[svec_idx[(gr, gs)]] += _SQRT2 * coeff
                        rrow[var_column[(block, r, s)]] += 2 * Fraction(coeff)
        float_rows.append(srow)
        float_rhs.append(polynomial.coefficient(alpha))
        rational_rows.append(rrow)

    # Pin cross-block entries to zero so the big Gram is block diagonal.
    for i in range(len(bases)):
        for j in range(i + 1, len(bases)):
            for a in range(offsets[i], offsets[i + 1]):
                for b in range(offsets[j], offsets[j + 1]):
                    zero_row = [0.0] * svec_dim
                    zero_row[svec_idx[(a, b)]] = 1.0
                    float_rows.append(zero_row)
                    float_rhs.append(0.0)

    proposal = solve_gram_program(
        total, np.array(float_rows), np.array(float_rhs), np.zeros(svec_dim)
    )
    if proposal.status != "solved" or proposal.gram is None:
        return _inconclusive(polynomial, f"SDP proposer: {proposal.detail}")

    gram = proposal.gram
    target = [Fraction(polynomial.coefficient(alpha)) for alpha in alpha_list]
    for denominator in denominators:
        rounded: list[Fraction] = []
        for block, basis in enumerate(bases):
            for r in range(len(basis)):
                for s in range(r, len(basis)):
                    rounded.append(_frac(gram[offsets[block] + r][offsets[block] + s], denominator))
        exact = project_coefficients_exact(rounded, rational_rows, target)
        if exact is None:
            continue

        blocks: list[tuple[tuple[Exponent, ...], list[list[Fraction]], tuple[Interval, ...]]] = []
        pivots_all: list[Interval] = []
        ok = True
        for block, basis in enumerate(bases):
            size = len(basis)
            block_gram = [[Fraction(0)] * size for _ in range(size)]
            for r in range(size):
                for s in range(r, size):
                    block_gram[r][s] = block_gram[s][r] = exact[var_column[(block, r, s)]]
            pivots = interval_ldlt_pivots(block_gram)
            if pivots is None or not all(p.lo > 0.0 for p in pivots):
                ok = False
                break
            blocks.append((basis, block_gram, pivots))
            pivots_all.extend(pivots)
        if not ok:
            continue

        multipliers = tuple(
            SOSMultiplier(
                constraint_index=block - 1,
                basis=tuple(basis),
                gram=tuple(tuple(str(entry) for entry in row) for row in block_gram),
            )
            for block, (basis, block_gram, _piv) in enumerate(blocks)
        )
        margin = min(p.lo for p in pivots_all)
        return PositivstellensatzCertificate(
            status="proved",
            n_vars=n,
            multipliers=multipliers,
            pivots=tuple((p.lo, p.hi) for p in pivots_all),
            pd_margin=margin,
            detail=(
                f"Putinar proof: {len(multipliers)} certified-SOS multipliers "
                f"(denominator {denominator}), all Gram blocks PD (margin {margin:.3e})"
            ),
        )

    return _inconclusive(
        polynomial,
        "rational rounding could not certify all multiplier Gram blocks PD at the tried "
        "denominators (try a larger half_degree, or the statement may be false)",
    )

Other public import paths

omnibias.sos.certify_nonneg_on_set
omnibias.sos.positivstellensatz.certify_nonneg_on_set

FUNCTION

is_nonneg_on_set

omnibias.sos.is_nonneg_on_setSource ↗

is_nonneg_on_set(polynomial: Polynomial, constraints: Sequence[Polynomial], *, half_degree: int | None=None) -> bool

True iff certify_nonneg_on_set returns a sound proof.

Parameters

Name	Type & default	Contract
`polynomial`positional-or-keyword	`Polynomial`Required	See the operation contract and implementation below.
`constraints`positional-or-keyword	`Sequence[Polynomial]`Required	See the operation contract and implementation below.
`half_degree`keyword-only	`int \| None`Default: None	See the operation contract and implementation below.

Returnsbool

Executed regression · interval constraint is proved and exact

Full file, imports & fixtures ↗

def test_interval_constraint_is_proved_and_exact() -> None:
    p = 2.0 * ONE1 - X1 * X1
    gs = [ONE1 - X1 * X1]  # [-1, 1]
    cert = certify_nonneg_on_set(p, gs)
    assert cert.certified
    assert _identity_holds(cert, p, gs)
    assert _min_in_set(p, gs) >= -1e-9
    assert is_nonneg_on_set(p, gs)

python -m pytest "packages/omnibias-sos/tests/test_positivstellensatz.py::test_interval_constraint_is_proved_and_exact" -q

Read the implementation

def is_nonneg_on_set(
    polynomial: Polynomial, constraints: Sequence[Polynomial], *, half_degree: int | None = None
) -> bool:
    """``True`` iff :func:`certify_nonneg_on_set` returns a sound proof."""
    return certify_nonneg_on_set(polynomial, constraints, half_degree=half_degree).certified

Other public import paths

omnibias.sos.is_nonneg_on_set
omnibias.sos.positivstellensatz.is_nonneg_on_set

FUNCTION

seal_positivstellensatz_certificate

omnibias.sos.seal_positivstellensatz_certificateSource ↗

seal_positivstellensatz_certificate(certificate: PositivstellensatzCertificate, *, claim: str, scope: SOSScope | None=None) -> Cert

Seal a proved Putinar certificate into a v1 positive_definite certificate.

The block-diagonal Gram's pivots are exactly the concatenation of the per-block pivots, so one allPivotsPos obligation certifies every multiplier PD at once.

Parameters

Name	Type & default	Contract
`certificate`positional-or-keyword	`PositivstellensatzCertificate`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.

ReturnsCert

Explicit validation & failure cases

When not certificate.certified, raises ValueError('cannot seal an inconclusive Positivstellensatz certificate').

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

Executed regression · sos bound is sealed

Full file, imports & fixtures ↗

def test_sos_bound_is_sealed(make_toy) -> None:  # type: ignore[no-untyped-def]
    pytest.importorskip("omnibias.sos")
    prob = make_toy([[1.0, -1.0], [-1.0, 1.0]])  # E = (x0 - x1)^2
    assignment, _ = decode(prob)
    cert = certify_gap(prob, assignment, level=1, bisection_steps=24)
    assert cert.method == "sos"
    assert cert.certified is True and cert.sealed is not None and cert.level == 1

python -m pytest "packages/omnibias-discrete/tests/test_certify.py::test_sos_bound_is_sealed" -q

Regression example · seal makes no unproven claim and is valid

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_seal_makes_no_unproven_claim_and_is_valid() -> None:
    p = 2.0 * ONE2 - X * X - Y * Y
    gs = [ONE2 - X * X - Y * Y]
    cert = certify_nonneg_on_set(p, gs)
    sealed = seal_positivstellensatz_certificate(
        cert, claim="2 - x^2 - y^2 >= 0 on the closed unit disk"
    )
    assert schema_errors_v1(sealed) == []
    assert verify_certificate_digest(sealed)
    assert sealed["honesty"]["unproven_claim"] is False
    assert sealed["meta"]["sos"]["form"] == "positivstellensatz"
    assert sealed["payload"]["type"] == "positive_definite"

python -m pytest packages/omnibias-sos/tests/test_positivstellensatz.py -k test_seal_makes_no_unproven_claim_and_is_valid -q

Read the implementation

def seal_positivstellensatz_certificate(
    certificate: PositivstellensatzCertificate,
    *,
    claim: str,
    scope: SOSScope | None = None,
) -> Cert:
    """Seal a proved Putinar certificate into a v1 ``positive_definite`` certificate.

    The block-diagonal Gram's pivots are exactly the concatenation of the per-block
    pivots, so one ``allPivotsPos`` obligation certifies every multiplier PD at once.
    """
    if not certificate.certified:
        raise ValueError("cannot seal an inconclusive Positivstellensatz certificate")
    if scope is None:
        scope = SOSScope(GLOBAL_POLYNOMIAL)
    pivots = [Interval(lo, hi) for lo, hi in certificate.pivots]

    # The certified interval LDL^T pivots concatenate the per-multiplier block pivots,
    # so the block-diagonal Gram (multiplier order) factorises to exactly those pivots.
    # Storing it lets an independent replay re-derive the PD fact from the exact matrix.
    total = sum(len(mult.basis) for mult in certificate.multipliers)
    block_diag = [["0"] * total for _ in range(total)]
    offset = 0
    for mult in certificate.multipliers:
        size = len(mult.basis)
        for i in range(size):
            for j in range(size):
                block_diag[offset + i][offset + j] = mult.gram[i][j]
        offset += size

    meta = {
        "generator": "omnibias-sos",
        "sos": {
            "form": "positivstellensatz",
            "scope": scope.kind,
            "truncation_order": scope.truncation_order,
            "system": scope.system,
            "n_vars": certificate.n_vars,
            "num_multipliers": len(certificate.multipliers),
            "pd_margin": certificate.pd_margin,
            "gram": [list(row) for row in block_diag],
        },
    }
    return positive_definite_certificate(claim, pivots, honesty=honesty_labels(scope), meta=meta)

Other public import paths

omnibias.sos.seal_positivstellensatz_certificate
omnibias.sos.positivstellensatz.seal_positivstellensatz_certificate

← Package overview Runnable learning examples →

omnibias.sos.positivstellensatz

PositivstellensatzCertificate​

Parameters

Fields & methods

SOSMultiplier​

Parameters

Fields & methods

certify_nonneg_on_set​

Parameters

is_nonneg_on_set​

Parameters

seal_positivstellensatz_certificate​

Parameters

PositivstellensatzCertificate

SOSMultiplier

certify_nonneg_on_set

is_nonneg_on_set

seal_positivstellensatz_certificate