diff --git a/README.md b/README.md index 4ac97c1..941bac5 100644 --- a/README.md +++ b/README.md @@ -11,6 +11,16 @@ Constructive Agda development for echo types as a first-class notion of structur loss that is not total erasure. +## πŸ—ΊοΈ Where things are + +**New here, or can't find something? Start with the +[Master Map](docs/echo-types/MAP.adoc).** It is the single source of +truth for every direction (Thermodynamic, Buchholz/Veblen ordinals, +Characteristic/EI, CNO/absolute-zero, JanusKey, Tropical/Dyadic, MAA, +Shannon β€” and ArghDA tooling), each status-tagged and back-linked to +its proofs and docs, with the retraction/proof-debt governance called +out. The scattered overview/roadmap docs are detail under it. + ## Core Idea Most formalisms foreground two clean cases: diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc new file mode 100644 index 0000000..8ee6bb4 --- /dev/null +++ b/docs/echo-types/MAP.adoc @@ -0,0 +1,197 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += echo-types: Master Map +:toc: macro +:toclevels: 3 +:source-highlighter: rouge + +[.lead] +*The single source of truth for "what is in echo-types and where."* +If you cannot find something, it is indexed here or it does not exist. +This file supersedes the navigational role of the scattered overview / +roadmap / taxonomy docs (which remain as detail, linked below). Keep it +current: every new direction or status change updates this file in the +same PR. + +NOTE: This is the *content/architecture* map. For the per-session audit +trail (which finding lives in which 6a2 capture) see `../../INDEX.adoc` +β€” different purpose, complementary. + +toc::[] + +== Status legend + +[cols="1,4"] +|=== +| `[REAL]` | Mechanised in Agda `--safe --without-K`, on `origin/main`. +| `[REAL*]` | Real but partial / graded β€” see the linked status. +| `[ROADMAP]` | Planned/specified, not yet built. +| `[OPEN]` | Acknowledged gap; explicitly *not* bridged yet. +| `[RETRACTED]` | Claim withdrawn by retraction R-2026-05-18; under a + falsifiable earn-back gate (see Governance). +| `[CLOSED-NEG]` | Settled as a *negative* result (do not reopen). +|=== + +The canonical state is always `origin/main`. Local working clones drift +behind β€” `git fetch` and read `origin/main` before trusting any survey. + +== Foundation + +*Echo functor / loss-with-residue.* The theory of the structured +remainder of information-losing computation: for `f : A β†’ B`, +`Echo f y := Ξ£ (x : A), (f x ≑ y)`. `[REAL]` + +* Proofs: `proofs/agda/Echo.agda` + ~24 `Echo*.agda` modules + (`EchoCategorical`, `EchoDecidable`, `EchoCharacteristic`, + `EchoApprox`, `EchoIndexed`, …). +* Library: `echo-types.agda-lib` (`depend: standard-library + absolute-zero`). +* Concept doc: `docs/echo-types/overview.md`, + `docs/echo-types/types-abstract.adoc`, + `docs/echo-types/paper.adoc`. + +== Directions + +=== Thermodynamic β€” Landauer/Bennett energy bounds `[REAL*]` +Finite-domain Landauer/Bennett bounds; `ThermodynamicallyReversible(p) +≙ Echo p Οƒ ≃ Echo id Οƒ`. Rated ~70% / C+ in STABILITY_ANALYSIS. + +* Proofs: `proofs/agda/EchoThermodynamics.agda`, + `proofs/agda/EchoFiberCount.agda`. +* Docs: `docs/ECHO-CNO-BRIDGE.adoc` Β§"Thermodynamic Bridge", + `docs/STABILITY_ANALYSIS.md` Β§3.3, `docs/WORK_PLAN.md` Β§5, + `docs/adjacency/hott-fibers.adoc`. +* Build: `just test-thermo`. + +=== Buchholz / Veblen ordinals β€” higher-order number systems `[REAL]` +Staged Buchholz-style collapsing in `--safe --without-K`. + +* Proofs: `proofs/agda/Ordinal/` (`Buchholz/`, `Brouwer`, `CNF`, + `Closure`, `Psi…`, `ExtendedOrder`). +* Docs: `docs/buchholz-plan.adoc`, + `docs/echo-types/buchholz-extended-wf.md`. +* Direct-constructor `_<ᡇ_` same-binder cases (Buchholz item B): + status tracked solely in the earn-back ledger + (`docs/echo-types/earn-back-plan.adoc`, row B) and + `docs/retractions.adoc` (F-2026-05-18b) β€” off the paper critical + path. (Reference-only by design: no status is snapshotted here, so + this line never drifts as the ledger moves.) + +=== Characteristic / EI β€” epistemic, choreographic, roles `[REAL]` +The echo-invariant line: epistemic structure, choreographies, roles. + +* Proofs: `proofs/agda/characteristic/` (15 modules β€” `ChoreoInjective`, + `RoleMode`, `RoleRole`, `RoleGraded`, `ModeGraded`, `NonTruncatable`, + `RecipeNonTriviality`, `RecipeTheorem`, …), `proofs/agda/EchoChoreo.agda`. +* Docs: `docs/characteristic.adoc`, `docs/EI2_REPORT.adoc`, + `docs/EI2_READINGS_COMPARISON.adoc`, `docs/integration-audit.adoc`. +* `EI-2` is `[CLOSED-NEG]` (terminated negative β€” do not reopen). + `RoleRole.agda`'s "REAL OBSTRUCTION" is a closed negative result, + not debt. + +=== CNO / absolute-zero `[REAL]` +Certified Null Operations = echo types where `f = id`. absolute-zero is +both a *dependency* of the core and a *bridge* target. + +* Proofs: `proofs/agda/EchoCNOBridge.agda`, `MinimalCNO.agda`, + `WorkingCNO.agda`. +* Docs: `docs/ECHO-CNO-BRIDGE.adoc`, + `docs/echo-types/cross-repo-bridge-status.md`. + +=== JanusKey reversibility `[REAL]` +Constructive fiber theory ↔ JanusKey "architecturally impossible data +loss". + +* Proofs: `proofs/agda/EchoJanusBridge.agda`. +* Docs: `docs/EchoJanusBridge.md`, `docs/EchoBridges.md`. + +=== Tropical / Dyadic `[REAL*]` +Bridge domains enumerated in `docs/EchoBridges.md` (JanusKey / CNO / +Tropical / Dyadic). Dyadic is mechanised; Tropical is named/early. + +* Proofs: `proofs/agda/Dyadic.agda`, `proofs/agda/DyadicEchoBridge.agda`. +* Docs: `docs/EchoBridges.md`. + +=== MAA Framework integration `[ROADMAP]` +Connect echo types with MAA's reversibility proofs +(`maa-echo-equivalence`). absolute-zero lives under +`…/verification-ecosystem/maa-framework/`. Planned, not built. + +* Docs: `docs/ProofRoadmap.md` Β§10, `docs/EchoJanusBridge.md`. + +=== Shannon / information theory `[OPEN]` +Explicitly *not bridged*. The Transport / Nyquist sampling work +(Gate-3) is the nearest built thread; a real Shannon-entropy / +mutual-information formalisation is open. + +* Proofs: `proofs/agda/examples/Transport.agda`. +* Docs: `docs/ECHO-CNO-BRIDGE.adoc` (lines ~104, ~254), + `docs/adjacency/information-flow.adoc`, + `docs/gate-3-canonical.adoc`, `docs/gate-3-transport-handoff.adoc`. + +== Tooling + +=== ArghDA β€” proof-ladder workspace manager `[REAL*]` +Language-agnostic proof-workspace engine (`arghda-core`, Rust). MVP. + +* Code: `arghda-core/` (Rust crate). +* Docs: `docs/arghda-spec.adoc`. + +== Governance β€” proof-debt & retraction + +The honesty layer. *Read before citing any claim above as final.* + +* `docs/retractions.adoc` β€” **R-2026-05-18** retracts the + graded-comonad / two-models / conservativity / universal-property + framing. Those are `[RETRACTED]`, now a *loss-graded reindexing + modality*; earn-back is gated, claims stay retracted until a gate + passes. +* `docs/echo-types/earn-back-plan.adoc` β€” the consolidated proof-debt + ledger + falsifiable gates F1–F4 (F1 = make-or-break graded comonad; + F2/F4 independent; F3 gated on F1). Current SoT for what is / isn't + proven. +* Gate handoffs: `docs/gate-1-distinct-phenomenon.adoc`, + `docs/gate-2-handoff.adoc`, `docs/gate-3-*.adoc`. + +== Documentation index (canonical vs historical) + +Multiple overlapping docs exist. Use the *canonical* column; the rest +are kept for history and **may overclaim** (pre-retraction). + +[cols="1,3,3"] +|=== +| Topic | Canonical (use this) | Historical / superseded + +| Project map (this file) +| `docs/echo-types/MAP.adoc` +| `INDEX.adoc` is the *audit* index (different role; keep) + +| Proof status / roadmap +| `docs/echo-types/earn-back-plan.adoc` + `docs/retractions.adoc` +| `ProofRoadmap.md`, `PRIORITIZED_PROOF_ROADMAP.md`, `WORK_PLAN.md`, + `roadmap.adoc`, `roadmap-gates.adoc`, `docs/echo-types/roadmap.md` + (pre-R-2026-05-18 β€” historical) + +| Concept / definition +| `docs/echo-types/overview.md`, `docs/echo-types/paper.adoc` +| `COMPREHENSIVE_DOCUMENTATION.md` + +| Bridges +| `docs/EchoBridges.md` + this file's Directions +| `docs/echo-types/cross-repo-bridge-status.md` (detail) + +| Adjacency / related theory +| `docs/adjacency/` (per-topic .adoc) +| β€” +|=== + +== Keeping this current + +This is a living document. Whenever a direction is added, a gate +passes/fails, or a claim is retracted/earned-back: + +. Update the relevant Directions/Governance entry *and* its status tag + here, in the same PR as the change. +. Never duplicate detail β€” link to the canonical proof module / doc. +. The GitHub wiki `Home` mirrors this file and must point back here as + SoT; do not fork content into the wiki.