feat(L1): Phase D slice 4 Phase 3b Stage 1a — tfuneff_lambda_free + Counterexample_L2_nested by hyperpolymath · Pull Request #252 · hyperpolymath/ephapax

hyperpolymath · 2026-05-30T17:16:05Z

Summary

Ships the Stage 1a slice of the four-stage Phase 3b resolution plan (parent #235 / Stage 1 #239 / Stages 2-4 #240-#242). Stage 1 splits into 1a (this PR — syntactic infrastructure + mechanised nested-lambda soundness-gap witness) and 1b (#249 — substitution lemma + preservation_l2 β wrapper) for shipping cadence.

What lands

NEW Fixpoint tfuneff_lambda_free : expr -> bool in formal/Syntax.v. Conservative leaf-only predicate: false on every ELam, compositional andb propagation through compound forms. Used by Stage 1b's substitution lemma to exfalso the inner T_Lam_L1_*_Eff cases.
NEW formal/Counterexample_L2_nested.v — three Qed lemmas (e_before_typed, e_step, e_after_untypable) mechanising the nested-TFunEff soundness gap. Sibling artifact to Counterexample_L2.v (PR docs+test: Phase D slice 4 Phase 4c — mechanised soundness-gap counterexample for TFunEff β #234): together the two files justify the two-condition preservation_l2 statement Stage 1 delivers — P1 (tfuneff_lambda_free ebody = true, rules out the nested-lambda gap class witnessed here) and P2 (regions_introduced_by ebody ⊆ R_in_v, rules out the fresh-region gap class witnessed in Counterexample_L2.v).
Wired into formal/_CoqProject after Counterexample_L2.v.
formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md gains a "Phase 3b Stage 1a (landed) — split from Stage 1" subsection documenting the 1a/1b split and the structural blocker (G-mismatch at compound binder rules).
.machine_readable/6a2/STATE.a2ml refreshes next_action to Stage 1b (Phase 3b Stage 1b: subst_typing_gen_l1_m_tfuneff + preservation_l2 β wrapper (deferred from #239) #249).

Configuration (nested-lambda counterexample)

outer    = ELam T_v (ELam (TBase TUnit) (EVar 1))
T_inner  = TFunEff (TBase TUnit) T_v [r2] [r2]
v        = ELam (TBase TUnit) EUnit   at T_v = TFunEff TUnit TUnit [] []
e_before = EApp outer v               at T_inner, R = []  (well-typed via T_App_L2_Eff)
e_after  = ELam (TBase TUnit) v       at T_inner, R = []  (untypable)

The inner lambda's body references the outer-bound variable via EVar 1; post-β substitutes v for the outer variable. The resulting ELam (TBase TUnit) v cannot retype the inner v at [r2] ⊄ [] = R_in_v.

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.

Test plan

just -f formal/Justfile all clean across all 12 .v files with coqc 8.18.0.
Print Assumptions on all three new Qed lemmas → Closed under the global context.
CI coq-build workflow passes (will check post-push).

Refs

Parent finding: Phase 3b design gap: option (a) precondition insufficient for T_Lam_L1_*_Eff body cases #235
Stage 1 tracking: Phase 3b Stage 1: leaf-only substitution lemma + 2-condition preservation_l2 + Counterexample_L2_nested #239 (partially closes — Stage 1a deliverables)
Stage 1b sub-issue: Phase 3b Stage 1b: subst_typing_gen_l1_m_tfuneff + preservation_l2 β wrapper (deferred from #239) #249
Stages 2-4: Phase 3b Stage 2 (L4 track): ELam annotation extension — R_in / R_out as program-level commitments #240 / Phase 3b Stage 3: relaxed restriction via declared_lambda_r_ins + CPS substitution lemma signature #241 / Phase 3b Stage 4 (Phase 5): compound non-linear values + unconditional preservation_l2 #242
Sibling counterexample: PR docs+test: Phase D slice 4 Phase 4c — mechanised soundness-gap counterexample for TFunEff β #234

🤖 Generated with Claude Code

…ounterexample_L2_nested Ships the Stage 1a slice of the four-stage Phase 3b resolution plan (parent #235 / Stage 1 #239 / Stages 2-4 #240-#242). Stage 1 splits into 1a (this PR — syntactic infrastructure + mechanised nested-lambda soundness-gap witness) and 1b (follow-up sub-issue — substitution lemma + preservation_l2 β wrapper). Ships: (1) NEW `Fixpoint tfuneff_lambda_free : expr -> bool` in `formal/Syntax.v`. Conservative leaf-only predicate: false on every `ELam`, compositional `andb` propagation through compound forms. Used by Stage 1b's substitution lemma to exfalso the inner `T_Lam_L1_*_Eff` cases. Stage 2 (#240) refines to TFunEff-specific once `ELam` carries `R_in / R_out` annotations. (2) NEW `formal/Counterexample_L2_nested.v` — three Qed lemmas (`e_before_typed`, `e_step`, `e_after_untypable`) mechanising the nested-TFunEff soundness gap. Configuration: outer = ELam T_v (ELam (TBase TUnit) (EVar 1)) T_inner = TFunEff (TBase TUnit) T_v [r2] [r2] v = ELam (TBase TUnit) EUnit at T_v = TFunEff TUnit TUnit [] [] e_before = EApp outer v at T_inner, R = [] (well-typed) e_after = ELam (TBase TUnit) v at T_inner, R = [] (untypable) The inner lambda's body references the outer-bound variable via EVar 1; post-β substitutes v for the outer variable. The resulting `ELam (TBase TUnit) v` cannot retype the inner v at `[r2] ⊄ [] = R_in_v` — T_Lam_L1_*_Eff's side condition `forall r, In r [r2] -> In r []` is contradicted by `In r2 [r2]`. Sibling artifact to `formal/Counterexample_L2.v` (PR #234): the two files together justify the **two-condition** preservation_l2 statement Stage 1 delivers — P1 (`tfuneff_lambda_free ebody = true`, rules out THIS file's nested-lambda gap class) and P2 (`regions_introduced_by ebody ⊆ R_in_v`, rules out Counterexample_L2.v's fresh-region gap class). (3) Wired `Counterexample_L2_nested.v` into `formal/_CoqProject` after `Counterexample_L2.v`. (4) `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md` gains a "Phase 3b Stage 1a (landed) — split from Stage 1" subsection documenting the Stage 1a / Stage 1b split and the structural blocker that motivated the split: Phase 3b's substitution lemma's compound rule cases (T_Let_L1 etc.) need to retype the substituent value `v` at different G (post-e1 used-flag updates), but `tfuneff_lambda_retype_l1_m` (PR #224) preserves G — unlike Phase 2's `ground_nonlinear_retype_l1_m` which is fully (R, G)-polymorphic. Stage 1b's machinery requires EITHER (a) a closed-value G-polymorphism helper or (b) a G-flag-polymorphic retype variant. Either path is its own sub-deliverable. (5) `.machine_readable/6a2/STATE.a2ml` refreshes next_action to Stage 1b (the deferred substitution-lemma + preservation wrapper half) and last_action to Stage 1a's deliverables. 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 (no sibling-region-disjointness, no region-weakening predicates on syntactic shape, no admit-shuffling, no legacy-preservation closure attempt). - ✅ Strictly NEW infrastructure orthogonal to legacy. Build oracle (coqc 8.18.0): clean across all 12 .v files. Print Assumptions on `e_before_typed`, `e_step`, `e_after_untypable` reports "Closed under the global context" (zero new admits/axioms). Refs: - ephapax issue #239 (Stage 1 tracking, this PR partial closure) - ephapax issue #235 (parent finding) - ephapax PR #234 (sibling counterexample for fresh-region gap) - ephapax PR #237 (4-stage resolution plan landed in design doc) - formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md §Phase 3b Stage 1a Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

… helpers (Syntax.v) Stage 1b's path-(i) machinery requires a syntactic closure predicate so that closed TFunEff values can be retyped at any G inside the substitution lemma's compound-rule cases. This commit ships the Syntax.v prerequisites; Semantics_L1.v body-transfer + closed-value G-poly helper + subst lemma follow in subsequent commits on this branch (single Stage 1b PR). Ships: (1) `Fixpoint expr_closed_below : nat -> expr -> bool` — canonical "no free de Bruijn variables ≥ k" check. Binder structure mirrors `shift` / `subst` (Syntax.v:542-606): - ELam _ e0: e0 at S k (one binder) - ELet e1 e2 / ELetLin e1 e2: e1 at k, e2 at S k - ECase e0 e1 e2: e0 at k, e1 and e2 at S k - All other forms: same k across sub-expressions `bool` target per the post-redesign Phase D convention (`is_linear_ty`, `is_ground_nonlinear_ty`, `tfuneff_lambda_free` are all bool); the legacy Prop predicates `expr_free_of_region` / `expr_strictly_free_of_region` are pre-redesign artefacts. (2) `Lemma closed_below_shift_id` — closed-below-c terms are shift- invariant at cutoff c. Proof: induction on e with c, d intro'd after `induction` to keep IH polymorphic over c. Each typing constructor's case dispatches via f_equal + IH application; the EVar case uses Nat.ltb_lt + Nat.leb_spec + lia. (3) `Lemma expr_closed_below_shift_mono` — closure is preserved under shifting at any cutoff. Required for the subst lemma's binder cases where the substituent gets shifted up by 1. (4) `Require Import Lia` — added for the EVar arithmetic case. Path-(i) elegance + correctness design choices baked in (this PR's stated priority hierarchy): - bool predicate target (matches post-redesign style; revising an earlier Prop draft). - The closed-value G-poly helper (in Semantics_L1.v, follow-up commit) will state "any G' works" — not "length-matched G'" — per "state what's actually true." - `tfuneff_lambda_free` (P1) precondition KEPT in the subst lemma (per "don't drop without owner consent" — the closure helper subsumes P1's exfalso content but re-staging is owner territory). 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 (canonical CS predicate; no sibling-region-disjointness, no region-weakening predicates on syntactic shape, no admit-shuffling, no legacy-preservation closure attempt). - ✅ Strictly NEW infrastructure orthogonal to legacy. Build oracle (coqc 8.18.0): clean across all 12 .v files post-edit. Refs: - ephapax issue #249 (Stage 1b tracking, this PR partial closure) - ephapax PR #252 (Stage 1a — tfuneff_lambda_free + Counterexample_L2_nested) - ephapax issue #239 (parent Stage 1) - formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3b Stage 1b Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Path-(i) machinery for the elegance-first Stage 1b. Closed TFunEff values are typed at ANY G — for closed values, G is genuinely irrelevant. The substitution lemma's compound-rule cases (next commit) consume this fact to discharge the G-mismatch gap that blocks `tfuneff_lambda_retype_l1_m` (G-preserving) from playing the same role Phase 2's `ground_nonlinear_retype_l1_m` plays for ground non-linear values. Ships: (1) `ctx_mark_used_app_lt` in Syntax.v — [ctx_mark_used] commutes with context append when the marked position lies within the head. Required by body-transfer's T_Var_Lin_L1 case (the only typing rule that changes G's flags). (2) `closed_below_k_typing_outer_tail_irrelevant_l1_m` in Semantics_L1.v — the body-transfer core. Structural induction on the typing derivation across 28+ rule cases. Statement: forall m R G e T R' G_out, has_type_l1 m R G e T R' G_out -> forall k G_head G_tail, G = G_head ++ G_tail -> length G_head = k -> expr_closed_below k e = true -> exists G_head_out, G_out = G_head_out ++ G_tail /\ length G_head_out = k /\ forall G_tail_new, has_type_l1 m R (G_head ++ G_tail_new) e T R' (G_head_out ++ G_tail_new). "Closed below k terms' typing depends only on G's first k positions; the outer tail is structurally irrelevant." Each typing-rule case threads (k, G_head, G_tail) through its sub-derivations and reconstructs the rule at the alternate tail. Binder rules (T_Let / T_LetLin / T_Lam_* / T_Case_*) apply IH at k+1 with the binder type cons'd onto G_head; Case rules cross-check branch agreement via `app_inv_tail`. (3) `closed_value_typing_G_poly_l1_m` in Semantics_L1.v — the consumer-facing helper. Statement (any-G' form per elegance-first decision: state what's actually true, not what fell out of the proof induction): is_value v -> expr_closed_below 0 v = true -> has_type_l1 m R G v (TFunEff T1 T2 R_in R_out) R G -> has_type_l1 m R G' v (TFunEff T1 T2 R_in R_out) R G'. Proof: invert is_value + has_type_l1 to T_Lam_L1_*_Eff cases; apply body-transfer at k=1, G_head=[(T1,false)], G_tail=G. (4) `closed_value_shift_id_l1_m` in Semantics_L1.v — companion: closed values' [shift 0 d] is identity. Specialises [Syntax.closed_below_shift_id] for the subst lemma's binder cases where [shift 0 1 v] must reduce to [v] for the typing reconstruction to fire. 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 (canonical CS infrastructure; no sibling-region-disjointness, no region-weakening predicates on syntactic shape, no admit-shuffling, no legacy-preservation closure attempt). - ✅ Strictly NEW infrastructure orthogonal to legacy. Build oracle (coqc 8.18.0): clean across all 12 .v files post-edit. Next commit on this branch: `subst_typing_gen_l1_m_tfuneff` Qed (~300 lines mirroring Phase 2 with the closed-value G-poly helper replacing `ground_nonlinear_retype_l1_m` where G-poly retype is needed). Then `preservation_l2_app_eff_beta_tfuneff_l1` + L2 wrapper in TypingL2.v. Refs: - ephapax issue #249 (Stage 1b tracking, this commit partial) - ephapax PR #252 (Stage 1a prerequisite — tfuneff_lambda_free + Counterexample_L2_nested) - ephapax issue #239 (parent Stage 1) - formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3b Stage 1b Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

… axioms) Ships the substitution-lemma half of Stage 1b. Closed TFunEff values can now be substituted at depth k into leaf-only outer expressions with full L1-typing preservation. Lemma signature: forall m R Gin e T R' Gout, has_type_l1 m R Gin e T R' Gout -> forall k Ta Tb R_in_v R_out_v v u_in, nth_error Gin k = Some (TFunEff Ta Tb R_in_v R_out_v, u_in) -> is_value v -> tfuneff_lambda_free e = true -> (P1) (forall r, In r (regions_introduced_by e) -> In r R_in_v) -> (P2) expr_closed_below 0 v = true -> (P3) has_type_l1 m R (remove_at k Gin) v (TFunEff Ta Tb R_in_v R_out_v) R (remove_at k Gin) -> forall u_out, nth_error Gout k = Some (TFunEff Ta Tb R_in_v R_out_v, u_out) -> has_type_l1 m R (remove_at k Gin) (subst k v e) T R' (remove_at k Gout). Mirrors Phase 2's [subst_typing_gen_l1_m_ground_nonlinear] structurally with two swaps: - Phase 2's [ground_nonlinear_retype_l1_m] (R, G-poly retype for ground non-linear values, no side conditions) is replaced by [closed_value_typing_RG_poly_l1_m] (closed TFunEff value RG-poly retype, requires R' ⊆ R_in side condition). The side condition is discharged at each compound-rule call site via [sub_R_in_R_in_via_value_l1_m]: chain (sub-derivation R' ⊆ outer R via count_occ_le_l1_m) + (outer R ⊆ R_in_v via the substituent's T_Lam_L1_*_Eff formation side condition, extracted by value_TFunEff_R_subset_R_in_l1_m). - Phase 2's [ground_nonlinear_value_shift_id_l1] is replaced by [closed_value_shift_id_l1_m] for binder-traversal shift-identity. Inner T_Lam_L1_* / T_Lam_L1_*_Eff cases discharge via [discriminate] on P1 (tfuneff_lambda_free (ELam _ _) = false). Two new supporting lemmas in Semantics_L1.v: - [closed_value_typing_RG_poly_l1_m] — combined RG-poly retype chaining [closed_value_typing_G_poly_l1_m] with [tfuneff_lambda_retype_l1_m] (PR #224). - [value_TFunEff_R_subset_R_in_l1_m] — extracts the lambda-formation side condition R ⊆ R_in from any TFunEff value typing. Trivial inversion proof. - [sub_R_in_R_in_via_value_l1_m] — packages the R-subset chain used at every compound-rule call site in subst_typing_gen_l1_m_tfuneff. Print Assumptions verdict on all four new lemmas: - subst_typing_gen_l1_m_tfuneff: Closed under the global context - closed_value_typing_G_poly_l1_m: Closed under the global context - closed_value_typing_RG_poly_l1_m: Closed under the global context - closed_below_k_typing_outer_tail_irrelevant_l1_m: Closed under the global context Zero new axioms. Zero new admits. Stage 1b's L1-level deliverable is complete; the L2 β-wrapper [preservation_l2_app_eff_beta_tfuneff_l1] + L2-judgment surface lemma ship next on this branch. 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 across all four stages of the 4-stage Phase 3b plan (#235 → #239 / #240 / #241 / #242). - ✅ Strictly NEW infrastructure orthogonal to legacy. Build oracle (coqc 8.18.0): clean across all 12 .v files. Refs: - ephapax issue #249 (Stage 1b tracking; this commit is the L1 half). - ephapax PR #252 (Stage 1a prerequisite — tfuneff_lambda_free + Counterexample_L2_nested + design doc). - ephapax issue #239 (parent Stage 1). - formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3b Stage 1b. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…ff substituents 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>

hyperpolymath enabled auto-merge (squash) May 30, 2026 17:16

hyperpolymath mentioned this pull request May 30, 2026

Phase 3b Stage 1: leaf-only substitution lemma + 2-condition preservation_l2 + Counterexample_L2_nested #239

Closed

hyperpolymath merged commit 7c4c3f5 into main May 30, 2026
0 of 16 checks passed

hyperpolymath deleted the proof-debt/phase-3b-stage-1-tfuneff-leaf branch May 30, 2026 17:42

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(L1): Phase D slice 4 Phase 3b Stage 1a — tfuneff_lambda_free + Counterexample_L2_nested#252

feat(L1): Phase D slice 4 Phase 3b Stage 1a — tfuneff_lambda_free + Counterexample_L2_nested#252
hyperpolymath merged 1 commit into
mainfrom
proof-debt/phase-3b-stage-1-tfuneff-leaf

hyperpolymath commented May 30, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

hyperpolymath commented May 30, 2026

Summary

What lands

Configuration (nested-lambda counterexample)

Owner-directive compliance (CLAUDE.md 2026-05-27)

Test plan

Refs

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant