Skip to content

Commit 37c3206

Browse files
committed
docs: classify new Echo* modules to satisfy kernel-guard CI
1 parent 99c589b commit 37c3206

2 files changed

Lines changed: 24 additions & 6 deletions

File tree

docs/echo-types/MAP.adoc

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -175,8 +175,11 @@ The honesty layer. *Read before citing any claim above as final.*
175175
F2/F4 independent; F3 gated on F1). Current SoT for what is / isn't
176176
proven. Current gate modules on `main` include
177177
`proofs/agda/EchoGradedComonadF1.agda`,
178-
`proofs/agda/EchoPullbackUnivF4.agda`, and
179-
`proofs/agda/EchoStepNDModelF2.agda`, each scoped by the ledger.
178+
`proofs/agda/EchoPullbackUnivF4.agda`,
179+
`proofs/agda/EchoStepNDModelF2.agda`,
180+
`proofs/agda/EchoGradedComonadInterface.agda`,
181+
`proofs/agda/EchoGradedComonadInstance1.agda`,
182+
and `proofs/agda/EchoGradedComonadInstance2.agda`, each scoped by the ledger.
180183
* Gate handoffs: `docs/gate-1-distinct-phenomenon.adoc`,
181184
`docs/gate-2-handoff.adoc`, `docs/gate-3-*.adoc`.
182185

@@ -222,3 +225,8 @@ passes/fails, or a claim is retracted/earned-back:
222225
. Never duplicate detail — link to the canonical proof module / doc.
223226
. The GitHub wiki `Home` mirrors this file and must point back here as
224227
SoT; do not fork content into the wiki.
228+
e entry *and* its status tag
229+
here, in the same PR as the change.
230+
. Never duplicate detail — link to the canonical proof module / doc.
231+
. The GitHub wiki `Home` mirrors this file and must point back here as
232+
SoT; do not fork content into the wiki.

docs/echo-types/echo-kernel-note.adoc

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -76,19 +76,29 @@ kernel** — the boundary is real and lives outside this core.
7676
`EchoEpistemicResidue`, `EchoExamples`, `EchoGraded`,
7777
`EchoLinear`, `EchoPullback`, `EchoRelModel`, `EchoScope`,
7878
`EchoStabilityTests`, `EchoThermodynamics`, `EchoCNOBridge`,
79-
`EchoThermodynamicsFinite`, `EchoIntegration`
79+
`EchoThermodynamicsFinite`, `EchoIntegration`, `EchoAccess`,
80+
`EchoCost`, `EchoCostInstance`, `EchoSearch`, `EchoSearchInstance`,
81+
`EchoExampleAbsInt`, `EchoExampleParser`, `EchoExampleProvenance`,
82+
`EchoExampleSignAnalysis`, `EchoExampleTruncation`,
83+
`EchoSearchExample`, `EchoThermodynamicsArbitrary`,
84+
`EchoThermoCollapseImpossible`
8085
| Multi-hop. `EchoThermodynamics` reaches the kernel via
8186
`EchoFiberCount` (no direct `Echo` import);
8287
`EchoThermodynamicsFinite` is its Bishop-finite transport layer.
88+
`EchoSearch` / `EchoCost` / `EchoAccess` are Axis 8 witness-search
89+
and cost-model extensions. `EchoExample*` are derived domain
90+
applications.
8391

8492
| *Earn-back gate modules* +
8593
(derived / scoped; not kernel)
8694
| `EchoGradedComonadF1`, `EchoPullbackUnivF4`,
87-
`EchoStepNDModelF2`
95+
`EchoStepNDModelF2`, `EchoGradedComonadInterface`,
96+
`EchoGradedComonadInstance1`, `EchoGradedComonadInstance2`
8897
| Falsifiable earn-back work tracked by
8998
`docs/echo-types/earn-back-plan.adoc` and `docs/retractions.adoc`.
9099
F4 and F2 are passed at their scoped strength; F1 is a feasibility
91-
spike / open gate as recorded in the ledger. None are kernel.
100+
spike / open gate as recorded in the ledger. F3 (Interface +
101+
Instances) is the abstract comonad record. None are kernel.
92102

93103
| *Retracted framing* +
94104
(typecheck; prose withdrawn)
@@ -99,7 +109,7 @@ kernel** — the boundary is real and lives outside this core.
99109
(R-2026-05-18), under a falsifiable earn-back gate. Not kernel.
100110

101111
| *Sibling (not kernel-derived)*
102-
| `EchoApprox`
112+
| `EchoApprox`, `EchoApproxInstance`
103113
| Does **not** `import Echo`; a parallel stdlib-only approximation
104114
module. Listed so the DAG audit is complete.
105115
|===

0 commit comments

Comments
 (0)