docs: tidy after earn-back closure + theory-work closure + examples cluster landed

Three small accuracy passes through `docs/echo-types/`:

1. `roadmap.md` §"Theory work — no proof assistant needed" — the
   section is now genuinely closed. Updated two stale items:
   * Axis 8 line said "the *decidability-respecting* candidate has
     shipped" and listed the other three as still candidate
     refinements. All four have now shipped: EchoDecidable
     (decidability), EchoCost (cost-indexed, #85), EchoAccess
     (graded access, #68/#75), EchoSearch (witness-search, #80).
   * Negative / co-echoes line was [unblocked]; now [landed] —
     AntiEcho (#69), tropical decomposition concrete + generic
     (#72 + #91), antiecho-partition-dec (#90). Names the
     obligation-5 / obligation-6 closures explicitly.

2. `roadmap.md` §"Example work" — three [unblocked] items now
   [landed]: ex. 5 (EchoExampleProvenance, #81), ex. 9
   (EchoExampleParser, #83), ex. 10 (EchoExampleAbsInt, #82). Only
   ex. 6 (approximate-echo numeric example) remains [unblocked].

3. `earn-back-plan.adoc`:
   * Header note "the gate discipline was historically attributed
     to a `roadmap-gates.adoc`; that file does not exist in-tree"
     is stale — the file IS in tree (created 2026-05-18). Header
     rewritten to list `roadmap-gates.adoc` alongside
     `retractions.adoc` / this plan / `next-questions.adoc` as the
     four canonical loci.
   * Ledger row D ("roadmap-gates.adoc does not exist") marked
     CLOSED 2026-05-20; cite reflects current reality.

Pure prose / docs only. No Agda content changes. `agda
proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit 0
under `--safe --without-K` (verified — confirms the docs say what
the code does).

Refs the closure side of #84 / #86 / #88 / #90 / #91 — does not
modify any Agda module, does not move any earned-back / retracted
claim.

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

Author: hyperpolymath

docs/echo-types/earn-back-plan.adoc

@@ -12,11 +12,13 @@ claims back into theorems — or to confirm, on the project's own gate
 discipline, that they cannot be earned. Nothing in `paper.adoc` /
 `conservativity.adoc` / `types-abstract.adoc` moves until the
 corresponding gate here passes. Methodology — explicit pass/fail,
-abandon criteria, outcomes logged in `docs/retractions.adoc`. (The
-gate discipline was historically attributed to a `roadmap-gates.adoc`;
-that file does not exist in-tree — see proof-debt ledger item *D*
-below. The canonical loci are `docs/retractions.adoc`, this plan, and
-`docs/next-questions.adoc`.)
+abandon criteria, outcomes logged in `docs/retractions.adoc`. The
+canonical loci of the gate discipline are
+`docs/roadmap-gates.adoc` (the protocol document, created 2026-05-18
+to resolve the earlier dangling reference), `docs/retractions.adoc`
+(the append-only retraction + earn-back log), this plan (the
+falsifiable program), and `docs/next-questions.adoc` (the open
+questions register).
 
 toc::[]
 
@@ -237,11 +239,15 @@ single index; it moves no claim.
   Completeness nice-to-have, lowest priority.
 
 | D
-| Doc-integrity: `docs/roadmap-gates.adoc` is cited as the canonical
-  gate ledger by ≥7 docs but does not exist in-tree. Role now split
-  across `retractions.adoc` / this plan / `next-questions.adoc`.
-| Open drift vector. Cheap to reconcile (back-link the citing docs;
-  do not fabricate retroactive gate history).
+| Doc-integrity: previously this entry recorded that
+  `docs/roadmap-gates.adoc` was cited as the canonical gate ledger
+  but did not exist in-tree. The file *does* exist (created
+  2026-05-18; see its preamble) and the dangling-reference issue is
+  resolved.
+| *CLOSED 2026-05-20.* `docs/roadmap-gates.adoc` is in tree as the
+  Gates Protocol. The canonical-loci list at the top of this plan
+  has been updated to include it explicitly alongside
+  `retractions.adoc` / `next-questions.adoc`.
 
 | E1
 | `examples/Transport.agda` (Gate-3): two disclosed open items, both

docs/echo-types/roadmap.md

@@ -37,17 +37,23 @@ Paths marked **[unblocked]** can proceed today. Paths marked
   lane C tracks the `taxonomy.md` §Axis-2 write-up).
 - **[landed]** Axis 8 (information-theoretic vs computational
   access): promoted from the candidates list to a numbered axis.
-  *Three* remaining candidate refinements of `Echo`
-  (cost-indexed, graded access modality, witness-search abstract
-  machine); the *decidability-respecting* candidate has shipped
-  as `proofs/agda/EchoDecidable.agda` (`EchoDec f y = Dec (Echo f
-  y)` with six headline lemmas including `echo-dec-intro`,
-  `echo-dec-fin`, `echo-dec-compose-iso`; see `taxonomy.md` §8).
-  Follow-up: pick one of the remaining three refinements and
-  formalise.
-- **[unblocked]** Negative / co-echoes: formulate `CoEcho(f)` and its
-  relationship to `Echo(f)`. Possibly resolves the quantitative /
-  structural tension hinted at by `EchoTropical`.
+  Every candidate refinement is now mechanised. Decidability-
+  respecting: `proofs/agda/EchoDecidable.agda`. Cost-indexed (over
+  an abstract `CostAlgebra`): `EchoCost.agda` + `EchoCostInstance.agda`
+  (PR #85). Graded access modality: `EchoAccess.agda` (PRs #68 +
+  #75). Witness-search abstract machine: `EchoSearch.agda` +
+  `EchoSearchInstance.agda` (PR #80). See `taxonomy.md` §8.
+- **[landed]** Negative / co-echoes: `AntiEcho f y := Σ A (λ x → f x ≢ y)`
+  shipped as `proofs/agda/AntiEcho.agda` (PR #69) with
+  `antiecho-{intro, disjoint, map-over}`, plus per-element
+  classification `antiecho-partition-dec` (PR #90, closes
+  `coecho.md` §5 obligation 5). Distinct from `EchoFiberTriangulation.CoEcho`
+  (which is the trivial opposite-orientation fibre); see naming
+  rationale in `AntiEcho.agda`'s preamble. The tropical decomposition
+  `TropEcho y ↔ Echo score y × (∀ z → y ≤ score z)` lands at the
+  concrete ℕ-scored level in `AntiEchoTropical.agda` (PR #72) and at
+  an abstract `OrderedCodomain` interface in `AntiEchoTropicalGeneric.agda`
+  (PR #91, closes `coecho.md` §5 obligation 6).
 - **[ruled out — see docs/echo-types/decisions/no-2-cat.adoc]**
   2-categorical shape. Every would-be 2-cell in the landed code
   is `refl` or forced trivial by propositionality (`≤g-prop`,
@@ -178,14 +184,20 @@ Paths marked **[unblocked]** can proceed today. Paths marked
 
 - **[unblocked]** Complete worked numeric example (ex. 6) with the
   approximate-echo shape, once the definition lands.
-- **[unblocked]** Parser residue example (ex. 9) as a toy Agda
-  example: parse of balanced parens, echo carries token stream.
-- **[unblocked]** Abstract-interpretation example (ex. 10) via a
-  Sign lattice.
-- **[unblocked]** Database provenance example (ex. 5) via
-  K-provenance semiring — text-only pass first, Agda optional.
-- **[unblocked]** Extend `EchoExamples.agda` with two to three
-  further canonical entries.
+- **[landed]** Parser residue example (ex. 9) — `EchoExampleParser.agda`
+  (PR #83): balanced parens, Boolean shadow `parses : List Token →
+  Bool` non-injective on `(())` vs `()()`, echo retains the token
+  stream.
+- **[landed]** Abstract-interpretation example (ex. 10) —
+  `EchoExampleAbsInt.agda` (PR #82): Sign lattice `{neg, zero, pos}`
+  over a hand-rolled five-element integer carrier; collapses
+  `{m1, m2} ↦ neg`, `{z} ↦ zero`, `{p1, p2} ↦ pos`.
+- **[landed]** Database provenance example (ex. 5) —
+  `EchoExampleProvenance.agda` (PR #81): K-provenance semiring,
+  distinct Bool-provenance rows projecting to the same payload.
+- **[unblocked]** Extend `EchoExamples.agda` with further canonical
+  entries (post-#81/#82/#83 the cluster has good coverage; only
+  ex. 6 remains).
 
 ---