proof(L2 Phase 2 / Phase D slice 2): T_Lam_L1_*_Eff rules + cascade (#204)

## Summary
- Adds `T_Lam_L1_Linear_Eff` + `T_Lam_L1_Affine_Eff` to `TypingL1.v`
typing effect-typed lambda values formed via `TFunEff T1 T2 R_in R_out`
(slice 1, PR #200).
- Side condition `forall r, In r R -> In r R_in` bridges outer/inner
envs, making `subst_typing_gen_l1_m` and
`region_shrink_preserves_typing_l1_gen_m` close.
- 3 inductive lemma cascades extended (~35 lines).

## Design (per formal/PHASE-D-REDESIGN.md + 2026-05-28 refinement)
R_in ⊇ R reading: body has access to at least formation regions,
possibly more. Balances:
- Substitution: Hregv : In rv R → In rv R_in via side condition.
- Env-shrinkage: TFunEff contains R_in (not outer R), preserved under
outer R shrinkage.

## Not in this PR
- T_App_L1_Eff + TFunEff_count_monotone → slice 3
- preservation_l1 lambda-rigidity closure → slice 4
- Phase B + Phase C re-attempts → slice 5

## Test plan
- [x] coqc 8.18.0 10/10 .v rebuild clean
- [x] Admit budget preserved (7 + 1 legacy = baseline)
- [x] Zero new Axiom; GPG-signed

🤖 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

@@ -473,6 +473,15 @@ Proof.
     apply T_Lam_L1_Linear. eapply IHHt; auto.
   - (* T_Lam_L1_Affine *)
     eapply T_Lam_L1_Affine. eapply IHHt; auto.
+  - (* T_Lam_L1_Linear_Eff — body's R_in is separate from outer R, but
+       the side condition [forall r, In r R -> In r R_in] survives
+       outer shrinkage (smaller outer R ⊆ original R ⊆ R_in). The body
+       typing at R_in is unchanged. *)
+    eapply T_Lam_L1_Linear_Eff; [|eassumption].
+    intros r0 Hin0. apply H. eapply remove_first_subset. exact Hin0.
+  - (* T_Lam_L1_Affine_Eff — same pattern. *)
+    eapply T_Lam_L1_Affine_Eff; [|eassumption].
+    intros r0 Hin0. apply H. eapply remove_first_subset. exact Hin0.
   - (* T_App_L1 *)
     destruct Hfree as [Hf1 Hf2].
     eapply T_App_L1; [eapply IHHt1; auto | eapply IHHt2; auto].
@@ -1002,6 +1011,13 @@ Proof.
   (* T_Lam_L1_Affine *)
   - assert (IH := IHHtype (S k) T_new ltac:(simpl; lia)).
     simpl in IH. eapply T_Lam_L1_Affine. exact IH.
+  (* T_Lam_L1_Linear_Eff — side condition + body via IH on (S k) shift.
+     The side condition is shift-invariant. *)
+  - assert (IH := IHHtype (S k) T_new ltac:(simpl; lia)).
+    simpl in IH. eapply T_Lam_L1_Linear_Eff; [exact H | exact IH].
+  (* T_Lam_L1_Affine_Eff — same. *)
+  - assert (IH := IHHtype (S k) T_new ltac:(simpl; lia)).
+    simpl in IH. eapply T_Lam_L1_Affine_Eff; [exact H | exact IH].
   (* T_App_L1 *)
   - eapply T_App_L1; [apply IHHtype1; assumption|].
     apply IHHtype2. assert (Hlen := typing_preserves_length_l1 _ _ _ _ _ _ _ Htype1). lia.
@@ -1459,6 +1475,25 @@ Proof.
       simpl; try eassumption; try reflexivity.
     apply loc_retype_at_R_l1_m. exact Hregv.
 
+  (* T_Lam_L1_Linear_Eff — body's R = R_in (separate from outer R), but
+     the side condition [H : forall r, In r R -> In r R_in] gives
+     In rv R_in from Hregv : In rv R. The body then types the
+     substituted location at R_in. *)
+  - assert (u_out = u_in) by congruence; subst.
+    eapply T_Lam_L1_Linear_Eff; [exact H |].
+    destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]].
+    eapply (IHHtype (S k0) (TString rv) (ELoc lv rv) u_in);
+      simpl; try eassumption; try reflexivity.
+    apply loc_retype_at_R_l1_m. apply H. exact Hregv.
+
+  (* T_Lam_L1_Affine_Eff — same. *)
+  - assert (u_out = u_in) by congruence; subst.
+    eapply T_Lam_L1_Affine_Eff; [exact H |].
+    destruct (linear_value_is_loc_l1 _ _ _ _ Hv_type Hval Hlin) as [lv [rv [-> [-> Hregv]]]].
+    eapply (IHHtype (S k0) (TString rv) (ELoc lv rv) u_in);
+      simpl; try eassumption; try reflexivity.
+    apply loc_retype_at_R_l1_m. apply H. exact Hregv.
+
   (* T_App_L1 *)
   - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid].
     eapply T_App_L1.

