echo-types: open establishment track (Pillar A landed, B–D scaffolded)

New third workstream: path to recognised type-theoretic standing as a
characterised graded comonad of structured loss, with the explicit
verdict that the linear/dependent judgmental ladder is a category
error (Echo is definitionally fib).

- docs/echo-types/establishment-plan.adoc: five-pillar plan + guardrails
- Pillar A (real): EchoFiberBridge.agda — echo↔fib bijection via mk↔ₛ′,
  refl round-trips; pinned in Smoke.agda, wired into All.agda
- Pillars B–D: declaration-free doc scaffolds (EchoPullback,
  EchoGradedComonad, EchoSeparating, EchoRelModel) tracked in All.agda
- CLAUDE.md: workstream 3 + 2026-05-17 rung state

agda All.agda and agda Smoke.agda both exit 0 under --safe --without-K.
No postulates introduced.

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

Author: hyperpolymath

CLAUDE.md

@@ -82,6 +82,25 @@ Two active workstreams:
    * Push the surface-route WF back into `Order.agda`'s main
      `_<ᵇ_` package.
 
+3. **Establishment track (`docs/echo-types/establishment-plan.adoc`).**
+   Path to recognised type-theoretic standing as a *characterised
+   graded comonad of structured loss* (coeffect/quantitative
+   lineage) — explicitly NOT the linear/dependent judgmental ladder.
+   Five pillars: A pin-the-identity, B universal property +
+   graded-comonad laws, C separating model, D second model +
+   conservativity, E external validation. Pillar A landed
+   (`EchoFiberBridge.agda`: `echo↔fib` definitional bridge, pinned
+   in `Smoke.agda`). Pillars B–D exist as declaration-free doc
+   scaffolds in `All.agda` (`EchoPullback`, `EchoGradedComonad`,
+   `EchoSeparating`, `EchoRelModel`) carrying intended signatures.
+
+   Open pieces on this track:
+   * Pillar B `EchoPullback.echo-pullback-univ` — start by relating
+     `EchoCategorical.SliceHom` to a pullback cone.
+   * Pillar B `EchoGradedComonad` — graded counit/comult + 3 laws,
+     reuse `EchoGraded._≤g_`/`_⊔g_`/`≤g-prop`.
+   * Pillars C/D and Pillar E (TYPES/CPP-ITP/Zenodo) not started.
+
 Cross-repo bridge status lives in `docs/echo-types/cross-repo-bridge-status.md`.
 
 # Build
@@ -144,7 +163,39 @@ work to `main` and refresh all documentation:
    name, the commits folded in, the remaining open pieces of the
    milestone, and the proposed smallest useful next advance.
 
-## Current rung state (2026-04-28)
+## Current rung state (2026-05-17)
+
+Just landed: **Establishment-track opening rung.** New third
+workstream (`docs/echo-types/establishment-plan.adoc`): the path to
+recognised type-theoretic standing as a characterised *graded comonad
+of structured loss*, with the explicit verdict that the
+linear/dependent judgmental ladder is the wrong target (Echo adds no
+new judgment — it is definitionally `fib`).
+
+* `docs/echo-types/establishment-plan.adoc` — five-pillar plan +
+  guardrails (no postulates / no `--safe` weakening; quarantine
+  funext; do not reopen EI-2).
+* **Pillar A (real, verified):** `proofs/agda/EchoFiberBridge.agda`
+  defines `fiber` (stdlib v2.3 has none) and ships
+  `echo↔fib : Echo f y ↔ fiber f y` via `mk↔ₛ′`, `refl` round-trips.
+  Pinned in `Smoke.agda` (`fiber; echo→fib; fib→echo; echo↔fib`),
+  wired into `All.agda`.
+* **Pillars B–D (scaffolds):** `EchoPullback`, `EchoGradedComonad`,
+  `EchoSeparating`, `EchoRelModel` — declaration-free doc modules
+  (no postulates, no holes), tracked in `All.agda`, carrying intended
+  signatures as commented specs.
+
+`agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` both
+exit 0 under `--safe --without-K`. No postulates introduced.
+
+Smallest useful next advance: Pillar B `EchoPullback.echo-pullback-univ`
+— relate `EchoCategorical.SliceHom` to a pullback cone and prove the
+terminal-cone universal property; it unblocks the graded-comonad
+framing (`EchoGradedComonad`).
+
+---
+
+## Previous rung state (2026-04-28)
 
 Just landed: **Honest-thermo rung + 5-decoration sweep close +
 cancel-iso packaging + extended-order lex constructors.** Five

docs/echo-types/establishment-plan.adoc

