hyperpolymath · Oct 2, 2026 · Oct 2, 2026
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -29,23 +29,24 @@ jobs:
       - uses: julia-actions/julia-buildpkg@e3eb439fad4f9aba7da2667e7510e4a46ebc46e1 # v1
       - uses: julia-actions/julia-runtest@6e050c8013b833b1195105ff2fce9cd802f53271 # v1
   proofs:
-    name: Agda proofs (2.7.0.1)
+    name: Agda proofs (Debian 2.6.4.3, stdlib 2.1)
     runs-on: ubuntu-24.04
     timeout-minutes: 30
+    # Same recipe as MetaManifold-Evidence and residual-evidence-types: Debian's
+    # agda and agda-stdlib packages at exact versions inside a digest-pinned
+    # image.  Nothing is fetched from GitHub releases or vendored by SHA;
+    # proofs/lib.sh refuses any other Agda.
+    container: debian:13-slim@sha256:d7e12182ce18b85b93007c1dedf31f2d29e01ccf3182cc4017c709b6259bc132
     env:
-      AGDA_SHA256: 975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a
+      LANG: C.UTF-8
+      LC_ALL: C.UTF-8
     steps:
-      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
-      - name: Install the pinned Agda release binary
+      - name: Install the pinned Debian toolchain
         run: |
-          set -euo pipefail
-          curl -fsSL -o "$RUNNER_TEMP/agda.tar.xz" \
-            https://github.com/agda/agda/releases/download/v2.7.0.1/Agda-v2.7.0.1-linux.tar.xz
-          echo "${AGDA_SHA256}  $RUNNER_TEMP/agda.tar.xz" | sha256sum --check
-          tar -xJf "$RUNNER_TEMP/agda.tar.xz" -C "$RUNNER_TEMP"
-          echo "Agda_datadir=$RUNNER_TEMP/Agda-v2.7.0.1/data" >> "$GITHUB_ENV"
-          echo "AGDA_BIN=$RUNNER_TEMP/Agda-v2.7.0.1/bin/agda" >> "$GITHUB_ENV"
-      - name: Type-check and axiom audit
-        run: proofs/bootstrap.sh
-      - name: Gate self-test (the gate must reject planted defects)
-        run: proofs/tests/gate-selftest.sh
+          apt-get update
+          apt-get install --no-install-recommends -y ca-certificates git agda-bin=2.6.4.3-1+b2 agda-stdlib=2.1-4
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
+        with:
+          persist-credentials: false
+      - name: Proof gate (axiom audit, type-check, reject controls, gate self-test)
+        run: proofs/check.sh
diff --git a/.gitignore b/.gitignore
@@ -1,5 +1,3 @@
 /Manifest.toml
-proofs/.vendor/
-proofs/.agda-libraries
 *.agdai
 _build/
diff --git a/README.md b/README.md
@@ -31,7 +31,7 @@ q = bh_adjust([0.01, 0.04, 0.2])                # equals R's p.adjust(, "BH")
 
 ## Proved and tested are kept apart
 
