docs: Phase 3b 4-stage staged resolution plan (#235 → #239 / #240 / #241 / #242) (#237)

## Summary

Phase D slice 4 Phase 3b — design-gap finding (#235) **+ 4-stage staged
resolution plan** owner-approved 2026-05-30 PM. Stages tracked at #239 /
#240 / #241 / #242.

No `formal/*.v` changes. No CI changes (the parallel-session PR #236
owns the Coq EACCES fix).

## 4-stage staged resolution plan

The original three-option framing in #235 is **superseded** by a staged
plan that captures all three "Interesting" values without committing to
any single option's downsides.

| Stage | Issue | Scope | Captures value of |
|---|---|---|---|
| **Stage 1 — IMMEDIATE** | #239 | Leaf-only Phase 3b via
`tfuneff_lambda_free` + `Counterexample_L2_nested.v` + 2-condition
`preservation_l2`. | Option (3) — principled deferral, honest
2-condition statement. |
| **Stage 2 — parallel L4 track** | #240 | `ELam T_param R_in R_out
body` annotation extension. AST + typing rule + cascading. | Option (1)
— L4 "type-level → program-level commitments". |
| **Stage 3 — post-Stage-2** | #241 | Relaxed Phase 3b via
`declared_lambda_r_ins ⊆ R_in_v` + CPS v-typing argument.
Nested-condition collapses. | Option (2) — higher-order proof style
enters codebase. |
| **Stage 4 — Phase 5** | #242 | Compound non-linear +
region-substitution machinery + **unconditional** `preservation_l2`. |
The final destination. |

### Why staging beats single-option commitments

- **(1) alone**: forces AST migration before unblocking preservation_l2.
- **(2) alone**: introduces inductive-over-derivations predicate with no
other use in the codebase.
- **(3) alone**: ends with conditional preservation_l2 forever (no path
to unconditional).

The staged plan: (3) ships today's value at Stage 1, (1) lands L4's
value at L4's timeline (Stage 2), (2)'s value is harvested at exactly
the point CPS is necessary not over-engineered (Stage 3), (4) reaches
unconditional preservation_l2 as the natural sum.

### Stage 1's correctness is delivered, not provisional

Each of the 2 conditions on Stage 1's `preservation_l2` has a
**mechanised counterexample**:

- `Counterexample_L2.v` (already on main, PR #234) — fresh-region gap.
- `Counterexample_L2_nested.v` (new in Stage 1) — nested-lambda gap.

Programs outside the conditional form a precisely-documented soundness
class.

### Sequencing

- Stage 1 green-lit (#239). Implementation ships next session.
- Stages 2-4 tracked but NOT actioned this session.
- Stage 3 blocked on Stage 2; Stage 4 blocked on Stage 3; Stage 2
independent of Stage 1.

## Changes

- `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md` — Phase 3b addendum (gap
finding + 3-options framing) **+ Phase 3b resolution addendum (4-stage
staged plan)**.
- `.machine_readable/6a2/STATE.a2ml` — phase = `implementation`;
next_action = Stage 1 (#239) implementation.

No `formal/*.v` changes; Coqc 8.18.0 unaffected.

## Predecessor PRs

- Phase 4a (#228) MERGED — `preservation_l2_app_eff_beta_linear`.
- Phase 4b (#233) MERGED —
`preservation_l2_app_eff_beta_ground_nonlinear_l1`.
- Phase 4c (#234) MERGED — `Counterexample_L2.v` 3-Qed soundness-gap
witness.

## Owner-directive compliance (across all 4 stages)

- ✅ No `Semantics.v` / `Typing.v` / `Counterexample.v` (legacy) touch.
- ✅ No new `Axiom` / `Admitted` markers.
- ✅ No closure of residual `Semantics_L1.v` admits — strictly NEW
infrastructure under the four-layer redesign.
- ✅ Per-layer derivation: preservation_l2 closes via L2 infra; legacy
preservation remains Admitted (PROVABLY FALSE) per 2026-05-27 directive.

## Test plan

- [ ] CI green (no code changes; Coq oracle should pass unchanged —
pending PR #236's EACCES fix landing).
- [ ] Issues #235 / #239 / #240 / #241 / #242 cross-referenced.

Refs: #225 (Phase 3b parking lot), #230 (`regions_introduced_by`), #233
(Phase 4b), #234 (Phase 4c), #235 (parent finding), #236 (parallel Coq
EACCES fix), #239 (Stage 1), #240 (Stage 2), #241 (Stage 3), #242 (Stage
4).

🤖 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,8 +6,8 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Phase D slice 4 Phase 3b — implement `subst_typing_gen_l1_m_tfuneff` with option (a)'s precondition `(forall r, In r (regions_introduced_by e) -> In r R_in_v)`. Per the parallel session's analysis (PR #230's body), this is ~400 lines mirroring Phase 2 with `shift_typing_gen_l1_m` threading at every binder-descent case (Phase 2's `ground_nonlinear_value_shift_id_l1` shortcut doesn't apply to non-scalar TFunEff lambdas — `shift c 1 (ELam T0 e0) = ELam T0 (shift (S c) 1 e0)`, which changes body's de Bruijn indices). The precondition propagates through compound rules (sub-expressions' `regions_introduced_by` are subsets of the parent's) and discharges directly at the T_Region_L1 case. After Phase 3b: Phase 4c wraps preservation_l2's T_App_L2_Eff β-case CONDITIONALLY — requiring the precondition `regions_introduced_by(ebody) ⊆ R_in_v`. Programs not satisfying it form a documented soundness-gap class per `Counterexample_L2.v` (this slot's predecessor, this PR). Phase 4d (compound non-linear) 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 4c soundness-gap counterexample LANDED (2026-05-30, this PR): `formal/Counterexample_L2.v` with three Qed lemmas (`e_before_typed`, `e_step`, `e_after_untypable`) mechanising preservation_l2's failure for TFunEff substituends inside fresh-region scopes. Configuration: outer = ELam (TFunEff TUnit TUnit [] []) (ERegion r2 (EVar 0)); v2 = ELam TUnit EUnit; e_before = EApp outer v2 (types at TFunEff via T_App_L2_Eff); e_after = ERegion r2 v2 (β-result, does NOT type because T_Lam_L1_*_Eff's side condition `forall r, In r [r2] -> In r []` is violated). The structural mechanism: T_Region_L1's `~ In r (free_regions T)` premise prevents fresh r from being in R_in_v ⊆ free_regions(TFunEff), so the post-β term's inner TFunEff value cannot re-type at the new R. Phase 4b (parallel session #233) also LANDED on 2026-05-30. SUBST-LEMMA-GENERALIZATION-DESIGN.md gained a Phase 4c addendum documenting the conditional preservation_l2 path and three resolution options. Counterexample_L2.v added to formal/_CoqProject after TypingL2.v. Coqc 8.18.0 clean rebuild across all 11 .v files. Zero new admits/axioms (`Print Assumptions` confirms all three lemmas Closed under the global context). `Semantics.v`/`Typing.v`/`Counterexample.v` (legacy) untouched. The mechanised counterexample is the L1/L2 analogue of Counterexample.v for the legacy preservation, providing rigorous justification for the conditional Phase 4c statement."
+next_action: "Phase D slice 4 Phase 3b Stage 1 (per #239): implement leaf-only Phase 3b. (a) NEW Fixpoint `tfuneff_lambda_free : expr -> bool` in `formal/Syntax.v` (~10 lines). (b) NEW `subst_typing_gen_l1_m_tfuneff` Qed in `formal/Semantics_L1.v` 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). (c) NEW `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`. (d) NEW `formal/Counterexample_L2_nested.v` (parallel to Counterexample_L2.v) mechanising the nested-TFunEff soundness gap — 3 Qed lemmas, zero axioms. (e) Add to `_CoqProject` after `Counterexample_L2.v`. (f) STATE/design-doc updates. Owner-approved 2026-05-30 PM via the 4-stage staged plan superseding the original three options. Stages 2-4 (#240/#241/#242) tracked but NOT actioned this session. 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 4-stage resolution plan LANDED (2026-05-30 PM, this PR + cross-issue filings): SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3b addendum (gap finding + 3-options framing) + Phase 3b resolution addendum (4-stage plan superseding 3-options) + STATE.a2ml refresh. Cross-issue filings: #235 (parent finding) + #239 (Stage 1 leaf-only Phase 3b, green-lit) + #240 (Stage 2 ELam annotation, parallel L4 track) + #241 (Stage 3 relaxed Phase 3b + CPS, blocked on #240) + #242 (Stage 4 compound non-linear + unconditional preservation_l2, blocked on #241). The 4-stage plan harvests all three Interesting values: L4-alignment (Stage 2 via ELam annotation), higher-order proof style (Stage 3 via CPS), principled deferral + honest 2-condition statement (Stage 1 immediate). Stage 1 ships unblocked preservation_l2 β-case for leaf-only ebody with two mechanised counterexamples (`Counterexample_L2.v` for fresh-region gap, new `Counterexample_L2_nested.v` for nested-lambda gap). No `formal/*.v` changes in this PR (Stage 1 implementation ships next session). Owner-directive compliance: ✅ no Semantics.v / Typing.v / Counterexample.v touch; ✅ escalation-then-resolution per CLAUDE.md §DO #4; ✅ anti-pattern detector clean across all four stages. Coqc 8.18.0 unaffected (no code changes)."
 updated: 2026-05-30T00:00:00Z
 
 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):

formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md

@@ -142,6 +142,62 @@ Estimated ~250-300 lines, paralleling the existing proof.
 
 Add a retype lemma for TFunEff lambdas (under R' ⊆ R_in side condition). Extend the substitution lemma to cover `T1 = TFunEff …` lambdas as substituends. This is the case actually needed for higher-order β-reductions where the lambda parameter is itself a function type.
 
+#### Phase 3b addendum (2026-05-30) — option (a) precondition is insufficient
+
+The originally-proposed option (a) precondition
+
+```coq
+(forall r, In r (regions_introduced_by e) -> In r R_in_v)
+```
+
+is **insufficient** for the planned `subst_typing_gen_l1_m_tfuneff` lemma. Filed as ephapax issue #235.
+
+**Why**: the substitution lemma recurses into inner lambda bodies (mirroring Phase 2 lines 1929-1942). At inner `T_Lam_L1_*_Eff` cases, the body sub-derivation is typed at the lambda's declared `R_in_inner`, which is **type-level** (lives in `TFunEff T1 T2 R_in_inner R_out_inner`), not syntactic. `regions_introduced_by(e)` only collects `ERegion` subterms' first-argument names; `R_in_inner` is invisible to it.
+
+`tfuneff_lambda_retype_l1_m` (the retype lemma shipped in PR #224) requires `R' ⊆ R_in_v`. To retype the substituee at `R_in_inner` we'd need `R_in_inner ⊆ R_in_v`. Nothing in option (a) provides this.
+
+Phase 2's `subst_typing_gen_l1_m_ground_nonlinear` (the sibling lemma at lines 1812-2073) dodges this via `ground_nonlinear_retype_l1_m`, which is fully `(m, R, G)`-polymorphic. Phase 3b has no analogous escape hatch.
+
+**Three resolution options for owner**:
+
+1. **Strengthen the precondition to a type-level over-approximation**. Define a helper that walks `ELam T body` extracting `R_in` from `T` when `T = TFunEff _ _ R_in _`. **Blocker**: `ELam` syntax carries the *parameter* type, not the function type — `R_in` is determined by typing, not syntax. Without an annotation extension to `ELam`, this helper can't be defined as a syntactic Fixpoint.
+
+2. **Semantic precondition over the derivation**. Quantify over sub-derivations of `Htype`: `forall R'_in appearing in Htype, R'_in ⊆ R_in_v`. Clean meaning, awkward in Coq (inductive predicate over derivations or fixpoint indexed by depth).
+
+3. **Restrict scope — Phase 3b leaf-only**. Add an inductive predicate `lambda_free e` (or `tfuneff_lambda_free e`) and condition the lemma on it. Unblocks the **immediate** consumer (preservation_l2 β-case for TFunEff arguments whose ambient `ebody` uses ERegion but not nested function abstractions). Recursive case rides Phase 5's compound-value redesign.
+
+**Recommendation**: option (3) as the tactical landing for Phase 3b. The substantive Phase 5 redesign can subsume option (1) or (2) at its leisure.
+
+Phase 3b implementation **does not start** until owner picks a resolution.
+
+#### Phase 3b resolution (2026-05-30 PM, owner-approved) — 4-stage staged plan
+
+The three-option framing above is **superseded** by a staged plan that captures the value of each "Interesting" angle without committing to any single option's downsides. Filed as ephapax issues #239 (Stage 1) / #240 (Stage 2) / #241 (Stage 3) / #242 (Stage 4) under parent #235.
+
+| Stage | Scope | Captures value of |
+|---|---|---|
+| **Stage 1 — immediate (#239)** | Leaf-only Phase 3b via `tfuneff_lambda_free` + `Counterexample_L2_nested.v` + 2-condition `preservation_l2`. | Option (3) — principled deferral, honest 2-condition statement. |
+| **Stage 2 — parallel L4 track (#240)** | `ELam T_param R_in R_out body` annotation extension. AST + typing rule + cascading inversion patterns. | Option (1) — L4 alignment "type-level → program-level commitments". |
+| **Stage 3 — post-Stage-2 (#241)** | Relaxed Phase 3b via `declared_lambda_r_ins ⊆ R_in_v` + **CPS-form** v-typing argument. Nested-condition collapses. | Option (2) — higher-order proof style enters the codebase. |
+| **Stage 4 — Phase 5 (#242)** | Compound non-linear values + region-substitution machinery + **unconditional** `preservation_l2`. | The final destination — last soundness condition closes. |
+
+**Why staging captures all the value**:
+
+- **Stage 1's 2-condition statement is delivered correctness, not a placeholder.** Each condition has a mechanised counterexample (`Counterexample_L2.v` for the fresh-region gap, the new `Counterexample_L2_nested.v` for the nested-lambda gap).
+- **Stage 2 ships independently** of Phase 3b — it's L4's own work (program-level commitments) that Phase 3b free-rides on at Stage 3.
+- **Stage 3 introduces CPS proof style** at exactly the point where it's strictly necessary (relaxed Phase 3b's inner `T_Lam_L1_*_Eff` cases must retype v at arbitrary `R_in_inner`'s) — not over-engineered for Stage 1.
+- **Stage 4 inherits the CPS precedent** from Stage 3 and closes the last soundness condition. `preservation_l2` Qed over `has_type_l2`.
+
+**Why this beats single-option commitments**:
+
+- (1) alone forces the AST migration before unblocking preservation_l2's β-case.
+- (2) alone introduces an inductive-over-derivations predicate with no other use in the codebase.
+- (3) alone ends with a conditional preservation_l2 forever (no path to unconditional).
+
+The staged plan: (3) ships today's value, (1) lands L4's value at L4's timeline, (2)'s value is harvested at exactly the point CPS is necessary, (4) reaches unconditional preservation_l2 as the natural sum of (1) + (2) + (3) applied in sequence.
+
+**Sequencing**: Stage 1 implementation green-lit. Stages 2-4 tracked. Stage 3 blocked on Stage 2; Stage 4 blocked on Stage 3; Stage 2 independent of Stage 1.
+
 ### Phase 4: close `preservation_l2` β-case using Phases 1-3
 
 With the substitution machinery in place, the T_App_L2_Eff β-case in `preservation_l2` closes by: