Skip to content

Commit bcc026b

Browse files
claudeclaude
committed
docs(pillar-e): write the ordinal appendix at the WF milestone; name order-type fidelity OPEN
Writes paper.adoc §"Ordinal / Buchholz consumer-evidence" (the last [EXPAND] tag) at the WEAKER milestone reading, fixing that reading on the page rather than leaving it to interpretation: * "milestone reached" = notation machinery E1–E7 + well-foundedness of the ν ≤ ω fragment (now unbudgeted on the sound carrier via wf-<ᵇ² / wf-<ᵇʳᶠ² / wf-<ᵇ⁺²). Nothing else. * Named non-claim (not a hedge): does NOT claim order-type fidelity. WF is necessary, not sufficient — proven a well-founded order, NOT proven the Bachmann–Howard ordinal order. Both carriers named with exact limits: native _<ᵇ_ is WF but ordinally unsound (the <ᵇ-+Ω counterexample has no ordinal meaning); the sound carrier _<ᵇ²_ via rank2 collapses heights — a termination measure, not a height-preserving denotation. * Open problem stated precisely: a verified order-preserving ‖·‖ : BT → 𝒪 of height ψ₀(Ω_ω), OR a direct order-type computation. No current module establishes either. * Echo's non-role as its own statement: echo is the collapse bridge, a component only; it does not supply the fidelity proof. The dual firewall — echo gets no credit for the ordinal work, the ordinal work leans on echo for none of its strength. Logs the open problem in the dated decision-log idiom as D-2026-06-14 (decisions/ordinal-bh-order-type-fidelity-open.adoc) so it is findable in the record a cold review reads, not buried in appendix prose. Status labels carry the caveat (not a bare "done"): paper.adoc banner, establishment-plan.adoc Pillar E bullet + table row + a dated revision entry, and wiki/Roadmap.adoc all record "Pillar E appendix: written at WF milestone; order-type fidelity OPEN". Doc-only; no .agda touched. https://claude.ai/code/session_017t53M7W7ubmXpwymveLcCE
1 parent ffa3152 commit bcc026b

4 files changed

Lines changed: 248 additions & 32 deletions

File tree

‎docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc‎

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,106 @@
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.

‎docs/echo-types/establishment-plan.adoc‎

Lines changed: 25 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -212,10 +212,14 @@ Authority is conferred socially, not internally. In cost/payoff order:
212212
`--safe --without-K` Agda artefact; these venues reward the
213213
retraction/gate discipline). *Draft started 2026-05-17:*
214214
`docs/echo-types/paper.adoc` — a *living* full-paper draft,
215-
written now while the result is fresh, with sections explicitly
216-
marked for expansion as more context (extended examples,
217-
comparison depth, the ordinal consumer-evidence) accrues. Not for
218-
submission until those land; see its own status banner.
215+
written now while the result is fresh. All four `[EXPAND]` tags are
216+
cleared as of 2026-06-14. *Pillar E appendix: written at WF
217+
milestone; order-type fidelity OPEN* — the ordinal consumer-evidence
218+
appendix is written at the well-foundedness milestone only, with
219+
the Bachmann–Howard order-type-fidelity proof recorded as a named
220+
open problem (decision-log `D-2026-06-14`), NOT claimed. Not for
221+
submission until venue/template are chosen and that caveat is judged
222+
acceptable; see the paper's status banner.
219223
. Zenodo DOI + installable library packaging (stable module API so
220224
others can `import echo-types`).
221225
. Circulate the strongest adjacency note (HoTT fibres / QTT-modal)
@@ -323,7 +327,7 @@ by `≤g-prop` / `⊑-prop`). → ruled out, see
323327
| D | `EchoRelModel.agda` (`GradedLossModel`/`GCLaws`, 2 models, `model-agreement`) | Landed
324328
| D | `docs/echo-types/conservativity.adoc` (metatheorem + 3-clause anchor) | Landed
325329
| E | `docs/echo-types/types-abstract.adoc` (TYPES extended abstract) | Drafted (content submission-ready)
326-
| E | `docs/echo-types/paper.adoc` (full CPP/ITP paper) | Living draft (sections tagged [EXPAND])
330+
| E | `docs/echo-types/paper.adoc` (full CPP/ITP paper) | Living draft; all [EXPAND] tags cleared. Ordinal appendix: written at WF milestone; order-type fidelity OPEN (`D-2026-06-14`)
327331
| E | Zenodo DOI / installable library packaging / outreach | Not started (offline / author-driven)
328332
|===
329333

