Claude/fix dirty orphans (#13)

* Delete duplicate broken orphan modules

These three modules were committed in 8b8fc03 ("further proofing bridges")
but never compiled and duplicated functionality already covered by
in-suite modules:

* EchoCategory.agda (58 sigs, 0 data) — duplicate of EchoCategorical.agda;
  had self-shadowing `_→_` and `_∘_` definitions that parse-errored.

* EchoCNO.agda (8 sigs) — duplicate of EchoCNOBridge.agda; used invalid
  `Σ (x : A) (λ _ → ...)` binder syntax and had a dangling top-level
  `where` clause.

* EchoJanusSimple.agda (9 sigs) — duplicate of EchoJanusBridge.agda;
  same invalid `Σ (x : A) (...)` binder syntax.

Nothing in the verified suite (All.agda) imported any of them. Deleting
them removes silently-broken Agda from the tree without changing what
compiles.

https://claude.ai/code/session_01JRLz84fAaWvRBKyXuc4tyK

* Fix DyadicEchoBridge universe error and wire in Dyadic

Three defects kept this file from typechecking:

1. Lines 29-32, 42: the body `Echo (λ _ → ⊤) ⊤` conflated the unit
   *type* (⊤ : Set) with the unit *value* (tt : ⊤). Echo expects a
   function A → B and a value y : B, not a function into Set. Changed
   to `Echo {A = ⊤} (λ _ → tt) tt` — pinning A explicitly because the
   inferred source type is not constrained anywhere else.

2. ProtocolProvenance pattern-matched on a SessionEcho input whose
   type depends on the Session constructor. The End case has type ⊤,
   not Echo, so the single-clause catch-all "ProtocolProvenance echo
   = echo" could not typecheck. Split into five clauses, synthesising
   a canonical Echo in the End case via echo-intro.

3. ProvenancePreservation returned the left echo verbatim, but its
   type was SessionEcho at (S1 >>= S2) rather than at S1. Pattern-
   match on S1 and synthesise a fresh canonical echo at the
   concatenated head; pass the right-hand echo through when S1 = End.

Also wired Dyadic + DyadicEchoBridge into All.agda so they join the
verified suite and cannot silently regress again.

https://claude.ai/code/session_01JRLz84fAaWvRBKyXuc4tyK

* Rewrite EchoThermodynamics to minimum viable compile

The previous file failed to typecheck in ~15 places: missing imports
(∃, Fin, _≤_, _≃_, proj₁, proj₂, sym, _-_, if-then-else), detached
top-level `where` clauses, chained `≤` that doesn't parse as written,
reversible-echo-preservation using _≃_ without importing it, a
self-assigning nested export module, and theorem bodies such as
"echo-to-cno-thermodynamic-mapping" that branched on a proof value as
if it were a Bool.

Rather than salvage each aspirational theorem, this commit strips the
module to the claims it can actually discharge:

* Thermodynamic types (Temperature, Energy, Information, Entropy) as ℕ.
* Landauer's bit-erasure energy `landauer-energy T = k * T`.
* A simplified `FiberSize` (always 1) with matching `fiber-energy`
  and `echo-energy-cost`.
* A concrete CNO model `cno-identity = id` on ProgramState.
* Three zero-cost lemmas at temperature zero:
    - `cno-fiber-size s ≡ 1`
    - `fiber-energy cno-identity s 0 ≡ 0`
    - `echo-energy-cost f x 0 ≡ 0`

Dropped but documented in-file as not-yet-discharged: CNO zero energy
at non-zero T (needs real fiber enumeration), involution-based
reversible-echo preservation (needs _≃_ plumbing), energy hierarchy
(needs a `≤` relation and non-trivial FiberSize), CNO-detection
predicates (need decidable equality on energies).

Wired into All.agda.

https://claude.ai/code/session_01JRLz84fAaWvRBKyXuc4tyK

* 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

---------

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

Author: hyperpolymath