Mirror the general EchoAggregation into the EchoTypes.jl finite-domain falsifier #280

Context

The general monoid/group EchoAggregation landed in echo-types (proofs/agda/EchoAggregation.agda, #175). EchoTypes.jl (hyperpolymath/EchoTypes.jl) is the executable Julia companion that mirrors echo-types' finite-domain shadow and falsifies-by-counterexample on concrete data — the Agda stays the source of truth. The EchoAggregation result is not yet mirrored there.

A paste-ready handoff prompt is committed at docs/handoffs/ECHOTYPES-JL-MIRROR-NEXT-CLAUDE-2026-06-27.adoc (PR #279, merged). Open a fresh session in an EchoTypes.jl checkout and paste the block under [#the-prompt].

Scope note

The work happens in the separate EchoTypes.jl repo, which is outside the current agent MCP repo-scope (cf. #263's new ordinal repo). This issue tracks the disposition; echo-types only holds the spec being mirrored.

What to build (Julia, executable, property-tested)

• A Monoid struct (carrier / ε / ⊕) + ⊕fold over a Vector, with a property test of the homomorphism law ⊕fold(m, vcat(xs, ys)) == ⊕fold(m, xs) ⊕ ⊕fold(m, ys) on random finite data.
• Instances sumMonoid / countMonoid / maxMonoid over Int and minMonoid over Union{Nothing,Int} (nothing = ∞); property-test each one's identity + associativity laws.
• aggregate_values(agg, kvs) + a test of aggregation-as-fold.
• pairsum((a,b)) = a + b with tests: pairsum_is_fold (equals the sumMonoid fold of [a,b]), non-injectivity, and no-canonical-disaggregation (no raise satisfies raise ∘ pairsum == id — two pairs share a total).

Honest scope (preserve — do not overclaim)

• aggregation-as-fold is the fold's monoid-homomorphism law, NOT SQL GROUP-BY operational semantics.
• avg is deliberately absent (not a monoid) — express as sum / count.
• no-canonical-disaggregation refutes a section (a LEFT inverse), not the existence of some representative choice. Do not restate it as a failed surjection (the aggregate map is onto).

Acceptance

• EchoAggregation module + @testset added to EchoTypes.jl; Pkg.test() green.
• Homomorphism + per-instance laws property-tested on random finite data.
• pairsum trio (is-fold / non-injective / no-canonical-disaggregation) witnessed on concrete collisions.
• Draft PR opened on claude/ecstatic-wright-OBEvx, cross-referencing echo-types Add EchoAggregation module — Monoid + GroupAggregator carriers for SQL aggregation-as-fold (consumer: affinescript db-theory #3) #175.

Filed at owner request to capture remaining work on the master scheduler.