From e6fda7ef630a39abcea5a672a144e4c2af649f9b Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 26 Oct 2026 16:56:15 +0000
Subject: [PATCH 1/2] docs: point the ordinal lane at
 hyperpolymath/ordinal-notation

echo-types#349 removed the ordinal lane, but the docs still described it
as present. Update them to match the tree.

- Living status documents now say the lane moved: CLAUDE.md, EXPLAINME,
  PROOF-STATUS, TOPOLOGY, roadmap Lane 3, MAP, proof-debt, bridge-status,
  proof-obligations, the kernel note, what-echo-is and the wiki.
- proof-debt: (d) is empty here. The two Fidelity postulates left with
  the lane, so one quarantined postulate block remains, under (c).
- EXPLAINME: correct "no Echo*.agda imports from Ordinal/".
  EchoOrdinal imports the two bridge leaves that stayed.
- The seven documents that moved with the lane keep a frozen copy here
  with a "moved" banner.
- Dated records (AFFIRMATION, proof logs, dated status files) are left
  as written. The paper's ordinal appendix gets a one-line note.

Docs only. kernel-guard and check-guardrails pass.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
---
 CHANGELOG.adoc                                | 19 ++++++
 CLAUDE.md                                     | 41 +++++++++--
 EXPLAINME.adoc                                | 14 +++-
 Fidelity-OPEN-postulates.adoc                 | 10 +++
 PROOF-STATUS.adoc                             | 48 +++++++------
 TOPOLOGY.adoc                                 |  4 +-
 docs/CLAIMS_AUDIT.adoc                        | 11 +++
 docs/bridge-status.adoc                       | 14 ++--
 docs/bridges/buchholz-extended-wf.adoc        | 10 +++
 docs/bridges/buchholz-plan.adoc               | 10 +++
 docs/bridges/buchholz-rank-obstruction.adoc   | 10 +++
 docs/echo-types/MAP.adoc                      | 68 ++++---------------
 .../echo-types/buchholz-rank-obstruction.adoc | 10 +++
 .../ordinal-bh-order-type-fidelity-open.adoc  | 10 +++
 .../ordinal-fidelity-ladder-parked.adoc       | 10 +++
 docs/echo-types/echo-kernel-note.adoc         |  8 ++-
 docs/echo-types/paper.adoc                    |  5 ++
 docs/echo-types/what-echo-is.adoc             |  4 +-
 docs/proof-debt.adoc                          | 59 +++++-----------
 docs/proof-obligations.adoc                   |  4 +-
 roadmap.adoc                                  | 16 ++++-
 wiki/Architecture.adoc                        |  6 +-
 wiki/Home.adoc                                |  8 +--
 wiki/Roadmap.adoc                             |  5 +-
 24 files changed, 252 insertions(+), 152 deletions(-)

diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index 375471d..9feccc1 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -7,6 +7,25 @@ Changelog].
 
 === [Unreleased]
 
+==== Removed (2026-10-20)
+
+* _The ordinal lane._ echo-types#349 removed `+proofs/agda/Ordinal/**+`
+except `+Ordinal/OmegaMarkers.agda+` and `+Ordinal/Buchholz/Syntax.agda+`,
+which the `+EchoOrdinal+` bridge imports. The lane now lives in
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation],
+carrying out decision `+D-2026-06-21+`. echo-types' quarantined postulates
+go from three to one: the two `+Fidelity.agda+` postulates left with the
+lane.
+
+==== Changed (2026-10-26)
+
+* _Docs point at ordinal-notation._ The living status documents (CLAUDE.md,
+EXPLAINME, PROOF-STATUS, TOPOLOGY, roadmap, MAP, proof-debt, bridge
+status, proof obligations, kernel note and the wiki) now say the ordinal
+lane has moved. The design documents that moved with it are kept here as
+frozen copies with a "moved" banner. Dated records (AFFIRMATION, proof
+logs, dated status files) are unchanged.
+
 ==== Removed (2026-09-30)
 
 * _The 27 `+.a2ml+` machine-readable records._ Removed by owner ruling:
diff --git a/CLAUDE.md b/CLAUDE.md
index 000b659..d684a0f 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -7,8 +7,8 @@ Adjacent projects, in one line each, for session bootstrapping:
 
 - echo-types — constructive Agda formalization of fiber-based structured
   loss ("echo types"); `Echo f y := Σ (x : A) , (f x ≡ y)`. Gated
-  identity-claim development; `--safe --without-K` throughout. Current
-  workstream: E (ordinal-notation / Buchholz collapsing layer).
+  identity-claim development; `--safe --without-K` throughout. The
+  ordinal-notation / Buchholz lane moved out on 2026-10-20 (see below).
   https://github.com/hyperpolymath/echo-types
 - PanLL — three-pane cognitive-relief HTI; Ambient/Symbolic/Neural/World panes.
   https://github.com/hyperpolymath/panll
@@ -40,6 +40,11 @@ Adjacent projects, in one line each, for session bootstrapping:
   repo 2026-05-30 — see echo-types#159) + `arghda-panll`
   (Gossamer/AffineScript presentation, planned). See docs/buchholz-plan.adoc
   appendix for the motivating proof pipeline.
