Skip to content

MAP.adoc

Latest commit

 

History

History
491 lines (425 loc) · 23.3 KB

MAP.adoc

File metadata and controls

491 lines (425 loc) · 23.3 KB
Raw

echo-types: Master Map

The single source of truth for "what is in echo-types and where." If you cannot find something, it is indexed here or it does not exist. This file supersedes the navigational role of the scattered overview / roadmap / taxonomy docs (which remain as detail, linked below). Keep it current: every new direction or status change updates this file in the same PR.

Note
 This is the content/architecture map. For the per-session audit trail (which finding lives in which 6a2 capture) see ../../INDEX.adoc — different purpose, complementary.
Table of Contents

Status legend

[REAL]

Mechanised in Agda --safe --without-K, on origin/main.

[REAL*]

Real but partial / graded — see the linked status.

[ROADMAP]

Planned/specified, not yet built.

[OPEN]

Acknowledged gap; explicitly not bridged yet.

[RETRACTED]

Claim withdrawn by retraction R-2026-05-18; under a falsifiable earn-back gate (see Governance).

[CLOSED-NEG]

Settled as a negative result (do not reopen).

The canonical state is always origin/main. Local working clones drift behind — git fetch and read origin/main before trusting any survey.

Foundation

Echo functor / loss-with-residue. The theory of the structured remainder of information-losing computation: for f : A → B, Echo f y := Σ (x : A), (f x ≡ y). [REAL]

  • Kernel: proofs/agda/EchoKernel.agda — the funext-free, postulate-free core (re-export of Echo + a pinned Kernel-contract). [REAL] Everything else imports Echo transitively; the kernel-vs-derived classification + funext-free certificate is docs/echo-types/echo-kernel-note.adoc.

  • Proofs: proofs/agda/Echo.agda, proofs/agda/EchoKernel.agda, proofs/agda/EchoFiberTriangulation.agda, and the derived Echo*.agda modules classified in docs/echo-types/echo-kernel-note.adoc.

  • Library: echo-types.agda-lib (depend: standard-library absolute-zero).

  • Concept doc: docs/echo-types/overview.md, docs/echo-types/types-abstract.adoc, docs/echo-types/paper.adoc.

Canonical identity layer [REAL]

The named-theorem load-bearing artefacts that promote Echo from a useful construction to a named structural object: the canonical fibre-completion functor + one leg of the (equivalence, projection) orthogonal factorisation system on Type. Landed 2026-05-27 under R-2026-05-18 honest-scope discipline — K-free skeletons land here; full HoTT-strength upgrades (contractible / propositional fibres, (-1)-truncation, full ↔) are documented as the next earn-back gates in the Pillar F4 template style.

  • Total completion — A ≃ Σ B (Echo f). The slogan-unlock: every irreversible map’s domain is canonically equivalent to the total space of its echoes. proofs/agda/EchoTotalCompletion.agda.

  • Orthogonal factorisation system — every f : A → B factors as A ─encode→ Σ B (Echo f) ─proj₁→ B with the left leg an equivalence (the totality theorem above) and the right leg a projection whose fibre at y is Echo f y. Architectural keystone. proofs/agda/EchoOrthogonalFactorizationSystem.agda.

  • Image factorisation — Image f := Σ B (Echo f); the proof- relevant image IS the total Echo space. Three classifications (Surjective, Injective, projection-uniqueness under injectivity). proofs/agda/EchoImageFactorization.agda.

  • Image factorisation, (epi, mono) form (2026-05-28) — the (epi, mono) earn-back module, module-parameterised in a truncation interface. Companion to EchoImageFactorization; the previously-pending (epi, mono) form now lands without committing the kernel to a specific truncation primitive. proofs/agda/EchoImageFactorizationProp.agda.

  • Generic no-section — no-section-of-collapsing-map: for ANY collapsing map with two distinct elements landing on the same image, no section exists. Lifts the previous single-instance result to a structural fact about non-injectivity-at-a-point; recovers the original as a one-line corollary. proofs/agda/EchoNoSectionGeneric.agda.

  • Loss taxonomy (function-side) — four-axis classification of f : A → B by echo shape: EQUIV ⇒ centre + projection-unique; INJ ⇒ projection-unique; SURJ ⇒ every fibre inhabited; CONST ⇒ section from the entire domain. K-free skeletons across all four. proofs/agda/EchoLossTaxonomy.agda.

  • Residue taxonomy (residue-side) — record ResidueForm f R packaging the per-output residue carrier + lowering shared by the eight decoration modules. Eight instances (as of 2026-05-28): the original endpoint pair (trivial (⊤), identity (Echo f)), the generic Σ-cert (echoR-residue), linear-affine-residue, the 2026-05-27 audit-follow-ons indexed-residue
    cost-residue, and the 2026-05-28 additions search-residue
    epistemic-residue. The remaining two decoration modules documented as structurally compatible. proofs/agda/EchoResidueTaxonomy.agda.

  • Decoration structure (observation-side) — record DecorationStructure G packaging the seven-field decoration recipe (order + refl + trans + propositionality + join + UMP) shared across the eight decoration modules. Three instances: Graded (3-grade), Linear (2-grade), Access (5-grade). proofs/agda/EchoDecorationStructure.agda.

  • Observational equivalence — mode-indexed equality ≡m on LEcho. Linear is witness-aware (≡); affine is witness-blind (⊤). Headline mode-equality-strictly-finer-at-linear exhibits a linear-distinct / affine-equal pair, closing the "affine forgets what linear retains" story at the equality level. proofs/agda/EchoObservationalEquivalence.agda.

