session: Tier-1+2+3 spine + audience moves + suite + F5 FULL PASS + Slice-2 adopted + narrative audit

Full session deliverable across all tiers + cross-repo upstream adoption.

Canonical identity layer (Tier 1, 4 new modules):
- EchoTotalCompletion (A ≃ Σ B (Echo f))
- EchoOrthogonalFactorizationSystem (ofs-witness)
- EchoImageFactorization (Image f := Σ B (Echo f))
- EchoNoSectionGeneric (structural no-section)

Classification grid (Tier 2, 4 new modules):
- EchoLossTaxonomy (function-side EQUIV/INJ/SURJ/CONST)
- EchoResidueTaxonomy (ResidueForm + 6 instances)
- EchoDecorationStructure (DecorationStructure + 4 instances + abstract degrade-compose)
- EchoObservationalEquivalence (_≡m_)

Pillar F Gate F5 FULL PASS (Tier 3, 3 new modules):
- EchoOFSUnivF5 (F5-1 strict factorisation triangle, funext-qualified)
- EchoOFSUnivF5Diag (F5-2 diagonal lifting, Pointwise + Strict modules)
- EchoOFSUnivF5Iso (F5-3 factorisation uniqueness via composition design)
F5-3 composition route avoids triangle-identity obligation via encode∘g⁻¹.

Audience-facing modules (4 new):
- EchoProvenance (database/lineage)
- EchoSecurity (region-exit/capability-flow; generalises RegionExitAudit walkthrough)
- EchoProbabilisticSupport (sampling/draw-id; NOT measure theory)
- EchoDifferential (sensitivity/perturbation tracking; NOT ε-DP)

Curated narrative deliverable:
- EchoCanonicalIdentitySuite (single-file entry point re-exporting load-bearing headlines)

Consolidation docs (2 new AsciiDoc):
- universal-property.adoc (pullback + F4 + F5/OFS arc end-to-end)
- fibration-package.adoc (map-over + composition + cancellation + pentagon arc)

Ordinal track Slice 2 adoption from upstream PRs #130/#131/#133/#134:
- HeadOmegaInversion.agda (new)
- RankPow.agda extensions (ω-rank-pow-succ + bump facts)
- RankPowDomination.agda (full headline domination via WfCNF structural recursion)
- Ordinal/Buchholz/Smoke.agda pins

Narrative audit + reinforcement across READMEs, MAP, theorem-index,
overview, establishment-plan, INDEX, paper, types-abstract,
composition, taxonomy, assessment, INDEX, retractions, earn-back-plan,
tutorial walkthroughs, and EchoExample* cross-references. Bidirectional
audience-abstract back-references closed where appropriate;
audience-asymmetry notes added where they don't apply.

Pillar F earn-back ledger F-2026-05-27a follow-up for F5 FULL PASS.

Build: --safe --without-K, zero postulates, no funext in trusted base.
Smoke.agda + All.agda both exit 0.

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

Author: hyperpolymath

CLAUDE.md

@@ -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

@@ -61,6 +61,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 +154,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

README.md

@@ -2,6 +2,28 @@
 
 Date: 2026-04-18
 
+[IMPORTANT]
+====
+*Forward-link (2026-05-27).* This M5 assessment is dated 2026-04-18
+and reflects the state at that time — basic Echo / Characteristic /
+Residue layer with the three identity-claim criteria met at the
+example level. Since then a substantially larger structural layer
+has landed:
+
+* *Pillars A–D LANDED* 2026-05-17 + Pillar F gates F1–F5 PASSED.
+* *Canonical identity layer + Tier-2 grid + Tier-3 audience-moves
+  spine + curated suite* LANDED 2026-05-27.
+
+The "distinct concept" verdict here is strictly stronger now: Echo
+is mechanically identified as the canonical fibre-completion
+functor + one leg of the (equivalence, projection) orthogonal
+factorisation system on Type (qualified earn-back F5 FULL PASS
+2026-05-27, follow-up F-2026-05-27a). See
+`docs/echo-types/MAP.adoc` §"Canonical identity layer" and
+`docs/echo-types/universal-property.adoc` for the canonical
+references. This assessment remains as the historical M5 record.
+====
+
 == Binary Conclusion
 
 *Established as distinct concept* (within the current formal scope of this repository).

docs/assessment.adoc

@@ -56,6 +56,142 @@ remainder of information-losing computation: for `f : A → B`,
   `docs/echo-types/types-abstract.adoc`,
   `docs/echo-types/paper.adoc`.
 
