fix(proofs): resolve Lean4 sorry in RMOOperations

Replace the sorry in obliterate_not_injective with a complete proof.
The theorem was strengthened with two additional hypotheses:
- hmapped: mapped blocks have same blockId, blockData.length, overwriteCount
- hlen: patterns list is nonempty (required — 0 passes cannot erase data)

Three auxiliary lemmas provide the proof infrastructure:
- overwriteBlock_determined_by_shape: same shape → same overwrite result
- overwritePathBlocks_storage_eq: one pass makes storage identical
- multiPassOverwrite_congr: equal inputs → equal outputs

Proof strategy: after one deterministic overwrite pass, mapped blocks
become byte-identical (pattern output depends only on shape, not data).
Remaining passes operate on equal StorageFS values, producing equal results.

Proof holes audit updated: 4 → 3 remaining gaps.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/PROOF_HOLES_AUDIT.md

@@ -66,16 +66,21 @@ Replaced with `obliterate_not_injective` — the correct formalization of "not r
 
 These are provable by induction on path length but require significant infrastructure. Axiomatized with clear specifications.
 
-## Remaining Real Gaps (4)
+## Remaining Real Gaps (3)
 
-### RMO Storage Proofs (2 gaps — low priority)
+### RMO Storage Proofs (1 gap remaining — low priority)
 
 | File | Line | Theorem | Gap |
 |------|------|---------|-----|
-| `lean4/RMOOperations.lean` | 197 | `obliterate_not_injective` | Storage equality under multiPassOverwrite |
 | `coq/rmo_operations.v` | 214 | `obliterate_overwrites_all_blocks` | Induction over overwrite passes |
 
-Both require showing that `multiPassOverwrite` is determined by the mapping and patterns, not by original block data. Non-trivial but purely mechanical induction.
+~~`lean4/RMOOperations.lean` `obliterate_not_injective`~~ **RESOLVED 2026-03-22** — Proved via
+three auxiliary lemmas (`overwriteBlock_determined_by_shape`, `overwritePathBlocks_storage_eq`,
+`multiPassOverwrite_congr`). The theorem was strengthened with a `hmapped` hypothesis (mapped blocks
+must have same blockId/length/overwriteCount) and `hlen` (patterns nonempty). After one deterministic
+overwrite pass, mapped blocks become byte-identical; remaining passes operate on equal inputs.
+
+The Coq gap (`obliterate_overwrites_all_blocks`) requires similar mechanical induction.
 
 ### Agda Deferred Proofs (2 gaps — medium priority)
 
@@ -95,7 +100,7 @@ Both have full proof sketches and are proven in corresponding Lean 4/Coq files.
 
 ## Recommendations
 
-1. **4 remaining gaps are all low-medium priority** — RMO is not user-facing, Agda proofs exist in Lean 4
+1. **3 remaining gaps are all low-medium priority** — RMO is not user-facing, Agda proofs exist in Lean 4
 2. **Axiom count is healthy** — 4 new axioms are well-known filesystem/type theory properties
 3. **Model improvement needed**: Parameterize `mkdir`/`createFile` with permissions for full reverse-direction reversibility
 4. **Consider**: Agda `--cubical` flag provides funext natively, removing 1 structural axiom

proofs/lean4/RMOOperations.lean

@@ -130,6 +130,64 @@ def noTraceRemains (p : Path) (sfs : StorageFS) : Prop :=
 -- Helper Lemmas
 -- ============================================================================
 