Qualified universal property (Pillar F, Gate F5 FULL PASS, 2026-05-27). Three slices in the F4 template (funext as explicit module parameter, never a postulate; unconditional pointwise corollaries kept funext-free) earn back the (equivalence, projection) orthogonal factorisation system on Type at the qualified level:

  • F5-1 — echo-factorisation-strict (funext) : f ≡ proj₁ ∘ encode f. proofs/agda/EchoOFSUnivF5.agda.

  • F5-2 — Diagonal lifting property (Pointwise + Strict modules). proofs/agda/EchoOFSUnivF5Diag.agda.

  • F5-3 — Factorisation uniqueness up to iso (Pointwise
    Strict modules) via the composition design φ.to = encode f ∘ g⁻¹. proofs/agda/EchoOFSUnivF5Iso.agda.

Retraction follow-up F-2026-05-27a logged in docs/retractions.adoc. See docs/echo-types/earn-back-plan.adoc status entry for the full gate-pass record.

Audience-facing modules (Tier 3, GPT-recommended order, all landed 2026-05-27). Each generalises one concrete example into the shape the audience speaks in. All four ship the abstract record + parametric headline theorems + worked instance
honest-bound matched-negative block.

  • Provenance — Provenance record + module ProvenanceTheorems. Worked bool-over-nat-provenance reproduces EchoExampleProvenance. proofs/agda/EchoProvenance.agda.

  • Security — Security record + module SecurityTheorems. Per-region exit collapse + audit-no-recovery (factored through EchoNoSectionGeneric.no-section-of-collapsing-map). Worked region-exit-audit-instance reproduces the tutorial/region_exit_audit/RegionExitAudit.agda walkthrough. Honest-bound: NOT bytes-zeroed / side-channel-safe / tamper-evident / oracle-recovery. proofs/agda/EchoSecurity.agda.

  • ProbabilisticSupport — Sampling record + module SamplingTheorems. Marginal non-injectivity, Echo carries which index, residue loses index. Worked bool-indexed-nat-sampling. Honest-bound: NOT measure-preserving / probability monad / Kantorovich / coupling / randomness extraction. proofs/agda/EchoProbabilisticSupport.agda.

  • Differential — Sensitivity record + module SensitivityTheorems. Blur non-injectivity, Echo carries which perturbation, residue loses perturbation. Worked bool-perturbed-nat-sensitivity. Honest-bound: NOT ε-DP / Lipschitz bound / noise calibration / adversary model. proofs/agda/EchoDifferential.agda.

