omnibias.core.verified.conditioning

0.5.0rc1Release candidatePython >=3.10Apache-2.0

Coefficient recurrences, activation contracts, jet algebra, and verified arithmetic shared by the numerical backends.

import omnibias.core.verified.conditioning

Module contract & mathematical conventions

Certified conditioning of a symmetric matrix -- the rigorous register of the eps -> 0 rank / regularization collapse.

Tikhonov-regularized solving x_eps = (A + eps I)^{-1} b collapses onto the minimum-norm / Moore-Penrose solution A^+ b as eps -> 0; naively taking eps to zero blows up whenever A is ill-conditioned or rank-deficient. This module certifies the quantities that govern that collapse, all in outward-rounded interval arithmetic on top of omnibias.core.verified.eig_operator:

certified_min_eigenvalue / certified_max_eigenvalue -- rigorous two-sided enclosures of lambda_min(A) / lambda_max(A) (the smallest / largest eigenvalue of the symmetric part of A) by inertia bisection.
certified_condition_number -- an enclosure of kappa(A) = lambda_max / lambda_min (upper endpoint +inf when positive-definiteness cannot be certified -- the honest rank-deficient signal).
certified_damping -- the smallest eps for which kappa(A + eps I) is provably <= target_condition (a certified damping *selection*).
certified_regularization_error -- a sound upper bound on ||x_eps - A^+ b||_2 on range(A) (the regime where the collapse converges), assuming a certified positive smallest eigenvalue.
conditioning_certificate -- a sealed v1 certificate bundling the above, carrying the LDL^T pivots so a positive-definiteness (lambda_min > 0) obligation can be handed to the Lean bridge unchanged.

This is a **rigorous** register: the enclosures are theorem-grade, but the underlying regularized solve is a numerical (LAPACK-class) operation carried out by the differentiable consumers (see omnibias.curvature.regularize). The eps -> 0 limit is a *distinct* collapse from the founding multi-bias delta -> 0 derivative limit and the beta -> inf feasibility penalty -- same spirit, different parameter, never conflated. Nothing here rides the sigma derivative tower; the omnibias value is the collapse framing plus the certificate.

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

FloatMatrix

omnibias.core.verified.conditioning.FloatMatrixSource ↗

FloatMatrix = Sequence[Sequence[float]]

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.

Read the implementation

FloatMatrix = Sequence[Sequence[float]]

CONSTANT

FloatVector

omnibias.core.verified.conditioning.FloatVectorSource ↗

FloatVector = Sequence[float]

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.

Read the implementation

FloatVector = Sequence[float]

FUNCTION

certified_condition_number

omnibias.core.verified.certified_condition_numberSource ↗

certified_condition_number(matrix: FloatMatrix) -> Interval

Enclosure of the spectral condition number kappa(A) = lambda_max / lambda_min.

When lambda_min cannot be certified positive (rank-deficient / indefinite A), the upper endpoint is +inf -- the honest statement that the condition number is not bounded above by this certificate.

Parameters

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

ReturnsInterval

Executed regression · condition number is infinite when rank deficient

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_condition_number_is_infinite_when_rank_deficient() -> None:
    rng = random.Random(7)
    for _ in range(10):
        n = rng.randint(3, 5)
        a = _rand_low_rank(rng, n, n - 1)
        k = certified_condition_number(a)
        assert k.hi == math.inf
        assert k.lo >= 1.0

python -m pytest "packages/omnibias-core/tests/verified/test_conditioning.py::test_condition_number_is_infinite_when_rank_deficient" -q

Regression example · condition number encloses grid and random

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_condition_number_encloses_grid_and_random() -> None:
    for a in _GRID:
        k = certified_condition_number(a)
        true_k = _true_cond(a)
        assert k.lo <= true_k <= k.hi
    rng = random.Random(11)
    for _ in range(15):
        a = _rand_spd(rng, rng.randint(2, 5))
        k = certified_condition_number(a)
        assert k.lo <= _true_cond(a) <= k.hi

