Bind formalized Lean targets to built artifacts in CI #119

Problem

Autoform resolves lean: names lexically across every .lean file, including declarations after #exit and modules outside the default Lake target. Generated verification CI builds and kernel-audits only the default target's artifact closure. A formalized article can therefore name an orphan, unbuilt, stale, or unsafe declaration and still pass CI.

This is G6 + G8 from #92's adversarial review. Formalize's instruction to import new modules mitigates accidents but does not establish machine-checked authority.

Existing work

• Draft Verify local Lean artifacts before publication #69 contains artifact-binding ideas but is stale/conflicting.
• Draft Open statements and a revision contract for shared Lean declarations #115 verifies built-environment membership only for its opt-in open-statement policy; strict projects still use the old path.

Acceptance criteria

• Generated CI passes every formalized local target and expected declaration kind to a post-clean, kernel-backed audit.
• Verification rejects a lean: target absent from the built root package, outside the trusted/default artifact closure, of the wrong kind, or backed by stale artifacts.
• The lexical index stops recognizing declarations after top-level #exit.
• An orphan module containing sorry or a new axiom fails Autoform verification even when the default lake build succeeds.
• Existing Mathlib/external targets retain an explicit, tested policy.
• Templates, bundled example, CLI diagnostics, and real-Lean CI exercise the same contract.

Carry-forward from #145

The refreshed implementation must preserve canonical root-module artifact lookup; exact packed/live .ilean, .olean, and .trace binding; complete retained project inputs including arbitrary non-Lean payloads and package overrides; root/dependency module-shadow defense; and primary-versus-supporting target semantics. It must also reject committed/prebuilt artifacts before rebuilding, bind .olean.private and .olean.server companions, preserve current open/retracted-statement semantics, and run real-Lake CI. Land #156 first and rebuild this gate as smaller current-main PRs. #167 owns isolation from project-controlled probe code; #160 is the downstream Mathlib-provenance layer.