docs(cleanup): residual pre-discovery framing in secondary docs (#186)

Follow-up to #184 + #185. Aligns 5 secondary entry surfaces (EXPLAINME,
TOPOLOGY, docs/vision, ephapax-linear/README,
.machine_readable/META.a2ml) with the post-counterexample doctrine.
ROADMAP.adoc + .gitignore + .gitattributes + wiki deferred (not blocking
proof work). See commit body for per-file detail.

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

.machine_readable/6a2/META.a2ml

@@ -22,7 +22,14 @@ status = "accepted"
 date = "2026-04-11"
 context = "Formal verification of the type system is required for high-assurance use."
 decision = "Dual formalization in Coq (operational semantics) and Idris2 (type structure)."
-consequences = "Fully closed proofs (67 Qed) ensuring the correctness of the linear logic engine."
+consequences = "Mechanised Coq + Idris2 chain. NOTE: as of 2026-05-26 the legacy preservation theorem in formal/Semantics.v was shown to be provably false by formal/Counterexample.v (5 Qed). The single-layer mechanisation has been superseded by the four-layer redesign captured in adr-005 below — see formal/PRESERVATION-DESIGN.md and STATUS.adoc."
+
+[project-meta.architecture-decisions.adr-005]
+status = "accepted"
+date = "2026-05-27"
+context = "On 2026-05-26 formal/Counterexample.v (5 Qed lemmas) demonstrated that preservation in the legacy single-layer judgment is provably false: region exit can invalidate sibling assumptions without the typing judgment tracking that dependency explicitly. The legacy judgment conflates four distinct concerns (structural discipline, region capabilities, dyadic interaction, echo residue)."
+decision = "Four-layer principled redesign with each layer's preservation theorem derived against its own explicit invariants. L1 = region capabilities (TypingL1.v + Semantics_L1.v, modality-indexed); L2 = structural modality Linear/Affine (Modality.v + m in has_type_l1); L3 = echo/residue (Echo.v, fiber-shaped, one type former, L2-mode dispatched at typing-rule boundary); L4 = dyadic interaction (designed only). Echo Types are orthogonal to structural discipline by construction — one Echo type former, Linear/Affine is a thin-poset of observation disciplines layered on top, not two separate echo types."
+consequences = "Preservation is re-derived per layer. Legacy formal/Semantics.v + formal/Typing.v are archaeology and must not be extended. Per-sublanguage proof debt tracked in PROOF-NEEDS.md. Past/present/future map in STATUS.adoc. Owner directive 2026-05-27 in CLAUDE.md is durable. Pre-2026-05-26 closure-plan PRs (#92, #102, #104, #106, #114, #116, #117, #121, #146) are archaeology, not instructions."
 
 # ── Development Practices ──────────────────────────────────────────────────
 [project-meta.development-practices]

EXPLAINME.adoc

@@ -151,64 +151,69 @@ Test `test_region_string_allocation` verifies in-region allocation.
 
 === Coq (`formal/`)
 
-The Coq operational semantics is a small-step substitution-based
-calculus over the Tofte-Talpin region-linear type system.
-
-[cols="3,1,2"]
+[IMPORTANT]
+.Post-counterexample 2026-05-26 — read this before any older proof claim
+====
+The legacy preservation theorem in `formal/Semantics.v` is **provably
+false**. `formal/Counterexample.v` (5 Qed lemmas) demonstrates a
+configuration that types under the legacy judgment, steps via the
+operational semantics, and lands at an untypable post-state. The
+`Admitted.` on `Theorem preservation` is correct — no proof closes it.
+
+The post-discovery work is the **four-layer principled redesign**
+documented in `formal/PRESERVATION-DESIGN.md`, where preservation is
+*re-derived per layer* from explicit invariants. Any earlier-in-this-
+README counts of "910 → 22 → 12 open goals" are archaeology, not
+instructions. See `STATUS.adoc` for the past/present/future map.
+====
+
+The Coq formalisation is now layered. Each layer has its own
+judgment, its own invariants, and its own per-layer preservation
+theorem.
+
+[cols="3,1,3"]
 |===
-| Theorem | Status | Where
+| Component | Status | Where
+
+| Counterexample regression (5 Qed)
+| ✅ Pinned
+| `formal/Counterexample.v` — `bad_input_untypable_l1` Qed under both modes
+
+| L1 judgment (`has_type_l1`)
+| ✅ 100% (2 Qed, 0 admits)
+| `formal/TypingL1.v` — modality-indexed, R-threaded
 
-| `no_leaks`
-| ✅ Qed
-| `formal/Semantics.v`
+| L1 semantics
+| 🟡 15 Qed, 9 admits (L2-integration debt)
+| `formal/Semantics_L1.v` — 9 admits are bullet-structure rewrites for new Affine-only constructors, *not* legacy patching
 
