diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml
index c288d3f..6bd23ea 100644
--- a/.github/workflows/proofs.yml
+++ b/.github/workflows/proofs.yml
@@ -20,6 +20,7 @@ on:
       - 'proofs/**'
       - 'src/**'
       - 'scripts/check-proof-patterns.sh'
+      - 'scripts/provision-agda-stdlib.sh'
       - 'tests/check-proof-patterns.sh'
       - '.machine_readable/contractiles/trust/trust.k9.ncl'
       - 'absolute-zero-abi.ipkg'
@@ -56,16 +57,11 @@ jobs:
         # version-matched stdlib from git instead (validated locally).
         run: sudo apt-get update && sudo apt-get install -y agda
       - name: Fetch + register agda-stdlib v1.7.3 (matches Agda 2.6.3)
-        run: |
-          git clone -q --depth 1 --branch v1.7.3 \
-            https://github.com/agda/agda-stdlib.git "$HOME/agda-stdlib"
-          # The upstream manifest is named `standard-library-1.7.3`; the repo's
-          # absolute-zero.agda-lib depends on `standard-library`, so align it.
-          sed -i 's/^name: .*/name: standard-library/' \
-            "$HOME/agda-stdlib/standard-library.agda-lib"
-          mkdir -p "$HOME/.agda"
-          echo "$HOME/agda-stdlib/standard-library.agda-lib" > "$HOME/.agda/libraries"
-          echo "standard-library" > "$HOME/.agda/defaults"
+        # Same script for CI and local runs: clones tag v1.7.3, fails unless it
+        # resolves to the pinned commit, renames the manifest to
+        # `standard-library` (what absolute-zero.agda-lib depends on), and writes
+        # ~/.agda/libraries + ~/.agda/defaults.
+        run: bash scripts/provision-agda-stdlib.sh
       - name: Type-check CNO + OND + EchoBridge (4 modules, PROOF-POLICY 2.1 + strict flags)
         working-directory: proofs/agda
         # The canonical invocation (standards PROOF-POLICY 2.1) is
diff --git a/ECHIDNA.adoc b/ECHIDNA.adoc
index cff270a..2dea62d 100644
--- a/ECHIDNA.adoc
+++ b/ECHIDNA.adoc
@@ -15,6 +15,16 @@ This document describes integrating the **hyperpolymath ECHIDNA neurosymbolic th
 
 **Status**: ✅ **TRUSTED** - Production-ready with comprehensive trust framework
 
+[IMPORTANT]
+.Archive notice (2026-10-10)
+====
+This plan was written around the Coq and Lean 4 trees, which were archived on
+2026-10-10 under `archive/proofs/` (with Isabelle/HOL and Mizar) and are no
+longer built or gated. Input paths below point at `archive/proofs/…`. The active
+stack is Agda (`proofs/agda/`) + Z3 bounded checks (`proofs/z3/`) + the Idris 2
+ABI, run by `proofs/verify-active-provers.sh`; see `PROOF-STATUS.adoc`.
+====
+
 ---
 
 == Trust Assessment
@@ -95,7 +105,7 @@ This document describes integrating the **hyperpolymath ECHIDNA neurosymbolic th
 
 == Architecture Integration
 
-=== Current Absolute Zero Stack
+=== Absolute Zero Stack (as of writing; historical since 2026-10-10)
 
 ```
 ┌─────────────────────────────────────────┐
@@ -229,7 +239,7 @@ pack install idris2-echidna
 
 # Test validator
 pack exec idris2-echidna -- validate \
-  --proof ~/Documents/hyperpolymath-repos/absolute-zero/proofs/coq/common/CNO.v \
+  --proof ~/Documents/hyperpolymath-repos/absolute-zero/archive/proofs/coq/common/CNO.v \
   --prover Coq
 ```
 
@@ -248,17 +258,17 @@ cd ~/Documents/hyperpolymath-repos/absolute-zero
 mkdir -p tools/echidna/cno-corpus
 
 # Coq proofs (Phase 1-4 complete)
-find proofs/coq -name "*.v" -exec cat {} \; > tools/echidna/cno-corpus/coq_proofs.v
+find archive/proofs/coq -name "*.v" -exec cat {} \; > tools/echidna/cno-corpus/coq_proofs.v
 
 # Lean 4 proofs
-find proofs/lean4 -name "*.lean" -exec cat {} \; > tools/echidna/cno-corpus/lean_proofs.lean
+find archive/proofs/lean4 -name "*.lean" -exec cat {} \; > tools/echidna/cno-corpus/lean_proofs.lean
 
 # Z3 SMT specifications
 cp proofs/z3/cno_properties.smt2 tools/echidna/cno-corpus/
 
 # Count theorems
-echo "Coq theorems:" $(grep -c "Theorem\|Lemma" proofs/coq/common/CNO.v)
-echo "Lean theorems:" $(grep -c "theorem\|lemma" proofs/lean4/CNO.lean)
+echo "Coq theorems:" $(grep -c "Theorem\|Lemma" archive/proofs/coq/common/CNO.v)
+echo "Lean theorems:" $(grep -c "theorem\|lemma" archive/proofs/lean4/CNO.lean)
 echo "Z3 assertions:" $(grep -c "assert.*theorem" proofs/z3/cno_properties.smt2)
 ```
 
@@ -340,7 +350,7 @@ echidna-repl:
 echidna-complete:
     @echo "Attempting to complete 21 Admitted proofs..."
     cd tools/echidna/neurosym && ./target/release/echidna complete \
-      --proof-dir ../../proofs/coq \
+      --proof-dir ../../archive/proofs/coq \
       --output-dir ../../proofs/coq-completed \
       --prover Coq \
       --max-tactics 50
@@ -359,7 +369,7 @@ Target: 21 Admitted → 0
 cd ~/Documents/hyperpolymath-repos/absolute-zero
 
 # List all Admitted proofs
-grep -rn "Admitted" proofs/coq/ | tee admitted_list.txt
+grep -rn "Admitted" archive/proofs/coq/ | tee admitted_list.txt
 
 # Use ECHIDNA to suggest completions
 just echidna-start
@@ -371,7 +381,7 @@ cat proofs/coq-completed/*.v
 # Manually verify and integrate
 for file in proofs/coq-completed/*.v; do
   echo "Reviewing: $file"
-  diff proofs/coq/$(basename $file) $file
+  diff archive/proofs/coq/$(basename $file) $file
   # If valid, replace
 done
 ```
@@ -379,7 +389,7 @@ done
 **Example ECHIDNA session:**
 
 ```coq
-echidna> load proofs/coq/physics/StatMech.v
+echidna> load archive/proofs/coq/physics/StatMech.v
 echidna> focus bennett_logical_implies_thermodynamic
 echidna> suggest
 
@@ -418,7 +428,7 @@ cd ~/Documents/hyperpolymath-repos/absolute-zero
 just echidna-start
 
 # Multi-prover verification
-for thm in $(grep "Theorem\|Lemma" proofs/coq/common/CNO.v | awk '{print $2}'); do
+for thm in $(grep "Theorem\|Lemma" archive/proofs/coq/common/CNO.v | awk '{print $2}'); do
   echo "Verifying $thm..."
 
   # Translate to multiple formats
@@ -508,7 +518,7 @@ echidna_neurosym:
     # Verify all proofs with multi-prover consensus
     - cd ../../..
     - ./tools/echidna/neurosym/target/release/echidna verify-all \
-        --proof-dir proofs/coq \
+        --proof-dir archive/proofs/coq \
         --provers "Coq,Lean4,Z3" \
         --consensus 2 \
         --output echidna-report.json
@@ -574,7 +584,7 @@ chmod +x .git/hooks/pre-commit
 # Interactive REPL session
 just echidna-repl
 
-echidna> load proofs/coq/physics/StatMech.v
+echidna> load archive/proofs/coq/physics/StatMech.v
 echidna> focus cno_logically_reversible
 echidna> suggest
 echidna> apply suggestion 1
@@ -604,14 +614,14 @@ cat verification_report.json | jq '.consensus'
 ```bash
 # Translate Coq proof to Lean 4
 ./tools/echidna/neurosym/target/release/echidna translate \
-  --input proofs/coq/common/CNO.v \
+  --input archive/proofs/coq/common/CNO.v \
   --from Coq \
   --to Lean4 \
   --output proofs/lean4/CNO_translated.lean
 
 # Verify translation is equivalent
 ./tools/echidna/neurosym/target/release/echidna diff \
