diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index 80be390..39cc766 100644 --- a/docs/echo-types/MAP.adoc +++ b/docs/echo-types/MAP.adoc @@ -253,6 +253,17 @@ 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]` *Curated suite — single-file entry point.* The narrative deliverable that pulls the Tier-1 / Tier-2 / Tier-3 named theorems diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc index e891627..45799aa 100644 --- a/docs/echo-types/echo-kernel-note.adoc +++ b/docs/echo-types/echo-kernel-note.adoc @@ -124,12 +124,16 @@ kernel** — the boundary is real and lives outside this core. residue / decoration / observational classifications. *Application/extension modules* (also added via the same sweep): `EchoEntropy`, `EchoLLEncoding`, `EchoProvenance`, `EchoSecurity`, - `EchoProbabilisticSupport`, `EchoDifferential`, `EchoDeniability` + `EchoProbabilisticSupport`, `EchoDifferential`, `EchoDeniability`, + `EchoAggregation` are derived domain applications mapped under their own headings in 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. - Imports `Echo` + `EchoNoSectionGeneric`. + `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`. | *Earn-back gate modules* + (derived / scoped; not kernel) diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 49a4eb2..6ddd59c 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -11,6 +11,7 @@ open import EchoOrthogonalFactorizationSystem open import EchoImageFactorization open import EchoImageFactorizationProp open import EchoNoSectionGeneric +open import EchoAggregation open import EchoLossTaxonomy open import EchoResidueTaxonomy open import EchoDecorationStructure diff --git a/proofs/agda/EchoAggregation.agda b/proofs/agda/EchoAggregation.agda new file mode 100644 index 0000000..3f28ecf --- /dev/null +++ b/proofs/agda/EchoAggregation.agda @@ -0,0 +1,188 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell + +-- EchoAggregation: micro→macro economic aggregation as structured loss. +-- +-- This module mechanises the keystone claim of the oikos/betlang +-- "aggregate library" design note (oikos +-- `docs/alib-aggregate-bridge.adoc` §2): economic *aggregation* — +-- rolling a micro ledger up into a macro observable — is literally an +-- `Echo` map, and the *non-identifiability* of the micro state from +-- the macro observable ("you cannot disaggregate") is literally the +-- repo's `no-section` theorem. +-- +-- The honest minimal instance. The alib's `MacroState` is a rich +-- record (population, elites, capital stock, …). Each of its fields +-- is an aggregation of the same shape: a sum (a Godley column) of +-- micro entries. The load-bearing structural fact is visible already +-- at the smallest faithful case — a two-account ledger collapsing to +-- a total: +-- +-- * `MicroLedger = ℕ × ℕ` two sector balances (e.g. household, +-- firm) — the micro state; +-- * `MacroTotal = ℕ` the aggregate money stock — one Godley +-- column sum, the macro observable; +-- * `aggregate (a , b) = a + b` the rollup. +-- +-- The full `MacroState` is then a product of such projections; the +-- structural story (many-to-one ⇒ no canonical disaggregation) is +-- identical field-by-field, so the single-column instance is the +-- right place to pin it. +-- +-- What is proved. +-- +-- * `ConsistentLedgers m = Echo aggregate m` — the fibre: ALL micro +-- ledgers consistent with the macro total `m`. This IS the +-- economist's "aggregation is many-to-one", as a type. +-- * `aggregate-non-injective` — two distinct micro ledgers, +-- `(0,1)` and `(1,0)`, are distinct echoes at the SAME macro +-- total `1`. The fibre is genuinely non-trivial. +-- * `no-canonical-disaggregation` (keystone) — `aggregate` admits +-- NO section: there is no `raise : MacroTotal → MicroLedger` +-- recovering the micro split from the macro total for every +-- input. This is the aggregation / non-identifiability problem, +-- as a theorem, obtained by instantiating the generic +-- `EchoNoSectionGeneric.no-section-of-collapsing-map`. +-- +-- This is the SAME `no-section` machinery that underwrites the +-- affine⊑linear story in the wasm proof layer (`EchoLinear.weaken`, +-- machine-checked equal to AffineScript subtyping in +-- `nextgen-typing`'s `EchoTyping.agda`). One type language serves +-- micro→macro aggregation, cross-language ABI, and uncertainty. +-- +-- Headlines (pinned in Smoke.agda): +-- +-- * aggregate -- the rollup map +-- * ConsistentLedgers -- its fibre, as an Echo +-- * aggregate-non-injective -- the fibre is non-trivial +-- * no-canonical-disaggregation -- the keystone: no section +-- +-- Scope guardrail. `aggregate` here is a concrete finite ℕ-valued +-- map; the theorem is about THIS map's non-injectivity. It does NOT +-- claim a quantitative bound on the size of fibres, nor anything +-- about the rich `MacroState` record's joint identifiability — those +-- are downstream, and named in the alib note's open questions. The +-- minimal claim is exactly the load-bearing one: aggregation is an +-- Echo, and the macro observable cannot in general be disaggregated. + +module EchoAggregation where + +open import Echo using (Echo; echo-intro) +open import EchoNoSectionGeneric using (no-section-of-collapsing-map) + +open import Data.Nat.Base using (ℕ; _+_) +open import Data.Product.Base using (Σ; _×_; _,_; proj₁) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl; cong) +open import Relation.Nullary using (¬_) + +---------------------------------------------------------------------- +-- The micro / macro types and the aggregation map. +---------------------------------------------------------------------- + +-- A micro ledger: two sector balances (e.g. household, firm). +MicroLedger : Set +MicroLedger = ℕ × ℕ + +-- The macro observable: one aggregate total (a Godley column sum). +MacroTotal : Set +MacroTotal = ℕ + +-- Aggregation: roll the micro ledger up into the macro total. +aggregate : MicroLedger → MacroTotal +aggregate (a , b) = a + b + +---------------------------------------------------------------------- +-- The fibre, as an Echo. +-- +-- `ConsistentLedgers m` is the type of ALL micro ledgers whose rollup +-- is exactly the macro total `m`. Definitionally it is +-- `Σ MicroLedger (λ l → aggregate l ≡ m)` — the fibre of `aggregate` +-- over `m`. "Aggregation is many-to-one" becomes "this type can have +-- more than one inhabitant" (witnessed below). +---------------------------------------------------------------------- + +ConsistentLedgers : MacroTotal → Set +ConsistentLedgers m = Echo aggregate m + +---------------------------------------------------------------------- +-- The fibre over macro total 1 is non-trivial: two distinct micro +-- ledgers, (0,1) and (1,0), both aggregate to 1. +---------------------------------------------------------------------- + +ledger₁ : MicroLedger +ledger₁ = 0 , 1 + +ledger₂ : MicroLedger +ledger₂ = 1 , 0 + +-- The two micro ledgers are distinct: their household balances differ +-- (0 vs 1). Refuted at the first projection by constructor clash. +ledger₁≢ledger₂ : ledger₁ ≢ ledger₂ +ledger₁≢ledger₂ eq with cong proj₁ eq +... | () + +-- … yet they collapse to the same macro total (both 1). +aggregate-collapses : aggregate ledger₁ ≡ aggregate ledger₂ +aggregate-collapses = refl + +-- As echoes at the same macro total. +echo-ledger₁ : ConsistentLedgers 1 +echo-ledger₁ = echo-intro aggregate ledger₁ + +echo-ledger₂ : ConsistentLedgers 1 +echo-ledger₂ = echo-intro aggregate ledger₂ + +-- The fibre is genuinely non-trivial: two distinct inhabitants at the +-- same macro observable. This is "aggregation is many-to-one", as a +-- checked theorem. +aggregate-non-injective : echo-ledger₁ ≢ echo-ledger₂ +aggregate-non-injective eq = ledger₁≢ledger₂ (cong proj₁ eq) + +---------------------------------------------------------------------- +-- The keystone: no canonical disaggregation. +-- +-- There is no section `raise : MacroTotal → MicroLedger` recovering +-- the micro split from the macro total for every input — i.e. no +-- function with `raise (aggregate l) ≡ l` for all micro ledgers `l`. +-- This is the aggregation / non-identifiability problem of +-- macroeconomics, obtained as a one-instance application of the +-- generic no-section theorem. +---------------------------------------------------------------------- + +no-canonical-disaggregation : + ¬ Σ (MacroTotal → MicroLedger) + (λ raise → ∀ l → raise (aggregate l) ≡ l) +no-canonical-disaggregation = + no-section-of-collapsing-map + aggregate + ledger₁ ledger₂ + ledger₁≢ledger₂ + aggregate-collapses + +---------------------------------------------------------------------- +-- Companion remark. +-- +-- Why this is the right level of generality: +-- +-- * The fibre `ConsistentLedgers m` is `Echo aggregate m` ON THE +-- NOSE (definitional), so every downstream `Echo`/`EchoResidue` +-- result applies to aggregation without restatement. In +-- particular the residue machinery names what the macro layer is +-- entitled to observe after the loss. +-- +-- * `no-canonical-disaggregation` refutes a LEFT inverse (a +-- section of `aggregate`). It does NOT refute the existence of +-- SOME right inverse / choice of representative — economists pick +-- representatives all the time (a "typical household"). The +-- content is precisely that no such choice is CANONICAL: it +-- cannot satisfy `raise ∘ aggregate ≡ id`, so it always discards +-- information about ledgers it did not pick. +-- +-- * Promoting this to the rich `MacroState` record is mechanical: +-- each field is an aggregation of this shape, and a section of +-- the product would restrict to a section of each projection, +-- which this theorem already refutes. No new proof idea is +-- needed; see the alib note §3–§4. +---------------------------------------------------------------------- diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 4fb697c..52c435f 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -108,6 +108,23 @@ open import EchoNoSectionGeneric using ; no-section-when-non-injective-at-y ) +-- EchoAggregation — micro→macro economic aggregation as structured +-- loss (the oikos/betlang "aggregate library" keystone). `aggregate` +-- rolls a two-account ledger up into a Godley column total; its fibre +-- `ConsistentLedgers m = Echo aggregate m` is the set of micro states +-- consistent with the macro observable. `aggregate-non-injective` +-- pins "aggregation is many-to-one"; `no-canonical-disaggregation` +-- pins the non-identifiability theorem (no section of `aggregate`) +-- via `no-section-of-collapsing-map`. +open import EchoAggregation using + ( aggregate + ; ConsistentLedgers + ; ledger₁≢ledger₂ + ; aggregate-collapses + ; aggregate-non-injective + ; no-canonical-disaggregation + ) + -- EchoImageFactorization — image-factorisation triangle in Echo -- language. `Image f := Σ B (Echo f)` IS the total Echo space. -- Three classifications (Surjective / Injective / projection-