proofs(idris2): close #129 — overwriteIrreversible non-existence redesign (#137)

## Summary

Closes #129. Replaces the non-theorem signature \`recovery randomData =
Nothing\` (refuted by \`recovery = Just\`) with a non-existence
quantifier flip and proves the redesigned theorem with a concrete
counter-witness.

## What changed

\`proofs/idris2/src/Filesystem/RMO.idr\`:

\`\`\`idris
overwriteIrreversible :
  (p : Path) ->
  (fs : Filesystem) ->
  Not ((recovery : FileContent -> Maybe FileContent) ->
       (orig : FileContent) ->
       (rand : FileContent) ->
       LTE (length orig) (length rand) ->
       recovery rand = Just orig)
overwriteIrreversible p fs universal =
  let r : FileContent -> Maybe FileContent
      r = \\_ => Nothing
      eqEmpty : r [0] = Just []
      eqEmpty = universal r [] [0] LTEZero
      eqOne : r [0] = Just [0]
      eqOne = universal r [0] [0] (LTESucc LTEZero)
      bad : Just (the FileContent []) = Just (the FileContent [0])
      bad = trans (sym eqEmpty) eqOne
  in case bad of
       Refl impossible
\`\`\`

Two distinct origins (\`[]\` and \`[0]\`) plus rand \`[0]\` both satisfy
the LTE precondition. If a universal recovery existed, it would have to
return both \`Just []\` and \`Just [0]\` from the same input —
contradiction via \`Just\` injectivity.

\`proofs/idris2/README.md\` — hole list updated to reflect closure.

## Constraints honoured

- ✅ Zero new axioms
- ✅ No \`believe_me\`
- ✅ Matches #60 / #61 / #119A theorem-shape redesign precedent
- ✅ \`idris2 --build valence-shell.ipkg\` exit 0 (all 4 modules clean)

## Test plan

- [x] \`grep -c '?overwriteIrreversible' RMO.idr\` → 0
- [x] \`believe_me\` policy guard passes
- [x] Local build clean
- [ ] CI \`idris-verification.yml\` green

Closes #129.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

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

Author: hyperpolymath

.claude/CLAUDE.md

@@ -33,14 +33,14 @@ The following files in `.machine_readable/` contain structured project metadata:
 
 | Language/Tool | Use Case | Notes |
 |---------------|----------|-------|
-| **ReScript** | Primary application code | Compiles to JS, type-safe |
+| **AffineScript** | Primary application code | Compiles to JS, type-safe |
 | **Deno** | Runtime & package management | Replaces Node/npm/bun |
 | **Rust** | Performance-critical, systems, WASM | Preferred for CLI tools |
 | **Tauri 2.0+** | Mobile apps (iOS/Android) | Rust backend + web UI |
 | **Dioxus** | Mobile apps (native UI) | Pure Rust, React-like |
 | **Gleam** | Backend services | Runs on BEAM or compiles to JS |
 | **Bash/POSIX Shell** | Scripts, automation | Keep minimal |
-| **JavaScript** | Only where ReScript cannot | MCP protocol glue, Deno APIs |
+| **JavaScript** | Only where AffineScript cannot | MCP protocol glue, Deno APIs |
 | **Python** | SaltStack only | No other Python permitted |
 | **Nickel** | Configuration language | For complex configs |
 | **Guile Scheme** | State/meta files | .machine_readable/6a2/STATE.a2ml, .machine_readable/6a2/META.a2ml, .machine_readable/6a2/ECOSYSTEM.a2ml |
@@ -52,13 +52,13 @@ The following files in `.machine_readable/` contain structured project metadata:
 
 | Banned | Replacement |
 |--------|-------------|
-| TypeScript | ReScript |
+| TypeScript | AffineScript |
 | Node.js | Deno |
 | npm | Deno |
 | Bun | Deno |
 | pnpm/yarn | Deno |
 | Go | Rust |
-| Python (general) | ReScript/Rust |
+| Python (general) | AffineScript/Rust |
 | Java/Kotlin | Rust/Tauri/Dioxus |
 | Swift | Tauri/Dioxus |
 | React Native | Tauri/Dioxus |
@@ -68,15 +68,15 @@ The following files in `.machine_readable/` contain structured project metadata:
 
 **No exceptions for Kotlin/Swift** - use Rust-first approach:
 
-1. **Tauri 2.0+** - Web UI (ReScript) + Rust backend, MIT/Apache-2.0
+1. **Tauri 2.0+** - Web UI (AffineScript) + Rust backend, MIT/Apache-2.0
 2. **Dioxus** - Pure Rust native UI, MIT/Apache-2.0
 
 Both are FOSS with independent governance (no Big Tech).
 
 ### Enforcement Rules
 
-1. **No new TypeScript files** - Convert existing TS to ReScript
-2. **No package.json for runtime deps** - Use deno.json imports
+1. **No new TypeScript files** - Convert existing TS to AffineScript
+2. **No package.json - use deno.json deps** - Use deno.json imports
 3. **No node_modules in production** - Deno caches deps automatically
 4. **No Go code** - Use Rust instead
 5. **Python only for SaltStack** - All other Python must be rewritten