Mirror EchoAggregation: monoid fold, homomorphism law, no-canonical-disaggregation

README.adoc

@@ -64,7 +64,10 @@ 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):
+re-export bundle). The unreleased `+EchoAggregation+` entry below is
+mirrored from a later commit,
+`+703dd77af402e959b46f49e8ce2e084521bedbae+`; every other row keeps the
+pin above:
 
 [width="100%",cols="50%,50%",options="header",]
 |===
@@ -136,6 +139,14 @@ 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+`,
+`+aggregate_values+`, `+aggregation_as_fold_holds+`, `+sum_monoid+` /
+`+count_monoid+` / `+max_monoid+` / `+min_monoid+`,
+`+no_canonical_disaggregation_of+`, `+pair_sum+` and its
+`+pair_sum_*+` checks |`+EchoAggregation.agda+` (general monoid/group
+aggregation, echo-types#175; the macro `+pairSum+` ledger is an instance.
+Laws are checked on samples, not proved; `+avg+` is absent because it is
+not a monoid)
 |===
 
 ==== What is intentionally NOT mirrored
@@ -233,8 +244,10 @@ 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). Test suite: *258 passing assertions
-across 19 testsets*, organised as finite shadows of named Agda lemmas
+paired source-side no-section). Unreleased on top of v0.3.0:
+`+EchoAggregation+` (mirrored from echo-types `+703dd77+`, not from
+`+eed4250+`). Test suite:
+*297 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*
 registered in the Julia General registry and intentionally *not* part of

src/EchoTypes.jl

@@ -24,6 +24,11 @@
 # 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
+# aggregation, echo-types#175), mirrored from echo-types origin/main
+# @ 703dd77af402e959b46f49e8ce2e084521bedbae. The rest of this header's
+# provenance pin is unchanged.
+#
 # Retraction discipline (R-2026-05-18): no graded-comonad framing,
 # no universal-property or conservativity claims appear here. F5 (full
 # OFS, honestly funext-qualified) earned back upstream 2026-05-27; the
@@ -88,7 +93,16 @@ export EchoWitness, echo_intro, in_fiber, fiber,
        # EchoLLEncoding (v0.3.0)
        LLShallowEncoding, trivial_encoding,
        trivial_encoding_has_section, ll_encoding_gap,
-       source_no_section_holds, gap_paired
+       source_no_section_holds, gap_paired,
+       # EchoAggregation (unreleased; general monoid/group form, echo-types#175)
+       Monoid, GroupAggregator, monoid_laws_hold,
+       oplus_fold, oplus_fold_append_holds,
+       aggregate_values, aggregation_as_fold_holds,
+       sum_monoid, count_monoid, max_monoid, min_monoid, min_inf,
+       count_aggregator, no_canonical_disaggregation_of,
+       pair_sum, pair_sum_is_fold, ledger1, ledger2,
+       pair_sum_collapses, pair_sum_non_injective,
+       no_canonical_disaggregation_pair_sum
 
 # ======================================================================
 # Kernel — Echo.agda
@@ -1276,4 +1290,182 @@ function gap_paired(linear_samples=(LEcho(true, Linear), LEcho(false, Linear)))
      source_no_section = source_no_section_holds(linear_samples))
 end
 
+# ======================================================================
+# EchoAggregation.agda — aggregation as a monoid fold (echo-types#175)
+#
+# The GENERAL aggregation form: a `Monoid` carrier, a `GroupAggregator`
+# mapping values into it, the fold `⊕-fold`, and the homomorphism law
+# `aggregation-as-fold` (aggregating a concatenation = combining the two
+# aggregates). The macro-economics reading (micro ledger -> macro total,
+# the Sonnenschein–Mantel–Debreu critique) is one INSTANCE, mirrored as
+# the `pair_sum` block below.
+#
+# Finite-shadow caveat: Agda proves `assoc`, `identity-l/r` and the fold
+# law for ALL inputs. Julia can only check them on supplied samples, so
+# every `*_holds` function below is a falsifier on the data it is given,
+# never a proof. `avg` is deliberately absent (not a monoid), as upstream.
+# ======================================================================
+
+"""
+    Monoid(ε, op)
+
+The aggregation carrier (`Monoid`, EchoAggregation.agda): a unit `ε` and
+an associative binary `op` (`_⊕_`). Laws are NOT enforced at construction;
+`monoid_laws_hold` checks them on samples.
+"""
+struct Monoid{E,OP}
+    ε::E
+    op::OP
+end
+
+"""
+    monoid_laws_hold(M, samples) -> Bool
+
+`assoc`, `identity-l`, `identity-r` of `M`, checked over every triple /
+element drawn from `samples`. A `false` is a counterexample; a `true` is
+evidence on those samples only. `samples` is materialised once, so one-shot
+iterators work; an empty `samples` is an error rather than a vacuous `true`.
+"""
+function monoid_laws_hold(M::Monoid, samples)
+    ss = collect(samples)   # materialise once: `samples` is traversed four times
+    isempty(ss) && error("monoid_laws_hold: samples must be non-empty")
+    all(a -> M.op(M.ε, a) == a && M.op(a, M.ε) == a, ss) &&
+        all(t -> M.op(M.op(t[1], t[2]), t[3]) == M.op(t[1], M.op(t[2], t[3])),
+            Iterators.product(ss, ss, ss))
+end
+
+# Items of a finite iterable as a plain Vector in iteration order. `vec` drops
+# any array shape, so `vcat` appends sequences rather than stacking rows.
+_items(xs) = vec(collect(xs))
+
+"""
+    oplus_fold(M, xs)
+
+`⊕-fold`: fold a list (any finite iterable, materialised once as a flat vector) through the
+monoid as a RIGHT fold,
+`x₁ ⊕ (x₂ ⊕ (… ⊕ ε))` (`foldr op ε`), matching Agda's `foldr`. For an
+associative `op` the direction is immaterial; for a non-associative one the
+result depends on it, so this fixes the reading falsifiers are run against.
+"""
+oplus_fold(M::Monoid, xs) = foldr(M.op, _items(xs); init = M.ε)
+
+"""
+    oplus_fold_append_holds(M, xs, ys) -> Bool
+
+`⊕-fold-++`: the fold is a monoid homomorphism on list concatenation,
+`⊕-fold (xs ++ ys) == ⊕-fold xs ⊕ ⊕-fold ys`, checked at `xs`, `ys`.
+"""
+function oplus_fold_append_holds(M::Monoid, xs, ys)
+    # Materialise once: `vcat` of two generators would nest them as elements.
+    xs, ys = _items(xs), _items(ys)
+    oplus_fold(M, vcat(xs, ys)) == M.op(oplus_fold(M, xs), oplus_fold(M, ys))
+end
+
+"""
+    GroupAggregator(agg)
+
+A value -> monoid-element aggregator (`GroupAggregator`,
+EchoAggregation.agda). The group-by key `K` is phantom upstream and has no
+runtime content here.
+"""
+struct GroupAggregator{AG}
+    agg::AG
+end
+
+"""
+    aggregate_values(G, M, vs)
+
+`aggregate-values`: map the aggregator over `vs`, then fold through `M`.
+"""
+aggregate_values(G::GroupAggregator, M::Monoid, vs) =
+    oplus_fold(M, map(G.agg, vs))
+
+"""
+    aggregation_as_fold_holds(G, M, vs, ws) -> Bool
+
+`aggregation-as-fold` (the #175 headline law): aggregating `vs ++ ws`
+equals combining `aggregate_values` of each, checked at `vs`, `ws`.
+Honest scope: the fold's homomorphism property, NOT SQL GROUP-BY's full
+operational semantics.
+"""
+function aggregation_as_fold_holds(G::GroupAggregator, M::Monoid, vs, ws)
+    vs, ws = _items(vs), _items(ws)   # see oplus_fold_append_holds
+    aggregate_values(G, M, vcat(vs, ws)) ==
+        M.op(aggregate_values(G, M, vs), aggregate_values(G, M, ws))
+end
+
+# --- The four concrete instances (ℕ modelled as non-negative Int) -----
+
+"`sumMonoid`: (ℕ, 0, +)."
+sum_monoid() = Monoid(0, +)
+
+"`countMonoid`: the SAME monoid as `sum_monoid`; counting happens in the aggregator."
+count_monoid() = sum_monoid()
+
+"`maxMonoid`: (ℕ, 0, max). 0 is the max-identity on ℕ."
+max_monoid() = Monoid(0, max)
+
+"""
+    min_inf(a, b)
+
+`_⊓∞_`: min over ℕ ∪ {∞}, with `nothing` = ∞ (the min-identity) and an
+`Int` standing for `just n`.
+"""
+min_inf(a::Nothing, b::Union{Nothing,Integer}) = b
+min_inf(a::Integer, b::Nothing) = a
+min_inf(a::Integer, b::Integer) = min(a, b)
+
+"`minMonoid`: (ℕ ∪ {∞}, ∞, ⊓∞) with `nothing` = ∞."
+min_monoid() = Monoid(nothing, min_inf)
+
+"`countAggregator`: every value contributes 1 to the sum monoid."
+count_aggregator() = GroupAggregator(_ -> 1)
+
+"""
+    no_canonical_disaggregation_of(agg_map, x, y) -> Bool
+
+`no-canonical-disaggregation-of`: an aggregation map with a collision
+(`x != y`, `agg_map(x) == agg_map(y)`) admits no section. This is
+`no_section_of_collapsing_map` under aggregation-flavoured names, as
+upstream. It refutes a *section* (a left inverse), NOT the existence of
+some representative choice.
+"""
+no_canonical_disaggregation_of(agg_map, x, y) =
+    no_section_of_collapsing_map(agg_map, x, y)
+
+# --- Example-PairSum: the macro instance (ℕ × ℕ -> ℕ by +) -------------
+
+"`pairSum (a , b) = a + b`."
+pair_sum(p::Tuple{Integer,Integer}) = p[1] + p[2]
+
+"""
+    pair_sum_is_fold(p) -> Bool
+
+`pairSum-is-fold`: `pair_sum` IS the `sum_monoid` fold of its two fields,
+so the macro instance is a special case of the general form.
+"""
+pair_sum_is_fold(p::Tuple{Integer,Integer}) =
+    pair_sum(p) == oplus_fold(sum_monoid(), [p[1], p[2]])
+
+"`ledger₁ = (0 , 1)`."
+ledger1() = (0, 1)
+
+"`ledger₂ = (1 , 0)`."
+ledger2() = (1, 0)
+
+"`pairSum-collapses`: both ledgers aggregate to 1."
+pair_sum_collapses() = pair_sum(ledger1()) == pair_sum(ledger2())
+
+"""
+    pair_sum_non_injective() -> Bool
+
+`pairSum-non-injective`: the two echoes over total 1 are distinct.
+"""
+pair_sum_non_injective() =
+    echo_intro(pair_sum, ledger1()) != echo_intro(pair_sum, ledger2())
+
+"`Example-PairSum.no-canonical-disaggregation`: no section of `pair_sum`."
+no_canonical_disaggregation_pair_sum() =
+    no_canonical_disaggregation_of(pair_sum, ledger1(), ledger2())
+
 end # module EchoTypes

test/runtests.jl

@@ -432,4 +432,96 @@ using Test
         @test gp.encoded_section
         @test gp.source_no_section
     end
+
+    # ------------------------------------------------------------------
+    # EchoAggregation (general monoid/group form, echo-types#175; mirrors
+    # echo-types main @ 703dd77). Finite shadow: laws are checked on
+    # samples, never proved. HONEST BOUND: the fold's homomorphism law,
+    # NOT SQL GROUP-BY semantics; `avg` is absent (not a monoid).
+    # ------------------------------------------------------------------
+
+    @testset "Aggregation: monoid fold + homomorphism law (EchoAggregation.agda)" begin
+        nat = 0:6
+        for M in (sum_monoid(), count_monoid(), max_monoid())
+            @test monoid_laws_hold(M, nat)
+        end
+        # min over ℕ ∪ {∞}: `nothing` is ∞.
+        mins = [nothing; collect(nat)]
+        @test monoid_laws_hold(min_monoid(), mins)
+
+        # Falsifier: a non-monoid is rejected (subtraction is not associative;
+        # 0 is only a right identity), so `monoid_laws_hold` can say `false`.
+        @test !monoid_laws_hold(Monoid(0, -), nat)
+
+        # Samples are materialised once (one-shot iterators work) and an
+        # empty sample is an error, not a vacuous `true`.
+        @test monoid_laws_hold(sum_monoid(), (x for x in nat))
+        @test_throws ErrorException monoid_laws_hold(sum_monoid(), Int[])
+
+        # `min_inf` keeps its domain closed: ℕ ∪ {∞} only.
+        @test min_inf(nothing, nothing) === nothing
+        @test_throws MethodError min_inf(nothing, "x")
+
+        # ⊕-fold is a RIGHT fold: for non-associative `-` it is 1-(2-(3-0)).
+        @test oplus_fold(Monoid(0, -), [1, 2, 3]) == 2
+
+        # ⊕-fold-++ at each instance.
+        @test oplus_fold_append_holds(sum_monoid(), [1, 2, 3], [4, 5])
+        @test oplus_fold_append_holds(max_monoid(), [1, 5, 3], [4, 2])
+        @test oplus_fold_append_holds(min_monoid(), [3, nothing, 1], [4, 2])
+        @test oplus_fold_append_holds(sum_monoid(), Int[], [4, 5])
+        @test oplus_fold_append_holds(min_monoid(), Union{Nothing,Int}[], Union{Nothing,Int}[])
+
+        # Generators / lazy iterables are accepted (not nested by `vcat`).
+        @test oplus_fold_append_holds(sum_monoid(), (x for x in 1:2), (y for y in 3:4))
+        @test oplus_fold_append_holds(sum_monoid(), (x for x in 1:6 if x > 2), (y for y in 3:4))
+        @test aggregation_as_fold_holds(count_aggregator(), sum_monoid(),
+                                        (v for v in 1:2), (v for v in 3:5))
+        @test oplus_fold(sum_monoid(), (x for x in 1:3 if x > 1)) == 5
+
+        # Arrays of any shape are read as their flat iteration sequence, so
+        # `vcat` appends them rather than stacking rows (non-commutative `*`).
+        S = Monoid("", *)
+        @test oplus_fold_append_holds(S, ["a" "b"], ["c" "d"])
+        @test aggregation_as_fold_holds(GroupAggregator(identity), S, ["a" "b"], ["c" "d"])
+        @test oplus_fold(S, ["a" "b"; "c" "d"]) == "acbd"   # column-major order
+
+        # Concrete fold values.
+        @test oplus_fold(sum_monoid(), [1, 2, 3]) == 6
+        @test oplus_fold(max_monoid(), [1, 5, 3]) == 5
+        @test oplus_fold(min_monoid(), [3, 1, 2]) == 1
+        @test oplus_fold(min_monoid(), Union{Nothing,Int}[]) === nothing   # empty min = ∞
+
+        # aggregation-as-fold with the worked count aggregator:
+        # count of a concatenation = sum of the counts.
+        C = count_aggregator()
+        @test aggregate_values(C, sum_monoid(), [:a, :b, :c]) == 3
+        @test aggregate_values(C, sum_monoid(), Symbol[]) == 0
+        @test aggregation_as_fold_holds(C, sum_monoid(), [:a, :b], [:c, :d, :e])
+
+        # A value-dependent aggregator over max.
+        G = GroupAggregator(v -> v.price)
+        rows = [(price = 3,), (price = 9,), (price = 4,)]
+        @test aggregate_values(G, max_monoid(), rows) == 9
+        @test aggregation_as_fold_holds(G, max_monoid(), rows[1:1], rows[2:3])
+    end
+
+    @testset "Aggregation: Example-PairSum macro instance + no-section (EchoAggregation.agda)" begin
+        # pairSum is the sumMonoid fold of its two fields.
+        @test all(pair_sum_is_fold, [(a, b) for a in 0:4 for b in 0:4])
+
+        # Many-to-one: distinct ledgers, one total, distinct echoes.
+        @test pair_sum_collapses()
+        @test ledger1() != ledger2()
+        @test pair_sum_non_injective()
+        @test in_fiber(pair_sum, echo_intro(pair_sum, ledger1()), 1)
+        @test in_fiber(pair_sum, echo_intro(pair_sum, ledger2()), 1)
+
+        # Keystone: no canonical disaggregation (no section).
+        @test no_canonical_disaggregation_pair_sum()
+
+        # Matched negative: an injective aggregation has no collision to
+        # exhibit, so the witness correctly does not fire.
+        @test !no_canonical_disaggregation_of(identity, ledger1(), ledger2())
+    end
 end