Skip to content

Commit 9654143

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
fix(lean): #125 — law axioms carry Coq's occupancy preconditions; axiom audit + CI job
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
1 parent 3c8796a commit 9654143

12 files changed

Lines changed: 973 additions & 81 deletions

File tree

‎.github/workflows/proofs.yml‎

Lines changed: 29 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,15 @@
99
# OND), and Z3 (CNO + OND bounded instances). Each is an INDEPENDENT job, so one
1010
# flaking never blocks the others.
1111
#
12-
# The heavy provers (Lean + multi-GB Mathlib, Isabelle ~1.2 GB, Mizar i386 + MML,
13-
# Idris 2 from source) are NOT run here — they are covered by the local/container
14-
# gate `proofs/verify-all-provers.sh` (ALL-PROVERS-GREEN). See PROOF-STATUS.adoc.
12+
# The Mathlib-free Lean core (CNO, OND, CNOCategory, CNOBridge, FilesystemCNO,
13+
# LambdaCNO) is built here too, with the toolchain pinned in
14+
# proofs/lean4/lean-toolchain, and proofs/lean4/AxiomAudit.lean pins the
15+
# signature of every axiom and the axiom list of every theorem (issue #125).
16+
#
17+
# The heavy provers (Lean + multi-GB Mathlib for QuantumCNO/StatMech, Isabelle
18+
# ~1.2 GB, Mizar i386 + MML, Idris 2 from source) are NOT run here — they are
19+
# covered by the local/container gate `proofs/verify-all-provers.sh`
20+
# (ALL-PROVERS-GREEN). See PROOF-STATUS.adoc.
1521
name: Proofs
1622

1723
on:
@@ -94,3 +100,23 @@ jobs:
94100
sh proofs/z3/verify.sh || true
95101
z3 proofs/z3/ond/OND_checks.smt2
96102
echo "✓ Z3: OND bounded instances checked"
103+
104+
lean:
105+
name: Lean — core CNO (6 modules + axiom audit)
106+
runs-on: ubuntu-24.04
107+
timeout-minutes: 20
108+
steps:
109+
- uses: actions/checkout@v7.0.1
110+
- name: Install elan v4.2.4 (sha256-verified) and the pinned toolchain
111+
# elan is fetched as a release tarball and checksum-verified rather than
112+
# via a third-party action, so the repo's Actions allow-list is not in
113+
# play. The toolchain itself comes from proofs/lean4/lean-toolchain.
114+
run: |
115+
curl -fsSL --retry 3 -o elan.tgz \
116+
https://github.com/leanprover/elan/releases/download/v4.2.4/elan-x86_64-unknown-linux-gnu.tar.gz
117+
echo "42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63 elan.tgz" | sha256sum -c -
118+
tar -xzf elan.tgz
119+
./elan-init -y --no-modify-path --default-toolchain none
120+
echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
121+
- name: Build the six Mathlib-free modules and run the axiom audit
122+
run: bash proofs/lean4/check-core.sh

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,7 @@ htmlcov/
8181
# Crash recovery artifacts
8282
ai-cli-crash-capture/
8383
proofs/lean4/.lake/
84+
proofs/lean4/_out/
8485

8586
# Coq build outputs
8687
*.vo

‎AUDIT.adoc‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,22 @@ PR #100 — see Resolved Audit Items below._
2525
|===
2626
|ID |Date resolved |Description |Resolution commit
2727

