Phase 3b Stage 1: leaf-only substitution lemma + 2-condition preservation_l2 + Counterexample_L2_nested

[hyperpolymath]

Stage 1 of the 4-stage Phase 3b resolution plan per #235. Implementation green-lit by owner 2026-05-30.

Scope

Ship Phase 3b under the leaf-only restriction: subst_typing_gen_l1_m_tfuneff proves only for ebody containing no nested TFunEff lambdas. The leaf restriction makes inner T_Lam_L1_*_Eff cases discharge via exfalso, sidestepping option (a)'s insufficiency (#235).

Deliverables:

1. tfuneff_lambda_free : expr -> bool — syntactic Fixpoint in formal/Syntax.v. ~10 lines.
2. subst_typing_gen_l1_m_tfuneff Qed — in formal/Semantics_L1.v. Direct (P1, P2) hypotheses (no CPS yet — Stage 3 introduces CPS when nested lambdas re-enter scope). Estimated ~300 lines mirroring subst_typing_gen_l1_m_ground_nonlinear (Phase 2).
3. preservation_l2_app_eff_beta_tfuneff_l1 + L2 wrapper Qed in formal/TypingL2.v. Conditional statement carries two soundness conditions:
   • tfuneff_lambda_free ebody = true, AND
   • forall r, In r (regions_introduced_by ebody) -> In r R_in_v.
4. formal/Counterexample_L2_nested.v — new file mechanising the nested-TFunEff soundness gap (parallel to Counterexample_L2.v which mechanises the fresh-region gap). 3 Qed lemmas (e_before_typed, e_step, e_after_untypable) with a nested-lambda configuration.
5. _CoqProject — add Counterexample_L2_nested.v after Counterexample_L2.v.
6. SUBST-LEMMA-GENERALIZATION-DESIGN.md — Phase 3b addendum updated: option (a) restated as Stage-1's tfuneff_lambda_free ∧ regions_introduced_by ⊆ R_in_v; original 3 options retired in favour of the staged plan.
7. STATE.a2ml — phase back to implementation; next_action points at Stage 1 implementation.

What this delivers

The conditional preservation_l2 statement is delivered correctness, not a placeholder. Each soundness condition has a mechanised counterexample (Counterexample_L2.v for fresh-region gap, Counterexample_L2_nested.v for nested-lambda gap). Programs outside the conditional form a precisely-documented soundness class.

What this does NOT deliver

• Inner T_Lam_L1_*_Eff cases of substitution: deferred to Stage 3 (#TBD2).
• Unconditional preservation_l2: deferred to Stage 4 (#TBD3) alongside compound non-linear (Phase 5).

Owner-directive compliance

• ✅ No Semantics.v / Typing.v / Counterexample.v (legacy) touch.
• ✅ No new Axiom or Admitted markers.
• ✅ No closure of residual Semantics_L1.v admits.
• ✅ Pure NEW infrastructure under has_type_l1 / has_type_l2.

References

• Phase 3b design gap: option (a) precondition insufficient for T_Lam_L1_*_Eff body cases #235 — Phase 3b design-gap finding (parent).
• Phase D slice 4 Phase 3b — TFunEff substitution-lemma extension (deferred from #224) #225 — Phase 3b parking lot (predecessor scaffolding).
• feat(syntax): regions_introduced_by helper — Phase 3b scaffolding (#225) #230 — regions_introduced_by helper.
• docs+test: Phase D slice 4 Phase 4c — mechanised soundness-gap counterexample for TFunEff β #234 — Phase 4c counterexample (Counterexample_L2.v) — parallel pattern for Counterexample_L2_nested.v.
• formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3 + Phase 4c addenda.

🤖 Generated with Claude Code

[hyperpolymath]

Cross-references resolved

• Stage 1 (this issue): Phase 3b Stage 1: leaf-only substitution lemma + 2-condition preservation_l2 + Counterexample_L2_nested #239 — leaf-only Phase 3b + Counterexample_L2_nested + 2-condition preservation_l2. Implementation green-lit.
• Stage 2: Phase 3b Stage 2 (L4 track): ELam annotation extension — R_in / R_out as program-level commitments #240 — ELam annotation extension (parallel L4 track).
• Stage 3: Phase 3b Stage 3: relaxed restriction via declared_lambda_r_ins + CPS substitution lemma signature #241 — relaxed restriction via declared_lambda_r_ins + CPS proof style. Blocked on Phase 3b Stage 2 (L4 track): ELam annotation extension — R_in / R_out as program-level commitments #240.
• Stage 4: Phase 3b Stage 4 (Phase 5): compound non-linear values + unconditional preservation_l2 #242 — compound non-linear + unconditional preservation_l2 (Phase 5). Blocked on Phase 3b Stage 3: relaxed restriction via declared_lambda_r_ins + CPS substitution lemma signature #241.

Parent finding: #235.

[hyperpolymath]

Stage 1a partial closure: PR #252 ships tfuneff_lambda_free Fixpoint + Counterexample_L2_nested.v (3 Qed lemmas, zero new axioms) + design-doc Stage 1a addendum + STATE.a2ml refresh. Stage 1b (subst_typing_gen_l1_m_tfuneff + preservation_l2 β wrapper) deferred to sub-issue #249 due to a structural blocker: tfuneff_lambda_retype_l1_m (PR #224) preserves G, but Phase 2's analog ground_nonlinear_retype_l1_m is fully G-polymorphic — substitution-lemma compound rule cases need to retype v at G' (post-e1 used-flag updates). Stage 1b machinery needs EITHER a closed-value G-poly helper OR a G-flag-polymorphic retype variant; see #249 for details.

[hyperpolymath]

Closing — Signal B (umbrella tracked by sub-tickets). Stage 1's scope is fully covered by Stage 1a (MERGED via #252) and Stage 1b (tracked in #249). The umbrella ticket itself no longer adds tracking value beyond the sub-tickets. Closing in favour of #249 as the live Stage 1 tracker.