Lean FilesystemCNO and LambdaCNO each prove False; lake build reports success and CI never runs the Lean leg

[hyperpolymath]

Found while assessing CNO as a possible substrate for a claim-checking layer in invariant-path (ADR-0001). Not a request to change the design — a soundness report. Everything below is read off the committed sources.

1. proofs/lean4/FilesystemCNO.lean is inconsistent

Three axioms combine to derive False:

• :98 axiom mkdir_rmdir_inverse — stated with no precondition, where the Coq counterpart FilesystemCNO.v:353-360 carries one explicitly
• :309 axiom mkdir_idempotent
• :233 axiom mkdir_not_identity

Together these yield fs = mkdir p fs for all fs, contradicting mkdir_not_identity. The dropped precondition looks like the whole cause — the Coq side states the same lemma correctly.

2. proofs/lean4/LambdaCNO.lean is inconsistent

:264 axiom eta_equivalence (f : LambdaTerm) : BetaReduceStar (LAbs (LApp f (LVar 0))) f

Unguarded, and refuted by this repository's own Coq: LambdaCNO.v:430 proves its negation. It fails at f = LVar 5 (the shift/capture side condition is missing).

Every theorem in both libraries is therefore vacuous.

3. Why nothing goes red

• lake build succeeds — an inconsistent axiom set is well-typed, so the build cannot see it.
• .github/workflows/proofs.yml:9-11 states outright that Lean, Isabelle, Mizar and Idris are not run in CI. So the Lean leg is gated only by proofs/verify-all-provers.sh on a local machine.
• No #print axioms is ever executed. grep -rn "#print axioms" proofs/lean4/ returns one hit, in a comment (CNOBridge.lean:14). Every "Closed under the global context" claim in PROOF-STATUS.adoc is prose.

Related, lower severity

• proofs/verify-all-provers.sh:46,53 — the Isabelle and Mizar guards do not set fail=1 when the tool is absent (contrast :19), so ALL-PROVERS-GREEN prints having run four of six named provers.
• :38 — the Z3 leg checks only the exit code. z3 exits 0 on any sat/unsat, so a result inverted against its comment still passes. proofs/z3/verify.sh:35 also references cno_properties.smt2, which does not exist in the repo.
• LandauerDerivation.v:404 Axiom cno_zero_energy_dissipation_derived — the flagship thermodynamic claim (is_CNO p -> work_dissipated = 0) is an axiom despite the _derived suffix, and is absent from PROOF-STATUS.adoc's otherwise-exhaustive remainder list. Same for :343 cno_preserves_shannon_entropy.
• CNOCategory.v:20,98 — the category laws rest on Coq.Logic.ProofIrrelevance. Consistent, but not "zero project axioms" as the summary implies.

Credit where due

The Coq side is genuinely strong and is not affected by 1 or 2: OND.v (17 Qed, zero axioms) and FilesystemCNO.v (35 Qed, zero axioms) are clean, there are zero real Admitted/sorry/postulate anywhere in the corpus, and several physics files explicitly correct their own triage docs where a claimed discharge was inaccurate. The problem is specifically the Lean mirror plus the summary layer.

Suggested minimum

1. Restore the precondition on mkdir_rmdir_inverse; delete or guard eta_equivalence.
2. Add #print axioms on every Lean headline theorem and Print Assumptions on every Coq one, with the gate diffing against an expected-axioms allowlist.
3. Make Isabelle/Mizar absence a hard failure, or rename the banner to name only what actually ran.
4. Assert the expected sat/unsat per Z3 block rather than trusting the exit code.

🤖 Generated with Claude Code