hyperpolymath · hyperpolymath · Jun 21, 2026 · Jun 21, 2026
@@ -14,7 +14,7 @@
 
 [metadata]
 project = "echo-types"
-last-updated = "2026-06-12"
+last-updated = "2026-06-21"
 
 # ============================================================
 # Architecture Decision Records
@@ -319,6 +319,38 @@ PRs #161/#162/#163.
 module = "proofs/agda/EchoEphapaxBridge.agda"
 supersedes = "none"
 
+[[architecture-decisions]]
+id = "adr-012"
+title = "Ordinal/Buchholz track RETIRED from echo-types; disposition = extraction"
+status = "accepted"
+date = "2026-06-21"
+context = """
+The transfinite ordinal / Buchholz / Veblen ascent (target ψ₀(Ω_ω)) outgrew
+echo-types. It was PARKED 2026-06-20 (D-2026-06-20: consumer-less after the
+Groove cleave resolved to a finite, well-foundedness-only zipper), then
+escalated to RETIRED 2026-06-21 (D-2026-06-21). The landed artifact is correct
+(--safe --without-K, zero postulates, in the green closure); Echo Core never
+depended on it beyond the OmegaMarkers <- Buchholz.Syntax <- EchoOrdinal bridge.
+"""
+decision = """
+No new ordinal rung is opened in echo-types. The disposition is extraction to
+its own ordinal-notation repository — the physical cross-repo cut is the
+owner's (tracking issue #263). Firewall: OmegaMarkers <- Buchholz.Syntax <-
+EchoOrdinal STAY; everything else under proofs/agda/Ordinal/ MOVES. Order-type
+fidelity to ψ₀(Ω_ω) (D-2026-06-14) remains an OPEN external problem —
+retirement neither closes nor over-claims it.
+"""
+consequences = """
+The [recent-work] / [current-workstream] blocks in STATE.a2ml are preserved as
+HISTORY of the 2026-06-05 -> 2026-06-12 ordinal-track arc, not live work.
+Hand-off record: docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc.
+Live tracks: composition (landed); establishment (Pillars A–D+F closed, Pillar
+E in-repo complete at the bounded-claim level); variance resolved (#243);
+aggregation generalised (#175).
+"""
+module = "proofs/agda/Ordinal/ (whole subtree except the STAY firewall)"
+supersedes = "none"
+
 # ============================================================
 # Development practices (relevant subset)
 # ============================================================

@@ -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-18.
+Last updated: 2026-06-21.
 
 This file is the single status ledger for echo-type bridge work that
 touches other repositories.
@@ -14,7 +14,7 @@ touches other repositories.
 | CNO bridge (Agda) | `proofs/agda/EchoCNOBridge.agda` | `absolute-zero/proofs/agda/CNO.agda` (direct import) | **Content-bridge done.** Bridge imports `IsCNO`, `empty-is-cno`, `halt-is-cno`, `cno-composition`, `absolute-zero-is-cno`, `seq-comp` from absolute-zero's `CNO.agda` and exhibits `cno-program-echo : (p : Program) → IsCNO p → ProgramEcho p` plus three concrete instances. `CNO.agda` builds clean under `--safe --without-K`, no postulates. | — (closed at content-bridge level; cross-prover theorem-statement alignment is the next row.) |
 | CNO core theorem alignment | `EchoCNOBridge` theorem family | `absolute-zero/proofs/coq/common/CNO.v`, `absolute-zero/proofs/lean4/CNO.lean` | Name-by-name correspondence table drafted (see §"CNO Agda↔Coq↔Lean4 correspondence" below). | (1) Coq's `eval` is relational; Agda+Lean are functional. (2) Coq has no `absolute_zero` alias. (3) Coq's single-instruction CNO is `nop_is_cno`; Agda+Lean use `halt_is_cno`. (4) Coq carries 3 axioms (`eval_deterministic`, `eval_respects_state_eq_{left,right}`) that echo-types' `--safe --without-K` policy forbids — porting must re-route through a functional formulation, where they hold by `refl`. (5) `ProgramEcho`/`Echo` itself is currently unilateral (Agda-only). |
 | JanusKey bridge | `proofs/agda/EchoJanusBridge.agda` | `januskey/src/abi/Types.idr` (`OpKind`, `IsFileOp`, `IsKeyOp`); `januskey/PROOF-NEEDS.md` | Name-bridge only — Agda side has a *local* 4-variant `JanusOp = Create \| Delete \| Modify \| Move`; canonical Idris2 ABI defines 8-variant `OpKind = Copy \| Move \| Delete \| Modify \| Obliterate \| KeyGen \| KeyRotate \| KeyRevoke` plus `IsFileOp`/`IsKeyOp` predicates. Already drifted (Create vs Copy; missing Obliterate + 3 key ops). | Decision recorded: structural-mirror the Agda enum to januskey's Idris2 `OpKind`; content-bridge deferred until januskey's `PROOF-NEEDS.md` lands content-bearing semantics. Agda↔Idris2 has no FFI, so any content-bridge must run via shared schema or trusted extraction. |