-  --proof1 proofs/coq/common/CNO.v \
+  --proof1 archive/proofs/coq/common/CNO.v \
   --proof2 proofs/lean4/CNO_translated.lean
 ```
 
diff --git a/Justfile b/Justfile
index 3d86215..e154ba0 100644
--- a/Justfile
+++ b/Justfile
@@ -21,6 +21,11 @@ default:
 build-all: build-agda build-idris
     @echo "✓ All builds complete"
 
+# Register the pinned Agda standard library (v1.7.3) — same script CI runs.
+# Writes $AGDA_DIR/libraries and defaults (AGDA_DIR defaults to ~/.agda).
+provision-agda-stdlib:
+    bash scripts/provision-agda-stdlib.sh
+
 # Build Agda proofs (CNO + OND + EchoBridge, 4 modules, --safe --without-K)
 build-agda:
     @echo "Building Agda proofs..."
diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 9c86a6b..2a5a3b2 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -14,7 +14,7 @@ by prover, and is explicit about which axioms remain and why.
 .2026-07-07 — both pillars machine-checked across six provers (HISTORICAL since 2026-10-10)
 ====
 *Historical (superseded by the 2026-10-10 archive ruling below):* all six
-provers were reproduced in this environment via `proofs/verify-all-provers.sh`
+provers were reproduced in this environment via `proofs/verify-all-provers.sh` (now archived as `archive/proofs/verify-all-provers.six-prover.sh`)
 (`ALL-PROVERS-GREEN`): *Coq, Agda, Lean 4 (+Mathlib), Z3, Isabelle/HOL, Mizar*,
 plus the *Idris 2* ABI. Today only Agda, Z3 (bounded) and the Idris 2 ABI are
 active — see the canonical table below. Both the CNO and OND pillars were covered.
@@ -23,7 +23,7 @@ and Mizar printed "skipped" and the gate could say GREEN on four of six), and Z3
 verdicts are compared with the `; expect sat|unsat` annotation on every `(check-sat)`
 (`proofs/z3/verify.sh`). Since 2026-09-23 the gate also runs the Coq `Print Assumptions` audit and
 its `--control` after the build, so a theorem resting on an axiom, or an audit that can no
-longer say no, turns it red. `proofs/tests/gate-selftest.sh` proves both gates turn red for
+longer say no, turns it red. The six-prover self-test (now `archive/proofs/tests/gate-selftest.six-prover.sh`) proved both gates turn red for
 each absent or failing prover, for each verdict mutant and for both audit mutants (16 cases, run in CI).
 ====
 
@@ -68,7 +68,7 @@ dropped, and axiom dependence is tracked per row.
 
 | `proofs/z3/` — `ond/OND_checks.smt2` via `proofs/z3/verify.sh`
 | ACTIVE as bounded-check solver (CI `z3` job)
-| `tested-only` — bounded SMT checks, no proof grade; every `(check-sat)` carries a `; expect sat|unsat` annotation. Receipt reproduced in this sandbox 2026-11-01 (`z3` 4.16.0, `Z3-CHECK OK`, sat/unsat/sat) — see receipts below
+| `tested-only` — bounded SMT checks, no proof grade; every `(check-sat)` carries a `; expect sat|unsat` annotation. Receipt reproduced in this sandbox 2026-11-01 (`z3` 4.16.0, `Z3-CHECK OK`, sat/unsat/sat). The 2026-11-09 OND-3 rewrite expects 5 verdicts, sat/unsat/sat/sat/sat, observed with `z3` 4.8.12 — see receipts below
 | Bounds: finite/bounded programs under a finite declared `O`; not a general proof
 
 | `src/abi/` + `absolute-zero-abi.ipkg` (Idris 2)
@@ -186,6 +186,29 @@ reported as passing: the Agda `--safe --without-K` checks, the
 build remain CI receipts (`proofs.yml`: `agda`, `z3`, `idris` jobs), not
 sandbox receipts. Archived provers stay archived and unexecuted.
 
+=== Reproduction receipts (this environment, 2026-11-09)
+
+Working tree on branch `claude/ephapax-architecture-plan-gzyctr` over `cbe9ae9`.
+
+* *Z3 — REPRODUCED HERE.* `Z3 version 4.8.12 - 64 bit`, on the rewritten
+OND-3 check.
+`z3 proofs/z3/ond/OND_checks.smt2` prints `sat unsat sat sat sat` (+ the OND-5
+model `s1 = 2, s2 = 3, pub = 0`), exit 0; `bash proofs/z3/verify.sh` →
+`ok: ond/OND_checks.smt2 — 5 (check-sat) verdict(s) match`, `Z3-CHECK OK`, exit 0.
+Mutation check: replacing `writer_step` by a step that copies the secret to
+the output cell turns the OND-3 dir 2 verdict from `unsat` to `sat`, so the
+check is no longer vacuous (see the Z3 section).
+* *Agda — REPRODUCED HERE, on the `CNO.agda` before #199* (so not a receipt for
+the current module). `Agda version 2.6.3`, stdlib registered by
+`scripts/provision-agda-stdlib.sh` (agda-stdlib `v1.7.3` =
+`0817da6877aa045932221134913d8511caa78d97`, into a scratch `AGDA_DIR`).
+`agda --safe --without-K` on `CNO.agda`, `OND.agda`, `EchoBridgeScaffold.agda`,
+`EchoBridgeCNO.agda`: exit 0 each. `agda --safe --without-K --cubical-compatible`
+on the same four: exit 0 each. (The stdlib modules themselves were checked under
+the stdlib's own pragmas, not re-checked under `--cubical-compatible`.)
+* *Gate self-test.* `bash proofs/tests/gate-selftest.sh` → `GATE-SELFTEST OK: 27/27 cases`.
+* *Idris 2* — not run here.
+
 === Role of this repository (consumer, not estate-wide ground truth)
 
 absolute-zero is a *consumer and domain formalisation*: it applies standard
@@ -212,11 +235,11 @@ Isabelle/HOL and Mizar (archived 2026-10-10) and *active* only for Agda, Z3
 is the canonical summary.
 ====
 
-== Coq — VERIFIED (this environment)
+== Coq — ARCHIVED (historical receipt, 2026-07-07; not built or gated since 2026-10-10)
 
 * `coqc` **8.18.0**; clean build from scratch (all `.vo`/`.glob` deleted first),
   via `coq_makefile -f _CoqProject` over **14/14 theories → zero errors**.
-* Reproduce: `cd proofs/coq && coq_makefile -f _CoqProject -o Makefile.all && make -f Makefile.all -j`.
+* Reproduce (historical; the tree is archived): `cd archive/proofs/coq && coq_makefile -f _CoqProject -o Makefile.all && make -f Makefile.all -j`.
 
 [cols="1,3",options="header"]
 |===
@@ -277,9 +300,9 @@ of these, each documented in-file with its blocker:
 These are the analogue of the OND-6 research fork: openly labelled, not silently
 assumed. `Print Assumptions` on each of the 17 theorems this document names in backticks
 prints `Closed under the global context` — no stdlib axiom and no project axiom (measured
-2026-09-23, Coq 8.18). That is CI-gated: `proofs/coq/audit/Assumptions.v` lists the 17 and
-`proofs/coq/check-assumptions.sh` (Coq job of `proofs.yml`, and the canonical
-`proofs/verify-all-provers.sh` gate since 2026-09-23) fails on any `Axioms:` block or a
+2026-09-23, Coq 8.18). That WAS CI-gated until the 2026-10-10 archive ruling (no longer run): `archive/proofs/coq/audit/Assumptions.v` lists the 17 and
+`archive/proofs/coq/check-assumptions.sh` (formerly the Coq job of `proofs.yml`, and the then-canonical
+`proofs/verify-all-provers.sh` gate, now `archive/proofs/verify-all-provers.six-prover.sh`) failed on any `Axioms:` block or a
 missing line; its `--control` mode proves the gate bites by requiring that
 `landauer_limit_positive`, which rests on `kB_positive`, is rejected. The wider tree is not
 closed — 109 of 182 top-level theorems are; the other 73 rest on stdlib classical axioms
@@ -287,7 +310,7 @@ and/or the tagged parameters — see #171 for the census and the tag-grammar wor
 
 === Reversibility <-> CNO bridge (2026-07-16, the theorem MAA cites)
 
-`proofs/coq/common/CNO.v` now carries the bridge between `reversible` and the
+`archive/proofs/coq/common/CNO.v` now carries the bridge between `reversible` and the
 "composes to a no-op" characterisation the MAA framework (aletheia) cites. All five
 new results are **`Closed under the global context` (zero axioms)**:
 
@@ -316,7 +339,7 @@ whereas the contract is two-sided. The in-file section header documents all thre
 This is a genuine statement-shape finding: it tells the aletheia contract to be
 stated two-sided and `=st=`-relative, not a proof dodged.
 
-*Lean mirror — `proofs/lean4/CNOBridge.lean` (UNVERIFIED in this environment).*
+*Lean mirror — `archive/proofs/lean4/CNOBridge.lean` (UNVERIFIED in this environment).*
 A functional-model mirror of the five bridge results was written for Lean 4, but
 it could **not** be machine-checked here: the Lean toolchain and Mathlib cache
 download from GitHub release assets, which the egress policy blocked (HTTP 403).
@@ -328,9 +351,9 @@ total function and `ProgramState.eq` includes the PC), a stronger/cleaner form
 than the Coq `=st=`-relative statement — a disclosed cross-model difference, not
 a claim of literal equivalence.
 
-== OND — VERIFIED (this environment), the disclosure pillar
+== OND — the disclosure pillar (Coq/Lean legs ARCHIVED; Agda + Z3 legs active)
 
-`proofs/coq/ond/OND.v` discharges roadmap obligations *OND-1..OND-5* with **zero
+`archive/proofs/coq/ond/OND.v` discharges roadmap obligations *OND-1..OND-5* with **zero
 axioms** — every theorem is `Closed under the global context`:
 
 * OND-1 `is_OND O o` — nullity parameterised by an observation model `O` over an
@@ -342,7 +365,7 @@ axioms** — every theorem is `Closed under the global context`:
 * OND-5 — a non-composition counterexample (two ONDs whose composite leaks by
   state-chaining).
 
-Mirrored in *Lean 4* (`proofs/lean4/OND.lean`), *Agda* (`proofs/agda/OND.agda`),
+Mirrored in *Lean 4* (`archive/proofs/lean4/OND.lean`), *Agda* (`proofs/agda/OND.agda`),
 and *Z3* (`proofs/z3/ond/OND_checks.smt2`, the bounded/finite instances). OND-7's
 residue register carries its first real instance
 (`proofs/residue/ct_select.residue`). *OND-6* (conditional composition, research
@@ -356,17 +379,21 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`.
   2026-09-23 CI checked only the first two and `EchoBridgeCNO.agda` had no pragma of its
   own. The EchoBridge modules take **funext as an explicit hypothesis**
   (not a global `postulate`); `OND.agda` uses zero postulates.
+* Standard library: agda-stdlib `v1.7.3` (commit `0817da6`), registered by
+  `scripts/provision-agda-stdlib.sh` (`just provision-agda-stdlib`) — the same
+  script the CI `agda` job runs; it fails if the tag no longer resolves to the
+  pinned commit. Set `AGDA_DIR` to keep it out of `~/.agda`.
 
-== Lean 4 — VERIFIED (this environment)
+== Lean 4 — ARCHIVED (historical receipt; not built or gated since 2026-10-10)
 
 * Toolchain `leanprover/lean4:v4.16.0` with Mathlib `@ v4.16.0`; `lake exe cache get`
   + `lake build` → **build completed successfully**. Covers the CNO libraries and the
