just proof-check-all is red: per-file checks resolve no modules; ABI/Types Idris2 mint templates do not typecheck #103

Observed during Phase 0 (PR #102); pre-existing on main, not fixed there (outside the brief, which forbade widening the PR).

Symptoms (Idris2 0.8.0, Agda 2.7.0.1, run from the repo root on claude/new-session-snuoro):

1. just proof-check-idris2 runs idris2 --check "$f" per file from the repo root, so every file fails with Module name Trope.Fidelity does not match file name … or Module Trope.Fidelity not found. Run from inside verification/proofs/idris2/, the eight Trope/*.idr modules and ABI/Foreign.idr check OK, but these do not:
   • ABI/Layout.idr (and ABI/Compliance.idr, which imports it): Undefined name NonZero
   • ABI/Platform.idr: Undefined name LTE
   • ABI/Pointers.idr: ABI.Pointers.SafePtr.(.nonNull) is not accessible in this context
   • Types.idr: fails after a shadowing warning
     These are RSR mint templates, never instantiated for this repo.
2. just proof-check-agda has the same per-file problem (agda --safe from the repo root: "The name of the top level module does not match the file name"), and lacks --without-K for Theorem B.
3. just proof-check-lean4 SKIPs silently when lean is absent — a gate that cannot fail.
4. just proof-scan-dangerous PASSes.

Why it matters: the recipe advertised as "the full sweep" is red for reasons unrelated to the proofs, so nobody runs it, and if it ever went green it would be green for the wrong reasons. The gates that actually attest the development are just check (Idris2 package typecheck + reference build + conformance), just build-agda, just trope-rust, and verify-all / proofs.yml.

Options (owner's call):

• (a) Make proof-check-idris2 / proof-check-agda delegate to the package-level gates (idris2 --typecheck trope.ipkg, build-agda) and drop per-file iteration; make proof-check-lean4 fail loudly when lean is missing (or delegate to build-lean).
• (b) Decide the fate of the ABI/* + Types.idr templates: instantiate them for the actual ABI seam (abi.ipkg at the root says the seam lives in src/interface/Abi/), or remove them as was done for the Coq/TLA+/Properties.agda templates in Phase 0: make the status surfaces true (trope-checker) #102 (ADR 0005 D5). Not deletion-by-recency: they have never typechecked.