omnibias.core.proof.lean_check

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.proof.lean_check

Module contract & mathematical conventions

The Lean-kernel bridge: turn a certificate's finite obligation into a theorem.

This runner connects the certificate format to the Lean kernel (formal/omnibias-verified-kernel). It

1. extracts the **finite, rational** obligation carried by a certificate (spectral-gap positivity, or the sign of an enclosed quantity), refusing any certificate whose digest does not match its body (tamper-evidence); 2. emits a tiny Lean source file (Omnibias/Generated.lean) that discharges the obligation by chaining the kernel's *proven* soundness lemmas; 3. invokes lake build so the **Lean kernel** re-checks it; and 4. reports whether the kernel accepted the proof.

It is deliberately dependency-free (standard library only) so it can live in omnibias.core. When no Lean toolchain (lake) or kernel checkout is present it degrades gracefully -- lean_check_available returns False and check_certificate returns an available=False result rather than raising -- so a normal test / CI run without Lean is unaffected. Only a genuine lake pass yields verified=True; the flag can never be forged by the certificate itself.

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

LeanCheckResult

omnibias.core.proof.LeanCheckResultSource ↗

class LeanCheckResult

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.

The outcome of a Lean-kernel check of a single certificate.

Parameters

Name	Type & default	Contract
`verified`dataclass field	`bool`Required	See the operation contract and implementation below.
`available`dataclass field	`bool`Required	See the operation contract and implementation below.
`obligation`dataclass field	`str`Required	See the operation contract and implementation below.
`detail`dataclass field	`str`Required	See the operation contract and implementation below.

Fields & methods

verifiedfield

verified: bool

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

View source ↗

availablefield

available: bool

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

View source ↗

obligationfield

obligation: str

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

View source ↗

detailfield

detail: str

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

View source ↗

Read the implementation

class LeanCheckResult:
    """The outcome of a Lean-kernel check of a single certificate."""

    verified: bool
    available: bool
    obligation: str
    detail: str

Other public import paths

omnibias.core.proof.LeanCheckResult
omnibias.core.proof.lean_check.LeanCheckResult

FUNCTION

check_certificate

omnibias.core.proof.check_certificateSource ↗

check_certificate(cert: Mapping[str, Any], *, timeout: float=600.0, start: Path | None=None) -> LeanCheckResult

Generate the obligation, run lake build, and report the kernel verdict.

The certificate must carry a **valid seal**: an absent or mismatched digest is rejected before any Lean is emitted. Accepting an unsealed payload here would let an unsigned mapping earn verified=True, defeating the tamper-evidence the seal exists to provide -- so a missing digest is refused exactly like a forged one. If the toolchain is unavailable the result has available=False and verified=False.

Parameters

Name	Type & default	Contract
`cert`positional-or-keyword	`Mapping[str, Any]`Required	See the operation contract and implementation below.
`timeout`keyword-only	`float`Default: 600.0	See the operation contract and implementation below.
`start`keyword-only	`Path \| None`Default: None	See the operation contract and implementation below.

ReturnsLeanCheckResult

Executed regression · zeta value identity earns theorem prover verified

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_zeta_value_identity_earns_theorem_prover_verified(self) -> None:
        verdict = check_identity_certificate(zeta_negative_odd_identity(2, _ZETA_NEG[2]))
        assert verdict.theorem_prover_verified

python -m pytest "packages/omnibias-difference/tests/test_identities.py::TestRealLeanKernelPass::test_zeta_value_identity_earns_theorem_prover_verified" -q

Regression example · actual kernel build when toolchain available

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_actual_kernel_build_when_toolchain_available(certificate):
    from omnibias.core.proof.lean_check import check_certificate, lean_check_available

    if not lean_check_available():
        pytest.skip("Lean toolchain unavailable")
    assert check_certificate(certificate).verified

python -m pytest packages/omnibias-core/tests/proof/test_realization_replay.py -k test_actual_kernel_build_when_toolchain_available -q

Read the implementation