+- ordinal-notation — the Brouwer / Veblen / Buchholz ordinal lane extracted
+  from echo-types on 2026-10-20 (#349; decision D-2026-06-21). Frozen
+  hand-off record; order-type fidelity to ψ₀(Ω_ω) OPEN, with its two
+  quarantined `Fidelity.agda` postulates.
+  https://github.com/hyperpolymath/ordinal-notation
 - EchoTypes.jl — executable Julia companion to echo-types, mirroring the
   finite-domain shadow of the Tier-1 + Tier-2 spine + the unconditional
   F5 OFS fragment. v0.2.0 (2026-05-27) extends v0.1.0's `Echo` /
@@ -72,7 +77,11 @@ Two active workstreams:
    the equivalence-record packaging `Echo-comp-pent-Σ-assoc :
    ... ↔ ...` (stdlib `Function.Bundles._↔_`) is in place.
 
-2. **Ordinal track — RETIRED FROM ECHO-TYPES (D-2026-06-21).** This research
+2. **Ordinal track — MOVED to hyperpolymath/ordinal-notation (2026-10-20,
+   #349).** Only `EchoOrdinal` + `Ordinal.OmegaMarkers` +
+   `Ordinal.Buchholz.Syntax` remain here; every other path named below is
+   gone from this repo. Ordinal TODOs belong in that repo. RETIRED FROM
+   ECHO-TYPES (D-2026-06-21). This research
    ladder *outgrew echo-types* and is no longer echo-types work: do NOT open new
    rungs here; the disposition is extraction to its own ordinal-notation repo
    (see `docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc` + the
@@ -215,7 +224,31 @@ work to `main` and refresh all documentation:
    name, the commits folded in, the remaining open pieces of the
    milestone, and the proposed smallest useful next advance.
 
-## Current rung state (2026-06-21)
+## Current rung state (2026-10-26)
+
+### Session arc 2026-10-20→26 — ordinal lane physically extracted (read this FIRST)
+
+The `D-2026-06-21` disposition is carried out. echo-types#349 (`b1dcc29`)
+removed `proofs/agda/Ordinal/**` except the two bridge leaves
+(`Ordinal/OmegaMarkers.agda`, `Ordinal/Buchholz/Syntax.agda`), unwired them
+from `All.agda` / `Smoke.agda`, and dropped `Fidelity` from the guardrail's
+`EXPLORATORY_EXEMPT`. The lane now lives in
+https://github.com/hyperpolymath/ordinal-notation (imported from `703dd77`,
+history kept in a filter-repo bundle; Agda under
+`verification/proofs/agda/`, gated by that repo's proof MANIFEST).
+
+* *Trust boundary here: 3 → 1 quarantined postulate block* —
+  only `EchoImageFactorizationPropPostulated` (c) remains. The two Fidelity
+  postulates left with the lane.
+* *Docs:* the living status docs point at the new repo. The moved design
+  documents (`docs/bridges/buchholz-*.adoc`,
+  `docs/echo-types/buchholz-rank-obstruction.adoc`, the two ordinal
+  decision records, `Fidelity-OPEN-postulates.adoc`) are kept here as
+  frozen copies with a "moved" banner. Dated records (AFFIRMATION,
+  CHANGELOG history, proof logs, dated STATUS files) are left as written.
+* *Ordinal sections in this file below are history.* Do not act on any
+  ordinal "next rung" / "open piece" here.
+
 
 ### Session arc 2026-06-21 (close-out) — gap-closing proofs #249–#258 + cross-repo docs audit + ⚠ ordinal-ledger contradiction flag (read this FIRST)
 
diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
index cdb1619..dc1e73d 100644
--- a/EXPLAINME.adoc
+++ b/EXPLAINME.adoc
@@ -147,10 +147,18 @@ Echo Core does NOT depend on the Ordinal / Buchholz track.
 ____
 
 How this is implemented::
-All ordinal modules live under `link:proofs/agda/Ordinal/[]`. No `Echo*.agda` file imports from `Ordinal/`. Dependency separation is structural (directory-level).
+The ordinal lane no longer lives here. It moved to
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]
+on 2026-10-20 (echo-types#349, decision `D-2026-06-21`). What stays in echo-types
+is the echo-to-ordinal bridge `link:proofs/agda/EchoOrdinal.agda[]` and the two
+small modules it imports, `Ordinal.OmegaMarkers` and `Ordinal.Buchholz.Syntax`.
+No other `Echo*.agda` file imports from `Ordinal/`.
 
 Caveat::
-The Ordinal track has open problems (unbudgeted `wf-<ᵇʳᶠ` closure, shared-binder internalization). These do not affect Echo Core. See `link:docs/buchholz-plan.adoc[]`.
+The ordinal lane's open problems (order-type fidelity to ψ₀(Ω_ω), the unbudgeted
+`wf-<ᵇʳᶠ` closure over the native order) are tracked in ordinal-notation. They do
+not affect Echo Core. The two bridge modules exist in both repositories and can
+drift; ordinal-notation's copies are the maintained ones.
 
 == Dogfooded Across The Account
 
@@ -200,7 +208,7 @@ The Ordinal track has open problems (unbudgeted `wf-<ᵇʳᶠ` closure, shared-b
 
 [CAUTION]
 ====
-**Buchholz shared-binder internalization is open.** The Ordinal track has well-foundedness for the current constructor core, but historical same-binder shapes are not internalized as constructors of the real order. Does not affect Echo Core. See `link:docs/buchholz-plan.adoc[]`.
+**The ordinal lane has moved.** The Buchholz / Veblen development, including its open problems, now lives in https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]. Only the `EchoOrdinal` bridge stays here. Does not affect Echo Core.
 ====
 
 == Evidence Index
diff --git a/Fidelity-OPEN-postulates.adoc b/Fidelity-OPEN-postulates.adoc
index a5d77d9..c7800ae 100644
--- a/Fidelity-OPEN-postulates.adoc
+++ b/Fidelity-OPEN-postulates.adoc
@@ -1,5 +1,15 @@
 == Fidelity — open postulates (trust boundaries)
 
+[IMPORTANT]
+====
+*Moved.* This document moved to
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]
+with the ordinal lane on 2026-10-20 (echo-types#349). The copy maintained there
+is the live one. This copy is frozen as of echo-types `703dd77`, and the
+`proofs/agda/Ordinal/…` paths it names, other than `OmegaMarkers` and
+`Buchholz/Syntax`, no longer exist in this repository.
+====
+
 Companion to `+proofs/agda/Ordinal/Buchholz/Fidelity.agda+`. Open
 problem *`+D-2026-06-14+`*
 (`+docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc+`).
diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 45c6bfa..0c17470 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -8,8 +8,11 @@
 Honest status of the echo-types Agda formalisation: what is *proved*, what is
 *open*, and the build/guardrail invariant. echo-types is a constructive Agda
 development (`--safe --without-K`); the main verified suite (`proofs/agda/All.agda`)
-is *postulate-free*. The single isolated exception (the order-type *Fidelity*
-scaffold) is enumerated explicitly below.
+is *postulate-free*. The one quarantined postulate block outside that suite
+(the `--safe --without-K` shadow of propositional truncation) is enumerated
+below. The ordinal lane, including its order-type *Fidelity* scaffold, moved to
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]
+on 2026-10-20.
 
 == Build invariant (verified)
 
@@ -47,41 +50,36 @@ scaffold) is enumerated explicitly below.
 `EchoDeniability`, and `EchoAggregation` (micro→macro aggregation as an Echo
 map; `aggregate-non-injective` + `no-canonical-disaggregation`).
 
