feat(L2): Phase D slice 4 Phase 4b — preservation_l2 β for ground-non-linear T1 (#233)

## Summary

Phase 4 continuation following PR #228's Phase 4a (linear T1). Closes
the \`T_App_L2_Eff\` β-case (\`S_App_Fun\` step) for ground-non-linear
T1 ∈ { \`TBase TUnit\`, \`TBase TBool\`, \`TBase TI32\` } via Phase 2's
\`subst_typing_gen_l1_m_ground_nonlinear\` (PR #220).

Two lemmas, mirroring #228's Linear pattern:

- **\`preservation_l2_app_eff_beta_ground_nonlinear_l1\`** — L1-level
kernel. Inversion on the lambda forces \`T_Lam_L1_*_Eff\` (TFun cases
discriminate); \`value_R_G_preserving_l1\` on the argument collapses
\`R_in\` / \`G''\` to \`R\` / \`G\`. The Linear case discharges the
\`|=L1\` (Linear) \`Hv_type\` premise directly with \`Harg\`; the Affine
case bridges via \`ground_nonlinear_retype_l1_m\` (cross-modality, same
R) since Phase 2's premise uses the Linear-only \`|=L1\` shorthand.

- **\`preservation_l2_app_eff_beta_ground_nonlinear\`** — 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). Defers to the L1 kernel and re-lifts via
\`L2_lift_l1\`.

Combined with PR #228's Phase 4a, this closes \`T_App_L2_Eff\` β for T1
∈ { **linear**, **ground-non-linear** }. Remaining open:
- **Phase 4c** (\`TFunEff T1\`) — blocked on Phase 3b, [issue
#225](#225).
- **Phase 4d** (compound: \`EPair\` / \`EInl\` / \`EInr\` / \`EEcho\`
with non-linear sub-components) — deferred to Phase 5 per
\`SUBST-LEMMA-GENERALIZATION-DESIGN.md\`.

## Build + assumption audit

\`\`\`
$ cd /tmp/ephapax-phase-4b/formal && just all
coq_makefile -f _CoqProject -o build.mk
make -f build.mk
COQDEP VFILES
COQC TypingL2.v
COQC L4.v
(exit 0)
\`\`\`

- Rocq 9.1.1 / Coq 8.18 clean rebuild across all 10 .v files.
- Zero new admits, zero new axioms.
- \`Print Assumptions preservation_l2_app_eff_beta_ground_nonlinear\`
shows only pre-existing axioms inherited transitively via
\`subst_typing_gen_l1_m_ground_nonlinear\` (PR #220's audit closed that
lemma under the global context).

## Net delta

- \`formal/TypingL2.v\`: +83 lines (one L1 kernel lemma + one L2 wrapper
lemma + ~30 line docstring).
- No other files touched.

## 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 (purely new
infrastructure).
- ✅ 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.

## Refs

- PR #220 — Phase 2 (\`subst_typing_gen_l1_m_ground_nonlinear\`)
- PR #228 — Phase 4a (linear T1 sibling)
- ephapax#225 — Phase 4c gating issue (TFunEff)
- formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 4
- formal/PRESERVATION-DESIGN.md §5.1

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

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

Author: hyperpolymath

formal/TypingL2.v

@@ -491,3 +491,86 @@ Proof.
        into the Type-sorted has_type_l2 goal is allowed. *)
     exfalso. inversion Hval.
 Qed.
+
+(** Phase D slice 4 Phase 4b — preservation_l2 β-case closure for
+    ground-non-linear T1.
+
+    Mirrors [preservation_l2_app_eff_beta_linear] (PR #228) but uses
+    Phase 2's [Semantics_L1.subst_typing_gen_l1_m_ground_nonlinear]
+    for the L1 substitution step. Covers T1 ∈ { TBase TUnit,
+    TBase TBool, TBase TI32 } — ground values whose typing is
+    R-irrelevant and modality-polymorphic, so they bridge across the
+    Linear-only [|=L1] premise of the Phase 2 lemma via
+    [ground_nonlinear_retype_l1_m] (Phase 1).
+
+    Combined with PR #228's [preservation_l2_app_eff_beta_linear],
+    this closes the [T_App_L2_Eff] β-case for T1 ∈ { linear,
+    ground-non-linear }. Phase 4c (TFunEff T1) and Phase 4d
+    (compound non-linear) remain open — see issue #225 / Phase 5
+    respectively.
+
+    Refs [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md] Phase 4,
+    [PRESERVATION-DESIGN.md §5.1]. *)
+
+Lemma preservation_l2_app_eff_beta_ground_nonlinear_l1 :
+  forall m R R1 G G' G'' v2 T1 T2 R_in R_out ebody,
+    is_value v2 ->
+    is_ground_nonlinear_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 Hgrd Hlam Harg.
+  inversion Hlam; subst.
+  - (* T_Lam_L1_Linear_Eff: m = Linear; body at R_in / (T1,false)::G'' →
+       R_out / (T1,true)::G''. Harg : has_type_l1 Linear R G v2 T1 R G
+       (after value_R_G_preserving_l1). Matches Phase 2's [|=L1]
+       premise directly. *)
+    destruct (value_R_G_preserving_l1 _ _ _ _ _ _ _ Hval Harg) as [<- <-].
+    eapply subst_typing_gen_l1_m_ground_nonlinear with
+      (k := 0) (u_in := false)
+      (Gin := (T1, false) :: G'')
+      (Gout := (T1, true) :: G'').
+    + unfold ctx_extend in *. eassumption.
+    + reflexivity.
+    + exact Hval.
+    + exact Hgrd.
+    + exact Harg.
+    + reflexivity.
+  - (* T_Lam_L1_Affine_Eff: m = Affine; bridge Harg (Affine) to Linear
+       via [ground_nonlinear_retype_l1_m] (cross-modality at same R). *)
+    destruct (value_R_G_preserving_l1 _ _ _ _ _ _ _ Hval Harg) as [<- <-].
+    eapply subst_typing_gen_l1_m_ground_nonlinear with
+      (k := 0) (u_in := false)
+      (Gin := (T1, false) :: G'')
+      (Gout := (T1, _) :: G'').
+    + unfold ctx_extend in *. eassumption.
+    + reflexivity.
+    + exact Hval.
+    + exact Hgrd.
+    + eapply ground_nonlinear_retype_l1_m;
+        [exact Hval | exact Hgrd | exact Harg].
+    + reflexivity.
+Qed.
+
+Lemma preservation_l2_app_eff_beta_ground_nonlinear :
+  forall m R R1 G G' G'' v2 T1 T2 R_in R_out ebody,
+    is_value v2 ->
+    is_ground_nonlinear_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 Hgrd Hlam Harg.
+  (* Lambda inversion: only [L2_lift_l1] survives ([T_App_L2_Eff]'s
+     expression is [EApp _ _], not [ELam _ _]). *)
+  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_ground_nonlinear_l1; eassumption.
+  - exfalso. inversion Hval.
+Qed.