def check_certificate(
    cert: Mapping[str, Any],
    *,
    timeout: float = 600.0,
    start: Path | None = None,
) -> LeanCheckResult:
    """Generate the obligation, run ``lake build``, and report the kernel verdict.

    The certificate must carry a **valid seal**: an absent or mismatched ``digest``
    is rejected before any Lean is emitted.  Accepting an unsealed payload here
    would let an unsigned mapping earn ``verified=True``, defeating the
    tamper-evidence the seal exists to provide -- so a missing digest is refused
    exactly like a forged one.  If the toolchain is unavailable the result has
    ``available=False`` and ``verified=False``.
    """
    if not verify_certificate_digest(cert):
        reason = (
            "certificate digest mismatch (tampered/stale)"
            if "digest" in cert
            else "unsealed certificate (no digest); seal it with seal_certificate() first"
        )
        return LeanCheckResult(False, True, "", reason)

    obligation = generate_obligation(cert)
    if obligation is None:
        return LeanCheckResult(False, True, "", "no finite Lean-checkable obligation in certificate")

    root = kernel_root(start)
    if root is None or shutil.which("lake") is None:
        return LeanCheckResult(False, False, obligation, "Lean toolchain or kernel checkout unavailable")

    from omnibias.core.proof.lean_lock import generated_lean_obligation

    generated = root / _GENERATED_REL
    try:
        with generated_lean_obligation(root, generated, obligation):
            proc = subprocess.run(
                ["lake", "build"],
                cwd=str(root),
                capture_output=True,
                text=True,
                timeout=timeout,
                check=False,
            )
            ok = proc.returncode == 0
            detail = "Lean kernel accepted the obligation" if ok else (proc.stderr or proc.stdout)[-2000:]
            return LeanCheckResult(ok, True, obligation, detail)
    except (OSError, subprocess.SubprocessError) as exc:  # pragma: no cover - env dependent
        return LeanCheckResult(False, False, obligation, f"lake invocation failed: {exc}")

Other public import paths

omnibias.core.proof.check_certificate
omnibias.core.proof.lean_check.check_certificate

FUNCTION

generate_obligation

omnibias.core.proof.generate_obligationSource ↗

generate_obligation(cert: Mapping[str, Any]) -> str | None

Return Lean source discharging cert's finite obligation, or None.

Supported obligations:

**spectral gap** -- a certificate carrying subdominant_ratio_upper < 1 yields 0 < gapNumerator rn rd via spectral_gap_pos;
**positive-definite matrix** -- a v1 positive_definite payload (interval LDL^T pivots) yields the inertia-vector obligation allPivotsPos [...] = true (matrix_positive_definite_certified) when every pivot's lower endpoint is positive -- the full PD statement, not a single scalar;
**enclosed-quantity sign** -- a v1 interval payload (or any mapping with a lo/hi interval) yields enclosed_quantity_pos (when lo > 0) or enclosed_quantity_neg (when hi < 0).
**rational identity** -- a rational_identity payload carrying integer lhs_terms [[c, m], ...] and an integer rhs yields the exact Int equality sum_i c_i m_i = rhs via enclosed_quantity_eq (the difference lies in the point interval [0, 0]). This is how a special-number identity (a Bernoulli recurrence, zeta(1-2m) = -B_2m/(2m), ...) -- scaled to a common Int denominator -- earns a kernel-checked *equality*, not a sign.
**integer matrix syzygy** -- an integer_matrix_syzygy payload makes Lean recompute every exact matrix-vector dot product and require zero.
**polynomial identity over Q** -- a polynomial_identity_q payload carries cleared-denominator coefficient rows and strict rational margins. Lean independently recomputes every integer product/sum and every cross-multiplied positivity inequality. The producer remains responsible for enumerating the polynomial coefficients and Bernstein subdivision leaves.
**rational box-cover tiling** -- a box_cover_tiling payload carries a recursive axis-bisection tree. Lean reconstructs both child boxes at every split, checks every terminal box exactly, and checks each leaf count is at most the declared uniform bound.
**winding integer isolation** -- a winding_integer_isolation payload lifts both binary64 endpoints to one exact dyadic denominator and asks Lean to prove that the reported integer is the unique integer in the closed interval.
**PDE finite margin** -- a pinn_aposteriori_error payload may carry finite_obligation.margin = threshold - error_bound. The kernel checks only the finite inequality, not the analytic PDE theorem.
**stencil consistency** -- a rational_stencil_consistency payload of (lhs, rhs) rational pairs (moments C_j and the reported C_N) yields allRatEq [...] = true via Omnibias.RationalStencil.
**stencil poisedness** -- a rational_poisedness payload yields allIntGe (Polya) and ratNez (nonzero determinant). Neither payload states a collapse or a remainder over a function class.
**interval replay trace** -- an interval_replay_trace payload (omnibias.core.proof.replay.ReplayTrace.to_payload) yields Omnibias.Replay.replayOk [...] = true via decide: the Lean kernel genuinely re-executes every recorded sub/mul step against its own proven ZInterval arithmetic and checks each recorded envelope contains the exact recomputation. Scoped to exactly the literal/sub/mul vocabulary Omnibias/Replay.lean implements; emitted unconditionally (no Python-side truth pre-check), since the entire point is that Lean is the independent arbiter, not a rubber stamp of a Python conclusion.
**domain-subdivision coverage** -- a domain_subdivision payload (omnibias.core.proof.replay.DomainSubdivisionCertificate.to_payload) yields Omnibias.Subdivision.coversNoGaps ... = true via decide, checking the visited leaves tile the claimed domain edge-to-edge. Only emitted when the Python-side covers_no_gaps() check already agrees (matching the existing positive-definite-pivot / poisedness pattern of gating on a Python-side truth check before asking Lean to re-derive it); a certificate whose leaves have a gap is refused here, before any Lean is emitted.

