Function assemble_observed 

pub fn assemble_observed(
    export: &str,
    target: &str,
    options: &BuildOptions,
    lean_print_axioms: Option<&[String]>,
) -> Result<PackageFiles, Verdict>

assemble_with, holding the result’s assumptions against what the pinned Lean’s own #print axioms reported for the target (Lean names), as the package’s contract says: any difference in either direction, and a native-rederived proof without Lean’s report, is an assumption_disagreement, and no package is handed out.