docs: past-present-future doctrine (STATUS + PROOF-NEEDS rewrite + README banner + L3 diagram + .v signposts) (#184)

## Summary

Single-PR landing of the orientation doctrine that prevents future
sessions from "redoing the old stuff". Seven coordinated artefacts so
the doctrine catches every reader at every entry point — human or
machine.

## Files

| Type | File | Purpose |
|---|---|---|
| NEW | `STATUS.adoc` | Single-page past / present / future map at repo
root. The doc that answers "where are we?" with a top-of-document
disambiguation banner (ephapax ≠ AffineScript). |
| REWRITE | `PROOF-NEEDS.md` | Per-sublanguage proof debt audit,
separated for ephapax-linear and ephapax-affine. Sections: done / todo /
banned (6 anti-pattern categories) / counts. Replaces the prior version
which still carried the pre-discovery legacy-preservation closure plan
as viable. |
| PATCH | `README.adoc` | Foundational-redesign-in-progress banner;
replaces pre-discovery "12 admits / 910 closed" Coq narrative with
post-discovery per-layer picture; adds "Three superpowers" section with
the NOT-a-tracing-GC-replacement caveat; adds "What this enables" (GDPR
/ verified resource management / policy enforcement); doc-map updated. |
| PATCH | `formal/PRESERVATION-DESIGN.md §6` | One-sentence anchor +
ASCII diagram + 3-point explanation of L3 architecture (one type former,
two observation disciplines, one-way Linear→Affine via degrade). |
| BANNER | `formal/Semantics.v` | 🛑 ARCHAEOLOGY — do not extend |
| BANNER | `formal/Typing.v` | 🛑 ARCHAEOLOGY — Counterexample.v depends
on falsity |
| BANNER | `formal/Semantics_L1.v` | ✅ ACTIVE — 9 admits are
L2-integration debt |
| BANNER | `formal/TypingL1.v` | ✅ ACTIVE — judgment 100%,
modality-indexed |
| BANNER | `formal/Modality.v` | ✅ ACTIVE — L2 (thin poset); L3 must not
pattern-match |
| BANNER | `formal/Echo.v` | ✅ ACTIVE — ONE type former; do not split
LinearEcho/AffineEcho |
| BANNER | `formal/Counterexample.v` | 📌 PINNED REGRESSION WITNESS — do
not weaken |

## Disambiguation reinforced

STATUS.adoc opens with a CAUTION callout aimed at both human + machine
readers: Ephapax ≠ AffineScript; ephapax-affine (the sublanguage
*inside* this repo) ≠ AffineScript. The lexical overlap of "affine" is a
coincidence of substructural-logic terminology, not a project
relationship. PROOF-NEEDS.md leads with the same disambiguation. The
README's existing IMPORTANT callout is strengthened with the cross-repo
lesson-warning.

## Safety envelope

- No `.v` semantic changes.
- No new `Admitted` or `Axiom` introduced.
- No legacy code touched (`Semantics.v`, `Typing.v`) except top-of-file
banner comments.
- L1, L2, L3 calculi unchanged.
- Counterexample.v unchanged.

## Closes

This PR is the canonical post-discovery doctrine landing. It supersedes
the in-flight #154 (filed 2026-05-26 with pre-consolidated framing).
#154 will be closed in a follow-up after this lands; any unique
linguistically-safe file-additions from #154 (`EXPLAINME.adoc`,
`EPHAPAX-VISION.adoc`, `spec/SPEC.md`, `site/index.md`,
`ephapax-linear/README.md`, `TOPOLOGY.md`) can be ported in a smaller
follow-up with the current framing.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

PROOF-NEEDS.md

@@ -36,15 +36,47 @@ repo*, one Rust crate, one AST, two structural disciplines. **`ephapax-affine`
 is not AffineScript.** When ambiguous, write "ephapax-affine sublanguage"
 vs "AffineScript language".
 
-Canonical disambiguation:
+Canonical disambiguation (read this before applying any cross-repo
+lesson):
 link:https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambiguation/ephapax-vs-affinescript.md[nextgen-languages/docs/disambiguation/ephapax-vs-affinescript.md].
 ====
 
