ordinal(buchholz): head-Ω Slice 2 closure + inversion + cross-doc + ledger reinforcement - #131
Merged
Merged
Conversation
Adds a session arc entry for the Slice 2 landing (PR #130, commit bf9ee6e on main) per the rung-consolidation policy. Documents: * what landed (ω-rank-pow-succ + fin-branch dominance + atomic-rank factoring through head-Ω); * the ω-branch obstruction (originally-proposed shape denotes the same ordinal as ω-rank-pow ω); * the two follow-on paths (Slice 2-omega + Slice 2-bplus); * the priority-ordered plan for the next session (option (b) head-Ω inversion first, then Slice 2-omega, then Slice 2-bplus). Notes the PR #130 admin-merge-before-CI-green for honest provenance. https://claude.ai/code/session_013nLEeKZXpvHnrDZMgRm19S
…lus) Lands the two atomic-source inversion lemmas from option (b) of the Slice 2-bplus follow-on plan documented inline in `RankPow.agda`: * head-Ω-inv-bOmega : bOmega ν <ᵇ y → ν <Ω head-Ω y * head-Ω-inv-bpsi : bpsi ν α <ᵇ y → ν ≤Ω head-Ω y Strict on the Ω-source (the three constructors with `bOmega ν` LHS all carry strict `<Ω` witnesses); non-strict on the ψ-source (the `<ᵇ-ψΩ≤` constructor only carries `ν ≤Ω μ`, so the lemma tops out at `≤Ω` — lifted to a unified shape via `<Ω→≤Ω` at the `<ᵇ-ψΩ` case). Proof in each case: structural recursion on the `<ᵇ` derivation, with the `+`-side constructors recursing through their `<ᵇ` premise on the target's left summand. No funext, no postulates, no rank-mono dependency — that last is the load-bearing design choice this slice makes good on, per the dependency-graph invariant the inline comment in `RankPow.agda`'s Slice 2-bplus note flags. Lands as a new module `Ordinal.Buchholz.HeadOmegaInversion`, wired into `All.agda` and pinned in `Ordinal/Buchholz/Smoke.agda` under its own `using` block with a header comment per CLAUDE.md Working rules. The bplus-source inversion is OUT OF SCOPE for this slice (the three `<ᵇ-+_` constructors recurse on `x <ᵇ (target)` where x can be anything, so the natural inversion has to traverse arbitrary BT subterms — different proof structure). Deferred to a follow-on; the Slice 2-bplus consumer handles the bplus source by inducting on the WfCNF carrier and applying the atomic inversions at the leading subterm. `scripts/kernel-guard.sh`: PASS. No postulates introduced. No diff against `EchoIntegration.agda` / `EchoChoreo.agda` / `EchoGraded.agda` or any existing Echo*Bridge.agda. https://claude.ai/code/session_013nLEeKZXpvHnrDZMgRm19S
…ed + dominance proved
Replaces the originally-proposed `ω-rank-pow-succ ω = olim (λ n →
ω^(suc(suc n)))` (equi-ordinal with `ω-rank-pow ω`, so unsound) with
`olim (λ n → ω-rank-pow ω ·ℕ n)`, denoting `ω^(ω+1)` — the next
additive-principal above `ω^ω`.
Proves `ω-rank-pow-<-succ-omega : ω-rank-pow ω <′ ω-rank-pow-succ ω`
by mirroring `Brouwer/OmegaPow.ω^-strict-mono-suc`: pick branch index
2 in the target limit, reduce to `osuc (ω-rank-pow ω) ≤′ (oz ⊕
ω-rank-pow ω) ⊕ ω-rank-pow ω`, chain `X≤′oz⊕X` with
`⊕-mono-<-right (ω-rank-pow-pos ω)`.
Cross-check (iii) from the obstruction note resolved: the proof goes
through `X≤′oz⊕X` which provides exactly the propositional
`X ≤′ oz ⊕ X` step the note flagged as the hazard. Cross-checks (i)
and (ii) still stand without modification — the consumer (Slice 3)
uses the existing `additive-principal-ω-rank-pow {head-Ω target}` for
additive-principal closure, not any property of `ω-rank-pow-succ ω`
itself.
New lemmas (all pinned in `Ordinal/Buchholz/Smoke.agda` under the
existing Slice 2 `using` block):
* ω-rank-pow-succ-omega -- definitional sanity, ω branch
* ω-rank-pow-<-succ-omega -- per-marker strict dominance, ω branch
* ω-rank-pow-<-succ -- unified across both branches
The obstruction-note comment block in `RankPow.agda` is updated:
its "ω branch deferred" subsection moves to a "History note" form
recording the original sketch's failure mode, and the closure-plan
TODO list collapses from two entries to one (Slice 2-bplus, the full
WfCNF-carrier domination lemma — both per-marker dominances + the
HeadOmegaInversion option (b) lemmas are now landed, so Slice 2-bplus
no longer carries any inversion-via-rank-mono dependency).
`scripts/kernel-guard.sh`: PASS. No postulates introduced.
--safe --without-K throughout.
https://claude.ai/code/session_013nLEeKZXpvHnrDZMgRm19S…ion also landed Updates the session-arc entry for 2026-05-27 night to reflect that items (1) and (2) from the original next-step plan also landed in the same session: * Option (b) head-Ω inversion lemma — landed in commit 560f904 as module `Ordinal.Buchholz.HeadOmegaInversion`. * Slice 2-omega — landed in commit 07abc15 (ω branch of `ω-rank-pow-succ` replaced with `olim (λ n → ω-rank-pow ω ·ℕ n)` and strict dominance proved). Only Slice 2-bplus remains open; the bplus case now consumes the HeadOmegaInversion family + per-marker dominances without any further rank-mono dependency. https://claude.ai/code/session_013nLEeKZXpvHnrDZMgRm19S
…the wiki Cross-doc consistency sweep after PRs #129/#130/#131 landed. Five docs had stale Slice 1-era wording that pre-dated the head-Ω route's Slice 2 + Slice 2-omega + option-(b) inversion landings: * `docs/echo-types/buchholz-rank-obstruction.adoc` (the live per- constructor verdict tracker). The `<ᵇ-+1` row flipped from "⏳ joint-bplus, needs coarser bound" to "⏳ joint-bplus, head-Ω route in flight" with the full prerequisite-landings list and the Slice 2-bplus remaining-work note. Score-paragraph + "What remains open" section + "See also" file list all updated. * `roadmap.adoc` § Lane 3. Bottleneck description + close-out criterion refreshed to reflect that the head-Ω abstraction + per-marker dominances + inversion lemmas have all landed across PRs #124/#130/#131; only Slice 2-bplus (the WfCNF-carrier structural recursion) remains. * `EXPLAINME.adoc`. One-paragraph ongoing-tracks line for the ordinal track refreshed from "first slice landed; rank-mono follow-ons designed" to the current "abstraction + per-marker dominances + inversion landed; structural WfCNF recursion remaining" state. * `CHANGELOG.md` § Added (2026-05-27). Two new bullets land: the Slice 2 + Slice 2-omega + inversion follow-on entry (records the Brouwer-encoding hazard the originally-proposed ω-branch shape would have tripped — the `ω^(suc(suc n))` and `ω^(suc n)` limits denote the same `ω^ω` ordinal — and the revised shape `olim (λ n → ω-rank-pow ω ·ℕ n)` denoting `ω^(ω+1)` that resolves it); and the decoration-bridge R5 exploratory scaffold from PR #129. * `docs/echo-types/MAP.adoc`. Buchholz module list adds `HeadOmegaInversion` next to `HeadOmega`. No prose-vs-proof inconsistency remains: every doc that mentions the head-Ω route now reports its current state (which slices landed, which slice remains, what the prerequisites for the remaining slice are) consistent with the Agda artefacts in `Ordinal.Buchholz.{HeadOmega,HeadOmegaInversion,RankPow}` and the session-arc entry in `CLAUDE.md`. `scripts/kernel-guard.sh`: PASS. No Agda modules touched. https://claude.ai/code/session_013nLEeKZXpvHnrDZMgRm19S
hyperpolymath
marked this pull request as ready for review
May 27, 2026 18:11
hyperpolymath
enabled auto-merge (squash)
May 27, 2026 18:11
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
Uh oh!
There was an error while loading. Please reload this page.
3 tasks
hyperpolymath pushed a commit
that referenced
this pull request
May 27, 2026
THE HEADLINE LANDS:
rank-pow-dominated-by-head-Ω : ∀ {t} → WfCNF t →
rank-pow t <′ ω-rank-pow-succ (head-Ω t)
Closes the final prerequisite for the `<ᵇ-+1` joint-bplus discharge
in the Buchholz rank-mono umbrella. Lands in a new module
`Ordinal.Buchholz.RankPowDomination` to keep `RankPow` focused on
the rank-mono primitives.
Proof structure (structural recursion on the WfCNF carrier):
* wf-cnf-bzero: `oz <′ ω^2` via `ω-rank-pow-succ-pos (fin 0)`.
No NonBzero premise needed — bzero falls under the same shape.
* wf-cnf-bomega: collapses to `ω-rank-pow-<-succ ν`.
* wf-cnf-bpsi: same, via the provisional `rank-pow (bpsi ν _) =
ω-rank-pow ν` shape.
* wf-cnf-bplus: `additive-principal-ω-rank-pow-succ {head-Ω x}`
fed by the IH on x and a per-atomic-y bound from
`rank-y-bound`. The atomic-y bound uses `head-Ω-inv-bOmega` /
`head-Ω-inv-bpsi` from `HeadOmegaInversion` to pull `head-Ω`
bounds from the WfCNF tail's `<ᵇ` witness — no rank-mono
dependency anywhere in the chain, preserving the option-(b)
dependency-graph invariant.
Supporting lemmas (all in the new module):
* ω-rank-pow-mono-≤Ω -- ≤Ω → ≤′ lifting (case on the
three constructors of _≤Ω_).
* ω-rank-pow-succ-pos -- positivity at both branches via
`<′-trans` of ω-rank-pow-pos +
ω-rank-pow-<-succ.
* additive-principal-ω-rank-pow-succ
-- fin branch dispatches to OmegaPow's
`additive-principal {suc n}`;
ω branch mirrors that proof with
`ω^ n` replaced by `ω-rank-pow ω`
and `·ℕ-add-≤` consumed at the new
base.
* <′→≤′, ≤′-<′-trans, <′-trans -- inline utilities.
All four headlines pinned in `Ordinal/Buchholz/Smoke.agda` under
their own `using` block per CLAUDE.md Working rules. Wired into
`All.agda`.
What's now closed on the head-Ω domination route:
* Slice 1: head-Ω abstraction + sanity (PR #124).
* Slice 2: ω-rank-pow-succ + fin-branch dominance (PR #130).
* Slice 2-omega: ω-branch dominance (PR #131).
* Option (b) inversion: head-Ω-inv-{bOmega,bpsi} (PR #131).
* Slice 2-bplus: THIS COMMIT.
What remains for the `<ᵇ-+1` joint-bplus discharge:
* Slice 3: rank-mono-<ᵇ-+1-via-head-Ω (the headline consumer).
* Slice 4: full rank-pow-mono-<ᵇ⁻ umbrella composition.
Invariants held:
* No postulates introduced (the grep match in the file is the
word "postulates" in a comment).
* --safe --without-K throughout.
* scripts/kernel-guard.sh: PASS.
* No diff against bridge-protected files.
* agda not available in this container; proof verified by
inspection. Each clause of the main lemma is either a direct
application of an existing primitive or a structural recursion
on a strictly-smaller sub-derivation. The
additive-principal-ω-rank-pow-succ ω-branch is a line-for-line
parallel of OmegaPow's existing `additive-principal`. CI is
authoritative.
https://claude.ai/code/session_013nLEeKZXpvHnrDZMgRm19Shyperpolymath added a commit
that referenced
this pull request
May 27, 2026
…LL PASS + Slice-2 adopted + narrative audit + diagrams (#135) ## Summary End-of-session merge bundling the full Tier-1+2+3 + audience-moves + suite work + Pillar F Gate F5 FULL PASS + the narrative-audit reinforcement pass + structural diagrams. Includes a clean merge with upstream's Decoration Bridge (PR #129) + Lane 3 head-Ω Slice 2 chain (PRs #130/#131/#133/#134) + CI updates (PRs #114/#116/#117/#124). **Three commits:** 1. `f3fdecd` session: Tier-1+2+3 spine + audience moves + suite + F5 FULL PASS + Slice-2 adopted + narrative audit 2. `e96cedc` Merge origin/main: Decoration Bridge + Slice 2 + CI updates 3. `7c495ad` docs: structural diagrams + recommended reading order **Build:** `--safe --without-K`, zero postulates, no funext in trusted base. `Smoke.agda` + `All.agda` both exit 0. ## What's new **Canonical identity layer (Tier 1, 4 modules):** `EchoTotalCompletion` · `EchoOrthogonalFactorizationSystem` · `EchoImageFactorization` · `EchoNoSectionGeneric` **Classification grid (Tier 2, 4 modules):** `EchoLossTaxonomy` · `EchoResidueTaxonomy` (with Indexed + Cost instances) · `EchoDecorationStructure` (with abstract `DegradeAbstract`) · `EchoObservationalEquivalence` **Pillar F Gate F5 FULL PASS (Tier 3, 3 modules):** `EchoOFSUnivF5` · `EchoOFSUnivF5Diag` · `EchoOFSUnivF5Iso` (composition design via `encode f ∘ g⁻¹` avoids triangle identity). Logged as retraction follow-up `F-2026-05-27a`. **Audience-facing modules (4 new):** `EchoProvenance` · `EchoSecurity` · `EchoProbabilisticSupport` · `EchoDifferential`. Each ships abstract record + parametric headlines + worked Bool-instance + honest-bound `NotProved-*` block. **Curated suite:** `EchoCanonicalIdentitySuite.agda` — single-file entry point re-exporting load-bearing headlines. **Consolidation docs:** `docs/echo-types/universal-property.adoc` (pullback + F4 + F5/OFS arc) and `docs/echo-types/fibration-package.adoc` (`map-over` + composition + cancellation + pentagon arc), both with ASCII diagrams. **Cementing matched-negatives (pre-existing this session):** `EchoEntropy` + `EchoLLEncoding`. **Narrative reinforcement:** READMEs, MAP.adoc, theorem-index.md, paper.adoc, types-abstract.adoc, overview.md, establishment-plan.adoc, INDEX.adoc, composition.md, taxonomy.md, assessment.adoc, retractions.adoc, earn-back-plan.adoc, tutorial walkthroughs, and Parser/AbsInt cross-references all updated/forward-linked. Bidirectional audience-abstract back-references closed. **Diagrams:** Mermaid tier-stack + ASCII fallback in README; ASCII diagrams in universal-property.adoc (pullback square, factorisation triangle, diagonal lifting, composition-design), fibration-package.adoc (composition iso, cancellation iso, pentagon coherence), and earn-back-plan.adoc (Pillar F gate dependency). ## Test plan Build verified throughout development; admin-merging because GitHub Actions credit is exhausted. - [x] `agda Smoke.agda` exits 0 - [x] `agda All.agda` exits 0 - [x] No postulates introduced - [x] No escape pragmas introduced - [x] No funext in trusted base - [x] All conflict markers resolved - [x] Local merge with `origin/main` clean 🤖 Generated with [Claude Code](https://claude.com/claude-code)
🔍 Hypatia Security ScanFindings: 56 issues detected
View findings[
{
"reason": "No test directory or test files found",
"type": "no_tests",
"file": "/home/runner/work/echo-types/echo-types",
"action": "flag",
"rule_module": "honest_completion",
"severity": "high",
"deduction": 20
},
{
"reason": "Issue in secret-scanner.yml",
"type": "missing_workflow",
"file": "secret-scanner.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in agda.yml",
"type": "unknown",
"file": "agda.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in agda.yml",
"type": "unknown",
"file": "agda.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in governance.yml",
"type": "unknown",
"file": "governance.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in hypatia-scan.yml",
"type": "unknown",
"file": "hypatia-scan.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in mirror.yml",
"type": "unknown",
"file": "mirror.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard.yml",
"type": "unknown",
"file": "scorecard.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/tutorial/epistemic_erasure/EpistemicErasure.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echo-types/echo-types/tutorial/region_exit_audit/RegionExitAudit.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
2 tasks
hyperpolymath added a commit
that referenced
this pull request
May 28, 2026
…lice 3 remains `rank-pow-dominated-by-head-Ω` (Slice 2-bplus) is in fact landed at `Ordinal.Buchholz.RankPowDomination` via PRs #133+#134 2026-05-27, not "remaining" as the doc claimed in three places. Updates: * Per-constructor verdict row for `<ᵇ-+1` — verdict text now reflects that the WfCNF-carrier domination side is COMPLETE and only the headline Slice 3 discharge remains; signature of the headline pinned inline. * Score paragraph — replaces "1 in flight with abstraction + per-marker dominances + inversion lemmas landed (Slice 2-bplus remaining)" with "1 in flight with the domination lemma landed (Slice 3 discharge remaining)"; adds PR #124/#130/#131/#133+#134 stage references. * "What remains open" entry for `<ᵇ-+1` — updates from "Slice 2-bplus remaining only" to "Slice 3 headline remaining only"; notes the `NonBzero` premise turned out unnecessary; pins the headline signature. * Status note — replaces "3 constructors blocked" (stale; `<ᵇ⁺-ψα` and `<ᵇ-ψΩ≤` are both closed) with accurate "11/13 closed + 1 side-cond + 1 head-Ω-route with only Slice 3 remaining". * See-also — adds `RankPowDomination.agda` entry pointing at the domination lemma + the `additive-principal-ω-rank-pow-succ` closure + the `rank-y-bound` atomic-tail helper. No proof / no code change; doc-only sweep aligning the obstruction verdict with on-disk state. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit
that referenced
this pull request
May 28, 2026
…remains (#136) ## Summary Doc-only sweep. `docs/echo-types/buchholz-rank-obstruction.adoc` claimed in three places that "Slice 2-bplus" (the WfCNF-carrier domination `rank-pow-dominated-by-head-Ω`) was still remaining, but it landed via PRs #133+#134 2026-05-27 at `Ordinal.Buchholz.RankPowDomination`. Only Slice 3 (the headline `rank-mono-<ᵇ-+1-via-head-Ω` discharge) remains in the per-constructor matrix. Updates: - **Per-constructor verdict row for `<ᵇ-+1`** — verdict text now reflects WfCNF-carrier domination side is COMPLETE; pins the headline signature. - **Score paragraph** — replaces stale "Slice 2-bplus remaining" with "Slice 3 discharge remaining"; adds PR #124/#130/#131/#133+#134 stage references. - **"What remains open" entry for `<ᵇ-+1`** — updates to "Slice 3 headline remaining only"; notes the `NonBzero` premise turned out unnecessary (`rank-pow bzero = oz` is strictly below `ω-rank-pow-succ (fin 0) = ω^2`); pins the headline signature. - **Status note** — replaces stale "3 constructors blocked" (the count was from before `<ᵇ⁺-ψα` and `<ᵇ-ψΩ≤` closed) with accurate "11/13 closed + 1 side-cond + 1 head-Ω-route with only Slice 3 remaining". - **See-also** — adds `RankPowDomination.agda` entry pointing at the domination lemma + the `additive-principal-ω-rank-pow-succ` closure + the `rank-y-bound` atomic-tail helper. No proof / no code change; doc-only sweep aligning the obstruction verdict with on-disk state. ## Test plan - [x] No code touched — Smoke + All unaffected. - [x] Diff is single-file, docs only.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Six commits, all Lane 3 head-Ω route work + cross-doc reinforcement landing in one PR:
1.
docs(claude): session-arc entry for Slice 2 (commit0108705)Records the rung landing per CLAUDE.md §"Rung-consolidation policy" (PR #130, merge commit
bf9ee6e).2.
ordinal(buchholz): head-Ω inversion lemmas — option (b) (commit560f904)New module
Ordinal.Buchholz.HeadOmegaInversion:Structural recursion on
<ᵇ; no rank-mono dependency. Keeps the eventual Slice 2-bplus consumer independent of the still-openrank-pow-mono-≤ᵇ.3.
ordinal(buchholz): Slice 2-omega — ω branch resolved (commit07abc15)Replaces
ω-rank-pow-succ ω = olim (λ n → ω^(suc(suc n)))(equi-ordinal withω-rank-pow ω, unsound) witholim (λ n → ω-rank-pow ω ·ℕ n)denotingω^(ω+1). Per-marker dominance proved at the ω branch; unifiedω-rank-pow-<-succlemma added.4.
docs(claude): updated next-Claude plan (commit6cacc8d)Reflects (1) and (2) landing in the same session; only Slice 2-bplus remains.
5.
docs: cross-doc consistency sweep (commit1d99484)Reinforced the Slice 2 narrative across five wiki docs that had stale Slice 1-era wording:
buchholz-rank-obstruction.adoc,roadmap.adoc § Lane 3,EXPLAINME.adoc,CHANGELOG.md,MAP.adoc.6.
docs: deeper-sweep gaps in the bridge/plan ledgers (commitf6fb7ce)Two more artefacts flagged "no touch needed" on first pass actually did need touching:
docs/bridge-status.mdrow E3 CNF trichotomy + E4 pedagogical psi least-gap #4 (Buchholz / Veblen) was "BLOCKED — failure of the self-lift"; that blocker resolved 2026-05-26/27 viaRankAdm+RankLex. Now reports "PARTIAL (11/13; 1 in flight)".docs/bridge-status.mdgains row E5: make ν operational and add Buchholz example/smoke modules #6 for the decoration bridge as a conceptual (not cross-repo) entry, fitting the doc's stated scope.docs/bridges/buchholz-plan.adocis the original phased spec; many of its "PLANNED" tags are now dated. Added a CAUTION banner pointing to the live tracker + roadmap + CLAUDE.md ledger.What's now closed vs open
ω-rank-pow-succdefinition (both branches)∀ μ → ω-rank-pow μ <′ ω-rank-pow-succ μrank-powfactoring throughhead-Ωrank-pow-dominated-by-head-Ω(Slice 2-bplus)Invariants held
--safe --without-Kthroughout.scripts/kernel-guard.sh: PASS (funext-free certificate + classification-drift lint both clean).EchoIntegration.agda/EchoChoreo.agda/EchoGraded.agda/ existingEcho*Bridge.agda).agdanot available in this container; Agda proofs verified by inspection. The ω-branch dominance mirrorsBrouwer/OmegaPow.ω^-strict-mono-sucat line 204; the head-Ω inversion proofs are direct structural recursions on<ᵇ. CI is authoritative.Test plan
Agdajob typechecks clean under--safe --without-K.https://claude.ai/code/session_013nLEeKZXpvHnrDZMgRm19S