diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc
index a13f16e..455775f 100644
--- a/docs/echo-types/MAP.adoc
+++ b/docs/echo-types/MAP.adoc
@@ -116,6 +116,11 @@ directory move is implied.
   shadows of selected Agda constructions. It is useful for examples,
   counterexample search, and executable intuition; it is not a proof
   repository and does not replace the Agda obligations.
+* *Autoformalisation fidelity (draft).* `docs/echos/` and
+  `proofs/agda/EchoFidelity.agda` sketch a fibre-accounting model of a
+  source-to-target translation step (what the checker sees versus what
+  an auditor sees). `[DRAFT]` — standalone, stdlib-only, unwired from
+  `All.agda` / `Smoke.agda`; no claim that fidelity is established.
 * *Separate language embodiment / consumer.* `Ephapax`
   (https://github.com/hyperpolymath/ephapax) is a distinct language
   project in which Echo Types are intended to become an embodied
diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc
index 2c9e031..bb6fb7a 100644
--- a/docs/echo-types/echo-kernel-note.adoc
+++ b/docs/echo-types/echo-kernel-note.adoc
@@ -225,6 +225,18 @@ kernel** — the boundary is real and lives outside this core.
   `proofs/agda/Echo/` (dotted submodules), so they are outside the
   flat `Echo*.agda` glob that Check B lints; recorded here for
   discoverability. Not kernel (the kernel remains exactly `Echo`).
+
+| *Standalone draft* +
+(stdlib only; outside the kernel cone)
+| `EchoFidelity`
+| Imports no in-repo module, not even `Echo`: its `Fibre` is a
+  hand-written Σ-type, so it is neither Tier 1 nor Tier 2. A small model
+  of an autoformalisation step as a fibre record (see
+  `docs/echos/`). `--safe --without-K`, no postulates, type-checks under
+  Agda 2.6.3 / stdlib 2.3, and is deliberately *not* wired into
+  `All.agda` / `Smoke.agda` until the maintainer asks. Listed here so the
+  classification-drift lint (kernel-guard check B) stays honest; it
+  carries no claim about the kernel.
 |===
 
 `EchoOrdinal` is Tier-1 off `Echo` but additionally pulls the
diff --git a/proofs/agda/EchoFidelity.agda b/proofs/agda/EchoFidelity.agda
index c6bd9b6..223c2db 100644
--- a/proofs/agda/EchoFidelity.agda
+++ b/proofs/agda/EchoFidelity.agda
@@ -1,11 +1,9 @@
 {-# OPTIONS --safe --without-K #-}
 -- SPDX-License-Identifier: MPL-2.0
 --
--- STATUS: DRAFT, NOT YET TYPE-CHECKED. Agda was not available in the
--- authoring environment. Before relying on this module, run
---   agda proofs/agda/EchoFidelity.agda
--- and fix any errors. It is deliberately NOT imported from All.agda or
--- Smoke.agda until it has been checked.
+-- STATUS: DRAFT. Type-checks under Agda 2.6.3 / agda-stdlib 2.3 (`--safe
+-- --without-K`, no postulates; checked 2026-10-19). Deliberately NOT imported
+-- from All.agda or Smoke.agda: it stays unwired until the maintainer asks.
 --
 -- Purpose: a small model of an autoformalisation step as a fibre record.
 -- Every source atom (hypothesis, constant, bound, conclusion) receives a