-=== Ordinal / Buchholz track (sound carrier)
-* Doubled-ladder relation `_<ᵇ²_` over the 12 core constructors + the umbrella
-  `rank2-mono-<ᵇ²` + `wf-<ᵇ²` (Gate 1 closed *for the sound carrier*).
-* `RecursiveSurfaceSound._<ᵇʳᶠ²_` + its *unbudgeted* `wf-<ᵇʳᶠ²`.
-* `Ordinal/Brouwer/OrdinalExp.agda` — `ω^^_` + the first ε-number `ε₀`
-  (Bachmann–Howard climb rung 1).
-* `Ordinal/Buchholz/BHTarget.agda` — a real `BHNotation` order + its
-  well-foundedness (no postulate).
+=== Ordinal / Buchholz track — moved
+The ordinal lane left echo-types on 2026-10-20 (echo-types#349, decision
+`D-2026-06-21`) and now lives in
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation],
+with its results and open problems. What stays here is the echo-to-ordinal
+bridge `EchoOrdinal` (`ordinal-collapse-non-injective`) and the two modules it
+imports, `Ordinal.OmegaMarkers` and `Ordinal.Buchholz.Syntax`.
 
 == Open (honest — NOT proved)
 
-* *Bachmann–Howard milestone* `ψ₀(Ω_ω)` order-type fidelity — *OPEN*
-  (`D-2026-06-14`). ε₀ is astronomically below the target
-  (ε₀ ≪ Γ₀ ≪ … ≪ ψ₀(Ω_ω)); the collapsing-function climb is the multi-session
-  frontier. The headline ordinal milestone is *not* reached.
-* *`Ordinal/Buchholz/Fidelity.agda` — 2 isolated postulates* (`denotation`,
-  `ordinal-upper-bound`). These are the ONLY postulates in the development,
-  quarantined under `Ordinal/Buchholz/` and tracked in `docs/.../proof-debt.md`
-  + `Fidelity-OPEN-postulates.md`. Dischargeable once the target collapse
-  heights exist.
+* *Bachmann–Howard order-type fidelity* — *OPEN*, now tracked in
+  ordinal-notation together with its two quarantined postulates (`denotation`,
+  `ordinal-upper-bound`).
+* *`EchoImageFactorizationPropPostulated.agda` — 1 isolated postulate block*
+  (four truncation primitives). Not imported by `All.agda`; tracked as (c) in
+  `docs/proof-debt.adoc`.
 * *(epi, mono) image truncation* — `∥_∥` is *constructed* only in the
   `--cubical` island `EchoImageFactorizationPropCubical.agda`; under
   `--safe --without-K` it remains a shadow (it cannot be built within
   `--safe --without-K` without HITs).
-* *Unbudgeted global `wf-<ᵇʳᶠ` over native `_<ᵇ_`* — walled: native `_<ᵇ_` is
-  ordinally unsound (documented counterexample), so no rank embedding maps it.
-  The achievable form landed on the sound carrier (`wf-<ᵇʳᶠ²`).
 * *Pillar E paper* (`docs/echo-types/paper.adoc`) — LIVING DRAFT with `[EXPAND]`
   tags (background, related work, evaluation, ordinal consumer-evidence
-  appendix gated on the BH milestone). Not submitted.
+  appendix gated on the BH milestone, now an ordinal-notation milestone). Not
+  submitted.
 
 == Discipline
 
-* No `postulate` in load-bearing tracks (the 2 Fidelity postulates are the
-  sole, isolated, documented exception).
+* No `postulate` in load-bearing tracks (the one truncation-shadow block in
+  `EchoImageFactorizationPropPostulated.agda` is the sole, isolated, documented
+  exception).
 * Every headline theorem is pinned in `Smoke.agda`; every module is wired into
   `All.agda` (orphan modules that compile but are not in `All.agda` are treated
   as dead code).
diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc
index 94bcd32..2567720 100644
--- a/TOPOLOGY.adoc
+++ b/TOPOLOGY.adoc
@@ -13,7 +13,7 @@ echo-types/
 │       ├── EchoCharacteristic.agda
 │       ├── EchoExamples.agda
 │       ├── Echo*Bridge.agda     # cross-system bridges (linear/graded/tropical/etc.)
-│       ├── Ordinal/             # Buchholz / Veblen track
+│       ├── Ordinal/             # bridge leaves only (OmegaMarkers, Buchholz/Syntax); the ordinal lane moved to hyperpolymath/ordinal-notation
 │       ├── examples/            # concrete usage demos
 │       └── characteristic/      # characteristic-style results (RoleGraded, etc.)
 ├── docs/                        # supplementary documentation
@@ -55,7 +55,7 @@ This is a foundation library; consumers are downstream Agda formalisations and d
 | Core echo theorems | constructive Agda, no postulates | `echo-intro`, `map-over`, `map-over-id`, `map-over-comp`, `map-square`
 | Characteristic family | constructive | `collapse-non-injective`, `no-section-*`, `echo-true≢echo-false`, `visible-constraint`
 | Bridge modules | constructive (per bridge) | linear / graded / tropical / choreo / epistemic / CNO / Janus / Dyadic / Ordinal
-| Ordinal Buchholz track | mostly admitted, some closed | `WellFounded`, extended-order tower; closure pending
+| Ordinal Buchholz track | moved (2026-10-20) | Now in https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]; only the `EchoOrdinal` bridge and its two imports stay here
 | EI-2 (integration recipe) | TERMINATED NEGATIVELY (PATH B) | Per-axis halves proved; full 2D iff theorem parked as not formalisable in safe Agda without postulates
 |===
 
