|
1 | 1 | // SPDX-License-Identifier: CC-BY-4.0 |
2 | 2 | = echo-types: explain me |
3 | | -:icons: font |
4 | | -:toc: |
5 | | -:toclevels: 2 |
6 | 3 |
|
7 | | -== One paragraph |
8 | | - |
9 | | -`echo-types` is a constructive Agda formalisation of *echo types* — a way of treating "loss that is not total erasure" as a first-class object. Given a function `f : A -> B`, the *echo* at `y : B` is `Σ (x : A), (f x ≡ y)`: the proof-relevant set of inputs that map to `y`. Echo types target the third case between fully reversible (no loss) and fully irreversible (forgotten): irreversible-but-with-retained-proof-relevant-constraint-on-what-was-lost. Bridges connect echoes to affine/linear types, graded modalities, tropical semirings, choreographic projections, and epistemic indistinguishability. |
10 | | - |
11 | | -== One sentence |
12 | | - |
13 | | -echo-types is part of the hyperpolymath ecosystem; it serves the *foundation* role for proof-relevant lossy computation. |
14 | | - |
15 | | -== Why does this exist? |
16 | | - |
17 | | -Many real-world transforms lose information but not all of it: a checkpoint hash retains a constraint on its preimage, a privacy projection retains a constraint on the original record, a choreographic role-projection retains a constraint on the global state. Without echo types, formal arguments about these constructions either pretend the loss is total (over-strong) or pretend the loss is reversible (under-strong). Echo types give the middle case a precise treatment. |
18 | | - |
19 | | -== Who is this for? |
20 | | - |
21 | | -* Authors of formally-verified protocols where role projections / privacy collapses / lossy aggregations need typed witnesses for what was retained. |
22 | | -* Authors of refinement-typed and graded type systems looking for a foundational vocabulary for loss-with-residue. |
23 | | -* Anyone designing audit / provenance / hash-chain systems who wants a proof-relevant account of what the audit step preserves. |
24 | | - |
25 | | -== Applied prototype hook |
26 | | - |
27 | | -`docs/echo-types/prototypes/warrant_debugger_prototype.jsx` is the |
28 | | -current doc-side React sketch for the warrant/debugging surface. It |
29 | | -belongs below the semantic-fibre vocabulary, not in the README |
30 | | -headline: it shows an empty-fibre contradiction and cost-disclosed |
31 | | -repair moves (weaken, widen, soft support) for readers who want to see |
32 | | -how "warrant" might appear in tooling. It is not an Agda proof artefact |
33 | | -and does not change the kernel/status claims. |
34 | | - |
35 | | -== Status snapshot |
36 | | - |
37 | | -Per `.machine_readable/6a2/STATE.a2ml`: |
38 | | - |
39 | | -* Core echo / fiber theorems present (`echo-intro`, `map-over`, `map-over-id`, `map-over-comp`, `map-square`). |
40 | | -* Characteristic non-injectivity / no-section family present. |
41 | | -* Bridges: linear, graded, tropical, choreographic, epistemic, CNO, Janus, Dyadic, Ordinal, Indexed, Relational, Categorical, Scope. |
42 | | -* Investigation EI-2 (integration-recipe distinctness) terminated negatively via PATH B. |
43 | | -* `.machine_readable/6a2/STATE.a2ml § ei-2` is the authoritative record; do not reopen. |
44 | | - |
45 | | -Ongoing tracks at a glance (point-in-time, see `roadmap.adoc` for the live status): |
46 | | - |
47 | | -* *Identity claim.* `docs/retractions.adoc` R-2026-05-18 narrows the public claim to a *loss-graded reindexing modality* over a thin poset (not a graded comonad). Every newer artefact is stated within those narrowings. |
48 | | -* *Ordinal / Buchholz track.* 11 of 13 per-constructor rank-mono cases closed under the WfCNF-restricted `_<ᵇ⁻_` via the `RankPow` / `RankAdm` / `RankLex` slices. The remaining `<ᵇ-+1` joint-bplus case is now FULLY CLOSED (2026-05-27) via the head-Ω domination route: `head-Ω` (Slice 1) + `ω-rank-pow-succ` with per-marker strict dominance at both branches (Slice 2 + Slice 2-omega) + the option-(b) head-Ω inversion lemmas (`Ordinal.Buchholz.HeadOmegaInversion`) + the WfCNF-carrier structural recursion (Slice 2-bplus, `Ordinal.Buchholz.RankPowDomination.rank-pow-dominated-by-head-Ω`). See `docs/echo-types/buchholz-rank-obstruction.adoc`. |
49 | | -* *Ordinal / Buchholz track — Slice 3 (2026-05-28).* `Ordinal.Buchholz.RankPowSlice3` lands three primitives — `NonBzero` (left-spine non-bzero predicate), `ω-rank-pow-succ-≤-via-<Ω` (strict-jump bridge), and `head-Ω-lower-bound` (dual of `rank-pow-dominated-by-head-Ω`). On top of those, `Ordinal.Buchholz.RankPowSlice3Headline` closes the Slice 3 headline `rank-mono-<ᵇ-+1-via-head-Ω` via Route A — a clean chain through the four prerequisites with no structural recursion, taking the strict-head premise `head-Ω x₁ <Ω head-Ω y₁` as an *external hypothesis*. PR #142 wired the umbrella case-split (`_<ᵇ¹_` extension with joint-bplus + strict-head dispatch). PR #143 added the lex-rank companion: the `bpsi-source-at-equality` ψ-rank discharge — closing the last remaining sub-case via rank-lex. The `<ᵇ-+1` joint-bplus rank-mono closure is now substantively complete via the head-Ω + lex-rank composition. |
50 | | -* *Canonical identity layer (Tier 1 + Tier 2 extensions, 2026-05-28).* `EchoImageFactorizationProp` lands the (epi, mono) earn-back module, module-parameterised in a truncation interface (Tier 2, adjacent to `EchoImageFactorization`). `EchoResidueTaxonomy`'s `ResidueForm f R` record gains `Search` and `Epistemic` instances bringing the total to eight (alongside the existing trivial, identity, generic Σ-cert, linear-affine, indexed, cost — the latter two landed 2026-05-27 as audit follow-ons). |
51 | | -* *CI / foundational hygiene (2026-05-28).* Kernel-guard discipline scaled to the canonical-identity cohort: 18 previously-unclassified `Echo*.agda` modules (the canonical-identity / OFS cohort plus the application/extension modules — `EchoEntropy`, `EchoLLEncoding`, `EchoProvenance`, `EchoSecurity`, `EchoProbabilisticSupport`, `EchoDifferential`) are now classified in `docs/echo-types/echo-kernel-note.adoc`. The (now-stale) `N5Falsifier` xfail gate was removed from `.github/workflows/agda.yml` following the 2026-05-27 resolution of `proofs/agda/characteristic/N5Falsifier.agda` (the unsolved-metas were an inference blocker, not a content blocker; four `applyRole` / `applyGrade` call sites had their implicit `r` / `grade` pinned). This is infrastructure honesty, not a proof-content advance. |
52 | | -* *Tutorial track (Lane 5).* Three worked walkthroughs under `tutorial/` (certified region-exit audit, epistemic erasure, provenance/debugging echo); each carries an honest-bound disclosure at the top and a matched-negative block at the bottom. The tutorial tree builds with the repo root added to the Agda include path; see `tutorial/README.adoc`. |
53 | | -* *Establishment track (Pillar E).* Internal programme (Pillars A–D) complete since 2026-05-17. The paper (`docs/echo-types/paper.adoc`) is a living draft with remaining `[EXPAND]` tags; the venue + Zenodo + outreach plan sits in `docs/echo-types/pillar-e-offline.adoc` (author-driven). |
54 | | - |
55 | | -== Where to look first |
56 | | - |
57 | | -* `docs/echo-types/MAP.adoc` — the master map (every direction, status-tagged). |
58 | | -* `docs/echo-types/echo-kernel-note.adoc` — kernel-vs-derived classification; status SoT for the `Echo*.agda` dependency cone. |
59 | | -* `docs/echo-types/prototypes/README.adoc` — doc-side UI prototype index; currently the warrant debugger sketch. |
60 | | -* `roadmap.adoc` + `roadmap-gates.adoc` — lane structure + identity-claim gates. |
61 | | -* `tutorial/README.adoc` — the pedagogy track if you want to read worked examples first. |
62 | | -* `docs/retractions.adoc` — read before citing any claim above as final. |
| 4 | +This file is a pointer: the canonical README is link:README.md[README.md]. The quick-orientation content formerly kept here was deduplicated on 2026-06-12 — the ecosystem-role line and the "who is this for" audience list were folded into README.md §"What Echo Types Are For"; the status snapshot lives at README.md §"Current Status Snapshot" (with `docs/echo-types/MAP.adoc` and `roadmap.adoc` as the live status sources). The full prior content remains available in git history. |
0 commit comments