+/-- Two blocks with equal id, data length, and overwrite count produce
+    identical results after overwriteBlock, regardless of original data. -/
+theorem overwriteBlock_determined_by_shape (blk1 blk2 : StorageBlock)
+    (pattern : OverwritePattern)
+    (hid : blk1.blockId = blk2.blockId)
+    (hlen : blk1.blockData.length = blk2.blockData.length)
+    (hcount : blk1.overwriteCount = blk2.overwriteCount) :
+    overwriteBlock blk1 pattern = overwriteBlock blk2 pattern := by
+  simp [overwriteBlock, hid, hlen, hcount]
+
+/-- overwritePathBlocks does not change the mapping -/
+theorem overwritePathBlocks_preserves_mapping (sfs : StorageFS) (p : Path)
+    (pattern : OverwritePattern) :
+    (overwritePathBlocks sfs p pattern).mapping = sfs.mapping := by
+  simp [overwritePathBlocks]
+
+/-- multiPassOverwrite does not change the mapping -/
+theorem multiPassOverwrite_preserves_mapping (sfs : StorageFS) (p : Path)
+    (patterns : List OverwritePattern) :
+    (multiPassOverwrite sfs p patterns).mapping = sfs.mapping := by
+  induction patterns generalizing sfs with
+  | nil => simp [multiPassOverwrite]
+  | cons pat rest ih =>
+    simp [multiPassOverwrite]
+    rw [ih]
+    exact overwritePathBlocks_preserves_mapping sfs p pat
+
+/-- For a block NOT in the mapping for path p, overwritePathBlocks
+    preserves it unchanged. -/
+theorem overwritePathBlocks_non_mapped (sfs : StorageFS) (p : Path)
+    (pattern : OverwritePattern) (bid : Nat)
+    (hnotmapped : bid ∉ sfs.mapping p) :
+    (overwritePathBlocks sfs p pattern).storage bid = sfs.storage bid := by
+  simp [overwritePathBlocks]
+  match h : sfs.storage bid with
+  | none => simp [h]
+  | some blk =>
+    simp [h]
+    have : (sfs.mapping p).contains bid = false := by
+      simp [List.contains] at hnotmapped ⊢
+      exact hnotmapped
+    simp [this]
+
+/-- For a block IN the mapping for path p, overwritePathBlocks overwrites
+    it with the pattern. The result depends only on blockId, blockData.length,
+    overwriteCount, and the pattern — not on the original data. -/
+theorem overwritePathBlocks_mapped (sfs : StorageFS) (p : Path)
+    (pattern : OverwritePattern) (bid : Nat) (blk : StorageBlock)
+    (hmapped : bid ∈ sfs.mapping p)
+    (hblk : sfs.storage bid = some blk) :
+    (overwritePathBlocks sfs p pattern).storage bid =
+      some (overwriteBlock blk pattern) := by
+  simp [overwritePathBlocks, hblk]
+  have : (sfs.mapping p).contains bid = true := by
+    simp [List.contains] at hmapped ⊢
+    exact hmapped
+  simp [this]
+
 /-- overwritePathBlocks preserves the filesystem tree -/
 theorem overwritePathBlocks_preserves_tree (sfs : StorageFS) (p : Path)
     (pattern : OverwritePattern) :
@@ -147,6 +205,62 @@ theorem multiPassOverwrite_preserves_tree (sfs : StorageFS) (p : Path)
     rw [ih]
     exact overwritePathBlocks_preserves_tree sfs p pat
 
+-- ============================================================================
+-- Storage Equality Lemmas for Non-Injectivity Proof
+-- ============================================================================
+
+/-- After one overwritePathBlocks pass, two filesystems with the same mapping,
+    identical non-mapped blocks, and shape-compatible mapped blocks produce
+    fully identical storage. This is the key lemma: after one pass of a
+    deterministic pattern, the mapped blocks become byte-for-byte identical
+    because overwriteBlock output depends only on shape (blockId, length,
+    overwriteCount) and the pattern, not on original data. -/
+theorem overwritePathBlocks_storage_eq (sfs1 sfs2 : StorageFS) (p : Path)
+    (pattern : OverwritePattern)
+    (hpre1 : obliteratePrecondition p sfs1)
+    (hpre2 : obliteratePrecondition p sfs2)
+    (hmap : sfs1.mapping = sfs2.mapping)
+    (hother : ∀ bid, bid ∉ sfs1.mapping p →
+      sfs1.storage bid = sfs2.storage bid)
+    (hmapped : ∀ bid, bid ∈ sfs1.mapping p →
+      ∀ blk1 blk2, sfs1.storage bid = some blk1 → sfs2.storage bid = some blk2 →
+        blk1.blockId = blk2.blockId ∧
+        blk1.blockData.length = blk2.blockData.length ∧
+        blk1.overwriteCount = blk2.overwriteCount) :
+    (overwritePathBlocks sfs1 p pattern).storage =
+    (overwritePathBlocks sfs2 p pattern).storage := by
+  funext bid
+  by_cases hmem : bid ∈ sfs1.mapping p
+  · -- Mapped block: both get overwriteBlock applied with same pattern.
+    -- The results are identical because the blocks have the same shape.
+    obtain ⟨blk1, hblk1⟩ := hpre1.2.2 bid hmem
+    have hmem2 : bid ∈ sfs2.mapping p := by rw [← hmap]; exact hmem
+    obtain ⟨blk2, hblk2⟩ := hpre2.2.2 bid hmem2
+    rw [overwritePathBlocks_mapped sfs1 p pattern bid blk1 hmem hblk1]
+    rw [overwritePathBlocks_mapped sfs2 p pattern bid blk2 hmem2 hblk2]
+    obtain ⟨hid, hlen, hcount⟩ := hmapped bid hmem blk1 blk2 hblk1 hblk2
+    exact congrArg some (overwriteBlock_determined_by_shape blk1 blk2 pattern hid hlen hcount)
+  · -- Non-mapped block: unchanged by overwrite, already equal by hother
+    have hmem2 : bid ∉ sfs2.mapping p := by rw [← hmap]; exact hmem
+    rw [overwritePathBlocks_non_mapped sfs1 p pattern bid hmem]
+    rw [overwritePathBlocks_non_mapped sfs2 p pattern bid hmem2]
+    exact hother bid hmem
+
+/-- When two StorageFS values have identical tree, storage, and mapping,
+    multiPassOverwrite produces identical results. This is trivially true
+    because equal inputs produce equal outputs. -/
+theorem multiPassOverwrite_congr (sfs1 sfs2 : StorageFS) (p : Path)
+    (patterns : List OverwritePattern)
+    (htree : sfs1.tree = sfs2.tree)
+    (hstorage : sfs1.storage = sfs2.storage)
+    (hmap : sfs1.mapping = sfs2.mapping) :
+    multiPassOverwrite sfs1 p patterns = multiPassOverwrite sfs2 p patterns := by
+  have : sfs1 = sfs2 := by
+    cases sfs1; cases sfs2
+    simp only [StorageFS.mk.injEq] at htree hstorage hmap ⊢
+    exact ⟨htree, hstorage, hmap⟩
+  rw [this]
+
 -- ============================================================================
 -- Theorems
 -- ============================================================================
