This file backs every factual claim in README.adoc with code paths and honest caveats. Read it if you are doing due diligence — checking whether the story matches the code.
- Claim-to-implementation map
- Core fiber laws are constructive under --safe --without-K with no postulates
- A ≃ Σ B (Echo f) is the standard total-space-of-fibers equivalence
- The middle object is the total fiber space, not the image
- The factorization gives a WFS; OFS is not yet proved
- funext is an explicit module parameter for Tier-3 results
- Matched-negatives prove Echo is not its obvious neighbours
- No-section family proves structured loss is irreversible
- Audience surfaces ship with honest bounds
- Retraction ledger is living and complete
- Ordinal / Buchholz track is parallel-independent
- Dogfooded Across The Account
- Known gaps
- Evidence Index
Core fiber laws (echo-intro, map-over, map-over-id, map-over-comp, map-square) — constructive,
--safe --without-K, no postulates.
- How this is implemented
-
All five laws are proved in
proofs/agda/Echo.agda. The file header confirms--safe --without-K. Nopostulateappears in any file underproofs/agda/. The laws:echo-intro(everyx : Alives in its own fiber),map-over(morphisms act on fibers),map-over-id(identity),map-over-comp(composition),map-square(action along commuting squares). - Caveat
-
These are generic sigma/fiber lemmas that hold for the standard homotopy fiber in any extensional type theory. They are not characteristically Echo-shaped. The identity claim does not rest on them.
Left leg (encode f): EQUIVALENCE — the standard total-space-of-fibers fact (HoTT Book §4.8), restated in Echo vocabulary.
- How this is implemented
-
proofs/agda/EchoTotalCompletion.agdaprovesA ↔ ΣEcho. The proof is the standard contractibility-of-fibers argument: the dependent sum of all fibers offis equivalent to the domain.proofs/agda/EchoCanonicalIdentitySuite.agdare-exports it as the Tier-1 headline. - Caveat
-
This theorem is not novel. It appears in the HoTT Book (§4.8) and is implicit in the encode-decode method throughout homotopy type theory. The repo’s contribution is the emphasis — treating this equivalence as the foundation for a structured-loss account rather than a bookkeeping fact. Whether emphasis alone is a contribution is a judgment the reader must make.
This is the domain-replacement factorization: the middle object Σ B (Echo f) is equivalent to A. It is not the image factorization in the HoTT sense, which requires propositional truncation of fibers.
- How this is implemented
-
proofs/agda/EchoImageFactorization.agdadefines the middle object asΣ B (Echo f)and proves the factorization exists. The Tier-1 equivalence inproofs/agda/EchoTotalCompletion.agdaconfirms the middle object ≃A. The HoTT image would beΣ (b : B), ∥ fib f b ∥₀, which is a strictly smaller object whenfis not surjective. No code in the repo defines or uses the truncated image. - Caveat
-
The module name
EchoImageFactorizationis a misnomer. It suggests the image, but the object is the total fiber space (≃ domain). The README now uses "domain replacement" language. The module should be renamed toEchoFiberTotalFactorization. No proof depends on the misnomer — the name is purely a clarity debt.
Diagonal lifts exist (F5-2) and factorisation is unique up to iso (F5-3), giving a weak factorization system. Unique diagonal fills — the requirement for orthogonality — are not yet proved.
- How this is implemented
-
Three F5 modules:
-
proofs/agda/EchoOFSUnivF5.agda— F5-1: strict triangle (f ≡ proj₁ ∘ encode fat function level), funext-qualified -
proofs/agda/EchoOFSUnivF5Diag.agda— F5-2: diagonal lifting (existence of fill) -
proofs/agda/EchoOFSUnivF5Iso.agda— F5-3: factorisation uniqueness up to iso (iff = p ∘ e = p' ∘ e'through two (equivalence, projection) factorizations, the middle objects are isomorphic)
-
- Caveat
-
An OFS requires unique diagonal fills (contractible solution spaces). F5-3 proves factorisation uniqueness up to iso, which is weaker. For equivalences specifically, any two diagonal fills are homotopic (equivalences have essentially unique inverses), so the gap is likely dischargeable — but the proof has not been written. The module
EchoOrthogonalFactorizationSystemshould be renamed toEchoWeakFactorizationSystem, andofs-witnessshould becomewfs-witness, until unique fills land.
The unconditional fragment under --safe --without-K covers factorization existence and fiber identification only. The strict triangle, diagonal lifting, and factorisation uniqueness require funext supplied by the caller.
- How this is implemented
-
All F5 modules accept
funextas an explicit module parameter (visible in the module telescope, never a postulate). Without funext: factorization existence, fiber identification, and pointwise-definitional triangle all hold. With funext: strict function-level triangle (F5-1), diagonal lifting (F5-2), factorisation uniqueness up to iso (F5-3). - Caveat
-
The Julia companion has no funext and therefore shadows only the unconditional fragment. This is honestly scoped under R-2026-05-18. The funext dependency means the most interesting categorical properties have no executable counterpart.
Novel separation proofs: Echo is not distinguished by Shannon entropy; LL !A := 1 gives a shallow-encoding gap; equal measure does not imply equal Echo.
- How this is implemented
-
-
proofs/agda/EchoEntropy.agda— Shannon entropy cannot distinguish distinct echoes over the same output. -
proofs/agda/EchoLLEncoding.agda— The linear logic encodingLL !A := 1collapses informative distinctions that Echo preserves. -
proofs/agda/EchoSeparation/NotResourceInstance.agda—equal-measure-does-not-imply-equal-echoandmeasure-not-injective: no residue measure determines the echo.
-
- Caveat
-
These establish negative identity (Echo ≠ X). The falsifiability criteria also require positive identity (characteristic theorems that are naturally Echo-shaped). The positive side is open.
No section of a collapsing map.
- How this is implemented
-
proofs/agda/EchoNoSectionGeneric.agdaprovesno-section-of-collapsing-map. Additional witnesses inproofs/agda/EchoCharacteristic.agda:collapse-non-injective,no-section-collapse,no-section-visible,no-section-collapse-to-residue,no-section-weaken. Distinct-echo witnesses:echo-true≢echo-false,stateA≢stateB. Retained-constraint witness:visible-constraint. - Caveat
-
Genuine and mechanised, but standard consequences of non-injectivity in dependent type theory. Their value is as canonical examples (falsifiability criterion 3), not as novel theorems (criterion 2).
Provenance, security, probabilistic, and differential views, each with honest bounds.
- How this is implemented
-
-
proofs/agda/EchoProvenance.agda— database/lineage audience -
proofs/agda/EchoSecurity.agda— region-exit/capability-flow audience (generalisestutorial/region_exit_audit/) -
proofs/agda/EchoProbabilisticSupport.agda— sampling/draw-id audience -
proofs/agda/EchoDifferential.agda— sensitivity/perturbation-tracking audience
-
Each ships: a record type, parametric headline theorems, a worked instance, and matched-negatives (honest-bound disclosure).
- Caveat
-
These are applications of the fiber construction to domain-specific concerns, not theorems establishing Echo as a distinct mathematical object. They support criterion 3 (canonical examples) but not criterion 2 (characteristic theorem family).
A living retraction ledger recording every retracted claim, its counterexample, and its narrowing.
- How this is implemented
-
docs/retractions.adocrecords R-2026-05-18 and follow-ups F-2026-05-18a, F-2026-05-20a/b, F-2026-05-27a.docs/echo-types/earn-back-plan.adocrecords Pillar F gates F1–F5 (all PASSED). Each retraction includes: the original claim, the counterexample or obstruction, the narrowing, and the earn-back status. - Caveat
-
None currently known. This is better practice than is standard in published work.
Echo Core does NOT depend on the Ordinal / Buchholz track.
- How this is implemented
-
All ordinal modules live under
proofs/agda/Ordinal/. NoEcho*.agdafile imports fromOrdinal/. Dependency separation is structural (directory-level). - Caveat
-
The Ordinal track has open problems (unbudgeted
wf-<ᵇʳᶠclosure, shared-binder internalization). These do not affect Echo Core. Seedocs/buchholz-plan.adoc.
| Technology / Pattern | Used here | Also used in |
|---|---|---|
Echo fiber vocabulary |
Core definitions + audience surfaces + matched-negatives |
|
Retraction ledger |
|
maa-framework (absolute-zero) |
Agda |
All proofs under |
|
Caution
|
Module naming debt: |
|
Caution
|
Module naming debt: |
|
Caution
|
OFS upgrade is open. The (equivalence, projection) factorization is a WFS. Upgrading to OFS requires proving unique diagonal fills. For equivalences, any two fills are homotopic, so the gap is likely dischargeable — but the proof has not been written. This is the most important open technical task for the factorization story. |
|
Caution
|
Positive identity is open. Matched-negatives give negative identity (Echo ≠ entropy, ≠ LL encoding, ≠ resource grade). Falsifiability criterion 2 requires a characteristic theorem family — results that are naturally Echo-shaped, not generic fiber lemmas. The Tier-1 theorem is standard (HoTT Book §4.8). The best current case for positive identity is emphasis + vocabulary + audience surfaces, which is a viewpoint contribution, not a theorem contribution. Whether this suffices is the question the repo is designed to answer. |
|
Caution
|
Cross-repo bridge conformance is not machine-checked. |
|
Caution
|
Buchholz shared-binder internalization is open. The Ordinal track has well-foundedness for the current constructor core, but historical same-binder shapes are not internalized as constructors of the real order. Does not affect Echo Core. See |
| Path | Proves |
|---|---|
|
Core fiber laws |
|
|
|
Domain-replacement factorization exists (module name is misnomer) |
|
No section of a collapsing map |
|
WFS witness (module name overclaims OFS) |
|
F5-1: strict triangle (funext-qualified) |
|
F5-2: diagonal lifting (existence) |
|
F5-3: factorisation uniqueness up to iso |
|
Shannon entropy does not distinguish echoes |
|
LL |
|
Four-axis function-side classification |
|
ResidueForm record + four instances |
|
DecorationStructure recipe + degrade-compose |
|
Provenance audience surface |
|
Security/capability-flow audience surface |
|
Probabilistic-support audience surface |
|
Differential/sensitivity audience surface |
|
Curated re-export of all load-bearing results |
|
Retraction ledger with dates, reasons, narrowings |
|
Pillar F gate ledger (F1–F5 all PASSED) |