Phase 3b Stage 4 (Phase 5): compound non-linear values + unconditional preservation_l2

[hyperpolymath]

Stage 4 of the 4-stage Phase 3b resolution plan per #235. Multi-session scope. Owner-approved 2026-05-30. Equivalent to Phase 5 in SUBST-LEMMA-GENERALIZATION-DESIGN.md.

Motivation

Stage 3 lands the relaxed Phase 3b for TFunEff lambdas (post-Stage-2 ELam annotation + CPS proof style). The final soundness condition on preservation_l2_app_eff_beta_tfuneff_l1 — regions_introduced_by ebody ⊆ R_in_v — remains.

Stage 4 closes this last condition by addressing compound non-linear values as substituends and arguments: EPair, EInl, EInr, EEcho, and EBorrow of non-locations. These are the value-shape categories not covered by Phase 1 (ground non-linear), Phase 2 (substitution lemma), or Phase 3 (TFunEff lambdas).

Why compound non-linear is the last gap

The current Phase 4c soundness gap (Counterexample_L2.v) — "TFunEff value substituted inside fresh-region scope" — generalises to:

A substituend v whose typing depends on regions r ∈ R, when substituted into a context that extends R via fresh-region introduction, may fail to re-type.

For TFunEff lambdas the dependency is via the side condition forall r, In r R -> In r R_in_v (concentrated in T_Lam_L1_*_Eff). For compound non-linear values (e.g. EPair (ELam …) (ELoc l r) or EEcho T (ELam …)), the dependency is via sub-components' typings.

A general region-substitution lemma at the value level — "rewriting r ↦ r' in a well-typed value preserves typing under appropriate side conditions" — closes both cases.

Deliverables

1. Region-substitution machinery:

   • region_subst_value_l1 : value -> region_name -> region_name -> value
   • region_subst_typing_preserves_l1 lemma.
   • Per-shape sub-lemmas for compound values.

2. Phase 5 substitution-lemma extension: subst_typing_gen_l1_m_compound covering EPair / EInl / EInr / EEcho / EBorrow substituends. Builds on Stage 3's CPS proof style.

3. Unconditional preservation_l2: preservation_l2_app_eff_beta Qed (no soundness-class condition). β-case CLOSED for all substituend shapes.

4. Counterexample_L2.v and Counterexample_L2_nested.v: retained as regression witnesses but annotated as "resolved by Stage 4" — they showed soundness gaps that the region-substitution machinery now closes.

5. preservation_l2 Qed over has_type_l2 — combining the β-case (this stage) with the L2_lift_l1 case (already shipped via preservation_l2_via_l1, PR feat(L2): preservation_l2_via_l1 — Phase D slice 4 partial landing #211).

Sequencing

Stage 4 is the natural successor to Stage 3 once the CPS proof style is established. Internally splits into:

Sub-stage	Scope
4a	EPair non-linear
4b	EInl / EInr non-linear
4c	EEcho
4d	EBorrow of non-location values
4e	Region-substitution machinery (potentially earlier if independently useful)
4f	Unconditional preservation_l2 wrap

Owner-directive compliance

• ✅ No Semantics.v / Typing.v / Counterexample.v (legacy) touch.
• ✅ No Axiom / Admitted markers.
• ✅ Strictly NEW infrastructure under the layered (L1/L2/L3/L4) redesign.
• L1/L2 closure achieved without patching legacy preservation — the legacy theorem remains Admitted (PROVABLY FALSE) as the owner directive requires.

References

• Phase 3b design gap: option (a) precondition insufficient for T_Lam_L1_*_Eff body cases #235 — Phase 3b design-gap finding (parent).
• Stage 1 (#TBD1) — leaf-only Phase 3b.
• Stage 2 (#TBD2) — ELam annotation extension.
• Stage 3 (#TBD3) — CPS substitution + relaxed Phase 3b (Stage 4 blocker).
• formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 5 (canonical predecessor scope).
• formal/PRESERVATION-DESIGN.md §5 — L2 closure design.

🤖 Generated with Claude Code

[hyperpolymath]

Cross-references resolved

• Stage 1: Phase 3b Stage 1: leaf-only substitution lemma + 2-condition preservation_l2 + Counterexample_L2_nested #239 — leaf-only Phase 3b.
• Stage 2: Phase 3b Stage 2 (L4 track): ELam annotation extension — R_in / R_out as program-level commitments #240 — ELam annotation extension.
• Stage 3: Phase 3b Stage 3: relaxed restriction via declared_lambda_r_ins + CPS substitution lemma signature #241 — relaxed Phase 3b + CPS. Blocker for this issue.
• Stage 4 (this issue): Phase 3b Stage 4 (Phase 5): compound non-linear values + unconditional preservation_l2 #242 — compound non-linear + unconditional preservation_l2 (Phase 5).

Parent finding: #235.