docs: refresh E3-E6 status; record same-binder internalisation blocker

Roadmap (`roadmap.adoc`): mark E3 (cnf-trichotomy), E4 (psi-notin-C /
psi-least), E5 (partial: Cν-monotone, psiν-notin-Cν, psiν-stage-lb;
psiν-least-gap still open), and E6 (BH-wf, psi-OmegaOmega-wf) as
DONE with landed-lemma inventories. Previous text still said PLANNED.

Buchholz plan (`docs/buchholz-plan.adoc`): add a 2026-04-24
investigation note on the "mathematical completion" follow-up. Adding
`<ᵇ-ψα` / `<ᵇ-+2` as constructors to `_<ᵇ_` typechecks and `<ᵇ-trans`
extends cleanly, but `<ᵇ-irrefl` (direct pattern) hits the
`--without-K` reflexive-equation blocker and `wf-<ᵇ` (direct) fails
Agda 2.8's termination checker because lex-Acc descent through a
passed-in `WellFounded _<ᵇ_` witness isn't recognised — even via
module parameter. Documents the three architectural moves that would
unblock (decouple comparison target's lex-WF from `wf-<ᵇ`, rebuild
via an independently-WF BT rank, or `--sized-types`), and the
landing decision (revert; same-binder shapes stay in `<ᵇ⁺` and `<ᵇˢ`
wrappers).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/buchholz-plan.adoc

@@ -221,6 +221,47 @@ Current Veblen-route status after this update:
    into the real order package and then re-close inversion,
    transitivity, and well-foundedness for that enlarged order
 
+Internalisation investigation (2026-04-24):
+
+* Adding `<ᵇ-ψα : α <ᵇ β → bpsi ν α <ᵇ bpsi ν β` and
+  `<ᵇ-+2  : y₂ <ᵇ z₂ → bplus x y₂ <ᵇ bplus x z₂` as constructors to
+  `_<ᵇ_` typechecks under `--safe --without-K` on Agda 2.8.
+* Transitivity `<ᵇ-trans` extends cleanly: every new left×right pair
+  either reduces to a strictly smaller `<ᵇ` / `<Ω` subproof, reuses a
+  head from an existing constructor, or transfers the result via the
+  existing recursive cases. No K-elimination is required for the
+  transitivity step because its inputs' shared middle term forces
+  unification against fresh implicits, not a reflexive equation.
+* `<ᵇ-irrefl` in its current direct-pattern form is blocked. Matching
+  `<ᵇ-ψα α<α : bpsi ν α <ᵇ bpsi ν α` needs the K-free unifier to
+  eliminate `ν = ν`, which it cannot. Workaround: delete the direct
+  `<ᵇ-irrefl` from `Order.agda` and rely on `<ᵇ-irreflexive` in
+  `WellFounded.agda` (derived from `wf-<ᵇ` via `wf⇒asym`). This
+  requires a working `wf-<ᵇ` for the enlarged order.
+* `wf-<ᵇ` (direct) is where the real blocker lives. The `<ᵇ-+2`
+  constructor makes `Acc _<ᵇ_ (bplus α β)` depend on Acc on the
+  right summand β, so the helper must take two Accs and descend
+  lex-wise. Agda 2.8's Foetus-style termination checker does not
+  recognise lex-Acc descent when the second Acc is obtained by
+  calling a passed-in `WellFounded _<ᵇ_` witness — even when the
+  witness enters via an anonymous-module parameter. Attempted
+  variants (standalone `<ᵇ-acc-bplus-lex` parameterised by wfB;
+  module-local `BplusLex`; inline lambda-matched `acc`) all produce
+  the same `[TerminationIssue]` diagnosis.
+* A full mechanisation therefore needs one of the heavier
+  architectural moves: (a) decouple `VeblenComparisonTarget`'s
+  `×-wellFounded'` from `wf-<ᵇ` (bootstrap the lex-WF on a
+  core-restricted `<ᵇ`), or (b) rebuild `wf-<ᵇ` over a BT-structural
+  measure known to be WF independently of `_<ᵇ_` (e.g. explicit
+  ordinal rank), or (c) enable `--sized-types` within this submodule
+  — verify compatibility with `--safe` first — and prove WF by
+  co-inductive size descent on the two-Acc helper. None of these
+  belong in a single incremental step.
+* Current landing (2026-04-24): revert the constructor additions;
+  keep the same-binder shapes in `<ᵇ⁺` (`ExtendedOrder`) and `<ᵇˢ`
+  (`SurfaceOrder`) as before. The blocker is documented here rather
+  than rediscovered.
+
 Risk-gated bridge currently admitted:
 
 * The original top-marker bridges remain as named specialised lemmas

roadmap.adoc

@@ -361,26 +361,50 @@ Pass condition for E2:
 * `C-monotone` compiles without postulates
 * full-suite and smoke CI jobs both still pass
 
-E3. Cantor normal form (next):
+E3. Cantor normal form:
 
 * add `proofs/agda/Ordinal/CNF.agda` — CNF fragment below ε₀
 * prove trichotomy of the CNF strict order
 
-Status: PLANNED
+Status: DONE (2026-04-24)
+
+Delivered in `proofs/agda/Ordinal/CNF.agda`:
+
+* `CNF`, `_<ᶜ_`
+* `<ᶜ-irrefl`, `<ᶜ-trans`
+* `cnf-trichotomy`
+* worked witnesses `one<ᶜtwo`, `two<ᶜω`, `one<ᶜω`
 
 E4. Pedagogical ψ:
 
 * add `proofs/agda/Ordinal/PsiSimple.agda`
 * prove `psi-notin-C` and `psi-least` on the ℕ-staged closure
 
-Status: PLANNED
+Status: DONE (2026-04-24)
+
+Delivered in `proofs/agda/Ordinal/PsiSimple.agda`:
+
+* `psi-notin-C`
+* `psi-at-1`
+* `psi-least`
 
 E5. Buchholz fragment (ν ≤ ω):
 
 * add `proofs/agda/Ordinal/Buchholz/{Syntax,Closure,Psi}.agda`
 * prove `Cν-monotone`, `psiν-notin-Cν`, `psiν-least-gap`
 
-Status: PLANNED
+Status: PARTIAL (2026-04-24)
+
+Delivered:
+
+* `Ordinal/Buchholz/Syntax.agda`, `Closure.agda`, `Psi.agda` all compile
+* `Cν-monotone`, `Cν-index-monotone`, `Cν-monotone-both`
+* `psiν-notin-Cν`, `psiν-stage-lb`, `psiν-index-bound`
+
+Still open:
+
+* `psiν-least-gap` — the stronger least-gap theorem (stage-lb gives `1 ≤ m`;
+  least-gap gives the sharper minimal-stage side).
 
 E6. Target expressibility:
 
@@ -389,7 +413,14 @@ E6. Target expressibility:
   `ψ_0(0)`, `ψ_0(1)`, `ψ_0(Ω)`, `ψ_0(Ω_ω)` (Bachmann–Howard),
   then the term corresponding to `ψ(Ω_Ω)` under the chosen reading
 
-Status: PLANNED
+Status: DONE (2026-04-24)
+
+Delivered in `proofs/agda/Ordinal/Buchholz/Examples.agda` + `WellFormed.agda`:
+
+* `bh-psi0-omega1`, `bh-psi0-omegaω` (Bachmann–Howard target term)
+* `psi0-expands`, `psi0-Omega1-target`
+* `BH`, `BH-wf`
+* `psi-OmegaOmega`, `psi-OmegaOmega-wf` (intended `ψ(Ω_Ω)` reading)
 
 E7. Echo bridge: