From 4e9e1c33a7433d4a52f3d554eb45d84e32572b0b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 17:54:27 +0000 Subject: [PATCH 1/3] =?UTF-8?q?Ordinal/Buchholz:=20checked=20refutation=20?= =?UTF-8?q?of=20rank-pow=20monotonicity=20at=20the=20<=E1=B5=87-+1=20?= =?UTF-8?q?=CF=88/=CE=A9=20cross-head=20boundary?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds Ordinal.Buchholz.RankPowMonoRefuted: a machine-checked counterexample showing the provisional rank-pow is not a monotone embedding of _<ᵇ_, even restricted to WfCNF terms. Exhibits WfCNF s, t with s <ᵇ t yet rank-pow t <′ rank-pow s (strict reversal) at the joint-bplus equal-marker boundary (bpsi ν _ vs bOmega ν). This sharpens the RankLexSlice3 / RankMonoUmbrellaSlice4 "open at the bplus-chain level" verdict to "false for this rank": it refutes the rank-mono GOAL directly (complementing the route refutations StrictLeftMonoRefuted / AdditivePrincipalGenericRefuted), upgrades the Slice 4 <ᵇ⁻ⁿ-shortfall-equal-head ⊤-alias placeholder to a checked theorem, and pins exactly the cross-head case the RankLexJointBplus rank-lex-jb pivot is load-bearing for. Headlines: s, t, wf-s, wf-t, s<ᵇt, rank-pow-strictly-reverses, RankPowMono/rank-pow-mono-refuted, RankPowMonoPlus1/rank-pow-mono-plus1-refuted. Wired into All.agda; pinned in Ordinal/Buchholz/Smoke.agda. --safe --without-K, zero postulates; All.agda + Smoke.agda + kernel-guard.sh all exit 0. https://claude.ai/code/session_01VwbFNQJw23tW8tqM7utWku --- proofs/agda/All.agda | 1 + .../Ordinal/Buchholz/RankPowMonoRefuted.agda | 244 ++++++++++++++++++ proofs/agda/Ordinal/Buchholz/Smoke.agda | 23 ++ 3 files changed, 268 insertions(+) create mode 100644 proofs/agda/Ordinal/Buchholz/RankPowMonoRefuted.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 8ffa1bd..d20de94 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -152,6 +152,7 @@ open import Ordinal.Buchholz.HeadOmegaInversion open import Ordinal.Buchholz.RankPowDomination open import Ordinal.Buchholz.RankPowSlice3 open import Ordinal.Buchholz.RankPowSlice3Headline +open import Ordinal.Buchholz.RankPowMonoRefuted open import Ordinal.Buchholz.RankDoubledLadder open import Ordinal.Buchholz.RankDoubledLadderMono open import Ordinal.Buchholz.RankDoubledLadderMonoPlus diff --git a/proofs/agda/Ordinal/Buchholz/RankPowMonoRefuted.agda b/proofs/agda/Ordinal/Buchholz/RankPowMonoRefuted.agda new file mode 100644 index 0000000..6f0975f --- /dev/null +++ b/proofs/agda/Ordinal/Buchholz/RankPowMonoRefuted.agda @@ -0,0 +1,244 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell + +-- Checked refutation: the provisional `rank-pow` is NOT a monotone +-- order-embedding of `_<ᵇ_` — not even restricted to WfCNF terms. It +-- STRICTLY REVERSES a concrete `<ᵇ` step at the `<ᵇ-+1` joint-bplus +-- ψ/Ω equal-marker boundary. +-- +-- ## Why this matters (sharpening the Slice 3 "open" verdict) +-- +-- `Ordinal.Buchholz.RankPowSlice3Headline.rank-mono-<ᵇ-+1-via-head-Ω` +-- closes the joint-bplus rank-mono case only UNDER A STRICT-HEAD +-- PREMISE `head-Ω x₁ <Ω head-Ω y₁`, and +-- `Ordinal.Buchholz.RankMonoUmbrellaSlice3._<ᵇ¹_` bakes that premise +-- into its joint-bplus constructor `<ᵇ¹-+1-+`. The equal-head +-- remainder (`head-Ω x₁ ≡ head-Ω y₁`) is documented in +-- `Ordinal.Buchholz.RankLexSlice3`'s design note as "CLOSED at the +-- ψ-rank level, OPEN at the bplus-chain level pending one of +-- (a)/(b)/(c)". +-- +-- This module sharpens that verdict from "open / unproven" to +-- "FALSE". The equal-head joint-bplus rank-mono statement does not +-- merely lack a proof for the current `rank-pow`: it has a +-- counterexample. No strengthening of the proof effort closes it. +-- The defect is structural — `rank-pow (bpsi ν _) = ω-rank-pow ν = +-- rank-pow (bOmega ν)` (`RankPow.agda:163,165`) gives ψ_ν(α) and Ω_ν +-- the SAME rank, so `rank-pow` cannot see the strict gap ψ_ν(α) < Ω_ν +-- that the intended ordinal semantics has. Closing the equal-head +-- case REQUIRES a different rank: one that places ψ_ν(α) strictly +-- below Ω_ν at a shared marker (option (c) of the RankLexSlice3 +-- design note — the non-local rank redesign). +-- +-- This is the `rank-pow`-level companion to the two Brouwer-arithmetic +-- refutations the closure routes lean on: +-- * `Ordinal.Brouwer.StrictLeftMonoRefuted` (route (b)), +-- * `Ordinal.Brouwer.AdditivePrincipalGenericRefuted` (route (a)). +-- Those refute the arithmetic lemmas a `rank-pow`-level closure would +-- have to consume. This module is more direct: it refutes the +-- rank-monotonicity GOAL itself, so a future session sees immediately +-- that the equal-head case is unreachable with this rank and does not +-- re-attempt it. Concretely it UPGRADES the placeholder matched- +-- negative `Ordinal.Buchholz.RankMonoUmbrellaSlice4. +-- <ᵇ⁻ⁿ-shortfall-equal-head` (a bare `⊤`-alias) to a checked +-- counterexample, in the same "promote a placeholder to a theorem" +-- spirit as `StrictLeftMonoRefuted`. +-- +-- The witness sits at the CROSS-HEAD flavour of the boundary — +-- `bpsi ν _` vs `bOmega ν` (syntactically distinct, `rank-pow`-equal) +-- — which `Ordinal.Buchholz.RankLexJointBplus` flags as the case its +-- `rank-lex-jb` pivot remains load-bearing for. This refutation is +-- exactly why that pivot to a DIFFERENT rank (one whose `bplus` +-- second component carries `leftmost-α`, placing ψ_ν(α) below Ω_ν) is +-- the only viable forward path: the present `rank-pow` cannot be +-- repaired into monotonicity here, it must be replaced. +-- +-- ## The witness (BOTH terms WfCNF) +-- +-- s = bplus (bpsi (fin 0) bzero) (bpsi (fin 0) bzero) -- ψ₀(0) + ψ₀(0) +-- t = bplus (bOmega (fin 0)) bzero -- Ω₀ + 0 +-- +-- * `s <ᵇ t` via `<ᵇ-+1 (<ᵇ-ψΩ≤ (fin 0 ≤Ω fin 0))`: the source's +-- leading summand ψ₀(0) is `<ᵇ` the target's leading summand Ω₀ +-- at the EQUAL marker fin 0 — exactly the `<ᵇ-ψΩ≤` boundary that +-- `head-Ω-inv-bpsi` can only bound non-strictly. +-- * Yet `rank-pow t = ω¹ ⊕ oz <′ ω¹ ⊕ ω¹ = rank-pow s`: `rank-pow` +-- ranks the SOURCE strictly ABOVE the TARGET, because both leading +-- summands collapse to ω¹ = `ω-rank-pow (fin 0)` and the source +-- carries a second ψ₀(0) summand while the target's tail is 0. +-- +-- Ordinally `s` really is below `t` (ψ₀(0)·2 < Ω₀, since Ω₀ is +-- additively principal); the reversal is purely an artefact of +-- `rank-pow`'s α-blind, ψ/Ω-collapsing shape. +-- +-- ## Headlines (pinned in `Ordinal/Buchholz/Smoke.agda`) +-- +-- * `s`, `t`, `wf-s`, `wf-t`, `s<ᵇt` -- the witness data +-- * `rank-pow-strictly-reverses` -- rank-pow t <′ rank-pow s +-- * `RankPowMono`, `rank-pow-mono-refuted` +-- -- ¬ (WfCNF rank-monotonicity) +-- * `RankPowMonoPlus1`, `rank-pow-mono-plus1-refuted` +-- -- ¬ (joint-bplus, no strict-head) + +module Ordinal.Buchholz.RankPowMonoRefuted where + +open import Data.Nat.Base using (zero; suc; z≤n) +open import Data.Empty using (⊥) +open import Data.Sum.Base using (inj₁; inj₂) +open import Relation.Nullary using (¬_) +open import Relation.Binary.PropositionalEquality using (refl) +open import Induction.WellFounded using (Acc; acc) + +open import Ordinal.Brouwer using (oz; osuc) +open import Ordinal.Brouwer.Phase13 using + ( _≤′_ + ; _<′_ + ; ≤′-zero + ; ≤′-trans + ; ⊕-mono-<-right + ; ⊕-mono-≤-right + ; wf-<′ + ) +open import Ordinal.Brouwer.OmegaPow using (ω^_; ω^_-pos) +open import Ordinal.OmegaMarkers using (fin; _≤Ω_; fin≤fin) +open import Ordinal.Buchholz.Syntax using + ( BT; bzero; bOmega; bplus; bpsi ) +open import Ordinal.Buchholz.Order using + ( _<ᵇ_; <ᵇ-0-Ω; <ᵇ-ψΩ≤; <ᵇ-+1 ) +open import Ordinal.Buchholz.WellFormed using (wf-fin) +open import Ordinal.Buchholz.WellFormedCNF using + ( WfCNF + ; wf-cnf-bzero + ; wf-cnf-bomega + ; wf-cnf-bpsi + ; wf-cnf-bplus + ; atomic-bzero + ; atomic-bpsi + ) +open import Ordinal.Buchholz.RankPow using (rank-pow) + +---------------------------------------------------------------------- +-- The witness terms +---------------------------------------------------------------------- + +-- s = ψ₀(0) + ψ₀(0); t = Ω₀ + 0. Both in Cantor normal form. +s : BT +s = bplus (bpsi (fin 0) bzero) (bpsi (fin 0) bzero) + +t : BT +t = bplus (bOmega (fin 0)) bzero + +---------------------------------------------------------------------- +-- Both witnesses are WfCNF +---------------------------------------------------------------------- + +-- s: left = ψ₀(0) (WfCNF), right = ψ₀(0) (atomic), tail bound by +-- equality (ψ₀(0) ≤ᵇ ψ₀(0) via `inj₂ refl`). +wf-s : WfCNF s +wf-s = + wf-cnf-bplus + (wf-cnf-bpsi wf-fin wf-cnf-bzero) + (wf-cnf-bpsi wf-fin wf-cnf-bzero) + atomic-bpsi + (inj₂ refl) + +-- t: left = Ω₀ (WfCNF), right = 0 (atomic), tail bound 0 ≤ᵇ Ω₀ via +-- `<ᵇ-0-Ω`. +wf-t : WfCNF t +wf-t = + wf-cnf-bplus + (wf-cnf-bomega wf-fin) + wf-cnf-bzero + atomic-bzero + (inj₁ <ᵇ-0-Ω) + +---------------------------------------------------------------------- +-- s <ᵇ t at the ψ/Ω equal-marker boundary +---------------------------------------------------------------------- + +-- fin 0 ≤Ω fin 0 (reflexive) — the `<ᵇ-ψΩ≤` constructor only needs +-- the NON-strict marker bound, so the equal marker fin 0 suffices. +fin0≤Ωfin0 : fin 0 ≤Ω fin 0 +fin0≤Ωfin0 = fin≤fin z≤n + +-- ψ₀(0) <ᵇ Ω₀ lifts to (ψ₀(0) + ψ₀(0)) <ᵇ (Ω₀ + 0) via `<ᵇ-+1` +-- (source-strict-on-the-leading-summand). +s<ᵇt : s <ᵇ t +s<ᵇt = <ᵇ-+1 (<ᵇ-ψΩ≤ fin0≤Ωfin0) + +---------------------------------------------------------------------- +-- rank-pow strictly REVERSES the step +---------------------------------------------------------------------- + +-- rank-pow t = ω-rank-pow (fin 0) ⊕ rank-pow bzero = ω¹ ⊕ oz +-- rank-pow s = ω-rank-pow (fin 0) ⊕ ω-rank-pow (fin 0) = ω¹ ⊕ ω¹ +-- and ω¹ ⊕ oz <′ ω¹ ⊕ ω¹ by strict right-monotonicity of `_⊕_` +-- (right summand oz <′ ω¹ via `ω^_-pos 1`). Both rank reductions are +-- definitional, so the inequality typechecks against the goal. +rank-pow-strictly-reverses : rank-pow t <′ rank-pow s +rank-pow-strictly-reverses = + ⊕-mono-<-right {ω^ 1} {oz} {ω^ 1} (ω^_-pos 1) + +-- The same reversal as a NON-strict bound, for the `≤′-trans` step in +-- the refutations below (rank-pow t ≤′ rank-pow s). +rank-pow-t≤s : rank-pow t ≤′ rank-pow s +rank-pow-t≤s = + ⊕-mono-≤-right {ω^ 1} {oz} {ω^ 1} (≤′-zero {ω^ 1}) + +---------------------------------------------------------------------- +-- Irreflexivity of `_<′_` from well-foundedness +---------------------------------------------------------------------- + +-- Standard derivation by structural recursion on `Acc _<′_ α` +-- (mirrors `Ordinal.Brouwer.StrictLeftMonoRefuted.<′-irrefl`). +acc-no-self : ∀ {α} → Acc _<′_ α → α <′ α → ⊥ +acc-no-self (acc rec) α<α = acc-no-self (rec α<α) α<α + +<′-irrefl : ∀ {α} → ¬ (α <′ α) +<′-irrefl {α} = acc-no-self (wf-<′ α) + +---------------------------------------------------------------------- +-- Refutation 1: general WfCNF rank-monotonicity over `_<ᵇ_` +---------------------------------------------------------------------- + +-- The property a single clean rank-mono theorem would assert: every +-- `<ᵇ` step between WfCNF terms is reflected by a strict rank +-- increase. This is precisely what fails — which is why the landed +-- programme proceeds constructor-by-constructor with the head-Ω / +-- strict-head machinery rather than as one inductive theorem. +RankPowMono : Set +RankPowMono = + ∀ {a b} → WfCNF a → WfCNF b → a <ᵇ b → rank-pow a <′ rank-pow b + +-- Feeding the witness `s <ᵇ t` to the hypothetical monotonicity gives +-- `rank-pow s <′ rank-pow t`; chaining with `rank-pow t ≤′ rank-pow s` +-- yields `rank-pow s <′ rank-pow s`, refuted by `<′-irrefl`. +rank-pow-mono-refuted : ¬ RankPowMono +rank-pow-mono-refuted mono = + <′-irrefl {rank-pow s} + (≤′-trans {osuc (rank-pow s)} {rank-pow t} {rank-pow s} + (mono wf-s wf-t s<ᵇt) rank-pow-t≤s) + +---------------------------------------------------------------------- +-- Refutation 2: joint-bplus shape WITHOUT the strict-head premise +---------------------------------------------------------------------- + +-- The exact statement `RankMonoUmbrellaSlice3.<ᵇ¹-+1-+` works around +-- by adding `head-Ω x₁ <Ω head-Ω y₁`. Without that premise (only the +-- source-strict witness `x₁ <ᵇ y₁` plus WfCNF), the joint-bplus +-- rank-mono conclusion is false: the witness instantiates it at +-- x₁ = ψ₀(0), x₂ = ψ₀(0), y₁ = Ω₀, y₂ = 0 (where head-Ω x₁ ≡ head-Ω y₁ +-- ≡ fin 0, so no strict-head premise is available). +RankPowMonoPlus1 : Set +RankPowMonoPlus1 = + ∀ {x₁ x₂ y₁ y₂} + → WfCNF (bplus x₁ x₂) → WfCNF (bplus y₁ y₂) + → x₁ <ᵇ y₁ + → rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂) + +rank-pow-mono-plus1-refuted : ¬ RankPowMonoPlus1 +rank-pow-mono-plus1-refuted mono = + <′-irrefl {rank-pow s} + (≤′-trans {osuc (rank-pow s)} {rank-pow t} {rank-pow s} + (mono wf-s wf-t (<ᵇ-ψΩ≤ fin0≤Ωfin0)) rank-pow-t≤s) diff --git a/proofs/agda/Ordinal/Buchholz/Smoke.agda b/proofs/agda/Ordinal/Buchholz/Smoke.agda index 81f9d79..2c3fd24 100644 --- a/proofs/agda/Ordinal/Buchholz/Smoke.agda +++ b/proofs/agda/Ordinal/Buchholz/Smoke.agda @@ -636,6 +636,29 @@ open import Ordinal.Buchholz.RankLexJointBplus using ; rank-lex-jb-bpsi-equal-head-from-tail-eq ) +-- Direct rank-pow refutation 2026-06-15 (own block per CLAUDE.md +-- Working rules): the `rank-pow`-level companion to +-- `StrictLeftMonoRefuted` / `AdditivePrincipalGenericRefuted`. Where +-- those refute the two arithmetic ROUTES a closure would consume, +-- this refutes the rank-monotonicity GOAL itself — a concrete pair of +-- WfCNF terms `s <ᵇ t` at the `<ᵇ-+1` ψ/Ω cross-head boundary where +-- `rank-pow` strictly REVERSES the order. Upgrades the Slice 4 +-- `<ᵇ⁻ⁿ-shortfall-equal-head` ⊤-alias placeholder to a checked +-- counterexample; pins exactly the case `RankLexJointBplus`'s +-- `rank-lex-jb` pivot is load-bearing for. +open import Ordinal.Buchholz.RankPowMonoRefuted using + ( s + ; t + ; wf-s + ; wf-t + ; s<ᵇt + ; rank-pow-strictly-reverses + ; RankPowMono + ; rank-pow-mono-refuted + ; RankPowMonoPlus1 + ; rank-pow-mono-plus1-refuted + ) + -- Slice 4 narrowing 2026-05-28 (own block per CLAUDE.md Working -- rules): the deliberately-narrowed `_<ᵇ⁻ⁿ_` umbrella covering -- ALL CASES THAT CLOSE AT THE RANK-POW LEVEL TODAY — 10 inherited From f067e18fe33a6fb7ddf8fc1998c54d9f79b923ab Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 00:25:49 +0000 Subject: [PATCH 2/3] =?UTF-8?q?feat(aggregation):=20mechanise=20micro?= =?UTF-8?q?=E2=86=92macro=20aggregation=20as=20Echo=20/=20no-section?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add EchoAggregation.agda: economic aggregation is an Echo map, and the non-identifiability of the micro state from the macro observable ("you cannot disaggregate") is the repo's no-section theorem. - aggregate : (ℕ × ℕ) → ℕ two-account ledger → Godley column total - ConsistentLedgers m = Echo aggregate m the fibre, definitionally - aggregate-non-injective the fibre is non-trivial (many-to-one) - no-canonical-disaggregation no section of aggregate, via no-section-of-collapsing-map Reuses the same no-section machinery that grounds the affine⊑linear wasm-typing story; the fibre identity is definitional, so downstream Echo/EchoResidue results apply to aggregation unchanged. Wired into All.agda; headlines pinned in Smoke.agda. Verifies under --safe --without-K with zero postulates (All.agda and Smoke.agda exit 0). Mechanises §2 of the oikos alib design note. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01VwbFNQJw23tW8tqM7utWku --- proofs/agda/All.agda | 1 + proofs/agda/EchoAggregation.agda | 188 +++++++++++++++++++++++++++++++ proofs/agda/Smoke.agda | 17 +++ 3 files changed, 206 insertions(+) create mode 100644 proofs/agda/EchoAggregation.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index d20de94..ea0b8c7 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -10,6 +10,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 362db23..87c6b99 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -87,6 +87,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- From b47e7beda39a3612df7fdb760b1faca21d338188 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 00:29:22 +0000 Subject: [PATCH 3/3] fix(ci): classify EchoAggregation in kernel-note and MAP.adoc kernel-guard.sh Check B (classification-drift lint) requires every proofs/agda/Echo*.agda module to be named in echo-kernel-note.adoc. Add EchoAggregation to the application/extension list there, plus a [REAL]-tagged audience-move bullet in MAP.adoc. Mirrors the EchoDeniability classification fix (2026-06-13). scripts/kernel-guard.sh exits 0 locally. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01VwbFNQJw23tW8tqM7utWku --- docs/echo-types/MAP.adoc | 11 +++++++++++ docs/echo-types/echo-kernel-note.adoc | 8 ++++++-- 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index aa2c526..663113b 100644 --- a/docs/echo-types/MAP.adoc +++ b/docs/echo-types/MAP.adoc @@ -245,6 +245,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 ac63585..d8ce23c 100644 --- a/docs/echo-types/echo-kernel-note.adoc +++ b/docs/echo-types/echo-kernel-note.adoc @@ -121,12 +121,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)