Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 33 additions & 3 deletions CLAUDE.md
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,12 @@ Two active workstreams:
the equivalence-record packaging `Echo-comp-pent-Σ-assoc :
... ↔ ...` (stdlib `Function.Bundles._↔_`) is in place.

2. **Ordinal track (buchholz-plan.adoc).** Target remains Bachmann–
2. **Ordinal track — 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
2026-06-21 ledger arc above). The summary below is the **frozen hand-off
record**, not an active TODO list. *Former* target was Bachmann–
Howard (ψ₀(Ω_ω)) as first credible milestone, stretch to ψ(Ω_Ω)
≈ TFBO. E1–E7 landed (OT syntax, ℕ-staged closure with
`C-monotone`, CNF with `cnf-trichotomy`, pedagogical ψ with
Expand All @@ -89,7 +94,7 @@ Two active workstreams:
alongside BT); the unbudgeted global WF theorem for `_<ᵇʳᶠ_`
remains open.

Open pieces on this track:
Frozen at retirement (for the extracted repo only — NOT echo-types TODOs):
* Full constructor set beyond the admitted core (K-limited
shared-binder cases such as `<ᵇ-ψα`, `<ᵇ-+2`).
* Unbudgeted `_<ᵇʳᶠ_` global WF — eliminate the explicit ℕ
Expand Down Expand Up @@ -210,7 +215,32 @@ 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-20)
## Current rung state (2026-06-21)

### Session arc 2026-06-21 — Ordinal ascent RETIRED FROM ECHO-TYPES (escalates the 2026-06-20 PARK) (read this first)

*Owner decision (D-2026-06-21).* The transfinite ordinal / Buchholz / Veblen
ascent is **no longer echo-types work** — it has **outgrown the project**. This
*escalates* the 2026-06-20 PARK (next arc) from "parked, resumable here" to
**RETIRED from this repo**: we are **not continuing the climb past its current
front**, and **no new ordinal rung is to be opened in echo-types**. The landed
artifact stays and is correct (it compiles `--safe --without-K`, zero
postulates, in the green closure); the *disposition* — extraction to its own
ordinal-notation repository — is now the **decided** path, not a flag (the
physical cross-repo cut remains the owner's). The detailed inventory + frontier
in `docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc` (now headed
by a D-2026-06-21 superseding banner) are the **hand-off record for that
separate repo**, NOT a resume-here plan.

*For subsequent agents and humans — unambiguous:* do **not** open Veblen /
Buchholz / ordinal-collapse rungs in echo-types; do **not** treat the "open
pieces" / "next rungs" language elsewhere in this file or in `roadmap.adoc`
§Lane 3 as echo-types TODOs — they are retired. Order-type fidelity to ψ₀(Ω_ω)
remains an OPEN external problem (`D-2026-06-14` stands) — retirement neither
closes nor over-claims it; the work simply lives elsewhere now. Echo Core never
depended on this lane (the `OmegaMarkers` / `Buchholz.Syntax` / `EchoOrdinal`
bridge stays; everything else under `Ordinal/` is the consumer-less artifact
that moves).

### Session arc 2026-06-20 — variance resolution + Veblen climb rungs 3–6 + ordinal-fidelity ladder PARKED (read this first)

Expand Down
16 changes: 16 additions & 0 deletions docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,22 @@ flagged OPEN (`D-2026-06-14` stands, unchanged). The ladder is correct,
well-built, `--safe --without-K`, zero-postulate — and, as of this date,
*unconsumed*. It is frozen at a clean rung and is fully resumable.

[IMPORTANT]
====
*SUPERSEDED — D-2026-06-21: escalated from PARK to RETIRED (owner decision).*
The ordinal / Veblen ascent has *outgrown the echo-types project* and is *no
longer echo-types work*. We are *not continuing the climb past its current
front*, and *no new ordinal rung is to be opened in echo-types* — so "fully
resumable" above now means *resumable only as the separate ordinal-notation
repository*, never here. The §"Disposition / re-home" extraction below is
therefore the *decided* disposition, not a flag (the physical cut remains the
owner's cross-repo operation). Nothing is over- or under-claimed: the artifact
is correct and stays in the green closure; order-type fidelity remains OPEN
(`D-2026-06-14` stands). Subsequent agents and humans: treat the inventory +
frontier below as the *hand-off record for the extracted repo*, not a
resume-here plan.
====

toc::[]

== Status
Expand Down
22 changes: 13 additions & 9 deletions roadmap.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -305,19 +305,23 @@ 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 [PARKED 2026-06-20, NOT LOAD-BEARING] — Ordinal / Buchholz

*PARKED (`D-2026-06-20`).* The transfinite ordinal-fidelity ladder is
*parked, resumable* — the only consumer of ψ₀(Ω_ω) order-type fidelity
(the Groove cleave) is resolved as a finite exact-round-trip zipper
needing well-foundedness only (RC-11 forbids ε₀+ in cleave ranks), so the
ladder is consumer-less. The Veblen climb (rungs 1–6: `ω^^`/ε₀ → φ₁ normal
=== Lane 3 [RETIRED FROM ECHO-TYPES 2026-06-21 — outgrew the project] — Ordinal / Buchholz

*RETIRED FROM ECHO-TYPES (`D-2026-06-21`, escalating the `D-2026-06-20`
PARK).* The transfinite ordinal-fidelity ladder has *outgrown the
echo-types project* and is *no longer echo-types work* — not "parked,
resumable here" but *retired from this repo*: no new rung is to be opened
here, and the disposition is extraction to its own ordinal-notation repo.
The trigger was already true at the PARK: the only consumer of ψ₀(Ω_ω)
order-type fidelity (the Groove cleave) is resolved as a finite
exact-round-trip zipper needing well-foundedness only (RC-11 forbids ε₀+ in
cleave ranks), so the ladder is consumer-less. The Veblen climb (rungs 1–6: `ω^^`/ε₀ → φ₁ normal
→ binary φ + Γ₀ → every level normal → first-arg monotonicity +
`Γ₀ ≤′ φ_Γ₀(0)`) is frozen at a clean rung; the next rung (Veblen mutual
fixed-point descent → Γ₀-least) is deliberately NOT opened. No postulate
closed; order-type fidelity REMAINS OPEN (`D-2026-06-14` stands). The
disposition is extraction to its own ordinal-notation repo (cut FLAGGED,
left to the owner). See
disposition is extraction to its own ordinal-notation repo (the decided
path as of `D-2026-06-21`; the physical cross-repo cut remains the owner's). See
`docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc`.

*Echo Core does NOT depend on this lane.* This is a separate
Expand Down
Loading