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

## Summary

Ships **Stage 1b** of the four-stage Phase 3b resolution plan (parent
#235 / Stage 1 #239 / Stages 2-4 #240-#242), closing the L1 substitution
+ L2 preservation β-case for closed TFunEff substituents in leaf-only
outer bodies.

**Builds on Stage 1a (PR #252, auto-merge armed)** which shipped the
syntactic infrastructure (`tfuneff_lambda_free`) + the soundness-gap
witness (`Counterexample_L2_nested.v`).

Closes ephapax issue #249. With this PR, Stage 1 (#239) is fully
delivered.

## What ships

### Syntax.v (canonical closure machinery)

- `expr_closed_below : nat -> expr -> bool` — Fixpoint, bool per
post-redesign convention. Standard CS "no free de Bruijn variables ≥ k"
predicate.
- `closed_below_shift_id` — closed-below-c terms are shift-invariant at
cutoff c.
- `expr_closed_below_shift_mono` — closure survives shifting.
- `ctx_mark_used_app_lt` — `ctx_mark_used` commutes with context append
when marked position lies within the head.

### Semantics_L1.v (body-transfer + RG-poly retype)

- `closed_below_k_typing_outer_tail_irrelevant_l1_m` — the body-transfer
core. Structural induction across 28+ typing rules; ~200 lines.
Establishes that closed-below-k terms' typing depends only on G's first
k positions; the tail is structurally irrelevant.
- `closed_value_typing_G_poly_l1_m` — closed TFunEff values type at any
G' (any-G' form per elegance-first "state what's actually true", not "G
of matching length").
- `closed_value_typing_RG_poly_l1_m` — combined RG-poly retype chaining
the G-poly helper with `tfuneff_lambda_retype_l1_m` (PR #224) for the
R-component under `R' ⊆ R_in` side condition.
- `closed_value_shift_id_l1_m` — cutoff-0 wrapper of
`closed_below_shift_id`.
- `value_TFunEff_R_subset_R_in_l1_m` — extracts `R ⊆ R_in` from a
TFunEff value's 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` Qed (~300 lines) — mirrors Phase 2's
`subst_typing_gen_l1_m_ground_nonlinear`. Inner `T_Lam_L1_*_Eff` cases
discharge via P1 `discriminate`; compound rules use the RG-poly retype +
R-subset chain to handle the G-mismatch.

### TypingL2.v (β-case closure)

- `preservation_l2_app_eff_beta_tfuneff_l1` — L1-level kernel. Inverts
the lambda derivation through `T_Lam_L1_Linear_Eff` /
`T_Lam_L1_Affine_Eff`; collapses R/G via `value_R_G_preserving_l1`;
defers to the substitution kernel above at k=0.
- `preservation_l2_app_eff_beta_tfuneff` — L2 wrapper. Inverts both
`has_type_l2` hypotheses through `L2_lift_l1` (the `T_App_L2_Eff` cases
discriminate via expression-shape mismatch).

### `.machine_readable/6a2/STATE.a2ml`

- `last_action` records the full Stage 1b deliverable surface.
- `next_action` advances to Stages 2-4 (#240/#241/#242).

## Two-condition statement (per Stage 1 framing)

```coq
Lemma preservation_l2_app_eff_beta_tfuneff :
  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 ->                           (* P1 *)
    (forall r, In r (regions_introduced_by ebody) -> In r R_in_v) ->  (* P2 *)
    expr_closed_below 0 v2 = true ->                              (* P3 *)
    has_type_l2 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_l2 m R1 G' v2 (TFunEff Ta Tb R_in_v R_out_v) R_in G'' ->
    has_type_l2 m R  G  (subst 0 v2 ebody) T2 R_out G''.
```

The mechanised soundness-gap witnesses for the conditional form:
- `Counterexample_L2.v` (PR #234, Phase 4c) — fresh-region gap
(counterexample to dropping P2).
- `Counterexample_L2_nested.v` (Stage 1a, PR #252) — nested-lambda gap
(counterexample to dropping P1).

Stage 4 (#242) achieves the unconditional form once the L4 annotation
extension (#240) and CPS argument (#241) land — the proof content of
this PR's `closed_value_typing_*` family is reused unchanged in Stage 4
as the closure-discharge kernel.

## Path-(i) elegance-first design choices

Per the priority order (elegance + correctness > everything; workload
least), this PR bakes in two explicit refinements over the issue body's
draft:

1. **`bool` predicate target** for `expr_closed_below` — matches
post-redesign convention (`is_linear_ty`, `is_ground_nonlinear_ty`,
`tfuneff_lambda_free` are all bool). The legacy Prop predicates
(`expr_free_of_region`) are pre-redesign artefacts.
2. **Any-G' statement form** for the closed-value helper — states what's
actually true ("for closed values, G is genuinely irrelevant"), not what
fell out of the proof induction.

Two refinements that touch approved scope were deliberately NOT made:
- P1 (`tfuneff_lambda_free`) precondition retained, not dropped —
re-staging is owner territory.
- 4-stage plan accepted as is — no re-staging proposal folded into Stage
1b.

## Print Assumptions verdict

All new Qed lemmas: **Closed under the global context**.

- `subst_typing_gen_l1_m_tfuneff`: Closed under the global context
- `closed_value_typing_G_poly_l1_m`: Closed under the global context
- `closed_value_typing_RG_poly_l1_m`: Closed under the global context
- `closed_below_k_typing_outer_tail_irrelevant_l1_m`: Closed under the
global context
- `preservation_l2_app_eff_beta_tfuneff_l1`: Closed under the global
context
- `preservation_l2_app_eff_beta_tfuneff`: Closed under the global
context

Zero new axioms. Zero new admits.

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

- ✅ No touch to `formal/Semantics.v` / `Typing.v` / `Counterexample.v`.
- ✅ No closure of residual `Semantics_L1.v` admits attempted.
- ✅ Anti-pattern detector clean (canonical CS infrastructure; no
sibling-region-disjointness, no region-weakening predicates on syntactic
shape, no admit-shuffling, no legacy-preservation closure attempt).
- ✅ Strictly NEW infrastructure orthogonal to legacy.

## Test plan

- [x] `just -f formal/Justfile all` clean across all 12 .v files
- [x] Print Assumptions on every new Qed lemma reports "Closed under the
global context"
- [x] No `Axiom` / `Admitted` introduced
- [x] No legacy file touched per owner directive
- [x] Stage 1a's contributions (`tfuneff_lambda_free`,
`Counterexample_L2_nested.v`) still build clean
- [x] Phase 2's contributions (`ground_nonlinear_retype_l1_m`,
`subst_typing_gen_l1_m_ground_nonlinear`) still build clean
- [x] Phase 4a + 4b L2 β-wrappers still build clean
- [ ] `coq-build.yml` CI workflow runs against this PR (gated on PR #231
/ #236 fixes)

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.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,