feat(L2): Phase 3b Stage 1b — preservation_l2 β-case for closed TFunEff substituents

hyperpolymath · claude · hyperpolymath · commit 3413a728ff7e · 2026-05-30T20:17:57.000+01:00
Ships the L2-judgment half of Stage 1b. Closes the [T_App_L2_Eff] β-case for T1 = TFunEff Ta Tb R_in_v R_out_v under the three-condition statement (P1 leaf-only body + P2 regions ⊆ R_in_v + P3 closure of v2). Mirrors PR #228's [preservation_l2_app_eff_beta_linear] (Phase 4a, linear T1) and Phase 4b's [preservation_l2_app_eff_beta_ground_nonlinear] (ground-non-linear T1) structurally with the same `value_R_G_preserving_l1`-collapse pattern. Two Qed lemmas: - `preservation_l2_app_eff_beta_tfuneff_l1` — the L1-level kernel. Inverts the lambda derivation through `T_Lam_L1_Linear_Eff` / `T_Lam_L1_Affine_Eff`; collapses R_in = R1 = R and G'' = G' = G via `value_R_G_preserving_l1`; then defers to the substitution kernel `subst_typing_gen_l1_m_tfuneff` (Phase 3b Stage 1b, this branch's prior commit) at k = 0. - `preservation_l2_app_eff_beta_tfuneff` — the L2 wrapper. Inverts both `has_type_l2` hypotheses through `L2_lift_l1` (the `T_App_L2_Eff` cases discriminate via expression-shape mismatch), then defers to the L1 kernel and re-lifts via `L2_lift_l1`. Combined with PRs #228 (Phase 4a, linear T1) and #233 (Phase 4b, ground-non-linear T1), this closes the `T_App_L2_Eff` β-case for T1 ∈ {linear, ground-non-linear, TFunEff}. Phase 4d (compound non- linear EPair / EInl / EInr / EEcho) remains open at Phase 5. Print Assumptions verdict: - preservation_l2_app_eff_beta_tfuneff_l1: Closed under the global context - preservation_l2_app_eff_beta_tfuneff: Closed under the global context Zero new axioms. Zero new admits. The mechanised soundness-gap witnesses for the conditional form are preserved in: - Counterexample_L2.v (PR #234, Phase 4c) — fresh-region gap (the counterexample to dropping P2). - Counterexample_L2_nested.v (Stage 1a, this PR's predecessor #252) — nested-lambda gap (the counterexample to dropping P1). The two files together justify why Stage 1 ships the two-condition (plus P3 closure) statement rather than an unconditional version. Stage 4 (#242) achieves the unconditional form once the L4 annotation extension (#240) and CPS argument (#241) land — the proof content of this PR's `closed_value_typing_*` family is reused unchanged in Stage 4 as the closure-discharge kernel. Also: STATE.a2ml refreshed — last_action now records the full Stage 1b deliverable surface; next_action advances to Stages 2-4. Owner-directive compliance (CLAUDE.md 2026-05-27): - ✅ No touch to formal/Semantics.v / Typing.v / Counterexample.v. - ✅ No closure of residual Semantics_L1.v admits attempted. - ✅ Anti-pattern detector clean. - ✅ Strictly NEW infrastructure orthogonal to legacy. Refs: - ephapax issue #249 (Stage 1b tracking — closes via this PR). - ephapax PR #252 (Stage 1a prerequisite). - ephapax issue #239 (parent Stage 1; closes via #252 + this PR). - formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3b Stage 1b. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
@@ -6,9 +6,9 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Phase D slice 4 Phase 3b Stage 1b (sibling to #239 — file as follow-up sub-issue): implement the deferred substitution-lemma half. (a) `closed_value_typing_G_poly_l1_m` helper in `formal/Semantics_L1.v` (G-polymorphic retype for closed TFunEff values, addressing the structural blocker discovered in Stage 1a). (b) `subst_typing_gen_l1_m_tfuneff` Qed mirroring `subst_typing_gen_l1_m_ground_nonlinear` (~300 lines); inner T_Lam_L1_*_Eff cases exfalso via the `tfuneff_lambda_free` precondition; direct (P1, P2) hypothesis form (no CPS yet — Stage 3 introduces CPS). May add a third precondition `expr_closed_below 0 v = true` to handle the G-mismatch at compound binder rules; document as Stage 1 restriction lifted in Stage 3/4. (c) `preservation_l2_app_eff_beta_tfuneff_l1` + L2 wrapper Qed in `formal/TypingL2.v` under the 2-condition statement: `tfuneff_lambda_free ebody = true ∧ regions_introduced_by ebody ⊆ R_in_v`. 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 — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority."
-last_action: "Phase D slice 4 Phase 3b Stage 1a LANDED (2026-05-30 PM, this PR): mechanised soundness-gap witness + Stage 1 syntactic infrastructure. (1) `tfuneff_lambda_free : expr -> bool` Fixpoint added to `formal/Syntax.v` (conservative leaf-only predicate; `false` on every `ELam`, compositional `andb` propagation through compound forms). (2) `formal/Counterexample_L2_nested.v` — three Qed lemmas (`e_before_typed`, `e_step`, `e_after_untypable`) mechanising the nested-TFunEff soundness gap with `outer = ELam T_v (ELam (TBase TUnit) (EVar 1))` configuration where inner R_in_inner = [r2] but substituent R_in_v = []; e_after = ELam TUnit v fails to retype the body at `[r2] ⊄ [] = R_in_v`. (3) Wired into `_CoqProject` after `Counterexample_L2.v`. (4) `SUBST-LEMMA-GENERALIZATION-DESIGN.md` gained a 'Phase 3b Stage 1a (landed) — split from Stage 1' subsection inside the Phase 3b resolution section, documenting the Stage 1a / Stage 1b split and the structural blocker (G-mismatch at compound binder rules — `tfuneff_lambda_retype_l1_m` preserves G but IH expects post-e1 G' with different used-flags) that motivated the split. Stage 1b (substitution lemma + preservation_l2 wrapper) ships next session via a follow-up sub-issue. Build oracle: coqc 8.18.0 clean across all 12 .v files; Print Assumptions on all three new Qed lemmas reports 'Closed under the global context' (zero new admits/axioms). Owner-directive compliance: ✅ no Semantics.v / Typing.v / Counterexample.v touch; ✅ no residual Semantics_L1.v admit closure attempted; ✅ anti-pattern detector clean. Sibling counterexample artifact to `Counterexample_L2.v` (PR #234) for the nested-lambda soundness-gap class; the two together justify the two-condition (P1 = `tfuneff_lambda_free`, P2 = `regions_introduced_by ⊆ R_in_v`) preservation_l2 statement Stage 1b delivers."
-updated: 2026-05-30T00:00:00Z
+next_action: "Phase D slice 4 Phase 3b Stages 2-4 (#240/#241/#242): Stage 1 (both 1a + 1b) complete. Stages 2-4 sequenced per the owner-approved 4-stage plan: Stage 2 (#240) ELam annotation extension — independent of Stage 1, ships when prioritised; Stage 3 (#241) CPS + relaxed Phase 3b — blocked on Stage 2; Stage 4 (#242) compound non-linear + unconditional preservation_l2 — blocked on Stage 3. Stage 4's destination collapses Stage 1b's three preconditions (P1 = tfuneff_lambda_free, P2 = regions_introduced_by ⊆ R_in_v, P3 = expr_closed_below 0 v) once typing-derived closure invariants land. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted`; no touching `Semantics.v` / `Typing.v` / `Counterexample.v`; no closure of residual `Semantics_L1.v` admits — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority."
+last_action: "Phase D slice 4 Phase 3b Stage 1b LANDED (2026-05-30 PM, this PR): elegance-first path-(i) substitution-lemma + L2 β wrapper, zero axioms. (1) Syntax.v: `expr_closed_below : nat -> expr -> bool` Fixpoint (canonical CS predicate, bool per post-redesign convention); `closed_below_shift_id` (closed terms shift-invariant); `expr_closed_below_shift_mono` (closure survives shifting); `ctx_mark_used_app_lt` (mark_used commutes with context append). (2) Semantics_L1.v: `closed_below_k_typing_outer_tail_irrelevant_l1_m` (the body-transfer core — structural induction over 28+ typing rules; closed-below-k terms' typing depends only on G's first k positions); `closed_value_typing_G_poly_l1_m` (any-G' form per elegance-first 'state what's actually true'); `closed_value_typing_RG_poly_l1_m` (combined RG-poly via chain to tfuneff_lambda_retype_l1_m); `closed_value_shift_id_l1_m` (cutoff-0 wrapper); `value_TFunEff_R_subset_R_in_l1_m` (extracts R ⊆ R_in from TFunEff value typing); `sub_R_in_R_in_via_value_l1_m` (chain helper packaging count_occ_le_l1_m + R-subset for compound-rule call sites); `subst_typing_gen_l1_m_tfuneff` (~300 lines mirroring Phase 2's ground-nonlinear template; inner T_Lam_L1_*_Eff cases discharge via P1 discriminate; compound rules use closed_value_typing_RG_poly_l1_m + sub_R_in_R_in_via_value_l1_m for the G-mismatch). (3) TypingL2.v: `preservation_l2_app_eff_beta_tfuneff_l1` (β-case kernel) + `preservation_l2_app_eff_beta_tfuneff` (L2 wrapper) under the three-condition statement (P1 leaf-only + P2 regions ⊆ R_in_v + P3 closure of v2). Build oracle: coqc 8.18.0 clean across all 12 .v files; Print Assumptions on every new Qed lemma reports 'Closed under the global context' (zero new admits / axioms). Owner-directive compliance: ✅ no Semantics.v / Typing.v / Counterexample.v touch; ✅ no residual Semantics_L1.v admit closure attempted; ✅ anti-pattern detector clean. Design decisions baked in per elegance-first priority: bool predicate (matches post-redesign style), any-G' statement form (the genuinely true claim), P1 RETAINED (re-staging is owner territory), staging-as-is (PR-level decisions don't deviate from owner-approved 4-stage plan)."
+updated: 2026-05-30T20:00:00Z
 
 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):
 # Captured durable directive — preservation work is the four-layer redesign,