-| Tropical alignment | `proofs/agda/EchoTropical.agda` | `tropical-resource-typing/Tropical.thy`, `tropical-resource-typing/TropicalSessionTypes.lean` (and 8 other `.thy` files) | Adjacent repo audit complete (2026-05-20). Repo present at `repos-monorepo/verification-ecosystem/tropical-resource-typing`; remote `hyperpolymath/tropical-resource-typing` active (last push 2026-05-18, language=Isabelle). First alignable theorem pair identified: Agda `⊕-idem` ↔ Isabelle `trop_add_idem` ↔ Lean `add_comm_trop`+`add_assoc_trop`. | Agda cannot import `.thy` or `.lean` directly; alignment is citation-level (statement correspondence with build-side independent proof per language), not import-level. Long-game target: `Tropical_Ordinal_Bridge.thy` ↔ echo-types ordinal track. |
+| Tropical alignment | `proofs/agda/EchoTropical.agda` | `tropical-resource-typing/Tropical.thy`, `tropical-resource-typing/TropicalSessionTypes.lean` (and 8 other `.thy` files) | Adjacent repo audit complete (2026-05-20). Repo present at `repos-monorepo/verification-ecosystem/tropical-resource-typing`; remote `hyperpolymath/tropical-resource-typing` active (last push 2026-05-18, language=Isabelle). First alignable theorem pair identified: Agda `⊕-idem` ↔ Isabelle `trop_add_idem` ↔ Lean `add_comm_trop`+`add_assoc_trop`. | Agda cannot import `.thy` or `.lean` directly; alignment is citation-level (statement correspondence with build-side independent proof per language), not import-level. Long-game target: `Tropical_Ordinal_Bridge.thy` ↔ the (now-RETIRED, extracting) echo-types ordinal track — that long-game alignment moves with the ordinal extraction (echo-types#263, owner decision D-2026-06-21); it is not an echo-types deliverable. |
 | EchoTypes.jl executable mirror | Tier-1+Tier-2 spine + unconditional F5 OFS fragment (modules: `Echo`, `EchoResidue`, `EchoFiberCount`, `EchoThermodynamics`, plus 2026-05-27 v0.2.0 additions: `EchoTotalCompletion`, `EchoOrthogonalFactorizationSystem`, `EchoImageFactorization`, `EchoNoSectionGeneric`, `EchoLossTaxonomy`, `EchoEntropy`, `EchoObservationalEquivalence`) | [`hyperpolymath/EchoTypes.jl`](https://github.com/hyperpolymath/EchoTypes.jl) v0.2.0 (pinned to `e7dded6`); registered in `julia-professional-registry` | **Executable companion shipped.** Mirrors run the finite-domain shadow of the upstream theorems on concrete data and falsify-by-counterexample; the companion makes no proof claims, the Agda here remains the source of truth. R-2026-05-18 retraction surface NOT mirrored; F5 funext-qualified clauses (uniqueness up to iso, diagonal lifting) NOT mirrored — Julia has no funext, the claims would be vacuous. UIP- and truncation-strength upgrades likewise honestly not mirrored. | — (shipped; honest scope holds verbatim from upstream). Future advances on the Tier-1+Tier-2 spine are candidates for new shadows in subsequent EchoTypes.jl releases, but no in-repo CI dependency exists in either direction. |
 | Ephapax L3 bridge (Agda↔Coq) | `proofs/agda/EchoEphapaxBridge.agda` | `ephapax/formal/Echo.v` (Coq, 584 lines, 24 `Qed`, zero `Admitted` / zero `Axiom`) — explicit port of `EchoLinear.agda` + `EchoResidue.agda` under a K-free / zero-axiom discipline equivalent to `--safe --without-K` | **Navigability bridge done; content bridge NARROW** (2026-05-30). Two definitional `refl`-renames: `ephapax-L3-weaken = EchoLinear.weaken` and `ephapax-L3-no-section-collapse = EchoResidue.no-section-collapse-to-residue`. Coq headlines `mode_le_prop`, `weaken_collapses_distinction`, `affine_canonical`, `degrade_mode_comp`, `no_section_collapse_to_residue` (line 502-517) each match an Agda counterpart pinned in `Smoke.agda`. Scope: **L3 only** — ephapax-affine has Rust checkers only; L1 has 5 `Axiom` + 11 `Admitted`; L4 has no mechanised theorems yet (cf. ephapax `formal/PRESERVATION-DESIGN.md`, `docs/echo-types/paper.adoc` §"Threats to validity"). | Per-bridge docs `docs/bridges/ECHO-EPHAPAX-BRIDGE.adoc` (CNO-equivalent) not yet authored; tracked as follow-up issue. Full content bridge (round-trip CI between Agda + Coq) would require an Agda mirror of ephapax `formal/Echo.v` and is **not foreclosed** by the NARROW stub. |
 | Valence Shell / Ochránce accountable-shell bridge (exploratory, downstream) | Structured-loss vocabulary only — `EchoResidue` / `EchoResidueTaxonomy` / `EchoLossTaxonomy` / `EchoObservationalEquivalence` / `EchoNoSectionGeneric` cited at the reading-aid level. **No bridge module**; nothing added to `All.agda`, `Smoke.agda`, or `EchoCanonicalIdentitySuite.agda`. | Valence Shell (`hyperpolymath/valence-shell`) — shell state transitions, undo/redo, checkpoints, diff/replay. Ochránce (`hyperpolymath/ochrance`) — A2ML manifests, Merkle state commitments, repair/attestation surfaces. | **Exploratory — candidate downstream consumer. Core Affect: NO.** Echo Types' structured-loss semantics may *classify* shell state transitions by residue / loss form (recoverable / constrained / residue-bearing / observationally equivalent / genuinely lost); Ochránce may supply concrete receipt evidence. Downstream application evidence only — not a new foundation. No mechanised cross-repo theorem currently exists. Companion: `docs/bridge-status.md` §7 and `docs/echo-types/explorations/accountable-shell/README.adoc`. | No shared schema and no Agda↔Idris2 / Agda↔Rust import path; the relationship is citation-level only. Echo Types makes **no** claim about Valence Shell / Ochránce implementation correctness, and **no** claim about POSIX, Rust, the Lean→Rust correspondence, secure deletion, GDPR, cryptographic integrity, or attestation. Valence Shell's RMR/RMO vocabulary, if referenced, is downstream application vocabulary and is not adopted into the Echo Types core. |

@@ -44,6 +44,14 @@ toc::[]
   (constant / no-section) case and the partial (injective / has-section)
   case, with the `IsConstantOpener` boundary and its connection to the
   affine mode.
+
+| <<Tutorial-Consuming-Echo.adoc#,Tutorial: Consuming Echo>>
+| End-user walkthrough: the one definition, making/reading an echo, the
+  totality completion, the no-section boundary, and four real consumers.
+
+| <<Maintainer-Runbook.adoc#,Maintainer Runbook>>
+| Gate-keeping + release runbook: the build cone, the identity gates,
+  rung-consolidation, machine-doc currency, and the release checklist.
 |===
 
 == Who is this for?
@@ -74,7 +82,9 @@ echo-types serves three audiences. Find your lane, then follow the reading order
   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).
+  `docs/bridges/cross-repo-bridge-status.md` (downstream ledger). +
+  5. <<Maintainer-Runbook.adoc#,Maintainer Runbook>> — the full gate-keeping +
+  release runbook (build cone, gates, rung-consolidation, release checklist).
 
 | *An end user* +
   (wiring Echo into another language)
@@ -85,7 +95,9 @@ echo-types serves three audiences. Find your lane, then follow the reading order
   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.
+  see the shape of a consumer-facing result. +
+  5. <<Tutorial-Consuming-Echo.adoc#,Tutorial: Consuming Echo>> — the
+  from-the-outside-in walkthrough (definition → totality → no-section → consumers).
 |===
 
 == Canonical sources of truth

@@ -0,0 +1,117 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Maintainer Runbook
+:toc: macro
+:toclevels: 2
+
+[.lead]
+For *maintainers* — gate-keeping changes, keeping the proof cone green, keeping
+the documentation honest, and cutting releases. Authoritative sources:
+`roadmap-gates.adoc`, `CLAUDE.md` (current-rung-state + per-arc DO-NOT-reopen
+lists), and `.machine_readable/6a2/`.
+
+toc::[]
+
+== 1. The non-negotiable build cone
+
+Every change must hold the invariant:
+
+[source,sh]
+----
+agda -i proofs/agda proofs/agda/All.agda     # exits 0
+agda -i proofs/agda proofs/agda/Smoke.agda   # exits 0
+sh scripts/kernel-guard.sh                   # PASS
+----
+
+under `--safe --without-K`, with *zero postulates* in the load-bearing tracks
+and no escape pragmas (`believe_me`, `assert_total`, `postulate`, `sorry`,
+`Admitted`, `unsafeCoerce`). Every headline theorem is pinned in `Smoke.agda`;
+every new module is wired into `All.agda` (an orphan module that compiles but
+is not in `All.agda` is treated as dead code).
+
+== 2. The identity gates (the falsifiability contract)
+
+The identity claim rests on three gates, each with an explicit *failure action*
+(see <<Roadmap.adoc#,Roadmap>> and `roadmap-gates.adoc`):
+
+. *Distinct phenomenon* — echo types name structured loss as distinct from
+  refinement types / lenses / HoTT fibres / quotients / provenance semirings.
+. *Characteristic theorems* — at least two theorems are naturally echo-shaped,
+  not generic Σ lemmas.
+. *Canonical examples* — at least one fully worked example where echo types are
+  the right explanatory unit.
+
+Gates are *reassessed at every tagged release* — surviving one round grants no
+immunity in the next. A failed gate is recorded in `docs/retractions.adoc` (a
+new dated `R-`/`F-` entry), *never silently revised*. Retractions are the
+mechanism that makes the claim falsifiable; they are not failures of the repo.
+
+== 3. When a proof rung lands — rung-consolidation policy
+
+Per `CLAUDE.md`, each named theorem / iso-shape that lands triggers:
+
+. *Branch housekeeping* — enumerate open remote branches ahead of `main`;
+  decide landing / superseded / abandoned.
+. *Cherry-pick* to a consolidation branch off latest `main`, in dependency
+  order (conflicts are usually additive, in `Smoke.agda` / `All.agda`).
+. *Human docs* — sweep `roadmap.adoc`, `docs/echo-types/composition.md`,
+  `overview.md`, and the wiki for stale `(Open)` tags; use honest labels
+  `(Landed)` / `(Partial)` / `(Open)`.
+. *Machine docs* — update `CLAUDE.md` current-rung-state and the `6a2/` files
+  (see Section 4).
+. *Verify* — the build cone (Section 1).
+. *Fast-forward `main`* and push.
+. *Session ledger* — record the rung, the commits folded in, the remaining
+  open pieces, and the smallest useful next advance.
+
+== 4. Machine-doc currency discipline
+
+When a *track's status changes*, the change must propagate to all of:
+
+* `.machine_readable/6a2/STATE.a2ml` — `[metadata]` phase + the current-workstream
+  framing (historical blocks are preserved, not deleted; mark them HISTORY).
+* `.machine_readable/6a2/META.a2ml` — add an ADR for any architecture-level
+  decision (status / supersedes per `[development-practices.versioning-of-decisions]`).
+* `docs/bridges/cross-repo-bridge-status.md` — the bridge ledger.
+* the wiki (<<Home.adoc#,Home>> one-line status + <<Roadmap.adoc#,Roadmap>>).
+
+Worked example: the 2026-06-21 ordinal-track *retirement* (`D-2026-06-21`) was
+swept through STATE.a2ml (currency note + phase), META.a2ml (adr-012), the
+bridge ledger (Tropical long-game row), and the wiki — keeping human and
+machine documentation consistent. Mirror that pattern.
+
+== 5. Release checklist
+
+Versioning is SemVer 2.0.0 (current target `0.1.1`; recipe-extension target
+`0.2.0+`). To cut a release:
+
+. [ ] Build cone green (Section 1) on `main`.
+. [ ] Identity gates reassessed (Section 2); any failure recorded in
+  `docs/retractions.adoc`.
+. [ ] `CHANGELOG.md` updated; `[Unreleased]` rolled to the version.
+. [ ] Machine docs current (Section 4): `6a2/STATE.a2ml`, `META.a2ml`,
+  bridge ledger, wiki one-line status.
+. [ ] Tag minted; mirrors (gitlab, codeberg) consistent.
+. [ ] *Then*, author-driven and *not* auto-run: Zenodo DOI, installable library
+  packaging, outreach. Flag to the owner; do not start unprompted.
+
+== 6. CI lanes and known parked failures
+
+Substantive lanes that must stay green: Agda (`check` + `cold-check`),
+`governance/*`, the secret scanners (`gitleaks`/`trufflehog`/`*-secrets`),
+CodeQL (`analyze`), and Hypatia. A docs-only change passes the Agda lanes
+trivially (no `.agda` touched).
+
+*Parked, do not chase:* `scorecard.yml` / `mirror.yml` `startup_failure` at 0s
+is the billing-wall *pattern B* (a structural reusable-workflow failure, not a
+Guix/Nix policy failure). Hypatia may post pre-existing repo-level findings
+(e.g. a stale Scorecard `TokenPermissionsID` code-scanning alert that cannot
+auto-clear while Scorecard is billing-walled); confirm the Hypatia *check
+conclusion* (it is usually `success`) before treating a comment as a gate.
+
+== 7. Branch hygiene
+
+Single-`main` policy (Hypatia `GS007`). Remote-branch deletion is *owner /
+GitHub-UI only* — agents get HTTP 403 and the MCP has no delete-branch
+endpoint, so stale-branch cleanup is flagged in an issue and actioned by the
+owner.