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

Author: claude

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

@@ -0,0 +1,106 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= D-2026-06-14 — Bachmann–Howard order-type fidelity (named open problem)
+:toc: macro
+:toclevels: 2
+:sectnums:
+:sectnumlevels: 2
+:icons: font
+
+[.lead]
+Records the remaining ordinal-track frontier in the same dated idiom
+as the retraction log's `R-2026-05-18`, so it is findable in the
+record a cold review reads — not buried in appendix prose. This entry
+is the *named non-claim* behind the Pillar E ordinal appendix
+(`paper.adoc` §"Ordinal / Buchholz consumer-evidence"), which was
+written at the *well-foundedness* milestone (machinery + WF exists),
+NOT at the order-type-fidelity milestone. It is an open-problem /
+scope-boundary record, not a retraction of an asserted claim (the
+order-type claim was never asserted).
+
+toc::[]
+
+== The bounded claim (what IS established)
+
+The Buchholz ordinal-notation track has reached its Bachmann–Howard
+milestone in the following bounded sense, and only this sense:
+
+. *Notation machinery E1–E7 mechanised* — OT syntax, CNF below ε₀
+  (`cnf-trichotomy`), the ℕ-staged closure `C-monotone`, the
+  pedagogical ψ (`psi-notin-C` / `psi-least`), the Buchholz Ω_ν scale
+  + C_ν + ψ_ν (`Cν-monotone`), well-formed *target terms* up to
+  ψ₀(Ω_ω) (`BH-wf` / `psi-OmegaOmega-wf`), and the echo collapse
+  bridge (`ordinal-collapse-non-injective`). The Bachmann–Howard
+  target term ψ₀(Ω_ω) is expressible and well-formed.
+. *Well-foundedness of the ν ≤ ω fragment* under `--safe --without-K`,
+  zero postulates: the native accessibility proof
+  `WellFounded.wf-<ᵇ`, and the ordinally-sound, *unbudgeted*
+  doubled-ladder routes `RankDoubledLadderUmbrella.wf-<ᵇ²`,
+  `RecursiveSurfaceSound.wf-<ᵇʳᶠ²`, and `OrderExtendedSound.wf-<ᵇ⁺²`.
+
+== The open problem (what is NOT established)
+
+*Order-type fidelity.* Well-foundedness is necessary but not
+sufficient: the notation is proven to be a *well-founded order*, and
+is NOT proven to be *the Bachmann–Howard ordinal order*. The two
+carriers each fall short of fidelity in precisely identified ways:
+
+* *Native `_<ᵇ_`* is well-founded but ordinally *unsound* — a
+  syntactic order engineered for the accessibility proof. The
+  constructor `<ᵇ-+Ω` admits
+  `bplus bzero (bOmega (fin 1)) <ᵇ bOmega (fin 0)`, a comparison with
+  no ordinal meaning (`buchholz-rank-obstruction.adoc`). So `wf-<ᵇ`
+  certifies termination, not order-type.
+* *The sound carrier `_<ᵇ²_`* (via the doubled-ladder rank `rank2`)
+  *is* ordinally sound but is a *termination measure*: it maps ψ_ν /
+  Ω_ν into small ω-power blocks `ω^(2ν+1)` / `ω^(2ν+2)` in Brouwer
+  ordinals, *collapsing the actual ordinal heights*. It is not a
+  height-preserving denotation and reaches nothing near ψ₀(Ω_ω) as a
+  height — by design; its job is well-foundedness.
+
+To close the frontier, supply *either*:
+
+[loweralpha]
+. a verified order-preserving denotation `‖·‖ : BT → 𝒪` into a
+  reference ordinal structure `𝒪` of height ψ₀(Ω_ω), with
+  order-preservation proved on the well-formed fragment
+  (`s <ᵇ t` iff `‖s‖ < ‖t‖`); or
+. a direct order-type computation showing the well-founded restricted
+  order has order-type ψ₀(Ω_ω) (fundamental sequences / a
+  collapsing-function correctness argument).
+
+No current module establishes either. This is the classical
+order-type-correctness content of an ordinal-notation system;
+well-foundedness (extensively hardened) is the prerequisite, not the
+result.
+
+== Echo's non-role
+
+Echo-types' role in the Buchholz track is the collapse bridge — a
+component only. Echo does not supply, and is not claimed to supply,
+the order-type fidelity proof. Loss-grading and ordinal-collapsing
+are structurally analogous, but the analogy is not an instance, and
+no part of the Bachmann–Howard milestone is discharged by echo's
+framing. This is the dual of the paper's existing firewall (which
+keeps the ordinal track from inflating the identity claim): here,
+echo gets no credit for the ordinal work, and the ordinal work leans
+on echo for none of its strength.
+
+== Status
+
+* Pillar E ordinal appendix: *written at WF milestone; order-type
+  fidelity OPEN.*
+* This frontier is the realistic remaining ordinal-track advance that
+  does not require external mathematical input; it is distinct from
+  the *walled* global-native `wf-<ᵇʳᶠ` (whose close-out is a
+  falsifiable verdict, per `buchholz-rank-obstruction.adoc`).
+
+== See also
+
+* `docs/echo-types/paper.adoc` §"Ordinal / Buchholz consumer-evidence"
+  — the appendix this record anchors.
+* `docs/echo-types/buchholz-rank-obstruction.adoc` — the carrier
+  soundness analysis + the doubled-ladder closure.
+* `docs/bridges/buchholz-plan.adoc` — the E-stage matrix and the
+  S1/S2/S3 Bachmann–Howard staging.
+* `roadmap.adoc` §Lane 3 — the ordinal-track open items.

