Merge branch 'main' into claude/inspiring-meitner-QHuNU

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -14,11 +14,20 @@
 # S-expr schema reference was:
 #   https://github.com/hyperpolymath/standards/blob/main/state-a2ml/spec/abnf/state.abnf
 #
-# Purpose: machine-readable current project state. The PRIMARY landed
-# workstream is the Buchholz/Ordinal rank-monotonicity + well-foundedness
-# track (Slice 3+4 Route A arc). The EI-2 termination capture (April
-# 2026) is preserved below as history — it prevents EI-2 from being
-# re-investigated, but it is no longer the whole document identity.
+# Purpose: machine-readable current project state.
+#
+# CURRENCY NOTE (2026-06-21): the ordinal / Buchholz track is RETIRED from
+# echo-types (owner decision D-2026-06-21) — it outgrew the project and is
+# being extracted to its own ordinal-notation repo (physical cut = owner;
+# tracking issue #263; hand-off record
+# docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc). The
+# detailed [recent-work] and [current-workstream] blocks below are preserved
+# as accurate HISTORY of the 2026-06-05 → 2026-06-12 arc, NOT live work. The
+# live tracks as of 2026-06-21 are: composition (landed); establishment
+# (Pillars A–D + F closed; Pillar E in-repo complete at the bounded-claim
+# level; order-type fidelity the one OPEN external problem, D-2026-06-14);
+# variance resolved (#243); aggregation generalised (#175). The EI-2
+# termination capture (April 2026) remains preserved below as history.
 
 [metadata]
 project = "echo-types"
@@ -29,9 +38,9 @@ version-target = "0.1.1"             # CHANGELOG still [Unreleased] over
                                      # [0.1.0+integration-pending]; no new
                                      # release tag minted as of 2026-06-12
 license = "MPL-2.0"
-last-updated = "2026-06-12"
+last-updated = "2026-06-21"
 status = "active development"
-phase = "ordinal track (Gate 1 blocked, Gate 3 mechanical-open) + Pillar E write-up + estate governance adopted"
+phase = "ordinal track RETIRED (D-2026-06-21, extraction pending #263); composition landed; establishment Pillars A–D+F closed + Pillar E in-repo complete (order-type fidelity OPEN external, D-2026-06-14); variance resolved (#243); aggregation generalised (#175)"
 
 # ============================================================
 # Recent work (2026-05-30 → 2026-06-12, from git log origin/main)

wiki/Home.adoc

@@ -46,6 +46,48 @@ toc::[]
   affine mode.
 |===
 
+== Who is this for?
+
+echo-types serves three audiences. Find your lane, then follow the reading order.
+
+[cols="1,3", options="header"]
+|===
+| You are… | Start here, in order
+
+| *A developer* +
+  (writing or extending proofs)
+| 1. <<Working-Rules.adoc#,Working-Rules>> — the non-negotiable discipline
+  (`--safe --without-K`, zero postulates, Smoke pins, `All.agda` wiring). +
+  2. `CLAUDE.md` — current rung-state + the per-arc *DO NOT reopen* lists. +
+  3. <<Architecture.adoc#,Architecture>> + `docs/echo-types/MAP.adoc` — the
+  module map and where a new theorem belongs. +
+  4. *Build:* `bash scripts/provision-agda.sh`, then
+  `agda -i proofs/agda proofs/agda/All.agda` (and `Smoke.agda`) must exit 0.
+
+| *A maintainer* +
+  (gates, releases, governance)
+| 1. <<Roadmap.adoc#,Roadmap>> + `roadmap-gates.adoc` — the three identity
+  gates and their *failure actions* (gates are reassessed every tagged
+  release). +
+  2. `docs/retractions.adoc` — how a failed gate is recorded (never silently
+  revised). +
+  3. `scripts/kernel-guard.sh` + `.github/workflows/agda.yml` — the CI cone
+  that must stay green. +
+  4. `.machine_readable/6a2/STATE.a2ml` (EI-2 record + current state) and
+  `docs/bridges/cross-repo-bridge-status.md` (downstream ledger).
+
+| *An end user* +
+  (wiring Echo into another language)
+| 1. `FOUNDATION_CONTRACT.md` — the stable `Echo.*` interface and the boundary
+  invariant *Echo IS-NOT a resource instance*. Read this first. +
+  2. <<Overview.adoc#,Overview>> — what Echo adds and, crucially, what it does
+  *not* add (honest scope). +
+  3. *EchoTypes.jl* — the executable Julia shadow; falsifies-by-counterexample
+  on concrete finite data. +
+  4. <<Deniability.adoc#,Deniability>> — a worked first-class echo property to
+  see the shape of a consumer-facing result.
+|===
+
 == Canonical sources of truth
 
 This wiki is a *distillation*. The authoritative records are:
@@ -61,11 +103,27 @@ This wiki is a *distillation*. The authoritative records are:
 * `.machine_readable/6a2/STATE.a2ml` — EI-2 record (permanent) + current-state block.
 * `docs/bridges/cross-repo-bridge-status.md` — cross-repo bridge ledger.
 