@@ -175,9 +289,15 @@ theorem obliterate_removes_mapping (p : Path) (sfs : StorageFS)
 /-- Theorem: RMO is not injective — different starting states produce the
     same result. This means no uniform recovery function exists.
 
-    Specifically: two filesystems that differ only in block data for path p
-    produce identical results after obliteration, because the block data is
-    overwritten with fixed patterns. -/
+    Specifically: two filesystems that differ only in block data content for
+    path p produce identical results after obliteration, because the block data
+    is overwritten with deterministic patterns. Requires at least one overwrite
+    pass (patterns nonempty) so the deterministic overwrite erases differences
+    in block content.
+
+    The `hmapped` hypothesis formalizes "differ only in block data": mapped
+    blocks must have the same blockId, blockData.length, and overwriteCount.
+    Only the actual byte content may differ. -/
 theorem obliterate_not_injective (p : Path)
     (sfs1 sfs2 : StorageFS)
     (patterns : List OverwritePattern)
@@ -186,55 +306,45 @@ theorem obliterate_not_injective (p : Path)
     (htree : sfs1.tree = sfs2.tree)
     (hmap : sfs1.mapping = sfs2.mapping)
     (hother : ∀ bid, bid ∉ sfs1.mapping p →
-      sfs1.storage bid = sfs2.storage bid) :
+      sfs1.storage bid = sfs2.storage bid)
+    (hmapped : ∀ bid, bid ∈ sfs1.mapping p →
+      ∀ blk1 blk2, sfs1.storage bid = some blk1 → sfs2.storage bid = some blk2 →
+        blk1.blockId = blk2.blockId ∧
+        blk1.blockData.length = blk2.blockData.length ∧
+        blk1.overwriteCount = blk2.overwriteCount)
+    (hlen : patterns.length > 0) :
     obliterate p sfs1 patterns = obliterate p sfs2 patterns := by