diff --git a/docs/CLAIMS_AUDIT.adoc b/docs/CLAIMS_AUDIT.adoc
index d92790b..4d04440 100644
--- a/docs/CLAIMS_AUDIT.adoc
+++ b/docs/CLAIMS_AUDIT.adoc
@@ -15,6 +15,17 @@ unjustified; the rows pair each surface sentence with a proposed
 `(module, theorem)` mapping or the literal token `NONE-PROPOSED` when
 no in-repo artefact corresponds.
 
+[NOTE]
+====
+*Since 2026-10-20 the ordinal lane is no longer in this repository.* It
+moved to
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]
+(echo-types#349). Rows below that map to `Ordinal.*`, `Ordinal/Buchholz/*`
+or `Ordinal/Buchholz/Smoke.agda` (S-002, S-015, S-063 and others) describe
+the tree as audited, not the current one. Only `EchoOrdinal`,
+`Ordinal.OmegaMarkers` and `Ordinal.Buchholz.Syntax` remain here.
+====
+
 toc::[]
 
 == Scope and absent surfaces
diff --git a/docs/bridge-status.adoc b/docs/bridge-status.adoc
index 6d4bf2f..3aac636 100644
--- a/docs/bridge-status.adoc
+++ b/docs/bridge-status.adoc
@@ -32,16 +32,12 @@ but broader ecosystem mapping remains incomplete.
 
 === 4. Buchholz / Veblen Ordinals
 
-* *Status:* PARTIAL (11/13 constructors closed under WfCNF; 1 in flight)
+* *Status:* MOVED (2026-10-20) to
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]
+(echo-types#349). Status, blockers and open problems are tracked there.
 * *Dependencies:* Standard Agda
-* *Blockers:* `+<ᵇ-+1+` joint-bplus is the single remaining open
-constructor. The head-Ω domination route (option A) has its abstraction
-+ per-marker dominances at both branches + the option-(b) head-Ω
-inversion lemmas all landed across 2026-05-27 (PRs #124 / #130 / #131);
-only the WfCNF-carrier structural recursion (Slice 2-bplus) remains. The
-earlier shared-binder-self-lift blocker is resolved (`+RankAdm+` +
-`+RankLex+` slices, 2026-05-26/27). Live tracker:
-`+docs/echo-types/buchholz-rank-obstruction.adoc+`.
+* *Still here:* the `+EchoOrdinal+` bridge and its two imports
+(`+Ordinal.OmegaMarkers+`, `+Ordinal.Buchholz.Syntax+`).
 * *Core Affect:* NO
 
 === 5. JanusKey / Categorical
diff --git a/docs/bridges/buchholz-extended-wf.adoc b/docs/bridges/buchholz-extended-wf.adoc
index 76c377f..16219db 100644
--- a/docs/bridges/buchholz-extended-wf.adoc
+++ b/docs/bridges/buchholz-extended-wf.adoc
@@ -1,5 +1,15 @@
 == Buchholz `+_<ᵇ⁺_+`: well-foundedness gap
 
+[IMPORTANT]
+====
+*Moved.* This document moved to
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]
+with the ordinal lane on 2026-10-20 (echo-types#349). The copy maintained there
+is the live one. This copy is frozen as of echo-types `703dd77`, and the
+`proofs/agda/Ordinal/…` paths it names, other than `OmegaMarkers` and
+`Buchholz/Syntax`, no longer exist in this repository.
+====
+
 `+Ordinal.Buchholz.OrderExtended._<ᵇ⁺_+` adds two shared-binder lex
 constructors on top of `+Ordinal.Buchholz.Order._<ᵇ_+`:
 
diff --git a/docs/bridges/buchholz-plan.adoc b/docs/bridges/buchholz-plan.adoc
index dd267b4..496423a 100644
--- a/docs/bridges/buchholz-plan.adoc
+++ b/docs/bridges/buchholz-plan.adoc
@@ -6,6 +6,16 @@
 :sectnums:
 :sectnumlevels: 2
 
+[IMPORTANT]
+====
+*Moved.* This document moved to
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]
+with the ordinal lane on 2026-10-20 (echo-types#349). The copy maintained there
+is the live one. This copy is frozen as of echo-types `703dd77`, and the
+`proofs/agda/Ordinal/…` paths it names, other than `OmegaMarkers` and
+`Buchholz/Syntax`, no longer exist in this repository.
+====
+
 [CAUTION]
 ====
 *Historical spec.*  This document is the original phased plan for the
diff --git a/docs/bridges/buchholz-rank-obstruction.adoc b/docs/bridges/buchholz-rank-obstruction.adoc
index 4b7adb4..1086ee1 100644
--- a/docs/bridges/buchholz-rank-obstruction.adoc
+++ b/docs/bridges/buchholz-rank-obstruction.adoc
@@ -3,6 +3,16 @@
 :date: 2026-05-20
 :toc:
 
+[IMPORTANT]
+====
+*Moved.* This document moved to
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]
+with the ordinal lane on 2026-10-20 (echo-types#349). The copy maintained there
+is the live one. This copy is frozen as of echo-types `703dd77`, and the
+`proofs/agda/Ordinal/…` paths it names, other than `OmegaMarkers` and
+`Buchholz/Syntax`, no longer exist in this repository.
+====
+
 This note records why the natural rank-embedding route to unbudgeted
 `WellFounded _<ᵇʳᶠ_` (and to `WellFounded _<ᵇ⁺_`) is *structurally
 impossible* for the `Ordinal.Buchholz.Order._<ᵇ_` relation as
diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc
index f4fe625..6d3493f 100644
--- a/docs/echo-types/MAP.adoc
+++ b/docs/echo-types/MAP.adoc
@@ -381,59 +381,21 @@ the standing B- freeze lifted because O-THERMO-∞ is now discharged
   `docs/adjacency/hott-fibers.adoc`.
 * Build: `just test-thermo`.
 
-=== Buchholz / Veblen ordinals — higher-order number systems `[REAL]`
-Staged Buchholz-style collapsing in `--safe --without-K`.
-
-* Proofs: `proofs/agda/Ordinal/` (`Buchholz/`, `Brouwer`, `CNF`,
-  `Closure`, `Psi…`, `ExtendedOrder`, `RankPow`, `RankAdm`,
-  `RankLex`, `HeadOmega`, `HeadOmegaInversion`, `RankPowDomination`,
-  `RankPowSlice3` (2026-05-28 — `NonBzero` + strict-jump bridge +
-  head-Ω lower bound), `RankPowSlice3Headline` (2026-05-28 — Slice 3
-  headline `rank-mono-<ᵇ-+1-via-head-Ω` closed under a strict-head
-  premise; umbrella case-split bumps `bpsi=bpsi at equal markers`
-  to rank-adm / rank-lex)), `RankLexJointBplus` (2026-05-28 PR #147
-  — parallel rank with `leftmost-α` discriminator for the bpsi-source-
-  at-equality joint-bplus sub-case; second-component strict-mono at
-  equal first components scaffolded; (a)+(b)+(c) assembly
-  completed 2026-05-30 via PRs #165 (b lex-first primitive) + #166
-  (c `BplusFirstTri` trichotomy + `first-eq-from-bpsi-source-at-
-  equal-head` consumer-side derivation)), `RankMonoUmbrellaSlice4`
-  (2026-05-28 PR #149 — narrowed `_<ᵇ⁻ⁿ_` umbrella record bundling
-  WfCNF endpoints + `_<ᵇ¹_` derivation; covers all 10 inherited
-  `_<ᵇ⁰_` cases + the strict-head joint-bplus; two shortfalls
-  (`<ᵇ-ψΩ≤` boundary; `<ᵇ-+1` at equal-head) pinned as `⊤`-aliases
-  with explicit lex-rank / rank-lex-jb pointers),
-  `RankMonoSameLeft` (2026-05-30 PR #167 — Path-3 prototype
-  source-rule enrichment via `<ᵇ⁺²-same-left`; one-line closure via
-  `rank-pow-bplus-right-mono`), `RankMonoUnion` (2026-05-30 PR #168
-  — architectural realisation: union umbrella
-  `_<ᵇᵘ_ = _<ᵇ¹_ ⊎ _<ᵇ⁺²_` via Sum + `[_,_]` mediator; per-extension
-  proof work + structural composition; extension recipe in preamble),
-  `RankMonoUnionWfCNF` (2026-05-30 PR #169 — WfCNF wrap `_<ᵇᵘⁿ_`
-  bundling canonical-form invariant alongside the union; mirrors
-  Slice 4's pattern, propagates automatically through new
-  extensions), `RankMonoUnionWF` (2026-05-30 PR #170 — Gate 2
-  closure: `WellFounded _<ᵇᵘ_` via `Subrelation.wellFounded` +
-  `On.wellFounded` rank-embedding transport from `wf-<′`).
-* Fidelity climb (2026-06-15 → 18): `Ordinal.Buchholz.BHTarget` (the
-  BH order-type target structure + its well-foundedness CONSTRUCTED
-  for real from the Brouwer order `Ord`/`_<′_`/`wf-<′`; zero
-  postulates; reduces the `Fidelity.agda` trust boundary from three
-  postulates to two), and `Ordinal.Brouwer.OrdinalExp` (ordinal
-  exponentiation `ω^^_ : Ord → Ord` + the first ε-number `ε₀`; rung 1
-  of the target-side climb). Order-type fidelity (ψ₀(Ω_ω)) itself
-  remains OPEN (`D-2026-06-14`) — these shrink the trust boundary and
-  start the climb; ε₀ ≪ ψ₀(Ω_ω).
-* Docs: `docs/buchholz-plan.adoc`,
-  `docs/echo-types/buchholz-extended-wf.md`,
-  `docs/echo-types/buchholz-rank-obstruction.adoc` (per-constructor
-  verdict table — see ledger for live count).
-* Direct-constructor `_<ᵇ_` same-binder cases (Buchholz item B):
-  status tracked solely in the earn-back ledger
-  (`docs/echo-types/earn-back-plan.adoc`, row B) and
-  `docs/retractions.adoc` (F-2026-05-18b) — off the paper critical
-  path. (Reference-only by design: no status is snapshotted here, so
-  this line never drifts as the ledger moves.)
+=== Buchholz / Veblen ordinals — moved to ordinal-notation
+The ordinal lane left echo-types on 2026-10-20 (echo-types#349, decision
+`D-2026-06-21`). Its proofs, design documents and open problems, including
+order-type fidelity to ψ₀(Ω_ω) and the two `Fidelity.agda` postulates, now
+live in
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation].
+
+* Still here: `proofs/agda/EchoOrdinal.agda` (the echo-to-ordinal bridge,
+  `ordinal-collapse-non-injective`) and the two modules it imports,
+  `proofs/agda/Ordinal/OmegaMarkers.agda` and
+  `proofs/agda/Ordinal/Buchholz/Syntax.agda`.
+* The design documents (`docs/bridges/buchholz-*.adoc`,
+  `docs/echo-types/buchholz-rank-obstruction.adoc` and the two ordinal
+  decision records) are kept here as frozen copies, each marked as moved.
+  The maintained copies are in ordinal-notation.
 
 === Characteristic / EI — epistemic, choreographic, roles `[REAL]`
 The echo-invariant line: epistemic structure, choreographies, roles.
diff --git a/docs/echo-types/buchholz-rank-obstruction.adoc b/docs/echo-types/buchholz-rank-obstruction.adoc
index d1f399d..089b104 100644
--- a/docs/echo-types/buchholz-rank-obstruction.adoc
+++ b/docs/echo-types/buchholz-rank-obstruction.adoc
@@ -3,6 +3,16 @@
 :date: 2026-05-20
 :toc:
 
+[IMPORTANT]
+====
+*Moved.* This document moved to
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]
+with the ordinal lane on 2026-10-20 (echo-types#349). The copy maintained there
+is the live one. This copy is frozen as of echo-types `703dd77`, and the
+`proofs/agda/Ordinal/…` paths it names, other than `OmegaMarkers` and
+`Buchholz/Syntax`, no longer exist in this repository.
+====
+
 This note records why the natural rank-embedding route to unbudgeted
 `WellFounded _<ᵇʳᶠ_` (and to `WellFounded _<ᵇ⁺_`) is *structurally
 impossible* for the `Ordinal.Buchholz.Order._<ᵇ_` relation as
diff --git a/docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc b/docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc
index 27a3909..f0a6ba2 100644
--- a/docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc
+++ b/docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc
@@ -7,6 +7,16 @@
 :sectnumlevels: 2
 :icons: font
 
+[IMPORTANT]
+====
+*Moved.* This document moved to
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]
+with the ordinal lane on 2026-10-20 (echo-types#349). The copy maintained there
+is the live one. This copy is frozen as of echo-types `703dd77`, and the
+`proofs/agda/Ordinal/…` paths it names, other than `OmegaMarkers` and
+`Buchholz/Syntax`, no longer exist in this repository.
+====
+
 [.lead]
 Records the remaining ordinal-track frontier in the same dated idiom
 as the retraction log's `R-2026-05-18`, so it is findable in the
diff --git a/docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc b/docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc
index bbd1009..d6da988 100644
--- a/docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc
+++ b/docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc
@@ -7,6 +7,16 @@
 :sectnumlevels: 2
 :icons: font
 
+[IMPORTANT]
+====
+*Moved.* This document moved to
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]
+with the ordinal lane on 2026-10-20 (echo-types#349). The copy maintained there
+is the live one. This copy is frozen as of echo-types `703dd77`, and the
+`proofs/agda/Ordinal/…` paths it names, other than `OmegaMarkers` and
+`Buchholz/Syntax`, no longer exist in this repository.
+====
+
 [.lead]
 Records, in the same dated idiom as `D-2026-06-14` (its parent) and the
 retraction log's `R-2026-05-18`, the decision to *park* the transfinite
diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc
index bb37e71..57011c9 100644
--- a/docs/echo-types/echo-kernel-note.adoc
+++ b/docs/echo-types/echo-kernel-note.adoc
@@ -231,9 +231,11 @@ kernel** — the boundary is real and lives outside this core.
   discoverability. Not kernel (the kernel remains exactly `Echo`).
 |===
 
-`EchoOrdinal` is Tier-1 off `Echo` but additionally pulls the
-`Ordinal/` subtree; it belongs to the Buchholz/Veblen Direction in
-the MAP, not the foundation kernel.
+`EchoOrdinal` is Tier-1 off `Echo` but additionally pulls two
+`Ordinal/` leaves (`Ordinal.OmegaMarkers`, `Ordinal.Buchholz.Syntax`);
+it is the echo-to-ordinal bridge, not the foundation kernel. The rest
+of the ordinal lane moved to `hyperpolymath/ordinal-notation` on
+2026-10-20.
 
 == Maintenance
 
diff --git a/docs/echo-types/paper.adoc b/docs/echo-types/paper.adoc
index a93884d..0a03fa5 100644
--- a/docs/echo-types/paper.adoc
+++ b/docs/echo-types/paper.adoc
@@ -1395,6 +1395,11 @@ instance. External validation is the remaining step.
 [#ordinal-appendix]
 == Ordinal / Buchholz consumer-evidence
 
+NOTE: Since 2026-10-20 the modules this appendix cites live in
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation], not in echo-types (echo-types#349). Only the `EchoOrdinal` bridge stays
+here. The appendix text is unchanged; module names are the same in both
+repositories.
+
 *Status: written at the well-foundedness milestone; order-type
 fidelity OPEN (decision-log `D-2026-06-14`,
 `docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc`).*
diff --git a/docs/echo-types/what-echo-is.adoc b/docs/echo-types/what-echo-is.adoc
index 49eb51c..19815dd 100644
--- a/docs/echo-types/what-echo-is.adoc
+++ b/docs/echo-types/what-echo-is.adoc
@@ -168,7 +168,9 @@ negatively, EI-2.)
   `echo-additive/` modules are absent from `All.agda`). Treat the variance result
   as a real-but-unwired artefact, exactly as `AFFIRMATION.adoc` records it.
 * *Bachmann–Howard order-type fidelity is POSTULATED*, in
