Commit 9dc1ec7
committed
docs(bridge-status): record the eclexia thermodynamic consumer bridge
Add section 8 to the cross-repo bridge ledger: hyperpolymath/eclexia
(PR eclexia#32) now consumes echo-types as a first-class Echo[A,B] type
former and mirrors the discrete EchoThermodynamics shadow in its own Coq
(EchoThermo.v: bennett_reversible_is_free, free_iff_reversible,
irreversible_costs_at_least_one_bit, erasure_monotone — axiom-free),
exposing it as landauer_cost(states, T) : Resource[Energy].
Honestly scoped: downstream application/consumer evidence, not a new
foundation here; echo-types makes no claim about eclexia's correctness, and
the infinite-carrier collapse functional remains negatively closed (S2). No
artefact in this repo; doc-only change, no Agda recompile.
https://claude.ai/code/session_01PWMMxryCcPrAjJ8tuGvygG1 parent 64ef20a commit 9dc1ec7
1 file changed
Lines changed: 6 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
47 | 47 | | |
48 | 48 | | |
49 | 49 | | |
| 50 | + | |
| 51 | + | |
| 52 | + | |
| 53 | + | |
| 54 | + | |
| 55 | + | |
0 commit comments