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

[hyperpolymath]

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

Problem

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

```idris
gdprDeletionCompliant :
(proof : GDPRDeletionProof) ->
(recovery : Filesystem -> Filesystem) ->
recovery = id
```

`recovery` is an arbitrary parameter; the conclusion `recovery = id` cannot be proven for any `recovery` — there exist non-identity functions of type `Filesystem -> Filesystem` (e.g., `const empty`, `addEntry Root Dir`, etc.) and the GDPR proof provides no premise that excludes them.

Honest closure path

Mirror the Coq formalisation in `proofs/coq/rmo_operations.v::obliterate_leaves_no_trace` (lines 576–588): GDPR compliance is the property "no trace remains after obliteration" (path doesn't exist + no blocks mapped + audit logged). Suggested restatement (sketch):

```idris
||| GDPR Article 17 compliance: after deletion the path no longer
||| exists in the filesystem and the obliteration is audit-logged.
||| This is the correct "compliance" statement — properties of the
||| post-deletion state, not impossibility-of-recovery quantification.
gdprDeletionCompliant :
(proof : GDPRDeletionProof) ->
(postFs : Filesystem) ->
-- After GDPR delete, path no longer exists
pathExists proof.path postFs = False
-- Plus: completionTime >= requestTime (timing constraint)
-- Plus: auditLog is non-empty (accountability)
```

The non-injectivity / irrecoverability claim belongs in the lower-layer `secureDeleteIrreversible` (see #60 redesign), not in the GDPR-compliance theorem. GDPR Article 17 doesn't require mathematical irrecoverability — it requires logical removal + audit. The two should be separated.

Why I am not submitting a PR for this hole alone

Per project policy in `QUICKSTART-DEV.adoc:108`: no new `believe_me` / `assert_total` / `Admitted` / `sorry` / `unsafeCoerce`. Closing the hole by writing the non-theorem proof would require `believe_me`. Re-stating the public API of an `export`ed theorem is a larger scope change than the user-requested closure.

Echo-types audit (per `feedback_proofs_must_check_and_cross_doc_echo_types`)

`hyperpolymath/echo-types` does not currently expose a "GDPR compliance" abstraction. The closest is `proofs/agda/EchoLossTaxonomy.agda` CONST case (informational shape of obliteration) which is appropriate for #60 but not for #170 — GDPR compliance is a state-property predicate, not an L3 (echo) obligation. RECORD AS NOT RELEVANT for echo-types reuse at this hole. Cross-document anchor: see #51 (L3 grounding) and #60 (sibling Idris2 hole).

Out-of-band note

Same Model.idr / Idris2-CI gating debt as #60 — Model.idr does not currently type-check under Idris2 0.8.0; there is no `build-idris2` Justfile target or CI workflow.

Closure preconditions

1. Owner decision on whether `gdprDeletionCompliant` API can be restated as a state-property predicate (breaking change to exported theorem).
2. Decide whether GDPR compliance proof should compose with [Idris2] close RMO.idr:92 secureDeleteIrreversibleProof — type signature is non-theorem (Tier-S blocker) #60's restated `secureDeleteNotInjective` ("compliance = removal-from-tree ∧ obliteration-witness") or stand alone.
3. Same Model.idr + Idris2-CI gating as [Idris2] close RMO.idr:92 secureDeleteIrreversibleProof — type signature is non-theorem (Tier-S blocker) #60.

Refs #41 (Phase 1 keystone), #60 (sibling hole)