docs+example: invariant-path as the echo-types application

classify_candidate is a non-injective classifier; the retained ClaimCandidate +
ClassificationOutcome.losses IS the echo (fiber) over a Classification. Adds a
runnable worked example + CI-covered integration tests (2 pass) showing two
distinct paths collapsing to Overextended with distinct retained losses, plus
docs/ECHO-TYPES.md mapping the estate's machine-checked Echo integration.

https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS

Author: claude

crates/invariant-path-core/examples/echo_structured_loss.rs

@@ -0,0 +1,75 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+//
+// Worked echo-types example: classification as fiber-based structured loss.
+//
+// Invariant Path's classifier
+//     classify_candidate : ClaimCandidate -> ClassificationOutcome
+// is a NON-INJECTIVE map: many distinct claim-paths collapse to the same
+// `Classification`. hyperpolymath/echo-types is the mechanised theory of
+// exactly this collapse — the fiber
+//     Echo f y  :=  Σ (x : A) , (f x ≡ y)
+// the proof-relevant record of *which* inputs map to y.
+//
+// This example materialises one echo: the fiber of `Overextended`. The bare
+// `Classification::Overextended` forgets which path produced it; Invariant
+// Path RETAINS the full candidate together with its `losses` — and that
+// retained structured loss IS the echo. Invariant Path is, in echo-types
+// terms, the runtime that keeps echoes instead of discarding them.
+//
+// Run:  cargo run -p invariant-path-core --example echo_structured_loss
+// See:  docs/ECHO-TYPES.md  and the Agda companion
+//       nextgen-typing/verification/proofs/agda/EchoTyping.agda
+
+use invariant_path_core::classifier::classify_candidate;
+use invariant_path_core::model::{ClaimCandidate, Classification, ClassificationOutcome, Span};
+
+/// Build a minimal candidate (spans are irrelevant to classification here).
+fn candidate(source: &str, target: &str, trigger: &str) -> ClaimCandidate {
+    ClaimCandidate {
+        span: Span { start: 0, end: 0 },
+        source_text: source.to_string(),
+        target_text: target.to_string(),
+        trigger: trigger.to_string(),
+        path_description: format!("{source}  ⟶  {target}"),
+    }
+}
+
+fn main() {
+    // Two genuinely different claim-paths …
+    let c1 = candidate("benchmark accuracy", "general capability", "therefore");
+    let c2 = candidate("the theorem proves", "production guarantee", "implies");
+
+    let o1 = classify_candidate(&c1);
+    let o2 = classify_candidate(&c2);
+
+    // … collapse to the SAME classification: the classifier is non-injective.
+    assert_eq!(o1.classification, Classification::Overextended);
+    assert_eq!(o2.classification, Classification::Overextended);
+    assert_ne!(c1, c2, "the two claim-paths are genuinely distinct");
+
+    // The echo (fiber over `Overextended`) is what Invariant Path RETAINS:
+    // the distinct candidates plus their distinct structured losses, which the
+    // bare `Classification` has forgotten.
+    let fiber: Vec<(ClaimCandidate, ClassificationOutcome)> = vec![(c1, o1), (c2, o2)];
+
+    println!("Echo(classify) over `Overextended` — the retained fiber:\n");
+    for (cand, out) in &fiber {
+        println!(
+            "  • {:<32}  losses = {:?}",
+            cand.path_description, out.losses
+        );
+    }
+
+    // Distinct losses ⇒ the classification truly dropped information the echo keeps.
+    assert_ne!(
+        fiber[0].1.losses, fiber[1].1.losses,
+        "each path's structured loss is distinct and retained"
+    );
+
+    println!(
+        "\nNon-injective: 2 distinct paths → 1 classification.\n\
+         The echo (candidate + losses) is the structured loss Invariant Path retains,\n\
+         and `path_description` is the section that recovers the source the verdict forgot."
+    );
+}

crates/invariant-path-core/tests/echo_structured_loss.rs

@@ -0,0 +1,54 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+//
+// CI-covered companion to examples/echo_structured_loss.rs.
+//
+// Pins the echo-types correspondence as a test: `classify_candidate` is a
+// non-injective classifier, and the fiber (echo) over a classification retains
+// the per-candidate structured loss that the bare `Classification` discards.
+// See docs/ECHO-TYPES.md.
+
+use invariant_path_core::classifier::classify_candidate;
+use invariant_path_core::model::{ClaimCandidate, Classification, Span};
+
+fn candidate(source: &str, target: &str, trigger: &str) -> ClaimCandidate {
+    ClaimCandidate {
+        span: Span { start: 0, end: 0 },
+        source_text: source.to_string(),
+        target_text: target.to_string(),
+        trigger: trigger.to_string(),
+        path_description: format!("{source} -> {target}"),
+    }
+}
+
+/// Two distinct claim-paths collapse to one classification: the classifier is
+/// non-injective, so the classification alone cannot recover the path.
+#[test]
+fn classification_is_non_injective() {
+    let c1 = candidate("benchmark accuracy", "general capability", "therefore");
+    let c2 = candidate("the theorem proves", "production guarantee", "implies");
+
+    let o1 = classify_candidate(&c1);
+    let o2 = classify_candidate(&c2);
+
+    assert_ne!(c1, c2);
+    assert_eq!(o1.classification, Classification::Overextended);
+    assert_eq!(o2.classification, Classification::Overextended);
+}
+
+/// The echo retains what the classification drops: distinct candidates over the
+/// same classification carry distinct, retained `losses` (the structured loss).
+#[test]
+fn echo_retains_structured_loss() {
+    let c1 = candidate("benchmark accuracy", "general capability", "therefore");
+    let c2 = candidate("the theorem proves", "production guarantee", "implies");
+
+    let o1 = classify_candidate(&c1);
+    let o2 = classify_candidate(&c2);
+
+    // same fiber (classification) …
+    assert_eq!(o1.classification, o2.classification);
+    // … but distinct, retained structured loss — the echo keeps it.
+    assert_ne!(o1.losses, o2.losses);
+    assert!(!o1.losses.is_empty() && !o2.losses.is_empty());
+}

docs/ECHO-TYPES.md

@@ -0,0 +1,78 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -->
+
+# Invariant Path × echo-types — structured loss as a first-class object
+
+Invariant Path is the **application example** of the
+[`echo-types`](https://github.com/hyperpolymath/echo-types) programme: it is a
+runtime that *keeps echoes instead of discarding them*.
+
+## The correspondence
+
+echo-types formalises **fiber-based structured loss**. For a function
+`f : A → B`, the *echo* of an output `y` is the fiber
+
+```
+Echo f y  :=  Σ (x : A) , (f x ≡ y)
+```
+
+— the proof-relevant record of **which** inputs `f` collapsed onto `y`. A
+non-injective `f` *forgets* that "which"; the echo is exactly what you must
+retain to recover it.
+
+Invariant Path's classifier is such an `f`:
+
+```rust
+classify_candidate : ClaimCandidate -> ClassificationOutcome
+```
+
+Many distinct claim-paths collapse to the same `Classification`
+(`ValidPath | Overextended | Conflation | Incomplete | Abstain`). The bare
+classification is the lossy codomain value; **the claim-path is the echo**.
+
+| echo-types                | Invariant Path                                   |
+|---------------------------|--------------------------------------------------|
+| `f : A → B` (lossy map)   | `classify_candidate` (claim-path → classification) |
+| codomain value `y`        | `Classification`                                 |
+| `Echo f y` (the fiber)    | the retained `ClaimCandidate` + `ClassificationOutcome` |
+| residue / structured loss | `ClassificationOutcome.losses : Vec<String>`     |
+| no-section (irreversible) | a `Classification` alone cannot recover its path |
+| the section that recovers | `Annotation.path_description` (retained provenance) |
+
+The domain model already names the loss: `ClassificationOutcome` carries
+`losses` and `preserved` precisely because a classification that *dropped* the
+path would be untraceable. echo-types is the mechanised backbone of that design
+choice — Invariant Path is "a claim-path debugger, not a truth engine" exactly
+because it stores echoes.
+
+## Worked example (runnable + tested)
+
+```bash
+cargo run -p invariant-path-core --example echo_structured_loss
+cargo test -p invariant-path-core --test echo_structured_loss
+```
+
+Two genuinely different claim-paths —
+`benchmark accuracy ⟶ general capability` and
+`the theorem proves ⟶ production guarantee` — both classify as `Overextended`,
+yet retain **distinct** structured losses (`task_transfer` vs
+`implementation_gap`). The classifier is non-injective; the echo keeps what it
+drops. See:
+
+- `crates/invariant-path-core/examples/echo_structured_loss.rs`
+- `crates/invariant-path-core/tests/echo_structured_loss.rs`
+
+## Cross-repo
+
+The same `Echo` underlies the type-system integration across the estate, all
+machine-checked under `--safe --without-K`:
+
+- **nextgen-typing** — `verification/proofs/agda/EchoTyping.agda`: affine
+  subtyping *is* echo `weaken`; refinement erasure *is* a fiber.
+- **nextgen-languages / kitchenspeak** — `proofs/agda/EchoBridge.agda`: the `@`
+  sensor witness *is* `Echo (fired …) true`.
+- **phronesis** — `academic/formal-verification/agda/PhronesisEcho.agda`: an
+  ethical verdict's provenance *is* `Echo verdict v`.
+
+Invariant Path is where that theory is *used*: a tool whose reason to exist is
+to retain the echo.