docs(proof-debt): refresh stale variance bullet — resolved by wired EchoVariance (#243) (#258)

## What

A one-line-spirit refresh of `docs/proof-debt.md`: the 2026-06-16
ground-truth-audit bullet still flagged the monad/comonad/adjunction
**variance** question as *"genuinely open"* — but it was **settled four
days later** by the **wired** `EchoVariance.agda` (#243, 2026-06-20).

## The fix

The bullet now:
- **preserves the dated audit observation** (true *as of 2026-06-16*:
the only variance material was the orphaned
`experimental/echo-additive/` track + `VarianceGate.agda`, which
self-declares "NO proven theorems");
- **records the resolution**: `EchoVariance.agda` (in `All.agda`,
`--safe --without-K`, zero postulates) — echo is a graded **monad of
accumulation** + a section/retraction **adjunction exact on the grade-0
fibre**, and is **NOT a graded comonad** (`no-bare-recovery` the
obstruction; sharpens `R-2026-05-18` from "withdrawn" to "decided
against");
- points at the **wired** `EchoVariance` +
`docs/echo-types/variance-resolution.adoc` as the citation, and notes
the orphaned experimental track is the *retired earlier attempt*.

This keeps the audit's honesty (it was accurate when written) while
removing the stale "open" status that contradicted the later wired
result.

Docs-only; `kernel-guard` PASS. Verified `EchoVariance` is wired
(`All.agda:107`) and `variance-resolution.adoc` exists.

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

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

---
_Generated by [Claude
Code](https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

docs/proof-debt.md

@@ -140,16 +140,26 @@ ledger above.
   and `Ordinal/Buchholz/Fidelity.agda` (d) — are guardrail-exempt,
   `--without-K`-only, and imported by no `All.agda`, so the `--safe`
   kernel cone depends on neither. Nothing slipped into the wired layer.
-- **⚠ Variance is NOT a proven result.** The `experimental/echo-additive/`
-  track (`GradedComonad` / `GradedMonad` / `GradedAdjunction` /
-  `VarianceGate.agda`) is present on `main` but **orphaned** (in no
-  `All.agda`, not CI-verified), and `VarianceGate.agda` self-declares
-  "This file contains NO proven theorems … OBLIGATION comments" + variance
-  **RETRACTED R-2026-05-18**. It typechecks `--safe` only because the
-  obligations are comments. **Do not cite the monad / comonad / adjunction
-  variance question as settled** — it remains genuinely open. Build instead
-  on the wired `Echo` / `EchoResidue`, `EchoGradedComonad` (coassoc/counit),
-  the composition isos, and `DyadicEchoBridge`.
+- **⚠ Variance was open AT AUDIT TIME; RESOLVED 2026-06-20.** As of this
+  audit (2026-06-16) the only variance material on `main` was the
+  `experimental/echo-additive/` track (`GradedComonad` / `GradedMonad` /
+  `GradedAdjunction` / `VarianceGate.agda`) — **orphaned** (in no
+  `All.agda`, not CI-verified; `VarianceGate.agda` self-declares "This file
+  contains NO proven theorems … OBLIGATION comments", variance **RETRACTED
+  R-2026-05-18**), so the monad / comonad / adjunction question was genuinely
+  open *then*. It was **settled four days later by the WIRED
+  `EchoVariance.agda`** (#243, 2026-06-20 — in `All.agda`, `--safe
+  --without-K`, zero postulates, pinned in `Smoke.agda`): echo is a graded
+  **monad of accumulation** (`accumulate = Echo-comp-iso-from`) with a
+  section/retraction **adjunction exact on the grade-0 fibre**
+  (`recoverable-fibre = A↔ΣEcho`), and is **NOT a graded comonad**
+  (`no-bare-recovery` via `no-section-of-collapsing-map` is the obstruction;
+  sharpens `R-2026-05-18` from "graded comonad withdrawn" to "decided
+  against"). Cite the WIRED `EchoVariance` for the verdict; the orphaned
+  `experimental/echo-additive/` track is the retired earlier attempt. See
+  `docs/echo-types/variance-resolution.adoc`. Build on the wired `Echo` /
+  `EchoResidue`, `EchoVariance`, `EchoGradedComonad` (coassoc/counit), the
+  composition isos, and `DyadicEchoBridge`.
 - **Env gotcha (fix before handoff).** A *dangling* libraries config
   (nix-store name mismatch + a non-existent `…/absolute-zero` path) causes
   **false "library name not found" failures** under the default config.