python -m pytest packages/omnibias-core/tests/verified/test_conditioning.py -k test_condition_number_encloses_grid_and_random -q

Read the implementation

def certified_condition_number(matrix: FloatMatrix) -> Interval:
    r"""Enclosure of the spectral condition number ``kappa(A) = lambda_max / lambda_min``.

    When ``lambda_min`` cannot be certified positive (rank-deficient / indefinite
    ``A``), the upper endpoint is ``+inf`` -- the honest statement that the
    condition number is not bounded above by this certificate.
    """
    a = _symmetrize(matrix)
    n = len(a)
    lam_min = generalized_eigenvalue_enclosure(a, identity_matrix(n), 1)
    lam_max = generalized_eigenvalue_enclosure(a, identity_matrix(n), n)
    return _condition_from(lam_min, lam_max)

Other public import paths

omnibias.core.verified.certified_condition_number
omnibias.core.verified.conditioning.certified_condition_number

FUNCTION

certified_damping

omnibias.core.verified.certified_dampingSource ↗

certified_damping(matrix: FloatMatrix, *, target_condition: float) -> float

Smallest eps >= 0 provably giving kappa(A + eps I) <= target_condition.

kappa(A + eps I) = (lambda_max + eps)/(lambda_min + eps) is decreasing in eps, so the sound threshold eps* = max(0, (lambda_max.hi - T * lambda_min.lo)/(T - 1)) -- built from the *upper* enclosure of lambda_max and the *lower* enclosure of lambda_min -- guarantees the target for the true matrix (a larger eps only lowers kappa, so the outward-rounded value is sufficient). Works for indefinite A too: the same eps lifts lambda_min + eps strictly positive.

Parameters

Name	Type & default	Contract
`matrix`positional-or-keyword	`FloatMatrix`Required	See the operation contract and implementation below.
`target_condition`keyword-only	`float`Required	See the operation contract and implementation below.

Returnsfloat

Explicit validation & failure cases

When t <= 1.0, raises ValueError('target_condition must be > 1').

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

Executed regression · certified damping zero when already conditioned

Full file, imports & fixtures ↗

def test_certified_damping_zero_when_already_conditioned() -> None:
    a = [[2.0, 0.0], [0.0, 3.0]]  # kappa = 1.5
    assert certified_damping(a, target_condition=10.0) == 0.0

python -m pytest "packages/omnibias-core/tests/verified/test_conditioning.py::test_certified_damping_zero_when_already_conditioned" -q

Regression example · certified damping rejects target le one

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_certified_damping_rejects_target_le_one() -> None:
    with pytest.raises(ValueError, match="target_condition"):
        certified_damping([[1.0, 0.0], [0.0, 1.0]], target_condition=1.0)

python -m pytest packages/omnibias-core/tests/verified/test_conditioning.py -k test_certified_damping_rejects_target_le_one -q

Read the implementation

def certified_damping(matrix: FloatMatrix, *, target_condition: float) -> float:
    r"""Smallest ``eps >= 0`` provably giving ``kappa(A + eps I) <= target_condition``.

    ``kappa(A + eps I) = (lambda_max + eps)/(lambda_min + eps)`` is decreasing in
    ``eps``, so the sound threshold ``eps* = max(0, (lambda_max.hi -
    T * lambda_min.lo)/(T - 1))`` -- built from the *upper* enclosure of
    ``lambda_max`` and the *lower* enclosure of ``lambda_min`` -- guarantees the
    target for the true matrix (a larger ``eps`` only lowers ``kappa``, so the
    outward-rounded value is sufficient). Works for indefinite ``A`` too: the same
    ``eps`` lifts ``lambda_min + eps`` strictly positive.
    """
    t = float(target_condition)
    if t <= 1.0:
        raise ValueError("target_condition must be > 1")
    a = _symmetrize(matrix)
    n = len(a)
    lam_min = generalized_eigenvalue_enclosure(a, identity_matrix(n), 1)
    lam_max = generalized_eigenvalue_enclosure(a, identity_matrix(n), n)
    num = Interval.point(lam_max.hi) - Interval.point(t) * Interval.point(lam_min.lo)
    den = Interval.point(t - 1.0)  # exact-point positive denominator
    eps = (num * den.reciprocal()).hi
    return max(0.0, eps)

