docs(truth): restore doc-code consistency for proof state + bury banned-preservation framing (#263)

## Summary

Foundational documentary-truth fix surfaced by a comprehensive meander
audit. Two systemic patterns repaired across 11 files (CLAUDE.md
deferred to the in-flight pr-253 SPDX-header sweep).

## Pattern A — "Counterexample.v has 3 Qed" cascade

Actual: **5 Qed** (`bad_typable`, `bad_step`, `bad_post_untypable`,
`t_loc_l1_R_preserving`, `bad_input_untypable_l1`). Stale 3-count
propagated through 8 documents; fixed at all sites in this PR.

## Pattern B — Banned legacy-preservation framing as live debt

Despite the durable owner directive 2026-05-27, 5 surfaces still framed
it as actionable:

- `README.adoc:744` contributing priorities — removed "Close
`preservation` to Qed (22 goals remaining)" + added NOTE explaining the
directive; replaced with Phase 3b Stages 2/3/4 + L1 progress.
- `ROADMAP.adoc` v1.0.0 — replaced with "Per-layer
`preservation_l1/l2/l3` closed" + NOTE; per-layer rollup refreshed.
- `EXPLAINME.adoc:367` + `ROADMAP.adoc` related-docs —
`PRESERVATION-HANDOFF.md` relabelled "archaeology only".
- `docs/proof-debt.adoc` + `docs/proof-debt.md` — both prefaced with
SUPERSEDED block.

## Pattern C — `PROOF-NEEDS.md §4` wholesale refresh

- Per-file map: `Semantics.v` Admitted 3→1; `Semantics_L1.v` Qed 26→37;
`TypingL2.v` "wrapper"→10 Qed with names; added Counterexample_L2.v +
Counterexample_L2_nested.v + L4.v rows.
- Seam audit: all 8 line numbers refreshed
(576/646/678/1994/2014/2028/3132/3133).
- Falsity audit added: identifies TWO provably-false-as-stated admits.

## Pattern D — `PROOF-NEEDS.md §1` status table

Reflects Phase 3b Stage 1a (#252) and Stage 1b (#253) landings; adds L2
β-case lemmas + L4 scaffold + Counterexample_L2 witnesses rows.

## SPDX headers

Moves SPDX on touched files from PMPL-1.0-or-later to MPL-2.0 (matches
workspace `Cargo.toml`, satisfies pre-commit hook). Strict subset of
what pr-253 sweep will land — no conflict, idempotent.

## Test plan

- [x] Local Coq build oracle green (`just -f formal/Justfile all`, 12/12
modules)
- [x] Pre-commit hook accepts all 11 files
- [ ] Confirm CI greens on PR

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

---------

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -41,7 +41,7 @@ updated: 2026-05-30T20:00:00Z
 #
 # Current state (verified by coqc 8.18 on main, post-#176/#177):
 #   - formal/Semantics.v `preservation`: Admitted — PROVABLY FALSE per
-#     Counterexample.v (three Qed lemmas). NOT to be closed.
+#     Counterexample.v (five Qed lemmas). NOT to be closed.
 #   - formal/Semantics.v `step_preserves_type`, `step_output_context_eq`,
 #     and their at_pre helpers are Qed but support legacy-preservation
 #     closure attempts that are now ruled out. Retained for diagnostic

0-AI-MANIFEST.a2ml

@@ -24,7 +24,7 @@ These 7 A2ML files MUST exist in `.machine_readable/6a2/` directory ONLY:
 
 ## CORE INVARIANTS
 
-1. **Formal Proof Integrity** — Coq proofs are layered per the four-layer redesign (`formal/PRESERVATION-DESIGN.md`). The legacy `preservation` in `Semantics.v` is provably FALSE per `Counterexample.v` (3 Qed lemmas) and remains `Admitted`. The L1 preservation chain (`Semantics_L1.v`) is in flight; explicit `Admitted` / `admit.` / `Axiom` sites are enumerated by `file:line` in `docs/proof-debt.adoc` per the standards#203 trusted-base reduction policy. Idris2 source has no `believe_me` / `assert_total` / `sorry`. ANY new escape hatch must be enumerated in `docs/proof-debt.adoc` before the trusted-base CI check will pass.
+1. **Formal Proof Integrity** — Coq proofs are layered per the four-layer redesign (`formal/PRESERVATION-DESIGN.md`). The legacy `preservation` in `Semantics.v` is provably FALSE per `Counterexample.v` (5 Qed lemmas) and remains `Admitted`. The L1 preservation chain (`Semantics_L1.v`) is in flight; explicit `Admitted` / `admit.` / `Axiom` sites are enumerated by `file:line` in `docs/proof-debt.adoc` per the standards#203 trusted-base reduction policy. Idris2 source has no `believe_me` / `assert_total` / `sorry`. ANY new escape hatch must be enumerated in `docs/proof-debt.adoc` before the trusted-base CI check will pass.
 2. **Dyadic Separation** - The boundary between affine and linear types must be strictly enforced.
 3. **SPDX Headers** - All source files MUST carry `SPDX-License-Identifier: PMPL-1.0-or-later`.
 4. **Author Attribution** - Always "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>".

EXPLAINME.adoc

@@ -93,7 +93,7 @@ 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
+* Counterexample at `formal/Counterexample.v` (all five 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
@@ -377,8 +377,11 @@ the per-crate breakdown). Key test categories:
 * `docs/specs/LANGUAGE-COMPARISON.adoc` — comparison against 10 languages
 * `docs/vision/EPHAPAX-VISION.adoc` — design rationale, why dyadic +
   regions + WASM
-* `formal/PRESERVATION-HANDOFF.md` — per-case checklist for the 22
-  remaining preservation goals
+* `formal/PRESERVATION-HANDOFF.md` — *archaeology only*: per-case
+  checklist from the pre-2026-05-26 legacy-judgment closure plan,
+  retained for historical context. The legacy `preservation` is
+  provably false; the path forward is the per-layer theorems documented
+  in `formal/PRESERVATION-DESIGN.md`.
 * `PROOF-NEEDS.md` — outstanding proof obligations + leverage
 
 == Questions?

PROOF-NEEDS.md

@@ -56,7 +56,10 @@ For the architectural background see
 | L1 judgment indexed by modality `m : Modality` | `formal/TypingL1.v` | landed via PRs #176 + #177 |
 | L2 modality core (`Modality.v`, `linear_to_affine`) | `formal/Modality.v` | 1 Qed, zero axioms |
 | L3 calculus (echo / residue fiber + degrade + no-section proof) | `formal/Echo.v` | 12 Qed, 0 admits |
-| Linear-mode forward progress lemmas | `formal/Semantics_L1.v` | 26 Qed (incl. 3 new from L3 slice 4: `preservation_l3_region_active_echo` / `preservation_l3_drop_echo` / `preservation_l3` umbrella); 3 outer `Admitted.` markers cover 5 internal `admit.` cases — all pre-existing L1 structural debt OR true parallel mirrors |
+| Linear-mode forward progress lemmas | `formal/Semantics_L1.v` | 37 Qed; 3 outer `Admitted.` markers cover 5 internal `admit.` cases at current lines 576/646/1994/2014/3132. Phase 3b Stage 1a (#252, MERGED 2026-05-30: `tfuneff_lambda_free` + `Counterexample_L2_nested.v`) and Stage 1b (#253, MERGED 2026-05-31: closed-value substitution + `preservation_l2_app_eff_beta` β-case for TFunEff). Slice 4 L3 wiring delivered `preservation_l3_region_active_echo` / `preservation_l3_drop_echo` / `preservation_l3` umbrella. |
+| L2 β-case lemmas (Stage 1b) | `formal/TypingL2.v` | 10 Qed total: `weaken_modality` family (5), `preservation_l2_via_l1` (conditional on `preservation_l1`), `linear_value_retype_l1_m`, and 3 `preservation_l2_app_eff_beta_*` variants (Linear / ground_nonlinear / tfuneff conditional on Stage 1b side conditions P1+P2+P3). Stage 2/3/4 (#240/#241/#242) drop the conditions. |
+| L4 labelling scaffold (Phase A, 2026-05-28) | `formal/L4.v` | `ProgramMode` enum (`PModeLinear` / `PModeAffine` / `PModeBoundaryMix`) + `program_mode_to_modality` round-trip. Definitions only — no theorems, zero axioms. |
+| Counterexample_L2 regression witnesses (Phase 4c + 3b) | `formal/Counterexample_L2.v`, `formal/Counterexample_L2_nested.v` | 5 + 5 Qed pinning the Phase 4c (fresh-region scope crossing) and Phase 3b (nested TFunEff) soundness-gap classes |
 | Counterexample regression witness | `formal/Counterexample.v` | 5 Qed (`bad_input_untypable_l1` proved under both modes) |
 | Operational checker (Rust, ephapax-linear sublanguage) | `ephapax-linear/src/linear.rs` | working — discharges resource-exact obligation |
 
@@ -68,7 +71,7 @@ For the architectural background see
 | Linear ⇒ Affine weakening | `formal/TypingL1.v` `linear_to_affine` | Qed, zero axioms |
 | Operational checker (Rust, ephapax-affine sublanguage) | `ephapax-linear/src/affine.rs` | working — permits weakening / graceful abandonment |
 | Affine-mode echo discipline (LEcho Affine = lowered triple) | `formal/Echo.v` (calculus) | calculus done; rule wiring pending |
-| Affine forward progress lemmas | `formal/Semantics_L1.v` | bullet-structure rewrites + subst_typing_gen_l1_m + region_shrink_preserves_typing_l1_gen_m m-polymorphic generalisations landed 2026-05-27; remaining 3 admits are L2-β deeper-than-bullet debt (see §2) |
+| Affine forward progress lemmas | `formal/Semantics_L1.v` | bullet-structure rewrites + `subst_typing_gen_l1_m` + `region_shrink_preserves_typing_l1_gen_m` m-polymorphic generalisations landed 2026-05-27; Phase 3b Stage 1a + 1b landed 2026-05-30/31 via #252 + #253. Remaining admits are pre-existing L1 structural debt + one provably-false-as-stated sub-case (`Semantics_L1.v:1994` / mirror `:2014` — closure requires Phase D reformulation, not direct proof). See §4 seam audit. |
 
 ### Counterexample regression
 
@@ -242,45 +245,57 @@ preservation, provably false per `Counterexample.v` + 3 outer
 `admit.` cases — all pre-existing L1 structural debt + parallel
 mirrors. See the per-file table and seam audit below.)
 
-### Per-file Qed / Admitted summary (as of 2026-05-28)
+### Per-file Qed / Admitted summary (as of 2026-06-01)
 
 | File | Qed | Admitted | Disposition |
 |---|---:|---:|---|
-| `formal/Semantics.v` (legacy) | n/a | **3** | 🛑 archaeology — do not extend |
+| `formal/Semantics.v` (legacy) | n/a | **1** | 🛑 archaeology — single `Admitted.` at line 9257 (`Theorem preservation`, provably false); do not extend |
 | `formal/Typing.v` (legacy) | n/a | 0 | 🛑 archaeology — `Counterexample.v` depends on falsity |
-| `formal/Counterexample.v` | **5** | 0 | ✅ pinned regression witness |
+| `formal/Counterexample.v` | **5** | 0 | ✅ pinned regression witness (`bad_typable`, `bad_step`, `bad_post_untypable`, `t_loc_l1_R_preserving`, `bad_input_untypable_l1`) |
+| `formal/Counterexample_L2.v` | **5** | 0 | ✅ Phase 4c soundness-gap witness — fresh-region scope crossing (`v_typed_at_empty`, `outer_typed`, `e_before_typed`, `e_step`, `e_after_untypable`) |
+| `formal/Counterexample_L2_nested.v` | **5** | 0 | ✅ Phase 3b soundness-gap witness — nested TFunEff (analogue structure to `Counterexample_L2.v`) |
 | `formal/TypingL1.v` | **2** | 0 | ✅ active — L1 judgment, modality-indexed |
-| `formal/Semantics_L1.v` | **26** | **3** | ✅ active — bullet-structure regressions + subst_typing_gen_l1_m + region_shrink_preserves_typing_l1_gen_m closed 2026-05-27; 3 residual outer `Admitted.` markers cover 5 internal `admit.` cases — all pre-existing L1 structural debt OR true parallel mirrors (T_Region_Active_*_L1_Echo shadowed sub-cases mirror T_Region_Active_L1's debt; the avoidable T_Region_L1_Echo mirror was closed in slice 4). Slice 4 added 3 new Qed: `preservation_l3_region_active_echo`, `preservation_l3_drop_echo`, `preservation_l3` (umbrella). Zero new admits. |
-| `formal/Modality.v` | **1** | 0 | ✅ active — L2 core, zero axioms |
-| `formal/Echo.v` | **12** | 0 | ✅ active — L3 calculus, not yet wired into L1 |
-| `formal/TypingL2.v` | (wrapper) | (wrapper) | ✅ thin re-indexing through `TypingL1.has_type_l1` |
-| `formal/L4.v` | (Definitions only) | 0 | ✅ active — L4 labelling discipline, no theorems (Phase A landed 2026-05-28) |
-| `src/abi/Ephapax/…` (Idris2) | n/a | n/a | ✅ active — ABI, Region linearity, no `believe_me` / `sorry` / `assert_total` |
-
-### Seam audit (slice 4, 2026-05-27): every admit/axiom classified
-
-Every `admit.` and `Admitted.` in `formal/*.v` after L3 slice 4
-landed. No new debt was introduced; the avoidable T_Region_L1_Echo
-mirror was closed. The remaining set is exactly the **pre-existing
-L1 structural debt** (with two true parallel mirrors that close
-when their originals close) plus the **sacrosanct legacy
-preservation** (provably false per `Counterexample.v`).
+| `formal/Semantics_L1.v` | **37+** | **3** | ✅ active — Phase 3b Stage 1a + 1b landed via PRs #252 + #253. 3 outer `Admitted.` markers cover 4 internal `admit.` cases. See seam audit below for current line numbers. |
+| `formal/Modality.v` | **1** | 0 | ✅ active — L2 core, zero axioms (`linear_to_affine`) |
+| `formal/Echo.v` | **12** | 0 | ✅ active — L3 calculus mechanised |
+| `formal/TypingL2.v` | **10** | 0 | ✅ active — `weaken_modality` (+ Affine_id + 3 `_le_*` variants), `preservation_l2_via_l1` (conditional on `preservation_l1`), `linear_value_retype_l1_m`, and 3 β-case lemmas (`preservation_l2_app_eff_beta_linear`, `_ground_nonlinear`, `_tfuneff` conditional on Stage 1b side conditions). NOT a wrapper. |
+| `formal/L4.v` | (Definitions only) | 0 | ✅ active — L4 labelling discipline (`PModeLinear` / `PModeAffine` / `PModeBoundaryMix` + `program_mode_to_modality` round-trip). No theorems. Phase A scaffold landed 2026-05-28. |
+| `src/abi/Ephapax/…` (Idris2) | n/a | (E1–E6 + compileOk = 7 `0`-quantity postulates) | ✅ active — ABI; postulates are explicit OWED-to-Coq forwards. See §1 Idris row below. |
+| `src/formal/Ephapax/…` (Idris2) | working | none | ✅ active — Region linearity, narrow no-escape proof; no `believe_me` / `sorry` / `assert_total` |
+
+### Seam audit (current 2026-06-01): every admit/axiom classified
+
+The current `admit.` / `Admitted.` set in `formal/*.v`. The remaining
+admits are exactly the **pre-existing L1 structural debt** (with one
+true parallel mirror that closes when its original closes) plus the
+**sacrosanct legacy preservation** (provably false per `Counterexample.v`).
 
 | Location | Class | Closes when |
 |---|---|---|
-| `Semantics_L1.v:553` (`admit.`) | **Pre-existing** L1 structural — `region_shrink_preserves_typing_l1_gen_m` / T_Region_Active_L1 shadowed sub-case; list-vs-multiset gap | L1 perm/multiset bridge OR `T_Region_*_L1` redesign |
-| `Semantics_L1.v:621` (`admit.`) | **Parallel mirror** of `:553` — T_Region_Active_L1_Echo shadowed sub-case; structurally identical | Same as `:553` (mechanical replay) |
-| `Semantics_L1.v:653` (`Admitted.`) | **Outer marker** — depends on internal `:553` + `:621` | When both internal admits close |
-| `Semantics_L1.v:1256` (`admit.`) | **Pre-existing** L1 structural — `region_liveness_at_split_l1_gen` / T_Region_Active_L1 `r = rv` sub-case; "GENUINELY FALSE" counterexample documented at site | L2 effect-typed `TFun` per `PRESERVATION-DESIGN.md §5.1` |
-| `Semantics_L1.v:1276` (`admit.`) | **Parallel mirror** of `:1256` — T_Region_Active_L1_Echo `r = rv` sub-case | Same as `:1256` (mechanical replay) |
-| `Semantics_L1.v:1290` (`Admitted.`) | **Outer marker** — depends on internal `:1256` + `:1276` | When both internal admits close |
-| `Semantics_L1.v:1694` (`admit.`) | **Pre-existing** — `preservation_l1` body; lambda-rigidity gap per `PRESERVATION-DESIGN.md §4.8` | L2 effect-typed `TFun` (Phase 2) |
-| `Semantics_L1.v:1695` (`Admitted.`) | **Outer marker** — depends on internal `:1694` | When `:1694` closes |
+| `Semantics_L1.v:576` (`admit.`) | **Pre-existing** L1 structural — `region_shrink_preserves_typing_l1_gen_m` / T_Region_Active_L1 shadowed sub-case; list-vs-multiset gap | L1 perm/multiset bridge OR `T_Region_*_L1` redesign (deferred to Phase D) |
+| `Semantics_L1.v:646` (`admit.`) | **Parallel mirror** of `:576` — T_Region_Active_L1_Echo shadowed sub-case; structurally identical | Same as `:576` (mechanical replay) |
+| `Semantics_L1.v:678` (`Admitted.`) | **Outer marker** — depends on internal `:576` + `:646` | When both internal admits close |
+| `Semantics_L1.v:1994` (`admit.`) | **Pre-existing** L1 structural — `region_liveness_at_split_l1_gen` / T_Region_Active_L1 `binder = rv` sub-case; **GENUINELY FALSE as stated** (single-case counterexample documented at site lines 1923-1926); current `Admitted.` is a transparency mark, not "almost done" | L2 effect-typed `TFun` per `PRESERVATION-DESIGN.md §5.1`; closure requires reformulation, not direct proof |
+| `Semantics_L1.v:2014` (`admit.`) | **Parallel mirror** of `:1994` — T_Region_Active_L1_Echo `binder = rv` sub-case; inherits same falsity | Same as `:1994` |
+| `Semantics_L1.v:2028` (`Admitted.`) | **Outer marker** — depends on internal `:1994` + `:2014` | When both internal admits close (i.e., never directly — only via reformulation) |
+| `Semantics_L1.v:3132` (`admit.`) | **Pre-existing** — `preservation_l1` body, covering S_StringConcat_Step2 + S_App_Step2 + S_Pair_Step2 cases; lambda-rigidity gap per `PRESERVATION-DESIGN.md §4.8` | Phase 3b Stages 2/3/4 (#240/#241/#242) — L2 effect-typed lambdas with `R_in/R_out` syntactic annotations |
+| `Semantics_L1.v:3133` (`Admitted.`) | **Outer marker** — depends on internal `:3132` | When `:3132` closes |
 | `Semantics.v:9257` (`Admitted.`) | **🛑 Sacrosanct** — legacy `Theorem preservation`, **provably false** per `Counterexample.v` (owner directive 2026-05-27) | Never. The `Admitted.` is correct. |
 
-No `Axiom` declarations in `formal/*.v`. Counterexample.v carries 5
-Qed; TypingL1.v / Modality.v / Echo.v / TypingL2.v are all
-admit-free.
+**Falsity audit** — two admits are not "unproven but true"; they are
+**provably false as stated**:
+
+1. `Semantics.v:9257` — refuted by `Counterexample.v`; sacrosanct.
+2. `Semantics_L1.v:1994` (and its mirror `:2014`) — refuted by single-case
+   counterexample `ERegion rv (EI32 5)` at `R=[rv]` documented in the
+   source at lines 1923-1926. Their `Admitted.` is a transparency mark
+   acknowledging the residual sub-case is false. Closure requires
+   reformulation at the L2 layer (lambda-rigidity gap), not a direct proof.
+
+No `Axiom` declarations in `formal/*.v`. `Counterexample.v` /
+`Counterexample_L2.v` / `Counterexample_L2_nested.v` carry 5 + 5 + 5
+Qed respectively; `TypingL1.v` / `Modality.v` / `Echo.v` / `TypingL2.v`
+are all `admit.`-free.
 
 ### Idris2 side (proof carriers, not Coq mechanisation)
 

README.adoc

@@ -750,14 +750,32 @@ Contributions welcome. Please see:
 
 The highest-leverage open work, in priority order:
 
-1. **Close `preservation` to Qed** (`formal/PRESERVATION-HANDOFF.md`)
-   — multi-day proof engineering, 22 goals remaining.
-2. **Fuel-refactor `Parse/Parser.idr`** from `%default covering` to
+1. **Phase 3b Stages 2 → 4** (issues #240/#241/#242) — `ELam` annotation
+   extension, CPS-form substitution, then compound non-linear values +
+   unconditional `preservation_l2`. The path forward; see
+   `formal/PRESERVATION-DESIGN.md §12.15` and `formal/PHASE-D-REDESIGN.md`.
+2. **Progress for L1** — state and prove `progress_l1` plus the L1
+   `canonical_*` lemmas (currently legacy-only at `Semantics.v:603-630`).
+   Combined with the conditional `preservation_l1`, this gives
+   conventional type-soundness in conditional form.
+3. **Fuel-refactor `Parse/Parser.idr`** from `%default covering` to
    `%default total`. Substantial — ~30 mutually-recursive combinators
    threaded through a `Stream` record.
-3. **Type-checker completion** (`ephapax-typing`) and **WASM codegen
+4. **Type-checker completion** (`ephapax-typing`) and **WASM codegen
    for lambda/app** (`ephapax-wasm`).
-4. **Native backend via Cranelift** (v0.2.0).
+5. **Native backend via Cranelift** (v0.2.0).
+
+[NOTE]
+====
+*Closing the legacy `Theorem preservation` in `formal/Semantics.v` is
+NOT a valid contribution.* That theorem is provably false (sealed by
+`formal/Counterexample.v`); its `Admitted.` is correct and durable per
+owner directive 2026-05-27. `formal/PRESERVATION-HANDOFF.md` is
+archaeology kept for context. The path forward is the per-layer
+preservation theorems (`preservation_l1`, `preservation_l2`,
+`preservation_l3`) on the redesigned judgment in `formal/Semantics_L1.v`.
+See `formal/PRESERVATION-DESIGN.md §12` and `PROOF-NEEDS.md §3`.
+====
 
 == Licence