docs: narrative alignment for 2026-05-28 PRs #147 #148 #149 + guardrails policy (#152)

Four narrative-alignment edits after the post-compact session:

- **CONTRIBUTING.md**: add Pre-merge checklist item #5 documenting
\`tools/check-guardrails.sh\` (the CI-enforced no-postulates + mandatory
\`--safe --without-K\` policy across \`proofs/agda/**\`). PR #148
(postulated \`EchoImageFactorizationPropPostulated\` consumer) was
closed precisely because this guardrail was not discoverable in
user-facing docs. **Critical** — addresses a real contributor gotcha.
- **docs/echo-types/MAP.adoc**: index the two new Buchholz modules from
this session — \`RankLexJointBplus\` (PR #147) and
\`RankMonoUmbrellaSlice4\` (PR #149) — alongside the existing Slice 3
trio.
- **roadmap.adoc**: refresh Lane 3 status — Slice 3 + Slice 4 both
LANDED 2026-05-28 with the two constructor-level shortfalls pinned as
\`⊤\`-aliases; bottleneck moves to unbudgeted \`_<ᵇʳᶠ_\` global WF.
- **README.md**: Ordinal track one-line ledger gains 2026-05-28 Slice 3
+ Slice 4 entry.

Pure narrative — no Agda touched, no proof obligations changed.

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

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

Author: hyperpolymath

CONTRIBUTING.md

@@ -24,8 +24,9 @@ git commit -s -m "feat: ..."
 2. CHANGELOG.md updated under `[Unreleased]`.
 3. `.machine_readable/6a2/STATE.a2ml` `last-updated` bumped if the change is significant.
 4. **Banned constructs.** No new `believe_me`, `assert_total`, `postulate`, `sorry`, `Admitted`, `unsafeCoerce`, or `Obj.magic` introduced. Estate-wide policy.
-5. **EI-2 discipline.** Per `.machine_readable/6a2/STATE.a2ml § ei-2`, the integration-recipe distinctness investigation is *terminated negatively* and is not to be reopened. If a change touches that territory, read `STATE.a2ml § ei-2` first; the `forbidden-rebrandings` list is a hard fence.
-6. **Naming traps.** `ModeGraded` (with trailing `d`) is canonical; never `ModeGrade`. See `STATE.a2ml § naming-traps`.
+5. **Guardrails are CI-enforced.** All `.agda` files under `proofs/agda/**` must declare `{-# OPTIONS --safe --without-K #-}` at the top. `tools/check-guardrails.sh` runs at CI time across every file (regardless of `All.agda` membership) and fails on: missing `--safe` / `--without-K`, escape pragmas (`TERMINATING`, `REWRITE`, `NO_POSITIVITY_CHECK`, etc.), `postulate` in code, or unsafe primitives (`primTrustMe`, `primEraseEquality`, `trustMe`). The `Exploratory` classification in `docs/echo-types/echo-kernel-note.adoc` only excuses `All.agda` membership — it does NOT excuse the guardrail. If you need postulates for a demo or earn-back-gate consumer, the file must live outside `proofs/agda/` (no current non-guarded path exists; widening the guardrail's allowlist requires a separate design discussion).
+6. **EI-2 discipline.** Per `.machine_readable/6a2/STATE.a2ml § ei-2`, the integration-recipe distinctness investigation is *terminated negatively* and is not to be reopened. If a change touches that territory, read `STATE.a2ml § ei-2` first; the `forbidden-rebrandings` list is a hard fence.
+7. **Naming traps.** `ModeGraded` (with trailing `d`) is canonical; never `ModeGrade`. See `STATE.a2ml § naming-traps`.
 
 ## Reviews
 

README.md

@@ -329,6 +329,7 @@ CLAUDE.md):
 - the new `LiftedOrder n` / `SurfaceDepth n` family shows that arbitrary finite same-binder depth can already be handled by iterated mediated wrappers
 - the new `_ <ᵇʳᶠ _` candidate shows that direct recursive derivations also reduce to those finite-depth fragments; what is still open is a single global mediated well-foundedness theorem for that union
 - the new budgeted layer on `ℕ × BT` isolates the missing global step: the recursive surface route is now well-founded once explicit budget is carried, and the remaining task is to discharge or eliminate that budget in the unbudgeted theorem
+- 2026-05-28 ordinal-track progress: Slice 3 (`rank-mono-<ᵇ-+1-via-head-Ω` headline under a strict-head premise) closed via PRs #141–#143; Slice 4 narrowed umbrella `_<ᵇ⁻ⁿ_` (covering all 10 inherited `_<ᵇ⁰_` cases plus the strict-head joint-bplus) closed via PR #149 (`RankMonoUmbrellaSlice4`); rank-lex pivot scaffold for the bpsi-source-at-equality sub-case landed via PR #147 (`RankLexJointBplus`). Two constructor-level shortfalls remain pinned as `⊤`-aliases: `<ᵇ-ψΩ≤` boundary (closes at lex-rank level only) and `<ᵇ-+1` at equal-head (gated on `RankLexJointBplus`-pivot completion). The unbudgeted `_<ᵇʳᶠ_` global WF and full-order internalisation into `Order.agda` remain open.
 - this still does not internalize the historically blocked shared-binder shapes as actual constructors of `_ <ᵇ _`; the full intended Buchholz order remains open at that step
 - remaining live mathematical work is therefore not the current-core WF route, but the mediated internalization of the shared-binder cases back into the real order package
 - as of 2026-05-27: the Buchholz rank-monotonicity matrix closes 11/13 constructor cases via the WfCNF-restricted `_<ᵇ⁻_` umbrella (9 via `RankPow` + `<ᵇ⁺-ψα` via `RankAdm` 2026-05-26 + `<ᵇ-ψΩ≤` via `RankLex` 2026-05-27); the last open case is `<ᵇ-+1` joint-bplus, with the `Ordinal.Buchholz.HeadOmega` first slice (leading-Ω-index head function + 4 definitional sanity lemmas) landed 2026-05-27 as the structural opening of option (A) per the obstruction doc

docs/echo-types/MAP.adoc

@@ -241,7 +241,15 @@ Staged Buchholz-style collapsing in `--safe --without-K`.
   head-Ω lower bound), `RankPowSlice3Headline` (2026-05-28 — Slice 3
   headline `rank-mono-<ᵇ-+1-via-head-Ω` closed under a strict-head
   premise; umbrella case-split bumps `bpsi=bpsi at equal markers`
-  to rank-adm / rank-lex)).
+  to rank-adm / rank-lex)), `RankLexJointBplus` (2026-05-28 PR #147
+  — parallel rank with `leftmost-α` discriminator for the bpsi-source-
+  at-equality joint-bplus sub-case; second-component strict-mono at
+  equal first components scaffolded), `RankMonoUmbrellaSlice4`
+  (2026-05-28 PR #149 — narrowed `_<ᵇ⁻ⁿ_` umbrella record bundling
+  WfCNF endpoints + `_<ᵇ¹_` derivation; covers all 10 inherited
+  `_<ᵇ⁰_` cases + the strict-head joint-bplus; two shortfalls
+  (`<ᵇ-ψΩ≤` boundary; `<ᵇ-+1` at equal-head) pinned as `⊤`-aliases
+  with explicit lex-rank / rank-lex-jb pointers).
 * Docs: `docs/buchholz-plan.adoc`,
   `docs/echo-types/buchholz-extended-wf.md`,
   `docs/echo-types/buchholz-rank-obstruction.adoc` (per-constructor

roadmap.adoc

@@ -310,9 +310,18 @@ the option-(b) head-Ω inversion lemmas, AND the WfCNF-carrier
 structural-recursion `rank-pow-dominated-by-head-Ω` have all landed
 across PRs #124 (Slice 1, 2026-05-27 late evening), #130 (Slice 2,
 session night), #131 (Slice 2-omega + inversion + ledger), and
-#133+#134 (Slice 2-bplus + the explicit-implicit fix). The remaining
-ordinal-track work is Slice 3 (`rank-mono-<ᵇ-+1-via-head-Ω` headline)
-+ Slice 4 (full `rank-pow-mono-<ᵇ⁻` umbrella composition).
+#133+#134 (Slice 2-bplus + the explicit-implicit fix). Slice 3 (`rank-mono-<ᵇ-+1-via-head-Ω` headline closed under a
+strict-head premise) LANDED 2026-05-28 via PRs #141–#143
+(`RankPowSlice3` + `RankPowSlice3Headline`). Slice 4 (the narrowed
+`_<ᵇ⁻ⁿ_` umbrella covering all 10 inherited `_<ᵇ⁰_` cases plus the
+strict-head joint-bplus) LANDED 2026-05-28 via PR #149
+(`RankMonoUmbrellaSlice4`); two constructor-level shortfalls
+(`<ᵇ-ψΩ≤` boundary closes at lex-rank level; `<ᵇ-+1` at equal-head
+gated on the `RankLexJointBplus` pivot from PR #147) are pinned as
+`⊤`-aliases. The remaining ordinal-track work is the unbudgeted
+`_<ᵇʳᶠ_` global well-foundedness (per `RankBrouwer.agda` preamble)
+and the full-order internalisation back into `Order.agda`'s main
+`_<ᵇ_` package.
 
 *Close-out criterion.* Either: