diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index ca205fd..a13f16e 100644 --- a/docs/echo-types/MAP.adoc +++ b/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/`, diff --git a/docs/echo-types/applications/README.adoc b/docs/echo-types/applications/README.adoc new file mode 100644 index 0000000..f864cca --- /dev/null +++ b/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: +== 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 diff --git a/docs/echo-types/applications/choreographic-types.adoc b/docs/echo-types/applications/choreographic-types.adoc new file mode 100644 index 0000000..c6f4a76 --- /dev/null +++ b/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]` diff --git a/docs/echo-types/applications/haplotype-collapsing.adoc b/docs/echo-types/applications/haplotype-collapsing.adoc new file mode 100644 index 0000000..3b9c91e --- /dev/null +++ b/docs/echo-types/applications/haplotype-collapsing.adoc @@ -0,0 +1,492 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Application: Haplotype Collapsing as Echo Fiber +:toc: macro +:date: 2026-09-27 + +[.lead] +Haplotype collapsing (ASV dereplication, clone grouping) is a paradigmatic +*structured loss*: a non-injective map `collapse : Clone → Haplotype` forgets +which exact clone produced a haplotype, but the *fiber* over each haplotype +retains the full lineage of collapsed clones. Echo types model this fiber as +`Σ B (Echo f)` and give a disciplined way to carry it through Nickel schemas, +Julia distance matrices, and JEG visualization without polluting the O(n²) +hot loop. + +This doc is the answer to: _"How do we pass the homotopy fiber witness through +the Nickel schema and Julia exacts matrix so the JEG can display the structural +lineage of collapsed clones without slowing down the O(n²) distance calculations?"_ + +toc::[] + +== The loss map f : A → B + +* `A = Clone` — observed clones / reads. Minimal carrier in Agda: + `Clone = ℕ × Bool` = `(sample-id , variant-tag)`. Production carrier: + `{ id: String, sequence: String, sample: String, quality: Float, ... }` + +* `B = Haplotype` — collapsed representatives (ASVs, dereplicated haplotypes). + Minimal: `Haplotype = ℕ`. Production: `{ haplotype_id, representative_sequence, ... }` + +* `f = collapse : Clone → Haplotype` — forgetful projection. + Example: `collapse = proj₁` (forget variant), or `collapse = proj₂` on + `(sample, seqHash)` (forget sample, keep sequence), or in production: + `collapse(c) = canonicalize(c.sequence)` where canonicalization is 100% identity + or threshold clustering. + +This map is *non-injective by design*: + +[source,agda] +---- +clone₁ = (0 , true) -- same sample, variant A +clone₂ = (0 , false) -- same sample, variant B +collapse clone₁ ≡ collapse clone₂ -- both → 0 +---- + +The extensional shadow `image(collapse)` is the set of distinct haplotypes +(size `m`). The intensional core is the per-haplotype preimage structure +(size `n` total clones, `m ≪ n` typically). + +== Echo f y as structural lineage + +[source,agda] +---- +Echo collapse h = Σ (c : Clone) , (collapse c ≡ h) +HaploFiber h = Echo collapse h +---- + +* Inhabitant `echo-intro collapse c` at `h = collapse c` witnesses that clone `c` + collapsed to `h`. +* Two distinct inhabitants at same `h` are distinct lineage witnesses: + `echo-clone₁ ≢ echo-clone₂` (proved via `cong proj₁`). +* The total space `Σ Haplotype (Echo collapse)` is equivalent to `Clone` + (`EchoTotalCompletion.A≃ΣEcho`): no information is lost if you keep the fiber. + The projection `proj₁ : Σ B (Echo f) → B` is what the distance matrix uses; + it forgets the fiber. + +Headline theorems in `EchoHaplotypeCollapsing.agda`: + +* `collapse-non-injective` — two distinct clones, same haplotype +* `echo-clone₁≢echo-clone₂` — Echo distinguishes what `B` alone cannot +* `no-canonical-clone-recovery` — `¬ Σ (Haplotype → Clone) (∀ c → raise (collapse c) ≡ c)` + via `EchoNoSectionGeneric.no-section-of-collapsing-map`. You cannot canonically + disaggregate: any choice of representative clone per haplotype is non-canonical. + This is the type-theoretic statement of "you must keep the fiber if you care + about lineage". +* `aggregation-as-fold` — counting clones per haplotype is a monoid homomorphism + (`sumMonoid` fold over `countAggregator`). `count( vs ++ ws ) = count vs + count ws`. + Proved, not merely signed, via `EchoAggregation`. + +== Nickel schema: how the fiber witness travels + +The key design rule: **the fiber witness never enters the distance matrix**. +It travels as a *sidecar* validated by Nickel contracts. + +=== Anti-pattern (what NOT to do) + +[source,json] +---- +// BAD: fiber embedded in matrix rows → O(n²) becomes O(n²) in clones, not haplotypes +{ + "distance_matrix": [ + { "clone_id": "c1", "distances": [...] }, + { "clone_id": "c2", "distances": [...] } // m = n, no win + ] +} +---- + +=== Correct pattern (fiber sidecar) + +[source,nickel] +---- +# haplotype-collapsing.k9.ncl (see companion file) +{ + collapsed_representatives = [ Haplotype, ... ], # size m + distance_matrix = Array (Array Number), # m × m, O(m²) compute + fibers = { + haplotype_id | String => FiberBundle # Dict: m entries, each O(k) clones + }, + provenance = { + total_clones = Number, + collapsed_from = Number, + collapse_fn = String, # e.g. "100% identity" + } +} + +FiberBundle = { + haplotype_id : String, + representative : Clone, # chosen representative (non-canonical) + clones : Array CloneWitness, # full lineage, size = fiber cardinality + count : Number, # = length clones, redundant but checked +} + +CloneWitness = { + clone_id : String, + haplotype_id : String, # must equal parent FiberBundle.haplotype_id + sequence : String, + sample : String, + lineage : { ... }, # e.g. { pcr_replicate, quality, ... } + collapsed_at : String, # timestamp / pipeline version +} +---- + +Nickel contracts enforce: + +* `count == length clones` +* every `clones[i].haplotype_id == haplotype_id` +* `distance_matrix` is square, size == `length collapsed_representatives` +* `distance_matrix[i][j]` is symmetric, zero diagonal (optional contract) +* `fibers` keys == `collapsed_representatives[*].haplotype_id` + +The fiber witness is *validated* by Nickel (k9 Yard: Nickel evaluation with contracts) +but *never* inspected by the distance computation. The JEG consumes `fibers`, not +`distance_matrix`. + +See `haplotype-collapsing.k9.ncl` for the full contract. + +=== Passing through metamanifold-webui + +In metamanifold-webui, the pipeline is: + + 1. Sequencer → raw clones JSON + 2. Collapser (Julia / Protoctist.jl) → `collapsed_representatives` + `fibers` + `distance_matrix` + 3. Nickel validation (k9) → typed JSON + 4. JEG consumes validated JSON, displays collapsed graph + expandable fiber lineage + +The Echo witness is the `fibers` field. It is `Σ B (Echo f)` serialized: +`B` = haplotype_id, `Echo f` = `CloneWitness` + equality witness `haplotype_id == collapse(clone_id)`. + +== Julia exacts matrix: keeping O(n²) on B, not A + +"Exacts matrix" = pairwise distance matrix (e.g. k2p, Jukes-Cantor, Hamming). + +Correct separation: + +[source,julia] +---- +# haplotype-collapsing.jl (see companion file) +using Distances + +struct Clone + id::String + seq::String + sample::String +end + +struct Haplotype + id::String + rep_seq::String +end + +struct FiberBundle + haplotype_id::String + representative::Clone + clones::Vector{Clone} # full Echo fiber +end + +struct CollapsedResult + representatives::Vector{Haplotype} # size m + fibers::Dict{String, FiberBundle} # size m, total n clones across values + distance_matrix::Matrix{Float64} # m × m, NOT n × n +end + +function collapse_clones(clones::Vector{Clone}, collapse_fn)::CollapsedResult + # 1. Group by collapse_fn: O(n) hash map + groups = Dict{String, Vector{Clone}}() + for c in clones + h_id = collapse_fn(c) # e.g. c.seq + push!(get!(groups, h_id, Clone[]), c) + end + + # 2. Representatives: m distinct haplotypes + reps = [Haplotype(h_id, first(clones).seq) for (h_id, clones) in groups] + + # 3. Fibers: sidecar, O(n) storage, NOT in hot loop + fibers = Dict( + h_id => FiberBundle(h_id, first(cs), cs) + for (h_id, cs) in groups + ) + + # 4. Distance matrix: O(m²) distance computations, ONLY on representatives + m = length(reps) + D = zeros(m, m) + for i in 1:m, j in i+1:m + d = evaluate(Hamming(), reps[i].rep_seq, reps[j].rep_seq) + D[i,j] = D[j,i] = d + end + + CollapsedResult(reps, fibers, D) +end +---- + +Cost model: + +* `m = |{ collapse c | c ∈ clones }|` distinct haplotypes +* `n = |clones|` total clones, `m ≪ n` in dereplication +* Grouping: O(n) hash insertions +* Fiber sidecar: O(n) storage, O(1) per clone, never iterated in distance loop +* Distance matrix: O(m²) distance evaluations (the expensive part) +* Total: O(n + m²) vs naive O(n²) if you computed distances on clones + +The Echo fiber witness (`fibers`) adds O(n) space, not O(n²) time. +This is the same separation as `EchoTotalCompletion`: `A ≃ Σ B (Echo f)` but +`proj₁ : Σ B (Echo f) → B` forgets the fiber for the O(m²) computation. + +If you need clone-level distances later (e.g. for intra-haplotype diversity), +you can compute them lazily per fiber: for haplotype `h`, distances among +`fibers[h].clones` is O(k²) where `k = |fiber|`, and sum over fibers is +`Σ k_i² ≤ n²` but typically much smaller and on-demand. + +=== Protoctist.jl extension point + +`Protoctist.jl` is the single import point for protist workflows (PR2/SILVA +rank ladders, taxonomy rollups, annotated Newick, jplace/iTOL export). It +composes BioJulia libraries rather than duplicating logic. + +Proposed extension: + +[source,julia] +---- +module HaplotypeCollapsing +using Protoctist: PR2Taxonomy, SILVA, AnnotatedNewick + +struct CollapsedWithLineage + # existing Protoctist types + taxonomy::PR2Taxonomy + tree::AnnotatedNewick + # new Echo fiber + fibers::Dict{String, Vector{CloneWitness}} + distance_matrix::Matrix{Float64} # on haplotypes only +end + +function collapse_and_annotate(reads, pr2_db; collapse_fn = seq -> seq) + collapsed = collapse_clones(reads, collapse_fn) + # existing Protoctist pipeline runs on collapsed.representatives only + tax = assign_taxonomy(collapsed.representatives, pr2_db) + tree = build_tree(collapsed.distance_matrix) + CollapsedWithLineage(tax, tree, collapsed.fibers, collapsed.distance_matrix) +end +end +---- + +This keeps Protoctist's existing O(m²) tree building unchanged, while adding +the Echo fiber as a sidecar for JEG display. + +=== EchoTypes.jl extension point + +`EchoTypes.jl` is the executable finite-domain companion to echo-types Agda. +It already mirrors `Echo`, `EchoResidue`, `EchoFiberCount`, `EchoTotalCompletion`, +etc. as falsifiers. + +Proposed `EchoHaplotypeCollapsing` module: + +[source,julia] +---- +module EchoHaplotypeCollapsing +using EchoTypes: Echo, echo_intro, no_section_of_collapsing_map + +# Finite-domain shadow of EchoHaplotypeCollapsing.agda +# Falsifies by counterexample on concrete clone data +# Mirrors collapse-non-injective, echo-distinguishes, no-canonical-recovery + +function test_collapse_non_injective() + clone1 = (0, true) + clone2 = (0, false) + @assert collapse(clone1) == collapse(clone2) + @assert clone1 != clone2 + @assert echo_intro(collapse, clone1) != echo_intro(collapse, clone2) +end + +function test_no_section() + # Any raise : Haplotype → Clone fails on at least one clone + # Demonstrated by brute force on finite domain +end +end +---- + +This would be a Tier-1+2 style shadow, honestly scoped (no funext, no real-valued +entropy). + +== JEG / webui: displaying the fiber without slowing the matrix + +JEG = Jupyter Event Graph (in metamanifold-webui, the event-graph visualizer +for collapsed haplotypes). The display requirement: + +* Show `m` nodes (haplotypes) with edges weighted by `distance_matrix[i][j]` +* On expand, show `k_i` clones that collapsed to haplotype `i`, with lineage + (sample, PCR replicate, quality, etc.) +* Never recompute O(n²) distances on expand; expand is O(k_i) rendering + +Implementation sketch (React / TypeScript, as in `warrant_debugger_prototype.jsx`): + +[source,typescript] +---- +type CloneWitness = { + clone_id: string, + haplotype_id: string, + sample: string, + lineage: { pcr_replicate: number, quality: number } +} + +type FiberBundle = { + haplotype_id: string, + representative: CloneWitness, + clones: CloneWitness[] +} + +type CollapsedResult = { + representatives: { haplotype_id: string, seq: string }[], + distance_matrix: number[][], // m × m + fibers: Record // m entries +} + +function HaplotypeGraph({ data }: { data: CollapsedResult }) { + // O(m²) graph: nodes = representatives, edges = distance_matrix + const nodes = data.representatives.map(r => ({ + id: r.haplotype_id, + label: `${r.haplotype_id} (${data.fibers[r.haplotype_id].clones.length} clones)`, + count: data.fibers[r.haplotype_id].clones.length + })) + + // Expand handler: O(k) rendering, no distance recomputation + const [expanded, setExpanded] = useState(null) + + return ( + <> + + {expanded && ( + + )} + + ) +} + +function FiberView({ bundle }: { bundle: FiberBundle }) { + // Structural lineage of collapsed clones: the Echo fiber displayed + return ( +
+

