Proofs: mechanize the first metatheory obligation

[hyperpolymath]

Backs proof-kind evidence. Area: verification/proofs/ (Coq/Agda/Idris2).

Closing implementation holes is not proving soundness; the metatheory must be mechanized separately and honestly.

Scope

• Pick the first load-bearing obligation (e.g. a Core preservation property, or codegen→target preservation through the typed ABI seam) and mechanize it.
• No axiomatic escapes in load-bearing tracks: no Admitted, no believe_me, no unsafeCoerce; Print Assumptions (or equivalent) must be clean.

Done when

• One obligation in docs/status/PROOF-NEEDS.adoc is discharged and recorded in docs/status/PROOF-STATUS.adoc.
• The proof is wired into CI so it can't silently rot.

Ref: docs/architecture/DESIGN-DISCIPLINE.adoc, docs/status/PROOF-NEEDS.adoc.