Function check_export 

pub fn check_export(
    export: &str,
    target: &str,
    evidence: &LeanEvidence,
    limits: &Limits,
) -> Checked

Run every in-process stage over a Lean export for the dotted Lean name target: intake, import and check, independent recheck, assumption policy, emission and package assembly. fresh_replay is left to the caller, which must replay the published package in a new process.