@@ -404,3 +408,19 @@ reason.
404408
`types-abstract.adoc` ("submission-ready" status withdrawn),
405409
`docs/retractions.adoc` R-2026-05-18. Pillars A–D stand at their
406410
*narrowed* strength; Pillar E re-review is the open item.
411+
* *2026-06-14 — trigger: ordinal appendix written at WF milestone.*
412+
The last `[EXPAND]` tag (tag 4, ordinal consumer-evidence appendix)
413+
is cleared: `paper.adoc` §"Ordinal / Buchholz consumer-evidence" is
414+
written at the *well-foundedness* milestone ("notation machinery
415+
E1–E7 + WF of the ν ≤ ω fragment exists", the latter now unbudgeted
416+
on the sound carrier via `wf-<ᵇ²` / `wf-<ᵇʳᶠ²` / `wf-<ᵇ⁺²`). The
417+
appendix does NOT claim order-type fidelity: well-foundedness is
418+
necessary, not sufficient; the notation is proven well-founded, NOT
419+
proven to be the Bachmann–Howard ordinal order. That order-type
420+
proof is recorded as a named open problem in decision-log
421+
`D-2026-06-14`
422+
(`decisions/ordinal-bh-order-type-fidelity-open.adoc`). *Status:
423+
Pillar E appendix written at WF milestone; order-type fidelity
424+
OPEN.* The in-repo half of Pillar E is complete at the
425+
bounded-claim level; submission logistics remain offline /
426+
author-driven.

‎docs/echo-types/paper.adoc‎

Lines changed: 106 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,14 @@
1111
====
1212
*STATUS: living draft, not for submission.* Written 2026-05-17 while
1313
the formal result is fresh, so the narrative is captured at full
14-
strength now. Sections tagged *[EXPAND]* are deliberate stubs to be
15-
filled as more context accrues; only the ordinal/Buchholz
16-
consumer-evidence appendix remains, and is gated on the ordinal
17-
track reaching Bachmann–Howard (see <<ordinal-appendix>>). Do not
18-
submit until that tag clears and the venue/template are chosen
19-
(Pillar E logistics are offline/author-driven). The TYPES extended
14+
strength now. All four `[EXPAND]` tags are now cleared: the
15+
ordinal/Buchholz consumer-evidence appendix was written 2026-06-14 at
16+
the *well-foundedness* milestone — "notation machinery + WF exists" —
17+
with order-type fidelity recorded as a named OPEN problem, not
18+
claimed (see <<ordinal-appendix>> and decision-log `D-2026-06-14`).
19+
Do not submit until the venue/template are chosen (Pillar E logistics
20+
are offline/author-driven) and the standing order-type-fidelity
21+
caveat is judged acceptable for the chosen venue. The TYPES extended
2022
abstract
2123
(`types-abstract.adoc`) is the short, already-submission-ready
2224
companion; this is the full CPP/ITP-style mechanised-metatheory
@@ -31,11 +33,14 @@ leg) cleared in PR #120, with the single-page reviewer companion at
3133
summary; tag 3 (evaluation — proof-size / cost table, honest
3234
account of the common-upper-bound idiom) cleared earlier in PR #84
3335
(see §"Evaluation and discussion"). Tag 4 (ordinal consumer-evidence
34-
appendix) is the only one remaining open, and it is *gated* on the
35-
ordinal-track milestone per `roadmap.adoc` §Lane 3 — not a missing
36-
deliverable for the in-repo half of Pillar E. Everything else
37-
(venue choice, Zenodo DOI, library packaging, outreach) is
38-
author-driven and is flagged but not auto-run.
36+
appendix) was cleared 2026-06-14: written at the well-foundedness
37+
milestone, with order-type fidelity stated as a named open problem
38+
(decision-log `D-2026-06-14`) rather than claimed. The in-repo half
39+
of Pillar E is therefore complete at the bounded-claim level; the
40+
order-type-fidelity proof remains the recorded ordinal-track
41+
frontier. Everything else (venue choice, Zenodo DOI, library
42+
packaging, outreach) is author-driven and is flagged but not
43+
auto-run.
3944
====
4045