28+
|AUDIT-2026-09-22-A
29+
|2026-09-22
30+
|*Unsoundness finding — Lean mirror (issue #125).* `proofs/lean4/FilesystemCNO.lean`
31+
stated the inverse laws `mkdir_rmdir_inverse`, `create_unlink_inverse` and
32+
`rename_inverse` WITHOUT the occupancy preconditions of the Coq lemmas they
33+
mirror; together with `mkdir_idempotent` and `mkdir_not_identity` the axioms
34+
proved `False`. `proofs/lean4/LambdaCNO.lean` still carried the unrestricted
35+
`eta_equivalence` axiom that AUDIT-2026-07-06-A had already found false in Coq.
36+
Fix: the preconditions were added verbatim (`noDirAt`, `noFileAt`, `noEntryAt`),
37+
`eta_equivalence` became the proved `noLambda`-guarded theorem, both old
38+
statements are refuted in-file (`unconditional_mkdir_rmdir_inverse_is_false`,
39+
`unrestricted_eta_equivalence_is_false`), and `proofs/lean4/AxiomAudit.lean`
40+
(run by the new CI job `lean` via `proofs/lean4/check-core.sh`) pins every axiom
41+
signature and every theorem's `#print axioms` list with `#guard_msgs`.
42+
|Fix PR for #125 (2026-09-22)
43+
2844
|AUDIT-2026-07-06-A
2945
|2026-07-06
3046
|*Unsoundness finding — 3 axioms.* During the two-pillar discharge, three

‎Justfile‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -99,6 +99,11 @@ verify-lean:
9999
@echo "Verifying Lean 4 proofs..."
100100
cd proofs/lean4 && lake build
101101

102+
# Verify the Mathlib-free Lean core + axiom audit (what the CI `lean` job runs; no Mathlib needed)
103+
verify-lean-core:
104+
@echo "Verifying Lean 4 core (6 modules + AxiomAudit.lean)..."
105+
bash proofs/lean4/check-core.sh
106+
102107
# Verify Agda proofs
103108
verify-agda: build-agda
104109
@echo "✓ Agda proofs verified"

‎PROOF-STATUS.adoc‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -160,6 +160,27 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`.
160160
* Toolchain `leanprover/lean4:v4.16.0` with Mathlib `@ v4.16.0`; `lake exe cache get`
161161
+ `lake build` → **build completed successfully**. Covers the CNO libraries and the
162162
new `OND` library (`proofs/lean4/OND.lean`, core-Lean only, zero `sorry`).
163+
* **Mathlib-free core is CI-gated (2026-09-22):** `proofs/lean4/check-core.sh` (job
164+
`lean` in `.github/workflows/proofs.yml`; toolchain from `lean-toolchain`, elan
165+
fetched as a checksum-verified tarball, zero third-party actions) compiles `CNO`,
166+
`OND`, `CNOCategory`, `CNOBridge`, `FilesystemCNO`, `LambdaCNO` with plain `lean`
167+
and runs `proofs/lean4/AxiomAudit.lean`: 96 `#guard_msgs` pinning every axiom
168+
signature, the three occupancy predicates in full, the #125 derivations as
169+
negative controls, and `#print axioms` for every theorem (no `sorryAx` anywhere).
170+
`just verify-lean-core` runs the same script locally.
171+
* **Issue #125 fixed — the Lean axioms no longer derive `False`:**
172+
`FilesystemCNO.lean` stated `mkdir_rmdir_inverse`, `create_unlink_inverse` and
173+
`rename_inverse` without the occupancy preconditions of the Coq lemmas they mirror;
174+
with `mkdir_idempotent` and `mkdir_not_identity` that proved `False`. They now
175+
carry `noDirAt` / `noFileAt` / `noEntryAt`, mirrored verbatim from
176+
`proofs/coq/filesystem/FilesystemCNO.v`, and the unconditional statement is refuted
177+
in-file (`unconditional_mkdir_rmdir_inverse_is_false`). `LambdaCNO.lean` carried the
178+
unrestricted `eta_equivalence` axiom (false as stated, the same `LVar 5`
179+
counterexample the Coq side documents above); it is now the proved
180+
`noLambda`-guarded theorem, `subst_closed_term` is proved, and the unrestricted
181+
claim is refuted (`unrestricted_eta_equivalence_is_false`). Lean axiom count:
182+
`FilesystemCNO` 21 → 21 (same names, three strengthened), `LambdaCNO` 3 → 1
183+
(`y_combinator_not_identity`, the Lean twin of Coq's class-A `y_not_cno`).
163184

164185
== Z3 — VERIFIED (this environment)
165186

‎docs/COOKBOOK.adoc‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -530,8 +530,12 @@ Valence Shell operations can be proven as CNOs:
530530

531531
[source,coq]
532532
----
533+
(* Precondition: no directory already at [path] — without it the law is false
534+
(repeat mkdir is idempotent), see proofs/coq/filesystem/FilesystemCNO.v and
535+
absolute-zero#125. *)
533536
Theorem mkdir_rmdir_is_cno :
534-
forall (path : Path),
537+
forall (path : Path) (fs : Filesystem),
538+
no_dir_at path fs ->
535539
mkdir path ;; rmdir path ≡ Nop.
536540
----
537541

‎docs/proof-debt.adoc‎

Lines changed: 41 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -44,22 +44,24 @@ https://github.com/hyperpolymath/absolute-zero/issues/27[#27].
4444
=== Phase 2a triage — Lean Lambda cluster (2026-05-27)
4545

4646
Per-cluster Lean triage rolling out 2026-05-27 in cluster-sized PRs.
47-
First cluster: `+proofs/lean4/LambdaCNO.lean+` (3 axioms).
47+
First cluster: `+proofs/lean4/LambdaCNO.lean+` (3 axioms at triage time; 1 since 2026-09-22 — see the rows).
4848

4949
[width="99%",cols=">14%,26%,28%,32%",options="header",]
5050
|===
5151
|Line |Identifier |Disposition |Justification
52-
|183 |`+subst_closed_term+` |§(d) DEBT |Standard metatheoretic property
53-
of lambda calculus; provable by induction on `+t+` once the
54-
substitution-on-closed-terms lemma is mechanised.
52+
|184 |`+subst_closed_term+` |THEOREM |Discharged 2026-09-22 (#125 fix PR):
53+
immediate from the semantic `+Closed+` definition.
5554

56-
|232 |`+y_combinator_not_identity+` |§(c) AXIOM |Non-termination claim
55+
|237 |`+y_combinator_not_identity+` |§(c) AXIOM |Non-termination claim
5756
about Y combinator; requires step-indexed semantics or coinduction (same
5857
justification as Coq `+y_not_cno+`).
5958

60-
|258 |`+eta_equivalence+` |§(c) AXIOM |η-equivalence is not derivable
61-
under β-only reduction (same justification as Coq `+eta_equivalence+` at
62-
LambdaCNO.v:376).
59+
|308 |`+eta_equivalence+` |THEOREM (restricted) |The unrestricted statement
60+
is *false* (counterexample `+f = LVar 5+`, exactly as Coq found at
61+
`+LambdaCNO.v+`; recorded in-file as
62+
`+unrestricted_eta_equivalence_is_false+`). Since 2026-09-22 (#125) it is the
63+
proved theorem for `+noLambda body = true+`, mirroring Coq's `+no_lambda+`
64+
guard. The axiom is gone.
6365
|===
6466

6567
The two §(c) entries are annotated inline with `+-- AXIOM:+` leading
@@ -98,15 +100,23 @@ in the model.
98100

99101
==== POSIX semantics specifications (§(c) AXIOM — mirror Coq, 6)
100102

103+
104+
*2026-09-22 (issue #125):* the three `+_inverse+` laws had been transcribed
105+
*without* the occupancy preconditions of the Coq lemmas they mirror; together
106+
with `+mkdir_idempotent+` and `+mkdir_not_identity+` the axioms proved
107+
`+False+`. They now carry `+noDirAt+` / `+noFileAt+` / `+noEntryAt+`
108+
(`+FilesystemCNO.lean:60–77+`, verbatim from `+FilesystemCNO.v+`), and
109+
`+proofs/lean4/AxiomAudit.lean+` (CI job `+lean+`) pins every signature.
110+
101111
[cols=">,,",options="header",]
102112
|===
103113
|Line |Identifier |Disposition
104-
|98 |`+mkdir_rmdir_inverse+` |§(c) AXIOM (mirrors Coq)
105-
|104 |`+create_unlink_inverse+` |§(c) AXIOM (mirrors Coq)
106-
|109 |`+read_write_identity+` |§(c) AXIOM (mirrors Coq)
107-
|115 |`+chmod_identity+` |§(c) AXIOM (mirrors Coq)
108-
|121 |`+rename_identity+` |§(c) AXIOM (mirrors Coq)
109-
|126 |`+rename_inverse+` |§(c) AXIOM (mirrors Coq)
114+
|127 |`+mkdir_rmdir_inverse+` |§(c) AXIOM (mirrors Coq, *with* its precondition `+noDirAt p fs+` — #125)
115+
|134 |`+create_unlink_inverse+` |§(c) AXIOM (mirrors Coq, *with* its precondition `+noFileAt p fs+` — #125)
116+
|140 |`+read_write_identity+` |§(c) AXIOM (mirrors Coq)
117+
|146 |`+chmod_identity+` |§(c) AXIOM (mirrors Coq)
118+
|152 |`+rename_identity+` |§(c) AXIOM (mirrors Coq)
119+
|158 |`+rename_inverse+` |§(c) AXIOM (mirrors Coq, *with* its preconditions `+p1 ≠ p2+` and `+noEntryAt p2 fs+` — #125)
110120
|===
111121

112122
==== Snapshot primitives (§(c) AXIOM — opaque ops, 2)
@@ -127,15 +137,17 @@ discharge PR — see §(d) DEBT below.
127137
[width="100%",cols=">17%,32%,35%,16%",options="header",]
128138
|===
129139
|Line |Identifier |Disposition |Plan
130-
|233 |`+mkdir_not_identity+` |§(d) DEBT |Existence proof; exhibit one
140+
|271 |`+mkdir_not_identity+` |§(d) DEBT |Existence proof; exhibit one
131141
concrete `+fs+` lacking the path.
132142

133-
|288 |`+snapshot_restore_identity+` |§(d) DEBT |Composite theorem;
143+
|320 |`+snapshot_restore_identity+` |§(d) DEBT |Composite theorem;
134144
derivable from `+snapshot+`/`+restore+` once a concrete snapshot model
135145
lands.
136146

137-
|309 |`+mkdir_idempotent+` |§(d) DEBT |Follows from
138-
`+mkdir_rmdir_inverse+` family with stronger repeat-mkdir semantics.
147+
|345 |`+mkdir_idempotent+` |§(d) DEBT |Does *not* follow from the
148+
`+mkdir_rmdir_inverse+` family — that combination derives `+False+` unless
149+
the inverse law carries its occupancy precondition (issue #125, fixed
150+
2026-09-22). Discharge = port the concrete Coq model.
139151
|===
140152

141153
All 18 §(c) entries above are annotated inline with `+-- AXIOM:+`
@@ -401,29 +413,28 @@ than discharging it. Should follow from
401413

402414
==== Lean — provable, awaiting proof
403415

404-
* `+proofs/lean4/LambdaCNO.lean:183+` — `+subst_closed_term+`
405-
** *Owner*: @hyperpolymath
406-
** *Plan*: discharge by induction on `+t : LambdaTerm+`; closed-term
407-
invariant carries through `+LVar+`, `+LAbs+`, `+LApp+` cases. Sibling to
408-
Coq’s `+subst+` lemmas in `+proofs/coq/lambda/LambdaCNO.v+`.
409-
** *Deadline*: INDEFINITE (no proof-PR scheduled yet — provable; awaits
410-
Lean-side discharge push).
411-
* `+proofs/lean4/FilesystemCNO.lean:233+` — `+mkdir_not_identity+`
416+
* `+proofs/lean4/LambdaCNO.lean:184+` — `+subst_closed_term+` — *DISCHARGED
417+
2026-09-22* (fix PR for #125): now a `+theorem+`; it is immediate from the
418+
semantic definition of `+Closed+` (`+h n s (Nat.zero_le n)+`).
419+
* `+proofs/lean4/FilesystemCNO.lean:271+` — `+mkdir_not_identity+`
412420
** *Owner*: @hyperpolymath
413421
** *Plan*: existence proof; exhibit one concrete `+fs+` lacking the
414422
path. Mirrors Coq site at `+FilesystemCNO.v:300+`.
415423
** *Deadline*: INDEFINITE.
416-
* `+proofs/lean4/FilesystemCNO.lean:288+` —
424+
* `+proofs/lean4/FilesystemCNO.lean:320+` —
417425
`+snapshot_restore_identity+`
418426
** *Owner*: @hyperpolymath
419427
** *Plan*: composite theorem; derivable from `+snapshot+`/`+restore+`
420428
primitives once a concrete snapshot model is in place. Mirrors Coq site
421429
at `+FilesystemCNO.v:453+`.
422430
** *Deadline*: INDEFINITE.
423-
* `+proofs/lean4/FilesystemCNO.lean:309+` — `+mkdir_idempotent+`
431+
* `+proofs/lean4/FilesystemCNO.lean:345+` — `+mkdir_idempotent+`
424432
** *Owner*: @hyperpolymath
425-
** *Plan*: follows from `+mkdir_rmdir_inverse+` + stronger repeat-mkdir
426-
semantics. Mirrors Coq site at `+FilesystemCNO.v:421+`.
433+
** *Plan*: does *not* follow from `+mkdir_rmdir_inverse+`: issue #125 showed
434+
that with an unconditional inverse law, idempotence plus
435+
`+mkdir_not_identity+` derives `+False+` (now recorded in-file as
436+
`+unconditional_mkdir_rmdir_inverse_is_false+`). Discharge = port the
437+
concrete Coq list model, where `+FilesystemCNO.v:421+` proves it.
427438
** *Deadline*: INDEFINITE.
428439
* `+proofs/lean4/QuantumCNO.lean:134+` — `+X_gate_not_identity+`
429440
** *Owner*: @hyperpolymath

0 commit comments

Comments
 (0)