proof(absolute-zero): close FilesystemCNO.lean sorry (idempotent != CNO)

Restructure the "idempotent does NOT imply CNO" example to destructure
mkdir_not_identity first and exhibit the specific witness path p, then
derive the contradiction with h_neq (h fs) in a single step — no sorry
needed.

Also drops the vestigial `import Std.Data.List.Basic`. That module does
not exist in current Lean 4 (Std.Data.List.Basic was subsumed by
Batteries / core Init in the 4.x line); the file uses only the `List`
type from core Init, so the import was scaffolding drift.

VERIFICATION STATUS:
  - Logical correctness of the fix: manually validated against the
    isFsCNO definition and mkdir_not_identity's type.
  - Local `lean --check` blocked by pre-existing drift elsewhere in the
    same file that is unrelated to this sorry:
      * line 39 / 46: `deriving Repr, BEq` on `def PermSet : Type := ...`
        aliases (not supported in current Lean 4).
      * line 100: `(meta : FileMetadata)` parameter binder — `meta` is
        now a reserved word in Lean 4.
    These are file-wide issues separate from the proof-debt sorry and
    would benefit from a coordinated absolute-zero toolchain refresh
    (pin `lean-toolchain`, run `lake update`, add `deriving` for the
    record types rather than the aliases, rename `meta` binder).

Refs: proof-debt-plan.md Dependability / absolute-zero Lean4.

Author: hyperpolymath

proofs/lean4/FilesystemCNO.lean

@@ -8,7 +8,8 @@
    License: AGPL-3.0 / Palimpsest 0.5
 -/
 
-import Std.Data.List.Basic
+-- Std.Data.List.Basic was vestigial in pre-Batteries layouts. The List
+-- type used here comes from core Lean 4's Init; no external imports required.
 
 namespace FilesystemCNO
 
@@ -287,15 +288,18 @@ def isIdempotent (op : FsOp) : Prop :=
 axiom mkdir_idempotent (p : Path) :
   isIdempotent (fun fs => mkdir p fs)
 
-/-- Idempotent does NOT imply CNO -/
+/-- Idempotent does NOT imply CNO.
+    Proof: destructure mkdir_not_identity to get a specific (p, fs) where
+    mkdir p fs ≠ fs, then exhibit `fun fs => mkdir p fs` as the witness.
+    It is idempotent (mkdir_idempotent), but it cannot be a CNO: if it were,
+    applying it to fs would leave fs unchanged, contradicting h_neq. -/
 example : ∃ op : FsOp, isIdempotent op ∧ ¬ isFsCNO op := by
-  exists (fun fs => mkdir "test" fs)
+  obtain ⟨p, fs, h_neq⟩ := mkdir_not_identity
+  exists (fun fs' => mkdir p fs')
   constructor
-  · exact mkdir_idempotent "test"
+  · exact mkdir_idempotent p
   · intro h
     unfold isFsCNO at h
-    obtain ⟨p, fs, h_neq⟩ := mkdir_not_identity
-    have := h fs
-    sorry  -- mkdir changes filesystem
+    exact h_neq (h fs)
 
 end FilesystemCNO