diff --git a/formal/TypingL2.v b/formal/TypingL2.v
@@ -574,3 +574,122 @@ Proof.
     eapply preservation_l2_app_eff_beta_ground_nonlinear_l1; eassumption.
   - exfalso. inversion Hval.
 Qed.
+
+(** ===== Phase D slice 4 Phase 4c (Stage 1b) — β-case closure for
+    closed TFunEff substituents in leaf-only bodies ====================
+
+    Mirrors [preservation_l2_app_eff_beta_linear] (Phase 4a, PR #228)
+    and [preservation_l2_app_eff_beta_ground_nonlinear] (Phase 4b)
+    but uses [Semantics_L1.subst_typing_gen_l1_m_tfuneff] (Phase 3b
+    Stage 1b) for the L1 substitution step. Covers T1 = TFunEff Ta Tb
+    R_in_v R_out_v — TFunEff-typed function arguments.
+
+    Two-condition statement (per ephapax issue #239's owner-approved
+    Stage 1 framing + Stage 1b's path-(i) closure precondition):
+
+    - [tfuneff_lambda_free ebody = true] (P1): the OUTER lambda's body
+      [ebody] is leaf-only with respect to TFunEff-typed lambdas.
+      Stage 3 (#241) relaxes via CPS once [declared_lambda_r_ins ⊆
+      R_in_v] becomes derivable from typing.
+
+    - [(forall r, In r (regions_introduced_by ebody) -> In r R_in_v)]
+      (P2): every region introduced syntactically in [ebody] is
+      contained in the substituent's declared input env.
+      [Counterexample_L2.v] (PR #234) mechanises the soundness gap
+      this precondition rules out (fresh-region introduction
+      under a stale lambda capture).
+
+    - [expr_closed_below 0 v2 = true] (P3): the substituent is
+      closed. Stage 4 (#242) replaces with a typing-derived
+      closure invariant.
+
+    The mechanised soundness-gap witnesses for the conditional form
+    live in [Counterexample_L2.v] (fresh-region gap, the
+    counterexample to dropping P2) and [Counterexample_L2_nested.v]
+    (nested-lambda gap, the counterexample to dropping P1). The two
+    files together justify why Stage 1 ships the two-condition (plus
+    P3 closure) statement rather than an unconditional version —
+    Stage 4 (#242) achieves the unconditional form once the L4
+    annotation extension (#240) and CPS argument (#241) land.
+
+    Combined with PRs #228 (Phase 4a, linear T1) and #233 (Phase 4b,
+    ground-non-linear T1), this closes the [T_App_L2_Eff] β-case for
+    T1 ∈ {linear, ground-non-linear, TFunEff}. Phase 4d (compound
+    non-linear EPair / EInl / EInr / EEcho) remains open (Phase 5).
+
+    Refs [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md] Phase 3b
+    Stage 1b, [PRESERVATION-DESIGN.md §5.1], ephapax issue #249,
+    ephapax issue #239 (parent Stage 1), [Counterexample_L2.v] +
+    [Counterexample_L2_nested.v] (mechanised soundness-gap witnesses). *)
+
+Lemma preservation_l2_app_eff_beta_tfuneff_l1 :
+  forall m R R1 G G' G'' v2 Ta Tb R_in_v R_out_v T2 R_in R_out ebody,
+    is_value v2 ->
+    tfuneff_lambda_free ebody = true ->
+    (forall r, In r (regions_introduced_by ebody) -> In r R_in_v) ->
+    expr_closed_below 0 v2 = true ->
+    TypingL1.has_type_l1 m R  G  (ELam (TFunEff Ta Tb R_in_v R_out_v) ebody)
+                                 (TFunEff (TFunEff Ta Tb R_in_v R_out_v) T2 R_in R_out) R1 G' ->
+    TypingL1.has_type_l1 m R1 G' v2 (TFunEff Ta Tb R_in_v R_out_v) R_in G'' ->
+    TypingL1.has_type_l1 m R  G  (subst 0 v2 ebody) T2 R_out G''.
+Proof.
+  intros m R R1 G G' G'' v2 Ta Tb R_in_v R_out_v T2 R_in R_out ebody
+         Hval Hflam Hreg Hclos Hlam Harg.
+  inversion Hlam; subst.
+  - (* T_Lam_L1_Linear_Eff: body at R_in / (Tfun, false)::G''
+       → R_out / (Tfun, true)::G''. Use value_R_G_preserving on Harg
+       to collapse R_in = R1 = R and G'' = G' = G. *)
+    destruct (value_R_G_preserving_l1 _ _ _ _ _ _ _ Hval Harg) as [<- <-].
+    eapply subst_typing_gen_l1_m_tfuneff with
+      (k := 0) (u_in := false)
+      (Gin := (TFunEff Ta Tb R_in_v R_out_v, false) :: G'')
+      (Gout := (TFunEff Ta Tb R_in_v R_out_v, true) :: G'').
+    + unfold ctx_extend in *. eassumption.
+    + reflexivity.
+    + exact Hval.
+    + exact Hflam.
+    + exact Hreg.
+    + exact Hclos.
+    + exact Harg.
+    + reflexivity.
+  - (* T_Lam_L1_Affine_Eff: body output is [(Tfun, u) :: G''] for some [u]. *)
+    destruct (value_R_G_preserving_l1 _ _ _ _ _ _ _ Hval Harg) as [<- <-].
+    eapply subst_typing_gen_l1_m_tfuneff with
+      (k := 0) (u_in := false)
+      (Gin := (TFunEff Ta Tb R_in_v R_out_v, false) :: G'')
+      (Gout := (TFunEff Ta Tb R_in_v R_out_v, _) :: G'').
+    + unfold ctx_extend in *. eassumption.
+    + reflexivity.
+    + exact Hval.
+    + exact Hflam.
+    + exact Hreg.
+    + exact Hclos.
+    + exact Harg.
+    + reflexivity.
+Qed.
+
+(** L2-judgment wrapper for [preservation_l2_app_eff_beta_tfuneff_l1].
+
+    Inverts both [has_type_l2] hypotheses through [L2_lift_l1] (the
+    [T_App_L2_Eff] cases discriminate: the lambda's head is [ELam]
+    not [EApp], and the argument is a value so it cannot be [EApp]),
+    then defers to the L1 kernel and re-lifts via [L2_lift_l1]. *)
+Lemma preservation_l2_app_eff_beta_tfuneff :
+  forall m R R1 G G' G'' v2 Ta Tb R_in_v R_out_v T2 R_in R_out ebody,
+    is_value v2 ->
+    tfuneff_lambda_free ebody = true ->
+    (forall r, In r (regions_introduced_by ebody) -> In r R_in_v) ->
+    expr_closed_below 0 v2 = true ->
+    has_type_l2 m R  G  (ELam (TFunEff Ta Tb R_in_v R_out_v) ebody)
+                        (TFunEff (TFunEff Ta Tb R_in_v R_out_v) T2 R_in R_out) R1 G' ->
+    has_type_l2 m R1 G' v2 (TFunEff Ta Tb R_in_v R_out_v) R_in G'' ->
+    has_type_l2 m R  G  (subst 0 v2 ebody) T2 R_out G''.
+Proof.
+  intros m R R1 G G' G'' v2 Ta Tb R_in_v R_out_v T2 R_in R_out ebody
+         Hval Hflam Hreg Hclos Hlam Harg.
+  inversion Hlam as [m0 R0 G0 e0 T0 R0' G0' Hlam_l1 | ]; subst.
+  inversion Harg as [m0' R0'' G0'' e0' T0' R0''' G0''' Harg_l1 | ]; subst.
+  - apply L2_lift_l1.
+    eapply preservation_l2_app_eff_beta_tfuneff_l1; eassumption.
+  - exfalso. inversion Hval.
+Qed.
