|
| 1 | +// SPDX-License-Identifier: CC-BY-SA-4.0 |
| 2 | +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | += D-2026-06-14 — Bachmann–Howard order-type fidelity (named open problem) |
| 4 | +:toc: macro |
| 5 | +:toclevels: 2 |
| 6 | +:sectnums: |
| 7 | +:sectnumlevels: 2 |
| 8 | +:icons: font |
| 9 | + |
| 10 | +[.lead] |
| 11 | +Records the remaining ordinal-track frontier in the same dated idiom |
| 12 | +as the retraction log's `R-2026-05-18`, so it is findable in the |
| 13 | +record a cold review reads — not buried in appendix prose. This entry |
| 14 | +is the *named non-claim* behind the Pillar E ordinal appendix |
| 15 | +(`paper.adoc` §"Ordinal / Buchholz consumer-evidence"), which was |
| 16 | +written at the *well-foundedness* milestone (machinery + WF exists), |
| 17 | +NOT at the order-type-fidelity milestone. It is an open-problem / |
| 18 | +scope-boundary record, not a retraction of an asserted claim (the |
| 19 | +order-type claim was never asserted). |
| 20 | + |
| 21 | +toc::[] |
| 22 | + |
| 23 | +== The bounded claim (what IS established) |
| 24 | + |
| 25 | +The Buchholz ordinal-notation track has reached its Bachmann–Howard |
| 26 | +milestone in the following bounded sense, and only this sense: |
| 27 | + |
| 28 | +. *Notation machinery E1–E7 mechanised* — OT syntax, CNF below ε₀ |
| 29 | + (`cnf-trichotomy`), the ℕ-staged closure `C-monotone`, the |
| 30 | + pedagogical ψ (`psi-notin-C` / `psi-least`), the Buchholz Ω_ν scale |
| 31 | + + C_ν + ψ_ν (`Cν-monotone`), well-formed *target terms* up to |
| 32 | + ψ₀(Ω_ω) (`BH-wf` / `psi-OmegaOmega-wf`), and the echo collapse |
| 33 | + bridge (`ordinal-collapse-non-injective`). The Bachmann–Howard |
| 34 | + target term ψ₀(Ω_ω) is expressible and well-formed. |
| 35 | +. *Well-foundedness of the ν ≤ ω fragment* under `--safe --without-K`, |
| 36 | + zero postulates: the native accessibility proof |
| 37 | + `WellFounded.wf-<ᵇ`, and the ordinally-sound, *unbudgeted* |
| 38 | + doubled-ladder routes `RankDoubledLadderUmbrella.wf-<ᵇ²`, |
| 39 | + `RecursiveSurfaceSound.wf-<ᵇʳᶠ²`, and `OrderExtendedSound.wf-<ᵇ⁺²`. |
| 40 | + |
| 41 | +== The open problem (what is NOT established) |
| 42 | + |
| 43 | +*Order-type fidelity.* Well-foundedness is necessary but not |
| 44 | +sufficient: the notation is proven to be a *well-founded order*, and |
| 45 | +is NOT proven to be *the Bachmann–Howard ordinal order*. The two |
| 46 | +carriers each fall short of fidelity in precisely identified ways: |
| 47 | + |
| 48 | +* *Native `_<ᵇ_`* is well-founded but ordinally *unsound* — a |
| 49 | + syntactic order engineered for the accessibility proof. The |
| 50 | + constructor `<ᵇ-+Ω` admits |
| 51 | + `bplus bzero (bOmega (fin 1)) <ᵇ bOmega (fin 0)`, a comparison with |
| 52 | + no ordinal meaning (`buchholz-rank-obstruction.adoc`). So `wf-<ᵇ` |
| 53 | + certifies termination, not order-type. |
| 54 | +* *The sound carrier `_<ᵇ²_`* (via the doubled-ladder rank `rank2`) |
| 55 | + *is* ordinally sound but is a *termination measure*: it maps ψ_ν / |
| 56 | + Ω_ν into small ω-power blocks `ω^(2ν+1)` / `ω^(2ν+2)` in Brouwer |
| 57 | + ordinals, *collapsing the actual ordinal heights*. It is not a |
| 58 | + height-preserving denotation and reaches nothing near ψ₀(Ω_ω) as a |
| 59 | + height — by design; its job is well-foundedness. |
| 60 | + |
| 61 | +To close the frontier, supply *either*: |
| 62 | + |
| 63 | +[loweralpha] |
| 64 | +. a verified order-preserving denotation `‖·‖ : BT → 𝒪` into a |
| 65 | + reference ordinal structure `𝒪` of height ψ₀(Ω_ω), with |
| 66 | + order-preservation proved on the well-formed fragment |
| 67 | + (`s <ᵇ t` iff `‖s‖ < ‖t‖`); or |
| 68 | +. a direct order-type computation showing the well-founded restricted |
| 69 | + order has order-type ψ₀(Ω_ω) (fundamental sequences / a |
| 70 | + collapsing-function correctness argument). |
| 71 | + |
| 72 | +No current module establishes either. This is the classical |
| 73 | +order-type-correctness content of an ordinal-notation system; |
| 74 | +well-foundedness (extensively hardened) is the prerequisite, not the |
| 75 | +result. |
| 76 | + |
| 77 | +== Echo's non-role |
| 78 | + |
| 79 | +Echo-types' role in the Buchholz track is the collapse bridge — a |
| 80 | +component only. Echo does not supply, and is not claimed to supply, |
| 81 | +the order-type fidelity proof. Loss-grading and ordinal-collapsing |
| 82 | +are structurally analogous, but the analogy is not an instance, and |
| 83 | +no part of the Bachmann–Howard milestone is discharged by echo's |
| 84 | +framing. This is the dual of the paper's existing firewall (which |
| 85 | +keeps the ordinal track from inflating the identity claim): here, |
| 86 | +echo gets no credit for the ordinal work, and the ordinal work leans |
| 87 | +on echo for none of its strength. |
| 88 | + |
| 89 | +== Status |
| 90 | + |
| 91 | +* Pillar E ordinal appendix: *written at WF milestone; order-type |
| 92 | + fidelity OPEN.* |
| 93 | +* This frontier is the realistic remaining ordinal-track advance that |
| 94 | + does not require external mathematical input; it is distinct from |
| 95 | + the *walled* global-native `wf-<ᵇʳᶠ` (whose close-out is a |
| 96 | + falsifiable verdict, per `buchholz-rank-obstruction.adoc`). |
| 97 | + |
| 98 | +== See also |
| 99 | + |
| 100 | +* `docs/echo-types/paper.adoc` §"Ordinal / Buchholz consumer-evidence" |
| 101 | + — the appendix this record anchors. |
| 102 | +* `docs/echo-types/buchholz-rank-obstruction.adoc` — the carrier |
| 103 | + soundness analysis + the doubled-ladder closure. |
| 104 | +* `docs/bridges/buchholz-plan.adoc` — the E-stage matrix and the |
| 105 | + S1/S2/S3 Bachmann–Howard staging. |
| 106 | +* `roadmap.adoc` §Lane 3 — the ordinal-track open items. |
0 commit comments