feat(applications): haplotype collapsing as Echo fiber

docs/echo-types/MAP.adoc

@@ -542,6 +542,55 @@ open. See Canonical identity layer for the cementing artefact.
   `docs/adjacency/information-flow.adoc`,
   `docs/gate-3-canonical.adoc`, `docs/gate-3-transport-handoff.adoc`.
 
+== Applications `[REAL*]`
+
+First-class examples where Echo fiber is the right explanatory unit,
+not just Σ renamed. Each application ships Agda anchor + Nickel schema
+(k9 contract) + Julia shadow + JEG/webui sketch. The directory
+`docs/echo-types/applications/` is the index.
+
+* *Compiler analysis* — `docs/echo-types/applications-compiler-analysis.adoc`
+  (parser error recovery, abstract-interpretation widening). `[DRAFT]` prose,
+  `[REAL]` Agda refs (`EchoApprox`, `EchoDecidable`, `EchoCost`, `EchoSearch`).
+  Sibling to `docs/echo-types/examples.adoc`.
+
+* *Haplotype collapsing* — `docs/echo-types/applications/haplotype-collapsing.adoc`
+  (ASV dereplication / clone grouping in protist workflows, metamanifold-webui,
+  Protoctist.jl, JEG). The loss map `collapse : Clone → Haplotype` is
+  non-injective; `Echo collapse h = Σ Clone (collapse c ≡ h)` is the structural
+  lineage of collapsed clones. Nickel schema carries fiber as sidecar
+  (`fibers: Dict Haplotype => FiberBundle`), Julia exacts matrix stays O(m²) on
+  haplotypes (representatives), not O(n²) on clones, JEG displays lineage by
+  expanding fiber. Choreographic framing: `Sequencer ⊑ Collapser ⊑ Visualizer`
+  is `keep ≤ residue ≤ forget` from `EchoGraded` / `EchoChoreo.applyChoreo`.
+
+  * Agda: `proofs/agda/EchoHaplotypeCollapsing.agda` `[REAL]` — `collapse-non-injective`,
+    `echo-clone₁≢echo-clone₂`, `no-canonical-clone-recovery` via
+    `no-section-of-collapsing-map`, `aggregation-as-fold` via `sumMonoid`,
+    `FiberBundle` sidecar, `HaploDist` separation (domain = B, not Echo f).
+  * Nickel: `docs/echo-types/applications/haplotype-collapsing.k9.ncl` `[DRAFT]` —
+    `CollapsedResult` with `distance_matrix : m×m`, `fibers : Dict`, contracts
+    for count = length clones, keys = representatives, square matrix.
+  * Julia: `docs/echo-types/applications/haplotype-collapsing.jl` `[DRAFT]` —
+    `collapse_clones : Vector Clone → CollapsedResult`, O(n) grouping + O(m²)
+    distances, `fibers` sidecar, `test_no_canonical_recovery`,
+    `test_aggregation_as_fold`, cost-model benchmark.
+  * JEG: React sketch in the adoc — graph on `representatives` + `distance_matrix`,
+    `FiberView` expands `fibers[haplotype_id].clones` O(k) rendering, no recompute.
+  * Extensions: Protoctist.jl `HaplotypeCollapsing` module (proposed, keeps
+    PR2/SILVA + tree building O(m²) unchanged, adds fiber sidecar for iTOL/jplace);
+    EchoTypes.jl `EchoHaplotypeCollapsing` finite-domain shadow (proposed).
+
+  Status: Agda `[REAL]` on `main`, Nickel/Julia/JEG `[DRAFT]`, Protoctist/EchoTypes.jl `[OPEN]`.
+
+* Applications index: `docs/echo-types/applications/README.adoc`.
+
+Choreographic note: every application with a "raw → collapsed → visualized"
+pipeline is an instance of `EchoChoreo._⊑c_` / `EchoGraded._≤g_` decoration
+order. The fiber is the choreographic residue that must travel across the
+collapse boundary, even though O(n²) computation lives only on the collapsed side.
+See `applications/haplotype-collapsing.adoc` §"Choreographic framing".
+
 == Tutorial / pedagogy `[REAL]`
 
 Three worked walkthroughs landing 2026-05-26/27 under `tutorial/`,

