omnibias.sos.certify

0.1.0a2AlphaPython >=3.10AGPL / commercial

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

import omnibias.sos.certify

Module contract & mathematical conventions

The sound part: rigorously certify a polynomial is a sum of squares.

certify_sos runs the full propose-then-prove pipeline:

1. propose a floating-point PD Gram Q with the SDP (omnibias.sos.solve); 2. round + exactly project it onto z^T Q z = p over the rationals (omnibias.sos.rounding); 3. **prove** the rational Gram is positive definite with the repo's rigorous interval LDL^T (omnibias.core.verified.eig_operator.interval_ldlt_pivots): every pivot's lower endpoint > 0 certifies Q PD, hence p(x) = z(x)^T Q z(x) >= 0 for **all** x.

Soundness over completeness: if the SDP is infeasible, the rational projection is not exact, or no tried denominator yields a certified-PD Gram, the result is status == "inconclusive" -- never a false positivity claim. (Because the proof requires a *strictly* PD Gram, a polynomial that is SOS only with a rank-deficient / boundary Gram -- e.g. one vanishing somewhere, like x^2 + y^2 -- is reported inconclusive rather than proved; this preserves soundness.)

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

DEFAULT_DENOMINATORS

omnibias.sos.DEFAULT_DENOMINATORSSource ↗

DEFAULT_DENOMINATORS: tuple[int, ...] = (2 ** 8, 2 ** 10, 2 ** 13, 2 ** 16, 2 ** 20, 2 ** 26, 2 ** 32, 2 ** 40)

Denominators tried (ascending precision) when rationalising the float Gram.

Read the implementation

DEFAULT_DENOMINATORS: tuple[int, ...] = (
    2**8,
    2**10,
    2**13,
    2**16,
    2**20,
    2**26,
    2**32,
    2**40,
)

Other public import paths

omnibias.sos.DEFAULT_DENOMINATORS
omnibias.sos.certify.DEFAULT_DENOMINATORS

FUNCTION

certify_sos

omnibias.sos.certify_sosSource ↗

certify_sos(polynomial: Polynomial, *, half_degree: int | None=None, denominators: Sequence[int]=DEFAULT_DENOMINATORS, external: GramProposer | None=None, basis: Sequence[Exponent] | MonomialBasis | None=None) -> SOSCertificate

Rigorously certify polynomial(x) >= 0 for all x via an SOS proof.

Parameters

polynomial: The polynomial to certify nonnegative. half_degree: Half the SOS degree (the monomial basis is taken up to this degree); defaults to ceil(deg(p) / 2). denominators: Rational-rounding denominators tried in order until one yields a certified-PD Gram. external: Optional external SDP backend forwarded to omnibias.sos.solve.solve_sos_gram (advisory; never trusted for the proof). basis: Optional monomial vector. When omitted, the total-degree basis up to half_degree (or ceil(deg(p)/2)) is used.

Returns

SOSCertificate status == "proved" is a sound universal-positivity proof carrying the exact rational Gram and its certified interval LDL^T pivots; status == "inconclusive" makes no claim.

Parameters

Name	Type & default	Contract
`polynomial`positional-or-keyword	`Polynomial`Required	The polynomial to certify nonnegative.
`half_degree`keyword-only	`int \| None`Default: None	Half the SOS degree (the monomial basis is taken up to this degree); defaults to `ceil(deg(p) / 2)`.
`denominators`keyword-only	`Sequence[int]`Default: DEFAULT_DENOMINATORS	Rational-rounding denominators tried in order until one yields a certified-PD Gram.
`external`keyword-only	`GramProposer \| None`Default: None	Optional external SDP backend forwarded to `omnibias.sos.solve.solve_sos_gram` (advisory; never trusted for the proof).
`basis`keyword-only	`Sequence[Exponent] \| MonomialBasis \| None`Default: None	Optional monomial vector. When omitted, the total-degree basis up to `half_degree` (or `ceil(deg(p)/2)`) is used.

ReturnsSOSCertificate

Executed regression · is sos helper agrees

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_is_sos_helper_agrees() -> None:
    assert is_sos(X * X - X * Y + Y * Y + ONE)
    assert not is_sos(Polynomial(2, {(4, 2): 1.0, (2, 4): 1.0, (2, 2): -3.0, (0, 0): 1.0}))

