docs(EXPLAINME): add L1/L3/L4 claim sections per PRESERVATION-DESIGN §12.3

EXPLAINME.adoc

@@ -16,7 +16,12 @@ is used after being freed, no resource is leaked, and region-scoped
 allocations are deallocated in bulk at scope exit.
 ____
 
-== Claim: Dyadic Type System
+== Claim: Dyadic Type System (L2)
+
+The dyad is L2 in the four-layer architecture (see
+`README.adoc#the-four-layers` and `docs/vision/EPHAPAX-VISION.adoc`).
+This section presents the Rust-side evidence for the L2 discipline;
+L1 / L3 / L4 evidence follows below.
 
 *Evidence*: The type checker (`src/ephapax-typing/src/lib.rs`) tracks
 `BindingForm` per context entry:
@@ -29,6 +34,9 @@ Tests `test_let_allows_unconsumed_linear` and `test_let_bang_rejects_unconsumed`
 verify the distinction. `test_let_bang_rejects_unconsumed_unrestricted` proves
 that `let!` enforces exactly-once even for unrestricted types like `I32`.
 
+The Coq-side L2 evidence is `linear_to_affine : Linear ≤ Affine` (Qed,
+zero axioms) in `formal/Modality.v`.
+
 == Claim: Two-Layer AST (Surface + Core)
 
 *Evidence*: Two separate crates:
