Struct TheoremRecheck 

pub struct TheoremRecheck {
    pub rechecks: bool,
    pub two_kernel_agreement: bool,
    pub error: Option<String>,
    pub axioms: AxiomUsage,
}

The outcome of independently re-checking a TheoremCertificate.

Fields

rechecks: bool

Whether the proof term type-checks to the claimed goal in the rebuilt context and rests on nothing ADMITTED. This is the load-bearing verdict — established by TYPE-CHECKING the term, never by re-running proof search.

The second conjunct is the part Lean leaves to the reader. A sorry-tainted proof type-checks, both kernels agree on it, and a caller that asks only “did it check?” is told yes. So the taint is folded into THIS field rather than offered beside it: there is no reading of rechecks == true under which the proof rests on an admission, and no command anyone has to remember to run.

two_kernel_agreement: bool

The strongest agreement reached: true when the SECOND, independent de Bruijn kernel (double_check) also verified the term to a definitionally-equal type (the full de Bruijn criterion). false when the term type-checks under the main kernel but sits outside the re-checker’s covered fragment (still a valid proof, honestly single-checked) or fails to re-check at all.

error: Option<String>

The reason a re-check failed, when it did.

axioms: AxiomUsage

Every axiom the proof rests on, TRANSITIVELY — our #print axioms, re-derived against the trusted base this check rebuilt rather than against whatever the minting side disclosed.

Populated even when the re-check FAILS, and deliberately: “which assumptions did this thing want?” is exactly the question a rejected certificate raises, and answering it is most of the diagnosis.

EMPTY on exactly two refusals, and in both the honest answer is “no report”: a version mismatch means the names were not checked against THIS base at all, and a delta that REDEFINES a trusted constant means a report naming dne would name the reader’s dne and not the certificate’s — which is the misreading that refusal exists to prevent.

Trait Implementations

impl Clone for TheoremRecheck

fn clone(&self) -> TheoremRecheck

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for TheoremRecheck

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for TheoremRecheck

fn eq(&self, other: &TheoremRecheck) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for TheoremRecheck