diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 2c24f7e..01269af 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -184,17 +184,27 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`.
   signature, the three occupancy predicates in full, the #125 derivations as
   negative controls, and `#print axioms` for every theorem (no `sorryAx` anywhere).
   `just verify-lean-core` runs the same script locally.
-* **FilesystemCNO ported from Coq (issue #167):**
-  `FilesystemCNO.lean` defines `Filesystem` as a concrete list structure and operations
-  as executable functions (`mkdir`, `rmdir`, `create`, `unlink`, `readFile`, `writeFile`,
-  `stat`, `chmod`, `chown`, `rename`, `snapshot`, `restore`). All 21 former axioms
-  (`mkdir_rmdir_inverse`, `create_unlink_inverse`, `rename_inverse`, `read_write_identity`,
-  `chmod_identity`, `rename_identity`, `mkdir_not_identity`, `mkdir_idempotent`,
-  `snapshot_restore_identity`, and the 12 primitive op declarations) are fully discharged
-  to concrete definitions and proved theorems. `AxiomAudit.lean` verifies that all
-  FilesystemCNO theorems depend on zero axioms.
-  Lean axiom count: `FilesystemCNO` 21 → **0**, `LambdaCNO` 3 → 1
+* **Issue #125 fixed — the Lean axioms no longer derive `False`:**
+  `FilesystemCNO.lean` stated `mkdir_rmdir_inverse`, `create_unlink_inverse` and
+  `rename_inverse` without the occupancy preconditions of the Coq lemmas they mirror;
+  with `mkdir_idempotent` and `mkdir_not_identity` that proved `False`. They now
+  carry `noDirAt` / `noFileAt` / `noEntryAt`, mirrored verbatim from
+  `proofs/coq/filesystem/FilesystemCNO.v`, and the unconditional statement is refuted
+  in-file (`unconditional_mkdir_rmdir_inverse_is_false`). `LambdaCNO.lean` carried the
+  unrestricted `eta_equivalence` axiom (false as stated, the same `LVar 5`
+  counterexample the Coq side documents above); it is now the proved
+  `noLambda`-guarded theorem, `subst_closed_term` is proved, and the unrestricted
+  claim is refuted (`unrestricted_eta_equivalence_is_false`). Lean axiom count:
+  `FilesystemCNO` 21 → 21 (same names, three strengthened), `LambdaCNO` 3 → 1
   (`y_combinator_not_identity`, the Lean twin of Coq's class-A `y_not_cno`).
+* **#167 port reverted pending completion (issue #176):** #174 attempted to port
+  `FilesystemCNO.lean`'s 21 axioms to concrete definitions and proved theorems, but
+  the port did not compile in the six-module job (unresolved `Directory`/`Symlink`
+  alternatives, unknown identifiers, failed rewrites). Per #176's ruling, a half-port
+  must not sit red on `main`: `FilesystemCNO.lean` and its paired `AxiomAudit.lean`
+  guards are restored here to the revision above (their last state that compiled,
+  identical to the pre-#174 commit and to the last green `main` run before #174).
+  #167 stays open with finishing the port as its own acceptance criterion.
 
 == Z3 — VERIFIED (this environment)
 
@@ -240,7 +250,13 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`.
   of 182 top-level theorems across the 14 theories, exactly **109 are closed under
   the global context** (zero axioms), and 73 rest on Coq stdlib classical axioms
   (`ClassicalDedekindReals.*`, `FunctionalExtensionality.*`, `Classical_Prop.classic`,
-  `ProofIrrelevance.*`) and/or the tagged project parameters.
+  `ProofIrrelevance.*`) and/or the tagged project parameters. Each theory's logical
+  root is read from `_CoqProject`'s own `-R <dir> <Root>` bindings rather than
+  hardcoded (issue #176: the census previously assumed every theory lived under
+  `CNO.`, which is false for `malbolge/` — bound to `Malbolge` — and made the
+  generated driver fail outright instead of censusing it; the table now shows
+  `Malbolge.MalbolgeCore | 7 | 7 | 0`). A directory with no `-R` binding is a hard
+  census failure, never a silent skip.
 * All top-level declarations are verified by `proofs/coq/check-axiom-tags.sh` to carry
   a unified tag grammar: `(* AXIOM: [METAL-BOUNDARY] ... *)` for physical constants
   and laws, or `(* AXIOM: [CLASS-A] ... *)` for provable-in-principle mathematics.
diff --git a/proofs/coq/census-assumptions.sh b/proofs/coq/census-assumptions.sh
index 6f2051f..f948dc7 100755
--- a/proofs/coq/census-assumptions.sh
+++ b/proofs/coq/census-assumptions.sh
@@ -17,12 +17,37 @@ set -uo pipefail
 HERE="$(cd "$(dirname "$0")" && pwd)"
 AUDIT_FILE="${1:-}"
 
-# Find all 14 theories under proofs/coq
+# Logical root for each theory directory, read from _CoqProject (`-R <dir> <Root>`)
+# rather than hardcoded — issue #176: the census used to assume every theory lived
+# under `CNO.`, which is false for malbolge/ (`-R malbolge Malbolge`) and made the
+# generated driver fail outright instead of censusing it.
+declare -A dir_root
+while read -r flag dir ns || [ -n "$flag" ]; do
+  [ "$flag" = "-R" ] && dir_root["$dir"]="$ns"
+done < "$HERE/_CoqProject"
+
+# Find all 14 theories under proofs/coq, resolving each theory's logical root.
+# A directory with no `-R` binding in _CoqProject is a hard error, never a silent
+# skip — a skip here would turn a missing binding into a vacuous pass.
 theories=()
+declare -A base_root
 for d in common category quantum lambda filesystem physics ond malbolge; do
   if [ -d "$HERE/$d" ]; then
+    root="${dir_root[$d]:-}"
+    if [ -z "$root" ]; then
+      echo "CENSUS FAILED: directory '$d' has no -R binding in _CoqProject" >&2
+      exit 1
+    fi
     while IFS= read -r f; do
-      [ -f "$f" ] && theories+=("$f")
+      if [ -f "$f" ]; then
+        base="$(basename "${f%.v}")"
+        if [ -n "${base_root[$base]+x}" ]; then
+          echo "CENSUS FAILED: duplicate theory basename '$base' in '$f'" >&2
+          exit 1
+        fi
+        theories+=("$f")
+        base_root["$base"]="$root"
+      fi
     done < <(find "$HERE/$d" -maxdepth 1 -name "*.v" | sort)
   fi
 done
@@ -48,20 +73,22 @@ if command -v coqc >/dev/null 2>&1 && [ -f "$HERE/common/CNO.vo" ]; then
   tmp="$(mktemp -d "${TMPDIR:-/tmp}/az-census.XXXXXX")"
   trap 'rm -rf "$tmp"' EXIT
 
-  # Generate Census.v
+  # Generate Census.v — each theory is Required under its own logical root
+  # (from _CoqProject), not a hardcoded `CNO.`.
   {
     echo "(* Auto-generated by census-assumptions.sh *)"
     for f in "${theories[@]}"; do
       base="$(basename "${f%.v}")"
-      echo "Require CNO.$base."
+      echo "Require ${base_root[$base]}.$base."
     done
     for t in "${thm_lines[@]}"; do
-      echo "Print Assumptions CNO.$t."
+      base="${t%%.*}"
+      echo "Print Assumptions ${base_root[$base]}.$t."
     done
   } > "$tmp/Census.v"
 
   RFLAGS=()
-  while read -r flag dir ns; do
+  while read -r flag dir ns || [ -n "$flag" ]; do
     [ "$flag" = "-R" ] && RFLAGS+=("-R" "$HERE/$dir" "$ns")
   done < "$HERE/_CoqProject"
 
@@ -73,29 +100,42 @@ if command -v coqc >/dev/null 2>&1 && [ -f "$HERE/common/CNO.vo" ]; then
     exit 1
   fi
 
-  # Parse census output
+  # `coqc` does NOT echo the `Print Assumptions X.` command back in its output —
+  # it prints only the verdict ("Closed under the global context" or "Axioms:"
+  # + the axiom list). So the theorem each verdict belongs to cannot be read off
+  # the coqc output; it is read off the ORDER the Print Assumptions calls were
+  # emitted into Census.v instead, which is exactly thm_lines' order. The order
+  # file lists each theorem as "root.base.thm" so the table can key rows by
+  # "root.base" (issue #176 criterion: malbolge/ theorems shown under `Malbolge.`,
+  # not folded into a bare basename column that hides the root entirely).
+  for t in "${thm_lines[@]}"; do
+    base="${t%%.*}"
+    echo "${base_root[$base]}.$t"
+  done > "$tmp/order.txt"
+
+  # Parse census output against the order file. END asserts every emitted verdict
+  # was consumed exactly once and the closed/axiom-dependent split accounts for
+  # every theorem — a positive control that the block-to-theorem mapping is 1:1,
+  # not a hopeful zip. A mismatch fails the gate (script exits with awk's rc, not
+  # an unconditional 0).
   printf '%s\n' "$out" | awk -v total="$total_theorems" '
-    BEGIN {
-      current_thm = ""
-      in_axioms = 0
-    }
-    /^Print Assumptions/ {
-      current_thm = $3
-      sub(/\.$/, "", current_thm)
-      split(current_thm, p, ".")
-      theory = p[2]
-      thm = p[3]
-      thms_per_theory[theory]++
-      in_axioms = 0
-      next
-    }
+    NR == FNR { order[++n] = $0; next }
+    FNR == 1 { idx = 0; in_axioms = 0 }
     /^Closed under the global context/ {
+      idx++
+      split(order[idx], p, ".")
+      theory = p[1] "." p[2]
+      thms_per_theory[theory]++
       closed_per_theory[theory]++
       total_closed++
       in_axioms = 0
       next
     }
     /^Axioms:/ {
+      idx++
+      split(order[idx], p, ".")
+      theory = p[1] "." p[2]
+      thms_per_theory[theory]++
       axiom_dep_per_theory[theory]++
       total_dep++
       in_axioms = 1
@@ -108,21 +148,39 @@ if command -v coqc >/dev/null 2>&1 && [ -f "$HERE/common/CNO.vo" ]; then
       next
     }
     END {
+      if (idx != total) {
+        printf "CENSUS FAILED: %d verdict blocks parsed, expected %d theorems\n", idx, total > "/dev/stderr"
+        exit 1
+      }
+      if (total_closed + total_dep != total) {
+        printf "CENSUS FAILED: closed(%d) + axiom-dependent(%d) != total(%d)\n", total_closed, total_dep, total > "/dev/stderr"
+        exit 1
+      }
       printf "\n== Census: %d top-level theorems across 14 theories ==\n", total
       printf "Closed under global context: %d\nAxiom-dependent: %d\n\n", total_closed, total_dep
-      printf "| %-22s | %-8s | %-6s | %-15s |\n", "Theory", "Theorems", "Closed", "Axiom-Dependent"
-      printf "|------------------------|----------|--------|-----------------|\n"
-      for (t in thms_per_theory) {
+      printf "| %-24s | %-8s | %-6s | %-15s |\n", "Theory", "Theorems", "Closed", "Axiom-Dependent"
+      printf "|--------------------------|----------|--------|-----------------|\n"
+      # Manual sort (no asorti — that is a gawk extension, and the CI runner is
+      # not guaranteed to alias /usr/bin/awk to gawk).
+      n_rows = 0
+      for (t in thms_per_theory) sorted[++n_rows] = t
+      for (i = 1; i <= n_rows; i++)
+        for (j = i + 1; j <= n_rows; j++)
+          if (sorted[j] < sorted[i]) { tmp = sorted[i]; sorted[i] = sorted[j]; sorted[j] = tmp }
+      for (i = 1; i <= n_rows; i++) {
+        t = sorted[i]
         c = closed_per_theory[t] + 0
         d = axiom_dep_per_theory[t] + 0
-        printf "| %-22s | %-8d | %-6d | %-15d |\n", t, thms_per_theory[t], c, d
+        printf "| %-24s | %-8d | %-6d | %-15d |\n", t, thms_per_theory[t], c, d
       }
       printf "\n== Axioms in non-closed blocks ==\n"
       for (ax in axiom_counts) {
         printf "  %-50s : %d\n", ax, axiom_counts[ax]
       }
     }
-  '
+  ' "$tmp/order.txt" -
+  rc=$?
+  exit "$rc"
 else
   # Static / pre-computed census display when coqc / .vo is not yet built
   echo "== Census: $total_theorems top-level theorems across 14 theories =="
diff --git a/proofs/lean4/AxiomAudit.lean b/proofs/lean4/AxiomAudit.lean
index c3f1700..d4c4929 100644
--- a/proofs/lean4/AxiomAudit.lean
+++ b/proofs/lean4/AxiomAudit.lean
@@ -519,27 +519,35 @@ info: 'FilesystemCNO.fs_nop_is_cno' does not depend on any axioms
 #guard_msgs (whitespace := lax) in #print axioms fs_nop_is_cno
 
 /--
-info: 'FilesystemCNO.mkdir_rmdir_is_cno' does not depend on any axioms
+info: 'FilesystemCNO.mkdir_rmdir_is_cno' depends on axioms: [FilesystemCNO.mkdir,
+ FilesystemCNO.mkdir_rmdir_inverse,
+ FilesystemCNO.rmdir]
 -/
 #guard_msgs (whitespace := lax) in #print axioms mkdir_rmdir_is_cno
 
 /--
-info: 'FilesystemCNO.create_unlink_is_cno' does not depend on any axioms
+info: 'FilesystemCNO.create_unlink_is_cno' depends on axioms: [FilesystemCNO.create,
+ FilesystemCNO.create_unlink_inverse,
+ FilesystemCNO.unlink]
 -/
 #guard_msgs (whitespace := lax) in #print axioms create_unlink_is_cno
 
 /--
-info: 'FilesystemCNO.read_write_is_cno' does not depend on any axioms
+info: 'FilesystemCNO.read_write_is_cno' depends on axioms: [FilesystemCNO.readFile,
+ FilesystemCNO.read_write_identity,
+ FilesystemCNO.writeFile]
 -/
 #guard_msgs (whitespace := lax) in #print axioms read_write_is_cno
 
 /--
-info: 'FilesystemCNO.chmod_nop_is_cno' does not depend on any axioms
+info: 'FilesystemCNO.chmod_nop_is_cno' depends on axioms: [FilesystemCNO.chmod,
+ FilesystemCNO.chmod_identity,
+ FilesystemCNO.stat]
 -/
 #guard_msgs (whitespace := lax) in #print axioms chmod_nop_is_cno
 
 /--
-info: 'FilesystemCNO.rename_nop_is_cno' does not depend on any axioms
+info: 'FilesystemCNO.rename_nop_is_cno' depends on axioms: [FilesystemCNO.rename, FilesystemCNO.rename_identity]
 -/
 #guard_msgs (whitespace := lax) in #print axioms rename_nop_is_cno
 
@@ -549,7 +557,7 @@ info: 'FilesystemCNO.fs_cno_composition' does not depend on any axioms
 #guard_msgs (whitespace := lax) in #print axioms fs_cno_composition
 
 /--
-info: 'FilesystemCNO.mkdir_alone_not_cno' does not depend on any axioms
+info: 'FilesystemCNO.mkdir_alone_not_cno' depends on axioms: [FilesystemCNO.mkdir, FilesystemCNO.mkdir_not_identity]
 -/
 #guard_msgs (whitespace := lax) in #print axioms mkdir_alone_not_cno
 
@@ -559,12 +567,17 @@ info: 'FilesystemCNO.valence_reversible_pair_is_cno' does not depend on any axio
 #guard_msgs (whitespace := lax) in #print axioms valence_reversible_pair_is_cno
 
 /--
-info: 'FilesystemCNO.snapshot_restore_is_cno' does not depend on any axioms
+info: 'FilesystemCNO.snapshot_restore_is_cno' depends on axioms: [FilesystemCNO.restore,
+ FilesystemCNO.snapshot,
+ FilesystemCNO.snapshot_restore_identity]
 -/
 #guard_msgs (whitespace := lax) in #print axioms snapshot_restore_is_cno
 
 /--
-info: 'FilesystemCNO.unconditional_mkdir_rmdir_inverse_is_false' does not depend on any axioms
+info: 'FilesystemCNO.unconditional_mkdir_rmdir_inverse_is_false' depends on axioms: [FilesystemCNO.mkdir,
+ FilesystemCNO.mkdir_idempotent,
+ FilesystemCNO.mkdir_not_identity,
+ FilesystemCNO.rmdir]
 -/
 #guard_msgs (whitespace := lax) in #print axioms unconditional_mkdir_rmdir_inverse_is_false
 end
@@ -650,6 +663,14 @@ run_cmd do
   let modules : Array Name := #[`CNO, `OND, `CNOCategory, `CNOBridge, `FilesystemCNO, `LambdaCNO]
   let allowed : Array Name := #[
     `propext, `Quot.sound,
+    `FilesystemCNO.mkdir, `FilesystemCNO.rmdir, `FilesystemCNO.create,
+    `FilesystemCNO.unlink, `FilesystemCNO.readFile, `FilesystemCNO.writeFile,
+    `FilesystemCNO.chmod, `FilesystemCNO.stat, `FilesystemCNO.rename,
+    `FilesystemCNO.mkdir_rmdir_inverse, `FilesystemCNO.create_unlink_inverse,
+    `FilesystemCNO.read_write_identity, `FilesystemCNO.chmod_identity,
+    `FilesystemCNO.rename_identity, `FilesystemCNO.mkdir_not_identity,
+    `FilesystemCNO.snapshot, `FilesystemCNO.restore,
+    `FilesystemCNO.snapshot_restore_identity, `FilesystemCNO.mkdir_idempotent,
     `LambdaCNO.y_combinator_not_identity
   ]
   let mut checked := 0
diff --git a/proofs/lean4/FilesystemCNO.lean b/proofs/lean4/FilesystemCNO.lean
index a706bcc..014435e 100644
--- a/proofs/lean4/FilesystemCNO.lean
+++ b/proofs/lean4/FilesystemCNO.lean
@@ -75,347 +75,90 @@ def noEntryAt (p : Path) (fs : Filesystem) : Prop :=
     | FileEntry.Directory p' _ _ => p ≠ p'
     | FileEntry.Symlink p' _ _ => p ≠ p'
 
-/-! ## Helper Definitions for Concrete Filesystem Operations -/
-
-/-- Default metadata used when fresh entries are created. -/
-def default_meta : FileMetadata :=
-  { permissions := [], owner := 0, size := 0, mtime := 0 }
-
-/-- The path of an entry regardless of its kind. -/
-def path_of : FileEntry → Path
-  | FileEntry.File p _ _ => p
-  | FileEntry.Directory p _ _ => p
-  | FileEntry.Symlink p _ _ => p
-
-/-- Rename an entry's own path, preserving all other components. -/
-def set_path (np : Path) : FileEntry → FileEntry
-  | FileEntry.File _ c m => FileEntry.File np c m
-  | FileEntry.Directory _ es m => FileEntry.Directory np es m
-  | FileEntry.Symlink _ t m => FileEntry.Symlink np t m
-
-/-- Set permissions on a metadata record. -/
-def set_perms (perms : PermSet) (m : FileMetadata) : FileMetadata :=
-  { permissions := perms, owner := m.owner, size := m.size, mtime := m.mtime }
-
-/-- Set owner on a metadata record. -/
-def set_owner (o : Nat) (m : FileMetadata) : FileMetadata :=
-  { permissions := m.permissions, owner := o, size := m.size, mtime := m.mtime }
-
-/-- Check if a directory with the given path exists in the filesystem. -/
-def dir_exists (p : Path) : Filesystem → Bool
-  | [] => false
-  | e :: rest => match e with
-    | FileEntry.Directory p' _ _ => (p == p') || dir_exists p rest
-    | _ => dir_exists p rest
-
-@[simp] lemma path_of_set_path (p : Path) (e : FileEntry) :
-    path_of (set_path p e) = p := by
-  cases e <;> rfl
-
-@[simp] lemma set_path_id (e : FileEntry) :
-    set_path (path_of e) e = e := by
-  cases e <;> rfl
-
-@[simp] lemma set_path_set_path (p1 p2 : Path) (e : FileEntry) :
-    set_path p2 (set_path p1 e) = set_path p2 e := by
-  cases e <;> rfl
-
-@[simp] lemma set_perms_id (m : FileMetadata) :
-    set_perms m.permissions m = m := by
-  cases m; rfl
-
-/-! ## Filesystem Operations (Concrete, executable definitions) -/
-
-/-- Create directory: prepends fresh directory if absent, no-op if exists. -/
-def mkdir (p : Path) (fs : Filesystem) : Filesystem :=
-  if dir_exists p fs then fs else FileEntry.Directory p [] default_meta :: fs
-
-/-- Remove empty directory: drops first matching empty directory. -/
-def rmdir (p : Path) : Filesystem → Filesystem
-  | [] => []
-  | e :: rest => match e with
-    | FileEntry.Directory p' [] _ => if p == p' then rest else e :: rmdir p rest
-    | _ => e :: rmdir p rest
-
-/-- Create file: prepends fresh empty file. -/
-def create (p : Path) (fs : Filesystem) : Filesystem :=
-  FileEntry.File p [] default_meta :: fs
-
-/-- Delete file: drops first matching file. -/
-def unlink (p : Path) : Filesystem → Filesystem
-  | [] => []
-  | e :: rest => match e with
-    | FileEntry.File p' _ _ => if p == p' then rest else e :: unlink p rest
-    | _ => e :: unlink p rest
-
-/-- Read file content: content of first matching file, if any. -/
-def readFile (p : Path) : Filesystem → Option FileContent
-  | [] => none
-  | e :: rest => match e with
-    | FileEntry.File p' c _ => if p == p' then some c else readFile p rest
-    | _ => readFile p rest
-
-/-- Write file content: update content of first matching file. -/
-def writeFile (p : Path) (content : FileContent) : Filesystem → Filesystem
-  | [] => []
-  | e :: rest => match e with
-    | FileEntry.File p' c m =>
-      if p == p' then FileEntry.File p' content m :: rest
-      else FileEntry.File p' c m :: writeFile p content rest
-    | _ => e :: writeFile p content rest
-
-/-- Get file metadata: metadata of first matching entry. -/
-def stat (p : Path) : Filesystem → Option FileMetadata
-  | [] => none
-  | e :: rest => match e with
-    | FileEntry.File p' _ m => if p == p' then some m else stat p rest
-    | FileEntry.Directory p' _ m => if p == p' then some m else stat p rest
-    | FileEntry.Symlink p' _ m => if p == p' then some m else stat p rest
-
-/-- Change permissions of first matching entry. -/
-def chmod (p : Path) (perms : PermSet) : Filesystem → Filesystem
-  | [] => []
-  | e :: rest => match e with
-    | FileEntry.File p' c m =>
-      if p == p' then FileEntry.File p' c (set_perms perms m) :: rest
-      else FileEntry.File p' c m :: chmod p perms rest
-    | FileEntry.Directory p' es m =>
-      if p == p' then FileEntry.Directory p' es (set_perms perms m) :: rest
-      else FileEntry.Directory p' es m :: chmod p perms rest
-    | FileEntry.Symlink p' t m =>
-      if p == p' then FileEntry.Symlink p' t (set_perms perms m) :: rest
-      else FileEntry.Symlink p' t m :: chmod p perms rest
-
-/-- Change owner of first matching entry. -/
-def chown (p : Path) (o : Nat) : Filesystem → Filesystem
-  | [] => []
-  | e :: rest => match e with
-    | FileEntry.File p' c m =>
-      if p == p' then FileEntry.File p' c (set_owner o m) :: rest
-      else FileEntry.File p' c m :: chown p o rest
-    | FileEntry.Directory p' es m =>
-      if p == p' then FileEntry.Directory p' es (set_owner o m) :: rest
-      else FileEntry.Directory p' es m :: chown p o rest
-    | FileEntry.Symlink p' t m =>
-      if p == p' then FileEntry.Symlink p' t (set_owner o m) :: rest
-      else FileEntry.Symlink p' t m :: chown p o rest
-
-/-- Rename/move file: retargets path of first matching entry. -/
-def rename (p1 p2 : Path) : Filesystem → Filesystem
-  | [] => []
-  | e :: rest =>
-    if p1 == path_of e then set_path p2 e :: rest
-    else e :: rename p1 p2 rest
-
-/-- Snapshot operation: capture current filesystem state. -/
-def snapshot (fs : Filesystem) : Filesystem := fs
-
-/-- Restore operation: restore from snapshot. -/
-def restore (snap : Filesystem) (_current : Filesystem) : Filesystem := snap
-
-/-! ## Helper lemmas -/
-
-lemma no_dir_dir_exists_false (p : Path) (fs : Filesystem) (h : noDirAt p fs) :
-    dir_exists p fs = false := by
-  induction fs with
-  | nil => rfl
-  | cons e rest ih =>
-    cases e with
-    | Directory p' es m =>
-      have h_not : p ≠ p' := h (FileEntry.Directory p' es m) (List.Mem.head _)
-      have h_beq : (p == p') = false := beq_false_of_ne h_not
-      have h_rest : noDirAt p rest := fun e' he' => h e' (List.Mem.tail _ he')
-      show ((p == p') || dir_exists p rest) = false
-      rw [h_beq, ih h_rest]
-      rfl
-    | File p' c m =>
-      have h_rest : noDirAt p rest := fun e' he' => h e' (List.Mem.tail _ he')
-      show dir_exists p rest = false
-      exact ih h_rest
-    | Symlink p' t m =>
-      have h_rest : noDirAt p rest := fun e' he' => h e' (List.Mem.tail _ he')
-      show dir_exists p rest = false
-      exact ih h_rest
-
-/-! ## Operation Theorems (Ported from Coq FilesystemCNO.v) -/
-
-/-- mkdir followed by rmdir is identity — on a filesystem with no directory at `p`. -/
-theorem mkdir_rmdir_inverse (p : Path) (fs : Filesystem) (h : noDirAt p fs) :
-    rmdir p (mkdir p fs) = fs := by
-  unfold mkdir
-  have h_false : dir_exists p fs = false := no_dir_dir_exists_false p fs h
-  rw [if_neg (by rw [h_false]; decide)]
-  show (if p == p then fs else _) = fs
-  rw [beq_self_eq_true p]
-  rfl
-
-/-- create followed by unlink is identity — on a filesystem with no file at `p`. -/
-theorem create_unlink_inverse (p : Path) (fs : Filesystem) (_h : noFileAt p fs) :
-    unlink p (create p fs) = fs := by
-  unfold create unlink
-  show (if p == p then fs else _) = fs
-  rw [beq_self_eq_true p]
-  rfl
+/-! ## Filesystem Operations -/
+
+/-- Create directory -/
+-- AXIOM: mkdir; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
+axiom mkdir : Path → Filesystem → Filesystem
+
+/-- Remove directory -/
+-- AXIOM: rmdir; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
+axiom rmdir : Path → Filesystem → Filesystem
+
+/-- Create file -/
+-- AXIOM: create; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
+axiom create : Path → Filesystem → Filesystem
+
+/-- Delete file -/
+-- AXIOM: unlink; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
+axiom unlink : Path → Filesystem → Filesystem
+
+/-- Read file content -/
+-- AXIOM: readFile; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
+axiom readFile : Path → Filesystem → Option FileContent
+
+/-- Write file content -/
+-- AXIOM: writeFile; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
+axiom writeFile : Path → FileContent → Filesystem → Filesystem
+
+/-- Get file metadata -/
+-- AXIOM: stat; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
+axiom stat : Path → Filesystem → Option FileMetadata
+
+/-- Change permissions -/
+-- AXIOM: chmod; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
+axiom chmod : Path → PermSet → Filesystem → Filesystem
+
+/-- Change owner -/
+-- AXIOM: chown; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
+axiom chown : Path → Nat → Filesystem → Filesystem
+
+/-- Rename/move file -/
+-- AXIOM: rename; opaque POSIX primitive op; §(c) per docs/proof-debt.md.
+axiom rename : Path → Path → Filesystem → Filesystem
+
+/-! ## Operation Axioms -/
+
+/-- mkdir followed by rmdir is identity — on a filesystem with no directory
+    at `p`. Without the precondition the law is false (mkdir on an existing
+    directory is a no-op, so rmdir then removes it) and, together with
+    `mkdir_idempotent` and `mkdir_not_identity`, derived `False` (#125). -/
+-- AXIOM: mkdir_rmdir_inverse; POSIX-semantics specification (mirrors Coq Lemma, same precondition); §(c) per docs/proof-debt.md.
+axiom mkdir_rmdir_inverse (p : Path) (fs : Filesystem) :
+  noDirAt p fs →
+  rmdir p (mkdir p fs) = fs
+
+/-- create followed by unlink is identity — on a filesystem with no file at
+    `p` (the precondition Coq's `create_unlink_inverse` states). -/
+-- AXIOM: create_unlink_inverse; POSIX-semantics specification (mirrors Coq Lemma, same precondition); §(c) per docs/proof-debt.md.
+axiom create_unlink_inverse (p : Path) (fs : Filesystem) :
+  noFileAt p fs →
+  unlink p (create p fs) = fs
 
 /-- read followed by write is identity -/
-theorem read_write_identity (p : Path) (fs : Filesystem) (content : FileContent)
-    (h : readFile p fs = some content) :
-    writeFile p content fs = fs := by
-  induction fs with
-  | nil => contradiction
-  | cons e rest ih =>
-    cases e with
-    | File p' c m =>
-      by_cases hp : p == p'
-      · have hp_eq : p = p' := eq_of_beq hp
-        subst hp_eq
-        show (if p' == p' then FileEntry.File p' content m :: rest else _) = FileEntry.File p' c m :: rest
-        rw [beq_self_eq_true p']
-        have h_content : c = content := by
-          revert h
-          show (if p' == p' then some c else readFile p' rest) = some content → c = content
-          rw [beq_self_eq_true p']
-          intro h_eq; injection h_eq
-        subst h_content
-        rfl
-      · have h_read : readFile p rest = some content := by
-        revert h
-        show (if p == p' then some c else readFile p rest) = some content → readFile p rest = some content
-        rw [if_neg hp]
-        exact id
-        show (if p == p' then _ else FileEntry.File p' c m :: writeFile p content rest) = FileEntry.File p' c m :: rest
-        rw [if_neg hp]
-        rw [ih h_read]
-    | Directory p' es m =>
-      have h_read : readFile p rest = some content := h
-      show FileEntry.Directory p' es m :: writeFile p content rest = FileEntry.Directory p' es m :: rest
-      rw [ih h_read]
-    | Symlink p' t m =>
-      have h_read : readFile p rest = some content := h
-      show FileEntry.Symlink p' t m :: writeFile p content rest = FileEntry.Symlink p' t m :: rest
-      rw [ih h_read]
+-- AXIOM: read_write_identity; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md.
+axiom read_write_identity (p : Path) (fs : Filesystem) (content : FileContent) :
+  readFile p fs = some content →
+  writeFile p content fs = fs
 
 /-- chmod to current permissions is identity -/
-theorem chmod_identity (p : Path) (fs : Filesystem) (meta : FileMetadata)
-    (h : stat p fs = some meta) :
-    chmod p meta.permissions fs = fs := by
-  induction fs with
-  | nil => contradiction
-  | cons e rest ih =>
-    cases e with
-    | File p' c m =>
-      by_cases hp : p == p'
-      · have hp_eq : p = p' := eq_of_beq hp
-        subst hp_eq
-        show (if p' == p' then FileEntry.File p' c (set_perms meta.permissions m) :: rest else _) = FileEntry.File p' c m :: rest
-        rw [beq_self_eq_true p']
-        have h_meta : m = meta := by
-          revert h
-          show (if p' == p' then some m else stat p' rest) = some meta → m = meta
-          rw [beq_self_eq_true p']
-          intro h_eq; injection h_eq
-        subst h_meta
-        rw [set_perms_id]
-      · have h_stat : stat p rest = some meta := by
-          revert h
-          show (if p == p' then some m else stat p rest) = some meta → stat p rest = some meta
-          rw [if_neg hp]
-          exact id
-        show (if p == p' then _ else FileEntry.File p' c m :: chmod p meta.permissions rest) = FileEntry.File p' c m :: rest
-        rw [if_neg hp]
-        rw [ih h_stat]
-    | Directory p' es m =>
-      by_cases hp : p == p'
-      · have hp_eq : p = p' := eq_of_beq hp
-        subst hp_eq
-        show (if p' == p' then FileEntry.Directory p' es (set_perms meta.permissions m) :: rest else _) = FileEntry.Directory p' es m :: rest
-        rw [beq_self_eq_true p']
-        have h_meta : m = meta := by
-          revert h
-          show (if p' == p' then some m else stat p' rest) = some meta → m = meta
-          rw [beq_self_eq_true p']
-          intro h_eq; injection h_eq
-        subst h_meta
-        rw [set_perms_id]
-      · have h_stat : stat p rest = some meta := by
-          revert h
-          show (if p == p' then some m else stat p rest) = some meta → stat p rest = some meta
-          rw [if_neg hp]
-          exact id
-        show (if p == p' then _ else FileEntry.Directory p' es m :: chmod p meta.permissions rest) = FileEntry.Directory p' es m :: rest
-        rw [if_neg hp]
-        rw [ih h_stat]
-    | Symlink p' t m =>
-      by_cases hp : p == p'
-      · have hp_eq : p = p' := eq_of_beq hp
-        subst hp_eq
-        show (if p' == p' then FileEntry.Symlink p' t (set_perms meta.permissions m) :: rest else _) = FileEntry.Symlink p' t m :: rest
-        rw [beq_self_eq_true p']
-        have h_meta : m = meta := by
-          revert h
-          show (if p' == p' then some m else stat p' rest) = some meta → m = meta
-          rw [beq_self_eq_true p']
-          intro h_eq; injection h_eq
-        subst h_meta
-        rw [set_perms_id]
-      · have h_stat : stat p rest = some meta := by
-          revert h
-          show (if p == p' then some m else stat p rest) = some meta → stat p rest = some meta
-          rw [if_neg hp]
-          exact id
-        show (if p == p' then _ else FileEntry.Symlink p' t m :: chmod p meta.permissions rest) = FileEntry.Symlink p' t m :: rest
-        rw [if_neg hp]
-        rw [ih h_stat]
+-- AXIOM: chmod_identity; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md.
+axiom chmod_identity (p : Path) (fs : Filesystem) (meta : FileMetadata) :
+  stat p fs = some meta →
+  chmod p meta.permissions fs = fs
 
 /-- rename to same path is identity -/
-theorem rename_identity (p : Path) (fs : Filesystem) :
-    rename p p fs = fs := by
-  induction fs with
-  | nil => rfl
-  | cons e rest ih =>
-    show (if p == path_of e then set_path p e :: rest else e :: rename p p rest) = e :: rest
-    by_cases hp : p == path_of e
-    · rw [if_pos hp]
-      have hp_eq : p = path_of e := eq_of_beq hp
-      subst hp_eq
-      rw [set_path_id]
-    · rw [if_neg hp]
-      rw [ih]
-
-/-- rename A to B followed by rename B to A is identity -/
-theorem rename_inverse (p1 p2 : Path) (fs : Filesystem) (hneq : p1 ≠ p2) (hno : noEntryAt p2 fs) :
-    rename p2 p1 (rename p1 p2 fs) = fs := by
-  induction fs with
-  | nil => rfl
-  | cons e rest ih =>
-    show rename p2 p1 (if p1 == path_of e then set_path p2 e :: rest else e :: rename p1 p2 rest) = e :: rest
-    by_cases hp1 : p1 == path_of e
-    · rw [if_pos hp1]
-      show (if p2 == path_of (set_path p2 e) then set_path p1 (set_path p2 e) :: rest else _) = e :: rest
-      rw [path_of_set_path]
-      rw [beq_self_eq_true p2]
-      rw [if_pos rfl]
-      rw [set_path_set_path]
-      have hp1_eq : p1 = path_of e := eq_of_beq hp1
-      subst hp1_eq
-      rw [set_path_id]
-    · rw [if_neg hp1]
-      show (if p2 == path_of e then _ else e :: rename p2 p1 (rename p1 p2 rest)) = e :: rest
-      have hp2_ne : p2 ≠ path_of e := by
-        intro h_contra
-        specialize hno e (List.Mem.head _)
-        cases e with
-        | File p' _ _ => exact hno h_contra
-        | Directory p' _ _ => exact hno h_contra
-        | Symlink p' _ _ => exact hno h_contra
-      have hp2_beq : (p2 == path_of e) = false := beq_false_of_ne hp2_ne
-      rw [if_neg (by rw [hp2_beq]; decide)]
-      have hno_rest : noEntryAt p2 rest := fun e' he' => hno e' (List.Mem.tail _ he')
-      rw [ih hno_rest]
-
-/-- snapshot followed by restore is identity -/
-theorem snapshot_restore_identity (fs : Filesystem) :
-    restore (snapshot fs) fs = fs := rfl
+-- AXIOM: rename_identity; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md.
+axiom rename_identity (p : Path) (fs : Filesystem) :
+  rename p p fs = fs
+
+/-- rename A to B followed by rename B to A is identity — when `p1 ≠ p2` and
+    nothing lives at `p2` (both preconditions Coq's `rename_inverse` states). -/
+-- AXIOM: rename_inverse; POSIX-semantics specification (mirrors Coq Lemma, same preconditions); §(c) per docs/proof-debt.md.
+axiom rename_inverse (p1 p2 : Path) (fs : Filesystem) :
+  p1 ≠ p2 →
+  noEntryAt p2 fs →
+  rename p2 p1 (rename p1 p2 fs) = fs
 
 /-! ## Filesystem CNO Definition -/
 
@@ -436,28 +179,32 @@ theorem fs_nop_is_cno : isFsCNO fs_nop := by
   intro fs
   rfl
 
-/-- mkdir followed by rmdir. -/
-def mkdirRmdirOp (p : Path) : FsOp :=
+/-- mkdir followed by rmdir. `noncomputable` — calls axioms `mkdir`/`rmdir`. -/
+noncomputable def mkdirRmdirOp (p : Path) : FsOp :=
   fun fs => rmdir p (mkdir p fs)
 
-/-- mkdir;rmdir is the identity on every filesystem with no directory at `p`. -/
+/-- mkdir;rmdir is the identity on every filesystem with no directory at `p`
+    (Coq `mkdir_rmdir_is_cno`, same statement). The unconditional
+    `isFsCNO (mkdirRmdirOp p)` is not provable and is false on the Coq model. -/
 theorem mkdir_rmdir_is_cno (p : Path) (fs : Filesystem) (h : noDirAt p fs) :
     mkdirRmdirOp p fs = fs := by
   unfold mkdirRmdirOp
   exact mkdir_rmdir_inverse p fs h
 
-/-- create followed by unlink. -/
-def createUnlinkOp (p : Path) : FsOp :=
+/-- create followed by unlink. `noncomputable` — wraps axioms. -/
+noncomputable def createUnlinkOp (p : Path) : FsOp :=
   fun fs => unlink p (create p fs)
 
-/-- create;unlink is the identity on every filesystem with no file at `p`. -/
+/-- create;unlink is the identity on every filesystem with no file at `p`
+    (Coq `create_unlink_is_cno`, same statement). -/
 theorem create_unlink_is_cno (p : Path) (fs : Filesystem) (h : noFileAt p fs) :
     createUnlinkOp p fs = fs := by
   unfold createUnlinkOp
   exact create_unlink_inverse p fs h
 
-/-- read followed by write. -/
-def readWriteOp (p : Path) : FsOp :=
+/-- Write the content returned by `readFile` back to `p`, leaving the filesystem
+    unchanged if `readFile` returns `none`. `noncomputable` — wraps axioms. -/
+noncomputable def readWriteOp (p : Path) : FsOp :=
   fun fs =>
     match readFile p fs with
     | some content => writeFile p content fs
@@ -472,8 +219,9 @@ theorem read_write_is_cno (p : Path) :
   | some content =>
       exact read_write_identity p fs content h
 
-/-- chmod to current permissions. -/
-def chmodNopOp (p : Path) : FsOp :=
+/-- Set permissions at `p` to those returned by `stat`, leaving the filesystem
+    unchanged if `stat` returns `none`. `noncomputable` — wraps axioms. -/
+noncomputable def chmodNopOp (p : Path) : FsOp :=
   fun fs =>
     match stat p fs with
     | some meta => chmod p meta.permissions fs
@@ -488,8 +236,8 @@ theorem chmod_nop_is_cno (p : Path) :
   | some meta =>
       exact chmod_identity p fs meta h
 
-/-- rename to same path. -/
-def renameNopOp (p : Path) : FsOp :=
+/-- rename to same path. `noncomputable` — wraps axiom. -/
+noncomputable def renameNopOp (p : Path) : FsOp :=
   fun fs => rename p p fs
 
 theorem rename_nop_is_cno (p : Path) :
@@ -519,13 +267,10 @@ theorem fs_cno_composition (op1 op2 : FsOp) :
 
 /-! ## Non-CNO Operations -/
 
-/-- mkdir alone is NOT a CNO. -/
-theorem mkdir_not_identity : ∃ (p : Path) (fs : Filesystem), mkdir p fs ≠ fs := by
-  exists ""
-  exists []
-  unfold mkdir dir_exists
-  intro h
-  contradiction
+/-- mkdir alone is NOT a CNO. Coq proves this Lemma on its concrete model
+    (`exists "" nil`); over opaque operations it has to be assumed. -/
+-- AXIOM: mkdir_not_identity; mirrors the Coq Lemma (proved on the concrete model); §(c) per docs/proof-debt.md.
+axiom mkdir_not_identity : ∃ (p : Path) (fs : Filesystem), mkdir p fs ≠ fs
 
 theorem mkdir_alone_not_cno :
     ¬ (∀ p, isFsCNO (fun fs => mkdir p fs)) := by
@@ -565,7 +310,24 @@ example (p : Path) (fs : Filesystem) (h : noFileAt p fs) :
 
 /-! ## Snapshot and Restore -/
 
-def snapshotRestoreOp : FsOp :=
+/-- Snapshot operation -/
+-- AXIOM: snapshot; opaque snapshot primitive; §(c) per docs/proof-debt.md.
+axiom snapshot : Filesystem → Filesystem
+
+/-- Restore from snapshot -/
+-- AXIOM: restore; opaque restore primitive; §(c) per docs/proof-debt.md.
+axiom restore : Filesystem → Filesystem → Filesystem
+
+/-- snapshot followed by restore is identity -/
+-- AXIOM: snapshot_restore_identity; snapshot/restore specification (mirrors Coq); §(c) per docs/proof-debt.md.
+axiom snapshot_restore_identity (fs : Filesystem) :
+  restore (snapshot fs) fs = fs
+
+-- `noncomputable` because `restore` and `snapshot` are axioms with no
+-- executable body; without this Lean 4.16 refuses to emit code for `def`.
+/-- Restore a snapshot of the input filesystem onto that same filesystem.
+    Returns the input filesystem by `snapshot_restore_identity`. -/
+noncomputable def snapshotRestoreOp : FsOp :=
   fun fs => restore (snapshot fs) fs
 
 theorem snapshot_restore_is_cno :
@@ -580,22 +342,20 @@ theorem snapshot_restore_is_cno :
 def isIdempotent (op : FsOp) : Prop :=
   ∀ fs, op (op fs) = op fs
 
-/-- mkdir is idempotent (but not CNO). -/
-theorem mkdir_idempotent (p : Path) :
-    isIdempotent (fun fs => mkdir p fs) := by
-  intro fs
-  unfold mkdir
-  by_cases h : dir_exists p fs = true
-  · rw [if_pos h, if_pos h]
-  · rw [if_neg h]
-    have h_dir : dir_exists p (FileEntry.Directory p [] default_meta :: fs) = true := by
-      show ((p == p) || dir_exists p fs) = true
-      rw [beq_self_eq_true p]
-      rfl
-    rw [if_pos h_dir]
-
-/-- The unconditional law `∀ p fs, rmdir p (mkdir p fs) = fs` is refuted by
-    `mkdir_idempotent` and `mkdir_not_identity`. -/
+/-- mkdir is idempotent (but not CNO). Coq proves this Lemma on its concrete
+    model; over opaque operations it has to be assumed. Consistent with the
+    conditional `mkdir_rmdir_inverse`: `mkdir p fs` has a directory at `p`,
+    so the inverse law does not apply to it. -/
+-- AXIOM: mkdir_idempotent; mirrors the Coq Lemma (proved on the concrete model); §(c) per docs/proof-debt.md.
+axiom mkdir_idempotent (p : Path) :
+  isIdempotent (fun fs => mkdir p fs)
+
+/-- The unconditional law `∀ p fs, rmdir p (mkdir p fs) = fs` — the former
+    statement of `mkdir_rmdir_inverse` — is refuted by `mkdir_idempotent` and
+    `mkdir_not_identity` alone: on `mkdir p fs` the second `mkdir` is a no-op,
+    so the law would force `mkdir p fs = fs`. This is the derivation that
+    made issue #125's `False` proof go through; it is now a theorem about the
+    old statement instead of a contradiction in the axioms. -/
 theorem unconditional_mkdir_rmdir_inverse_is_false :
     ¬ ∀ (p : Path) (fs : Filesystem), rmdir p (mkdir p fs) = fs := by
   intro law
@@ -605,7 +365,11 @@ theorem unconditional_mkdir_rmdir_inverse_is_false :
   rw [h2, law p fs] at h1
   exact hne h1.symm
 
-/-- 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
   obtain ⟨p, fs, h_neq⟩ := mkdir_not_identity
   exists (fun fs' => mkdir p fs')