docs(lockdown): CLAUDE.md + banners — block recurrence of legacy-preservation patching (#175)

## Summary

Owner directive 2026-05-27 (received during a session that had just
shipped PR #170 doing exactly the patching the directive forbids):

> We are no longer treating preservation as a proof-engineering problem.
… Do not optimize for smallest patch size. Make sure that never happens
again, and it is very clear what the work is wherever needs documenting;
no further time can be spent on the 'old approach'.

This PR makes the directive impossible to miss across every doc surface
an agent (or human) might encounter when picking up \`formal/\` work.

## What this changes

### NEW: \`CLAUDE.md\` at repo root

Agent-facing guidance with:
- 60-second TL;DR of why preservation in \`Semantics.v\` cannot be
closed.
- Explicit **DO NOT** list (5 items): no closing legacy preservation, no
extending \`Semantics.v\` with closure-supporting lemmas, no closing
\`region_liveness_at_split_l1\` axiom via proof tricks, no following
pre-2026-05-26 closure plans, no patching legacy \`Typing.v\`.
- Affirmative path: read \`PRESERVATION-DESIGN.md\` first; work proceeds
per-layer (L1 / L2 / L3 / L4).
- File reference table marking each \`formal/*.v\` as legacy-frozen vs
active-layered vs forward-looking.
- Two diagnostic questions to ask before touching \`formal/\`.

### Banner: \`formal/PRESERVATION-DESIGN.md\`

CANONICAL banner at top. Same 4-item anti-pattern list as CLAUDE.md plus
the **anti-pattern detector**: "if a session is producing
sibling-region-disjointness side conditions, region-weakening predicates
indexed on syntactic shape, or admit-shuffling between Semantics.v and a
new lemma — escalate to a layer-design discussion."

### Banner: \`formal/PRESERVATION-HANDOFF.md\`

Strengthened from "Superseded" to "ARCHAEOLOGY ONLY — do NOT follow the
closure plans in this file." Keeps the historical 910→12 reduction data
for diagnostic value but explicitly marks it not-a-plan.

### Surgery: \`ROADMAP.adoc\`

- v0.1 "Coq: close preservation to Qed" checkbox rewritten in layered
terms (the work is per-layer derivation, not legacy-theorem closure).
- The 230-line **§ Preservation closure plan** body (5 phases, all aimed
at closing the falsified theorem) is removed. Git history retains it for
forensic value.
- Replaced with a brief "superseded by four-layer redesign" section
pointing at the design doc + CLAUDE.md.

### Memory store


\`~/.claude/.../memory/feedback_ephapax_no_patching_legacy_preservation.md\`
captures the durable directive. The \`MEMORY.md\` index surfaces it in
the always-on disambiguation block alongside the existing
ephapax/affinescript disambiguation entry so future Claude sessions see
it on load.

## What this does NOT change

- No \`.v\` files. The Coq code is untouched.
- No PR closures. PRs landed before this lockdown remain as-is.
- No deletion of \`PRESERVATION-HANDOFF.md\`; the per-case diagnostic
data may still inform layered-design work.

## Test plan

- [x] \`cat CLAUDE.md\` renders sensibly at repo root
- [x] \`PRESERVATION-DESIGN.md\` banner is the first visual block after
the title
- [x] \`ROADMAP.adoc\` no longer contains "Lemma B" / "5-phase" / "close
preservation to Qed" as instructions
- [x] No Coq files modified (no rebuild needed)

🤖 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

@@ -0,0 +1,135 @@
+<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell -->
+
+# CLAUDE.md — Ephapax agent guidance
+
+> **Read this before touching `formal/`.** Several Claude sessions
+> burned hours walking the pre-discovery patching path. This file
+> exists so that doesn't happen again.
+
+## TL;DR — the work, in one paragraph
+
+Ephapax preservation as originally stated in `formal/Semantics.v` is
+**provably false**. `formal/Counterexample.v` exhibits a concrete
+configuration that types, steps, and lands at an untypable post-state
+— all three lemmas `Qed`. The work is therefore **not** to close
+`Theorem preservation` in `Semantics.v`. The work is the **four-layer
+principled redesign** (L1 region capabilities / L2 modality / L3 echo
+/ L4 dyadic mode) documented in `formal/PRESERVATION-DESIGN.md`.
+Preservation is **re-derived** in the new architecture from explicit
+invariants, not forced through the old one.
+
+## DO NOT
+
+These are anti-patterns that have wasted real session time. Refuse
+them if asked; if asked anyway, push back and link this file.
+
+1. **DO NOT close `Theorem preservation` in `formal/Semantics.v`.**
+   It is FALSE. No proof technique closes it because no proof
+   exists. The `Admitted.` is correct.
+
+2. **DO NOT extend `formal/Semantics.v`** with new lemmas aimed at
+   closing the legacy preservation: not Lemma B variants
+   (`sibling_typing_transfers_across_step` /
+   `step_output_context_eq` were earlier attempts in this class),
+   not `region_add_typing_for_non_values`, not strengthened
+   substitution lemmas. The legacy judgment lacks the structural
+   invariant the counterexample demands; no lemma collection bolted
+   onto it will help.
+
+3. **DO NOT close the `region_liveness_at_split_l1` axiom in
+   `formal/Semantics_L1.v` by adding proof tricks, side-conditions
+   discharged ad-hoc, or strengthened lemma signatures within the
+   current judgment shape.** This is *the same kind of patching
+   that produced the legacy admits*, one layer up. The axiom is
+   false-as-stated; it surfaces a real gap that L2/L3 close
+   structurally (cross-layer dependency — see
+   PRESERVATION-DESIGN.md §5.1).
+
+4. **DO NOT follow the "Preservation closure plan" steps in
+   historical PRs / branches / comments.** Anything dated before
+   2026-05-26 (the counterexample landing) that proposes closing
+   `preservation` to `Qed.` is pre-discovery. PRs #92, #102, #104,
+   #106, #114, #116, #117, #121 are part of the historical
+   reduction-from-910-goals record; treat them as archaeology, not
+   instructions.
+
+5. **DO NOT patch the legacy `Typing.v` judgment.** It is the
+   pre-redesign judgment. Counterexample.v depends on its falsity
+   for the regression theorem. Leave it.
+
+## DO
+
+1. **DO read `formal/PRESERVATION-DESIGN.md` first.** It is the
+   canonical design source. The four-layer architecture, the
+   missing-invariant statement, and the per-layer plan are all
+   there.
+
+2. **DO continue the layered build:**
+   - L1 (`TypingL1.v` + `Semantics_L1.v`): R-threading, mostly in
+     place; preservation_l1 has open admits — these are L1 design
+     follow-ups, not legacy patching.
+   - L2 (`TypingL2.v` + `Modality.v`): skeleton landed (#168);
+     mode-specific rules + cross-layer integration are next.
+   - L3 (`Echo.v`): forward-looking scaffold (#166, #167); not
+     wired into L1 yet — that's L1 ⇒ L3 follow-up.
+   - L4: not started; design in §7 of the design doc.
+
+3. **DO derive preservation per-layer.** `preservation_l1` is
+   proved in the L1 vocabulary, against the L1 judgment, using L1
+   invariants. Same for L2, L3. There is no single
+   `preservation` for the unified calculus until L4 composition.
+
+4. **DO escalate before patching.** If a proof attempt requires
+   adding a side-condition to fix a sibling-region-disjointness
+   issue (or analogous cross-rule constraint), that is the signal
+   to escalate to a layer-design discussion — the architecture is
+   asking for a new invariant, not a clever lemma.
+
+## File reference
+
+| File | Status | What it is |
+|---|---|---|
+| `formal/Syntax.v` | shared AST | safe to edit (with care) |
+| `formal/Typing.v` | **legacy** `has_type` | frozen — depends on counterexample's regression role |
+| `formal/Semantics.v` | shared `step` + falsified `preservation` | frozen for the preservation theorem; `step` may need extension at L2/L3 |
+| `formal/Counterexample.v` | three Qed lemmas | the verified soundness gap; do not edit the legacy section |
+| `formal/TypingL1.v` | L1 judgment | active layered work |
+| `formal/Semantics_L1.v` | L1 lemmas + `preservation_l1` | active layered work |
+| `formal/Modality.v` | L2 thin-poset infrastructure | active |
+| `formal/TypingL2.v` | L2 judgment skeleton | active |
+| `formal/Echo.v` | L3 scaffold | forward-looking |
+| `formal/PRESERVATION-DESIGN.md` | **canonical design source** | read this first |
+| `formal/PRESERVATION-HANDOFF.md` | **superseded** diagnostic record | historical only |
+| `ROADMAP.adoc` | scheduling | preservation entries point at design doc |
+
+## If you're unsure
+
+Two questions to ask before touching `formal/`:
+
+1. **Am I about to add an `Admitted` or `Axiom` to close a gap in
+   the old judgment?** If yes — stop. The old judgment is provably
+   incomplete; the right answer is to encode the missing invariant
+   in a new layer, not to admit it.
+
+2. **Am I about to close an L1/L2/L3 admit by reasoning that
+   crosses layers?** If yes — check
+   `PRESERVATION-DESIGN.md §5.1` (cross-layer dependency). The
+   layered design intentionally splits some closures across L1+L2
+   or L1+L3; trying to close them within L1 alone is the trap.
+
+If unsure: ask the owner before writing code. Pause to escalate
+costs less than a 4-hour patching session.
+
+## Memory hooks
+
+If you have access to the user's auto-memory store, relevant entries
+include:
+
+- `project_ephapax_four_layer_redesign.md` — the canonical project
+  state for this redesign.
+- `feedback_ephapax_no_patching_legacy_preservation.md` — the
+  durable directive captured from the 2026-05-27 conversation that
+  produced this CLAUDE.md.
+- `feedback_ephapax_affine_proofs_not_done.md` — what counts as
+  "done" for the ephapax-affine half.