hyperpolymath · Nov 9, 2026 · Nov 9, 2026
@@ -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, --safe --without-K)
         working-directory: proofs/agda
         run: |

@@ -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,15 +381,15 @@ 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
 ```
 
 **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
 ```
 

@@ -9,7 +9,7 @@ This file backs every factual claim in link:README.adoc[README.adoc] with code p
 
 [IMPORTANT]
 ====
-*Archive notice (2026-10-10, reconciled 2026-11-01).* The active proof stack is Agda (`proofs/agda/`, `--safe --without-K`, zero postulates) + Z3 as a bounded-check solver + the Idris 2 ABI. Coq, Lean 4, Isabelle/HOL and Mizar now live under `archive/proofs/`; paths below of the form `proofs/coq/…` / `proofs/lean4/…` refer to the *archived* trees (`archive/proofs/coq/…` etc.), and counts such as "115 Qed / 61 Axioms" are *historical* figures of those archived trees. The canonical active-vs-archived proof-status table is link:PROOF-STATUS.adoc[PROOF-STATUS.adoc], which also records the estate proof grades (mathesis `estate-mathematical-architecture` §5) and the closed ledger vocabulary of `hyperpolymath/standards` (`proven` / `proven-with-postulates` / `tested-only` / `argued` / `open`): the active Agda proofs are `proven` at **Grade 3** (local strict-flag check, no independent-foundation translation), the Z3 bounded checks are `tested-only`, and OND-6 is `open`.
+*Archive notice (2026-10-10, reconciled 2026-11-01).* The active proof stack is Agda (`proofs/agda/`, `--safe --without-K`, zero postulates) + Z3 as a bounded-check solver + the Idris 2 ABI. Coq, Lean 4, Isabelle/HOL and Mizar now live under `archive/proofs/`; paths of the form `proofs/coq/…` / `proofs/lean4/…` in older prose and dated records refer to the *archived* trees (`archive/proofs/coq/…` etc.), and counts such as "115 Qed / 61 Axioms" are *historical* figures of those archived trees. The canonical active-vs-archived proof-status table is link:PROOF-STATUS.adoc[PROOF-STATUS.adoc], which also records the estate proof grades (mathesis `estate-mathematical-architecture` §5) and the closed ledger vocabulary of `hyperpolymath/standards` (`proven` / `proven-with-postulates` / `tested-only` / `argued` / `open`): the active Agda proofs are `proven` at **Grade 3** (local strict-flag check, no independent-foundation translation), the Z3 bounded checks are `tested-only`, and OND-6 is `open`.
 ====
 
 == Claim-to-implementation map
@@ -44,7 +44,7 @@ OND proofs are axiom-free *relative to the declared observation model `O`*. The
 ____115 Qed / 0 Admitted / 61 Axioms across 13 files — every theorem is discharged (no Admitted), but the development rests on 61 Coq + 52 Lean axioms.____
 
 How this is implemented::
-`link:proofs/coq/[]` contains all CNO theories. CI runs `coq_makefile` and confirms Qed counts and axiom counts. The axioms are domain-specific assumptions (quantum-gate unitarity, complex-analysis identities, Shannon-entropy non-negativity, filesystem inverse laws) that are *assumed* but not derived within Coq.
+`link:archive/proofs/coq/[]` contains all CNO theories (ARCHIVED 2026-10-10, not built or gated). Until the archive ruling, CI ran `coq_makefile` and confirmed Qed counts and axiom counts; it no longer does. The axioms are domain-specific assumptions (quantum-gate unitarity, complex-analysis identities, Shannon-entropy non-negativity, filesystem inverse laws) that are *assumed* but not derived within Coq.
 
 Caveat::
 **This is not an axiom-free machine-checked proof.** "Machine-checked" here means the proof is valid *assuming the axioms hold*. If an axiom is false in the intended model, the theorem fails. The 61 Coq + 52 Lean axioms represent the proof debt. Discharging them (especially quantum unitarity and filesystem inverse laws) is the next major obligation.
@@ -55,18 +55,18 @@ Caveat::
 ____Verify CNO properties in six independent proof systems.____
 
 How this is implemented::
-Artefacts exist for Coq, Lean 4, Agda, Z3, Isabelle, and Mizar in `link:proofs/[]`. `link:proofs/verify-all-provers.sh[]` orchestrates verification. CI gates Coq, Lean 4, and Agda.
+Active artefacts (Agda, Z3) are in `link:proofs/[]`; `link:proofs/verify-active-provers.sh[]` runs the active gate (Agda + Z3 bounded + Idris 2 ABI), and CI (`proofs.yml`: `agda`, `z3`, `idris` jobs) gates the same three. The Coq, Lean 4, Isabelle/HOL and Mizar artefacts are ARCHIVED under `link:archive/proofs/[]`, as is the former six-prover gate (`link:archive/proofs/verify-all-provers.six-prover.sh[]`); they are not built or gated.
 
 Caveat::
-**Z3, Isabelle, and Mizar are generated but not yet run in CI.** The artefacts exist but are not evidence until machine-executed and green. The "six prover" claim describes the target architecture, not the current CI gate.
+**The six-prover claim is historical.** All six provers were reproduced on 2026-07-07 (see link:PROOF-STATUS.adoc[PROOF-STATUS.adoc]); since the 2026-10-10 archive ruling only Agda, Z3 (bounded) and the Idris 2 ABI are run. Archived artefacts are not current evidence.
 
 === Thermodynamic reversibility follows from Landauer's principle
 
 [quote, README.adoc]
 ____ThermodynamicallyReversible(p) — Zero energy____
 
 How this is implemented::
-`link:proofs/coq/physics/StatMech.v[]` and `link:proofs/lean4/StatMech.lean[]` formalise Landauer's principle and Bennett's reversible computing, proving CNOs dissipate zero energy because they erase no information.
+`link:archive/proofs/coq/physics/StatMech.v[]` and `link:archive/proofs/lean4/StatMech.lean[]` (both ARCHIVED 2026-10-10, not built or gated) formalise Landauer's principle and Bennett's reversible computing, proving CNOs dissipate zero energy because they erase no information.
 
 Caveat::
 The physics formalisation relies on axioms about the physical model (e.g., that the thermodynamic system satisfies the assumptions of Landauer's principle). This is standard for formalisations of physics, but the gap between the mathematical model and physical metal is real.
@@ -88,8 +88,8 @@ This is a standard result. The practical consequence is that the verified CNOs i
 |===
 | Technology / Pattern | Used here | Also used in
 
-| Coq CNO/OND formalisation
-| `proofs/coq/`
+| Coq CNO/OND formalisation (archived)
+| `archive/proofs/coq/`
 | link:https://github.com/hyperpolymath/echo-types[echo-types] (EchoBridgeCNO)
 
 | Multi-prover pattern

@@ -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..."