Skip to content

Commit d87781b

Browse files
hyperpolymathhyperpolymath
committed
Sync README and roadmap status across echo and bridge tracks
1 parent 0b6693d commit d87781b

4 files changed

Lines changed: 194 additions & 42 deletions

File tree

‎README.md‎

Lines changed: 129 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -1,53 +1,152 @@
11
# echo-types
22

3-
Constructive Agda formalization of echo types / fibers:
3+
Constructive Agda development for echo types as a first-class notion of structured loss:
4+
5+
loss that is not total erasure.
6+
7+
## Core Idea
8+
9+
Most formalisms foreground two clean cases:
10+
11+
- reversible / injective / linear-ish: no important loss
12+
- ordinary irreversible: loss occurs and is usually forgotten
13+
14+
Echo types target a third case:
15+
16+
- irreversible, but with a retained proof-relevant constraint on what was lost
17+
18+
This repository treats that third case as the primary object of study.
19+
20+
## Definition (Foundation)
21+
22+
Given `f : A → B`, define the fiber/echo at `y : B`:
423

524
`Echo f y := Σ (x : A) , (f x ≡ y)`
625

7-
This repository provides a minimal, explicit development in ordinary intensional dependent type theory (`--safe --without-K`) with:
26+
Current formal foundation is in:
27+
28+
- `proofs/agda/Echo.agda`
29+
- `proofs/agda/EchoCharacteristic.agda`
30+
- `proofs/agda/EchoResidue.agda`
31+
- `proofs/agda/EchoExamples.agda`
32+
- `proofs/agda/EchoChoreo.agda`
33+
- `proofs/agda/EchoEpistemic.agda`
34+
- `proofs/agda/EchoLinear.agda`
35+
- `proofs/agda/EchoGraded.agda`
36+
- `proofs/agda/EchoTropical.agda`
37+
- `proofs/agda/EchoIntegration.agda`
38+
39+
with constructive proofs (`--safe --without-K`, no postulates in `proofs/agda`):
40+
41+
- `echo-intro` (introduction into own fiber)
42+
- `map-over` (action on fibers for morphisms over fixed base)
43+
- `map-over-id` (identity law)
44+
- `map-over-comp` (composition law)
45+
- `map-square` (action along commuting squares)
46+
47+
Characteristic M2 results include:
48+
49+
- explicit non-injectivity witnesses for collapse maps
50+
- impossibility of full reconstruction from plain visible output (`no-section-*` family)
51+
- distinct echoes over the same visible value (`echo-true≢echo-false`, `stateA≢stateB`)
52+
- retained-constraint theorem for projection-style structured loss (`visible-constraint`)
53+
54+
Scope-broadening stages now include:
55+
56+
- choreographic bridge (`RoleEcho` over role projections, commuting-square transport)
57+
- epistemic bridge (indistinguishability and echo-indexed knowledge)
58+
- affine/linear bridge (strict weakening from full echoes to residues)
59+
- graded bridge (grade order and compositional degradation law)
60+
- tropical bridge (argmin-style witness residues under tropical collapse)
61+
- integration bridge (knowledge preservation under choreography plus controlled graded degradation)
62+
- indexed/relational/categorical packaging (`EchoIndexed`, `EchoRelational`, `EchoCategorical`, `EchoScope`)
63+
- cross-ecosystem bridges (`EchoCNOBridge`, `EchoJanusBridge`, `DyadicEchoBridge`, `EchoOrdinal`)
64+
65+
## Current Status Snapshot (2026-04-23)
66+
67+
On `main`, the following are true:
68+
69+
- full suite compiles: `agda -i proofs/agda proofs/agda/All.agda`
70+
- core echo/fiber laws are smoke-pinned (`echo-intro`, `map-over`, `map-over-id`, `map-over-comp`, `map-square`)
71+
- non-injectivity/no-section family is present (`collapse-non-injective`, `no-section-collapse`, `no-section-visible`, `no-section-collapse-to-residue`, `no-section-weaken`)
72+
- distinct-witness and retained-constraint exemplars are present (`echo-true≢echo-false`, `stateA≢stateB`, `visible-constraint`)
873

9-
- fiber introduction (`echo-intro`)
10-
- action on fibers over a fixed base (`map-over`)
11-
- identity law (`map-over-id`)
12-
- composition law (`map-over-comp`)
13-
- action along commuting squares (`map-square`)
74+
Ordinal/Buchholz track status:
1475