python -m pytest "packages/omnibias-sos/tests/test_certify.py::test_is_sos_helper_agrees" -q

Regression example · negative polynomial is inconclusive

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_negative_polynomial_is_inconclusive() -> None:
    cert = certify_sos(-ONE - X * X)  # <= -1 everywhere
    assert cert.status == "inconclusive"
    assert not cert.certified

python -m pytest packages/omnibias-sos/tests/test_certify.py -k test_negative_polynomial_is_inconclusive -q

Read the implementation

def certify_sos(
    polynomial: Polynomial,
    *,
    half_degree: int | None = None,
    denominators: Sequence[int] = DEFAULT_DENOMINATORS,
    external: GramProposer | None = None,
    basis: Sequence[Exponent] | MonomialBasis | None = None,
) -> SOSCertificate:
    r"""Rigorously certify ``polynomial(x) >= 0`` for all ``x`` via an SOS proof.

    Parameters
    ----------
    polynomial:
        The polynomial to certify nonnegative.
    half_degree:
        Half the SOS degree (the monomial basis is taken up to this degree);
        defaults to ``ceil(deg(p) / 2)``.
    denominators:
        Rational-rounding denominators tried in order until one yields a
        certified-PD Gram.
    external:
        Optional external SDP backend forwarded to
        :func:`omnibias.sos.solve.solve_sos_gram` (advisory; never trusted for the
        proof).
    basis:
        Optional monomial vector. When omitted, the total-degree basis up
        to ``half_degree`` (or ``ceil(deg(p)/2)``) is used.

    Returns
    -------
    SOSCertificate
        ``status == "proved"`` is a sound universal-positivity proof carrying the
        exact rational Gram and its certified interval ``LDL^T`` pivots;
        ``status == "inconclusive"`` makes no claim.
    """
    return _run_certification(
        polynomial, polynomial,
        half_degree=half_degree, denominators=denominators, external=external,
        basis=basis,
    )

Other public import paths

omnibias.sos.certify_sos
omnibias.sos.certify.certify_sos

FUNCTION

certify_sos_rational

omnibias.sos.certify_sos_rationalSource ↗

certify_sos_rational(polynomial: RationalPolynomial, *, half_degree: int | None=None, denominators: Sequence[int]=DEFAULT_DENOMINATORS, external: GramProposer | None=None) -> SOSCertificate

Certify a polynomial with **exact rational** coefficients is a sum of squares.

Identical to certify_sos but the coefficient-matching targets are the exact ~fractions.Fraction coefficients (the SDP still proposes on the float image). This is what the auxiliary-functional method certifies, since its residual C - Phi - grad(V) . f must be represented exactly.

Parameters

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

ReturnsSOSCertificate

Read the implementation

def certify_sos_rational(
    polynomial: RationalPolynomial,
    *,
    half_degree: int | None = None,
    denominators: Sequence[int] = DEFAULT_DENOMINATORS,
    external: GramProposer | None = None,
) -> SOSCertificate:
    r"""Certify a polynomial with **exact rational** coefficients is a sum of squares.

    Identical to :func:`certify_sos` but the coefficient-matching targets are the
    exact :class:`~fractions.Fraction` coefficients (the SDP still proposes on the
    float image).  This is what the auxiliary-functional method certifies, since
    its residual ``C - Phi - grad(V) . f`` must be represented exactly.
    """
    return _run_certification(
        polynomial.to_float(), polynomial,
        half_degree=half_degree, denominators=denominators, external=external,
    )

Other public import paths

omnibias.sos.certify_sos_rational
omnibias.sos.certify.certify_sos_rational

FUNCTION

degree_reduction_report

omnibias.sos.degree_reduction_reportSource ↗

degree_reduction_report(*, max_degree: int=6) -> list[dict[str, object]]

Compare total-degree vs arrangement-adapted certifying degrees (G5).

Parameters

Name	Type & default	Contract
`max_degree`keyword-only	`int`Default: 6	See the operation contract and implementation below.

Returnslist[dict[str, object]]

Executed regression · g5 degree drop on at least half

Full file, imports & fixtures ↗

def test_g5_degree_drop_on_at_least_half() -> None:
    rows = degree_reduction_report()
    assert len(rows) == len(named_adapted_problems())
    wins = sum(1 for r in rows if r["win"])
    assert wins >= (len(rows) + 1) // 2, rows
    # Failures stay in the report.
    assert all("name" in r and "drop" in r for r in rows)

