Skip to content

Home

Jump to bottom
hyperpolymath edited this page May 28, 2026 · 12 revisions

echo-types — Project Map

Source of truth: docs/echo-types/MAP.adoc in the repo. This wiki mirrors it for browsing; it never forks content — always trust the in-repo file.

Structural overview

flowchart TD
    F["<b>Foundation</b><br/>Echo f y := Σ (x : A) , (f x ≡ y)<br/>= homotopy fibre"]
    AD["<b>Pillars A–D</b> (establishment plan, LANDED 2026-05-17)<br/>A: echo↔fib · B: pullback UP · C: separating model · D: carrier-parametric"]
    PF["<b>Pillar F gates</b> (earn-back, ALL PASSED)<br/>F1 graded-comonad witness · F2 2nd Echo-functor model<br/>F3 2nd non-iso grade-monoid · F4 funext-qualified pullback UP<br/>F5 funext-qualified full OFS"]
    T1["<b>Tier 1 · Canonical identity layer</b> (2026-05-27, extended 2026-05-28)<br/>EchoTotalCompletion (A ≃ Σ B Echo f) · OFS-witness · Image · no-section-of-collapsing-map · ImageFactorizationProp (epi,mono earn-back)"]
    T2["<b>Tier 2 · Classification grid</b><br/>LossTaxonomy (function-side) · ResidueTaxonomy (residue-side, 8 instances incl. Indexed, Cost, Search, Epistemic) · DecorationStructure · _≡m_"]
    T3["<b>Tier 3 · Qualified universal property</b> (Gate F5)<br/>echo-factorisation-strict · diagonal lifting · factorisation uniqueness up to iso"]
    AUD["<b>Audience surfaces</b><br/>EchoProvenance · EchoSecurity · EchoProbabilisticSupport · EchoDifferential"]
    SUITE["<b>EchoCanonicalIdentitySuite</b><br/>(curated single-file entry point)"]

    F --> AD
    AD --> PF
    F --> T1
    T1 --> T2
    T2 --> T3
    PF -.->|F5 underpins| T3
    T1 --> AUD
    T2 --> AUD
    T3 --> AUD
    T1 --> SUITE
    T2 --> SUITE
    T3 --> SUITE
    AUD --> SUITE
Loading

Recommended reading order

  1. MAP.adoc — master content map (status-tagged).
  2. EchoCanonicalIdentitySuite.agda — curated single-file Agda entry point.
  3. universal-property.adoc — categorical-UP arc end-to-end (pullback + F4 + F5/OFS), with ASCII diagrams.
  4. fibration-package.adoc — fibration-side arc (map-over + composition + cancellation + pentagon).
  5. paper.adoc — Pillar E paper (§"Post-establishment structural extensions" weaves Tier-1+2+3).
  6. retractions.adoc + earn-back-plan.adoc — honesty + Pillar F gate ledger.

Foundation: Echo functor / loss-with-residue [REAL]

Canonical identity layer [REAL] (2026-05-27): 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. K-free skeletons under --safe --without-K; full HoTT-strength upgrades documented as the next earn-back gates (Pillar F4 template).

  • Total completion — A ≃ Σ B (Echo f) (EchoTotalCompletion.agda). Every irreversible map's domain is canonically equivalent to the total space of its echoes.
  • Orthogonal factorisation system (EchoOrthogonalFactorizationSystem.agda). Every f : A → B factors as A ─encode→ Σ B (Echo f) ─proj₁→ B; left leg an equivalence, right leg a projection whose fibre at y is Echo f y.
  • Image factorisation (EchoImageFactorization.agda). Image f := Σ B (Echo f); three classifications (Surjective, Injective, projection-uniqueness). The (epi, mono) truncation form lands as EchoImageFactorizationProp.agda (2026-05-28): TruncInterface record packaging the four ∥_∥ obligations + module ImageProp with mono right leg (is-prop on truncated second component) + mere-surjective left leg (rec into truncated preimage Σ). Module-parameterised in TruncInterface — consumer plugs in Cubical ∥_∥₋₁ / HIT / postulated interface; this module stays --safe --without-K, zero postulates.
  • Generic no-section (EchoNoSectionGeneric.agda). For any collapsing map with two distinct elements landing on the same image, no section exists — structural fact, not an example.
  • Loss taxonomy (function-side) (EchoLossTaxonomy.agda). Four-axis classification: EQUIV ⇒ centre + projection-unique; INJ ⇒ projection-unique; SURJ ⇒ inhabited; CONST ⇒ section.
  • Residue taxonomy (residue-side) (EchoResidueTaxonomy.agda). record ResidueForm f R packaging the per-output residue carrier + lowering shared by the eight decoration modules. All eight decoration modules now packaged (2026-05-28 completion): trivial (⊤) / identity (Echo f) / generic Σ-cert (echoR-residue) / linear-affine / Indexed / Cost (parametric over CostAlgebra) / Search (parametric over search-completeness witness, mirrors Cost) / Epistemic (identity-residue (obs r) — indistinguishability class IS the fibre).
  • Decoration structure (observation-side) (EchoDecorationStructure.agda). record DecorationStructure G — seven-field recipe (order + refl + trans + prop + join + UMP) shared across the eight decoration modules. Four instances: Graded (3-grade), Linear (2-grade), Access (5-grade), Choreo (2-role). Plus module DegradeAbstract proving abstract degrade-compose + degrade-via-join once over the record.
  • Observational equivalence (EchoObservationalEquivalence.agda). Mode-indexed equality _≡m_ on LEcho. Linear witness-aware; affine witness-blind. Headline pins a linear-distinct / affine-equal pair as a checked theorem.

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

