Skip to content

Commit 376734d

Browse files
committed
docs(roadmap): note the doubled-ladder Gate 1 closure in Lane 3
Refresh roadmap.adoc Lane 3 (ordinal/Buchholz) per the rung- consolidation policy: record the doubled-ladder route (PRs #204#210) that closed the equal-Ω boundary + the bplus-target <ᵇ-+1 on the complete sound carrier _<ᵇ², with wf-<ᵇ². Flags the honest scope (it's a stronger sound carrier, not a native projection) and that it does NOT discharge the three still-open ordinal items (unbudgeted <ᵇʳᶠ WF, K-limited shared-binder cases, native-_<ᵇ_ internalisation). Doc-only. https://claude.ai/code/session_017t53M7W7ubmXpwymveLcCE
1 parent 8df6d0e commit 376734d

1 file changed

Lines changed: 25 additions & 3 deletions

File tree

roadmap.adoc

Lines changed: 25 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -384,11 +384,33 @@ and Path-4 same-right is refuted by the same lemma.
384384
cannot close under `--safe --without-K` for the current `_<ᵇ_`,
385385
with the WfCNF-restricted `_<ᵇ⁻_` accepted as the final form.
386386

387+
*Doubled-ladder Gate 1 closure (2026-06-14, PRs #204–#210).* A
388+
second, complete route to a sound rank landed: the doubled-index
389+
ladder `rank2` (ψ_ν ↦ ω^(2ν+1), Ω_ν ↦ ω^(2ν+2)) gives ψ and Ω their
390+
own interleaved exponent blocks, so the cross-index gap survives the
391+
equal-Ω boundary `<ᵇ-ψΩ≤` the single ladder could not order. ALL 12
392+
core constructors close at the per-case level under `rank2`, and the
393+
umbrella `rank2-mono-<ᵇ²` + `wf-<ᵇ² : WellFounded _<ᵇ²_` land over the
394+
complete sound carrier `_<ᵇ²_` (`RankDoubledLadderUmbrella`). This is
395+
a STRICTLY STRONGER sound carrier than the single-ladder union
396+
`_<ᵇᵘ_` — it closes the equal-Ω boundary AND the bplus-target
397+
`<ᵇ-+1` (the single-ladder Gate 1 blocker) with one ordinally-sound
398+
scalar rank. *Honest scope:* `_<ᵇ²_` is a sound carrier (like
399+
`_<ᵇ⁰_`/`_<ᵇᵘ_`), excluding the ordinally-unsound native witnesses;
400+
there is no faithful native projection (native `_<ᵇ_` is ordinally
401+
unsound — see the `<ᵇ-+Ω` counterexample in the obstruction note),
402+
and native WF is already proved directly in `WellFounded.wf-<ᵇ`. So
403+
this closes the *carrier* Gate-1 story but does NOT discharge the
404+
three open items above (unbudgeted `_<ᵇʳᶠ_` WF; the K-limited
405+
shared-binder cases; native-`_<ᵇ_` internalisation, which is
406+
rank-embedding-impossible).
407+
387408
*Artefacts.* See `docs/buchholz-plan.adoc`,
388409
`docs/echo-types/buchholz-rank-obstruction.adoc` (live per-constructor
389-
verdict), and the `Ordinal/Buchholz/` subtree. Per-session ledger in
390-
CLAUDE.md §"Session arc 2026-05-20" and §"Session arc 2026-05-27 late
391-
evening".
410+
verdict + the doubled-ladder closure section), and the
411+
`Ordinal/Buchholz/` subtree. Per-session ledger in CLAUDE.md
412+
§"Session arc 2026-06-14 Ordinal track — doubled-ladder Gate 1
413+
closure".
392414

393415
*Status.* Continue on parallel branches. Lane 1 does not wait.
394416

0 commit comments

Comments
 (0)