formal/TypingL1.v

@@ -182,6 +182,52 @@ Inductive has_type_l1
       R ; ctx_extend G T1 |=L1[Affine] e : T2 -| R ; (T1, u) :: G ->
       R ; G               |=L1[Affine] ELam T1 e : TFun T1 T2 -| R ; G
 
+  (** ===== Phase D slice 2 — Effect-typed lambda rules =====
+
+      [T_Lam_L1_Linear_Eff] / [T_Lam_L1_Affine_Eff] parallel
+      [T_Lam_L1_Linear] / [T_Lam_L1_Affine] but record the body's
+      R-flow into the function type via [TFunEff T1 T2 R_in R_out]
+      (slice 1, PR #200; refined per [formal/PHASE-D-REDESIGN.md]).
+
+      **Design choice (2026-05-28 final):** the rule carries a
+      side condition [forall r, In r R -> In r R_in], i.e., the
+      body's input env [R_in] is a SUPERSET of the formation env
+      [R]. This makes:
+
+      * Substitution: any value at outer R has its region rv ∈ R;
+        side condition gives rv ∈ R_in, which is what the body
+        needs after substitution.
+      * Env-shrinkage lemmas: the type T = TFunEff T1 T2 R_in R_out
+        contains R_in (not the outer R). Shrinking outer R from R
+        to remove_first rr R preserves the side condition (smaller
+        R is still a subset of R_in).
+
+      Why not R_in = R (tighter)? That ties the type to the
+      formation env, breaking env-shrinkage lemmas (the type
+      changes when env shrinks). Why not R_in unconstrained? That
+      breaks substitution (the substituted value's region might
+      not be in R_in).
+
+      The R_in ⊇ R reading: "the body has access to AT LEAST the
+      formation regions, possibly more (declared up front)." Natural
+      and compositional. An explicit weakening for use at different
+      call-site Rs ships in slice 3 (T_App_L1_Eff).
+
+      Per the L3 wiring playbook (parallel-rule strategy): existing
+      [TFun]-typed programs continue to type via [T_Lam_L1_Linear] /
+      [T_Lam_L1_Affine] unchanged. New code uses these [_Eff] rules
+      to opt into effect-typed lambdas. *)
+
+  | T_Lam_L1_Linear_Eff : forall R G T1 T2 e R_in R_out,
+      (forall r, In r R -> In r R_in) ->
+      R_in ; ctx_extend G T1 |=L1[Linear] e : T2 -| R_out ; (T1, true) :: G ->
+      R ; G                  |=L1[Linear] ELam T1 e : TFunEff T1 T2 R_in R_out -| R ; G
+
+  | T_Lam_L1_Affine_Eff : forall R G T1 T2 e u R_in R_out,
+      (forall r, In r R -> In r R_in) ->
+      R_in ; ctx_extend G T1 |=L1[Affine] e : T2 -| R_out ; (T1, u) :: G ->
+      R ; G                  |=L1[Affine] ELam T1 e : TFunEff T1 T2 R_in R_out -| R ; G
+
   | T_App_L1 : forall m R R1 R2 G G' G'' e1 e2 T1 T2,
       R  ; G  |=L1[m] e1 : TFun T1 T2 -| R1 ; G' ->
       R1 ; G' |=L1[m] e2 : T1          -| R2 ; G'' ->