feat(L1): Phase D slice 4 Phase 3a — tfuneff_lambda_retype_l1_m (#223)

## Summary

- Adds `tfuneff_lambda_retype_l1_m` to `formal/Semantics_L1.v` —
re-types values at `TFunEff T1 T2 R_in R_out` across `R → R'` under the
side condition `forall r, In r R' -> In r R_in`.
- Phase 3a of the SUBST-LEMMA-GENERALIZATION-DESIGN.md plan; mirrors
Phase 1 / Phase 2 split shipped in #219 / #220.
- Zero new admits, zero new axioms, no patch to legacy `preservation` in
`Semantics.v`.

## Why

For values typed at `TFunEff T1 T2 R_in R_out`, the lambda's body is
typed at `R_in` (carried in the type, independent of the outer `R`). The
outer `R` enters the typing rule only through the side condition `forall
r, In r R -> In r R_in`. Re-typing at any `R'` reduces to discharging
the analogous side condition for `R'`.

Two value-shape × typing-rule cases survive `inversion`:
- `T_Lam_L1_Linear_Eff` — Linear-modality TFunEff lambda
- `T_Lam_L1_Affine_Eff` — Affine-modality TFunEff lambda

Legacy `T_Lam_L1_Linear` and `T_Lam_L1_Affine` produce `TFun …` (not
`TFunEff …`) so `inversion` auto-discharges them via
constructor-conclusion equation discrimination. Non-lambda value shapes
(`EUnit` / `EBool` / `EI32` / `EPair` / `EInl` / `EInr` / `ELoc` /
`EBorrow` / `EEcho`) are typed at base / product / sum / borrow / region
/ echo types — all distinct from `TFunEff` — and discharge identically.

## Why split Phase 3 into 3a + 3b

SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3 originally combined (a) the
retype lemma + (b) the substitution-lemma extension. Splitting follows
the Phase 1 / Phase 2 pattern (Phase 1 = retype lemma; Phase 2 = subst
lemma) and keeps the PR minimal-purpose. Phase 3b (extend
`subst_typing_gen_l1_m` to TFunEff lambda substituends) is queued as a
follow-on.

## Constraints preserved (owner directive 2026-05-27)

- ✅ Does not patch legacy `Semantics.v` `preservation` (provably false
via `Counterexample.v`).
- ✅ Does not extend `Semantics.v` with closure-support lemmas.
- ✅ Does not close residual `Semantics_L1.v` axioms via proof tricks —
Phase 3a adds NEW infrastructure orthogonal to legacy admits.
- ✅ Does not follow pre-2026-05-26 closure plans.
- ✅ Works per-layer (L1 infrastructure → L2 preservation closure
downstream).
- ✅ Modality `m` preserved (cannot vary like Phase 1's ground lemma —
body's modality matches conclusion's).
- ✅ Context `G` preserved (body typed in `ctx_extend G T1`).

## Build

`just -f formal/Justfile all` — Rocq 9.1.1 / Coq 8.18.x.

\`\`\`
COQC Syntax.v
COQC Typing.v
COQC Modality.v
COQC TypingL1.v
COQC Semantics.v
COQC Semantics_L1.v   ← contains the new lemma
COQC Counterexample.v
COQC Echo.v
COQC TypingL2.v
COQC L4.v
\`\`\`

Zero errors, zero new admits.

## Diff

- \`formal/Semantics_L1.v\` +60 (lemma + 35-line docstring)

## Refs

Refs hyperpolymath/standards#124 (estate proof-debt epic)
Refs hyperpolymath/standards#134 (ephapax sub-issue)
Refs \`formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md\` Phase 3

## Phase ladder

- ✅ Phase 1 — \`ground_nonlinear_retype_l1_m\` (#219)
- ✅ Phase 2 — \`subst_typing_gen_l1_m_ground_nonlinear\` + helpers
(#220)
- ✅ Phase 3a — \`tfuneff_lambda_retype_l1_m\` ← **this PR**
- ⏳ Phase 3b — \`subst_typing_gen_l1_m_tfuneff\` (extend subst to
TFunEff substituends)
- ⏳ Phase 4 — close \`preservation_l2\` β-case using Phases 1-3
- ⏳ Phase 5 (deferred) — compound non-linear values

## Test plan

- [x] Toolchain build green (\`just -f formal/Justfile all\`)
- [x] No new \`Admitted.\`, no new \`Axiom\`
- [x] GPG-signed commit

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

formal/Semantics_L1.v

@@ -1217,6 +1217,66 @@ Proof.
   - (* v = EI32 n, T = TBase TI32 *) apply T_I32_L1.
 Qed.
 
+(** TFunEff lambda retype across [R → R'] under [R' ⊆ R_in].
+
+    For values typed at [TFunEff T1 T2 R_in R_out], the lambda's body
+    is typed at [R_in] (carried in the type, independent of the outer
+    [R]). The outer [R] enters the typing rule only through the side
+    condition [forall r, In r R -> In r R_in]. Re-typing at any [R']
+    reduces to discharging the analogous side condition
+    [forall r, In r R' -> In r R_in].
+
+    Two value-shape × typing-rule cases survive [inversion]:
+    [T_Lam_L1_Linear_Eff] and [T_Lam_L1_Affine_Eff]. Both produce
+    [TFunEff …] in the conclusion; the legacy [T_Lam_L1_Linear] and
+    [T_Lam_L1_Affine] rules produce [TFun …] and are discharged
+    automatically by [inversion]'s constructor-conclusion equation.
+    Non-lambda value shapes ([EUnit] / [EBool] / [EI32] / [EPair] /
+    [EInl] / [EInr] / [ELoc] / [EBorrow] / [EEcho]) are typed at base /
+    product / sum / borrow / region / echo types — all distinct from
+    [TFunEff] — and discharge identically.
+
+    The modality [m] is preserved across the retype: [T_Lam_L1_*_Eff]'s
+    conclusion modality must match the body's typing modality, so
+    unlike [ground_nonlinear_retype_l1_m] we cannot vary [m]. The
+    context [G] is also preserved: the body is typed in [ctx_extend G T1]
+    and varying outer [G] would require analogous machinery for context
+    weakening that is out of scope here.
+
+    Used by Phase D slice 4 Phase 3b (subst-lemma extension to TFunEff
+    lambda substituends) — any β-reduction with [T1 = TFunEff …] feeds
+    a lambda whose typing must be re-stated at sub-expression-internal
+    region environments inside the substitution lemma's [ebody].
+
+    Refs [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md] Phase 3.
+
+    Orthogonal to legacy [preservation] in [Semantics.v]: this lemma
+    adds NEW infrastructure constrained to the post-redesign
+    [has_type_l1] judgment carrying the modality parameter [m]. It
+    does not extend or patch [Semantics.v]. *)
+Lemma tfuneff_lambda_retype_l1_m :
+  forall (m : Modality) (R R' : region_env) (G : ctx)
+         (v : expr) (T1 T2 : ty) (R_in R_out : region_env),
+    is_value v ->
+    has_type_l1 m R G v (TFunEff T1 T2 R_in R_out) R G ->
+    (forall r, In r R' -> In r R_in) ->
+    has_type_l1 m R' G v (TFunEff T1 T2 R_in R_out) R' G.
+Proof.
+  intros m R R' G v T1 T2 R_in R_out Hval Ht HR'.
+  destruct Hval as
+    [ | b | n
+    | T0 e0 | v1 v2 Hv1 Hv2
+    | T0 v0 Hv0 | T0 v0 Hv0
+    | l r
+    | v0 Hv0
+    | T0 v0 Hv0 ];
+    inversion Ht; subst.
+  - (* v = ELam T0 e0, T_Lam_L1_Linear_Eff *)
+    eapply T_Lam_L1_Linear_Eff; [exact HR' | eassumption].
+  - (* v = ELam T0 e0, T_Lam_L1_Affine_Eff *)
+    eapply T_Lam_L1_Affine_Eff; [exact HR' | eassumption].
+Qed.
+
 (** Ground non-linear values are closed terms — they contain no
     de Bruijn variables, so de Bruijn [shift] is the identity on them.