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

kernel-guard.sh Check B (classification-drift lint) requires every
proofs/agda/Echo*.agda module to be named in echo-kernel-note.adoc.
Add EchoAggregation to the application/extension list there, plus a
[REAL]-tagged audience-move bullet in MAP.adoc.

Mirrors the EchoDeniability classification fix (2026-06-13).

scripts/kernel-guard.sh exits 0 locally.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VwbFNQJw23tW8tqM7utWku

Author: claude

docs/echo-types/MAP.adoc

@@ -253,6 +253,17 @@ honest-bound matched-negative block.
   the `affine` mode in `EchoObservationalEquivalence`. Honest-bound:
   NOT side-channel-safe / cryptographic deniability / adaptive
   adversary. `proofs/agda/EchoDeniability.agda`. `[REAL]`
+* *Aggregation* — `aggregate` rolls a two-account ledger up to a
+  Godley column total. The fibre `ConsistentLedgers m = Echo
+  aggregate m` is "aggregation is many-to-one" as a type;
+  `aggregate-non-injective` exhibits two distinct micro ledgers at
+  the same macro total; `no-canonical-disaggregation` is the
+  non-identifiability theorem (no section of `aggregate`, via
+  `no-section-of-collapsing-map`). The mechanised keystone of the
+  oikos/betlang alib note (`oikos:docs/alib-aggregate-bridge.adoc`).
+  Honest-bound: NOT a quantitative fibre-size bound / joint
+  identifiability of the full MacroState record.
+  `proofs/agda/EchoAggregation.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

@@ -124,12 +124,16 @@ 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`, `EchoDeniability`
+  `EchoProbabilisticSupport`, `EchoDifferential`, `EchoDeniability`,
+  `EchoAggregation`
   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`.
+  `EchoAggregation` formalises micro→macro economic aggregation: the
+  rollup `aggregate` is an `Echo` map and non-disaggregability is
+  `no-section-of-collapsing-map` (the mechanised keystone of the
+  oikos/betlang alib note).  Imports `Echo` + `EchoNoSectionGeneric`.
 
 | *Earn-back gate modules* +
 (derived / scoped; not kernel)