-  `Ordinal/Buchholz/Fidelity.agda`, *outside* the `--safe` kernel cone. The
+  `Ordinal/Buchholz/Fidelity.agda`, *outside* the `--safe` kernel cone. (Since
+  2026-10-20 that file and the whole ordinal tower live in
+  https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation], not here.) The
   ordinal-notation tower's sound-carrier well-foundedness is proved and in the
   closure; the bridge from that notation to the Bachmann–Howard ordinal is an
   explicit, auditable trust boundary, not a closed theorem. "Mechanized
diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc
index 1b01971..f136d1d 100644
--- a/docs/proof-debt.adoc
+++ b/docs/proof-debt.adoc
@@ -19,7 +19,11 @@ closing by the cubical endpoint rule), then re-proves
 `+prop-factor-left-mere-surjective+` (epi). This realises the axiom the
 `+--without-K+` demo under (c) only assumes — see (c).
 * *Bachmann–Howard target structure (`+BHNotation+` + its
-well-foundedness)* — discharged 2026-06-15 in the `+--safe --without-K+`
+well-foundedness)* — *moved out of this repository* (2026-10-20,
+echo-types#349) to
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation],
+where it is still discharged. The record below is historical; the paths
+it names no longer exist here. Originally discharged 2026-06-15 in the `+--safe --without-K+`
 kernel by `+proofs/agda/Ordinal/Buchholz/BHTarget.agda+` (zero
 postulates; wired into `+All.agda+`, pinned in
 `+Ordinal/Buchholz/Smoke.agda+`). The abstract `+BHNotation+` interface