docs/echo-types/establishment-plan.adoc

@@ -212,10 +212,14 @@ Authority is conferred socially, not internally. In cost/payoff order:
   `--safe --without-K` Agda artefact; these venues reward the
   retraction/gate discipline). *Draft started 2026-05-17:*
   `docs/echo-types/paper.adoc` — a *living* full-paper draft,
-  written now while the result is fresh, with sections explicitly
-  marked for expansion as more context (extended examples,
-  comparison depth, the ordinal consumer-evidence) accrues. Not for
-  submission until those land; see its own status banner.
+  written now while the result is fresh. All four `[EXPAND]` tags are
+  cleared as of 2026-06-14. *Pillar E appendix: written at WF
+  milestone; order-type fidelity OPEN* — the ordinal consumer-evidence
+  appendix is written at the well-foundedness milestone only, with
+  the Bachmann–Howard order-type-fidelity proof recorded as a named
+  open problem (decision-log `D-2026-06-14`), NOT claimed. Not for
+  submission until venue/template are chosen and that caveat is judged
+  acceptable; see the paper's status banner.
 . Zenodo DOI + installable library packaging (stable module API so
   others can `import echo-types`).
 . Circulate the strongest adjacency note (HoTT fibres / QTT-modal)
@@ -323,7 +327,7 @@ by `≤g-prop` / `⊑-prop`). → ruled out, see
 | D | `EchoRelModel.agda` (`GradedLossModel`/`GCLaws`, 2 models, `model-agreement`) | Landed
 | D | `docs/echo-types/conservativity.adoc` (metatheorem + 3-clause anchor) | Landed
 | E | `docs/echo-types/types-abstract.adoc` (TYPES extended abstract) | Drafted (content submission-ready)
