echo-kernel-note.adoc

echo-types: kernel vs derived (one-page note)

Which Agda modules are the kernel (the dependency-light, funext-free core everything imports) and which are derived. Companion to proofs/agda/EchoKernel.agda. Status SoT is docs/echo-types/MAP.adoc; honesty SoT is docs/retractions.adoc (R-2026-05-18). This note links, it does not duplicate.

The kernel is exactly Echo

Echo f y := Σ (x : A), (f x ≡ y). The audit of Echo.agda plus the Echo*.agda modules (intra-repo open import DAG, origin/main, 2026-05-18) shows a single root: every kernel-derived Echo* module transitively imports Echo, and Echo imports nothing from the repo — only agda-stdlib:

• Level, Function.Base, Function.Bundles, Data.Product.Base, Relation.Binary.PropositionalEquality (+ .Properties).

So no smaller subset is "the core": Echo.agda is already minimal and has no internal fat to trim (the heaviest content, the cancel-iso path algebra, is still first-order — see below). proofs/agda/EchoKernel.agda re-exports it (open import Echo public) and pins the load-bearing lemma types in a Kernel-contract submodule so the public surface cannot silently weaken.

Funext-free certificate

The kernel cone (Echo + the stdlib modules above) contains no Axiom.Extensionality / funext anywhere, zero postulates, and zero escape pragmas; it builds under --safe --without-K. That successful build is the certificate: every lemma re-exported by EchoKernel is funext-free by construction, mechanically, not by assertion. The kernel keeps the cancel-iso round-trips funext-free deliberately by taking the two triangle coherences (triangle₁, triangle₂) as explicit hypotheses; deriving them instead would need funext.

Caution

Funext-free is not "no funext anywhere in the project". Per R-2026-05-18, the genuine funext-relativity is the pointwise-only mediator property in EchoPullback (echo-pullback-univ proves only ∀ v → m' v ≡ m v, not m' ≡ m). That module is derived, not kernel — the boundary is real and lives outside this core.

Classification

