fix(lean4): remove dead contradiction — greens the Lean 4 CI (#155)

## What & why

`proofs/lean4/FilesystemModel.lean` fails `lake build` on `main` under
Lean 4.12.0:

```
error: FilesystemModel.lean:97:4: no goals to be solved
```

In `nonempty_path_ne_parent`, the `simp at hp2` on the preceding line
derives the impossible `rest = x :: rest` and **closes the goal by
itself**, so the trailing `contradiction` was dead code — which newer
Lean rejects rather than ignores. Removing it fixes the build.

This was a **pre-existing failure on `main`** (surfaced red on
#152/#153/#154, none of which touched Lean), so it isn't a regression
from any recent PR — it's just been chronically red.

## Verification

Reproduced and fixed with the **same toolchain CI uses** (`elan` →
`leanprover/lean4:v4.12.0`):

```
cd proofs/lean4 && lake build
# before: error: FilesystemModel.lean:97:4: no goals to be solved → build failed
# after:  Build completed successfully.
```

Greens both Lean jobs — `Verify Lean 4 Proofs` (rust-cli.yml) and `Build
and Test Lean Extraction Pipeline` (lean-verification.yml). Only
harmless `unused variable hpre` lints remain (warnings, not errors).

## Not included
The **fuzzing** red checks (`pr_fuzzing`) are a separate, unrelated
CI-infra issue — `cargo install cargo-fuzz` fails to build (`thiserror`
E0463) in the OSS-Fuzz base image, before any project code is compiled.
That needs its own pass (pin `cargo-fuzz` or the base image), not a code
change here.

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

https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU

---
_Generated by [Claude
Code](https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

proofs/lean4/FilesystemModel.lean

@@ -93,8 +93,10 @@ theorem nonempty_path_ne_parent (p : Path) (h : p ≠ []) :
     -- Which means rest = x :: rest (after reverse cancellation), impossible
     have hp2 : p.reverse = x :: rest := hp
     rw [heq] at hp2
+    -- `simp` derives `rest = x :: rest` in `hp2`, which is impossible, so it
+    -- closes the goal on its own; a trailing `contradiction` is dead here
+    -- (Lean 4.12 rejects it as "no goals to be solved").
     simp at hp2
-    contradiction
 
 theorem pathExists_emptyFS_root :
     pathExists rootPath emptyFS := by