chore(naming)+ci: migrate 6a2 → descriptiles; harden proofs CI (#102)

## Summary

Follow-up to the completed docs sweep (#101), doing the two things
flagged there
plus the wiki publish (already pushed live — see below).

### 1. `6a2/` → `descriptiles/` (estate naming mandate)
The machine-readable metadata family is `descriptiles`; `6a2` is fully
deprecated
(estate mandate 2026-06-30, `standards/CANONICAL-NAMES.adoc`). This
renames
`.machine_readable/6a2/` → `.machine_readable/descriptiles/` (as git
renames,
history preserved) and migrates **every** `6a2` reference across the
repo (21
files: docs, wiki, AUDIT, GOVERNANCE, RSR_COMPLIANCE, the contractile
`Mustfile`
validation invariants, `.well-known/ai.txt`, and the metadata files' own
cross-references). Zero residual `6a2`.

### 2. Harden the proofs CI (`.github/workflows/proofs.yml`)
- Three **independent** jobs — Coq (14 theories, both pillars), Agda
(CNO + OND),
  Z3 (CNO + OND bounded) — so one flaking never reds the others.
- Pinned to **`ubuntu-24.04`** (ships Coq 8.18 — exactly what the proofs
need) to
stop apt version drift; `concurrency` cancel-in-progress; SHA-pinned
checkout;
  `contents: read`.
- Heavy provers (Lean+Mathlib, Isabelle, Mizar, Idris) stay on the local
gate
  `proofs/verify-all-provers.sh`, documented in-file.

### Wiki (done, live)
The 13-page `docs/wiki` — previously **never published** (the live wiki
was a
1-line stub) — has been published to the GitHub wiki, with repo-relative
links
rewritten to `blob/main` URLs and sibling links to wiki-style.
`docs/wiki`
remains the in-repo source of truth. (Wiki push is separate from this
PR.)

## Test
`just build-coq` → 14/14; `proofs.yml` validates; `git grep 6a2` →
empty.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

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

Author: hyperpolymath

.github/workflows/proofs.yml

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

.machine_readable/contractiles/Dustfile.a2ml

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

.machine_readable/contractiles/Intentfile.a2ml

@@ -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]

.machine_readable/contractiles/Mustfile.a2ml

@@ -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]]

.machine_readable/6a2/0-AI-MANIFEST.a2ml …readable/descriptiles/0-AI-MANIFEST.a2ml.machine_readable/6a2/0-AI-MANIFEST.a2ml renamed to .machine_readable/descriptiles/0-AI-MANIFEST.a2ml .machine_readable/6a2/0-AI-MANIFEST.a2ml renamed to .machine_readable/descriptiles/0-AI-MANIFEST.a2ml

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

.machine_readable/6a2/AGENTIC.a2ml …chine_readable/descriptiles/AGENTIC.a2ml.machine_readable/6a2/AGENTIC.a2ml renamed to .machine_readable/descriptiles/AGENTIC.a2ml .machine_readable/6a2/AGENTIC.a2ml renamed to .machine_readable/descriptiles/AGENTIC.a2ml

@@ -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)

.machine_readable/6a2/ECOSYSTEM.a2ml …ine_readable/descriptiles/ECOSYSTEM.a2ml.machine_readable/6a2/ECOSYSTEM.a2ml renamed to .machine_readable/descriptiles/ECOSYSTEM.a2ml .machine_readable/6a2/ECOSYSTEM.a2ml renamed to .machine_readable/descriptiles/ECOSYSTEM.a2ml

@@ -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)