diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml
index 4b44e4b..7d2148d 100644
--- a/0-AI-MANIFEST.a2ml
+++ b/0-AI-MANIFEST.a2ml
@@ -23,7 +23,7 @@ These 6 A2ML files MUST exist in `.machine_readable/6a2/` directory ONLY:
 
 ## CORE INVARIANTS
 
-1. **Formal Proof Integrity** - No `Admitted` in Coq or `believe_me`/`assert_total` in Idris2. All proofs MUST remain closed (67/67 Qed).
+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.
 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>".