From 879ec9bf7a5dbc6ac992d16aaf9eebe778c4c636 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 12:02:10 +0000 Subject: [PATCH 1/3] =?UTF-8?q?docs(licence):=20long-form=20prose=20?= =?UTF-8?q?=E2=86=92=20CC-BY-SA-4.0=20(9=20docs)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Re-applies the owner-authorised relicensing (orig f6cc023) that never landed on main: move 9 long-form prose docs from MPL-2.0 to the estate-designated prose licence CC-BY-SA-4.0 (per GOVERNANCE.adoc: "MPL-2.0 for code, CC-BY-SA-4.0 for prose"; already used in 29+ files). Header-line swap only; copyright / SPDX-FileCopyrightText lines untouched. Files: FOUNDATION_CONTRACT.md, docs/CLAIMS_AUDIT.adoc, docs/echo-types/{fibration-package,universal-property}.adoc, docs/theorem-index.md, wiki/{Architecture,Overview,Roadmap,Working-Rules}.adoc. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01VwbFNQJw23tW8tqM7utWku --- FOUNDATION_CONTRACT.md | 2 +- docs/CLAIMS_AUDIT.adoc | 2 +- docs/echo-types/fibration-package.adoc | 2 +- docs/echo-types/universal-property.adoc | 2 +- docs/theorem-index.md | 2 +- wiki/Architecture.adoc | 2 +- wiki/Overview.adoc | 2 +- wiki/Roadmap.adoc | 2 +- wiki/Working-Rules.adoc | 2 +- 9 files changed, 9 insertions(+), 9 deletions(-) diff --git a/FOUNDATION_CONTRACT.md b/FOUNDATION_CONTRACT.md index e49fef1..f25d1d6 100644 --- a/FOUNDATION_CONTRACT.md +++ b/FOUNDATION_CONTRACT.md @@ -1,5 +1,5 @@ diff --git a/docs/CLAIMS_AUDIT.adoc b/docs/CLAIMS_AUDIT.adoc index 89c72e8..d92790b 100644 --- a/docs/CLAIMS_AUDIT.adoc +++ b/docs/CLAIMS_AUDIT.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Claims Audit — Gate G1 input :toc: macro diff --git a/docs/echo-types/fibration-package.adoc b/docs/echo-types/fibration-package.adoc index 6f24d4d..bd288fe 100644 --- a/docs/echo-types/fibration-package.adoc +++ b/docs/echo-types/fibration-package.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell = echo-types: The Fibration Package diff --git a/docs/echo-types/universal-property.adoc b/docs/echo-types/universal-property.adoc index 3d1646c..4a492f4 100644 --- a/docs/echo-types/universal-property.adoc +++ b/docs/echo-types/universal-property.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell = echo-types: The Universal Property Story diff --git a/docs/theorem-index.md b/docs/theorem-index.md index f0ad656..9122cb4 100644 --- a/docs/theorem-index.md +++ b/docs/theorem-index.md @@ -1,5 +1,5 @@ diff --git a/wiki/Architecture.adoc b/wiki/Architecture.adoc index ce0c15a..0ce92c8 100644 --- a/wiki/Architecture.adoc +++ b/wiki/Architecture.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell = Architecture :toc: macro diff --git a/wiki/Overview.adoc b/wiki/Overview.adoc index b229a4d..cbf20b8 100644 --- a/wiki/Overview.adoc +++ b/wiki/Overview.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell = Overview :toc: macro diff --git a/wiki/Roadmap.adoc b/wiki/Roadmap.adoc index 36d7444..77da45c 100644 --- a/wiki/Roadmap.adoc +++ b/wiki/Roadmap.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell = Roadmap :toc: macro diff --git a/wiki/Working-Rules.adoc b/wiki/Working-Rules.adoc index 41133c9..c565600 100644 --- a/wiki/Working-Rules.adoc +++ b/wiki/Working-Rules.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell = Working Rules :toc: macro From c97d0c44070af558c8df08264b36929b3e736f00 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 17:05:13 +0000 Subject: [PATCH 2/3] feat(aggregation): generalize EchoAggregation to monoid/group form (#175) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Generalize EchoAggregation from the macro-economics-specific module into the general monoid-aggregation form requested by #175 (the SQL GROUP-BY-as-monoid-homomorphism consumer in affinescript db-theory #3): * record Monoid (Elem/ε/_⊕_/assoc/identity-l/identity-r); * ⊕-fold + ⊕-fold-++ (fold is a monoid homomorphism over _++_); * record GroupAggregator (agg : V → Elem) + aggregate-values; * aggregation-as-fold — the #175 headline law, PROVED (not merely signed): aggregating a concatenation equals combining the aggregates; * sumMonoid / countMonoid / maxMonoid (ℕ) + minMonoid (Maybe ℕ, nothing = ∞) + a worked countAggregator; * no-canonical-disaggregation-of — generic non-disaggregability (any collision ⇒ no section, via no-section-of-collapsing-map); this also discharges #174's no-section sibling. The macro→micro economics reading survives mechanised as module Example-PairSum (pairSum : ℕ × ℕ → ℕ IS the sumMonoid fold — pairSum-is-fold — so it is an instance of the general form, nothing re-proved or lost): pairSum-non-injective + no-canonical-disaggregation (the Sonnenschein–Mantel–Debreu / representative-agent critique type-theoretically). oikos reads that instance at macro scale under the name MacroAggregation, cited back here. --safe --without-K, zero postulates, kernel-guard PASS; All.agda + Smoke.agda exit 0. Smoke pins + MAP.adoc + echo-kernel-note.adoc + cross-repo-bridge-status.md swept to the general/macro split. Refs #175, #174 Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01VwbFNQJw23tW8tqM7utWku --- CLAUDE.md | 88 +++++- docs/bridges/cross-repo-bridge-status.md | 15 +- docs/echo-types/MAP.adoc | 33 +- docs/echo-types/echo-kernel-note.adoc | 14 +- proofs/agda/EchoAggregation.agda | 369 ++++++++++++++--------- proofs/agda/Smoke.agda | 43 ++- 6 files changed, 392 insertions(+), 170 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index b777896..1d5fb85 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -212,7 +212,93 @@ work to `main` and refresh all documentation: ## Current rung state (2026-06-18) -### Session arc 2026-06-18 — EchoAggregation / oikos alib bridge (read this first) +### Session arc 2026-06-18 — EchoAggregation general/macro split + long-form prose relicense (read this first) + +*Where we started:* three housekeeping loose ends from the EchoAggregation / +oikos-alib work. (1) stale branch `session/slice-4-narrowing` (a git-ancestor +of `estate-standardization-20260607`, zero unique commits); (2) an +owner-authorised prose relicensing (`f6cc023`) that never re-landed — 9 +long-form docs still `MPL-2.0` while the estate prose licence is +`CC-BY-SA-4.0`; (3) a NAME COLLISION: the merged economics module (#230) +squatted `EchoAggregation`, the name open issue **#175** wants for the +*general* monoid/group aggregation (SQL GROUP-BY-as-fold; consumer = +affinescript db-theory #3). + +*User decision (the pivot):* echo-types' `EchoAggregation` becomes the +GENERAL / fundamental form (serving #175); the MACRO economics reading moves +to oikos under a distinct name + a context statement. Key fact making this +loss-free: `pairSum (a,b) = a+b` IS literally the `sumMonoid` fold of a +two-element list, so the macro result is just an *instance* of the general +form — nothing is re-proved. + +*Where we ended:* two echo-types commits on `claude/ecstatic-wright-OBEvx` +(draft PR), plus an oikos doc commit (draft PR): + +* **Commit A — `docs(licence): long-form prose → CC-BY-SA-4.0 (9 docs)`** + (`879ec9b`). Header-line swap only (`SPDX-License-Identifier: MPL-2.0` → + `…: CC-BY-SA-4.0`) on `FOUNDATION_CONTRACT.md`, `docs/theorem-index.md`, + `docs/CLAIMS_AUDIT.adoc`, `docs/echo-types/{fibration-package,universal-property}.adoc`, + `wiki/{Architecture,Overview,Roadmap,Working-Rules}.adoc`. Copyright / + `SPDX-FileCopyrightText` lines untouched. (Re-applies orig `f6cc023`.) + +* **Commit B — `feat(aggregation): generalize EchoAggregation to monoid/group + form (#175)`.** `proofs/agda/EchoAggregation.agda` rewritten: + `record Monoid ℓ` (`Elem`/`ε`/`_⊕_`/`assoc`/`identity-l`/`identity-r`); + `⊕-fold` + `⊕-fold-++` (fold-is-a-monoid-homomorphism over `_++_`); + `record GroupAggregator {ℓ}(K V)(M)` (`agg : V → Elem`); `aggregate-values` + + the *proved* `aggregation-as-fold` law (#175's headline, by induction — + no `map-++` needed); four instances `sumMonoid`/`countMonoid`/`maxMonoid` + (ℕ,0,+ / + / ⊔) + `minMonoid` over `Maybe ℕ` (`nothing` = ∞, `_⊓∞_` with + `⊓∞-assoc`/`⊓∞-identity-r`); `countAggregator`; generic + `no-canonical-disaggregation-of` (= `no-section-of-collapsing-map`, also + covers #174); and `module Example-PairSum` (the OLD macro `ℕ×ℕ→ℕ` ledger, + neutrally framed: `pairSum-is-fold`, `pairSum-non-injective`, + `no-canonical-disaggregation`) — the mechanised anchor oikos cites. + `Smoke.agda` pins rewritten to the general headlines + a separate + `open EchoAggregation.Example-PairSum using (…)` block. Docs swept: + `echo-kernel-note.adoc` (Check B still PASS — name unchanged), `MAP.adoc` + (general bullet, cites #175/#174), `docs/bridges/cross-repo-bridge-status.md` + (bridge row + new revision entry: echo-types = general, oikos = macro). + +* **oikos — `docs(alib): macro-aggregation reading cites the general + EchoAggregation`.** `oikos/docs/alib-aggregate-bridge.adoc` extended with + the macro reading + the context statement (it is the EchoAggregation of + echo-types read at macro scale; named `MacroAggregation` here because + aggregation is a fundamental there) + §8 pointer updated (macro is now an + *instance* of the general form). NO Agda in oikos (Rust + AffineScript + + Haskell); citation-level, per its own §8. + +Build invariant held: `EchoAggregation.agda` + `All.agda` + `Smoke.agda` +exit 0 under `--safe --without-K`, zero postulates, `kernel-guard.sh` PASS. + +*Honest scope.* `aggregation-as-fold` is the fold's monoid-homomorphism law, +NOT full SQL GROUP-BY operational semantics. `avg` is deliberately absent +(not a monoid — express as `sum / count`, per #175). +`no-canonical-disaggregation-of` refutes a *section* (left inverse), NOT the +existence of *some* representative choice (economists pick representatives; +the content is that no choice is canonical). + +*Flagged (non-executable here):* deleting `session/slice-4-narrowing` (and, +post-merge, `chore/prose-licence-longform-cc-by-sa`) is a manual GitHub-UI +step — `git push --delete` returns HTTP 403 and the GitHub MCP has no +delete-branch endpoint. The genuinely-open `Fidelity.agda` order-type +fidelity debt (`D-2026-06-14`) is untouched. + +*Plan for the next Claude.* (1) After the echo-types PR merges, a frugal +one-line note on #175 that the general form landed (covers #174 too). +(2) `EchoTypes.jl` mirror — add an `EchoAggregation` finite-domain shadow +(the `Monoid`/`sumMonoid` instances + `pairSum` are directly executable). +(3) oikos alib Route-B build, gated on the owner's Route A vs B decision. + +DO NOT reopen: the general/macro split design (the macro IS the +`Example-PairSum` instance — `pairSum` is the `sumMonoid` fold, so nothing is +lost by hosting the general form here); the `no-section` refutation target +(a section is a *left* inverse — exactly what non-disaggregability denies; do +NOT restate it as a failed surjection, which is false since the maps are +onto); the citation-level scope of the oikos bridge (oikos is Rust; no +Agda↔Rust import path). + +### Session arc 2026-06-18 — EchoAggregation / oikos alib bridge (the original macro-only landing) *Where we started:* user asked (cross-repo) to investigate the wasm / typed-wasm route, then to scope an oikos/betlang "alib" aggregate library diff --git a/docs/bridges/cross-repo-bridge-status.md b/docs/bridges/cross-repo-bridge-status.md index 3c7c9ad..37be14b 100644 --- a/docs/bridges/cross-repo-bridge-status.md +++ b/docs/bridges/cross-repo-bridge-status.md @@ -22,7 +22,7 @@ touches other repositories. | **Verdict-provenance (phronesis)** | `Echo`, `echo-intro` | `phronesis/academic/formal-verification/agda/PhronesisEcho.agda` (imports echo-types directly) | **Content bridge done (2026-06-12).** An ethical verdict's provenance IS `Echo verdict v`: `eval` is non-injective, so the fiber retains *which* expressions justify a verdict the bare `Bool` forgets (`verdict-forgets-provenance`); `proj₁` is the recovering section. Machine-checked vs real echo-types. (Also fixed 4 pre-existing bugs making `Phronesis.agda` compile.) | — (closed; downstream consumer in the agentic-ethics language). | | **KitchenSpeak `@` witness (nextgen-languages)** | `Echo` | `nextgen-languages/kitchenspeak/proofs/agda/EchoBridge.agda` | **Status upgraded to MACHINE-CHECKED (2026-06-12).** Previously "hand-verified, not machine-checked"; now typechecks against the real `Echo`. The `@` sensor witness IS `Echo (fired sensor thr) true` (`witness⇒echo` / `echo⇒witness`). PoachedEgg stdlib-v2.3 drift (`toWitness {Q=}`→`{a?=}`) fixed so the suite type-checks. | — (the `--` comments in `kitchenspeak.agda-lib` need Agda ≥ 2.6.4; on the 2.6.3 CI toolchain use the explicit `-i` form, documented in the module). | | **Invariant Path application (invariant-path)** | Structured-loss vocabulary (the `Echo` fiber concept) — citation-level | `invariant-path` (Rust): `classify_candidate` + `docs/ECHO-TYPES.md` + `crates/invariant-path-core/{examples,tests}/echo_structured_loss.rs` | **Application example (2026-06-12).** `classify_candidate` is a non-injective classifier; the retained `ClaimCandidate` + `ClassificationOutcome.losses` IS the echo (fiber) over a `Classification`. Invariant Path is "a claim-path debugger, not a truth engine" precisely because it retains echoes. Runnable example + 2 CI-covered tests. | No Agda↔Rust import path; citation-level — the application *uses* the echo principle; no mechanised cross-repo theorem. | -| **oikos alib aggregation bridge (economics)** | `proofs/agda/EchoAggregation.agda` (`aggregate : MicroLedger → MacroTotal` IS an `Echo`; `no-canonical-disaggregation = no-section-of-collapsing-map`) | `oikos/docs/alib-aggregate-bridge.adoc` (toolchain-free design note for the alib aggregate library; oikos is the Rust SFC-macro DSL) | **Keystone formalisation + design note landed (2026-06-18).** Micro→macro economic aggregation is mechanised as an `Echo` map: the fibre over a macro total is exactly the set of micro ledgers consistent with it, and non-disaggregability is `no-section-of-collapsing-map` (no canonical `raise : MacroTotal → MicroLedger` left-inverse exists). This is the type-theoretic form of the Sonnenschein–Mantel–Debreu / representative-agent critique — it refutes a *section* (left inverse), not a representative *choice*. `EchoAggregation.agda` is self-contained in echo-types (imports `Echo` + `EchoNoSectionGeneric` only), `--safe --without-K`, zero postulates, pinned in `Smoke.agda`, classified in the kernel-note. The oikos design note recommends Route B (alib as an aggregation-morphism library over `MacroState`). | No Agda↔Rust import path; citation-level — echo-types proves the aggregation principle, oikos's alib will *consume* it. The alib library itself is not yet built (design-note stage; open questions §"Route A vs B" pending owner decision). | +| **oikos alib aggregation bridge (economics)** | `proofs/agda/EchoAggregation.agda` — the GENERAL aggregation form (`Monoid` + `GroupAggregator` + `aggregation-as-fold` homomorphism + `sumMonoid`/`countMonoid`/`maxMonoid`/`minMonoid` + `no-canonical-disaggregation-of`); the macro economics is the `Example-PairSum` instance (`pairSum` IS the `sumMonoid` fold) | `oikos/docs/alib-aggregate-bridge.adoc` (toolchain-free design note; oikos is the Rust SFC-macro DSL) — names the macro reading `MacroAggregation`, cited back to echo-types | **General/macro split landed (2026-06-18, gen. rung).** echo-types now hosts the *general* monoid-aggregation form requested by issue #175 (SQL GROUP-BY as a monoid homomorphism; consumer = affinescript db-theory #3); the `aggregation-as-fold` law is *proved*, not merely signed, and generic non-disaggregability `no-canonical-disaggregation-of` also discharges #174's no-section sibling. The *macro→micro economics* reading — micro ledger rolled up to a Godley total, the Sonnenschein–Mantel–Debreu / representative-agent critique (refuting a *section* / left inverse, not a representative *choice*) — is the `Example-PairSum` instance, read at macro scale in oikos under the name `MacroAggregation` (naming it `EchoAggregation` there would be odd: aggregation is a *fundamental* of echo-types). `EchoAggregation.agda` is self-contained (imports `Echo` + `EchoNoSectionGeneric` only), `--safe --without-K`, zero postulates, pinned in `Smoke.agda`, classified in the kernel-note + `MAP.adoc`. The oikos design note recommends Route B (alib as an aggregation-morphism library over `MacroState`). | No Agda↔Rust import path; citation-level — echo-types proves the general aggregation principle (and its macro instance), oikos's alib will *consume* it. The alib library itself is not yet built (design-note stage; Route A vs B pending owner decision). | ## Immediate next actions @@ -72,6 +72,19 @@ precisely to paper over this in the relational model. ## Revision history +- 2026-06-18: **EchoAggregation general/macro split.** Generalised + `EchoAggregation.agda` from the macro-economics-specific module into the + general monoid-aggregation form requested by issue #175 (`Monoid` + + `GroupAggregator` + the *proved* `aggregation-as-fold` homomorphism law + + `sumMonoid`/`countMonoid`/`maxMonoid`/`minMonoid` + generic + `no-canonical-disaggregation-of`, which also covers #174). The + macro→micro economics reading survives mechanised as the `Example-PairSum` + instance (`pairSum` IS the `sumMonoid` fold — nothing re-proved or lost); + oikos reads that instance at macro scale under the name `MacroAggregation` + (aggregation is a fundamental of echo-types, so re-using the name there + would be odd). Updated the bridge row, `MAP.adoc`, and + `echo-kernel-note.adoc`; `--safe --without-K`, zero postulates, + kernel-guard PASS. - 2026-06-18: **oikos alib aggregation bridge.** Added the economics-aggregation row recording `EchoAggregation.agda` (micro→macro rollup is an `Echo`; non-disaggregability is `no-section-of-collapsing-map` diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index fc4356d..4a74b15 100644 --- a/docs/echo-types/MAP.adoc +++ b/docs/echo-types/MAP.adoc @@ -253,17 +253,28 @@ 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]` +* *Aggregation (general, issue #175)* — aggregation-as-fold over a + `Monoid`, with a `GroupAggregator` and the monoid-homomorphism law + `aggregation-as-fold` (aggregating a concatenation = combining the + aggregates; proved, not merely signed). Four concrete instances + (`sumMonoid` / `countMonoid` / `maxMonoid` / `minMonoid`, the last + over `ℕ ∪ {∞}` via `Maybe ℕ`), a worked `countAggregator`, and + generic non-disaggregability `no-canonical-disaggregation-of` (any + collision ⇒ no section, via `no-section-of-collapsing-map`; this + also discharges issue #174's no-section sibling). The + macro→micro *economic* reading lives in `module Example-PairSum`: + `pairSum : ℕ × ℕ → ℕ` IS the `sumMonoid` fold (`pairSum-is-fold`), + is many-to-one (`pairSum-non-injective`), and has no canonical + disaggregation (`no-canonical-disaggregation`) — the + Sonnenschein–Mantel–Debreu / representative-agent critique + type-theoretically. That instance is the mechanised anchor the + oikos/betlang alib note cites (`oikos:docs/alib-aggregate-bridge.adoc`), + where it is read at macro scale and named `MacroAggregation`. + Consumer of the general form: affinescript db-theory #3 (SQL + GROUP-BY as a monoid homomorphism). Honest-bound: `aggregation-as-fold` + is the fold's homomorphism law, NOT full SQL GROUP-BY operational + semantics; `avg` is deliberately absent (not a monoid — express as + `sum / count`). `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 45799aa..f3564a8 100644 --- a/docs/echo-types/echo-kernel-note.adoc +++ b/docs/echo-types/echo-kernel-note.adoc @@ -130,10 +130,16 @@ kernel** — the boundary is real and lives outside this core. 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. - `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`. + `EchoAggregation` is the general aggregation form (issue #175): + aggregation-as-fold over a `Monoid`, a `GroupAggregator`, the + monoid-homomorphism law `aggregation-as-fold`, the four concrete + instances (`sumMonoid`/`countMonoid`/`maxMonoid`/`minMonoid`), and + generic non-disaggregability `no-canonical-disaggregation-of` (any + collision ⇒ no section, via `no-section-of-collapsing-map`; also + covers #174). The macro→micro economic reading is the + `Example-PairSum` instance the oikos/betlang alib note cites + (`pairSum` IS the `sumMonoid` fold). Imports `Echo` + + `EchoNoSectionGeneric`. | *Earn-back gate modules* + (derived / scoped; not kernel) diff --git a/proofs/agda/EchoAggregation.agda b/proofs/agda/EchoAggregation.agda index 3f28ecf..0b545a3 100644 --- a/proofs/agda/EchoAggregation.agda +++ b/proofs/agda/EchoAggregation.agda @@ -2,187 +2,276 @@ -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell --- EchoAggregation: micro→macro economic aggregation as structured loss. +-- EchoAggregation: aggregation-as-fold over a monoid, with the +-- structured-loss (Echo / no-section) reading. -- --- 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. +-- This module is the GENERAL aggregation form requested by issue #175 +-- (a `Monoid` carrier + a `GroupAggregator`, for the SQL group-by / +-- aggregation-as-monoid-homomorphism consumer in affinescript +-- db-theory #3). Aggregation-as-Echo is a *fundamental* of echo-types, +-- so the clean name `EchoAggregation` names the general construction. -- --- 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: +-- The MACRO-economics reading — rolling a micro ledger up into a macro +-- observable, and the Sonnenschein–Mantel–Debreu / representative-agent +-- "you cannot disaggregate" critique — is the oikos `alib` bridge's +-- *interpretation* of this general form. It lives in +-- `oikos/docs/alib-aggregate-bridge.adoc` and cites the +-- `Example-PairSum` instance below. Because aggregation is a +-- fundamental here, naming the macro instance `EchoAggregation` over in +-- oikos would be odd; oikos names it `MacroAggregation` and cites back. -- --- * `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. +-- ## What lands (all --safe --without-K, zero postulates) -- --- 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. +-- * `Monoid` — the aggregation carrier (#175): +-- `ε`, `_⊕_`, `assoc`, `identity-l`, +-- `identity-r`. +-- * `GroupAggregator` — a value→element aggregator over a monoid, +-- keyed by `K` (#175). +-- * `⊕-fold` / `⊕-fold-++` +-- — fold a list through the monoid; the fold is a +-- monoid homomorphism (it distributes over +-- `_++_`). +-- * `aggregate-values` / `aggregation-as-fold` +-- — group-aggregation as a fold, and its +-- homomorphism law (the #175 "aggregation-as- +-- fold" property — PROVED here, not merely +-- signed: aggregating a concatenation equals +-- combining the aggregates). +-- * `sumMonoid` / `countMonoid` / `maxMonoid` / `minMonoid` +-- — the four concrete instances #175 asks for +-- (`min` over `ℕ ∪ {∞}` via `Maybe ℕ`, +-- `nothing` = ∞). +-- * `countAggregator` — a worked `GroupAggregator` (every value +-- contributes 1 to `sumMonoid`). +-- * `no-canonical-disaggregation-of` +-- — generic non-disaggregability: any aggregation +-- with a collision admits NO section (a LEFT +-- inverse). A re-export of +-- `EchoNoSectionGeneric.no-section-of-collapsing-map` +-- at aggregation-flavoured names; also covers +-- issue #174's no-section sibling. +-- * `module Example-PairSum` +-- — the worked instance: a two-field record summed +-- to a total (`ℕ × ℕ → ℕ`). It is non-injective +-- and admits no section; and `pairSum` IS the +-- `sumMonoid` fold of its two fields +-- (`pairSum-is-fold`). This is the mechanised +-- anchor the oikos macro reading cites. -- --- What is proved. +-- ## Honest scope -- --- * `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. +-- `aggregation-as-fold` is the monoid-homomorphism property of the fold +-- (folding a concatenation = combining the folds). It is NOT a claim +-- about SQL GROUP-BY's full operational semantics. `avg` is +-- deliberately absent: it is not a monoid (no identity); express it as +-- `sum / count`, per #175. `no-canonical-disaggregation-of` refutes a +-- section (a left inverse), NOT the existence of *some* representative +-- choice — economists pick representatives all the time; the content is +-- that no such choice is canonical. 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 Level using (Level; 0ℓ; suc) +open import Data.Nat.Base using (ℕ; _+_; _⊔_; _⊓_) +open import Data.Nat.Properties using ( +-assoc; +-identityˡ; +-identityʳ + ; ⊔-assoc; ⊔-identityˡ; ⊔-identityʳ + ; ⊓-assoc ) +open import Data.Maybe.Base using (Maybe; just; nothing) +open import Data.List.Base using (List; []; _∷_; _++_; map; foldr) +open import Data.Product.Base using (Σ; _×_; _,_; proj₁; proj₂) open import Relation.Binary.PropositionalEquality - using (_≡_; _≢_; refl; cong) + using (_≡_; _≢_; refl; sym; trans; cong) open import Relation.Nullary using (¬_) ---------------------------------------------------------------------- --- The micro / macro types and the aggregation map. +-- The aggregation carrier: a monoid (issue #175). ---------------------------------------------------------------------- --- A micro ledger: two sector balances (e.g. household, firm). -MicroLedger : Set -MicroLedger = ℕ × ℕ +record Monoid (ℓ : Level) : Set (suc ℓ) where + field + Elem : Set ℓ + ε : Elem + _⊕_ : Elem → Elem → Elem + assoc : (a b c : Elem) → (a ⊕ b) ⊕ c ≡ a ⊕ (b ⊕ c) + identity-l : (a : Elem) → ε ⊕ a ≡ a + identity-r : (a : Elem) → a ⊕ ε ≡ a --- The macro observable: one aggregate total (a Godley column sum). -MacroTotal : Set -MacroTotal = ℕ +---------------------------------------------------------------------- +-- Folding a list through a monoid, and the homomorphism law. +-- +-- `⊕-fold M` is the monoid fold; `⊕-fold-++` proves it is a monoid +-- homomorphism on `(List Elem, _++_, [])` → `(Elem, _⊕_, ε)`: +-- folding a concatenation equals combining the two folds. Stated +-- top-level (taking `M` explicitly) so the headlines pin directly. +---------------------------------------------------------------------- --- Aggregation: roll the micro ledger up into the macro total. -aggregate : MicroLedger → MacroTotal -aggregate (a , b) = a + b +⊕-fold : ∀ {ℓ} (M : Monoid ℓ) → List (Monoid.Elem M) → Monoid.Elem M +⊕-fold M = foldr (Monoid._⊕_ M) (Monoid.ε M) + +⊕-fold-++ : ∀ {ℓ} (M : Monoid ℓ) (xs ys : List (Monoid.Elem M)) → + ⊕-fold M (xs ++ ys) ≡ Monoid._⊕_ M (⊕-fold M xs) (⊕-fold M ys) +⊕-fold-++ M [] ys = sym (Monoid.identity-l M (⊕-fold M ys)) +⊕-fold-++ M (x ∷ xs) ys = + trans (cong (Monoid._⊕_ M x) (⊕-fold-++ M xs ys)) + (sym (Monoid.assoc M x (⊕-fold M xs) (⊕-fold M ys))) ---------------------------------------------------------------------- --- 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). +-- Group aggregator (issue #175): a value→element map over a monoid, +-- keyed by `K` (the group-by key; phantom in the carrier, used by the +-- SQL consumer to partition rows before folding each group). ---------------------------------------------------------------------- -ConsistentLedgers : MacroTotal → Set -ConsistentLedgers m = Echo aggregate m +record GroupAggregator {ℓ} (K V : Set) (M : Monoid ℓ) : Set ℓ where + field + agg : V → Monoid.Elem M + +-- Aggregate a list of values: map the aggregator, then fold. +aggregate-values : ∀ {ℓ} {K V : Set} {M : Monoid ℓ} + → GroupAggregator K V M → List V → Monoid.Elem M +aggregate-values {M = M} G vs = ⊕-fold M (map (GroupAggregator.agg G) vs) + +-- Aggregation-as-fold (the #175 headline law): aggregating a +-- concatenation equals combining the two aggregates. Proved by +-- induction (no `map-++` lemma needed — the cons case reduces +-- definitionally through `map` and `foldr`). +aggregation-as-fold : ∀ {ℓ} {K V : Set} {M : Monoid ℓ} + (G : GroupAggregator K V M) (vs ws : List V) → + aggregate-values G (vs ++ ws) + ≡ Monoid._⊕_ M (aggregate-values G vs) (aggregate-values G ws) +aggregation-as-fold {M = M} G [] ws = + sym (Monoid.identity-l M (aggregate-values G ws)) +aggregation-as-fold {M = M} G (v ∷ vs) ws = + trans (cong (Monoid._⊕_ M (GroupAggregator.agg G v)) (aggregation-as-fold G vs ws)) + (sym (Monoid.assoc M (GroupAggregator.agg G v) + (aggregate-values G vs) (aggregate-values G ws))) ---------------------------------------------------------------------- --- The fibre over macro total 1 is non-trivial: two distinct micro --- ledgers, (0,1) and (1,0), both aggregate to 1. +-- The four concrete monoid instances (issue #175). ---------------------------------------------------------------------- -ledger₁ : MicroLedger -ledger₁ = 0 , 1 +-- Sum / count: (ℕ, 0, +). `count` is "sum of 1s" — the SAME monoid; +-- the counting happens in the aggregator (`countAggregator`). +sumMonoid : Monoid 0ℓ +sumMonoid = record + { Elem = ℕ ; ε = 0 ; _⊕_ = _+_ + ; assoc = +-assoc ; identity-l = +-identityˡ ; identity-r = +-identityʳ } + +countMonoid : Monoid 0ℓ +countMonoid = sumMonoid -ledger₂ : MicroLedger -ledger₂ = 1 , 0 +-- Max: (ℕ, 0, ⊔). 0 is the max-identity on ℕ (0 ≤ n for all n). +maxMonoid : Monoid 0ℓ +maxMonoid = record + { Elem = ℕ ; ε = 0 ; _⊕_ = _⊔_ + ; assoc = ⊔-assoc ; identity-l = ⊔-identityˡ ; identity-r = ⊔-identityʳ } --- 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 -... | () +-- Min: (ℕ ∪ {∞}, ∞, ⊓). `ℕ` has no top, so adjoin one as `nothing` +-- (= ∞, the min-identity); `just n` = n. +_⊓∞_ : Maybe ℕ → Maybe ℕ → Maybe ℕ +nothing ⊓∞ y = y +just a ⊓∞ nothing = just a +just a ⊓∞ just b = just (a ⊓ b) --- … yet they collapse to the same macro total (both 1). -aggregate-collapses : aggregate ledger₁ ≡ aggregate ledger₂ -aggregate-collapses = refl +⊓∞-identity-r : (x : Maybe ℕ) → x ⊓∞ nothing ≡ x +⊓∞-identity-r nothing = refl +⊓∞-identity-r (just a) = refl --- As echoes at the same macro total. -echo-ledger₁ : ConsistentLedgers 1 -echo-ledger₁ = echo-intro aggregate ledger₁ +⊓∞-assoc : (x y z : Maybe ℕ) → (x ⊓∞ y) ⊓∞ z ≡ x ⊓∞ (y ⊓∞ z) +⊓∞-assoc nothing y z = refl +⊓∞-assoc (just a) nothing z = refl +⊓∞-assoc (just a) (just b) nothing = refl +⊓∞-assoc (just a) (just b) (just c) = cong just (⊓-assoc a b c) -echo-ledger₂ : ConsistentLedgers 1 -echo-ledger₂ = echo-intro aggregate ledger₂ +minMonoid : Monoid 0ℓ +minMonoid = record + { Elem = Maybe ℕ ; ε = nothing ; _⊕_ = _⊓∞_ + ; assoc = ⊓∞-assoc ; identity-l = λ _ → refl ; identity-r = ⊓∞-identity-r } --- 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) +-- A worked aggregator: count. Every value contributes 1 to the sum +-- monoid; `aggregate-values countAggregator` is then list length, and +-- `aggregation-as-fold` specialises to "count of a concatenation = +-- sum of the counts". +countAggregator : ∀ {K V : Set} → GroupAggregator K V sumMonoid +countAggregator = record { agg = λ _ → 1 } ---------------------------------------------------------------------- --- The keystone: no canonical disaggregation. +-- Generic non-disaggregability. -- --- 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. +-- Any aggregation map with a collision (two distinct inputs, the same +-- output) admits NO section: there is no `raise` recovering the input +-- from the aggregate for every input. This is exactly +-- `EchoNoSectionGeneric.no-section-of-collapsing-map` at aggregation- +-- flavoured names, and it is also issue #174's no-section sibling. ---------------------------------------------------------------------- -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 +no-canonical-disaggregation-of : + ∀ {a r} {A : Set a} {R : Set r} + (agg-map : A → R) (x y : A) → x ≢ y → agg-map x ≡ agg-map y → + ¬ Σ (R → A) (λ raise → ∀ z → raise (agg-map z) ≡ z) +no-canonical-disaggregation-of agg-map x y x≢y collides = + no-section-of-collapsing-map agg-map x y x≢y collides ---------------------------------------------------------------------- --- Companion remark. --- --- Why this is the right level of generality: +-- Worked instance: a two-field record summed to a total. -- --- * 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. +-- The smallest faithful aggregation — `ℕ × ℕ → ℕ` by `+`. This is the +-- mechanised anchor the oikos macro-economics reading cites (a micro +-- ledger of two sector balances rolled up into one Godley column +-- total). It exhibits, concretely: -- --- * `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. +-- * `pairSum-is-fold` — `pairSum` IS the `sumMonoid` fold of +-- the two fields (it is an instance of +-- the general form, not a separate idea); +-- * `pairSum-non-injective` — two distinct ledgers, same total, +-- distinct echoes ("aggregation is +-- many-to-one", as a theorem); +-- * `no-canonical-disaggregation` +-- — no section: the total cannot in general +-- be disaggregated (SMD / representative- +-- agent critique, type-theoretically). ---------------------------------------------------------------------- + +module Example-PairSum where + + Pair : Set + Pair = ℕ × ℕ + + pairSum : Pair → ℕ + pairSum (a , b) = a + b + + -- `pairSum` is exactly the `sumMonoid` fold of its two fields, so the + -- macro instance is a *special case* of the general aggregation form. + pairSum-is-fold : (p : Pair) → pairSum p ≡ ⊕-fold sumMonoid (proj₁ p ∷ proj₂ p ∷ []) + pairSum-is-fold (a , b) = cong (a +_) (sym (+-identityʳ b)) + + -- The fibre over total 1 is non-trivial: (0,1) and (1,0) both sum to 1. + ledger₁ : Pair + ledger₁ = 0 , 1 + + ledger₂ : Pair + ledger₂ = 1 , 0 + + ledger₁≢ledger₂ : ledger₁ ≢ ledger₂ + ledger₁≢ledger₂ eq with cong proj₁ eq + ... | () + + pairSum-collapses : pairSum ledger₁ ≡ pairSum ledger₂ + pairSum-collapses = refl + + echo-ledger₁ : Echo pairSum 1 + echo-ledger₁ = echo-intro pairSum ledger₁ + + echo-ledger₂ : Echo pairSum 1 + echo-ledger₂ = echo-intro pairSum ledger₂ + + pairSum-non-injective : echo-ledger₁ ≢ echo-ledger₂ + pairSum-non-injective eq = ledger₁≢ledger₂ (cong proj₁ eq) + + -- The keystone: no canonical disaggregation of the total. + no-canonical-disaggregation : + ¬ Σ (ℕ → Pair) (λ raise → ∀ p → raise (pairSum p) ≡ p) + no-canonical-disaggregation = + no-canonical-disaggregation-of pairSum ledger₁ ledger₂ ledger₁≢ledger₂ pairSum-collapses diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 81f17a9..0b3c858 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -108,20 +108,37 @@ 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`. +-- EchoAggregation — the GENERAL aggregation form (issue #175): +-- aggregation-as-fold over a `Monoid`, with a `GroupAggregator` and +-- the monoid-homomorphism law `aggregation-as-fold` (aggregating a +-- concatenation = combining the aggregates). Four concrete instances +-- (`sumMonoid`/`countMonoid`/`maxMonoid`/`minMonoid`), a worked +-- `countAggregator`, and generic non-disaggregability +-- `no-canonical-disaggregation-of` (any collision ⇒ no section, via +-- `no-section-of-collapsing-map`; also covers #174). The MACRO +-- economics reading (micro→macro ledger, SMD critique) is the oikos +-- alib bridge's interpretation of the `Example-PairSum` instance: +-- `pairSum` IS the `sumMonoid` fold (`pairSum-is-fold`), is +-- many-to-one (`pairSum-non-injective`), and has no canonical +-- disaggregation (`no-canonical-disaggregation`). open import EchoAggregation using - ( aggregate - ; ConsistentLedgers - ; ledger₁≢ledger₂ - ; aggregate-collapses - ; aggregate-non-injective + ( Monoid + ; GroupAggregator + ; ⊕-fold + ; ⊕-fold-++ + ; aggregate-values + ; aggregation-as-fold + ; sumMonoid + ; countMonoid + ; maxMonoid + ; minMonoid + ; countAggregator + ; no-canonical-disaggregation-of + ) +open EchoAggregation.Example-PairSum using + ( pairSum + ; pairSum-is-fold + ; pairSum-non-injective ; no-canonical-disaggregation ) From 8744a255263bd2d8d58fe60454a28724e16a3110 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 19 Jun 2026 22:37:12 +0000 Subject: [PATCH 3/3] docs(affirmation): refresh AFFIRMATION + add 2026-06-19 status tables Re-anchor AFFIRMATION.adoc to claude/ecstatic-wright-OBEvx @ c97d0c4, verified green this session under Agda 2.6.3 + stdlib 2.3 + absolute-zero (All.agda / Smoke.agda / characteristic/All.agda exit 0; kernel-guard PASS; postulate declarations confined to the two unwired fenced modules). Add docs/status/STATUS-2026-06-19.adoc: the musts / intends / wishes table with the normative MUST = the Oikos accounting DSL, echo-types positioned as the verified proof companion (general EchoAggregation #175). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01VwbFNQJw23tW8tqM7utWku --- AFFIRMATION.adoc | 331 ++++++++++++----------------- docs/status/STATUS-2026-06-19.adoc | 173 +++++++++++++++ 2 files changed, 310 insertions(+), 194 deletions(-) create mode 100644 docs/status/STATUS-2026-06-19.adoc diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index fcf3ba7..ff2d733 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -1,6 +1,6 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -= AFFIRMATION — echo-types, as of 2026-06-16 += AFFIRMATION — echo-types, as of 2026-06-19 :toc: macro :toclevels: 2 @@ -91,25 +91,25 @@ record, not a won argument. [cols="1,3"] |=== | *Repo* | `hyperpolymath/echo-types` (the constructive Agda formalisation of structured loss) -| *Branch* | `docs/proof-trust-audit-2026-06-16` -| *Commit (HEAD)* | `59375b60379f3f1356161c1a257736d13bd75b2f` -| *Permalink* | https://github.com/hyperpolymath/echo-types/tree/59375b60379f3f1356161c1a257736d13bd75b2f -| *Verified (UTC)* | 2026-06-16T12:16:59Z -| *Working-tree delta at verification* | Clean (`git status --porcelain` empty) except this untracked `AFFIRMATION.adoc`. The green results below are HEAD itself. -| *Toolchain* | Agda 2.8.0 · just 1.50.0 · git 2.43.0 -| *Agda libraries (load-bearing)* | `standard-library` from the worktree `/home/hyperpolymath/developer/worktrees/agda-stdlib-tweak` (lib flag `--warning=noUnsupportedIndexedMatch`) + `absolute-zero` from `/home/hyperpolymath/developer/repos/absolute-zero`. See the environment note below. +| *Branch* | `claude/ecstatic-wright-OBEvx` +| *Commit (HEAD)* | `c97d0c44070af558c8df08264b36929b3e736f00` +| *Permalink* | https://github.com/hyperpolymath/echo-types/tree/c97d0c44070af558c8df08264b36929b3e736f00 +| *Verified (UTC)* | 2026-06-19 (this session; the green runs below were taken at ~22:28–22:34Z) +| *Working-tree delta at verification* | Clean (`git status --porcelain` empty); the green results below are commit `c97d0c4` *itself*. This AFFIRMATION refresh and the new `docs/status/STATUS-2026-06-19.adoc` are added on top of the verified commit. +| *Toolchain* | Agda 2.6.3 · agda-stdlib 2.3 · git +| *Agda libraries (load-bearing)* | `standard-library` (v2.3) at `/opt/agda-stdlib` + `absolute-zero` at `/home/user/absolute-zero`, both *registered and resolving* in `~/.agda/libraries`. See the environment note below. |=== [IMPORTANT] -*Environment note (read before you call anything broken).* The machine's -`~/.agda/libraries` registers a `standard-library` path -(`…/developer/repos/agda-stdlib/standard-library.agda-lib`) that *does not -exist* — it is dangling at this moment. We did NOT typecheck against the -dangling path. We pointed Agda at the working stdlib worktree above (plus -`absolute-zero`) and that is the environment in which the green results hold. If -you run a bare `agda` and it fails only with "library not found", that is an -*environment artefact, not a proof defect*; wire the worktree stdlib first (see -<>). +*Environment note.* On *this* machine, unlike the 2026-06-16 affirmation's +environment, `~/.agda/libraries` resolves cleanly — both `/opt/agda-stdlib` +and `/home/user/absolute-zero` exist. The green results below were produced with +the include flags shown in <> (`-i proofs/agda -i . -i +/home/user/absolute-zero/proofs/agda`) against that registered stdlib. This also +*resolves a long-standing doc/toolchain tension*: the green `--safe --without-K` +closure now verifies under the `CLAUDE.md`-documented *Agda 2.6.3 + stdlib 2.3*, +in addition to the *Agda 2.8.0* worktree under which the 2026-06-16 affirmation +checked it. The closure is robust across both. [IMPORTANT] If you are reading this at a _later_ commit, the claims may have drifted. @@ -122,101 +122,61 @@ drift from what we verified, we say so here rather than quietly leave the reader to find out. * *`README.adoc`* — *absent.* The canonical README for this repo is - link:README.md[`README.md`] (the richest of the trio; `readme.adoc` and - `EXPLAINME.adoc` are deliberate one-line pointers _to_ it, per the 2026-06-12 - deduplication). So the estate's nominal `README.adoc` filename is not present, - but a canonical README _is_ — `README.md`. Noted, not glossed. -* *`EXPLAINME.adoc`* — *present*, but as a pointer: - link:EXPLAINME.adoc[`EXPLAINME.adoc`] now just redirects to `README.md` - §"What Echo Types Are For" / §"Current Status Snapshot". There is no longer a - standalone "prove every README claim with code paths" body in it. Honest gap: - the dedicated EXPLAINME role is folded into the README rather than separate. -* *GitHub repo description* — _"Constructive Agda library for Echo Types: a - formal model of structured loss (non-total erasure). Mechanized - Bachmann-Howard ordinals, Buchholz/Veblen hierarchies, and thermodynamic - stability proofs."_ Cross-check against what we verified: -** "Constructive Agda library … structured loss" — *matches*: the verified - closure typechecks `--safe --without-K`, and `Echo f y := Σ (x : A), (f x ≡ y)` - is its core. -** "Mechanized Bachmann–Howard ordinals … Buchholz/Veblen hierarchies" — - *partly aspirational*. A large ordinal-notation development is present and in - the green closure (Buchholz/Veblen modules, well-foundedness for the _sound - carriers_ `_<ᵇ⁰_` / `_<ᵇ²_` / `_<ᵇʳᶠ²_`). But by the repo's own internal - record the Bachmann–Howard _target_ is a milestone-in-progress, not a closed - end-to-end theorem: the unbudgeted global WF for native `_<ᵇ_` is documented - as not closable as stated, and order-type fidelity to BH is an explicit - _postulated_ trust boundary (`Ordinal/Buchholz/Fidelity.agda`, - `Fidelity-OPEN-postulates.md`) that lives OUTSIDE the `--safe` closure. Read - "mechanized BH" as "a mechanized notation system aimed at BH", not "BH proved". -** "thermodynamic stability proofs" — the thermodynamics modules - (`EchoThermodynamics`, `EchoEntropy`, …) are in the green closure and - typecheck; their own headers scope the entropy results to the _discrete, - finite-domain_ shadow (not real-valued Shannon entropy). The `Justfile`'s - "stability 92/100" numerals are *not* a checked output — see the loud-failure - note below. -* *GitHub topics* — `agda`, `category-theory`, `formal-verification`, - `type-theory`, `echo-types`, `constructive-mathematics`, - `homotopy-type-theory`, `modal-logic`. Cross-check: `agda`, - `formal-verification`, `type-theory`, `constructive-mathematics` are _earned_ - by the green `--safe --without-K` closure. `homotopy-type-theory` is loose — - the library is deliberately `--without-K` and several results are honestly - flagged as needing UIP / truncation / Cubical that the safe core does NOT - assume (e.g. the truncated image factorisation lives only in a postulated / - separate-flag module). + link:README.md[`README.md`]; `readme.adoc` and `EXPLAINME.adoc` are deliberate + one-line pointers _to_ it. So the estate's nominal `README.adoc` filename is + not present, but a canonical README _is_ — `README.md`. Noted, not glossed. +* *`EXPLAINME.adoc`* — *present*, as a pointer redirecting to `README.md`. +* *`docs/status/STATUS-2026-06-19.adoc`* — *present (new this session)*: the + musts/intends/wishes status table (normative MUST = the Oikos accounting DSL), + with echo-types positioned as the verified proof companion. This affirmation is + the receipt for the echo-types green-closure rows in that table. +* *`CLAUDE.md` build note* — cites "Agda 2.6.3 + stdlib 2.3 + absolute-zero". We + verified green under exactly that this session (see the environment note). No + drift. == The honest state (one breath) *echo-types is a real, constructive Agda formalisation of fiber-based structured -loss whose verified closure typechecks green under `--safe --without-K` with -zero postulates and no escape pragmas — a genuinely machine-checked CORE -(the Echo Σ-fiber calculus, its totality / orthogonal-factorisation / no-section -/ graded-loss / decoration spine, and a large sound-carrier ordinal-notation -development) — alongside an explicitly fenced PERIPHERY of documented postulate -trust-boundaries, experiments, and unwired modules that are deliberately kept -out of that closure, plus a still-open Bachmann–Howard milestone and a stale +loss whose verified closure typechecks green under `--safe --without-K` with a +funext-free, postulate-free kernel cone and no escape pragmas in the closure — a +genuinely machine-checked CORE (the Echo Σ-fiber calculus, its totality / +orthogonal-factorisation / no-section / graded-loss / decoration spine, the +general monoid/group `EchoAggregation` theorem, and a large sound-carrier +ordinal-notation development) — alongside an explicitly fenced PERIPHERY of +documented postulate trust-boundaries, experiments, and unwired modules kept out +of that closure, plus a still-open Bachmann–Howard milestone and a stale `Justfile`.* === What is solid (and how we checked) -* *The verified module closure typechecks green — this moment.* - `agda --safe --without-K -i proofs/agda proofs/agda/All.agda` *exits 0*. - `proofs/agda/All.agda` transitively forces *151 top-level `open import`s* - (the Echo core, the establishment-track Pillar A–D modules, the F1–F5 - earn-back gates, the audience-facing modules, the deniability module, and the - whole `Ordinal.*` / `Ordinal.Buchholz.*` / `Ordinal.Brouwer.*` notation tower). - All under `--safe --without-K`. _How checked:_ ran the command just now against - the worktree stdlib + absolute-zero; tail showed every module `Checking …` - through `Smoke` with exit code 0. -* *The characteristic lane typechecks green — this moment.* - `agda --safe --without-K -i proofs/agda proofs/agda/characteristic/All.agda` - *exits 0* (14 modules: `ChoreoInjective`, `RoleGraded`, `RoleMode`, - `RoleRole`, `RoleModeGrade`, `ModeGraded`, `N5Falsifier`, `NonTruncatable`, - `RecipeSpec`/`RecipeTheorem`/`RecipeNonTriviality`, `InteractionTest`, - `IntegrationAudit`, `VisibleConstraintAudit`). The named theorems we eyeballed - are real: `choreo-grade-commute` (`characteristic/RoleGraded.agda:193`) and - `client-to-server-injective-on-proj₁` (`characteristic/ChoreoInjective.agda:136`). - _Honest note on output:_ the run prints `UnsupportedIndexedMatch` *warnings* - that originate in the stdlib worktree's own `Relation/Nullary/Decidable.agda` - (the lib sets `--warning=noUnsupportedIndexedMatch`); they are warnings, not - errors, and the typecheck exits 0. We grepped the output for `error` / `unsolved` - and found none. -* *Zero postulates / escape pragmas in the green closure.* No module reachable - from `proofs/agda/All.agda` carries a `postulate`, `TERMINATING`, `trustMe`, - or `primTrustMe`. We confirmed this by grepping the shipped tree: the only - `postulate`-bearing files (`EchoImageFactorizationPropPostulated.agda`, - `Ordinal/Buchholz/Fidelity.agda`) are NOT imported by `All.agda` (see - <>); the only `TERMINATING`-bearing files are under the unwired - `proofs/agda/experimental/` tree. +* *The verified module closure typechecks green — this session.* + `agda --safe --without-K -i proofs/agda -i . -i /home/user/absolute-zero/proofs/agda proofs/agda/All.agda` + *exits 0*. `proofs/agda/All.agda` forces *153 top-level `open import`s* (the Echo + core, the establishment-track Pillar A–D modules, the F1–F5 earn-back gates, the + audience-facing modules, `EchoAggregation`, the deniability module, and the whole + `Ordinal.*` / `Ordinal.Buchholz.*` / `Ordinal.Brouwer.*` notation tower), all + under `--safe --without-K`. `proofs/agda/Smoke.agda` *exits 0* too. +* *The characteristic lane typechecks green — this session.* + `agda --safe --without-K … proofs/agda/characteristic/All.agda` *exits 0*; a grep + of its output for `error`/`unsolved` finds nothing. +* *Postulate-free, escape-free GREEN CLOSURE.* No module reachable from + `proofs/agda/All.agda` carries a `postulate`, `TERMINATING`, `trustMe`, or + `primTrustMe`. We confirmed by grepping the tree: the only `postulate` + *declarations* are in `EchoImageFactorizationPropPostulated.agda` (one block) and + `Ordinal/Buchholz/Fidelity.agda` (two blocks) — *neither imported by* `All.agda` + (see <>). * *The funext-free kernel certificate holds.* `sh scripts/kernel-guard.sh` *exits 0*: "Check A — cone is `{ Echo, EchoKernel }`, no funext / postulate / escape" PASS, and "Check B — all `Echo*.agda` modules are classified in the kernel note" PASS. +* *The general aggregation theorem is real (#175).* `EchoAggregation.agda` — the + `Monoid` / `GroupAggregator` records, the proved `aggregation-as-fold` law, the + `sum`/`count`/`max`/`min` instances, the generic `no-canonical-disaggregation-of`, + and the macro `Example-PairSum` anchor — is in the green closure, zero postulates. * *The experimental ℕ∪{∞} grade dioid is proved-but-unwired.* - `proofs/agda/experimental/echo-additive/Grade.agda` (the R0 min-plus / tropical - grade semiring, `Grade = ℕ ∪ {∞}` with `_+g_` and `_⊓g_`) typechecks standalone - under `--safe --without-K`, *exit 0*, zero postulates — but it is *absent from - `All.agda`*, so it does not count toward the verified-closure claims above. We - record it as a real-but-not-wired-in artefact, exactly as found. + `proofs/agda/experimental/echo-additive/Grade.agda` typechecks standalone under + `--safe --without-K`, *exit 0*, zero postulates — but is *absent from `All.agda`*, + so it does not count toward the closure claims above. [#nuance] === The honest nuance you must not lose (proved CORE vs everything else) @@ -225,126 +185,110 @@ The green `--safe --without-K` typecheck proves that *the Agda in the closure is internally consistent and the stated lemmas hold as written*. It does NOT prove: * *that the ordinal notation faithfully denotes the Bachmann–Howard ordinal.* - Order-type fidelity is an _external mathematical claim_ deliberately isolated - as TWO named `postulate`s in `Ordinal/Buchholz/Fidelity.agda` (a height-preserving + Order-type fidelity is an _external mathematical claim_ deliberately isolated as + TWO named `postulate`s in `Ordinal/Buchholz/Fidelity.agda` (a height-preserving denotation `⟦·⟧` and an `ordinal-upper-bound`). That module is OUTSIDE the - `--safe` kernel cone *by design* — not imported by `All.agda`/`Smoke.agda` — so - the green closure depends on none of those postulates, and equally does not - _prove_ them. `Fidelity-OPEN-postulates.md` is the standing record. Anyone - reading "Bachmann–Howard, mechanized" as "BH is a closed theorem here" is - over-reading; the honest claim is "a notation system, with sound-carrier - well-foundedness proved, aimed at BH, with the order-type bridge left as an - explicit auditable trust boundary." + `--safe` kernel cone *by design* — not imported by `All.agda`/`Smoke.agda` — so the + green closure depends on none of those postulates, and equally does not _prove_ + them. `Fidelity-OPEN-postulates.md` is the standing record. Read "Bachmann–Howard, + mechanized" as "a notation system, sound-carrier well-foundedness proved, aimed at + BH, with the order-type bridge left as an explicit auditable trust boundary." * *that the truncated (epi, mono) image factorisation holds in the safe core.* It needs propositional truncation; the safe `EchoImageFactorizationProp` is - zero-postulate, while the truncated demonstration is confined to the unwired - `EchoImageFactorizationPropPostulated.agda` (four scoped, documented postulates). -* *that any downstream consumer (EchoTypes.jl, ephapax, …) faithfully - implements this calculus.* That is a separate, unverified bridge in each - consumer repo, not something this typecheck touches. + zero-postulate, the truncated demonstration is confined to the unwired + `EchoImageFactorizationPropPostulated.agda` (postulated `∥_∥`) — and that `∥_∥` is + *constructed for real* in the separate `--cubical` island + `EchoImageFactorizationPropCubical.agda` (a different flag profile, by design not + importable into the `--safe --without-K` cone). +* *that any downstream consumer (Oikos, EchoTypes.jl, ephapax, …) faithfully + implements this calculus.* The Oikos macro-aggregation bridge cites the + `EchoAggregation` principle at the *citation level* (there is no Agda↔Rust import + path); it is a separate, unverified bridge, not something this typecheck touches. "Proved core calculus" + "documented trust boundaries kept out of the core" + "aspirational milestone narrative in the README" are three different things, and -we are naming them as three. +we name them as three. === Known-incomplete but honestly fenced (loud, never a silent green) -* *The `Justfile` is stale and partly fictional — do not trust its `@echo`s.* - Its `build-echo`/`test-*` recipes call paths that *do not exist at this commit* - (e.g. `proofs/agda/Echo/Core.agda`, `proofs/agda/Echo/Bridges/EchoCNOBridge.agda`), - and `build-echo` runs bare `agda -i proofs/agda …` with no stdlib wiring, so on - this machine (dangling registry path) it would fail to find the library. Worse, - the `stability-report` / `test-all` recipes *print* hard-coded numerals - ("Stability: 92/100", "Core Echo Types 98/100", "✅ All tests passed") that are - *not computed from anything* — they are `@echo` literals, not a checked result. - We are NOT citing them. The real, runnable verification is the two `agda … - All.agda` commands in <> plus `scripts/kernel-guard.sh`. +* *The `Justfile` is stale — carried from the 2026-06-16 audit, not re-run today.* + Per that audit its `stability-report` / `test-all` recipes *print* hard-coded + numerals ("92/100" etc.) that are `@echo` literals, not computed results, and some + recipes reference paths that do not exist. We did *not* re-execute the `Justfile` + this session and we are NOT citing its numerals. The real, runnable verification is + the `agda … All.agda` / `Smoke.agda` / `characteristic/All.agda` commands plus + `scripts/kernel-guard.sh` in <>. === Outstanding / weak / refuted (no spin) * *Unbudgeted global well-foundedness for native `_<ᵇ_` is OPEN and, as stated, - argued-unclosable.* The repo's own record (`RankBrouwer.agda` preamble, - `buchholz-rank-obstruction.adoc`) is that the rank-embedding route is walled by - the `<ᵇ-+Ω` counterexample; the achievable result is WF for the _sound carriers_ - (`_<ᵇ⁰_`, `_<ᵇ²_`, `_<ᵇʳᶠ²_`), which ARE in the green closure. The native global - WF is not a gap we are claiming closed. -* *Bachmann–Howard order-type fidelity: postulated (trust boundary), not proved* - — see <>. -* *Truncated (epi, mono) image factorisation: postulated* in a separate, - unwired module; the safe core proves only the K-free `injective-fibres-proj-unique` - fragment. -* *Several "full" results are honestly funext-/UIP-qualified* (the F4/F5 - earn-back gates take `funext` as an explicit hypothesis; the constant-fibre - `↔ A` packaging needs UIP on `B`). These are stated as qualified, not as - unconditional, in their modules — and that qualification is the honest content, - not a defect. + argued-unclosable* (`RankBrouwer.agda` preamble, `buchholz-rank-obstruction.adoc`); + the achievable result is WF for the _sound carriers_ (`_<ᵇ⁰_`, `_<ᵇ²_`, `_<ᵇʳᶠ²_`), + which ARE in the green closure. +* *Bachmann–Howard order-type fidelity: postulated (trust boundary), not proved* — + see <>. ε₀ has been climbed (`OrdinalExp.agda`), but ε₀ ≪ Γ₀ ≪ … ≪ ψ₀(Ω_ω); + the milestone is not reached. +* *Truncated (epi, mono) image factorisation: postulated* in an unwired module + (and constructed in a separate `--cubical` island); the safe core proves only the + K-free `injective-fibres-proj-unique` fragment. +* *Several "full" results are honestly funext-/UIP-qualified* (the F4/F5 earn-back + gates take `funext` as an explicit hypothesis). That qualification is the honest + content, not a defect. * *The retracted "graded comonad" reading stands retracted* (R-2026-05-18): echo-types is a loss-graded _reindexing modality_ (thin-poset action); the - experimental `echo-additive/` tree's own STATE records the variance question as - settled toward "graded MONAD, not comonad/adjunction". None of that experimental - work is wired into the shipped closure. -* *Status docs vs live run.* The `Justfile` numerals are refuted by the live - runs (above). The repo's `CLAUDE.md` build note cites "Agda 2.6.3 + stdlib 2.3"; - we actually verified green under *Agda 2.8.0* with the stdlib *worktree*. Where - those differ, the live run wins. + experimental `echo-additive/` tree is not wired into the shipped closure. [#reproduce] == Reproduce it yourself -From the repo root, at the commit above. First wire the working stdlib (the -machine's registered path is dangling at this commit), then typecheck: +From the repo root, at the commit above, with `~/.agda/libraries` registering the +stdlib 2.3 + absolute-zero paths (already the case on the verifying machine): [source,sh] ---- -# 1. Point Agda at the WORKING stdlib worktree + absolute-zero (env-local, -# does not touch the repo). Adjust paths to your checkout. -export AGDA_DIR="$(mktemp -d)" -cat > "$AGDA_DIR/libraries" <<'LIBS' -/home/hyperpolymath/developer/worktrees/agda-stdlib-tweak/standard-library.agda-lib -/home/hyperpolymath/developer/repos/absolute-zero/absolute-zero.agda-lib -LIBS - -# 2. Typecheck the verified closure (expect exit 0). -agda --safe --without-K -i proofs/agda proofs/agda/All.agda - -# 3. Typecheck the characteristic lane (expect exit 0; stdlib -# UnsupportedIndexedMatch WARNINGS print but are not errors). -agda --safe --without-K -i proofs/agda proofs/agda/characteristic/All.agda - -# 4. Funext-free kernel certificate + classification lint (expect exit 0). +# 1. Typecheck the verified closure (expect exit 0; 153 modules ending at Smoke). +LC_ALL=C.UTF-8 agda --safe --without-K \ + -i proofs/agda -i . -i /home/user/absolute-zero/proofs/agda \ + proofs/agda/All.agda + +# 2. Smoke pins (expect exit 0). +LC_ALL=C.UTF-8 agda --safe --without-K \ + -i proofs/agda -i . -i /home/user/absolute-zero/proofs/agda \ + proofs/agda/Smoke.agda + +# 3. Characteristic lane (expect exit 0; no error/unsolved). +LC_ALL=C.UTF-8 agda --safe --without-K \ + -i proofs/agda -i . -i /home/user/absolute-zero/proofs/agda \ + proofs/agda/characteristic/All.agda + +# 4. Funext-free kernel certificate + classification lint (expect exit 0 / PASS). sh scripts/kernel-guard.sh # Optional: the experimental, UNWIRED ℕ∪{∞} grade dioid (expect exit 0; -# this is NOT part of the verified closure). -agda --safe --without-K -i proofs/agda proofs/agda/experimental/echo-additive/Grade.agda +# NOT part of the verified closure). +LC_ALL=C.UTF-8 agda --safe --without-K \ + -i proofs/agda -i . -i /home/user/absolute-zero/proofs/agda \ + proofs/agda/experimental/echo-additive/Grade.agda ---- -Expected outputs at this commit: - -* Step 2 → `agda … All.agda` exits `0` (151 top-level modules forced through the - checker, ending at `Checking Smoke … `). -* Step 3 → `agda … characteristic/All.agda` exits `0`; `grep -iE 'error|unsolved'` - over its output finds nothing (only stdlib `-W…UnsupportedIndexedMatch` warnings). -* Step 4 → `kernel-guard: PASS — funext-free certificate enforced; classification in sync.` -* Optional → `Grade.agda` exits `0`. - -*Do NOT* rely on `just build-all` / `just test-all` / `just stability-report` to -reproduce these: those recipes reference non-existent paths and print hard-coded -"92/100" numerals that are not a computed result (see the loud-failure note above). +*Do NOT* rely on `just build-all` / `just test-all` / `just stability-report`: +those recipes print hard-coded numerals that are not a computed result (see the +loud-failure note above). == One-line characterisation (quote this) [quote] ____ "A real constructive Agda library for structured loss (`Echo f y := Σ x, f x ≡ y`) -whose verified closure typechecks green under `--safe --without-K` with zero -postulates and a funext-free kernel certificate — a genuinely machine-checked -CORE plus a large sound-carrier ordinal-notation tower — with Bachmann–Howard -order-type fidelity left as an explicit, isolated POSTULATE outside that core, -the experimental additive-grade work proved-but-unwired, and a stale `Justfile` -whose stability numerals are decorative, not checked. Serious foundational -artefact; the headline 'BH mechanized' is a milestone-in-progress, not a closed -theorem. No intentional overclaim." +whose verified closure typechecks green under `--safe --without-K` with a +funext-free, postulate-free kernel certificate — a genuinely machine-checked CORE +(now including the general monoid/group aggregation theorem) plus a large +sound-carrier ordinal-notation tower — with Bachmann–Howard order-type fidelity +left as an explicit, isolated POSTULATE outside that core, the experimental +additive-grade work proved-but-unwired, and a stale `Justfile` whose stability +numerals are decorative, not checked. Serious foundational artefact; the headline +'BH mechanized' is a milestone-in-progress, not a closed theorem. No intentional +overclaim." ____ == Joint attestation @@ -354,15 +298,14 @@ timestamp above, every claim in this file is true and was checked as described* — with no intentional overclaim, and with the open gaps stated rather than hidden. -* *Engineering party (AI):* Claude Opus 4.8 (`claude-opus-4-8[1m]`) — ran the - build/test/proof checks recorded here (the two `agda … All.agda` typechecks, - `scripts/kernel-guard.sh`, and the standalone `Grade.agda` check) on - 2026-06-16T12:16:59Z and stands behind the wording above as a faithful report - of those runs. +* *Engineering party (AI):* Claude Opus 4.8 — ran the build/proof checks recorded + here (the `agda … All.agda` / `Smoke.agda` / `characteristic/All.agda` + typechecks, `scripts/kernel-guard.sh`, the postulate grep, and the standalone + `Grade.agda` check) on 2026-06-19 and stands behind the wording above as a + faithful report of those runs. * *Owner / maintainer:* Jonathan D.A. Jewell — _signs by committing this file - with `-S` (`id_ed25519_signing`); the git commit signature over this content, - at the commit SHA recorded above, is the cryptographic form of this - affirmation._ + with `-S`; the git commit signature over this content, at the commit SHA recorded + above, is the cryptographic form of this affirmation._ + Signed-off-date: ____________________ (fill on signing) diff --git a/docs/status/STATUS-2026-06-19.adoc b/docs/status/STATUS-2026-06-19.adoc new file mode 100644 index 0000000..0fdbf80 --- /dev/null +++ b/docs/status/STATUS-2026-06-19.adoc @@ -0,0 +1,173 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += STATUS — musts / intends / wishes, as of 2026-06-19 +:toc: macro +:toclevels: 2 + +_A dated, cross-repo status snapshot grouped into the three commitment tiers, +with the normative MUST being the **Oikos accounting DSL** (the compiler +guarantee "a model that violates an accounting identity does not compile"). +This copy lives in `echo-types`; an identical-in-substance copy lives in +`oikos/docs/status/`. This file is the **detail behind the chat status table**._ + +[NOTE] +==== +*Three tiers.* *MUST* = the normative core the whole programme must deliver +(the Oikos compiler guarantee). *INTENDS* = funded, designed, in-flight work +we mean to land. *WISHES* = desirable, unscheduled, or externally-gated. + +Status labels are honest: *(Landed)* = real + checked this session; *(Partial)* = +real but scoped/incomplete; *(Open)* / *(Blocked)* = not done, with the blocker +named. Where a doc and a live toolchain run disagree, **the live run wins** and +the contradiction is flagged. +==== + +toc::[] + +== Where echo-types sits in this programme + +`echo-types` is the **verified proof companion**. It does not host the Oikos +compiler (that is Rust, in the `oikos` repo). echo-types supplies the +machine-checked *principle* the MUST's economics reading rests on: that +micro→macro aggregation is a structured-loss (`Echo`) map with **no canonical +disaggregation** — there is no left inverse (section) recovering the micro +ledger from the macro total. That is the Sonnenschein–Mantel–Debreu / +representative-agent critique stated type-theoretically, and as of 2026-06-18 +(issue #175) it is the *general* monoid/group aggregation theorem, with the +macro economics as one instance (`Example-PairSum`). + +== MUST — the normative core (the Oikos compiler guarantee) + +[cols="3,3,1,4",options="header"] +|=== +| Item | What it guarantees | Status | Evidence (live this session) + +| Godley column-sum balance +| A model whose Godley matrix columns do not net to zero is *rejected at compile* +| (Landed) +| `oikos-check` `godley_check` — `check_model` returns `Err(GodleyImbalance{sector,net})` on imbalance, `Ok` on balance; 10 tests green + +| Instrument coverage +| Every instrument is accounted across sectors +| (Landed) +| `oikos-check` `instrument_check` — 11 tests green + +| Currency soundness +| `GBP + USD` and Stock+Flow mixes are type errors +| (Landed) +| `oikos-check` `currency_check` — 4 tests green; phantom types in `oikos-syntax` + +| Cross-reference / name resolution +| Dangling references do not resolve +| (Landed) +| `oikos-check` `cross_ref` + `resolve` — 4 tests green + +| Surface parser (Logos + Chumsky) +| Source text parses to the typed AST +| (Partial) +| `oikos-parser` — 33 tests green (further along than the README's "in progress") + +| Desugar → Ephapax IR +| Lower to Ephapax's linear-typed / region / typestate IR +| (Blocked) +| `oikos-desugar` — 0 tests, stub; **blocked on the upstream Ephapax parser milestone** + +| Verified economics principle the MUST rests on +| Micro→macro aggregation is non-disaggregable (no canonical section) +| (Landed) +| echo-types `EchoAggregation` general form (#175), `--safe --without-K`, green + +| End-to-end source → verdict pipeline +| parse → check → desugar wired as one path +| (Partial) +| check + parse green *separately*; full wiring gated on the desugar block +|=== + +== INTENDS — designed / in-flight + +[cols="3,4,2",options="header"] +|=== +| Item | Note | Status + +| `alib` aggregate library (Route A vs B) +| Bridge accounting/bookkeeping ↔ the macroeconomic disciplines, over `MacroState`. Route B (aggregation-morphism library) recommended; **owner decision still open** +| (Design / owner-gated) + +| EchoAggregation macro reading +| The SMD / representative-agent critique as the `MacroAggregation` instance of the general theorem +| (Cited) — `oikos/docs/alib-aggregate-bridge.adoc`; echo-types `Example-PairSum` + +| betlang stochastic seam +| Probabilistic wagers over `MacroState` (ternary `bet` DSL, Racket) +| (Design) + +| `EchoTypes.jl` executable mirror +| Add an `EchoAggregation` finite-domain shadow to the Julia falsifier +| (Intended — not this session) + +| OikosBot AffineScript port +| Code-analysis GitHub App (the *other* Oikos product; separate from the DSL) +| (In-flight) — `oikos/bot-integration-affine/` +|=== + +== WISHES — desirable, unscheduled, or externally-gated + +[cols="3,4,2",options="header"] +|=== +| Item | Note | Status + +| Full SFC model library +| Runnable Godley–Lavoie models end-to-end through the compiler +| (Wish) — gated on the desugar block + +| Ephapax integration complete +| Inherit linear types, Tofte–Talpin regions, typestate from Ephapax +| (Wish) — gated on upstream `hyperpolymath/ephapax` + +| Bachmann–Howard milestone (echo-types ordinal track) +| ψ₀(Ω_ω) order-type fidelity for the Buchholz notation +| (Open) — `Ordinal/Buchholz/Fidelity.agda` carries the fidelity as a *postulated* trust boundary (`D-2026-06-14`); ε₀ climbed, milestone not reached + +| External validation / publication +| TYPES extended abstract + CPP/ITP paper; formal SFC semantics +| (Wish) — echo-types `paper.adoc` has open `[EXPAND]` tags +|=== + +== echo-types internal state (the proof layer), 2026-06-19 + +* *Verified closure green this session.* `agda --safe --without-K … proofs/agda/All.agda` + *exits 0* (153 top-level modules forced, ending at `Smoke`); `… Smoke.agda` *exits 0*; + `characteristic/All.agda` *exits 0* (no `error`/`unsolved`); `sh scripts/kernel-guard.sh` + *PASS* (cone `{Echo, EchoKernel}`, no funext / postulate / escape; all `Echo*.agda` classified). +* *Establishment track Pillars A–D complete* (graded-comonad reading retracted under + R-2026-05-18; the shipped framing is a loss-graded reindexing modality). +* *EchoAggregation generalised to the monoid/group form (#175)* — `Monoid`, + `GroupAggregator`, the proved `aggregation-as-fold` law, the + `sum/count/max/min` instances, the generic `no-canonical-disaggregation-of`, + and the macro `Example-PairSum` anchor. Green, zero postulates in the cone. +* *Ordinal track:* well-foundedness proved for the **sound carriers** + (`_<ᵇ⁰_`, `_<ᵇ²_`, `_<ᵇʳᶠ²_`); native global WF for `_<ᵇ_` is argued-unclosable + as stated; BH order-type fidelity is the explicit postulated boundary. +* *Honest fences (not in the green cone):* exactly two `postulate`-bearing files — + `Ordinal/Buchholz/Fidelity.agda` (the two BH-fidelity postulates) and + `EchoImageFactorizationPropPostulated.agda` (the truncation, *constructed for real* + in the `--cubical` island `EchoImageFactorizationPropCubical.agda`). Neither is + imported by `All.agda`/`Smoke.agda`. The F4/F5 "full" results are funext-qualified + by design. + +== Honest cross-cutting notes + +* The normative MUST is **real and tested at the check layer on the AST** (the + Godley/instrument/currency/cross-ref tests build hand-constructed models and + assert reject-on-violation). It is *not yet* demonstrated end-to-end from + surface source through the parser and desugar, because desugar is blocked. +* echo-types contributes the *principle*, not the *enforcement*: there is no + Agda↔Rust import path. The bridge is citation-level by design. + +== See also + +* `AFFIRMATION.adoc` (this repo) — the dated, signed, falsifiable receipt for the + echo-types green closure at the anchored commit. +* `oikos/AFFIRMATION.adoc` + `oikos/docs/status/STATUS-2026-06-19.adoc` — the + Oikos-side receipt and the same tables from the compiler's vantage. +* `docs/bridges/cross-repo-bridge-status.md` — the standing cross-repo bridge ledger.