diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc
index 857e345..e84287e 100644
--- a/docs/echo-types/echo-kernel-note.adoc
+++ b/docs/echo-types/echo-kernel-note.adoc
@@ -148,22 +148,15 @@ kernel** — the boundary is real and lives outside this core.
   module. Listed so the DAG audit is complete.
 
 | *Exploratory (not in `All.agda`)*
-| `EchoDecorationBridge`, `EchoImageFactorizationPropPostulated`
+| `EchoDecorationBridge`
 | Deliberately omitted from `proofs/agda/All.agda` so the verified
-  suite is unaffected. `EchoDecorationBridge` re-issues
-  `EchoIntegration`'s integration claim through a `DecorationFit`
-  record; exploratory per `roadmap.adoc` § R5 and
+  suite is unaffected. Re-issues `EchoIntegration`'s integration
+  claim through a `DecorationFit` record. Listed here only to
+  satisfy the classification-drift lint
+  (`scripts/kernel-guard.sh` Check B); the module itself is
+  exploratory per `roadmap.adoc` § R5 and
   `docs/echo-types/explorations/decoration-bridge/README.adoc`.
-  `EchoImageFactorizationPropPostulated` is the postulated-
-  truncation-interface consumer for `EchoImageFactorizationProp`
-  (flag profile `--without-K` only, no `--safe`, because
-  `postulate` is forbidden under `--safe`) — demonstrates the
-  parametric `TruncInterface` slot is plug-in-usable; the
-  postulates assert the standard (-1)-truncation laws without
-  proving them.  Both modules listed here to satisfy the
-  classification-drift lint (`scripts/kernel-guard.sh` Check B);
-  neither is kernel, neither load-bearing, both subject to
-  abandonment.
+  Not kernel, not load-bearing, subject to abandonment.
 |===
 
 `EchoOrdinal` is Tier-1 off `Echo` but additionally pulls the