-  new `OND` library (`proofs/lean4/OND.lean`, core-Lean only, zero `sorry`).
-* **Mathlib-free core is CI-gated (2026-09-22):** `proofs/lean4/check-core.sh` (job
+  new `OND` library (`archive/proofs/lean4/OND.lean`, core-Lean only, zero `sorry`).
+* **Mathlib-free core WAS CI-gated (2026-09-22 until the 2026-10-10 archive ruling; the `lean` job no longer exists):** `archive/proofs/lean4/check-core.sh` (job
   `lean` in `.github/workflows/proofs.yml`; toolchain from `lean-toolchain`, elan
   fetched as a checksum-verified tarball, zero third-party actions) compiles `CNO`,
   `OND`, `CNOCategory`, `CNOBridge`, `FilesystemCNO`, `LambdaCNO` with plain `lean`
-  and runs `proofs/lean4/AxiomAudit.lean`: 96 `#guard_msgs` pinning every axiom
+  and runs `archive/proofs/lean4/AxiomAudit.lean`: 96 `#guard_msgs` pinning every axiom
   signature, the three occupancy predicates in full, the #125 derivations as
   negative controls, and `#print axioms` for every theorem (no `sorryAx` anywhere).
   `just verify-lean-core` runs the same script locally.
@@ -375,7 +402,7 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`.
   `rename_inverse` without the occupancy preconditions of the Coq lemmas they mirror;
   with `mkdir_idempotent` and `mkdir_not_identity` that proved `False`. They now
   carry `noDirAt` / `noFileAt` / `noEntryAt`, mirrored verbatim from
-  `proofs/coq/filesystem/FilesystemCNO.v`, and the unconditional statement is refuted
+  `archive/proofs/coq/filesystem/FilesystemCNO.v`, and the unconditional statement is refuted
   in-file (`unconditional_mkdir_rmdir_inverse_is_false`). `LambdaCNO.lean` carried the
   unrestricted `eta_equivalence` axiom (false as stated, the same `LVar 5`
   counterexample the Coq side documents above); it is now the proved
@@ -392,28 +419,44 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`.
   identical to the pre-#174 commit and to the last green `main` run before #174).
   #167 stays open with finishing the port as its own acceptance criterion.
 
-== Z3 — VERIFIED (this environment)
-
-* `z3` 4.16.0 on `proofs/z3/ond/OND_checks.smt2`: the OND-3 timing-leak witness is
-  `sat`, `writer`-is-OND is `unsat` (no secret distinguishes it), and the OND-5
-  composite leak is `sat` with a concrete model — the "decidable for bounded
-  programs" demonstration.
-
-== Isabelle/HOL — VERIFIED (this environment)
-
-* `Isabelle2025-2`, session `AbsoluteZero-CNO` (`proofs/isabelle/ROOT`): `CNO.thy`
+== Z3 — ACTIVE, bounded checks (`tested-only`)
+
+* *Historical (2026-07-07):* `z3` 4.16.0 on `proofs/z3/ond/OND_checks.smt2`: the
+  OND-3 timing-leak witness is `sat`, `writer`-is-OND is `unsat`, and the OND-5
+  composite leak is `sat` with a concrete model. *Correction (2026-11-09):* the
+  `writer`-is-OND block then asserted `(not (and (= 0 0) (= 1 1)))` — the writer's
+  observables written down as constants — which is `unsat` for any program, so
+  that `unsat` checked nothing about the writer.
+* *Current (2026-11-09, z3 4.8.12, 5 verdicts `sat unsat sat sat sat`):* the
+  OND-3 dir 2 block now models `writer_op` per `archive/proofs/coq/ond/OND.v`:
+  memory as `(Array Int Int)`, `inj s p`, `writer_step m = store m 0 7`,
+  `writer_time = 1`, and the `O_all` observable (output cell 2, time) *computed*
+  from them; asserting the observables differ for two secrets at the same public
+  input is `unsat` (writer is OND under `O_all`). A control block runs the same
+  query on a writer that copies the secret to the output cell (`sat`), and a
+  third block witnesses `writer_not_null` (`sat`). Mutating `writer_step` to leak
+  flips the main verdict to `sat`.
+* *Remaining scope limit:* the OND-3 dir 1 block (`time_leaky secret = secret`)
+  and the OND-5 block (`p_out = 0`, `comp_out = secret`) still state the
+  observables directly rather than computing them from step functions; they are
+  hand transcriptions of the OND.v results, not independent checks of the
+  composition.
+
+== Isabelle/HOL — ARCHIVED (historical receipt; not built or gated since 2026-10-10)
+
+* `Isabelle2025-2`, session `AbsoluteZero-CNO` (`archive/proofs/isabelle/ROOT`): `CNO.thy`
   (repaired — the reserved-keyword `value` type was renamed and the failing `nop`/`step`
   lemmas fixed) and `OND.thy` (new, OND-1..5) build with no `sorry`/`oops`.
 
-== Mizar — VERIFIED (this environment)
+== Mizar — ARCHIVED (historical receipt; not built or gated since 2026-10-10)
 
-* Mizar `8.1.15`; `accom CNO && verifier CNO` on `proofs/mizar/CNO.miz` completes
+* Mizar `8.1.15`; `accom CNO && verifier CNO` on `archive/proofs/mizar/CNO.miz` completes
   with an **empty `CNO.err`** (zero errors). `MIZFILES` points at the bundled MML.
   The original article was machine-generated and unverifiable (277 errors); it was
   *rewritten* into a genuine article (StateSpace = pair of `Funcs(NAT,NAT)`;
   state-preserving / pure / reversible / terminating / thermo-reversible attributes;
   12 proved theorems incl. composition with a real inverse construction). Requires the
-  committed private vocabulary `proofs/mizar/dict/cno.voc` (lowercase filename, needed
+  committed private vocabulary `archive/proofs/mizar/dict/cno.voc` (lowercase filename, needed
   on Linux). Verifier build artifacts are git-ignored.
 
 == Idris 2 — VERIFIED (this environment), the ABI boundary
@@ -430,9 +473,13 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`.
 * Multi-prover, not cross-prover *equivalence* — each prover checks its own
   formalisation of the two pillars.
 * "Verified here" = a reproduced compiler/checker run in this environment, not a
-  reading of in-file comments. Reproduce everything with
-  `proofs/verify-all-provers.sh`.
-* Axiom census (machine-generated via `proofs/coq/census-assumptions.sh`):
+  reading of in-file comments. Reproduce the active stack with
+  `proofs/verify-active-provers.sh` (after `scripts/provision-agda-stdlib.sh`);
+  the former six-prover gate is archived as
+  `archive/proofs/verify-all-provers.six-prover.sh` and is not run.
+* The Coq census and tag-grammar bullets below describe the archived tree
+  (`archive/proofs/coq/`); their scripts are no longer run.
+* Axiom census (machine-generated via `archive/proofs/coq/census-assumptions.sh`):
   of 182 top-level theorems across the 14 theories, exactly **109 are closed under
   the global context** (zero axioms), and 73 rest on Coq stdlib classical axioms
   (`ClassicalDedekindReals.*`, `FunctionalExtensionality.*`, `Classical_Prop.classic`,
@@ -443,11 +490,11 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`.
   generated driver fail outright instead of censusing it; the table now shows
   `Malbolge.MalbolgeCore | 7 | 7 | 0`). A directory with no `-R` binding is a hard
   census failure, never a silent skip.
-* All top-level declarations are verified by `proofs/coq/check-axiom-tags.sh` to carry
+* All top-level declarations are verified by `archive/proofs/coq/check-axiom-tags.sh` to carry
   a unified tag grammar: `(* AXIOM: [METAL-BOUNDARY] ... *)` for physical constants
   and laws, or `(* AXIOM: [CLASS-A] ... *)` for provable-in-principle mathematics.
   The two former unsound declarations in `StatMechBasis.v` (`prob_nonneg` and
   `prob_normalized`, which claimed Kolmogorov properties over raw unconstrained
   functions `ProgramState -> R`) have been deleted; zero theorems depend on either.
 * The 17 named headline theorems remain 100% closed under the global context (zero axioms,
-  CI-gated by `check-assumptions.sh`).
+  formerly CI-gated by `archive/proofs/coq/check-assumptions.sh`; not run since the 2026-10-10 archive ruling).
diff --git a/README.adoc b/README.adoc
index b1094ba..bf5b625 100644
--- a/README.adoc
+++ b/README.adoc
@@ -124,7 +124,7 @@ Core proofs
 --
 Malbolge / Brainfuck / Whitespace CNO verification
 *Novel application*
-`+interpreters/+`, `+proofs/coq/malbolge/+`
+`+interpreters/+`, `+archive/proofs/coq/malbolge/+` (archived)
 --
 
 |===
@@ -235,26 +235,32 @@ is recorded, the Z3 checks are `tested-only` (bounded), and OND-6 is
 
 [verse]
 --
-`+proofs/coq/+`
-Coq proofs: CNO framework, Malbolge, physics, category theory, lambda, quantum, filesystem, OND
+`+proofs/agda/+`
+Active Agda proofs: CNO, OND, EchoBridge (checked in CI, `--safe --without-K`)
 --
 
 [verse]
 --
-`+proofs/lean4/+`
-Lean 4 mirrors of CNO and OND modules
+`+proofs/z3/+`
+Active Z3 bounded checks (expect-annotated; `tested-only`)
 --
 
 [verse]
 --
-`+proofs/agda/+`, `+proofs/z3/+`, `+proofs/isabelle/+`, `+proofs/mizar/+`
-Additional prover artefacts (Agda checked in CI; others generated but not yet run)
+`+archive/proofs/coq/+`
+ARCHIVED 2026-10-10 (not built or gated): Coq proofs: CNO framework, Malbolge, physics, category theory, lambda, quantum, filesystem; OND module in `+archive/proofs/coq/ond/+`
 --
 
 [verse]
 --
-`+proofs/ond/+`
-OND Coq module (OND-1..5 proved, zero axioms)
+`+archive/proofs/lean4/+`
+ARCHIVED 2026-10-10 (not built or gated): Lean 4 mirrors of CNO and OND modules
+--
+
+[verse]
+--
+`+archive/proofs/isabelle/+`, `+archive/proofs/mizar/+`
+ARCHIVED 2026-10-10 (not built or gated): Isabelle/HOL and Mizar artefacts
 --
 
 [verse]
@@ -321,6 +327,6 @@ Prose documentation is licensed under CC-BY-SA-4.0; see
 
 [verse]
 --
-`+proofs/coq/+`
-Coq proofs: CNO framework, Malbolge, physics, category theory, lambda, quantum, filesystem, OND
+`+archive/proofs/coq/+`
+ARCHIVED 2026-10-10 (not built or gated): Coq proofs: CNO framework, Malbolge, physics, category theory, lambda, quantum, filesystem, OND
 --
diff --git a/ROADMAP.adoc b/ROADMAP.adoc
index df073c8..89838d7 100644
--- a/ROADMAP.adoc
+++ b/ROADMAP.adoc
@@ -42,21 +42,25 @@ See `PROOF-STATUS.adoc` for the canonical active-vs-archived proof-status table.
 
 === What genuinely verifies
 
-* *Coq (reproduced):* **14 theories** compile from scratch under `coqc 8.18.0`
+The Coq, Lean 4, Isabelle/HOL and Mizar entries below are *historical receipts
+(2026-07-07)*: those trees were ARCHIVED on 2026-10-10 under `archive/proofs/` and
+are no longer built or gated. Agda, Z3 (bounded) and the Idris 2 ABI are active.
+
+* *Coq (reproduced 2026-07-07; ARCHIVED):* **14 theories** compiled from scratch under `coqc 8.18.0`
   (`coq_makefile -f _CoqProject`) — `common`, `category`, `quantum`, `lambda`,
   `filesystem`, `physics`, `malbolge`, and the new `ond`. Both pillars.
-* *OND pillar (reproduced):* `proofs/coq/ond/OND.v` proves **OND-1..5** with
+* *OND pillar (reproduced):* the archived `archive/proofs/coq/ond/OND.v` proved **OND-1..5** with
   **zero axioms** (every theorem `Closed under the global context`); mirrored in
   Lean 4, Agda, and Z3.
 * *Agda (reproduced):* `CNO.agda`, `OND.agda`, `EchoBridgeCNO.agda` type-check
   under `agda 2.6.3` (`--safe --without-K`); funext is an *explicit hypothesis*.
-* *Lean 4 (reproduced):* `lake build` green with Mathlib — CNO libraries + the
-  new `OND` library (`proofs/lean4/OND.lean`, 0 `sorry`).
+* *Lean 4 (reproduced 2026-07-07; ARCHIVED):* `lake build` was green with Mathlib — CNO libraries + the
+  new `OND` library (`archive/proofs/lean4/OND.lean`, 0 `sorry`).
 * *Z3 (reproduced):* CNO checks + OND bounded instances (`proofs/z3/ond/OND_checks.smt2`).
-* *Isabelle/HOL (reproduced):* session `AbsoluteZero-CNO` — `CNO.thy` (repaired)
-  + `OND.thy` build under Isabelle2025-2, 0 `sorry`.
-* *Mizar (reproduced):* `CNO.miz` rewritten into a genuine 12-theorem article;
-  `accom`+`verifier` → empty `CNO.err` (needs `proofs/mizar/dict/cno.voc`).
+* *Isabelle/HOL (reproduced 2026-07-07; ARCHIVED):* session `AbsoluteZero-CNO` — `CNO.thy` (repaired)
+  + `OND.thy` built under Isabelle2025-2, 0 `sorry`.
+* *Mizar (reproduced 2026-07-07; ARCHIVED):* `CNO.miz` rewritten into a genuine 12-theorem article;
+  `accom`+`verifier` → empty `CNO.err` (needs `archive/proofs/mizar/dict/cno.voc`).
 * *Idris 2 ABI (reproduced):* `absolute-zero-abi.ipkg` builds clean.
 * *Rust interpreters:* Brainfuck and Whitespace interpreters are real.
 
@@ -77,8 +81,10 @@ See `PROOF-STATUS.adoc` for the canonical active-vs-archived proof-status table.
   coinductive/step-indexed β non-termination argument).
 | OND-6 | Open by design | The conditional-composition theorem — research
   capstone; OND-1..5 landed, so the pillar is in honest, publishable shape.