Parameters

Name	Type & default	Contract
`cert`positional-or-keyword	`Mapping[str, Any]`Required	See the operation contract and implementation below.

Returnsstr | None

Executed regression · ratio at or above one is not a gap obligation

Full file, imports & fixtures ↗

def test_ratio_at_or_above_one_is_not_a_gap_obligation() -> None:
    assert generate_obligation({"subdominant_ratio_upper": 1.0}) is None
    assert generate_obligation({"subdominant_ratio_upper": 1.5}) is None

python -m pytest "packages/omnibias-core/tests/test_lean_check.py::test_ratio_at_or_above_one_is_not_a_gap_obligation" -q

Regression example · generate negative interval obligation

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_generate_negative_interval_obligation() -> None:
    cert = interval_certificate("q", Interval(-2.0, -0.5))
    src = generate_obligation(cert)
    assert src is not None
    assert "enclosed_quantity_neg" in src

python -m pytest packages/omnibias-core/tests/test_lean_check.py -k test_generate_negative_interval_obligation -q

Read the implementation

def generate_obligation(cert: Mapping[str, Any]) -> str | None:
    r"""Return Lean source discharging ``cert``'s finite obligation, or ``None``.

    Supported obligations:

    * **spectral gap** -- a certificate carrying ``subdominant_ratio_upper`` ``< 1``
      yields ``0 < gapNumerator rn rd`` via ``spectral_gap_pos``;
    * **positive-definite matrix** -- a v1 ``positive_definite`` payload (interval
      ``LDL^T`` pivots) yields the inertia-vector obligation ``allPivotsPos [...] =
      true`` (``matrix_positive_definite_certified``) when every pivot's lower
      endpoint is positive -- the full PD statement, not a single scalar;
    * **enclosed-quantity sign** -- a v1 ``interval`` payload (or any mapping with a
      ``lo``/``hi`` interval) yields ``enclosed_quantity_pos`` (when ``lo > 0``) or
      ``enclosed_quantity_neg`` (when ``hi < 0``).
    * **rational identity** -- a ``rational_identity`` payload carrying integer
      ``lhs_terms`` ``[[c, m], ...]`` and an integer ``rhs`` yields the exact ``Int``
      equality ``sum_i c_i m_i = rhs`` via ``enclosed_quantity_eq`` (the difference
      lies in the point interval ``[0, 0]``).  This is how a special-number identity
      (a Bernoulli recurrence, ``zeta(1-2m) = -B_2m/(2m)``, ...) -- scaled to a
      common ``Int`` denominator -- earns a kernel-checked *equality*, not a sign.
    * **integer matrix syzygy** -- an ``integer_matrix_syzygy`` payload makes Lean
      recompute every exact matrix-vector dot product and require zero.
    * **polynomial identity over Q** -- a ``polynomial_identity_q`` payload carries
      cleared-denominator coefficient rows and strict rational margins. Lean
      independently recomputes every integer product/sum and every cross-multiplied
      positivity inequality. The producer remains responsible for enumerating the
      polynomial coefficients and Bernstein subdivision leaves.
    * **rational box-cover tiling** -- a ``box_cover_tiling`` payload carries a
      recursive axis-bisection tree. Lean reconstructs both child boxes at every
      split, checks every terminal box exactly, and checks each leaf count is at
      most the declared uniform bound.
    * **winding integer isolation** -- a ``winding_integer_isolation`` payload lifts
      both binary64 endpoints to one exact dyadic denominator and asks Lean to prove
      that the reported integer is the unique integer in the closed interval.
    * **PDE finite margin** -- a ``pinn_aposteriori_error`` payload may carry
      ``finite_obligation.margin = threshold - error_bound``.  The kernel checks
      only the finite inequality, not the analytic PDE theorem.
    * **stencil consistency** -- a ``rational_stencil_consistency`` payload of
      ``(lhs, rhs)`` rational pairs (moments ``C_j`` and the reported ``C_N``)
      yields ``allRatEq [...] = true`` via ``Omnibias.RationalStencil``.
    * **stencil poisedness** -- a ``rational_poisedness`` payload yields
      ``allIntGe`` (Polya) and ``ratNez`` (nonzero determinant). Neither
      payload states a collapse or a remainder over a function class.
    * **interval replay trace** -- an ``interval_replay_trace`` payload
      (:meth:`omnibias.core.proof.replay.ReplayTrace.to_payload`) yields
      ``Omnibias.Replay.replayOk [...] = true`` via ``decide``: the Lean
      kernel genuinely re-executes every recorded ``sub``/``mul`` step
      against its own proven ``ZInterval`` arithmetic and checks each
      recorded envelope contains the exact recomputation. Scoped to
      exactly the ``literal``/``sub``/``mul`` vocabulary
      ``Omnibias/Replay.lean`` implements; emitted unconditionally (no
      Python-side truth pre-check), since the entire point is that Lean is
      the independent arbiter, not a rubber stamp of a Python conclusion.
    * **domain-subdivision coverage** -- a ``domain_subdivision`` payload
      (:meth:`omnibias.core.proof.replay.DomainSubdivisionCertificate.to_payload`)
      yields ``Omnibias.Subdivision.coversNoGaps ... = true`` via
      ``decide``, checking the visited leaves tile the claimed domain
      edge-to-edge. Only emitted when the Python-side
      ``covers_no_gaps()`` check already agrees (matching the existing
      positive-definite-pivot / poisedness pattern of gating on a
      Python-side truth check before asking Lean to re-derive it); a
      certificate whose leaves have a gap is refused here, before any Lean
      is emitted.
    """
    if isinstance(cert.get("payload"), Mapping) and cert["payload"].get("type") == "realization_replay":
        from omnibias.core.proof.realization_replay import generate_replay_obligation

        return generate_replay_obligation(cert)
    header = (
        "/- AUTO-GENERATED by omnibias.core.proof.lean_check. DO NOT EDIT. -/\n"
        "import Omnibias.Certificate\n\n"
        "namespace Omnibias.Generated\n\n"
    )
    stencil_header = (
        "/- AUTO-GENERATED by omnibias.core.proof.lean_check. DO NOT EDIT. -/\n"
        "import Omnibias.RationalStencil\n\n"
        "namespace Omnibias.Generated\n\n"
    )
    footer = "\nend Omnibias.Generated\n"

    box_cover = _extract_box_cover_tiling(cert)
    if box_cover is not None:
        parent, tree, uniform_bound = box_cover

        def rat_literal(value: tuple[int, int]) -> str:
            return f"(({value[0]} : Int), ({value[1]} : Int))"

        def box_literal(
            box: list[tuple[tuple[int, int], tuple[int, int]]],
        ) -> str:
            return "[" + ", ".join(
                f"({rat_literal(lo)}, {rat_literal(hi)})"
                for lo, hi in box
            ) + "]"

        def tree_literal(node: tuple[Any, ...]) -> str:
            if node[0] == "leaf":
                return (
                    f"(CoverTree.leaf {box_literal(node[1])} "
                    f"({node[2]} : Int))"
                )
            return (
                f"(CoverTree.split {node[1]} {rat_literal(node[2])} "
                f"{tree_literal(node[3])} {tree_literal(node[4])})"
            )

        body = (
            "/-- Exact rational intervals and recursive axis-bisection covers. -/\n"
            "abbrev RatQ := Int × Int\n"
            "abbrev RatIv := RatQ × RatQ\n\n"
            "def ratLt (a b : RatQ) : Bool :=\n"
            "  decide (0 < a.2 ∧ 0 < b.2 ∧ a.1 * b.2 < b.1 * a.2)\n\n"
            "def ratEq (a b : RatQ) : Bool :=\n"
            "  decide (0 < a.2 ∧ 0 < b.2 ∧ a.1 * b.2 = b.1 * a.2)\n\n"
            "def intervalValid (a : RatIv) : Bool := ratLt a.1 a.2\n\n"
            "def boxValid (box : List RatIv) : Bool :=\n"
            "  !box.isEmpty && box.all intervalValid\n\n"
            "def boxEq (a b : List RatIv) : Bool :=\n"
            "  a.length == b.length && (a.zip b).all (fun pair =>\n"
            "    ratEq pair.1.1 pair.2.1 && ratEq pair.1.2 pair.2.2)\n\n"
            "inductive CoverTree where\n"
            "  | leaf (box : List RatIv) (count : Int)\n"
            "  | split (axis : Nat) (cut : RatQ) (left right : CoverTree)\n\n"
            "def checkTree (bound : Int) (expected : List RatIv) : CoverTree -> Bool\n"
            "  | .leaf box count =>\n"
            "      boxValid box && boxEq expected box && decide (0 ≤ count ∧ count ≤ bound)\n"
            "  | .split axis cut left right =>\n"
            "      match expected[axis]? with\n"
            "      | none => false\n"
            "      | some interval =>\n"
            "          ratLt interval.1 cut && ratLt cut interval.2 &&\n"
            "          checkTree bound (expected.set axis (interval.1, cut)) left &&\n"
            "          checkTree bound (expected.set axis (cut, interval.2)) right\n\n"
            "set_option maxRecDepth 100000\n\n"
            "/-- Every recursive child pair exactly tiles its parent and every\n"
            "terminal count obeys the same finite bound. -/\n"
            "theorem obligation :\n"
            f"    boxValid {box_literal(parent)} &&\n"
            f"    checkTree ({uniform_bound} : Int) {box_literal(parent)} "
            f"{tree_literal(tree)} = true := by\n"
            "  decide\n"
        )
        return header + body + footer

    polynomial_identity = _extract_polynomial_identity_q(cert)
    if polynomial_identity is not None:
        equations, positive = polynomial_identity
        row_literals = ", ".join(
            "(["
            + ", ".join(f"(({left} : Int), ({right} : Int))" for left, right in terms)
            + f"], ({rhs} : Int))"
            for terms, rhs in equations
        )
        positive_literals = ", ".join(
            f"((0 : Int), (1 : Int), ({num} : Int), ({den} : Int))"
            for num, den in positive
        )
        body = (
            "/-- Cleared-denominator coefficient identities. Each pair is one\n"
            "integer product; Lean recomputes every sum independently. -/\n"
            "def productSum : List (Int × Int) -> Int\n"
            "  | [] => 0\n"
            "  | (a, b) :: rest => a * b + productSum rest\n\n"
            "def coefficientRow (row : List (Int × Int) × Int) : Bool :=\n"
            "  productSum row.1 == row.2\n\n"
            "def polynomialIdentity (rows : List (List (Int × Int) × Int)) : Bool :=\n"
            "  !rows.isEmpty && rows.all coefficientRow\n\n"
            "set_option maxRecDepth 100000\n\n"
            "/-- The identity rows and every signed Bernstein margin are exact.\n"
            "Topology and the Harnack implication remain external. -/\n"
            "theorem obligation :\n"
            f"    polynomialIdentity [{row_literals}] = true ∧\n"
            f"    allRatLt [{positive_literals}] = true := by\n"
            "  decide\n"
        )
        return stencil_header + body + footer

    matrix_syzygy = _extract_integer_matrix_syzygy(cert)
    if matrix_syzygy is not None:
        matrix, vector = matrix_syzygy
        row_literals = ", ".join(
            "[" + ", ".join(f"({value} : Int)" for value in row) + "]"
            for row in matrix
        )
        vector_literal = ", ".join(f"({value} : Int)" for value in vector)
        body = (
            "/-- Exact cleared-denominator Q[h] syzygy. Lean recomputes every\n"
            "matrix-vector product; no floating rank or Python residual is trusted. -/\n"
            "def dotInt : List Int -> List Int -> Int\n"
            "  | [], [] => 0\n"
            "  | a :: xs, b :: ys => a * b + dotInt xs ys\n"
            "  | _, _ => 1\n\n"
            "def rowSyzygy (row vector : List Int) : Bool :=\n"
            "  row.length == vector.length && dotInt row vector == 0\n\n"
            "def matrixSyzygy (matrix : List (List Int)) (vector : List Int) : Bool :=\n"
            "  !matrix.isEmpty && !vector.isEmpty && matrix.all (fun row => rowSyzygy row vector)\n\n"
            f"theorem obligation : matrixSyzygy [{row_literals}] [{vector_literal}] = true := by\n"
            "  decide\n"
        )
        return header + body + footer

    winding_isolation = _extract_winding_integer_isolation(cert)
    if winding_isolation is not None:
        lo_num, hi_num, denominator, integer = winding_isolation
        body = (
            "/-- The reported winding number is the unique integer in the exact\n"
            "dyadic lift of the outward binary64 enclosure. The analytic argument-\n"
            "principle enclosure is a trusted certificate input, not re-derived. -/\n"
            "def windingIsolated (lo hi denominator integer : Int) : Bool :=\n"
            "  decide (0 < denominator ∧\n"
            "    (integer - 1) * denominator < lo ∧\n"
            "    lo ≤ integer * denominator ∧\n"
            "    integer * denominator ≤ hi ∧\n"
            "    hi < (integer + 1) * denominator)\n\n"
            "theorem obligation :\n"
            f"    windingIsolated ({lo_num}) ({hi_num}) ({denominator}) ({integer}) = true := by\n"
            "  decide\n"
        )
        return header + body + footer

    stencil_pairs = _extract_stencil_pairs(cert)
    if stencil_pairs is not None:
        lits = ", ".join(
            f"(({p}), {q}, {r}, {s})" for p, q, r, s in stencil_pairs
        )
        body = (
            "/-- Finite stencil identities: each (p/q) = (r/s) is the Int\n"
            "cross-multiplication p*s = r*q with nonzero denominators. Algebra\n"
            "only; no collapse and no remainder over a function class. -/\n"
            f"theorem obligation : allRatEq [{lits}] = true := by decide\n"
        )
        return stencil_header + body + footer



    replay_steps = _extract_replay_trace(cert)
    if replay_steps is not None:
        lits = ", ".join(
            f"⟨{kind}, {a0}, {a1}, {lo}, {hi}, {exp}⟩" for kind, a0, a1, lo, hi, exp in replay_steps
        )
        replay_header = (
            "/- AUTO-GENERATED by omnibias.core.proof.lean_check. DO NOT EDIT. -/\n"
            "import Omnibias.Replay\n\n"
            "namespace Omnibias.Generated\n\n"
        )
        body = (
            "/-- Finite straight-line replay: every recorded `sub`/`mul` step's\n"
            "envelope genuinely contains the exact recomputation from prior\n"
            "recorded steps, via the kernel's proven `ZInterval` arithmetic.\n"
            "`literal` steps are trusted inputs, not re-derived. -/\n"
            f"theorem obligation : Omnibias.Replay.replayOk [{lits}] = true := by decide\n"
        )
        return replay_header + body + footer

    subdivision = _extract_domain_subdivision(cert)
    if subdivision is not None:
        resolution, leaves = subdivision
        lits = ", ".join(f"⟨{lo}, {hi}⟩" for lo, hi in leaves)
        subdivision_header = (
            "/- AUTO-GENERATED by omnibias.core.proof.lean_check. DO NOT EDIT. -/\n"
            "import Omnibias.Subdivision\n\n"
            "namespace Omnibias.Generated\n\n"
        )
        body = (
            "/-- Finite domain-subdivision coverage: the visited leaves tile\n"
            f"[0, {resolution}] edge-to-edge, with no gap and no overlap. Says\n"
            "nothing about any individual leaf's own analytic conclusion. -/\n"
            f"theorem obligation : "
            f"Omnibias.Subdivision.coversNoGaps ({resolution}) [{lits}] = true := by decide\n"
        )
        return subdivision_header + body + footer

    poised = _extract_poisedness(cert)
    if poised is not None:
        polya, det_n, det_d = poised
        polya_lits = ", ".join(f"(({have}), {need})" for have, need in polya)
        body = (
            "/-- Finite poisedness: Polya integer comparisons and a nonzero\n"
            "rational determinant witness. Algebra only. -/\n"
            f"theorem obligation : allIntGe [{polya_lits}] = true ∧ "
            f"ratNez ({det_n}) {det_d} = true := by decide\n"
        )
        return stencil_header + body + footer



    pivots = _extract_pd_pivots(cert)
    if pivots is not None:
        scaled = [_scaled_pair(lo, hi) for lo, hi in pivots]
        if scaled and all(ilo > 0 for ilo, _ihi in scaled):
            pivot_lits = ", ".join(f"⟨{ilo}, {ihi}⟩" for ilo, ihi in scaled)
            pd_header = (
                "/- AUTO-GENERATED by omnibias.core.proof.lean_check. DO NOT EDIT. -/\n"
                "import Omnibias.LDLT\n\n"
                "namespace Omnibias.Generated\n\n"
            )
            body = (
                "/-- Certified positive-definite LDLᵀ inertia: every pivot interval is\n"
                "strictly positive, so the negative inertia is zero -- the matrix box is\n"
                "positive definite (factorisation a trusted Python input). -/\n"
                f"theorem obligation : allPivotsPos [{pivot_lits}] = true := by decide\n"
            )
            return pd_header + body + footer

    identity = _extract_rational_identity(cert)
    if identity is not None:
        lhs_terms, rhs = identity
        lhs = " + ".join(f"({c}) * ({m})" for c, m in lhs_terms)
        body = (
            f"/-- Rational special-number identity: sum_i c_i m_i = {rhs} (integers over a\n"
            f"common denominator), certified as an exact Int equality via the point interval\n"
            f"[0, 0] and `enclosed_quantity_eq`. -/\n"
            f"theorem obligation : ({lhs} : Int) = {rhs} := by\n"
            f"  have hx : ZInterval.Mem (({lhs}) - ({rhs})) ⟨0, 0⟩ := by\n"
            f"    simp only [ZInterval.Mem]; omega\n"
            f"  have key : ({lhs}) - ({rhs}) = 0 := ZInterval.eq_of_mem_point hx (by decide)\n"
            f"  omega\n"
        )
        return header + body + footer

    ratio = cert.get("subdominant_ratio_upper")
    if isinstance(ratio, int | float) and 0.0 <= float(ratio) < 1.0:
        frac = Fraction(float(ratio))
        rn, rd = frac.numerator, frac.denominator
        if rd <= 0:
            rn, rd = -rn, -rd
        body = (
            f"/-- Spectral-gap positivity from subdominant-ratio upper bound "
            f"{rn}/{rd} < 1. -/\n"
            f"theorem obligation : 0 < gapNumerator {rn} {rd} :=\n"
            f"  spectral_gap_pos (by decide) (by decide)\n"
        )
        return header + body + footer

    interval = _extract_interval(cert)
    if interval is not None:
        lo, hi = interval
        ilo, ihi = _scaled_pair(lo, hi)
        if ilo > 0:
            body = (
                f"/-- Enclosed quantity is positive: x in [{ilo}, {ihi}] => 0 < x. -/\n"
                f"theorem obligation (x : Int) "
                f"(hx : ZInterval.Mem x ⟨{ilo}, {ihi}⟩) : 0 < x :=\n"
                f"  enclosed_quantity_pos hx (by decide)\n"
            )
            return header + body + footer
        if ihi < 0:
            body = (
                f"/-- Enclosed quantity is negative: x in [{ilo}, {ihi}] => x < 0. -/\n"
                f"theorem obligation (x : Int) "
                f"(hx : ZInterval.Mem x ⟨{ilo}, {ihi}⟩) : x < 0 :=\n"
                f"  enclosed_quantity_neg hx (by decide)\n"
            )
            return header + body + footer
    return None

