Phase 3b Stage 1b: subst_typing_gen_l1_m_tfuneff + preservation_l2 β wrapper (deferred from #239)

[hyperpolymath]

Stage 1 of the four-stage Phase 3b resolution plan (#235 → #239 / #240 / #241 / #242) splits into two slices for shipping cadence. Stage 1a landed in PR (proof-debt/phase-3b-stage-1-tfuneff-leaf, soon to be linked): tfuneff_lambda_free Fixpoint + Counterexample_L2_nested.v. Stage 1b (this issue) ships the deferred substitution-lemma + preservation_l2 β wrapper half.

Deliverables

(a) NEW subst_typing_gen_l1_m_tfuneff Qed in formal/Semantics_L1.v mirroring subst_typing_gen_l1_m_ground_nonlinear (lines 1812-2073, ~300 lines). Signature:

Lemma subst_typing_gen_l1_m_tfuneff :
  forall m R Gin e T R' Gout,
    has_type_l1 m R Gin e T R' Gout ->
    forall k Ta Tb R_in_v R_out_v v u_in,
      nth_error Gin k = Some (TFunEff Ta Tb R_in_v R_out_v, u_in) ->
      is_value v ->
      tfuneff_lambda_free e = true ->
      (forall r, In r (regions_introduced_by e) -> In r R_in_v) ->
      has_type_l1 m R (remove_at k Gin) v
                  (TFunEff Ta Tb R_in_v R_out_v) R (remove_at k Gin) ->
      forall u_out,
        nth_error Gout k = Some (TFunEff Ta Tb R_in_v R_out_v, u_out) ->
        has_type_l1 m R (remove_at k Gin) (subst k v e) T R' (remove_at k Gout).

Inner T_Lam_L1_*_Eff cases exfalso via the tfuneff_lambda_free precondition. Direct (P1, P2) hypothesis form — no CPS yet (Stage 3 #241 introduces CPS).

(b) NEW preservation_l2_app_eff_beta_tfuneff_l1 + L2 wrapper Qed in formal/TypingL2.v under the 2-condition statement:

Lemma preservation_l2_app_eff_beta_tfuneff_l1 :
  forall m R R1 G G' G'' v2 Ta Tb R_in_v R_out_v T2 R_in R_out ebody,
    is_value v2 ->
    tfuneff_lambda_free ebody = true ->
    (forall r, In r (regions_introduced_by ebody) -> In r R_in_v) ->
    has_type_l1 m R  G  (ELam (TFunEff Ta Tb R_in_v R_out_v) ebody)
                        (TFunEff (TFunEff Ta Tb R_in_v R_out_v) T2 R_in R_out) R1 G' ->
    has_type_l1 m R1 G' v2 (TFunEff Ta Tb R_in_v R_out_v) R_in G'' ->
    has_type_l1 m R  G  (subst 0 v2 ebody) T2 R_out G''.

Plus L2 wrapper mirroring preservation_l2_app_eff_beta_ground_nonlinear.

The structural blocker that required the split

Phase 2's analog (subst_typing_gen_l1_m_ground_nonlinear) uses ground_nonlinear_retype_l1_m to retype the substituent at sub-derivation contexts. That retype is fully (R, G)-polymorphic — any R', G' works.

Phase 3b's tfuneff_lambda_retype_l1_m (PR #224) is R-polymorphic but G-preserving. The substitution lemma's compound rule cases (T_Let_L1, T_LetLin_L1, T_Case_L1_, T_StringConcat_L1, T_App_L1, T_Pair_L1, T_If_L1_) need to retype v at G' (post-e1's context with possibly different used-flag patterns) which is not the same G as the original Hv_type.

Two paths to resolve, both their own sub-deliverable:

• Path (i) — Closed-value G-polymorphism helper: add expr_closed_below 0 v = true precondition + prove closed_value_typing_G_poly_l1_m (G-poly retype for closed TFunEff lambdas, provable via inversion on T_Lam_L1_*_Eff formation rules but adds a Stage 1 restriction lifted in Stage 3/4).
• Path (ii) — G-flag-polymorphic retype variant: prove that for TFunEff values, typing depends on G's TYPE info but not used-flags (the formation rule outputs the same outer G unchanged, so used-flag patterns at non-referenced positions don't affect formation). Heavier proof.

Stage 1b implementation should pick a path, document the choice, and ship.

Anti-pattern compliance (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.

Links

• Parent finding: Phase 3b design gap: option (a) precondition insufficient for T_Lam_L1_*_Eff body cases #235
• Stage 1 (this issue's parent): Phase 3b Stage 1: leaf-only substitution lemma + 2-condition preservation_l2 + Counterexample_L2_nested #239
• Stages 2-4: Phase 3b Stage 2 (L4 track): ELam annotation extension — R_in / R_out as program-level commitments #240 (ELam annotation), Phase 3b Stage 3: relaxed restriction via declared_lambda_r_ins + CPS substitution lemma signature #241 (CPS + relaxed Phase 3b), Phase 3b Stage 4 (Phase 5): compound non-linear values + unconditional preservation_l2 #242 (compound non-linear + unconditional)
• Stage 1a PR: proof-debt/phase-3b-stage-1-tfuneff-leaf (forthcoming PR)
• Design doc: `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md` §Phase 3b Stage 1a (landed)

[hyperpolymath]

Closing via PR #253 (Stage 1b L1 substitution + L2 β wrapper, zero axioms). Stage 1 (#239) is now fully delivered (Stage 1a in #252 + Stage 1b here).