-| CI proof verification | Missing | No workflow yet runs the provers; the local
-  gate `proofs/verify-all-provers.sh` is the reproducible source of truth.
+| CI proof verification | Active stack only | The CI `agda`, `z3` and `idris` jobs
+  (`proofs.yml`) check the active stack; `proofs/verify-active-provers.sh` is the local gate for the active
+  stack. The former six-prover gate is archived
+  (`archive/proofs/verify-all-provers.six-prover.sh`) and not run.
 | Paper | Draft stub | `papers/.latex/main.tex` is a lone draft.
 | Tests | Empty placeholder | `tests/` holds a README only.
 |===
@@ -137,7 +143,7 @@ coordinates as a pinned submodule. The theorem MAA actually cites is the
 *general reversibility biconditional*.
 
 * [x] *Reversibility <-> CNO bridge — landed in Coq (2026-07-16, zero axioms).*
-  `proofs/coq/common/CNO.v` proves the forward direction of the aletheia contract
+  `archive/proofs/coq/common/CNO.v` (archived 2026-10-10) proves the forward direction of the aletheia contract
   (`reversible_bridge_forward`: a two-sided inverse makes both composites
   `cno_equiv _ []`) and the backward direction up to `=st=`
   (`reversible_bridge_backward_upto`), via the core lemma
diff --git a/docs/COOKBOOK.adoc b/docs/COOKBOOK.adoc
index ed13ae2..36edcbe 100644
--- a/docs/COOKBOOK.adoc
+++ b/docs/COOKBOOK.adoc
@@ -13,6 +13,18 @@ v1.0, 2025-11-22
 
 This cookbook provides practical, step-by-step instructions for working with the *Absolute Zero* project — a formal verification framework for Certified Null Operations (CNOs).
 
+[IMPORTANT]
+.Archive notice (2026-10-10)
+====
+The Coq, Lean 4, Isabelle/HOL and Mizar trees this cookbook was written around
+were archived on 2026-10-10 under `archive/proofs/` and are no longer built or
+gated. The active stack is Agda (`proofs/agda/`) + Z3 bounded checks
+(`proofs/z3/`) + the Idris 2 ABI; run `just verify`
+(`proofs/verify-active-provers.sh`). Paths below that name the archived provers
+point at `archive/proofs/…`; the workflows and status figures for those provers
+are historical. See `PROOF-STATUS.adoc` for the canonical status table.
+====
+
 === What This Project Does
 
 Absolute Zero formally proves that certain programs provably compute *nothing*:
@@ -30,11 +42,11 @@ Absolute Zero formally proves that certain programs provably compute *nothing*:
 
 |Coq 8.19
 |Core CNO theory, physics proofs
-|70% complete
+|ARCHIVED 2026-10-10 (historical: 70% complete)
 
 |Lean 4
 |Alternative verification, category theory
-|66% complete
+|ARCHIVED 2026-10-10 (historical: 66% complete)
 
 |Z3 4.13
 |SMT-based automated verification
@@ -46,7 +58,7 @@ Absolute Zero formally proves that certain programs provably compute *nothing*:
 
 |Isabelle/HOL
 |Higher-order logic
-|100% (foundational)
+|ARCHIVED 2026-10-10 (historical: 100% foundational)
 |===
 
 == Quick Start
@@ -158,13 +170,13 @@ If neither `just` nor Oil shell is available:
 [source,bash]
 ----
 # Build Coq proofs
-cd proofs/coq/common && coqc CNO.v
+cd archive/proofs/coq/common && coqc CNO.v
 cd ../physics && coqc -R ../common CNO StatMech.v
 cd ../physics && coqc -R ../common CNO LandauerDerivation.v
 cd ../quantum && coqc -R ../common CNO QuantumMechanicsExact.v
 
 # Build Lean 4 proofs
-cd proofs/lean4 && lake build
+cd archive/proofs/lean4 && lake build
 
 # Verify Z3 specifications
 z3 proofs/z3/cno_properties.smt2
@@ -180,7 +192,7 @@ npm install && npm run build
 ==== Project Structure
 [source,text]
 ----
-proofs/coq/
+archive/proofs/coq/
 ├── common/
 │   └── CNO.v              # Core CNO theory (Phase 1)
 ├── physics/
@@ -233,10 +245,10 @@ just verify-coq
 [source,bash]
 ----
 # How many theorems are incomplete?
-grep -r "Admitted\." proofs/coq/ | wc -l
+grep -r "Admitted\." archive/proofs/coq/ | wc -l
 
 # Where are they?
-grep -r "Admitted\." proofs/coq/
+grep -r "Admitted\." archive/proofs/coq/
 
 # Proof statistics
 just proof-status
@@ -247,7 +259,7 @@ just proof-status
 ==== Project Structure
 [source,text]
 ----
-proofs/lean4/
+archive/proofs/lean4/
 ├── lakefile.lean          # Build configuration
 ├── CNO.lean               # Core CNO theory
 ├── StatMech.lean          # Statistical mechanics
@@ -280,7 +292,7 @@ theorem my_new_theorem (p : CNO.Program) :
 
 [source,bash]
 ----
-cd proofs/lean4
+cd archive/proofs/lean4
 
 # Update dependencies
 lake update
@@ -329,7 +341,7 @@ z3 proofs/z3/cno_properties.smt2
 
 *Status*: All proofs complete, 0 `Admitted`
 
-Key theorems in `proofs/coq/common/CNO.v`:
+Key theorems in `archive/proofs/coq/common/CNO.v`:
 
 [cols="1,2"]
 |===
