docs(CLAUDE): four-layer guidance + proof-debt bounds (#156)

## Summary

Adds the four-layer overview promised by \`PRESERVATION-DESIGN.md
§12.8\`, deferred from PR #154 because CLAUDE.md was on the disambig
branch at the time. Now that the disambig PR has merged, this is the
small follow-on.

## What's added to CLAUDE.md

- **"The four orthogonal layers" section** — L1/L2/L3/L4 table with the
one-line question an agent should ask to identify which layer their
question touches.
- **Standing rule** about not patching with sibling-region-disjointness
side conditions; the four-layer threading should make that derivable.
- **Disambiguation reminder** for the overlapping L/Linear/Affine name
spaces.
- **Updated standing reminders**: TypingL1.v authoritative alongside
Semantics.v; legacy closure plan superseded; ephapax-affine proof debt
bound spelled out (§12.15).

## Test plan

- [x] CLAUDE.md edits applied cleanly, no other files touched
- [ ] CI green
- [ ] Review: layer-question phrasing matches §12.8 draft text

Refs ephapax#153, ephapax#154, ephapax#152 (disambig PR that landed
CLAUDE.md initially).

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

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

Author: hyperpolymath

CLAUDE.md

@@ -45,8 +45,26 @@ Structured project metadata lives in `.machine_readable/6a2/`:
 - `NEUROSYM.a2ml` — neurosymbolic integration config.
 - `PLAYBOOK.a2ml` — operational runbook.
 
+## The four orthogonal layers
+
+When working in this repo, the typing system has four layers. Knowing which layer a question touches is the first step in answering it:
+
+| Layer | One-line question to ask |
+|---|---|
+| **L1 — Region capabilities** | "Does this involve `R_in`, `R_out`, or `In r R`?" |
+| **L2 — Structural modality** | "Is this about consumption, weakening, or Linear vs Affine?" |
+| **L3 — Echo residue** | "Is this about *what was lost* when an irreversible step fired?" |
+| **L4 — Dyadic mode** | "Is this a project-level mode declaration question?" |
+
+Most questions touch exactly one layer. The design rationale is in `formal/PRESERVATION-DESIGN.md`. The verified counterexample that forced the redesign is in `formal/Counterexample.v` (3 lemmas under the legacy judgment + `bad_input_untypable_l1` under the new `has_type_l1`).
+
+**Standing rule**: if a proposed change appears to require a side condition on a compound typing rule (e.g. "the sibling doesn't reference this region"), pause — the four-layer threading should make that side condition *derivable*, not stated.
+
+**Disambiguation reminder**: the names L1/L2/L3/L4 (layer names), `ephapax-linear`/`ephapax-affine` (L2 modes / the Rust crate), and `Linear`/`Affine` as used in echo-types (L3 modes) deliberately overlap because the underlying thin-poset construction is shared. Agents must disambiguate by context.
+
 ## Standing reminders
 
-- Formal-proof work touches `formal/Semantics.v` (Coq) and `src/abi/Ephapax/…/*.idr` (Idris2). Both build oracles are authoritative; `coqc` and `idris2 --check` are the only "is this proved?" answers.
-- Preservation closure plan: see `ROADMAP.adoc` § "Preservation closure plan" and `formal/PRESERVATION-HANDOFF.md`.
+- Formal-proof work touches `formal/Semantics.v` + `formal/TypingL1.v` (Coq) and `src/abi/Ephapax/…/*.idr` (Idris2). Both build oracles are authoritative; `coqc` and `idris2 --check` are the only "is this proved?" answers.
+- The legacy preservation closure plan is superseded by `formal/PRESERVATION-DESIGN.md` (four-layer redesign). `formal/PRESERVATION-HANDOFF.md` carries the historical diagnostic record only.
+- Ephapax-affine type proofs are **NOT** done — `formal/` mechanises a single legacy judgment + L1's `has_type_l1`; there is no separate mechanised ephapax-affine until L2 + the Linear ⇒ Affine weakening lemma land. See `PRESERVATION-DESIGN.md §12.15`.
 - All commits GPG-signed (key `4A03639C1EB1F86C7F0C97A91835A14A2867091E`), email `6759885+hyperpolymath@users.noreply.github.com`. Auto-merge ON for every PR.