+== Canonical identity layer `[REAL]`
+
+The named-theorem load-bearing artefacts that promote Echo from a
+useful construction to a *named* structural object: the canonical
+fibre-completion functor + one leg of the (equivalence, projection)
+orthogonal factorisation system on Type. Landed 2026-05-27 under
+R-2026-05-18 honest-scope discipline — K-free skeletons land here;
+full HoTT-strength upgrades (contractible / propositional fibres,
+(-1)-truncation, full ↔) are documented as the next earn-back gates
+in the Pillar F4 template style.
+
+* *Total completion* — `A ≃ Σ B (Echo f)`. The slogan-unlock: every
+  irreversible map's domain is canonically equivalent to the total
+  space of its echoes. `proofs/agda/EchoTotalCompletion.agda`.
+* *Orthogonal factorisation system* — every `f : A → B` factors as
+  `A ─encode→ Σ B (Echo f) ─proj₁→ B` with the left leg an
+  equivalence (the totality theorem above) and the right leg a
+  projection whose fibre at `y` is `Echo f y`. Architectural
+  keystone. `proofs/agda/EchoOrthogonalFactorizationSystem.agda`.
+* *Image factorisation* — `Image f := Σ B (Echo f)`; the proof-
+  relevant image IS the total Echo space. Three classifications
+  (Surjective, Injective, projection-uniqueness under injectivity).
+  The (epi, mono) truncation form is the next earn-back gate.
+  `proofs/agda/EchoImageFactorization.agda`.
+* *Generic no-section* — `no-section-of-collapsing-map`: for ANY
+  collapsing map with two distinct elements landing on the same
+  image, no section exists. Lifts the previous single-instance
+  result to a structural fact about non-injectivity-at-a-point;
+  recovers the original as a one-line corollary.
+  `proofs/agda/EchoNoSectionGeneric.agda`.
+* *Loss taxonomy* (function-side) — four-axis classification of
+  `f : A → B` by echo shape: EQUIV ⇒ centre + projection-unique;
+  INJ ⇒ projection-unique; SURJ ⇒ every fibre inhabited; CONST ⇒
+  section from the entire domain. K-free skeletons across all four.
+  `proofs/agda/EchoLossTaxonomy.agda`.
+* *Residue taxonomy* (residue-side) — `record ResidueForm f R`
+  packaging the per-output residue carrier + lowering shared by the
+  eight decoration modules. Four instances: trivial (⊤), identity
+  (`Echo f`), generic Σ-cert (`echoR-residue`), and the worked
+  `linear-affine-residue`. The other six decoration modules
+  documented as structurally compatible.
+  `proofs/agda/EchoResidueTaxonomy.agda`.
+* *Decoration structure* (observation-side) — `record
+  DecorationStructure G` packaging the seven-field decoration
+  recipe (order + refl + trans + propositionality + join + UMP)
+  shared across the eight decoration modules. Three instances:
+  Graded (3-grade), Linear (2-grade), Access (5-grade).
+  `proofs/agda/EchoDecorationStructure.agda`.
+* *Observational equivalence* — mode-indexed equality `_≡m_` on
+  `LEcho`. Linear is witness-aware (`_≡_`); affine is witness-blind
+  (`⊤`). Headline `mode-equality-strictly-finer-at-linear` exhibits
+  a linear-distinct / affine-equal pair, closing the
+  "affine forgets what linear retains" story at the equality level.
+  `proofs/agda/EchoObservationalEquivalence.agda`.
+
+*Qualified universal property (Pillar F, Gate F5 FULL PASS,
+2026-05-27).* Three slices in the F4 template (`funext` as
+explicit module parameter, never a postulate; unconditional
+pointwise corollaries kept funext-free) earn back the
+(equivalence, projection) orthogonal factorisation system on
+Type at the qualified level:
+
+* *F5-1* — `echo-factorisation-strict (funext) : f ≡ proj₁ ∘
+  encode f`. `proofs/agda/EchoOFSUnivF5.agda`.
+* *F5-2* — Diagonal lifting property (Pointwise + Strict
+  modules). `proofs/agda/EchoOFSUnivF5Diag.agda`.
+* *F5-3* — Factorisation uniqueness up to iso (Pointwise +
+  Strict modules) via the composition design `φ.to = encode f ∘
+  g⁻¹`. `proofs/agda/EchoOFSUnivF5Iso.agda`.
+
+Retraction follow-up `F-2026-05-27a` logged in
+`docs/retractions.adoc`. See `docs/echo-types/earn-back-plan.adoc`
+status entry for the full gate-pass record.
+
+*Audience-facing modules (Tier 3, GPT-recommended order, all
+landed 2026-05-27).* Each generalises one concrete example into
+the shape the audience speaks in. All four ship the abstract
+record + parametric headline theorems + worked instance +
+honest-bound matched-negative block.
+
+* *Provenance* — `Provenance` record + `module ProvenanceTheorems`.
+  Worked `bool-over-nat-provenance` reproduces
+  `EchoExampleProvenance`. `proofs/agda/EchoProvenance.agda`.
+* *Security* — `Security` record + `module SecurityTheorems`.
+  Per-region exit collapse + audit-no-recovery (factored through
+  `EchoNoSectionGeneric.no-section-of-collapsing-map`). Worked
+  `region-exit-audit-instance` reproduces the
+  `tutorial/region_exit_audit/RegionExitAudit.agda` walkthrough.
+  Honest-bound: NOT bytes-zeroed / side-channel-safe /
+  tamper-evident / oracle-recovery.
+  `proofs/agda/EchoSecurity.agda`.
+* *ProbabilisticSupport* — `Sampling` record + `module
+  SamplingTheorems`. Marginal non-injectivity, Echo carries which
+  index, residue loses index. Worked `bool-indexed-nat-sampling`.
+  Honest-bound: NOT measure-preserving / probability monad /
+  Kantorovich / coupling / randomness extraction.
+  `proofs/agda/EchoProbabilisticSupport.agda`.
+* *Differential* — `Sensitivity` record + `module
+  SensitivityTheorems`. Blur non-injectivity, Echo carries which
+  perturbation, residue loses perturbation. Worked
+  `bool-perturbed-nat-sensitivity`. Honest-bound: NOT ε-DP /
+  Lipschitz bound / noise calibration / adversary model.
+  `proofs/agda/EchoDifferential.agda`.
+
+*Curated suite — single-file entry point.* The narrative
+deliverable that pulls the Tier-1 / Tier-2 / Tier-3 named theorems
+into one readable file. Re-exports load-bearing headlines from
+every module under suite-side names; companion remark documents
+honest scope at the suite level. External-reader workflow: start
+here + read source-module companion remarks for the headlines that
+interest you. `proofs/agda/EchoCanonicalIdentitySuite.agda`.
+
+*Consolidation docs (2026-05-27).* Two doc-only narratives
+threading the universal-property and fibration-package stories
+end-to-end. Each cites the source modules + reading order; no new
+proofs.
+
+* `docs/echo-types/universal-property.adoc` — pullback presentation
+  + R-2026-05-18 narrowing + Gate F4 + Gate F5 (full OFS, three
+  slices). Threads the categorical universal-property arc.
+* `docs/echo-types/fibration-package.adoc` — `map-over*` action +
+  `Echo-comp-iso` accumulation + `cancel-iso` cancellation +
+  pentagon coherence. Threads the fibration-side story.
+
+*Cementing matched-negatives.* Two shadow encodings that have been
+proposed as adequate substitutes for Echo, now provably aren't:
+
+* *Shannon-entropy non-distinguishing* — the fibre-count entropic
+  shadow agrees on `echo-true` vs `echo-false`, while the witness
+  side distinguishes them (matched-negative against
+  `EchoAbstractionBarrier.sigma-distinguishes`).
+  `proofs/agda/EchoEntropy.agda`.
+* *Linear-logic shallow-encoding gap* — the canonical LL `!A := 1`
+  shadow admits a section that the source `LEcho` provably does
+  not. `proofs/agda/EchoLLEncoding.agda`.
+
 == Directions
 
 === Thermodynamic — Landauer/Bennett energy bounds `[REAL]`