-A dyadic linear+affine type system for compile-time WebAssembly
-memory safety. Resources are tracked through the type system so the
-compiler can guarantee — without a garbage collector — that no value
-is used after being freed, no resource is leaked, and region-scoped
-allocations are deallocated in bulk at scope exit.
+[WARNING]
+.🔄 Foundational redesign in progress — read `STATUS.adoc` before opening any `.v` file
+====
+On 2026-05-26 a verified Coq counterexample
+(link:formal/Counterexample.v[`formal/Counterexample.v`], 5 Qed
+lemmas) showed that preservation as stated in the legacy typing
+judgment is **provably false**. The repo is in the middle of a
+*four-layer principled redesign* (regions / modality / echo / dyadic
+mode) where preservation is *re-derived per layer* from explicit
+invariants rather than forced through the old judgment.
+
+Anything in this README dated before 2026-05-26 that describes a
+"preservation closure plan" or counts "910 → 22 → 12 open goals" is
+**archaeology, not instructions**. The authoritative status is in
+link:STATUS.adoc[`STATUS.adoc`] (past / present / future map),
+link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md`]
+(four-layer architecture), and link:PROOF-NEEDS.md[`PROOF-NEEDS.md`]
+(per-sublanguage proof debt with explicit do-not-do list).
+
+Quick read: **L1** (region capabilities) substantially complete;
+**L2** (Linear/Affine modality) core landed with zero axioms; **L3**
+(echo / residue) calculus done locally, integration into the typing
+judgment is the next-block work; **L4** (dyadic mode) not started.
+====
+
+Ephapax is a research language for **principled handling of
+irreversible boundaries** (region exits, drops, key erasure, audit
+trails) in compile-time-memory-safe WebAssembly. Real systems are
+irreversible — operating systems deallocate, databases drop tables,
+security systems erase keys, compilers collapse high-level
+distinctions. Ephapax gives a disciplined, machine-checkable
+framework to handle those boundaries responsibly: the type system
+tracks not just *what is owned* but *what was lost when it was given
+up*, so reclamation can carry mandatory evidence where it matters
+(audit, compliance, cryptographic erasure) and degrade to free where
+it doesn't (inference loops, hot paths).
 
 The core calculus is mechanically formalised. Soundness theorems on
 the dynamic side (Coq) and structural-safety theorems on the type
@@ -95,6 +127,94 @@ Ephapax is a programming language with:
   reference counting, no allocator-per-object metadata.
 |===
 
+== Three superpowers
+
+The L3 echo / residue layer (Ephapax's contribution to the four-layer
+design) opens three things proper reversible programming struggles
+with:
+
+[cols="1,3"]
+|===
+| Superpower | What it gives you
+
+| **A. Accountability of irreversible reclamation**
+| You can free memory (`S_Region_Exit`, `S_Drop`) and the type system
+  *knows* you lost the data — and tracks what depended on it. Under
+  the Linear modality the reclamation event carries a mandatory
+  evidence-bearing `Echo` value; under Affine you opt out for
+  performance. Pairs cleanly with region-based memory management
+  (deterministic bulk free) to deliver high-assurance reclamation
+  that tracing GC cannot — by design, tracing GC *hides* the
+  reclamation evidence.
+
+| **B. Selective reversibility (thin-poset)**
+| Linear ≤ Affine is a two-point thin poset at the L2 modality. You
+  pick per-region (or per-project) which discipline applies. Same
+  code shape, different evidence obligations. Concrete examples:
+  *Linear* during backpropagation (must keep the gradient residue);
+  *Affine* during inference (drop the residue, save memory). You get
+  the safety of reversibility where you need it, and the performance
+  of irreversibility where you don't.
+
+| **C. Debugging + provenance**
+| Attach Linear Echoes to critical state changes. The type system
+  guarantees the receipt (preimage) of that state change was retained
+  — so when a bug fires, the inputs that produced the error are
+  recoverable by construction. In Affine mode you opt out of this
+  debugging info, with the same code shape. The evidence is a
+  *theorem-level guarantee*, not a runtime convention.
+|===
+
+[CAUTION]
+.Echo Types are NOT a tracing-GC replacement
+====
+Echo Types do **not** solve reachability or cycles. They are not a
+"fire-and-forget" automatic memory manager. Their strength is
+*accountability of irreversible reclamation* in systems that already
+know when and how to deallocate (regions, explicit drop, deterministic
+ownership). Treating them as competition for mark-and-sweep or
+generational GC is a category error.
+
+The committed v1 direction is *Linear Echo + Region-Based Memory
+Management* (deterministic bulk free with mandatory certified
+evidence). A speculative future direction is an optional Linear
+discipline on deterministic Rust-style drop for critical resources
+(keys, sensitive buffers requiring provable erasure) — flagged but
+not committed.
+====
+
+== What this enables
+
+The three superpowers translate to concrete use cases the type
+system can *prove* properties about:
+
+* **Mandatory evidence for critical actions.** By making certain
+  echoes Linear (mandatory observation), the type system guarantees
+  that a region exit *always* emits an audit trail, or that a drop
+  *always* triggers a required cleanup.
+
+* **GDPR "right to be forgotten" with certified evidence of
+  erasure.** Linear-echo discipline on the `S_Drop` of a personal-data
+  resource is a type-level proof that erasure happened *and* that the
+  required notification / log was produced. Auditors get a
+  machine-checkable artefact instead of a process attestation.
+
+* **Verified resource management for keys, secrets, and sensitive
+  buffers.** Linear-echo on the deallocation of a key buffer
+  guarantees provable erasure; the typing rule cannot be silenced.
+
+* **Selective reversibility without redesigning your language.**
+  The thin-poset means you don't redesign the runtime to be
+  bijective. You add *one* type former (the fiber) and layer
+  existing L2 modalities over it. Orthogonal and compositional.
+
+* **Machine-checkable foundation for policy enforcement.** The
+  thin-poset Linear ≤ Affine + the proven non-invertibility
+  (`EchoResidue.no-section-collapse-to-residue`) gives sharp,
+  proof-relevant reasoning: *weakening obligations is allowed*,
+  *strengthening them back is impossible*. Clean logical foundation
+  for compliance work.
+
 == What this isn't
 
 * **Not Rust.** Rust uses ownership + borrowing with a single discipline
@@ -226,25 +346,46 @@ Two complementary formalisations, both run on every push:
 === Coq (`formal/`)
 
 Operational semantics with small-step reduction over a substitution-
-based calculus. Proves dynamic properties (no stuck states, region
-exits free everything, substitution preserves typing).
-
-Currently `Qed`-closed: `no_leaks`, `subst_preserves_typing`,
-`typing_ctx_transfer`, `region_env_perm_typing`, `region_add_typing`,
-`region_shrink_preserves_typing`, plus 70+ supporting lemmas.
-
-Currently `Admitted`: `preservation`. **12 open goals remain** after
-the reduction chain — down from **910** at the start of the campaign
-(98.7% reduction across PRs #92 / #102 / #104 / #106 / #114 / #116 /
-#117 / #121, 2026-05-20 → 2026-05-21). Phase 1 scaffold of the
-closure plan (Lemma B `step_output_context_eq`) landed; per-case
-discharges next. The remaining 12 are 11 congruence cases (blocked
-on Lemma B's per-case proofs — linearity-context drift between IH
-and sibling) + 1 `S_Region_Step + T_Region_Active` case (blocked on
-region-env weakening for non-values). Canonical closure path:
-**`ROADMAP.adoc` §"Preservation closure plan"** (5 phases, ~3
-sessions of focused work). See also `formal/PRESERVATION-HANDOFF.md`
-for the per-case diagnostic record.
+based calculus. Post-2026-05-26 the formalisation is layered:
+
+* **Legacy** (`formal/Semantics.v`, `formal/Typing.v`) — the original
+  pre-discovery judgment. `Theorem preservation` here is **provably
+  false** (the counterexample at `formal/Counterexample.v` is 5 Qed
+  lemmas proving it). The `Admitted.` is correct. **Do not extend.**
+  Treat as archaeology — see link:STATUS.adoc[`STATUS.adoc`] for the
+  pre-discovery PR list and the explicit do-not-do reasoning.
+
+* **Layer 1 — region capabilities** (`formal/TypingL1.v`,
+  `formal/Semantics_L1.v`). The new judgment is modality-indexed
+  (`has_type_l1 m : ...`) and threads a capability environment `R`
+  through compound rules. Judgment 100% (0 admits, 2 Qed); semantics
+  carries 9 supporting-lemma admits that are *L2-integration debt*
+  (bullet-structure rewrites for new Affine-only constructors), not
+  legacy patching.
+
+* **Layer 2 — structural modality** (`formal/Modality.v`). Linear
+  vs Affine as a K-free thin-poset decoration. `linear_to_affine`
+  is **Qed with zero axioms**. Landed via PRs #176 + #177.
+
+* **Layer 3 — echo / residue** (`formal/Echo.v`). 12 Qed lemmas
+  covering the fiber calculus, degrade map, and the
+  `no-section-collapse-to-residue` irreversibility theorem (mirrors
+  the upstream Agda development at
+  https://github.com/hyperpolymath/echo-types[`hyperpolymath/echo-types`]).
+  Calculus is done; *wiring into the typing rules* (`T_Observe`,
+  collapse-function emission on irreversible steps,
+  `G`-context threading) is the next-block work.
+
+* **Layer 4 — dyadic interaction**. Design in
+  link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md §7`].
+  Not started.
+
+Per-sublanguage proof debt with explicit do-not-do list lives in
+link:PROOF-NEEDS.md[`PROOF-NEEDS.md`]. The four-layer architecture
+rationale is in
+link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md`].
+The counterexample itself is
+link:formal/Counterexample.v[`formal/Counterexample.v`] (5 Qed).
 
 [source,bash]
 ----
@@ -379,9 +520,25 @@ generics, effects, traits, comptime, contracts) lives on
 | ✅ Qed
 |
 
-| Coq `preservation`
-| 🟡 Admitted (22 open / 910 closed)
-| Multi-day proof-engineering campaign in flight
+| Coq legacy `preservation`
+| 🛑 Admitted — provably false
+| Counterexample at `formal/Counterexample.v` (5 Qed). Not closable. Archaeology.
+
+| Coq L1 (region capabilities)
+| ✅ Judgment 100%; 🟡 semantics 9 admits
+| 9 admits = L2-integration debt. See `PROOF-NEEDS.md`.
+
+| Coq L2 (modality)
+| ✅ Core landed (PRs #176 + #177); 0 axioms
+| `linear_to_affine` Qed. Integration debt absorbed by L1 admits above.
+
+| Coq L3 (echo / residue calculus)
+| ✅ 12 Qed, 0 admits
+| Calculus done locally; integration into typing rules pending.
+
+| Coq L4 (dyadic interaction)
+| 🔲 Not started
+| Design in `formal/PRESERVATION-DESIGN.md §7`.
 
 | Idris2 region-linearity theorems
 | ✅ Complete (zero unsafe)
@@ -405,21 +562,41 @@ generics, effects, traits, comptime, contracts) lives on
 | link:README.adoc[README]
 | You are here. Overview + quickstart.
 
+| link:STATUS.adoc[STATUS.adoc]
+| **Past / present / future map.** Single page that answers "where
+  are we?" Read this before any `.v` file or any PR comment dated
+  before 2026-05-26.
+
+| link:PROOF-NEEDS.md[PROOF-NEEDS.md]
+| Per-sublanguage proof debt audit. What's done (Qed), what's todo,
+  what's banned (anti-pattern detector). Separated for ephapax-linear
+  and ephapax-affine sublanguages.
+
+| link:formal/PRESERVATION-DESIGN.md[formal/PRESERVATION-DESIGN.md]
+| **Canonical four-layer design doctrine.** Why the counterexample
+  forced the redesign, the four orthogonal concerns, per-layer plans.
+
+| link:formal/Counterexample.v[formal/Counterexample.v]
+| The 5 Qed lemmas that pin the soundness gap of the legacy judgment.
+  Authoritative source of the gap; future proofs must coexist with it.
+
+| link:CLAUDE.md[CLAUDE.md]
+| Agent guidance. Carries the 2026-05-27 owner directive,
+  anti-pattern detector, escalation rule.
+
 | link:EXPLAINME.adoc[EXPLAINME.adoc]
 | "Show me the receipts" — every claim in this README backed by a
   specific file, test, or proof.
 
 | link:ROADMAP.adoc[ROADMAP.adoc]
-| Quantitative milestones (v0.1.0 → v1.0.0), per-version checklists,
-  current open work.
-
-| link:PROOF-NEEDS.md[PROOF-NEEDS.md]
-| Outstanding proof obligations: what's `Admitted` / `covering` /
-  `partial` and why.
+| Milestones (v0.1.0 → v1.0.0), per-version checklists, current open
+  work. Note: any pre-2026-05-26 closure-plan content is superseded
+  by STATUS.adoc + PRESERVATION-DESIGN.md.
 
 | link:formal/PRESERVATION-HANDOFF.md[formal/PRESERVATION-HANDOFF.md]
-| Per-case checklist for the 22 remaining preservation goals. Read
-  this if you're picking up the Coq proof work.
+| **Archaeology only** — historical diagnostic record of the
+  pre-counterexample closure attempts. Reads as a closure plan; isn't
+  one. Useful only for understanding *why* the redesign happened.
 
 | link:RUST-SPARK-STANCE.adoc[RUST-SPARK-STANCE.adoc]
 | Stance on Rust + SPARK interop and where Ephapax fits.