Rewrite EchoStabilityTests against surviving modules

The previous file cross-linked four modules. Three of them
(EchoCategory, EchoCNO, EchoCNO's thermodynamic mapping) were deleted
or rewritten in earlier commits on this branch, leaving roughly 75 %
of the tests pointing at missing symbols. On top of that the file
itself never typechecked — bad Σ-binder syntax, bogus `where` at top
level, self-assigning export module.

Rewrite strategy: keep only tests that lock upstream shapes via refl
against modules we still ship, document the dropped sections in
comments so follow-up work can repopulate them. The surviving tests
are:

Section 1 (Echo core)
  echo-intro-fst    — proj₁ of echo-intro lands at the supplied x
  map-over-fst      — map-over advances the first component by u
  map-over-id-check — map-over with identity is the identity

Section 2 (thermodynamic core)
  cno-fiber-is-one         — the CNO fiber proof is refl
  cno-zero-T-check         — fiber-energy of CNO at T=0 is 0
  echo-cost-zero-T-check   — echo-energy-cost of any f at T=0 is 0

Dropped sections (noted in-file for future work): universal-CNO /
categorical equivalence (needs EchoCategorical API parity),
CNO-singleton equivalence (needs tests against EchoCNOBridge's
CNOEcho/nullop-echo), thermodynamic optimality / hierarchy (needs
non-trivial FiberSize and a _≤_ on energies).

Wired into All.agda.

https://claude.ai/code/session_01JRLz84fAaWvRBKyXuc4tyK

Author: claude

proofs/agda/All.agda

@@ -25,6 +25,7 @@ open import EchoJanusBridge
 open import Dyadic
 open import DyadicEchoBridge
 open import EchoThermodynamics
+open import EchoStabilityTests
 
 open import Ordinal.Base
 open import Ordinal.Closure