Curated suite — single-file entry point. The narrative deliverable that pulls the Tier-1 / Tier-2 / Tier-3 named theorems into one readable file. Re-exports load-bearing headlines from every module under suite-side names; companion remark documents honest scope at the suite level. External-reader workflow: start here + read source-module companion remarks for the headlines that interest you. proofs/agda/EchoCanonicalIdentitySuite.agda.

Consolidation docs (2026-05-27). Two doc-only narratives threading the universal-property and fibration-package stories end-to-end. Each cites the source modules + reading order; no new proofs.

  • docs/echo-types/universal-property.adoc — pullback presentation + R-2026-05-18 narrowing + Gate F4 + Gate F5 (full OFS, three slices). Threads the categorical universal-property arc.

  • docs/echo-types/fibration-package.adoc — map-over* action
    Echo-comp-iso accumulation + cancel-iso cancellation
    pentagon coherence. Threads the fibration-side story.

Cementing matched-negatives. Two shadow encodings that have been proposed as adequate substitutes for Echo, now provably aren’t:

  • Shannon-entropy non-distinguishing — the fibre-count entropic shadow agrees on echo-true vs echo-false, while the witness side distinguishes them (matched-negative against EchoAbstractionBarrier.sigma-distinguishes). proofs/agda/EchoEntropy.agda.

  • Linear-logic shallow-encoding gap — the canonical LL !A := 1 shadow admits a section that the source LEcho provably does not. proofs/agda/EchoLLEncoding.agda.

Directions

Thermodynamic — Landauer/Bennett energy bounds [REAL]

Landauer/Bennett bound shape; ThermodynamicallyReversible(p) ≙ Echo p σ ≃ Echo id σ. Zero-cost (Bennett) proved for every injective map on any Bishop-finite carrier, and lifted to an arbitrary carrier with no finiteness at all (K-free subsingleton / occupancy route), certified faithful against the established count and instantiated on the genuine infinite absolute-zero Program CNO — "a CNO dissipates zero Landauer energy" is now a real theorem, not the historically vacuous claim. The one residual — the quantitative collapse functional on an infinite carrier, O-THERMO-∞ — is now [CLOSED-NEG]: its impossibility is mechanised (collapse-cost-impossible, the doc’s own kill condition discharged negatively). No open obligation remains for this Direction; tag advanced [REAL*] → [REAL]. Re-rated B / ~95% in STABILITY_ANALYSIS §3.3 (was C+ / ~70% then B- / ~90%, 2026-05-18); the standing B- freeze lifted because O-THERMO-∞ is now discharged (negatively). The Information-Theory bridge is a separate Direction (see Shannon entry), not part of this one.

  • Proofs: proofs/agda/EchoThermodynamics.agda, proofs/agda/EchoFiberCount.agda, proofs/agda/EchoThermodynamicsFinite.agda, proofs/agda/EchoThermodynamicsArbitrary.agda, proofs/agda/EchoThermoCollapseImpossible.agda.

  • Docs: docs/ECHO-CNO-BRIDGE.adoc §"Thermodynamic Bridge", docs/STABILITY_ANALYSIS.md §3.3, docs/adjacency/hott-fibers.adoc.

  • Build: just test-thermo.

Buchholz / Veblen ordinals — higher-order number systems [REAL]

