Lean: port the Coq concrete filesystem model so the FilesystemCNO law axioms become theorems (follow-up to #125/#165)

[hyperpolymath]

Context

#165 (fix for #125) makes the Lean filesystem law axioms carry the occupancy preconditions the Coq versions state, and proves unconditional_mkdir_rmdir_inverse_is_false. What remains axiomatic in proofs/lean4/FilesystemCNO.lean after that PR is the model: mkdir, rmdir, create, unlink, rename, read, write, chmod, snapshot/restore are opaque constants and the laws about them are axioms (21 in total, 3 now with preconditions). LambdaCNO.lean keeps one axiom, y_combinator_not_identity.

The Coq side (proofs/coq/filesystem/*.v) has a concrete model where the same laws are theorems. Porting that model discharges, in one move:

• mkdir_not_identity (FilesystemCNO.lean:271)
• mkdir_idempotent (FilesystemCNO.lean:345)
• snapshot_restore_identity (FilesystemCNO.lean:320)
• the three inverse laws (mkdir_rmdir_inverse, create_unlink_inverse, rename_inverse) and the identity laws around them

The ledger rows in docs/proof-debt.adoc (dated 2026-09-22) name this as the discharge route; #70 tracks the wider "overly-cautious OWED" pattern on the Coq side and is not this issue.

Acceptance criteria

• FilesystemCNO.lean defines Filesystem as a concrete structure (e.g. a finite map from Path to entries) and the operations as functions; noDirAt/noFileAt/noEntryAt stay as the semantic predicates introduced by fix(lean): #125 — law axioms carry Coq's occupancy preconditions; axiom audit + CI job #165.
• Each of the laws listed above becomes a theorem; AxiomAudit.lean §D #print axioms for every downstream theorem lists none of them (the guards are updated to the new expected output, not deleted).
• unconditional_mkdir_rmdir_inverse_is_false still holds (it must, since the model witnesses it).
• proofs/lean4/check-core.sh stays green in the lean job; the audit guard count in the PR description is the new measured number.
• Mutant: replacing one ported theorem's proof with sorry reds #print axioms (guard shows sorryAx).
• PROOF-STATUS.adoc and docs/proof-debt.adoc axiom counts updated from the measured output.

🤖 Generated with Claude Code

[hyperpolymath]

RULING D204 (2026-09-30T14:29Z) · scope: estate · basis: owner (direct answer, selector)

NW-1 ONE filesystem-reversibility model: absolute-zero factors out an ABSTRACT CNO interface (Coq Module Type/Class over state + equivalence + step); valence-shell Require-Imports it and proves is_CNO over ITS OWN filesystem model (first real feeder import); januskey's ops refine valence-shell's model; absolute-zero FilesystemCNO.v retires or becomes a toy instance (absolute-zero#167 rescoped). Answers januskey#137's formal-home question and absolute-zero#167

surface: hyperpolymath/standards#787 (comment) · direction doc: valence-shell docs/THEORY-FEED.adoc (NW-1)