feat(L2): T_App_L2_Eff — Phase D slice 3 option 5a code lands (#209)

## Summary

Phase D slice 3 implementation under option 5a (owner-picked in PR
#208). Adds `T_App_L2_Eff` as a sibling constructor to `L2_lift_l1` in
`has_type_l2`, moving the elimination form of effect-typed `TFunEff`
lambdas out of L1 and into L2 per `PRESERVATION-DESIGN.md` §5.1 lines
468-474.

## What changed

- **New constructor `T_App_L2_Eff`** in `formal/TypingL2.v` after
`L2_lift_l1`. Threading: `e1 : (R → R1)` produces an effect-typed
lambda; `e2 : (R1 → R_in)` evaluates the argument matching the lambda's
declared input env; `EApp e1 e2 : (R → R_out)` consumes the body's
declared output region. No side condition at elimination (the `(forall
r, In r R -> In r R_in)` side condition already lives on
`T_Lam_L1_*_Eff` slice 2).

- **`project_l2_to_l1` refactored to option-return.** `T_App_L2_Eff`
cases have no L1 counterpart by design — that is the architectural point
of option 5a. The comment block documents the migration path for
callers.

- **`weaken_modality` rewritten by structural induction.** Old: project
to L1, weaken at L1, lift back. New: case on the L2 derivation;
`L2_lift_l1` lifts via `linear_to_affine`; `T_App_L2_Eff` weakens the
two sub-derivations recursively and reconstructs at Affine.

## Verification

- `coqc 8.18.0` full `formal/` build clean (10 .v files)
- Zero new `Admitted` / `Axiom` / `admit.` in `TypingL2.v`
- `Print Assumptions weaken_modality` → `Closed under the global
context`
- `Print Assumptions weaken_modality_le` → `Closed under the global
context`
- `Print Assumptions weaken_modality_le_strict_is_weaken_modality` →
`Closed under the global context`

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

- ✅ `Semantics.v` untouched (legacy `preservation` left as `Admitted`)
- ✅ `Typing.v` untouched (legacy judgment intact for `Counterexample.v`)
- ✅ `Counterexample.v` untouched
- ✅ No new admits or axioms anywhere
- ✅ Cross-layer fix per `PRESERVATION-DESIGN.md` §5.1 — not a
single-layer patch

## Companion docs

- `formal/PHASE-D-REDESIGN.md` slice 3 sub-sub-addendum (landed in #208)
- `.machine_readable/6a2/STATE.a2ml` phase flipped `owner-escalation →
implementation` (#208)

## What this does NOT close

`preservation_l1` as currently stated cannot Qed under option 5a alone —
slice 4a (TFunEff path) closes by inversion vacuity at L1, but slice 4b
(legacy `TFun` body-R-rigidity) carries forward into `preservation_l2`
via L1 importation as honest inherited debt.

## Next slices (out of scope here)

1. State `preservation_l2` over `has_type_l2`. Effect-typed paths get
the slice 4a case for free; legacy `TFun` paths carry forward the L1
admit via `L2_lift_l1`.
2. Phase B Slice 1 (TEcho linearity wire) + Phase C (list-vs-multiset
bridge) unlock once `preservation_l2` lands.

## Test plan

- [x] `coqc 8.18.0` build clean
- [x] `Print Assumptions` confirms zero axioms on new code
- [x] Diff scoped to `formal/TypingL2.v` only (no Makefile noise)
- [ ] CI green on merge

🤖 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

@@ -19,12 +19,14 @@
     Per design-doc §5 and the same "first slice" framing used for
     L3 (#166), this PR ships:
 
-    - The [has_type_l2] inductive shape — currently with a single
-      [L2_lift_l1] constructor that lifts any L1 derivation into the
-      L2 judgment at either mode. This is sound: per §5's
-      preservation table, "[Affine derivations are L1-safe by
-      weakening]" and Linear derivations are precisely the strict
-      L1 derivations.
+    - The [has_type_l2] inductive shape — with [L2_lift_l1] (lifts
+      any L1 derivation into the L2 judgment at either mode) and
+      [T_App_L2_Eff] (effect-typed application; the elimination form
+      of [TFunEff] lambdas, moved out of L1 per option 5a / Phase D
+      slice 3 / [PHASE-D-REDESIGN.md] slice 3 sub-sub-addendum). The
+      L2_lift_l1 case is sound: per §5's preservation table,
+      "[Affine derivations are L1-safe by weakening]" and Linear
+      derivations are precisely the strict L1 derivations.
 
     - [weaken_modality] — the headline §5 lemma, Qed. In this
       skeleton the proof is a single induction; future PRs will add
@@ -88,7 +90,29 @@ Inductive has_type_l2
   | L2_lift_l1 :
       forall m R G e T R' G',
         TypingL1.has_type_l1 m R G e T R' G' ->
-        has_type_l2 m R G e T R' G'.
+        has_type_l2 m R G e T R' G'
+  (** [T_App_L2_Eff] — effect-typed application (Phase D slice 3,
+      option 5a). The elimination form for [TFunEff] lambdas. Lives
+      at L2 because effect-typed application is an effect-semantic
+      operation (consuming [R_in / R_out] annotations meaningfully)
+      and the canonical home for it is the typing-layer judgment per
+      [PRESERVATION-DESIGN.md] §5.1.
+
+      Threading: [e1] produces an effect-typed lambda value at
+      ([R → R1]). [e2] evaluates the argument, threading
+      [R1 → R_in] (the lambda's declared input env). The body runs
+      [R_in → R_out] per the type, so the whole [EApp] consumes
+      [R → R_out].
+
+      Side condition: none at elimination. The intro side condition
+      [(forall r, In r R -> In r R_in)] (T_Lam_L1_*_Eff slice 2)
+      already ensures formation-time region availability; at the
+      call site [e2] supplies [R_in] explicitly via its output env. *)
+  | T_App_L2_Eff :
+      forall m R R1 G G' G'' e1 e2 T1 T2 R_in R_out,
+        has_type_l2 m R  G  e1 (TFunEff T1 T2 R_in R_out) R1   G' ->
+        has_type_l2 m R1 G' e2 T1                         R_in G'' ->
+        has_type_l2 m R  G  (EApp e1 e2) T2               R_out G''.
 
 (** Notation following the Agda upstream [_;_⊢_ℓ_:_-|_;_]. *)
 
@@ -114,16 +138,27 @@ Definition lift_l1_to_affine
   has_type_l2 Affine R G e T R' G' :=
   L2_lift_l1 Affine R G e T R' G' H.
 
-(** Projection: extract the underlying L1 derivation from an L2 one.
-    Witnesses that the L2 skeleton is a strict extension — no
-    information loss vs L1. *)
+(** Partial projection: extract the underlying L1 derivation from
+    an L2 one when (and only when) the L2 derivation is a lift.
+
+    Post-slice-3 (option 5a), [has_type_l2] also carries
+    [T_App_L2_Eff], which has no L1 counterpart — effect-typed
+    application is L2-only by design. The projection is therefore
+    [option]-valued: [Some H1] for [L2_lift_l1] cases, [None] for
+    the [T_App_L2_Eff] case.
+
+    Callers that previously assumed totality (e.g. the old
+    [weaken_modality] proof) must instead do structural induction
+    on the L2 derivation; see [weaken_modality] below for the
+    updated pattern. *)
 
 Definition project_l2_to_l1
   {m R G e T R' G'}
   (H : has_type_l2 m R G e T R' G') :
-  TypingL1.has_type_l1 m R G e T R' G' :=
+  option (TypingL1.has_type_l1 m R G e T R' G') :=
   match H with
-  | L2_lift_l1 _ _ _ _ _ _ _ H1 => H1
+  | L2_lift_l1 _ _ _ _ _ _ _ H1 => Some H1
+  | T_App_L2_Eff _ _ _ _ _ _ _ _ _ _ _ _ _ _ => None
   end.
 
 (** ===== Headline §5 lemma: Linear ⇒ Affine weakening =====
@@ -136,15 +171,29 @@ Definition project_l2_to_l1
     one constructor case; future mode-specific constructors will
     introduce mode-switch cases. *)
 
+(** Post-slice-3 (option 5a), the proof is by structural induction
+    on the L2 derivation. The [L2_lift_l1] case lifts via
+    [linear_to_affine]; the [T_App_L2_Eff] case weakens the two
+    sub-derivations recursively and reconstructs by [T_App_L2_Eff]
+    at [Affine]. *)
+
 Theorem weaken_modality :
   forall {R G e T R' G'},
     has_type_l2 Linear R G e T R' G' ->
     has_type_l2 Affine R G e T R' G'.
 Proof.
   intros R G e T R' G' H.
-  apply lift_l1_to_affine.
-  apply TypingL1.linear_to_affine.
-  exact (project_l2_to_l1 H).
+  remember Linear as m eqn:Hm.
+  induction H as
+    [ m' R0 G0 e0 T0 R0' G0' H1
+    | m' R0 R1 G0 G0' G0'' e1 e2 T1 T2 R_in R_out He1 IHe1 He2 IHe2 ];
+    subst m'.
+  - apply lift_l1_to_affine.
+    apply TypingL1.linear_to_affine.
+    exact H1.
+  - eapply T_App_L2_Eff.
+    + apply IHe1; reflexivity.
+    + apply IHe2; reflexivity.
 Qed.
 
 (** Idempotence at [Affine]: an Affine derivation re-weakened to