Context

Owner decision D-2026-06-21 RETIRED the transfinite ordinal / Buchholz / Veblen ascent from echo-types (escalating the 2026-06-20 PARK). The ladder outgrew echo-types. The landed artifact is correct (--safe --without-K, zero postulates, in the green closure) and stays compiling; no new ordinal rung is opened here.

This issue tracks the disposition: extraction to a dedicated ordinal-notation repository. The physical cross-repo cut is the owner's — creating the new repo and moving history is outside agent scope (and the new repo is outside the current agent MCP repo-scope).

Hand-off record (authoritative)

docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc — the frontier + inventory for the extracted repo. This is a hand-off record, NOT a resume-here plan.

Firewall (verified clean)

• STAY (Echo Core's bridge): OmegaMarkers ← Buchholz.Syntax ← EchoOrdinal.
• MOVE: everything else under proofs/agda/Ordinal/ (Brouwer/*, Buchholz/* beyond Syntax, Veblen*, RecursiveSurface*, the rank/rank2 ladders, Fidelity.agda, BHTarget.agda, …).

Frozen open items (for the extracted repo only — NOT echo-types TODOs)

1. Unbudgeted _<ᵇʳᶠ_ global WF over native _<ᵇ_ (all five standard routes walled; realistic close-out is a falsifiable "cannot close under --safe --without-K" verdict).
2. Full K-limited shared-binder constructor set (<ᵇ-ψα, <ᵇ-+2).
3. Order-type fidelity to ψ₀(Ω_ω) (D-2026-06-14) — an OPEN external problem. Retirement neither closes nor over-claims it.

Acceptance

• New ordinal-notation repo exists (owner).
• Moved modules compile there under --safe --without-K, zero postulates.
• echo-types retains only the STAY firewall set + a one-line pointer; All.agda / Smoke.agda updated; kernel-guard.sh PASS.

Housekeeping (owner / GitHub-UI only — agent cannot delete remote branches, returns HTTP 403)

• Delete stale branch session/slice-4-narrowing (zero unique commits; git-ancestor of estate-standardization-20260607).