-| E | `docs/echo-types/paper.adoc` (full CPP/ITP paper) | Living draft (sections tagged [EXPAND])
+| 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`)
 | E | Zenodo DOI / installable library packaging / outreach | Not started (offline / author-driven)
 |===
 
@@ -404,3 +408,19 @@ reason.
   `types-abstract.adoc` ("submission-ready" status withdrawn),
   `docs/retractions.adoc` R-2026-05-18. Pillars A–D stand at their
   *narrowed* strength; Pillar E re-review is the open item.
+* *2026-06-14 — trigger: ordinal appendix written at WF milestone.*
+  The last `[EXPAND]` tag (tag 4, ordinal consumer-evidence appendix)
+  is cleared: `paper.adoc` §"Ordinal / Buchholz consumer-evidence" is
+  written at the *well-foundedness* milestone ("notation machinery
+  E1–E7 + WF of the ν ≤ ω fragment exists", the latter now unbudgeted
+  on the sound carrier via `wf-<ᵇ²` / `wf-<ᵇʳᶠ²` / `wf-<ᵇ⁺²`). The
+  appendix does NOT claim order-type fidelity: well-foundedness is
+  necessary, not sufficient; the notation is proven well-founded, NOT
+  proven to be the Bachmann–Howard ordinal order. That order-type
+  proof is recorded as a named open problem in decision-log
+  `D-2026-06-14`
+  (`decisions/ordinal-bh-order-type-fidelity-open.adoc`). *Status:
+  Pillar E appendix written at WF milestone; order-type fidelity
+  OPEN.* The in-repo half of Pillar E is complete at the
+  bounded-claim level; submission logistics remain offline /
+  author-driven.

docs/echo-types/paper.adoc

@@ -11,12 +11,14 @@
 ====
 *STATUS: living draft, not for submission.* Written 2026-05-17 while
 the formal result is fresh, so the narrative is captured at full
-strength now. Sections tagged *[EXPAND]* are deliberate stubs to be
-filled as more context accrues; only the ordinal/Buchholz
-consumer-evidence appendix remains, and is gated on the ordinal
-track reaching Bachmann–Howard (see <<ordinal-appendix>>). Do not
-submit until that tag clears and the venue/template are chosen
-(Pillar E logistics are offline/author-driven). The TYPES extended
+strength now. All four `[EXPAND]` tags are now cleared: the
+ordinal/Buchholz consumer-evidence appendix was written 2026-06-14 at
+the *well-foundedness* milestone — "notation machinery + WF exists" —
+with order-type fidelity recorded as a named OPEN problem, not
+claimed (see <<ordinal-appendix>> and decision-log `D-2026-06-14`).
+Do not submit until the venue/template are chosen (Pillar E logistics
+are offline/author-driven) and the standing order-type-fidelity
+caveat is judged acceptable for the chosen venue. The TYPES extended
 abstract
 (`types-abstract.adoc`) is the short, already-submission-ready
 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
 summary; tag 3 (evaluation — proof-size / cost table, honest
 account of the common-upper-bound idiom) cleared earlier in PR #84
 (see §"Evaluation and discussion"). Tag 4 (ordinal consumer-evidence
-appendix) is the only one remaining open, and it is *gated* on the
-ordinal-track milestone per `roadmap.adoc` §Lane 3 — not a missing
-deliverable for the in-repo half of Pillar E. Everything else
-(venue choice, Zenodo DOI, library packaging, outreach) is
-author-driven and is flagged but not auto-run.
+appendix) was cleared 2026-06-14: written at the well-foundedness
+milestone, with order-type fidelity stated as a named open problem
+(decision-log `D-2026-06-14`) rather than claimed. The in-repo half
+of Pillar E is therefore complete at the bounded-claim level; the
+order-type-fidelity proof remains the recorded ordinal-track
+frontier. Everything else (venue choice, Zenodo DOI, library
+packaging, outreach) is author-driven and is flagged but not
+auto-run.
 ====
 
 toc::[]
@@ -789,9 +794,12 @@ reading accordingly.
 ==== Sample-size on consumer evidence
 
 The two consumer-evidence streams (`absolute-zero` for compute-side
-identity programs; the planned Buchholz ordinal-notation track) are
-each *one* downstream; the ordinal track is gated on reaching
-Bachmann–Howard and is not yet in scope (see <<ordinal-appendix>>).
+identity programs; the Buchholz ordinal-notation track) are each
+*one* downstream; the ordinal track is summarised in
+<<ordinal-appendix>> at the *well-foundedness* milestone only, with
+order-type fidelity recorded as a named open problem (decision-log
+`D-2026-06-14`) — so it corroborates the Echo–`<ᵇ` collapse bridge,
+not any ordinal-strength claim.
 A failure mode of this paper would be over-reading either as
 external validation of the *thesis*; both are validations of
 particular technical bridges (the Echo–CNO bridge and the eventual
@@ -1363,14 +1371,90 @@ instance. External validation is the remaining step.
 
 [appendix]
 [#ordinal-appendix]
-== Ordinal / Buchholz consumer-evidence [EXPAND]
-
-NOTE: *[EXPAND]* — the ordinal-notation / Buchholz collapsing track
-is *consumer evidence* (an independent heavy user of the echo
-machinery), firewalled from the identity claim exactly as
-`roadmap.md` mandates. Summarise it here as an appendix only, with
-the firewall stated explicitly, once that track reaches its
-Bachmann–Howard milestone.
+== Ordinal / Buchholz consumer-evidence
+
+*Status: written at the well-foundedness milestone; order-type
+fidelity OPEN (decision-log `D-2026-06-14`,
+`docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc`).*
+
+The ordinal-notation / Buchholz collapsing track is *consumer
+evidence* — an independent heavy user of the echo machinery (the
+Echo–`<ᵇ` collapse bridge), firewalled from the identity claim
+exactly as `roadmap.adoc` §Lane 3 mandates. This appendix summarises
+it at a *deliberately bounded* milestone, and fixes that reading on
+the page so it is not left to interpretation.
+
+=== What "milestone reached" means here
+
+For this appendix, "the Buchholz track has reached its Bachmann–Howard
+milestone" means exactly, and only, the following two things:
+
+. *Notation machinery (E1–E7) is mechanised.* OT syntax + structural
+  induction (E1); the CNF fragment below ε₀ with `cnf-trichotomy`
+  (E2); the ℕ-staged closure family `C-monotone` (E3); the
+  pedagogical ψ as least gap, `psi-notin-C` / `psi-least` (E4); the
+  Buchholz Ω_ν scale + C_ν + ψ_ν, `Cν-monotone` / `psiν-notin-Cν`
+  (E5); well-formed *target terms* up to ψ₀(Ω_ω), `BH-wf` /
+  `psi-OmegaOmega-wf` (E6); and the echo collapse bridge
+  `ordinal-collapse-non-injective` (E7). The Bachmann–Howard target
+  term ψ₀(Ω_ω) is expressible and well-formed.
+. *Well-foundedness of the ν ≤ ω fragment is established*, under
+  `--safe --without-K`, zero postulates. The direct accessibility
+  proof `WellFounded.wf-<ᵇ` covers the native core; the doubled-ladder
+  sound carrier adds the ordinally-sound, *unbudgeted* routes
+  `RankDoubledLadderUmbrella.wf-<ᵇ²`,
+  `RecursiveSurfaceSound.wf-<ᵇʳᶠ²`, and `OrderExtendedSound.wf-<ᵇ⁺²`,
+  all via the `rank2` embedding into Brouwer ordinals.
+
+"Machinery + well-foundedness exists" is the whole of what this
+appendix asserts the track has reached. Nothing else.
+
+=== The named non-claim (an open problem, not a hedge)
+
+This appendix does NOT claim *order-type fidelity*. Well-foundedness
+is necessary but not sufficient: the notation is proven to be a
+*well-founded order*, and is NOT proven to be *the Bachmann–Howard
+ordinal order*. The two carriers each fall short of fidelity in
+precisely identified ways:
+
+* *Native `_<ᵇ_`* is well-founded (`WellFounded.wf-<ᵇ`) but ordinally
+  *unsound*: a syntactic order engineered for the accessibility
+  proof, not the genuine ordinal order. The constructor `<ᵇ-+Ω`
+  admits `bplus bzero (bOmega (fin 1)) <ᵇ bOmega (fin 0)` — a
+  comparison with *no ordinal meaning* (a sum dominated by a large
+  tail placed below a small Ω). So `wf-<ᵇ` certifies termination, not
+  order-type.
+* *The sound carrier `_<ᵇ²_`* (via the doubled-ladder rank `rank2`)
+  *is* ordinally sound, but `rank2` is a *termination measure*: it
+  maps ψ_ν and Ω_ν into small ω-power blocks `ω^(2ν+1)` / `ω^(2ν+2)`
+  in Brouwer ordinals, *collapsing the actual ordinal heights*. It is
+  not a height-preserving denotation, and reaches nothing near
+  ψ₀(Ω_ω) as a height — by design; its job is well-foundedness.
+
+The open problem, stated precisely, is to supply *either*:
+
+[loweralpha]
+. a verified order-preserving denotation `‖·‖ : BT → 𝒪` into a
+  reference ordinal structure `𝒪` of height ψ₀(Ω_ω), with
+  order-preservation proved on the well-formed fragment
+  (`s <ᵇ t` iff `‖s‖ < ‖t‖`); or
+. a direct order-type computation showing the well-founded restricted
+  order has order-type ψ₀(Ω_ω) (fundamental sequences / a
+  collapsing-function correctness argument).
+
+No current module establishes either. This is the remaining frontier,
+recorded as decision-log `D-2026-06-14`.
+
+=== Echo's non-role
+
+Echo-types' role in the Buchholz track is the collapse bridge — a
+component only. Echo does not supply, and is not claimed to supply,
+the order-type fidelity proof. Loss-grading and ordinal-collapsing
+are structurally analogous, but the analogy is not an instance, and
+no part of the Bachmann–Howard milestone is discharged by echo's
+framing. This is the dual of the paper's existing firewall: echo gets
+no credit for the ordinal work, and the ordinal work leans on echo
+for none of its strength.
 
 [appendix]
 == Artefact statement

wiki/Roadmap.adoc

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