@@ -119,8 +119,9 @@ directory move is implied.
 * *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.
+  an auditor sees); its `Fibre` is `Echo (account T) (mapped t)`.
+  `[DRAFT]` — Tier-1 derived, type-checked, 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
 
@@ -65,7 +65,7 @@ kernel** — the boundary is real and lives outside this core.
   `EchoFiberBridge`, `EchoFiberCount`, `EchoFiberTriangulation`,
   `EchoIndexed`, `EchoRelational`, `EchoTruncation`,
   `EchoJanusBridge`, `EchoTropical`, `EchoSeparating`,
-  `EchoTotalCompletion`, `EchoDisplayed`
+  `EchoTotalCompletion`, `EchoDisplayed`, `EchoFidelity`
 | One hop off the kernel. `EchoJanusBridge`/`EchoTropical` are
   *Directions* (see MAP). `EchoFiberTriangulation` is the external
   stdlib triangulation hardening item. `EchoSeparating` carries
@@ -75,6 +75,10 @@ kernel** — the boundary is real and lives outside this core.
   displayed-type / `DispHom` / `fromHomOver` fibration packaging of
   the categorical base (faithful mirror of typed-wasm's Idris
   `Echo.idr`; no variance / graded-comonad claim, per R-2026-05-18).
+  `EchoFidelity` models an autoformalisation step as a fibre record whose
+  `Fibre` is literally `Echo (account T) (mapped t)`; it is `[DRAFT]` and
+  deliberately unwired from `All.agda` / `Smoke.agda` until the maintainer
+  asks (see `docs/echos/`).
 
 | *Derived — Tier 2* +
 (depend on Tier-1 `Echo*`)
@@ -225,18 +229,6 @@ 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
 
@@ -15,7 +15,7 @@ Context you must read first:
 
 * `docs/echos/README.adoc` (scope, status, ground truth)
 * `docs/echos/FIDELITY-FIBRE-DESIGN.adoc` (design and what is not claimed)
-* `proofs/agda/EchoFidelity.agda` (draft model, NOT yet type-checked)
+* `proofs/agda/EchoFidelity.agda` (draft model; type-checked under Agda 2.6.3 / stdlib 2.3 on 2026-10-19)
 * `proofs/agda/EchoEpistemic.agda` (existing knowledge/observation model)
 * `docs/CLAIMS_AUDIT.adoc` (how this repo audits its own claims)
 
 
@@ -15,7 +15,8 @@ Verdict TA = mapped t | dropped reason
 ----
 
 The fibre of a target atom `t` is the set of source atoms whose verdict is
-`mapped t`. This is the echo-type reading: `Fibre t = Σ s. account s ≡ mapped t`.
+`mapped t`. This is the echo-type reading: `Fibre t = Σ s. account s ≡ mapped t`, which
+`EchoFidelity.agda` now states as `Echo (account T) (mapped t)` itself.
 
 == What the types buy
 
 
@@ -22,7 +22,7 @@ ____
 |===
 |Item |Status |Where
 
-|Fibre accounting model (Agda) |DRAFT, unverified |`proofs/agda/EchoFidelity.agda`
+|Fibre accounting model (Agda) |Type-checked (Agda 2.6.3, stdlib 2.3); `Fibre` is `Echo`; still a draft |`proofs/agda/EchoFidelity.agda`
 |Design note (what fibres do and do not give) |Draft |`FIDELITY-FIBRE-DESIGN.adoc`
 |Investigation brief for a repo-tied bot |Ready to use |`BOT-PROMPT.adoc`
 |Wired into `All.agda` / `Smoke.agda` |No |Deliberately not wired until checked
 
@@ -1,26 +1,31 @@
 {-# 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: type-checks under Agda 2.6.3 / agda-stdlib 2.3 (`--safe
+-- --without-K`, no postulates). Deliberately NOT imported from All.agda or
+-- Smoke.agda: it stays unwired until the maintainer asks for that.
 --
 -- Purpose: a small model of an autoformalisation step as a fibre record.
 -- Every source atom (hypothesis, constant, bound, conclusion) receives a
 -- verdict: mapped to a target atom, or dropped with a recorded reason.
 -- The types enforce that nothing is silently lost. They do NOT establish
 -- semantic fidelity; see docs/echos/FIDELITY-FIBRE-DESIGN.adoc.
+--
+-- The fibre of a target atom IS an `Echo` of the accounting map: `Fibre`
+-- below is `Echo (account T) (mapped t)` by definition, so the structure
+-- theory of Echo (EchoKernel contract, `map-over`, ...) applies to it
+-- unchanged. This makes the module a Tier-1 derived module (only `Echo` +
+-- stdlib).
 
 module EchoFidelity where
 
 open import Agda.Builtin.String using (String)
 open import Data.Empty using (⊥)
+open import Echo using (Echo; echo-intro)
 open import Data.List.Base using (List)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product.Base using (Σ; _,_)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
 
 ------------------------------------------------------------------------
 -- Verdicts for a single source atom.
@@ -46,12 +51,45 @@ open Translation public
 
 ------------------------------------------------------------------------
 -- Fibres: the source atoms that a given target atom traces back to.
--- A fibre is a Σ-type of source atoms together with a proof that the
--- source atom is mapped to that target atom.
+-- A fibre is the Echo of the accounting map at the verdict `mapped t`:
+-- a source atom together with a proof that it is mapped to that target.
 ------------------------------------------------------------------------
 
 Fibre : {SA TA : Set} → Translation SA TA → TA → Set
-Fibre T t = Σ _ (λ s → account T s ≡ mapped t)
+Fibre T t = Echo (account T) (mapped t)
+
+-- The identification with Echo is definitional, so the structure theory of
+-- Echo applies to fibres with no transport.
+fibre-is-echo :
+  {SA TA : Set} (T : Translation SA TA) (t : TA) →
+  Fibre T t ≡ Echo (account T) (mapped t)
+fibre-is-echo T t = refl
+
+-- A source atom that the account maps to t lies in the fibre of t.
+mapped-in-fibre :
+  {SA TA : Set} (T : Translation SA TA) (s : SA) (t : TA) →
+  account T s ≡ mapped t → Fibre T t
+mapped-in-fibre T s t p = s , p
+
+-- Every source atom lies in the fibre of the verdict it received, when that
+-- verdict is a mapping (`echo-intro` at the accounting map).
+fibre-of-image :
+  {SA TA : Set} (T : Translation SA TA) (s : SA) (t : TA) →
+  account T s ≡ mapped t → Echo (account T) (account T s)
+fibre-of-image T s t _ = echo-intro (account T) s
+
+-- A dropped atom is in no fibre: the two verdicts are different
+-- constructors. This is the "dropped means recorded, not hidden" half of
+-- the accounting: an atom with a drop reason cannot also be claimed as the
+-- source of a target atom.
+dropped-not-mapped :
+  {TA : Set} {r : String} {t : TA} → dropped r ≡ mapped t → ⊥
+dropped-not-mapped ()
+
+dropped-not-in-fibre :
+  {SA TA : Set} (T : Translation SA TA) (s : SA) (r : String) →
+  account T s ≡ dropped r → (t : TA) → account T s ≡ mapped t → ⊥
+dropped-not-in-fibre T s r d t p = dropped-not-mapped (trans (sym d) p)
 
 -- A target atom with an empty fibre has no source: it is fabricated
 -- relative to this step. Stated here as the definition of "fabricated";