Skip to content

Commit f6fb7ce

Browse files
committed
docs: close two deeper-sweep gaps in the bridge/plan ledgers
Two artefacts I'd flagged as "no touch needed" on first audit actually did need touching once I re-read them: * `docs/bridge-status.md` row #4 (Buchholz / Veblen Ordinals) said "BLOCKED — Well-foundedness of shared-binder cases is blocked by the failure of the self-lift." That blocker is resolved (`RankAdm` + `RankLex`, 2026-05-26/27). Updated to "PARTIAL (11/13 constructors closed under WfCNF; 1 in flight)" with the head-Ω-route landings named and a pointer to the live tracker. * `docs/bridge-status.md` gains row #6 for the decoration bridge as a conceptual (not cross-repo) entry — the doc's stated scope is "experimental extensions and bridges between the minimal core of Echo Types and other domains", which the decoration bridge fits even though it has no adjacent-repo side. * `docs/bridges/buchholz-plan.adoc` is the original phased spec from when E1–E7 were ahead of us. Its "PLANNED" tags for Phase 2.2 rank-mono etc. are now dated; many of those phases landed under different module names. Added a CAUTION banner at the top of the document pointing to the live tracker (`buchholz-rank-obstruction.adoc`), the live lane status (`roadmap.adoc` § Lane 3), and the per-session ledger (`CLAUDE.md`). The body is left intact for provenance — it's still the cleanest single source of the original design context. `scripts/kernel-guard.sh`: PASS. No Agda modules touched. https://claude.ai/code/session_013nLEeKZXpvHnrDZMgRm19S
1 parent 1d99484 commit f6fb7ce

2 files changed

Lines changed: 23 additions & 2 deletions

File tree

docs/bridge-status.md

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,13 +23,19 @@ This document strictly tracks the status of experimental extensions and bridges
2323
- **Core Affect:** NO
2424

2525
## 4. Buchholz / Veblen Ordinals
26-
- **Status:** BLOCKED
26+
- **Status:** PARTIAL (11/13 constructors closed under WfCNF; 1 in flight)
2727
- **Dependencies:** Standard Agda
28-
- **Blockers:** Well-foundedness of shared-binder cases is blocked by the failure of the self-lift.
28+
- **Blockers:** `<ᵇ-+1` joint-bplus is the single remaining open constructor. The head-Ω domination route (option A) has its abstraction + per-marker dominances at both branches + the option-(b) head-Ω inversion lemmas all landed across 2026-05-27 (PRs #124 / #130 / #131); only the WfCNF-carrier structural recursion (Slice 2-bplus) remains. The earlier shared-binder-self-lift blocker is resolved (`RankAdm` + `RankLex` slices, 2026-05-26/27). Live tracker: `docs/echo-types/buchholz-rank-obstruction.adoc`.
2929
- **Core Affect:** NO
3030

3131
## 5. JanusKey / Categorical
3232
- **Status:** EXPLORATORY
3333
- **Dependencies:** Categorical foundations
3434
- **Blockers:** Higher-level abstractions (monads, adjunctions) are still evolving; core functors are stable.
3535
- **Core Affect:** NO
36+
37+
## 6. Decoration bridge (conceptual, not cross-repo)
38+
- **Status:** EXPLORATORY (R5 deferred-research; cleanly abandonable)
39+
- **Dependencies:** `EchoIntegration`, `EchoChoreo`, `EchoGraded` (import only)
40+
- **Blockers:** Bridge is bounded by construction. Closes under any of the documented termination criteria: Track A/B/C failure, all candidate analogies retired, redundancy with retracted-prose graded-comonad framing, forbidden-rebrandings register addition, retraction-watch trip. Companion: `docs/echo-types/explorations/decoration-bridge/README.adoc`; module: `proofs/agda/EchoDecorationBridge.agda` (deliberately not in `All.agda`).
41+
- **Core Affect:** NO

docs/bridges/buchholz-plan.adoc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,21 @@
44
:sectnums:
55
:sectnumlevels: 2
66

7+
[CAUTION]
8+
====
9+
*Historical spec.* This document is the original phased plan for the
10+
ordinal-notation / collapsing-function workstream as written when E1–E7
11+
were ahead of us. The "PLANNED" tags below are dated; many phases have
12+
since landed under different module names (E1–E7 closed; the WfCNF
13+
restriction + `RankPow` / `RankAdm` / `RankLex` slices replace the
14+
generic `Phase 2.2 rank-mono`; the WF-0/WF-1 well-foundedness is in
15+
`Ordinal.Buchholz.WellFounded`). *Live per-constructor verdict*:
16+
`docs/echo-types/buchholz-rank-obstruction.adoc`. *Live lane status*:
17+
`roadmap.adoc` § Lane 3. *Per-session ledger*: `CLAUDE.md` § "Current
18+
rung state". This file is retained for provenance and design context;
19+
treat its concrete "PLANNED" items as superseded.
20+
====
21+
722
[.lead]
823
This document scopes the ordinal-notation / collapsing-function workstream
924
(Workstream E in `roadmap.adoc`). It is a spec, not a theorem file.

0 commit comments

Comments
 (0)