Skip to content

Commit 96d4d6f

Browse files
docs(bridge-status): record the eclexia thermodynamic consumer bridge (#180)
## Summary Records the new **eclexia ↔ echo-types thermodynamic consumer bridge** in the cross-repo bridge ledger (doc-only; no Agda artefact in this repo). `hyperpolymath/eclexia` (PR [eclexia#32](hyperpolymath/eclexia#32)) now: - integrates Echo as a **first-class `Echo[A, B]` type former** in its type system, and - mirrors the **discrete** thermodynamic shadow of this repo's `EchoThermodynamics` in its *own* Coq metatheory — `formal/coq/src/EchoThermo.v` (`bennett_reversible_is_free`, `free_iff_reversible`, `irreversible_costs_at_least_one_bit`, `erasure_monotone`; axiom-free, `Print Assumptions` clean), and - exposes it at the language level as `landauer_cost(states, T) : Resource[Energy]`, pricing the erasure of a collapsed fibre (`k_B·T·ln N`; reversible retention is free). ## Scope / honesty This is **downstream application/consumer evidence, not a new foundation here**. echo-types makes **no** claim about eclexia's implementation correctness; the real-valued `k T ln 2` scaling and the language runtime live entirely in that repo. The infinite-carrier collapse functional in this repo remains negatively closed (`collapse-cost-impossible`, §2) — eclexia consumes only the finite/discrete shadow. Doc-only change to `docs/bridge-status.md` (new §8). Nothing is imported into `All.agda` / `Smoke.agda`; no Agda recompile required. 🤖 Generated with [Claude Code](https://claude.ai/code) https://claude.ai/code/session_01PWMMxryCcPrAjJ8tuGvygG --- _Generated by [Claude Code](https://claude.ai/code/session_01PWMMxryCcPrAjJ8tuGvygG)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent 8aa922f commit 96d4d6f

1 file changed

Lines changed: 6 additions & 0 deletions

File tree

docs/bridge-status.md

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,3 +47,9 @@ This document strictly tracks the status of experimental extensions and bridges
4747
- **Dependencies:** None in this repo. Adjacent (downstream) only: Valence Shell (`hyperpolymath/valence-shell` — shell state transitions, undo/redo, checkpoints, diff/replay); Ochránce (`hyperpolymath/ochrance` — A2ML manifests, Merkle state commitments, repair/attestation surfaces).
4848
- **Blockers:** No shared schema and no mechanised cross-repo theorem exist. The relationship is citation-level only: Echo Types' structured-loss vocabulary (recoverable / constrained / residue-bearing / observationally equivalent / genuinely lost) is a *candidate* classifier for shell state transitions, and Ochránce may supply concrete receipt evidence. This is downstream application evidence, not a new foundation. Echo Types makes **no** claim about Valence Shell or Ochránce implementation correctness, and **no** claim about POSIX, Rust, the Lean→Rust correspondence, secure deletion, GDPR, cryptographic integrity, or attestation. Companion note: `docs/echo-types/explorations/accountable-shell/README.adoc`. Nothing for this bridge is imported into `proofs/agda/All.agda`, `proofs/agda/Smoke.agda`, or `proofs/agda/EchoCanonicalIdentitySuite.agda`.
4949
- **Core Affect:** NO
50+
51+
## 8. Eclexia consumer (thermodynamic resource bridge)
52+
- **Status:** LANDED (downstream consumer-side, in `hyperpolymath/eclexia` — PR eclexia#32). No artefact in *this* repo.
53+
- **Dependencies:** None in this repo. Adjacent (downstream) only: Eclexia (`hyperpolymath/eclexia` — the resource-typed "economics-as-code" language).
54+
- **Blockers:** None outstanding on the consumer side; this is application evidence, not a new foundation here. Eclexia integrates Echo as a first-class `Echo[A, B]` type former and, separately in its *own* Coq metatheory, mirrors the **discrete** thermodynamic shadow of this repo's `EchoThermodynamics` (`formal/coq/src/EchoThermo.v`: `bennett_reversible_is_free`, `free_iff_reversible`, `irreversible_costs_at_least_one_bit`, `erasure_monotone` — axiom-free, `Print Assumptions` clean), and exposes it at the language level as `landauer_cost(states, T) : Resource[Energy]` — pricing the erasure of a collapsed fibre (`k_B·T·ln N`; reversible retention is free). Echo Types makes **no** claim about Eclexia's implementation correctness; the real-valued `k T ln 2` scaling and the language runtime live entirely in that repo. The infinite-carrier collapse functional here remains negatively closed (`collapse-cost-impossible`, see §2) — eclexia consumes only the finite/discrete shadow. Nothing for this bridge is imported into `proofs/agda/All.agda` or `proofs/agda/Smoke.agda`.
55+
- **Core Affect:** NO

0 commit comments

Comments
 (0)