-| `subst_preserves_typing`
-| ✅ Qed
-| `formal/Semantics.v` (line 2808)
+| L2 modality (`Modality.v`)
+| ✅ Core landed (1 Qed, 0 axioms)
+| `formal/Modality.v` + `m : Modality` in `has_type_l1`. PRs #176 + #177. `linear_to_affine` Qed with zero axioms.
 
-| `typing_ctx_transfer`
-| ✅ Qed
-| `formal/Semantics.v`
+| L3 echo / residue calculus
+| ✅ 12 Qed, 0 admits (calculus); ⏳ integration pending
+| `formal/Echo.v` — one type former (fiber `Echo f y := Σ x. f x ≡ y`) + degrade map + no-section-collapse-to-residue proof. Not yet wired into `has_type_l1` or step rules.
 
-| `region_env_perm_typing`, `region_add_typing`, `region_shrink_preserves_typing`
-| ✅ Qed
-| `formal/Semantics.v` (lines 2960, 3042, 3107)
+| L4 dyadic interaction
+| 🔲 Not started
+| Design in `formal/PRESERVATION-DESIGN.md §7`.
 
-| **`preservation`**
-| 🟡 Admitted
-| `formal/Semantics.v` (Theorem at line 3207). **12 open goals** as of 2026-05-21 (was 910). See ROADMAP §"Preservation closure plan" + `formal/PRESERVATION-HANDOFF.md`.
+| Legacy `Theorem preservation` (`formal/Semantics.v`)
+| 🛑 Provably false (Admitted)
+| Pinned by `Counterexample.v`. **Do not attempt closure.** Archaeology.
 |===
 
