[Idris2] close RMO.idr:92 secureDeleteIrreversibleProof — type signature is non-theorem (Tier-S blocker)

[hyperpolymath]

Parent: #41 (Phase 1 keystone). Sub-issue surfaced during 2026-06-01 closure attempt.

Problem

The hole at `proofs/idris2/src/Filesystem/RMO.idr:92` (`?secureDeleteIrreversibleProof`) cannot be closed because the surrounding type signature is not a theorem.

```idris
secureDeleteIrreversible :
(p : Path) ->
(fs : Filesystem) ->
(prf : ObliterationProof p) ->
(recovery : Filesystem -> Filesystem) ->
recovery fs = fs -> -- premise
Void -- conclusion
```

The premise `recovery fs = fs` is satisfied by `recovery = id` for every `fs`. Given that premise we cannot derive `Void` — there is no contradiction. The statement asserts that no recovery function fixes `fs`, which is straightforwardly false (`id` always fixes `fs`).

Honest closure path

Mirror the Coq formalisation in `proofs/coq/rmo_operations.v::obliterate_not_injective` (lines 504–531): irreversibility is information-theoretic non-injectivity, not the impossibility of "recovery functions that fix the state." Suggested restatement (sketch):

```idris
||| Secure deletion is not injective: two distinct pre-deletion states
||| produce the same post-deletion state. This is the correct shape
||| of "information destruction" — many distinct inputs collapse to
||| one output, so no inverse function can exist.
secureDeleteNotInjective :
(p : Path) ->
(fs1, fs2 : Filesystem) ->
(prf1 : ObliterationProof p) ->
(prf2 : ObliterationProof p) ->
-- Pre-deletion: fs1 and fs2 disagree only on content at p
(agreeOff : (q : Path) -> Not (q = p) -> getEntry q fs1 = getEntry q fs2) ->
-- Pre-deletion contents differ
(differAtP : getEntry p fs1 /= getEntry p fs2) ->
-- Post-deletion states are equal (information lost)
removeEntry p fs1 = removeEntry p fs2
```

This restatement IS provable by case analysis on the entry lookup + filter semantics; matches the Coq `obliterate_not_injective` shape (currently `Admitted` in Coq pending #57 — see also Coq admit cluster #56/#57/#58 — but the Idris2 restatement only needs filesystem-level equality, no block-overwrite model, so it can land cleanly while Coq closure waits).

Why I am not submitting a PR for this hole alone

Per project policy in `QUICKSTART-DEV.adoc:108`: "No `believe_me` or `assert_total` (Idris2); no new `Admitted.` (Coq); no `sorry` (Lean); no `unsafeCoerce` (Haskell)". Closing the hole by writing the non-theorem proof would require `believe_me`, which is forbidden. Re-stating the public API of an `export`ed theorem with a different type signature is a larger scope change than the user-requested closure and warrants a separate design decision.

Echo-types audit (per `feedback_proofs_must_check_and_cross_doc_echo_types`)

`hyperpolymath/echo-types` ships `proofs/agda/EchoLossTaxonomy.agda` with a CONST case that is exactly the echo-shape of obliteration (information-destroying, all-fibres-equivalent-to-domain). The taxonomy is Agda, not directly importable into Idris2, but the shape is the right L3 reuse. Cross-document: see #51 (L3 grounding in echo-types LAYER3).

Out-of-band note

There is a separate pre-existing block: `proofs/idris2/src/Filesystem/Model.idr` does not currently type-check under Idris2 0.8.0 (`isJust` undefined; missing `Eq Path` / `Eq (Path, FSEntry)` instances at lines 103/108/135/152/169). The valence-shell `Justfile` has no `build-idris2` target and CI does not exercise the Idris2 proofs. Closing this hole productively is gated on that adjacent debt.

Closure preconditions

1. Owner decision on whether `secureDeleteIrreversible` API can be restated to `secureDeleteNotInjective` form (breaking change to exported theorem).
2. Fix Model.idr type-check failures (separate sub-issue would help).
3. Wire `build-idris2` / `verify-idris2` recipe in `Justfile` + CI workflow so future drift is caught.

Refs #41 (Phase 1 keystone)