docs(roadmap): note the doubled-ladder Gate 1 closure in Lane 3 (#211)

## What

Refreshes `roadmap.adoc` Lane 3 (ordinal/Buchholz) per the
rung-consolidation policy, recording this session's doubled-ladder route
(#204–#210). The section was stale — it didn't mention the
doubled-ladder closure.

## What it records

- The doubled-ladder route closing the equal-Ω boundary `<ᵇ-ψΩ≤` + the
bplus-target `<ᵇ-+1` on the complete sound carrier `_<ᵇ²_`, with
`wf-<ᵇ²`.
- The **honest scope**: a strictly stronger sound carrier than `_<ᵇᵘ_`,
not a native projection — and explicitly that it does **not** discharge
the three still-open ordinal items (unbudgeted `_<ᵇʳᶠ_` WF; the
K-limited shared-binder cases `<ᵇ-ψα`/`<ᵇ-+2`; native-`_<ᵇ_`
internalisation, which is rank-embedding-impossible).

## Verification

Doc-only; no `.agda` touched, proof suite unchanged. No `Version:`
strings.

https://claude.ai/code/session_017t53M7W7ubmXpwymveLcCE

---
_Generated by [Claude
Code](https://claude.ai/code/session_017t53M7W7ubmXpwymveLcCE)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

roadmap.adoc

@@ -384,11 +384,33 @@ and Path-4 same-right is refuted by the same lemma.
   cannot close under `--safe --without-K` for the current `_<ᵇ_`,
   with the WfCNF-restricted `_<ᵇ⁻_` accepted as the final form.
 
+*Doubled-ladder Gate 1 closure (2026-06-14, PRs #204–#210).* A
+second, complete route to a sound rank landed: the doubled-index
+ladder `rank2` (ψ_ν ↦ ω^(2ν+1), Ω_ν ↦ ω^(2ν+2)) gives ψ and Ω their
+own interleaved exponent blocks, so the cross-index gap survives the
+equal-Ω boundary `<ᵇ-ψΩ≤` the single ladder could not order. ALL 12
+core constructors close at the per-case level under `rank2`, and the
+umbrella `rank2-mono-<ᵇ²` + `wf-<ᵇ² : WellFounded _<ᵇ²_` land over the
+complete sound carrier `_<ᵇ²_` (`RankDoubledLadderUmbrella`). This is
+a STRICTLY STRONGER sound carrier than the single-ladder union
+`_<ᵇᵘ_` — it closes the equal-Ω boundary AND the bplus-target
+`<ᵇ-+1` (the single-ladder Gate 1 blocker) with one ordinally-sound
+scalar rank. *Honest scope:* `_<ᵇ²_` is a sound carrier (like
+`_<ᵇ⁰_`/`_<ᵇᵘ_`), excluding the ordinally-unsound native witnesses;
+there is no faithful native projection (native `_<ᵇ_` is ordinally
+unsound — see the `<ᵇ-+Ω` counterexample in the obstruction note),
+and native WF is already proved directly in `WellFounded.wf-<ᵇ`. So
+this closes the *carrier* Gate-1 story but does NOT discharge the
+three open items above (unbudgeted `_<ᵇʳᶠ_` WF; the K-limited
+shared-binder cases; native-`_<ᵇ_` internalisation, which is
+rank-embedding-impossible).
+
 *Artefacts.* See `docs/buchholz-plan.adoc`,
 `docs/echo-types/buchholz-rank-obstruction.adoc` (live per-constructor
-verdict), and the `Ordinal/Buchholz/` subtree. Per-session ledger in
-CLAUDE.md §"Session arc 2026-05-20" and §"Session arc 2026-05-27 late
-evening".
+verdict + the doubled-ladder closure section), and the
+`Ordinal/Buchholz/` subtree. Per-session ledger in CLAUDE.md
+§"Session arc 2026-06-14 Ordinal track — doubled-ladder Gate 1
+closure".
 
 *Status.* Continue on parallel branches. Lane 1 does not wait.