EchoTypes.jl

An executable companion to the Agda library hyperpolymath/echo-types.

It computes the finite-domain shadow of theorems that are mechanised in Agda under --safe --without-K with zero postulates. It lets you run the echo / residue / Landauer constructions on concrete finite data and check their stated laws numerically.

What this is — and is not

• ✅ It is a finite, executable model: enumerate fibres, exercise functoriality and the composition/cancel isomorphisms, lower echoes to residues, and compute the finite Landauer/Bennett bound shape.

• ❌ It is not a proof. Julia has no proof checker. Every guarantee lives in the Agda. This package can falsify by counterexample but it cannot prove.

• ❌ No retracted claims appear here. Per echo-types docs/retractions.adoc R-2026-05-18, the graded-comonad, two-models, universal-property and conservativity framings are [RETRACTED] and under upstream earn-back gates. None of that surface is reproduced here. What is here is the post-retraction honest core: a loss-graded reindexing view (Echo functor + functoriality
  accumulation iso), the residue weakening (EchoR, with its strict non-recoverability witness), and the finite-domain Landauer/Bennett bound shapes.

Semantic fibre in finite domains

The Agda repository is the formal source of truth. This package is the executable finite-domain shadow: it lets you compute concrete preimage fibres and inspect what they would license in examples.

In this companion, a semantic fibre is usually the vector returned by fiber(f, domain, y): the finite set of witnesses x in domain such that f(x) == y. A value is being used avec fibre when that declared map/domain/output triple accompanies it. A value is sans fibre when it is only known as a target-side value; no source-side origin constraint follows from the value alone.

using EchoTypes

collapse = isodd
avec = fiber(collapse, -2:2, true)       # declared map + domain
Set(w.x for w in avec) == Set([-1, 1])   # possible origins

target_only = true                       # just a Bool: sans fibre

Finite examples can demonstrate nontrivial constraints on possible origins and can falsify over-specific claims by counterexample. They do not establish proof obligations; those belong upstream in Agda.

Source of truth

The Agda. This release mirrors hyperpolymath/echo-types at origin/main commit eed42503a1a4c54ec0a347ebef3440b4d4db30c9 (2026-05-28 head, after the Tier-3 audience-facing spine landed — EchoProvenance, EchoSecurity, EchoProbabilisticSupport, EchoDifferential, EchoLLEncoding, plus the EchoCanonicalIdentitySuite re-export bundle):

Julia surface	Mirrors Agda module / lemmas
EchoWitness, echo_intro, fiber, map_over*, comp_iso_*, cancel_iso_*	Echo.agda (kernel — also re-pinned via EchoKernel.agda upstream)
EchoR, echo_to_residue, residue_strictly_loses	EchoResidue.agda (echo-to-residue, strict-weakening-collapse)
fiber_size, flog2, landauer_bound, fiber_erasure_bound, bennett_reversible, landauer_collapse	EchoFiberCount.agda EchoThermodynamics.agda
v0.2.0 encode, decode, *_roundtrip, f_factors_via_projection	EchoTotalCompletion.agda (A↔ΣEcho, the slogan-unlock)
v0.2.0 echo_factorisation, fibre_of_proj1_*, projection_fibre_roundtrips, ofs_witness	EchoOrthogonalFactorizationSystem.agda (factorisation existence projection-fibre identification — funext-qualified clauses NOT mirrored)
v0.2.0 image, image_factor_*, is_surjective, is_injective, injective_fibres_proj_unique	EchoImageFactorization.agda
v0.2.0 no_section_of_collapsing_map, no_section_when_non_injective_at	EchoNoSectionGeneric.agda
v0.2.0 HasInverse, equiv_fibre_center, equiv_implies_injective, equiv_fibre_proj_unique, const_fun, const_fibre_section	EchoLossTaxonomy.agda (4-case classifier — EQUIV/INJ/SURJ/CONST K-free skeletons)
v0.2.0 collapse_as_fin, entropy_shadow, shannon_shadow, entropy_shadow_blind	EchoEntropy.agda (discrete Shannon shadow)
v0.2.0 LEcho, EchoMode, equal_at_mode, mode_equality_strictly_finer_at_linear	EchoObservationalEquivalence.agda (mode-indexed equality)
v0.3.0 Provenance, ProvRecord, provenance_collapses_at, prov_echo_tag1/2, echoes_distinguish_tag, prov_residue_collapses_tags, bool_over_nat_provenance	EchoProvenance.agda (Tier-3 audience move 1 — 4 parametric theorems + Bool-over-ℕ instance)
v0.3.0 Security, exit_collapses_at, audit_no_recovery_at, region_exit_audit_instance	EchoSecurity.agda (Tier-3 audience move 2 — per-region audit no-recovery via the generic no-section gadget)
v0.3.0 Sampling, Sample, support_collapses_at, samp_echo_idx1/2, echo_carries_which_index, samp_residue_loses_index, bool_indexed_nat_sampling	EchoProbabilisticSupport.agda (Tier-3 audience move 3 — marginal loses sampling index)
v0.3.0 Sensitivity, Perturbed, blur_collapses_perturbations_at, diff_echo_pert1/2, echo_carries_perturbation, diff_residue_loses_perturbation, bool_perturbed_nat_sensitivity	EchoDifferential.agda (Tier-3 audience move 4 — blur loses perturbation tag)
v0.3.0 LLShallowEncoding, trivial_encoding, trivial_encoding_has_section, ll_encoding_gap, source_no_section_holds, gap_paired	EchoLLEncoding.agda (cementing-negative — the LL !A := 1 shadow admits an encoded section paired with source-side no-section)