-  simp [obliterate, removeBlockMapping]
-  constructor
-  · -- tree: deleteFile on same tree (after multiPassOverwrite preserves tree)
-    rw [multiPassOverwrite_preserves_tree, multiPassOverwrite_preserves_tree, htree]
-  constructor
-  · -- storage: both overwrite the same blocks with same patterns, other blocks same
-    -- PROOF OBLIGATION: multiPassOverwrite produces identical storage given:
-    --   (a) same block mapping (hmap), (b) same overwrite patterns, and
-    --   (c) non-mapped blocks are identical (hother).
-    --
-    -- WHY DEFERRED: Requires an auxiliary lemma:
-    --   multiPassOverwrite_storage_determined :
-    --     ∀ (sfs1 sfs2 : StorageFS) (p : Path) (patterns : List OverwritePattern),
-    --       sfs1.mapping = sfs2.mapping →
-    --       (∀ bid, bid ∉ sfs1.mapping p → sfs1.storage bid = sfs2.storage bid) →
-    --       (multiPassOverwrite sfs1 p patterns).storage =
-    --         (multiPassOverwrite sfs2 p patterns).storage
-    --
-    -- PROOF SKETCH:
-    --   Induction on patterns.
-    --   Base case: trivial (multiPassOverwrite [] = identity).
-    --   Inductive case: After one overwritePathBlocks pass, blocks in mapping p
-    --     are overwritten with the same pattern data (determined solely by pattern
-    --     and block size). Blocks NOT in mapping p are unchanged. Since block sizes
-    --     in the mapping are determined by storage (and non-mapped blocks are same
-    --     by hother), the result after one pass has the same property: non-mapped
-    --     blocks still equal, mapped blocks now identical. Apply IH.
-    --
-    --   The key sub-lemma is that overwriteBlock depends only on blockData.length
-    --   and the pattern, not on the original data. Two blocks with the same length
-    --   produce identical results after overwriteBlock.
-    --
-    -- ADDITIONAL LEMMAS NEEDED:
-    --   1. overwriteBlock_length_determined: block sizes equal → overwriteBlock equal
-    --   2. overwritePathBlocks_non_mapped_preserved: non-mapped blocks unchanged
-    --   3. overwritePathBlocks_mapped_determined: mapped blocks depend only on size+pattern
-    --
-    -- BLOCKED: Proving functional extensionality on Storage (Nat → Option StorageBlock)
-    -- after multi-pass overwrite requires the 3 auxiliary lemmas above, plus induction
-    -- on the pattern list. The proof is structurally sound (sketch verified) but
-    -- formalizing it requires ~50 lines of auxiliary lemmas about List.map, List.range,
-    -- and overwriteBlock determinism. This is a genuine proof obligation, not a gap
-    -- in the theorem statement.
-    sorry  -- BLOCKED: requires 3 auxiliary lemmas (see comments above)
-  · -- mapping: same since hmap
-    funext p'
-    simp [hmap]
+  -- Decompose patterns into pat :: rest (guaranteed nonempty by hlen)
+  match patterns, hlen with
+  | pat :: rest, _ =>
+    simp [obliterate, removeBlockMapping]
+    constructor
+    · -- tree: deleteFile on same tree (multiPassOverwrite preserves tree)
+      rw [multiPassOverwrite_preserves_tree, multiPassOverwrite_preserves_tree, htree]
+    constructor
+    · -- storage: After one pass of overwritePathBlocks, both filesystems have
+      -- identical storage (by overwritePathBlocks_storage_eq). The remaining
+      -- passes (multiPassOverwrite on rest) then operate on identical inputs
+      -- and produce identical outputs.
+      simp [multiPassOverwrite]
+      -- Step 1: After one pass, storage is identical
+      have hstorage_eq := overwritePathBlocks_storage_eq sfs1 sfs2 p pat
+        hpre1 hpre2 hmap hother hmapped
+      -- Step 2: Tree and mapping are also preserved identically
+      have htree_eq : (overwritePathBlocks sfs1 p pat).tree =
+                      (overwritePathBlocks sfs2 p pat).tree := by
+        rw [overwritePathBlocks_preserves_tree, overwritePathBlocks_preserves_tree, htree]
+      have hmap_eq : (overwritePathBlocks sfs1 p pat).mapping =
+                     (overwritePathBlocks sfs2 p pat).mapping := by
+        rw [overwritePathBlocks_preserves_mapping, overwritePathBlocks_preserves_mapping, hmap]
+      -- Step 3: Equal inputs → equal outputs for remaining passes
+      have h := multiPassOverwrite_congr
+        (overwritePathBlocks sfs1 p pat) (overwritePathBlocks sfs2 p pat)
+        p rest htree_eq hstorage_eq hmap_eq
+      exact congrArg StorageFS.storage h
+    · -- mapping: same since hmap
+      funext p'
+      simp [hmap]
 
 /-- Theorem: Obliteration preserves unrelated paths -/
 theorem obliterate_preserves_other_paths (p p' : Path) (sfs : StorageFS)
@@ -260,11 +370,11 @@ theorem obliterate_leaves_no_trace (p : Path) (sfs : StorageFS)
 /-
   Summary of Proven Claims:
 
-  ✓ obliterate_removes_path - RMO removes path from filesystem
-  ✓ obliterate_removes_mapping - RMO removes block mappings
-  ✓ obliterate_not_reversible - RMO is NOT reversible (key distinction from RMR)
-  ✓ obliterate_preserves_other_paths - RMO preserves unrelated paths
-  ✓ obliterate_leaves_no_trace - GDPR Article 17 compliance
+  obliterate_removes_path - RMO removes path from filesystem
+  obliterate_removes_mapping - RMO removes block mappings
+  obliterate_not_injective - RMO is NOT injective (different data, same result)
+  obliterate_preserves_other_paths - RMO preserves unrelated paths
+  obliterate_leaves_no_trace - GDPR Article 17 compliance
 -/
 
 end ValenceShell.RMO