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

## Summary

Executes [`formal/PRESERVATION-DESIGN.md`
§12.3](../blob/main/formal/PRESERVATION-DESIGN.md) — the EXPLAINME
rollout.

### What changed

1. **"Dyadic Type System" → "Dyadic Type System (L2)"** — labelled and
cross-references the README four-layers section + `EPHAPAX-VISION.adoc`.
Adds the Coq-side L2 evidence pointer (`linear_to_affine` Qed in
`formal/Modality.v`).
2. **New claim: "Sibling-safe region capabilities (L1)"** — inserted
after Region-Based Memory. Cites `Counterexample.v` + `has_type_l1`
judgment + §3-§4 design rationale. Honestly labels 9 residual L1 admits
as L2-integration debt.
3. **New claim: "Irreversibility residue is first-class (L3, planned)"**
— upstream + local evidence pointers; integration honestly labelled
planned.
4. **New claim: "Dyadic mode is project-level only (L4)"** — cites
`formal/L4.v` definitions + `L4-DYADIC.md` design note; explicit "no
theorems by design" claim.

### Honesty constraint preserved

§12.3 explicitly says: *"the evidence is the design doc +
counterexample, not a passing proof — say so honestly"*. The new
sections follow that — where evidence is a design doc or planned, it is
labelled as such.

### Scope

Pure documentation. Companion to README #256 (§12.2 half).

## Test plan

- [x] All claims back-cite a real artefact (verified each pointer exists
in repo).
- [x] GPG-signed commit.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

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

Author: hyperpolymath

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"]