Skip to content

Commit 22e278e

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
proof(L1): experiment 3b — preservation_l1 is provably FALSE as stated [owner ratification] (#344)
> **⚠️ Deliberately NOT armed for auto-merge.** This PR recasts the status of the L1 capstone theorem; per the estate PR rule's ratification exception, it waits for your call. ## The finding Completion of experiment 3 (#342). The value-anchored escape hatch the step_pop counterexample left open is **closed**, and the capstone falls. **`formal/Counterexample_PreservationL1.v` (Qed, zero axioms):** ``` e = EStringConcat (ELoc 0 rv) (ESnd (EPair (ERegion rv (EI32 0)) (EVar 0))) R = [rv] G = [(TString rv, false)] T = TString rv ``` - **Types** in both modalities (`wit2_types`). - **Steps**: `S_StringConcat_Step2 → S_Snd_Step → S_Pair_Step1 → S_Region_Exit` — the sibling's region-exit pops the **only** `rv`, so `R' = []`. - **Post-state untypable** at the same indices: the surviving operand is an `ELoc` **value** whose only rule `T_Loc_L1` demands `In rv []` (`wit2_post_untypable`). - Hence `preservation_l1_FALSE`. ## What it means With #342, **both remaining L1 `Admitted.` markers were hiding falsehoods**, not unfinished proofs. The judgment lets one operand's evaluation consume an ambient region that a sibling's value-typing depends on — region-liveness-through-reduction, the single invariant behind all four historical admit faces (June audit), now Qed-fatal to the capstone as stated. The L1 redesign correctly rejects the *legacy* counterexample (`bad_input_untypable_l1` still holds) — this witness enters through a different door in the same semantic class. **Preservation for L1 is not reachable by more lemmas.** The judgment must carry the temporal invariant. Two directions, your call: 1. **Choreographic-foundational** (your committed route, now Qed-mandatory rather than preferred): coherence/liveness as a judgment-level input, per `L1ChoreoExperiment2.v`'s trace model + `L1-ELIMINATOR-FORK.md` §3–§7. 2. **Leaf-rule strengthening** (A′ / path-3 family): make typing reject the witness at the leaves. The earlier failure analyses of this family predate this witness and should be re-examined against it. Recommendation: (1), with the decision recorded in `PRESERVATION-DESIGN.md` and the two `Admitted` markers then replaced by reformulated statements in a ratified follow-up. ## Fences `Semantics_L1.v` untouched — this only **adds** a regression witness (house pattern: `Counterexample.v` did exactly this for the legacy preservation) + updates `PROOF-NEEDS.md §5.2`. Verified: fresh `coqc` 8.18.0 build of all of `formal/` including the new file; `Print Assumptions` clean. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
1 parent 92cd278 commit 22e278e

3 files changed

Lines changed: 167 additions & 1 deletion

File tree

‎PROOF-NEEDS.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -386,7 +386,7 @@ future drift is flagged. (A′ shifts the line numbers but not the count.)
386386
| 1 | `region_shrink_preserves_typing_l1_gen_m` | `Semantics_L1.v:441` | `:572`, `:642` | **live structural** (list-vs-multiset tear) | **Dissolves** — carrier refactor `region_env : list` → count-map. `L1-REGION-REFOUNDATION-PLAN.md` |
387387
| 2 | `region_liveness_at_split_l1_gen` | `Semantics_L1.v:1904` | `:1956`, `:1976` | **provably FALSE** as written (witness `ERegion rv (EI32 5)` at `R=[rv]`) | **Repaired** — restate as graded `live R rv ∧ no-exit-of-rv ⇒ live R' rv`; prove from `count_occ_le_l1_m` monotonicity + ~13-site call audit. `L1-REGION-REFOUNDATION-PLAN.md §5` |
388388
| 3 | `step_pop_disjoint_from_type_l1` | `Semantics_L1.v` | **1** (reduced from ~9–11 in 2026 via the `step_R_change_shape` rewrite — see `L1-ELIMINATOR-FORK.md` §8). The single residual obligation is `step exits r0 ∧ r0 ∈ free_regions(T) ⟹ cnt r0 R ≥ 2`; its direct-exit sub-case is vacuous, the residue is congruence-exit count-coherence. Diagnosis corrected: **not** §4.8 lambda-rigidity (the witness has no lambda) but region-count coherence at a region exit. **⚠️ 2026-07-07 (experiment 3): provably FALSE AS STATED** — `formal/Counterexample_StepPop.v` (Qed, zero axioms) exhibits `EPair (ERegion rv (EI32 5)) (EVar 0)` at `R=[rv]`: it types (`T_Var_Lin_L1` has no `In rv R` premise), steps (`S_Region_Exit` under `S_Pair_Step1`), and lands at `R'=[]` with `rv ∈ free_regions(T)`. Same class as admit #2's history: the `Admitted.` hides a falsehood, not a gap. | **the eliminator fork** — now with a Qed forcing argument that typing ⇏ trace coherence | **Reformulation, owner-gated** — restate with a liveness/coherence premise or restrict to value-anchored consumers (the sole caller retypes an `ELoc` value whose `T_Loc_L1` typing carried `In r R`; the refuting sibling is a variable, which no `S_*_Step2` case retypes at `R'`). The choreographic route's task is now provably "make coherence a judgment-level input", not "derive it". `Counterexample_StepPop.v` header + `L1-ELIMINATOR-FORK.md` §3–§8 |
389-
| 4 | `preservation_l1` (capstone) | `Semantics_L1.v:3367` | `:3379` | **gated** on 1–3 | follows once 1–3 land |
389+
| 4 | `preservation_l1` (capstone) | `Semantics_L1.v:3367` | `:3379` | **⚠️ provably FALSE AS STATED (2026-07-07, experiment 3b)** — `formal/Counterexample_PreservationL1.v` (Qed, zero axioms): `EStringConcat (ELoc 0 rv) (ESnd (EPair (ERegion rv (EI32 0)) (EVar 0)))` at `R=[rv]` types in both modalities, steps (the sibling's region-exit pops the only `rv`), and the post-state is untypable — the `ELoc` anchor's `T_Loc_L1` demands `In rv []`. The value-anchored escape hatch suggested by `Counterexample_StepPop.v` is closed: the dangling dependence here IS a value. | **NOT closable by lemmas** — the judgment must carry the temporal invariant (region-liveness-through-reduction): either coherence as a judgment input (choreographic-foundational route, now Qed-mandatory) or leaf-rule strengthening that rejects the witness at typing (A′/path-3 family, to be re-examined against this witness). Owner decision; record in `PRESERVATION-DESIGN.md`. |
390390

391391
`preservation_l3` (`Semantics_L1.v`, **Qed**) is real and depends on **only**
392392
admit #1 (`region_shrink`); it flips **unconditional** the moment #1 closes.

‎formal/Counterexample_PreservationL1.v‎

Lines changed: 165 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,165 @@
1+
(* SPDX-License-Identifier: MPL-2.0 *)
2+
(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *)
3+
4+
(** * Counterexample — [preservation_l1] is FALSE as stated.
5+
6+
(Experiment 3b of the choreographic series — the completion of
7+
[Counterexample_StepPop.v]. Regression witness in the tradition of
8+
[Counterexample.v], which did the same for the LEGACY preservation.)
9+
10+
The Admitted capstone [preservation_l1] ([Semantics_L1.v]) claims:
11+
12+
step (mu,R,e) (mu',R',e') ->
13+
has_type_l1 m R G e T R_final G' ->
14+
has_type_l1 m R' G e' T R_final G'.
15+
16+
This file exhibits a configuration that types (in BOTH modalities),
17+
steps, and whose post-state is UNTYPABLE at the same indices — [Qed],
18+
zero axioms. Together with [Counterexample_StepPop.v]: BOTH remaining
19+
L1 Admitted markers were hiding falsehoods, not unfinished proofs.
20+
21+
** The witness (value-anchored — closes the StepPop file's open door)
22+
23+
e = EStringConcat (ELoc 0 rv)
24+
(ESnd (EPair (ERegion rv (EI32 0)) (EVar 0)))
25+
R = [rv] G = [(TString rv, false)] T = TString rv
26+
27+
- The LEFT operand is an [ELoc] VALUE. Its one typing rule
28+
[T_Loc_L1] demands [In rv R] — satisfied pre-step ([R = [rv]]).
29+
- The RIGHT operand evaluates [ERegion rv (EI32 0)] under
30+
[ESnd (EPair _ (EVar 0))]; the pair's second component supplies
31+
the [TString rv] the concat needs, typed by [T_Var_Lin_L1] at the
32+
already-popped env (no [In rv R] premise).
33+
- Stepping: [S_StringConcat_Step2] -> [S_Snd_Step] -> [S_Pair_Step1]
34+
-> [S_Region_Exit] pops the ONLY [rv]: [R' = []].
35+
- Post-state: the anchor [ELoc 0 rv] must retype at [R' = []], and
36+
[T_Loc_L1] demands [In rv []] — no derivation exists
37+
([wit2_post_untypable], by double inversion).
38+
39+
[Counterexample_StepPop.v] suggested a value-anchored RESTRICTION of
40+
step_pop "may be provable" because its refuting sibling was a
41+
variable. This witness closes that door: the dangling dependence
42+
here IS a value ([ELoc]), living one congruence away from the popped
43+
region. The hole is not variable-typing alone; it is that the
44+
snapshot judgment lets ONE operand's evaluation consume an ambient
45+
region a SIBLING's value-typing depends on — region-liveness-
46+
through-reduction, the one invariant behind all four historical L1
47+
admit faces (per the 2026-06 audit), now [Qed]-fatal to the capstone
48+
as stated.
49+
50+
** What this forces (experiment 3 verdict, completed)
51+
52+
The L1 redesign closed the LEGACY counterexample ([Counterexample.v]
53+
still proves [bad_input_untypable_l1]: that configuration is
54+
REJECTED at typing). This file shows the post-L2-hybrid judgment
55+
still admits a configuration in the same semantic class through a
56+
different door. Preservation for L1 is NOT provable by more lemmas;
57+
it requires the judgment to carry the missing temporal invariant:
58+
59+
- either typing-level: region-liveness / trace-coherence as a
60+
judgment input (the choreographic-foundational route — now
61+
provably MANDATORY, not merely preferred), per
62+
[L1ChoreoExperiment2.v]'s model + [L1-ELIMINATOR-FORK.md] §3-§7;
63+
- or rule-level: strengthen the leaves ([T_Var_*_L1], and the
64+
interplay of [T_Loc_L1] with sibling threading) so the witness
65+
is rejected at typing, and re-derive — the A'/path-3 family,
66+
whose earlier failure analyses should be revisited IN LIGHT OF
67+
this witness (the failure probes predate it).
68+
69+
Direction choice is the owner's (PRESERVATION-DESIGN.md is the
70+
canonical place for the decision record). Fences respected: this
71+
file only ADDS a witness; [Semantics_L1.v] is untouched and its
72+
Admitted markers stand until the reformulation is ratified. *)
73+
74+
Require Import Coq.Lists.List.
75+
Import ListNotations.
76+
Require Import Coq.Strings.String.
77+
Open Scope string_scope.
78+
79+
From Ephapax Require Import Syntax.
80+
From Ephapax Require Import Modality.
81+
From Ephapax Require Import Typing.
82+
From Ephapax Require Import TypingL1.
83+
From Ephapax Require Import Semantics.
84+
From Ephapax Require Import Semantics_L1.
85+
86+
Definition rv : region_name := "rv".
87+
Definition anchor : expr := ELoc 0 rv.
88+
Definition popper : expr := ESnd (EPair (ERegion rv (EI32 0)) (EVar 0)).
89+
Definition wit2 : expr := EStringConcat anchor popper.
90+
Definition wit2_G : ctx := [(TString rv, false)].
91+
92+
(** Pre-state types — in BOTH modalities: both operands [TString rv],
93+
region env threading [rv] -> []. *)
94+
Lemma wit2_types : forall m,
95+
has_type_l1 m [rv] wit2_G wit2 (TString rv) [] (ctx_mark_used wit2_G 0).
96+
Proof.
97+
intro m.
98+
unfold wit2, anchor, popper.
99+
eapply T_StringConcat_L1 with (R1 := [rv]).
100+
- apply T_Loc_L1. simpl; auto.
101+
- eapply T_Snd_L1 with (T1 := TBase TI32).
102+
+ eapply T_Pair_L1 with (R1 := remove_first_L1 rv [rv]).
103+
* eapply T_Region_Active_L1.
104+
-- simpl; auto.
105+
-- simpl. intro Hin. exact Hin.
106+
-- simpl; auto.
107+
-- apply T_I32_L1.
108+
* simpl. eapply T_Var_Lin_L1; reflexivity.
109+
+ reflexivity.
110+
Qed.
111+
112+
(** The step: concat's Step2 congruence -> snd congruence -> pair
113+
congruence -> region exit. [R] goes [[rv]] -> [[]]. *)
114+
Lemma wit2_steps : forall mu,
115+
step (mu, [rv], wit2)
116+
(mem_free_region mu rv, [],
117+
EStringConcat anchor (ESnd (EPair (EI32 0) (EVar 0)))).
118+
Proof.
119+
intro mu.
120+
unfold wit2, anchor, popper.
121+
replace ([] : region_env) with (remove_first rv [rv]).
122+
2: { simpl. destruct (string_dec rv rv); [reflexivity | congruence]. }
123+
apply S_StringConcat_Step2; [constructor|].
124+
apply S_Snd_Step.
125+
apply S_Pair_Step1.
126+
apply S_Region_Exit.
127+
- constructor.
128+
- simpl. left. reflexivity.
129+
- simpl. exact I.
130+
Qed.
131+
132+
(** Post-state is UNTYPABLE at the same indices: the anchor [ELoc]'s
133+
only rule demands [In rv []]. *)
134+
Lemma wit2_post_untypable :
135+
~ has_type_l1 Linear [] wit2_G
136+
(EStringConcat anchor (ESnd (EPair (EI32 0) (EVar 0))))
137+
(TString rv) [] (ctx_mark_used wit2_G 0).
138+
Proof.
139+
intro H.
140+
inversion H; subst.
141+
match goal with
142+
| Ha : has_type_l1 _ [] _ anchor _ _ _ |- _ =>
143+
inversion Ha; subst
144+
end.
145+
match goal with
146+
| Hin : In rv [] |- _ => exact Hin
147+
end.
148+
Qed.
149+
150+
(** ** THE REFUTATION *)
151+
Theorem preservation_l1_FALSE :
152+
~ (forall m mu R e mu' R' e',
153+
step (mu, R, e) (mu', R', e') ->
154+
forall G T R_final G',
155+
has_type_l1 m R G e T R_final G' ->
156+
has_type_l1 m R' G e' T R_final G').
157+
Proof.
158+
intro H.
159+
apply wit2_post_untypable.
160+
eapply (H Linear [] [rv] wit2).
161+
- apply wit2_steps.
162+
- apply wit2_types.
163+
Qed.
164+
165+
Print Assumptions preservation_l1_FALSE.

‎formal/_CoqProject‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ L1ChoreoExperiment2.v
1616
Counterexample.v
1717
Counterexample_RegionShrink.v
1818
Counterexample_StepPop.v
19+
Counterexample_PreservationL1.v
1920
Echo.v
2021
Modality.v
2122
TypingL2.v

0 commit comments

Comments
 (0)