@@ -146,12 +282,16 @@ Connect echo types with MAA's reversibility proofs
 
 * Docs: `roadmap.adoc` §"Deferred research track", `docs/EchoJanusBridge.md`.
 
-=== Shannon / information theory `[OPEN]`
-Explicitly *not bridged*. The Transport / Nyquist sampling work
-(Gate-3) is the nearest built thread; a real Shannon-entropy /
-mutual-information formalisation is open.
+=== Shannon / information theory `[REAL*]`
+Partial. The *discrete non-distinguishing* form lands as
+`EchoEntropy.agda` — the fibre-count shadow (uniform-prior Shannon
+surrogate) cannot tell echoes apart at a collapsing point, while
+the witness side can. Real-valued `H(P) = -Σ p log p`, mutual
+information, and the Transport/Nyquist (Gate-3) bridge remain
+open. See Canonical identity layer for the cementing artefact.
 
-* Proofs: `proofs/agda/examples/Transport.agda`.
+* Proofs: `proofs/agda/EchoEntropy.agda`,
+  `proofs/agda/examples/Transport.agda`.
 * Docs: `docs/ECHO-CNO-BRIDGE.adoc` (lines ~104, ~254),
   `docs/adjacency/information-flow.adoc`,
   `docs/gate-3-canonical.adoc`, `docs/gate-3-transport-handoff.adoc`.
@@ -256,8 +396,3 @@ passes/fails, or a claim is retracted/earned-back:
 . Never duplicate detail — link to the canonical proof module / doc.
 . The GitHub wiki `Home` mirrors this file and must point back here as
   SoT; do not fork content into the wiki.
-e entry *and* its status tag
-  here, in the same PR as the change.
-. Never duplicate detail — link to the canonical proof module / doc.
-. The GitHub wiki `Home` mirrors this file and must point back here as
-  SoT; do not fork content into the wiki.

docs/echo-types/MAP.adoc

@@ -4,6 +4,16 @@
 conjectures. Every result backed by the current Agda development is
 marked *Agda-backed*; every conjectural claim is labelled explicitly.
 
+> **Forward-link (2026-05-27).** The composition-track narrative this
+> doc maintains has been consolidated into
+> [`fibration-package.adoc`](fibration-package.adoc) (`map-over` action
+> + `Echo-comp-iso` accumulation + `cancel-iso` cancellation +
+> pentagon coherence, threaded with reading order). The
+> fibration-package consolidation is now the recommended entry point;
+> this doc remains as the longer-form working-note narrative with the
+> per-section conjecture-vs-proof labelling. The proofs cited herein
+> are all Agda-backed and pinned in `Smoke.agda`.
+
 ---
 
 ## The central question