feat(proofs): complete CNO + OND pillars, verified across six provers#100
Merged
Conversation
Both pillars of Absolute Zero are now machine-checked end-to-end. A single gate (proofs/verify-all-provers.sh) builds every prover and prints ALL-PROVERS-GREEN: Coq, Agda, Lean 4 (+Mathlib), Z3, Isabelle/HOL, Mizar, plus the Idris 2 ABI. OND pillar (disclosure) — NEW, zero axioms: - OND-1..5 proved in Coq (ond/OND.v, all Closed under the global context), mirrored in Lean 4 (OND.lean), Agda (OND.agda), and Z3 (bounded instances). - OND-3 independence anchored to the real core is_CNO. - OND-7 residue register seeded (ct_select.residue, O_all.model). - Only OND-6 (conditional composition, research capstone) left open by design. CNO pillar (effect) — axiom discharge, 98 -> small classified remainder: - filesystem 26->0, category 1->0, QuantumMechanicsExact 2->0 (Closed under global context); QuantumCNO 41->12 (19 discharged, 8 concretised). - Removed two latent-unsound axioms (no_cloning was provably false; Cconj_Cexp false for a genuine phase). - Physics postulates (kB>0, temperature>0, Landauer, Second Law) kept and tagged METAL-BOUNDARY; state_dec kept (nat->nat not decidably equal). - Honest class-A remainder, openly labelled: y_not_cno (Y non-termination), CNOT_gate_unitary, unitary_inverse_property, fidelity_bound. Other provers / ABI: - Isabelle CNO.thy repaired (reserved `value` type; failing nop/step lemmas) and OND.thy added; session ROOT added. - Mizar CNO.miz verifies with an empty .err. - Idris ABI: packaging fixed (module paths vs sourcedir) + six latent type errors repaired; builds clean. Narrative updated alongside the maths: TWO-PILLARS and OND-ROADMAP status, PROOF-STATUS rewritten to the reproduced six-prover reality. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ewrite findings - proofs/mizar/dict/cno.voc (private vocabulary) is REQUIRED for CNO.miz to accom/verify; the earlier .gitignore excluded it. Un-ignore the .voc source (keep verifier build artifacts ignored) and commit it. Verified: a clean tree with only CNO.miz + dict/cno.voc reproduces an empty CNO.err. - PROOF-STATUS: note the Mizar article was rewritten (original machine-generated, 277 errors) and requires cno.voc. - PROOF-STATUS: disclose a THIRD latent-unsound finding — LambdaCNO eta_equivalence was false as stated (counterexample f = LVar 5; subst does not re-index under binders); replaced by an honest no_lambda-guarded theorem. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jul 7, 2026
…ble) (#101) ## Summary Estate-hygiene follow-up to PR #100 (the CNO+OND six-prover completion). Brings the **human docs, machine-readable/bot docs, CI, and wiki** into line with the now-completed two pillars. No proof code changes. ### Human documentation - **README.md**: OND no longer "design/roadmap stage" (OND-1..5 proved); real toolchains in prerequisites (dropped banned npm/rescript); fixed directory tree and the `.gitlab-ci.yml` → GitHub Actions reference. - **ROADMAP.adoc**: rewrote "Honest Current State" to the reproduced six-prover reality; OND status → OND-1..5 landed / OND-6 open. - **AUDIT.adoc**: resolved `AUDIT-2026-05-20-A` (Idris errors, fixed in #100); logged the three unsound-axiom removals + completion; fixed stale `META.scm` paths. - **CHANGELOG.md**: Unreleased entries. - **docs/**: dated status banners on the historical proof docs (VERIFICATION_RESULTS, PROOF-COMPLETION-PLAN, PROOF-CLASSIFICATION, proof-debt, proof-debt-triage); OND-PILLAR-STRUCTURE + MACHINE_VERIFICATION updated. ### Machine-readable / bot docs (`.machine_readable/6a2/`) - **STATE.a2ml**: full refresh (per-prover components, milestones, blockers, next-actions, session-history). - **AGENTIC.a2ml**: corrected **dangerously stale** directives — `lean4-sorry 18→0`, `coq-admitted 19→0`, "never touch Lean/Idris" removed (they now build); added a no-new-axiom rule. - **META.a2ml**: ADR-011..014 (OND model, OND-1..5 landed, unsound removals, class-A acceptance). - **NEUROSYM.a2ml**, **PLAYBOOK.a2ml**: prover list + build/verify procedures. ### Build / CI - **Justfile**: `build-coq` now builds all 14 theories via `coq_makefile`; added `build-mizar`/`build-idris`/`verify` (canonical gate) + `verify-mizar`/`-idris`; fixed `verify-z3`; dropped banned rescript/typescript from `build-all`. - **.github/workflows/proofs.yml** (new): Coq (14 theories) + Z3 verification on PRs touching `proofs/`. Lightweight provers only (Lean+Mathlib/Isabelle/Mizar are too heavy for standard runners; the full gate runs via `proofs/verify-all-provers.sh`). ## Owner decisions flagged (not actioned) 1. **Live wiki**: `docs/wiki` (13 rich pages, updated here) is **not published** to the GitHub wiki, which is a 1-line stub with no sync workflow. Wire a publish workflow or do a one-time push? (Not pushed here — outward-facing.) 2. **`6a2/` → `descriptiles/`**: the machine-readable dir still uses the deprecated `6a2` name (estate-wide rename, led by rsr-template-repo — left as-is). 3. **CI scope**: `proofs.yml` runs on every matching PR (Actions minutes). ## Test `just build-coq` → 14/14; `.github/workflows/proofs.yml` validates; no proof code touched. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Completes both pillars of Absolute Zero and makes every prover reproducible in one gate.
proofs/verify-all-provers.shbuilds all of them and printsALL-PROVERS-GREEN:Coq · Agda · Lean 4 (+Mathlib) · Z3 · Isabelle/HOL · Mizar, plus the Idris 2 ABI.
OND pillar (disclosure) — new, zero axioms
OND-1..5proved in Coq (proofs/coq/ond/OND.v, every theorem Closed under the global context), mirrored in Lean 4, Agda, and Z3 (bounded instances).OND-3independence anchored to the real coreis_CNO.CNO pillar (effect) — axiom discharge, 98 → small classified remainder
no_cloningprovably false;Cconj_Cexpfalse).state_deckept (nat→nat undecidable eq).y_not_cno,CNOT_gate_unitary,unitary_inverse_property,fidelity_bound.Other provers / ABI
CNO.thyrepaired +OND.thyadded (session ROOT).CNO.mizverifies (empty.err).Decisions worth owner ratification (draft)
no_cloning/Cconj_Cexpand two unused non-compiling ABIDecEqinstances.Test
proofs/verify-all-provers.sh→ALL-PROVERS-GREEN.🤖 Generated with Claude Code