Retraction follow-up F-2026-05-27a logged in docs/retractions.adoc. Full Pillar F gate ledger: docs/echo-types/earn-back-plan.adoc.

Audience-facing modules (Tier 3, all landed 2026-05-27 per GPT-recommended order; each ships the abstract record + parametric theorems + worked instance + honest-bound matched-negatives):

  • Provenance (EchoProvenance.agda). Provenance record + four parametric theorems. Worked bool-over-nat-provenance instance.
  • Security (EchoSecurity.agda). Security record + per-region collapse + audit-no-recovery (factored through no-section-of-collapsing-map). Worked region-exit-audit-instance. Matched-negatives: NOT bytes-zeroed / side-channel / tamper-evident / oracle.
  • ProbabilisticSupport (EchoProbabilisticSupport.agda). Sampling record + marginal non-injectivity + Echo-carries-index + residue-loses-index. Matched-negatives: NOT measure-preserving / probability monad / Kantorovich / coupling / randomness extraction.
  • Differential (EchoDifferential.agda). Sensitivity record + blur non-injectivity + Echo-carries-perturbation
    • residue-loses-perturbation. Matched-negatives: NOT ε-DP / Lipschitz / noise calibration / adversary model.

Curated suite — single-file entry point: EchoCanonicalIdentitySuite.agda. Re-exports the load-bearing headlines from every Tier-1 / Tier-2 / Tier-3 module in the "why Echo deserves a name" reading order.

Consolidation docs (2026-05-27): two doc-only narratives threading source modules into end-to-end stories with ASCII diagrams: universal-property.adoc (pullback + F4 + F5 / OFS arc) and fibration-package.adoc (map-over + composition + cancellation + pentagon).

Plus two cementing matched-negatives against shadow encodings: Shannon-entropy non-distinguishing (EchoEntropy.agda) and the linear-logic !A := 1 shallow-encoding gap (EchoLLEncoding.agda).

Directions: Thermodynamic (Landauer/Bennett) [REAL*] · Buchholz/Veblen ordinals [REAL] (head-Ω domination LANDED 2026-05-27 PRs #130/#131/#133/#134; Slice 3 closes at ψ-rank-level 2026-05-28 via PRs #137 prereqs + #141 headline + #142 _<ᵇ¹_ umbrella + #143 RankLexSlice3 ψ-rank discharge — bplus-chain-level extension to rank-pow structurally blocked under current Brouwer arithmetic, documented in RankLexSlice3.agda; Slice 4 narrowed umbrella _<ᵇ⁻ⁿ_ LANDED 2026-05-28 via PR #149 (RankMonoUmbrellaSlice4) covering 10 inherited _<ᵇ⁰_ cases plus the strict-head joint-bplus; rank-lex pivot for the bpsi-source-at-equality sub-case scaffolded via PR #147 (RankLexJointBplus); two shortfalls pinned as ⊤-aliases (<ᵇ-ψΩ≤ boundary at lex-rank only; <ᵇ-+1 at equal-head gated on pivot completion); unbudgeted wf-<ᵇʳᶠ + full-order internalisation remain) · Characteristic/EI — epistemic, choreographic, roles [REAL] · CNO/absolute-zero [REAL] · JanusKey [REAL] · Tropical/Dyadic [REAL*] · MAA Framework [ROADMAP] · Shannon/information theory [REAL*] (discrete non-distinguishing landed; real-valued / mutual-information open) · Decoration Bridge (R5 exploratory, PR #129).

Tutorial / pedagogy [REAL]: three worked walkthroughs under tutorial/ — certified region-exit audit (Walkthrough 1, killer-app candidate), epistemic erasure (Walkthrough 2, KDF / no-section-via-residue), provenance / debugging (Walkthrough 3, section/no-section contrast across three residue layers). Each carries an honest-bound disclosure at the top and a matched-negative block at the bottom.

Tooling: ArghDA proof-ladder [REAL*]

Establishment track (Pillar E): internal programme (Pillars A–D) complete since 2026-05-17 within R-2026-05-18 narrowings. Paper

  • TYPES extended abstract under docs/echo-types/. Offline plan (venue + Zenodo + outreach) at pillar-e-offline.adoc. Paper §"Post-establishment structural extensions" weaves the 2026-05-27 Tier-1+2+3 spine into the central argument.

Governance: retraction R-2026-05-18 + earn-back ledger (F1–F5 ALL PASSED) — read before citing any claim as final.

Julia companion: EchoTypes.jl

Executable finite-domain companion — runnable shadow of the Agda library, NOT a proof. Each Julia testset = finite shadow of one named Agda lemma. Latest pin: echo-types eed4250 (2026-05-28).

  • Repo: hyperpolymath/EchoTypes.jl
  • Current release: v0.3.0 (Tier-3 audience-facing spine + cementing LL-encoding gap)
  • Hands-on exercises bridging both repos: Julia-Companion-Exercises — walk through each tier with a Julia REPL session, an Agda-side link, and an "extend this" prompt.

The companion explicitly does NOT mirror:

  • Funext-qualified surfaces (F5 strict / pullback strict, F4 template) — Julia has no funext.
  • Retracted (R-2026-05-18) framings (graded-comonad, conservativity, two-models, universal-property).
  • HoTT-strength upgrades (UIP, propositional truncation, HITs).
  • Ordinal-lane work (Slice 3/4, RankPow*, HeadOmegaInversion, RankLexJointBplus) — separate pillar; would need a new Bord carrier design.

The mirror covers exactly the K-free Tier 1+2+3 spine + the cementing matched-negatives (Entropy, LL-encoding gap). 253 passing test assertions across 18 testsets.

Edit the in-repo MAP.adoc (via a PR), not this page.

Clone this wiki locally