15-
## Controlled Scope Broadening
76+
- `Ordinal.Buchholz.WellFounded` provides `wf-<ᵇ : WellFounded _<ᵇ_` for the currently admitted constructor core
77+
- top-marker `bplus` bridges are admitted and inverted: `<ᵇ-+ω`, `<ᵇ-+ψω`, `<ᵇ-inv-+Ωω`, `<ᵇ-inv-+ψω`
78+
- open work remains for general `Ω/+` and `ψ/+` comparisons and shared-binder cases (`<ᵇ-ψα`, `<ᵇ-+2`) in a `--without-K`-compatible style
1679

17-
The formal scope is extended in controlled phases:
80+
## External Bridge Targets (local workspace)
1881

19-
- Phase A (`proofs/agda/EchoIndexed.agda`): role-indexed echoes `Echoᵢ` with trace-level witness separation.
20-
- Phase B (`proofs/agda/EchoEpistemicResidue.agda`): residue-based epistemic echoes `EchoR` with strict weakening/no-section results.
21-
- Phase C (`proofs/agda/EchoRelational.agda`): relational semantics `Step : S → O → Set` and output fibers `Σ s , Step s o`.
22-
- Phase D (`proofs/agda/EchoCategorical.agda`): slice/fibration packaging over the compiled deterministic and relational layers.
82+
Current bridge targets in this workspace are:
83+
84+
- `absolute-zero`: `/var/mnt/eclipse/repos/verification-ecosystem/maa-framework/absolute-zero`
85+
- `januskey`: `/var/mnt/eclipse/repos/developer-ecosystem/januskey`
86+
- `tropical-resource-typing` (potential target, not recently audited): `/var/mnt/eclipse/repos/verification-ecosystem/tropical-resource-typing` (upstream: `https://github.com/hyperpolymath/tropical-resource-typing`)
87+
88+
Note: `januskey` is not currently nested under `maa-framework` in this workspace layout.
89+
90+
Cross-repo status:
91+
92+
- bridge formalisms live in this repo (`EchoCNOBridge`, `EchoJanusBridge`, tropical-collapse witness work in `EchoTropical`)
93+
- end-to-end conformance against upstream codebases is a separate track and is not yet fully machine-checked here
94+
- see `docs/echo-types/roadmap.md` for staged cross-repo verification gates
95+
96+
## What Echo Types Are For
97+
98+
Echo types are useful when outputs are:
99+
100+
- insufficient to reconstruct their source exactly
101+
- still sufficient to constrain the source non-trivially
102+
103+
Intended proof-use cases include:
104+
105+
- non-injective computation
106+
- provenance
107+
- structured irreversibility
108+
- partial recoverability
109+
- classification up to equivalence
110+
- forensic inference from residues
111+
- refined taxonomies of information loss
112+
113+
## Identity Claim and Falsifiability
114+
115+
This repo is trying to establish echo types as a concept with its own identity.
116+
Since `Echo` is built from sigma/fiber machinery, identity will not come from syntax.
117+
It must come from role and theorems.
118+
119+
We treat the claim as established only if all three are met:
120+
121+
1. Distinct phenomenon: structured loss under non-injective computation.
122+
2. Characteristic theorem family: results that are naturally echo-shaped, not just generic sigma lemmas.
123+
3. Canonical examples: cases where echo type is the right explanatory unit.
124+
125+
If these fail, we record that result and stop the identity claim.
23126

24127
## Build
25128

26129
```bash
27130
cd /var/mnt/eclipse/repos/echo-types
28131
agda -i proofs/agda proofs/agda/Echo.agda
29-
agda -i proofs/agda proofs/agda/All.agda
30-
for f in proofs/agda/*.agda; do agda -i proofs/agda "$f"; done
31132
```
32133

33-
## Bridge to Certified Null Operations (CNOs)
134+
Full suite:
34135

35-
This repository now includes a theoretical bridge to **Certified Null Operations (CNOs)** from the [Absolute Zero](https://gitlab.com/maa-framework/6-the-foundation/absolute-zero) project.
136+
```bash
137+
cd /var/mnt/eclipse/repos/echo-types
138+
agda -i proofs/agda proofs/agda/All.agda
139+
```
36140

37-
**Key Insight**: CNOs are singleton echo types over identity functions.
141+
## Roadmap
38142

39-
**Bridge Modules**:
40-
- `proofs/agda/EchoCNO.agda` - Basic bridge with core theorems
41-
- `proofs/agda/EchoCNOBridge.agda` - Comprehensive bridge with full mapping
143+
Proof milestones and decision gates are in:
42144

43-
**Documentation**: See `docs/ECHO-CNO-BRIDGE.adoc` for detailed explanation.
145+
- `roadmap.adoc`
146+
- `docs/buchholz-plan.adoc`
44147

45-
**Main Theorems**:
46-
- `cno-echo-equivalence`: CNOs ≃ singleton echoes over identity
47-
- `all-cnos-are-echos`: All state-preserving programs are echoes over identity
48-
- `cno-composition-echo`: CNO composition preserves echo structure
148+
Open/gated work and cross-repo follow-ups are tracked in:
49149

50-
This bridge enables:
51-
- Using echo type theory for CNO verification
52-
- Cross-repository theorem sharing
53-
- Unified foundation for structured loss and null operations
150+
- `docs/echo-types/roadmap.md`
151+
- `docs/echo-types/taxonomy.md`
152+
- `docs/echo-types/composition.md`

‎docs/echo-types/roadmap.md‎

Lines changed: 14 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,14 @@
33
**Status:** planning document. Partitions work by dependency on the
44
two identified bottlenecks:
55

6-
- **Bottleneck B1.** The `--without-K` shared-binder irreflexivity
7-
block in the Buchholz `_<ᵇ_` order (`claude/buchholz-order-def`
8-
branch). Blocks full totality + WF of Buchholz notation; everything
9-
downstream that needs ordinal semantics is gated on this.
6+
- **Bottleneck B1.** The `--without-K` shared-binder constructor
7+
block in the Buchholz `_<ᵇ_` order. `wf-<ᵇ` is landed for the
8+
currently admitted core, but full totality + full-constructor
9+
well-foundedness remain gated on a K-free treatment of the shared-
10+
binder cases.
1011
- **Bottleneck B2.** Tool-scope limitations on adjacent repos
11-
(`maa-framework`, `januskey`, `absolute-zero`). Blocks end-to-end
12-
audit of the CNO and Janus bridges.
12+
(`maa-framework/absolute-zero`, `januskey`,
13+
`tropical-resource-typing`). Blocks end-to-end bridge audits.
1314

1415
Paths marked **[unblocked]** can proceed today. Paths marked
1516
**[gated on B1]** or **[gated on B2]** cannot.
@@ -107,9 +108,9 @@ Paths marked **[unblocked]** can proceed today. Paths marked
107108
Requires the shared-binder constructors, which the current Agda
108109
2.6.3 `--without-K` blocks via pattern-matching. Either an Agda
109110
upgrade or a rank-embedding proof strategy unblocks this.
110-
- **[gated on B1]** Well-foundedness `WellFounded _<ᵇ_`.
111-
Technically independent of irreflexivity if done via
112-
rank-embedding, but conventionally proved after totality.
111+
- **[gated on B1]** Extension of totality + well-foundedness proofs to
112+
the full constructor set (including shared-binder cases such as
113+
`<ᵇ-ψα` and `<ᵇ-+2`).
113114
- **[gated on B1]** Ordinal semantics of BT terms: denotation
114115
`BT → Ordinal` preserving order. Requires a formal `Ordinal` type
115116
as a prerequisite, which is itself downstream of WF.
@@ -123,6 +124,10 @@ Paths marked **[unblocked]** can proceed today. Paths marked
123124
- **[gated on B2]** Janus reversible-file-operations bridge
124125
verification against `januskey`'s actual API. Needs cross-repo
125126
access.
127+
- **[gated on B2]** Tropical-resource-typing alignment: first do a repo
128+
inventory (it is currently not recently audited), then validate
129+
`EchoTropical` witness/residue claims against that neighbouring
130+
tropical typing development.
126131
- **[gated on B2]** `maa-framework` integration. Out of scope for
127132
the current tooling; needs scope expansion or file export.
128133

‎readme.adoc‎

Lines changed: 43 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,8 @@ Current formal foundation is in:
3030

3131
* `proofs/agda/Echo.agda`
3232
* `proofs/agda/EchoCharacteristic.agda`
33+
* `proofs/agda/EchoResidue.agda`
34+
* `proofs/agda/EchoExamples.agda`
3335
* `proofs/agda/EchoChoreo.agda`
3436
* `proofs/agda/EchoEpistemic.agda`
3537
* `proofs/agda/EchoLinear.agda`
@@ -60,6 +62,42 @@ Scope-broadening stages now include:
6062
* graded bridge (grade order and compositional degradation law)
6163
* tropical bridge (argmin-style witness residues under tropical collapse)
6264
* integration bridge (knowledge preservation under choreography plus controlled graded degradation)
65+
* indexed / relational / categorical packaging (`EchoIndexed`, `EchoRelational`, `EchoCategorical`, `EchoScope`)
66+
* cross-ecosystem bridges (`EchoCNOBridge`, `EchoJanusBridge`, `DyadicEchoBridge`, `EchoOrdinal`)
67+
68+
== Current Status Snapshot (2026-04-23)
69+
70+
On `main`, the following are true right now:
71+
72+
* Full suite compiles (`agda -i proofs/agda proofs/agda/All.agda`).
73+
* Core echo/fiber theorems are present and smoke-pinned (`echo-intro`, `map-over`, `map-over-id`, `map-over-comp`, `map-square`).
74+
* Characteristic non-injectivity/no-section family is present (`collapse-non-injective`, `no-section-collapse`, `no-section-visible`, `no-section-collapse-to-residue`, `no-section-weaken`).
75+
* Distinct-witness and retained-constraint exemplars are present (`echo-true≢echo-false`, `stateA≢stateB`, `visible-constraint`).
76+
77+
Ordinal/Buchholz track status:
78+
79+
* `Ordinal.Buchholz.WellFounded` provides `wf-<ᵇ : WellFounded _<ᵇ_` for the currently admitted constructor core.
80+
* Top-marker `bplus` bridges are now admitted and inverted:
81+
** `<ᵇ-+ω`, `<ᵇ-+ψω`
82+
** `<ᵇ-inv-+Ωω`, `<ᵇ-inv-+ψω`
83+
* Open work remains for general `Ω/+` and `ψ/+` comparisons and for the shared-binder cases (`<ᵇ-ψα`, `<ᵇ-+2`) in a `--without-K`-compatible style.
84+
85+
== External Bridge Targets (local workspace)
86+
87+
Current bridge targets in this workspace are:
88+
89+
* `absolute-zero`: `/var/mnt/eclipse/repos/verification-ecosystem/maa-framework/absolute-zero`
90+
* `januskey`: `/var/mnt/eclipse/repos/developer-ecosystem/januskey`
91+
* `tropical-resource-typing` (potential target, not recently audited): `/var/mnt/eclipse/repos/verification-ecosystem/tropical-resource-typing`
92+
(upstream: `https://github.com/hyperpolymath/tropical-resource-typing`)
93+
94+
Note: `januskey` is not currently nested under `maa-framework` in this workspace layout.
95+
96+
Cross-repo status:
97+
98+
* Bridge formalisms live in this repo (`EchoCNOBridge`, `EchoJanusBridge`, tropical-collapse witness work in `EchoTropical`).
99+
* End-to-end conformance against upstream codebases is a separate track and is not yet fully machine-checked here.
100+
* See `docs/echo-types/roadmap.md` for staged cross-repo verification gates.
63101

64102
== What Echo Types Are For
65103

@@ -113,7 +151,10 @@ agda -i proofs/agda proofs/agda/All.agda
113151
Proof milestones and decision gates are in:
114152

115153
* `roadmap.adoc`
154+
* `docs/buchholz-plan.adoc`
116155

117-
Open hard questions are tracked in:
156+
Open/gated work and cross-repo follow-ups are tracked in:
118157

119-
* `docs/next-questions.adoc`
158+
* `docs/echo-types/roadmap.md`
159+
* `docs/echo-types/taxonomy.md`
160+
* `docs/echo-types/composition.md`

‎roadmap.adoc‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,13 @@ Decision policy:
1313
* If the claim can be established with precise theorems and examples, continue and scale.
1414
* If it cannot be established, document failure clearly and stop the identity claim.
1515

16+
Document map (to keep status/docs aligned):
17+
18+
* `README.md` / `readme.adoc`: current snapshot and build entry points.
19+
* `roadmap.adoc` (this file): canonical milestone log for the echo-theory track.
20+
* `docs/buchholz-plan.adoc`: canonical status for the ordinal/Buchholz WF track.
21+
* `docs/echo-types/roadmap.md`: gated and cross-repo follow-up queue.
22+
1623
== Current Foundation (Established)
1724

1825
File: `proofs/agda/Echo.agda`
@@ -118,7 +125,7 @@ Delivered in `proofs/agda/EchoCharacteristic.agda`:
118125
* `no-section-collapse`
119126
* `echo-true≢echo-false`
120127
* `visible-constraint`
121-
* `stateA≢stateB`
128+
* `state₁≢state₂`
122129
* `no-section-visible`
123130
* `transport-visible-not`
124131

0 commit comments

Comments
 (0)