fix(ci): classify EchoDeniability in kernel-note and MAP.adoc

kernel-guard Check B requires every Echo*.agda module to appear in
docs/echo-types/echo-kernel-note.adoc. EchoDeniability is Tier 2
(imports Echo + EchoNoSectionGeneric). MAP.adoc gains a Deniability
bullet under the audience-moves section with [REAL] tag.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

docs/echo-types/MAP.adoc

@@ -235,6 +235,16 @@ honest-bound matched-negative block.
   `bool-perturbed-nat-sensitivity`. Honest-bound: NOT ε-DP /
   Lipschitz bound / noise calibration / adversary model.
   `proofs/agda/EchoDifferential.agda`.
+* *Deniability* — `IsDeniable` predicate + `IsConstantOpener`
+  restricted class. Two production functions: `produce-perfect`
+  (constant — perfectly deniable, no section via
+  `no-section-of-collapsing-map`) and `produce-partial` (injective
+  — not deniable for arbitrary openers, section exists via
+  `partial-witness`). The no-section/has-section pair is a checked
+  duality theorem. `IsConstantOpener` is the type-level analogue of
+  the `affine` mode in `EchoObservationalEquivalence`. Honest-bound:
+  NOT side-channel-safe / cryptographic deniability / adaptive
+  adversary. `proofs/agda/EchoDeniability.agda`. `[REAL]`
 
 *Curated suite — single-file entry point.* The narrative
 deliverable that pulls the Tier-1 / Tier-2 / Tier-3 named theorems

docs/echo-types/echo-kernel-note.adoc

@@ -121,8 +121,12 @@ kernel** — the boundary is real and lives outside this core.
   residue / decoration / observational classifications.
   *Application/extension modules* (also added via the same sweep):
   `EchoEntropy`, `EchoLLEncoding`, `EchoProvenance`, `EchoSecurity`,
-  `EchoProbabilisticSupport`, `EchoDifferential` are derived domain
-  applications mapped under their own headings in MAP.adoc.
+  `EchoProbabilisticSupport`, `EchoDifferential`, `EchoDeniability`
+  are derived domain applications mapped under their own headings in
+  MAP.adoc.  `EchoDeniability` formalises residue deniability: the
+  perfect (constant / no-section) case and the partial (injective /
+  has-section) case, with `IsConstantOpener` as the exact cut-point.
+  Imports `Echo` + `EchoNoSectionGeneric`.
 
 | *Earn-back gate modules* +
 (derived / scoped; not kernel)