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

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).