Skip to content

Commit f257c7a

Browse files
claudehyperpolymath
claude
authored and
hyperpolymath
committed
docs: reframe status surfaces — "gestating, not dead" (v1 → v2)
The status surfaces (README warning, STATUS.adoc, CLAUDE.md, the v2 grammar spec) opened with "provably false / archaeology / do not extend / ❌ NOT doing". Every word was true, but the cumulative effect was that humans *and* bots concluded the project was dead and bailed — including skipping the live, tractable v2 work. This reframes without losing one honest fact. The legacy preservation theorem is still stated as provably false (it is; the Counterexample.v Qed lemmas stand) and the flat v1 grammar is still superseded — but those are now framed as the *receipts of a language learning from its first draft*, not an obituary. Ephapax is gestating: two parallel v1 → v2 transitions (grammar; soundness proof), both landing. - NEW `V1-TO-V2.adoc` — canonical narrative both humans and bots point to. Tells the grammar and proof v1 → v2 stories under one frame; has a human lead and a machine-readable orientation block; lists the live work; restates the two genuinely-settled facts in full (transparency). - `README.adoc` — WARNING → NOTE, leads with gestation, keeps every layer-status fact, points to V1-TO-V2.adoc. - `STATUS.adoc` — orientation + "Past" + "fences" reframed; structure unchanged. "Past — archaeology (do not extend)" → "Past — the v1 lesson (read it, don't build on it)". - `CLAUDE.md` — bot-facing: adds a "where the tractable work is" orientation before the prohibitions so agents engage instead of bailing; guardrails kept verbatim in intent, framed as two narrow fences. - `spec/ephapax-v2-grammar.ebnf` — stale "DRAFT — not yet implemented" → "ACTIVE — landing in phases" (the v2_grammar_phase_* tests pass). - `STATE.a2ml` — adds a FRAME pointer to the bot-facing directive block. https://claude.ai/code/session_017t53M7W7ubmXpwymveLcCE
1 parent 75aad69 commit f257c7a

6 files changed

Lines changed: 429 additions & 58 deletions

File tree

‎.machine_readable/6a2/STATE.a2ml‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,14 @@ updated: 2026-06-02T13:30:00Z
1515
# NOT closure of the legacy theorem. Pre-discovery patching paths are
1616
# closed.
1717
#
18+
# FRAME (read first): ephapax is GESTATING, not dead — a deliberate second
19+
# draft on two tracks (grammar + proof), both landing. See ../../V1-TO-V2.adoc.
20+
# The DO-NOTs below fence off exactly TWO v1 artefacts (the falsified legacy
21+
# preservation theorem; the superseded flat grammar). Everything in v2 is
22+
# OPEN and tractable: L1 structural admits, unconditional preservation_l3,
23+
# the v2 grammar phases, L4 semantics. Do NOT read these guardrails as
24+
# "nothing to do here" — engage with the v2 work.
25+
#
1826
# DO NOT:
1927
# - close `Theorem preservation` in formal/Semantics.v (provably false)
2028
# - extend Semantics.v with closure-support lemmas (Lemma B variants,

‎CLAUDE.md‎

