docs: point the ordinal lane at hyperpolymath/ordinal-notation

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:

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)
 

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

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+`).

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).

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
 |===
 

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

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

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._<ᵇ_+`:
 

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
@@ -14,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.

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