hyperpolymath · hyperpolymath · Jul 7, 2026 · Jul 7, 2026
@@ -1,11 +1,14 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 #
-# Proof verification CI. Runs the LIGHTWEIGHT provers that are feasible on a
-# standard GitHub runner — Coq (both pillars, all 14 theories) and Z3 (CNO +
-# OND bounded instances). The full six-prover gate (adds Lean+Mathlib, Agda,
-# Isabelle, Mizar, Idris) is heavy and runs locally / in a container via
-# `proofs/verify-all-provers.sh`; see PROOF-STATUS.adoc.
+# Proof verification CI. Runs the LIGHTWEIGHT provers that are fast and reliable
+# on a standard GitHub runner — Coq (both pillars, all 14 theories), Agda (CNO +
+# OND), and Z3 (CNO + OND bounded instances). Each is an INDEPENDENT job, so one
+# flaking never blocks the others.
+#
+# The heavy provers (Lean + multi-GB Mathlib, Isabelle ~1.2 GB, Mizar i386 + MML,
+# Idris 2 from source) are NOT run here — they are covered by the local/container
+# gate `proofs/verify-all-provers.sh` (ALL-PROVERS-GREEN). See PROOF-STATUS.adoc.
 name: Proofs
 
 on:
@@ -24,10 +27,15 @@ on:
 permissions:
   contents: read
 
+# Cancel superseded runs on the same ref (don't pile up on force-pushes).
+concurrency:
+  group: proofs-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   coq:
     name: Coq — CNO + OND (14 theories)
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4
       - name: Install Coq
@@ -40,9 +48,35 @@ jobs:
           make -f Makefile.all -j"$(nproc)"
           echo "✓ Coq: 14/14 theories compiled (CNO + OND)"
 
+  agda:
+    name: Agda — CNO + OND
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4
+      - name: Install Agda + stdlib
+        run: sudo apt-get update && sudo apt-get install -y agda agda-stdlib
+      - name: Register the standard library
+        run: |
+          mkdir -p "$HOME/.agda"
+          LIB="$(dpkg -L agda-stdlib | grep -m1 'standard-library.*\.agda-lib' || true)"
+          if [ -n "$LIB" ]; then
+            echo "$LIB" > "$HOME/.agda/libraries"
+            echo "standard-library" > "$HOME/.agda/defaults"
+            echo "registered: $LIB"
+          else
+            echo "agda-stdlib .agda-lib not found via dpkg -L" >&2; exit 1
+          fi
+      - name: Type-check CNO + OND (--safe --without-K)
+        working-directory: proofs/agda
+        run: |
+          agda --version
+          agda --safe --without-K CNO.agda
+          agda --safe --without-K OND.agda
+          echo "✓ Agda: CNO + OND type-check"
+
   z3:
-    name: Z3 — OND bounded checks
-    runs-on: ubuntu-latest
+    name: Z3 — CNO + OND bounded checks
+    runs-on: ubuntu-24.04
     steps:
       - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4
       - name: Install Z3

@@ -43,7 +43,7 @@ notes = "Exercised precedent: PR #69 repinned orphan reusable SHAs (97df7621/4fd
 
 [[recovery]]
 id = "stale-machine-metadata"
-asset = ".machine_readable/ (6a2, contractiles, bot_directives)"
+asset = ".machine_readable/ (descriptiles, contractiles, bot_directives)"
 reversible = true
 handler = "Regenerate from repo facts: git log since the last STATE date + repo docs, per the governance-checkpoint discipline; prior states recoverable from git history"
 notes = "STATE refreshes are additive light-bumps; never invent facts — omit unknown keys."

@@ -12,7 +12,7 @@
 #
 # Populated 2026-06-12 (governance checkpoint): replaces the
 # rsr-template-repo stub. Sources: README.adoc, ROADMAP.adoc,
-# 6a2/STATE.a2ml ([route-to-mvp], [critical-next-actions], [blockers-and-issues]).
+# descriptiles/STATE.a2ml ([route-to-mvp], [critical-next-actions], [blockers-and-issues]).
 # A2ML here is TOML-flavoured.
 
 [metadata]

@@ -17,7 +17,7 @@
 repo = "absolute-zero"
 contractile-verb = "must"
 last-updated = "2026-06-12"
