Add EchoAggregation module — Monoid + GroupAggregator carriers for SQL aggregation-as-fold (consumer: affinescript db-theory #3)

[hyperpolymath]

Context (consumer)

AffineScript ships db-theory #3 in the next PR — a new stdlib/Aggregate.affine module exposing SQL group-by + aggregation primitives (count / sum / min / max / avg) plus a db_group_by convenience returning the grouped result-set as JSON. The proof-relevant property is the classical aggregation-as-monoid-homomorphism claim (Green / Karvounarakis / Tannen, provenance semirings): each aggregator is a commutative monoid; group-by is the indexed sum.

Sibling to echo-types#174 (Transaction safety / no-section-of-collapsing-map).

Audit summary (2026-06-01)

Echo-types currently carries no reusable monoid/semiring infrastructure. The closest scaffolding:

1. EchoCost.CostAlgebra — left-identity + monotonicity, no composition law. Reusable as a Monoid instance once Monoid exists.
2. Ordinal/Brouwer/OmegaPow.agda#additive-principal — exactly the monoid closure property for ω^n exponents.
3. EchoDecorationStructure.agda — observer-level lattice, not data-level algebra.

docs/adjacency/provenance-semirings.adoc already names the relevant distinctness story (echo adds types; semirings add scalars; this module bridges both).

Proposed module shape

module EchoAggregation where

open import Level using (Level; suc)
open import Relation.Binary.PropositionalEquality using (_≡_)

record Monoid (ℓ : Level) : Set (suc ℓ) where
 field
 Elem : Set ℓ
 ε : Elem
 _⊕_ : Elem → Elem → Elem
 assoc : ∀ a b c → (a ⊕ b) ⊕ c ≡ a ⊕ (b ⊕ c)
 identity-l : ∀ a → ε ⊕ a ≡ a
 identity-r : ∀ a → a ⊕ ε ≡ a

-- A GroupAggregator over keys K, values V, monoid M is the data of:
-- an aggregator agg : V → M.Elem
-- that lifts to a fold over rows, indexed by their K-key.
record GroupAggregator {ℓ} (K V : Set) (M : Monoid ℓ) : Set ℓ where
 open Monoid M
 field
 agg : V → Elem
 -- Headline lemma (proof TBD upstream; consumer references):
 -- aggregation-as-fold :
 -- (rows : List (K × V)) →
 -- aggregate-by-key (partition rows by .fst)
 -- (λ vs → foldr (λ v acc → agg v ⊕ acc) ε vs)
 -- ≡ the actual SQL GROUP-BY semantics.

-- Concrete instances:
-- countMonoid : Monoid ℓ-zero (ℕ, 0, +)
-- sumMonoid : Monoid ℓ-zero (ℕ, 0, +)
-- minMonoid : Monoid ℓ-zero (ℕ ∪ {∞}, ∞, min)
-- maxMonoid : Monoid ℓ-zero (ℕ ∪ {-∞}, -∞, max)
-- -- avg is NOT a monoid (no identity); express as sum / count.

Why this matters

• Bridge between the existing EchoCost ordered-monoid sketch (now formalisable as a Monoid instance) and the provenance-semirings.adoc adjacency.
• Foundation for downstream proof obligations: db-theory E3 CNF trichotomy + E4 pedagogical psi least-gap #4 (selection / filtered projection — distributivity of agg over filter), db-theory E5: make ν operational and add Buchholz example/smoke modules #6 (B+ tree / hash indices — agg over indexed scans), and db-theory Add partial _<ᵇ_ order on Buchholz terms (WF-0, partial) #9 (CRDTs — OR-Set / GCounter are monoid instances with convergence).
• Acceptance criteria: zero new axioms (Print Assumptions clean); concrete countMonoid / sumMonoid / minMonoid / maxMonoid instances; signature for aggregation-as-fold (the proof itself may follow in a stacked PR).

Cross-doc

• Consumer cross-doc lands at affinescript/docs/academic/proofs/db-theory-3-aggregation-as-fold.md and back-links this issue.
• Sibling: echo-types#174 (Transaction safety / no-section-of-collapsing-map).