python -m pytest "packages/omnibias-sos/tests/test_adapted_basis.py::test_g5_degree_drop_on_at_least_half" -q

Read the implementation

def degree_reduction_report(*, max_degree: int = 6) -> list[dict[str, object]]:
    """Compare total-degree vs arrangement-adapted certifying degrees (G5)."""
    from omnibias.sos.monomials import arrangement_adapted_basis

    out: list[dict[str, object]] = []
    for spec in named_adapted_problems():
        poly = spec["polynomial"]
        assert isinstance(poly, Polynomial)
        arrangement = spec["arrangement"]
        total = None
        adapted = None
        for deg in range(0, int(max_degree) + 1):
            if total is None and certify_sos(poly, half_degree=deg).certified:
                total = deg
            if adapted is None:
                basis = arrangement_adapted_basis(poly, arrangement, degree=deg)
                if certify_sos(poly, basis=basis).certified:
                    adapted = deg
            if total is not None and adapted is not None:
                break
        drop = None if total is None or adapted is None else int(total) - int(adapted)
        out.append(
            {
                "name": spec["name"],
                "total_degree": total,
                "adapted_degree": adapted,
                "drop": drop,
                "win": drop is not None and drop >= 2,
            }
        )
    return out

Other public import paths

omnibias.sos.degree_reduction_report
omnibias.sos.certify.degree_reduction_report

FUNCTION

is_sos

omnibias.sos.is_sosSource ↗

is_sos(polynomial: Polynomial, *, half_degree: int | None=None) -> bool

True iff certify_sos returns a sound proof of nonnegativity.

Parameters

