From 96541439595fffe2acd6700635e528c74e74bb09 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 22 Sep 2026 23:19:56 +0100
Subject: [PATCH 1/3] =?UTF-8?q?fix(lean):=20#125=20=E2=80=94=20law=20axiom?=
 =?UTF-8?q?s=20carry=20Coq's=20occupancy=20preconditions;=20axiom=20audit?=
 =?UTF-8?q?=20+=20CI=20job?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The Lean mirror of FilesystemCNO transcribed mkdir_rmdir_inverse,
create_unlink_inverse and rename_inverse WITHOUT the preconditions the
Coq lemmas state, so together with mkdir_idempotent and
mkdir_not_identity the axioms derived False (issue #125). LambdaCNO's
eta_equivalence axiom was likewise the unrestricted statement, which
eta_general_claim_is_false already refutes.

FilesystemCNO.lean
- noDirAt / noFileAt / noEntryAt occupancy predicates (verbatim from
  FilesystemCNO.v); the three inverse laws now take them as hypotheses
  (rename_inverse also takes p1 ≠ p2). Axiom count stays 21 = 21; no
  axiom was added, three were strengthened.
- unconditional_mkdir_rmdir_inverse_is_false records the #125
  derivation as a theorem: the old law is refutable from the remaining
  axioms, so it can never be reintroduced silently.

LambdaCNO.lean
- subst_closed_term: axiom → theorem (immediate from Closed).
- eta_equivalence: axiom → theorem, restricted to noLambda body = true
  exactly as Coq's no_lambda guard; unrestricted_eta_equivalence_is_false
  records why the restriction is necessary. Axiom count 3 → 1
  (y_combinator_not_identity remains, §(c)).

AxiomAudit.lean (new, 96 #guard_msgs)
- pins the signature of every axiom in the six Mathlib-free modules,
  prints the three predicates, keeps the #125 derivation and the
  unrestricted η use as NEGATIVE controls that must fail to elaborate,
  and runs #print axioms over every theorem (no sorryAx anywhere).

check-core.sh + proofs.yml job `lean` + `just verify-lean-core`
- builds CNO, OND, CNOCategory, CNOBridge, FilesystemCNO, LambdaCNO
  with the pinned toolchain (elan v4.2.4 sha256-verified in CI) and
  runs the audit. Mathlib-dependent modules stay in
  verify-all-provers.sh.

Measured locally (lean 4.16.0):
- positive control: 6 modules compiled, 96 guards matched, rc=0.
- mutant M1 (drop the noDirAt hypothesis): build red at
  FilesystemCNO.lean:191/300 "function expected".
- mutant M2 (noDirAt := True): six modules build, the audit fails on
  the `#print noDirAt` guard, and the #125 `example : False` compiles
  again — so only the audit catches a weakened predicate.
- the pre-fix `example : False` no longer elaborates on this tree.

Docs: proof-debt ledger rows refreshed (line numbers, two Lambda axioms
discharged, the mkdir_idempotent plan corrected — it does NOT follow
from the inverse family, that combination IS #125), COOKBOOK Coq
example carries the precondition, AUDIT.adoc row, PROOF-STATUS.

Fixes #125.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57
---
 .github/workflows/proofs.yml    |  32 +-
 .gitignore                      |   1 +
 AUDIT.adoc                      |  16 +
 Justfile                        |   5 +
 PROOF-STATUS.adoc               |  21 +
 docs/COOKBOOK.adoc              |   6 +-
 docs/proof-debt.adoc            |  71 ++--
 proofs/lean4/AxiomAudit.lean    | 655 ++++++++++++++++++++++++++++++++
 proofs/lean4/FilesystemCNO.lean | 123 ++++--
 proofs/lean4/LambdaCNO.lean     |  71 +++-
 proofs/lean4/check-core.sh      |  46 +++
 proofs/lean4/lakefile.lean      |   7 +
 12 files changed, 973 insertions(+), 81 deletions(-)
 create mode 100644 proofs/lean4/AxiomAudit.lean
 create mode 100755 proofs/lean4/check-core.sh

diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml
index c42da48..6e2b3d4 100644
--- a/.github/workflows/proofs.yml
+++ b/.github/workflows/proofs.yml
@@ -9,9 +9,15 @@
 # OND), and Z3 (CNO + OND bounded instances). Each is an INDEPENDENT job, so one
 # flaking never blocks the others.
 #
-# The heavy provers (Lean + multi-GB Mathlib, Isabelle ~1.2 GB, Mizar i386 + MML,
-# Idris 2 from source) are NOT run here — they are covered by the local/container
-# gate `proofs/verify-all-provers.sh` (ALL-PROVERS-GREEN). See PROOF-STATUS.adoc.
+# The Mathlib-free Lean core (CNO, OND, CNOCategory, CNOBridge, FilesystemCNO,
+# LambdaCNO) is built here too, with the toolchain pinned in
+# proofs/lean4/lean-toolchain, and proofs/lean4/AxiomAudit.lean pins the
+# signature of every axiom and the axiom list of every theorem (issue #125).
+#
+# The heavy provers (Lean + multi-GB Mathlib for QuantumCNO/StatMech, Isabelle
+# ~1.2 GB, Mizar i386 + MML, Idris 2 from source) are NOT run here — they are
+# covered by the local/container gate `proofs/verify-all-provers.sh`
+# (ALL-PROVERS-GREEN). See PROOF-STATUS.adoc.
 name: Proofs
 
 on:
@@ -94,3 +100,23 @@ jobs:
           sh proofs/z3/verify.sh || true
           z3 proofs/z3/ond/OND_checks.smt2
           echo "✓ Z3: OND bounded instances checked"
+
+  lean:
+    name: Lean — core CNO (6 modules + axiom audit)
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@v7.0.1
+      - name: Install elan v4.2.4 (sha256-verified) and the pinned toolchain
+        # elan is fetched as a release tarball and checksum-verified rather than
+        # via a third-party action, so the repo's Actions allow-list is not in
+        # play. The toolchain itself comes from proofs/lean4/lean-toolchain.
+        run: |
+          curl -fsSL --retry 3 -o elan.tgz \
+            https://github.com/leanprover/elan/releases/download/v4.2.4/elan-x86_64-unknown-linux-gnu.tar.gz
+          echo "42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63  elan.tgz" | sha256sum -c -
+          tar -xzf elan.tgz
+          ./elan-init -y --no-modify-path --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Build the six Mathlib-free modules and run the axiom audit
+        run: bash proofs/lean4/check-core.sh
diff --git a/.gitignore b/.gitignore
index 252dbf3..bfcb9f0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -81,6 +81,7 @@ htmlcov/
 # Crash recovery artifacts
 ai-cli-crash-capture/
 proofs/lean4/.lake/
+proofs/lean4/_out/
 
 # Coq build outputs
 *.vo
diff --git a/AUDIT.adoc b/AUDIT.adoc
index 61f0668..a6364f1 100644
--- a/AUDIT.adoc
+++ b/AUDIT.adoc
@@ -25,6 +25,22 @@ PR #100 — see Resolved Audit Items below._
 |===
 |ID |Date resolved |Description |Resolution commit
 
+|AUDIT-2026-09-22-A
+|2026-09-22
+|*Unsoundness finding — Lean mirror (issue #125).* `proofs/lean4/FilesystemCNO.lean`
+ stated the inverse laws `mkdir_rmdir_inverse`, `create_unlink_inverse` and
+ `rename_inverse` WITHOUT the occupancy preconditions of the Coq lemmas they
+ mirror; together with `mkdir_idempotent` and `mkdir_not_identity` the axioms
+ proved `False`. `proofs/lean4/LambdaCNO.lean` still carried the unrestricted
+ `eta_equivalence` axiom that AUDIT-2026-07-06-A had already found false in Coq.
+ Fix: the preconditions were added verbatim (`noDirAt`, `noFileAt`, `noEntryAt`),
+ `eta_equivalence` became the proved `noLambda`-guarded theorem, both old
+ statements are refuted in-file (`unconditional_mkdir_rmdir_inverse_is_false`,
+ `unrestricted_eta_equivalence_is_false`), and `proofs/lean4/AxiomAudit.lean`
+ (run by the new CI job `lean` via `proofs/lean4/check-core.sh`) pins every axiom
+ signature and every theorem's `#print axioms` list with `#guard_msgs`.
+|Fix PR for #125 (2026-09-22)
+
 |AUDIT-2026-07-06-A
 |2026-07-06
 |*Unsoundness finding — 3 axioms.* During the two-pillar discharge, three
diff --git a/Justfile b/Justfile
index 0c5c302..6c96198 100644
--- a/Justfile
+++ b/Justfile
@@ -99,6 +99,11 @@ verify-lean:
     @echo "Verifying Lean 4 proofs..."
     cd proofs/lean4 && lake build
 
+# Verify the Mathlib-free Lean core + axiom audit (what the CI `lean` job runs; no Mathlib needed)
+verify-lean-core:
+    @echo "Verifying Lean 4 core (6 modules + AxiomAudit.lean)..."
+    bash proofs/lean4/check-core.sh
+
 # Verify Agda proofs
 verify-agda: build-agda
     @echo "✓ Agda proofs verified"
diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 04be5d4..3ae3963 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -160,6 +160,27 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`.
 * Toolchain `leanprover/lean4:v4.16.0` with Mathlib `@ v4.16.0`; `lake exe cache get`
   + `lake build` → **build completed successfully**. Covers the CNO libraries and the
   new `OND` library (`proofs/lean4/OND.lean`, core-Lean only, zero `sorry`).
+* **Mathlib-free core is CI-gated (2026-09-22):** `proofs/lean4/check-core.sh` (job
+  `lean` in `.github/workflows/proofs.yml`; toolchain from `lean-toolchain`, elan
+  fetched as a checksum-verified tarball, zero third-party actions) compiles `CNO`,
+  `OND`, `CNOCategory`, `CNOBridge`, `FilesystemCNO`, `LambdaCNO` with plain `lean`
+  and runs `proofs/lean4/AxiomAudit.lean`: 96 `#guard_msgs` pinning every axiom
+  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.
+* **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`).
 
 == Z3 — VERIFIED (this environment)
 
diff --git a/docs/COOKBOOK.adoc b/docs/COOKBOOK.adoc
index 8a75168..b3b1421 100644
--- a/docs/COOKBOOK.adoc
+++ b/docs/COOKBOOK.adoc
@@ -530,8 +530,12 @@ Valence Shell operations can be proven as CNOs:
 
 [source,coq]
 ----
+(* Precondition: no directory already at [path] — without it the law is false
+   (repeat mkdir is idempotent), see proofs/coq/filesystem/FilesystemCNO.v and
+   absolute-zero#125. *)
 Theorem mkdir_rmdir_is_cno :
-  forall (path : Path),
+  forall (path : Path) (fs : Filesystem),
+    no_dir_at path fs ->
     mkdir path ;; rmdir path ≡ Nop.
 ----
 
diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc
index 086065c..05d1527 100644
--- a/docs/proof-debt.adoc
+++ b/docs/proof-debt.adoc
@@ -44,22 +44,24 @@ https://github.com/hyperpolymath/absolute-zero/issues/27[#27].
 === Phase 2a triage — Lean Lambda cluster (2026-05-27)
 
 Per-cluster Lean triage rolling out 2026-05-27 in cluster-sized PRs.
-First cluster: `+proofs/lean4/LambdaCNO.lean+` (3 axioms).
+First cluster: `+proofs/lean4/LambdaCNO.lean+` (3 axioms at triage time; 1 since 2026-09-22 — see the rows).
 
 [width="99%",cols=">14%,26%,28%,32%",options="header",]
 |===
 |Line |Identifier |Disposition |Justification
-|183 |`+subst_closed_term+` |§(d) DEBT |Standard metatheoretic property
-of lambda calculus; provable by induction on `+t+` once the
-substitution-on-closed-terms lemma is mechanised.
+|184 |`+subst_closed_term+` |THEOREM |Discharged 2026-09-22 (#125 fix PR):
+immediate from the semantic `+Closed+` definition.
 
-|232 |`+y_combinator_not_identity+` |§(c) AXIOM |Non-termination claim
+|237 |`+y_combinator_not_identity+` |§(c) AXIOM |Non-termination claim
 about Y combinator; requires step-indexed semantics or coinduction (same
 justification as Coq `+y_not_cno+`).
 
-|258 |`+eta_equivalence+` |§(c) AXIOM |η-equivalence is not derivable
-under β-only reduction (same justification as Coq `+eta_equivalence+` at
-LambdaCNO.v:376).
+|308 |`+eta_equivalence+` |THEOREM (restricted) |The unrestricted statement
+is *false* (counterexample `+f = LVar 5+`, exactly as Coq found at
+`+LambdaCNO.v+`; recorded in-file as
+`+unrestricted_eta_equivalence_is_false+`). Since 2026-09-22 (#125) it is the
+proved theorem for `+noLambda body = true+`, mirroring Coq's `+no_lambda+`
+guard. The axiom is gone.
 |===
 
 The two §(c) entries are annotated inline with `+-- AXIOM:+` leading
@@ -98,15 +100,23 @@ in the model.
 
 ==== POSIX semantics specifications (§(c) AXIOM — mirror Coq, 6)
 
+
+*2026-09-22 (issue #125):* the three `+_inverse+` laws had been transcribed
+*without* the occupancy preconditions of the Coq lemmas they mirror; together
+with `+mkdir_idempotent+` and `+mkdir_not_identity+` the axioms proved
+`+False+`. They now carry `+noDirAt+` / `+noFileAt+` / `+noEntryAt+`
+(`+FilesystemCNO.lean:60–77+`, verbatim from `+FilesystemCNO.v+`), and
+`+proofs/lean4/AxiomAudit.lean+` (CI job `+lean+`) pins every signature.
+
 [cols=">,,",options="header",]
 |===
 |Line |Identifier |Disposition
-|98 |`+mkdir_rmdir_inverse+` |§(c) AXIOM (mirrors Coq)
-|104 |`+create_unlink_inverse+` |§(c) AXIOM (mirrors Coq)
-|109 |`+read_write_identity+` |§(c) AXIOM (mirrors Coq)
-|115 |`+chmod_identity+` |§(c) AXIOM (mirrors Coq)
-|121 |`+rename_identity+` |§(c) AXIOM (mirrors Coq)
-|126 |`+rename_inverse+` |§(c) AXIOM (mirrors Coq)
+|127 |`+mkdir_rmdir_inverse+` |§(c) AXIOM (mirrors Coq, *with* its precondition `+noDirAt p fs+` — #125)
+|134 |`+create_unlink_inverse+` |§(c) AXIOM (mirrors Coq, *with* its precondition `+noFileAt p fs+` — #125)
+|140 |`+read_write_identity+` |§(c) AXIOM (mirrors Coq)
+|146 |`+chmod_identity+` |§(c) AXIOM (mirrors Coq)
+|152 |`+rename_identity+` |§(c) AXIOM (mirrors Coq)
+|158 |`+rename_inverse+` |§(c) AXIOM (mirrors Coq, *with* its preconditions `+p1 ≠ p2+` and `+noEntryAt p2 fs+` — #125)
 |===
 
 ==== Snapshot primitives (§(c) AXIOM — opaque ops, 2)
@@ -127,15 +137,17 @@ discharge PR — see §(d) DEBT below.
 [width="100%",cols=">17%,32%,35%,16%",options="header",]
 |===
 |Line |Identifier |Disposition |Plan
-|233 |`+mkdir_not_identity+` |§(d) DEBT |Existence proof; exhibit one
+|271 |`+mkdir_not_identity+` |§(d) DEBT |Existence proof; exhibit one
 concrete `+fs+` lacking the path.
 
-|288 |`+snapshot_restore_identity+` |§(d) DEBT |Composite theorem;
+|320 |`+snapshot_restore_identity+` |§(d) DEBT |Composite theorem;
 derivable from `+snapshot+`/`+restore+` once a concrete snapshot model
 lands.
 
-|309 |`+mkdir_idempotent+` |§(d) DEBT |Follows from
-`+mkdir_rmdir_inverse+` family with stronger repeat-mkdir semantics.
+|345 |`+mkdir_idempotent+` |§(d) DEBT |Does *not* follow from the
+`+mkdir_rmdir_inverse+` family — that combination derives `+False+` unless
+the inverse law carries its occupancy precondition (issue #125, fixed
+2026-09-22). Discharge = port the concrete Coq model.
 |===
 
 All 18 §(c) entries above are annotated inline with `+-- AXIOM:+`
@@ -401,29 +413,28 @@ than discharging it. Should follow from
 
 ==== Lean — provable, awaiting proof
 
-* `+proofs/lean4/LambdaCNO.lean:183+` — `+subst_closed_term+`
-** *Owner*: @hyperpolymath
-** *Plan*: discharge by induction on `+t : LambdaTerm+`; closed-term
-invariant carries through `+LVar+`, `+LAbs+`, `+LApp+` cases. Sibling to
-Coq’s `+subst+` lemmas in `+proofs/coq/lambda/LambdaCNO.v+`.
-** *Deadline*: INDEFINITE (no proof-PR scheduled yet — provable; awaits
-Lean-side discharge push).
-* `+proofs/lean4/FilesystemCNO.lean:233+` — `+mkdir_not_identity+`
+* `+proofs/lean4/LambdaCNO.lean:184+` — `+subst_closed_term+` — *DISCHARGED
+2026-09-22* (fix PR for #125): now a `+theorem+`; it is immediate from the
+semantic definition of `+Closed+` (`+h n s (Nat.zero_le n)+`).
+* `+proofs/lean4/FilesystemCNO.lean:271+` — `+mkdir_not_identity+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: existence proof; exhibit one concrete `+fs+` lacking the
 path. Mirrors Coq site at `+FilesystemCNO.v:300+`.
 ** *Deadline*: INDEFINITE.
-* `+proofs/lean4/FilesystemCNO.lean:288+` —
+* `+proofs/lean4/FilesystemCNO.lean:320+` —
 `+snapshot_restore_identity+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: composite theorem; derivable from `+snapshot+`/`+restore+`
 primitives once a concrete snapshot model is in place. Mirrors Coq site
 at `+FilesystemCNO.v:453+`.
 ** *Deadline*: INDEFINITE.
-* `+proofs/lean4/FilesystemCNO.lean:309+` — `+mkdir_idempotent+`
+* `+proofs/lean4/FilesystemCNO.lean:345+` — `+mkdir_idempotent+`
 ** *Owner*: @hyperpolymath
-** *Plan*: follows from `+mkdir_rmdir_inverse+` + stronger repeat-mkdir
-semantics. Mirrors Coq site at `+FilesystemCNO.v:421+`.
+** *Plan*: does *not* follow from `+mkdir_rmdir_inverse+`: issue #125 showed
+that with an unconditional inverse law, idempotence plus
+`+mkdir_not_identity+` derives `+False+` (now recorded in-file as
+`+unconditional_mkdir_rmdir_inverse_is_false+`). Discharge = port the
+concrete Coq list model, where `+FilesystemCNO.v:421+` proves it.
 ** *Deadline*: INDEFINITE.
 * `+proofs/lean4/QuantumCNO.lean:134+` — `+X_gate_not_identity+`
 ** *Owner*: @hyperpolymath
diff --git a/proofs/lean4/AxiomAudit.lean b/proofs/lean4/AxiomAudit.lean
new file mode 100644
index 0000000..c5655fc
--- /dev/null
+++ b/proofs/lean4/AxiomAudit.lean
@@ -0,0 +1,655 @@
+import CNO
+import OND
+import CNOCategory
+import CNOBridge
+import FilesystemCNO
+import LambdaCNO
+
+/-!
+# Axiom audit for the Mathlib-free Lean core (issue #125)
+
+Every `#guard_msgs` below pins the EXACT output Lean produces, so this file is a
+regression test on the axiom surface of the six core modules:
+
+* Section A — the signature of every declared axiom, with the preconditions that
+  issue #125 showed to be necessary (`noDirAt`, `noFileAt`, `noEntryAt`,
+  `noLambda`). Dropping a precondition changes the printed signature and turns
+  this file red.
+* Section B — the occupancy predicates, printed in full, so they cannot be
+  weakened to `True` silently.
+* Section C — the #125 derivations of `False`, verbatim, as NEGATIVE controls:
+  each must fail to typecheck with exactly the recorded error.
+* Section D — `#print axioms` for every theorem in the six modules: the closed
+  list of axioms each theorem rests on. `sorryAx` never appears.
+
+Run with `proofs/lean4/check-core.sh` (CI job `lean` in
+`.github/workflows/proofs.yml`). Whitespace is compared laxly so a change in the
+pretty-printer's line width cannot cause a spurious failure; any change in the
+TEXT of a signature or axiom list does.
+-/
+
+/-! ## Section A — axiom signatures -/
+section
+open FilesystemCNO
+
+/--
+info: mkdir : Path → Filesystem → Filesystem
+-/
+#guard_msgs (whitespace := lax) in #check @mkdir
+
+/--
+info: rmdir : Path → Filesystem → Filesystem
+-/
+#guard_msgs (whitespace := lax) in #check @rmdir
+
+/--
+info: create : Path → Filesystem → Filesystem
+-/
+#guard_msgs (whitespace := lax) in #check @create
+
+/--
+info: unlink : Path → Filesystem → Filesystem
+-/
+#guard_msgs (whitespace := lax) in #check @unlink
+
+/--
+info: readFile : Path → Filesystem → Option FileContent
+-/
+#guard_msgs (whitespace := lax) in #check @readFile
+
+/--
+info: writeFile : Path → FileContent → Filesystem → Filesystem
+-/
+#guard_msgs (whitespace := lax) in #check @writeFile
+
+/--
+info: stat : Path → Filesystem → Option FileMetadata
+-/
+#guard_msgs (whitespace := lax) in #check @stat
+
+/--
+info: chmod : Path → PermSet → Filesystem → Filesystem
+-/
+#guard_msgs (whitespace := lax) in #check @chmod
+
+/--
+info: chown : Path → Nat → Filesystem → Filesystem
+-/
+#guard_msgs (whitespace := lax) in #check @chown
+
+/--
+info: rename : Path → Path → Filesystem → Filesystem
+-/
+#guard_msgs (whitespace := lax) in #check @rename
+
+/--
+info: mkdir_rmdir_inverse : ∀ (p : Path) (fs : Filesystem), noDirAt p fs → rmdir p (mkdir p fs) = fs
+-/
+#guard_msgs (whitespace := lax) in #check @mkdir_rmdir_inverse
+
+/--
+info: create_unlink_inverse : ∀ (p : Path) (fs : Filesystem), noFileAt p fs → unlink p (create p fs) = fs
+-/
+#guard_msgs (whitespace := lax) in #check @create_unlink_inverse
+
+/--
+info: read_write_identity : ∀ (p : Path) (fs : Filesystem) (content : FileContent),
+  readFile p fs = some content → writeFile p content fs = fs
+-/
+#guard_msgs (whitespace := lax) in #check @read_write_identity
+
+/--
+info: chmod_identity : ∀ (p : Path) (fs : Filesystem) (meta : FileMetadata),
+  stat p fs = some meta → chmod p meta.permissions fs = fs
+-/
+#guard_msgs (whitespace := lax) in #check @chmod_identity
+
+/--
+info: rename_identity : ∀ (p : Path) (fs : Filesystem), rename p p fs = fs
+-/
+#guard_msgs (whitespace := lax) in #check @rename_identity
+
+/--
+info: rename_inverse : ∀ (p1 p2 : Path) (fs : Filesystem), p1 ≠ p2 → noEntryAt p2 fs → rename p2 p1 (rename p1 p2 fs) = fs
+-/
+#guard_msgs (whitespace := lax) in #check @rename_inverse
+
+/--
+info: mkdir_not_identity : ∃ p fs, mkdir p fs ≠ fs
+-/
+#guard_msgs (whitespace := lax) in #check @mkdir_not_identity
+
+/--
+info: snapshot : Filesystem → Filesystem
+-/
+#guard_msgs (whitespace := lax) in #check @snapshot
+
+/--
+info: restore : Filesystem → Filesystem → Filesystem
+-/
+#guard_msgs (whitespace := lax) in #check @restore
+
+/--
+info: snapshot_restore_identity : ∀ (fs : Filesystem), restore (snapshot fs) fs = fs
+-/
+#guard_msgs (whitespace := lax) in #check @snapshot_restore_identity
+
+/--
+info: mkdir_idempotent : ∀ (p : Path), isIdempotent fun fs => mkdir p fs
+-/
+#guard_msgs (whitespace := lax) in #check @mkdir_idempotent
+end
+
+section
+open LambdaCNO
+
+/--
+info: y_combinator_not_identity : ¬BetaReduceStar (y_combinator.LApp lambda_id) lambda_id
+-/
+#guard_msgs (whitespace := lax) in #check @y_combinator_not_identity
+
+/--
+info: noLambda : LambdaTerm → Bool
+-/
+#guard_msgs (whitespace := lax) in #check @noLambda
+end
+
+/-! ## Section B — the occupancy predicates, in full -/
+section
+open FilesystemCNO
+
+/--
+info: def FilesystemCNO.noDirAt : Path → Filesystem → Prop :=
+fun p fs =>
+  ∀ (e : FileEntry),
+    e ∈ fs →
+      match e with
+      | FileEntry.Directory p' a a_1 => p ≠ p'
+      | x => True
+-/
+#guard_msgs (whitespace := lax) in #print noDirAt
+
+/--
+info: def FilesystemCNO.noFileAt : Path → Filesystem → Prop :=
+fun p fs =>
+  ∀ (e : FileEntry),
+    e ∈ fs →
+      match e with
+      | FileEntry.File p' a a_1 => p ≠ p'
+      | x => True
+-/
+#guard_msgs (whitespace := lax) in #print noFileAt
+
+/--
+info: def FilesystemCNO.noEntryAt : Path → Filesystem → Prop :=
+fun p fs =>
+  ∀ (e : FileEntry),
+    e ∈ fs →
+      match e with
+      | FileEntry.File p' a a_1 => p ≠ p'
+      | FileEntry.Directory p' a a_1 => p ≠ p'
+      | FileEntry.Symlink p' a a_1 => p ≠ p'
+-/
+#guard_msgs (whitespace := lax) in #print noEntryAt
+end
+
+/-! ## Section C — the #125 derivations must NOT typecheck (negative controls)
+
+Each `example` below is the pre-fix use of a law axiom, i.e. the step of the
+#125 `False` proof that the missing precondition made possible. The recorded
+error is the precondition being demanded. If any of these ever elaborates,
+the axiom has lost its precondition. -/
+section
+open FilesystemCNO
+
+/--
+error: type mismatch
+  mkdir_rmdir_inverse p fs
+has type
+  noDirAt p fs → rmdir p (mkdir p fs) = fs : Prop
+but is expected to have type
+  rmdir p (mkdir p fs) = fs : Prop
+-/
+#guard_msgs (whitespace := lax) in
+example (p : Path) (fs : Filesystem) : rmdir p (mkdir p fs) = fs :=
+  mkdir_rmdir_inverse p fs
+
+/--
+error: type mismatch
+  create_unlink_inverse p fs
+has type
+  noFileAt p fs → unlink p (create p fs) = fs : Prop
+but is expected to have type
+  unlink p (create p fs) = fs : Prop
+-/
+#guard_msgs (whitespace := lax) in
+example (p : Path) (fs : Filesystem) : unlink p (create p fs) = fs :=
+  create_unlink_inverse p fs
+
+/--
+error: type mismatch
+  rename_inverse p1 p2 fs h
+has type
+  noEntryAt p2 fs → rename p2 p1 (rename p1 p2 fs) = fs : Prop
+but is expected to have type
+  rename p2 p1 (rename p1 p2 fs) = fs : Prop
+-/
+#guard_msgs (whitespace := lax) in
+example (p1 p2 : Path) (fs : Filesystem) (h : p1 ≠ p2) :
+    rename p2 p1 (rename p1 p2 fs) = fs :=
+  rename_inverse p1 p2 fs h
+
+/--
+error: type mismatch
+  mkdir_rmdir_inverse p (mkdir p fs)
+has type
+  noDirAt p (mkdir p fs) → rmdir p (mkdir p (mkdir p fs)) = mkdir p fs : Prop
+but is expected to have type
+  rmdir p (mkdir p (mkdir p fs)) = mkdir p fs : Prop
+---
+error: unsolved goals
+case intro.intro
+p : Path
+fs : Filesystem
+hne : mkdir p fs ≠ fs
+h1 : rmdir p (mkdir p fs) = mkdir p fs
+h2 : mkdir p (mkdir p fs) = mkdir p fs
+⊢ noDirAt p fs
+-/
+#guard_msgs (whitespace := lax) in
+example : False := by
+  obtain ⟨p, fs, hne⟩ := mkdir_not_identity
+  have h1 : rmdir p (mkdir p (mkdir p fs)) = mkdir p fs := mkdir_rmdir_inverse p (mkdir p fs)
+  have h2 : mkdir p (mkdir p fs) = mkdir p fs := mkdir_idempotent p fs
+  rw [h2, mkdir_rmdir_inverse p fs] at h1
+  exact hne h1.symm
+end
+
+section
+open LambdaCNO LambdaCNO.LambdaTerm
+
+/--
+error: type mismatch
+  eta_equivalence f
+has type
+  noLambda f = true → BetaReduceStar (f.LAbs.LApp (LVar 0)).LAbs f.LAbs : Prop
+but is expected to have type
+  BetaReduceStar (f.LApp (LVar 0)).LAbs f : Prop
+-/
+#guard_msgs (whitespace := lax) in
+example (f : LambdaTerm) : BetaReduceStar (LAbs (LApp f (LVar 0))) f :=
+  eta_equivalence f
+
+/--
+error: application type mismatch
+  eta_general_claim_is_false (eta_equivalence (LVar 5))
+argument
+  eta_equivalence (LVar 5)
+has type
+  noLambda (LVar 5) = true → BetaReduceStar ((LVar 5).LAbs.LApp (LVar 0)).LAbs (LVar 5).LAbs : Prop
+but is expected to have type
+  BetaReduceStar ((LVar 5).LApp (LVar 0)).LAbs (LVar 5) : Prop
+-/
+#guard_msgs (whitespace := lax) in
+example : False :=
+  eta_general_claim_is_false (eta_equivalence (LVar 5))
+end
+
+/-! ## Section D — the axiom list of every theorem in the six modules -/
+
+section
+open CNO
+
+/--
+info: 'CNO.terminates_always' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms terminates_always
+
+/--
+info: 'CNO.empty_is_cno' depends on axioms: [propext, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in #print axioms empty_is_cno
+
+/--
+info: 'CNO.nop_preserves_most_state' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms nop_preserves_most_state
+
+/--
+info: 'CNO.halt_is_cno' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms halt_is_cno
+
+/--
+info: 'CNO.cno_terminates' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms cno_terminates
+
+/--
+info: 'CNO.cno_preserves_state' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms cno_preserves_state
+
+/--
+info: 'CNO.cno_pure' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms cno_pure
+
+/--
+info: 'CNO.cno_reversible' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms cno_reversible
+
+/--
+info: 'CNO.eval_seqComp' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms eval_seqComp
+
+/--
+info: 'CNO.state_eq_trans' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms state_eq_trans
+
+/--
+info: 'CNO.pure_trans' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms pure_trans
+
+/--
+info: 'CNO.cno_composition' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms cno_composition
+
+/--
+info: 'CNO.crazy_op_zero' depends on axioms: [propext]
+-/
+#guard_msgs (whitespace := lax) in #print axioms crazy_op_zero
+
+/--
+info: 'CNO.triple_rotation_identity' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms triple_rotation_identity
+
+/--
+info: 'CNO.loadStore_preserves_memory' depends on axioms: [propext, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in #print axioms loadStore_preserves_memory
+
+/--
+info: 'CNO.nop_minimal_complexity' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms nop_minimal_complexity
+
+/--
+info: 'CNO.halt_minimal_complexity' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms halt_minimal_complexity
+
+/--
+info: 'CNO.absoluteZero_is_cno' depends on axioms: [propext, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in #print axioms absoluteZero_is_cno
+end
+
+section
+open OND
+
+/--
+info: 'OND.OND2_skip_is_OND' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms OND2_skip_is_OND
+
+/--
+info: 'OND.leaky_cno_is_null' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms leaky_cno_is_null
+
+/--
+info: 'OND.leaky_cno_not_OND_time' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms leaky_cno_not_OND_time
+
+/--
+info: 'OND.writer_is_OND_all' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms writer_is_OND_all
+
+/--
+info: 'OND.writer_not_null' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms writer_not_null
+
+/--
+info: 'OND.OND3_cno_ond_independent' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms OND3_cno_ond_independent
+
+/--
+info: 'OND.OND4_ct_select_is_OND_all' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms OND4_ct_select_is_OND_all
+
+/--
+info: 'OND.p_op_is_OND_all' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms p_op_is_OND_all
+
+/--
+info: 'OND.q_op_is_OND_all' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms q_op_is_OND_all
+
+/--
+info: 'OND.OND5_composition_leaks' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms OND5_composition_leaks
+
+/--
+info: 'OND.OND5_non_composition' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms OND5_non_composition
+end
+
+section
+open CNOCategory
+
+/--
+info: 'CNOCategory.cno_categorical_equiv' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms cno_categorical_equiv
+
+/--
+info: 'CNOCategory.functor_preserves_cno' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms functor_preserves_cno
+
+/--
+info: 'CNOCategory.cno_model_independent' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms cno_model_independent
+
+/--
+info: 'CNOCategory.yoneda_cno' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms yoneda_cno
+end
+
+section
+open CNOBridge
+
+/--
+info: 'CNOBridge.reversible_iff_exists_reverses' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms reversible_iff_exists_reverses
+
+/--
+info: 'CNOBridge.reverses_seq_computes_identity' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms reverses_seq_computes_identity
+
+/--
+info: 'CNOBridge.cnoEquiv_seq_empty_of_reverses' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms cnoEquiv_seq_empty_of_reverses
+
+/--
+info: 'CNOBridge.reversible_bridge_forward' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms reversible_bridge_forward
+
+/--
+info: 'CNOBridge.reversible_bridge_backward' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms reversible_bridge_backward
+
+/--
+info: 'CNOBridge.reverses_iff_cnoEquiv_seq_empty' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms reverses_iff_cnoEquiv_seq_empty
+end
+
+section
+open FilesystemCNO
+
+/--
+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' 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' 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' 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' 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' depends on axioms: [FilesystemCNO.rename, FilesystemCNO.rename_identity]
+-/
+#guard_msgs (whitespace := lax) in #print axioms rename_nop_is_cno
+
+/--
+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' depends on axioms: [FilesystemCNO.mkdir, FilesystemCNO.mkdir_not_identity]
+-/
+#guard_msgs (whitespace := lax) in #print axioms mkdir_alone_not_cno
+
+/--
+info: 'FilesystemCNO.valence_reversible_pair_is_cno' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms valence_reversible_pair_is_cno
+
+/--
+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' 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
+
+section
+open LambdaCNO
+
+/--
+info: 'LambdaCNO.lambda_id_is_cno_weak' depends on axioms: [propext, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in #print axioms lambda_id_is_cno_weak
+
+/--
+info: 'LambdaCNO.lambda_id_normal_form' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms lambda_id_normal_form
+
+/--
+info: 'LambdaCNO.lambda_id_is_cno' depends on axioms: [propext, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in #print axioms lambda_id_is_cno
+
+/--
+info: 'LambdaCNO.BetaReduceStar_app_right' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms BetaReduceStar_app_right
+
+/--
+info: 'LambdaCNO.BetaReduceStar_app_left' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms BetaReduceStar_app_left
+
+/--
+info: 'LambdaCNO.BetaReduceStar_trans' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms BetaReduceStar_trans
+
+/--
+info: 'LambdaCNO.subst_closed_term' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms subst_closed_term
+
+/--
+info: 'LambdaCNO.lambda_cno_composition' depends on axioms: [propext, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in #print axioms lambda_cno_composition
+
+/--
+info: 'LambdaCNO.y_not_cno' depends on axioms: [LambdaCNO.y_combinator_not_identity]
+-/
+#guard_msgs (whitespace := lax) in #print axioms y_not_cno
+
+/--
+info: 'LambdaCNO.eta_general_claim_is_false' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms eta_general_claim_is_false
+
+/--
+info: 'LambdaCNO.unrestricted_eta_equivalence_is_false' does not depend on any axioms
+-/
+#guard_msgs (whitespace := lax) in #print axioms unrestricted_eta_equivalence_is_false
+
+/--
+info: 'LambdaCNO.subst_noLambda_self' depends on axioms: [propext, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in #print axioms subst_noLambda_self
+
+/--
+info: 'LambdaCNO.eta_equivalence' depends on axioms: [propext, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in #print axioms eta_equivalence
+
+/--
+info: 'LambdaCNO.eta_expanded_id_is_cno' depends on axioms: [propext, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in #print axioms eta_expanded_id_is_cno
+end
diff --git a/proofs/lean4/FilesystemCNO.lean b/proofs/lean4/FilesystemCNO.lean
index 122c700..21464d0 100644
--- a/proofs/lean4/FilesystemCNO.lean
+++ b/proofs/lean4/FilesystemCNO.lean
@@ -49,6 +49,32 @@ inductive FileEntry where
 /-- Filesystem state. `abbrev` so List instances propagate. -/
 abbrev Filesystem : Type := List FileEntry
 
+/-! ## Occupancy predicates
+
+These are the preconditions of the Coq lemmas in
+`proofs/coq/filesystem/FilesystemCNO.v`, mirrored verbatim. The laws below
+hold on the concrete Coq model ONLY under them; stating the laws without
+them let `False` be derived (issue #125). -/
+
+/-- No directory entry at `p`. Precondition of Coq's `mkdir_rmdir_inverse`. -/
+def noDirAt (p : Path) (fs : Filesystem) : Prop :=
+  ∀ e, e ∈ fs → match e with
+    | FileEntry.Directory p' _ _ => p ≠ p'
+    | _ => True
+
+/-- No file entry at `p`. Precondition of Coq's `create_unlink_inverse`. -/
+def noFileAt (p : Path) (fs : Filesystem) : Prop :=
+  ∀ e, e ∈ fs → match e with
+    | FileEntry.File p' _ _ => p ≠ p'
+    | _ => True
+
+/-- No entry of any kind at `p`. Precondition of Coq's `rename_inverse`. -/
+def noEntryAt (p : Path) (fs : Filesystem) : Prop :=
+  ∀ e, e ∈ fs → match e with
+    | FileEntry.File p' _ _ => p ≠ p'
+    | FileEntry.Directory p' _ _ => p ≠ p'
+    | FileEntry.Symlink p' _ _ => p ≠ p'
+
 /-! ## Filesystem Operations -/
 
 /-- Create directory -/
@@ -93,15 +119,20 @@ axiom rename : Path → Path → Filesystem → Filesystem
 
 /-! ## Operation Axioms -/
 
-/-- mkdir followed by rmdir is identity -/
--- AXIOM: mkdir_rmdir_inverse; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md.
+/-- 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) :
-  -- Precondition: p doesn't exist
+  noDirAt p fs →
   rmdir p (mkdir p fs) = fs
 
-/-- create followed by unlink is identity -/
--- AXIOM: create_unlink_inverse; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md.
+/-- 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 -/
@@ -121,10 +152,12 @@ axiom chmod_identity (p : Path) (fs : Filesystem) (meta : FileMetadata) :
 axiom rename_identity (p : Path) (fs : Filesystem) :
   rename p p fs = fs
 
-/-- rename A to B followed by rename B to A is identity -/
--- AXIOM: rename_inverse; POSIX-semantics specification (mirrors Coq); §(c) per docs/proof-debt.md.
+/-- 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 -/
@@ -150,21 +183,24 @@ theorem fs_nop_is_cno : isFsCNO fs_nop := by
 noncomputable def mkdirRmdirOp (p : Path) : FsOp :=
   fun fs => rmdir p (mkdir p fs)
 
-theorem mkdir_rmdir_is_cno (p : Path) :
-    isFsCNO (mkdirRmdirOp p) := by
-  unfold isFsCNO mkdirRmdirOp
-  intro fs
-  exact mkdir_rmdir_inverse p fs
+/-- 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. `noncomputable` — wraps axioms. -/
 noncomputable def createUnlinkOp (p : Path) : FsOp :=
   fun fs => unlink p (create p fs)
 
-theorem create_unlink_is_cno (p : Path) :
-    isFsCNO (createUnlinkOp p) := by
-  unfold isFsCNO createUnlinkOp
-  intro fs
-  exact create_unlink_inverse p fs
+/-- 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. `noncomputable` — wraps axioms. -/
 noncomputable def readWriteOp (p : Path) : FsOp :=
@@ -229,7 +265,9 @@ theorem fs_cno_composition (op1 op2 : FsOp) :
 
 /-! ## Non-CNO Operations -/
 
-/-- mkdir alone is NOT a CNO -/
+/-- 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 :
@@ -256,23 +294,17 @@ theorem valence_reversible_pair_is_cno (op op_inv : FsOp) :
   intro fs
   exact h fs
 
-/-- Example: mkdir/rmdir pair from Valence Shell -/
-example (p : Path) :
-    valenceReversible
-      (fun fs => mkdir p fs)
-      (fun fs => rmdir p fs) := by
-  unfold valenceReversible
-  intro fs
-  exact mkdir_rmdir_inverse p fs
-
-/-- Example: create/unlink pair from Valence Shell -/
-example (p : Path) :
-    valenceReversible
-      (fun fs => create p fs)
-      (fun fs => unlink p fs) := by
-  unfold valenceReversible
-  intro fs
-  exact create_unlink_inverse p fs
+/-- Example: mkdir/rmdir pair from Valence Shell (Coq `valence_mkdir_rmdir`):
+    reversible on every filesystem with no directory at `p`. -/
+example (p : Path) (fs : Filesystem) (h : noDirAt p fs) :
+    rmdir p (mkdir p fs) = fs :=
+  mkdir_rmdir_inverse p fs h
+
+/-- Example: create/unlink pair from Valence Shell (Coq `valence_create_unlink`):
+    reversible on every filesystem with no file at `p`. -/
+example (p : Path) (fs : Filesystem) (h : noFileAt p fs) :
+    unlink p (create p fs) = fs :=
+  create_unlink_inverse p fs h
 
 /-! ## Snapshot and Restore -/
 
@@ -305,10 +337,29 @@ theorem snapshot_restore_is_cno :
 def isIdempotent (op : FsOp) : Prop :=
   ∀ fs, op (op fs) = op fs
 
-/-- mkdir is idempotent (but not CNO) -/
+/-- 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
+  obtain ⟨p, fs, hne⟩ := mkdir_not_identity
+  have h1 : rmdir p (mkdir p (mkdir p fs)) = mkdir p fs := law p (mkdir p fs)
+  have h2 : mkdir p (mkdir p fs) = mkdir p fs := mkdir_idempotent p fs
+  rw [h2, law p fs] at h1
+  exact hne h1.symm
+
 /-- 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.
diff --git a/proofs/lean4/LambdaCNO.lean b/proofs/lean4/LambdaCNO.lean
index 066c61e..69b734b 100644
--- a/proofs/lean4/LambdaCNO.lean
+++ b/proofs/lean4/LambdaCNO.lean
@@ -177,11 +177,13 @@ theorem BetaReduceStar_trans (a b c : LambdaTerm)
 def Closed (t : LambdaTerm) (n : Nat) : Prop :=
   ∀ m s, m ≥ n → subst m s t = t
 
-/-- Substitution on closed terms is identity.
-    This is a standard metatheoretic property of lambda calculus:
-    replacing a variable that doesn't occur free has no effect. -/
-axiom subst_closed_term (t s : LambdaTerm) (n : Nat) :
-  Closed t 0 → subst n s t = t
+/-- Substitution on closed terms is identity. Under this file's semantic
+    `Closed` (substitution-invariance at every level ≥ n) this is immediate;
+    Coq proves the structural `closed_at` form as `subst_closed_at`.
+    Formerly an axiom (#125). -/
+theorem subst_closed_term (t s : LambdaTerm) (n : Nat)
+    (h : Closed t 0) : subst n s t = t :=
+  h n s (Nat.zero_le n)
 
 /-! ## Composition Theorem -/
 
@@ -257,12 +259,59 @@ example : BetaReduceStar (LApp church_zero church_zero) (LAbs (LVar 0)) := by
 
 /-! ## Eta Equivalence -/
 
-/-- Eta reduction: (λx. f x) ≡ f -/
--- AXIOM: eta_equivalence; η-equivalence is not derivable under β-only reduction —
---   requires an extra reduction rule or extensional equality.
---   §(c) NECESSARY AXIOM per docs/proof-debt.md (Lean Lambda triage 2026-05-27).
-axiom eta_equivalence (f : LambdaTerm) :
-  BetaReduceStar (LAbs (LApp f (LVar 0))) f
+/-- The unrestricted claim `BetaReduceStar (LAbs (LApp f (LVar 0))) f` for
+    ANY `f` is FALSE under this file's `BetaReduce`/`subst`: at `f = LVar 5`
+    the term `LAbs (LApp (LVar 5) (LVar 0))` contains no redex, so it is its
+    own unique normal form and reduces only to itself. The former
+    `axiom eta_equivalence` stated exactly that claim and therefore derived
+    `False` (#125). Mirrors Coq's `eta_general_claim_is_false`. -/
+theorem eta_general_claim_is_false :
+    ¬ BetaReduceStar (LAbs (LApp (LVar 5) (LVar 0))) (LVar 5) := by
+  intro h
+  cases h
+  rename_i t2 hs hr
+  cases hs
+  rename_i body' hb
+  cases hb <;> rename_i hv <;> cases hv
+
+/-- The former statement of `eta_equivalence` — for ANY `f` — is refuted. -/
+theorem unrestricted_eta_equivalence_is_false :
+    ¬ ∀ f : LambdaTerm, BetaReduceStar (LAbs (LApp f (LVar 0))) f :=
+  fun h => eta_general_claim_is_false (h (LVar 5))
+
+/-- `true` when the term contains no abstraction (a "flat" body).
+    Mirrors Coq's `no_lambda`. -/
+def noLambda : LambdaTerm → Bool
+  | LVar _ => true
+  | LApp t1 t2 => noLambda t1 && noLambda t2
+  | LAbs _ => false
+
+/-- Substituting `LVar n` for variable `n` in an abstraction-free body is the
+    identity (Coq `subst_no_lambda_self`). -/
+theorem subst_noLambda_self (body : LambdaTerm) (n : Nat)
+    (h : noLambda body = true) : subst n (LVar n) body = body := by
+  induction body generalizing n with
+  | LVar m =>
+    by_cases hnm : n = m
+    · subst hnm; simp [subst]
+    · simp [subst, hnm]
+  | LApp t1 t2 ih1 ih2 =>
+    simp only [noLambda, Bool.and_eq_true] at h
+    simp only [subst, ih1 n h.1, ih2 n h.2]
+  | LAbs _ _ =>
+    simp [noLambda] at h
+
+/-- Restricted eta-equivalence: `(λx. (λy.body) x) →* (λy.body)` for every
+    abstraction-free `body`. Under this file's non-shifting `subst` this is
+    the honest, provable core of eta; the unrestricted form is refuted above.
+    Mirrors Coq's `eta_equivalence` (Theorem, Qed). -/
+theorem eta_equivalence (body : LambdaTerm) (h : noLambda body = true) :
+    BetaReduceStar (LAbs (LApp (LAbs body) (LVar 0))) (LAbs body) := by
+  apply BetaReduceStar.beta_step
+  · apply BetaReduce.beta_abs
+    apply BetaReduce.beta_app
+  · rw [subst_noLambda_self body 0 h]
+    apply BetaReduceStar.beta_refl
 
 /-- Eta-expanded identity is a CNO: for arguments in normal form,
     it terminates and acts as identity -/
diff --git a/proofs/lean4/check-core.sh b/proofs/lean4/check-core.sh
new file mode 100755
index 0000000..50fa87c
--- /dev/null
+++ b/proofs/lean4/check-core.sh
@@ -0,0 +1,46 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Build the six Mathlib-free Lean 4 modules with the toolchain pinned in
+# `lean-toolchain` and run the axiom audit (AxiomAudit.lean). This is the
+# CI-side Lean gate (job `lean` in .github/workflows/proofs.yml); the two
+# Mathlib-dependent modules (QuantumCNO, StatMech) stay on `lake build` in the
+# local/container gate `proofs/verify-all-provers.sh`.
+#
+# Exit status is non-zero if any module fails to compile or if any
+# `#guard_msgs` in AxiomAudit.lean does not match Lean's actual output.
+set -euo pipefail
+
+here="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+cd "$here"
+
+toolchain="$(tr -d '[:space:]' < lean-toolchain)"
+if [ -z "$toolchain" ]; then
+  echo "::error::lean-toolchain is empty" >&2
+  exit 1
+fi
+# `elan toolchain install` exits non-zero when the toolchain is already present
+# (measured: "error: 'leanprover/lean4:v4.16.0' is already installed"), so
+# install only when it is absent; `elan run` below fails loudly if it is unusable.
+if ! elan toolchain list | awk '{print $1}' | grep -qxF -- "$toolchain"; then
+  elan toolchain install "$toolchain"
+fi
+echo "toolchain: $toolchain"
+elan run "$toolchain" lean --version
+
+out="${LEAN_CORE_OUT:-$here/_out}"
+rm -rf "$out"
+mkdir -p "$out"
+
+# Dependency order: CNOCategory and CNOBridge import CNO. The rest are leaves.
+modules=(CNO OND CNOCategory CNOBridge FilesystemCNO LambdaCNO)
+for m in "${modules[@]}"; do
+  echo "== lean $m"
+  LEAN_PATH="$out" elan run "$toolchain" lean --root=. -o "$out/$m.olean" "$m.lean"
+done
+
+echo "== axiom audit: every #guard_msgs in AxiomAudit.lean must match"
+guards="$(grep -c '^#guard_msgs' AxiomAudit.lean)"
+LEAN_PATH="$out" elan run "$toolchain" lean --root=. AxiomAudit.lean
+echo "✓ Lean core: ${#modules[@]} modules compiled, $guards guards matched (toolchain $toolchain)"
diff --git a/proofs/lean4/lakefile.lean b/proofs/lean4/lakefile.lean
index 4a91343..c2ced4d 100644
--- a/proofs/lean4/lakefile.lean
+++ b/proofs/lean4/lakefile.lean
@@ -38,3 +38,10 @@ lean_lib OND
 -- unverified in that environment and must not gate the standard `lake build`.
 -- Build/verify explicitly with `lake build CNOBridge`.
 lean_lib CNOBridge
+
+-- Axiom audit for the Mathlib-free core (issue #125): `#guard_msgs` on every axiom
+-- signature and every theorem's `#print axioms`. Run via `proofs/lean4/check-core.sh`
+-- (the CI `lean` job) — plain `lean`, no Mathlib. Not a default target so a
+-- Mathlib-less `lake build` of the other libs is unaffected; `lake build AxiomAudit`
+-- also works.
+lean_lib AxiomAudit

From 7a4970db7669ac4827ce8e8fba91297ba13f73c7 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 22 Sep 2026 23:28:35 +0100
Subject: [PATCH 2/3] docs(ledger): cite Coq y_not_cno by file:line so the
 trusted-base gate keys on it; audit row names PR #165
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The governance Trusted-base reduction gate went red on the first push
(1/78 undocumented: proofs/coq/lambda/LambdaCNO.v:399, Axiom y_not_cno).
The Coq axiom was never annotated inline; on main it counted as documented
only because one unrelated §(d) sentence ("port from Coq's subst lemmas in
proofs/coq/lambda/LambdaCNO.v") contained the file path, and the gate's
third arm accepts any mention of the path. Marking subst_closed_term as
discharged removed that sentence. The ledger row for
y_combinator_not_identity already names y_not_cno as its justification;
it now cites it by file:line, which is the gate's precise arm and survives
future prose edits.

Reproduced locally with standards main's check-trusted-base.sh: origin/main
80/80 documented, branch before this commit 77/78, after 78/78.

AUDIT.adoc: the 2026-09-22 row now names PR #165.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57
---
 AUDIT.adoc           | 2 +-
 docs/proof-debt.adoc | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/AUDIT.adoc b/AUDIT.adoc
index a6364f1..a44d0d6 100644
--- a/AUDIT.adoc
+++ b/AUDIT.adoc
@@ -39,7 +39,7 @@ PR #100 — see Resolved Audit Items below._
  `unrestricted_eta_equivalence_is_false`), and `proofs/lean4/AxiomAudit.lean`
  (run by the new CI job `lean` via `proofs/lean4/check-core.sh`) pins every axiom
  signature and every theorem's `#print axioms` list with `#guard_msgs`.
-|Fix PR for #125 (2026-09-22)
+|PR #165 for #125 (2026-09-22)
 
 |AUDIT-2026-07-06-A
 |2026-07-06
diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc
index 05d1527..64ec10e 100644
--- a/docs/proof-debt.adoc
+++ b/docs/proof-debt.adoc
@@ -54,7 +54,7 @@ immediate from the semantic `+Closed+` definition.
 
 |237 |`+y_combinator_not_identity+` |§(c) AXIOM |Non-termination claim
 about Y combinator; requires step-indexed semantics or coinduction (same
-justification as Coq `+y_not_cno+`).
+justification as Coq `+y_not_cno+`, `+proofs/coq/lambda/LambdaCNO.v:399+`).
 
 |308 |`+eta_equivalence+` |THEOREM (restricted) |The unrestricted statement
 is *false* (counterexample `+f = LVar 5+`, exactly as Coq found at

From da9289c89e71d8b0cc7d5673ef3935d45e3f6c25 Mon Sep 17 00:00:00 2001
From: "coderabbitai[bot]"
 <136622811+coderabbitai[bot]@users.noreply.github.com>
Date: Tue, 22 Sep 2026 23:04:28 +0000
Subject: [PATCH 3/3] fix(lean): audit all core theorem axioms and preserve
 custom output directories

Correct the cookbook's mkdir/rmdir inverse example.
---
 docs/COOKBOOK.adoc           |  2 +-
 proofs/lean4/AxiomAudit.lean | 43 ++++++++++++++++++++++++++++++++++--
 proofs/lean4/check-core.sh   |  4 +++-
 3 files changed, 45 insertions(+), 4 deletions(-)

diff --git a/docs/COOKBOOK.adoc b/docs/COOKBOOK.adoc
index b3b1421..4d95661 100644
--- a/docs/COOKBOOK.adoc
+++ b/docs/COOKBOOK.adoc
@@ -536,7 +536,7 @@ Valence Shell operations can be proven as CNOs:
 Theorem mkdir_rmdir_is_cno :
   forall (path : Path) (fs : Filesystem),
     no_dir_at path fs ->
-    mkdir path ;; rmdir path ≡ Nop.
+    rmdir path (mkdir path fs) = fs.
 ----
 
 == Troubleshooting
diff --git a/proofs/lean4/AxiomAudit.lean b/proofs/lean4/AxiomAudit.lean
index c5655fc..d4c4929 100644
--- a/proofs/lean4/AxiomAudit.lean
+++ b/proofs/lean4/AxiomAudit.lean
@@ -1,3 +1,4 @@
+import Lean
 import CNO
 import OND
 import CNOCategory
@@ -19,8 +20,9 @@ regression test on the axiom surface of the six core modules:
   weakened to `True` silently.
 * Section C — the #125 derivations of `False`, verbatim, as NEGATIVE controls:
   each must fail to typecheck with exactly the recorded error.
-* Section D — `#print axioms` for every theorem in the six modules: the closed
-  list of axioms each theorem rests on. `sorryAx` never appears.
+* Section D — pinned `#print axioms` output for named theorems, followed by an
+  environment-wide check of every theorem in the six modules (including private
+  declarations). Only the recorded axioms are allowed; `sorryAx` never appears.
 
 Run with `proofs/lean4/check-core.sh` (CI job `lean` in
 `.github/workflows/proofs.yml`). Whitespace is compared laxly so a change in the
@@ -653,3 +655,40 @@ info: 'LambdaCNO.eta_expanded_id_is_cno' depends on axioms: [propext, Quot.sound
 -/
 #guard_msgs (whitespace := lax) in #print axioms eta_expanded_id_is_cno
 end
+
+open Lean Elab Command
+
+run_cmd do
+  let env ← getEnv
+  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
+  for moduleName in modules do
+    let some moduleIdx := env.getModuleIdx? moduleName
+      | throwError "axiom audit: missing module {moduleName}"
+    let theorems := env.constants.toList.filterMap fun (name, info) =>
+      if info.isTheorem && env.getModuleIdxFor? name == some moduleIdx then
+        some name
+      else
+        none
+    if theorems.isEmpty then
+      throwError "axiom audit: no theorems found in {moduleName}"
+    for name in theorems.toArray.qsort Name.lt do
+      let axioms ← collectAxioms name
+      for axiomName in axioms do
+        unless allowed.contains axiomName do
+          throwError "axiom audit: {name} depends on unexpected axiom {axiomName}"
+      logInfo m!"axiom audit: {name} depends on {axioms.qsort Name.lt |>.toList}"
+      checked := checked + 1
+  logInfo m!"axiom audit: checked {checked} theorems in {modules.size} modules"
diff --git a/proofs/lean4/check-core.sh b/proofs/lean4/check-core.sh
index 50fa87c..aadc875 100755
--- a/proofs/lean4/check-core.sh
+++ b/proofs/lean4/check-core.sh
@@ -30,7 +30,9 @@ echo "toolchain: $toolchain"
 elan run "$toolchain" lean --version
 
 out="${LEAN_CORE_OUT:-$here/_out}"
-rm -rf "$out"
+if [ "$out" = "$here/_out" ]; then
+  rm -rf -- "$out"
+fi
 mkdir -p "$out"
 
 # Dependency order: CNOCategory and CNOBridge import CNO. The rest are leaves.