-== One-line status (as of 2026-06-13)
-
-* *Composition track* — landed (Echo-comp-iso, cancel-iso, pentagon).
-* *Ordinal track* — partial (Buchholz; Slice 3+4 Route A; target Bachmann–Howard ψ₀(Ω_ω)).
-* *Establishment track* — Pillars A–D + Pillar F (F1–F4) closed; Pillar E paper open.
+== One-line status (as of 2026-06-21)
+
+* *Composition track* — landed (Echo-comp-iso, cancel-iso, pentagon). No open
+  headline items.
+* *Establishment track* — Pillars A–D and F (F1–F4) closed; the in-repo half of
+  Pillar E is complete at the bounded-claim level. One named *OPEN external*
+  problem remains: *order-type fidelity* to ψ₀(Ω_ω) (decision-log
+  `D-2026-06-14`).
+* *Variance* — resolved (`EchoVariance.agda`, #243): an echo is a graded
+  *monad of accumulation* with a section/retraction adjunction exact on the
+  grade-0 fibre — *not* a graded comonad (that reading is the lossless
+  complement-storing writer).
+* *Aggregation* — `EchoAggregation.agda` generalised to the monoid/group form
+  (`aggregation-as-fold`; #175), with `no-canonical-disaggregation` (the
+  Sonnenschein–Mantel–Debreu / representative-agent critique, stated
+  type-theoretically).
+* *Ordinal track* — *RETIRED from echo-types* (owner decision `D-2026-06-21`):
+  the transfinite Buchholz/Veblen ladder outgrew the project. The landed
+  artifact is correct and stays; the disposition is *extraction to its own
+  ordinal-notation repo* (the physical cut is the owner's; tracking: #263).
+  See <<Roadmap.adoc#ordinal,Roadmap § Ordinal>>.
 * *Deniability track* — `EchoDeniability.agda` landed: perfect/partial duality,
   `IsConstantOpener` boundary, no-section / section duality as a checked theorem pair.
 

wiki/Roadmap.adoc

@@ -55,21 +55,25 @@ The base accumulation iso, cancellation iso, and pentagon coherence are all
 landed and packaged as `_↔_`. No open headline items; further work is
 consolidation / doc-threading.
 
-=== Ordinal track — partial (the active bottleneck)
-
-Target: *Bachmann–Howard* ψ₀(Ω_ω). Open, in priority order:
-
-. *Unbudgeted `_<ᵇʳᶠ_` global WF* — the GLOBAL form over native `_<ᵇ_`
-  is *walled* (all five standard routes; native `_<ᵇ_` is ordinally
-  unsound — see `buchholz-rank-obstruction.adoc`). The SOUND-CARRIER
-  form is *DONE* (2026-06-14, PR #212): `RecursiveSurfaceSound.wf-<ᵇʳᶠ²`
-  is unbudgeted, built over `_<ᵇ²_` + the doubled-ladder `rank2`
-  embedding. Remaining open is only the global-over-native form, whose
-  realistic close-out is a falsifiable "cannot close under
-  `--safe --without-K`" verdict rather than a positive proof.
-. *Full constructor set beyond the admitted core* — the K-limited shared-binder
-  cases `<ᵇ-ψα`, `<ᵇ-+2`.
-. *Push the surface-route WF back* into `Order.agda`'s main `_<ᵇ_` package.
+[#ordinal]
+=== Ordinal track — RETIRED from echo-types (owner decision D-2026-06-21)
+
+The transfinite Buchholz/Veblen ascent *outgrew echo-types* and is *no longer
+echo-types work*. The landed artifact is correct (`--safe --without-K`, zero
+postulates, in the green closure) and *stays compiling*; *no new ordinal rung
+is opened here*. The disposition is *extraction to its own ordinal-notation
+repository* — the physical cross-repo cut is the owner's. Tracking: *#263*.
+
+* *Hand-off record* (frontier + inventory for the extracted repo, NOT a
+  resume-here plan): `docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc`.
+* *Firewall (verified):* `OmegaMarkers` ← `Buchholz.Syntax` ← `EchoOrdinal`
+  STAY (Echo Core's bridge); everything else under `proofs/agda/Ordinal/` MOVES.
+* *Frozen open items* (for the extracted repo only — NOT echo-types TODOs):
+  unbudgeted `_<ᵇʳᶠ_` global WF over native `_<ᵇ_` (the sound-carrier form
+  `RecursiveSurfaceSound.wf-<ᵇʳᶠ²` is already DONE, PR #212); the full
+  K-limited shared-binder constructor set (`<ᵇ-ψα`, `<ᵇ-+2`); and order-type
+  fidelity to ψ₀(Ω_ω) (`D-2026-06-14`, an OPEN *external* problem — retirement
+  neither closes nor over-claims it).
 
 === Establishment track — Pillar E only
 
@@ -92,8 +96,9 @@ Pillar E is complete at the bounded-claim level. Remaining:
 The full debt list, with effort/impact, lives in
 `.machine_readable/agent_instructions/debt.a2ml`. Highlights:
 
-* *Should:* the two ordinal WF items above; image factorisation (epi, mono)
-  earn-back (needs propositional truncation — a substantial design decision).
+* *Should:* image factorisation (epi, mono) earn-back (needs propositional
+  truncation — a substantial design decision). (The ordinal WF items moved out
+  with the ordinal-track retirement — see #263.)
 * *Could:* decoration-zoo wiring (Cost/Search/Indexed/Epistemic as
   ResidueForm/DecorationStructure instances); the Q2.1 truncation
   generalisation; rsr-conformance chores (@sha256 pins, README/roadmap