Other public import paths

omnibias.core.verified.certified_damping
omnibias.core.verified.conditioning.certified_damping

FUNCTION

certified_max_eigenvalue

omnibias.core.verified.certified_max_eigenvalueSource ↗

certified_max_eigenvalue(matrix: FloatMatrix) -> Interval

Rigorous enclosure of the largest eigenvalue of the symmetric part of matrix.

Parameters

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

ReturnsInterval

Executed regression · extreme eigenvalues enclose random

Full file, imports & fixtures ↗

def test_extreme_eigenvalues_enclose_random() -> None:
    rng = random.Random(20260729)
    for _ in range(20):
        n = rng.randint(2, 5)
        a = _rand_spd(rng, n)
        ev = _eigvals_sym(a)
        assert certified_min_eigenvalue(a).lo <= ev[0]
        assert certified_min_eigenvalue(a).hi >= ev[0]
        assert certified_max_eigenvalue(a).lo <= ev[-1] <= certified_max_eigenvalue(a).hi

python -m pytest "packages/omnibias-core/tests/verified/test_conditioning.py::test_extreme_eigenvalues_enclose_random" -q

Regression example · extreme eigenvalues enclose grid

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_extreme_eigenvalues_enclose_grid() -> None:
    for a in _GRID:
        ev = _eigvals_sym(a)
        lo = certified_min_eigenvalue(a)
        hi = certified_max_eigenvalue(a)
        assert lo.lo <= ev[0] <= lo.hi
        assert hi.lo <= ev[-1] <= hi.hi
        # tight relative to the spectrum
        assert lo.width <= 1e-6 * max(1.0, abs(ev[0]))
        assert hi.width <= 1e-6 * max(1.0, abs(ev[-1]))

python -m pytest packages/omnibias-core/tests/verified/test_conditioning.py -k test_extreme_eigenvalues_enclose_grid -q

Read the implementation

def certified_max_eigenvalue(matrix: FloatMatrix) -> Interval:
    r"""Rigorous enclosure of the largest eigenvalue of the symmetric part of ``matrix``."""
    a = _symmetrize(matrix)
    n = len(a)
    return generalized_eigenvalue_enclosure(a, identity_matrix(n), n)

Other public import paths

omnibias.core.verified.certified_max_eigenvalue
omnibias.core.verified.conditioning.certified_max_eigenvalue

FUNCTION

certified_min_eigenvalue

omnibias.core.verified.certified_min_eigenvalueSource ↗

certified_min_eigenvalue(matrix: FloatMatrix) -> Interval

Rigorous enclosure of the smallest eigenvalue of the symmetric part of matrix.

Wraps ~omnibias.core.verified.eig_operator.generalized_eigenvalue_enclosure on the pencil (A, I) at index 1. The .lo endpoint is a certified lower bound on lambda_min; it is <= 0 exactly when positive-definiteness cannot be certified (a rank-deficient / indefinite signal).

Parameters

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

ReturnsInterval

Executed regression · regularization error requires positive eigenvalue

Full file, imports & fixtures ↗

def test_regularization_error_requires_positive_eigenvalue() -> None:
    a = _rand_low_rank(random.Random(5), 4, 3)  # singular
    with pytest.raises(ValueError, match="smallest"):
        certified_regularization_error(a, [1.0, 1.0, 1.0, 1.0], 1e-2)

