diff --git a/CLAUDE.md b/CLAUDE.md index 2f4dec4..c506799 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -257,20 +257,23 @@ island) + the two `Ordinal/Buchholz/Fidelity.agda` postulates (d, `denotation` / `ordinal-upper-bound`). See `proof-debt.md` (a)–(d). Echo Core is postulate-free and hole-free. -**⚠ OWNER-DECISION FLAG — ordinal: retired-in-ledger but committing-on-main.** +**✅ OWNER-DECISION RECONCILED (2026-06-21) — ordinal artifact VALID + KEPT; trajectory CLOSED.** `main` (this arc's base, `9c56d40`) carries TWO ordinal climb rungs dated **2026-06-21**, landed the SAME DAY as the `D-2026-06-21` retirement: `f89a3aa` (BH rung 7 — `nextFix` is the LEAST pre-fixed point; reverse-Γ₀ reduced) and `a096764` (BH rung 8 — Veblen engine monotone in its iterated function). This **contradicts** the retirement banner in this file (arc below) and in `roadmap.adoc` §Lane 3 ("no new ordinal rung is to be opened here"). -Meanwhile `wiki/Architecture.adoc` ("Track 2 — Ordinal (partial)") and -`wiki/Roadmap.adoc` ("Ordinal track — partial (the active bottleneck)") still -frame the climb as ACTIVE — i.e. they are consistent with the *code* but not -the *decision*. **Do NOT propagate the retirement to the wiki, and do NOT -delete the ordinal artifact, until the owner reconciles** which is -authoritative: the retirement decision, or the continued climb. Both readings -are live; the fix direction depends entirely on that call. (Also landed on +At flag time `wiki/Architecture.adoc` ("Track 2 — Ordinal (partial)") and +`wiki/Roadmap.adoc` ("the active bottleneck") still framed the climb as ACTIVE +— consistent with the *code* but not the *decision*. **RECONCILED by the owner +(2026-06-21): "treat it as valid itself, but no further work on that trajectory +is needed."** So the landed artifact (incl. rungs 7–8) is VALID and KEPT — +*frozen, not deleted*; the retirement stands as to **direction** — no further +climb, no new ordinal rung in echo-types; disposition = extraction to its own +ordinal-notation repo. The wiki is now ALIGNED (`wiki/Roadmap.adoc` retired via +`e09eba5`; `wiki/Architecture.adoc` Track 2 reframed to "RETIRED … valid + +frozen" this arc). Do NOT reopen this as a live contradiction. (Also landed on `main` same day, non-ordinal: `4883ae2` `EchoTransaction` closes #174; `bd43ad4` `EchoSelectiveProjection` closes #176; `9c56d40` `entropy-blind-parametric`.) diff --git a/wiki/Architecture.adoc b/wiki/Architecture.adoc index 0ce92c8..00df191 100644 --- a/wiki/Architecture.adoc +++ b/wiki/Architecture.adoc @@ -55,27 +55,43 @@ The Σ-algebra of echoes under function composition. Docs: `docs/echo-types/{composition,fibration-package,universal-property}.adoc`. -== Track 2 — Ordinal (partial) +== Track 2 — Ordinal (RETIRED from echo-types, owner decision D-2026-06-21) A Buchholz collapsing layer; the consumer-evidence that echo's non-injectivity bridges to ordinal-collapsing non-injectivity. -* Target: *Bachmann–Howard* ψ₀(Ω_ω) as the first credible milestone; stretch - ψ(Ω_Ω) ≈ TFBO. +*Status (reconciled 2026-06-21): the landed artifact is valid and kept — +no further work on this trajectory.* It compiles `--safe --without-K` with +zero postulates and stays in the green closure; the climb is *not continued* +and *no new ordinal rung is to be opened here*. The disposition is extraction +to its own ordinal-notation repository. Echo Core never depended on this track: +the `OmegaMarkers` ← `Buchholz.Syntax` ← `EchoOrdinal` bridge STAYS; everything +else under `proofs/agda/Ordinal/` is the consumer-less artifact that MOVES. +Order-type fidelity to ψ₀(Ω_ω) remains an *open external problem* +(`D-2026-06-14`) — retirement neither closes nor over-claims it. + +The inventory below is the *frozen hand-off record* for the extracted repo, +**not** an echo-types TODO list: + +* Former target: *Bachmann–Howard* ψ₀(Ω_ω) as the first credible milestone; + stretch ψ(Ω_Ω) ≈ TFBO. * E1–E7 landed: OT syntax, ℕ-staged closure, CNF, pedagogical ψ, Buchholz scaffold, well-formedness, echo bridge (`ordinal-collapse-non-injective`). * Rank-monotonicity under the *WfCNF* restriction with a limit-shaped ω-power rank: `RankPow` / `RankPowDomination` / `HeadOmega` / `HeadOmegaInversion`. * Slice 3+4 Route A arc (PRs #165–#170): the `RankMonoUnion` umbrella over source-rule extensions, and well-foundedness of `_<ᵇᵘ_` via rank-embedding - transport (#170). + transport (#170); later the Veblen climb reached rungs 7–8 (the artifact's + current front, kept as-is). -*Open:* the unbudgeted `_<ᵇʳᶠ_` global WF (eliminate the ℕ budget without -leaving `--safe --without-K`); the K-limited shared-binder cases (`<ᵇ-ψα`, -`<ᵇ-+2`); push the surface-route WF back into `Order.agda`'s main `_<ᵇ_`. This -track is *solo, not swarmable*. +*Frozen (for the extracted repo, NOT echo-types work):* the unbudgeted +`_<ᵇʳᶠ_` global WF (eliminate the ℕ budget without leaving `--safe +--without-K`); the K-limited shared-binder cases (`<ᵇ-ψα`, `<ᵇ-+2`); pushing +the surface-route WF back into `Order.agda`'s main `_<ᵇ_`. -Docs: `docs/echo-types/buchholz-plan.adoc`, `buchholz-rank-obstruction.adoc`. +Docs: `docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc` +(D-2026-06-21 superseding banner), `docs/echo-types/buchholz-plan.adoc`, +`buchholz-rank-obstruction.adoc`. == Track 3 — Establishment (Pillars A–D + F closed; E open)