@@ -65,46 +69,17 @@ because `+∥_∥+` cannot be built WITHIN `+--safe --without-K+` itself.
 
 === (d) DEBT — actively to be closed
 
-* `+proofs/agda/Ordinal/Buchholz/Fidelity.agda+` — *two* top-level
-`+postulate+`s (reduced from three on 2026-06-15; see (a)) forming the
-trust boundary of the *order-type fidelity scaffold* (open problem
-`+D-2026-06-14+`,
-`+docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc+`):
-** `+denotation+` — assumed faithful, height-preserving order-embedding
-`+⟦·⟧ : BT → 𝒪+` into the (now-real) Brouwer target (the missing object;
-*not* `+rank2+`, which deliberately collapses heights and is a
-termination measure only).
-** `+ordinal-upper-bound+` — the `+⟦·⟧+`-level upper half of the
-sandwich (downstream of `+denotation+`).
-** *Discharged (2026-06-15)*: the former `+bh-notation+` postulate (an
-opaque whole BH structure) is gone — the `+BHNotation+` interface and a
-real `+bh-notation-from+` instance now live in the `+--safe+` kernel
-module `+Ordinal.Buchholz.BHTarget+`, so the target order and its
-well-foundedness (Brouwer `+_<′_+` / `+wf-<′+`) are proved, not assumed.
-The candidate BH height is an explicit parameter to
-`+Fidelity.AtHeight+`, not a postulate. See (a).
-** *Classification*: DEBT, to be discharged when order-type fidelity is
-proved — these are _not_ permanently-accepted axioms. Each is annotated
-inline with an `+AXIOM:+` leading comment.
-** *Justification / scope*: the module is quarantined — `+--without-K+`
-only, NOT imported by `+All.agda+` / `+Smoke.agda+` — so the `+--safe+`
-kernel cone depends on neither postulate. Nothing in the module asserts
-that order type ψ₀(Ω_ω) is _proven_; the status surfaces (appendix,
-decision log, roadmap) read "`written at WF milestone; order-type
-fidelity OPEN`".
-** *Citation*: `+D-2026-06-14+`; full per-postulate spec (statement /
-what closes it / owner) in `+Fidelity-OPEN-postulates.md+`.
-** *PARKED (2026-06-20, `+D-2026-06-20+`)*: the transfinite ladder these
-postulates sit atop is now _consumer-less_ — the Groove cleave (the only
-consumer of ψ₀(Ω_ω) order-type fidelity) is resolved as a finite
-exact-round-trip zipper needing well-foundedness only, and RC-11 forbids
-ε₀+ in cleave ranks. The debt is therefore _parked, resumable_, not
-actively being closed. No postulate closed; `+D-2026-06-14+` stands. See
-`+docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc+`.
-** *Guardrail status*: allow-listed in `+tools/check-guardrails.sh+`
-(`+EXPLORATORY_EXEMPT+`) and the inline `+hypatia: allow+` pragma at the
-module head. (`+BHTarget+` is NOT exempt — it is real kernel content and
-passes the guardrail.)
+* (none in this repository)
+
+*Moved (2026-10-20, echo-types#349).* The order-type fidelity scaffold
+`+Ordinal/Buchholz/Fidelity.agda+` and its two postulates
+(`+denotation+`, `+ordinal-upper-bound+`) left echo-types with the rest of
+the ordinal lane (`+D-2026-06-21+`). They now live in
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation],
+quarantined in its proof MANIFEST and tracked in its
+`+Fidelity-OPEN-postulates.adoc+`. Order-type fidelity to ψ₀(Ω_ω)
+remains OPEN there (`+D-2026-06-14+` stands). echo-types now carries
+exactly *one* quarantined postulate block, under (c).
 
 === Notes
 
@@ -131,6 +106,8 @@ often-cited "`676 files / 52k lines`" headline is inflated by
 `+.claude/worktrees/+` duplicate snapshots; real source ≈ 190 `+.agda+`
 files / ~36k lines.
 * *The quarantined postulates are correctly _outside_ the wired cone.*
+(Audit-time state. Since 2026-10-20 the `+Fidelity.agda+` file is no
+longer in this repository; see (d).)
 The audit independently confirms the two postulate-bearing files this
 ledger already lists — `+EchoImageFactorizationPropPostulated.agda+` (c)
 and `+Ordinal/Buchholz/Fidelity.agda+` (d) — are guardrail-exempt,
diff --git a/docs/proof-obligations.adoc b/docs/proof-obligations.adoc
index fb33f81..b0fba5f 100644
--- a/docs/proof-obligations.adoc
+++ b/docs/proof-obligations.adoc
@@ -26,5 +26,5 @@ natively constructible. See `+docs/retracted/retractions.adoc+`)
 * *CNO Bridge (Absolute Zero):* PARTIAL
 * *JanusKey Integration:* PARTIAL
 * *Tropical Semantics (Argmin residues):* PARTIAL
-* *Buchholz/Veblen Ordinal Representation:* BLOCKED (Well-foundedness of
-shared-binder cases blocked on self-lift)
+* *Buchholz/Veblen Ordinal Representation:* MOVED (2026-10-20) to
+`hyperpolymath/ordinal-notation`; its obligations are tracked there
diff --git a/roadmap.adoc b/roadmap.adoc
index 4a3f14f..6d08339 100644
--- a/roadmap.adoc
+++ b/roadmap.adoc
@@ -158,8 +158,9 @@ DOI mint, library packaging, outreach — which is author-driven
   notation primer) cleared 2026-05-20 via PR #73; tag 3 (evaluation —
   proof-size / cost table, common-upper-bound idiom) cleared in
   PR #84 (§"Evaluation and discussion"). Tag 4 (ordinal
-  consumer-evidence appendix) is gated on the Lane 3 Buchholz
-  milestone and is not load-bearing for Lane 1 — see paper status
+  consumer-evidence appendix) is gated on the Buchholz milestone,
+  which now belongs to hyperpolymath/ordinal-notation, and is not
+  load-bearing for Lane 1 — see paper status
   banner.
 . *LANDED 2026-05-26.* `proofs/agda/EchoAbstractionBarrier.agda`
   ships the consumer-side free theorem at the affine instance
@@ -305,7 +306,16 @@ narrowed — no unique-mediator claim. Demand 4 ("parametricity") must
 be *consumer-side at the affine instance*, not full Reynolds. See
 respective §s in the synthesis doc.
 
-=== Lane 3 [RETIRED FROM ECHO-TYPES 2026-06-21 — outgrew the project] — Ordinal / Buchholz
+=== Lane 3 [MOVED 2026-10-20 to hyperpolymath/ordinal-notation] — Ordinal / Buchholz
+
+*MOVED (2026-10-20, echo-types#349).* The extraction decided in
+`D-2026-06-21` is done. The ordinal lane, its design documents and its two
+open `Fidelity.agda` postulates now live in
+https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation].
+echo-types keeps only the `EchoOrdinal` bridge and its two imports
+(`Ordinal.OmegaMarkers`, `Ordinal.Buchholz.Syntax`). The rest of this
+section is the record as of the retirement; module paths it names are no
+longer in this repository.
 
 *RETIRED FROM ECHO-TYPES (`D-2026-06-21`, escalating the `D-2026-06-20`
 PARK).* The transfinite ordinal-fidelity ladder has *outgrown the
diff --git a/wiki/Architecture.adoc b/wiki/Architecture.adoc
index 00df191..2eac303 100644
--- a/wiki/Architecture.adoc
+++ b/wiki/Architecture.adoc
@@ -55,7 +55,11 @@ The Σ-algebra of echoes under function composition.
 
 Docs: `docs/echo-types/{composition,fibration-package,universal-property}.adoc`.
 
-== Track 2 — Ordinal (RETIRED from echo-types, owner decision D-2026-06-21)
+== Track 2 — Ordinal (MOVED to ordinal-notation, 2026-10-20)
+
+*Moved.* Since 2026-10-20 (echo-types#349) the lane lives in https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation]. What
+follows is the record at the retirement; only the `EchoOrdinal` bridge and its
+two imports remain under `proofs/agda/`.
 
 A Buchholz collapsing layer; the consumer-evidence that echo's
 non-injectivity bridges to ordinal-collapsing non-injectivity.
diff --git a/wiki/Home.adoc b/wiki/Home.adoc
index fc7a8a0..5099baa 100644
--- a/wiki/Home.adoc
+++ b/wiki/Home.adoc
@@ -131,10 +131,10 @@ This wiki is a *distillation*. The authoritative records are:
   (`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).