-abstract = "Physical-state invariants for absolute-zero: required governance files, the flat contractile set, the 6a2 metadata set, and the absence of superseded duplicate metadata."
+abstract = "Physical-state invariants for absolute-zero: required governance files, the flat contractile set, the descriptiles metadata set, and the absence of superseded duplicate metadata."
 
 [[checks]]
 id = "license-present"
@@ -57,14 +57,14 @@ severity = "critical"
 
 [[checks]]
 id = "six-a2ml-present"
-description = "6a2 directory has all six A2ML files plus manifest and README"
-run = "test -f .machine_readable/6a2/STATE.a2ml && test -f .machine_readable/6a2/META.a2ml && test -f .machine_readable/6a2/ECOSYSTEM.a2ml && test -f .machine_readable/6a2/AGENTIC.a2ml && test -f .machine_readable/6a2/NEUROSYM.a2ml && test -f .machine_readable/6a2/PLAYBOOK.a2ml && test -f .machine_readable/6a2/0-AI-MANIFEST.a2ml"
+description = "descriptiles directory has all six A2ML files plus manifest and README"
+run = "test -f .machine_readable/descriptiles/STATE.a2ml && test -f .machine_readable/descriptiles/META.a2ml && test -f .machine_readable/descriptiles/ECOSYSTEM.a2ml && test -f .machine_readable/descriptiles/AGENTIC.a2ml && test -f .machine_readable/descriptiles/NEUROSYM.a2ml && test -f .machine_readable/descriptiles/PLAYBOOK.a2ml && test -f .machine_readable/descriptiles/0-AI-MANIFEST.a2ml"
 severity = "critical"
 
 [[checks]]
 id = "anchor-directory"
-description = "6a2/anchor/ exists with ANCHOR.a2ml (realignment record)"
-run = "test -d .machine_readable/6a2/anchor && test -f .machine_readable/6a2/anchor/ANCHOR.a2ml"
+description = "descriptiles/anchor/ exists with ANCHOR.a2ml (realignment record)"
+run = "test -d .machine_readable/descriptiles/anchor && test -f .machine_readable/descriptiles/anchor/ANCHOR.a2ml"
 severity = "warning"
 
 [[checks]]
@@ -81,14 +81,14 @@ severity = "warning"
 
 [[checks]]
 id = "no-duplicate-root-scm"
-description = "No duplicate root .machine_readable/*.scm set (removed by estate wave 2026-06; 6a2/*.a2ml is canonical)"
+description = "No duplicate root .machine_readable/*.scm set (removed by estate wave 2026-06; descriptiles/*.a2ml is canonical)"
 run = "test -z \"$(ls .machine_readable/*.scm 2>/dev/null)\""
 severity = "critical"
 
 [[checks]]
 id = "a2ml-parses-as-toml"
-description = "Every 6a2 A2ML file parses as TOML"
-run = "for f in .machine_readable/6a2/STATE.a2ml .machine_readable/6a2/META.a2ml .machine_readable/6a2/ECOSYSTEM.a2ml .machine_readable/6a2/AGENTIC.a2ml .machine_readable/6a2/NEUROSYM.a2ml .machine_readable/6a2/PLAYBOOK.a2ml; do python3 -c \"import tomllib;tomllib.load(open('$f','rb'))\" || exit 1; done"
+description = "Every descriptiles A2ML file parses as TOML"
+run = "for f in .machine_readable/descriptiles/STATE.a2ml .machine_readable/descriptiles/META.a2ml .machine_readable/descriptiles/ECOSYSTEM.a2ml .machine_readable/descriptiles/AGENTIC.a2ml .machine_readable/descriptiles/NEUROSYM.a2ml .machine_readable/descriptiles/PLAYBOOK.a2ml; do python3 -c \"import tomllib;tomllib.load(open('$f','rb'))\" || exit 1; done"
 severity = "critical"
 
 [[checks]]

@@ -1,8 +1,8 @@
-# AI Manifest for 6a2 Directory
+# AI Manifest for descriptiles Directory
 
 ## Purpose
 
-This manifest declares the AI-assistant context for the 6a2 machine-readable metadata directory.
+This manifest declares the AI-assistant context for the descriptiles machine-readable metadata directory.
 
 ## Canonical Locations
 

@@ -51,6 +51,6 @@ recommended = ["read", "edit", "bash", "grep", "glob"]
 permissions = "read-all"
 
 [automation-hooks]
