proof: typing_free_of_absent_region (Qed) — Brief C kernel

[hyperpolymath]

Summary

Adds the static-shadowing-prevention lemma referenced by the forward comment at formal/Semantics.v:9096 (post-MIDDLE-narrowing diagnostic block):

Lemma typing_free_of_absent_region :
  forall R G e T G' r,
    R; G |- e : T -| G' ->
    ~ In r R ->
    expr_free_of_region r e.

Proved by structural induction on the typing derivation (26 cases, ~50 LOC). Each typing rule's region premise is incompatible with ~In r R when applied at r:

• T_Loc and T_StringNew force the r0 <> r case via their In r0 R premise.
• T_Region's body recurses under r0 :: R where ~In r (r0 :: R) still holds when r <> r0.
• T_Region_Active contradicts directly when r = r0.

Why this matters

Does not close any preservation admit on its own — the touches_region RIGHT cases have In r R (not ~In r R) by construction. But this lemma is the kernel of Brief C's structural recursion: any closure path that traces an exited region back to its introducing ERegion via inversion-on-Hstep will need this fact to establish sibling-disjointness from the inner T_Region's ~In premise.

Lands as a Qed building block alongside region_shrink_preserves_typing_dup (also adjunct), available for Brief C work to pull in.

Test plan

• make -f Makefile.coq Semantics.vo clean rebuild on rocq toolchain → exits 0
• grep -c "^Admitted\." formal/Semantics.v == 1 (only preservation)
• GPG-signed (key 4A03639C1EB1F86C7F0C97A91835A14A2867091E)
• Co-author tag for Claude Opus 4.7

Refs ephapax#146.

🤖 Generated with Claude Code