diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc
index d799087..bb8d11c 100644
--- a/docs/echo-types/echo-kernel-note.adoc
+++ b/docs/echo-types/echo-kernel-note.adoc
@@ -117,6 +117,17 @@ kernel** — the boundary is real and lives outside this core.
 | `EchoApprox`, `EchoApproxInstance`
 | Does **not** `import Echo`; a parallel stdlib-only approximation
   module. Listed so the DAG audit is complete.
+
+| *Exploratory (not in `All.agda`)*
+| `EchoDecorationBridge`
+| Deliberately omitted from `proofs/agda/All.agda` so the verified
+  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`.
+  Not kernel, not load-bearing, subject to abandonment.
 |===
 
 `EchoOrdinal` is Tier-1 off `Echo` but additionally pulls the
diff --git a/docs/echo-types/explorations/decoration-bridge/01-decoration-instances.adoc b/docs/echo-types/explorations/decoration-bridge/01-decoration-instances.adoc
new file mode 100644
index 0000000..5c58415
--- /dev/null
+++ b/docs/echo-types/explorations/decoration-bridge/01-decoration-instances.adoc
@@ -0,0 +1,264 @@
+= Decoration bridge — candidate instance sketches
+:toc: macro
+:toclevels: 2
+:sectnums:
+:sectnumlevels: 2
+:icons: font
+:source-highlighter: rouge
+
+[CAUTION]
+====
+Exploratory pseudocode.  Not committed Agda.  Each candidate is an
+*analogy that may or may not fit* the `Choreo × Graded` shape that
+`EchoIntegration` integrates, with an explicit falsifier.  Failure to
+fit retires the candidate; success commits nothing beyond the
+candidate itself.  See `README.adoc` § "Scope discipline".
+====
+
+toc::[]
+
+== Reading these sketches
+
+Each candidate names: (a) the *external construction* it draws on,
+(b) the *fit shape* — what would need to be supplied to discharge the
+`DecorationFit` record from `proofs/agda/EchoDecorationBridge.agda`,
+(c) one or two pseudo-Agda lines showing the would-be predicate /
+stability witness / knowledge witness, and (d) the *falsifier* — the
+concrete condition under which the analogy collapses and the
+candidate is retired.
+
+The pseudocode is illustrative.  It uses the names from
+`EchoChoreo` (`Role`, `Client`, `Server`, `Global`,
+`scramble-server`, `client-stability`), `EchoEpistemic` (`Knows`),
+and `EchoGraded` (`keep`, `residue`, `keep≤residue`, `degrade`).
+No file in this directory is intended to typecheck as-is.
+
+== Candidate A — CRDT join semilattices
+
+*External construction.*  A replicated value held at two replicas
+(`Client` and `Server`); each replica maintains a local update log.
+A merge operation combines logs into a joined state.
+
+*Fit shape.*
+
+* `Pred` names the invariant "the client's locally-observed value is
+  `b : Bool`".  Local observation is preserved across the merge step
+  whenever the merge is observation-preserving from the client's
+  side — which is precisely the `scramble-client-square` shape
+  `EchoChoreo` already pins.
+* `Pred-stable` is the witness that the merge step does not change
+  the client-side observation.  In CRDT terms, this is *the
+  client-side projection of the merge is a no-op on the merged
+  bit*.  For a state-based CRDT whose merge is the lattice join,
+  this is the *join-idempotence* property restricted to the
+  client-observable component.
+* `knowledge` is the proof that every client-side preimage of a
+  given visible value satisfies `Pred`.  For a Boolean-bit CRDT,
+  this is exhaustion over the two-element preimage.
+
+*Pseudocode.*
+
+[source,agda]
+----
+-- pseudocode; not committed
+PredA : Global → Set
+PredA (cBit , _) = cBit ≡ true   -- "client observes true"
+
+stableA : ∀ g → PredA g → PredA (scramble-server g)
+stableA (true , _) refl = refl    -- merge does not touch cBit
+
+knowledgeA : Knows Client PredA true
+knowledgeA ((true , _) , refl) = refl
+----
+
+*Falsifier.*  If the CRDT's merge is genuinely commutative — i.e.
+*both* `Pred-stable` and a hypothetical `Pred-stable-reverse` hold
+under a symmetric `scramble-client` and `scramble-server` — then no
+residue survives composition, and the analogy fits but says nothing
+the CRDT's own commutativity proof did not already say.  This is the
+candidate's *commutative-merge collapse*: the bridge characterises a
+property the system already has by design, not a phenomenon worth
+naming.  Retire if the target CRDT's merge is uniformly commutative
+on the observable.
+
+*Why this is not generic Σ.*  The fit *requires* the stability
+witness to mention `scramble-server` — a specific update on `Global`,
+not a generic Σ-projection.  A `Σ`-only encoding would have no way to
+name the merge step; it would have to project to the visible bit and
+discard the structure that makes `Pred-stable` mean anything.
+
+== Candidate B — Local-first causal histories
+
+*External construction.*  A document is edited by the client; the
+server periodically reconciles.  The document state carries
+`(cBit, sBit)`: `cBit` is the client's last committed edit, `sBit` is
+the server's reconciled view.  A reconciliation step is the
+`scramble-server` analogue: it may update `sBit` without changing
+`cBit`.
+
+*Fit shape.*
+
+* `Pred` names the invariant "the client's edit history reaches a
+  state where `cBit ≡ true`".  Causal-history depth is bounded by
+  the client's edit count.
+* `Pred-stable` is the witness that reconciliation does not rewrite
+  client history.  This is the *no-server-side-rewrite* property
+  local-first systems offer by design.
+* `knowledge` is the proof that any client-observable witness
+  (a state with `cBit ≡ true`) lies in the predicate.
+
+*Pseudocode.*
+
+[source,agda]
+----
+-- pseudocode; not committed
+PredB : Global → Set
+PredB (cBit , _) = cBit ≡ true   -- "client history reached true"
+
+stableB : ∀ g → PredB g → PredB (scramble-server g)
+stableB (true , _) refl = refl    -- reconciliation does not rewrite cBit
+
+knowledgeB : Knows Client PredB true
+knowledgeB ((true , _) , refl) = refl
+----
+
+*Falsifier.*  If the local-first system already maintains a complete
+causal-history record on every document state (vector clocks, OT
+metadata, full event-log), then the residue the bridge names is
+*already captured* in the system's own provenance metadata.  The
+analogy fits but is redundant: the bridge says nothing the system
+did not already say.  This is the candidate's *metadata-already-complete*
+failure mode.  Retire if the target system's provenance metadata
+fully reconstructs the residue.
+
+*Why this is not generic Σ.*  Same reason as Candidate A — the
+stability witness has to mention `scramble-server` specifically.  But
+there is a second reason: the `Knows Client P y` predicate is
+fundamentally about *what every preimage satisfies*, which is a
+universal quantification a `Σ`-only encoding would have to write out
+explicitly.  The bridge inherits the universal quantification from
+`EchoEpistemic.Knows`.
+
+== Candidate C — Gossip partial views
+
+*External construction.*  A node maintains a partial view of the
+cluster membership; gossip messages refresh the view.  Local
+observation is the *fresh-or-stale bit* of the node's own view;
+remote-side updates may change which peer a node is observing
+without changing the freshness bit.
+
+*Fit shape.*
+
+* `Pred` names the invariant "the node's view of its own freshness
+  bit is `true`".
+* `Pred-stable` is the witness that a remote-view refresh
+  (`scramble-server`-analogue) does not change the local freshness
+  bit.  This is the *view-update-locality* property gossip protocols
+  guarantee.
+* `knowledge` is the proof that any local-observable witness lies in
+  the predicate.
+
+*Pseudocode.*
+
+[source,agda]
+----
+-- pseudocode; not committed
+PredC : Global → Set
+PredC (cBit , _) = cBit ≡ true   -- "local freshness bit is true"
+
+stableC : ∀ g → PredC g → PredC (scramble-server g)
+stableC (true , _) refl = refl    -- view refresh does not touch cBit
+
+knowledgeC : Knows Client PredC true
+knowledgeC ((true , _) , refl) = refl
+----
+
+*Falsifier.*  Most gossip protocols are designed to be
+*view-oblivious*: the node accepts any refresh that arrives without
+caring which peer sent it.  If view-obliviousness is the design
+intent, the residue the bridge would name is *intentionally
+discarded* — the protocol is built precisely to erase that residue.
+The bridge characterises a property the protocol does not have and
+does not want.  Retire if the target protocol's design discards
+peer-provenance on refresh.
+
+*Why this is not generic Σ.*  Same as Candidates A and B.
+
+== The shared pseudocode shape (and why it matters)
+
+All three candidates instantiate the same record:
+
+[source,agda]
+----
+-- pseudocode; the actual record is in proofs/agda/EchoDecorationBridge.agda
+record DecorationFit (y : Bool) : Set₁ where
+  field
+    Pred        : Global → Set
+    Pred-stable : ∀ g → Pred g → Pred (scramble-server g)
+    knowledge   : Knows Client Pred y
+----
+
+That every candidate shares the same record is the bridge's *only*
+positive content — the claim that "decorations on shared state
+evolution" is a structural pattern that admits a uniform fit shape.
+If two candidates need genuinely different records to express their
+fit, the bridge's positive content collapses and the exploration
+loses its motivation.
+
+[NOTE]
+====
+"Same record" is not "same instance".  The three candidates above all
+discharge `DecorationFit` with the same `Pred` (`λ (cBit , _) → cBit
+≡ true`) and the same trivial proofs.  That is because they are
+pseudocode sketches over the same toy `Global = Bool × Bool`.  Real
+candidates would differ in their `Pred` (CRDT lattice element vs
+causal-history segment vs view-freshness predicate), their stability
+witness (idempotent join vs server-side-rewrite-freedom vs
+view-update-locality), and the `Global` carrier they project from.
+The toy version is what types under the actual
+`EchoChoreo.Global = Bool × Bool`.  Promoting any candidate to a real
+discharge is a rung-consolidation, with its own forbidden-rebrandings
+audit.
+====
+
+== Falsifier summary
+
+The three falsifiers above are *distinct*.  None subsumes another.
+The bridge's exploratory value is in the cases where *exactly one*
+candidate fits — that is, the case is non-commutative enough to have
+a residue (rules out A's commutative collapse), the system does not
+already track that residue (rules out B's metadata-already-complete
+collapse), and the system does not want to discard the residue
+(rules out C's view-obliviousness collapse).  If no domain
+construction simultaneously falsifies all three, the bridge has no
+useful target and retires.
+
+== What an actual fit would need
+
+Promoting any candidate from sketch to discharged instance would
+require:
+
+. A concrete `Global` carrier richer than `Bool × Bool`.  The
+  `Choreo × Graded` shape `EchoIntegration` integrates is fixed to
+  `Bool × Bool` for the obvious reason of toy-size; a real candidate
+  needs a domain-appropriate carrier, and the bridge then has to
+  exhibit role-projections (`obs Client`, `obs Server`) that respect
+  the domain's natural observation interface.
+. A real predicate stability proof — not a one-line `refl` over
+  exhaustion, but a structural argument that the
+  `scramble-server`-analogue update preserves the candidate's
+  `Pred`.  This is where the real content lives, and where most
+  candidates will fail.
+. A real `Knows` witness, which means a real `Echo` over the
+  domain's observation map — not the toy
+  `obs Client (cBit , _) = cBit`.
+. A real-domain falsifier check: the analogy must demonstrably
+  *fail* in some natural instance of the candidate's domain, not
+  just in pathological edge cases.  A candidate that fits every
+  instance is suspicious and almost certainly trips
+  "the recipe is uniformly applicable" in the
+  forbidden-rebrandings register.
+
+Any session attempting such a promotion should consult
+`README.adoc` § "Termination criteria" first; promotion is *not*
+pre-authorised.
diff --git a/docs/echo-types/explorations/decoration-bridge/02-non-commuting-residue.adoc b/docs/echo-types/explorations/decoration-bridge/02-non-commuting-residue.adoc
new file mode 100644
index 0000000..ae24cc2
--- /dev/null
+++ b/docs/echo-types/explorations/decoration-bridge/02-non-commuting-residue.adoc
@@ -0,0 +1,192 @@
+= Decoration bridge — non-commuting residue
+:toc: macro
+:toclevels: 2
+:sectnums:
+:sectnumlevels: 2
+:icons: font
+
+[CAUTION]
+====
+Conceptual core, not a theorem.  Asks: when two decorations on a
+shared state evolution do not commute, what characterises the
+residue, and why is this not generic `Σ` + `≡`?  Stays scoped to the
+`Choreo × Graded` axis pair `EchoIntegration` integrates.  See
+`README.adoc` § "Scope discipline".
+====
+
+toc::[]
+
+== The question
+
+Suppose `s : Global → Global` and `t : Global → Global` are two
+state-update steps representing two different *decorations* — one a
+role-projection-respecting update (say, `scramble-server` from
+`EchoChoreo`), one a graded degradation (say, the
+`degrade keep≤residue` map's underlying state action).  Two
+compositions are possible: `s ∘ t` or `t ∘ s`.  When `s ∘ t ≡ t ∘ s`
+holds extensionally, the decorations *commute* and the order of
+application does not matter.  When it does not, *something is
+recorded* by the fact of taking one order rather than the other.
+
+The bridge's exploratory question is: in the `Choreo × Graded` axis
+pair, *what* is recorded, and *where* does it live?
+
+== The known facts (carried in from `EchoIntegration`)
+
+The integration claim
+`knowledge-and-controlled-degradation` (re-issued by the bridge as
+`decoration-claim`) packages two facts about the `Choreo × Graded`
+pair:
+
+. *Knowledge preservation along the choreography step.*  If `P`
+  holds on every preimage of `y` under `obs Client`, and `P` is
+  preserved by `scramble-server`, then `P` continues to hold after
+  the choreography step (`client-stability`).  In symbols:
+  `Knows Client P y` implies `∀ e → P (proj₁ (client-stability e))`.
+. *Merge at the residue grade.*  The two witnesses `echo-true` and
+  `echo-false`, which are *distinct* at grade `keep`
+  (`echo-true ≢ echo-false`), become *definitionally equal* after
+  `degrade keep≤residue`.  This is `merged-at-residue`, and its
+  proof is `refl` once `keep≤residue` has been applied.
+
+These two facts live on *independent* surfaces of the integration
+claim.  Fact 1 is purely choreographic; fact 2 is purely graded.
+The integration claim is the conjunction — a product, not a
+non-trivial interaction (as EI-2 established, and as
+`docs/gate-2-handoff.adoc` / `IntegrationAudit.agda` separately
+exhibits).
+
+== Where the residue could live
+
+If the two decorations did *interact* — if the order of application
+made an observable difference — the residue would have to live in
+one of three places:
+
+. *In the visible value `y`.*  If applying `scramble-server` then
+  `degrade` produced a different visible bit from applying `degrade`
+  then `scramble-server`, the residue would be the witnessing
+  inequality.  *This is not the case.*  Both decorations are
+  observation-preserving on the client-side projection — that is
+  the definitional property each was set up to have.  Composition
+  in either order leaves the client-side visible bit unchanged.
+. *In the preimage `x : Global`.*  If applying the two decorations
+  in either order produced different `x`-values that still mapped to
+  the same `y`, the residue would be the preimage difference.
+  *This is the residue the bridge cares about, if it exists.*
+. *In the equality proof `f x ≡ y`.*  If the equality proof itself
+  carried different content — different choices of `cong`-paths,
+  say — the residue would be witnessed by the proof asymmetry.
+  *This is not the case under `--without-K`.*  All proofs of
+  `f x ≡ y` are equal (up to the propositional discipline this
+  project respects), so the equality leg cannot carry residue.
+
+Item 2 is the only place the residue can be.  This is *not* a
+contingent fact about the toy `Global = Bool × Bool`; it is the
+structural shape of `Echo f y = Σ A (f x ≡ y)` together with
+`--safe --without-K`.  The equality leg is forced; the visible value
+is preserved by hypothesis; so the only space for a meaningful
+residue is the witness `x`.
+
+== What this gives that generic `Σ` does not
+
+A bare `Σ A (λ x → f x ≡ y)` lets the consumer extract `x` via
+`proj₁` at will.  No information about how `x` was constructed is
+retained — the act of taking `proj₁` is the act of forgetting
+provenance.  The bridge's framing is the *opposite*: the consumer is
+asked to commit, before extracting, to a *decoration discipline* —
+the role projection and the graded order — under which extraction is
+either constrained (at `keep`) or impossible to disambiguate (at
+`residue`).
+
+In particular, four properties the bridge inherits from the
+integration claim do *not* hold for generic `Σ`:
+
+. *Monotone reindexing along a thin poset.*  `Σ` has no built-in
+  notion of "this witness is the same one, just less precisely
+  named".  `degrade : g1 ≤g g2 → GEcho g1 → GEcho g2` provides
+  exactly that, and the bridge consumes it.  A `Σ`-only
+  reconstruction would need to invent a degradation order, prove it
+  propositional, and re-discover `≤g-prop` — at which point the
+  reconstruction is no longer `Σ`-only.
+. *Definitional collapse at the residue grade.*  `merged-at-residue`
+  is `refl`.  Two distinct witnesses produce identical residues, by
+  computation, not by an extensional argument.  A `Σ`-only
+  encoding would have to *prove* the equality post-hoc, and the
+  proof would not be `refl`.
+. *Role-projection transport along a commuting square.*
+  `client-stability = map-square (obs Client) (obs Client)
+  scramble-server id scramble-client-square` — a structural
+  property of the `obs Client`-fibre, not a property of the
+  witness `x` alone.  Generic `Σ` has no notion of "transport along
+  a square"; the witness-transport leg `scramble-server` would have
+  to be threaded through every consumer manually.
+. *The no-section dual.*
+  `no-recovery-after-residue-degrade` (cited transitively through
+  the integration claim) is the constructive proof that the
+  degradation has no left-inverse.  `Σ` has no such asymmetry —
+  `proj₁` is always a valid (set-theoretic) extraction; the
+  no-section dual is the proof-relevant statement that *no
+  function* can recover the original witness, not just that the
+  current consumer chose not to extract it.
+
+The bridge depends on (1) and (3) substantively.  (2) is the
+canonical "this is what the residue *is*" witness; the bridge's
+`decoration-claim` re-issues it directly.  (4) is structural
+inheritance that the bridge does not currently exercise in code but
+relies on for the *meaning* of the residue characterisation.
+
+== What this does *not* give
+
+The bridge does not give:
+
+* a *uniqueness* statement about the residue.  There is no claim
+  that the witness `x` is the *unique* element of `Global` satisfying
+  both decorations' constraints; only that the `Echo`-discipline
+  retains *something* — the asymmetry between `keep` and `residue`
+  — that bare `Σ` does not.  Uniqueness language would trip
+  retraction-watch (Pillar B narrowing — pointwise, not full UP).
+* a *generalisation* over decoration pairs.  The framing is
+  `Choreo × Graded` only; cf. forbidden-rebrandings entry "the recipe
+  is uniformly applicable across all 2D axis pairs".
+* a *categorical* characterisation.  The residue is a witness in a
+  type, not a limit of a diagram.  Categorical language would trip
+  retraction-watch (Pillar B again; also the "graded comonad"
+  narrowing).
+* a *quantitative* statement about residue size or content.  The
+  residue is identified up to definitional equality at the residue
+  grade; how much information was *lost* in moving from `keep` to
+  `residue` is a separate quantitative track owned by
+  `EchoFiberCount` / `EchoThermodynamics*`, not by this bridge.
+
+== Why the framing stays narrow
+
+The temptation, given the framing above, is to say "the bridge
+identifies the residue as the witness-asymmetry that survives any
+non-commuting decoration pair".  This is the forbidden-rebrandings
+trip: it generalises across pairs.  The bridge identifies the
+residue in *one* axis pair, where two specific decorations
+(`scramble-server` and `degrade keep≤residue`) interact in a
+specific known way.  Other axis pairs are not addressed; they are
+not within scope.
+
+If the bridge ever produces a lemma whose statement quantifies over
+decoration pairs (rather than fixing them), or whose proof relies
+on a generic structural property of "decorations" abstracted away
+from `Choreo × Graded`, that lemma is out of scope and the bridge
+closes pending review per `README.adoc` § "Termination criteria"
+item 4.
+
+== Closing observation
+
+The exploratory value, if any, of this directory is the observation
+that the *one* axis pair `EchoIntegration` integrates makes a
+specific structural choice — putting the residue in the witness
+`x`, not in `y` and not in the equality leg — and that this choice
+might resemble what other adjacent-domain constructions do when they
+build provenance metadata.  The three candidates in
+`01-decoration-instances.adoc` test that resemblance against falsifiers.
+
+Whether the resemblance is real, useful, or merely structural is the
+question this directory exists to ask.  Whether the answer ever
+warrants promotion to core is a separate, gated decision the
+exploration does not pre-authorise.
diff --git a/docs/echo-types/explorations/decoration-bridge/README.adoc b/docs/echo-types/explorations/decoration-bridge/README.adoc
new file mode 100644
index 0000000..8cb9535
--- /dev/null
+++ b/docs/echo-types/explorations/decoration-bridge/README.adoc
@@ -0,0 +1,497 @@
+= Decoration bridge — exploratory
+:toc: macro
+:toclevels: 2
+:sectnums:
+:sectnumlevels: 2
+:icons: font
+
+[CAUTION]
+====
+*EXPLORATORY — not part of Gate theory.* Not load-bearing for the
+identity claim.  Subject to abandonment.  Does not constrain Pillar E
+or any Lane 1–4 close-out.  Status anchored at `roadmap.adoc` §
+"Deferred research track" § R5; the Agda artefact
+`proofs/agda/EchoDecorationBridge.agda` is deliberately omitted from
+`proofs/agda/All.agda` so the verified suite is unaffected by anything
+in this directory.
+====
+
+toc::[]
+
+== Scope, in one paragraph
+
+The integration construction `EchoIntegration.agda` combines
+`EchoChoreo`'s role-projection transport with `EchoGraded`'s
+compositional degradation.  This directory is a bounded exploration of
+whether the *one specific* `Choreo × Graded` axis pair that
+`EchoIntegration` integrates resembles the shape that arises when
+adjacent-domain constructions try to compose two different
+*decorations* on a shared state evolution — CRDT merge strategies,
+gossip partial views, local-first causal histories, and so on.  The
+exploration is scoped to candidate analogies for the `Choreo × Graded`
+shape.  It is not a generalisation claim, not a new identity claim,
+not a pillar, not a gate.  It is a place where the question "could the
+integration shape say something useful about adjacent-domain
+constructions?" can be asked without the answer back-propagating into
+load-bearing code.
+
+== Motivation
+
+Several adjacent-domain constructions exhibit a recurring pattern:
+state evolves over time, and *two* orthogonal disciplines decorate the
+same evolution.  In a CRDT, replicas and merge-order decorate update
+streams.  In a local-first system, client/server roles and causal
+history decorate document edits.  In a partial-view gossip protocol,
+membership views and view freshness decorate node knowledge.
+
+Each pattern resembles `EchoIntegration`'s shape: one decoration looks
+like a role projection (who sees what), the other looks like a graded
+loss order (what survives composition).  When the two decorations
+*commute*, the composed echo is well-behaved; when they do not, the
+echo retains a *residue* characterising the order in which the
+decorations were applied.  The question worth asking — bounded, not
+generalised — is whether that residue, in any of these external
+analogies, is the same residue the `EchoIntegration` claim names.
+
+The framing must be read carefully.  This is not the claim that the
+integration recipe generalises across decoration pairs; that is
+forbidden under the EI-2 termination
+(`.machine_readable/6a2/STATE.a2ml` § `forbidden-rebrandings`).  It is
+the strictly narrower question: does the *one* axis pair that
+`EchoIntegration` already integrates — `Choreo × Graded` — describe a
+shape that occurs in adjacent domains, well enough to be worth a
+documented analogy?  Each candidate gets a *falsifier* (see
+<<_three_candidate_instances>>).  Candidates that need a different
+axis pair fail the fit by construction; they are out of scope.
+
+== Scope discipline (read before adding content)
+
+. *One axis pair only.*  The bridge frames `Choreo × Graded`, the pair
+  `EchoIntegration` uses.  `Mode × Grade`, `Role × Role`, and 3D
+  combinations are foreclosed by EI-2 and not reopened here.
+. *External instances are analogies.*  Every candidate in
+  <<_three_candidate_instances>> is framed as an analogy that may or
+  may not fit.  It is never framed as evidence that the integration
+  recipe applies across other decoration pairs.
+. *Falsifier per candidate.*  Every candidate carries a falsifier — a
+  concrete condition under which the analogy fails and the candidate
+  is retired.  Retirement is silent; it does not require new gate
+  theory.
+. *No new identity claim.*  This directory does not assert that
+  decoration bridges are a distinct phenomenon.  Identity claims live
+  in `roadmap-gates.adoc`, not in `docs/echo-types/explorations/`.
+. *No promotion path is implied.*  Promotion of any content from this
+  directory into core would require its own rung-consolidation per
+  CLAUDE.md § "Rung-consolidation policy", including a fresh
+  forbidden-rebrandings audit.  This directory does not pre-authorise
+  any such promotion.
+
+== What this is NOT
+
+The exploration is *not*:
+
+* a smart-contract verifier or any kind of programmable-money artefact;
+* a reversibility claim about consensus, replication, or finality;
+* a zero-knowledge proof system;
+* a claim that echo types fix any production system's bugs or
+  reliability properties;
+* a reopening of EI-2 under a new framing (see
+  <<_forbidden_rebrandings_check>>);
+* an alternative to `EchoIntegration` or a wrapper around it that is
+  expected to land in core;
+* a Pillar, a Gate, or a Lane-1/2/3/4/5 deliverable;
+* a categorical characterisation of decoration-residue
+  (R-2026-05-18 retraction-watch applies — see
+  <<_retraction_watch>>).
+
+Anything that drifts toward one of the items above is out of scope and
+triggers immediate retirement of the offending content.
+
+== Echo-vs-Σ clearance argument
+
+Per `roadmap.adoc` Lane 2, any echo-types construction must clear the
+Track A/B/C bar set out in `core/skepticisms/is-this-just-sigma-types.md`:
+the construction has to lean on at least one echo-specific property
+that bare `Σ` + `≡` does not give.  The bridge clears the bar via four
+inherited properties, in descending order of confidence:
+
+. *Monotone reindexing on a propositional decoration order.*  The
+  bridge consumes `EchoGraded._≤g_`, `EchoGraded.≤g-prop`, and
+  `EchoGraded.degrade` to talk about *down-step under composition*.
+  Bare `Σ` has no notion of monotone reindexing along a thin poset;
+  the bridge inherits this property and depends on it (the
+  `merged-at-residue` fact, re-issued by the bridge's
+  `decoration-claim`, is the witness pair becoming definitionally
+  equal at `residue` grade — a statement that has no analogue for raw
+  `Σ`).
+. *No-section dual on the down-step.*  The bridge cites
+  `EchoResidue.no-section-collapse-to-residue` transitively through
+  `EchoIntegration.no-recovery-after-residue-degrade`, which is part
+  of the integration claim the bridge re-issues.  Raw `Σ` projects
+  trivially via `proj₁`; the no-section dual is the dual asymmetry
+  the bridge cares about.
+. *Choreographic transport along a commuting square.*  The bridge
+  consumes `EchoChoreo.client-stability` and the
+  `scramble-server`-stability discipline.  This is `Echo.map-square`
+  applied at a role-projection square; it has no `Σ`-only analogue
+  because the witness-transport leg `swap` (or `scramble-server`,
+  here) is part of the structure, not merely the index.
+. *Knowledge witness at a Bool target.*  The bridge consumes
+  `EchoEpistemic.Knows`, which is the role-indexed knowledge predicate
+  defined over role-echoes.  Bare `Σ` has no role-indexing primitive.
+
+The bridge depends on (1) and (3) substantively; (2) and (4) are
+inherited through the integration claim.  If the bridge content can be
+reproduced using only `Σ` + `≡` — that is, if the `DecorationFit`
+record's `Pred-stable` and `knowledge` fields can be discharged
+without using `client-stability` or `scramble-server` or `Knows` —
+then the bridge has failed Track A/B/C and is retired.  This is the
+explicit falsifier for the exploration's existence.
+
+== Relationship to `EchoIntegration`
+
+The bridge depends on `EchoIntegration` at four named surfaces.  No
+other surface of `EchoIntegration` is consumed.  The non-dependency
+list is given so the dependency is auditable if `EchoIntegration`
+later evolves.
+
+[cols="1,3", options="header"]
+|===
+| Used by the bridge | What the bridge does with it
+
+| `EchoIntegration.knowledge-and-controlled-degradation`
+| Re-issued *verbatim* through the `DecorationFit` record — the
+  bridge's `decoration-claim` is literally a one-line wrapper that
+  unpacks the record and applies this lemma.  If this lemma's
+  signature changes, the bridge is re-checked, and if patching it
+  would impose any constraint on upstream code the bridge is retired
+  (signature-change policy in the Agda module's prose header).
+
+| `EchoIntegration.knowledge-preserved-under-choreo`
+| Mentioned in the bridge's signature (the first conjunct of
+  `decoration-claim`'s return type names
+  `proj₁ (client-stability e)`, which is the value
+  `knowledge-preserved-under-choreo` operates on).
+
+| `EchoIntegration.merged-at-residue`
+| Mentioned by name in the Agda module's prose header and in
+  `02-non-commuting-residue.adoc` as the canonical "decorations
+  commute *at the residue grade*" witness — the second conjunct of
+  `decoration-claim` is this fact.
+
+| `EchoIntegration.distinct-at-keep`
+| Imported but not consumed in the current scaffold.  Retained in the
+  bridge's import list as a *witness of intent*: it names the
+  asymmetry between `keep` (witnesses distinct) and `residue`
+  (witnesses merged) the bridge is theorising about.
+|===
+
+Non-dependencies (explicit, for auditability if `EchoIntegration`
+evolves):
+
+* The bridge does *not* consume any non-`Choreo`-non-`Graded` content
+  in `EchoIntegration`.  In particular, it does not consume the
+  `EchoCharacteristic`-derived parts (`echo-true≢echo-false`) except
+  transitively via the integration claim's return type.
+* The bridge does not consume `EchoResidue` directly — only through
+  `EchoIntegration.no-recovery-after-residue-degrade`, which the
+  bridge does not re-export.  Adding a direct `EchoResidue` import
+  would widen the bridge's surface and trigger a scope re-audit.
+* The bridge does not consume any module under `Ordinal/`.  Lane 3 is
+  parallel-independent.
+
+== Three candidate instances
+
+The bridge ships three candidate external analogies for the
+`Choreo × Graded` shape, each as a short narrative in this README and
+a pseudocode sketch in `01-decoration-instances.adoc`.  All three are
+*possible* analogies, not committed instances.  Each carries a
+falsifier.
+
+=== Candidate A — CRDT join semilattices
+
+*The shape.*  A replicated value carries two decorations: which
+replica observed the update (the role-projection decoration) and at
+what merge-order rank (the graded-loss decoration).  A CRDT's merge
+operation is the analogue of `client-stability`: it can change the
+remote replica's state while preserving the local replica's
+observation.  The merge-order rank is the analogue of `_≤g_`:
+post-merge states are *more degraded* (less precisely attributable to
+a single replica) than pre-merge states.
+
+*What residue would mean.*  When two replicas merge their states out
+of order, the surviving witness records *which replica's update was
+absorbed first*.  This is the residue the bridge would name.
+
+*Falsifier.*  If the CRDT's merge is genuinely commutative
+(observation-preserving regardless of merge order), there is no
+residue to name; the analogy fits but says nothing the CRDT's own
+commutativity proof did not already say.  This is the candidate's
+"interesting only in the non-commutative case" failure mode.
+
+=== Candidate B — Local-first causal histories
+
+*The shape.*  A document evolves under client edits with optional
+server reconciliation.  The client / server split is the
+role-projection decoration directly (it *is*
+`EchoChoreo.Role = { Client, Server }`).  The causal history's depth
+or staleness is the graded-loss decoration: deeper-staleness states
+are more degraded than fresher ones.
+
+*What residue would mean.*  When a client edit and a server
+reconciliation interleave non-trivially, the surviving witness records
+which path through the interleaving the document took.  This is the
+provenance information local-first systems already track in vector
+clocks or operational-transform metadata.
+
+*Falsifier.*  If the local-first system already maintains a complete
+causal-history record on every document state, the bridge says
+nothing the system did not already say; the analogy fits but is
+redundant.  This is the candidate's "the residue is the metadata,
+already captured" failure mode.
+
+=== Candidate C — Gossip partial views
+
+*The shape.*  A node in a gossip protocol maintains a partial view of
+the cluster membership and forwards updates to a subset of peers.
+The view (which peers this node observes) is the role-projection
+decoration.  The view's freshness — how recently the node received a
+heartbeat — is the graded-loss decoration; stale views are more
+degraded than fresh ones.
+
+*What residue would mean.*  When a node's view goes stale and is
+refreshed by gossip, the surviving witness records *which peer's
+gossip restored which observation*.  This is provenance for the
+refresh path.
+
+*Falsifier.*  Most gossip protocols are designed to be view-oblivious:
+the node accepts any refresh that arrives without caring which peer
+sent it.  If view-obliviousness is the design intent, the residue the
+bridge would name is intentionally discarded; the bridge correctly
+characterises a property the protocol deliberately erases.  That is
+not a useful fit.  This is the candidate's "the protocol erases the
+residue on purpose" failure mode.
+
+[NOTE]
+====
+None of the three candidates is an *instance* in the Agda sense —
+none discharges `DecorationFit` for a concrete predicate.  They are
+narrative analogies to motivate the scaffold.  A future session that
+wanted to commit to one would need to discharge `DecorationFit` for a
+real `Pred`, a real stability proof, and a real `Knows`-witness, and
+that discharge would itself be the rung where the candidate either
+clears the bar or fails it.
+====
+
+== Open questions
+
+Bridge-only.  Scope-flagged.  Do NOT migrate into
+`docs/next-questions.adoc` or any main open-questions file — these are
+exploration-internal and have no priority claim on core work.
+
+[cols="1,3", options="header"]
+|===
+| Tag | Question
+
+| QB-1
+| Is there an adjacent-domain construction whose stability witness
+  (analogue of `scramble-server`-stability) is *not already* expressible
+  as a standard CRDT/state-machine invariant?  If every candidate's
+  stability is already a known invariant, the bridge's `Pred-stable`
+  field adds no information and the bridge is redundant.
+
+| QB-2
+| Does any candidate need a non-`Bool` visible codomain?  The bridge
+  currently fixes `y : Bool` (inherited from `EchoIntegration`).
+  Widening to arbitrary `B` is technically straightforward but a scope
+  change; flagging here so the decision is visible.
+
+| QB-3
+| If a candidate's residue characterisation matches `merged-at-residue`
+  literally (i.e. the candidate's "two distinct witnesses collapse at
+  the residue grade" reduces to the same `refl` proof
+  `EchoIntegration` already pins), does the analogy say anything the
+  retracted-prose `EchoGraded` framing did not already say?  This is
+  the question that drives <<_termination_criteria>> item 3 — if the
+  answer is no, the bridge retires.
+
+| QB-4
+| The three candidates here are deliberately *not* taken from the
+  rollup / consensus / ZK literature, to keep the framing away from
+  programmable-money territory.  Is the omission self-restraining
+  enough, or does it need a stronger boundary statement somewhere in
+  the project?
+|===
+
+== Forbidden-rebrandings check
+
+The framing was checked, item-by-item, against the two
+`forbidden-rebrandings` registers in
+`.machine_readable/6a2/STATE.a2ml`:
+
+. The EI-2 list under `(define forbidden-rebrandings ...)`
+  (lines 223–229).
+. The graded-comonad earn-back list under
+  `earn-back-summary`, field `forbidden-rebrandings`
+  (lines 317–321).
+
+[cols="1,2,2", options="header"]
+|===
+| Register entry | Adjacency to bridge framing | Verdict
+
+| "the integration argument carries gate-1's distinctness load"
+| The bridge re-issues `EchoIntegration.knowledge-and-controlled-degradation`.
+  Adjacency exists.
+| *Cleared.*  The bridge explicitly states (see <<_what_this_is_not>>)
+  that this directory does not assert distinctness; identity claims
+  live in `roadmap-gates.adoc`, not here.
+
+| "the recipe is uniformly applicable across all 2D axis pairs"
+| *Closest match.*  External candidate analogies could be mis-read as
+  "the recipe applies to CRDTs / gossip / local-first" — a
+  uniform-applicability claim.
+| *Cleared by construction.*  Scope is strictly `Choreo × Graded`
+  (the one axis pair `EchoIntegration` already uses).  Each candidate
+  is an *analogy that may or may not fit* and carries a falsifier;
+  no candidate is framed as evidence the recipe extends.  See
+  <<_scope_discipline_read_before_adding_content>> items 1 and 2.
+
+| "non-loss-only is sufficient for substantive simultaneous interaction"
+| The bridge does not invoke a non-loss-only criterion.
+| *Not engaged.*  No claim made.
+
+| "five axes simultaneously as a distinctness claim"
+| The bridge uses two axes.
+| *Not engaged.*  No claim made.
+
+| "Mode × Grade is a falsifier in some weaker sense"
+| The bridge does not address Mode × Grade.
+| *Not engaged.*  No claim made.
+
+| "Role × Role would have produced substantive content with a better family choice"
+| The bridge does not address Role × Role.
+| *Not engaged.*  No claim made.
+
+| "EchoGraded is a graded comonad"
+| The bridge consumes `EchoGraded.degrade`.  Adjacency exists.
+| *Cleared.*  The Agda module's retraction-watch header forbids
+  describing the records as a graded comonad; the README's
+  <<_retraction_watch>> section repeats the cite.
+
+| "the F1 construction reinstates EchoGraded's retracted comonad claim"
+| The bridge does not consume any F1/F3 surface.
+| *Not engaged.*
+
+| "the F3 two-models result reinstates EchoRelModel's retracted two-models claim"
+| The bridge does not consume `EchoRelModel`.
+| *Not engaged.*
+
+| "the title or central thesis of paper.adoc moves on F1 or F3 alone"
+| The bridge is an exploration; it does not propose paper edits.
+| *Not engaged.*
+|===
+
+There is no documented mechanism for prospectively adding entries to
+either register, and inventing one is out of scope for the bridge.
+If a future audit identifies a new forbidden-rebranding that the
+bridge would otherwise trip on, the correct response is to add the
+entry to the register via the normal audit process and trigger the
+automatic-termination clause in <<_termination_criteria>>.
+
+== Retraction-watch
+
+Per `docs/retractions.adoc` R-2026-05-18, the bridge inherits three
+narrowings from its upstream dependencies.  Each drift condition
+trips retraction-watch and closes the bridge pending review.
+
+[cols="1,2", options="header"]
+|===
+| Narrowing | Drift condition
+
+| Pillar B is funext-relative pointwise, not full universal property
+| If the bridge ever produces content described as a "categorical
+  universal property of decoration-residue" or a "limit of a
+  cospan of decorations" or any variant thereof.
+
+| `EchoGraded` is a thin-poset reindexing modality, not a graded comonad
+| If the bridge ever produces content described as a "graded
+  comonad of decorations" or "nested decoration degradation
+  satisfying the comonad laws" or any variant thereof.
+
+| `EchoRelModel` is carrier-parametricity over a fixed grade poset, not model-independence
+| If the bridge ever produces content described as a "model-independent
+  decoration semantics" or "decoration bridge across multiple
+  models" or any variant thereof.
+|===
+
+== Termination criteria
+
+The exploration closes — and the four files plus the roadmap
+references are deleted, returning the repo to its pre-scaffolding
+state — under any of the following conditions.  Closure is silent and
+does not require gate theory.
+
+. *Track A/B/C failure.*  The bridge content can be reproduced using
+  only `Σ` + `≡` (see <<_echo_vs_σ_clearance_argument>>).  In that
+  case the bridge is renamed `SigmaDecorationBridge.agda` and moved
+  to a draft branch, or — preferred — simply deleted, since the
+  point of the exploration is to study the *echo*-shape and a `Σ`-only
+  reduction proves there is no echo-shape to study.
+
+. *All three candidates fail their falsifiers without a replacement
+  surfacing.*  If Candidates A, B, C are all retired (per the
+  failure modes named in <<_three_candidate_instances>>) and no
+  fourth candidate surfaces within one rung-consolidation cycle, the
+  exploration has no remaining motivation and closes.
+
+. *Redundancy with retracted-prose framing (QB-3).*  If the analysis
+  in `02-non-commuting-residue.adoc` reduces to a re-statement of
+  the retracted `EchoGraded` graded-comonad framing — i.e. the
+  bridge's residue characterisation is exactly the graded-comonad
+  framing R-2026-05-18 narrowed — the bridge is closed because it
+  adds nothing the retraction did not already document.
+
+. *Forbidden-rebranding addition.*  If any subsequent audit pass adds
+  the bridge framing (or a near-paraphrase of it) to
+  `.machine_readable/6a2/STATE.a2ml § forbidden-rebrandings` or to
+  `earn-back-summary § forbidden-rebrandings`, the exploration
+  terminates immediately and the files are deleted as part of the
+  audit's closure, not reopened.  The audit's authority on closure
+  is final; the bridge does not get a say in whether its own framing
+  has been added to a register.
+
+. *Retraction-watch trip.*  If the bridge produces content matching
+  any of the three drift conditions in <<_retraction_watch>>, the
+  bridge closes pending review.  Review concludes with either the
+  drift being removed (bridge reopens at the pre-drift state) or
+  the bridge closing for cause (files deleted).
+
+. *Cleanup invariant.*  Closure under any clause above means
+  deleting `proofs/agda/EchoDecorationBridge.agda`,
+  `docs/echo-types/explorations/decoration-bridge/`, the R5 entry
+  in `roadmap.adoc`, the Lane 4 one-liner cross-reference in
+  `roadmap.adoc`, and the row in
+  `docs/echo-types/echo-kernel-note.adoc`.  No other file is touched
+  by closure.  The repo returns to its pre-scaffolding state with
+  zero residue.
+
+== Pointers
+
+* Companion documents in this directory:
+** `01-decoration-instances.adoc` — pseudocode sketches of the three
+   candidates above with their `DecorationFit` shapes and falsifiers.
+** `02-non-commuting-residue.adoc` — conceptual core: what
+   characterises the residue when two decorations do not commute,
+   and why this is not generic `Σ`.
+* Agda artefact: `proofs/agda/EchoDecorationBridge.agda` — scaffold
+  module with `DecorationFit` record and `decoration-claim` plug-in.
+  Not in `proofs/agda/All.agda`; typecheck standalone via
+  `agda -i proofs/agda proofs/agda/EchoDecorationBridge.agda`.
+* Roadmap anchor: `roadmap.adoc` § "Deferred research track" § R5,
+  with a one-liner cross-reference under Lane 4 for navigability.
+* Forbidden-rebrandings register:
+  `.machine_readable/6a2/STATE.a2ml` § `forbidden-rebrandings` and
+  the `earn-back-summary § forbidden-rebrandings` list.
+* EI-2 termination record: `docs/EI2_REPORT.adoc` § "Status".
+* R-2026-05-18 retraction record: `docs/retractions.adoc`.
+* Track A/B/C bar: `core/skepticisms/is-this-just-sigma-types.md`.
diff --git a/proofs/agda/EchoDecorationBridge.agda b/proofs/agda/EchoDecorationBridge.agda
new file mode 100644
index 0000000..8030c9c
--- /dev/null
+++ b/proofs/agda/EchoDecorationBridge.agda
@@ -0,0 +1,201 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- ============================================================
+-- EchoDecorationBridge.agda  (EXPLORATORY)
+-- ============================================================
+--
+-- Status.  Exploratory bridge module.  Not load-bearing for the
+-- identity claim, not part of Gate theory, not imported by
+-- All.agda, subject to abandonment without notice.  See:
+--
+--   docs/echo-types/explorations/decoration-bridge/README.adoc
+--   roadmap.adoc § Deferred research track § R5
+--
+-- The bridge frames adjacent-domain constructions (CRDT merges,
+-- gossip partial views, local-first causal histories) as
+-- candidate analogies for the EchoIntegration shape, NOT as
+-- evidence that the integration recipe generalises.  Scope is
+-- strictly the Choreo × Graded axis pair that EchoIntegration
+-- already integrates.  External candidates that need to vary the
+-- axis pair are out of scope.
+--
+-- Imports (the *only* upstream surfaces this module touches).
+--   * EchoIntegration:
+--       knowledge-and-controlled-degradation
+--       knowledge-preserved-under-choreo
+--       merged-at-residue
+--       distinct-at-keep
+--   * EchoChoreo:
+--       Role, Client
+--       Global
+--       client-stability
+--       scramble-server
+--   * EchoGraded:
+--       keep≤residue
+--       degrade
+--   * EchoCharacteristic (transitive surface mentioned in
+--     EchoIntegration's return type):
+--       echo-true, echo-false
+--   * EchoEpistemic (transitive surface mentioned in
+--     EchoIntegration's input type):
+--       Knows
+--
+-- Signature-change policy.  If any listed upstream lemma changes
+-- signature, this module is re-checked.  If patching it to track
+-- the new signature would impose *any* constraint on upstream
+-- code — even a benign-looking one — this module is retired, not
+-- patched.  Exploratory code does not get to vote on what
+-- upstream code is allowed to look like; that is the whole point
+-- of the isolation discipline.
+--
+-- Reverse-import discipline.  No non-bridge module imports this
+-- one.  Adding such an import re-attaches the exploration to
+-- load-bearing code, defeats the cleanly-abandonable property,
+-- and is a violation.  If a downstream use case appears, the
+-- correct response is to promote the relevant content to a
+-- proper core module via the normal rung-consolidation policy,
+-- not to import EchoDecorationBridge.
+--
+-- Retraction-watch (docs/retractions.adoc R-2026-05-18).  Do not
+-- describe the records or functions below as:
+--   * a categorical characterisation of decoration-residue
+--     (Pillar B is funext-relative pointwise, not full UP);
+--   * a graded comonad structure (EchoGraded is a thin-poset
+--     reindexing modality, not a graded comonad);
+--   * a model-independent decoration semantics (EchoRelModel is
+--     carrier-parametricity over a fixed grade poset, not
+--     model-independence).
+-- If the bridge ever produces content that looks like any of the
+-- above, retraction-watch trips and the bridge closes pending
+-- review.
+--
+-- Forbidden-rebrandings discipline.
+-- (.machine_readable/6a2/STATE.a2ml § forbidden-rebrandings)
+-- The framing is scoped to the *one* Choreo × Graded axis pair
+-- that EchoIntegration uses.  External candidate instances are
+-- analogies that may or may not fit, never evidence that the
+-- integration recipe is uniformly applicable across 2D axis
+-- pairs.  See README §"Forbidden-rebrandings check" for the
+-- auditable cite-by-name verdict.
+
+module EchoDecorationBridge where
+
+----------------------------------------------------------------------
+-- Imports.  Tight and audited (see header).
+----------------------------------------------------------------------
+
+open import EchoChoreo using
+  ( Role; Client
+  ; Global
+  ; client-stability
+  ; scramble-server
+  )
+open import EchoGraded using
+  ( keep≤residue
+  ; degrade
+  )
+open import EchoIntegration using
+  ( knowledge-and-controlled-degradation
+  ; knowledge-preserved-under-choreo
+  ; merged-at-residue
+  ; distinct-at-keep
+  )
+
+-- Transitive surfaces (mentioned in EchoIntegration's input /
+-- return types; the bridge re-issues those types verbatim).
+open import EchoCharacteristic using (echo-true; echo-false)
+open import EchoEpistemic using (Knows)
+
+open import Data.Bool.Base using (Bool)
+open import Data.Product.Base using (_×_; _,_; proj₁)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+
+----------------------------------------------------------------------
+-- Section 1.  The fit shape.
+--
+-- An external candidate instance fits the EchoIntegration shape
+-- precisely when it can supply the inputs that
+-- `knowledge-and-controlled-degradation` consumes:
+--
+--   (a) a predicate on Global naming the candidate's invariant;
+--   (b) a proof that the invariant is preserved under
+--       `scramble-server`, the specific hidden-state update
+--       EchoChoreo names (NB: not a general invariance claim —
+--       only this one update);
+--   (c) a Client-side knowledge witness at a fixed Bool target.
+--
+-- This record names that fit shape.  It does NOT generalise over
+-- the role pair, the grade lattice, the choreographic update, or
+-- the visible-codomain shape.  Any candidate that would need to
+-- vary one of those is out of scope for this scaffold and fails
+-- the fit by construction.
+--
+-- TODO(bridge): the record currently mirrors EchoIntegration's
+-- inputs one-to-one.  That is intentional for the scaffold —
+-- making the fit shape strictly narrower than the integration
+-- claim it triggers means external candidates have somewhere
+-- precise to land or honestly fail to land.
+----------------------------------------------------------------------
+
+record DecorationFit (y : Bool) : Set₁ where
+  field
+    Pred        : Global → Set
+    Pred-stable : ∀ g → Pred g → Pred (scramble-server g)
+    knowledge   : Knows Client Pred y
+
+----------------------------------------------------------------------
+-- Section 2.  Plug-in: a fitting candidate inherits the
+-- EchoIntegration conclusion verbatim.
+--
+-- This is the bridge's *only* current substantive content — a
+-- type-level demonstration that the integration shape is what
+-- candidates must produce, not a new theorem.  The body is
+-- literally the integration lemma applied to the record's
+-- fields; the value of the wrapper is that an external candidate
+-- can see, in one place, exactly what it owes the bridge.
+--
+-- TODO(bridge): there is no second-order content here.  If a
+-- real candidate ever lands and forces a genuinely new lemma
+-- (rather than a re-package), that lemma is the moment to
+-- re-audit the bridge scope against the forbidden-rebrandings
+-- register, because "novel cross-axis content" is structurally
+-- adjacent to several entries.
+----------------------------------------------------------------------
+
+decoration-claim :
+  ∀ {y : Bool} (fit : DecorationFit y) →
+  (∀ e → DecorationFit.Pred fit (proj₁ (client-stability e)))
+  × (degrade keep≤residue echo-true ≡ degrade keep≤residue echo-false)
+decoration-claim fit =
+  knowledge-and-controlled-degradation
+    (DecorationFit.Pred-stable fit)
+    (DecorationFit.knowledge fit)
+
+----------------------------------------------------------------------
+-- Section 3.  What is intentionally absent (and why).
+--
+-- The following are NOT in this module, and adding them would
+-- exceed the bridge scope:
+--
+--   * A second axis pair.  Mode × Grade, Role × Role, and 3D
+--     combinations are all foreclosed by EI-2.  The bridge does
+--     not re-attempt them under a new framing.
+--   * A "general candidate" record polymorphic over decoration
+--     pairs.  That structure is precisely what the EI-2
+--     termination shows does not carry substantive simultaneous
+--     content; framing it as a bridge-side interface would be a
+--     forbidden-rebranding under STATE.forbidden-rebrandings
+--     entry "the recipe is uniformly applicable across all 2D
+--     axis pairs".
+--   * Composition of `decoration-claim` with itself across
+--     different `y` values.  The EchoIntegration claim is at one
+--     y; composing two such claims is meaningful only inside the
+--     core development, where `client-stability`'s functorial
+--     law lives.  The bridge does not lift that machinery.
+--   * Universal-property language for `DecorationFit`.  It is a
+--     record, not a limit; describing it as terminal among
+--     candidates would trip retraction-watch.
+--
+-- TODO(bridge): if any of these become tempting during a future
+-- session, stop and read this section first.
+----------------------------------------------------------------------
diff --git a/roadmap.adoc b/roadmap.adoc
index 8971368..7ef786f 100644
--- a/roadmap.adoc
+++ b/roadmap.adoc
@@ -255,6 +255,11 @@ target codebases. Two architectural options when unparking:
 The first option is preferred unless the user's broader-research-plan
 priorities (per 2026-05-26) explicitly favour tighter integration.
 
+*Conceptual (non-cross-repo) bridge cross-reference.* See § R5
+(Deferred research track) for the exploratory decoration bridge —
+not in scope for Lane 4 cross-repo verification work; navigability
+pointer only.
+
 === Lane 5 [PARKED] — Tutorial / pedagogy
 
 *Unblocking condition.* Lane 1 closes, OR a single "killer
@@ -429,6 +434,61 @@ close it, and why it is parked.
 * *Difficulty.* Hard. Smallest-step start: lift `IsArgmin` over an
   arbitrary `Fin n`-indexed score family; compose with `degrade`.
 
+=== R5 — Decoration bridge (exploratory, not identity-bearing)
+
+[NOTE]
+====
+*Schema note.* This entry carries an additional `*Termination*`
+bullet that R1–R4 do not.  The divergence is intentional: this lane
+has automatic-closure conditions tied to the forbidden-rebrandings
+register, so the termination criterion needs to be visible at the
+roadmap level rather than only in the bridge's own README.  Future
+R-series entries should not inherit the extra bullet by default —
+add it only if the new entry also has automatic-closure conditions.
+====
+
+* *Gap.* The integration construction `EchoIntegration.agda` combines
+  `EchoChoreo`'s role-projection transport with `EchoGraded`'s
+  compositional degradation.  Whether that *one* axis pair resembles
+  the shape adjacent-domain constructions exhibit when they compose
+  two decorations on a shared state evolution (CRDT merges, gossip
+  partial views, local-first causal histories) is unaddressed — and
+  asking the question inside core would re-attach it to load-bearing
+  code in a way EI-2's termination forbids.
+* *Closure.* A bounded set of analogies in
+  `docs/echo-types/explorations/decoration-bridge/` plus a scaffold
+  Agda module `proofs/agda/EchoDecorationBridge.agda` (not in
+  `All.agda`), each candidate carrying a falsifier.  Closure is
+  *either* the discovery of a candidate whose discharge would clear
+  Track A/B/C and warrant a separate rung-consolidation, *or*
+  retirement under one of the explicit termination conditions.
+* *Difficulty.* Unknown.  Bounded by construction — abandonment is
+  the default outcome, not a failure.
+* *Termination.* The exploration terminates immediately if any of
+  the following holds:
+  (i) the bridge content reduces to plain `Σ` + `≡` (Track A/B/C
+  failure);
+  (ii) all three candidate analogies fail their falsifiers without
+  a replacement surfacing;
+  (iii) the residue analysis reduces to the retracted-prose
+  `EchoGraded` graded-comonad framing (R-2026-05-18);
+  (iv) any subsequent audit pass adds the bridge framing (or a
+  near-paraphrase) to
+  `.machine_readable/6a2/STATE.a2ml § forbidden-rebrandings` or to
+  `earn-back-summary § forbidden-rebrandings`;
+  (v) retraction-watch trips on any of the three R-2026-05-18
+  narrowings (Pillar B pointwise mediator, `EchoGraded` thin-poset
+  reindexing, `EchoRelModel` carrier-parametricity).
+  Closure means deleting the bridge module, the docs directory,
+  this R5 entry, the Lane 4 cross-reference one-liner, and the row
+  in `docs/echo-types/echo-kernel-note.adoc`; no other file is
+  touched.
+* *Anchor.*
+  `docs/echo-types/explorations/decoration-bridge/README.adoc`.
+* *Retraction-watch.* Three drift conditions; see the bridge
+  README § "Retraction-watch".  Tripping any condition closes the
+  bridge pending review.
+
 == Lane discipline rules
 
 . *Cap.* 5 open lanes maximum. Opening a 6th requires closing or