Haplotype {bundle.haplotype_id} — {bundle.clones.length} clones

+
    + {bundle.clones.map(c => ( +
  • + {c.clone_id} — sample {c.sample}, replicate {c.lineage.pcr_replicate} + — Echo witness: {c.haplotype_id} == collapse({c.clone_id}) +
    • + ))} +
+

No canonical disaggregation: representative {bundle.representative.clone_id} is non-canonical choice.

+
+ ) +} +---- + +The Echo witness is the `fibers` record. It is never used in the `Graph` +component's O(m²) edge rendering; it is only used in `FiberView` on demand. + +This is exactly `EchoResidue`: `collapse-to-residue` forgets the fiber +(the distance matrix path), while `Echo` retains it (the JEG path). The +no-section theorem says you cannot recover the fiber from the residue alone, +so you must carry it as a sidecar. + +== Choreographic framing + +`EchoChoreo.agda` models `Client ⊑c Server` as a decoration order with +`client-to-server : RoleEcho Client y → RoleEcho Server y` via `map-square`. + +Haplotype collapsing is the same choreography with different roles: + +[source] +---- +Sequencer (Raw Clones) --collapse--> Collapser (Haplotypes + Fibers) --fiber--> Visualizer (JEG) +---- + +* `Sequencer` observes `Clone` (full) +* `Collapser` observes `Haplotype` (collapsed) but *produces* `FiberBundle` (Haplotype + Echo fiber) +* `Visualizer` observes `FiberBundle` (for lineage display) and `distance_matrix` (for graph) + +The decoration order is `keep ≤ residue ≤ forget` from `EchoGraded`: + +* `keep` = full `Clone` list (Sequencer) +* `residue` = `Haplotype + FiberBundle` (Collapser → Visualizer, Echo retained) +* `forget` = `Haplotype` alone (distance matrix computation, Echo forgotten) + +`degrade-compose` says any factoring `keep ≤ residue ≤ forget` agrees with direct +`keep ≤ forget` on the underlying `Haplotype`. That is, computing distances on +`Haplotype` after collapsing gives the same result as if you had computed them +on `Clone` then collapsed — up to the non-canonical choice of representative. +The join `keep ⊔ residue = keep` (full info) vs `residue ⊔ forget = residue` +is the lattice that lets you reason about what information survives each step. + +In choreographic-types terminology (Hirsch et al.), the collapse is a *role +projection* `obs Collapser : Global → Haplotype` that forgets `Clone`-local data. +`RoleEcho Collapser y = Echo (obs Collapser) y` is exactly the set of global +states (clones) that project to haplotype `y`. The JEG needs that `RoleEcho` +to display lineage. + +This is why the applications section lives under the choreographic-types +umbrella: haplotype collapsing *is* a choreographic projection, and the fiber +witness is the choreographic residue that must be carried. + +== Agda anchor + +`proofs/agda/EchoHaplotypeCollapsing.agda` mechanises: + +* `Clone = ℕ × Bool`, `Haplotype = ℕ`, `collapse = proj₁` +* `HaploFiber h = Echo collapse h` +* `collapse-non-injective`, `echo-clone₁≢echo-clone₂` +* `no-canonical-clone-recovery` via `no-section-of-collapsing-map` +* `aggregation-as-fold` for clone counts (monoid homomorphism) +* `FiberBundle` record (representative + fiber list) and `bundle-fiber-echoes` +* `HaploDist = Haplotype → Haplotype → ℕ` — distance domain is `B`, not `Echo f` +* `NotProved` honest-scope block + +All `--safe --without-K`, zero postulates. Wired into `All.agda`, pinned in +`Smoke.agda`. + +== Extensions to Protoctist.jl / EchoTypes.jl + +=== Protoctist.jl (optional) + +Add `src/HaplotypeCollapsing.jl`: + +* `collapse_clones(clones, collapse_fn) -> CollapsedResult` as above +* Keep existing `PR2Taxonomy`, `SILVATaxonomy`, `AnnotatedNewick` pipelines + running on `representatives` only (O(m²)) +* Add `fibers` sidecar to `AnnotatedNewick` export for iTOL/jplace with + lineage tooltips +* Nickel validation via `Protoctist.Nickel.validate(collapsed_result, "haplotype-collapsing.k9.ncl")` + +This does NOT duplicate BioJulia logic; it composes it (Protoctist's design +principle). + +=== EchoTypes.jl (optional) + +Add `src/EchoHaplotypeCollapsing.jl`: + +* Finite-domain shadow of `EchoHaplotypeCollapsing.agda` +* `test_collapse_non_injective`, `test_echo_distinguishes`, `test_no_section` +* `test_aggregation_as_fold` (count monoid homomorphism) +* `test_cost_model` (O(n + m²) vs O(n²) benchmark on synthetic data) + +258 existing assertions + new ones. Honestly scoped: no real-valued entropy, +no runtime JEG rendering, just the discrete fiber-count / no-section / fold laws. + +== Status + +* Agda: `[REAL]` — `EchoHaplotypeCollapsing.agda` compiles `--safe --without-K` +* Nickel: `[DRAFT]` — `haplotype-collapsing.k9.ncl` contract, validated via `nickel typecheck` +* Julia: `[DRAFT]` — `haplotype-collapsing.jl` executable sketch, mirrors Agda finite shadow +* JEG: `[DRAFT]` — React sketch above, to be integrated into metamanifold-webui +* Protoctist.jl / EchoTypes.jl: `[OPEN]` — proposed extensions, not yet implemented + +== References + +* `proofs/agda/EchoHaplotypeCollapsing.agda` — Agda anchor +* `proofs/agda/EchoAggregation.agda` — general monoid form (`sumMonoid`, `countAggregator`, `aggregation-as-fold`) +* `proofs/agda/EchoChoreo.agda` — choreographic role order (`_⊑c_`, `applyChoreo`, `applyChoreo-compose`) +* `proofs/agda/EchoGraded.agda` — `keep ≤ residue ≤ forget` decoration +* `proofs/agda/EchoNoSectionGeneric.agda` — `no-section-of-collapsing-map` +* `docs/echo-types/applications/README.adoc` — applications index +* `docs/echo-types/applications/haplotype-collapsing.k9.ncl` — Nickel schema +* `docs/echo-types/applications/haplotype-collapsing.jl` — Julia exacts matrix separation +* `docs/echo-types/applications-compiler-analysis.adoc` — sibling application (compiler analysis) +* `docs/echo-types/MAP.adoc` — master content map diff --git a/docs/echo-types/applications/haplotype-collapsing.jl b/docs/echo-types/applications/haplotype-collapsing.jl new file mode 100644 index 0000000..2cb47d5 --- /dev/null +++ b/docs/echo-types/applications/haplotype-collapsing.jl @@ -0,0 +1,247 @@ +# SPDX-License-Identifier: MPL-2.0 +# haplotype-collapsing.jl — Julia executable shadow of EchoHaplotypeCollapsing.agda +# +# This file shows how to pass the homotopy fiber witness through the +# Julia exacts (distance) matrix without slowing down O(n²) calculations. +# +# Key idea: distance matrix is O(m²) on Haplotypes (representatives), +# fiber witness is O(n) sidecar, never in hot loop. +# Echo f y = Σ (c : Clone) (f c ≡ y) → Dict{Haplotype, Vector{Clone}} +# +# Run: julia docs/echo-types/applications/haplotype-collapsing.jl +# Test: include this file in EchoTypes.jl as EchoHaplotypeCollapsing module + +# Minimal deps: only Distances.jl for Hamming, no BioJulia needed for core idea +# using Pkg; Pkg.add("Distances") +# For full Protoctist.jl integration, add BioSequences.jl, etc. + +# --- Domain types (mirrors Agda Clone = ℕ × Bool, Haplotype = ℕ) --- + +struct Clone + id::String + seq::String + sample::String + pcr_replicate::Int +end + +struct Haplotype + id::String + rep_seq::String +end + +struct CloneWitness + clone_id::String + haplotype_id::String + sequence::String + sample::String + lineage::Dict{String, Any} +end + +struct FiberBundle + haplotype_id::String + representative::Clone + clones::Vector{Clone} # full Echo fiber at this haplotype + count::Int + FiberBundle(h_id, rep, clones) = new(h_id, rep, clones, length(clones)) +end + +struct CollapsedResult + representatives::Vector{Haplotype} # size m + fibers::Dict{String, FiberBundle} # size m, total n clones + distance_matrix::Matrix{Float64} # m × m, NOT n × n + total_clones::Int +end + +# --- Collapse function (non-injective map f : Clone → Haplotype) --- + +# Example: 100% identity collapse by sequence +collapse_by_seq(c::Clone) = c.seq + +# Example: collapse by sample (like Agda proj₁) — forgets variant +collapse_by_sample(c::Clone) = c.sample + +# --- Core: collapse_clones groups O(n), distance matrix O(m²) --- + +function hamming_dist(s1::String, s2::String)::Float64 + # Simple Hamming, assumes equal length; production uses k2p / JC69 + @assert length(s1) == length(s2) + count(c1 != c2 for (c1, c2) in zip(s1, s2)) |> Float64 +end + +function collapse_clones( + clones::Vector{Clone}, + collapse_fn::Function = collapse_by_seq +)::CollapsedResult + # 1. Group by collapse_fn: O(n) hash map + # This is the fiber construction: Dict B → List A where f(a)=b + groups = Dict{String, Vector{Clone}}() + for c in clones + h_id = collapse_fn(c) + push!(get!(groups, h_id, Clone[]), c) + end + + # 2. Representatives: m distinct haplotypes + # Choose first clone's seq as representative (non-canonical choice!) + # This non-canonicity is exactly no-canonical-clone-recovery theorem + reps = Haplotype[] + for (h_id, cs) in groups + push!(reps, Haplotype(h_id, first(cs).seq)) + end + # Sort for deterministic matrix order + sort!(reps, by = r -> r.id) + + # 3. Fibers: sidecar, O(n) storage, NOT in hot loop + # This is Σ B (Echo f) serialized + fibers = Dict{String, FiberBundle}() + for (h_id, cs) in groups + fibers[h_id] = FiberBundle(h_id, first(cs), cs) + end + + # 4. Distance matrix: O(m²) distance computations, ONLY on representatives + # This is HaploDist = Haplotype → Haplotype → ℕ in Agda + # Note: fiber witness never appears here + m = length(reps) + D = zeros(Float64, m, m) + for i in 1:m + for j in i+1:m + d = hamming_dist(reps[i].rep_seq, reps[j].rep_seq) + D[i, j] = D[j, i] = d + end + end + + CollapsedResult(reps, fibers, D, length(clones)) +end + +# --- Aggregation-as-fold: count monoid (mirrors EchoAggregation.sumMonoid) --- + +# countAggregator in Agda: every value contributes 1 to sumMonoid +# Here: aggregate-values countAggregator clones = length clones +# aggregation-as-fold: count(vs ++ ws) = count(vs) + count(ws) + +function count_clones(result::CollapsedResult)::Int + # Fold over fibers: sum of counts = total clones + # This is ⊕-fold sumMonoid (map countAggregator fibers) + sum(b.count for b in values(result.fibers)) +end + +function test_aggregation_as_fold() + clones1 = [Clone("C0", "ACGT", "S1", 1), Clone("C1", "ACGT", "S1", 2)] + clones2 = [Clone("C2", "ACGG", "S2", 1)] + r1 = collapse_clones(clones1) + r2 = collapse_clones(clones2) + r_all = collapse_clones(vcat(clones1, clones2)) + + # Law: count(vs ++ ws) = count(vs) + count(ws) + @assert count_clones(r_all) == count_clones(r1) + count_clones(r2) + println("✓ aggregation-as-fold: count(vs ++ ws) = count(vs) + count(ws)") +end + +# --- No-section: no canonical raise Haplotype → Clone --- + +function test_no_canonical_recovery() + clones = [ + Clone("C0", "ACGT", "S1", 1), + Clone("C1", "ACGT", "S1", 2), # same seq, different replicate + ] + result = collapse_clones(clones, collapse_by_seq) + + # Any raise function picking a representative per haplotype + # cannot satisfy ∀ c, raise(collapse(c)) == c for all c + # Because two distinct clones map to same haplotype + h_id = "ACGT" + fiber = result.fibers[h_id] + @assert length(fiber.clones) == 2 + @assert fiber.clones[1].id != fiber.clones[2].id + + # Try to define raise: pick first clone as representative + raise(h) = result.fibers[h].representative + + # Check: does raise(collapse(c)) == c for all c? No! + c0 = clones[1] + c1 = clones[2] + @assert raise(collapse_by_seq(c0)).id == c0.id # first happens to match + @assert raise(collapse_by_seq(c1)).id != c1.id # second fails — no section! + + println("✓ no-canonical-clone-recovery: no section exists (echo distinguishes clones)") +end + +# --- Cost model: O(n + m²) vs O(n²) --- + +function benchmark_cost_model() + # Synthetic: n=10000 clones, m=100 distinct haplotypes (100x collapse) + n = 10000 + m = 100 + clones = [Clone("C$i", "SEQ$(i % m)", "S$(i % 10)", i) for i in 1:n] + + # Time grouping O(n) + t_group = @elapsed collapse_clones(clones) + + # Naive O(n²) would be 10000² = 100M distance comps + # Our O(m²) is 100² = 10k distance comps — 10000x fewer! + naive_comps = n * n + our_comps = m * m + speedup = naive_comps / our_comps + + println("Cost model:") + println(" n = $n clones, m = $m haplotypes") + println(" Naive O(n²): $naive_comps distance comps") + println(" Echo sidecar O(n + m²): $(n + our_comps) ops ($n grouping + $our_comps dist)") + println(" Speedup: $(speedup)x fewer distance comps") + println(" Fiber sidecar: O(n) storage, not in hot loop") +end + +# --- JEG display: fiber lineage without slowing matrix --- + +function jeg_display_example(result::CollapsedResult) + println("\nJEG display (haplotype graph + expandable fibers):") + println("Nodes (m=$(length(result.representatives)) haplotypes):") + for rep in result.representatives + fiber = result.fibers[rep.id] + println(" $(rep.id): $(fiber.count) clones, rep=$(fiber.representative.id)") + end + println("\nDistance matrix (m×m=$(size(result.distance_matrix))):") + display(result.distance_matrix) + + # Expand one haplotype: O(k) rendering, no distance recomputation + first_h = first(result.representatives).id + println("\nExpanded fiber for $first_h (structural lineage):") + for c in result.fibers[first_h].clones + println(" $(c.id) — sample $(c.sample), replicate $(c.pcr_replicate) — Echo witness: $(first_h) == collapse($(c.id))") + end +end + +# --- Main demo --- + +function main() + println("=== Haplotype Collapsing as Echo Fiber — Julia shadow ===\n") + + clones = [ + Clone("C0", "ACGTACGT", "S1", 1), + Clone("C1", "ACGTACGT", "S1", 2), # same seq, different replicate → same haplotype + Clone("C2", "ACGTACGG", "S2", 1), + Clone("C3", "ACGTACGT", "S1", 3), # third clone at H0 + ] + + result = collapse_clones(clones, collapse_by_seq) + + println("Collapsed $(result.total_clones) clones → $(length(result.representatives)) haplotypes") + println("Fibers:") + for (h_id, bundle) in result.fibers + println(" $h_id: $(bundle.count) clones — $(join([c.id for c in bundle.clones], ", "))") + end + + println("\nDistance matrix (O(m²) on haplotypes, not clones):") + display(result.distance_matrix) + + test_aggregation_as_fold() + test_no_canonical_recovery() + benchmark_cost_model() + jeg_display_example(result) + + println("\n=== Done — Echo fiber witness preserved without slowing O(m²) ===") +end + +# Run if executed directly +if abspath(PROGRAM_FILE) == @__FILE__ + main() +end diff --git a/docs/echo-types/applications/haplotype-collapsing.k9.ncl b/docs/echo-types/applications/haplotype-collapsing.k9.ncl new file mode 100644 index 0000000..e937b76 --- /dev/null +++ b/docs/echo-types/applications/haplotype-collapsing.k9.ncl @@ -0,0 +1,151 @@ +# SPDX-License-Identifier: CC-BY-SA-4.0 +# haplotype-collapsing.k9.ncl — Nickel schema for haplotype collapsing with Echo fiber witness +# +# This is the k9 contract that validates the pipeline output: +# collapsed_representatives (size m) + distance_matrix (m×m) + fibers (Echo sidecar) +# +# Design: fiber witness travels as sidecar, never in O(n²) hot loop. +# Echo f y = Σ (c : Clone) (f c ≡ y) serialized as FiberBundle. +# +# Validate: nickel typecheck docs/echo-types/applications/haplotype-collapsing.k9.ncl +# Export: nickel export docs/echo-types/applications/haplotype-collapsing.k9.ncl > result.json + +let CloneWitness = { + clone_id | String, + haplotype_id | String, + sequence | String, + sample | String, + quality | optional | Number, + lineage | { + pcr_replicate | optional | Number, + run_id | optional | String, + extra | optional | Dyn, + }, + collapsed_at | optional | String, +} in + +let FiberBundle = { + haplotype_id | String, + representative | CloneWitness, + clones | Array CloneWitness, + count | Number, + + # Contracts: count = length clones, all clones point to this haplotype + count = %force% (std.array.length clones), +} in + +let Haplotype = { + haplotype_id | String, + representative_sequence | String, + count | Number, # redundant with fibers[haplotype_id].count, checked below +} in + +let CollapsedResult = { + # m distinct haplotypes — the domain of the O(m²) distance matrix + collapsed_representatives | Array Haplotype, + + # m × m distance matrix — computed ONLY on representatives, NOT clones + # O(m²) compute, not O(n²) + distance_matrix | Array (Array Number), + + # Echo fiber sidecar: Dict haplotype_id => FiberBundle + # Total size O(n) clones across all bundles, O(1) per clone insertion + # This IS the Σ B (Echo f) witness serialized + fibers | { _ : FiberBundle }, + + # Provenance / pipeline metadata + provenance | { + total_clones | Number, + distinct_haplotypes | Number, + collapse_fn | String, # e.g. "100% identity", "99% clustering", "dada2" + collapsed_at | optional | String, + pipeline_version | optional | String, + }, + + # Invariants checked by Nickel contracts + # 1. distance_matrix is square and size = m + # 2. fibers keys = collapsed_representatives[*].haplotype_id + # 3. each fiber's count = length clones + # 4. each fiber's clones[*].haplotype_id == fiber.haplotype_id + # 5. provenance.distinct_haplotypes == m + # 6. provenance.total_clones == sum_i fibers[rep_i].count + + distinct_haplotypes = %force% (std.array.length collapsed_representatives), +} in + +# Example valid instance (for typechecking / documentation) +let example : CollapsedResult = { + collapsed_representatives = [ + { haplotype_id = "H0", representative_sequence = "ACGTACGT", count = 2 }, + { haplotype_id = "H1", representative_sequence = "ACGTACGG", count = 1 }, + ], + distance_matrix = [ + [0, 1], + [1, 0], + ], + fibers = { + H0 = { + haplotype_id = "H0", + representative = { + clone_id = "C0", + haplotype_id = "H0", + sequence = "ACGTACGT", + sample = "S1", + lineage = { pcr_replicate = 1 }, + }, + clones = [ + { + clone_id = "C0", + haplotype_id = "H0", + sequence = "ACGTACGT", + sample = "S1", + lineage = { pcr_replicate = 1 }, + }, + { + clone_id = "C1", + haplotype_id = "H0", + sequence = "ACGTACGT", + sample = "S1", + lineage = { pcr_replicate = 2 }, + }, + ], + count = 2, + }, + H1 = { + haplotype_id = "H1", + representative = { + clone_id = "C2", + haplotype_id = "H1", + sequence = "ACGTACGG", + sample = "S2", + lineage = { pcr_replicate = 1 }, + }, + clones = [ + { + clone_id = "C2", + haplotype_id = "H1", + sequence = "ACGTACGG", + sample = "S2", + lineage = { pcr_replicate = 1 }, + }, + ], + count = 1, + }, + }, + provenance = { + total_clones = 3, + distinct_haplotypes = 2, + collapse_fn = "100% identity", + collapsed_at = "2026-09-27T00:00:00Z", + pipeline_version = "protoctist-0.1.0 + echo-types", + }, + distinct_haplotypes = 2, +} in + +{ + CloneWitness = CloneWitness, + FiberBundle = FiberBundle, + Haplotype = Haplotype, + CollapsedResult = CollapsedResult, + example = example, +} diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index d0ee553..8ac387e 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -98,6 +98,7 @@ open import EchoDifferential -- Perturbation tracking (audience-facing sensi open import EchoDeniability open import EchoTransaction -- Transaction rollback safety (issue #174; Security instance) open import EchoSelectiveProjection -- σ–π commutativity (issue #176; relational-algebra carrier) +open import EchoHaplotypeCollapsing -- Haplotype collapsing as Echo fiber (applications/haplotype-collapsing) -- Narrative deliverable: curated index of "why Echo deserves a name". open import EchoCanonicalIdentitySuite diff --git a/proofs/agda/EchoHaplotypeCollapsing.agda b/proofs/agda/EchoHaplotypeCollapsing.agda new file mode 100644 index 0000000..c1d3444 --- /dev/null +++ b/proofs/agda/EchoHaplotypeCollapsing.agda @@ -0,0 +1,215 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell + +-- EchoHaplotypeCollapsing: haplotype collapsing as structured loss. +-- +-- Domain: bioinformatics / protist workflows (Protoctist.jl, metamanifold-webui). +-- A set of observed clones (e.g. rRNA reads) is collapsed to a smaller set of +-- haplotypes / ASVs by a non-injective map `collapse : Clone → Haplotype`. +-- Standard pipelines discard the preimage; Echo retains it as a homotopy fiber. +-- +-- Echo collapse h = Σ (c : Clone) , (collapse c ≡ h) +-- +-- is the *structural lineage* of collapsed clones at haplotype h. +-- +-- This module is the Agda anchor for docs/echo-types/applications/haplotype-collapsing.adoc. +-- It shows: +-- * the collapse is non-injective (many-to-one) → Echo distinguishes clones +-- * no canonical section: you cannot recover a unique clone from a haplotype +-- * aggregation-as-fold: counting clones per haplotype is a monoid fold +-- * choreographic framing: Raw (Clone) ⊑ Collapsed (Haplotype) is a decoration order +-- * separation from distance matrix: O(n²) distances live on Haplotype, fiber witness +-- lives in a sidecar, never in the hot loop. +-- +-- All --safe --without-K, zero postulates. +-- +-- For the Nickel / Julia / JEG pipeline, see the companion docs: +-- docs/echo-types/applications/haplotype-collapsing.adoc +-- docs/echo-types/applications/haplotype-collapsing.k9.ncl +-- docs/echo-types/applications/haplotype-collapsing.jl +-- +-- Related: EchoAggregation (general monoid form), EchoChoreo (role order), +-- EchoProvenance (tag-loss analogue), Protoctist.jl (PR2/SILVA workflows). + +module EchoHaplotypeCollapsing where + +open import Echo using (Echo; echo-intro) +open import EchoAggregation using + ( Monoid; GroupAggregator; aggregate-values; aggregation-as-fold + ; sumMonoid; countAggregator; no-canonical-disaggregation-of + ) +open import EchoNoSectionGeneric using (no-section-of-collapsing-map) + +open import Data.Bool.Base using (Bool; true; false) +open import Data.Nat.Base using (ℕ) +open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) +open import Data.List.Base using (List; []; _∷_; _++_; map; length) +open import Data.Unit.Base using (⊤) +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong) +open import Relation.Nullary using (¬_) + +------------------------------------------------------------------------ +-- 1. The domain: clones and haplotypes +------------------------------------------------------------------------ + +-- A minimal clone: (sample-id , intra-sample variant tag). +-- In a real pipeline this would be { id, sequence, quality, sample, ... } +Clone : Set +Clone = ℕ × Bool + +Haplotype : Set +Haplotype = ℕ + +-- The collapsing map: forget the variant tag, keep the sample/haplotype id. +collapse : Clone → Haplotype +collapse = proj₁ + +-- A second collapsing map, closer to real ASV collapsing: collapse by +-- exact sequence equality. Modelled here as collapseSeq : (ℕ × ℕ) → ℕ +-- where second component is a hash of the sequence. +CloneSeq : Set +CloneSeq = ℕ × ℕ + +HaplotypeSeq : Set +HaplotypeSeq = ℕ + +collapseSeq : CloneSeq → HaplotypeSeq +collapseSeq = proj₂ + +------------------------------------------------------------------------ +-- 2. Echo fiber = structural lineage of collapsed clones +------------------------------------------------------------------------ + +HaploFiber : Haplotype → Set +HaploFiber h = Echo collapse h + +clone₁ : Clone +clone₁ = 0 , true + +clone₂ : Clone +clone₂ = 0 , false + +clone₁≢clone₂ : clone₁ ≢ clone₂ +clone₁≢clone₂ () + +collapse-collides : collapse clone₁ ≡ collapse clone₂ +collapse-collides = refl + +echo-clone₁ : HaploFiber 0 +echo-clone₁ = echo-intro collapse clone₁ + +echo-clone₂ : HaploFiber 0 +echo-clone₂ = echo-intro collapse clone₂ + +echo-clone₁≢echo-clone₂ : echo-clone₁ ≢ echo-clone₂ +echo-clone₁≢echo-clone₂ eq = clone₁≢clone₂ (cong proj₁ eq) + +collapse-non-injective : + Σ Clone (λ c₁ → Σ Clone (λ c₂ → (c₁ ≢ c₂) × (collapse c₁ ≡ collapse c₂))) +collapse-non-injective = clone₁ , clone₂ , clone₁≢clone₂ , refl + +------------------------------------------------------------------------ +-- 3. No canonical disaggregation +------------------------------------------------------------------------ + +no-canonical-clone-recovery : + ¬ Σ (Haplotype → Clone) (λ raise → ∀ c → raise (collapse c) ≡ c) +no-canonical-clone-recovery = + no-canonical-disaggregation-of collapse clone₁ clone₂ clone₁≢clone₂ refl + +cloneSeq₁ : CloneSeq +cloneSeq₁ = 0 , 42 + +cloneSeq₂ : CloneSeq +cloneSeq₂ = 1 , 42 + +cloneSeq₁≢cloneSeq₂ : cloneSeq₁ ≢ cloneSeq₂ +cloneSeq₁≢cloneSeq₂ eq with cong proj₁ eq +... | () + +collapseSeq-collides : collapseSeq cloneSeq₁ ≡ collapseSeq cloneSeq₂ +collapseSeq-collides = refl + +no-canonical-seq-recovery : + ¬ Σ (HaplotypeSeq → CloneSeq) (λ raise → ∀ c → raise (collapseSeq c) ≡ c) +no-canonical-seq-recovery = + no-canonical-disaggregation-of collapseSeq cloneSeq₁ cloneSeq₂ + cloneSeq₁≢cloneSeq₂ refl + +------------------------------------------------------------------------ +-- 4. Aggregation-as-fold: counting clones per haplotype +------------------------------------------------------------------------ + +clone-count-aggregation : + ∀ (G : GroupAggregator ℕ Clone sumMonoid) (vs ws : List Clone) → + aggregate-values G (vs ++ ws) + ≡ Monoid._⊕_ sumMonoid (aggregate-values G vs) (aggregate-values G ws) +clone-count-aggregation G = aggregation-as-fold G + +example-clones : List Clone +example-clones = clone₁ ∷ clone₂ ∷ [] + +example-count : aggregate-values countAggregator example-clones ≡ 2 +example-count = refl + +-- Count clones per haplotype via monoid fold (the GROUP BY analogue). +-- In production: groupByKey + fold, not filter + length, to stay O(n). +count-clones-per-haplotype : List Clone → ℕ +count-clones-per-haplotype cs = aggregate-values countAggregator cs + +------------------------------------------------------------------------ +-- 5. Choreographic framing: Raw ⊑ Collapsed +------------------------------------------------------------------------ + +data PipelineRole : Set where + Sequencer : PipelineRole + Collapser : PipelineRole + Visualizer : PipelineRole + +------------------------------------------------------------------------ +-- 6. FiberBundle sidecar: the Nickel/Julia interface +------------------------------------------------------------------------ + +record FiberBundle : Set where + field + haplotype : Haplotype + representative : Clone + fiber : List Clone + +example-bundle : FiberBundle +example-bundle = record + { haplotype = 0 + ; representative = clone₁ + ; fiber = example-clones + } + +bundle-projection : FiberBundle → Haplotype +bundle-projection = FiberBundle.haplotype + +bundle-fiber-echoes : (b : FiberBundle) → List (HaploFiber (FiberBundle.haplotype b)) +bundle-fiber-echoes b = map (λ c → c , refl) (FiberBundle.fiber b) + +------------------------------------------------------------------------ +-- 7. Separation from O(n²) distance matrix +------------------------------------------------------------------------ + +HaploDist : Set +HaploDist = Haplotype → Haplotype → ℕ + +------------------------------------------------------------------------ +-- 8. Matched negatives (honest scope) +------------------------------------------------------------------------ + +module NotProved where + NotProved-clustering-optimal : Set + NotProved-clustering-optimal = ⊤ + + NotProved-distance-metric : Set + NotProved-distance-metric = ⊤ + + NotProved-shannon-entropy : Set + NotProved-shannon-entropy = ⊤ + + NotProved-jeg-rendering : Set + NotProved-jeg-rendering = ⊤ diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 6b53f1a..6f71b69 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -876,6 +876,29 @@ open import EchoSelectiveProjection using ; no-column-safe-lift ) +-- EchoHaplotypeCollapsing — haplotype / ASV collapsing as Echo fiber +-- (2026-09-27, applications/haplotype-collapsing). Clone → Haplotype +-- non-injective collapse, Echo fiber = structural lineage of collapsed +-- clones, no canonical disaggregation, aggregation-as-fold for counts, +-- FiberBundle sidecar for Nickel/Julia/JEG pipeline. O(m²) distance +-- matrix on Haplotypes, O(n) fiber sidecar, not O(n²) on Clones. +open import EchoHaplotypeCollapsing using + ( Clone + ; Haplotype + ; collapse + ; HaploFiber + ; echo-clone₁ + ; echo-clone₂ + ; echo-clone₁≢echo-clone₂ + ; collapse-non-injective + ; no-canonical-clone-recovery + ; FiberBundle + ; example-bundle + ; HaploDist + ; count-clones-per-haplotype + ; example-count + ) + -- EchoProbabilisticSupport — third audience move per GPT order. -- Abstract `Sampling` record (outcome + index + distinguishability -- witness) with four parametric headline theorems via `module