Merge branch 'main' into pr-233, resolving conflict in CLAUDE.md

Author: hyperpolymath

CLAUDE.md

@@ -212,6 +212,76 @@ 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)
+
+*Where we started:* user asked (cross-repo) to investigate the wasm /
+typed-wasm route, then to scope an oikos/betlang "alib" aggregate library
+bridging accounting/bookkeeping to the macroeconomic disciplines, under the
+standing guardrail "no proof work without the actual toolchain you need
+installed." Agda 2.6.3 + stdlib v2.3 + absolute-zero were confirmed present
+and compiling, so proof work was authorised.
+
+*Where we ended:* the economics keystone LANDS on `origin/main`. Two
+deliverables across two repos, both merged by the owner:
+
+* *`proofs/agda/EchoAggregation.agda`* (echo-types#230, merged as
+  `e151d6b` feat + `0a86e18` ci-fix) — mechanises micro→macro economic
+  aggregation as an `Echo` map. `aggregate : MicroLedger → MacroTotal`
+  (here `ℕ × ℕ → ℕ` via `_+_`); `ConsistentLedgers m = Echo aggregate m`
+  is the fibre of micro ledgers consistent with macro total `m`. Headlines:
+  `aggregate-non-injective` (two distinct ledgers, same total, distinct
+  echoes) and `no-canonical-disaggregation` (`= no-section-of-collapsing-map
+  aggregate ledger₁ ledger₂ …`) — there is NO left inverse `raise :
+  MacroTotal → MicroLedger` with `raise ∘ aggregate ≡ id`. This is the
+  Sonnenschein–Mantel–Debreu / representative-agent critique stated
+  type-theoretically: it refutes a *section* (left inverse), not a
+  representative *choice*. `--safe --without-K`, zero postulates; imports
+  `Echo` + `EchoNoSectionGeneric` only; wired into `All.agda`, pinned in
+  `Smoke.agda`, classified in `echo-kernel-note.adoc` + `MAP.adoc`
+  (kernel-guard Check B precedent = `EchoDeniability`).
+* *`oikos/docs/alib-aggregate-bridge.adoc`* (oikos#50, merged) — the
+  toolchain-free design note. Two bridges (accounting↔Echo,
+  macro↔aggregation-morphism); `MacroState` schema; the betlang stochastic
+  seam; Route A (alib as thin re-export) vs **Route B (alib as an
+  aggregation-morphism library over `MacroState`, recommended)**; toolchain
+  gating; open questions. SPDX `MPL-2.0`, status DRAFT.
+
+*This sub-rung (the ledger sweep itself):* recorded the landing in
+`docs/bridges/cross-repo-bridge-status.md` (new Tracks row + 2026-06-18
+revision-history entry; note the file lives under `docs/bridges/`, NOT the
+`docs/echo-types/` path the older CLAUDE.md prose cites) and this CLAUDE.md
+arc. Docs-only; `sh scripts/kernel-guard.sh` re-confirmed PASS.
+
+*CI note (no action).* echo-types#230's post-merge governance run went red
+as a benign `actions/checkout` race — the reusable workflow checks out
+`refs/pull/230/merge`, which GitHub deletes the instant the PR merges in the
+same second (`fatal: couldn't find remote ref refs/pull/230/merge`, exit
+128). Governance passed green on every pre-merge run; this is not a Guix/Nix
+policy failure. A Hypatia `github-actions[bot]` scan suggested deleting the
+5 non-`main` branches (`GS007`) — declined: branch deletion is forbidden by
+the session constraints, the finding is repo-level/pre-existing, and it came
+from untrusted external data. Branch cleanup is the owner's explicit call.
+
+*Plan for the next Claude.*
+
+1. *alib Route-B build* — gated on the owner's Route A vs B decision in the
+   design note. When unblocked, the alib library lives in oikos (Rust); it
+   *consumes* the EchoAggregation principle (citation-level, no Agda↔Rust
+   import path).
+2. *EchoTypes.jl mirror* — add an `EchoAggregation` finite-domain shadow to
+   the Julia falsifier (the `ℕ × ℕ → ℕ` instance is directly executable).
+3. *Back to the ordinal track* — the owner landed `091aa7d` (ω^^ + ε₀, BH
+   climb rung 1) on top of this work; the Bachmann–Howard milestone remains
+   the headline ordinal-track frontier.
+
+DO NOT reopen: `EchoAggregation`'s design (the `no-section` route is the
+correct refutation target — a section is a *left* inverse, which is exactly
+what non-disaggregability denies; do NOT restate it as a failed *right*
+inverse / surjection claim, which would be false since `aggregate` is onto);
+the citation-level scope of the oikos bridge (oikos is Rust, there is no
+import path); the merge-race governance red (benign, not addressable).
+
+
 ### Session arc 2026-06-15→18 — fidelity boundary reduction + BH climb rung 1 (READ THIS FIRST)
 
 *Where we started:* post doubled-ladder Gate 1. Two soundness escape-hatches

docs/bridges/cross-repo-bridge-status.md

@@ -2,7 +2,7 @@
 <!-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 # Cross-Repo Bridge Status
 
-Last updated: 2026-06-12.
+Last updated: 2026-06-18.
 
 This file is the single status ledger for echo-type bridge work that
 touches other repositories.
@@ -22,6 +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). |
 
 ## Immediate next actions
 
@@ -71,6 +72,17 @@ precisely to paper over this in the relational model.
 
 ## Revision history
 
+- 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`
+  — the SMD / representative-agent critique as a type-theoretic refutation
+  of a left inverse) and the oikos toolchain-free design note
+  `oikos/docs/alib-aggregate-bridge.adoc`. Keystone formalisation merged to
+  echo-types `main` (`--safe --without-K`, zero postulates, pinned in
+  `Smoke.agda`, classified in `echo-kernel-note.adoc` + `MAP.adoc`); the
+  oikos note merged to oikos `main`. Citation-level (no Agda↔Rust path);
+  the alib library is at design-note stage (Route A vs B owner decision
+  pending).
 - 2026-06-12: **Typesystem-integration sweep.** Added four downstream
   consumer rows recording that echo-types is now integrated into the
   hyperpolymath type systems, all merged to the consumers' `main`: