feat(aggregation): generalize EchoAggregation to monoid/group form (#175)

Generalize EchoAggregation from the macro-economics-specific module
into the general monoid-aggregation form requested by #175 (the SQL
GROUP-BY-as-monoid-homomorphism consumer in affinescript db-theory #3):

  * record Monoid (Elem/ε/_⊕_/assoc/identity-l/identity-r);
  * ⊕-fold + ⊕-fold-++ (fold is a monoid homomorphism over _++_);
  * record GroupAggregator (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 (Maybe ℕ,
    nothing = ∞) + a worked countAggregator;
  * no-canonical-disaggregation-of — generic non-disaggregability
    (any collision ⇒ no section, via no-section-of-collapsing-map);
    this also discharges #174's no-section sibling.

The macro→micro economics reading survives mechanised as
module Example-PairSum (pairSum : ℕ × ℕ → ℕ IS the sumMonoid fold —
pairSum-is-fold — so it is an instance of the general form, nothing
re-proved or lost): pairSum-non-injective + no-canonical-disaggregation
(the Sonnenschein–Mantel–Debreu / representative-agent critique
type-theoretically). oikos reads that instance at macro scale under
the name MacroAggregation, cited back here.

--safe --without-K, zero postulates, kernel-guard PASS; All.agda +
Smoke.agda exit 0. Smoke pins + MAP.adoc + echo-kernel-note.adoc +
cross-repo-bridge-status.md swept to the general/macro split.

Refs #175, #174

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

Author: claude

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

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)