The formal bridge
The public substrate contains a bridge from supported certificate obligations to a Lean check. It is a narrow verification path with explicit availability and result reporting. It does not turn every model output or analytic assertion into a theorem.
Inspect availability and the supported obligation
The current public entry points are lean_check_available, generate_obligation, and check_certificate in omnibias.core.proof.lean_check. The older verify_with_lean example is not the current API.
The bridge first interprets a supported finite obligation from the certificate. Its generated proof and toolchain execution are distinct from the numerical computation that produced the certificate. Record the exact source revision, obligation, toolchain availability, check result, and diagnostic message when reporting an outcome.
Three different questions
- Integrity: has the recorded certificate payload changed?
- Replay: does the independent replay procedure reproduce the supported numerical claim?
- Formal checking: did the supported emitted obligation pass the configured proof-checking path?
A success in one category is not evidence of success in the others. Inspect the returned result and its scope rather than relying on a label supplied by untrusted input. Toolchain absence, unsupported obligations, timeouts, and failed checks must remain visible.
Boundary of the claim
A finite rational obligation does not establish an unrestricted analytic theorem. It only proves the statement that was encoded under the checker's assumptions. Higher-level application claims require their own reduction, domain conditions, and evidence. See exactness and scope and verified arithmetic.