Name	Type & default	Contract
`polynomial`positional-or-keyword	`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 · is sos helper agrees

Full file, imports & fixtures ↗

def test_is_sos_helper_agrees() -> None:
    assert is_sos(X * X - X * Y + Y * Y + ONE)
    assert not is_sos(Polynomial(2, {(4, 2): 1.0, (2, 4): 1.0, (2, 2): -3.0, (0, 0): 1.0}))

python -m pytest "packages/omnibias-sos/tests/test_certify.py::test_is_sos_helper_agrees" -q

Regression example · indefinite polynomials are never proved

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_indefinite_polynomials_are_never_proved() -> None:
    """A polynomial with a negative direction must never earn a certificate."""
    for seed in range(150):
        rng = np.random.default_rng(seed + 10_000)
        n_vars = int(rng.integers(2, 4))
        poly = _random_indefinite_polynomial(rng, n_vars)
        worst = _min_over_samples(poly, rng, n_vars)
        if worst >= 0.0:
            continue  # the sample failed to expose the negative direction
        assert certify_sos(poly).status != _PROVED, (
            f"seed={seed}: certify_sos proved a polynomial that reaches {worst!r} < 0"
        )
        assert not is_sos(poly)

python -m pytest packages/omnibias-sos/tests/test_psd_soundness_regression.py -k test_indefinite_polynomials_are_never_proved -q

Read the implementation

def is_sos(polynomial: Polynomial, *, half_degree: int | None = None) -> bool:
    """``True`` iff :func:`certify_sos` returns a sound proof of nonnegativity."""
    return certify_sos(polynomial, half_degree=half_degree).certified

Other public import paths

omnibias.sos.is_sos
omnibias.sos.certify.is_sos

FUNCTION

named_adapted_problems

omnibias.sos.named_adapted_problemsSource ↗

named_adapted_problems() -> tuple[dict[str, object], ...]

Named positivity problems for the arrangement-adapted G5 suite.

Returnstuple[dict[str, object], ...]

Executed regression · adapted basis is sparser than total degree

Full file, imports & fixtures ↗

def test_adapted_basis_is_sparser_than_total_degree() -> None:
    spec = named_adapted_problems()[0]
    poly = spec["polynomial"]
    adapted = arrangement_adapted_basis(poly, spec["arrangement"], degree=1)
    assert certify_sos(poly, basis=adapted).certified
    assert not certify_sos(poly, half_degree=1).certified

python -m pytest "packages/omnibias-sos/tests/test_adapted_basis.py::test_adapted_basis_is_sparser_than_total_degree" -q

Regression example · g5 degree drop on at least half

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_g5_degree_drop_on_at_least_half() -> None:
    rows = degree_reduction_report()
    assert len(rows) == len(named_adapted_problems())
    wins = sum(1 for r in rows if r["win"])
    assert wins >= (len(rows) + 1) // 2, rows
    # Failures stay in the report.
    assert all("name" in r and "drop" in r for r in rows)

python -m pytest packages/omnibias-sos/tests/test_adapted_basis.py -k test_g5_degree_drop_on_at_least_half -q

Read the implementation

def named_adapted_problems() -> tuple[dict[str, object], ...]:
    """Named positivity problems for the arrangement-adapted G5 suite."""
    def _pure(n_vars: int, axis: int, power: int, const: float = 1.0) -> Polynomial:
        exp = [0] * n_vars
        exp[axis] = power
        return Polynomial.monomial(tuple(exp), 1.0) + Polynomial.constant(const, n_vars)

    x4 = _pure(2, 0, 4)
    y4 = _pure(2, 1, 4) - Polynomial.constant(1.0, 2)
    x6y2 = _pure(2, 0, 6) + Polynomial.monomial((0, 2), 1.0)
    return (
        {"name": "x6_plus_one", "polynomial": _pure(1, 0, 6), "arrangement": ((1.0,),)},
        {"name": "x8_plus_one", "polynomial": _pure(1, 0, 8), "arrangement": ((1.0,),)},
        {
            "name": "x4_plus_y4_plus_one",
            "polynomial": x4 + y4,
            "arrangement": ((1.0, 0.0), (0.0, 1.0)),
        },
        {"name": "x10_plus_one", "polynomial": _pure(1, 0, 10), "arrangement": ((1.0,),)},
        {"name": "x6_plus_y2_plus_one", "polynomial": x6y2, "arrangement": ((1.0, 0.0),)},
        {
            "name": "x4_plus_2x2_plus_one",
            "polynomial": _pure(1, 0, 4) + Polynomial.monomial((2,), 2.0),
            "arrangement": ((1.0,),),
        },
    )

Other public import paths

omnibias.sos.named_adapted_problems
omnibias.sos.certify.named_adapted_problems

FUNCTION

rational_gram

omnibias.sos.rational_gramSource ↗

rational_gram(certificate: SOSCertificate) -> RationalGram | None

Recover the exact rational Gram matrix from a proved certificate.

Parameters

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

ReturnsRationalGram | None

Executed regression · proved cases are sound

Full file, imports & fixtures ↗

def test_proved_cases_are_sound(name: str, poly: Polynomial) -> None:
    cert = certify_sos(poly)
    assert cert.certified, f"{name}: expected proved, got {cert.status} ({cert.detail})"
    # The rational Gram matches the polynomial coefficients exactly ...
    assert cert.coeff_residual == 0.0
    assert _reconstruction_matches(cert, poly)
    # ... every certified interval LDL^T pivot is strictly positive ...
    assert cert.pivots
    assert all(lo > 0.0 for lo, _hi in cert.pivots)
    assert cert.pd_margin > 0.0
    assert cert.pd_margin == min(lo for lo, _hi in cert.pivots)
    # ... and the polynomial really is nonnegative (independent numeric cross-check).
    assert _sampled_min(poly) >= -1e-9

python -m pytest "packages/omnibias-sos/tests/test_certify.py::test_proved_cases_are_sound[completed-square-shift]" -q

Read the implementation

def rational_gram(certificate: SOSCertificate) -> RationalGram | None:
    """Recover the exact rational Gram matrix from a proved certificate."""
    if certificate.gram is None:
        return None
    return [[Fraction(entry) for entry in row] for row in certificate.gram]

Other public import paths

omnibias.sos.rational_gram
omnibias.sos.certify.rational_gram

← Package overview Runnable learning examples →

omnibias.sos.certify

DEFAULT_DENOMINATORS​

certify_sos​

Parameters

certify_sos_rational​

Parameters

degree_reduction_report​

Parameters

is_sos​

Parameters

named_adapted_problems​

rational_gram​

Parameters

DEFAULT_DENOMINATORS

certify_sos

certify_sos_rational

degree_reduction_report

is_sos

named_adapted_problems

rational_gram