@@ -0,0 +1,190 @@
+= Echo Types — Establishment Plan
+:toc: macro
+:toclevels: 3
+:sectnums:
+:sectnumlevels: 3
+:icons: font
+
+[.lead]
+This document sets out the path by which "echo types" can acquire
+*recognised type-theoretic standing*. It is deliberately separate from
+`roadmap.md` (work partitioned by bottleneck) and `roadmap-gates.adoc`
+(the falsifiable identity claim). This document answers a different
+question: _given_ the gated identity claim, what makes a construction
+like this *established* in the sense that linear, dependent, or graded
+modal types are established — and what specifically must this repository
+ship to get there.
+
+toc::[]
+
+== The honest type-theoretic verdict
+
+`Echo f y := Σ (x : A) , (f x ≡ y)` is *definitionally* the homotopy
+fibre `fib f y` (HoTT book Def. 4.2.4). This fact governs the entire
+strategy and is owned, not hedged:
+
+* *"Linear" and "dependent" are the wrong target — comparing to them is
+  a category error.* Dependent types are a _formation_ discipline
+  (types depend on terms; semantics = LCCC / CwF). Linear and
+  substructural types are a _structural-rule_ discipline
+  (contraction/weakening restricted; semantics = symmetric monoidal
+  closed categories / Benton's LNL). Both change the _judgmental_
+  apparatus of the theory. Echo introduces no new judgment, context
+  structure, or formation rule — it is a derived Σ-type. Shipping
+  bespoke "echo introduction/elimination rules" dressed as primitive
+  would be the fastest possible way to lose every informed reader.
+
+* *The strength that befits echo is a graded comonadic modality —
+  the coeffect / quantitative lineage.* That _is_ an established
+  type strength in the modern sense (Petriček–Orchard–Mycroft
+  coeffects; Brunel–Gaboardi–Mazza–Zdancewic; Atkey's Quantitative
+  Type Theory; Orchard–Liepelt–Eades / Granule; Gaboardi et al.
+  graded modal types). The repo's own code already has the shape:
+  `EchoGraded`'s loss-grade lattice with join and universal property,
+  `EchoLinear`'s two-mode degradation, `EchoCategorical`'s
+  slice/fibration functor laws. It is not yet *named, characterised,
+  and proved* as a graded comonad of structured loss.
+
+[#thesis]
+.The establishment thesis
+****
+Echo is the homotopy fibre, equipped with a loss-grade lattice,
+forming a *definitionally-grounded graded comonad of structured loss*.
+Its authority comes not from being a new object but from being a
+*characterised* one: a universal property, multiple models, an
+irreducibility metatheorem, and a falsifiable retraction discipline.
+****
+
+Owning "it is just `fib`" loudly is a credibility asset: it pre-empts
+the reviewer's first and strongest objection.
+
+== The five pillars
+
+Each pillar names the artefact it must ship and the *authority effect*
+— the specific reason a referee or community would upgrade their
+assessment.
+
+=== Pillar A — Pin the identity
+
+`Echo ≃ fib` currently lives in prose (`docs/gate-1-distinct-phenomenon.adoc`).
+Reviewers want the bridge as a checked lemma.
+
+* Artefact: `proofs/agda/EchoFiberBridge.agda` — `echo↔fib :
+  Echo f y ↔ fiber f y` (definitional; `refl`-level round-trips).
+  Pinned in `Smoke.agda`, wired into `All.agda`. *(landed — see
+  §"Status".)*
+* Authority effect: converts the project's most honest admission into
+  a machine-checked artefact. Referees trust projects that formalise
+  their own deflationary claims.
+
+=== Pillar B — The universal property
+
+The single biggest lever. Echo has functoriality (`map-over` + id/comp),
+the composition iso, cancel-iso, pentagon — but no _characterisation_.
+
+* Artefact 1: `EchoPullback.agda` — `Echo f y` as the pullback of `f`
+  along `y : ⊤ → B`, with the terminal-cone universal property
+  `echo-pullback-univ`. The categorical-semantics anchor.
+* Artefact 2: `EchoGradedComonad.agda` (headline new family) — reuse
+  `EchoGraded._≤g_`, `_⊔g_`, `≤g-prop`; define the graded counit /
+  comultiplication and prove the three graded-comonad laws over the
+  loss-grade lattice.
+* Authority effect: "has a universal property + is a graded comonad"
+  is the line between a named lemma cluster and an established notion.
+
+=== Pillar C — An irreducibility metatheorem
+
+Harden Gate 2. The existing `VisibleConstraintAudit` /
+`IntegrationAudit` _negative_ exhibits (collapsing pseudo-theorems to
+`proj₂`) are exemplary practice; go one step further.
+
+* Artefact: `EchoSeparating.agda` — a *separating model*: a structure
+  satisfying generic Σ-functoriality in which the loss-grade
+  composition law (`degrade-compose` / `degrade-via-join`) fails.
+* Authority effect: answers "isn't this all Σ-lemmas with new names?"
+  with a model, not an argument. Separating models are the gold
+  standard for "this structure is real, not bookkeeping".
+
+=== Pillar D — A second model + conservativity
+
+A notion is established only if it is model-independent.
+
+* Artefact 1: `EchoRelModel.agda` — extend
+  `EchoCategorical.Fibration` / `EchoRelational`; show the
+  graded-comonad laws of Pillar B transport into the relational /
+  presheaf model. Two independent models = robustness.
+* Artefact 2: `docs/echo-types/conservativity.adoc` (+ formal anchor)
+  — because `Echo = Σ`, a small graded calculus with a loss modality
+  embeds *conservatively and definitionally* into MLTT+Σ. State this
+  as a metatheorem. "Conservative, definitionally-grounded extension"
+  is exactly the clean result that earns trust.
+* Authority effect: model-independence + a conservativity theorem turn
+  the deflation into a published positive result.
+
+=== Pillar E — External validation
+
+Authority is conferred socially, not internally. In cost/payoff order:
+
+. TYPES abstract (low bar, fast expert feedback) — "Echo: a
+  definitionally-grounded graded comonad of structured loss".
+. A mechanised-metatheory paper at CPP or ITP (natural venue for a
+  `--safe --without-K` Agda artefact; these venues reward the
+  retraction/gate discipline).
+. Zenodo DOI + installable library packaging (stable module API so
+  others can `import echo-types`).
+. Circulate the strongest adjacency note (HoTT fibres / QTT-modal)
+  to those communities; the adjacency docs already pre-empt referee
+  objections — use them as outreach.
+. Keep the falsifiable gates and a public retraction log. This _is_
+  the biggest authority asset; never soften it.
+
+== Sequencing and guardrails
+
+*Order:* A → B(pullback) → B(graded comonad) → C(separating model) →
+D(second model + conservativity) → E(write-up). A–C are the
+credibility core and need no external unblocker. The ordinal / Buchholz
+track is impressive _consumer evidence_, not foundation — keep it
+firewalled from the identity claim exactly as `roadmap.md` already does.
+
+*Hard guardrails (credibility hazards):*
+
+* Never add a postulate or drop `--safe --without-K` to force a
+  "stronger" result — the conservativity _is_ the product.
+* The funext boundary is real and known (`examples/Transport.agda`
+  stalls because `Field = Fin n → ℚ` forces funext, unavailable under
+  `--safe`). Quarantine any funext-requiring result behind an
+  explicitly labelled, isolated assumption module; never let it touch
+  the core.
+* Do *not* reopen the five-axis simultaneous-integration claim — EI-2
+  settled it negatively, and having cleanly killed it is part of the
+  authority story.
+
+== Status
+
+[cols="1,4,1", options="header"]
+|===
+| Pillar | Artefact | State
+
+| A | `EchoFiberBridge.agda` (`echo↔fib`, pinned in `Smoke.agda`) | Landed
+| B | `EchoPullback.agda` | Scaffolded (doc-only module, in `All.agda`)
+| B | `EchoGradedComonad.agda` | Scaffolded (doc-only module, in `All.agda`)
+| C | `EchoSeparating.agda` | Scaffolded (doc-only module, in `All.agda`)
+| D | `EchoRelModel.agda` | Scaffolded (doc-only module, in `All.agda`)
+| D | `docs/echo-types/conservativity.adoc` | Not started
+| E | TYPES abstract / CPP-ITP paper / Zenodo / library packaging | Not started
+|===
+
+The Pillar B–D scaffolds are documentation-only Agda modules (no
+declarations, hence no postulates or holes — they typecheck under
+`--safe --without-K` and are tracked in `All.agda` per the
+rung-consolidation policy). They carry the intended theorem signatures
+as commented specifications so a fresh session can start filling them
+without re-deriving the design.
+
+== Revision policy
+
+Update this document when a pillar artefact changes state, when a
+guardrail is hit, or when external validation (Pillar E) advances.
+Append-only revision history, each entry annotated with its trigger.
+The stable thesis (<<thesis>>) does not change without a recorded
+reason.

proofs/agda/All.agda

@@ -31,6 +31,15 @@ open import EchoThermodynamics
 open import EchoStabilityTests
 open import VecRotation
 
+-- Establishment-plan pillars (docs/echo-types/establishment-plan.adoc).
+-- A is a real bridge; B–D are doc-only scaffolds (no declarations,
+-- typecheck under --safe --without-K, tracked here per policy).
+open import EchoFiberBridge     -- Pillar A (landed)
+open import EchoPullback        -- Pillar B (scaffold)
+open import EchoGradedComonad   -- Pillar B (scaffold)
+open import EchoSeparating      -- Pillar C (scaffold)
+open import EchoRelModel        -- Pillar D (scaffold)
+
 open import Ordinal.Base
 open import Ordinal.Closure
 open import Ordinal.CNF

proofs/agda/EchoFiberBridge.agda

@@ -0,0 +1,56 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Pillar A of docs/echo-types/establishment-plan.adoc.
+--
+-- `Echo f y` is *definitionally* the homotopy fibre of `f` at `y`
+-- (HoTT book Def. 4.2.4). The gate-1 distinctness argument states
+-- this in prose; this module turns it into a machine-checked
+-- artefact. The bijection is the identity with `refl` round-trips —
+-- that triviality is the entire point. Formalising the project's own
+-- deflationary admission ("Echo adds no new object; it *is* fib") is
+-- a credibility asset, not a redundancy: it pins the identity so the
+-- universal-property work (Pillar B) builds on a stated, not
+-- asserted, foundation.
+
+module EchoFiberBridge where
+
+open import Echo using (Echo)
+
+open import Level using (Level; _⊔_)
+open import Data.Product.Base using (Σ; _,_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Function.Bundles using (_↔_; mk↔ₛ′)
+
+-- The homotopy fibre of `f` at `y`, in its standard MLTT / HoTT form:
+-- a point of the domain together with a proof that `f` sends it to
+-- `y`. The agda-stdlib (v2.3) ships no `fiber`, so it is defined here
+-- precisely so the bridge below is honest about being definitional.
+fiber : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → B → Set (a ⊔ b)
+fiber {A = A} f y = Σ A (λ x → f x ≡ y)
+
+-- Echo IS the homotopy fibre. Not "equivalent up to homotopy" —
+-- definitionally equal, so both directions are the identity.
+echo→fib :
+  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (y : B) →
+  Echo f y → fiber f y
+echo→fib _ _ e = e
+
+fib→echo :
+  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (y : B) →
+  fiber f y → Echo f y
+fib→echo _ _ e = e
+
+-- The bijection, packaged via stdlib's `Function.Bundles._↔_` and
+-- `mk↔ₛ′` — the same equivalence-record convention used throughout
+-- `Echo.agda` (`Echo-comp-iso`, `cancel-iso`). Both round-trips are
+-- `refl`: there is no path algebra here because there is no gap to
+-- bridge.
+echo↔fib :
+  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (y : B) →
+  Echo f y ↔ fiber f y
+echo↔fib f y =
+  mk↔ₛ′
+    (echo→fib f y)
+    (fib→echo f y)
+    (λ _ → refl)
+    (λ _ → refl)

proofs/agda/EchoGradedComonad.agda

@@ -0,0 +1,43 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Pillar B (part 2) of docs/echo-types/establishment-plan.adoc.
+--
+-- SCAFFOLD ONLY. Documentation module (no declarations → no
+-- postulates, no holes; typechecks under `--safe --without-K`,
+-- tracked in `All.agda`).
+--
+-- Goal: exhibit echo, indexed by the loss-grade lattice, as a
+-- *graded comonad of structured loss*. This is the headline new
+-- theorem family: it is what makes "echo" a modality in the
+-- recognised (coeffect / quantitative) sense, slotting it into the
+-- QTT / Granule lineage rather than leaving it a Σ-lemma cluster.
+--
+-- Reuse from `EchoGraded.agda`: the grade order `_≤g_`, its
+-- propositionality `≤g-prop`, the join `_⊔g_` with
+-- `≤g-⊔g-{left,right,univ}`, and `degrade` / `degrade-comp`.
+--
+-- Intended signatures (to be filled, in dependency order):
+--
+--   -- Graded object map (Echo decorated by a loss grade).
+--   GEcho : Grade → (A → B) → B → Set
+--
+--   -- Graded counit: zero-loss grade extracts the bare echo.
+--   gextract : GEcho g0 f y → Echo f y
+--
+--   -- Graded comultiplication along the grade lattice.
+--   gduplicate : g₁ ≤g (g₁ ⊔g g₂) → GEcho (g₁ ⊔g g₂) f y
+--                                  → GEcho g₁ f (GEcho g₂ ...)
+--
+--   -- The three graded-comonad laws (left counit, right counit,
+--   -- coassociativity) stated over `_≤g_` / `_⊔g_`, each reduced
+--   -- to `degrade-compose` + `≤g-prop` where possible.
+--   gcomonad-counit-l   : ...
+--   gcomonad-counit-r   : ...
+--   gcomonad-coassoc    : ...
+--
+-- Note: keep every law a corollary of an existing `EchoGraded`
+-- lemma plus `≤g-prop`. If a law needs genuinely new path algebra,
+-- that is a design signal worth recording in the establishment plan
+-- before proceeding.
+
+module EchoGradedComonad where