-The `preservation` reduction story is recent and load-bearing:
-
-* **910 → 29 goals** via the standard preservation pattern
-  (`remember (mu, R, e) as cfg eqn:Hcfg` + `inversion Hcfg; subst`
-  inside each case). Lands as PR #102 (2026-05-20). 97% reduction.
-* **29 → 22 goals** via `revert mu R e mu' R' e' Hcfg Hcfg'` before
-  `induction Hstep`, so each case's IH carries clean universal
-  quantification over the inner step's config rather than the
-  inconsistent outer-cfg equation. Lands as PR #106.
-* **22 → 12 goals** via per-case manual proofs using the new
-  `step_R_eq_or_touches_region` region-invariance lemma (PR #114
-  for the lemma, PR #116 for the 10 case closures: β-reduction,
-  value-step, and atomic cases like `S_Let_Val`, `S_App_Fun`,
-  `S_If_True/False`, `S_Fst`, `S_Snd`, `S_Case_Inl/Inr`, `S_Copy`).
-* **Phase 1 scaffold landed** (PR #121): `step_output_context_eq`
-  (Lemma B) stated with induction-on-step skeleton. Per-case
-  discharges are the next session's substantive work.
-* The remaining 12 are 11 congruence cases blocked on Lemma B
-  (linearity-context drift between IH's output context and
-  sibling's pre-context) + 1 `S_Region_Step + T_Region_Active`
-  case blocked on the documented region-env weakening lemma for
-  non-values.
-
-The canonical closure path is **`ROADMAP.adoc` §"Preservation
-closure plan"** — 5 phases, ~3 sessions of focused work.
-
-An earlier in-file comment (corrected by PR #92, 2026-05-20) claimed
-preservation was Qed-closed on 2026-04-27. That claim was
-unsubstantiated — `coqc` 8.18.0 rejected the proof script. The
-chain above is the honest closure work in progress.
+What's done = `Modality.linear_to_affine` (Linear ⇒ Affine weakening,
+zero axioms), the L1 judgment, L3 fiber + degrade calculus, and the
+counterexample regression witness. What's todo = close the 9
+Semantics_L1 admits (L2-integration debt), wire L3 into the typing
+judgment + step rules, then state per-layer preservation. What's
+banned = closing the legacy theorem, adding new `Axiom` declarations
+to discharge L1/L2 gaps, conflating `ephapax-affine` (this repo's
+sublanguage) with `AffineScript` (a separate language at
+`hyperpolymath/affinescript`). Full per-sublanguage breakdown in
+`PROOF-NEEDS.md`.
 
 === Idris2 (`idris2/src/Ephapax/` + `src/formal/`)
 

TOPOLOGY.md

@@ -1,6 +1,27 @@
 <!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
 <!-- TOPOLOGY.md — Project architecture map and completion dashboard -->
-<!-- Last updated: 2026-03-22 -->
+<!-- Last updated: 2026-05-27 (post-counterexample doctrine landing) -->
+
+> ## Post-counterexample doctrine — read before editing this file
+>
+> This TOPOLOGY map predates the 2026-05-26 counterexample landing in
+> parts of its system architecture diagram. The canonical *current*
+> architecture lives in:
+>
+> - [`STATUS.adoc`](STATUS.adoc) — past/present/future map
+> - [`formal/PRESERVATION-DESIGN.md`](formal/PRESERVATION-DESIGN.md) — four-layer architecture
+> - [`PROOF-NEEDS.md`](PROOF-NEEDS.md) — per-sublanguage proof debt
+> - [`CLAUDE.md`](CLAUDE.md) — agent guidance + owner directive 2026-05-27
+>
+> ### Layer mapping (formal/ contents post-2026-05-27)
+>
+> | Layer | Concern | File(s) | Status |
+> |---|---|---|---|
+> | **L1** | Region capabilities + capability environment threading | `formal/TypingL1.v` + `formal/Semantics_L1.v` | judgment 100%, semantics 15 Qed / 9 admits (L2-integration debt) |
+> | **L2** | Structural modality (Linear vs Affine) | `formal/Modality.v` + `m : Modality` in `has_type_l1` | core landed, `linear_to_affine` Qed with zero axioms |
+> | **L3** | Echo / residue (irreversibility evidence) | `formal/Echo.v` + upstream `hyperpolymath/echo-types` | calculus done (12 Qed), wiring into typing pending |
+> | **L4** | Dyadic interaction semantics | (none yet) | design in `PRESERVATION-DESIGN.md §7` |
+> | 🛑 | Legacy `formal/Semantics.v` + `formal/Typing.v` | archaeology | preservation provably false — see `formal/Counterexample.v` |
 
 # ephapax (selur) — Project Topology
 

docs/vision/EPHAPAX-VISION.adoc

@@ -5,6 +5,42 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 :toclevels: 3
 :icons: font
 
+[IMPORTANT]
+.Post-counterexample reorientation 2026-05-27
+====
+This vision document is **the design rationale**. The architecture
+described here was reframed on 2026-05-26 when a verified Coq
+counterexample showed the original single-layer typing judgment was
+*provably false*. The current architecture is a *four orthogonal
+layers* design (region capabilities / structural modality / echo
+residue / dyadic mode) where preservation is re-derived per layer
+from explicit invariants.
+
+The *intent* below — dyadic discipline, region-based memory, no
+tracing GC, WASM target — survives the redesign intact. The
+*mechanisation* is layered.
+
+For implementation status (per-layer counts, what's done, what's
+todo, what's banned), read in this order:
+
+. link:../../STATUS.adoc[`STATUS.adoc`] — past/present/future map.
+. link:../../formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md`] — the four-layer architecture doctrine.
+. link:../../PROOF-NEEDS.md[`PROOF-NEEDS.md`] — per-sublanguage proof debt.
+====
+
+[NOTE]
+.Disambiguation (ephapax ≠ AffineScript)
+====
+This is **`hyperpolymath/ephapax`** — a research language with
+mechanised Coq + Idris2 proofs. It is **not**
+`hyperpolymath/affinescript`, which is a separate JS/TS/ReScript
+successor with no mechanised proofs. The lexical overlap of "affine"
+in both names is a coincidence of substructural-logic terminology.
+Internal naming trap: `ephapax-affine` (the sublanguage *inside*
+this repo) is also **not** AffineScript. Canonical disambiguation:
+https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambiguation/ephapax-vs-affinescript.md.
+====
+
 == What Ephapax Is
 
 Ephapax is a *programming language*. Not a proof assistant, not a type checker

ephapax-linear/README.md

@@ -1,5 +1,26 @@
 # ephapax-linear
 
+> ## 🛑 First-read disambiguation
+>
+> This crate is part of **`hyperpolymath/ephapax`** — a research language for
+> compile-time WebAssembly memory safety, formally verified in Coq + Idris2.
+>
+> **`ephapax-linear` is *not* `hyperpolymath/affinescript`.** AffineScript is
+> a separate, unrelated language (JS/TS/ReScript successor, OCaml + ReScript
+> runtime). The two share only the compile target (`hyperpolymath/typed-wasm`).
+>
+> **Internal naming trap (important):** This crate implements *both*
+> sublanguages of Ephapax — `ephapax-linear` (strict core) AND `ephapax-affine`
+> (versatile prototyping companion). The name of the crate is `ephapax-linear`
+> for historical reasons, but **the affine grammar in this crate is NOT
+> `AffineScript`.** The lexical overlap of the word `affine` is a coincidence
+> of substructural-logic family terminology, not a project relationship. Do
+> not apply tactics, lessons, or framings from `hyperpolymath/affinescript`
+> here, and vice versa.
+>
+> Canonical disambiguation:
+> [`hyperpolymath/nextgen-languages/docs/disambiguation/ephapax-vs-affinescript.md`](https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambiguation/ephapax-vs-affinescript.md).
+
 Standalone linear/affine discipline checker for the Ephapax language.
 
 ## Dual Grammars