Function recheck_theorem 

pub fn recheck_theorem(cert: &TheoremCertificate) -> TheoremRecheck

Independently re-validate a TheoremCertificate.

Rebuilds the prelude + disclosed delta, infers the proof term’s type, and requires it to be the claimed goal (up to definitional equality / cumulativity). The verdict comes from TYPE-CHECKING, not from re-running the prover’s backward-chaining search — so the checker is a genuinely independent witness. Where the term lies inside the second kernel’s fragment, double_check corroborates it, giving the full de Bruijn two-kernel guarantee (two_kernel_agreement).

The admission gate — and why it is a gate rather than a note

The transitive axiom closure is computed FIRST, against the rebuilt context, and a proof that rests on anything is_admitted_axiom recognises does not re-check at all. This is the one place LOGOS deliberately does more than Lean, and the reason is the shape of the failure: sorryAx proves anything, so a tainted proof type-checks, BOTH kernels agree on it, and verified == true really does hold. Lean warns on the declaration that CONTAINS the sorry and says nothing about its dependants, so a theorem three lemmas downstream looks finished and #print axioms is a command you must remember to run. Here the closure is transitive and the verdict carries it, so the taint cannot be lost by renaming, re-exporting, citing at a distance — or by a caller reading only rechecks.

Tracking is not banning: a proof resting on Classical_choice, propext or Quot_sound is a perfectly good proof and re-checks, with those names reported in axioms. The gate is for the names that mark a proof as NOT FINISHED.