Claude/fix dirty orphans (#10)

* 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

proofs/agda/All.agda

@@ -22,6 +22,10 @@ open import EchoCategorical
 open import EchoScope
 open import EchoOrdinal
 open import EchoJanusBridge
+open import Dyadic
+open import DyadicEchoBridge
+open import EchoThermodynamics
+open import EchoStabilityTests
 
 open import Ordinal.Base
 open import Ordinal.Closure

proofs/agda/DyadicEchoBridge.agda

@@ -26,19 +26,25 @@ SessionAsFunction {p} (Select S1 S2) q = SessionAsFunction S1 q ⊎ SessionAsFun
 -- Simplified echo over session types (avoiding universe issues)
 SessionEcho : ∀ {p} → (q : Party) → Session p → Set
 SessionEcho q End = ⊤
-SessionEcho q (Send A S) = Echo (λ _ → ⊤) ⊤
-SessionEcho q (Recv A S) = Echo (λ _ → ⊤) ⊤
-SessionEcho q (Choice S1 S2) = Echo (λ _ → ⊤) ⊤
-SessionEcho q (Select S1 S2) = Echo (λ _ → ⊤) ⊤
+SessionEcho q (Send A S) = Echo {A = ⊤} (λ _ → tt) tt
+SessionEcho q (Recv A S) = Echo {A = ⊤} (λ _ → tt) tt
+SessionEcho q (Choice S1 S2) = Echo {A = ⊤} (λ _ → tt) tt
+SessionEcho q (Select S1 S2) = Echo {A = ⊤} (λ _ → tt) tt
 
 -- Example: Echo over Alice's send protocol
 AliceSendEcho : SessionEcho Alice AliceSendsUnit
-AliceSendEcho = echo-intro (λ _ → tt) tt
-
--- Protocol provenance: echo retains session structure
-ProtocolProvenance : ∀ {p} {S : Session p} {q : Party} → 
-                      SessionEcho q S → Echo (λ _ → ⊤) ⊤
-ProtocolProvenance echo = echo
+AliceSendEcho = echo-intro {A = ⊤} (λ _ → tt) tt
+
+-- Protocol provenance: echo retains session structure. For non-End
+-- sessions SessionEcho q S is already Echo {A = ⊤} (λ _ → tt) tt; for End it
+-- is ⊤ and we synthesize the canonical echo.
+ProtocolProvenance : ∀ {p} {S : Session p} {q : Party} →
+                      SessionEcho q S → Echo {A = ⊤} (λ _ → tt) tt
+ProtocolProvenance {S = End}        _    = echo-intro {A = ⊤} (λ _ → tt) tt
+ProtocolProvenance {S = Send _ _}   echo = echo
+ProtocolProvenance {S = Recv _ _}   echo = echo
+ProtocolProvenance {S = Choice _ _} echo = echo
+ProtocolProvenance {S = Select _ _} echo = echo
 
 -- Dyadic echo: session with echo-indexed provenance
 DyadicEcho : ∀ {p} → Session p → Set
@@ -50,12 +56,19 @@ AliceSendWithProvenance = Alice , AliceSendEcho
 
 -- Bob's receive protocol with provenance
 BobReceiveWithProvenance : DyadicEcho BobReceivesUnit
-BobReceiveWithProvenance = Bob , echo-intro (λ _ → tt) tt
+BobReceiveWithProvenance = Bob , echo-intro {A = ⊤} (λ _ → tt) tt
 
--- Provenance preservation under session concatenation
+-- Provenance preservation under session concatenation. We synthesize
+-- a fresh echo at the concatenated session, since SessionEcho at a
+-- Send/Recv/Choice/Select head is always Echo {A = ⊤} (λ _ → tt) tt and at
+-- End it is ⊤.
 ProvenancePreservation : ∀ {p} {S1 S2 : Session p} →
                           DyadicEcho S1 → DyadicEcho S2 → DyadicEcho (S1 >>= S2)
-ProvenancePreservation (q1 , echo1) (q2 , echo2) = q1 , echo1
+ProvenancePreservation {S1 = End}        _         (q2 , echo2) = q2 , echo2
+ProvenancePreservation {S1 = Send _ _}   (q1 , _)  _            = q1 , echo-intro {A = ⊤} (λ _ → tt) tt
+ProvenancePreservation {S1 = Recv _ _}   (q1 , _)  _            = q1 , echo-intro {A = ⊤} (λ _ → tt) tt
+ProvenancePreservation {S1 = Choice _ _} (q1 , _)  _            = q1 , echo-intro {A = ⊤} (λ _ → tt) tt
+ProvenancePreservation {S1 = Select _ _} (q1 , _)  _            = q1 , echo-intro {A = ⊤} (λ _ → tt) tt
 
 -- Echo-safe dyadic protocols: protocols where echoes preserve safety
 EchoSafe : ∀ {p} → Session p → Set