feat(L1+L2): Phase D slice 4 Phase 3b Stage 1b — closed-value substitution + preservation_l2 β closure (closes #249) by hyperpolymath · Pull Request #253 · hyperpolymath/ephapax

hyperpolymath · 2026-05-30T19:17:18Z

Summary

Ships Stage 1b of the four-stage Phase 3b resolution plan (parent #235 / Stage 1 #239 / Stages 2-4 #240-#242), closing the L1 substitution + L2 preservation β-case for closed TFunEff substituents in leaf-only outer bodies.

Builds on Stage 1a (PR #252, auto-merge armed) which shipped the syntactic infrastructure (tfuneff_lambda_free) + the soundness-gap witness (Counterexample_L2_nested.v).

Closes ephapax issue #249. With this PR, Stage 1 (#239) is fully delivered.

What ships

Syntax.v (canonical closure machinery)

expr_closed_below : nat -> expr -> bool — Fixpoint, bool per post-redesign convention. Standard CS "no free de Bruijn variables ≥ k" predicate.
closed_below_shift_id — closed-below-c terms are shift-invariant at cutoff c.
expr_closed_below_shift_mono — closure survives shifting.
ctx_mark_used_app_lt — ctx_mark_used commutes with context append when marked position lies within the head.

Semantics_L1.v (body-transfer + RG-poly retype)

closed_below_k_typing_outer_tail_irrelevant_l1_m — the body-transfer core. Structural induction across 28+ typing rules; ~200 lines. Establishes that closed-below-k terms' typing depends only on G's first k positions; the tail is structurally irrelevant.
closed_value_typing_G_poly_l1_m — closed TFunEff values type at any G' (any-G' form per elegance-first "state what's actually true", not "G of matching length").
closed_value_typing_RG_poly_l1_m — combined RG-poly retype chaining the G-poly helper with tfuneff_lambda_retype_l1_m (PR feat(L1): Phase D slice 4 Phase 3a — tfuneff_lambda_retype_l1_m + is_tfuneff_ty #224) for the R-component under R' ⊆ R_in side condition.
closed_value_shift_id_l1_m — cutoff-0 wrapper of closed_below_shift_id.
value_TFunEff_R_subset_R_in_l1_m — extracts R ⊆ R_in from a TFunEff value's 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 Qed (~300 lines) — mirrors Phase 2's subst_typing_gen_l1_m_ground_nonlinear. Inner T_Lam_L1_*_Eff cases discharge via P1 discriminate; compound rules use the RG-poly retype + R-subset chain to handle the G-mismatch.

TypingL2.v (β-case closure)

preservation_l2_app_eff_beta_tfuneff_l1 — L1-level kernel. Inverts the lambda derivation through T_Lam_L1_Linear_Eff / T_Lam_L1_Affine_Eff; collapses R/G via value_R_G_preserving_l1; defers to the substitution kernel above at k=0.
preservation_l2_app_eff_beta_tfuneff — L2 wrapper. Inverts both has_type_l2 hypotheses through L2_lift_l1 (the T_App_L2_Eff cases discriminate via expression-shape mismatch).

`.machine_readable/6a2/STATE.a2ml`

last_action records the full Stage 1b deliverable surface.
next_action advances to 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).

Two-condition statement (per Stage 1 framing)

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 ->                           (* P1 *)
    (forall r, In r (regions_introduced_by ebody) -> In r R_in_v) ->  (* P2 *)
    expr_closed_below 0 v2 = true ->                              (* P3 *)
    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''.

The mechanised soundness-gap witnesses for the conditional form:

Counterexample_L2.v (PR docs+test: Phase D slice 4 Phase 4c — mechanised soundness-gap counterexample for TFunEff β #234, Phase 4c) — fresh-region gap (counterexample to dropping P2).
Counterexample_L2_nested.v (Stage 1a, PR feat(L1): Phase D slice 4 Phase 3b Stage 1a — tfuneff_lambda_free + Counterexample_L2_nested #252) — nested-lambda gap (counterexample to dropping P1).

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.

Path-(i) elegance-first design choices

Per the priority order (elegance + correctness > everything; workload least), this PR bakes in two explicit refinements over the issue body's draft:

bool predicate target for expr_closed_below — matches post-redesign convention (is_linear_ty, is_ground_nonlinear_ty, tfuneff_lambda_free are all bool). The legacy Prop predicates (expr_free_of_region) are pre-redesign artefacts.
Any-G' statement form for the closed-value helper — states what's actually true ("for closed values, G is genuinely irrelevant"), not what fell out of the proof induction.

Two refinements that touch approved scope were deliberately NOT made:

P1 (tfuneff_lambda_free) precondition retained, not dropped — re-staging is owner territory.
4-stage plan accepted as is — no re-staging proposal folded into Stage 1b.

Print Assumptions verdict

All new Qed lemmas: Closed under the global context.

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
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.

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.

Test plan

just -f formal/Justfile all clean across all 12 .v files
Print Assumptions on every new Qed lemma reports "Closed under the global context"
No Axiom / Admitted introduced
No legacy file touched per owner directive
Stage 1a's contributions (tfuneff_lambda_free, Counterexample_L2_nested.v) still build clean
Phase 2's contributions (ground_nonlinear_retype_l1_m, subst_typing_gen_l1_m_ground_nonlinear) still build clean
Phase 4a + 4b L2 β-wrappers still build clean
coq-build.yml CI workflow runs against this PR (gated on PR ci: add Coq build oracle workflow (closes #227) #231 / ci(coq-build): run coqorg/coq container as root to fix actions/checkout EACCES #236 fixes)

🤖 Generated with Claude Code

… 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 19:17

This was referenced May 30, 2026

Phase 3b Stage 1b: subst_typing_gen_l1_m_tfuneff + preservation_l2 β wrapper (deferred from #239) #249

Closed

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

Closed

hyperpolymath and others added 4 commits May 30, 2026 20:17

hyperpolymath force-pushed the proof-debt/phase-3b-stage-1b-tfuneff-subst branch from 2267bcf to 3413a72 Compare May 30, 2026 19:19

hyperpolymath merged commit 6ce16d1 into main May 31, 2026
0 of 16 checks passed

hyperpolymath deleted the proof-debt/phase-3b-stage-1b-tfuneff-subst branch May 31, 2026 06:28

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(L1+L2): Phase D slice 4 Phase 3b Stage 1b — closed-value substitution + preservation_l2 β closure (closes #249)#253

feat(L1+L2): Phase D slice 4 Phase 3b Stage 1b — closed-value substitution + preservation_l2 β closure (closes #249)#253
hyperpolymath merged 4 commits into
mainfrom
proof-debt/phase-3b-stage-1b-tfuneff-subst

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 ships

Syntax.v (canonical closure machinery)

Semantics_L1.v (body-transfer + RG-poly retype)

TypingL2.v (β-case closure)

.machine_readable/6a2/STATE.a2ml

Two-condition statement (per Stage 1 framing)

Path-(i) elegance-first design choices

Print Assumptions verdict

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

Test plan

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

`.machine_readable/6a2/STATE.a2ml`