From ae94a73fbdcf2e426273ea480b8f6f3aebd788b2 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Thu, 28 May 2026 08:45:53 +0100
Subject: [PATCH 1/3] =?UTF-8?q?docs(buchholz):=20update=20obstruction=20do?=
 =?UTF-8?q?c=20=E2=80=94=20Slice=202-bplus=20landed,=20only=20Slice=203=20?=
 =?UTF-8?q?remains?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`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>
---
 .../echo-types/buchholz-rank-obstruction.adoc | 79 ++++++++++++-------
 1 file changed, 49 insertions(+), 30 deletions(-)

diff --git a/docs/echo-types/buchholz-rank-obstruction.adoc b/docs/echo-types/buchholz-rank-obstruction.adoc
index 21acd25..164156e 100644
--- a/docs/echo-types/buchholz-rank-obstruction.adoc
+++ b/docs/echo-types/buchholz-rank-obstruction.adoc
@@ -305,22 +305,23 @@ constructors discharge by additive-principal closure.
 | `<ᵇ-+ψ`    | ✓ closed  | Same as `<ᵇ-+Ω` since `rank-pow (bpsi ν _) = ω-rank-pow ν`.
 | `<ᵇ⁺-ψα`   | ✓ closed (Lane 3, 2026-05-26) | `rank-adm (bpsi ν α) = ω-rank-pow ν ⊕ rank-pow α`; `⊕-mono-<-right` closes the shared-Ω-index lex case from `rank-pow α <′ rank-pow β` (which the existing `_<ᵇ⁰_` umbrella discharges).  Primitive `rank-mono-<ᵇ⁺-ψα-from-pow` in `Ordinal.Buchholz.RankAdm`.
 | `<ᵇ-ψΩ≤`   | ✓ closed (Lane 3 follow-on, 2026-05-27) | Lex-pair rank `rank-lex : BT → RankLex` in `Ordinal.Buchholz.RankLex`, with `rank-lex (bOmega ν) = mkLex (ω-rank-pow ν) (ω-rank-pow ν)` and `rank-lex (bpsi ν α) = mkLex (ω-rank-pow ν) (rank-pow α)`.  Both sub-cases close via `rank-mono-<ᵇ-ψΩ≤-lex`: ν<μ via `<lex-first` + `ω-rank-pow-mono`; ν=μ via `<lex-second` + the admissibility bound `rank-pow α <′ ω-rank-pow ν`.  The "structurally impossible under any rank shape with `ω-rank-pow ν ≤ rank-adm (bpsi ν α)`" verdict from `RankAdm.agda` was scoped to *scalar* ranks; option (A) lex-pair sidesteps it cleanly.
-| `<ᵇ-+1`    | ⏳ joint-bplus, head-Ω route in flight | The dominator-function unblock (option A from `RankPow.agda`'s preamble) is now partially landed: `head-Ω : BT → OmegaIndex` (Slice 1, `Ordinal.Buchholz.HeadOmega`), `ω-rank-pow-succ` + per-marker strict dominance at *both* branches (Slice 2 + Slice 2-omega, `Ordinal.Buchholz.RankPow`), the unified `ω-rank-pow-<-succ`, and the option-(b) head-Ω inversion lemmas `head-Ω-inv-{bOmega,bpsi}` (`Ordinal.Buchholz.HeadOmegaInversion`).  Remaining: the WfCNF-carrier structural recursion `rank-pow-dominated-by-head-Ω` (Slice 2-bplus) + the headline `rank-mono-<ᵇ-+1-via-head-Ω` discharge.  No further rank-mono dependency in the bplus case — option (b) bought independence from the still-open `rank-pow-mono-≤ᵇ`.
+| `<ᵇ-+1`    | ⏳ joint-bplus, headline `rank-mono-<ᵇ-+1-via-head-Ω` remaining (Slice 3) | The dominator-function unblock (option A from `RankPow.agda`'s preamble) is now COMPLETE on the WfCNF-carrier domination side: `head-Ω : BT → OmegaIndex` (Slice 1, `Ordinal.Buchholz.HeadOmega`), `ω-rank-pow-succ` + per-marker strict dominance at *both* branches (Slice 2 + Slice 2-omega, `Ordinal.Buchholz.RankPow`), the unified `ω-rank-pow-<-succ`, the option-(b) head-Ω inversion lemmas `head-Ω-inv-{bOmega,bpsi}` (`Ordinal.Buchholz.HeadOmegaInversion`), AND the WfCNF-carrier structural recursion `rank-pow-dominated-by-head-Ω : ∀ {t} → WfCNF t → rank-pow t <′ ω-rank-pow-succ (head-Ω t)` (Slice 2-bplus, `Ordinal.Buchholz.RankPowDomination` — landed via PRs #133+#134 2026-05-27).  Remaining: the headline `rank-mono-<ᵇ-+1-via-head-Ω` discharge (Slice 3), consuming the domination lemma plus a head-Ω lower-bound + strict-jump bridge.  No further rank-mono dependency anywhere in the chain — option (b) bought independence from the still-open `rank-pow-mono-≤ᵇ`.
 | `<ᵇ-0-+`   | ✓ closed* | `rank-pow bzero = oz`, and `rank-pow (bplus x y) ≥′ oz` strictly when *either* `x` or `y` is non-`bzero` and the term is WfCNF.  The degenerate `bplus bzero bzero` is excluded by WfCNF (atomic-right ≤ left forces both `bzero` and then the sum reduces to a `bzero`-shaped equivalent that doesn't pattern-match as a `bplus` under CNF normalisation — covered as a side-condition).
 |===
 
 *Score: 11/13 constructors closed (9 under the original `rank-pow`
 umbrella + 1 under the `rank-adm` slice + 1 under the `rank-lex`
-slice); 1 in flight under the head-Ω route with abstraction +
-per-marker dominances + inversion lemmas landed (`<ᵇ-+1` joint-bplus,
-Slice 2-bplus remaining); 1 closed conditionally with documented side
-condition. The Lane-3 active-push slice on 2026-05-26 closed `<ᵇ⁺-ψα`
-(rank-adm) and re-classified `<ᵇ-ψΩ≤` to "encoding mismatch"; the
-Lane-3 follow-on slice on 2026-05-27 closed `<ᵇ-ψΩ≤` via option (A)
-(lex pair); the head-Ω route landed in stages across 2026-05-27 (Slice 1,
-session-night PR #130 closing Slice 2, PR #131 closing Slice 2-omega +
-option (b) inversion).  Only `<ᵇ-+1` joint-bplus remains in the
-per-constructor matrix.*
+slice); 1 in flight under the head-Ω route with the WfCNF-carrier
+domination lemma `rank-pow-dominated-by-head-Ω` landed (the headline
+`rank-mono-<ᵇ-+1-via-head-Ω` Slice 3 discharge remaining); 1 closed
+conditionally with documented side condition.  The Lane-3 active-push
+slice on 2026-05-26 closed `<ᵇ⁺-ψα` (rank-adm) and re-classified
+`<ᵇ-ψΩ≤` to "encoding mismatch"; the Lane-3 follow-on slice on
+2026-05-27 closed `<ᵇ-ψΩ≤` via option (A) (lex pair); the head-Ω
+route landed in stages across 2026-05-27 (Slice 1 PR #124, Slice 2
+PR #130, Slice 2-omega + option (b) inversion PR #131, Slice 2-bplus
+domination PRs #133+#134).  Only the headline `rank-mono-<ᵇ-+1-via-head-Ω`
+discharge (Slice 3) remains in the per-constructor matrix.*
 
 === What remains open
 
@@ -335,22 +336,29 @@ per-constructor matrix.*
   case ν=μ no longer needs the additive-principal closure; the
   admissibility bound `rank-pow α <′ ω-rank-pow ν` discharges it
   directly on the second component of the lex pair.
-* *`<ᵇ-+1` joint-bplus* — *Slice 2-bplus remaining only.*  The
+* *`<ᵇ-+1` joint-bplus* — *Slice 3 headline remaining only.*  The
   head-Ω route's prerequisite slices are all landed: `head-Ω`
   (Slice 1), `ω-rank-pow-succ` + per-marker strict dominance at
-  both branches (Slice 2 + Slice 2-omega), and the option-(b)
-  head-Ω inversion lemmas (preserving the dependency-graph
-  invariant that the eventual `rank-pow-dominated-by-head-Ω`
-  doesn't depend on the still-open `rank-pow-mono-≤ᵇ`).
-  Slice 2-bplus proves the WfCNF-carrier structural recursion
-  `rank-pow-dominated-by-head-Ω : (t : BT) → NonBzero t → WfCNF t
-  → rank-pow t <′ ω-rank-pow-succ (head-Ω t)` and the headline
-  `rank-mono-<ᵇ-+1-via-head-Ω`.  The `Slice 2-omega` historical
-  hazard (the originally-proposed `ω-rank-pow-succ ω` shape
-  `olim (λ n → ω^(suc(suc n)))` is equi-ordinal with `ω-rank-pow ω`,
-  so doesn't strictly dominate) is resolved by the revised shape
-  `olim (λ n → ω-rank-pow ω ·ℕ n)` (denoting `ω^(ω+1)`) — see
-  `RankPow.agda`'s "History note" comment block for the full record.
+  both branches (Slice 2 + Slice 2-omega), the option-(b) head-Ω
+  inversion lemmas (preserving the dependency-graph invariant
+  that `rank-pow-dominated-by-head-Ω` doesn't depend on the
+  still-open `rank-pow-mono-≤ᵇ`), AND the WfCNF-carrier structural
+  recursion `rank-pow-dominated-by-head-Ω : ∀ {t} → WfCNF t →
+  rank-pow t <′ ω-rank-pow-succ (head-Ω t)` itself
+  (`Ordinal.Buchholz.RankPowDomination`, Slice 2-bplus, PRs
+  #133+#134 2026-05-27 — the `NonBzero` premise turned out
+  unnecessary: `rank-pow bzero = oz` is strictly below
+  `ω-rank-pow-succ (fin 0) = ω^2` via `ω^_-pos 2`).  Slice 3
+  consumes the domination lemma plus a head-Ω lower-bound
+  + strict-jump bridge to derive the headline
+  `rank-mono-<ᵇ-+1-via-head-Ω : ∀ {x₁ x₂ y₁ y₂} → WfCNF (bplus x₁ x₂)
+  → WfCNF (bplus y₁ y₂) → x₁ <ᵇ y₁ → rank-pow (bplus x₁ x₂) <′
+  rank-pow (bplus y₁ y₂)`.  The `Slice 2-omega` historical hazard
+  (the originally-proposed `ω-rank-pow-succ ω` shape `olim (λ n
+  → ω^(suc(suc n)))` is equi-ordinal with `ω-rank-pow ω`, so doesn't
+  strictly dominate) is resolved by the revised shape `olim (λ n →
+  ω-rank-pow ω ·ℕ n)` (denoting `ω^(ω+1)`) — see `RankPow.agda`'s
+  "History note" comment block for the full record.
 * *Mutual recursion for `rank-pow-mono-<ᵇ⁻`*.  The case-specific
   primitives above are individually proven, but the umbrella theorem
   `x <ᵇ⁻ y → rank-pow x <′ rank-pow y` needs a mutual `<ᵇ` / `≤ᵇ`
@@ -365,11 +373,17 @@ per-constructor matrix.*
 The "rank-embedding route is closed" framing from this document's
 introduction is *narrowed*: it remains true for the unrestricted
 `_<ᵇ_`, but the WfCNF restriction `_<ᵇ⁻_` together with the limit-
-shaped rank-pow discharges 9 of the 13 constructor cases.  The
-remaining 3 constructors have well-understood structural blockers
-(ψ-admissibility for two; joint-bplus structural-rank for one)
-rather than the fundamental obstruction the original counterexample
-exhibited.
+shaped rank-pow discharges 11 of the 13 constructor cases (9 under
+the original `rank-pow` umbrella + `<ᵇ⁺-ψα` via `rank-adm` + `<ᵇ-ψΩ≤`
+via `rank-lex`) plus 1 under documented side-condition (`<ᵇ-0-+`).
+The remaining `<ᵇ-+1` joint-bplus case has its head-Ω domination
+prerequisites all landed (Slice 1 + Slice 2 + Slice 2-omega + option-(b)
+inversion + Slice 2-bplus); only the headline Slice 3 discharge
+`rank-mono-<ᵇ-+1-via-head-Ω` remains.  The original "fundamental
+obstruction" verdict was scoped to unrestricted `_<ᵇ_` with scalar
+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).
 
 == See also
 
@@ -383,6 +397,11 @@ exhibited.
 * `proofs/agda/Ordinal/Buchholz/RankPow.agda` — Slice 2 + Slice 2-omega;
   `ω-rank-pow-succ` + per-marker strict dominance at both branches +
   the unified `ω-rank-pow-<-succ`.
+* `proofs/agda/Ordinal/Buchholz/RankPowDomination.agda` — Slice 2-bplus;
+  the WfCNF-carrier structural recursion `rank-pow-dominated-by-head-Ω`
+  + the `additive-principal-ω-rank-pow-succ` closure + the `rank-y-bound`
+  atomic-tail helper.  Consumed by the (still open) Slice 3 headline
+  `rank-mono-<ᵇ-+1-via-head-Ω`.
 * `proofs/agda/Ordinal/Buchholz/Order.agda` — the K-free core; the
   13 constructors that pin the syntactic order.
 * `proofs/agda/Ordinal/Buchholz/WellFounded.agda` — the direct

From d3987c0e26c6f5d1f8cd5834aee1690e0860c70f Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Thu, 28 May 2026 09:00:52 +0100
Subject: [PATCH 2/3] docs(kernel-note): classify 18 Echo* modules to unblock
 kernel-guard CI
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

PR #136 (session/doc-sweep-slice-2bplus-landed) introduced or touched
18 Echo*.agda modules without entries in echo-kernel-note.adoc, so
scripts/kernel-guard.sh Check B (classification-drift lint) failed
with exit 1 before Agda was even installed.

Classifications (by in-repo import set):
- EchoTotalCompletion: Tier 1 (only Echo + stdlib) — A ↔ Σ Echo
  encode/decode pair anchoring the F5 canonical-identity cohort
- 17 others: Tier 2 (multi-hop) — split between the F5 canonical-
  identity / OFS cohort and the application/extension modules.
  F5 cohort: EchoOrthogonalFactorizationSystem, EchoImageFactorization,
  EchoNoSectionGeneric, EchoLossTaxonomy, EchoResidueTaxonomy,
  EchoDecorationStructure, EchoObservationalEquivalence, EchoOFSUnivF5,
  EchoOFSUnivF5Diag, EchoOFSUnivF5Iso, EchoCanonicalIdentitySuite.
  Application/extension: EchoEntropy, EchoLLEncoding, EchoProvenance,
  EchoSecurity, EchoProbabilisticSupport, EchoDifferential.

Kernel-guard check A (funext-free certificate) continues to pass.
Both checks PASS locally after this change.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 docs/echo-types/echo-kernel-note.adoc | 31 ++++++++++++++++++++++++---
 1 file changed, 28 insertions(+), 3 deletions(-)

diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc
index bb8d11c..8051ef6 100644
--- a/docs/echo-types/echo-kernel-note.adoc
+++ b/docs/echo-types/echo-kernel-note.adoc
@@ -64,11 +64,14 @@ kernel** — the boundary is real and lives outside this core.
 | `EchoCharacteristic`, `EchoChoreo`, `EchoDecidable`,
   `EchoFiberBridge`, `EchoFiberCount`, `EchoFiberTriangulation`,
   `EchoIndexed`, `EchoRelational`, `EchoTruncation`,
-  `EchoJanusBridge`, `EchoTropical`, `EchoSeparating`
+  `EchoJanusBridge`, `EchoTropical`, `EchoSeparating`,
+  `EchoTotalCompletion`
 | One hop off the kernel. `EchoJanusBridge`/`EchoTropical` are
   *Directions* (see MAP). `EchoFiberTriangulation` is the external
   stdlib triangulation hardening item. `EchoSeparating` carries
-  retracted prose framing (below).
+  retracted prose framing (below). `EchoTotalCompletion` is the
+  `A ↔ Σ Echo` encode/decode pair anchoring the F5 canonical-
+  identity cohort (Tier 2 below).
 
 | *Derived — Tier 2* +
 (depend on Tier-1 `Echo*`)
@@ -81,7 +84,14 @@ kernel** — the boundary is real and lives outside this core.
   `EchoExampleAbsInt`, `EchoExampleParser`, `EchoExampleProvenance`,
   `EchoExampleSignAnalysis`, `EchoExampleTruncation`,
   `EchoSearchExample`, `EchoThermodynamicsArbitrary`,
-  `EchoThermoCollapseImpossible`, `EchoAbstractionBarrier`
+  `EchoThermoCollapseImpossible`, `EchoAbstractionBarrier`,
+  `EchoOrthogonalFactorizationSystem`, `EchoImageFactorization`,
+  `EchoNoSectionGeneric`, `EchoLossTaxonomy`, `EchoResidueTaxonomy`,
+  `EchoDecorationStructure`, `EchoObservationalEquivalence`,
+  `EchoOFSUnivF5`, `EchoOFSUnivF5Diag`, `EchoOFSUnivF5Iso`,
+  `EchoCanonicalIdentitySuite`, `EchoDifferential`, `EchoEntropy`,
+  `EchoLLEncoding`, `EchoProbabilisticSupport`, `EchoProvenance`,
+  `EchoSecurity`
 | Multi-hop. `EchoThermodynamics` reaches the kernel via
   `EchoFiberCount` (no direct `Echo` import);
   `EchoThermodynamicsFinite` is its Bishop-finite transport layer.
@@ -93,6 +103,21 @@ kernel** — the boundary is real and lives outside this core.
   `EchoLinear`, landed 2026-05-26 via PR #119.  `EchoExample*` are
   derived domain
   applications.
+  *F5 canonical-identity / OFS cohort* (added via Slice-2b+ doc
+  sweep): `EchoOrthogonalFactorizationSystem` is the
+  (encode-mono / decode-epi) factorisation keystone;
+  `EchoImageFactorization` carries the image side;
+  `EchoOFSUnivF5`/`Diag`/`Iso` are the F5 universal-property work
+  routing composition through totality;
+  `EchoCanonicalIdentitySuite` re-exports the cohort as a single
+  entry point; `EchoNoSectionGeneric` / `EchoLossTaxonomy` /
+  `EchoResidueTaxonomy` / `EchoDecorationStructure` /
+  `EchoObservationalEquivalence` are the no-section / loss /
+  residue / decoration / observational classifications.
+  *Application/extension modules* (also added via the same sweep):
+  `EchoEntropy`, `EchoLLEncoding`, `EchoProvenance`, `EchoSecurity`,
+  `EchoProbabilisticSupport`, `EchoDifferential` are derived domain
+  applications mapped under their own headings in MAP.adoc.
 
 | *Earn-back gate modules* +
 (derived / scoped; not kernel)

From 41ff391aed592b0e975ad4d51fb6c6fa3d881851 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Thu, 28 May 2026 09:10:57 +0100
Subject: [PATCH 3/3] =?UTF-8?q?ci(agda):=20drop=20N5Falsifier=20xfail=20ga?=
 =?UTF-8?q?te=20=E2=80=94=20module=20now=20typechecks?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The "Expected-failure gate (N5Falsifier is known-broken)" step was
asserting that proofs/agda/characteristic/N5Falsifier.agda fails the
typechecker (per the 2026-05-18 foundation audit). That hold no longer
holds: the module was resolved 2026-05-27 by pinning the implicit r /
grade at the four applyRole / applyGrade call sites, and is already
imported by characteristic/All.agda (line 33). The xfail step's own
self-disclosed instructions fired in the previous CI run, telling us to
"register it in characteristic/All.agda and remove this xfail gate".

In-source bookkeeping is already complete on this branch:
- N5Falsifier.agda banner rewritten as "HISTORICAL BROKEN BANNER
  (resolved 2026-05-27)" with the resolution narrative.
- characteristic/All.agda has the import (line 33).
- The previous CI run confirmed N5Falsifier typechecks (the xfail
  gate failed precisely because it succeeded) and that
  characteristic/All.agda typechecks WITH the import.

Net diff: -17 lines from .github/workflows/agda.yml. No Agda code
changed by this commit.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 .github/workflows/agda.yml | 17 -----------------
 1 file changed, 17 deletions(-)

diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml
index 12947a2..2381117 100644
--- a/.github/workflows/agda.yml
+++ b/.github/workflows/agda.yml
@@ -142,23 +142,6 @@ jobs:
       - name: Typecheck examples lane (Gate #3 canonical examples)
         run: agda -i proofs/agda proofs/agda/examples/All.agda
 
-      # Disclosed known-broken module (foundation audit 2026-05-18):
-      # characteristic/N5Falsifier.agda has unsolved metas and is NOT
-      # in any green closure. This gate ASSERTS it still fails, so the
-      # hole stays monitored: if it ever typechecks, this step fails
-      # loudly and tells us to register it + drop the xfail.
-      - name: Expected-failure gate (N5Falsifier is known-broken)
-        run: |
-          if agda -i proofs/agda proofs/agda/characteristic/N5Falsifier.agda \
-               > /tmp/n5.log 2>&1; then
-            echo "::error::N5Falsifier now typechecks — register it in"
-            echo "::error::characteristic/All.agda and remove this xfail gate."
-            exit 1
-          else
-            echo "N5Falsifier fails as expected (disclosed in its banner"
-            echo "and the proof-debt ledger). Hole monitored, not hidden."
-          fi
-
   cold-check:
     # Belt-and-braces: NO interface cache, --ignore-interfaces cold
     # build. A green here cannot be a stale-.agdai artefact (matters