Skip to content

Commit fadef64

Browse files
Revert "echo(image-factorization-prop): postulated-truncation consume… (#154)
…r + Expl…" This reverts commit 48debd0.
1 parent 48debd0 commit fadef64

2 files changed

Lines changed: 7 additions & 181 deletions

File tree

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

Lines changed: 7 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -148,22 +148,15 @@ kernel** — the boundary is real and lives outside this core.
148148
module. Listed so the DAG audit is complete.
149149

150150
| *Exploratory (not in `All.agda`)*
151-
| `EchoDecorationBridge`, `EchoImageFactorizationPropPostulated`
151+
| `EchoDecorationBridge`
152152
| Deliberately omitted from `proofs/agda/All.agda` so the verified
153-
suite is unaffected. `EchoDecorationBridge` re-issues
154-
`EchoIntegration`'s integration claim through a `DecorationFit`
155-
record; exploratory per `roadmap.adoc` § R5 and
153+
suite is unaffected. Re-issues `EchoIntegration`'s integration
154+
claim through a `DecorationFit` record. Listed here only to
155+
satisfy the classification-drift lint
156+
(`scripts/kernel-guard.sh` Check B); the module itself is
157+
exploratory per `roadmap.adoc` § R5 and
156158
`docs/echo-types/explorations/decoration-bridge/README.adoc`.
157-
`EchoImageFactorizationPropPostulated` is the postulated-
158-
truncation-interface consumer for `EchoImageFactorizationProp`
159-
(flag profile `--without-K` only, no `--safe`, because
160-
`postulate` is forbidden under `--safe`) — demonstrates the
161-
parametric `TruncInterface` slot is plug-in-usable; the
162-
postulates assert the standard (-1)-truncation laws without
163-
proving them. Both modules listed here to satisfy the
164-
classification-drift lint (`scripts/kernel-guard.sh` Check B);
165-
neither is kernel, neither load-bearing, both subject to
166-
abandonment.
159+
Not kernel, not load-bearing, subject to abandonment.
167160
|===
168161

169162
`EchoOrdinal` is Tier-1 off `Echo` but additionally pulls the

proofs/agda/EchoImageFactorizationPropPostulated.agda

Lines changed: 0 additions & 167 deletions
This file was deleted.

0 commit comments

Comments
 (0)