-# on-enter: Read AI.a2ml, then .machine_readable/6a2/STATE.a2ml
-# on-exit: Update .machine_readable/6a2/STATE.a2ml with session outcomes
+# on-enter: Read AI.a2ml, then .machine_readable/descriptiles/STATE.a2ml
+# on-exit: Update .machine_readable/descriptiles/STATE.a2ml with session outcomes
 # on-commit: Run just validate-rsr (if available)
@@ -31,14 +31,14 @@ build-mizar     = "just build-mizar"
 build-idris     = "just build-idris"
 
 [incident-response]
-# 1. Check .machine_readable/6a2/STATE.a2ml for current status
+# 1. Check .machine_readable/descriptiles/STATE.a2ml for current status
 # 2. Review recent commits: git log --oneline -10
 # 3. Run `just validate` if available
 # 4. Run `just security` for vulnerability audit
 # 5. For proof failures: check proofs/<system>/ for unsaved Admitted/sorry
 
 [release-process]
-# 1. Update version in .machine_readable/6a2/STATE.a2ml and META.a2ml
+# 1. Update version in .machine_readable/descriptiles/STATE.a2ml and META.a2ml
 # 2. Resolve all Admitted/sorry entries to target count
 # 3. Run `just build-all` to confirm no regressions
 # 4. Tag and push to origin (GitHub only)

@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-# A2ML 6a2 Directory
+# A2ML descriptiles Directory
 
 This directory contains the 6 core A2ML machine-readable metadata files for this repository.
 