Lines changed: 40 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -74,24 +74,50 @@ Most questions touch exactly one layer. The design rationale is in `formal/PRESE
7474

7575
---
7676

77-
## 🛑 Owner directive 2026-05-27 — preservation work
78-
79-
> Read this before touching anything in `formal/`. Several Claude sessions
80-
> burned hours walking the pre-discovery patching path. This block
81-
> exists so that doesn't happen again.
77+
## Orientation: this language is gestating — engage with v2
78+
79+
**Read `V1-TO-V2.adoc` first.** Ephapax is *not* dead, broken, or
80+
abandoned — it is part-way through a deliberate second draft on two
81+
tracks (grammar and soundness proof), both landing. Do not read the
82+
prohibitions below as "there is nothing to do here." They fence off
83+
exactly **two** v1 artefacts; everything in v2 is open and wants work.
84+
85+
**Where the tractable work is (engage with this):**
86+
87+
- **Proof, L1** — close the residual L1 structural admits in
88+
`formal/Semantics_L1.v` (list/multiset bridge;
89+
`region_shrink_preserves_typing_l1_gen_m`; `TFun` effect typing).
90+
These are *v2 design follow-ups*, not legacy patching. See
91+
`PROOF-NEEDS.md §4`.
92+
- **Proof, L3** — state + prove the **unconditional** `preservation_l3`
93+
(currently conditional on an L1 admit).
94+
- **Grammar, v2** — continue the phase work in
95+
`spec/ephapax-v2-grammar.ebnf` + the `v2_grammar_phase_*` CLI tests.
96+
- **Proof, L4** — Phase A scaffold landed; mother–child dyadic
97+
semantics (`PRESERVATION-DESIGN.md §7`) is the next design step.
98+
99+
## 🛑 Owner directive 2026-05-27 — the two fences (narrow, load-bearing)
100+
101+
> The guardrails below are narrow by design. They stop one specific
102+
> wasted path (several sessions burned hours trying to close a theorem
103+
> that is *proven* unclosable). They do **not** mean "skip this repo."
104+
> Engage with the v2 work listed above; just keep off the two fenced
105+
> v1 artefacts.
82106
83107
### TL;DR
84108

85109
Ephapax preservation as originally stated in `formal/Semantics.v` is
86-
**provably false**. `formal/Counterexample.v` exhibits a concrete
87-
configuration that types, steps, and lands at an untypable post-state
88-
— all three lemmas `Qed`. The work is therefore **not** to close
89-
`Theorem preservation` in `Semantics.v`. The work is the **four-layer
90-
principled redesign** (L1 region capabilities / L2 modality (now
91-
`m`-indexed into `has_type_l1`) / L3 echo / L4 dyadic mode) documented
92-
in `formal/PRESERVATION-DESIGN.md`. Preservation is **re-derived** in
93-
the new architecture from explicit invariants, not forced through
94-
the old one.
110+
**provably false** — and that is a *result*, not a defeat:
111+
`formal/Counterexample.v` exhibits a concrete configuration that types,
112+
steps, and lands at an untypable post-state (5 lemmas `Qed`), which
113+
named the exact invariant the redesign needed. So the work is **not** to
114+
close `Theorem preservation` in `Semantics.v` (no closure exists; the
115+
`Admitted` is deliberate). The work is the **four-layer principled
116+
redesign** (L1 region capabilities / L2 modality, now `m`-indexed into
117+
`has_type_l1` / L3 echo / L4 dyadic mode) in
118+
`formal/PRESERVATION-DESIGN.md`, where preservation is **re-derived
119+
per layer** from explicit invariants. Three of the four layers already
120+
carry `Qed` theorems — this is a healthy build, not a stalled one.
95121

96122
### DO NOT
97123

‎README.adoc‎

Lines changed: 44 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -41,34 +41,52 @@ lesson):
4141
link:https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambiguation/ephapax-vs-affinescript.md[nextgen-languages/docs/disambiguation/ephapax-vs-affinescript.md].
4242
====
4343

44-
[WARNING]
45-
.🔄 Foundational redesign in progress — read `STATUS.adoc` before opening any `.v` file
44+
[NOTE]
45+
.🌱 Ephapax is gestating — second-draft in progress, and going well (start with `V1-TO-V2.adoc`)
4646
====
47-
On 2026-05-26 a verified Coq counterexample
48-
(link:formal/Counterexample.v[`formal/Counterexample.v`], 5 Qed
49-
lemmas) showed that preservation as stated in the legacy typing
50-
judgment is **provably false**. The repo is in the middle of a
51-
*four-layer principled redesign* (regions / modality / echo / dyadic
52-
mode) where preservation is *re-derived per layer* from explicit
53-
invariants rather than forced through the old judgment.
54-
55-
Anything in this README dated before 2026-05-26 that describes a
56-
"preservation closure plan" or counts "910 → 22 → 12 open goals" is
57-
**archaeology, not instructions**. The authoritative status is in
58-
link:STATUS.adoc[`STATUS.adoc`] (past / present / future map),
47+
This language is **not dead, abandoned, or frozen** — it is mid-way
48+
through a deliberate *second draft*, on two independent tracks, and both
49+
are landing. The full story (and why the older "provably false /
50+
archaeology" wording misled readers into writing the project off) is in
51+
link:V1-TO-V2.adoc[`V1-TO-V2.adoc`]. Read that first; this box is the
52+
short version.
53+
54+
**The grammar (v1 → v2).** The flat v1 surface worked for the core but
55+
could not grow into modules / generics / effects / comptime. v2 adds the
56+
missing layer — *surface → desugar → core* — and is **landing in phases,
57+
tests green** (`spec/ephapax-v2-grammar.ebnf` + the `v2_grammar_phase_*`
58+
suite).
59+
60+
**The soundness proof (v1 → v2).** On 2026-05-26 a machine-checked Coq
61+
counterexample (link:formal/Counterexample.v[`formal/Counterexample.v`],
62+
5 Qed lemmas) *proved* that preservation as stated in the legacy
63+
single-judgment design is unsound — a region exit could invalidate a
64+
sibling's assumptions untracked. Discovering that **with a proof, before
65+
anyone depended on it**, is the rare correct thing, not a failure. The
66+
redesign re-derives preservation across *four orthogonal layers* (regions
67+
/ modality / echo / dyadic mode), each from its own explicit invariants.
68+
The legacy theorem stays `Admitted` on purpose — it is proven unclosable,
69+
so it is fenced off, not abandoned.
70+
71+
Quick proof-status read: **L1** (region capabilities) substantially
72+
complete; **L2** (Linear/Affine modality) core landed with zero axioms;
73+
**L3** (echo / residue) wiring landed (slice 4, 2026-05-27) —
74+
`preservation_l3` + `preservation_l3_region_active_echo` +
75+
`preservation_l3_drop_echo` all Qed (conditional on L1 structural admits,
76+
see PROOF-NEEDS.md §4); **L4** (dyadic mode) Phase A scaffold landed
77+
2026-05-28 (`formal/L4.v`, definitions by design).
78+
79+
**For anyone (human or bot) doing the work:** the only fenced-off
80+
artefacts are the *one* falsified legacy theorem and the *one* superseded
81+
flat grammar. Everything in the v2 columns — the grammar phases and the
82+
per-layer proofs — is open and tractable. Authoritative maps:
83+
link:V1-TO-V2.adoc[`V1-TO-V2.adoc`] (the frame),
84+
link:STATUS.adoc[`STATUS.adoc`] (operational past/present/future),
5985
link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md`]
60-
(four-layer architecture), and link:PROOF-NEEDS.md[`PROOF-NEEDS.md`]
61-
(per-sublanguage proof debt with explicit do-not-do list).
62-
63-
Quick read: **L1** (region capabilities) substantially complete;
64-
**L2** (Linear/Affine modality) core landed with zero axioms; **L3**
65-
(echo / residue) wiring landed (slice 4, 2026-05-27): `preservation_l3`
66-
+ `preservation_l3_region_active_echo` + `preservation_l3_drop_echo`
67-
all Qed (conditional on L1 structural admits — see PROOF-NEEDS.md §4);
68-
**L4** (dyadic mode) Phase A scaffold landed 2026-05-28 (`formal/L4.v`
69-
— `PModeLinear` / `PModeAffine` / `PModeBoundaryMix` + the
70-
`program_mode_to_modality` round-trip; definitions only by design, no
71-
proof obligations).
86+
(four-layer architecture), link:PROOF-NEEDS.md[`PROOF-NEEDS.md`] (proof
87+
debt + do-not-do list). Anything dated before 2026-05-26 describing a
88+
"preservation closure plan" or "910 → 12 goals" is the record of how the
89+
first draft hit its wall — read it as history, not instructions.
7290
====
7391

