feat(L1+L2): Phase D slice 4 Phase 3b Stage 1b — closed-value substitution + preservation_l2 β closure (closes #249)

.machine_readable/6a2/STATE.a2ml

@@ -6,9 +6,9 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Phase D slice 4 Phase 3b Stage 1b (sibling to #239 — file as follow-up sub-issue): implement the deferred substitution-lemma half. (a) `closed_value_typing_G_poly_l1_m` helper in `formal/Semantics_L1.v` (G-polymorphic retype for closed TFunEff values, addressing the structural blocker discovered in Stage 1a). (b) `subst_typing_gen_l1_m_tfuneff` Qed mirroring `subst_typing_gen_l1_m_ground_nonlinear` (~300 lines); inner T_Lam_L1_*_Eff cases exfalso via the `tfuneff_lambda_free` precondition; direct (P1, P2) hypothesis form (no CPS yet — Stage 3 introduces CPS). May add a third precondition `expr_closed_below 0 v = true` to handle the G-mismatch at compound binder rules; document as Stage 1 restriction lifted in Stage 3/4. (c) `preservation_l2_app_eff_beta_tfuneff_l1` + L2 wrapper Qed in `formal/TypingL2.v` under the 2-condition statement: `tfuneff_lambda_free ebody = true ∧ regions_introduced_by ebody ⊆ R_in_v`. 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 — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority."
-last_action: "Phase D slice 4 Phase 3b Stage 1a LANDED (2026-05-30 PM, this PR): mechanised soundness-gap witness + Stage 1 syntactic infrastructure. (1) `tfuneff_lambda_free : expr -> bool` Fixpoint added to `formal/Syntax.v` (conservative leaf-only predicate; `false` on every `ELam`, compositional `andb` propagation through compound forms). (2) `formal/Counterexample_L2_nested.v` — three Qed lemmas (`e_before_typed`, `e_step`, `e_after_untypable`) mechanising the nested-TFunEff soundness gap with `outer = ELam T_v (ELam (TBase TUnit) (EVar 1))` configuration where inner R_in_inner = [r2] but substituent R_in_v = []; e_after = ELam TUnit v fails to retype the body at `[r2] ⊄ [] = R_in_v`. (3) Wired into `_CoqProject` after `Counterexample_L2.v`. (4) `SUBST-LEMMA-GENERALIZATION-DESIGN.md` gained a 'Phase 3b Stage 1a (landed) — split from Stage 1' subsection inside the Phase 3b resolution section, documenting the Stage 1a / Stage 1b split and the structural blocker (G-mismatch at compound binder rules — `tfuneff_lambda_retype_l1_m` preserves G but IH expects post-e1 G' with different used-flags) that motivated the split. Stage 1b (substitution lemma + preservation_l2 wrapper) ships next session via a follow-up sub-issue. Build oracle: coqc 8.18.0 clean across all 12 .v files; Print Assumptions on all three new Qed lemmas reports 'Closed under the global context' (zero new admits/axioms). Owner-directive compliance: ✅ no Semantics.v / Typing.v / Counterexample.v touch; ✅ no residual Semantics_L1.v admit closure attempted; ✅ anti-pattern detector clean. Sibling counterexample artifact to `Counterexample_L2.v` (PR #234) for the nested-lambda soundness-gap class; the two together justify the two-condition (P1 = `tfuneff_lambda_free`, P2 = `regions_introduced_by ⊆ R_in_v`) preservation_l2 statement Stage 1b delivers."
-updated: 2026-05-30T00:00:00Z
+next_action: "Phase D slice 4 Phase 3b Stages 2-4 (#240/#241/#242): Stage 1 (both 1a + 1b) complete. Stages 2-4 sequenced per the owner-approved 4-stage plan: Stage 2 (#240) ELam annotation extension — independent of Stage 1, ships when prioritised; Stage 3 (#241) CPS + relaxed Phase 3b — blocked on Stage 2; Stage 4 (#242) compound non-linear + unconditional preservation_l2 — blocked on Stage 3. Stage 4's destination collapses Stage 1b's three preconditions (P1 = tfuneff_lambda_free, P2 = regions_introduced_by ⊆ R_in_v, P3 = expr_closed_below 0 v) once typing-derived closure invariants land. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted`; no touching `Semantics.v` / `Typing.v` / `Counterexample.v`; no closure of residual `Semantics_L1.v` admits — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority."
+last_action: "Phase D slice 4 Phase 3b Stage 1b LANDED (2026-05-30 PM, this PR): elegance-first path-(i) substitution-lemma + L2 β wrapper, zero axioms. (1) Syntax.v: `expr_closed_below : nat -> expr -> bool` Fixpoint (canonical CS predicate, bool per post-redesign convention); `closed_below_shift_id` (closed terms shift-invariant); `expr_closed_below_shift_mono` (closure survives shifting); `ctx_mark_used_app_lt` (mark_used commutes with context append). (2) Semantics_L1.v: `closed_below_k_typing_outer_tail_irrelevant_l1_m` (the body-transfer core — structural induction over 28+ typing rules; closed-below-k terms' typing depends only on G's first k positions); `closed_value_typing_G_poly_l1_m` (any-G' form per elegance-first 'state what's actually true'); `closed_value_typing_RG_poly_l1_m` (combined RG-poly via chain to tfuneff_lambda_retype_l1_m); `closed_value_shift_id_l1_m` (cutoff-0 wrapper); `value_TFunEff_R_subset_R_in_l1_m` (extracts R ⊆ R_in from TFunEff value typing); `sub_R_in_R_in_via_value_l1_m` (chain helper packaging count_occ_le_l1_m + R-subset for compound-rule call sites); `subst_typing_gen_l1_m_tfuneff` (~300 lines mirroring Phase 2's ground-nonlinear template; inner T_Lam_L1_*_Eff cases discharge via P1 discriminate; compound rules use closed_value_typing_RG_poly_l1_m + sub_R_in_R_in_via_value_l1_m for the G-mismatch). (3) TypingL2.v: `preservation_l2_app_eff_beta_tfuneff_l1` (β-case kernel) + `preservation_l2_app_eff_beta_tfuneff` (L2 wrapper) under the three-condition statement (P1 leaf-only + P2 regions ⊆ R_in_v + P3 closure of v2). Build oracle: coqc 8.18.0 clean across all 12 .v files; Print Assumptions on every new Qed lemma reports 'Closed under the global context' (zero new admits / axioms). Owner-directive compliance: ✅ no Semantics.v / Typing.v / Counterexample.v touch; ✅ no residual Semantics_L1.v admit closure attempted; ✅ anti-pattern detector clean. Design decisions baked in per elegance-first priority: bool predicate (matches post-redesign style), any-G' statement form (the genuinely true claim), P1 RETAINED (re-staging is owner territory), staging-as-is (PR-level decisions don't deviate from owner-approved 4-stage plan)."
+updated: 2026-05-30T20:00:00Z
 
 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):
 # Captured durable directive — preservation work is the four-layer redesign,