diff --git a/CLAUDE.md b/CLAUDE.md index 429fd8d..3bcff8f 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -72,7 +72,19 @@ 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 (buchholz-plan.adoc) — ABANDONED (`D-2026-06-21`).** + *Do not resume this track.* It was PARKED (`D-2026-06-20`) and is now + ABANDONED: ended work, not resumable barring **new grammar or a major + redesign** (and a returning consumer — there is none). It ended at + Veblen rung 6 — `Γ₀` defined + `Γ₀-prefixed : Γ₀ ≤′ φ Γ₀ oz` (one + direction); the Γ₀-least wall (mutual fixed-point descent) was never + opened and even closing it reaches only Feferman–Schütte, galaxies + below the ψ₀(Ω_ω) milestone. The ladder stays in-tree (correct, `--safe`, + zero-postulate, `Fidelity` outside the kernel cone); the `--safe` core + depends on none of it. Record: + `docs/echo-types/decisions/ordinal-fidelity-ladder-abandoned.adoc`. + The historical summary below is retained for reference only. + 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 diff --git a/docs/echo-types/decisions/ordinal-fidelity-ladder-abandoned.adoc b/docs/echo-types/decisions/ordinal-fidelity-ladder-abandoned.adoc new file mode 100644 index 0000000..693c218 --- /dev/null +++ b/docs/echo-types/decisions/ordinal-fidelity-ladder-abandoned.adoc @@ -0,0 +1,109 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += D-2026-06-21 — Ordinal-fidelity ladder ABANDONED (supersedes the D-2026-06-20 park) +:toc: macro +:toclevels: 2 +:sectnums: +:sectnumlevels: 2 +:icons: font + +[.lead] +Upgrades the `D-2026-06-20` *park* of the transfinite ordinal-fidelity ladder +to an *abandonment*. The park was framed as "frozen at a clean rung, fully +resumable". This entry records the owner decision (2026-06-21) that the track +is *ended work*: it is not worth resuming under the current grammar/design. +The only conditions under which it would be revisited are *new grammar or a +major redesign* — and even then, only if a consumer for ψ₀(Ω_ω) order-type +fidelity returns (none exists; see `D-2026-06-20` §Reason). + +Nothing about the honest record changes: order-type fidelity was always +flagged OPEN (`D-2026-06-14` stands), no postulate was closed, and the +`--safe --without-K` core depends on none of the ladder. + +toc::[] + +== Status + +*Ordinal-fidelity ladder: ABANDONED.* No further rung is to be opened — now or +on a consumer's return — without first a new grammar or a major redesign. The +"resumable / cold-resume here" framing of `D-2026-06-20` is *withdrawn*: not +because the frontier moved, but because the approach itself is judged a dead +end for the milestone. + +== Where it finally got to (the terminal endpoint) + +The Brouwer-side Veblen climb ended at *rung 6* (`#247`, commit `b6d0d18`). + +Landed, `--safe --without-K`, zero postulates, no `TERMINATING`: + +* `ω^^` (ω to an ordinal power) + ε₀ (`ε₀-ε-number`, `ω^^-infl`); +* φ₁ as the ε-number enumeration and a normal function (`next-ε-least`, + `φ₁-mono` / `φ₁-strict-mono` / `φ₁-continuous`); +* the binary Veblen `φ : Ord → Ord → Ord` with the generic fixed-point engine + (`deriv` / `nextFix` / `commonStep`; `nextFix-fixed-{≤,≥}`); +* *every* level a normal function (`φ-mono₂`, `φ-infl`, the Veblen recurrence + `φ-level-fixed-{≤,≥}`); +* first-argument monotonicity in the *adjacent* and *below-a-limit* cases + (`φ-mono₁-step`, `φ-mono₁-into-lim`); +* the diagonal `Γ₀` (Feferman–Schütte) defined; and +* *`Γ₀-prefixed : Γ₀ ≤′ φ Γ₀ oz`* — *one* direction of the diagonal fixed point. + +The wall, *not opened and not to be opened*: the reverse `φ_Γ₀(0) ≤′ Γ₀` +(Γ₀-least), gated on the Veblen *mutual fixed-point descent* lemma (first-arg +monotonicity ⟷ "a fixed point of `φ_β` is a fixed point of `φ_α` for `α ≤′ β`", +mutually recursive over the level). + +Even closing that wall reaches only *Γ₀* — unboundedly below the *ψ₀(Ω_ω)* +milestone. Downstream, OPEN and now abandoned with the rest: the *ψ collapsing +function* (with fundamental sequences, producing `bh-height`), and the two +`Ordinal.Buchholz.Fidelity` postulates `denotation` / `ordinal-upper-bound` +(gated on the collapse). `Fidelity` is outside the `--safe` kernel cone and is +imported by neither `All.agda` nor `Smoke.agda`. + +*Final position in one line:* a correct, zero-postulate Veblen ladder that +reaches a *pre-fixed point of Γ₀* and stops one mutual induction short of +Γ₀-least — itself galaxies short of the milestone. + +== Why abandon, not merely park + +The `D-2026-06-20` reasons stand and harden: + +. *Consumer-less.* The Groove cleave — the only consumer that ever wanted + ψ₀(Ω_ω) order-type fidelity — resolved to a finite exact-round-trip zipper + needing well-foundedness only; Groove RC-11 forbids ε₀+ in cleave ranks, and + the ladder is past ε₀ from rung 2. The target is outside the (former) + consumer's permitted range by construction. +. *The hard lemma does not reach the thing.* Every remaining rung — the + mutual-descent lemma included — is structure on the *near side* of the open + `denotation` map. A clean Γ₀-least reaches Feferman–Schütte, not the + milestone; the intricate mutual induction buys an ordinal galaxies too small. +. *Dead end under the current design.* Closing the distance to ψ₀(Ω_ω) is not + more rungs of the same kind — it needs the ordinal-collapsing layer (ψ with + fundamental sequences), a different construction. Absent a consumer, that + multi-session core is not worth building. Hence only *new grammar or major + redesign* (and a returning consumer) would reopen it. + +== Disposition (the artifact stays; extraction remains the owner's optional cut) + +The ladder is correct and harmless in-tree: `--safe --without-K`, zero +postulates, no `TERMINATING`, kernel-guard PASS, and `Fidelity` (the only +postulate-bearing module) sits outside the kernel cone, imported by neither +`All.agda` nor `Smoke.agda`. + +*Abandoned ≠ deleted.* This entry does not remove or extract anything. The +`D-2026-06-20` firewall remains the clean cut-line *if* the owner later chooses +to extract the consumer-less subtree to its own ordinal-notation repository: +the bridge trio `Ordinal.OmegaMarkers` ← `Ordinal.Buchholz.Syntax` ← +`EchoOrdinal` *STAYS*; everything else under `proofs/agda/Ordinal/` *MOVES*. +That cut is a cross-repo operation left, as before, to the owner — now with no +expectation that the ladder will be resumed in echo-types. + +== See also + +* `docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc` — + `D-2026-06-20`, the park this supersedes (full artifact inventory + the + verified firewall). +* `docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc` — + `D-2026-06-14`, the parent open-problem record (stands, unchanged). +* `Fidelity-OPEN-postulates.md` — the two open `Fidelity.agda` postulates. +* `roadmap.adoc` §Lane 3 — the ordinal-track items (now abandoned). diff --git a/docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc b/docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc index f6500fa..5e03a29 100644 --- a/docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc +++ b/docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc @@ -7,6 +7,17 @@ :sectnumlevels: 2 :icons: font +[IMPORTANT] +==== +*SUPERSEDED (2026-06-21).* This park was upgraded to an *abandonment* — +the track is ended work, not resumable, barring new grammar or a major +redesign. See +`docs/echo-types/decisions/ordinal-fidelity-ladder-abandoned.adoc` +(`D-2026-06-21`). The terminal endpoint, artifact inventory, and firewall +recorded below remain accurate; only the "frozen, fully resumable" framing +is withdrawn. +==== + [.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/roadmap.adoc b/roadmap.adoc index 3d222bf..5bb2464 100644 --- a/roadmap.adoc +++ b/roadmap.adoc @@ -305,20 +305,24 @@ 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 -→ 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 -`docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc`. +=== Lane 3 [ABANDONED 2026-06-21, NOT LOAD-BEARING] — Ordinal / Buchholz + +*ABANDONED (`D-2026-06-21`, supersedes the `D-2026-06-20` park).* The +transfinite ordinal-fidelity ladder is *ended work* — not resumable barring +new grammar or a major redesign (and a returning consumer; there is none). +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)`) ended at a clean rung; the +next rung (Veblen mutual fixed-point descent → Γ₀-least) was never opened, and +even closing it reaches only Feferman–Schütte (Γ₀), galaxies below the +milestone. No postulate closed; order-type fidelity REMAINS OPEN +(`D-2026-06-14` stands). The ladder STAYS in-tree (correct, `--safe`, +zero-postulate); extraction to its own ordinal-notation repo remains the +owner's optional cut. See +`docs/echo-types/decisions/ordinal-fidelity-ladder-abandoned.adoc` +(and the superseded `…-parked.adoc`). *Echo Core does NOT depend on this lane.* This is a separate proof-theoretic research project that happens to share the