`EchoBridgeCNO.agda` has no `--safe --without-K` pragma and is not checked by proofs.yml, while PROOF-STATUS:154 says it type-checks under `--safe`

[hyperpolymath]

Measured (2026-09-22, main = 74202cb)

• proofs/agda/EchoBridgeCNO.agda: 0 OPTIONS lines. CNO.agda and OND.agda carry {-# OPTIONS --safe --without-K #-}.
• .github/workflows/proofs.yml:80–82 runs agda --safe --without-K on CNO.agda and OND.agda only.
• PROOF-STATUS.adoc:154–155: "agda 2.6.3, --safe --without-K: CNO.agda, OND.agda, EchoBridgeCNO.agda type-check. The EchoBridge modules take funext as an explicit hypothesis".
• echo-types pins absolute-zero at 3ff5cee7 (2026-05-18) with a rev-parse guard, and residual-evidence-types depends on echo-types, so this file is transitively upstream of the residual receipts.

Acceptance criteria

1. EchoBridgeCNO.agda gets {-# OPTIONS --safe --without-K #-} at line 1, and proofs.yml checks it alongside the other two (same job, same flags).
2. Watched-failing → green: grep -c OPTIONS proofs/agda/EchoBridgeCNO.agda is 0 today, 1 after; the fix commit's run is green with three agda invocations in the log.
3. If the file does not pass under --safe (funext as a hypothesis is fine; a postulate is not), PROOF-STATUS.adoc:154 is corrected instead and the file is listed as unsafe-by-design.
4. README.adoc names the file as it exists (EchoBridgeCNO, not EchoCNOBridge).

🤖 Generated with Claude Code