Staged Buchholz-style collapsing in --safe --without-K.

  • Proofs: proofs/agda/Ordinal/ (Buchholz/, Brouwer, CNF, Closure, Psi…, ExtendedOrder, RankPow, RankAdm, RankLex, HeadOmega, HeadOmegaInversion, RankPowDomination, RankPowSlice3 (2026-05-28 — NonBzero + strict-jump bridge
    head-Ω lower bound), RankPowSlice3Headline (2026-05-28 — Slice 3 headline rank-mono-<ᵇ-1-via-head-Ω` closed under a strict-head premise; umbrella case-split bumps `bpsi=bpsi at equal markers` to rank-adm / rank-lex)), `RankLexJointBplus` (2026-05-28 PR #147 — parallel rank with `leftmost-α` discriminator for the bpsi-source- at-equality joint-bplus sub-case; second-component strict-mono at equal first components scaffolded; (a)(b)+(c) assembly completed 2026-05-30 via PRs #165 (b lex-first primitive) + #166 (c `BplusFirstTri trichotomy + first-eq-from-bpsi-source-at- equal-head consumer-side derivation)), RankMonoUmbrellaSlice4 (2026-05-28 PR #149 — narrowed <ᵇ⁻ⁿ umbrella record bundling WfCNF endpoints + <ᵇ¹ derivation; covers all 10 inherited <ᵇ⁰ cases + the strict-head joint-bplus; two shortfalls (<ᵇ-ψΩ≤ boundary; <ᵇ-+1 at equal-head) pinned as ⊤-aliases with explicit lex-rank / rank-lex-jb pointers), RankMonoSameLeft (2026-05-30 PR #167 — Path-3 prototype source-rule enrichment via <ᵇ⁺²-same-left; one-line closure via rank-pow-bplus-right-mono), RankMonoUnion (2026-05-30 PR #168 — architectural realisation: union umbrella <ᵇᵘ = <ᵇ¹ ⊎ <ᵇ⁺² via Sum + [,] mediator; per-extension proof work + structural composition; extension recipe in preamble), RankMonoUnionWfCNF (2026-05-30 PR #169 — WfCNF wrap <ᵇᵘⁿ bundling canonical-form invariant alongside the union; mirrors Slice 4’s pattern, propagates automatically through new extensions), RankMonoUnionWF (2026-05-30 PR #170 — Gate 2 closure: WellFounded <ᵇᵘ via Subrelation.wellFounded
    On.wellFounded rank-embedding transport from wf-<′).

  • Docs: docs/buchholz-plan.adoc, docs/echo-types/buchholz-extended-wf.md, docs/echo-types/buchholz-rank-obstruction.adoc (per-constructor verdict table — see ledger for live count).

  • Direct-constructor <ᵇ same-binder cases (Buchholz item B): status tracked solely in the earn-back ledger (docs/echo-types/earn-back-plan.adoc, row B) and docs/retractions.adoc (F-2026-05-18b) — off the paper critical path. (Reference-only by design: no status is snapshotted here, so this line never drifts as the ledger moves.)

Characteristic / EI — epistemic, choreographic, roles [REAL]

