docs: Phase D slice 4 Phase 3b design-gap finding — escalate per CLAUDE.md DO #4 (closes nothing, files #235)

Pre-implementation review of Phase 3b's option (a) precondition

  (forall r, In r (regions_introduced_by e) -> In r R_in_v)

found it 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 the IH at formal/Semantics_L1.v:1929-1942). Inner
T_Lam_L1_*_Eff bodies type at the lambda's declared R_in_inner. R_in
is type-level — it lives in the TFunEff slot of the function's TYPE,
not in syntax. `regions_introduced_by(e)` only collects ERegion
subterms' first arguments; R_in_inner is invisible to it.

`tfuneff_lambda_retype_l1_m` (PR #224) requires R' ⊆ R_in_v to
discharge T_Lam_L1_*_Eff's side condition. We have no way to bound
inner R_in by R_in_v.

Phase 2's `subst_typing_gen_l1_m_ground_nonlinear` dodges this via
`ground_nonlinear_retype_l1_m`, which is fully (m, R, G)-polymorphic.
Phase 3b's TFunEff retype has no analogous escape.

Three resolution options documented:
  1. Syntactic helper `declared_lambda_r_ins` — requires ELam
     annotation extension (parameter type only in current syntax).
  2. Semantic precondition over the derivation — clean meaning,
     awkward in Coq.
  3. Leaf-only Phase 3b via `tfuneff_lambda_free e` predicate —
     tactical landing; Phase 5 compound-value redesign subsumes
     (1)/(2) at leisure.

Recommended: option (3). Owner decision required before Phase 3b
implementation can start.

This PR contains documentation only:
  - formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md gains a Phase 3b
    addendum documenting the gap and three resolution options.
  - .machine_readable/6a2/STATE.a2ml flips phase to
    `blocked-on-owner-decision` with next_action pointing at #235.

No formal/*.v changes.

Predecessor PRs unaffected:
  - Phase 4a (#228) MERGED.
  - Phase 4b (parallel session, #233) MERGED.
  - Phase 4c counterexample (#234) auto-merge pending.

Phase 4c's `Counterexample_L2.v` independently justifies the
conditional preservation_l2 statement regardless of which Phase 3b
resolution lands.

Per CLAUDE.md owner directive §DO #4 (escalate before patching):
this PR IS the escalation.

Owner-directive compliance:
  - No Semantics.v / Typing.v / Counterexample.v touch
  - No new Axiom / Admitted markers
  - No closure of residual Semantics_L1.v admits
  - No sibling-region-disjointness side conditions
  - No proposal to close `Theorem preservation` to Qed.

Refs: #225 (Phase 3b parking lot), #230 (regions_introduced_by
helper), #233 (Phase 4b), #234 (Phase 4c counterexample),

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: "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."
+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)."
 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,34 @@ 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 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: