Phase D slice 4 Phase 3b — TFunEff substitution-lemma extension (deferred from #224)

[hyperpolymath]

Context

Phase 3a (#224) shipped the retype half of Phase 3 per formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md — is_tfuneff_ty predicate and tfuneff_lambda_retype_l1_m lemma. The substitution-lemma extension was descoped from #224 after structural analysis.

This issue tracks Phase 3b: extend subst_typing_gen_l1_m (or a sibling lemma subst_typing_gen_l1_m_tfuneff_lambda) to cover T1 = TFunEff … lambda substituends, so that Phase 4 can close preservation_l2's T_App_L2_Eff β-case for the TFunEff non-linear T1 case.

The obstacle

Every compound case in subst_typing_gen_l1_m_ground_nonlinear (Phase 2) relies on the retype lemma being fully R-polymorphic (no side condition). For TFunEff lambda values, the retype lemma carries a side condition forall r, In r R' → In r R_in_arg, where R_in_arg is fixed by the value's type TFunEff T1 T2 R_in_arg R_out_arg.

The substitution lemma's compound cases need to retype the substituted value vv at threaded R values R_n arising inside the substitution target e. T_Region_L1 firings inside e introduce fresh regions r ∉ R_outer — and freshness wrt the threaded R does not imply r ∈ R_in_arg.

Concretely: in T_Region_L1's body, the new R is r' :: R_outer where r' is fresh wrt R_outer. To retype vv at r' :: R_outer, we need r' ∈ R_in_arg, but r' is fresh in a way that's unconstrained relative to R_in_arg.

Three candidate solutions

(a) Syntactic side condition on e

Add a Definition regions_introduced_by : expr → list region_name and require forall r, In r (regions_introduced_by e) → In r R_in_arg as a precondition. Each compound case threads the predicate to its sub-expressions (region-introductions in a parent expression contain those of all sub-expressions). T_Region_L1 case discharges r' ∈ R_in_arg directly from the side condition.

Pros: clean to state, syntactically computable.
Cons: propagating the predicate through ~28 cases is mechanical churn.

(b) Universal-R Hv_type with per-case side-condition discharge

Replace the simple Hv_type premise with a universal-R version:

(forall R_any,
   (forall r, In r R_any → In r R_in_arg) →
   has_type_l1 m R_any (remove_at k Gin) vv Tsub R_any (remove_at k Gin))

Each compound case picks the R it needs and discharges the side condition.

Pros: no new Definitions.
Cons: still doesn't help in T_Region_L1 (the new R contains a fresh region not necessarily in R_in_arg).

(c) Restrict to region-free terms

Add expr_strictly_free_of_region predicates for the introduced regions. Effectively restricts the lemma to terms without T_Region_L1 firings.

Pros: simple.
Cons: very restrictive; may not cover the actual Phase 4 use shape.

Recommendation

Prototype Phase 4 closure of preservation_l2's T_App_L2_Eff β-case first. The actual shape of subst 0 varg ebody (where ebody is vlam's body, typed at R_in_big not R_in_arg) will reveal whether T_Region_L1 firings inside ebody are a real obstacle or an edge case.

If the Phase 4 use shape only ever needs the substitution lemma for ebody with bounded R-flow, option (a) is appropriate. If T_Region_L1 inside ebody is generic, options (a)+(b) compose.

References

• formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md — original Phase 3 design.
• formal/Semantics_L1.v — subst_typing_gen_l1_m_ground_nonlinear (Phase 2 template) at line 1752.
• formal/Semantics_L1.v — tfuneff_lambda_retype_l1_m (Phase 3a, feat(L1): Phase D slice 4 Phase 3a — tfuneff_lambda_retype_l1_m + is_tfuneff_ty #224).
• .machine_readable/6a2/STATE.a2ml — next_action documents the three candidates.
• standards#134 — proof-debt epic.

[hyperpolymath]

Status drift (audit, 2026-05-30)

PR #230 (`feat(syntax): regions_introduced_by helper — Phase 3b scaffolding`) landed on main today, which commits to option (a) from the issue body's "Three candidate solutions" section: syntactic side condition on `e` with a `regions_introduced_by` predicate.

The remaining scope for closing #225 is therefore the substitution-lemma extension proper — wiring the new helper into `subst_typing_gen_l1_m` (or a sibling lemma) and discharging the per-case obligations through the ~28 compound cases the design doc enumerates.

PR #233 (Phase 4b — preservation_l2 β for ground-non-linear T1) is open, which suggests Phase 4's actual use shape is still being prototyped — per the issue body's recommendation, this is the right ordering (Phase 4 first, Phase 3b extension second once the use-shape obstacles are known).

(Audit/no-code: leaving the substitution-lemma extension itself for the owner who has Phase 4 context.)

[hyperpolymath]

Phase 4c prototyping: option (a)'s precondition is necessary AND blocks legitimate programs

Prototyping Phase 4c (TFunEff-T1 β-case) on paper reveals a concrete counterexample that constrains the design space.

Counterexample

Consider the program (Affine mode, schematic Coq):

```
T1 = TFunEff TUnit TUnit [] [] (* substituee's type, R_in_v = [] )
outer_lambda = ELam T1 (ERegion r2 (EVar 0)) ( body introduces fresh r2, returns the substituted var )
v2 = ELam TUnit EUnit ( a value of type T1 with R_in_v = [] *)
e_before = EApp outer_lambda v2
```

Input types via T_App_L2_Eff at `R = []`:

• `outer_lambda` types at `TFunEff T1 T1 [] []` via T_Lam_L1_Affine_Eff with R_in = [].
  • Body: T_Region_L1 fires (r2 fresh wrt [], r2 ∉ free_regions(T1) = []).
  • Inner: `[r2]; (T1, false) :: G ⊢ EVar 0 : T1 ⊣ [r2]; (T1, false) :: G` via T_Var_Unr_L1.
• `v2` types at `T1` via T_Lam_L1_Affine_Eff with R_in = [].

β-step (S_App_Fun): `subst 0 v2 (ERegion r2 (EVar 0)) = ERegion r2 v2`.

Post-β term `ERegion r2 v2` does not type at `R = []; G ⊢ ? : T1 ⊣ ?; G`:

• T_Region_L1: r2 fresh, r2 ∉ free_regions(T1) = []. Inner must type at `[r2]`.
• Inner `[r2]; G ⊢ v2 : T1` requires T_Lam_L1_*_Eff with side condition `forall r, In r [r2] → In r R_in_v = []`.
• r2 ∈ [r2] but r2 ∉ []. Side condition FAILS.

There is no other typing path: `v2 = ELam ...` only types via the *_Eff lambda formation rules, all of which carry the same side condition.

What this means for the three Phase 3b candidates

• Option (a) (`regions_introduced_by(e) ⊆ R_in_v`): makes the substitution lemma stateable and inapplicable to this counterexample. `regions_introduced_by(ERegion r2 (EVar 0)) = [r2]`, `R_in_v = []`, so `[r2] ⊆ []` is false. The lemma's precondition cannot be discharged at this β-site. Necessary, but not sufficient for full Phase 4c closure.
• Option (b) (universal-R Hv_type): same obstacle — the universal Hv_type still carries the side condition, which fails at the fresh-region introduction. Equivalent in power to (a).
• Option (c) (restrict to region-free `e`): rules out the counterexample by construction. Maximally rigorous but very restrictive.

The structural obstacle

T_Region_L1's premise `~ In r (free_regions T)` is what prevents the fresh r from being in R_in_v (since R_in_v ⊆ free_regions(TFunEff)). This is by design — regions are not supposed to leak into types that don't already mention them. But the consequence is: TFunEff values formed at narrow R_in cannot be re-typed inside broader region scopes, even via β-substitution that places them there.

This is the L1/L2 analogue of the legacy `Counterexample.v` soundness gap — preservation as stated is FALSE for a class of legitimate-looking programs.

Resolution paths (broader than (a)/(b)/(c))

1. (a) + conditional preservation_l2: add the syntactic precondition to preservation_l2's β-case. Preservation holds for programs where `regions_introduced_by(ebody) ⊆ R_in_v`; other programs are not in the theorem's scope. Honest but limits the theorem's reach.
2. Region-polymorphic TFunEff: change the type so `TFunEff T1 T2 R_in R_out` is polymorphic in additional regions that the body doesn't actually use. Major type-system change.
3. (c) restrict to region-free ebody: simplest but most restrictive.
4. L2-level region transfer combinator: introduce a new L2 rule that explicitly transfers a fresh region into a TFunEff lambda's R_in for the duration of a scope. Adds L2 expressiveness.

Recommendation

Ship Phase 3b with option (a) (the `regions_introduced_by` scaffold from #230 already supports this), then write Phase 4c conditionally — require the precondition on the β-step. Programs not satisfying the precondition are left as a documented soundness-gap class, mirroring how the legacy preservation handles its 10 `touches_region` RIGHT branches via `Counterexample.v`.

This keeps the layered design clean: Phase 3b ships the substitution lemma with option (a)'s precondition; Phase 4c ships preservation_l2 over the precondition-satisfying class; remaining programs become a known soundness-gap subclass requiring either (2) region-polymorphic TFunEff or (4) an L2 transfer combinator.

Refs: this prototype done on paper; the `/tmp/ephapax-phase-4b` parallel session is currently shipping Phase 4b (ground-non-linear T1) which doesn't hit this obstacle (ground values are fully (m, R)-polymorphic via `ground_nonlinear_retype_l1_m`).