python -m pytest "packages/omnibias-core/tests/verified/test_conditioning.py::test_regularization_error_requires_positive_eigenvalue" -q

Regression example · extreme eigenvalues enclose random

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_extreme_eigenvalues_enclose_random() -> None:
    rng = random.Random(20260729)
    for _ in range(20):
        n = rng.randint(2, 5)
        a = _rand_spd(rng, n)
        ev = _eigvals_sym(a)
        assert certified_min_eigenvalue(a).lo <= ev[0]
        assert certified_min_eigenvalue(a).hi >= ev[0]
        assert certified_max_eigenvalue(a).lo <= ev[-1] <= certified_max_eigenvalue(a).hi

python -m pytest packages/omnibias-core/tests/verified/test_conditioning.py -k test_extreme_eigenvalues_enclose_random -q

Read the implementation

def certified_min_eigenvalue(matrix: FloatMatrix) -> Interval:
    r"""Rigorous enclosure of the smallest eigenvalue of the symmetric part of ``matrix``.

    Wraps :func:`~omnibias.core.verified.eig_operator.generalized_eigenvalue_enclosure`
    on the pencil ``(A, I)`` at index ``1``. The ``.lo`` endpoint is a certified
    lower bound on ``lambda_min``; it is ``<= 0`` exactly when positive-definiteness
    cannot be certified (a rank-deficient / indefinite signal).
    """
    a = _symmetrize(matrix)
    return generalized_eigenvalue_enclosure(a, identity_matrix(len(a)), 1)

Other public import paths

omnibias.core.verified.certified_min_eigenvalue
omnibias.core.verified.conditioning.certified_min_eigenvalue

FUNCTION

certified_regularization_error

omnibias.core.verified.certified_regularization_errorSource ↗

certified_regularization_error(matrix: FloatMatrix, rhs: FloatVector, eps: float, *, min_eig: float | None=None) -> Interval

Sound upper bound on ||(A + eps I)^{-1} b - A^+ b||_2 on range(A).

On the range of a symmetric A the Tikhonov error is x_eps - x0 = -eps (A + eps I)^{-1} x0 with x0 = A^+ b, so

The returned interval is [0, bound] with bound built from the certified lower bound lambda_min.lo (the value that maximises -- hence soundly bounds -- the error) and an outward enclosure of ||b||_2.

Scope (range_consistent): this bounds the error only for the component of b in range(A). If b has a null-space component the naive Tikhonov solve carries a (1/eps) b_null term that **diverges** as eps -> 0 -- exactly the blow-up the collapse must avoid -- and is *not* covered here. For a rank-deficient A pass min_eig = a certified lower bound on the smallest **nonzero** eigenvalue (and drive the null space out with omnibias.curvature.regularize.min_norm_solve).

Parameters

Name	Type & default	Contract
`matrix`positional-or-keyword	`FloatMatrix`Required	See the operation contract and implementation below.
`rhs`positional-or-keyword	`FloatVector`Required	See the operation contract and implementation below.
`eps`positional-or-keyword	`float`Required	See the operation contract and implementation below.
`min_eig`keyword-only	`float \| None`Default: None	See the operation contract and implementation below.

ReturnsInterval

Explicit validation & failure cases

When e < 0.0, raises ValueError('eps must be >= 0').
When lam_lo <= 0.0, raises ValueError('certified_regularization_error needs a positive certified smallest eigenvalue; for rank-deficient A pass min_eig = a certified lower bound on the smallest nonzero eigenvalue (range-consistent scope)').

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

Executed regression · regularization error requires positive eigenvalue

Full file, imports & fixtures ↗

def test_regularization_error_requires_positive_eigenvalue() -> None:
    a = _rand_low_rank(random.Random(5), 4, 3)  # singular
    with pytest.raises(ValueError, match="smallest"):
        certified_regularization_error(a, [1.0, 1.0, 1.0, 1.0], 1e-2)

python -m pytest "packages/omnibias-core/tests/verified/test_conditioning.py::test_regularization_error_requires_positive_eigenvalue" -q

Regression example · regularization error sound spd random

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_regularization_error_sound_spd_random() -> None:
    rng = random.Random(31415)
    for _ in range(20):
        n = rng.randint(2, 5)
        a = _rand_spd(rng, n)
        b = [rng.uniform(-2.0, 2.0) for _ in range(n)]
        for eps in (1e-1, 1e-2, 1e-4):
            bound = certified_regularization_error(a, b, eps)
            xe = _solve(_add_diag(a, eps), b)
            x0 = _solve(a, b)  # full rank: min-norm == exact solve
            true_err = _l2([xe[i] - x0[i] for i in range(n)])
            assert bound.lo == 0.0
            assert bound.hi >= true_err - 1e-15

python -m pytest packages/omnibias-core/tests/verified/test_conditioning.py -k test_regularization_error_sound_spd_random -q

Read the implementation

def certified_regularization_error(
    matrix: FloatMatrix, rhs: FloatVector, eps: float, *, min_eig: float | None = None
) -> Interval:
    r"""Sound upper bound on ``||(A + eps I)^{-1} b - A^+ b||_2`` on ``range(A)``.

    On the range of a symmetric ``A`` the Tikhonov error is
    ``x_eps - x0 = -eps (A + eps I)^{-1} x0`` with ``x0 = A^+ b``, so

    .. math:: \|x_\eps - x_0\| \le \frac{\eps}{\lambda_{\min}+\eps}\,\frac{\|b\|}{\lambda_{\min}}.

    The returned interval is ``[0, bound]`` with ``bound`` built from the certified
    lower bound ``lambda_min.lo`` (the value that maximises -- hence soundly
    bounds -- the error) and an outward enclosure of ``||b||_2``.

    Scope (``range_consistent``): this bounds the error only for the component of
    ``b`` in ``range(A)``. If ``b`` has a null-space component the naive Tikhonov
    solve carries a ``(1/eps) b_null`` term that **diverges** as ``eps -> 0`` --
    exactly the blow-up the collapse must avoid -- and is *not* covered here. For a
    rank-deficient ``A`` pass ``min_eig`` = a certified lower bound on the smallest
    **nonzero** eigenvalue (and drive the null space out with
    :func:`omnibias.curvature.regularize.min_norm_solve`).
    """
    e = float(eps)
    if e < 0.0:
        raise ValueError("eps must be >= 0")
    if min_eig is None:
        lam_lo = certified_min_eigenvalue(matrix).lo
    else:
        lam_lo = float(min_eig)
    if lam_lo <= 0.0:
        raise ValueError(
            "certified_regularization_error needs a positive certified smallest "
            "eigenvalue; for rank-deficient A pass min_eig = a certified lower bound "
            "on the smallest nonzero eigenvalue (range-consistent scope)"
        )
    lam_iv = Interval.point(lam_lo)
    eps_iv = Interval.point(e)
    factor = eps_iv * (lam_iv + eps_iv).reciprocal()  # eps / (lambda_min + eps) <= 1
    bound = factor * (_l2_norm_enclosure(rhs) * lam_iv.reciprocal())
    return Interval(0.0, bound.hi)

Other public import paths

omnibias.core.verified.certified_regularization_error
omnibias.core.verified.conditioning.certified_regularization_error

FUNCTION

conditioning_certificate

omnibias.core.verified.conditioning_certificateSource ↗

conditioning_certificate(matrix: FloatMatrix, *, target_condition: float | None=None, eps: float | None=None) -> dict[str, Any]

A sealed v1 certificate bundling the certified conditioning of matrix.

Carries the lambda_min / lambda_max / kappa enclosures and, when the symmetric part is certified positive definite, its interval LDL^T pivots -- the exact payload the Lean bridge turns into the allPivotsPos (lambda_min > 0) obligation. When target_condition is given the certified damping is recorded; when eps is given (and the matrix is PD) the regularization-error bound is attached. theorem_prover_verified is *not* set here -- it is earned only by passing the sealed certificate through the proof machine with a Lean toolchain present.

Parameters

Name	Type & default	Contract
`matrix`positional-or-keyword	`FloatMatrix`Required	See the operation contract and implementation below.
`target_condition`keyword-only	`float \| None`Default: None	See the operation contract and implementation below.
`eps`keyword-only	`float \| None`Default: None	See the operation contract and implementation below.

Returnsdict[str, Any]

Executed regression · certificate is tamper evident

Full file, imports & fixtures ↗

def test_certificate_is_tamper_evident() -> None:
    cert = conditioning_certificate(_GRID[4])
    cert["payload"]["positive_definite"] = False  # flip a claim
    assert not verify_certificate_digest(cert)

python -m pytest "packages/omnibias-core/tests/verified/test_conditioning.py::test_certificate_is_tamper_evident" -q

Regression example · conditioning certificate rank deficient is 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_conditioning_certificate_rank_deficient_is_honest() -> None:
    a = _rand_low_rank(random.Random(3), 4, 3)
    cert = conditioning_certificate(a)
    assert schema_errors_v1(cert) == []
    assert cert["payload"]["positive_definite"] is False
    assert decode_interval(cert["payload"]["condition_number"]).hi == math.inf

python -m pytest packages/omnibias-core/tests/verified/test_conditioning.py -k test_conditioning_certificate_rank_deficient_is_honest -q

Read the implementation

def conditioning_certificate(
    matrix: FloatMatrix, *, target_condition: float | None = None, eps: float | None = None
) -> dict[str, Any]:
    r"""A sealed v1 certificate bundling the certified conditioning of ``matrix``.

    Carries the ``lambda_min`` / ``lambda_max`` / ``kappa`` enclosures and, when
    the symmetric part is certified positive definite, its interval ``LDL^T``
    pivots -- the exact payload the Lean bridge turns into the ``allPivotsPos``
    (``lambda_min > 0``) obligation. When ``target_condition`` is given the
    certified damping is recorded; when ``eps`` is given (and the matrix is PD) the
    regularization-error bound is attached. ``theorem_prover_verified`` is *not*
    set here -- it is earned only by passing the sealed certificate through the
    proof machine with a Lean toolchain present.
    """
    from omnibias.core.proof.certificate import encode_interval, make_certificate

    a = _symmetrize(matrix)
    n = len(a)
    lam_min = generalized_eigenvalue_enclosure(a, identity_matrix(n), 1)
    lam_max = generalized_eigenvalue_enclosure(a, identity_matrix(n), n)
    kappa = _condition_from(lam_min, lam_max)
    pivots = interval_ldlt_pivots(a)
    is_pd = pivots is not None and all(p.lo > 0.0 for p in pivots)

    payload: dict[str, Any] = {
        "type": "conditioning",
        "n": n,
        "lambda_min": encode_interval(lam_min),
        "lambda_max": encode_interval(lam_max),
        "condition_number": encode_interval(kappa),
        "positive_definite": is_pd,
    }
    if pivots is not None:
        payload["pivots"] = [encode_interval(p) for p in pivots]
    if target_condition is not None:
        payload["target_condition"] = float(target_condition)
        payload["certified_damping"] = certified_damping(a, target_condition=target_condition)
    if eps is not None:
        payload["eps"] = float(eps)
        if is_pd:
            # The error bound scales linearly in ||b||, so expose the certified
            # per-unit-||b|| factor eps / ((lambda_min + eps) * lambda_min).
            eps_iv = Interval.point(float(eps))
            unit_factor = eps_iv * (lam_min + eps_iv).reciprocal() * lam_min.reciprocal()
            payload["regularization_error_per_unit_rhs_norm"] = encode_interval(
                Interval(0.0, unit_factor.hi)
            )

    meta = {"scope": "symmetric_part", "collapse_axis": "eps->0"}
    honesty = {"unproven_claim": False}
    return make_certificate(
        claim=f"conditioning enclosure of a {n}x{n} symmetric matrix (eps->0 collapse)",
        payload=payload,
        honesty=honesty,
        meta=meta,
    )