+* *Ordinal track* — *MOVED* to https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation] on 2026-10-20 (echo-types#349),
+  carrying out owner decision `D-2026-06-21`: the transfinite Buchholz/Veblen
+  ladder outgrew the project. Only the `EchoOrdinal` bridge and its two
+  imports stay here.
   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.
diff --git a/wiki/Roadmap.adoc b/wiki/Roadmap.adoc
index 7df31cc..4644183 100644
--- a/wiki/Roadmap.adoc
+++ b/wiki/Roadmap.adoc
@@ -56,7 +56,10 @@ landed and packaged as `_↔_`. No open headline items; further work is
 consolidation / doc-threading.
 
 [#ordinal]
-=== Ordinal track — RETIRED from echo-types (owner decision D-2026-06-21)
+=== Ordinal track — MOVED to ordinal-notation (2026-10-20)
+
+*Moved.* The extraction decided in `D-2026-06-21` is done: the lane now lives
+in https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation] (echo-types#349). What follows is the record at the retirement.
 
 The transfinite Buchholz/Veblen ascent *outgrew echo-types* and is *no longer
 echo-types work*. The landed artifact is correct (`--safe --without-K`, zero

From 2d6afddc6e9e458f73a22ad95298ec3774674d3d Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 26 Oct 2026 18:05:54 +0000
Subject: [PATCH 2/2] docs: date the wiki status block; mark the frozen plan's
 pointers as at-extraction

Two inconsistencies introduced by the previous commit, found in review:

- wiki/Home.adoc: the status block was still dated 2026-06-21 but now
  records the 2026-10-20 move. Re-date it, and point the establishment
  bullet's open fidelity problem at ordinal-notation.
- docs/bridges/buchholz-plan.adoc is a frozen copy, so its "Live"
  pointers are now wrong. Relabel them as the state at extraction.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
---
 docs/bridges/buchholz-plan.adoc | 4 ++--
 wiki/Home.adoc                  | 8 ++++----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/docs/bridges/buchholz-plan.adoc b/docs/bridges/buchholz-plan.adoc
index 496423a..28914d1 100644
--- a/docs/bridges/buchholz-plan.adoc
+++ b/docs/bridges/buchholz-plan.adoc
@@ -24,8 +24,8 @@ were ahead of us.  The "PLANNED" tags below are dated; many phases have
 since landed under different module names (E1–E7 closed; the WfCNF
 restriction +  `RankPow` / `RankAdm` / `RankLex` slices replace the
 generic `Phase 2.2 rank-mono`; the WF-0/WF-1 well-foundedness is in
-`Ordinal.Buchholz.WellFounded`).  *Live per-constructor verdict*:
-`docs/echo-types/buchholz-rank-obstruction.adoc`.  *Live lane status*:
+`Ordinal.Buchholz.WellFounded`).  *Per-constructor verdict at extraction*:
+`docs/echo-types/buchholz-rank-obstruction.adoc`.  *Lane status at extraction*:
 `roadmap.adoc` § Lane 3.  *Per-session ledger*: `CLAUDE.md` § "Current
 rung state".  This file is retained for provenance and design context;
 treat its concrete "PLANNED" items as superseded.
diff --git a/wiki/Home.adoc b/wiki/Home.adoc
index 5099baa..6fecb50 100644
--- a/wiki/Home.adoc
+++ b/wiki/Home.adoc
@@ -115,14 +115,14 @@ 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-21)
+== One-line status (as of 2026-10-26)
 
 * *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`).
+  Pillar E is complete at the bounded-claim level. The one named *OPEN
+  external* problem, *order-type fidelity* to ψ₀(Ω_ω) (decision-log
+  `D-2026-06-14`), moved with the ordinal lane to ordinal-notation (below).
 * *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