The echo-invariant line: epistemic structure, choreographies, roles.

  • Proofs: proofs/agda/characteristic/ (15 modules — ChoreoInjective, RoleMode, RoleRole, RoleGraded, ModeGraded, NonTruncatable, RecipeNonTriviality, RecipeTheorem, …), proofs/agda/EchoChoreo.agda.

  • Docs: docs/characteristic.adoc, docs/EI2_REPORT.adoc, docs/EI2_READINGS_COMPARISON.adoc, docs/integration-audit.adoc.

  • EI-2 is [CLOSED-NEG] (terminated negative — do not reopen). `RoleRole.agda’s "REAL OBSTRUCTION" is a closed negative result, not debt.

CNO / absolute-zero [REAL]

Certified Null Operations = echo types where f = id. absolute-zero is both a dependency of the core and a bridge target.

  • Proofs: proofs/agda/EchoCNOBridge.agda, MinimalCNO.agda, WorkingCNO.agda.

  • Docs: docs/ECHO-CNO-BRIDGE.adoc, docs/echo-types/cross-repo-bridge-status.md.

JanusKey reversibility [REAL]

Constructive fiber theory ↔ JanusKey "architecturally impossible data loss".

  • Proofs: proofs/agda/EchoJanusBridge.agda.

  • Docs: docs/EchoJanusBridge.md, docs/EchoBridges.md.

Ephapax L3 — linear/affine modality bridge [REAL]

Cross-repo navigability marker for the hyperpolymath/ephapax programming-language project, whose L3 layer (formal/Echo.v, 584 lines, 24 Qed, zero Admitted / zero Axiom) is an explicit Coq port of EchoLinear.agda + EchoResidue.agda under a K-free / zero-axiom discipline equivalent to --safe --without-K. The Coq headlines (mode_le_prop, weaken_collapses_distinction, affine_canonical, degrade_mode_comp, no_section_collapse_to_residue) each carry the same theorem as the Agda counterpart.

Scope is intentionally NARROW: this is import-time documentation
two definitional refl-renames of the load-bearing Agda symbols under ephapax-L3--prefixed names, so a silent upstream rename trips Smoke.agda. The cross-repo content correspondence is already discharged by coqc on the ephapax side; no Lane 4 CI dependency.

  • Proofs: proofs/agda/EchoEphapaxBridge.agda (ephapax-L3-weaken ↔ EchoLinear.weaken ↔ ephapax formal/Echo.v weaken; ephapax-L3-no-section-collapse ↔ EchoResidue.no-section-collapse-to-residue ↔ ephapax formal/Echo.v:502-517 no_section_collapse_to_residue).

  • External corroboration scope: L3 only — ephapax-affine and L1/L2/L4 are NOT mechanised to the same standard (see ephapax formal/PRESERVATION-DESIGN.md + docs/echo-types/paper.adoc §"Threats to validity").

Tropical / Dyadic [REAL*]

Bridge domains enumerated in docs/EchoBridges.md (JanusKey / CNO / Tropical / Dyadic). Dyadic is mechanised; Tropical is named/early.

  • Proofs: proofs/agda/Dyadic.agda, proofs/agda/DyadicEchoBridge.agda.

  • Docs: docs/EchoBridges.md.

MAA Framework integration [ROADMAP]

Connect echo types with MAA’s reversibility proofs (maa-echo-equivalence). absolute-zero lives under …/verification-ecosystem/maa-framework/. Planned, not built.

  • Docs: roadmap.adoc §"Deferred research track", docs/EchoJanusBridge.md.

Shannon / information theory [REAL*]

Partial. The discrete non-distinguishing form lands as EchoEntropy.agda — the fibre-count shadow (uniform-prior Shannon surrogate) cannot tell echoes apart at a collapsing point, while the witness side can. Real-valued H(P) = -Σ p log p, mutual information, and the Transport/Nyquist (Gate-3) bridge remain open. See Canonical identity layer for the cementing artefact.

  • Proofs: proofs/agda/EchoEntropy.agda, proofs/agda/examples/Transport.agda.

  • Docs: docs/ECHO-CNO-BRIDGE.adoc (lines ~104, ~254), docs/adjacency/information-flow.adoc, docs/gate-3-canonical.adoc, docs/gate-3-transport-handoff.adoc.

Tutorial / pedagogy [REAL]

Three worked walkthroughs landing 2026-05-26/27 under tutorial/, each following the honest-bound + matched-negative discipline (disclosure at top + NotProved-* ⊤-aliases at bottom). Build with agda --library-file=/tmp/agda-libs -i . -i proofs/agda tutorial/All.agda.

  • Walkthrough 1 — certified region-exit audit (tutorial/region_exit_audit/). ephapax-L3-style region exit modelled type-level via EchoLinear.no-section-weaken. Formally-accepted killer-app artefact per roadmap.adoc §"Closed lanes" (Lane 5 close-out 2026-05-30).

  • Walkthrough 2 — epistemic erasure (tutorial/epistemic_erasure/). 4-seed → 2-key KDF with no-section-via-residue lifted from EchoResidue.no-section-collapse-to-residue. Heads off the "does echo-types prove key zeroing?" category-error question.

  • Walkthrough 3 — provenance / debugging (tutorial/provenance_debugging/). 4-element State with two orthogonal sign bits walked through 3 residue layers. Ships both a section (Layer 1) and its absence (Layer 2), exhibiting the boundary at which type-level recovery flips.

Track-level docs: tutorial/README.adoc, plus per-walkthrough README.adoc files. Lane policy status: see roadmap.adoc §"Closed lanes" — Lane 5 closed 2026-05-30 via the formally-accepted killer-app branch (Walkthrough 1).

Tooling

ArghDA — proof-ladder workspace manager [REAL*]

Language-agnostic proof-workspace engine (arghda-core, Rust). MVP. Extracted to its own repository 2026-05-30 (see echo-types#159 for the move record); was previously in-tree under arghda-core/.

  • Repo: https://github.com/hyperpolymath/arghda-core

  • Docs: docs/arghda-spec.adoc (in the new repo).

  • Relationship to echo-types: motivated by the proof pipeline here but operates on any --safe --without-K Agda workspace; not a build-dependency.

EchoTypes.jl — Executable Julia companion [REAL]

Mirrors the finite-domain shadow of the Tier-1 + Tier-2 spine + the unconditional fragment of the F5 OFS earn-back. v0.2.0 (2026-05-27, pinned to e7dded6) extends the original v0.1.0 coverage (Echo, EchoResidue, EchoFiberCount, EchoThermodynamics) with seven new shadows for the canonical-identity spine: EchoTotalCompletion, EchoOrthogonalFactorizationSystem (unconditional fragment), EchoImageFactorization, EchoNoSectionGeneric, EchoLossTaxonomy, EchoEntropy, EchoObservationalEquivalence.

  • Repo: https://github.com/hyperpolymath/EchoTypes.jl

  • Registry: julia-professional-registry (registered via PR #16).

  • Scope inheritance: R-2026-05-18 retraction surface NOT mirrored; F5 funext-qualified clauses (uniqueness up to iso, diagonal lifting) NOT mirrored — Julia has no funext, the claims would be vacuous; UIP- and truncation-strength upgrades likewise honestly not mirrored.

  • Discipline: falsifies-by-counterexample over concrete finite data; the companion makes no proof claims, the Agda here remains the source of truth. No in-repo CI dependency in either direction.

Bridge-status row: docs/bridges/cross-repo-bridge-status.md §"EchoTypes.jl executable mirror".

Governance — proof-debt & retraction

The honesty layer. Read before citing any claim above as final.

  • docs/retractions.adoc — R-2026-05-18 retracts the graded-comonad / two-models / conservativity / universal-property framing. Those are [RETRACTED], now a loss-graded reindexing modality; earn-back is gated, claims stay retracted until a gate passes.

  • docs/echo-types/earn-back-plan.adoc — the consolidated proof-debt ledger + falsifiable gates F1–F4 (F1 = make-or-break graded comonad; F2/F4 independent; F3 gated on F1). Current SoT for what is / isn’t proven. Current gate modules on main include proofs/agda/EchoGradedComonadF1.agda, proofs/agda/EchoPullbackUnivF4.agda, proofs/agda/EchoStepNDModelF2.agda, proofs/agda/EchoGradedComonadInterface.agda, proofs/agda/EchoGradedComonadInstance1.agda, and proofs/agda/EchoGradedComonadInstance2.agda, each scoped by the ledger.

  • Gate handoffs: docs/gate-1-distinct-phenomenon.adoc, docs/gate-2-handoff.adoc, docs/gate-3-*.adoc.

Documentation index (canonical vs historical)

Multiple overlapping docs exist. Use the canonical column; the rest are kept for history and may overclaim (pre-retraction).

Topic Canonical (use this) Historical / superseded

Project map (this file)

docs/echo-types/MAP.adoc

INDEX.adoc is the audit index (different role; keep)

Proof status / roadmap

roadmap.adoc (single canonical roadmap; lanes, gates, deferred research) + docs/echo-types/earn-back-plan.adoc
docs/retractions.adoc

roadmap-gates.adoc (pre-R-2026-05-18 — historical; folded into roadmap.adoc)

Concept / definition

docs/echo-types/overview.md, docs/echo-types/paper.adoc

COMPREHENSIVE_DOCUMENTATION.md

Bridges

docs/EchoBridges.md + this file’s Directions

docs/echo-types/cross-repo-bridge-status.md (detail)

Adjacency / related theory

docs/adjacency/ (per-topic .adoc)

—

Keeping this current

This is a living document. Whenever a direction is added, a gate passes/fails, or a claim is retracted/earned-back:

  1. Update the relevant Directions/Governance entry and its status tag here, in the same PR as the change.

  2. Never duplicate detail — link to the canonical proof module / doc.

  3. The GitHub wiki Home mirrors this file and must point back here as SoT; do not fork content into the wiki.