@@ -16,9 +16,9 @@ last-updated = "2026-06-12"
 date = "2026-06-12"
 title = "Estate standardization + governance checkpoint"
 what-changed = [
-  "Merged origin/estate-standardization-20260607: flat .machine_readable/contractiles/ layout, svc/k9 → self-validating/ rename, GOVERNANCE.adoc + MAINTAINERS.adoc + .github/CODEOWNERS, Guix manifest.scm, 6a2 0-AI-MANIFEST.a2ml + README.adoc + anchor/, removal of the duplicate root .machine_readable/*.scm set and the root contractiles/ template dir, SPDX header normalization",
+  "Merged origin/estate-standardization-20260607: flat .machine_readable/contractiles/ layout, svc/k9 → self-validating/ rename, GOVERNANCE.adoc + MAINTAINERS.adoc + .github/CODEOWNERS, Guix manifest.scm, descriptiles 0-AI-MANIFEST.a2ml + README.adoc + anchor/, removal of the duplicate root .machine_readable/*.scm set and the root contractiles/ template dir, SPDX header normalization",
   "Conflict resolution: .github/workflows/rust-ci.yml kept at origin/main's version; .claude/CLAUDE.md kept identical to origin/main",
-  "Governance checkpoint layer: bot_directives/ (README.adoc, hypatia.a2ml, gitbot-fleet.a2ml, git-private-farm.a2ml); flat contractiles fully populated with repo-true content (template stubs replaced; old nested bust/trust content ported; new Dustfile.a2ml + Bustfile.a2ml); 6a2/STATE.a2ml light-bump to 2026-06-12 with [recent-work]; README.md pointer-ized to canonical README.adoc; docs/archive/ index README; wiki Home.md currency fixes (license MPL-2.0, axiom count 72, status note)",
+  "Governance checkpoint layer: bot_directives/ (README.adoc, hypatia.a2ml, gitbot-fleet.a2ml, git-private-farm.a2ml); flat contractiles fully populated with repo-true content (template stubs replaced; old nested bust/trust content ported; new Dustfile.a2ml + Bustfile.a2ml); descriptiles/STATE.a2ml light-bump to 2026-06-12 with [recent-work]; README.md pointer-ized to canonical README.adoc; docs/archive/ index README; wiki Home.md currency fixes (license MPL-2.0, axiom count 72, status note)",
 ]
 why = "Per-repo governance refresh aligning absolute-zero with the estate standard fully landed in echo-types (PR #185 there); checkpoint of 2026-06-12"
 evidence = [

@@ -5,7 +5,7 @@
 User-Agent: *
 Manifest: /0-AI-MANIFEST.a2ml
 EntryPoint: /docs/CLAUDE.adoc
-State: /.machine_readable/6a2/STATE.a2ml
+State: /.machine_readable/descriptiles/STATE.a2ml
 Roadmap: /ROADMAP.adoc
 Allow: training-with-attribution
 Allow: documentation-summarisation

@@ -19,22 +19,22 @@ purpose = """
 [entry-points]
 # Where an AI agent should look first.
 root-context  = "docs/CLAUDE.adoc"
-project-state = ".machine_readable/6a2/STATE.a2ml"
+project-state = ".machine_readable/descriptiles/STATE.a2ml"
 roadmap       = "ROADMAP.adoc"
 contributing  = "CONTRIBUTING.adoc"
 audit-trail   = "AUDIT.adoc"
 rsr-status    = "RSR_COMPLIANCE.adoc"
 
 [machine-readable]
-# Authoritative metadata artefacts; .a2ml format under 6a2/ supersedes
+# Authoritative metadata artefacts; .a2ml format under descriptiles/ supersedes
 # the older Guile-Scheme .scm format. Both kept side-by-side during the
 # migration window for legacy tooling compatibility.
-state     = ".machine_readable/6a2/STATE.a2ml"
-meta      = ".machine_readable/6a2/META.a2ml"
-ecosystem = ".machine_readable/6a2/ECOSYSTEM.a2ml"
-agentic   = ".machine_readable/6a2/AGENTIC.a2ml"
-neurosym  = ".machine_readable/6a2/NEUROSYM.a2ml"
-playbook  = ".machine_readable/6a2/PLAYBOOK.a2ml"
+state     = ".machine_readable/descriptiles/STATE.a2ml"
+meta      = ".machine_readable/descriptiles/META.a2ml"
+ecosystem = ".machine_readable/descriptiles/ECOSYSTEM.a2ml"
+agentic   = ".machine_readable/descriptiles/AGENTIC.a2ml"
+neurosym  = ".machine_readable/descriptiles/NEUROSYM.a2ml"
+playbook  = ".machine_readable/descriptiles/PLAYBOOK.a2ml"
 
 legacy-scm-meta      = ".machine_readable/META.scm"
 legacy-scm-ecosystem = ".machine_readable/ECOSYSTEM.scm"
@@ -67,5 +67,5 @@ tools = [
 
 [delivery]
 commit-policy = "conventional commits; never amend published commits"
-state-update  = "update .machine_readable/6a2/STATE.a2ml whenever phase/progress changes"
+state-update  = "update .machine_readable/descriptiles/STATE.a2ml whenever phase/progress changes"
 adr-tracking  = "architectural changes recorded in .machine_readable/META.scm `architecture-decisions`"
@@ -13,7 +13,7 @@ audits, and other trust-boundary events.
 
 For architectural decisions (which are forward-looking design choices
 rather than backward-looking audit events), see
-`.machine_readable/6a2/META.a2ml` `architecture-decisions`.
+`.machine_readable/descriptiles/META.a2ml` `architecture-decisions`.
 
 == Open Audit Items
 
@@ -74,7 +74,7 @@ PR #100 — see Resolved Audit Items below._
 |2026-05-20
 |`eval_deterministic` discharged from Axiom → Theorem via
  `step_deterministic_strong` helper. First post-T0 axiom audit win.
-|PR #24 (see 6a2/META.a2ml ADR-007)
+|PR #24 (see descriptiles/META.a2ml ADR-007)
 
 |AUDIT-2026-05-20-#32
 |2026-05-20
@@ -83,7 +83,7 @@ PR #100 — see Resolved Audit Items below._
  (`=st=`); re-proved `cno_eval_on_equal_states` +
  `cno_logically_reversible` via `cno_terminates` +
  `cno_preserves_state`.
-|PR #32 (see 6a2/META.a2ml ADR-008)
+|PR #32 (see descriptiles/META.a2ml ADR-008)
 
 |AUDIT-2026-02-05
 |2026-02-05
@@ -102,6 +102,6 @@ Audit IDs follow `AUDIT-<YYYY-MM-DD>-<seq-or-PR>`:
 
 == See also
 
-* `.machine_readable/6a2/META.a2ml` — forward-looking architecture decisions (ADR-001…N)
+* `.machine_readable/descriptiles/META.a2ml` — forward-looking architecture decisions (ADR-001…N)
 * `docs/archive/` — historical session / audit artefacts (dated)
 * `RSR_COMPLIANCE.adoc` — Rhodium Standard Repository compliance status
@@ -128,7 +128,7 @@ This repository adheres to hyperpolymath estate-wide policies:
 
 | **Contractiles** | Mustfile, Trustfile, Intendfile, Adjustfile in root
 
-| **Machine Readable** | META.a2ml in .machine_readable/6a2/
+| **Machine Readable** | META.a2ml in .machine_readable/descriptiles/
 
 | **CI/CD** | GitHub Actions workflows in .github/workflows/
 

@@ -37,7 +37,7 @@ For the RSR taxonomy itself (what the template prescribes), see
 
 |Machine-readable artefacts
 |✅ Passing
-|`.machine_readable/6a2/{STATE,META,ECOSYSTEM,AGENTIC,NEUROSYM,PLAYBOOK}.a2ml`
+|`.machine_readable/descriptiles/{STATE,META,ECOSYSTEM,AGENTIC,NEUROSYM,PLAYBOOK}.a2ml`
  + legacy `.scm` siblings during migration window.
 
 |`0-AI-MANIFEST.a2ml`
@@ -98,4 +98,4 @@ For the RSR taxonomy itself (what the template prescribes), see
 * `docs/RSR_OUTLINE.adoc` — the RSR template's own README (what the standard prescribes)
 * `AUDIT.adoc` — audit trail for unsoundness/dead-code findings
 * `0-AI-MANIFEST.a2ml` — AI-agent entry-point manifest
-* `.machine_readable/6a2/STATE.a2ml` — live project state
+* `.machine_readable/descriptiles/STATE.a2ml` — live project state
@@ -10,7 +10,7 @@ snapshots or by updating the live documents listed below.
 
 Authoritative live sources:
 
-* Project state — `.machine_readable/6a2/STATE.a2ml`
+* Project state — `.machine_readable/descriptiles/STATE.a2ml`
 * Roadmap — `ROADMAP.adoc` (repo root)
 * Proof-debt disposition — `docs/proof-debt-triage.md` and `docs/proof-debt.md`
 * Audit findings — `AUDIT.adoc` (repo root)
@@ -21,9 +21,9 @@ Authoritative live sources:
 |===
 | File | Date | What it was | Superseded by
 
-| `CURRENT-STATUS-2026-02-05.md` | 2026-02-05 | Point-in-time project status | `.machine_readable/6a2/STATE.a2ml`
+| `CURRENT-STATUS-2026-02-05.md` | 2026-02-05 | Point-in-time project status | `.machine_readable/descriptiles/STATE.a2ml`
 | `ECHIDNA-2025-11-22.adoc` | 2025-11-22 | Early ECHIDNA integration notes | `ECHIDNA.adoc`
-| `INTEGRATION-STATUS-2026-02-05.adoc` | 2026-02-05 | Integration status snapshot | `.machine_readable/6a2/STATE.a2ml`
+| `INTEGRATION-STATUS-2026-02-05.adoc` | 2026-02-05 | Integration status snapshot | `.machine_readable/descriptiles/STATE.a2ml`
 | `LICENSE-AUDIT-2026-02-05.adoc` | 2026-02-05 | License audit snapshot | `LICENSE` (MPL-2.0)
 | `PROOF-COMPLETION-2026-02-06.md` | 2026-02-06 | Proof-completion plan snapshot | `docs/PROOF-COMPLETION-PLAN.adoc`
 | `PROOF-STATUS-2026-05-18.md` | 2026-05-18 | Tier-0 rescue proof-status ledger | `docs/proof-debt-triage.md`, `AUDIT.adoc`

@@ -44,7 +44,7 @@ just fmt
 ## ADR / Audit trail
 
 * If your change is an **architectural decision** going forward, add an ADR
-  entry to [`.machine_readable/6a2/META.a2ml`](../../.machine_readable/6a2/META.a2ml)
+  entry to [`.machine_readable/descriptiles/META.a2ml`](../../.machine_readable/descriptiles/META.a2ml)
   (next ADR-NNN).
 * If your change **discharges a postulate / deletes unsound code**, add an
   AUDIT entry to [`AUDIT.adoc`](../../AUDIT.adoc).

@@ -66,7 +66,7 @@ external world, not gaps in the verification of the computational claim.
 
 ### Where's the live state?
 
-`.machine_readable/6a2/STATE.a2ml`. Updated on every meaningful change.
+`.machine_readable/descriptiles/STATE.a2ml`. Updated on every meaningful change.
 
 ### Why "Absolute Zero"?