feat(L2): Phase D slice 4 Phase 4a — preservation_l2_app_eff_beta_linear + hotfix duplicate tfuneff_lambda_retype_l1_m (#228)

## Summary

Two L2-layer additions and one hotfix for a parallel-session merge
collision.

### Phase 4a — β-case closure for linear T1

The `T_App_L2_Eff` β-case (S_App_Fun step) closes for linear T1 via the
existing m-indexed substitution lemma `subst_typing_gen_l1_m`. Pure new
infrastructure orthogonal to legacy admits.

- **`preservation_l2_app_eff_beta_linear_l1`** — L1-level kernel. Takes
inverted T_App_L2_Eff premises (lambda formed at `TFunEff` + value
argument typed at `T1`) and produces the post-β L1 typing of `subst 0 v2
ebody`. Inversion on the lambda forces `T_Lam_L1_*_Eff`;
`value_R_G_preserving_l1` on the argument collapses `R_in` / `G''` to
`R` / `G`.
- **`preservation_l2_app_eff_beta_linear`** — L2 wrapper. Inverts both
`has_type_l2` hypotheses through `L2_lift_l1` (the `T_App_L2_Eff`
discriminate cases: lambda's head is `ELam` not `EApp`; argument is a
value so cannot be `EApp`). Defers to the L1 kernel and re-lifts via
`L2_lift_l1`.
- **`linear_value_retype_l1_m`** — small local m-poly helper. Linear
values at L1 are exactly locations (`T_Loc_L1` is m-polymorphic); retype
at any `m'`. Needed because `subst_typing_gen_l1_m`'s premise 5 uses the
bare `|=L1` notation which is Linear-mode-only, so the Affine branch
must re-derive the substituend at Linear.

**Phase 4 follow-ons** (NOT in this PR):
- 4b: ground-non-linear `T1` via Phase 2's
`subst_typing_gen_l1_m_ground_nonlinear`.
- 4c: TFunEff non-linear `T1` — blocked on Phase 3b (issue #225).
- 4d: compound non-linear — deferred to Phase 5.

These three helpers compose with `preservation_l2_via_l1` toward
eventual closure of `preservation_l2` over the full `has_type_l2`
judgment.

### Hotfix — duplicate \`tfuneff_lambda_retype_l1_m\`

PRs #223 and #224 (parallel-session merges 2026-05-30) both added
\`tfuneff_lambda_retype_l1_m\` with different argument orders, leaving
main with a Coq "already exists" compile error. CI didn't catch it
because there's no Coq build job in the gates — this PR surfaces that
gap as a seam observation (Coq is the only merge oracle for proof PRs,
but is not part of CI).

Kept the chronologically-first definition (PR #223: \`(Hval, Ht, HR')\`
arg order) and removed the second (PR #224: \`(Hval, Hsub, Ht)\`). Both
proofs were semantically equivalent. No external call sites existed yet,
so argument order is free choice.

## Build + assumption audit

- coqc 8.18.0 clean rebuild across all 10 .v files.
- \`Print Assumptions preservation_l2_app_eff_beta_linear\` shows only
the pre-existing \`region_liveness_at_split_l1_gen\` axiom inherited
transitively via \`subst_typing_gen_l1_m\`. **No new admits/axioms.**
- \`Print Assumptions linear_value_retype_l1_m\` shows "Closed under the
global context" — fully axiom-free.

## Owner-directive compliance (CLAUDE.md 2026-05-27)

- ✅ Does not close \`Theorem preservation\` in \`formal/Semantics.v\`.
- ✅ Does not extend \`Semantics.v\` / \`Typing.v\` /
\`Counterexample.v\`.
- ✅ Does not close any residual \`Semantics_L1.v\` admit (the
duplicate-removal is mechanical de-duplication, not proof closure).
- ✅ Works per-layer: L1 kernel + L2 wrapper, both at the post-redesign
m-indexed \`has_type_l1\` judgment.
- ✅ Reads \`PRESERVATION-DESIGN.md\` /
\`SUBST-LEMMA-GENERALIZATION-DESIGN.md\` first.
- ✅ No new \`Axiom\` or \`Admitted\` markers.

## Test plan

- [x] \`coqc -R . Ephapax\` rebuild across all 10 .v files, zero errors
/ warnings.
- [x] \`Print Assumptions\` audit shows no new axioms beyond the
pre-existing L1 \`region_liveness_at_split_l1_gen\`.
- [x] Duplicate hotfix verified by \`grep -n
"tfuneff_lambda_retype_l1_m\b" Semantics_L1.v\` showing single hit.

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

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -6,8 +6,8 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Phase D slice 4 Phase 3b — extend the substitution lemma to cover `T1 = TFunEff …` lambdas as substituends. Phase 3a (this slot's predecessor) shipped `is_tfuneff_ty` + `tfuneff_lambda_retype_l1_m`; the substitution extension was DESCOPED to 3b after structural analysis. The obstacle: a TFunEff value's retype across `R -> R'` requires the side condition `forall r, In r R' -> In r R_in_arg`, where `R_in_arg` is FIXED by the value's type. The substitution lemma's compound cases need to retype the substituted value at threaded `R_n` values that arise inside `e`. `T_Region_L1` firings inside `e` introduce fresh regions `r ∉ R_outer`; freshness wrt the threaded R does NOT imply membership in R_in_arg. Three candidate solutions for 3b: (a) require an explicit syntactic side condition on `e` constraining `regions_introduced_by(e) ⊆ R_in_arg`; (b) supply Hv_type universally R-quantified with a side condition discharged per-case; (c) restrict to terms with no internal `T_Region_L1` firings. Choose after Phase 4 prototyping reveals the actual use shape of `subst 0 varg ebody` where ebody is `vlam`'s body. After Phase 3b, Phase 4 closes `preservation_l2`'s `T_App_L2_Eff` β-case for: (a) linear T1 via existing `subst_typing_gen_l1_m`; (b) ground non-linear T1 via Phase 2's `subst_typing_gen_l1_m_ground_nonlinear`; (c) TFunEff non-linear T1 via Phase 3b; (d) compound non-linear T1 deferred to Phase 5. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted` to close cases; no touching `Semantics.v`/`Typing.v`/`Counterexample.v`; no closure of residual `Semantics_L1.v` admits via this work — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority."
-last_action: "Phase D slice 4 Phase 3a LANDED (2026-05-30): `is_tfuneff_ty` predicate added to `formal/Syntax.v` (mirrors `is_ground_nonlinear_ty`'s shape, returns true for `TFunEff _ _ _ _` only). `tfuneff_lambda_retype_l1_m` lemma added to `formal/Semantics_L1.v` (after `ground_nonlinear_value_shift_id_l1`). Signature: `(m, R, G) -> (m, R', G)` retype under side condition `forall r, In r R' -> In r R_in`, where `R_in` is part of the value's type `TFunEff T1 T2 R_in R_out`. Proof inverts on `is_value v`, then on `Ht`; non-ELam value forms discriminate (their typing rules produce non-TFunEff types); ELam at TFunEff resolves to either `T_Lam_L1_Linear_Eff` or `T_Lam_L1_Affine_Eff` (both `T_Lam_L1_Linear` / `T_Lam_L1_Affine` discriminate via TFun ≠ TFunEff). Re-applies the appropriate _Eff rule with the supplied side condition; body typing carries via `eassumption`. Lemma is m-monomorphic (cross-modality TFunEff retype would require `linear_to_affine` over the body — not needed for Phase 4). Phase 3b (substitution-lemma extension) DESCOPED from this PR after structural analysis revealed `T_Region_L1` fresh-region obstacle: the threaded R inside `e` can grow beyond R_in_arg via fresh-region introduction, and the retype side condition fails for arbitrary fresh regions. 3b candidate solutions in next_action. Coqc 8.18.0 clean rebuild across all 10 .v files. Zero new admits/axioms. `Semantics.v`/`Typing.v`/`Counterexample.v` untouched. Phase 3a is clean infrastructure usable in 3b and 4."
+next_action: "Phase D slice 4 Phase 4b — ground-non-linear T1 path for the `T_App_L2_Eff` β-case (uses Phase 2's `subst_typing_gen_l1_m_ground_nonlinear`). Then Phase 4c (TFunEff non-linear T1, blocked on Phase 3b per issue #225) and Phase 4d (compound, deferred to Phase 5). Phase 4a (this slot's predecessor) shipped `preservation_l2_app_eff_beta_linear_l1` + `preservation_l2_app_eff_beta_linear` in TypingL2.v, closing the β-case for linear T1. Phase 3b is still parked at issue #225 with three candidate solutions; Phase 4a prototyping confirmed the substitution shape used for linear T1 (k=0, raw cons in Gin/Gout, m-poly via `linear_value_retype_l1_m` for the Affine branch). For 3b, the actual subst shape will mirror Phase 4a's but with the value being a TFunEff lambda — the substitution premise will need a TFunEff-typed substituend at the threaded R, with the side condition propagating through. Recommend prototyping Phase 4c next (it forces 3b's design hand). Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted` to close cases; no touching `Semantics.v`/`Typing.v`/`Counterexample.v`; no closure of residual `Semantics_L1.v` admits via this work — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority."
+last_action: "Phase D slice 4 Phase 4a LANDED (2026-05-30, this PR): `preservation_l2_app_eff_beta_linear_l1` + `preservation_l2_app_eff_beta_linear` added to `formal/TypingL2.v`. The L1-level kernel takes inverted T_App_L2_Eff premises (a TFunEff lambda + a value argument typed at linear T1) and produces the post-β L1 typing via `subst_typing_gen_l1_m` at k=0. The L2 wrapper inverts both has_type_l2 hypotheses through L2_lift_l1 (T_App_L2_Eff discriminates: lambda's head is ELam not EApp; argument is a value so cannot be EApp). Two structural reductions inside the kernel: inversion on Hlam forces T_Lam_L1_*_Eff (the only formation rules producing TFunEff), exposing body typing at R_in; `value_R_G_preserving_l1` on Harg collapses R_in→R, G''→G. Then subst at k=0 with raw cons in the `with` clause (ctx_extend was too opaque for unification of remove_at 0 _ = G'') — and for the Affine branch, the linear v2 is re-derived at Linear mode via local helper `linear_value_retype_l1_m` (because subst_typing_gen_l1_m's premise 5 uses the bare `|=L1` notation which is Linear-mode-only). The same PR hotfixes a duplicate `tfuneff_lambda_retype_l1_m` from PR #223 + PR #224 (parallel-session merge collision); kept the chronologically-first definition (Hval, Ht, HR' arg order) and removed the second. Coqc 8.18.0 clean rebuild across all 10 .v files. Zero new admits/axioms (Print Assumptions confirms only the pre-existing `region_liveness_at_split_l1_gen` axiom inherited via `subst_typing_gen_l1_m`). `Semantics.v`/`Typing.v`/`Counterexample.v` untouched. Phase 4a is clean infrastructure composable with `preservation_l2_via_l1` toward full `preservation_l2` over has_type_l2."
 updated: 2026-05-30T00:00:00Z
 
 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):

formal/TypingL2.v

@@ -71,6 +71,9 @@
       [T_Lam_*_L2]. L2 Phase 2 + L3 Phase 3 jointly close the L1
       gap. *)
 
