Repository navigation
Lean FilesystemCNO and LambdaCNO each prove False; lake build reports success and CI never runs the Lean leg #125
Description
Activity
Owner ruling 2026-09-22 (selection UI; booked on hyperpolymath/standards#787, rows D78–D81): fix first. This issue is ordered before any other absolute-zero work in the residual-evidence-types family plan (Phase 4a). The honesty-gate items (
paths:filter,z3 … || true, skipped provers, no assumption check) are filed separately and follow it.Acceptance criteria for the fix, as ruled:
- Watched failing today: a scratch
example : False := …built from the currentFilesystemCNO.lean/LambdaCNO.leanaxioms compiles. - Green: the same example no longer type-checks;
lake buildis green;#print axiomson each headline theorem lists nosorryAxand only the intended axioms (the axioms carry the preconditions the Coq versions state, or become definitions). - Mutant: re-add one unconditional axiom; the
Falseexample compiles again. - The Lean leg runs in CI on the fix commit (today
proofs.ymlnever runs it) and the run id is cited here. CNOBridge.leanis measured in CI, not on a workstation (the Mathlib fetch returned 403 locally on 2026-09-22).
🤖 Generated with Claude Code
- Watched failing today: a scratch
Fix is up as #165 (branch
fix/125-lean-axiom-preconditions, commit 9654143).FilesystemCNO.lean: the three inverse laws now carry the occupancy preconditions the Coq versions state (noDirAt/noFileAt/noEntryAt);unconditional_mkdir_rmdir_inverse_is_falseproves the old unconditional form refutable from the remaining axioms. 21 → 21 axioms, three strengthened.LambdaCNO.lean:subst_closed_termand the restrictedeta_equivalenceare theorems;unrestricted_eta_equivalence_is_falseproves the general η claim refutable. 3 → 1 axioms.AxiomAudit.lean(96#guard_msgs) pins every remaining axiom's signature, the predicates' definitions,#print axiomsfor every theorem, and two negative controls: this issue'sexample : Falsederivation and the unrestricted η use must fail to elaborate.- CI: new
leanjob inproofs.yml, green on the PR head — run 35792229108, job 106963182842.
Mutants measured locally: deleting the
noDirAthypothesis reds the build (function expectedat consumers); weakeningnoDirAttoTruebuilds green but fails exactly one audit guard, and theFalsederivation compiles again against that tree. The audit, not the build, is what catches the second shape.🤖 Generated with Claude Code
Landed on
mainas 828399a (PR #165, merged 2026-09-22T23:07:11Z).Receipt: Proofs run 35795836824 on
main, job "Lean — core CNO (6 modules + axiom audit)" = success (https://github.com/hyperpolymath/absolute-zero/actions/runs/35795836824).proofs/lean4/AxiomAudit.leancarries the negative controls (the #125Falsederivations must now fail with the recorded error) and Section D also walks every theorem in the six modules withcollectAxiomsagainst a closed allow-list, so a newsorryAxor an unlisted axiom fails the job.For the record: the merge rule-suite (4183559643) reads
bypass— thepull_requestrule was failing on CodeRabbit's changes-requested review and thecode_scanningrule was still expecting the CodeQL results for the autofix head da9289c. Every post-merge push run onmainis green (CodeQL, Hypatia, Proofs, Rust CI, Governance, Secret Scanner, Language Policy, Mirror).🤖 Generated with Claude Code
- added a commit that references this issue
on Oct 1, 2026
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.leanis inconsistentThree axioms combine to derive
False::98axiom mkdir_rmdir_inverse— stated with no precondition, where the Coq counterpartFilesystemCNO.v:353-360carries one explicitly:309axiom mkdir_idempotent:233axiom mkdir_not_identityTogether these yield
fs = mkdir p fsfor allfs, contradictingmkdir_not_identity. The dropped precondition looks like the whole cause — the Coq side states the same lemma correctly.2.
proofs/lean4/LambdaCNO.leanis inconsistent:264axiom eta_equivalence (f : LambdaTerm) : BetaReduceStar (LAbs (LApp f (LVar 0))) fUnguarded, and refuted by this repository's own Coq:
LambdaCNO.v:430proves its negation. It fails atf = LVar 5(the shift/capture side condition is missing).Every theorem in both libraries is therefore vacuous.
3. Why nothing goes red
lake buildsucceeds — an inconsistent axiom set is well-typed, so the build cannot see it..github/workflows/proofs.yml:9-11states outright that Lean, Isabelle, Mizar and Idris are not run in CI. So the Lean leg is gated only byproofs/verify-all-provers.shon a local machine.#print axiomsis ever executed.grep -rn "#print axioms" proofs/lean4/returns one hit, in a comment (CNOBridge.lean:14). Every "Closed under the global context" claim inPROOF-STATUS.adocis prose.Related, lower severity
proofs/verify-all-provers.sh:46,53— the Isabelle and Mizar guards do not setfail=1when the tool is absent (contrast:19), soALL-PROVERS-GREENprints having run four of six named provers.:38— the Z3 leg checks only the exit code.z3exits 0 on anysat/unsat, so a result inverted against its comment still passes.proofs/z3/verify.sh:35also referencescno_properties.smt2, which does not exist in the repo.LandauerDerivation.v:404Axiom cno_zero_energy_dissipation_derived— the flagship thermodynamic claim (is_CNO p -> work_dissipated = 0) is an axiom despite the_derivedsuffix, and is absent fromPROOF-STATUS.adoc's otherwise-exhaustive remainder list. Same for:343 cno_preserves_shannon_entropy.CNOCategory.v:20,98— the category laws rest onCoq.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(17Qed, zero axioms) andFilesystemCNO.v(35Qed, zero axioms) are clean, there are zero realAdmitted/sorry/postulateanywhere 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
mkdir_rmdir_inverse; delete or guardeta_equivalence.#print axiomson every Lean headline theorem andPrint Assumptionson every Coq one, with the gate diffing against an expected-axioms allowlist.sat/unsatper Z3 block rather than trusting the exit code.🤖 Generated with Claude Code