diff --git a/CITATION.cff b/CITATION.cff
index cf0ab67..11e9b35 100644
--- a/CITATION.cff
+++ b/CITATION.cff
@@ -23,3 +23,5 @@ keywords:
   - "scientific-software"
   - "typed-provenance"
   - "veridical-computing"
+version: 0.4.0
+date-released: 2026-10-20
diff --git a/Project.toml b/Project.toml
index f9ceb0d..1fd81cc 100644
--- a/Project.toml
+++ b/Project.toml
@@ -6,7 +6,7 @@
 name = "EchoTypes"
 uuid = "a8ca608b-856a-4215-8c3d-f9ffd1705524"
 authors = ["Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>"]
-version = "0.3.0"
+version = "0.4.0"
 
 [compat]
 julia = "1.10"
diff --git a/README.adoc b/README.adoc
index cd518c4..5ef5635 100644
--- a/README.adoc
+++ b/README.adoc
@@ -64,7 +64,7 @@ The Agda. This release mirrors `+hyperpolymath/echo-types+` at
 (2026-05-28 head, after the Tier-3 audience-facing spine landed —
 EchoProvenance, EchoSecurity, EchoProbabilisticSupport,
 EchoDifferential, EchoLLEncoding, plus the EchoCanonicalIdentitySuite
-re-export bundle). The unreleased `+EchoAggregation+` entry below is
+re-export bundle). The `+EchoAggregation+` entry below (new in v0.4.0) is
 mirrored from a later commit,
 `+703dd77af402e959b46f49e8ce2e084521bedbae+`; every other row keeps the
 pin above:
@@ -139,7 +139,7 @@ audience move 4 — blur loses perturbation tag)
 `+source_no_section_holds+`, `+gap_paired+` |`+EchoLLEncoding.agda+`
 (cementing-negative — the LL `+!A := 1+` shadow admits an encoded
 section paired with source-side no-section)
-|*unreleased* `+Monoid+`, `+GroupAggregator+`, `+oplus_fold+`,
+|*v0.4.0* `+Monoid+`, `+GroupAggregator+`, `+oplus_fold+`,
 `+aggregate_values+`, `+aggregation_as_fold_holds+`, `+sum_monoid+` /
 `+count_monoid+` / `+max_monoid+` / `+min_monoid+`,
 `+no_canonical_disaggregation_of+`, `+pair_sum+` and its
@@ -237,16 +237,16 @@ green and is the only correctness claim this package makes about itself.
 
 === Status
 
-`+v0.3.0+`, local development. The v0.1.0 surface (`+Echo+`,
+`+v0.4.0+`. The v0.1.0 surface (`+Echo+`,
 `+EchoResidue+`, `+EchoFiberCount+`, `+EchoThermodynamics+`) and the
 v0.2.0 Tier-1+Tier-2 canonical-identity spine are preserved unchanged;
 v0.3.0 adds executable shadows of the Tier-3 audience-facing spine that
 landed upstream on 2026-05-27/28 (`+EchoProvenance+`, `+EchoSecurity+`,
 `+EchoProbabilisticSupport+`, `+EchoDifferential+`) plus the
 cementing-negative `+EchoLLEncoding+` (LL shallow-encoding gap with
-paired source-side no-section). Unreleased on top of v0.3.0:
-`+EchoAggregation+` (mirrored from echo-types `+703dd77+`, not from
-`+eed4250+`). Test suite:
+paired source-side no-section). v0.3.0 was never tagged on its own; its
+content ships in v0.4.0, which adds `+EchoAggregation+` (mirrored from
+echo-types `+703dd77+`, not from `+eed4250+`). Test suite:
 *302 passing assertions across 21 testsets*, organised as finite shadows of named Agda lemmas
 plus the semantic-fibre vocabulary exercise over the kernel. Registered
 as `+EchoTypes+` in the hyperpolymath professional registry; *not*