-`proofs/agda` holds machine-checked proofs (Agda 2.7.0.1, `--safe --without-K`,
+`proofs/agda` holds machine-checked proofs (Debian 13's Agda 2.6.4.3 with agda-stdlib 2.1, `--safe --without-K`,
 no postulates) of the algebraic properties the methods rely on. Each CLR theorem is
 mirrored by a Julia property test. Each property test is in turn shown to reject
 a planted mutant (`test/mutants.jl`). The Benjamini–Hochberg step-up (P5: q ≥ p,
@@ -54,7 +54,7 @@ criterion; see [`docs/R-SUNSET.md`](docs/R-SUNSET.md).
 
 ```sh
 julia --project -e 'using Pkg; Pkg.test()'
-proofs/bootstrap.sh && proofs/tests/gate-selftest.sh   # needs Agda 2.7.0.1
+proofs/check.sh                                   # Debian 13: apt install agda agda-stdlib
 ```
 
 ## Licence

diff --git a/proofs/.gitignore b/proofs/.gitignore
@@ -1,7 +1,3 @@
-# Vendored Agda standard library (bootstrap.sh fetches it at the pinned SHA).
-.vendor/
-# Generated by bootstrap.sh; points at absolute paths on one machine.
-.agda-libraries
-# Agda interface files.
+# Agda interface files and the per-version build cache.
 _build/
 *.agdai
diff --git a/proofs/PROOF-STATUS.md b/proofs/PROOF-STATUS.md
@@ -5,8 +5,8 @@ SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@
 
 # Proof status
 
-Machine-checked proofs for CompositionalDA.jl, in **Agda 2.7.0.1** with
-**agda-stdlib pinned at `2ffa8b7d4e8e818717ad643d184f055a4d1b0447`**, under
+Machine-checked proofs for CompositionalDA.jl, in **Agda 2.6.4.3** with
+**agda-stdlib 2.1** (Debian 13's `agda-bin` and `agda-stdlib` packages), under
 `--safe --without-K`. Three words are kept apart throughout this file:
 
 - **proved** — type-checked by Agda with zero postulates, zero holes and
@@ -17,24 +17,24 @@ Machine-checked proofs for CompositionalDA.jl, in **Agda 2.7.0.1** with
   shown to reject a planted mutant in `test/mutants.jl`.
 - **not done** — neither of the above. Listed, not implied.
 
-> **The stdlib pin is a development SHA, not a release.** The branch's own
-> library file declares `name: standard-library-3.0` and no `v3.0` tag exists.
-> `proofs/bootstrap.sh` normalises the name and refuses any other revision.
+> **The toolchain is the Debian 13 pin, not a vendored release.** `proofs/lib.sh`
+> resolves `/usr/bin/agda` before anything on `PATH`, checks the version is
+> 2.6.4.3 and the library is `standard-library-2.1`, and refuses any other.
 
 ## Gates
 
 | Gate | Command | Result |
 | --- | --- | --- |
-| Type-check every proof, then audit | `proofs/bootstrap.sh` | PASS — exit 0, no warnings |
+| Type-check every proof, audit, then self-test | `proofs/check.sh` | PASS — exit 0, no warnings |
 | Axiom audit on its own | `proofs/tests/axiom-audit.sh` | PASS — 7/7 modules reachable from `CompositionalDA.All`, no postulates, no FFI, no unsound flags, no holes, all `--safe` |
 | Gate self-test (does the gate reject anything?) | `proofs/tests/gate-selftest.sh` | PASS — see "Last verified" below for the count |
 
-The CI job `proofs` in `.github/workflows/ci.yml` runs exactly those first and
-third commands with `AGDA_BIN` and `Agda_datadir` set to the pinned release
-tarball. `bootstrap.sh` vendors the stdlib at the pinned SHA into
-`proofs/.vendor` (git-ignored) and writes `proofs/.agda-libraries`; the
-self-test reads that file, so the two scripts cannot disagree about which
-library they checked against.
+The CI job `proofs` in `.github/workflows/ci.yml` runs `proofs/check.sh` in a
+digest-pinned `debian:13-slim` container with `agda-bin=2.6.4.3-1+b2` and
+`agda-stdlib=2.1-4` installed from apt. `check.sh` type-checks, audits and
+then runs the self-test; both scripts resolve the prover and the library
+through `proofs/lib.sh`, so they cannot disagree about what they checked
+against.
 
 The exact commands, exit codes and counts of the most recent run are in
 "Last verified" at the end of this file.
@@ -221,41 +221,42 @@ is one control per check in `axiom-audit.sh` (seven). The controls:
 ## Reproducing
 
 ```sh
-proofs/bootstrap.sh                 # vendor the stdlib at the pin, type-check, audit
+proofs/check.sh                     # type-check, audit, then the gate self-test
 proofs/tests/gate-selftest.sh       # prove the gate rejects planted defects
 proofs/tests/axiom-audit.sh         # the audit alone
 ```
 
-`bootstrap.sh` needs exactly `Agda version 2.7.0.1` as `AGDA_BIN` or `agda`
-on `PATH`, with `Agda_datadir` pointing at the release tarball's `data/`
-directory; it prints the install steps and fails if the version differs. It
-does not install Agda (no package manager, no Python) and never writes into
-the toolchain's data directory. **An absent prover is a failure, never a
+`check.sh` needs Debian 13's `agda-bin` 2.6.4.3 and `agda-stdlib` 2.1
+(`apt install agda agda-stdlib`); `lib.sh` fails, naming the version it saw,
+if anything else is found first. Nothing is downloaded and nothing is written
+into the toolchain's data directory. **An absent prover is a failure, never a
 skip** — in CI and locally alike.
 
 ## Last verified
 
-2026-10-02, one run of the unmodified CI interface, from an **empty**
-`proofs/.vendor` (so the stdlib was fetched at the pin and type-checked from
-scratch), with the release binary the CI job downloads:
+2026-10-02, after rebasing onto PR #2 (`320513d`, which added `StepUp` and
+the 18-control self-test), one run of the CI interface with Debian 13's
+packages (`agda-bin 2.6.4.3-1+b2`, `agda-stdlib 2.1-4`), interface files
+deleted first so every module was checked from source:
 
 ```
-AGDA_BIN=…/Agda-v2.7.0.1/bin/agda  Agda_datadir=…/Agda-v2.7.0.1/data
-proofs/bootstrap.sh              → exit 0   (7 modules reachable from CompositionalDA.All; axiom-audit: clean)
+proofs/check.sh                  → exit 0   (check: Agda version 2.6.4.3, standard-library-2.1;
+                                             axiom-audit: 7 module(s) reachable from CompositionalDA.All, clean;
+                                             CompositionalDA/All.agda type-checks;
+                                             gate-selftest: 18/18 controls behaved correctly)
 proofs/tests/gate-selftest.sh    → exit 0   (gate-selftest: 18/18 controls behaved correctly)
 proofs/tests/axiom-audit.sh      → exit 0   (auditing 7 module(s); axiom-audit: clean)
 ```
 
-Wall-clock 14:18:26Z → 14:22:32Z, almost all of it the stdlib. The self-test
-was re-run after rebasing onto PR #1, which added the four remaining audit
-controls; a planted wrong reason on one of them was reported as a FAIL
-(17/18), so the reason check is live. The 18
-controls are the 14 mutations, the 3 `reject/` files and the pristine tree
-listed above; each mutation was confirmed to have changed its file before the
-gate was run, and each `reject/` file was refused with exit 42 and the error
-its `-- EXPECT:` line names.
+Wall-clock 14:58:02Z → 15:00:00Z. The only source change the 2.1 library
+needed was `_≡?_` → `_≟_` on ℤ in `Prelude.agda`; `StepUp.agda` needed
+none. The 18 controls are the 14 mutations, the 3 `reject/` files and the
+pristine tree listed above; each mutation is confirmed to have changed its
+file before the gate runs, and each `reject/` file is refused with exit 42
+and the error its `-- EXPECT:` line names. The same 18/18 was obtained on
+Agda 2.7.0.1 with the stdlib development SHA at PR #2 (14:18Z–14:22Z).
 
-The Julia side, same day:
+The Julia side, same run:
 
 ```
 julia --project -e 'using Pkg; Pkg.test()'   → exit 0   (Test Summary: CompositionalDA | Pass 43 | Total 43)

diff --git a/proofs/agda/CompositionalDA/Prelude.agda b/proofs/agda/CompositionalDA/Prelude.agda
@@ -23,7 +23,7 @@ module CompositionalDA.Prelude where
 
 open import Data.Integer as ℤ using (ℤ; +_; +0; +[1+_]; -[1+_]; _*_; _+_; _≤_)
 open import Data.Integer.Properties as ℤₚ
-  using (pos-*; pos-+; *-comm; *-zeroˡ; _≡?_; *-monoʳ-≤-nonNeg)
+  using (pos-*; pos-+; *-comm; *-zeroˡ; _≟_; *-monoʳ-≤-nonNeg)
   renaming (+-*-commutativeRing to +-*-commutativeRingℤ)
 open import Data.Nat.Base using (z≤n)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
@@ -44,7 +44,7 @@ open import Relation.Nullary.Decidable using (yes; no)
 infix 4 _≟ℚᵘ_
 
 _≟ℚᵘ_ : Decidable _≃_
-p ≟ℚᵘ q with (↥ p * ↧ q) ≡? (↥ q * ↧ p)
+p ≟ℚᵘ q with (↥ p * ↧ q) ≟ (↥ q * ↧ p)
 ... | yes e  = yes (*≡* e)
 ... | no  ¬e = no (λ where (*≡* e) → ¬e e)
 
@@ -67,7 +67,7 @@ import Algebra.Solver.Ring.Simple as RingSolver
 module ℚᵘ-Solver = RingSolver (fromCommutativeRing +-*-commutativeRing) _≟ℚᵘ_
 open ℚᵘ-Solver public using (con; _:+_; _:*_; _:=_) renaming (solve to solve-ℚ)
 
-module ℤ-Solver = RingSolver (fromCommutativeRing +-*-commutativeRingℤ) _≡?_
+module ℤ-Solver = RingSolver (fromCommutativeRing +-*-commutativeRingℤ) _≟_
 open ℤ-Solver public using ()
   renaming (solve to solve-ℤ; _:=_ to _:=ℤ_; con to conℤ; _:+_ to _:+ℤ_; _:*_ to _:*ℤ_)
 

diff --git a/proofs/agda/compositionalda.agda-lib b/proofs/agda/compositionalda.agda-lib
@@ -1,4 +1,4 @@
 name: compositionalda
 include: .
-depend: standard-library
+depend: standard-library-2.1
 flags: --safe --without-K