4146
toc::[]
@@ -789,9 +794,12 @@ reading accordingly.
789794
==== Sample-size on consumer evidence
790795

791796
The two consumer-evidence streams (`absolute-zero` for compute-side
792-
identity programs; the planned Buchholz ordinal-notation track) are
793-
each *one* downstream; the ordinal track is gated on reaching
794-
Bachmann–Howard and is not yet in scope (see <<ordinal-appendix>>).
797+
identity programs; the Buchholz ordinal-notation track) are each
798+
*one* downstream; the ordinal track is summarised in
799+
<<ordinal-appendix>> at the *well-foundedness* milestone only, with
800+
order-type fidelity recorded as a named open problem (decision-log
801+
`D-2026-06-14`) — so it corroborates the Echo–`<ᵇ` collapse bridge,
802+
not any ordinal-strength claim.
795803
A failure mode of this paper would be over-reading either as
796804
external validation of the *thesis*; both are validations of
797805
particular technical bridges (the Echo–CNO bridge and the eventual
@@ -1363,14 +1371,90 @@ instance. External validation is the remaining step.
13631371

13641372
[appendix]
13651373
[#ordinal-appendix]
1366-
== Ordinal / Buchholz consumer-evidence [EXPAND]
1367-
1368-
NOTE: *[EXPAND]* — the ordinal-notation / Buchholz collapsing track
1369-
is *consumer evidence* (an independent heavy user of the echo
1370-
machinery), firewalled from the identity claim exactly as
1371-
`roadmap.md` mandates. Summarise it here as an appendix only, with
1372-
the firewall stated explicitly, once that track reaches its
1373-
Bachmann–Howard milestone.
1374+
== Ordinal / Buchholz consumer-evidence
1375+
1376+
*Status: written at the well-foundedness milestone; order-type
1377+
fidelity OPEN (decision-log `D-2026-06-14`,
1378+
`docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc`).*
1379+
1380+
The ordinal-notation / Buchholz collapsing track is *consumer
1381+
evidence* — an independent heavy user of the echo machinery (the
1382+
Echo–`<ᵇ` collapse bridge), firewalled from the identity claim
1383+
exactly as `roadmap.adoc` §Lane 3 mandates. This appendix summarises
1384+
it at a *deliberately bounded* milestone, and fixes that reading on
1385+
the page so it is not left to interpretation.
1386+
1387+
=== What "milestone reached" means here
1388+
1389+
For this appendix, "the Buchholz track has reached its Bachmann–Howard
1390+
milestone" means exactly, and only, the following two things:
1391+
1392+
. *Notation machinery (E1–E7) is mechanised.* OT syntax + structural
1393+
induction (E1); the CNF fragment below ε₀ with `cnf-trichotomy`
1394+
(E2); the ℕ-staged closure family `C-monotone` (E3); the
1395+
pedagogical ψ as least gap, `psi-notin-C` / `psi-least` (E4); the
1396+
Buchholz Ω_ν scale + C_ν + ψ_ν, `Cν-monotone` / `psiν-notin-Cν`
1397+
(E5); well-formed *target terms* up to ψ₀(Ω_ω), `BH-wf` /
1398+
`psi-OmegaOmega-wf` (E6); and the echo collapse bridge
1399+
`ordinal-collapse-non-injective` (E7). The Bachmann–Howard target
1400+
term ψ₀(Ω_ω) is expressible and well-formed.
1401+
. *Well-foundedness of the ν ≤ ω fragment is established*, under
1402+
`--safe --without-K`, zero postulates. The direct accessibility
1403+
proof `WellFounded.wf-<ᵇ` covers the native core; the doubled-ladder
1404+
sound carrier adds the ordinally-sound, *unbudgeted* routes
1405+
`RankDoubledLadderUmbrella.wf-<ᵇ²`,
1406+
`RecursiveSurfaceSound.wf-<ᵇʳᶠ²`, and `OrderExtendedSound.wf-<ᵇ⁺²`,
1407+
all via the `rank2` embedding into Brouwer ordinals.
1408+
1409+
"Machinery + well-foundedness exists" is the whole of what this
1410+
appendix asserts the track has reached. Nothing else.
1411+
1412+
=== The named non-claim (an open problem, not a hedge)
1413+
1414+
This appendix does NOT claim *order-type fidelity*. Well-foundedness
1415+
is necessary but not sufficient: the notation is proven to be a
1416+
*well-founded order*, and is NOT proven to be *the Bachmann–Howard
1417+
ordinal order*. The two carriers each fall short of fidelity in
1418+
precisely identified ways:
1419+
1420+
* *Native `_<ᵇ_`* is well-founded (`WellFounded.wf-<ᵇ`) but ordinally
1421+
*unsound*: a syntactic order engineered for the accessibility
1422+
proof, not the genuine ordinal order. The constructor `<ᵇ-+Ω`
1423+
admits `bplus bzero (bOmega (fin 1)) <ᵇ bOmega (fin 0)` — a
1424+
comparison with *no ordinal meaning* (a sum dominated by a large
1425+
tail placed below a small Ω). So `wf-<ᵇ` certifies termination, not
1426+
order-type.
1427+
* *The sound carrier `_<ᵇ²_`* (via the doubled-ladder rank `rank2`)
1428+
*is* ordinally sound, but `rank2` is a *termination measure*: it
1429+
maps ψ_ν and Ω_ν into small ω-power blocks `ω^(2ν+1)` / `ω^(2ν+2)`
1430+
in Brouwer ordinals, *collapsing the actual ordinal heights*. It is
1431+
not a height-preserving denotation, and reaches nothing near
1432+
ψ₀(Ω_ω) as a height — by design; its job is well-foundedness.
1433+
1434+
The open problem, stated precisely, is to supply *either*:
1435+
1436+
[loweralpha]
1437+
. a verified order-preserving denotation `‖·‖ : BT → 𝒪` into a
1438+
reference ordinal structure `𝒪` of height ψ₀(Ω_ω), with
1439+
order-preservation proved on the well-formed fragment
1440+
(`s <ᵇ t` iff `‖s‖ < ‖t‖`); or
1441+
. a direct order-type computation showing the well-founded restricted
1442+
order has order-type ψ₀(Ω_ω) (fundamental sequences / a
1443+
collapsing-function correctness argument).
1444+
1445+
No current module establishes either. This is the remaining frontier,
1446+
recorded as decision-log `D-2026-06-14`.
1447+
1448+
=== Echo's non-role
1449+
1450+
Echo-types' role in the Buchholz track is the collapse bridge — a
1451+
component only. Echo does not supply, and is not claimed to supply,
1452+
the order-type fidelity proof. Loss-grading and ordinal-collapsing
1453+
are structurally analogous, but the analogy is not an instance, and
1454+
no part of the Bachmann–Howard milestone is discharged by echo's
1455+
framing. This is the dual of the paper's existing firewall: echo gets
1456+
no credit for the ordinal work, and the ordinal work leans on echo
1457+
for none of its strength.
13741458

13751459
[appendix]
13761460
== Artefact statement

‎wiki/Roadmap.adoc‎

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -73,11 +73,17 @@ Target: *Bachmann–Howard* ψ₀(Ω_ω). Open, in priority order:
7373

7474
=== Establishment track — Pillar E only
7575

76-
Pillars A–D and F (F1–F4) are closed. Remaining:
77-
78-
. Clear the `paper.adoc` `[EXPAND]` tags: related-work pass, evaluation
79-
(proof-size/cost table), and the *ordinal consumer-evidence appendix* — the
80-
last *gated on the Bachmann–Howard milestone*.
76+
Pillars A–D and F (F1–F4) are closed. All four `paper.adoc` `[EXPAND]`
77+
tags are cleared, the last (ordinal consumer-evidence appendix) on
78+
2026-06-14 — *written at the well-foundedness milestone, with
79+
order-type fidelity recorded as a named OPEN problem*
80+
(decision-log `D-2026-06-14`), NOT claimed. The in-repo half of
81+
Pillar E is complete at the bounded-claim level. Remaining:
82+
83+
. *Order-type fidelity* (the named open problem `D-2026-06-14`): a
84+
verified order-preserving denotation `BT → 𝒪` of height ψ₀(Ω_ω), or
85+
a direct order-type computation. The genuine remaining
86+
ordinal-strength frontier; no current module establishes it.
8187
. *Then*, author-driven and *not* auto-run: Zenodo DOI, installable library
8288
packaging, outreach. Flag to the user; do not start unprompted.
8389

0 commit comments

Comments
 (0)