Other public import paths

omnibias.core.verified.conditioning_certificate
omnibias.core.verified.conditioning.conditioning_certificate

FUNCTION

positive_definite_pivots_certificate

omnibias.core.verified.positive_definite_pivots_certificateSource ↗

positive_definite_pivots_certificate(matrix: FloatMatrix, *, claim: str | None=None) -> dict[str, Any]

A sealed positive-definiteness certificate (lambda_min > 0) for matrix.

Convenience wrapper that seals the interval LDL^T pivots of the symmetric part as a scalar lambda_min lower-bound interval certificate -- the Lean-dischargeable lambda_min >= c > 0 obligation. Raises ValueError when positive-definiteness cannot be certified.

Parameters

Name	Type & default	Contract
`matrix`positional-or-keyword	`FloatMatrix`Required	See the operation contract and implementation below.
`claim`keyword-only	`str \| None`Default: None	See the operation contract and implementation below.

Returnsdict[str, Any]

Explicit validation & failure cases

When lam_min.lo <= 0.0, raises ValueError('matrix is not certified positive definite (lambda_min.lo <= 0)').

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

Executed regression · positive definite pivots certificate

Full file, imports & fixtures ↗

def test_positive_definite_pivots_certificate() -> None:
    pd = positive_definite_pivots_certificate(_GRID[2])
    assert schema_errors_v1(pd) == []
    assert verify_certificate_digest(pd)
    with pytest.raises(ValueError, match="positive definite"):
        positive_definite_pivots_certificate(_rand_low_rank(random.Random(1), 4, 3))

python -m pytest "packages/omnibias-core/tests/verified/test_conditioning.py::test_positive_definite_pivots_certificate" -q

Read the implementation

def positive_definite_pivots_certificate(
    matrix: FloatMatrix, *, claim: str | None = None
) -> dict[str, Any]:
    r"""A sealed positive-definiteness certificate (``lambda_min > 0``) for ``matrix``.

    Convenience wrapper that seals the interval ``LDL^T`` pivots of the symmetric
    part as a scalar ``lambda_min`` lower-bound interval certificate -- the
    Lean-dischargeable ``lambda_min >= c > 0`` obligation. Raises ``ValueError``
    when positive-definiteness cannot be certified.
    """
    from omnibias.core.proof.certificate import interval_certificate

    lam_min = certified_min_eigenvalue(matrix)
    if lam_min.lo <= 0.0:
        raise ValueError("matrix is not certified positive definite (lambda_min.lo <= 0)")
    return interval_certificate(
        claim or "lambda_min(A) certified positive",
        lam_min,
        meta={"scope": "symmetric_part", "collapse_axis": "eps->0"},
    )

Other public import paths

omnibias.core.verified.positive_definite_pivots_certificate
omnibias.core.verified.conditioning.positive_definite_pivots_certificate

← Package overview Runnable learning examples →

omnibias.core.verified.conditioning

FloatMatrix​

FloatVector​

certified_condition_number​

Parameters

certified_damping​

Parameters

certified_max_eigenvalue​

Parameters

certified_min_eigenvalue​

Parameters

certified_regularization_error​

Parameters

conditioning_certificate​

Parameters

positive_definite_pivots_certificate​

Parameters

FloatMatrix

FloatVector

certified_condition_number

certified_damping

certified_max_eigenvalue

certified_min_eigenvalue

certified_regularization_error

conditioning_certificate

positive_definite_pivots_certificate