ordinal: ω-power infrastructure + 9-of-13 rank-mono primitives (#87)

Five-slice ω-power infrastructure for the Buchholz `_<ᵇ_`
rank-monotonicity unblock.  Closes 9 of 13 constructor cases under
the WfCNF restriction `_<ᵇ⁻_`; 3 cases remain open under documented
structural blockers (ψ-admissibility, joint-bplus).

See `docs/echo-types/buchholz-rank-obstruction.adoc` for the full
analysis (narrowed verdict updated this session).

## Slices

| Slice | Module(s) | What lands |
|-------|-----------|------------|
| 1 | `Ordinal.Brouwer.OmegaPow` | `_·ℕ_`, `ω^_`, basic identifications,
`ω^-strict-mono-suc`, `ω^-step` |
| 2 | `Ordinal.Brouwer.Phase13`, OmegaPow | `⊕-mono-≤-left`,
`·ℕ-mono-≤-left`, `ω^-mono-≤`, `ω^-strict-mono` |
| 3 | Phase13, OmegaPow | `⊕-assoc-≤` / `⊕-assoc-≥` (both funext-free
`≤′` directions), `·ℕ-add-≤`, **`additive-principal`** at `ω^(suc n)` |
| 4 | `Ordinal.Buchholz.RankPow` | `ω-rank-pow` (limit-shaped),
`rank-pow`, `ω-rank-pow-{pos,mono}`, `rank-pow-bplus-right-mono`,
`rank-pow-via-left`, `additive-principal-ω-rank-pow`,
`rank-pow-bplus-into-ω-rank-pow` |
| 5 | RankPow | 9 per-constructor rank-mono primitives
(relation-agnostic): `rank-mono-<ᵇ-0-Ω`, `rank-mono-<ᵇ-0-ψ`,
`rank-mono-<ᵇ-ΩΩ`, `rank-mono-<ᵇ-Ωψ`, `rank-mono-<ᵇ-ψΩ`,
`rank-mono-<ᵇ-Ω+`, `rank-mono-<ᵇ-ψ+`, `rank-mono-<ᵇ-+Ω`,
`rank-mono-<ᵇ-+ψ` |

## Reusable design

The Slice-5 primitives are stated purely in terms of rank inequalities,
not the driving relation.  Consumers — whether `_<ᵇ⁻_` (this track) or
`_<ᵇʳᶠ_` (parallel-session track) — pattern-match on their relation's
constructor and apply the matching primitive.  No relation-specific
recursion lives in RankPow.

## Open under documented blockers

- `<ᵇ-ψα`, `<ᵇ-ψΩ≤` — provisional `rank-pow (bpsi ν _) = ω-rank-pow ν`
  doesn't discriminate on α.  Closed by ψ-admissibility predicate
  (`WellFormedAdmissible.agda`, ~80 lines).
- `<ᵇ-+1` — `rank-pow (bplus z₁ z₂)` is not additive principal in
  general.  Needs either a coarser dominator function or richer rank.
- `rank-pow-mono-<ᵇ⁻` umbrella — gated on `<ᵇ-+1`.

## Build invariants

- `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit
  0 under `--safe --without-K`.
- No postulates, no escape pragmas, no funext.
- Every headline pinned in `Smoke.agda`.

## Commits (20)

Branched from `8c9ddcb`.  Includes prior session work on the WfCNF
predicate (`Ordinal.Buchholz.WellFormedCNF`) and the `_<ᵇ⁻_`
subrelation (`Ordinal.Buchholz.OrderRestricted`); the path-1
foundation those modules established is now operational.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

CLAUDE.md

@@ -193,7 +193,7 @@ work to `main` and refresh all documentation:
 
 ## Current rung state (2026-05-20)
 
-### Session arc 2026-05-20 (read this first)
+### Session arc 2026-05-20 daytime (theory closure waves 1 + 2 + 3)
 
 *Where we started today (commit `888dee0`, post-#73):* the establishment
 track was complete A–D + Pillar E paper drafting in progress. The
@@ -342,7 +342,126 @@ EchoAccess existential carriers (`decisions/echo-access-trivial-carrier.adoc`);
 the Pillar A–D internal programme (complete since 2026-05-17);
 any §"Theory work" item — the section is closed.
 
-### Session arc 2026-05-17 (read this first)
+### Session arc 2026-05-20 evening — ω-power rank-mono unblock (read this first)
+
+*Where we started today (commit `8c9ddcb` on `harden/ci-flake-pin-2026-05-18`):*
+the ordinal track had the WfCNF predicate plus the `_<ᵇ⁻_` subrelation
+foundations from the earlier session.  The rank-embedding route to
+unbudgeted `wf-<ᵇʳᶠ_` was framed as "closed impossible" in
+`docs/echo-types/buchholz-rank-obstruction.adoc` — the
+`<ᵇ-+Ω <ᵇ-0-Ω : bplus bzero (bOmega (fin 1)) <ᵇ bOmega (fin 0)`
+counterexample forced a rank inversion under additive Brouwer rank
+with `nat-to-ord` successor-stack `ω-rank`.  4 of 13 constructors
+admitted rank-mono via `RankPartial.agda`; 9 were structurally
+walled.
+
+*Where we ended (PR #87, branch `session-2026-05-20/buchholz-budgeted-plus`,
+23 commits ahead of `8c9ddcb`):* the "closed impossible" verdict is
+**narrowed** — under the WfCNF restriction `_<ᵇ⁻_` together with a
+*limit-shaped* ω-power rank, **10 of 13 constructors close** via
+relation-agnostic compositional primitives.  3 cases remain open
+under documented structural blockers (ψ-admissibility, joint-bplus).
+
+Eight slices landed in order, each with `agda proofs/agda/All.agda`
+and `agda proofs/agda/Smoke.agda` exiting 0 under `--safe --without-K`,
+zero postulates, zero escape pragmas, no funext:
+
+1. **Slice 1** — `Ordinal.Brouwer.OmegaPow.agda` lands `_·ℕ_`, `ω^_`,
+   basic identifications (`ω^0≡one`, `one·ℕ≡nat-to-ord`,
+   `·ℕ-zero`, `·ℕ-suc`), positivity `ω^_-pos`, one-step strict-mono
+   `ω^-strict-mono-suc`, weakening `ω^-step`.
+2. **Slice 2** — left-monotonicity of `_⊕_` (`⊕-mono-≤-left` in
+   `Phase13.agda`) + `·ℕ-mono-≤-left`, `ω^-mono-≤`, `ω^-strict-mono`
+   (general gap).  Block comment in Phase13 documenting why strict
+   left-mono of `_⊕_` is *not* a theorem (the `α + ω = β + ω`
+   counterexample).
+3. **Slice 3** — `⊕-assoc-≤` / `⊕-assoc-≥` (both funext-free `≤′`
+   directions in Phase13), `·ℕ-add-≤` bridge, and the keystone
+   **`additive-principal`** at `ω^(suc n)`.  The closure-under-addition
+   property that makes ω-powers the right rank target for plus-side
+   `_<ᵇ_` constructors.
+4. **Slice 4** — `Ordinal.Buchholz.RankPow.agda`: limit-shaped
+   `ω-rank-pow : OmegaIndex → Ord` (`fin n ↦ ω^(suc n)`), `rank-pow :
+   BT → Ord` consuming it, plus reusable compositional primitives
+   (`rank-pow-bplus-right-mono`, `rank-pow-via-left`,
+   `rank-pow-bplus-into-ω-rank-pow`, `additive-principal-ω-rank-pow`).
+5. **Slice 5** — 9 per-constructor rank-mono primitives in RankPow:
+   `rank-mono-<ᵇ-0-Ω/0-ψ/ΩΩ/Ωψ/ψΩ/Ω+/ψ+/+Ω/+ψ`.  Each stated purely
+   in terms of rank inequalities (not the relation), so both `<ᵇ⁻`
+   and `<ᵇʳᶠ` consumers reuse them by pattern-matching on their own
+   relation's constructor.
+6. **Item 1** — `rank-mono-<ᵇ-+1-via-target` parametric in the
+   target's additive-principal witness; `rank-mono-<ᵇ-+1-Ω-target`
+   and `rank-mono-<ᵇ-+1-ψ-target` convenience wrappers.  Closes
+   `<ᵇ-+1` for atomic targets; bplus-target sub-case explicitly
+   deferred.
+7. **Item 2** — `Ordinal.Buchholz.WellFormedAdmissible.agda` lands
+   `WfAdm : BT → Set` strengthening WfCNF with `rank-pow α <′
+   ω-rank-pow ν` on each `bpsi ν α`.  Carrier only; rank refinement
+   for `<ᵇ-ψα` / `<ᵇ-ψΩ≤` discharge deferred (cross-case interaction
+   with `<ᵇ-+ψ` documented in the module preamble).
+8. **Item 3** — `Ordinal.Buchholz.RankMonoUmbrella.agda`: the
+   rank-soundness-ready relation `_<ᵇ⁰_` with 10 constructors
+   (tail-bounds baked in via `_≤ᵇ⁰_`) plus the umbrella theorem
+   **`rank-pow-mono-<ᵇ⁰ : x <ᵇ⁰ y → rank-pow x <′ rank-pow y`**
+   proved by direct structural recursion over the 10 cases.
+
+*Closure-doc update*: `docs/echo-types/buchholz-rank-obstruction.adoc`
+gains a "Slices 1–5 of the ω-power unblock" section with an updated
+per-constructor verdict table (10 closed / 3 open).  The "rank-
+embedding route is closed" framing is narrowed: closed for
+unrestricted `_<ᵇ_`, opens up under the WfCNF restriction with
+limit-shaped rank.
+
+**Open work on this track (documented blockers):**
+
+* `<ᵇ-ψα`, `<ᵇ-ψΩ≤` — provisional `rank-pow (bpsi ν _) = ω-rank-pow ν`
+  doesn't discriminate on α.  Closed by ψ-admissibility predicate
+  (carrier landed in Item 2); the rank refinement is a separate
+  slice that needs to resolve the `<ᵇ-+ψ` cross-case.
+* `<ᵇ-+1` joint-bplus — `rank-pow (bplus z₁ z₂)` is not additive
+  principal in general.  Needs a coarser dominator function (e.g.,
+  `leading-Ω-index : BT → OmegaIndex` returning the leftmost-deepest
+  Ω-marker) or a richer rank shape.
+* `rank-pow-mono-<ᵇ⁻` (full umbrella over `_<ᵇ⁻_` — gated on the
+  above two).  The 10-of-13 `_<ᵇ⁰_` umbrella is the working closure;
+  consumers needing the full `_<ᵇ⁻_` form bridge through the
+  3-cases-open gap.
+
+Build invariant held every slice: `All.agda` + `Smoke.agda` exit 0
+under `--safe --without-K`, zero postulates, zero escape pragmas, no
+funext.  All headlines pinned in `Smoke.agda` (or
+`Ordinal/Buchholz/Smoke.agda` for the Buchholz-layer modules).
+
+**Reusable design constraint**: Per a parallel-session note on
+`_<ᵇʳᶠ_`, the rank-mono primitives are stated *relation-agnostically*
+(rank-input, rank-output, no `<ᵇ` constructor patterns).  Both the
+`_<ᵇ⁻_` consumer (this track) and the `_<ᵇʳᶠ_` consumer (parallel
+session's wf-`<ᵇʳᶠ` milestone) can pattern-match on their own
+relation's constructor and apply the matching primitive.
+
+*Plan for the next Claude:* PR #87 is the deliverable.  Closure
+work continues in three follow-ons, prioritised:
+
+1. **ψ-admissibility rank refinement** (closes `<ᵇ-ψα`, `<ᵇ-ψΩ≤`,
+   2 of 3 open cases).  Define `rank-adm : BT → Ord` using
+   `ω-rank-pow ν ⊕ rank-pow α` for ψ under WfAdm.  Cross-case fix
+   for `<ᵇ-+ψ`: under admissibility, source-rank is bounded by
+   `ω-rank-pow ν` (the structural admissibility-source-bound lemma).
+2. **Leading-Ω-index domination** (closes `<ᵇ-+1` general).  Define
+   `head-Ω : BT → OmegaIndex` returning the leftmost-deepest Ω
+   marker.  Prove `rank-pow t <′ ω-rank-pow-succ (head-Ω t)` for
+   non-bzero WfCNF terms.  Then `<ᵇ-+1` discharges via head-Ω
+   inversion + additive-principal at the head-Ω's successor.
+3. **Full `rank-pow-mono-<ᵇ⁻` umbrella** — composition of 1+2
+   with the existing 10-constructor `_<ᵇ⁰_` umbrella.
+
+DO NOT reopen: the closed 10 constructors (their primitives are
+correct under WfCNF); the unbudgeted `_<ᵇʳᶠ_` rank route per
+`RankBrouwer.agda` preamble (genuinely impossible for unrestricted
+`_<ᵇ_`).  The umbrella works on `_<ᵇ⁰_`, not on `_<ᵇ_` directly.
+
+### Session arc 2026-05-17 (legacy — read second)
 
 *Where we started today (commit `8a2b908`):* the establishment
 track was a plan plus scaffolds — Pillar A landed; Pillars B–D were

docs/adjacency/README.adoc

@@ -180,14 +180,126 @@ this directory is the intended structure.
 | File | Neighbour
 
 | `quotients.adoc`            | Quotient types / setoid quotients
+| `setoid-quotients.adoc`     | Setoid quotients (extrinsic, named-relation variant)
 | `galois-connections.adoc`   | Galois connections / abstract interpretation
 | `refinement-types.adoc`     | Refinement types (Σ-relevant and propositional variants)
 | `information-flow.adoc`     | Information-flow non-interference (Goguen-Meseguer lineage)
 | `provenance.adoc`           | Provenance / data lineage
+| `provenance-semirings.adoc` | K-provenance (Green-Karvounarakis-Tannen semirings)
 | `modal-type-theories.adoc`  | QTT, Reed-Pfenning modal calculi, adjoint modalities
 | `hott-fibers.adoc`          | HoTT homotopy fibers (cubical and Book HoTT)
+| `cubical-systems.adoc`      | Cubical Agda, RedPRL, redtt, cooltt
+| `lenses-and-optics.adoc`    | Lenses, prisms, profunctor optics
+| `INSERTION_NOTE.adoc`       | _Meta_: doc-surgery instructions for `gate-1-distinct-phenomenon.adoc`
+| `README.adoc`               | _Meta_: this file (index + argument families + axis-coverage matrix)
 |===
 
+== Axis coverage matrix (Gate 1 refresh 2026-05-20)
+
+Cross-reference of each adjacency note against the 8 taxonomy axes
+defined in `docs/echo-types/taxonomy.md`. Refreshed 2026-05-20 — most
+notes predate axis 8 (added with the `EchoDecidable`/`EchoFiberCount`
+landings) and therefore do not currently engage it; the open ○
+markings below flag where axis-8 implications exist but are not
+formally argued.
+
+Legend: ● primary axis (load-bearing in the note's distinctness
+claim); ○ axis-8 implication exists but is open / post-dates the
+note; — axis not engaged.
+
+[cols="3,^1,^1,^1,^1,^1,^1,^1,^1", options="header"]
+|===
+| Note
+| 1 Ext/Int
+| 2 Exact/Approx
+| 3 Loc/Glob
+| 4 Canon/Pres
+| 5 Comp/Non
+| 6 Stat/Dyn
+| 7 PR/PI
+| 8 IT/Comp
+
+| cubical-systems       | ● | — | — | ● | — | — | ● | —
+| galois-connections    | — | — | — | — | ● | — | ● | —
+| hott-fibers           | ● | — | — | — | — | — | ● | —
+| information-flow      | — | — | — | — | — | ● | ● | ○
+| lenses-and-optics     | — | — | — | ● | ● | — | ● | —
+| modal-type-theories   | — | — | — | — | ● | — | ● | ○
+| provenance            | — | — | — | — | — | — | ● | —
+| provenance-semirings  | — | — | — | — | ● | — | ● | ○
+| quotients             | ● | — | — | — | ● | — | ● | —
+| refinement-types      | — | — | — | — | — | — | ● | —
+| setoid-quotients      | ● | — | — | ● | — | — | ● | —
+|===
+
+=== Observations from the matrix
+
+* *Axis 7 (proof-relevant vs proof-irrelevant) is universal.* Every
+  one of the 11 substantive notes routes its distinctness through
+  axis 7. This is the "truncation argument" family's load-bearing
+  axis — the formal certificate is `echo-not-prop`.
+* *Axis 5 (compositional vs non-compositional) carries the 2-cell
+  argument.* Galois, quotients, modal-type-theories, lenses-and-
+  optics, provenance-semirings all engage axis 5 — these are the
+  notes whose distinctness arguments route through composition
+  structure (`EchoCategorical`, the per-decoration composition
+  sweep, the `Echo-comp-iso` pentagon).
+* *Axis 1 (extensional vs intensional)* shows up in four notes —
+  the ones contrasting echo's intensional-witness stance against
+  a neighbour's extensional / propositional collapse (cubical,
+  hott-fibers, quotients, setoid-quotients).
+* *Axis 4 (canonical vs presentation-dependent)* picks up three
+  notes — cubical (equality choice), lenses-and-optics (get/put
+  split), setoid-quotients (named equivalence vs implicit kernel).
+* *Axes with no neighbour coverage* — see §"Gaps" below.
+
+=== Gaps
+
+* *Axis 2 (exact vs approximate)* has *no* adjacency note. The
+  axis-2 artifact is `EchoApprox.agda` (parametric pseudo-metric,
+  three headline lemmas); its closest neighbour analogue — e.g.
+  metric category theory, V-categories, weighted limits — is
+  unwritten. Candidate future note: `metric-categories.adoc`.
+* *Axis 3 (local vs global)* has no adjacency note. The closest
+  candidates are sheaf-theoretic / local-trivialisation framings;
+  not yet written.
+* *Axis 6 (static vs dynamic)* has only one note (`information-
+  flow`, via knowledge update). Other dynamic-typing or temporal
+  neighbours (reactive / temporal logic / coalgebraic process
+  theory) are unwritten.
+* *Axis 8 (information-theoretic vs computational access)* has
+  *no* formal neighbour treatment. Three notes have open
+  implications, flagged ○ above:
+  ** `information-flow.adoc` — cryptographic threat models route
+     through axis 8 when low observers are computationally bounded.
+     Not addressed in the current relational framing.
+  ** `modal-type-theories.adoc` — QTT-style quantitative
+     annotations are proxies for resource control (taxonomy
+     §"Axis 8" lines 236–238) but are not full
+     computational-access tracking. The note treats QTT as a
+     decoration neighbour (axis 5/7), not an axis-8 neighbour.
+  ** `provenance-semirings.adoc` — K-semirings with a cost-tracking
+     interpretation (e.g. tropical `(min, +)`-semirings) would
+     engage axis 8. The current note treats K-provenance as a
+     decoration neighbour (axis 5/7).
+
+  Candidate future notes that *would* directly engage axis 8:
+  `cryptographic-one-way-functions.adoc` (witness inhabitedness vs
+  poly-time witness extraction); `cost-monads.adoc` (resource
+  monads à la Hindley-Milner with cost effects); `complexity-classes
+  -as-modalities.adoc` (P/NP/PSPACE as access modalities).
+
+=== Stale claims flagged for re-evaluation
+
+None of the 11 substantive notes' verdicts is *incorrect* against
+the current taxonomy. Three notes carry framings that would benefit
+from explicit axis-8 disclaimers (the three ○ rows). No note's
+distinctness claim is invalidated by the post-hoc addition of axis
+8; the omission is one of *coverage*, not *contradiction*.
+
+The `INSERTION_NOTE.adoc` describes a doc-surgery operation. As a
+meta-note it has no axis engagement; retained for traceability.
+
 == What's formalised, what's not
 
 The truncation argument has formal exhibits for three of its

docs/adjacency/cubical-systems.adoc

@@ -1,6 +1,8 @@
 = Adjacency: Cubical Systems
 :toc: macro
 
+_Axes engaged: 1 (Ext/Int), 4 (Canon/Pres), 7 (PR/PI). See `README.adoc` § "Axis coverage matrix"._
+
 toc::[]
 
 == 1. Nearest existing construction

docs/adjacency/galois-connections.adoc

@@ -1,6 +1,8 @@
 = Adjacency: Galois connections / abstract interpretation
 :toc: macro
 
+_Axes engaged: 5 (Comp), 7 (PR/PI). See `README.adoc` § "Axis coverage matrix"._
+
 [.lead]
 *Verdict: distinct, by 2-cell argument.* The natural 2-cell in the
 abstraction lattice is the meet, which is structurally

docs/adjacency/hott-fibers.adoc

@@ -1,6 +1,8 @@
 = Adjacency: HoTT homotopy fibers
 :toc: macro
 
+_Axes engaged: 1 (Ext/Int), 7 (PR/PI). See `README.adoc` § "Axis coverage matrix"._
+
 [.lead]
 *Verdict: not distinct from HoTT homotopy fibers — echo IS the
 homotopy fiber.* The win is over the *propositional truncation

docs/adjacency/information-flow.adoc

@@ -1,6 +1,8 @@
 = Adjacency: information-flow non-interference
 :toc: macro
 
+_Axes engaged: 6 (Stat/Dyn), 7 (PR/PI); axis 8 (IT/Comp) open — cryptographic threat models route through axis 8 when low observers are computationally bounded. See `README.adoc` § "Axis coverage matrix"._
+
 [.lead]
 *Verdict: distinct against relational IFC (Goguen-Meseguer
 lineage); open question against type-theoretic IFC.* The

docs/adjacency/lenses-and-optics.adoc

@@ -1,6 +1,8 @@
 = Adjacency: Lenses and Optics
 :toc: macro
 
+_Axes engaged: 4 (Canon/Pres), 5 (Comp), 7 (PR/PI). See `README.adoc` § "Axis coverage matrix"._
+
 toc::[]
 
 == 1. Nearest existing construction

docs/adjacency/modal-type-theories.adoc

@@ -1,6 +1,8 @@
 = Adjacency: modal type theories
 :toc: macro
 
+_Axes engaged: 5 (Comp), 7 (PR/PI); axis 8 (IT/Comp) open — QTT-style quantitative annotations are proxies for resource control (taxonomy §8) but not full computational-access tracking. See `README.adoc` § "Axis coverage matrix"._
+
 [.lead]
 *Verdict: co-extensive with QTT-class systems on bare echo.* Not
 distinct from native modal type theories on the type level; the

docs/adjacency/provenance-semirings.adoc

@@ -1,6 +1,8 @@
 = Adjacency: Provenance Semirings
 :toc: macro
 
+_Axes engaged: 5 (Comp), 7 (PR/PI); axis 8 (IT/Comp) open — K-semirings with a cost-tracking interpretation (e.g. tropical) would engage axis 8. See `README.adoc` § "Axis coverage matrix"._
+
 toc::[]
 
 == 1. Nearest existing construction

docs/adjacency/provenance.adoc

@@ -1,6 +1,8 @@
 = Adjacency: provenance / data lineage
 :toc: macro
 
+_Axes engaged: 7 (PR/PI). See `README.adoc` § "Axis coverage matrix"._
+
 [.lead]
 *Verdict: distinct against single-witness provenance variants by
 the multiplicity argument.* Transitive provenance under composition