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),
#235 (this finding).

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 4b — ground-non-linear T1 path for the `T_App_L2_Eff` β-case (uses Phase 2's `subst_typing_gen_l1_m_ground_nonlinear`). Then Phase 4c (TFunEff non-linear T1, blocked on Phase 3b per issue #225) and Phase 4d (compound, deferred to Phase 5). Phase 4a (this slot's predecessor) shipped `preservation_l2_app_eff_beta_linear_l1` + `preservation_l2_app_eff_beta_linear` in TypingL2.v, closing the β-case for linear T1. Phase 3b is still parked at issue #225 with three candidate solutions; Phase 4a prototyping confirmed the substitution shape used for linear T1 (k=0, raw cons in Gin/Gout, m-poly via `linear_value_retype_l1_m` for the Affine branch). For 3b, the actual subst shape will mirror Phase 4a's but with the value being a TFunEff lambda — the substitution premise will need a TFunEff-typed substituend at the threaded R, with the side condition propagating through. Recommend prototyping Phase 4c next (it forces 3b's design hand). 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 4a LANDED (2026-05-30, this PR): `preservation_l2_app_eff_beta_linear_l1` + `preservation_l2_app_eff_beta_linear` added to `formal/TypingL2.v`. The L1-level kernel takes inverted T_App_L2_Eff premises (a TFunEff lambda + a value argument typed at linear T1) and produces the post-β L1 typing via `subst_typing_gen_l1_m` at k=0. The L2 wrapper inverts both has_type_l2 hypotheses through L2_lift_l1 (T_App_L2_Eff discriminates: lambda's head is ELam not EApp; argument is a value so cannot be EApp). Two structural reductions inside the kernel: inversion on Hlam forces T_Lam_L1_*_Eff (the only formation rules producing TFunEff), exposing body typing at R_in; `value_R_G_preserving_l1` on Harg collapses R_in→R, G''→G. Then subst at k=0 with raw cons in the `with` clause (ctx_extend was too opaque for unification of remove_at 0 _ = G'') — and for the Affine branch, the linear v2 is re-derived at Linear mode via local helper `linear_value_retype_l1_m` (because subst_typing_gen_l1_m's premise 5 uses the bare `|=L1` notation which is Linear-mode-only). The same PR hotfixes a duplicate `tfuneff_lambda_retype_l1_m` from PR #223 + PR #224 (parallel-session merge collision); kept the chronologically-first definition (Hval, Ht, HR' arg order) and removed the second. Coqc 8.18.0 clean rebuild across all 10 .v files. Zero new admits/axioms (Print Assumptions confirms only the pre-existing `region_liveness_at_split_l1_gen` axiom inherited via `subst_typing_gen_l1_m`). `Semantics.v`/`Typing.v`/`Counterexample.v` untouched. Phase 4a is clean infrastructure composable with `preservation_l2_via_l1` toward full `preservation_l2` over has_type_l2."
+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 4b (parallel session PR #233) + Phase 4c counterexample (PR #234 auto-merge pending) are both unaffected — 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) auto-merge pending. 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: