docs: tidy after earn-back closure + theory-work closure + examples cluster landed (#92)

## Summary

Three small accuracy passes through `docs/echo-types/` after the
earn-back programme, the §"Theory work — no proof assistant needed"
section, and the canonical examples cluster (5/9/10) all closed in
this session. Pure prose; no Agda changes.

### 1. `roadmap.md` §"Theory work" — two stale items refreshed

* **Axis 8** line said the *decidability-respecting* candidate had
  shipped but listed the other three as still candidate refinements.
  All four have now shipped: `EchoDecidable`, `EchoCost` (#85),
  `EchoAccess` (#68 / #75), `EchoSearch` (#80). Updated to credit all
  four.
* **Negative / co-echoes** line was `[unblocked]`; now `[landed]` —
  `AntiEcho` (#69), tropical decomposition concrete + generic (#72 +
  #91), `antiecho-partition-dec` (#90). Names the `coecho.md` §5
  obligation-5 / obligation-6 closures explicitly.

After these edits, every item in §"Theory work — no proof assistant
needed" is either `[landed]` or `[ruled out]`/`[refreshed]` — the
section is genuinely closed.

### 2. `roadmap.md` §"Example work" — three items landed

* ex. 5 (`EchoExampleProvenance`, #81) → `[landed]`
* ex. 9 (`EchoExampleParser`, #83) → `[landed]`
* ex. 10 (`EchoExampleAbsInt`, #82) → `[landed]`

Only ex. 6 (approximate-echo numeric example) remains `[unblocked]`.

### 3. `earn-back-plan.adoc` — stale `roadmap-gates.adoc` claim
corrected

* Header note used to say "the gate discipline was historically
  attributed to a `roadmap-gates.adoc`; that file does not exist
  in-tree". The file **does** exist (created 2026-05-18; see its
  preamble). Header rewritten to list `roadmap-gates.adoc` alongside
  `retractions.adoc` / this plan / `next-questions.adoc` as the four
  canonical loci.
* Ledger row D (the "doesn't exist" entry) marked **CLOSED 2026-05-20**
  with the cite reflecting current reality.

## Test plan

* [x] Pure docs / `.adoc` / `.md` edits — no Agda touched
* [x] `agda proofs/agda/All.agda` exit 0 (confirms docs match code)
* [x] `agda proofs/agda/Smoke.agda` exit 0
* [x] No retracted-claim language moved; no earned-back claim
      overclaimed; `paper.adoc` / `types-abstract.adoc` /
      `conservativity.adoc` untouched

## Scope

Disjoint from all currently-open PRs:
* #88 (F3) — touches Agda + `retractions.adoc` (different sections)
  + `earn-back-plan.adoc` Status (different section from header /
  ledger-D)
* #90 (partition-dec) — touches Agda only
* #91 (generic-codomain) — touches Agda + preamble comments

No retracted claim is moved. No earned-back claim is overclaimed.
`paper.adoc` / `types-abstract.adoc` / `conservativity.adoc` are
intentionally untouched (owner-gated, per the posture set by #86 /
#88).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

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).
 
 ---