Skip to content

Commit 84a7bdc

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
proof(L1): experiment 3 — step_pop_disjoint_from_type_l1 is provably FALSE as stated (#342)
## The finding Experiment 3 of the choreographic series (the wiring-lemma attempt named by #332) went **adversarial-first**: before proving `typing ⇒ valid trace`, try to refute the target. The refutation landed. **`formal/Counterexample_StepPop.v` (Qed, zero axioms):** ``` e = EPair (ERegion rv (EI32 5)) (EVar 0) R = [rv] G = [(TString rv, false)] ``` - **Types** (both modalities): the active-region rule pops the ambient `rv`; `T_Var_Lin_L1` then types `EVar 0 : TString rv` at the **empty** region env — it has no `In rv R` premise. - **Steps**: `S_Region_Exit` under `S_Pair_Step1`, so `R' = []`. - `rv ∈ free_regions(T)`, `rv ∈ R`, but `In rv R'` is **False**. So the Admitted `step_pop_disjoint_from_type_l1` was hiding a **falsehood**, not an unfinished proof — the same class as `region_liveness_at_split_l1` (removed 2026-06-26). No proof effort can close it as stated. ## Why this matters for the choreographic route `typed_but_incoherent` (Qed) ties it to experiment 2: the witness is exactly the congruence dichotomy's "impossible third situation" — its trace `[Close; Use]` from balance 1 is incoherent — **yet it types**. Typing does not imply trace coherence, so `wiring_obligation` is unprovable for any faithful trace extraction. The coherence the model needs is a **missing premise of the judgment** — the standing rule's "architecture is asking for a new invariant" signal, now with a machine-checked forcing argument. The choreographic route's task is provably "make coherence a judgment-level input", not "derive it". ## Owner decision needed (reformulation direction) 1. **Liveness/coherence premise** on `step_pop` (foundational-choreographic: coherence becomes a typing input), or 2. **Value-anchored restriction**: the lemma's sole caller (`S_StringConcat_Step2`) retypes an `ELoc` **value** whose `T_Loc_L1` typing already carried `In r R`; the refuting sibling is a **variable**, which no `S_*_Step2` case ever retypes at `R'` — the restricted form may be provable outright. ## Fences `Semantics_L1.v` untouched. This PR only **adds** a regression witness (house pattern: `Counterexample.v` / `Counterexample_RegionShrink.v`) + updates `PROOF-NEEDS.md §5.2`. Verified: fresh `coqc` 8.18.0 build of `formal/` including the new file, green; both theorems `Print Assumptions`-clean. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
1 parent b2ee89e commit 84a7bdc

3 files changed

Lines changed: 177 additions & 1 deletion

File tree

‎PROOF-NEEDS.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -385,7 +385,7 @@ future drift is flagged. (A′ shifts the line numbers but not the count.)
385385
|---|---|---|---|---|---|
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` |
388-
| 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. | **the eliminator fork** | **Open research** — the tropically-graded choreography over time segments. `L1-ELIMINATOR-FORK.md` §3–§8 |
388+
| 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 |
389389
| 4 | `preservation_l1` (capstone) | `Semantics_L1.v:3367` | `:3379` | **gated** on 1–3 | follows once 1–3 land |
390390

391391
`preservation_l3` (`Semantics_L1.v`, **Qed**) is real and depends on **only**

‎formal/Counterexample_StepPop.v‎

Lines changed: 175 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,175 @@
1+
(* SPDX-License-Identifier: MPL-2.0 *)
2+
(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *)
3+
4+
(** * Counterexample — [step_pop_disjoint_from_type_l1] is FALSE as stated.
5+
6+
(Experiment 3 of the choreographic series; regression witness in the
7+
tradition of [Counterexample.v] / [Counterexample_RegionShrink.v].)
8+
9+
The Admitted lemma [step_pop_disjoint_from_type_l1]
10+
([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+
In r (free_regions T) -> In r R -> In r R'.
15+
16+
This file exhibits a configuration that satisfies every premise and
17+
falsifies the conclusion, [Qed], zero axioms. The Admitted marker was
18+
therefore hiding a FALSEHOOD, not an unfinished proof — the same
19+
class as the removed [region_liveness_at_split_l1] (2026-06-26).
20+
No proof effort can close the lemma as stated; the honest move is
21+
reformulation (see "What this forces", below).
22+
23+
** The witness
24+
25+
e = EPair (ERegion rv (EI32 5)) (EVar 0)
26+
R = [rv] G = [(TString rv, false)]
27+
T = TProd (TBase TI32) (TString rv)
28+
29+
Typing ([wit_types]): the active-region rule types e1 and pops the
30+
ambient [rv] ([remove_first_L1 rv [rv] = []]); [T_Var_Lin_L1] then
31+
types [EVar 0 : TString rv] at the EMPTY region env — it has no
32+
[In rv R] premise. The pair's type carries [rv] via its second
33+
component, so [In rv (free_regions T)] holds.
34+
35+
Stepping ([wit_steps]): [EI32 5] is a value, so [S_Region_Exit]
36+
fires under the [S_Pair_Step1] congruence, giving [R' = []].
37+
Conclusion demanded: [In rv []] — False.
38+
39+
** Relation to the choreographic trace model (experiment 2)
40+
41+
[L1ChoreoExperiment2.v]'s congruence dichotomy proves the "third
42+
situation" — the stepping sibling net-closes the outer [rv] while the
43+
surviving sibling still USES it — is never trace-COHERENT
44+
([sibling_use_keeps_region_live]). The witness is EXACTLY that third
45+
situation, and it TYPES. Hence ([typed_but_incoherent], below):
46+
47+
has_type_l1 does NOT imply trace coherence.
48+
49+
So experiment 2's wiring lemma ([wiring_obligation]) is unprovable
50+
for any trace extraction faithful enough to record the sibling's
51+
rv-dependence as a [Use]: the coherence the model needs is not a
52+
CONSEQUENCE of the current judgment — it is a MISSING PREMISE of it.
53+
54+
** What this forces (the experiment-3 verdict)
55+
56+
The four-layer architecture's standing rule says: when a closure
57+
needs a side condition the judgment cannot supply, the architecture
58+
is asking for a NEW INVARIANT, not a cleverer lemma. This witness is
59+
that signal, now [Qed]-forced:
60+
61+
- [step_pop_disjoint_from_type_l1] must be REFORMULATED with a
62+
liveness/coherence premise (or restricted to consumers that
63+
anchor the region operationally — its only caller,
64+
S_StringConcat_Step2, retypes an [ELoc _ r] VALUE whose
65+
[T_Loc_L1] typing already carried [In r R]; note the witness's
66+
dangling sibling is a VARIABLE, which no [S_*_Step2] case ever
67+
needs to retype at R', suggesting the value-anchored restriction
68+
may be provable);
69+
- the choreographic route's job description changes from "derive
70+
coherence from typing" (impossible — this file) to "make
71+
coherence a judgment-level input" — the foundational thesis,
72+
now with a machine-checked forcing argument.
73+
74+
Owner escalation, not patching: this file only ADDS a regression
75+
witness. [Semantics_L1.v] is untouched; its Admitted markers stand
76+
until the owner ratifies a reformulation. *)
77+
78+
Require Import Coq.Lists.List.
79+
Import ListNotations.
80+
Require Import Coq.Strings.String.
81+
Open Scope string_scope.
82+
83+
From Ephapax Require Import Syntax.
84+
From Ephapax Require Import Modality.
85+
From Ephapax Require Import Typing.
86+
From Ephapax Require Import TypingL1.
87+
From Ephapax Require Import Semantics.
88+
From Ephapax Require Import Semantics_L1.
89+
From Ephapax Require Import L1ChoreoExperiment2.
90+
91+
Definition rv : region_name := "rv".
92+
Definition wit_e1 : expr := ERegion rv (EI32 5).
93+
Definition wit_e2 : expr := EVar 0.
94+
Definition wit : expr := EPair wit_e1 wit_e2.
95+
Definition wit_G : ctx := [(TString rv, false)].
96+
Definition wit_T : ty := TProd (TBase TI32) (TString rv).
97+
98+
(** The witness types under [has_type_l1] — in BOTH modalities — with
99+
[R = [rv]], landing at the empty region env. *)
100+
Lemma wit_types : forall m,
101+
has_type_l1 m [rv] wit_G wit wit_T [] (ctx_mark_used wit_G 0).
102+
Proof.
103+
intro m.
104+
unfold wit, wit_e1, wit_e2, wit_T.
105+
eapply T_Pair_L1 with (R1 := remove_first_L1 rv [rv]).
106+
- (* e1 = ERegion rv (EI32 5) : TBase TI32 — active-region rule,
107+
consumes the ambient rv. *)
108+
eapply T_Region_Active_L1.
109+
+ simpl; auto.
110+
+ simpl. intro Hin. exact Hin.
111+
+ simpl; auto.
112+
+ apply T_I32_L1.
113+
- (* e2 = EVar 0 : TString rv — at the ALREADY-EMPTY region env.
114+
T_Var_Lin_L1 has no In rv R premise; this is the door. *)
115+
simpl.
116+
eapply T_Var_Lin_L1.
117+
+ reflexivity.
118+
+ reflexivity.
119+
Qed.
120+
121+
(** The witness steps: the inner region exits under the pair congruence,
122+
popping the only [rv]. *)
123+
Lemma wit_steps : forall mu,
124+
step (mu, [rv], wit) (mem_free_region mu rv, [], EPair (EI32 5) wit_e2).
125+
Proof.
126+
intro mu.
127+
unfold wit, wit_e1.
128+
replace ([] : region_env) with (remove_first rv [rv]).
129+
2: { simpl. destruct (string_dec rv rv); [reflexivity | congruence]. }
130+
apply S_Pair_Step1.
131+
apply S_Region_Exit.
132+
- constructor.
133+
- simpl. left. reflexivity.
134+
- simpl. exact I.
135+
Qed.
136+
137+
(** [rv] is free in the result type (via the surviving sibling). *)
138+
Lemma wit_free : In rv (Typing.free_regions wit_T).
139+
Proof. simpl. auto. Qed.
140+
141+
(** ** THE REFUTATION *)
142+
Theorem step_pop_disjoint_from_type_l1_FALSE :
143+
~ (forall mu R e mu' R' e' m G T R_final G',
144+
step (mu, R, e) (mu', R', e') ->
145+
has_type_l1 m R G e T R_final G' ->
146+
forall r, In r (Typing.free_regions T) -> In r R -> In r R').
147+
Proof.
148+
intro H.
149+
assert (Hin : In rv ([] : region_env)).
150+
{ eapply (H [] [rv] wit (mem_free_region [] rv) [] (EPair (EI32 5) wit_e2)
151+
Linear wit_G wit_T [] (ctx_mark_used wit_G 0)).
152+
- apply wit_steps.
153+
- apply wit_types.
154+
- apply wit_free.
155+
- simpl; auto. }
156+
simpl in Hin. exact Hin.
157+
Qed.
158+
159+
(** ** Tie-in to experiment 2's trace model
160+
161+
The witness's faithful single-region trace is [Close; Use] from
162+
initial balance [cnt rv [rv] = 1]: e1's evaluation closes the
163+
ambient [rv]; the surviving sibling's rv-dependence is the [Use],
164+
ordered after it. That trace is INCOHERENT — so the configuration
165+
the type system just accepted is exactly one the trace model
166+
(correctly) rejects. Typing does not imply coherence; coherence is
167+
the missing invariant. *)
168+
Example typed_but_incoherent :
169+
~ valid 1 (Close :: Use :: []).
170+
Proof.
171+
simpl. intros [_ [Huse _]]. inversion Huse.
172+
Qed.
173+
174+
Print Assumptions step_pop_disjoint_from_type_l1_FALSE.
175+
Print Assumptions typed_but_incoherent.

‎formal/_CoqProject‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ L1ChoreoExperiment.v
1515
L1ChoreoExperiment2.v
1616
Counterexample.v
1717
Counterexample_RegionShrink.v
18+
Counterexample_StepPop.v
1819
Echo.v
1920
Modality.v
2021
TypingL2.v

0 commit comments

Comments
 (0)