docs+build: update to two-pillar six-prover completion (post-PR #100)

- Justfile: build-coq now builds all 14 theories (CNO+OND) via coq_makefile;
  add build-mizar/build-idris/verify (canonical gate → verify-all-provers.sh)
  + verify-mizar/verify-idris; drop banned rescript/typescript from build-all;
  fix verify-z3 (cno_properties.smt2 → verify.sh + ond/OND_checks.smt2).
- .machine_readable/6a2/STATE.a2ml: refresh proof state to the six-prover
  completion — tech-stack, per-prover components, working-features, milestones,
  blockers, next-actions, and a 2026-07-06 session-history entry.
- README.md: OND no longer "design/roadmap stage" (OND-1..5 proved); fix
  directory tree (ond/, verify-all-provers.sh); rewrite prerequisites/build to
  the real toolchains (drop banned npm/rescript, add all six provers + Idris).
- ROADMAP.adoc: rewrite "Honest Current State" to the reproduced reality;
  flip OND status to OND-1..5 landed / OND-6 open.
- docs/OND-PILLAR-STRUCTURE.adoc, docs/MACHINE_VERIFICATION.adoc: dated status
  banners; OND modules authored, examples marked historical.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -11,90 +11,83 @@ repo = "github.com/hyperpolymath/absolute-zero"
 version = "1.0.0-alpha"
 schema-version = "1.0"
 created = "2026-01-03"
-last-updated = "2026-06-12"
+last-updated = "2026-07-07"
 status = "active"
 
 [project-context]
 name = "Absolute Zero"
-tagline = "Formal Verification of Certified Null Operations"
-tech-stack = ["Coq", "Lean 4", "Z3", "Agda", "Isabelle", "ReScript", "Rust"]
+tagline = "Formal Verification of Two Null-Operation Pillars: Certified Null Effect (CNO) and Observational Null Disclosure (OND)"
+tech-stack = ["Coq", "Lean 4", "Agda", "Z3", "Isabelle", "Mizar", "Idris 2", "Rust"]
 
 [position]
-phase = "proof-completion"
-completion-percentage = 65
+phase = "two-pillar completion / hardening"
+completion-percentage = 88
 maturity = "experimental"
 
 [recent-work]
-# Delta since the previous STATE update (2026-05-27), from
-# `git log --since=2026-05-27 --oneline origin/main`.
 since = "2026-05-27"
-summary = "CI/governance work only — no proof-track changes since the Phase-1 axiom triage (PR #58)"
+summary = "Two-pillar completion (PR #100): both CNO and OND machine-checked across six provers + Idris; OND pillar authored from scratch; CNO axioms cut 98→small classified remainder; three latent-unsound axioms found and fixed"
 items = [
-  "PR #68 — ci(scorecard): add job-level permissions for reusable workflow",
-  "PR #69 — ci: repin orphan reusable SHAs (97df7621/4fdf4314 → live)",
-  "PR #71 — ci(codeql): cron weekly→monthly (cut 3, standards#233 Option B)",
-  "PR #72 — chore(deps): bump the actions group with 2 updates",
-  "README sponsor badge added (commit 4867f1f)",
-  "2026-06-12 — estate-standardization-20260607 merged on the governance-checkpoint branch: flat .machine_readable/contractiles/, svc/k9 → self-validating/ rename, GOVERNANCE.adoc + MAINTAINERS.adoc + .github/CODEOWNERS, Guix manifest.scm, 6a2 manifest/README + anchor/, removal of the duplicate root .machine_readable/*.scm set and the root contractiles/ template dir, SPDX header normalization",
-  "2026-06-12 — governance checkpoint: bot_directives/ trio, fully-populated flat contractiles (incl. new Dustfile/Bustfile), 6a2/anchor/ANCHOR.a2ml, README dedup (README.md → pointer), docs/archive/ index, wiki currency fixes",
+  "PR #100 (MERGED, squash 6b591f12) — feat(proofs): complete CNO + OND pillars, verified across six provers",
+  "proofs/verify-all-provers.sh → ALL-PROVERS-GREEN (Coq 14/14, Agda, Lean 4+Mathlib, Z3, Isabelle/HOL, Mizar, Idris 2 ABI)",
+  "OND pillar authored: proofs/coq/ond/OND.v (OND-1..5, all Closed under global context) + Lean/Agda/Z3 mirrors; OND-6 open by design; OND-7 residue register seeded",
+  "CNO axiom discharge: filesystem 26→0, category 1→0, QuantumMechanicsExact 2→0; QuantumCNO 41→12; physics postulates kept + tagged METAL-BOUNDARY",
+  "Soundness fixes: removed no_cloning (provably false) + Cconj_Cexp (false); corrected eta_equivalence (false as stated → no_lambda-guarded theorem)",
+  "Idris ABI packaging fixed + 6 latent type errors repaired; Isabelle CNO.thy repaired + OND.thy added; Mizar CNO.miz rewritten and verifies (needs dict/cno.voc)",
 ]
 
 [components]
-# Format: name = [percentage, "notes"]
-coq-proofs = [90, "11/11 files compile (Coq 8.18.0+8.20.1); 0 Admitted (rescue 2026-05-18); 75→72 Axioms + 42 Parameters; Phase 1 triage 2026-05-27 (PR #58) classifies 72 Coq Axioms into §c TRUSTED-BASE (52) + §a DISCHARGE backlog (17) + §b PROPERTY-TEST (3); see docs/proof-debt-triage.md"]
-lean4-proofs = [95, "lake build 1631/1632 green (mathlib + 6 lean_lib targets); verified 2026-05-20"]
-z3-proofs = [90, "10 theorems encoded, needs z3 runtime"]
-agda-proofs = [60, "CNO.agda type-checks clean — 0 postulates/holes/unsolved metas (verified 2026-05-18)"]
-isabelle-proofs = [40, "phase 1 complete"]
-mizar-proofs = [10, "stub, needs installation"]
+# Format: name = [percentage, "notes"]. Reproduce all via proofs/verify-all-provers.sh → ALL-PROVERS-GREEN.
+coq-proofs = [95, "14/14 theories compile (Coq 8.18.0), both pillars, via coq_makefile -f _CoqProject; 0 Admitted. CNO axioms 98→small: filesystem/category/QuantumMechanicsExact fully discharged (0); QuantumCNO 41→12 (2 metal-boundary physics + 4 class-A open); physics postulates kept + tagged METAL-BOUNDARY. OND pillar ond/OND.v OND-1..5 all Closed under global context (0 axioms)."]
+lean4-proofs = [95, "lake build green (Mathlib + CNO libs + new OND lib proofs/lean4/OND.lean, 0 sorry); verified 2026-07-06"]
+z3-proofs = [95, "CNO checks (proofs/z3/verify.sh) + OND bounded instances (proofs/z3/ond/OND_checks.smt2, sat/unsat/sat); z3 4.16.0"]
+agda-proofs = [90, "CNO.agda + new OND.agda type-check clean (--safe --without-K, 0 postulates); verified 2026-07-06"]
+isabelle-proofs = [90, "CNO.thy repaired + new OND.thy; session AbsoluteZero-CNO builds (Isabelle2025-2), 0 sorry"]
+mizar-proofs = [90, "CNO.miz rewritten into a genuine 12-theorem article; accom+verifier → empty CNO.err (Mizar 8.1.15); requires proofs/mizar/dict/cno.voc"]
+idris-abi = [95, "absolute-zero-abi.ipkg builds clean (idris2 0.8.0); packaging + 6 latent type errors fixed"]
 
 [working-features]
 features = [
-  "Core CNO theory fully proven",
-  "Category theory fully proven",
-  "Statistical mechanics fully proven",
-  "Lambda calculus 90% proven",
-  "Quantum computing 70% proven",
-  "Filesystem 57% proven",
+  "CNO pillar (certified null effect): core theory, category, statistical mechanics, filesystem, quantum (1-qubit fragment) — headline results proved, not axiomatised",
+  "OND pillar (certified null disclosure): OND-1 definition, OND-2 trivial case, OND-3 CNO⊥OND independence (anchored to real core is_CNO), OND-4 real-op template, OND-5 non-composition — all proved, zero axioms",
+  "Six-prover reproducible verification gate (proofs/verify-all-provers.sh)",
+  "Idris 2 ABI boundary builds and type-checks",
 ]
 
 [route-to-mvp]
 milestones = [
-  { id = "v0.8", label = "Compliance sprint",     status = "in-progress",  completion = 40 },
-  { id = "v0.9", label = "Container verification", status = "not-started",  completion = 0 },
-  { id = "v1.0", label = "Publication release",    status = "not-started",  completion = 0 },
+  { id = "v0.8", label = "Two-pillar six-prover completion", status = "done",         completion = 100 },
+  { id = "v0.9", label = "Container / CI proof verification", status = "in-progress",  completion = 20 },
+  { id = "v1.0", label = "Publication release",               status = "not-started",  completion = 0 },
 ]
 
 [blockers-and-issues]
 critical = []
-high = [
-  "Python interpreters violate RSR",
-]
+high = []
 medium = [
-  "LandauerDerivation.v needs measure theory",
-  "17 §a DISCHARGE Coq axioms backlog (post-Phase-1 triage, see docs/proof-debt-triage.md)",
-  "Triage Phase 2 for 52 Lean axioms + 7 Idris2 postulates (#27) still pending",
+  "OND-6 conditional composition theorem — research capstone, deliberately open (see docs/OND-ROADMAP.adoc)",
+  "Class-A open axioms (true, provable in principle): CNOT_gate_unitary + unitary_inverse_property + fidelity_bound (need finite-dim/tensor QM model); y_not_cno (needs coinductive/step-indexed β non-termination argument)",
 ]
 low = [
-  "y_not_cno non-termination proof",
+  "Physics-constant deduplication (kB_positive/temperature_positive declared across QuantumCNO/StatMech/LandauerDerivation)",
+  "No CI job yet builds/verifies the proofs — add a proof-verification workflow",
 ]
 
 [critical-next-actions]
 immediate = [
-  "Phase 2 triage: Lean axioms (52) + Idris2 postulates (#27, 7)",
+  "Owner ratification of the three PR #100 judgment calls (OND model shape; accepting the class-A remainder; unsound-axiom removals) — already merged, revisit only if desired",
 ]
 this-week = [
-  "Begin discharging the 17 §a Coq DISCHARGE-backlog axioms (lowest-hanging: cno_zero_energy_dissipation_derived, fidelity_bound, unitary_inverse_property, *_not_identity existence pair)",
-  "Physics-constant deduplication (kB_positive/temperature_positive declared 3x across QuantumCNO/StatMech/LandauerDerivation)",
-  "Migrate Python to Rust",
+  "Add a CI workflow that runs the lighter provers (Coq/Agda/Z3/Idris) on PRs",
 ]
 this-month = [
   "Container pipeline",
-  "Paper draft",
+  "Paper draft (both pillars, six-prover story)",
 ]
 
 [session-history]
 sessions = [
+  { date = "2026-07-06", agent = "opus", summary = "Two-pillar completion (PR #100, MERGED squash 6b591f12). Installed all six provers to ~/.local (Z3 4.16, Isabelle2025-2, Mizar 8.1.15, Lean 4.16+Mathlib). Authored the OND disclosure pillar from scratch — OND-1..5 proved in Coq (ond/OND.v, all Closed under global context, zero axioms) + Lean/Agda/Z3 mirrors; OND-3 anchored to real core is_CNO; OND-6 left open (research). Discharged CNO axioms 98→small: filesystem 26→0, category 1→0, QuantumMechanicsExact 2→0; QuantumCNO 41→12 (kept 2 metal-boundary physics + 4 class-A). FOUND+FIXED three latent-unsound axioms: no_cloning (provably false), Cconj_Cexp (false), eta_equivalence (false as stated → no_lambda-guarded theorem). Repaired Isabelle CNO.thy + added OND.thy; rewrote Mizar CNO.miz (verifies, needs dict/cno.voc); fixed Idris ABI packaging + 6 type errors. Single gate proofs/verify-all-provers.sh → ALL-PROVERS-GREEN. Method: Opus coordinated, fanned out per-file discharge + per-prover repair to sub-agents (each machine-checked with its prover, no Admitted/admit/new-axiom cheats)." },
   { date = "2026-05-27", agent = "opus", summary = "Phase 1 per-axiom triage of all 72 Coq Axioms per standards#203 trusted-base policy. Classification: 52 §c TRUSTED-BASE (physics constants, quantum primitives, POSIX semantics, Kolmogorov+Shannon axioms, Cexp algebra, physical laws), 17 §a DISCHARGE (derivable theorems incl. 2 named *_derived), 3 §b PROPERTY-TEST (decidability over opaque types). Surfaced 5 follow-ups (physics-constant dedup ×3, quantum-law dedup ×2, Cexp constructive in Complex.v). PR #58 MERGED 2026-05-27 (commit e17256b). Also: traced phantom '315 Lean sorries' figure to a metric mismatch — actual local user-sorry count = 0; canonical figure is 129 (now 124) escape hatches across all proof languages per standards#195 + scripts/check-trusted-base.sh." },
   { date = "2026-05-20", agent = "opus", summary = "Post-T0 axiom audit: 117 declarations triaged into Tier A/B/C; 2 unsound axioms (eval_respects_state_eq_left/right) deleted with downstream refactor; logically_reversible weakened to =st=; cno_eval_on_equal_states + cno_logically_reversible re-proved without axioms; 75→73 Axioms total" },
   { date = "2026-05-20", agent = "opus", summary = "Rescue branch rebased onto current main (clean); eval_deterministic Axiom discharged → Theorem (via step_deterministic_strong helper); Print Assumptions Closed under global context; 11/11 Coq + 1631/1632 Lean targets green; PR #24 MERGED (admin-squash 69e7a22)" },

Justfile

@@ -14,43 +14,53 @@ default:
 # Build Commands
 # ============================================================================
 
-# Build everything
-build-all: build-rescript build-coq build-lean build-agda build-isabelle build-typescript
+# Build everything (all six prover backends + the Idris ABI)
+build-all: build-coq build-lean build-agda build-isabelle build-mizar build-idris
     @echo "✓ All builds complete"
 
 # Build ReScript interpreters
 build-rescript:
     @echo "Building ReScript interpreters..."
     cd interpreters/rescript && npx rescript build
 
-# Build Coq proofs
+# Build Coq proofs — all 14 theories (CNO + OND pillars) via coq_makefile
 build-coq:
-    @echo "Building Coq proofs..."
+    @echo "Building Coq proofs (14 theories, both pillars)..."
     @if command -v coqc >/dev/null 2>&1; then \
-        cd proofs/coq/common && coqc CNO.v && \
-        cd ../physics && coqc -R ../common CNO StatMech.v && \
-        coqc -R ../common CNO LandauerDerivation.v && \
-        cd ../quantum && coqc -R ../common CNO QuantumMechanicsExact.v && \
-        cd ../malbolge && coqc -R ../common CNO MalbolgeCore.v && \
-        echo "✓ Coq proofs compiled"; \
+        cd proofs/coq && coq_makefile -f _CoqProject -o Makefile.all >/dev/null && \
+        make -f Makefile.all -j"$(nproc)" && \
+        echo "✓ Coq proofs compiled (CNO + OND)"; \
     else \
         echo "⚠ coqc not found, skipping Coq build"; \
     fi
 
-# Build Lean 4 proofs
+# Build Lean 4 proofs (CNO libs + OND; needs Mathlib cache)
 build-lean:
     @echo "Building Lean 4 proofs..."
     cd proofs/lean4 && lake build
 
-# Build Agda proofs
+# Build Agda proofs (CNO + OND, --safe --without-K)
 build-agda:
     @echo "Building Agda proofs..."
-    cd proofs/agda && agda CNO.agda
+    cd proofs/agda && agda --safe --without-K CNO.agda && agda --safe --without-K OND.agda
 
-# Build Isabelle/HOL proofs
+# Build Isabelle/HOL proofs (CNO + OND session)
 build-isabelle:
     @echo "Building Isabelle/HOL proofs..."
-    isabelle build -D proofs/isabelle
+    isabelle build -d proofs/isabelle AbsoluteZero-CNO
+
+# Build Mizar article (needs MIZFILES + proofs/mizar/dict/cno.voc)
+build-mizar:
+    @echo "Building Mizar CNO article..."
+    @if command -v verifier >/dev/null 2>&1; then \
+        cd proofs/mizar && accom CNO && verifier CNO && \
+        { test -s CNO.err && { echo "✗ Mizar errors (CNO.err)"; exit 1; } || echo "✓ Mizar verified"; }; \
+    else echo "⚠ mizar verifier not found, skipping"; fi
+
+# Build the Idris 2 ABI package
+build-idris:
+    @echo "Building Idris 2 ABI..."
+    idris2 --build absolute-zero-abi.ipkg
 
 # Build TypeScript
 build-typescript:
@@ -62,19 +72,24 @@ build-typescript:
 # Verification Commands
 # ============================================================================
 
-# Verify all proofs
-verify-all: verify-coq verify-z3 verify-lean verify-agda verify-isabelle
+# Verify BOTH pillars across ALL six provers + the Idris ABI (canonical gate).
+# Single source of truth; prints ALL-PROVERS-GREEN on success.
+verify:
+    @proofs/verify-all-provers.sh
+
+# Verify all proofs (per-prover targets; `just verify` is the canonical one-shot)
+verify-all: verify-coq verify-z3 verify-lean verify-agda verify-isabelle verify-mizar verify-idris
     @echo "✓ All verifications complete"
 
 # Verify Coq proofs
 verify-coq: build-coq
     @echo "✓ Coq proofs verified"
 
-# Verify Z3 SMT properties
+# Verify Z3 SMT properties (CNO checks + OND bounded instances)
 verify-z3:
     @echo "Verifying Z3 SMT properties..."
     @if command -v z3 >/dev/null 2>&1; then \
-        z3 proofs/z3/cno_properties.smt2 && echo "✓ Z3 verification complete"; \
+        sh proofs/z3/verify.sh && z3 proofs/z3/ond/OND_checks.smt2 && echo "✓ Z3 verification complete"; \
     else \
         echo "⚠ z3 not found, skipping Z3 verification"; \
     fi
@@ -92,6 +107,14 @@ verify-agda: build-agda
 verify-isabelle: build-isabelle
     @echo "✓ Isabelle/HOL proofs verified"
 
+# Verify the Mizar CNO article
+verify-mizar: build-mizar
+    @echo "✓ Mizar proofs verified"
+
+# Verify the Idris 2 ABI package
+verify-idris: build-idris
+    @echo "✓ Idris ABI verified"
+
 # ============================================================================
 # Testing Commands
 # ============================================================================

README.md

@@ -68,9 +68,13 @@ proof and the physical metal.
 
 See **`docs/TWO-PILLARS.adoc`** (narrative), **`docs/OND-ROADMAP.adoc`**
 (prioritised obligations), and **`docs/OND-PILLAR-STRUCTURE.adoc`**
-(module layout). The OND pillar is at the design/roadmap stage: its
-obligations are currently `Admitted` (specified, not yet proved) — the
-normal honest starting state, mirroring CNO’s own open obligations.
+(module layout). **Both pillars are now machine-checked.** OND obligations
+**OND-1..5** are proved with **zero axioms** in Coq (`proofs/coq/ond/OND.v`,
+every theorem *Closed under the global context*), mirrored in Lean 4, Agda,
+and Z3; the independence theorem is anchored to the real core `is_CNO`. Only
+**OND-6** (conditional composition, the research capstone) remains open, by
+design. Reproduce the whole estate — both pillars, all six provers plus the
+Idris ABI — with **`proofs/verify-all-provers.sh`** (`ALL-PROVERS-GREEN`).
 
 # Project Structure
 
@@ -97,9 +101,11 @@ normal honest starting state, mirroring CNO’s own open obligations.
     │   ├── agda/                # Agda proofs (dependent types)
     │   ├── isabelle/            # Isabelle/HOL (production-grade)
     │   ├── mizar/               # Mizar proofs (mathematical library)
+    │   ├── ond/                 # OND Coq module (OND-1..5 proved, zero axioms)
     │   ├── observation-models/  # OND: declared observation models O (proof inputs)
-    │   └── residue/             # OND: residue lists (the model-vs-metal gap)
-    │   # Each prover dir hosts CNO.* and (to author) co-equal OND.* modules
+    │   ├── residue/             # OND: residue lists (the model-vs-metal gap)
+    │   └── verify-all-provers.sh # one-shot gate: both pillars, all six provers + Idris
+    │   # Each prover dir hosts CNO.* and co-equal OND.* modules (OND now authored)
     │
     ├── interpreters/            # Language interpreters with CNO detection
     │   ├── rescript/            # Malbolge (ReScript)
@@ -126,33 +132,38 @@ normal honest starting state, mirroring CNO’s own open obligations.
     │
     ├── Justfile                 # Build automation
     ├── Containerfile            # Containerized verification (Podman/Docker)
-    ├── VERIFICATION.md          # Detailed verification status
-    └── .gitlab-ci.yml           # CI/CD pipeline
+    ├── PROOF-STATUS.adoc        # Reproduced verification status, prover by prover
+    └── .github/workflows/       # CI/CD (GitHub Actions)
 
 # Quick Start
 
 ## Prerequisites
 
-**Fedora**: `` `bash `` `sudo` `dnf` `install` `coq` `z3` `nodejs`
-`opam` `just` `npm` `install` `-g` `rescript@11.1`\`
+The proofs span six provers plus the Idris 2 ABI. Coq, Agda, Z3, and Idris 2 are
+the lightest; Lean needs Mathlib, and Isabelle/Mizar are large downloads.
 
-**Ubuntu**: `` `bash `` `sudo` `apt` `install` `coq` `z3` `nodejs` `npm`
-`npm` `install` `-g` `rescript@11.1` `cargo` `install` `just`\`
+- **Coq** 8.18+ (`coqc`, `coq_makefile`)
+- **Agda** 2.6.3 (with agda-stdlib)
+- **Lean 4** (via `elan`; toolchain pinned in `proofs/lean4/lean-toolchain`, needs Mathlib)
+- **Z3** 4.16+
+- **Isabelle** 2025-2 (ships a prebuilt HOL image)
+- **Mizar** 8.1.x (set `MIZFILES` to its MML)
+- **Idris 2** 0.8+
+- **just** (task runner), **Rust/cargo** (interpreters/tools)
 
-## Build
+## Build & verify
 
 ```bash
-# Install dependencies
-npm install
+# One-shot: both pillars, all six provers + the Idris ABI → ALL-PROVERS-GREEN
+proofs/verify-all-provers.sh
 
-# Build everything
-just build-all
+# Or via the task runner (canonical gate)
+just verify
 
-# Verify all proofs
-just verify-all
-
-# Run tests
-just test-all
+# Individual prover targets also exist, e.g.
+just build-coq      # all 14 Coq theories (CNO + OND) via coq_makefile
+just verify-agda
+just verify-mizar
 ```
 
 ## Container (Podman/Docker)