Skip to content

Commit 73f9345

Browse files
hyperpolymathhyperpolymath
committed
Merge remote-tracking branch 'origin/docs/echo-types-master-map'
2 parents 3e4d556 + 645ddcf commit 73f9345

2 files changed

Lines changed: 207 additions & 0 deletions

File tree

‎README.md‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,16 @@ Constructive Agda development for echo types as a first-class notion of structur
1111

1212
loss that is not total erasure.
1313

14+
## 🗺️ Where things are
15+
16+
**New here, or can't find something? Start with the
17+
[Master Map](docs/echo-types/MAP.adoc).** It is the single source of
18+
truth for every direction (Thermodynamic, Buchholz/Veblen ordinals,
19+
Characteristic/EI, CNO/absolute-zero, JanusKey, Tropical/Dyadic, MAA,
20+
Shannon — and ArghDA tooling), each status-tagged and back-linked to
21+
its proofs and docs, with the retraction/proof-debt governance called
22+
out. The scattered overview/roadmap docs are detail under it.
23+
1424
## Core Idea
1525

1626
Most formalisms foreground two clean cases:

‎docs/echo-types/MAP.adoc‎

Lines changed: 197 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,197 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
= echo-types: Master Map
4+
:toc: macro
5+
:toclevels: 3
6+
:source-highlighter: rouge
7+
8+
[.lead]
9+
*The single source of truth for "what is in echo-types and where."*
10+
If you cannot find something, it is indexed here or it does not exist.
11+
This file supersedes the navigational role of the scattered overview /
12+
roadmap / taxonomy docs (which remain as detail, linked below). Keep it
13+
current: every new direction or status change updates this file in the
14+
same PR.
15+
16+
NOTE: This is the *content/architecture* map. For the per-session audit
17+
trail (which finding lives in which 6a2 capture) see `../../INDEX.adoc`
18+
— different purpose, complementary.
19+
20+
toc::[]
21+
22+
== Status legend
23+
24+
[cols="1,4"]
25+
|===
26+
| `[REAL]` | Mechanised in Agda `--safe --without-K`, on `origin/main`.
27+
| `[REAL*]` | Real but partial / graded — see the linked status.
28+
| `[ROADMAP]` | Planned/specified, not yet built.
29+
| `[OPEN]` | Acknowledged gap; explicitly *not* bridged yet.
30+
| `[RETRACTED]` | Claim withdrawn by retraction R-2026-05-18; under a
31+
falsifiable earn-back gate (see Governance).
32+
| `[CLOSED-NEG]` | Settled as a *negative* result (do not reopen).
33+
|===
34+
35+
The canonical state is always `origin/main`. Local working clones drift
36+
behind — `git fetch` and read `origin/main` before trusting any survey.
37+
38+
== Foundation
39+
40+
*Echo functor / loss-with-residue.* The theory of the structured
41+
remainder of information-losing computation: for `f : A → B`,
42+
`Echo f y := Σ (x : A), (f x ≡ y)`. `[REAL]`
43+
44+
* Proofs: `proofs/agda/Echo.agda` + ~24 `Echo*.agda` modules
45+
(`EchoCategorical`, `EchoDecidable`, `EchoCharacteristic`,
46+
`EchoApprox`, `EchoIndexed`, …).
47+
* Library: `echo-types.agda-lib` (`depend: standard-library
48+
absolute-zero`).
49+
* Concept doc: `docs/echo-types/overview.md`,
50+
`docs/echo-types/types-abstract.adoc`,
51+
`docs/echo-types/paper.adoc`.
52+
53+
== Directions
54+
55+
=== Thermodynamic — Landauer/Bennett energy bounds `[REAL*]`
56+
Finite-domain Landauer/Bennett bounds; `ThermodynamicallyReversible(p)
57+
≙ Echo p σ ≃ Echo id σ`. Rated ~70% / C+ in STABILITY_ANALYSIS.
58+
59+
* Proofs: `proofs/agda/EchoThermodynamics.agda`,
60+
`proofs/agda/EchoFiberCount.agda`.
61+
* Docs: `docs/ECHO-CNO-BRIDGE.adoc` §"Thermodynamic Bridge",
62+
`docs/STABILITY_ANALYSIS.md` §3.3, `docs/WORK_PLAN.md` §5,
63+
`docs/adjacency/hott-fibers.adoc`.
64+
* Build: `just test-thermo`.
65+
66+
=== Buchholz / Veblen ordinals — higher-order number systems `[REAL]`
67+
Staged Buchholz-style collapsing in `--safe --without-K`.
68+
69+
* Proofs: `proofs/agda/Ordinal/` (`Buchholz/`, `Brouwer`, `CNF`,
70+
`Closure`, `Psi…`, `ExtendedOrder`).
71+
* Docs: `docs/buchholz-plan.adoc`,
72+
`docs/echo-types/buchholz-extended-wf.md`.
73+
* Direct-constructor `_<ᵇ_` same-binder cases (Buchholz item B):
74+
status tracked solely in the earn-back ledger
75+
(`docs/echo-types/earn-back-plan.adoc`, row B) and
76+
`docs/retractions.adoc` (F-2026-05-18b) — off the paper critical
77+
path. (Reference-only by design: no status is snapshotted here, so
78+
this line never drifts as the ledger moves.)
79+
80+
=== Characteristic / EI — epistemic, choreographic, roles `[REAL]`
81+
The echo-invariant line: epistemic structure, choreographies, roles.
82+
83+
* Proofs: `proofs/agda/characteristic/` (15 modules — `ChoreoInjective`,
84+
`RoleMode`, `RoleRole`, `RoleGraded`, `ModeGraded`, `NonTruncatable`,
85+
`RecipeNonTriviality`, `RecipeTheorem`, …), `proofs/agda/EchoChoreo.agda`.
86+
* Docs: `docs/characteristic.adoc`, `docs/EI2_REPORT.adoc`,
87+
`docs/EI2_READINGS_COMPARISON.adoc`, `docs/integration-audit.adoc`.
88+
* `EI-2` is `[CLOSED-NEG]` (terminated negative — do not reopen).
89+
`RoleRole.agda`'s "REAL OBSTRUCTION" is a closed negative result,
90+
not debt.
91+
92+
=== CNO / absolute-zero `[REAL]`
93+
Certified Null Operations = echo types where `f = id`. absolute-zero is
94+
both a *dependency* of the core and a *bridge* target.
95+
96+
* Proofs: `proofs/agda/EchoCNOBridge.agda`, `MinimalCNO.agda`,
97+
`WorkingCNO.agda`.
98+
* Docs: `docs/ECHO-CNO-BRIDGE.adoc`,
99+
`docs/echo-types/cross-repo-bridge-status.md`.
100+
101+
=== JanusKey reversibility `[REAL]`
102+
Constructive fiber theory ↔ JanusKey "architecturally impossible data
103+
loss".
104+
105+
* Proofs: `proofs/agda/EchoJanusBridge.agda`.
106+
* Docs: `docs/EchoJanusBridge.md`, `docs/EchoBridges.md`.
107+
108+
=== Tropical / Dyadic `[REAL*]`
109+
Bridge domains enumerated in `docs/EchoBridges.md` (JanusKey / CNO /
110+
Tropical / Dyadic). Dyadic is mechanised; Tropical is named/early.
111+
112+
* Proofs: `proofs/agda/Dyadic.agda`, `proofs/agda/DyadicEchoBridge.agda`.
113+
* Docs: `docs/EchoBridges.md`.
114+
115+
=== MAA Framework integration `[ROADMAP]`
116+
Connect echo types with MAA's reversibility proofs
117+
(`maa-echo-equivalence`). absolute-zero lives under
118+
`…/verification-ecosystem/maa-framework/`. Planned, not built.
119+
120+
* Docs: `docs/ProofRoadmap.md` §10, `docs/EchoJanusBridge.md`.
121+
122+
=== Shannon / information theory `[OPEN]`
123+
Explicitly *not bridged*. The Transport / Nyquist sampling work
124+
(Gate-3) is the nearest built thread; a real Shannon-entropy /
125+
mutual-information formalisation is open.
126+
127+
* Proofs: `proofs/agda/examples/Transport.agda`.
128+
* Docs: `docs/ECHO-CNO-BRIDGE.adoc` (lines ~104, ~254),
129+
`docs/adjacency/information-flow.adoc`,
130+
`docs/gate-3-canonical.adoc`, `docs/gate-3-transport-handoff.adoc`.
131+
132+
== Tooling
133+
134+
=== ArghDA — proof-ladder workspace manager `[REAL*]`
135+
Language-agnostic proof-workspace engine (`arghda-core`, Rust). MVP.
136+
137+
* Code: `arghda-core/` (Rust crate).
138+
* Docs: `docs/arghda-spec.adoc`.
139+
140+
== Governance — proof-debt & retraction
141+
142+
The honesty layer. *Read before citing any claim above as final.*
143+
144+
* `docs/retractions.adoc` — **R-2026-05-18** retracts the
145+
graded-comonad / two-models / conservativity / universal-property
146+
framing. Those are `[RETRACTED]`, now a *loss-graded reindexing
147+
modality*; earn-back is gated, claims stay retracted until a gate
148+
passes.
149+
* `docs/echo-types/earn-back-plan.adoc` — the consolidated proof-debt
150+
ledger + falsifiable gates F1–F4 (F1 = make-or-break graded comonad;
151+
F2/F4 independent; F3 gated on F1). Current SoT for what is / isn't
152+
proven.
153+
* Gate handoffs: `docs/gate-1-distinct-phenomenon.adoc`,
154+
`docs/gate-2-handoff.adoc`, `docs/gate-3-*.adoc`.
155+
156+
== Documentation index (canonical vs historical)
157+
158+
Multiple overlapping docs exist. Use the *canonical* column; the rest
159+
are kept for history and **may overclaim** (pre-retraction).
160+
161+
[cols="1,3,3"]
162+
|===
163+
| Topic | Canonical (use this) | Historical / superseded
164+
165+
| Project map (this file)
166+
| `docs/echo-types/MAP.adoc`
167+
| `INDEX.adoc` is the *audit* index (different role; keep)
168+
169+
| Proof status / roadmap
170+
| `docs/echo-types/earn-back-plan.adoc` + `docs/retractions.adoc`
171+
| `ProofRoadmap.md`, `PRIORITIZED_PROOF_ROADMAP.md`, `WORK_PLAN.md`,
172+
`roadmap.adoc`, `roadmap-gates.adoc`, `docs/echo-types/roadmap.md`
173+
(pre-R-2026-05-18 — historical)
174+
175+
| Concept / definition
176+
| `docs/echo-types/overview.md`, `docs/echo-types/paper.adoc`
177+
| `COMPREHENSIVE_DOCUMENTATION.md`
178+
179+
| Bridges
180+
| `docs/EchoBridges.md` + this file's Directions
181+
| `docs/echo-types/cross-repo-bridge-status.md` (detail)
182+
183+
| Adjacency / related theory
184+
| `docs/adjacency/` (per-topic .adoc)
185+
| —
186+
|===
187+
188+
== Keeping this current
189+
190+
This is a living document. Whenever a direction is added, a gate
191+
passes/fails, or a claim is retracted/earned-back:
192+
193+
. Update the relevant Directions/Governance entry *and* its status tag
194+
here, in the same PR as the change.
195+
. Never duplicate detail — link to the canonical proof module / doc.
196+
. The GitHub wiki `Home` mirrors this file and must point back here as
197+
SoT; do not fork content into the wiki.

0 commit comments

Comments
 (0)