docs/echo-types/applications/README.adoc

@@ -0,0 +1,69 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Applications of Echo Types
+:toc: macro
+
+[.lead]
+Echo Types began as a foundation (fiber as structured loss) and grew a taxonomy,
+but the identity claim lives or dies on *applications* where the fiber is the
+right explanatory unit — not just Σ renamed. This directory collects such
+applications, each with:
+
+* an Agda anchor (`proofs/agda/Echo*.agda`) proving the loss shape,
+* a Nickel schema (k9 contract) showing how the fiber witness travels through config,
+* a Julia shadow (EchoTypes.jl / Protoctist.jl style) showing executable intuition,
+* a JEG / webui sketch for how a visualizer consumes the residue.
+
+toc::[]
+
+== Index
+
+* `haplotype-collapsing.adoc` — haplotype / ASV collapsing in protist workflows
+  (metamanifold-webui, Protoctist.jl, JEG). Status: `[REAL]` Agda + `[DRAFT]` Nickel/Julia.
+* `../applications-compiler-analysis.adoc` — compiler analysis as structured loss
+  (parser recovery, abstract interpretation). Status: `[DRAFT]` prose, `[REAL]` Agda refs.
+
+== Why an applications/ directory?
+
+The earlier `applications-compiler-analysis.adoc` lived as a single file because
+compiler analysis was the only worked application. Haplotype collapsing is the
+second, and it is structurally different: it is a *many-to-one* aggregation where
+the fiber is a *lineage* that must survive an O(n²) distance-matrix optimization.
+That pattern recurs (DB GROUP BY, deduplication, clustering), so it deserves a
+directory.
+
+Each application doc follows the template:
+
+[source]
+----
+= Application: <name>
+== The loss map f : A → B
+== Echo f y as structural lineage
+== Nickel schema: how the fiber witness travels
+== Julia exacts matrix: keeping O(n²) on B, not A
+== JEG / webui: displaying the fiber without slowing the matrix
+== Choreographic framing
+== Agda anchor
+== Extensions to Protoctist.jl / EchoTypes.jl
+----
+
+== Choreographic types as application carrier
+
+EchoChoreo (`proofs/agda/EchoChoreo.agda`) models `Client ⊑c Server` as a
+decoration order with a canonical `client-to-server` map-square lift. Every
+application that has a "raw → collapsed → visualized" pipeline is a choreography:
+
+  Sequencer (Raw) --collapse--> Collapser (Collapsed) --fiber--> Visualizer (JEG)
+
+The fiber is the choreographic residue that must be carried across the
+collapse boundary, even though the O(n²) computation lives only on the collapsed
+side. This is the same recipe as `EchoGraded.degrade-compose` / `applyChoreo-compose`:
+different paths through the decoration order agree, and the join is the top.
+
+Applications are thus *instances* of the choreographic decoration structure,
+not a separate theory.
+
+== Status legend (same as MAP.adoc)
+
+* `[REAL]` — mechanised in Agda `--safe --without-K`, on `origin/main`
+* `[DRAFT]` — prose / schema / Julia sketch, not yet mechanised
+* `[OPEN]` — acknowledged gap

docs/echo-types/applications/choreographic-types.adoc

