Phase 3b design gap: option (a) precondition insufficient for T_Lam_L1_*_Eff body cases

[hyperpolymath]

Finding

Phase D slice 4 Phase 3b's stated precondition

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

(option (a) per formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md) is insufficient to discharge the 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 (mirroring Phase 2's subst_typing_gen_l1_m_ground_nonlinear at lines 1929-1942 of formal/Semantics_L1.v). For inner T_Lam_L1_*_Eff cases, the body sub-derivation is typed at the inner lambda's declared R_in_inner, not at the outer R or at any region listed in regions_introduced_by(e):

• T_Lam_L1_Linear_Eff / T_Lam_L1_Affine_Eff formation rules (TypingL1.v:221, 226):

  R_in ; ctx_extend G T1 |=L1[m] ebody : T2 -| R_out ; ((T1, _) :: G)
  

  The body is typed at R_in, an arbitrary declared region environment in the FUNCTION TYPE.

• The IH at this case wants v retyped at R_in_inner. The available retype lemma is tfuneff_lambda_retype_l1_m (Semantics_L1.v:1257-1278), which requires R' ⊆ R_in_v.

• Neither regions_introduced_by(e) (syntactic ERegion subterms) nor the outer R contains R_in_inner's regions in general. R_in_inner is type-level, not syntactic.

Phase 2 dodge that doesn't apply

Phase 2's subst_typing_gen_l1_m_ground_nonlinear discharges the same cases via ground_nonlinear_retype_l1_m, which is fully (m, R, G)-polymorphic — ground non-linear values type at ANY region env. Phase 3b's TFunEff retype carries the R' ⊆ R_in_v obligation, which has no analogous escape hatch.

Three resolution options

(1) Strengthen the precondition to a type-level over-approximation

Add a helper Fixpoint declared_lambda_r_ins (e : expr) : list region_name that walks ELam T body, extracts R_in from T when T = TFunEff _ _ R_in _, and unions with the recursive call.

Blocker: ELam syntax (Syntax.v) carries the parameter type, not the function type. The function type's R_in is determined by typing, not syntax. So this helper can't be defined as a syntactic Fixpoint without an annotation extension to ELam.

(2) Semantic precondition over the derivation

State the precondition as: "for every sub-derivation Htype' of Htype at R'_in, R'_in ⊆ R_in_v". Clean meaning, awkward in Coq (would require either an inductive predicate over has_type_l1 derivations or a fixpoint indexed by derivation depth).

(3) Restrict scope — Phase 3b leaf-only

Ship Phase 3b only for the leaf-lambda case: bodies that do not themselves contain T_Lam_L1_*_Eff sub-derivations. Add an inductive predicate lambda_free e and condition the lemma on it. Document the limitation; defer the recursive case to Phase 5 (compound non-linear).

Recommendation

Option (3) as a tactical landing for Phase 3b. The leaf-only case unblocks the immediate consumer (preservation_l2 β-case for TFunEff arguments whose body uses ERegion but not nested function abstractions). The recursive case rides Phase 5's compound-value redesign.

Owner decision needed before Phase 3b implementation can start.

Owner-directive compliance

• Does NOT propose closing legacy preservation in Semantics.v.
• Does NOT extend Semantics.v.
• Does NOT close residual Semantics_L1.v admits.
• Reports a structural finding before patching; per CLAUDE.md §"DO" Claude/ephapax linear types e00 zs #4 ("Escalate before patching when a side-condition is needed").

References

• formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3 (canonical design).
• formal/Semantics_L1.v:1257-1278 — tfuneff_lambda_retype_l1_m retype lemma.
• formal/Semantics_L1.v:1812-2073 — Phase 2 sibling lemma (subst_typing_gen_l1_m_ground_nonlinear) for pattern.
• formal/Semantics_L1.v:1929-1942 — Phase 2's T_Lam_L1_*_Eff cases (where Phase 3b breaks).
• formal/TypingL1.v:221-229 — T_Lam_L1_*_Eff formation rules carrying the body's R_in.
• PR Phase D slice 4 Phase 3b — TFunEff substitution-lemma extension (deferred from #224) #225 — Phase 3b inference + design predecessor.
• PR feat(syntax): regions_introduced_by helper — Phase 3b scaffolding (#225) #230 — regions_introduced_by helper (option (a)'s syntactic component).
• PR docs+test: Phase D slice 4 Phase 4c — mechanised soundness-gap counterexample for TFunEff β #234 — Phase 4c counterexample mechanising the conditional preservation_l2 path.

[hyperpolymath]

Resolution: 4-stage staged plan (owner-approved 2026-05-30)

The original three options framing has been superseded by a staged plan that captures the value of each "Interesting" bullet without committing to any single option's downsides:

Stage	Issue	Scope	Captures value of
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.
2 (parallel L4 track)	#240	ELam T_param R_in R_out body annotation extension. AST + typing rule + cascading inversion patterns.	Option (1) — L4-aligned "type-level → program-level commitments".
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, illuminating cross-cutting invariants.
4 (Phase 5)	#242	Compound non-linear values + region-substitution machinery + unconditional preservation_l2.	The final destination — closes the last soundness condition.

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 fresh-region gap, Counterexample_L2_nested.v for 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.
• Stage 3 introduces CPS proof style at the only point where it's strictly necessary — the relaxed Phase 3b's inner T_Lam_L1_*_Eff cases.
• Stage 4 inherits the CPS precedent from Stage 3 and closes the last soundness condition. Phase 3b becomes unconditional and preservation_l2 Qed over has_type_l2.

Sequencing

• Stage 1 implementation green-lit (Phase 3b Stage 1: leaf-only substitution lemma + 2-condition preservation_l2 + Counterexample_L2_nested #239). 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 is independent of Stage 1.

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 that has 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 not over-engineered, (4) reaches unconditional preservation_l2 as the natural sum of (1) + (2) + (3) applied in sequence.

Owner-directive compliance (across all 4 stages)

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

Closing this issue once Stage 1 (#239) is implemented; until then it remains open as the parent-finding tracker.

[hyperpolymath]

Closing — Signal A (analysis-gap ticket resolved to plan). The design gap analysed here resolved to the 4-stage plan now documented in formal/PRESERVATION-DESIGN.md and tracked stage-by-stage in #239 (Stage 1, now split into #252 Stage 1a + #249 Stage 1b), #240 (Stage 2), #241 (Stage 3), and #242 (Stage 4). The analysis itself is complete; the implementation work lives on the stage tickets.