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
19 changes: 11 additions & 8 deletions CLAUDE.md
Original file line number Diff line number Diff line change
Expand Up @@ -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`.)
Expand Down
34 changes: 25 additions & 9 deletions wiki/Architecture.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
Loading