docs: Phase 3b 4-stage staged resolution plan (owner-approved, supersedes 3-options framing)

Owner-approved 2026-05-30 PM. Captures all three "Interesting" values
from the option-1/2/3 analysis without committing to any single
option's downsides.

| Stage | Issue | Scope |
|---|---|---|
| Stage 1 — IMMEDIATE | #239 | Leaf-only Phase 3b via tfuneff_lambda_free + Counterexample_L2_nested.v + 2-condition preservation_l2. |
| Stage 2 — parallel L4 track | #240 | ELam T_param R_in R_out body annotation extension. |
| Stage 3 — post-Stage-2 | #241 | Relaxed Phase 3b via declared_lambda_r_ins + CPS proof style. Nested-condition collapses. |
| Stage 4 — Phase 5 | #242 | Compound non-linear + region-substitution machinery + UNCONDITIONAL preservation_l2. |

Stage 1 green-lit, ships next session. Stages 2-4 tracked but not
actioned. Stage 3 blocked on Stage 2; Stage 4 blocked on Stage 3;
Stage 2 independent of Stage 1.

Why staging beats single-option commitments:
- (1) alone forces AST migration before unblocking preservation_l2.
- (2) alone introduces inductive-over-derivations with no other use.
- (3) alone ends with conditional preservation_l2 forever.

The staged plan harvests:
- (3)'s tactical landing + honest 2-condition statement at Stage 1.
- (1)'s L4 alignment when L4 is ready at Stage 2.
- (2)'s higher-order proof style at exactly the point CPS is
  necessary (Stage 3) — not over-engineered before.
- (4)'s region-substitution machinery as the natural sum.

Stage 1's 2-condition statement is delivered correctness, not a
placeholder. Each condition has a mechanised counterexample
(Counterexample_L2.v for fresh-region gap, new
Counterexample_L2_nested.v for nested-lambda gap).

This PR contains documentation only:
  - formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md gains a Phase 3b
    resolution addendum (the 4-stage plan superseding 3-options).
  - .machine_readable/6a2/STATE.a2ml flips phase back to
    `implementation`; next_action points at Stage 1 (#239).

No formal/*.v changes in this PR.

Owner-directive compliance (across all 4 stages):
  - No Semantics.v / Typing.v / Counterexample.v (legacy) touch
  - No 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

Refs: #235 (parent finding), #239 (Stage 1), #240 (Stage 2),
#241 (Stage 3), #242 (Stage 4).

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -5,9 +5,9 @@
 # See: standards/a2ml-templates/STATE.a2ml.v2.spec.adoc
 
 @state(version="2.0"):
-phase: "blocked-on-owner-decision"
-next_action: "BLOCKED on owner decision per ephapax issue #235. Phase D slice 4 Phase 3b's stated option (a) precondition `(forall r, In r (regions_introduced_by e) -> In r R_in_v)` is INSUFFICIENT to discharge T_Lam_L1_*_Eff body cases of the planned `subst_typing_gen_l1_m_tfuneff` lemma. Why: the substitution lemma recurses into inner lambda bodies (Phase 2 does so via IH at Semantics_L1.v:1929-1942); inner T_Lam_L1_*_Eff bodies type 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-arg names; `R_in_inner` is invisible to it. `tfuneff_lambda_retype_l1_m` requires `R' ⊆ R_in_v` — we have no way to bound `R_in_inner` by `R_in_v`. Phase 2 dodges this via fully (m,R,G)-poly `ground_nonlinear_retype_l1_m`; Phase 3b has no analogous escape. Three resolution options documented in `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md` Phase 3b addendum + issue #235: (1) syntactic helper `declared_lambda_r_ins` requires ELam annotation extension (parameter type only in syntax); (2) semantic precondition over derivation; (3) leaf-only Phase 3b via `tfuneff_lambda_free e` predicate. Recommended: (3) as tactical landing; Phase 5 compound-value redesign subsumes (1)/(2) at leisure. Per CLAUDE.md owner directive `DO #4 (escalate before patching)`: this STATE update IS the escalation. No code changes to `formal/*.v` until owner picks a resolution. Phase 4a (PR #228) + Phase 4b (parallel session PR #233) + Phase 4c counterexample (PR #234) all LANDED 2026-05-30. Phase 4c's `Counterexample_L2.v` independently justifies the conditional preservation_l2 statement regardless of which Phase 3b resolution lands. Phase 4d (compound non-linear) remains 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 3b design-gap finding LANDED (2026-05-30, this PR): SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3b addendum + STATE.a2ml flag-blocking + ephapax issue #235. The finding emerged during pre-implementation review of Phase 3b's structure — option (a)'s precondition was checked against each rule of the planned induction and found to leave T_Lam_L1_*_Eff body cases (Phase 2 analog Semantics_L1.v:1929-1942) un-dischargeable, because inner lambdas' R_in is type-level (TFunEff R_in slot) not syntactic. Predecessor PRs unaffected: Phase 4a (TypingL2.v `preservation_l2_app_eff_beta_linear`, PR #228) MERGED 2026-05-30; Phase 4b (parallel session, PR #233 `preservation_l2_app_eff_beta_ground_nonlinear_l1`) MERGED 2026-05-30; Phase 4c (`Counterexample_L2.v` 3-Qed soundness-gap witness, PR #234) MERGED 2026-05-30. The Phase 4c counterexample mechanises the soundness-gap class regardless of which Phase 3b resolution option lands. No `formal/*.v` changes in this PR. Owner-directive compliance: ✅ no Semantics.v / Typing.v / Counterexample.v touch; ✅ escalation before patching per CLAUDE.md §DO #4; ✅ anti-pattern detector clean — no side-condition added, no axiom added, no admit-shuffling. Coqc 8.18.0 unaffected (no code changes)."
+phase: "implementation"
+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

@@ -170,6 +170,34 @@ Phase 2's `subst_typing_gen_l1_m_ground_nonlinear` (the sibling lemma at lines 1
 
 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: