session 2026-05-27: Tier-1+2+3 spine + audience moves + suite + F5 FULL 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)

Author: hyperpolymath

CHANGELOG.md

@@ -23,9 +23,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
     a two-level compositional convenience) — first slice of option
     (A) for the remaining `<ᵇ-+1` joint-bplus discharge; no
     rank-mono yet.
-- *Lane 3 head-Ω route — Slice 2 + Slice 2-omega + inversion (option (b))
-  landed.* Follow-on to the Slice 1 head-Ω landing above (session night,
-  PRs #130 + #131):
+- *Lane 3 head-Ω route — Slice 2 + Slice 2-omega + inversion + Slice 2-bplus
+  ALL LANDED 2026-05-27.* Follow-on to the Slice 1 head-Ω landing above
+  (PRs #130 + #131 + #133 + #134):
   - `Ordinal.Buchholz.RankPow` gains `ω-rank-pow-succ : OmegaIndex →
     Ord` with per-marker strict dominance at *both* branches
     (`ω-rank-pow-<-succ-fin` via `ω^-strict-mono-suc`;
@@ -44,16 +44,16 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
     `⊕-mono-<-right (ω-rank-pow-pos ω)`.  Full record in
     `Ordinal.Buchholz.RankPow`'s "History note" block.
   - New module `Ordinal.Buchholz.HeadOmegaInversion` lands the
-    option-(b) inversion lemmas `head-Ω-inv-bOmega :
-    bOmega ν <ᵇ y → ν <Ω head-Ω y` (strict — three constructors
-    with `bOmega ν` LHS all carry strict `<Ω` witnesses) and
-    `head-Ω-inv-bpsi : bpsi ν α <ᵇ y → ν ≤Ω head-Ω y` (non-strict —
-    the `<ᵇ-ψΩ≤` constructor tops out at `≤Ω`).  Both proved by
-    structural recursion on the `<ᵇ` derivation; no rank-mono
-    dependency.  Picking option (b) over option (a) keeps the
-    eventual `rank-pow-dominated-by-head-Ω` (Slice 2-bplus,
-    remaining open) independent of the still-open `rank-pow-mono-≤ᵇ`
-    on the original `_<ᵇ_`.
+    option-(b) inversion lemmas `head-Ω-inv-bOmega` (strict) and
+    `head-Ω-inv-bpsi` (non-strict). Both proved by structural
+    recursion on the `<ᵇ` derivation; no rank-mono dependency.
+  - New module `Ordinal.Buchholz.RankPowDomination` lands the
+    Slice 2-bplus headline `rank-pow-dominated-by-head-Ω` by
+    structural recursion on WfCNF, plus the supporting lemmas
+    (`<′→≤′`, `≤′-<′-trans`, `<′-trans`, `ω-rank-pow-mono-≤Ω`,
+    `ω-rank-pow-succ-pos`, `additive-principal-ω-rank-pow-succ`,
+    `rank-y-bound`). PR #134 was the one-line explicit-implicit
+    fix for the initial `ω≤ω` case of `ω-rank-pow-mono-≤Ω`.
 - *Decoration bridge — R5 exploratory entry scaffolded (PR #129).*
   `docs/echo-types/explorations/decoration-bridge/` lands a bounded
   exploration of whether the Choreo × Graded integration shape
@@ -69,6 +69,22 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
   deliberately not in `All.agda`, classified as "Exploratory (not in
   All.agda)" in `docs/echo-types/echo-kernel-note.adoc` so CI's
   classification-drift lint stays green.
+- *Tier-1+2+3 spine + audience moves + suite + F5 FULL PASS
+  LANDED 2026-05-27.* My session's contribution sitting on top of
+  the parallel-session ordinal work above. See CLAUDE.md's
+  "Slice-2 upstream adoption" + "broad-cleanup close" session arcs
+  for the deliverable list; key headlines: `EchoTotalCompletion.A↔ΣEcho`,
+  `EchoOrthogonalFactorizationSystem.ofs-witness`,
+  `EchoNoSectionGeneric.no-section-of-collapsing-map`, the four
+  Tier-2 classification-grid records (`ResidueForm` /
+  `DecorationStructure` / function-side / observational), the
+  Pillar F Gate F5 FULL PASS triple (F5-1 / F5-2 / F5-3) earning
+  back the qualified OFS, four audience-facing modules
+  (`EchoProvenance` / `EchoSecurity` / `EchoProbabilisticSupport`
+  / `EchoDifferential`), and the curated single-file entry
+  `EchoCanonicalIdentitySuite`. Two consolidation narratives
+  `docs/echo-types/{universal-property,fibration-package}.adoc`.
+  Retraction follow-up F-2026-05-27a logged in `docs/retractions.adoc`.
 - *Lane 5 tutorial track — the originally-scaffolded triplet is
   complete.* `tutorial/` ships three worked walkthroughs with
   honest-bound disclosure at top + matched-negative `NotProved-*`

CLAUDE.md

@@ -33,7 +33,7 @@ Per `.machine_readable/6a2/STATE.a2ml`:
 Ongoing tracks at a glance (point-in-time, see `roadmap.adoc` for the live status):
 
 * *Identity claim.* `docs/retractions.adoc` R-2026-05-18 narrows the public claim to a *loss-graded reindexing modality* over a thin poset (not a graded comonad). Every newer artefact is stated within those narrowings.
-* *Ordinal / Buchholz track.* 11 of 13 per-constructor rank-mono cases closed under the WfCNF-restricted `_<ᵇ⁻_` via the `RankPow` / `RankAdm` / `RankLex` slices. Remaining open case `<ᵇ-+1` joint-bplus is in flight under the head-Ω domination route: `head-Ω` (Slice 1) + `ω-rank-pow-succ` with per-marker strict dominance at both branches (Slice 2 + Slice 2-omega) + the option-(b) head-Ω inversion lemmas (`Ordinal.Buchholz.HeadOmegaInversion`) all landed; only the WfCNF-carrier structural recursion (Slice 2-bplus) remains. See `docs/echo-types/buchholz-rank-obstruction.adoc`.
+* *Ordinal / Buchholz track.* 11 of 13 per-constructor rank-mono cases closed under the WfCNF-restricted `_<ᵇ⁻_` via the `RankPow` / `RankAdm` / `RankLex` slices. The remaining `<ᵇ-+1` joint-bplus case is now FULLY CLOSED (2026-05-27) via the head-Ω domination route: `head-Ω` (Slice 1) + `ω-rank-pow-succ` with per-marker strict dominance at both branches (Slice 2 + Slice 2-omega) + the option-(b) head-Ω inversion lemmas (`Ordinal.Buchholz.HeadOmegaInversion`) + the WfCNF-carrier structural recursion (Slice 2-bplus, `Ordinal.Buchholz.RankPowDomination.rank-pow-dominated-by-head-Ω`). See `docs/echo-types/buchholz-rank-obstruction.adoc`.
 * *Tutorial track (Lane 5).* Three worked walkthroughs under `tutorial/` (certified region-exit audit, epistemic erasure, provenance/debugging echo); each carries an honest-bound disclosure at the top and a matched-negative block at the bottom. The tutorial tree builds with the repo root added to the Agda include path; see `tutorial/README.adoc`.
 * *Establishment track (Pillar E).* Internal programme (Pillars A–D) complete since 2026-05-17. The paper (`docs/echo-types/paper.adoc`) is a living draft with remaining `[EXPAND]` tags; the venue + Zenodo + outreach plan sits in `docs/echo-types/pillar-e-offline.adoc` (author-driven).
 

EXPLAINME.adoc

@@ -8,6 +8,32 @@ the 6a2 capture and the supporting documents. A new session
 should read this in under 60 seconds before doing anything
 else.
 
+[IMPORTANT]
+====
+*Status forward-link (2026-05-27).* This INDEX is scoped to the
+EI-2 investigation + 6a2 capture (April 29 2026); it is the
+*audit-trail* index for that specific work. Since then the world
+has moved on substantially:
+
+* *Establishment-plan Pillars A–D LANDED* 2026-05-17 (with
+  R-2026-05-18 narrowings).
+* *Pillar F gates F1, F2, F3, F4, F5 all PASSED*, retraction
+  follow-ups F-2026-05-18a / F-2026-05-20a/b / F-2026-05-27a
+  logged in `docs/retractions.adoc`.
+* *Canonical identity layer + Tier-2 classification grid + Tier-3
+  audience-moves spine + curated suite all LANDED* 2026-05-27.
+* *Lane 5 tutorial triplet (W1+W2+W3) LANDED* 2026-05-26/27.
+* *Ordinal Buchholz rank-mono umbrella* closes 11/13 constructors;
+  HeadOmega slice 1+2 partial.
+
+For the CURRENT state of the repo, read `docs/echo-types/MAP.adoc`
+(the master content map), `CLAUDE.md` (the session-by-session
+ledger), and `docs/echo-types/earn-back-plan.adoc` (the Pillar F
+gate ledger). This file remains AS THE AUDIT INDEX for the EI-2
+work; the EI-2 termination + its forbidden-rebrandings still
+stand, and gate G-001 (no reopening EI-2) is still enforced.
+====
+
 toc::[]
 
 == Why this file exists

INDEX.adoc

@@ -21,6 +21,115 @@ Shannon — and ArghDA tooling), each status-tagged and back-linked to
 its proofs and docs, with the retraction/proof-debt governance called
 out. The scattered overview/roadmap docs are detail under it.
 
+## 📐 Structural overview
+
+```mermaid
+flowchart TD
+    F["<b>Foundation</b><br/>Echo f y := Σ (x : A) , (f x ≡ y)<br/>= homotopy fibre"]
+    AD["<b>Pillars A–D</b> (establishment plan, LANDED 2026-05-17)<br/>A: echo↔fib · B: pullback UP · C: separating model · D: carrier-parametric"]
+    PF["<b>Pillar F gates</b> (earn-back, ALL PASSED)<br/>F1: graded-comonad witness · F2: 2nd Echo-functor model<br/>F3: 2nd non-iso grade-monoid · F4: funext-qualified pullback UP<br/>F5: funext-qualified full OFS"]
+    T1["<b>Tier 1 · Canonical identity layer</b> (2026-05-27)<br/>EchoTotalCompletion (A ≃ Σ B Echo f) · OFS-witness · Image · no-section-of-collapsing-map"]
+    T2["<b>Tier 2 · Classification grid</b><br/>LossTaxonomy (function-side) · ResidueTaxonomy (residue-side) · DecorationStructure · _≡m_"]
+    T3["<b>Tier 3 · Qualified universal property</b> (Gate F5)<br/>echo-factorisation-strict · diagonal lifting · factorisation uniqueness up to iso"]
+    AUD["<b>Audience surfaces</b><br/>EchoProvenance · EchoSecurity · EchoProbabilisticSupport · EchoDifferential"]
+    SUITE["<b>EchoCanonicalIdentitySuite</b><br/>(curated single-file entry point)"]
+
+    F --> AD
+    AD --> PF
+    F --> T1
+    T1 --> T2
+    T2 --> T3
+    PF -.->|F5 underpins| T3
+    T1 --> AUD
+    T2 --> AUD
+    T3 --> AUD
+    T1 --> SUITE
+    T2 --> SUITE
+    T3 --> SUITE
+    AUD --> SUITE
+```
+
+The diagram above renders on GitHub; for terminal viewers an ASCII
+version of the same stack:
+
+```
+┌─────────────────────────────────────────────────────────────────┐
+│  EchoCanonicalIdentitySuite   ← curated single-file entry        │
+├─────────────────────────────────────────────────────────────────┤
+│  Audience surfaces:                                              │
+│  Provenance · Security · ProbabilisticSupport · Differential     │
+├─────────────────────────────────────────────────────────────────┤
+│  Tier 3 (Gate F5, funext-qualified):                             │
+│  F5-1 strict triangle · F5-2 diagonal lifting · F5-3 uniqueness  │
+├─────────────────────────────────────────────────────────────────┤
+│  Tier 2 (classification grid):                                   │
+│  LossTaxonomy · ResidueTaxonomy · DecorationStructure · _≡m_     │
+├─────────────────────────────────────────────────────────────────┤
+│  Tier 1 (canonical identity layer):                              │
+│  TotalCompletion · OFS · ImageFactorization · NoSectionGeneric   │
+├─────────────────────────────────────────────────────────────────┤
+│  Pillar F gates F1–F5  (earn-back ledger, ALL PASSED)            │
+├─────────────────────────────────────────────────────────────────┤
+│  Pillars A–D  (establishment plan, LANDED 2026-05-17)            │
+├─────────────────────────────────────────────────────────────────┤
+│  Foundation: Echo f y := Σ (x : A) , (f x ≡ y)                   │
+└─────────────────────────────────────────────────────────────────┘
+```
+
+**The headline factorisation** (Tier 1 + Pillar F Gate F5):
+
+```
+                  encode f
+        A ────────────────────→ Σ B (Echo f)
+         ╲                            │
+          ╲                           │
+         f ╲                          │ proj₁
+            ╲                         │
+             ╲                        │
+              ╲                       ↓
+               ────────────────────→ B
+
+      Left leg  (encode f) :  EQUIVALENCE          ← EchoTotalCompletion.A↔ΣEcho
+      Right leg (proj₁)    :  PROJECTION
+      Triangle             :  f ≡ proj₁ ∘ encode f ← strict given funext (F5-1)
+                                                    pointwise definitional otherwise
+```
+
+This is **the** structural fact the repo establishes: every irreversible
+`f` factors canonically through its total Echo space, with the left leg
+an equivalence (the *slogan-unlock*) and the right leg a projection.
+Under `--safe --without-K` the factorisation existence + fibre
+identification (`ofs-witness`) are unconditional; the function-level
+universal-property clauses are earned back under Pillar F Gate F5
+(`funext` as explicit module parameter, never a postulate).
+
+## 📖 Recommended reading order
+
+For someone landing here for the first time and wanting the full arc:
+
+1. **[`docs/echo-types/MAP.adoc`](docs/echo-types/MAP.adoc)** — the
+   master content map, status-tagged.
+2. **[`proofs/agda/EchoCanonicalIdentitySuite.agda`](proofs/agda/EchoCanonicalIdentitySuite.agda)** —
+   the curated single-file Agda entry point, re-exporting every
+   load-bearing headline from Tier 1, Tier 2, Tier 3, and the
+   audience surfaces.
+3. **[`docs/echo-types/universal-property.adoc`](docs/echo-types/universal-property.adoc)** —
+   the categorical-universal-property story end-to-end (pullback +
+   F4 + F5 / OFS), with the diagrams above as the spine.
+4. **[`docs/echo-types/fibration-package.adoc`](docs/echo-types/fibration-package.adoc)** —
+   the fibration-side companion (`map-over` + composition +
+   cancellation + pentagon).
+5. **[`docs/echo-types/paper.adoc`](docs/echo-types/paper.adoc)** —
+   the long-form Pillar E paper (LIVING DRAFT with `[EXPAND]` tags;
+   §"Post-establishment structural extensions" weaves the
+   2026-05-27 Tier-1+2+3 spine into the central argument).
+6. **[`docs/retractions.adoc`](docs/retractions.adoc)** +
+   **[`docs/echo-types/earn-back-plan.adoc`](docs/echo-types/earn-back-plan.adoc)** —
+   honesty layer: R-2026-05-18 narrowing + Pillar F gate ledger
+   (F1–F5 ALL PASSED).
+7. **[`CLAUDE.md`](CLAUDE.md)** — the session-by-session ledger
+   for what got built when (read after the canonical docs).
+
 ## Core Idea
 
 Most formalisms foreground two clean cases:
@@ -61,6 +170,63 @@ with constructive proofs (`--safe --without-K`, no postulates in `proofs/agda`):
 - `map-over-comp` (composition law)
 - `map-square` (action along commuting squares)
 
+## Canonical identity layer (2026-05-27)
+
+The named-theorem load-bearing artefacts that promote Echo from a
+useful construction to a *named* structural object — the canonical
+fibre-completion functor plus one leg of the (equivalence,
+projection) orthogonal factorisation system on Type. **Read
+[`docs/echo-types/MAP.adoc`](docs/echo-types/MAP.adoc) §"Canonical
+identity layer" for the full status-tagged listing; this section
+is the README-side hook.**
+
+Single-file curated entry point:
+[`proofs/agda/EchoCanonicalIdentitySuite.agda`](proofs/agda/EchoCanonicalIdentitySuite.agda)
+re-exports every load-bearing headline under the suite-side index.
+
+Tier 1 (the canonical identity layer itself):
+
+- `proofs/agda/EchoTotalCompletion.agda` — `A ≃ Σ B (Echo f)` (the slogan-unlock)
+- `proofs/agda/EchoOrthogonalFactorizationSystem.agda` — `ofs-witness` (the OFS witness at the K-free level)
+- `proofs/agda/EchoImageFactorization.agda` — `Image f := Σ B (Echo f)` (image factorisation in Echo language)
+- `proofs/agda/EchoNoSectionGeneric.agda` — `no-section-of-collapsing-map` (the structural no-section theorem)
+
+Tier 2 (the classification grid — kinds-of-loss × shapes-of-residue):
+
+- `proofs/agda/EchoLossTaxonomy.agda` — four-axis function-side classification (EQUIV / INJ / SURJ / CONST)
+- `proofs/agda/EchoResidueTaxonomy.agda` — `ResidueForm` record + four instances
+- `proofs/agda/EchoDecorationStructure.agda` — `DecorationStructure` record (seven-field recipe) + four instances + abstract degrade-compose
+- `proofs/agda/EchoObservationalEquivalence.agda` — mode-indexed equality `_≡m_` on `LEcho`
+
+Tier 3 / Pillar F Gate F5 FULL PASS (2026-05-27, qualified OFS earn-back):
+
+- `proofs/agda/EchoOFSUnivF5.agda` — F5-1 strict factorisation triangle (funext-qualified)
+- `proofs/agda/EchoOFSUnivF5Diag.agda` — F5-2 diagonal lifting property
+- `proofs/agda/EchoOFSUnivF5Iso.agda` — F5-3 factorisation uniqueness up to iso
+
+Audience-facing surfaces (each ships `record + parametric headline theorems + worked instance + honest-bound matched-negatives`):
+
+- `proofs/agda/EchoProvenance.agda` — database / lineage audience
+- `proofs/agda/EchoSecurity.agda` — region-exit / capability-flow audience (generalises `tutorial/region_exit_audit/`)
+- `proofs/agda/EchoProbabilisticSupport.agda` — sampling / draw-id audience
+- `proofs/agda/EchoDifferential.agda` — sensitivity / perturbation-tracking audience
+
+Cementing matched-negatives (shadow encodings that provably don't substitute for Echo):
+
+- `proofs/agda/EchoEntropy.agda` — Shannon-entropy non-distinguishing theorem
+- `proofs/agda/EchoLLEncoding.agda` — LL `!A := 1` shallow-encoding gap
+
+Consolidation narratives:
+
+- [`docs/echo-types/universal-property.adoc`](docs/echo-types/universal-property.adoc) — pullback + F4 + F5 / OFS arc end-to-end
+- [`docs/echo-types/fibration-package.adoc`](docs/echo-types/fibration-package.adoc) — map-over + composition + cancellation + pentagon arc
+
+Pillar F gate ledger + retraction follow-ups:
+[`docs/echo-types/earn-back-plan.adoc`](docs/echo-types/earn-back-plan.adoc)
+(gates F1–F5, all PASSED) +
+[`docs/retractions.adoc`](docs/retractions.adoc) (R-2026-05-18 +
+follow-ups F-2026-05-18a, F-2026-05-20a/b, F-2026-05-27a).
+
 Characteristic M2 results include:
 
 - explicit non-injectivity witnesses for collapse maps
@@ -97,6 +263,8 @@ On `main`, the following are true:
 - distinct-witness and retained-constraint exemplars are present (`echo-true≢echo-false`, `stateA≢stateB`, `visible-constraint`)
 - degrade-law family lands across decoration layers (graded, linear/affine, choreographic, access, cost, search); see `docs/theorem-index.md` for the aggregate
 - Pillars A–D of the establishment plan are LANDED (with R-2026-05-18 narrowings; see `docs/retractions.adoc`); Pillar E (paper) is in progress
+- Pillar F gates F1–F5 all PASSED (F1 graded-comonad-witness; F2 Echo-functor second model; F3 second non-isomorphic grade-monoid; F4 funext-qualified pullback UP; F5 funext-qualified full OFS — F-2026-05-27a)
+- Canonical identity layer + Tier-2 grid + audience surfaces LANDED 2026-05-27 (see "Canonical identity layer" section above + `EchoCanonicalIdentitySuite.agda` for the curated entry point)
 - Lane 5 tutorial triplet LANDED 2026-05-27 under `tutorial/`: region-exit audit, epistemic erasure, and provenance / debugging — each with honest-bound + matched-negative disclosure discipline; build via `agda --library-file=/tmp/agda-libs -i . -i proofs/agda tutorial/All.agda`
 
 Per-lane status, close-out criteria, and the identity-claim verdict