7492
Ephapax is a research language for **principled handling of

‎STATUS.adoc‎

Lines changed: 35 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -31,27 +31,38 @@ https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambiguation
3131
[discrete]
3232
==== One-paragraph orientation
3333

34+
Ephapax is **gestating** — part-way through a deliberate second draft,
35+
on two independent tracks (grammar and soundness proof), both landing.
36+
For the why-this-is-healthy framing, read link:V1-TO-V2.adoc[`V1-TO-V2.adoc`]
37+
first; this document is the *operational* map underneath it.
38+
3439
On 2026-05-26 a verified Coq counterexample (`formal/Counterexample.v`,
35-
5 Qed lemmas) showed that preservation as stated in the legacy typing
36-
judgment (`formal/Semantics.v`) is **provably false**. The work since
37-
is **not** to close that theorem — no closure exists. The work is a
38-
*four-layer principled redesign* (`formal/PRESERVATION-DESIGN.md`)
39-
where preservation is **re-derived per layer** from explicit
40-
invariants instead of forced through the old judgment.
41-
42-
This document is the single-page map of what that means for the repo:
43-
which work is past (archaeology — don't touch), which is present
44-
(active — extend), and which is future (next moves). Read this before
45-
opening any `.v` file or any PR comment dated before 2026-05-26.
40+
5 Qed lemmas) *proved* that preservation as stated in the legacy
41+
single-judgment design (`formal/Semantics.v`) is unsound. Proving your
42+
own first draft's limit, before anyone depends on it, is the rare correct
43+
move — and it named exactly the invariant the redesign needed. The work
44+
since is **not** to close that theorem (no closure exists; the
45+
`Admitted` is deliberate) but to build the *four-layer principled
46+
redesign* (`formal/PRESERVATION-DESIGN.md`) where preservation is
47+
**re-derived per layer** from explicit invariants. Three of the four
48+
layers already carry `Qed` theorems.
49+
50+
This document maps what that means for the repo: which work is **past**
51+
(the v1 lesson — read it, don't build on it), which is **present**
52+
(the v2 layers — active, extend), and which is **future** (next moves).
53+
The two fenced-off v1 artefacts are narrow; everything in the v2 columns
54+
is open and tractable. Read this before opening any `.v` file or any PR
55+
comment dated before 2026-05-26.
4656

4757
toc::[]
4858

49-
== Past — archaeology (do not extend)
59+
== Past — the v1 lesson (read it, don't build on it)
5060

51-
These artefacts exist on main as the historical record of how we
52-
reached the counterexample. They have documentation value (they show
53-
the *pathway to* the soundness gap). They have **zero merge value**
54-
going forward.
61+
These artefacts are the v1 first draft and the trail that proved its
62+
limit. Their value is real but specific: they are *why the v2 redesign
63+
has the shape it has* — the precise record of the missing invariant.
64+
Keep them readable as the lesson; do **not** build forward on them (the
65+
v2 layers below are where forward work goes).
5566

5667
[cols="2,3,2"]
5768
|===
@@ -264,7 +275,14 @@ ownership). Treating them as competition for mark-and-sweep is a
264275
category error.
265276
====
266277

267-
== What we are NOT doing
278+
== The fences (narrow by design)
279+
280+
These are the guardrails — and they are deliberately *narrow*. Items 1–5
281+
all fence off the **one** falsified v1 artefact (the legacy preservation
282+
theorem and attempts to close it). Items 6–7 are two **design invariants**
283+
that keep the v2 layers orthogonal. Nothing here closes off the live v2
284+
work: the per-layer proofs and the grammar phases remain open. Read this
285+
as "mind these specific posts," not "the field is closed."
268286

269287
* ❌ Closing the legacy `Theorem preservation` in `formal/Semantics.v`.
270288
It is FALSE. No proof closes it.

0 commit comments

Comments
 (0)