Function check_statement 

pub fn check_statement(
    document: &EmittedDocument,
    reference: &ReferenceDeclaration,
) -> Result<(), EmissionFault>

Rule R8: the target’s REPARSED statement against reference, an independent translation of the Lean declaration (reference::reference_declaration) in the importer’s names. The reference is carried into LOGOS names through the correspondence alone — the emitter’s own terms play no part — and must name the target, bind the same universe parameters in the same order, and state the same type up to α.