feat(L1): Phase D slice 4 Phase 3a — tfuneff_lambda_retype_l1_m + is_tfuneff_ty (#224)

## Summary

- Ships the **retype lemma half** of Phase 3 per
`formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md`.
- Adds `is_tfuneff_ty` predicate (Syntax.v) mirroring
`is_ground_nonlinear_ty`.
- Adds `tfuneff_lambda_retype_l1_m` lemma (Semantics_L1.v): retype
TFunEff lambda value across `(m, R, G) → (m, R', G)` under side
condition `forall r, In r R' → In r R_in`.
- **Phase 3b (substitution-lemma extension) DESCOPED** to a follow-up PR
after structural analysis revealed the `T_Region_L1` fresh-region
obstacle. STATE.a2ml documents the three candidate solutions.

## Why split

`SUBST-LEMMA-GENERALIZATION-DESIGN.md` Phase 3 proposed two pieces
(retype + substitution extension). Walking the substitution proof
revealed: every retype across a threaded `R_n` inside the term `e`
demands `forall r, In r R_n → In r R_in_arg`, and `T_Region_L1` firings
inside `e` introduce fresh `r ∉ R_outer` — freshness wrt the threaded R
does **not** imply membership in the value-type's fixed `R_in_arg`.
Three candidate fixes (syntactic side condition on `e`; universal-R
Hv_type with per-case discharge; restrict to region-free terms) need
Phase 4 prototyping of the actual `subst 0 varg ebody` shape before
choosing. Phase 3a's retype lemma stands on its own as clean
infrastructure usable in 3b and Phase 4.

## Proof shape

`tfuneff_lambda_retype_l1_m`:
- `destruct Hval` (10 value-form cases)
- `inversion Ht; subst; try discriminate`
  - Non-ELam forms: types don't match TFunEff → `discriminate`.
- ELam at TFun (legacy rules `T_Lam_L1_Linear` / `T_Lam_L1_Affine`):
type mismatch TFun ≠ TFunEff → `discriminate`.
- ELam at TFunEff (`T_Lam_L1_Linear_Eff` / `T_Lam_L1_Affine_Eff`):
re-apply rule with new `Hsub`, body via `eassumption`.

Zero new admits, zero new axioms. Coqc 8.18.0 clean rebuild across all
10 .v files.

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

- ✅ No closure of legacy `preservation` in `Semantics.v` (untouched).
- ✅ No closure-support lemmas in `Semantics.v` (untouched).
- ✅ No closure of residual `Semantics_L1.v` admits — strictly NEW
orthogonal infrastructure.
- ✅ No patching `Typing.v` (untouched).
- ✅ No new `Admitted` / `Axiom`.
- ✅ Anti-pattern detector clean.

## Test plan

- [x] `coqc -Q . Ephapax` clean across all 10 .v files locally.
- [ ] CI green on `formal/` build job.

Refs: standards#134 (proof-debt epic), #220 (Phase 2), #213 (design
doc).

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -6,8 +6,8 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Phase D slice 4 Phase 3 — ship `tfuneff_lambda_retype_l1_m` per `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md` §'Phase 3'. Retype lemma for TFunEff-typed lambdas (`ELam T0 e` typed at `TFunEff T1 T2 R_in R_out`) under the side condition `forall r, In r R' -> In r R_in`. Extend the Phase 2 substitution lemma to cover `T1 = TFunEff …` lambdas as substituends. The TFun (non-Eff) lambda case has body-R-rigidity (same gap as legacy preservation_l1 slice 4b) — explicitly OUT OF SCOPE for Phase 3 per design doc §'Open design questions' #2 (recommended: TFunEff only). After Phase 3, 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 3; (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 2 LANDED (2026-05-30): `subst_typing_gen_l1_m_ground_nonlinear` parallel substitution lemma added to `formal/Semantics_L1.v` mirroring `subst_typing_gen_l1_m`'s 28+ case structure for `is_ground_nonlinear_ty T1 = true`. Three key divergences from the linear lemma: (i) T_Var_Lin_L1 i=k0 → exfalso via `is_linear_ty Tsub = false` vs rule's premise `is_linear_ty T = true`; (ii) T_Var_Unr_L1 i=k0 → CONSTRUCTIVE case applying `ground_nonlinear_retype_l1_m` to lift Hv_type from Linear to active modality m; (iii) compound rules use `ground_nonlinear_retype_l1_m` directly (no `linear_value_is_loc_l1` / `loc_retype_at_R_l1_m` / `region_liveness_at_split_l1_gen` pipeline — ground retype takes any R, any G, any m). Phase 1's `ground_nonlinear_retype_l1_m` generalised in this PR to (m → m', R → R', G → G')-polymorphic (Phase 1 ships m-monomorphic R-only retype; Phase 2 needs the cross-modality cross-context bridge). New helper `ground_nonlinear_value_shift_id_l1` proves `shift c d v = v` for ground non-linear values; used to rewrite the `shift 0 1 vv` introduced by `subst`'s descent through term binders in T_Let_L1 / T_LetLin_L1 / T_Lam_L1_* (4 lambda rules) / T_Case_L1_* (2 case rules). Coqc 8.18.0 clean rebuild across all 10 .v files. Zero new admits/axioms. `Semantics.v`/`Typing.v`/`Counterexample.v` untouched. Phase 2 unblocks Phase 3 (TFunEff lambda retype) and Phase 4 (close preservation_l2 β-case for ground non-linear T1). Sibling-lemma approach preserves ~30 Qed downstreams of `subst_typing_gen_l1_m`."
+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."
 updated: 2026-05-30T00:00:00Z
 
 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):

formal/Semantics_L1.v

@@ -1308,6 +1308,79 @@ Proof.
     inversion Ht; subst; try discriminate Hgrd; reflexivity.
 Qed.
 
+(** TFunEff lambda retype lemma — Phase D slice 4 Phase 3 per
+    [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md].
+
+    A [TFunEff]-typed lambda value [ELam T0 e] is formed by either
+    [T_Lam_L1_Linear_Eff] or [T_Lam_L1_Affine_Eff] (per
+    [formal/TypingL1.v]). Both rules carry the side condition
+    [forall r, In r R -> In r R_in] at the formation env [R], and
+    type the body [e] at the BODY env [R_in] (which is part of the
+    function type [TFunEff T1 T2 R_in R_out]).
+
+    The body's typing is therefore INDEPENDENT of the outer formation
+    env [R]. Re-applying the formation rule at any [R'] satisfying the
+    rule's side condition [forall r, In r R' -> In r R_in] re-derives
+    the lambda's typing at [R'] — the body typing carries over
+    unchanged.
+
+    Contrast with [ground_nonlinear_retype_l1_m] (Phase 1), which
+    retypes EUnit / EBool / EI32 across ANY [R'] without a side
+    condition (those values have no R-dependent body).
+
+    Non-ELam value forms (EUnit, EBool, EI32, EPair, EInl, EInr, ELoc,
+    EBorrow, EEcho) do not type at [TFunEff …] (their typing rules
+    produce different type shapes). Inversion closes those cases via
+    [discriminate] on the type-equation residue.
+
+    For ELam at [TFunEff …], inversion of [Ht] yields one of four
+    [T_Lam_L1_*] constructors. The two non-Eff constructors
+    ([T_Lam_L1_Linear], [T_Lam_L1_Affine]) produce [TFun T1 T2]
+    (no R_in / R_out fields), so the type-equation residue
+    [TFun … = TFunEff …] discriminates. The two Eff constructors
+    fire constructively, with re-application supplying the new R'
+    and the supplied side condition [Hsub].
+
+    Note on modality monomorphism: unlike
+    [ground_nonlinear_retype_l1_m] (which is [m -> m']-polymorphic
+    via the modality-independence of ground constructors), this
+    lemma is [m]-monomorphic. A TFunEff lambda formed via
+    [T_Lam_L1_Linear_Eff] (mode Linear) cannot be directly re-derived
+    via [T_Lam_L1_Affine_Eff] (mode Affine) without lifting the body
+    typing across the [Linear -> Affine] modality bridge (which is
+    [linear_to_affine] in [TypingL2.v], but that operates on full
+    derivations not under retype). Phase 3 does not require cross-mode
+    retype — the Phase 4 [T_App_L2_Eff] β-case uses a single fixed [m]
+    throughout. Cross-modality TFunEff retype, if ever needed, would
+    layer [linear_to_affine] over this lemma.
+
+    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 ->
+    (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 ->
+    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 Hsub Ht.
+  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; try discriminate.
+  - (* v = ELam T0 e0, T_Lam_L1_Linear_Eff *)
+    eapply T_Lam_L1_Linear_Eff; [exact Hsub | eassumption].
+  - (* v = ELam T0 e0, T_Lam_L1_Affine_Eff *)
+    eapply T_Lam_L1_Affine_Eff; [exact Hsub | eassumption].
+Qed.
+
 (** Narrower axiom (region-liveness at compound-rule split points).
 
     Given a well-typed sub-derivation [R; G |=L1 e1 : T1 -| R1; G']

formal/Syntax.v

@@ -472,6 +472,22 @@ Definition is_ground_nonlinear_ty (T : ty) : bool :=
   | _ => false
   end.
 
+(** Check if a type is an effect-typed function type [TFunEff _ _ _ _].
+    Values at these types are TFunEff lambdas whose body is typed at a
+    fixed [R_in] (independent of the formation env [R]); a retype across
+    [R -> R'] is conditionally valid under the side condition
+    [forall r, In r R' -> In r R_in] (the same side condition the
+    [T_Lam_L1_*_Eff] formation rules require).
+
+    Introduced for [Semantics_L1.tfuneff_lambda_retype_l1_m] and the
+    Phase D slice 4 non-linear substitution-lemma generalisation
+    (formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3). *)
+Definition is_tfuneff_ty (T : ty) : bool :=
+  match T with
+  | TFunEff _ _ _ _ => true
+  | _ => false
+  end.
+
 (** Check if all linear variables in context have been used *)
 Fixpoint ctx_all_linear_used (G : ctx) : Prop :=
   match G with