@@ -531,7 +543,7 @@ Valence Shell operations can be proven as CNOs:
 [source,coq]
 ----
 (* Precondition: no directory already at [path] — without it the law is false
-   (repeat mkdir is idempotent), see proofs/coq/filesystem/FilesystemCNO.v and
+   (repeat mkdir is idempotent), see archive/proofs/coq/filesystem/FilesystemCNO.v and
    absolute-zero#125. *)
 Theorem mkdir_rmdir_is_cno :
   forall (path : Path) (fs : Filesystem),
@@ -548,7 +560,7 @@ Theorem mkdir_rmdir_is_cno :
 *Solution*:
 [source,bash]
 ----
-cd proofs/coq/common && coqc CNO.v
+cd archive/proofs/coq/common && coqc CNO.v
 ----
 
 *Problem*: `Admitted` statements
@@ -562,7 +574,7 @@ cd proofs/coq/common && coqc CNO.v
 *Solution*:
 [source,bash]
 ----
-cd proofs/lean4
+cd archive/proofs/lean4
 lake update
 ----
 
@@ -671,10 +683,10 @@ See `FORMAL_ANALYSIS_PHASE1.md` for complete analysis.
 |`VERIFICATION_RESULTS.md`
 |Latest verification results
 
-|`proofs/coq/common/CNO.v`
+|`archive/proofs/coq/common/CNO.v`
 |Core Coq proofs (Phase 1)
 
-|`proofs/lean4/CNO.lean`
+|`archive/proofs/lean4/CNO.lean`
 |Core Lean 4 proofs
 
 |`proofs/z3/cno_properties.smt2`
diff --git a/docs/ECOSYSTEM-CONNECTIONS.adoc b/docs/ECOSYSTEM-CONNECTIONS.adoc
index a8b3508..94a2621 100644
--- a/docs/ECOSYSTEM-CONNECTIONS.adoc
+++ b/docs/ECOSYSTEM-CONNECTIONS.adoc
@@ -19,8 +19,8 @@ sibling projects in the hyperpolymath estate.
 *Connection:*
 JanusKey relies on the mathematical guarantee that filesystem actions carry sufficient
 inversion data to guarantee exact state restoration. Absolute Zero's
-`FilesystemCNO` (`proofs/coq/filesystem/FilesystemCNO.v` and `proofs/lean4/FilesystemCNO.lean`)
-provides the formal verification kernel for JanusKey:
+`FilesystemCNO` (`archive/proofs/coq/filesystem/FilesystemCNO.v` and `archive/proofs/lean4/FilesystemCNO.lean`,
+both archived 2026-10-10 and no longer built or gated) provided the formal verification kernel for JanusKey:
 
 * `mkdir_rmdir_inverse` and `create_unlink_inverse` verify atomic create/destroy inverse pairs under occupancy preconditions (`noDirAt`, `noFileAt`).
 * `read_write_identity` and `chmod_identity` verify that idempotent updates cause zero net state delta.
@@ -41,7 +41,7 @@ provides the formal verification kernel for JanusKey:
 *Domain:* Type-theoretic verification engine and categorical foundations for database query validation.
 
 *Connection:*
-* `proofs/coq/category/CNOCategory.v` and `proofs/lean4/CNOCategory.lean` prove that CNOs correspond to identity morphisms in the category of state transitions.
+* `archive/proofs/coq/category/CNOCategory.v` and `archive/proofs/lean4/CNOCategory.lean` (archived 2026-10-10, no longer built or gated) proved that CNOs correspond to identity morphisms in the category of state transitions.
 * Functors preserving CNOs guarantee that query transformations do not introduce side effects or alter transactional consistency invariants.
 
 == 4. Robodog Defensive Systems Lab (`hyperpolymath/robodog-defensive-systems-lab`)
diff --git a/docs/JUSTFILE-COOKBOOK.adoc b/docs/JUSTFILE-COOKBOOK.adoc
index 60d83d6..dbd34fb 100644
--- a/docs/JUSTFILE-COOKBOOK.adoc
+++ b/docs/JUSTFILE-COOKBOOK.adoc
@@ -13,7 +13,7 @@ v1.0, 2025-11-22
 
 This cookbook documents all `just` recipes in the Absolute Zero project. Every recipe is explained with examples, flags, and common usage patterns.
 
-WARNING: `just --list` is authoritative. The Appendix recipe list and dependency graph were regenerated from it on 2026-10-01. Nine per-recipe sections below describe recipes the Justfile no longer defines: `build-z3`, `check-tools`, `clean-all`, `docs-adoc`, `docs-all`, `docs-proof-stats`, `install-help`, `loc` and `quick-check`. Treat them as historical until this cookbook is rewritten.
+WARNING: `just --list` is authoritative. The Appendix recipe list and dependency graph were regenerated from it on 2026-10-01. Nine per-recipe sections below describe recipes the Justfile no longer defines: `build-z3`, `check-tools`, `clean-all`, `docs-adoc`, `docs-all`, `docs-proof-stats`, `install-help`, `loc` and `quick-check`. Treat them as historical until this cookbook is rewritten. The `build-coq`, `build-lean` and `verify-coq` sections are historical too: the Coq, Lean 4, Isabelle/HOL and Mizar trees were archived on 2026-10-10 under `archive/proofs/` and are no longer built or gated. Paths in those sections point at the archived trees (sample outputs are left as originally written). The active gate is `just verify` (`proofs/verify-active-provers.sh`: Agda + Z3 bounded + Idris 2 ABI).
 
 === Quick Reference
 
@@ -30,9 +30,9 @@ just ci                 # Run full CI pipeline
 
 === build-all
 
-Build all proof systems and interpreters.
+Build the active provers and the Idris ABI.
 
-*Dependencies*: build-coq, build-lean, build-agda, build-isabelle, build-mizar, build-idris
+*Dependencies*: build-agda, build-idris
 
 [source,bash]
 ----
@@ -40,12 +40,11 @@ just build-all
 ----
 
 *What it does*:
-1. Compiles Coq proofs
-2. Compiles Lean 4 proofs
-3. Compiles Agda proofs
-4. Builds Isabelle/HOL proofs
-5. Checks Mizar proofs
-6. Builds the Idris2 ABI
+1. Compiles the Agda proofs (`build-agda`)
+2. Builds the Idris2 ABI (`build-idris`)
+
+Coq, Lean 4, Isabelle/HOL and Mizar were part of this recipe until the
+2026-10-10 archive ruling; they are archived under `archive/proofs/` and not built.
 
 *Exit codes*:
 - `0`: All builds successful
@@ -61,11 +60,11 @@ just build-coq
 ----
 
 *Build order*:
-1. `proofs/coq/common/CNO.v` (core definitions)
-2. `proofs/coq/physics/StatMech.v` (requires CNO)
-3. `proofs/coq/physics/LandauerDerivation.v` (requires CNO)
-4. `proofs/coq/quantum/QuantumMechanicsExact.v` (requires CNO)
-5. `proofs/coq/malbolge/MalbolgeCore.v` (requires CNO)
+1. `archive/proofs/coq/common/CNO.v` (core definitions)
+2. `archive/proofs/coq/physics/StatMech.v` (requires CNO)
+3. `archive/proofs/coq/physics/LandauerDerivation.v` (requires CNO)
+4. `archive/proofs/coq/quantum/QuantumMechanicsExact.v` (requires CNO)
+5. `archive/proofs/coq/malbolge/MalbolgeCore.v` (requires CNO)
 
 *Flags used*:
 - `-R ../common CNO`: Maps `common` directory to `CNO` namespace
@@ -95,7 +94,7 @@ just build-lean
 ----
 
 *What it does*:
-1. Changes to `proofs/lean4/`
+1. Changes to `archive/proofs/lean4/`
 2. Runs `lake build`
 3. Compiles all `.lean` files
 4. Downloads Mathlib dependencies if needed
@@ -103,7 +102,7 @@ just build-lean
 *First-time setup*:
 [source,bash]
 ----
-cd proofs/lean4
+cd archive/proofs/lean4
 lake update  # Update dependencies
 lake build   # Build everything
 ----
@@ -398,11 +397,11 @@ just clean-coq
 *Files removed*:
 [source,bash]
 ----
-find proofs/coq -name "*.vo" -delete
-find proofs/coq -name "*.vok" -delete
-find proofs/coq -name "*.vos" -delete
-find proofs/coq -name "*.glob" -delete
-find proofs/coq -name ".*.aux" -delete
+find archive/proofs/coq -name "*.vo" -delete
+find archive/proofs/coq -name "*.vok" -delete
+find archive/proofs/coq -name "*.vos" -delete
+find archive/proofs/coq -name "*.glob" -delete
+find archive/proofs/coq -name ".*.aux" -delete
 ----
 
 === clean-lean
@@ -417,7 +416,7 @@ just clean-lean
 *What it does*:
 [source,bash]
 ----
-cd proofs/lean4 && lake clean
+cd archive/proofs/lean4 && lake clean
 ----
 
 *Removes*:
@@ -720,7 +719,7 @@ import "justfile"
 
 # Override build-coq with custom flags
 build-coq-custom:
-    coqc -verbose -R proofs/coq/common CNO proofs/coq/common/CNO.v
+    coqc -verbose -R archive/proofs/coq/common CNO archive/proofs/coq/common/CNO.v
 ----
 
 Then:
diff --git a/docs/MACHINE_VERIFICATION.adoc b/docs/MACHINE_VERIFICATION.adoc
index d23a385..0c2305d 100644
--- a/docs/MACHINE_VERIFICATION.adoc
+++ b/docs/MACHINE_VERIFICATION.adoc
@@ -71,11 +71,11 @@ Verifying Coq proofs...
 Run this to count incomplete proofs:
 
 ```bash
-# Count Coq admits
-find proofs/coq -name "*.v" -exec grep -c "Admitted" {} + | awk -F: '{sum += $2} END {print "Coq Admitted:", sum}'
+# Count Coq admits (archived tree)
+find archive/proofs/coq -name "*.v" -exec grep -c "Admitted" {} + | awk -F: '{sum += $2} END {print "Coq Admitted:", sum}'
 
-# Count Lean 4 sorries
-find proofs/lean4 -name "*.lean" -exec grep -c "sorry" {} + | awk -F: '{sum += $2} END {print "Lean sorry:", sum}'
+# Count Lean 4 sorries (archived tree)
+find archive/proofs/lean4 -name "*.lean" -exec grep -c "sorry" {} + | awk -F: '{sum += $2} END {print "Lean sorry:", sum}'
 ```
 
 ### Step 4: Address Failures
diff --git a/docs/OND-PILLAR-STRUCTURE.adoc b/docs/OND-PILLAR-STRUCTURE.adoc
index 5f798a5..c05032b 100644
--- a/docs/OND-PILLAR-STRUCTURE.adoc
+++ b/docs/OND-PILLAR-STRUCTURE.adoc
@@ -14,13 +14,22 @@ artifacts CNO does not need: *declared observation models* and *residue lists*.
 .STATUS — 2026-07-07: OND modules AUTHORED (PR #100)
 ====
 The dedicated proof effort has run. The OND modules specified below now exist and
-are machine-checked: `proofs/coq/ond/OND.v` (OND-1..5, zero axioms, all *Closed
-under the global context*), plus `proofs/lean4/OND.lean`, `proofs/agda/OND.agda`,
-`proofs/isabelle/OND.thy`, and `proofs/z3/ond/OND_checks.smt2`. The first residue
+were machine-checked: `archive/proofs/coq/ond/OND.v` (OND-1..5, zero axioms, all *Closed
+under the global context*), plus `archive/proofs/lean4/OND.lean`, `proofs/agda/OND.agda`,
+`archive/proofs/isabelle/OND.thy`, and `proofs/z3/ond/OND_checks.smt2`. The first residue
 instance (`proofs/residue/ct_select.residue`) and observation model
 (`proofs/observation-models/O_all.model`) are populated. Note: the Coq module
 landed at `proofs/coq/ond/OND.v` (not the `observational/` path sketched below).
 Only OND-6 remains to author.
+
+*Archive update (2026-10-10).* The Coq, Lean 4, Isabelle/HOL and Mizar trees
+were archived under `archive/proofs/` and are no longer built or gated; the Coq
+OND module is now `archive/proofs/coq/ond/OND.v`. The active OND legs are
+`proofs/agda/OND.agda` and `proofs/z3/ond/OND_checks.smt2`. The layout tables
+below are the original design sketch: their `proofs/coq/…`, `proofs/lean4/…`,
+`proofs/isabelle/…` and `proofs/mizar/…` paths name the pre-archive layout, and
+some (`observational/`, `ond_verify.sh`, the `ONDIndependence`/`ONDComposition`
+splits, `OND.miz`) exist in neither `proofs/` nor `archive/proofs/`.
 ====
 
 == Co-equality principle
@@ -36,9 +45,10 @@ CNO analogue.
 
 == Per-prover module layout (mirrors CNO — AUTHORED)
 
-Each OND module sits beside its CNO counterpart. As of PR #100 these files exist
-and are verified (Coq/Lean/Agda/Z3/Isabelle); the Coq module is at
-`proofs/coq/ond/OND.v`.
+Each OND module sits beside its CNO counterpart. As of PR #100 these files existed
+and were verified (Coq/Lean/Agda/Z3/Isabelle); the Coq module landed at
+`proofs/coq/ond/OND.v`, now archived as `archive/proofs/coq/ond/OND.v`. The table
+below is the design sketch (see the archive update above).
 
 [cols="1,2,2,3",options="header"]
 |===
diff --git a/docs/OND-ROADMAP.adoc b/docs/OND-ROADMAP.adoc
index 8c002a0..659ca30 100644
--- a/docs/OND-ROADMAP.adoc
+++ b/docs/OND-ROADMAP.adoc
@@ -17,8 +17,9 @@ proofs themselves are deferred to a dedicated effort.
 .STATUS UPDATE — 2026-07-06: OND-1..5 + OND-7 LANDED
 ====
 The dedicated effort has since run. *OND-1, OND-2, OND-3, OND-4, and OND-5 are
-now proved and machine-checked* — Coq (`proofs/coq/ond/OND.v`), Lean 4
-(`proofs/lean4/OND.lean`), and Agda (`proofs/agda/OND.agda`), with the bounded
+now proved and machine-checked* — Coq (`archive/proofs/coq/ond/OND.v`), Lean 4
+(`archive/proofs/lean4/OND.lean`) — both archived 2026-10-10 and no longer
+built or gated — and Agda (`proofs/agda/OND.agda`), with the bounded
 instances confirmed in Z3 (`proofs/z3/ond/OND_checks.smt2`). Every OND theorem
 in Coq reports `Closed under the global context` — *zero axioms, zero admits*.
 The independence theorem (OND-3) is additionally anchored to the *real* core
diff --git a/docs/VERIFICATION_RESULTS.adoc b/docs/VERIFICATION_RESULTS.adoc
index e1e80b5..fdd3249 100644
--- a/docs/VERIFICATION_RESULTS.adoc
+++ b/docs/VERIFICATION_RESULTS.adoc
@@ -3,9 +3,11 @@
 # Verification Results: Phase 1 Completion and Cross-Solver Proofs
 
 > **SUPERSEDED / HISTORICAL (2025-11-22 session).** This is a point-in-time
-> session log. Current reproduced status: both pillars machine-checked across
-> six provers + Idris (PR #100, 2026-07-06) — see `PROOF-STATUS.adoc` and run
-> `proofs/verify-all-provers.sh` (`ALL-PROVERS-GREEN`). Counts below are historical.
+> session log. Both pillars were machine-checked across six provers + Idris
+> (PR #100, 2026-07-06); since the 2026-10-10 archive ruling the active stack is
+> Agda + Z3 (bounded) + the Idris 2 ABI — run `proofs/verify-active-provers.sh`
+> (`ACTIVE-PROVERS-GREEN`). The Coq and Lean files cited below are archived under
+> `archive/proofs/`. See `PROOF-STATUS.adoc`. Counts below are historical.
 
 **Date**: 2025-11-22
 **Session**: Proof Completion and Automated Verification
diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc
index 1827b8b..2aa053f 100644
--- a/docs/proof-debt.adoc
+++ b/docs/proof-debt.adoc
@@ -9,6 +9,11 @@ tagged `+METAL-BOUNDARY+` and (b) a small openly-labelled class-A set
 `+fidelity_bound+`). Three axioms turned out *unsound* and were
 removed/corrected (`+no_cloning+`, `+Cconj_Cexp+`, `+eta_equivalence+`).
 Current disposition: `+PROOF-STATUS.adoc+`.
+
+*Archive update (2026-10-10):* the Coq and Lean 4 trees this ledger cites were
+archived under `+archive/proofs/+` and are no longer built or gated; the file
+pointers below have been updated to the archived paths (line numbers are as
+recorded at triage time).
 ____
 
 *Schema*:
@@ -44,7 +49,7 @@ https://github.com/hyperpolymath/absolute-zero/issues/27[#27].
 === Phase 2a triage — Lean Lambda cluster (2026-05-27)
 
 Per-cluster Lean triage rolling out 2026-05-27 in cluster-sized PRs.
-First cluster: `+proofs/lean4/LambdaCNO.lean+` (3 axioms at triage time; 1 since 2026-09-22 — see the rows).
+First cluster: `+archive/proofs/lean4/LambdaCNO.lean+` (3 axioms at triage time; 1 since 2026-09-22 — see the rows).
 
 [width="99%",cols=">14%,26%,28%,32%",options="header",]
 |===
@@ -54,7 +59,7 @@ immediate from the semantic `+Closed+` definition.
 
 |237 |`+y_combinator_not_identity+` |§(c) AXIOM |Non-termination claim
 about Y combinator; requires step-indexed semantics or coinduction (same
-justification as Coq `+y_not_cno+`, `+proofs/coq/lambda/LambdaCNO.v:399+`).
+justification as Coq `+y_not_cno+`, `+archive/proofs/coq/lambda/LambdaCNO.v:399+`).
 
 |308 |`+eta_equivalence+` |THEOREM (restricted) |The unrestricted statement
 is *false* (counterexample `+f = LVar 5+`, exactly as Coq found at
@@ -69,7 +74,7 @@ comments. The §(d) entry below has an owner + deadline.
 
 === Phase 2c triage — Lean Filesystem cluster (2026-05-27, DISCHARGED 2026-09-26)
 
-Second Lean cluster: `+proofs/lean4/FilesystemCNO.lean+` (**21 → 0 axioms** — *DISCHARGED 2026-09-26*, issue #167).
+Second Lean cluster: `+archive/proofs/lean4/FilesystemCNO.lean+` (**21 → 0 axioms** — *DISCHARGED 2026-09-26*, issue #167).
 All 10 primitive operations (`mkdir`, `rmdir`, `create`, `unlink`, `readFile`,
 `writeFile`, `stat`, `chmod`, `chown`, `rename`), the 2 snapshot operations (`snapshot`, `restore`),
 and all 9 laws and properties (`mkdir_rmdir_inverse`, `create_unlink_inverse`,
@@ -81,7 +86,7 @@ the Coq concrete filesystem model. `AxiomAudit.lean` §D verifies that all
 
 === Phase 2d triage — Lean Quantum cluster (2026-05-27)
 
-Third Lean cluster: `+proofs/lean4/QuantumCNO.lean+` (14 axioms).
+Third Lean cluster: `+archive/proofs/lean4/QuantumCNO.lean+` (14 axioms).
 
 ==== Hilbert-space + gate primitives (§(c) AXIOM, 7)
 
@@ -147,7 +152,7 @@ leading comments.
 
 === Phase 2e triage — Lean StatMech cluster (2026-05-27)
 
-Fourth Lean cluster: `+proofs/lean4/StatMech.lean+` (14 axioms).
+Fourth Lean cluster: `+archive/proofs/lean4/StatMech.lean+` (14 axioms).
 
 ==== Physical constants (§(c) AXIOM — duplicate of Coq, 4)
 
@@ -229,7 +234,7 @@ longer in §(d).
 
 ==== Coq — provable, awaiting proof
 
-* `+proofs/coq/category/CNOCategory.v:323+` — `+hom_functor+`
+* `+archive/proofs/coq/category/CNOCategory.v:323+` — `+hom_functor+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: replace `+Axiom hom_functor : ... Functor C C+` with the
 proper Yoneda construction `+Functor C SetCategory+`. The file’s leading
@@ -242,93 +247,93 @@ comment (L312-322) records why this is currently axiomatised: (1)
 (Phase 1, #58).
 ** *Deadline*: INDEFINITE (blocked on `+SetCategory+` instance —
 universe-polymorphism scaffolding precondition).
-* `+proofs/coq/filesystem/FilesystemCNO.v:300+` — `+mkdir_not_identity+`
+* `+archive/proofs/coq/filesystem/FilesystemCNO.v:300+` — `+mkdir_not_identity+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: existence proof; exhibit one concrete `+fs+` lacking the
 path. Triaged DISCHARGE in #58.
 ** *Deadline*: INDEFINITE (small proof; awaits a discharge PR).
-* `+proofs/coq/filesystem/FilesystemCNO.v:316+` —
+* `+archive/proofs/coq/filesystem/FilesystemCNO.v:316+` —
 `+write_different_not_identity+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: existence proof; exhibit one concrete content mismatch.
 Triaged DISCHARGE in #58.
 ** *Deadline*: INDEFINITE.
-* `+proofs/coq/filesystem/FilesystemCNO.v:397+` — `+transaction_cno+`
+* `+archive/proofs/coq/filesystem/FilesystemCNO.v:397+` — `+transaction_cno+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: composite theorem; derivable from primitive `+_inverse+`
 axioms once a `+transaction+` definition is in place. Triaged DISCHARGE
 in #58.
 ** *Deadline*: INDEFINITE (blocked on `+transaction+` definition).
-* `+proofs/coq/filesystem/FilesystemCNO.v:421+` — `+mkdir_idempotent+`
+* `+archive/proofs/coq/filesystem/FilesystemCNO.v:421+` — `+mkdir_idempotent+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: follows from `+mkdir_rmdir_inverse+` family + stronger
 repeat-mkdir semantics. Triaged DISCHARGE in #58.
 ** *Deadline*: INDEFINITE.
-* `+proofs/coq/filesystem/FilesystemCNO.v:453+` —
+* `+archive/proofs/coq/filesystem/FilesystemCNO.v:453+` —
 `+snapshot_restore_identity+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: composite theorem; derivable from primitive `+_identity+` /
 `+_inverse+` axioms once a snapshot model lands. Triaged DISCHARGE in
 #58.
 ** *Deadline*: INDEFINITE.
-* `+proofs/coq/quantum/QuantumCNO.v:258+` — `+global_phase_unitary+`
+* `+archive/proofs/coq/quantum/QuantumCNO.v:258+` — `+global_phase_unitary+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: derivable from gate algebra: `+(e^{iθ} U)+` is unitary iff
 `+U+` is. Triaged DISCHARGE in #58 (Phase 2d).
 ** *Deadline*: INDEFINITE (needs `+is_unitary+` algebraic lemmas).
-* `+proofs/coq/quantum/QuantumCNO.v:283+` — `+X_gate_not_identity+`
+* `+archive/proofs/coq/quantum/QuantumCNO.v:283+` — `+X_gate_not_identity+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: existence proof; exhibit `\|0⟩` as witness once a concrete
 basis state is in the model. Triaged DISCHARGE in #58 (Phase 2d).
 ** *Deadline*: INDEFINITE (blocked on concrete basis-state model).
-* `+proofs/coq/quantum/QuantumCNO.v:296+` — `+H_gate_not_identity+`
+* `+archive/proofs/coq/quantum/QuantumCNO.v:296+` — `+H_gate_not_identity+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: existence proof; exhibit `\|0⟩` as witness. Triaged
 DISCHARGE in #58 (Phase 2d).
 ** *Deadline*: INDEFINITE (blocked on concrete basis-state model).
-* `+proofs/coq/quantum/QuantumCNO.v:487+` — `+unitary_inverse_property+`
+* `+archive/proofs/coq/quantum/QuantumCNO.v:487+` — `+unitary_inverse_property+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: follows from `+is_unitary+` definition (`+U†U = I+`). Triaged
 DISCHARGE in #58 (Phase 2d).
 ** *Deadline*: INDEFINITE.
-* `+proofs/coq/quantum/QuantumCNO.v:545+` —
+* `+archive/proofs/coq/quantum/QuantumCNO.v:545+` —
 `+unitary_zero_entropy_change+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: derivable from `+unitary_preserves_entropy+` + entropy
 definition. Triaged DISCHARGE in #58 (Phase 2d).
 ** *Deadline*: INDEFINITE.
-* `+proofs/coq/quantum/QuantumCNO.v:551+` —
+* `+archive/proofs/coq/quantum/QuantumCNO.v:551+` —
 `+reversible_quantum_zero_dissipation+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: derivable from `+quantum_landauer_bound+` + unitarity.
 Triaged DISCHARGE in #58 (Phase 2d).
 ** *Deadline*: INDEFINITE.
-* `+proofs/coq/quantum/QuantumCNO.v:584+` — `+fidelity_bound+`
+* `+archive/proofs/coq/quantum/QuantumCNO.v:584+` — `+fidelity_bound+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: provable from `+inner_product_pos_def+` + Cauchy-Schwarz.
 Triaged DISCHARGE in #58 (Phase 2d).
 ** *Deadline*: INDEFINITE.
-* `+proofs/coq/physics/StatMech.v:229+` —
+* `+archive/proofs/coq/physics/StatMech.v:229+` —
 `+reversible_zero_dissipation+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: derivable from `+landauer_principle+` + reversibility
 hypothesis. Triaged DISCHARGE in #58 (Phase 2e).
 ** *Deadline*: INDEFINITE.
-* `+proofs/coq/physics/LandauerDerivation.v:81+` —
+* `+archive/proofs/coq/physics/LandauerDerivation.v:81+` —
 `+shannon_entropy_additive+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: chain rule of entropy; provable from the definition of
 `+H(X,Y)+` given an independence hypothesis. Triaged DISCHARGE in #58
 (Phase 2e).
 ** *Deadline*: INDEFINITE (blocked on `+product_dist+` semantics).
-* `+proofs/coq/physics/LandauerDerivation.v:277+` —
+* `+archive/proofs/coq/physics/LandauerDerivation.v:277+` —
 `+cno_preserves_shannon_entropy+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: should follow from the CNO definition (state in = state out)
 + functional Shannon entropy. Triaged DISCHARGE in #58 (Phase 2e).
 ** *Deadline*: INDEFINITE (blocked on bijection-preserves-entropy
 machinery).
-* `+proofs/coq/physics/LandauerDerivation.v:326+` —
+* `+archive/proofs/coq/physics/LandauerDerivation.v:326+` —
 `+cno_zero_energy_dissipation_derived+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: name literally says `+_derived+`; the file admits this rather
@@ -339,23 +344,23 @@ than discharging it. Should follow from
 
 ==== Lean — provable, awaiting proof
 
-* `+proofs/lean4/LambdaCNO.lean:184+` — `+subst_closed_term+` — *DISCHARGED
+* `+archive/proofs/lean4/LambdaCNO.lean:184+` — `+subst_closed_term+` — *DISCHARGED
 2026-09-22* (fix PR for #125): now a `+theorem+`; it is immediate from the
 semantic definition of `+Closed+` (`+h n s (Nat.zero_le n)+`).
-* `+proofs/lean4/FilesystemCNO.lean+` — all 21 axioms (`mkdir_not_identity`,
+* `+archive/proofs/lean4/FilesystemCNO.lean+` — all 21 axioms (`mkdir_not_identity`,
 `snapshot_restore_identity`, `mkdir_idempotent`, operations and laws) — *DISCHARGED
 2026-09-26* (issue #167): concrete model ported from Coq `FilesystemCNO.v`.
-* `+proofs/lean4/QuantumCNO.lean:134+` — `+X_gate_not_identity+`
+* `+archive/proofs/lean4/QuantumCNO.lean:134+` — `+X_gate_not_identity+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: existence proof; exhibit `\|0⟩` as witness once a concrete
 basis state is in the model. Mirrors Coq site at `+QuantumCNO.v:283+`.
 ** *Deadline*: INDEFINITE.
-* `+proofs/lean4/QuantumCNO.lean:144+` — `+H_gate_not_identity+`
+* `+archive/proofs/lean4/QuantumCNO.lean:144+` — `+H_gate_not_identity+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: existence proof; exhibit `\|0⟩` as witness. Mirrors Coq site
 at `+QuantumCNO.v:296+`.
 ** *Deadline*: INDEFINITE.
-* `+proofs/lean4/QuantumCNO.lean:235+` — `+unitary_inverse_property+`
+* `+archive/proofs/lean4/QuantumCNO.lean:235+` — `+unitary_inverse_property+`
 ** *Owner*: @hyperpolymath
 ** *Plan*: follows from `+isUnitary+` definition (`+U†U = I+`). Mirrors
 Coq site at `+QuantumCNO.v:487+`.
diff --git a/docs/wiki/Architecture.md b/docs/wiki/Architecture.md
index e9b1b74..7520b8a 100644
--- a/docs/wiki/Architecture.md
+++ b/docs/wiki/Architecture.md
@@ -62,16 +62,16 @@ absolute-zero calls into it via the `echidna-llm-mcp` BoJ cartridge —
 ## Data flow on `just verify`
 
 ```
-verification/setup-and-verify.sh
-  ├── proofs/coq         → coqc -R common CNO ...
-  ├── proofs/lean4       → lake build
-  ├── proofs/agda        → agda CNO.agda
-  ├── proofs/isabelle    → isabelle build
-  ├── proofs/z3          → z3 *.smt2
-  ├── src/abi            → idris2 --build absolute-zero-abi.ipkg
-  └── cargo build --release
+proofs/verify-active-provers.sh
+  ├── proofs/agda        → agda --safe --without-K (CNO, OND, EchoBridgeScaffold, EchoBridgeCNO)
+  ├── proofs/z3          → proofs/z3/verify.sh (expect-annotated bounded checks)
+  └── src/abi            → idris2 --build absolute-zero-abi.ipkg
 ```
 
+The Coq, Lean 4, Isabelle/HOL and Mizar trees were archived on 2026-10-10
+under `archive/proofs/` (`coq/`, `lean4/`, `isabelle/`, `mizar/`) and are not run.
+The former six-prover gate is `archive/proofs/verify-all-provers.six-prover.sh`.
+
 ## Why this taxonomy
 
 The directory layout follows the [RSR-template-repo](../RSR_OUTLINE.adoc)
diff --git a/docs/wiki/Audit-Trail.md b/docs/wiki/Audit-Trail.md
index 4b5c5d7..6242662 100644
--- a/docs/wiki/Audit-Trail.md
+++ b/docs/wiki/Audit-Trail.md
@@ -24,8 +24,8 @@ Short summary; the authoritative ledger is [`AUDIT.adoc`](../../AUDIT.adoc).
 
 ## Axiom classification
 
-The 73 Coq Axioms + 42 Parameters in `proofs/coq/` are model-layer
-assumptions:
+The 73 Coq Axioms + 42 Parameters in `archive/proofs/coq/` (archived 2026-10-10;
+historical counts) are model-layer assumptions:
 
 * **Physics**: thermodynamic laws, Landauer bound, statistical mechanics
 * **Quantum**: Hilbert-space axioms, unitarity
diff --git a/docs/wiki/Home.md b/docs/wiki/Home.md
index 9554620..bb45096 100644
--- a/docs/wiki/Home.md
+++ b/docs/wiki/Home.md
@@ -38,10 +38,10 @@ of 23+ languages.
 
 ## Status (live)
 
-* **Phase**: two-pillar completion / hardening (~88%). Both pillars machine-checked across **six provers + Idris** (PR #100) — run `proofs/verify-all-provers.sh` → `ALL-PROVERS-GREEN`.
-* **Coq**: 14/14 theories compile (CNO + OND), 0 Admitted; CNO axioms cut 98→small classified remainder; **OND** (`ond/OND.v`) OND-1..5 proved with zero axioms.
-* **Lean 4**: `lake build` green (Mathlib) incl. the new `OND` lib; 0 `sorry`.
-* **Agda / Z3 / Isabelle / Mizar**: CNO + OND verified (Agda `OND.agda`; Z3 `ond/OND_checks.smt2`; Isabelle `AbsoluteZero-CNO` session; Mizar `CNO.miz` → empty `.err`).
+* **Phase**: two-pillar completion / hardening (~88%). Both pillars were machine-checked across **six provers + Idris** (PR #100, 2026-07-06). Since the 2026-10-10 archive ruling the active stack is **Agda + Z3 (bounded) + Idris 2 ABI** — run `proofs/verify-active-provers.sh` → `ACTIVE-PROVERS-GREEN`. Coq, Lean 4, Isabelle/HOL and Mizar are archived under `archive/proofs/` (not built or gated); the six-prover gate is `archive/proofs/verify-all-provers.six-prover.sh`.
+* **Coq (archived, `archive/proofs/coq/`)**: 14/14 theories compiled (CNO + OND), 0 Admitted; CNO axioms cut 98→small classified remainder; **OND** (`ond/OND.v`) OND-1..5 proved with zero axioms.
+* **Lean 4 (archived, `archive/proofs/lean4/`)**: `lake build` was green (Mathlib) incl. the new `OND` lib; 0 `sorry`.
+* **Agda / Z3** (active): Agda type-checks CNO + OND (`CNO.agda`, `OND.agda`); Z3 runs the OND bounded checks (`ond/OND_checks.smt2`). **Isabelle / Mizar** (archived): Isabelle `AbsoluteZero-CNO` session and Mizar `CNO.miz` → empty `.err` were verified on 2026-07-07.
 * **Idris2 ABI**: `absolute-zero-abi.ipkg` builds clean under 0.8.0.
 * For the authoritative live state, read [`.machine_readable/descriptiles/STATE.a2ml`](../../.machine_readable/descriptiles/STATE.a2ml)
 
@@ -49,8 +49,8 @@ of 23+ languages.
 provers + the Idris ABI: the OND (disclosure) pillar was authored from scratch
 (OND-1..5 proved, zero axioms; OND-6 open by design), CNO axioms were cut from 98
 to a small classified remainder, three latent-unsound axioms were found and fixed,
-and Isabelle/Mizar/Idris were brought to green. Reproduce with
-`proofs/verify-all-provers.sh`.
+and Isabelle/Mizar/Idris were brought to green. Reproduced then with
+`proofs/verify-all-provers.sh` (now archived as `archive/proofs/verify-all-provers.six-prover.sh`).
 
 ## Project layout (RSR-aligned)
 
diff --git a/docs/wiki/Proof-Systems.md b/docs/wiki/Proof-Systems.md
index 6e78a6e..d26fd31 100644
--- a/docs/wiki/Proof-Systems.md
+++ b/docs/wiki/Proof-Systems.md
@@ -23,7 +23,12 @@ flags a foundational dependency worth understanding.
 
 ## What lives where
 
-### `proofs/coq/` (the load-bearing system)
+Since the 2026-10-10 archive ruling the active stack is Agda (`proofs/agda/`),
+Z3 bounded checks (`proofs/z3/`) and the Idris 2 ABI. The Coq, Lean 4,
+Isabelle/HOL and Mizar trees below are archived under `archive/proofs/` and are
+no longer built or gated; their status lines are historical receipts.
+
+### `archive/proofs/coq/` (archived; formerly the load-bearing system)
 * `common/CNO.v` — core CNO definitions and properties
 * `physics/StatMech.v` — Landauer bound axiomatised
 * `physics/LandauerDerivation.v` — Landauer bound derived (the two
@@ -35,7 +40,7 @@ flags a foundational dependency worth understanding.
 * `malbolge/MalbolgeCore.v` — Malbolge VM semantics
 * `filesystem/FilesystemCNO.v` — filesystem CNOs
 
-Status (PR #100, 2026-07-06): **14/14 theories compile, 0 Admitted**, now
+Status (PR #100, 2026-07-06): **14/14 theories compiled, 0 Admitted**, now
 including `ond/OND.v` (the OND pillar, OND-1..5, zero axioms). CNO axioms cut
 98→small classified remainder: filesystem/category/QuantumMechanicsExact fully
 discharged; genuine physical postulates kept as tagged `METAL-BOUNDARY`; a few
@@ -43,10 +48,10 @@ class-A items openly labelled; three unsound axioms removed/corrected. See
 [`PROOF-STATUS.adoc`](../../PROOF-STATUS.adoc) and
 [`docs/PROOF-CLASSIFICATION.adoc`](../PROOF-CLASSIFICATION.adoc).
 
-### `proofs/lean4/`
+### `archive/proofs/lean4/` (archived)
 * `CNO.lean`, `StatMech.lean`, `CNOCategory.lean`, `LambdaCNO.lean`,
   `QuantumCNO.lean`, `FilesystemCNO.lean`
-* Built with `lake build`; mathlib + 6 lean_lib targets;
+* Was built with `lake build`; mathlib + 6 lean_lib targets;
   1631/1632 green (verified 2026-05-20).
 
 ### `proofs/z3/`
@@ -56,21 +61,22 @@ candidate CNO claims before committing to a constructive proof.
 ### `proofs/agda/`
 Type-level CNO certificates exploiting dependent types.
 
-### `proofs/isabelle/`, `proofs/mizar/`
+### `archive/proofs/isabelle/`, `archive/proofs/mizar/` (archived)
 Cross-validation. Catches Coq-specific tactic quirks; connects
 Mizar's standard maths library.
 
 ## Reproducible build
 
 ```bash
-just build-coq      # coqc -R common CNO physics/StatMech.v ...
-just build-lean     # cd proofs/lean4 && lake build
-just build-agda     # agda CNO.agda
-just build-isabelle # isabelle build
-just build-z3       # z3 *.smt2 (when present)
-just verify         # all of the above + ABI + Rust
+just build-agda     # agda --safe --without-K on the four Agda modules
+just build-idris    # idris2 --build absolute-zero-abi.ipkg
+just verify-z3      # bash proofs/z3/verify.sh (expect-annotated)
+just verify         # proofs/verify-active-provers.sh → ACTIVE-PROVERS-GREEN
 ```
 
+The former `build-coq`, `build-lean`, `build-isabelle` and `build-z3` recipes no
+longer exist in the Justfile.
+
 ## Discharged axioms (recent)
 
 * **ADR-007** (2026-05-20, PR #24): `eval_deterministic`
diff --git a/docs/wiki/Roadmap.md b/docs/wiki/Roadmap.md
index e9ad2a4..5b7495c 100644
--- a/docs/wiki/Roadmap.md
+++ b/docs/wiki/Roadmap.md
@@ -8,9 +8,9 @@ Short summary; the authoritative version is [`ROADMAP.adoc`](../../ROADMAP.adoc)
 
 ## Now (post v1.0.0-alpha)
 
-* ✅ Both pillars machine-checked across six provers + Idris (PR #100) — `proofs/verify-all-provers.sh`
-* ✅ OND pillar authored (OND-1..5 proved, zero axioms); ✅ Idris ABI builds; ✅ Isabelle + Mizar verify
-* Wire proof verification into CI (`.github/workflows/proofs.yml` runs Coq + Z3; extend to more provers)
+* ✅ Both pillars machine-checked across six provers + Idris (PR #100) — via `proofs/verify-all-provers.sh`, now archived as `archive/proofs/verify-all-provers.six-prover.sh`; since 2026-10-10 the active gate is `proofs/verify-active-provers.sh` (Agda + Z3 bounded + Idris 2 ABI)
+* ✅ OND pillar authored (OND-1..5 proved, zero axioms); ✅ Idris ABI builds; ✅ Isabelle + Mizar verified (2026-07-07; both archived under `archive/proofs/` since 2026-10-10)
+* Wire proof verification into CI (`.github/workflows/proofs.yml` runs the `agda`, `z3` and `idris` jobs; the Coq and Lean 4 jobs were dropped when those trees were archived on 2026-10-10)
 * Discharge the class-A remainder (needs finite-dim/tensor QM + coinductive-β machinery) — optional
 * Prove **OND-6** (conditional composition) — the research capstone
 
diff --git a/docs/wiki/Verification.md b/docs/wiki/Verification.md
index 7b06576..84b2cd3 100644
--- a/docs/wiki/Verification.md
+++ b/docs/wiki/Verification.md
@@ -24,29 +24,30 @@ The `verification/` directory contains the top-level scripts.
 Or via `Justfile` recipes (more granular):
 
 ```bash
-just build-all        # everything
-just build-coq        # Coq only
-just build-lean       # Lean 4 only
+just build-all        # Agda + Idris 2 ABI (the active stack)
 just build-agda
-just build-isabelle
-just build-affinescript
-just verify           # build + check
+just build-idris
+just verify           # proofs/verify-active-provers.sh → ACTIVE-PROVERS-GREEN
 ```
 
+The Coq, Lean 4, Isabelle/HOL and Mizar trees were archived on 2026-10-10 under
+`archive/proofs/` and have no build recipes; the commands below for them are
+historical and run against the archived trees.
+
 ## Per-prover commands
 
-### Coq
+### Coq (archived)
 ```bash
-cd proofs/coq/common && coqc CNO.v
+cd archive/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
 ```
 
-### Lean 4
+### Lean 4 (archived)
 ```bash
-cd proofs/lean4 && lake build
+cd archive/proofs/lean4 && lake build
 ```
 
 ### Agda
@@ -97,5 +98,8 @@ See [`.machine_readable/descriptiles/STATE.a2ml`](../../.machine_readable/descri
 and [`PROOF-STATUS.adoc`](../../PROOF-STATUS.adoc) for live status. Summary: both
 pillars verified across **six provers + Idris** — Coq 14/14, Lean+Mathlib green,
 Agda (CNO+OND), Z3, Isabelle (`AbsoluteZero-CNO`), Mizar (`CNO.miz` empty `.err`),
-Idris ABI builds clean. One-shot: `proofs/verify-all-provers.sh` →
-`ALL-PROVERS-GREEN`.
+Idris ABI builds clean. One-shot then: `proofs/verify-all-provers.sh` (now archived as
+`archive/proofs/verify-all-provers.six-prover.sh`) → `ALL-PROVERS-GREEN`.
+
+Since the 2026-10-10 archive ruling only Agda, Z3 (bounded) and the Idris 2 ABI
+are active: run `proofs/verify-active-provers.sh` → `ACTIVE-PROVERS-GREEN`.
diff --git a/proofs/verify-active-provers.sh b/proofs/verify-active-provers.sh
index e554a87..5964843 100755
--- a/proofs/verify-active-provers.sh
+++ b/proofs/verify-active-provers.sh
@@ -9,7 +9,8 @@
 #
 # Every active prover is REQUIRED: an absent toolchain is a failure, never a skip.
 # Needs on PATH: agda, z3, idris2. The Agda standard library is registered via
-# ~/.agda/libraries (see .github/workflows/proofs.yml for the pinned setup).
+# ~/.agda/libraries: run scripts/provision-agda-stdlib.sh first (pinned v1.7.3,
+# the same script CI runs).
 set -uo pipefail
 export PATH="$HOME/.local/bin:$HOME/.elan/bin:$PATH"
 HERE="$(cd "$(dirname "$0")" && pwd)"
diff --git a/proofs/z3/ond/OND_checks.smt2 b/proofs/z3/ond/OND_checks.smt2
index 8744670..fe54ac7 100644
--- a/proofs/z3/ond/OND_checks.smt2
+++ b/proofs/z3/ond/OND_checks.smt2
@@ -1,5 +1,5 @@
 ; Absolute Zero — OND pillar, bounded/finite verification (Z3)
-; Mirrors proofs/coq/ond/OND.v. Memory cells are integers:
+; Mirrors archive/proofs/coq/ond/OND.v (archived 2026-10-10). Memory cells are integers:
 ;   cell0 = secret, cell1 = public, cell2 = declared output channel.
 ; "Decidable for bounded programs under a finite observation model O" (OND-ROADMAP).
 
@@ -14,12 +14,53 @@
 (pop)
 
 ; ---- OND-3 dir 2: writer is OND on (output,timing) yet NOT a null op.
-; output cell2 stays 0, time = 1 (both secret-independent) => OND holds:
+; Modelled per archive/proofs/coq/ond/OND.v (writer_op, inj, run, O_all):
+;   memory      = (Array Int Int), cells >= 0 stand for OND.v's nat addresses;
+;   inj s p     = all cells 0, then cell0 := s, cell1 := p   (cell2 stays 0);
+;   writer_step = mem_update m secret_cell 7                  (op_step writer_op);
+;   writer_time = 1                                           (op_time writer_op);
+;   run         = (output cell2 of writer_step (inj s p), writer_time (inj s p)).
+; The observable is COMPUTED from the step function, not written down as a
+; constant. (Before 2026-11-09 this block asserted (not (and (= 0 0) (= 1 1))),
+; which is unsat for any program and so checked nothing about the writer.)
 (push)
-(declare-const s1 Int) (declare-const s2 Int)
-; observable of writer = (out=0, time=1) regardless of secret
-(assert (not (and (= 0 0) (= 1 1)))) ; negation of "observable equal across secrets"
-(check-sat) ; expect unsat => writer IS OND (no secret distinguishes its observable)
+(define-fun inj ((s Int) (p Int)) (Array Int Int)
+  (store (store ((as const (Array Int Int)) 0) 0 s) 1 p))
+(define-fun writer_step ((m (Array Int Int))) (Array Int Int) (store m 0 7))
+(define-fun writer_time ((m (Array Int Int))) Int 1)
+(define-fun writer_out ((s Int) (p Int)) Int (select (writer_step (inj s p)) 2))
+(define-fun writer_tm ((s Int) (p Int)) Int (writer_time (inj s p)))
+(declare-const s1 Int) (declare-const s2 Int) (declare-const pub Int)
+(assert (>= s1 0)) (assert (>= s2 0)) (assert (>= pub 0))
+; negation of is_OND O_all writer_op: some secret pair, same public input,
+; whose (output, time) observables differ.
+(assert (not (and (= (writer_out s1 pub) (writer_out s2 pub))
+                  (= (writer_tm s1 pub) (writer_tm s2 pub)))))
+(check-sat) ; expect unsat => writer IS OND under O_all (no secret pair distinguishes it)
+(pop)
+
+; ---- OND-3 dir 2, control: the same check BITES on a writer that leaks.
+; leaky_writer writes the secret to the output cell; same model, same query.
+; If this were unsat the query above would be vacuous.
+(push)
+(define-fun inj ((s Int) (p Int)) (Array Int Int)
+  (store (store ((as const (Array Int Int)) 0) 0 s) 1 p))
+(define-fun leak_step ((m (Array Int Int))) (Array Int Int) (store m 2 (select m 0)))
+(define-fun leak_out ((s Int) (p Int)) Int (select (leak_step (inj s p)) 2))
+(declare-const s1 Int) (declare-const s2 Int) (declare-const pub Int)
+(assert (>= s1 0)) (assert (>= s2 0)) (assert (>= pub 0))
+; time is the constant 1 for both runs, so the observables differ iff outputs do.
+(assert (not (= (leak_out s1 pub) (leak_out s2 pub))))
+(check-sat) ; expect sat: control — a leaking writer IS distinguished by the same query
+(pop)
+
+; ---- OND-3 dir 2, second half: writer is NOT a null op (writer_not_null).
+; Some memory is changed by writer_step (cell0 becomes 7).
+(push)
+(define-fun writer_step ((m (Array Int Int))) (Array Int Int) (store m 0 7))
+(declare-const m (Array Int Int))
+(assert (not (= (writer_step m) m)))
+(check-sat) ; expect sat: a memory writer_step changes, so writer is not a null op
 (pop)
 
 ; ---- OND-5: p_op and q_op each OND under O_all, composite p;q LEAKS.
diff --git a/scripts/provision-agda-stdlib.sh b/scripts/provision-agda-stdlib.sh
new file mode 100755
index 0000000..2a59dc1
--- /dev/null
+++ b/scripts/provision-agda-stdlib.sh
@@ -0,0 +1,62 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Absolute Zero — reproducible Agda standard-library registration.
+#
+# The Agda proofs (proofs/agda/, absolute-zero.agda-lib) `depend: standard-library`.
+# This script fetches ONE pinned agda-stdlib release, checks that the tag still
+# resolves to the pinned commit, and registers it for Agda. CI
+# (.github/workflows/proofs.yml, `agda` job) and local runs use this same script,
+# so both type-check against the same library bytes.
+#
+# Pin: agda-stdlib v1.7.3 (the release that matches Agda 2.6.3, the version
+# Ubuntu 24.04 ships and CI installs). Tag v1.7.3 -> commit STDLIB_COMMIT below,
+# read with `git ls-remote https://github.com/agda/agda-stdlib.git refs/tags/v1.7.3^{}`
+# on 2026-11-09. If the tag is ever moved, this script fails rather than
+# silently using different sources.
+#
+# Usage:
+#   bash scripts/provision-agda-stdlib.sh
+# Environment (all optional):
+#   AGDA_DIR           Agda's config directory (Agda's own variable; default ~/.agda).
+#                      `libraries` and `defaults` are written here.
+#   AGDA_STDLIB_DIR    Where to put the checkout (default $AGDA_DIR/agda-stdlib-v1.7.3).
+#
+# Idempotent: an existing checkout at the pinned commit is reused. The
+# `libraries` / `defaults` files are OVERWRITTEN to name exactly this library,
+# so run it with a dedicated AGDA_DIR if you keep other Agda libraries in ~/.agda.
+set -euo pipefail
+
+STDLIB_REPO="https://github.com/agda/agda-stdlib.git"
+STDLIB_TAG="v1.7.3"
+STDLIB_COMMIT="0817da6877aa045932221134913d8511caa78d97"
+
+AGDA_DIR="${AGDA_DIR:-$HOME/.agda}"
+AGDA_STDLIB_DIR="${AGDA_STDLIB_DIR:-$AGDA_DIR/agda-stdlib-$STDLIB_TAG}"
+
+mkdir -p "$AGDA_DIR"
+
+if [ -d "$AGDA_STDLIB_DIR/.git" ]; then
+  echo "reusing checkout $AGDA_STDLIB_DIR"
+else
+  git -c advice.detachedHead=false clone -q --depth 1 --branch "$STDLIB_TAG" "$STDLIB_REPO" "$AGDA_STDLIB_DIR"
+fi
+
+have="$(git -C "$AGDA_STDLIB_DIR" rev-parse HEAD)"
+if [ "$have" != "$STDLIB_COMMIT" ]; then
+  echo "PROVISION FAILED: $AGDA_STDLIB_DIR is at $have, expected $STDLIB_TAG = $STDLIB_COMMIT" >&2
+  exit 1
+fi
+
+# absolute-zero.agda-lib depends on the unversioned name `standard-library`;
+# the upstream manifest calls itself `standard-library-1.7.3`. Rename in place
+# (the only local modification to the checkout).
+lib="$AGDA_STDLIB_DIR/standard-library.agda-lib"
+[ -f "$lib" ] || { echo "PROVISION FAILED: $lib missing" >&2; exit 1; }
+sed -i 's/^name: .*/name: standard-library/' "$lib"
+
+printf '%s\n' "$lib" > "$AGDA_DIR/libraries"
+printf '%s\n' "standard-library" > "$AGDA_DIR/defaults"
+
+echo "registered standard-library ($STDLIB_TAG @ $STDLIB_COMMIT)"
+echo "  libraries: $AGDA_DIR/libraries -> $lib"
+echo "  defaults:  $AGDA_DIR/defaults"