Skip to content

EXPLAINME.adoc

Latest commit

 

History

History
51 lines (36 loc) · 6.49 KB

EXPLAINME.adoc

File metadata and controls

51 lines (36 loc) · 6.49 KB
Raw

echo-types: explain me

Table of Contents

One paragraph

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.

One sentence

echo-types is part of the hyperpolymath ecosystem; it serves the foundation role for proof-relevant lossy computation.

Why does this exist?

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.

Who is this for?

  • Authors of formally-verified protocols where role projections / privacy collapses / lossy aggregations need typed witnesses for what was retained.

  • Authors of refinement-typed and graded type systems looking for a foundational vocabulary for loss-with-residue.

  • Anyone designing audit / provenance / hash-chain systems who wants a proof-relevant account of what the audit step preserves.

Status snapshot

Per .machine_readable/6a2/STATE.a2ml:

  • Core echo / fiber theorems present (echo-intro, map-over, map-over-id, map-over-comp, map-square).

  • Characteristic non-injectivity / no-section family present.

  • Bridges: linear, graded, tropical, choreographic, epistemic, CNO, Janus, Dyadic, Ordinal, Indexed, Relational, Categorical, Scope.

  • Investigation EI-2 (integration-recipe distinctness) terminated negatively via PATH B.

  • .machine_readable/6a2/STATE.a2ml § ei-2 is the authoritative record; do not reopen.

Ongoing tracks at a glance (point-in-time, see roadmap.adoc for the live status):

  • 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.

  • 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.

  • 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.

  • 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).

  • 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.

  • 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.

  • 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).

Where to look first

  • docs/echo-types/MAP.adoc — the master map (every direction, status-tagged).

  • docs/echo-types/echo-kernel-note.adoc — kernel-vs-derived classification; status SoT for the Echo*.agda dependency cone.

  • roadmap.adoc + roadmap-gates.adoc — lane structure + identity-claim gates.

  • tutorial/README.adoc — the pedagogy track if you want to read worked examples first.

  • docs/retractions.adoc — read before citing any claim above as final.