fix(proofs/idris2): rename AuditEntry.proof to avoid Idris2 0.8.0 keyword clash (#112)

Root cause: `proof` is a reserved token in Idris2 0.8.0 (used as part of the
tactic / proof-search vocabulary), so it cannot appear as a record field name.
When the parser encounters `proof :` inside a record block it bails with a
confusingly-positioned "Expected end of input" pointing at the *preceding*
docstring (line 230 in the original file), making it look like the docstring
was the offender. It isn't — the same record had three earlier `|||` docstrings
that parsed fine.

Repro (minimal):

    record TestEntry where
      constructor MkTestEntry
      path  : String
      proof : String   -- parser fails here

Removing the docstring does NOT fix it; renaming the field DOES. The
dependency `ObliterationProof path` is also fine — the issue is purely the
field-name token.

Fix: rename the field from `proof` to `obliterated`. The new name matches the
precedent already established by `GDPRDeletionProof.obliterated` (line 144 of
the same file), which holds the same `ObliterationProof path` payload, so
this is the smallest possible change and is internally consistent.

No call sites reference `AuditEntry.proof` (only the record and constructor
names are used elsewhere), so no other files need updating.

Local verification: with this rename plus an unrelated temporary stub for
`hardwareEraseIrreversible` (other-agent's PR territory; not committed here),
the build progresses past `AuditEntry` and now fails on `overwriteIrreversible`
(`>=` Bool/Type mismatch at line 120) and `auditTrailCompleteness` (undefined
`Elem` at line 251) — pre-existing, unrelated, separate fixes.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

proofs/idris2/src/Filesystem/RMO.idr

@@ -235,7 +235,7 @@ record AuditEntry where
   ||| Deletion level
   level : SecureDeleteLevel
   ||| Proof that deletion succeeded
-  proof : ObliterationProof path
+  obliterated : ObliterationProof path
 
 ||| Audit log is append-only (cannot be modified)
 |||