feat(aggregation): general EchoAggregation monoid/group form (#175) + long-form prose relicense (#239)

## What

Two commits closing housekeeping loose ends from the EchoAggregation /
oikos-alib work.

### A — `docs(licence): long-form prose → CC-BY-SA-4.0 (9 docs)`
(`879ec9b`)

Re-applies the owner-authorised prose relicensing (`f6cc023`) that never
re-landed. Header-line swap only (`SPDX-License-Identifier: MPL-2.0` →
`…: CC-BY-SA-4.0`), copyright lines untouched, on:
`FOUNDATION_CONTRACT.md`, `docs/theorem-index.md`,
`docs/CLAIMS_AUDIT.adoc`,
`docs/echo-types/{fibration-package,universal-property}.adoc`,
`wiki/{Architecture,Overview,Roadmap,Working-Rules}.adoc`.
`CC-BY-SA-4.0` is the designated estate prose licence (already on 29+
files); `MPL-2.0` stays for code.

### B — `feat(aggregation): generalize EchoAggregation to monoid/group
form (#175)` (`c97d0c4`)

The merged economics module (#230) squatted the name **#175** wants for
the *general* monoid/group aggregation. Per the owner's decision,
`EchoAggregation` becomes the general / fundamental form; the macro
economics reading moves to oikos under a distinct name. Key fact making
this loss-free: `pairSum (a,b) = a+b` **is** literally the `sumMonoid`
fold, so the macro result is just an *instance* of the general form.

`proofs/agda/EchoAggregation.agda` now ships:

- `record Monoid ℓ`
(`Elem`/`ε`/`_⊕_`/`assoc`/`identity-l`/`identity-r`);
- `⊕-fold` + `⊕-fold-++` (the fold is a monoid homomorphism over
`_++_`);
- `record GroupAggregator {ℓ} (K V) (M)` (`agg : V → Elem`) +
`aggregate-values`;
- **`aggregation-as-fold`** — the #175 headline law, *proved* (not
merely signed): aggregating a concatenation equals combining the
aggregates;
- `sumMonoid` / `countMonoid` / `maxMonoid` (ℕ) + `minMonoid` over
`Maybe ℕ` (`nothing` = ∞) + a worked `countAggregator`;
- `no-canonical-disaggregation-of` — generic non-disaggregability (any
collision ⇒ no section, via `no-section-of-collapsing-map`); **also
discharges #174's no-section sibling**;
- `module Example-PairSum` — the macro `ℕ × ℕ → ℕ` ledger, neutrally
framed: `pairSum-is-fold` (it IS the `sumMonoid` fold),
`pairSum-non-injective`, `no-canonical-disaggregation` (the
Sonnenschein–Mantel–Debreu / representative-agent critique
type-theoretically). This instance is the mechanised anchor the oikos
alib note cites (where it is read at macro scale and named
`MacroAggregation`).

Docs swept: `Smoke.agda` pins, `MAP.adoc`, `echo-kernel-note.adoc`,
`docs/bridges/cross-repo-bridge-status.md`, `CLAUDE.md`.

## Honest scope

`aggregation-as-fold` is the fold's monoid-homomorphism law, NOT full
SQL GROUP-BY operational semantics. `avg` is deliberately absent (not a
monoid — express as `sum / count`, per #175).
`no-canonical-disaggregation-of` refutes a *section* (left inverse), NOT
the existence of *some* representative choice.

## Verification

```
agda proofs/agda/EchoAggregation.agda   exit 0   (--safe --without-K)
agda proofs/agda/All.agda               exit 0
agda proofs/agda/Smoke.agda             exit 0
scripts/kernel-guard.sh                 PASS     (Check A funext-free + Check B classification)
grep postulate                          none     (zero postulates)
```

## Companion

oikos draft PR extends `docs/alib-aggregate-bridge.adoc` with the macro
reading (`MacroAggregation`) citing this general theorem — no Agda in
oikos (Rust); citation-level per its own §8.

Refs #175, #174 (owner decides closure).

---
🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_01VwbFNQJw23tW8tqM7utWku

---
_Generated by [Claude
Code](https://claude.ai/code/session_01VwbFNQJw23tW8tqM7utWku)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

CLAUDE.md

@@ -212,7 +212,93 @@ work to `main` and refresh all documentation:
 
 ## Current rung state (2026-06-18)
 
-### Session arc 2026-06-18 — EchoAggregation / oikos alib bridge (read this first)
+### Session arc 2026-06-18 — EchoAggregation general/macro split + long-form prose relicense (read this first)
+
+*Where we started:* three housekeeping loose ends from the EchoAggregation /
+oikos-alib work. (1) stale branch `session/slice-4-narrowing` (a git-ancestor
+of `estate-standardization-20260607`, zero unique commits); (2) an
+owner-authorised prose relicensing (`f6cc023`) that never re-landed — 9
+long-form docs still `MPL-2.0` while the estate prose licence is
+`CC-BY-SA-4.0`; (3) a NAME COLLISION: the merged economics module (#230)
+squatted `EchoAggregation`, the name open issue **#175** wants for the
+*general* monoid/group aggregation (SQL GROUP-BY-as-fold; consumer =
+affinescript db-theory #3).
+
+*User decision (the pivot):* echo-types' `EchoAggregation` becomes the
+GENERAL / fundamental form (serving #175); the MACRO economics reading moves
+to oikos under a distinct name + a context statement. Key fact making this
+loss-free: `pairSum (a,b) = a+b` IS literally the `sumMonoid` fold of a
+two-element list, so the macro result is just an *instance* of the general
+form — nothing is re-proved.
+
+*Where we ended:* two echo-types commits on `claude/ecstatic-wright-OBEvx`
+(draft PR), plus an oikos doc commit (draft PR):
+
+* **Commit A — `docs(licence): long-form prose → CC-BY-SA-4.0 (9 docs)`**
+  (`879ec9b`). Header-line swap only (`SPDX-License-Identifier: MPL-2.0` →
+  `…: CC-BY-SA-4.0`) on `FOUNDATION_CONTRACT.md`, `docs/theorem-index.md`,
+  `docs/CLAIMS_AUDIT.adoc`, `docs/echo-types/{fibration-package,universal-property}.adoc`,
+  `wiki/{Architecture,Overview,Roadmap,Working-Rules}.adoc`. Copyright /
+  `SPDX-FileCopyrightText` lines untouched. (Re-applies orig `f6cc023`.)
+
+* **Commit B — `feat(aggregation): generalize EchoAggregation to monoid/group
+  form (#175)`.** `proofs/agda/EchoAggregation.agda` rewritten:
+  `record Monoid ℓ` (`Elem`/`ε`/`_⊕_`/`assoc`/`identity-l`/`identity-r`);
+  `⊕-fold` + `⊕-fold-++` (fold-is-a-monoid-homomorphism over `_++_`);
+  `record GroupAggregator {ℓ}(K V)(M)` (`agg : V → Elem`); `aggregate-values`
+  + the *proved* `aggregation-as-fold` law (#175's headline, by induction —
+  no `map-++` needed); four instances `sumMonoid`/`countMonoid`/`maxMonoid`
+  (ℕ,0,+ / + / ⊔) + `minMonoid` over `Maybe ℕ` (`nothing` = ∞, `_⊓∞_` with
+  `⊓∞-assoc`/`⊓∞-identity-r`); `countAggregator`; generic
+  `no-canonical-disaggregation-of` (= `no-section-of-collapsing-map`, also
+  covers #174); and `module Example-PairSum` (the OLD macro `ℕ×ℕ→ℕ` ledger,
+  neutrally framed: `pairSum-is-fold`, `pairSum-non-injective`,
+  `no-canonical-disaggregation`) — the mechanised anchor oikos cites.
+  `Smoke.agda` pins rewritten to the general headlines + a separate
+  `open EchoAggregation.Example-PairSum using (…)` block. Docs swept:
+  `echo-kernel-note.adoc` (Check B still PASS — name unchanged), `MAP.adoc`
+  (general bullet, cites #175/#174), `docs/bridges/cross-repo-bridge-status.md`
+  (bridge row + new revision entry: echo-types = general, oikos = macro).
+
+* **oikos — `docs(alib): macro-aggregation reading cites the general
+  EchoAggregation`.** `oikos/docs/alib-aggregate-bridge.adoc` extended with
+  the macro reading + the context statement (it is the EchoAggregation of
+  echo-types read at macro scale; named `MacroAggregation` here because
+  aggregation is a fundamental there) + §8 pointer updated (macro is now an
+  *instance* of the general form). NO Agda in oikos (Rust + AffineScript +
+  Haskell); citation-level, per its own §8.
+
+Build invariant held: `EchoAggregation.agda` + `All.agda` + `Smoke.agda`
+exit 0 under `--safe --without-K`, zero postulates, `kernel-guard.sh` PASS.
+
+*Honest scope.* `aggregation-as-fold` is the fold's monoid-homomorphism law,
+NOT full SQL GROUP-BY operational semantics. `avg` is deliberately absent
+(not a monoid — express as `sum / count`, per #175).
+`no-canonical-disaggregation-of` refutes a *section* (left inverse), NOT the
+existence of *some* representative choice (economists pick representatives;
+the content is that no choice is canonical).
+
+*Flagged (non-executable here):* deleting `session/slice-4-narrowing` (and,
+post-merge, `chore/prose-licence-longform-cc-by-sa`) is a manual GitHub-UI
+step — `git push --delete` returns HTTP 403 and the GitHub MCP has no
+delete-branch endpoint. The genuinely-open `Fidelity.agda` order-type
+fidelity debt (`D-2026-06-14`) is untouched.
+
+*Plan for the next Claude.* (1) After the echo-types PR merges, a frugal
+one-line note on #175 that the general form landed (covers #174 too).
+(2) `EchoTypes.jl` mirror — add an `EchoAggregation` finite-domain shadow
+(the `Monoid`/`sumMonoid` instances + `pairSum` are directly executable).
+(3) oikos alib Route-B build, gated on the owner's Route A vs B decision.
+
+DO NOT reopen: the general/macro split design (the macro IS the
+`Example-PairSum` instance — `pairSum` is the `sumMonoid` fold, so nothing is
+lost by hosting the general form here); the `no-section` refutation target
+(a section is a *left* inverse — exactly what non-disaggregability denies; do
+NOT restate it as a failed surjection, which is false since the maps are
+onto); the citation-level scope of the oikos bridge (oikos is Rust; no
+Agda↔Rust import path).
+
+### Session arc 2026-06-18 — EchoAggregation / oikos alib bridge (the original macro-only landing)
 
 *Where we started:* user asked (cross-repo) to investigate the wasm /
 typed-wasm route, then to scope an oikos/betlang "alib" aggregate library

FOUNDATION_CONTRACT.md

@@ -1,5 +1,5 @@
 <!--
-SPDX-License-Identifier: MPL-2.0
+SPDX-License-Identifier: CC-BY-SA-4.0
 SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 

docs/CLAIMS_AUDIT.adoc

@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: MPL-2.0
+// SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = Claims Audit — Gate G1 input
 :toc: macro

docs/bridges/cross-repo-bridge-status.md

@@ -22,7 +22,7 @@ touches other repositories.
 | **Verdict-provenance (phronesis)** | `Echo`, `echo-intro` | `phronesis/academic/formal-verification/agda/PhronesisEcho.agda` (imports echo-types directly) | **Content bridge done (2026-06-12).** An ethical verdict's provenance IS `Echo verdict v`: `eval` is non-injective, so the fiber retains *which* expressions justify a verdict the bare `Bool` forgets (`verdict-forgets-provenance`); `proj₁` is the recovering section. Machine-checked vs real echo-types. (Also fixed 4 pre-existing bugs making `Phronesis.agda` compile.) | — (closed; downstream consumer in the agentic-ethics language). |
 | **KitchenSpeak `@` witness (nextgen-languages)** | `Echo` | `nextgen-languages/kitchenspeak/proofs/agda/EchoBridge.agda` | **Status upgraded to MACHINE-CHECKED (2026-06-12).** Previously "hand-verified, not machine-checked"; now typechecks against the real `Echo`. The `@` sensor witness IS `Echo (fired sensor thr) true` (`witness⇒echo` / `echo⇒witness`). PoachedEgg stdlib-v2.3 drift (`toWitness {Q=}`→`{a?=}`) fixed so the suite type-checks. | — (the `--` comments in `kitchenspeak.agda-lib` need Agda ≥ 2.6.4; on the 2.6.3 CI toolchain use the explicit `-i` form, documented in the module). |
 | **Invariant Path application (invariant-path)** | Structured-loss vocabulary (the `Echo` fiber concept) — citation-level | `invariant-path` (Rust): `classify_candidate` + `docs/ECHO-TYPES.md` + `crates/invariant-path-core/{examples,tests}/echo_structured_loss.rs` | **Application example (2026-06-12).** `classify_candidate` is a non-injective classifier; the retained `ClaimCandidate` + `ClassificationOutcome.losses` IS the echo (fiber) over a `Classification`. Invariant Path is "a claim-path debugger, not a truth engine" precisely because it retains echoes. Runnable example + 2 CI-covered tests. | No Agda↔Rust import path; citation-level — the application *uses* the echo principle; no mechanised cross-repo theorem. |
-| **oikos alib aggregation bridge (economics)** | `proofs/agda/EchoAggregation.agda` (`aggregate : MicroLedger → MacroTotal` IS an `Echo`; `no-canonical-disaggregation = no-section-of-collapsing-map`) | `oikos/docs/alib-aggregate-bridge.adoc` (toolchain-free design note for the alib aggregate library; oikos is the Rust SFC-macro DSL) | **Keystone formalisation + design note landed (2026-06-18).** Micro→macro economic aggregation is mechanised as an `Echo` map: the fibre over a macro total is exactly the set of micro ledgers consistent with it, and non-disaggregability is `no-section-of-collapsing-map` (no canonical `raise : MacroTotal → MicroLedger` left-inverse exists). This is the type-theoretic form of the Sonnenschein–Mantel–Debreu / representative-agent critique — it refutes a *section* (left inverse), not a representative *choice*. `EchoAggregation.agda` is self-contained in echo-types (imports `Echo` + `EchoNoSectionGeneric` only), `--safe --without-K`, zero postulates, pinned in `Smoke.agda`, classified in the kernel-note. The oikos design note recommends Route B (alib as an aggregation-morphism library over `MacroState`). | No Agda↔Rust import path; citation-level — echo-types proves the aggregation principle, oikos's alib will *consume* it. The alib library itself is not yet built (design-note stage; open questions §"Route A vs B" pending owner decision). |
+| **oikos alib aggregation bridge (economics)** | `proofs/agda/EchoAggregation.agda` — the GENERAL aggregation form (`Monoid` + `GroupAggregator` + `aggregation-as-fold` homomorphism + `sumMonoid`/`countMonoid`/`maxMonoid`/`minMonoid` + `no-canonical-disaggregation-of`); the macro economics is the `Example-PairSum` instance (`pairSum` IS the `sumMonoid` fold) | `oikos/docs/alib-aggregate-bridge.adoc` (toolchain-free design note; oikos is the Rust SFC-macro DSL) — names the macro reading `MacroAggregation`, cited back to echo-types | **General/macro split landed (2026-06-18, gen. rung).** echo-types now hosts the *general* monoid-aggregation form requested by issue #175 (SQL GROUP-BY as a monoid homomorphism; consumer = affinescript db-theory #3); the `aggregation-as-fold` law is *proved*, not merely signed, and generic non-disaggregability `no-canonical-disaggregation-of` also discharges #174's no-section sibling. The *macro→micro economics* reading — micro ledger rolled up to a Godley total, the Sonnenschein–Mantel–Debreu / representative-agent critique (refuting a *section* / left inverse, not a representative *choice*) — is the `Example-PairSum` instance, read at macro scale in oikos under the name `MacroAggregation` (naming it `EchoAggregation` there would be odd: aggregation is a *fundamental* of echo-types). `EchoAggregation.agda` is self-contained (imports `Echo` + `EchoNoSectionGeneric` only), `--safe --without-K`, zero postulates, pinned in `Smoke.agda`, classified in the kernel-note + `MAP.adoc`. The oikos design note recommends Route B (alib as an aggregation-morphism library over `MacroState`). | No Agda↔Rust import path; citation-level — echo-types proves the general aggregation principle (and its macro instance), oikos's alib will *consume* it. The alib library itself is not yet built (design-note stage; Route A vs B pending owner decision). |
 
 ## Immediate next actions
 
@@ -72,6 +72,19 @@ precisely to paper over this in the relational model.
 
 ## Revision history
 
+- 2026-06-18: **EchoAggregation general/macro split.** Generalised
+  `EchoAggregation.agda` from the macro-economics-specific module into the
+  general monoid-aggregation form requested by issue #175 (`Monoid` +
+  `GroupAggregator` + the *proved* `aggregation-as-fold` homomorphism law +
+  `sumMonoid`/`countMonoid`/`maxMonoid`/`minMonoid` + generic
+  `no-canonical-disaggregation-of`, which also covers #174). The
+  macro→micro economics reading survives mechanised as the `Example-PairSum`
+  instance (`pairSum` IS the `sumMonoid` fold — nothing re-proved or lost);
+  oikos reads that instance at macro scale under the name `MacroAggregation`
+  (aggregation is a fundamental of echo-types, so re-using the name there
+  would be odd). Updated the bridge row, `MAP.adoc`, and
+  `echo-kernel-note.adoc`; `--safe --without-K`, zero postulates,
+  kernel-guard PASS.
 - 2026-06-18: **oikos alib aggregation bridge.** Added the
   economics-aggregation row recording `EchoAggregation.agda` (micro→macro
   rollup is an `Echo`; non-disaggregability is `no-section-of-collapsing-map`

docs/echo-types/MAP.adoc

@@ -253,17 +253,28 @@ 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]`
+* *Aggregation (general, issue #175)* — aggregation-as-fold over a
+  `Monoid`, with a `GroupAggregator` and the monoid-homomorphism law
+  `aggregation-as-fold` (aggregating a concatenation = combining the
+  aggregates; proved, not merely signed). Four concrete instances
+  (`sumMonoid` / `countMonoid` / `maxMonoid` / `minMonoid`, the last
+  over `ℕ ∪ {∞}` via `Maybe ℕ`), a worked `countAggregator`, and
+  generic non-disaggregability `no-canonical-disaggregation-of` (any
+  collision ⇒ no section, via `no-section-of-collapsing-map`; this
+  also discharges issue #174's no-section sibling). The
+  macro→micro *economic* reading lives in `module Example-PairSum`:
+  `pairSum : ℕ × ℕ → ℕ` IS the `sumMonoid` fold (`pairSum-is-fold`),
+  is many-to-one (`pairSum-non-injective`), and has no canonical
+  disaggregation (`no-canonical-disaggregation`) — the
+  Sonnenschein–Mantel–Debreu / representative-agent critique
+  type-theoretically. That instance is the mechanised anchor the
+  oikos/betlang alib note cites (`oikos:docs/alib-aggregate-bridge.adoc`),
+  where it is read at macro scale and named `MacroAggregation`.
+  Consumer of the general form: affinescript db-theory #3 (SQL
+  GROUP-BY as a monoid homomorphism). Honest-bound: `aggregation-as-fold`
+  is the fold's homomorphism law, NOT full SQL GROUP-BY operational
+  semantics; `avg` is deliberately absent (not a monoid — express as
+  `sum / count`). `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

@@ -130,10 +130,16 @@ kernel** — the boundary is real and lives outside this core.
   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.
-  `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`.
+  `EchoAggregation` is the general aggregation form (issue #175):
+  aggregation-as-fold over a `Monoid`, a `GroupAggregator`, the
+  monoid-homomorphism law `aggregation-as-fold`, the four concrete
+  instances (`sumMonoid`/`countMonoid`/`maxMonoid`/`minMonoid`), and
+  generic non-disaggregability `no-canonical-disaggregation-of` (any
+  collision ⇒ no section, via `no-section-of-collapsing-map`; also
+  covers #174).  The macro→micro economic reading is the
+  `Example-PairSum` instance the oikos/betlang alib note cites
+  (`pairSum` IS the `sumMonoid` fold).  Imports `Echo` +
+  `EchoNoSectionGeneric`.
 
 | *Earn-back gate modules* +
 (derived / scoped; not kernel)

docs/echo-types/fibration-package.adoc

@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: MPL-2.0
+// SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = echo-types: The Fibration Package

docs/echo-types/universal-property.adoc

@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: MPL-2.0
+// SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = echo-types: The Universal Property Story

docs/theorem-index.md

@@ -1,5 +1,5 @@
 <!--
-SPDX-License-Identifier: MPL-2.0
+SPDX-License-Identifier: CC-BY-SA-4.0
 Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 <!-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->