diff --git a/src/EchoTypes.jl b/src/EchoTypes.jl
index 4b6cacc..600a1a9 100644
--- a/src/EchoTypes.jl
+++ b/src/EchoTypes.jl
@@ -24,7 +24,7 @@
 # worked instance`) + cementing-negative EchoLLEncoding (the
 # trivial-⊤-shadow LL gap with paired source-side no-section).
 #
-# Unreleased on top of v0.3.0: EchoAggregation (general monoid/group
+# v0.4.0 adds EchoAggregation (general monoid/group
 # aggregation, echo-types#175), mirrored from echo-types origin/main
 # @ 703dd77af402e959b46f49e8ce2e084521bedbae. The rest of this header's
 # provenance pin is unchanged.
@@ -94,7 +94,7 @@ export EchoWitness, echo_intro, in_fiber, fiber,
        LLShallowEncoding, trivial_encoding,
        trivial_encoding_has_section, ll_encoding_gap,
        source_no_section_holds, gap_paired,
-       # EchoAggregation (unreleased; general monoid/group form, echo-types#175)
+       # EchoAggregation (v0.4.0; general monoid/group form, echo-types#175)
        Monoid, GroupAggregator, monoid_laws_hold,
        oplus_fold, oplus_fold_append_holds,
        aggregate_values, aggregation_as_fold_holds,
diff --git a/wiki/Exercises.md b/wiki/Exercises.md
index 2df2528..78797b2 100644
--- a/wiki/Exercises.md
+++ b/wiki/Exercises.md
@@ -33,7 +33,8 @@ julia> using EchoTypes
 ```
 
 The package is **not** in Julia's General registry. It carries its
-own SoT pin tying v0.3.0 to echo-types `eed4250` (2026-05-28).
+own SoT pin tying v0.4.0 to echo-types `eed4250` (2026-05-28), except
+`EchoAggregation`, which is pinned to `703dd77`.
 
 ---
 
diff --git a/wiki/Home.md b/wiki/Home.md
index 86adc59..9c93ee8 100644
--- a/wiki/Home.md
+++ b/wiki/Home.md
@@ -51,10 +51,12 @@ Agda repo remains the formal source of truth.
 
 ## Current pin
 
-`v0.3.0` mirrors echo-types `origin/main` at
-`eed42503a1a4c54ec0a347ebef3440b4d4db30c9` (2026-05-28). The
-package's preamble carries the SoT pin; re-pin a fresh clone if
-you want to track HEAD.
+`v0.4.0` mirrors echo-types `origin/main` at
+`eed42503a1a4c54ec0a347ebef3440b4d4db30c9` (2026-05-28) for every
+module except `EchoAggregation`, which is mirrored from
+`703dd77af402e959b46f49e8ce2e084521bedbae`. The package's preamble
+carries the SoT pin; re-pin a fresh clone if you want to track HEAD.
+(`v0.3.0` was never tagged on its own; its content ships in v0.4.0.)
 
 ## Coverage map (one-line summary)
 
@@ -63,7 +65,8 @@ you want to track HEAD.
 | Foundation (v0.1.0) | Echo / EchoResidue / EchoFiberCount / EchoThermodynamics | 7 |
 | Canonical identity (v0.2.0) | TotalCompletion / OFS / Image / NoSectionGeneric / LossTaxonomy / Entropy / ObsEquivalence | 7 |
 | Audience-facing + LL gap (v0.3.0) | Provenance / Security / ProbabilisticSupport / Differential / LLEncoding | 5 |
-| **Total** | **15 Agda modules + semantic-fibre vocabulary exercise** | **19 testsets, 258 passing assertions** |
+| Aggregation (v0.4.0) | Aggregation (monoid fold, homomorphism law, no-canonical-disaggregation, `pairSum` instance) | 2 |
+| **Total** | **16 Agda modules + semantic-fibre vocabulary exercise** | **21 testsets, 302 passing assertions** |
 
 ## Intentionally NOT mirrored