Phase 3b Stage 3: relaxed restriction via declared_lambda_r_ins + CPS substitution lemma signature

[hyperpolymath]

Stage 3 of the 4-stage Phase 3b resolution plan per #235. Blocked on Stage 2 (ELam annotation). Owner-approved 2026-05-30.

Motivation

Stage 1 ships Phase 3b under the leaf-only restriction (tfuneff_lambda_free ebody). Stage 3 RELAXES this once Stage 2's ELam annotation makes inner R_in/R_out syntactically visible.

Deliverables

1. declared_lambda_r_ins : expr -> list region_name — syntactic Fixpoint in formal/Syntax.v. Walks ELam T R_in R_out body and accumulates R_in ++ declared_lambda_r_ins body. (Defined in Stage 2 already; Stage 3 uses it.)

2. CPS-form substitution lemma: replace

   has_type_l1 m R (remove_at k Gin) v (TFunEff Targ Tret R_in_v R_out_v) R (remove_at k Gin)

   with the continuation-passing form

   (forall R'' G_local,
      (forall r, In r R'' -> In r R_in_v) ->
      has_type_l1 m R'' G_local v (TFunEff Targ Tret R_in_v R_out_v) R'' G_local)

   in subst_typing_gen_l1_m_tfuneff's hypothesis list.

3. Relaxed precondition: replace tfuneff_lambda_free e = true with

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

   This combines with the (retained) regions_introduced_by e ⊆ R_in_v precondition.

4. Proof body update: inner T_Lam_L1_*_Eff cases now CONSTRUCTIVELY discharge by:

   • Extracting R_in_inner from the syntactic annotation (Stage 2's premise gives R_in_inner ⊆ declared_lambda_r_ins e ⊆ R_in_v).
   • Invoking the CPS-form v-typing at R_in_inner.
   • Recursing on the body with the CPS predicate threaded.

5. preservation_l2_app_eff_beta_tfuneff_l1 updated: drop tfuneff_lambda_free condition. Conditional preservation_l2's nested-condition collapses.

6. Counterexample_L2_nested.v stays Qed but is annotated as "superseded by Stage 3" — kept for historical/regression value.

Why CPS form is necessary HERE

In Stage 1's leaf-only restriction, inner T_Lam_L1_*_Eff cases are exfalso — v is never retyped at fresh R_in_inner's. Direct (P1, P2) hypotheses suffice.

In Stage 3's relaxed restriction, inner cases ARE constructive — v retypes at potentially-arbitrary R_in_inner's. The direct form would need v's typing parametric over an unbounded family of R's; CPS form bundles "v retypes anywhere satisfying P" into a single hypothesis the caller discharges once.

Sets cross-cutting precedent

Stage 3 is the first proof in the codebase using higher-order CPS-style hypotheses. Sets the pattern Stage 4 (compound non-linear) inherits — illuminates where future cross-cutting invariants live.

Owner-directive compliance

• ✅ No Semantics.v / Typing.v / Counterexample.v touch.
• ✅ No new Axiom or Admitted markers.
• ✅ No closure of residual Semantics_L1.v admits — strictly NEW infrastructure under post-Stage-2 ELam annotation.

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 3 supersedes its restriction).
• Stage 2 (#TBD2) — ELam annotation extension (Stage 3 blocker).
• Stage 4 (#TBD4) — Phase 5 compound non-linear (Stage 3's CPS precedent feeds it).

🤖 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 (this issue supersedes its restriction).
• Stage 2: Phase 3b Stage 2 (L4 track): ELam annotation extension — R_in / R_out as program-level commitments #240 — ELam annotation extension. Blocker for this issue.
• Stage 3 (this issue): Phase 3b Stage 3: relaxed restriction via declared_lambda_r_ins + CPS substitution lemma signature #241 — relaxed Phase 3b + CPS. Blocked on Phase 3b Stage 2 (L4 track): ELam annotation extension — R_in / R_out as program-level commitments #240.
• Stage 4: Phase 3b Stage 4 (Phase 5): compound non-linear values + unconditional preservation_l2 #242 — compound non-linear (inherits the CPS precedent this issue establishes).

Parent finding: #235.