diff --git a/proofs/agda/EchoImageFactorizationPropPostulated.agda b/proofs/agda/EchoImageFactorizationPropPostulated.agda
deleted file mode 100644
index 90f8dab..0000000
--- a/proofs/agda/EchoImageFactorizationPropPostulated.agda
+++ /dev/null
@@ -1,167 +0,0 @@
-{-# OPTIONS --without-K #-}
-
--- Postulated-truncation consumer for `EchoImageFactorizationProp`.
---
--- ## Purpose
---
--- `EchoImageFactorizationProp` is module-parameterised in a
--- `TruncInterface`, deliberately scoped to ship the (epi, mono)
--- factorisation content WITHOUT committing to any particular
--- implementation of propositional truncation.  The base module
--- itself is `--safe --without-K` with zero postulates; the
--- propositional-truncation OBLIGATION is bumped to the consumer.
---
--- This module demonstrates the parameter is USABLE by exhibiting a
--- concrete `TruncInterface ℓ` instance built from four postulates
--- matching the four interface fields, then opens
--- `ImageProp T f` to confirm the parametric content goes through
--- on a concrete consumer.
---
--- ## Honest scope
---
--- This is a POSTULATED-INTERFACE demonstration, NOT a HIT
--- construction.  The postulates assert that propositional
--- truncation exists and satisfies its standard laws — they do not
--- prove the existence; they assume it.
---
--- The classification consequence:
---
---   * The flag profile is `--without-K` only (no `--safe`),
---     because `--safe` forbids `postulate` entirely.  This module
---     therefore lives OUTSIDE the kernel cone and outside
---     `proofs/agda/All.agda` (per the existing
---     `EchoDecorationBridge` Exploratory precedent in
---     `docs/echo-types/echo-kernel-note.adoc`).
---   * Classification: Exploratory.  Listed in the note to satisfy
---     `scripts/kernel-guard.sh` Check B (classification-drift
---     lint), not load-bearing.
---   * The base `EchoImageFactorizationProp` remains kernel-cone
---     compatible (`--safe --without-K`, zero postulates) and is
---     the load-bearing artefact.
---
--- ## What this module ships
---
---   * Four `postulate` declarations realising the
---     `TruncInterface ℓ` record fields.
---   * `trunc : TruncInterface ℓ` — the packaged interface.
---   * `module ImagePropPostulated f` re-opening
---     `EchoImageFactorizationProp.ImageProp trunc f` for any
---     `f : A → B` at the chosen levels.
---   * `prop-factor-right-injective-demo` — a pinned re-export of
---     the mono-side theorem from the parametric content,
---     specialised to the postulated interface.
---   * `prop-factor-left-mere-surjective-demo` — same for the
---     epi-side.
---
--- ## What this module deliberately DOES NOT prove
---
---   * That the postulated `Trunc` IS the standard (-1)-truncation.
---     It satisfies the interface laws by assumption; that is all
---     the parametric proofs in `ImageProp` need.
---   * Anything about the postulates' consistency.  The standard
---     HoTT discipline says the four laws together characterise
---     `Trunc A` up to equivalence (and Cubical Agda or a hand-
---     rolled HIT realises them concretely); we cite that
---     literature rather than mechanise it.
---
--- The mechanical contribution: pin that the parameterised
--- `EchoImageFactorizationProp.ImageProp` module can be CONSUMED
--- via interface plug-in.  The demonstrative side-effect is a
--- visible auditable check that the base module's parameter slots
--- match a real `TruncInterface ℓ` shape.
---
--- ## Headlines (this module's contribution)
---
---   * `trunc`                                    — the packaged interface
---   * `prop-factor-right-injective-demo`         — mono side, plugged
---   * `prop-factor-left-mere-surjective-demo`    — epi side, plugged
-
-module EchoImageFactorizationPropPostulated where
-
-open import EchoImageFactorizationProp using (TruncInterface; module ImageProp)
-open import Echo                       using (Echo)
-
-open import Level                   using (Level; suc)
-open import Data.Product.Base       using (Σ; _,_)
-open import Relation.Binary.PropositionalEquality
-                                    using (_≡_)
-
-private variable
-  ℓ : Level
-
-----------------------------------------------------------------------
--- Postulated truncation interface
-----------------------------------------------------------------------
-
--- The four standard propositional-truncation obligations.  Cubical
--- Agda or a hand-rolled HIT realises these concretely; here we take
--- them as assumed.
-
-postulate
-  Trunc-pos    : Set ℓ → Set ℓ
-  ∣_∣-pos      : ∀ {A : Set ℓ} → A → Trunc-pos A
-  is-prop-pos  : ∀ {A : Set ℓ} (x y : Trunc-pos A) → x ≡ y
-  rec-pos      : ∀ {A B : Set ℓ}
-                 → ((x y : B) → x ≡ y)
-                 → (A → B)
-                 → Trunc-pos A → B
-
-----------------------------------------------------------------------
--- Packaged `TruncInterface ℓ` from the postulates
-----------------------------------------------------------------------
-
--- Repackage the four postulates as the `TruncInterface ℓ` record
--- consumed by `EchoImageFactorizationProp.module ImageProp`.
-
-trunc : TruncInterface ℓ
-trunc = record
-  { Trunc   = Trunc-pos
-  ; ∣_∣     = ∣_∣-pos
-  ; is-prop = is-prop-pos
-  ; rec     = rec-pos
-  }
-
-----------------------------------------------------------------------
--- Consumer demonstration: open `ImageProp trunc f` and re-export
-----------------------------------------------------------------------
-
--- Both `A` and `B` need to live at the SAME level `ℓ` per
--- `ImageProp`'s implicit-equal-level signature.  Same-level is the
--- common Σ-product case in practice; cross-level consumers would
--- need to lift to a common level (`Level.Lift`).
-
-module ImagePropPostulated {A B : Set ℓ} (f : A → B) where
-  -- Open the parametric module with the postulated interface
-  -- plugged in.  Every name inside `ImageProp` is now available
-  -- under this module's namespace.
-  open ImageProp trunc f public
-
-----------------------------------------------------------------------
--- Demonstrative pinned exports
-----------------------------------------------------------------------
-
--- Headline 1 — MONO side, plugged.  Pin the mono-side theorem at
--- the postulated-interface specialisation.  This confirms the
--- parametric content goes through under interface plug-in (the
--- proof type-checks at the concrete instance).
-
-prop-factor-right-injective-demo :
-  ∀ {A B : Set ℓ} (f : A → B)
-    {z₁ z₂ : Σ B (λ y → Trunc-pos (Echo f y))}
-  → ImagePropPostulated.prop-factor-right f z₁
-    ≡
-    ImagePropPostulated.prop-factor-right f z₂
-  → z₁ ≡ z₂
-prop-factor-right-injective-demo f =
-  ImagePropPostulated.prop-factor-right-injective f
-
--- Headline 2 — EPI side, plugged.  Pin the epi-side theorem at the
--- postulated-interface specialisation.  The truncated existence is
--- exactly the standard (-1)-truncated surjectivity.
-
-prop-factor-left-mere-surjective-demo :
-  ∀ {A B : Set ℓ} (f : A → B)
-    (z : Σ B (λ y → Trunc-pos (Echo f y)))
-  → Trunc-pos (Σ A λ a → ImagePropPostulated.prop-factor-left f a ≡ z)
-prop-factor-left-mere-surjective-demo f =
-  ImagePropPostulated.prop-factor-left-mere-surjective f