Context
hyperpolymath/EchoTypes.jl is the executable Julia companion to this repo — it runs the finite-domain shadow of theorems mechanised here on concrete data. The companion was at v0.1.0 (pinned to 2ca3122, late April baseline mirroring Echo, EchoResidue, EchoFiberCount, EchoThermodynamics) and was effectively invisible from this repo's documentation.
Today (2026-05-27) it landed at v0.2.0, re-pinned to e7dded6 (current main), with seven new executable shadows for the Tier-1+Tier-2 canonical-identity spine + the unconditional fragment of the F5 OFS earn-back. Source: hyperpolymath/EchoTypes.jl#4, tag v0.1.0 shipped + v0.2.0 follows once the PR merges. Registered in julia-professional-registry via julia-professional-registry#16.
This issue asks for the upstream docs to be updated so the existence + capabilities of the companion are discoverable from this repo.
What the v0.2.0 companion now mirrors
| Companion module |
Mirrors |
Echo*, MapOver, comp/cancel iso |
Echo.agda (also re-pinned via EchoKernel.agda) |
EchoR, echo_to_residue, residue_strictly_loses |
EchoResidue.agda |
Landauer / Bennett bound shapes, fiber_size, flog2 |
EchoFiberCount.agda + EchoThermodynamics.agda |
v0.2.0 encode/decode/round-trips + f_factors_via_projection |
EchoTotalCompletion.agda |
v0.2.0 echo_factorisation, fibre_of_proj1_*, projection_fibre_roundtrips, ofs_witness |
EchoOrthogonalFactorizationSystem.agda (unconditional fragment only) |
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_*, const_fun, const_fibre_section |
EchoLossTaxonomy.agda |
v0.2.0 collapse_as_fin, entropy_shadow, shannon_shadow, entropy_shadow_blind |
EchoEntropy.agda |
v0.2.0 LEcho, EchoMode, equal_at_mode, mode_equality_strictly_finer_at_linear |
EchoObservationalEquivalence.agda |
Honest scope held verbatim from upstream: R-2026-05-18 retraction surface (graded-comonad / two-models / UP / conservativity) does NOT appear; F5-funext-qualified clauses (uniqueness up to iso, diagonal lifting) are NOT mirrored — Julia has no funext, the claims would be vacuous; UIP- and truncation-strength upgrades are likewise honestly not mirrored.
Doc-update checklist
These edits all happen in this repo and only mention the companion's existence + scope; no Agda content changes.
Why this is a documentation-only update
The companion makes no proof claims and adds no theorems — it only runs the shadow on finite data, and falsifies-by-counterexample. The Agda remains the sole source of truth. The docs change exists so future contributors and reviewers can discover the companion without already knowing it's there.
Constraint
I (the EchoTypes.jl maintainer's Claude session) am explicitly not editing this repo directly per session-level instruction. This issue is the hand-off; the upstream maintainer-bot (or maintainer) can pick up the checklist.
🤖 Generated with Claude Code — companion-side updates landed in hyperpolymath/EchoTypes.jl#4 (auto-merge ON).
Context
hyperpolymath/EchoTypes.jlis the executable Julia companion to this repo — it runs the finite-domain shadow of theorems mechanised here on concrete data. The companion was at v0.1.0 (pinned to2ca3122, late April baseline mirroringEcho,EchoResidue,EchoFiberCount,EchoThermodynamics) and was effectively invisible from this repo's documentation.Today (2026-05-27) it landed at v0.2.0, re-pinned to
e7dded6(currentmain), with seven new executable shadows for the Tier-1+Tier-2 canonical-identity spine + the unconditional fragment of the F5 OFS earn-back. Source: hyperpolymath/EchoTypes.jl#4, tagv0.1.0shipped +v0.2.0follows once the PR merges. Registered injulia-professional-registryvia julia-professional-registry#16.This issue asks for the upstream docs to be updated so the existence + capabilities of the companion are discoverable from this repo.
What the v0.2.0 companion now mirrors
Echo*,MapOver, comp/cancel isoEcho.agda(also re-pinned viaEchoKernel.agda)EchoR,echo_to_residue,residue_strictly_losesEchoResidue.agdafiber_size,flog2EchoFiberCount.agda+EchoThermodynamics.agdaencode/decode/round-trips +f_factors_via_projectionEchoTotalCompletion.agdaecho_factorisation,fibre_of_proj1_*,projection_fibre_roundtrips,ofs_witnessEchoOrthogonalFactorizationSystem.agda(unconditional fragment only)image,image_factor_*,is_surjective,is_injective,injective_fibres_proj_uniqueEchoImageFactorization.agdano_section_of_collapsing_map,no_section_when_non_injective_atEchoNoSectionGeneric.agdaHasInverse,equiv_*,const_fun,const_fibre_sectionEchoLossTaxonomy.agdacollapse_as_fin,entropy_shadow,shannon_shadow,entropy_shadow_blindEchoEntropy.agdaLEcho,EchoMode,equal_at_mode,mode_equality_strictly_finer_at_linearEchoObservationalEquivalence.agdaHonest scope held verbatim from upstream: R-2026-05-18 retraction surface (graded-comonad / two-models / UP / conservativity) does NOT appear; F5-funext-qualified clauses (uniqueness up to iso, diagonal lifting) are NOT mirrored — Julia has no funext, the claims would be vacuous; UIP- and truncation-strength upgrades are likewise honestly not mirrored.
Doc-update checklist
These edits all happen in this repo and only mention the companion's existence + scope; no Agda content changes.
README.md— add a one-line "Executable companion" pointer near the top of the project description (e.g., under the synopsis), linking tohyperpolymath/EchoTypes.jl..claude/CLAUDE.md— under "Ecosystem context", add anEchoTypes.jlbullet matching the existing one-line style ofEphapax/VeriSimetc. (e.g., "executable Julia companion mirroring the finite-domain shadow of the Tier-1+Tier-2 spine; honestly scoped under R-2026-05-18.")docs/echo-types/cross-repo-bridge-status.md— add anEchoTypes.jlrow to whatever bridge-status table is canonical there.docs/echo-types/MAP.adoc— under "Canonical identity layer" (or a new "Executable companions" sub-section), point at the v0.2.0 surface table and note the F5 / R-2026-05-18 scoping inheritance.docs/echo-types/paper.adoc— if the Pillar E[EXPAND]Evaluation section ever wants a concrete "executable shadow exists" data point, this is one.Why this is a documentation-only update
The companion makes no proof claims and adds no theorems — it only runs the shadow on finite data, and falsifies-by-counterexample. The Agda remains the sole source of truth. The docs change exists so future contributors and reviewers can discover the companion without already knowing it's there.
Constraint
I (the EchoTypes.jl maintainer's Claude session) am explicitly not editing this repo directly per session-level instruction. This issue is the hand-off; the upstream maintainer-bot (or maintainer) can pick up the checklist.
🤖 Generated with Claude Code — companion-side updates landed in hyperpolymath/EchoTypes.jl#4 (auto-merge ON).