Other public import paths

omnibias.core.proof.generate_obligation
omnibias.core.proof.lean_check.generate_obligation

FUNCTION

kernel_root

omnibias.core.proof.kernel_rootSource ↗

kernel_root(start: Path | None=None) -> Path | None

Locate formal/omnibias-verified-kernel by walking up from start.

Parameters

Name	Type & default	Contract
`start`positional-or-keyword	`Path \| None`Default: None	See the operation contract and implementation below.

ReturnsPath | None

Executed regression · zeta value identity earns theorem prover verified

Full file, imports & fixtures ↗

    def test_zeta_value_identity_earns_theorem_prover_verified(self) -> None:
        verdict = check_identity_certificate(zeta_negative_odd_identity(2, _ZETA_NEG[2]))
        assert verdict.theorem_prover_verified

python -m pytest "packages/omnibias-difference/tests/test_identities.py::TestRealLeanKernelPass::test_zeta_value_identity_earns_theorem_prover_verified" -q

Regression example · kernel root is discoverable

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_kernel_root_is_discoverable() -> None:
    root = kernel_root()
    assert root is not None
    assert root.name == "omnibias-verified-kernel"
    assert (root / "lakefile.lean").is_file()
    assert (root / "Omnibias" / "Certificate.lean").is_file()

python -m pytest packages/omnibias-core/tests/test_lean_check.py -k test_kernel_root_is_discoverable -q

Read the implementation

def kernel_root(start: Path | None = None) -> Path | None:
    """Locate ``formal/omnibias-verified-kernel`` by walking up from ``start``."""
    here = (start or Path(__file__)).resolve()
    for parent in [here, *here.parents]:
        candidate = parent / _KERNEL_REL
        if (candidate / "lakefile.lean").is_file():
            return candidate
    return None

Other public import paths

omnibias.core.proof.kernel_root
omnibias.core.proof.lean_check.kernel_root

FUNCTION

lean_check_available

omnibias.core.proof.lean_check_availableSource ↗

lean_check_available(start: Path | None=None) -> bool

True iff both a lake executable and the kernel checkout are present.

Parameters

Name	Type & default	Contract
`start`positional-or-keyword	`Path \| None`Default: None	See the operation contract and implementation below.

Returnsbool

Executed regression · actual kernel build when toolchain available

Full file, imports & fixtures ↗

def test_actual_kernel_build_when_toolchain_available(certificate):
    from omnibias.core.proof.lean_check import check_certificate, lean_check_available

    if not lean_check_available():
        pytest.skip("Lean toolchain unavailable")
    assert check_certificate(certificate).verified