@@ -77,6 +85,56 @@ demonstrate where they diverge on identical programs (e.g.
 Test `test_region_non_escaping` verifies escape detection.
 Test `test_region_string_allocation` verifies in-region allocation.
 
+== Claim: Sibling-safe region capabilities (L1)
+
+*Evidence*: Region capabilities are threaded as input/output
+environments through every compound typing rule. A sibling cannot
+reference a region a previous sibling has exited — this is the
+soundness invariant the legacy judgment was missing.
+
+* Counterexample at `formal/Counterexample.v` (all three lemmas
+  `Qed`) demonstrates the soundness gap the threading fixes.
+* The new `has_type_l1` judgment lives in `formal/TypingL1.v` and
+  carries the R-threading directly. Step relation at
+  `formal/Semantics_L1.v`.
+* Design rationale at `formal/PRESERVATION-DESIGN.md §3-§4`.
+* Status: judgment landed; 9 L1 supporting-lemma admits remain as
+  L2-integration debt (tracked in `PROOF-NEEDS.md`).
+
+== Claim: Irreversibility residue is first-class (L3, planned)
+
+*Evidence (planned)*: Operations that erase information (region
+exit, drop) will produce typed residue witnesses, following the
+https://github.com/hyperpolymath/echo-types[echo-types]
+formulation. Linear mode requires the residue to be observed;
+Affine mode permits silent lowering.
+
+* Upstream theory at
+  `~/developer/repos/echo-types/proofs/agda/EchoLinear.agda` (lines
+  30–101), already mechanised.
+* Local mirror at `formal/Echo.v` — the L3 calculus is mechanised
+  here (modes, `LEcho`, `weaken`, `degrade_mode`, all `Qed`).
+* Forward-looking design at `formal/PRESERVATION-DESIGN.md §6`.
+* Status: **planned** integration — `Echo.v` is wired up
+  internally, but no ephapax typing rule yet introduces `TEcho`.
+  The L3 extension follows L1's residual admit closure.
+
+== Claim: Dyadic mode is project-level only (L4)
+
+*Evidence*: L4 is a labelling discipline, not a proof layer.
+`formal/L4.v` carries `ProgramMode` (three-constructor enum) and
+`program_mode_to_modality` (total mapping to L2's modality). No
+theorems, no admits, no axioms — by design.
+
+* Companion design note: `formal/L4-DYADIC.md`.
+* Canonical design source: `formal/PRESERVATION-DESIGN.md §7`.
+* Surface syntax for the L4 declaration
+  (`#![ephapax_linear]` / `#![ephapax_affine]` /
+  `#![module_boundary_mix(...)]`) is not yet wired into the parser
+  or borrow checker; the mechanical scaffold is a citable type for
+  downstream tools (Idris2 ABI, Rust borrow checker, surface
+  parser).
+
 == Technology Choices
 
 [cols="1,2"]

README.adoc

@@ -63,7 +63,9 @@ link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md`]
 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.
+judgment is the next-block work; **L4** (dyadic mode) mechanical
+scaffold landed (`formal/L4.v` — definitions only by design; no proof
+obligations).
 ====
 
 Ephapax is a research language for **principled handling of
@@ -100,15 +102,19 @@ Ephapax is a programming language with:
 |===
 | Property | What this means
 
-| **Dyadic discipline**
+| **Dyadic discipline (L2)**
 | Each binding is *either* affine (`let` — used at most once,
   weakening allowed) *or* linear (`let!` — used exactly once,
-  weakening forbidden). Type checker enforces.
+  weakening forbidden). Type checker enforces. See "The four layers"
+  below for how this composes with L1/L3/L4.
 
-| **Region-based memory**
-| Allocations live in named regions (`region r: ...`); when the
-  region's scope ends, the runtime bulk-frees every resource in it.
-  No allocator overhead per object; no per-object frees.
+| **Region-based memory (L1)**
+| Allocations live in named regions (`region r: ...`). The type
+  system threads a region-capability environment through every
+  expression so a sibling cannot read from a region another sibling
+  has just exited. When a region's scope ends, the runtime bulk-frees
+  every resource in it. No allocator overhead per object; no
+  per-object frees.
 
 | **Second-class borrows**
 | `&x` gives temporary access without consuming `x`. Borrows cannot
@@ -127,6 +133,57 @@ Ephapax is a programming language with:
   reference counting, no allocator-per-object metadata.
 |===
 
+== The four layers
+
+Ephapax composes four orthogonal disciplines. Each is a thin-poset
+refinement, so they compose without coherence obligations
+(https://github.com/hyperpolymath/echo-types[echo-types] supplies the
+recipe).
+
+[cols="1,3"]
+|===
+| Layer | What it enforces
+
+| **L1 — Region capabilities**
+| Every live region is tracked in an input/output environment threaded
+  through every expression. A region cannot be referenced after a
+  sibling has exited it. Soundness proof in `formal/TypingL1.v` +
+  `formal/Semantics_L1.v`.
+
+| **L2 — Structural discipline (linear ↔ affine)**
+| The *modality* of the surrounding program decides whether linear
+  bindings must be consumed (Linear: ephapax-linear) or may be dropped
+  (Affine: ephapax-affine). Same syntax, same semantics — different
+  admissible derivations. Linear ⊆ Affine, proved by `linear_to_affine`
+  Qed in `formal/Modality.v`.
+
+| **L3 — Irreversibility residue (Echo)**
+| Operations that erase information (region exit, drop) produce
+  proof-relevant residue — `Echo f y := Σ A (λ x → f x ≡ y)`. In
+  Linear mode the residue must be observed; in Affine mode it may be
+  silently lowered. Calculus mechanised in `formal/Echo.v`;
+  integration into the typing judgment is the next-block work.
+
+| **L4 — Dyadic interaction mode**
+| A project-level declaration of which side of the dyad the program
+  speaks from (`ephapax_linear` / `ephapax_affine` /
+  `module_boundary_mix`). Selects the L2 modality and the L3
+  observation discipline. No proof obligations of its own — mechanical
+  scaffold in `formal/L4.v` carries definitions only by design.
+|===
+
+.Soundness story
+****
+The four-layer separation is *not* decorative — it exists because the
+original "linear+affine + regions" framing admitted a verified
+counterexample to preservation (see `formal/Counterexample.v` and
+`formal/PRESERVATION-DESIGN.md`). The four-layer redesign restores
+soundness by making each discipline's invariants explicit and
+orthogonal: preservation is *re-derived per layer* from explicit
+invariants rather than forced through a single judgment that hides
+them.
+****
+
 == Three superpowers
 
 The L3 echo / residue layer (Ephapax's contribution to the four-layer