@@ -0,0 +1,87 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Choreographic Types as Application Carrier
+:toc: macro
+
+[.lead]
+`EchoChoreo.agda` (`Client ⊑c Server`) is not just an example — it is the
+*carrier* for applications that have a raw → collapsed → visualized pipeline.
+This note explains how to use the choreographic decoration order as the
+scaffolding for any application, with haplotype collapsing as the worked instance.
+
+toc::[]
+
+== The pattern
+
+Every lossy pipeline has three roles:
+
+  1. Producer (Raw) — sees `A` (Clone, TokenStream, Concrete Value)
+  2. Collapser — maps `A → B` (Haplotype, SyntaxTree, AbstractValue) + produces fiber `Echo f`
+  3. Consumer (Visualizer, Debugger, Auditor) — needs `B` for O(n²) work + `Echo f` for lineage
+
+In `EchoChoreo`, this is `Role = Client | Server` with `obs : Role → Global → Bool`.
+In general, it is `PipelineRole = Sequencer | Collapser | Visualizer`.
+
+The decoration order `keep ≤ residue ≤ forget` from `EchoGraded` is the same as
+`Client ⊑c Server` from `EchoChoreo`:
+
+* `keep` = full `A` (Producer)
+* `residue` = `B + Echo f` (Collapser → Consumer, Echo retained)
+* `forget` = `B` alone (distance matrix, type-checker, etc., Echo forgotten)
+
+`degrade-compose` / `applyChoreo-compose` says: any factoring `keep ≤ residue ≤ forget`
+agrees with direct `keep ≤ forget` on `B`. That is, computing on `B` after
+collapsing gives same result as computing on `A` then collapsing — up to
+non-canonical choice of representative (no-section theorem).
+
+== Why this matters for applications
+
+* Compiler analysis (`applications-compiler-analysis.adoc`):
+  `Source ⊑ IR ⊑ Abstract` with `Echo α` as widening residue
+* Haplotype collapsing (`haplotype-collapsing.adoc`):
+  `Sequencer ⊑ Collapser ⊑ Visualizer` with `HaploFiber` as lineage residue
+* DB GROUP BY (`EchoAggregation`):
+  `Row ⊑ Summary` with `Echo groupBy` as provenance residue
+* Region exit (`RegionExitAudit`):
+  `LiveAt r ⊑ ExitedAt r` with `Echo collapse_r` as linear residue
+
+All are instances of the same `DecorationStructure` record from
+`EchoDecorationStructure.agda`:
+
+[source,agda]
+----
+record DecorationStructure G where
+  _≤_ : G → G → Set
+  ≤-refl, ≤-trans, ≤-prop, join, ≤-join-left/right/univ
+----
+
+`graded-decoration-structure`, `linear-decoration-structure`,
+`access-decoration-structure`, `choreo-decoration-structure` are four
+witnesses. Haplotype collapsing proposes a fifth:
+
+[source,agda]
+----
+haplo-decoration-structure : DecorationStructure PipelineRole
+-- keep = Sequencer, residue = Collapser, forget = Visualizer
+-- join = Visualizer (top, has least info)
+----
+
+== How to add a new application
+
+1. Identify `f : A → B` (the loss map)
+2. Prove `f` non-injective → `Echo f y` distinguishes witnesses
+3. Prove `no-section` → disaggregation non-canonical, must keep fiber
+4. Identify `Monoid` for aggregation (if counting / summing)
+5. Define `FiberBundle` sidecar: `B + List A` with Nickel contract
+6. Show O(n²) separation: distance / analysis on `B` only, fiber O(n) sidecar
+7. Choreographic framing: map roles to `keep ≤ residue ≤ forget`
+8. Agda anchor + Nickel schema + Julia shadow + JEG sketch
+
+See `haplotype-collapsing.adoc` for the full template.
+
+== Status
+
+* `EchoChoreo` `[REAL]` — role order + `applyChoreo-compose`
+* `EchoGraded` `[REAL]` — `keep ≤ residue ≤ forget`
+* `EchoDecorationStructure` `[REAL]` — abstract recipe
+* Applications using it: `haplotype-collapsing` `[REAL]` Agda + `[DRAFT]` rest,
+  `compiler-analysis` `[DRAFT]`