Skip to content

Commit 2b9be9c

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs: canonical echo-types Master Map + README front door
Single source of truth for project structure/discoverability. ~50 docs with several overlapping roadmaps and no authoritative entry point made real work (Thermodynamic, etc.) effectively unfindable — even by the author. docs/echo-types/MAP.adoc indexes every direction status-tagged ([REAL]/[ROADMAP]/[OPEN]/[RETRACTED]/[CLOSED-NEG]) and back-links proofs + canonical docs; resolves the roadmap fragmentation (canonical vs pre-R-2026-05-18 historical); respects retraction governance. README now front-doors it. Links, does not duplicate. Living doc. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 2ca3122 commit 2b9be9c

2 files changed

Lines changed: 203 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: 193 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,193 @@
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+
* Known structural-fidelity gap on direct-constructor `_<ᵇ_` (Buchholz
74+
item B in the earn-back ledger) — off the paper critical path.
75+
76+
=== Characteristic / EI — epistemic, choreographic, roles `[REAL]`
77+
The echo-invariant line: epistemic structure, choreographies, roles.
78+
79+
* Proofs: `proofs/agda/characteristic/` (15 modules — `ChoreoInjective`,
80+
`RoleMode`, `RoleRole`, `RoleGraded`, `ModeGraded`, `NonTruncatable`,
81+
`RecipeNonTriviality`, `RecipeTheorem`, …), `proofs/agda/EchoChoreo.agda`.
82+
* Docs: `docs/characteristic.adoc`, `docs/EI2_REPORT.adoc`,
83+
`docs/EI2_READINGS_COMPARISON.adoc`, `docs/integration-audit.adoc`.
84+
* `EI-2` is `[CLOSED-NEG]` (terminated negative — do not reopen).
85+
`RoleRole.agda`'s "REAL OBSTRUCTION" is a closed negative result,
86+
not debt.
87+
88+
=== CNO / absolute-zero `[REAL]`
89+
Certified Null Operations = echo types where `f = id`. absolute-zero is
90+
both a *dependency* of the core and a *bridge* target.
91+
92+
* Proofs: `proofs/agda/EchoCNOBridge.agda`, `MinimalCNO.agda`,
93+
`WorkingCNO.agda`.
94+
* Docs: `docs/ECHO-CNO-BRIDGE.adoc`,
95+
`docs/echo-types/cross-repo-bridge-status.md`.
96+
97+
=== JanusKey reversibility `[REAL]`
98+
Constructive fiber theory ↔ JanusKey "architecturally impossible data
99+
loss".
100+
101+
* Proofs: `proofs/agda/EchoJanusBridge.agda`.
102+
* Docs: `docs/EchoJanusBridge.md`, `docs/EchoBridges.md`.
103+
104+
=== Tropical / Dyadic `[REAL*]`
105+
Bridge domains enumerated in `docs/EchoBridges.md` (JanusKey / CNO /
106+
Tropical / Dyadic). Dyadic is mechanised; Tropical is named/early.
107+
108+
* Proofs: `proofs/agda/Dyadic.agda`, `proofs/agda/DyadicEchoBridge.agda`.
109+
* Docs: `docs/EchoBridges.md`.
110+
111+
=== MAA Framework integration `[ROADMAP]`
112+
Connect echo types with MAA's reversibility proofs
113+
(`maa-echo-equivalence`). absolute-zero lives under
114+
`…/verification-ecosystem/maa-framework/`. Planned, not built.
115+
116+
* Docs: `docs/ProofRoadmap.md` §10, `docs/EchoJanusBridge.md`.
117+
118+
=== Shannon / information theory `[OPEN]`
119+
Explicitly *not bridged*. The Transport / Nyquist sampling work
120+
(Gate-3) is the nearest built thread; a real Shannon-entropy /
121+
mutual-information formalisation is open.
122+
123+
* Proofs: `proofs/agda/examples/Transport.agda`.
124+
* Docs: `docs/ECHO-CNO-BRIDGE.adoc` (lines ~104, ~254),
125+
`docs/adjacency/information-flow.adoc`,
126+
`docs/gate-3-canonical.adoc`, `docs/gate-3-transport-handoff.adoc`.
127+
128+
== Tooling
129+
130+
=== ArghDA — proof-ladder workspace manager `[REAL*]`
131+
Language-agnostic proof-workspace engine (`arghda-core`, Rust). MVP.
132+
133+
* Code: `arghda-core/` (Rust crate).
134+
* Docs: `docs/arghda-spec.adoc`.
135+
136+
== Governance — proof-debt & retraction
137+
138+
The honesty layer. *Read before citing any claim above as final.*
139+
140+
* `docs/retractions.adoc` — **R-2026-05-18** retracts the
141+
graded-comonad / two-models / conservativity / universal-property
142+
framing. Those are `[RETRACTED]`, now a *loss-graded reindexing
143+
modality*; earn-back is gated, claims stay retracted until a gate
144+
passes.
145+
* `docs/echo-types/earn-back-plan.adoc` — the consolidated proof-debt
146+
ledger + falsifiable gates F1–F4 (F1 = make-or-break graded comonad;
147+
F2/F4 independent; F3 gated on F1). Current SoT for what is / isn't
148+
proven.
149+
* Gate handoffs: `docs/gate-1-distinct-phenomenon.adoc`,
150+
`docs/gate-2-handoff.adoc`, `docs/gate-3-*.adoc`.
151+
152+
== Documentation index (canonical vs historical)
153+
154+
Multiple overlapping docs exist. Use the *canonical* column; the rest
155+
are kept for history and **may overclaim** (pre-retraction).
156+
157+
[cols="1,3,3"]
158+
|===
159+
| Topic | Canonical (use this) | Historical / superseded
160+
161+
| Project map (this file)
162+
| `docs/echo-types/MAP.adoc`
163+
| `INDEX.adoc` is the *audit* index (different role; keep)
164+
165+
| Proof status / roadmap
166+
| `docs/echo-types/earn-back-plan.adoc` + `docs/retractions.adoc`
167+
| `ProofRoadmap.md`, `PRIORITIZED_PROOF_ROADMAP.md`, `WORK_PLAN.md`,
168+
`roadmap.adoc`, `roadmap-gates.adoc`, `docs/echo-types/roadmap.md`
169+
(pre-R-2026-05-18 — historical)
170+
171+
| Concept / definition
172+
| `docs/echo-types/overview.md`, `docs/echo-types/paper.adoc`
173+
| `COMPREHENSIVE_DOCUMENTATION.md`
174+
175+
| Bridges
176+
| `docs/EchoBridges.md` + this file's Directions
177+
| `docs/echo-types/cross-repo-bridge-status.md` (detail)
178+
179+
| Adjacency / related theory
180+
| `docs/adjacency/` (per-topic .adoc)
181+
| —
182+
|===
183+
184+
== Keeping this current
185+
186+
This is a living document. Whenever a direction is added, a gate
187+
passes/fails, or a claim is retracted/earned-back:
188+
189+
. Update the relevant Directions/Governance entry *and* its status tag
190+
here, in the same PR as the change.
191+
. Never duplicate detail — link to the canonical proof module / doc.
192+
. The GitHub wiki `Home` mirrors this file and must point back here as
193+
SoT; do not fork content into the wiki.

0 commit comments

Comments
 (0)