Layer	Modules	Notes
Kernel	Echo (via EchoKernel)	Funext-free, postulate-free root. Re-export + contract: EchoKernel.agda. [REAL]
Derived — Tier 1 (only Echo + stdlib)	EchoCharacteristic, EchoChoreo, EchoDecidable, EchoFiberBridge, EchoFiberCount, EchoFiberTriangulation, EchoIndexed, EchoRelational, EchoTruncation, EchoJanusBridge, EchoTropical, EchoSeparating, EchoTotalCompletion, EchoDisplayed	One hop off the kernel. EchoJanusBridge/EchoTropical are Directions (see MAP). EchoFiberTriangulation is the external stdlib triangulation hardening item. EchoSeparating carries retracted prose framing (below). EchoTotalCompletion is the A ↔ Σ Echo encode/decode pair anchoring the F5 canonical- identity cohort (Tier 2 below). EchoDisplayed is the displayed-type / DispHom / fromHomOver fibration packaging of the categorical base (faithful mirror of typed-wasm’s Idris Echo.idr; no variance / graded-comonad claim, per R-2026-05-18).
Derived — Tier 2 (depend on Tier-1 Echo*)	EchoCategorical, EchoResidue, EchoEpistemic, EchoEpistemicResidue, EchoExamples, EchoGraded, EchoLinear, EchoPullback, EchoRelModel, EchoScope, EchoStabilityTests, EchoThermodynamics, EchoCNOBridge, EchoEphapaxBridge, EchoThermodynamicsFinite, EchoIntegration, EchoAccess, EchoCost, EchoCostInstance, EchoSearch, EchoSearchInstance, EchoExampleAbsInt, EchoExampleParser, EchoExampleProvenance, EchoExampleSignAnalysis, EchoExampleTruncation, EchoSearchExample, EchoThermodynamicsArbitrary, EchoThermoCollapseImpossible, EchoAbstractionBarrier, EchoOrthogonalFactorizationSystem, EchoImageFactorization, EchoImageFactorizationProp, EchoNoSectionGeneric, EchoLossTaxonomy, EchoResidueTaxonomy, EchoDecorationStructure, EchoObservationalEquivalence, EchoOFSUnivF5, EchoOFSUnivF5Diag, EchoOFSUnivF5Iso, EchoCanonicalIdentitySuite, EchoDifferential, EchoEntropy, EchoLLEncoding, EchoProbabilisticSupport, EchoProvenance, EchoSecurity	Multi-hop. EchoThermodynamics reaches the kernel via EchoFiberCount (no direct Echo import); EchoThermodynamicsFinite is its Bishop-finite transport layer. EchoSearch / EchoCost / EchoAccess are Axis 8 witness-search and cost-model extensions. EchoAbstractionBarrier is the Lane 1 / Lane 2 consumer-side free-theorem artefact (Track B — affine-consumer-cannot-distinguish plus raw-Σ counter-program sigma-distinguishes); imports Echo + EchoCharacteristic EchoLinear, landed 2026-05-26 via PR #119. EchoExample* are derived domain applications. F5 canonical-identity / OFS cohort (added via Slice-2b+ doc sweep): EchoOrthogonalFactorizationSystem is the (encode-mono / decode-epi) factorisation keystone; EchoImageFactorization carries the image side; EchoOFSUnivF5/Diag/Iso are the F5 universal-property work routing composition through totality; EchoImageFactorizationProp is the (epi, mono) earn-back module-parameterised in a TruncInterface (closes the truncation gate flagged by EchoImageFactorization); EchoCanonicalIdentitySuite re-exports the cohort as a single entry point; EchoNoSectionGeneric / EchoLossTaxonomy / EchoResidueTaxonomy / EchoDecorationStructure / EchoObservationalEquivalence are the no-section / loss / residue / decoration / observational classifications. Application/extension modules (also added via the same sweep): EchoEntropy, EchoLLEncoding, EchoProvenance, EchoSecurity, EchoProbabilisticSupport, EchoDifferential, EchoDeniability, EchoAggregation are derived domain applications mapped under their own headings in MAP.adoc. EchoDeniability formalises residue deniability: the perfect (constant / no-section) case and the partial (injective / has-section) case, with IsConstantOpener as the exact cut-point. EchoAggregation formalises micro→macro economic aggregation: the rollup aggregate is an Echo map and non-disaggregability is no-section-of-collapsing-map (the mechanised keystone of the oikos/betlang alib note). Imports Echo + EchoNoSectionGeneric.
Earn-back gate modules (derived / scoped; not kernel)	EchoGradedComonadF1, EchoPullbackUnivF4, EchoStepNDModelF2, EchoGradedComonadInterface, EchoGradedComonadInstance1, EchoGradedComonadInstance2	Falsifiable earn-back work tracked by docs/echo-types/earn-back-plan.adoc and docs/retractions.adoc. F4 and F2 are passed at their scoped strength; F1 is a feasibility spike / open gate as recorded in the ledger. F3 (Interface Instances) is the abstract comonad record. None are kernel.
Retracted framing (typecheck; prose withdrawn)	EchoGradedComonad, EchoPullback, EchoRelModel, EchoSeparating	Agda unchanged and [REAL] as mechanised; the graded-comonad / two-models / universal-property descriptions are [RETRACTED] (R-2026-05-18), under a falsifiable earn-back gate. Not kernel.
Sibling (not kernel-derived)	EchoApprox, EchoApproxInstance	Does not import Echo; a parallel stdlib-only approximation module. Listed so the DAG audit is complete.
Exploratory (not in All.agda)	EchoDecorationBridge, EchoImageFactorizationPropPostulated, EchoImageFactorizationPropCubical	Deliberately omitted from proofs/agda/All.agda so the verified suite is unaffected. EchoDecorationBridge re-issues EchoIntegration’s integration claim through a `DecorationFit record; exploratory per roadmap.adoc § R5 and docs/echo-types/explorations/decoration-bridge/README.adoc. EchoImageFactorizationPropPostulated is the postulated- truncation-interface consumer for EchoImageFactorizationProp (flag profile --without-K only, no --safe, because postulate is forbidden under --safe) — demonstrates the parametric TruncInterface slot is plug-in-usable; the postulates assert the standard (-1)-truncation laws without proving them. EchoImageFactorizationPropCubical is the REAL (--cubical --safe, zero-postulate) counterpart: it CONSTRUCTS ∥_∥ as a higher inductive type, realises the same four TruncInterface obligations as theorems (is-prop-∥∥ from squash; rec-∥∥ via the path recursor), and re-proves the (epi, mono) factorisation — discharging the truncation axiom the postulated module only assumes. It is a --cubical flag island because Agda forbids a --cubical module importing the --safe --without-K Echo cone, so it restates the minimal interface Echo locally. All three modules listed here to satisfy the classification-drift lint (scripts/kernel-guard.sh Check B); none is kernel, none load-bearing, all subject to abandonment.
Foundation contract surface (dotted Echo.* namespace; curated public interface)	Echo.Index.ThinPoset, Echo.Modality.Interface, Echo.Modality.Core, Echo.Separation.NotResourceInstance, Echo.Measure.Interface, Echo.Measure.Examples	The stable exported foundation for downstream languages (FOUNDATION_CONTRACT.md). Thin re-export / packaging over the proven flat modules: ThinPoset / grade-thinPoset (echo index), EchoModality / grade-echoModality with degrade / degrade-id / degrade-compose + no-section (modality), echo-degrade-not-generic-sigma equal-measure-does-not-imply-equal-echo (anti-collapse), and the ResidueMeasure / OrderedCarrier seam with cost / tropical / confidence examples. Echo.Measure. may depend on the order interface; Echo.Modality. and Echo.Index. are measure-independent (no semiring import) — the boundary invariant *Echo IS-NOT a resource instance. These files live under proofs/agda/Echo/ (dotted submodules), so they are outside the flat Echo*.agda glob that Check B lints; recorded here for discoverability. Not kernel (the kernel remains exactly Echo).

EchoOrdinal is Tier-1 off Echo but additionally pulls the Ordinal/ subtree; it belongs to the Buchholz/Veblen Direction in the MAP, not the foundation kernel.

Maintenance

Living classification. If a module’s import set changes, or a retraction/earn-back moves a module between layers, update this table and the [REAL]/[RETRACTED] tag in docs/echo-types/MAP.adoc in the same PR. Never duplicate proof detail here — link the module or the canonical doc.