+Require Import Coq.Lists.List.
+Import ListNotations.
+
 From Ephapax Require Import Syntax Typing TypingL1 Modality Semantics Semantics_L1.
 
 (** ===== The L2 judgment (skeleton) =====
@@ -352,3 +355,139 @@ Proof.
   intros m mu R e mu' R' e' Hstep G T R_final G' H1.
   eapply preservation_l2_via_l1; eassumption.
 Qed.
+
+(** ===== Phase D slice 4 Phase 4a — β-case closure for linear T1 =====
+
+    The [T_App_L2_Eff] β-case (S_App_Fun step) closes for linear [T1]
+    via the existing m-indexed substitution lemma
+    [subst_typing_gen_l1_m]. This slice ships pure new infrastructure
+    orthogonal to the legacy admits; it does not patch [Semantics.v],
+    [Typing.v], [Counterexample.v], or close any residual
+    [Semantics_L1.v] marker.
+
+    Structure:
+
+    - [preservation_l2_app_eff_beta_linear_l1] — the L1-level kernel.
+      Takes the inverted T_App_L2_Eff premises (a lambda formed at
+      [TFunEff] + a value argument typed at [T1]) and produces the
+      post-β L1 typing of [subst 0 v2 ebody]. Two structural reductions
+      inside: inversion on the lambda derivation forces [T_Lam_L1_*_Eff]
+      (the only formation rules producing [TFunEff] types), exposing
+      the body typing at [R_in]; [value_R_G_preserving_l1] on the
+      argument forces [R_in = R1 = R] and [G'' = G' = G], collapsing
+      the threaded environments to a uniform [R / G] triple. Then
+      [subst_typing_gen_l1_m] at [k = 0] fires with [is_linear_ty T1].
+
+    - [preservation_l2_app_eff_beta_linear] — the L2 wrapper. Inverts
+      both [has_type_l2] hypotheses through [L2_lift_l1] (the
+      [T_App_L2_Eff] cases discriminate: the lambda's head is [ELam]
+      not [EApp], and the argument is a value so it cannot be [EApp]),
+      then defers to the L1 kernel and re-lifts via [L2_lift_l1].
+
+    Phase 4 follow-ons (not in this PR):
+    - 4b: ground-non-linear [T1] via Phase 2's
+      [subst_typing_gen_l1_m_ground_nonlinear].
+    - 4c: [TFunEff] non-linear [T1] — blocked on Phase 3b
+      (issue #225, the substitution-lemma extension for [TFunEff]
+      lambdas as substituends).
+    - 4d: compound non-linear (EPair / EInl / EInr / EEcho) deferred
+      to Phase 5.
+
+    These three helpers compose with [preservation_l2_via_l1] (the
+    L2_lift_l1 case) toward eventual closure of [preservation_l2]
+    over the full [has_type_l2] judgment. *)
+
+(** Auxiliary: m-polymorphic retype for linear values. Linear values
+    at L1 are exactly locations (per [Semantics_L1.linear_value_is_loc_l1]),
+    and [T_Loc_L1] is m-polymorphic; the value retypes at any [m']
+    without further structure. Local to this file because the only
+    consumer is the Affine branch of
+    [preservation_l2_app_eff_beta_linear_l1] (the subst lemma's
+    [|=L1] premise is Linear-mode-only). *)
+
+Lemma linear_value_retype_l1_m :
+  forall m m' R G v T,
+    TypingL1.has_type_l1 m R G v T R G ->
+    is_value v ->
+    is_linear_ty T = true ->
+    TypingL1.has_type_l1 m' R G v T R G.
+Proof.
+  intros m m' R G v T Htype Hval Hlin.
+  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 Htype; subst; try discriminate Hlin.
+  apply T_Loc_L1; assumption.
+Qed.
+
+Lemma preservation_l2_app_eff_beta_linear_l1 :
+  forall m R R1 G G' G'' v2 T1 T2 R_in R_out ebody,
+    is_value v2 ->
+    is_linear_ty T1 = true ->
+    TypingL1.has_type_l1 m R  G  (ELam T1 ebody)
+                                 (TFunEff T1 T2 R_in R_out) R1 G' ->
+    TypingL1.has_type_l1 m R1 G' v2 T1 R_in G'' ->
+    TypingL1.has_type_l1 m R  G  (subst 0 v2 ebody) T2 R_out G''.
+Proof.
+  intros m R R1 G G' G'' v2 T1 T2 R_in R_out ebody Hval Hlin Hlam Harg.
+  inversion Hlam; subst.
+  - (* T_Lam_L1_Linear_Eff: body at R_in / (T1,false)::G'' → R_out / (T1,true)::G''
+       (R and G eliminated by inversion equalities; R_in and G'' remain. Use
+       raw cons (not [ctx_extend]) in the [with] clause so unification of
+       [remove_at 0 Gin = G''] does not stall on δ-unfolding.) *)
+    destruct (value_R_G_preserving_l1 _ _ _ _ _ _ _ Hval Harg) as [<- <-].
+    eapply subst_typing_gen_l1_m with
+      (k := 0) (u_in := false)
+      (Gin := (T1, false) :: G'')
+      (Gout := (T1, true) :: G'').
+    + (* body typing: H10 has [ctx_extend G'' T1] which is δ-equal to [(T1,false)::G''] *)
+      unfold ctx_extend in *. eassumption.
+    + reflexivity.
+    + exact Hval.
+    + exact Hlin.
+    + exact Harg.
+    + reflexivity.
+  - (* T_Lam_L1_Affine_Eff: body output is [(T1, u) :: G''] for some [u]
+       introduced by inversion. The subst lemma's [|=L1] premise is
+       Linear-mode-only, so Harg (Affine-typed) is re-derived at Linear
+       via [linear_value_retype_l1_m]. *)
+    destruct (value_R_G_preserving_l1 _ _ _ _ _ _ _ Hval Harg) as [<- <-].
+    eapply subst_typing_gen_l1_m with
+      (k := 0) (u_in := false)
+      (Gin := (T1, false) :: G'')
+      (Gout := (T1, _) :: G'').
+    + unfold ctx_extend in *. eassumption.
+    + reflexivity.
+    + exact Hval.
+    + exact Hlin.
+    + apply (linear_value_retype_l1_m Affine Linear); assumption.
+    + reflexivity.
+Qed.
+
+Lemma preservation_l2_app_eff_beta_linear :
+  forall m R R1 G G' G'' v2 T1 T2 R_in R_out ebody,
+    is_value v2 ->
+    is_linear_ty T1 = true ->
+    has_type_l2 m R  G  (ELam T1 ebody)
+                        (TFunEff T1 T2 R_in R_out) R1 G' ->
+    has_type_l2 m R1 G' v2 T1 R_in G'' ->
+    has_type_l2 m R  G  (subst 0 v2 ebody) T2 R_out G''.
+Proof.
+  intros m R R1 G G' G'' v2 T1 T2 R_in R_out ebody Hval Hlin Hlam Harg.
+  (* Lambda inversion: [T_App_L2_Eff]'s expression is [EApp _ _],
+     not [ELam _ _], so it discriminates; only [L2_lift_l1] remains. *)
+  inversion Hlam as [m0 R0 G0 e0 T0 R0' G0' Hlam_l1 | ]; subst.
+  (* Argument inversion: [v2] is a value, so the [T_App_L2_Eff] case
+     would force [v2 = EApp _ _], contradicting [Hval]. *)
+  inversion Harg as [m0' R0'' G0'' e0' T0' R0''' G0''' Harg_l1 | ]; subst.
+  - apply L2_lift_l1.
+    eapply preservation_l2_app_eff_beta_linear_l1; eassumption.
+  - (* T_App_L2_Eff case for Harg forces v2 = EApp _ _ but Hval : is_value v2.
+       [exfalso] switches to Prop so the Prop-elim of Hval (is_value : ... -> Prop)
+       into the Type-sorted has_type_l2 goal is allowed. *)
+    exfalso. inversion Hval.
+Qed.