Saved in:
| Main Author: | |
|---|---|
| Format: | Recurso digital |
| Language: | |
| Published: |
Zenodo
2026
|
| Online Access: | https://doi.org/10.5281/zenodo.19671784 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Table of Contents:
- <p>Preliminary Agda formalisation of echo types as a first-class notion of structured loss.</p> <p>What's in this release Eight Agda modules (safe, no postulates) establishing:</p> <p>the core fiber definition and introduction (Echo.agda); action on fibers for morphisms over a fixed base, with identity and composition laws; action along commuting squares; explicit non-injectivity witnesses for collapse maps; no-section results establishing the impossibility of full reconstruction from visible output alone; a retained-constraint result for projection-style structured loss (EchoCharacteristic.agda); scope-broadening bridges toward choreographic, epistemic, affine/linear, graded, and tropical settings.</p> <p>Status This is a work in progress. The identity claim for echo types — that they name a distinct phenomenon worth studying as a primary object rather than a decorative wrapper around existing fiber machinery — is treated as falsifiable. Three decision gates operationalise this in roadmap.adoc:</p> <p>distinct phenomenon; characteristic theorem family not reducible to generic sigma lemmas; canonical examples where "echo type" is the right explanatory unit.</p> <p>If any gate fails during development, the outcome is recorded in docs/retractions.adoc and the identity claim is retracted. Build agda -i proofs/agda proofs/agda/All.agda Citing This release is archived on Zenodo. A DOI will appear on the release page once the Zenodo integration has processed it (usually a few minutes).</p>