What is intentionally NOT mirrored

• Funext-qualified surfaces. The F5 earn-back gate gave the full OFS (uniqueness up to iso + diagonal lifting) upstream under funext, and EchoPullbackUnivF4 gives the strict pullback universal property the same way. Julia has no funext to take as hypothesis; the conditional claims would be vacuous. Only the unconditional fragment of ofs-witness is mirrored.

• Retracted surface (R-2026-05-18). Graded-comonad framing, two-models, universal-property, conservativity. The mechanised laws survive upstream (and so does the model-independence theorem), but the framing is retracted; the companion does not reproduce any of it.

• Higher type-theoretic structure. UIP-strength claims (full Σ-pair equality under injectivity, A ↔ Echo(const y0), contractible fibres), propositional truncation (the (epi, mono) collapse of the image factorisation), and HoTT identification types beyond decidable equality. The proof-relevant upper of each pair is what’s mirrored, in line with the --safe --without-K discipline upstream.

• Ordinal-lane work (Ordinal/Buchholz/*). The Slice-3 + Slice-4 rank-mono umbrella, RankPow*, head-Ω inversion, joint-bplus scaffolds — all live in echo-types’s ordinal pillar, separate from the echo functor / residue / thermodynamics core this companion mirrors. Adding ordinal shadows would require a new Bord carrier in Julia and a redesigned scope agreement. Not in v0.3.0; out-of-scope for the companion’s stated discipline.

Honest-bound discipline (Tier 3)

The four v0.3.0 audience-facing modules ship explicit “what is NOT proved” lists upstream — EchoSecurity is type-level no-section, NOT bytes-zeroed / side-channel-safe / tamper-evident; EchoProbabilisticSupport is support tracking, NOT measure theory / coupling / extraction; EchoDifferential is perturbation tracking, NOT ε-DP / Lipschitz / noise calibration. The Julia testsets preserve this scope in their comments. Consumers should not promote a green test to a real-world security or privacy claim — those need additional structure beyond the finite shadow.

Scope limits are inherited honestly: the thermodynamics is a finite-domain bound shape in arbitrary natural units — not quantitative physics, and not defined over infinite state spaces (the upstream Fin n restriction).

Downstream bridges (Valence Shell / Ochránce)

No current action. Valence Shell and Ochránce may later become downstream examples of Echo Types applied to shell state transitions and filesystem receipts — but this package does not claim to prove anything about those systems, and no integration is present here.

If such a bridge is ever added it will be a toy finite model of residue classification only: a fixed finite set of pre-states mapped to post-states, with fibres / residues computed to classify recoverable vs. collapsed information — and no filesystem, POSIX, secure-deletion, GDPR, cryptographic-attestation, filesystem-integrity, or production-security claim attached. Source of truth remains the Agda; real-world receipt and security guarantees belong to Valence Shell and Ochránce, not EchoTypes.jl.

Use

julia> using EchoTypes

julia> f = x -> x % 3;                 # a lossy map

julia> fiber(f, 0:8, 1)                # the constructive Echo fibre over 1
3-element Vector{EchoWitness{Int64}}:  #  x = 1, 4, 7

julia> fiber_erasure_bound(_ -> 0, 0:15, 0, 7)   # full-collapse Landauer bound
28                                                #  = k·T·⌊log₂ 16⌋ = 1·7·4

Test

julia --project=. -e 'using Pkg; Pkg.test()'

The testsets are finite shadows of named Agda lemmas, plus the small semantic-fibre vocabulary exercise over the kernel. The suite must stay green and is the only correctness claim this package makes about itself.

Status

v0.3.0, local development. The v0.1.0 surface (Echo, EchoResidue, EchoFiberCount, EchoThermodynamics) and the v0.2.0 Tier-1+Tier-2 canonical-identity spine are preserved unchanged; v0.3.0 adds executable shadows of the Tier-3 audience-facing spine that landed upstream on 2026-05-27/28 (EchoProvenance, EchoSecurity, EchoProbabilisticSupport, EchoDifferential) plus the cementing-negative EchoLLEncoding (LL shallow-encoding gap with paired source-side no-section). Test suite: 258 passing assertions across 19 testsets, organised as finite shadows of named Agda lemmas plus the semantic-fibre vocabulary exercise over the kernel. Registered as EchoTypes in the hyperpolymath professional registry; not registered in the Julia General registry and intentionally not part of the AcceleratorGate→KnotTheory→Skein→KRLAdapter chain — it is a standalone companion.

Licence

MPL-2.0; MPL-2.0 (see LICENSE) is the automatic legal fallback until PMPL is formally recognised. The LICENSE file, this statement, and every source SPDX header agree — one consistent licence, deliberately not a Project-vs-source split.