docs(ordinal): record the doubled-ladder Gate 1 closure in the obstruction note (#209)

## What

Doc-only consolidation (per the rung-consolidation policy) recording
this session's doubled-ladder route in the canonical
`docs/echo-types/buchholz-rank-obstruction.adoc` — a new `==
Doubled-ladder closure (2026-06-14)` section plus See-also entries for
the five new modules.

## Why

The obstruction note previously recorded the single-ladder programme
reaching 12/13 with Gate 1 (the `<ᵇ-+1` cross-head rank-equal sub-case)
as the sole open blocker, and the umbrella deferred. This session's
doubled-ladder route is a **different, complete** approach that the note
didn't yet reflect.

## What it records

- The doubled-index design (`ψ_ν ↦ ω^(2ν+1)`, `Ω_ν ↦ ω^(2ν+2)`) giving ψ
and Ω their own interleaved exponent blocks, so the cross-index gap
survives the equal-Ω boundary the single ladder collapsed.
- All 12 core constructors closing at the per-case level under `rank2`
(including `<ᵇ-ψΩ≤` equal-Ω and the bplus-target `<ᵇ-+1`).
- The `<ᵇ-+ψ` leading-power bridge via `rank2-bounded`.
- The umbrella `rank2-mono-<ᵇ²` + `wf-<ᵇ²` over the sound carrier
`_<ᵇ²_`.
- **Honest scope**: `_<ᵇ²_` is a *sound carrier* (like the existing
`_<ᵇ⁰_` / `_<ᵇᵘ_`) — it excludes the ordinally-unsound native witnesses
(the `<ᵇ-+Ω` counterexample isn't an `_<ᵇ²_` derivation). Native `_<ᵇ_`
is ordinally unsound, so no rank embedding maps it faithfully; its WF is
already proved directly in `WellFounded.wf-<ᵇ`. The doubled ladder's
contribution is a *strictly stronger sound carrier* than the
single-ladder union, closing the equal-Ω boundary and `<ᵇ-+1` with one
ordinally-sound scalar rank.

## Verification

Doc-only; no `.agda` files touched, so the proof suite is unchanged
(still green from #208). AsciiDoc, no `Version:` strings added.

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

docs/echo-types/buchholz-rank-obstruction.adoc

@@ -387,6 +387,60 @@ rank — the per-case closures all sidestep it via either WfCNF
 restriction (rank-pow + admissibility), lex-pair refinement
 (rank-lex), or head-Ω domination (the next slice).
 
+== Doubled-ladder closure (2026-06-14)
+
+A second, complete route to a sound rank lands this session: the
+*doubled-index ladder* `rank2 : BT → Ord`
+(`Ordinal.Buchholz.RankDoubledLadder`).  Where the single ω-power
+ladder gives ψ and Ω the *same* exponent block (so `rank-pow`
+collapses `ψ_ν` / `Ω_ν` and cannot order the equal-Ω boundary
+`<ᵇ-ψΩ≤`, and `rank-adm` inverts `<ᵇ-Ωψ`), the doubled ladder maps
+level `ν` to *two* interleaved blocks:
+
+----
+ψ_ν(α) ↦ ω^(2ν+1) ⊕ rank2 α      Ω_ν ↦ ω^(2ν+2)
+----
+
+so the atomic order `… < ψ_ν(α) < Ω_ν < ψ_{ν+1}(β) < Ω_{ν+1} < …`
+embeds with *strict room everywhere* — consecutive levels are two
+exponent blocks apart, so the cross-index gap `Ω_μ < ψ_{μ+1}(…)`
+survives even at the boundary `ν = suc μ` that defeated the single
+ladder.  The arithmetic spine (`ψ-block-below-Ω-block`,
+`Ω-block-below-next-ψ`, `double-cross-gap`, `ω-rank-pow-reflects-<Ω`)
+and the WfAdm→rank2 scale-transfer bridge `rank2-bounded`
+(`rank2 t <′ ω-rank-pow (double μ)` from `rank-pow t <′ ω-rank-pow μ`)
+discharge the equal-Ω boundary directly.
+
+*All 12 core constructors close at the per-case level* under `rank2`
+(`Ordinal.Buchholz.RankDoubledLadderMono` / `…MonoPlus` / `…AddPrincipal`
+/ `…MonoPlus2`), including the two the single ladder left to side
+conditions or open: `<ᵇ-ψΩ≤` (equal-Ω, both `ν<μ` and `ν=μ`) and the
+bplus-target `<ᵇ-+1`.  The `<ᵇ-+ψ` leading-power obstruction (the
+source must rank below the ψ-block's *leading* power, not the whole
+ψ-rank) is bridged through `rank2-bounded`.
+
+*The umbrella + well-foundedness land* in
+`Ordinal.Buchholz.RankDoubledLadderUmbrella`: a rank2-soundness-ready
+relation `_<ᵇ²_` over all 12 constructors (WfAdm witnesses + leading-
+power bound + WfCNF tail bounds baked in), the umbrella
+`rank2-mono-<ᵇ² : s <ᵇ² t → rank2 s <′ rank2 t` (structural recursion,
+no `TERMINATING`), and `wf-<ᵇ² : WellFounded _<ᵇ²_` via the standard
+`Subrelation` + `On.wellFounded rank2 wf-<′` transport.
+
+*Scope.*  `_<ᵇ²_` is a *sound carrier* relation, like the existing
+`_<ᵇ⁰_` / `_<ᵇᵘ_`: it bakes in the WfCNF/admissibility soundness
+conditions and so excludes the ordinally-unsound witnesses (the
+`<ᵇ-+Ω` counterexample above is *not* an `_<ᵇ²_` derivation, because
+its tail bound `y ≤ᵇ² x` fails — `rank2 (bOmega (fin 1))` does not sit
+below `rank2 (bOmega (fin 0))`).  This is the expected restriction,
+not a gap: native `_<ᵇ_` is ordinally unsound, so no rank embedding
+maps it faithfully, and its well-foundedness is already proved
+directly in `Ordinal.Buchholz.WellFounded.wf-<ᵇ`.  The doubled
+ladder's contribution is a *strictly stronger sound carrier* than the
+single-ladder union `_<ᵇᵘ_`: it closes the equal-Ω boundary and the
+bplus-target `<ᵇ-+1` that the single-ladder Gate 1 left open, with a
+single ordinally-sound scalar rank.
+
 == See also
 
 * `proofs/agda/Ordinal/Buchholz/HeadOmega.agda` — Slice 1; the
@@ -408,6 +462,15 @@ restriction (rank-pow + admissibility), lex-pair refinement
   13 constructors that pin the syntactic order.
 * `proofs/agda/Ordinal/Buchholz/WellFounded.agda` — the direct
   accessibility proof of `wf-<ᵇ`; structural, no rank.
+* `proofs/agda/Ordinal/Buchholz/RankDoubledLadder.agda` — the
+  doubled-index ladder `rank2` + the arithmetic spine
+  (`double-cross-gap`, `rank2-bpsi-below-bOmega`,
+  `ω-rank-pow-reflects-<Ω`, `rank2-bounded`).
+* `proofs/agda/Ordinal/Buchholz/RankDoubledLadderMono.agda`,
+  `…MonoPlus.agda`, `…AddPrincipal.agda`, `…MonoPlus2.agda` — the 12
+  per-constructor `rank2`-mono primitives.
+* `proofs/agda/Ordinal/Buchholz/RankDoubledLadderUmbrella.agda` — the
+  `_<ᵇ²_` carrier, the umbrella `rank2-mono-<ᵇ²`, and `wf-<ᵇ²`.
 * `proofs/agda/Ordinal/Buchholz/RecursiveSurfaceBudget.agda` —
   budgeted `wf-<ᵇʳᶠᵇ`, the existing model.
 * `proofs/agda/Ordinal/Buchholz/OrderExtendedBudget.agda` — new in