python -m pytest "packages/omnibias-core/tests/proof/test_realization_replay.py::test_actual_kernel_build_when_toolchain_available[certificate0]" -q

Regression example · actual kernel algebra build when toolchain available

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_actual_kernel_algebra_build_when_toolchain_available(certificate):
    from omnibias.core.proof.lean_check import check_certificate, lean_check_available

    if not lean_check_available():
        pytest.skip("Lean toolchain unavailable")
    assert check_certificate(certificate).verified

python -m pytest packages/omnibias-core/tests/proof/test_realization_algebra_replay.py -k test_actual_kernel_algebra_build_when_toolchain_available -q

Read the implementation

def lean_check_available(start: Path | None = None) -> bool:
    """``True`` iff both a ``lake`` executable and the kernel checkout are present."""
    return shutil.which("lake") is not None and kernel_root(start) is not None

Other public import paths

omnibias.core.proof.lean_check_available
omnibias.core.proof.lean_check.lean_check_available

← Package overview Runnable learning examples →

omnibias.core.proof.lean_check

LeanCheckResult​

Parameters

Fields & methods

check_certificate​

Parameters

generate_obligation​

Parameters

kernel_root​

Parameters

lean_check_available​

Parameters

LeanCheckResult

check_certificate

generate_obligation

kernel_root

lean_check_available