pub fn theorem_certificate(
input: &str,
) -> Result<Option<TheoremCertificate>, ParseError>Expand description
Build an INDEPENDENTLY RE-CHECKABLE certificate for a proved English ## Theorem.
A largo prove ✓ is a boolean the caller must trust the prover for. A
kernel::certificate::TheoremCertificate is instead a portable artifact — the
kernel proof term, the goal it proves, and the theorem’s DISCLOSED environment delta
(its declared vocabulary + stated premises as hypotheses) — that a third party can
re-verify with nothing but the kernel, by TYPE-CHECKING the term, never by re-running
proof search.
Returns Ok(None) when the theorem block parses but is NOT kernel-certified (an
unproved goal has no proof term, so no certificate exists — the honest outcome).
Only a genuine kernel derivation yields a certificate; there is no finite-enumeration
path here that could mint one.