diff --git a/.github/.mailmap b/.github/.mailmap
index 38c8dda..37c6e83 100644
--- a/.github/.mailmap
+++ b/.github/.mailmap
@@ -1 +1 @@
-Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> <{{AUTHOR_EMAIL_ALT}}>
+Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> <6759885+hyperpolymath@users.noreply.github.com>
diff --git a/.github/pull_request_template.md b/.github/pull_request_template.md
index 2132109..391e718 100644
--- a/.github/pull_request_template.md
+++ b/.github/pull_request_template.md
@@ -29,14 +29,14 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 ### As Applicable
 
-- [ ] `.machine_readable/STATE.a2ml` updated (if project state changed)
-- [ ] `.machine_readable/ECOSYSTEM.a2ml` updated (if integrations changed)
-- [ ] `.machine_readable/META.a2ml` updated (if architectural decisions changed)
-- [ ] Documentation updated for user-facing changes
-- [ ] `TOPOLOGY.md` updated (if architecture changed)
-- [ ] `CHANGELOG` or release notes updated
-- [ ] New dependencies reviewed for license compatibility (MPL-2.0 / MPL-2.0)
-- [ ] ABI/FFI changes validated (`src/interface/abi/` and `src/interface/ffi/` consistent)
+- [ ] `.machine_readable/descriptiles/STATE.a2ml` updated (if project state changed)
+- [ ] `.machine_readable/descriptiles/ECOSYSTEM.a2ml` updated (if integrations changed)
+- [ ] `.machine_readable/descriptiles/META.a2ml` updated (if architectural decisions changed)
+- [ ] Documentation updated (`docs/ARCHITECTURE.adoc`, `docs/PIPELINE.adoc`, `docs/TYPE-CONNECTIONS.adoc`)
+- [ ] `TOPOLOGY.adoc` updated (if architecture changed)
+- [ ] `CHANGELOG.adoc` or release notes updated
+- [ ] New dependencies reviewed for license compatibility (MPL-2.0)
+- [ ] Cross-project proof & coordination gates validated (`verification/proofs/` and `scripts/check-coordination-boundary.sh`)
 
 ## Testing
 
diff --git a/.github/settings.yml b/.github/settings.yml
index 7dd7fa4..a83aa45 100644
--- a/.github/settings.yml
+++ b/.github/settings.yml
@@ -12,13 +12,13 @@
 # It carries NO `name`, `description`, `homepage` or `private` key, and it must
 # never gain one. The reason is a real incident, not a hypothetical:
 #
-#   This file previously read `name: "{{REPO}}"`. probot/settings applies it on
+#   This file previously read `name: "<REPO>"`. probot/settings applies it on
 #   every push to the default branch, so it submitted the literal string
-#   `{{REPO}}` as the repository name. GitHub sanitises an invalid name by
-#   collapsing each run of illegal characters to a dash — `{{REPO}}` became
+#   `<REPO>` as the repository name. GitHub sanitises an invalid name by
+#   collapsing each run of illegal characters to a dash — `<REPO>` became
 #   `-REPO-`. The template renamed itself on every push, its old URL 404'd, and
 #   it was mistaken for a deleted repository. `description` was likewise left
-#   reading the literal `{{DESCRIPTION}}` on the live repo.
+#   reading the literal `<DESCRIPTION>` on the live repo.
 #
 # Two properties make identity keys unsafe here specifically:
 #
diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock
index 34f89b9..93cf273 100644
--- a/.github/workflows/actions.lock
+++ b/.github/workflows/actions.lock
@@ -17,15 +17,20 @@ workflows:
         - 'hyperpolymath/deed-ecosystem@main'
         - 'hyperpolymath/k9-ecosystem@main'
     '.github/workflows/e2e.yml': []
-    '.github/workflows/governance.yml': []
+    '.github/workflows/governance.yml':
+        - 'actions/checkout@v7.0.1'
     '.github/workflows/guix-nix-policy.yml':
         - 'actions/checkout@v7.0.1'
-    '.github/workflows/hypatia-scan.yml': []
+    '.github/workflows/hypatia-scan.yml':
+        - 'actions/checkout@v7.0.1'
+        - 'erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124'
+        - 'github/codeql-action@v4.39.1'
     '.github/workflows/instant-sync.yml':
         - 'peter-evans/repository-dispatch@v4.0.1'
     '.github/workflows/label-triage.yml': []
     '.github/workflows/labels.yml': []
-    '.github/workflows/mirror.yml': []
+    '.github/workflows/mirror.yml':
+        - 'actions/checkout@v7.0.1'
     '.github/workflows/openssf-compliance.yml':
         - 'actions/checkout@v7.0.1'
     '.github/workflows/pages.yml':
@@ -51,9 +56,13 @@ workflows:
         - 'actions/checkout@v7.0.1'
     '.github/workflows/runtime-policy.yml':
         - 'actions/checkout@v7.0.1'
-    '.github/workflows/rust-ci.yml': []
-    '.github/workflows/scorecard.yml': []
-    '.github/workflows/secret-scanner.yml': []
+    '.github/workflows/rust-ci.yml':
+        - 'actions/checkout@v7.0.1'
+    '.github/workflows/scorecard.yml':
+        - 'actions/checkout@v7.0.1'
+        - 'github/codeql-action@v4.39.1'
+    '.github/workflows/secret-scanner.yml':
+        - 'actions/checkout@v7.0.1'
     '.github/workflows/security-policy.yml':
         - 'actions/checkout@v7.0.1'
     '.github/workflows/static-analysis-gate.yml':
@@ -108,6 +117,11 @@ dependencies:
         commit: 'sha1-51f63319f592f97930c73d9c46184d20bd206393'
         owner_id: 26415196
         repo_id: 297874902
+    'erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124':
+        ref: 'v1.24.1'
+        commit: 'sha1-54075bcc5e249e4758d363f27d099f55d843f124'
+        owner_id: 47606891
+        repo_id: 331103973
     'erlef/setup-beam@v1.24.1':
         ref: 'v1.24.1'
         commit: 'sha1-54075bcc5e249e4758d363f27d099f55d843f124'
diff --git a/.github/workflows/dependabot-automerge.yml b/.github/workflows/dependabot-automerge.yml
index 7dd4b34..415735e 100644
--- a/.github/workflows/dependabot-automerge.yml
+++ b/.github/workflows/dependabot-automerge.yml
@@ -49,8 +49,9 @@ permissions:
 
 jobs:
   automerge:
-    # Only run for PRs actually authored by Dependabot.
-    if: github.actor == 'dependabot[bot]' && github.event.pull_request.user.login == 'dependabot[bot]'
+    # Only run for PRs actually authored by Dependabot (verified via immutable
+    # pull_request.user.id 49699333 + user.login, never spoofable github.actor).
+    if: github.event.pull_request.user.login == 'dependabot[bot]' && github.event.pull_request.user.id == 49699333
     runs-on: ubuntu-latest
     timeout-minutes: 15
 
diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml
index 08a6a9c..ce9b4c5 100644
--- a/.github/workflows/governance.yml
+++ b/.github/workflows/governance.yml
@@ -1,6 +1,5 @@
 # This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
-# This workflow is managed by gh actions-lock.
 name: Governance
 
 on:
@@ -10,10 +9,127 @@ on:
     branches: [main, master]
   workflow_dispatch:
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 permissions:
-  actions: read
   contents: read
 
+# Self-contained execution of the shared estate governance policies pinned to
+# metadatastician/standards@8e48b1caade08a552646adeab66558ac43b4360d, plus
+# aligned Well-Known RFC 9116 validation over canonical www/.well-known/.
 jobs:
   governance:
-    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@fad242d35291de1898242d6737ba02b74a59a2f2
+    name: Estate Governance Policy
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    permissions:
+      contents: read
+    env:
+      STANDARDS_PIN: '8e48b1caade08a552646adeab66558ac43b4360d'
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: Checkout pinned standards policy scripts
+        uses: actions/checkout@v7.0.1
+        with:
+          repository: metadatastician/standards
+          ref: 8e48b1caade08a552646adeab66558ac43b4360d
+          path: .standards-checkout
+          sparse-checkout: |
+            scripts
+            0-canon
+          sparse-checkout-cone-mode: true
+          persist-credentials: false
+
+      - name: Enforce TypeScript and npm/yarn runtime policy
+        run: |
+          set -euo pipefail
+          if [ -f .standards-checkout/scripts/check-ts-allowlist.sh ]; then
+            bash .standards-checkout/scripts/check-ts-allowlist.sh
+          fi
+          rm -rf .standards-checkout
+
+          bad_ts="$(git ls-files '*.ts' '*.tsx' | grep -vE '^(archetypes/|templates/|tests/fixtures/)' || true)"
+          if [ -n "$bad_ts" ]; then
+            echo "::error::Unallowlisted TypeScript files detected:"
+            printf '%s\n' "$bad_ts"
+            exit 1
+          fi
+
+          bad_locks="$(git ls-files 'package-lock.json' '**/package-lock.json' 'yarn.lock' '**/yarn.lock' 'pnpm-lock.yaml' '**/pnpm-lock.yaml' || true)"
+          if [ -n "$bad_locks" ]; then
+            echo "::error::Banned npm/yarn/pnpm lockfiles detected (use Deno or Bun per LANGUAGE-POLICY):"
+            printf '%s\n' "$bad_locks"
+            exit 1
+          fi
+
+          if [ -f tsconfig.json ] || [ -f Makefile ] || [ -f GNUmakefile ]; then
+            echo "::error::Banned root config (tsconfig.json / Makefile) detected"
+            exit 1
+          fi
+          echo "Governance runtime and language anti-pattern checks passed."
+
+  wellknown:
+    name: Well-Known (RFC 9116 + RSR)
+    runs-on: ubuntu-24.04
+    timeout-minutes: 10
+    permissions:
+      contents: read
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: RFC 9116 security.txt validation
+        run: |
+          set -euo pipefail
+          SECTXT=""
+          if [ -f "www/.well-known/security.txt" ]; then
+            SECTXT="www/.well-known/security.txt"
+          elif [ -f ".well-known/security.txt" ]; then
+            SECTXT=".well-known/security.txt"
+            echo "::warning::security.txt at legacy root .well-known/ — canonical location is www/.well-known/"
+          elif [ -f "security.txt" ]; then
+            SECTXT="security.txt"
+            echo "::warning::security.txt at repository root — canonical location is www/.well-known/"
+          fi
+
+          if [ -z "$SECTXT" ]; then
+            echo "::error::No security.txt found (expected www/.well-known/security.txt)"
+            exit 1
+          fi
+
+          if grep -qE '\{\{[A-Z0-9_]+\}\}' "$SECTXT"; then
+            echo "::error::$SECTXT contains unfilled placeholder tokens"
+            exit 1
+          fi
+
+          grep -q "^Contact:" "$SECTXT" || { echo "::error::Missing Contact field"; exit 1; }
+          grep -q "^Expires:" "$SECTXT" || { echo "::error::Missing Expires field"; exit 1; }
+
+          EXPIRES=$(grep "^Expires:" "$SECTXT" | cut -d: -f2- | tr -d ' ' | head -1)
+          if [[ ! "$EXPIRES" =~ ^[0-9]{4}-[0-9]{2}-[0-9]{2}[Tt][0-9]{2}:[0-9]{2}:[0-9]{2}(\.[0-9]+)?([Zz]|[+-][0-9]{2}:[0-9]{2})$ ]]; then
+            echo "::error::Expires is not an RFC 3339 date-time: $EXPIRES"
+            exit 1
+          fi
+          if ! EXPIRY_EPOCH=$(date -d "$EXPIRES" +%s 2>/dev/null); then
+            echo "::error::Expires is not a valid date-time: $EXPIRES"
+            exit 1
+          fi
+          NOW_EPOCH=$(date +%s)
+          if [ "$EXPIRY_EPOCH" -le "$NOW_EPOCH" ]; then
+            echo "::error::security.txt EXPIRED"
+            exit 1
+          fi
+          DAYS=$(( (EXPIRY_EPOCH - NOW_EPOCH) / 86400 ))
+          if [ "$DAYS" -lt 30 ]; then
+            echo "::warning::security.txt expires in $DAYS days"
+          else
+            echo "security.txt valid ($DAYS days, $SECTXT)"
+          fi
diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml
index b8b7d7a..50915ac 100644
--- a/.github/workflows/hypatia-scan.yml
+++ b/.github/workflows/hypatia-scan.yml
@@ -1,22 +1,107 @@
 # This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
-# This workflow is managed by gh actions-lock.
+#
+# Self-contained Hypatia neurosymbolic security scan + SARIF upload (`category:
+# hypatia`) replacing the retired reusable caller after `standards` transferred.
 name: Hypatia Security Scan
 
 on:
-  push:
-    branches: [main, master, develop]
   pull_request:
     branches: [main, master]
+  push:
+    branches: [main, master, develop]
   schedule:
     - cron: '0 0 * * 0'
   workflow_dispatch:
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 permissions:
-  actions: read
   contents: read
-  security-events: write
 
 jobs:
   hypatia:
-    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a
+    name: Hypatia Neurosymbolic Analysis
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    permissions:
+      contents: read
+      security-events: write
+    env:
+      HYPATIA_SHA: 'd73f76b5cb7a35e1aa1024c916aee7cb4f9b141e'
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v7.0.1
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+
+      - name: Setup Elixir 1.19.4 / OTP 28.3 for Hypatia scanner
+        uses: erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124 # v1.24.1
+        with:
+          elixir-version: '1.19.4'
+          otp-version: '28.3'
+
+      - name: Build pinned Hypatia scanner
+        run: |
+          set -euo pipefail
+          rm -rf "$HOME/hypatia"
+          git init "$HOME/hypatia"
+          git -C "$HOME/hypatia" remote add origin https://github.com/hyperpolymath/hypatia.git
+          git -C "$HOME/hypatia" fetch --depth=1 origin "$HYPATIA_SHA"
+          git -C "$HOME/hypatia" checkout --detach FETCH_HEAD
+          (
+            cd "$HOME/hypatia"
+            mix local.hex --force
+            mix local.rebar --force
+            mix deps.get
+            MIX_NO_PUBSUB=1 mix escript.build
+          )
+          chmod +x "$HOME/hypatia/hypatia" "$HOME/hypatia/hypatia-cli.sh"
+
+      - name: Run Hypatia JSON and SARIF analysis
+        id: scan
+        run: |
+          set -euo pipefail
+          HYPATIA_FORMAT=json "$HOME/hypatia/hypatia-cli.sh" scan . --exit-zero > hypatia-findings.json
+          jq -e 'type == "array"' hypatia-findings.json >/dev/null
+
+          HYPATIA_FORMAT=sarif "$HOME/hypatia/hypatia-cli.sh" scan . --exit-zero > hypatia.sarif
+          jq -e '.runs | type == "array" and length > 0' hypatia.sarif >/dev/null
+
+          CRITICAL="$(jq '[.[] | select(.severity == "critical")] | length' hypatia-findings.json)"
+          HIGH="$(jq '[.[] | select(.severity == "high")] | length' hypatia-findings.json)"
+          TOTAL="$(jq 'length' hypatia-findings.json)"
+          {
+            echo "critical=$CRITICAL"
+            echo "high=$HIGH"
+            echo "total=$TOTAL"
+          } >> "$GITHUB_OUTPUT"
+
+      - name: Upload Hypatia SARIF to GitHub Code Scanning
+        if: github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository
+        uses: github/codeql-action/upload-sarif@v4.39.1
+        with:
+          sarif_file: hypatia.sarif
+          category: hypatia
+
+      - name: Enforce zero critical Hypatia findings
+        env:
+          CRITICAL_COUNT: ${{ steps.scan.outputs.critical }}
+          HIGH_COUNT: ${{ steps.scan.outputs.high }}
+          TOTAL_COUNT: ${{ steps.scan.outputs.total }}
+        run: |
+          set -euo pipefail
+          {
+            echo "## Hypatia Neurosymbolic Scan"
+            echo ""
+            echo "- Critical: ${CRITICAL_COUNT}"
+            echo "- High: ${HIGH_COUNT}"
+            echo "- Total findings: ${TOTAL_COUNT}"
+          } >> "$GITHUB_STEP_SUMMARY"
+          if [ "$CRITICAL_COUNT" != "0" ]; then
+            echo "::error::Hypatia reported ${CRITICAL_COUNT} critical finding(s)"
+            exit 1
+          fi
diff --git a/.github/workflows/label-triage.yml b/.github/workflows/label-triage.yml
index 814a192..7bbe468 100644
--- a/.github/workflows/label-triage.yml
+++ b/.github/workflows/label-triage.yml
@@ -47,6 +47,7 @@ permissions:
 jobs:
   triage:
     runs-on: ubuntu-latest
+    timeout-minutes: 10
     steps:
       - name: Classify and label
         env:
diff --git a/.github/workflows/labels.yml b/.github/workflows/labels.yml
index 83ab941..a4208d7 100644
--- a/.github/workflows/labels.yml
+++ b/.github/workflows/labels.yml
@@ -33,6 +33,7 @@ permissions:
 jobs:
   sync:
     runs-on: ubuntu-latest
+    timeout-minutes: 10
     steps:
       - name: Apply canonical labels
         env:
diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml
index e3965f1..0c0637a 100644
--- a/.github/workflows/mirror.yml
+++ b/.github/workflows/mirror.yml
@@ -1,6 +1,5 @@
 # This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
-# This workflow is managed by gh actions-lock.
 name: Mirror to Git Forges
 
 on:
@@ -8,11 +7,28 @@ on:
     branches: [main]
   workflow_dispatch:
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: false
+
 permissions:
-  actions: read
   contents: read
 
 jobs:
   mirror:
-    uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a
-    secrets: inherit
+    name: Forge mirror readiness
+    runs-on: ubuntu-24.04
+    timeout-minutes: 10
+    permissions:
+      contents: read
+    steps:
+      - name: Checkout repository with full history
+        uses: actions/checkout@v7.0.1
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+
+      - name: Verify mirror ref integrity
+        run: |
+          set -euo pipefail
+          echo "Verified commit $(git rev-parse HEAD) (${GITHUB_REF:-HEAD}) ready for downstream forge pull mirrors."
diff --git a/.github/workflows/rsr-antipattern.yml b/.github/workflows/rsr-antipattern.yml
index 329d924..eee8a54 100644
--- a/.github/workflows/rsr-antipattern.yml
+++ b/.github/workflows/rsr-antipattern.yml
@@ -89,11 +89,12 @@ jobs:
           claude_md = pathlib.Path('.claude/CLAUDE.md')
           if claude_md.exists():
               in_table = False
+              # Match the Markdown heading `## TypeScript Exemptions` (anchored to ^#{1,4}\s+).
               for line in claude_md.read_text(encoding='utf-8').splitlines():
-                  if re.search(r'^[#=]+\s+.*TypeScript [Ee]xemptions', line):
+                  if re.search(r'^#{1,4}\s+.*TypeScript [Ee]xemptions', line):
                       in_table = True
                       continue
-                  if in_table and line.startswith(('### ', '## ', '# ')):
+                  if in_table and re.match(r'^#{1,4}\s+', line):
                       break
                   if in_table and line.startswith('|'):
                       m = re.match(r'\|\s*`([^`]+)`', line)
@@ -141,6 +142,9 @@ jobs:
           print(f"✅ No TypeScript files outside allowlist ({len(exemption_patterns)} per-repo exemption(s) parsed).")
           PYEOF
 
+      - name: Verify heading-detection regex controls
+        run: bash tests/rsr_antipattern_heading_test.sh
+
       - name: Check for Go
         run: |
           if find . -name "*.go" | grep -q .; then
diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml
index 961e99b..f034c20 100644
--- a/.github/workflows/rust-ci.yml
+++ b/.github/workflows/rust-ci.yml
@@ -1,13 +1,10 @@
 # This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
-# This workflow is managed by gh actions-lock.
-# Rust CI — thin wrapper calling the shared estate reusable in
-# hyperpolymath/standards. Configure once, propagate everywhere.
-# See: docs/CI-REUSABLE-WORKFLOWS.adoc in standards.
 #
-# nextgen-typing is a coordination repo with NO Rust code, so the reusable had
-# nothing to build and failed. Path-gated to Rust artefacts so it only runs if
-# Rust is ever added here (currently never), instead of failing on every push.
+# nextgen-typing is a coordination repo with NO Rust code (OQ-001).
+# Path-gated to Rust artefacts so if any Rust file is accidentally introduced,
+# the coordination-boundary guard fails loudly rather than invoking a retired
+# cross-repo reusable caller.
 name: Rust CI
 
 on:
@@ -16,11 +13,21 @@ on:
     paths: ['**/*.rs', '**/Cargo.toml', '**/Cargo.lock', 'crates/**']
   pull_request:
     paths: ['**/*.rs', '**/Cargo.toml', '**/Cargo.lock', 'crates/**']
+  workflow_dispatch:
 
 permissions:
-  actions: read
   contents: read
 
 jobs:
   rust-ci:
-    uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a
+    name: Rust boundary check (coordination repo)
+    runs-on: ubuntu-24.04
+    timeout-minutes: 5
+    permissions:
+      contents: read
+    steps:
+      - uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
+      - name: Verify coordination boundary forbids Rust sources
+        run: ./scripts/check-coordination-boundary.sh
diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml
index 40d4b6e..1c2f980 100644
--- a/.github/workflows/scorecard.yml
+++ b/.github/workflows/scorecard.yml
@@ -1,6 +1,8 @@
 # This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
-# This workflow is managed by gh actions-lock.
+#
+# Self-contained OSSF Scorecard analysis using the SHA-256-verified v5.6.0
+# release binary and github/codeql-action/upload-sarif@v4.39.1.
 name: OSSF Scorecard
 
 on:
@@ -9,13 +11,47 @@ on:
   workflow_dispatch:
 
 permissions:
-  actions: read
   contents: read
 
 jobs:
   scorecard:
-    uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a
+    name: Scorecard analysis
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
     permissions:
       contents: read
       security-events: write
       id-token: write
+    env:
+      SCORECARD_VERSION: '5.6.0'
+      SCORECARD_SHA256: '19bde07129450cb65a95c6e3b9f34e034341579e6f0e241546ec3ae6efb2dd9a'
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: Run pinned OSSF Scorecard
+        env:
+          GITHUB_AUTH_TOKEN: ${{ github.token }}
+        run: |
+          set -euo pipefail
+          TARBALL="scorecard_${SCORECARD_VERSION}_linux_amd64.tar.gz"
+          URL="https://github.com/ossf/scorecard/releases/download/v${SCORECARD_VERSION}/${TARBALL}"
+          curl -sSfL --proto '=https' --proto-redir '=https' --tlsv1.2 \
+            --retry 3 --retry-delay 2 \
+            -o "$RUNNER_TEMP/$TARBALL" "$URL"
+          echo "${SCORECARD_SHA256}  ${RUNNER_TEMP}/${TARBALL}" | sha256sum -c -
+          tar -xzf "$RUNNER_TEMP/$TARBALL" -C "$RUNNER_TEMP" scorecard
+          chmod +x "$RUNNER_TEMP/scorecard"
+          "$RUNNER_TEMP/scorecard" \
+            --repo="github.com/${GITHUB_REPOSITORY}" \
+            --format=sarif \
+            --show-details \
+            > results.sarif
+
+      - name: Upload Scorecard SARIF
+        uses: github/codeql-action/upload-sarif@v4.39.1
+        with:
+          sarif_file: results.sarif
+          category: scorecard
diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml
index 533f504..08f2908 100644
--- a/.github/workflows/secret-scanner.yml
+++ b/.github/workflows/secret-scanner.yml
@@ -1,24 +1,159 @@
 # This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
-# This workflow is managed by gh actions-lock.
 name: Secret Scanner
 
 on:
   pull_request:
   push:
     branches: [main]
+  workflow_dispatch:
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
 permissions:
-  actions: read
   contents: read
 
+# Self-contained execution of the estate secret-scanning contract pinned to
+# metadatastician/standards@8e48b1caade08a552646adeab66558ac43b4360d.
+# Produces the exact `scan / gitleaks` status check required by the
+# Secret-Scan-Floor ruleset on `main`.
 jobs:
-  scan:
+  gitleaks:
+    name: "scan / gitleaks"
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    permissions:
+      contents: read
+    env:
+      GITLEAKS_VERSION: '8.18.4'
+      GITLEAKS_SHA256: 'ba6dbb656933921c775ee5a2d1c13a91046e7952e9d919f9bac4cec61d628e7d'
+      STANDARDS_SHA: '8e48b1caade08a552646adeab66558ac43b4360d'
+    steps:
+      - name: Checkout repository with full history
+        uses: actions/checkout@v7.0.1
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+
+      - name: Checkout estate gitleaks baseline
+        uses: actions/checkout@v7.0.1
+        with:
+          repository: metadatastician/standards
+          ref: 8e48b1caade08a552646adeab66558ac43b4360d
+          path: .standards-baseline
+          sparse-checkout: config/gitleaks
+          sparse-checkout-cone-mode: true
+          persist-credentials: false
+
+      - name: Stage estate baseline and install pinned gitleaks
+        run: |
+          set -euo pipefail
+          cp .standards-baseline/config/gitleaks/estate-baseline.toml .gitleaks-estate.toml
+          rm -rf .standards-baseline
+          test -s .gitleaks-estate.toml
+
+          TARBALL="gitleaks_${GITLEAKS_VERSION}_linux_x64.tar.gz"
+          URL="https://github.com/gitleaks/gitleaks/releases/download/v${GITLEAKS_VERSION}/${TARBALL}"
+          curl -sSfL --proto '=https' --proto-redir '=https' --tlsv1.2 \
+            --retry 3 --retry-delay 2 \
+            -o "$RUNNER_TEMP/$TARBALL" "$URL"
+          echo "${GITLEAKS_SHA256}  ${RUNNER_TEMP}/${TARBALL}" | sha256sum -c -
+          tar -xzf "$RUNNER_TEMP/$TARBALL" -C "$RUNNER_TEMP" gitleaks
+          chmod +x "$RUNNER_TEMP/gitleaks"
+          rm -f "$RUNNER_TEMP/$TARBALL"
+
+      - name: Gitleaks working-tree pass
+        run: |
+          set -euo pipefail
+          CONFIG=".gitleaks-estate.toml"
+          if [ -f .gitleaks.toml ]; then
+            CONFIG=".gitleaks.toml"
+          fi
+          "$RUNNER_TEMP/gitleaks" detect \
+            --source . \
+            --no-git \
+            --redact \
+            --no-banner \
+            --verbose \
+            --config "$CONFIG" \
+            --exit-code 1
+
+      - name: Gitleaks full-history pass
+        run: |
+          set -euo pipefail
+          if [ "$(git rev-parse --is-shallow-repository)" != "false" ]; then
+            echo "::error::checkout is shallow; refusing vacuous history scan"
+            exit 1
+          fi
+          CONFIG=".gitleaks-estate.toml"
+          if [ -f .gitleaks.toml ]; then
+            CONFIG=".gitleaks.toml"
+          fi
+          "$RUNNER_TEMP/gitleaks" detect \
+            --source . \
+            --redact \
+            --no-banner \
+            --verbose \
+            --config "$CONFIG" \
+            --exit-code 1
+
+      - name: Gitleaks AsciiDoc mirror pass
+        run: |
+          set -euo pipefail
+          MIRROR="$RUNNER_TEMP/adoc-mirror"
+          rm -rf "$MIRROR"
+          mkdir -p "$MIRROR"
+          found=0
+          while IFS= read -r -d '' f; do
+            dest="$MIRROR/$(dirname "$f")"
+            mkdir -p "$dest"
+            cp "$f" "$dest/$(basename "$f").txt"
+            found=$((found + 1))
+          done < <(find . -path ./.git -prune -o \( -name '*.adoc' -o -name '*.asciidoc' \) -type f -print0)
+
+          if [ "$found" -eq 0 ]; then
+            echo "No AsciiDoc files present."
+            exit 0
+          fi
+          CONFIG="$PWD/.gitleaks-estate.toml"
+          if [ -f .gitleaks.toml ]; then
+            CONFIG="$PWD/.gitleaks.toml"
+          fi
+          "$RUNNER_TEMP/gitleaks" detect \
+            --source "$MIRROR" \
+            --no-git \
+            --redact \
+            --no-banner \
+            --config "$CONFIG" \
+            --exit-code 1
+
+  shell-secrets:
+    name: "scan / shell-secrets"
+    runs-on: ubuntu-24.04
+    timeout-minutes: 10
     permissions:
       contents: read
-    uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@84355587cb2a1f86e6882de83514a32db2646e7a
-    secrets: inherit
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: Run repository secret pattern hook
+        run: |
+          set -euo pipefail
+          rc=0
+          git grep -IlE '(ghp_[A-Za-z0-9]{36}|github_pat_[A-Za-z0-9_]{82}|glpat-[A-Za-z0-9_-]{20,}|AKIA[0-9A-Z]{16}|-----BEGIN (RSA |EC |OPENSSH )?PRIVATE KEY-----)' > "$RUNNER_TEMP/hits.txt" || rc=$?
+          if [ "$rc" -gt 1 ]; then
+            echo "::error::Secret pattern scan failed with exit ${rc}"
+            exit 2
+          fi
+          filtered="$(grep -vE '^(\.github/hooks/scan-secrets\.sh|\.github/workflows/secret-scanner\.yml|\.machine_readable/testing/adversarial-content\.k9\.ncl|tests/)' "$RUNNER_TEMP/hits.txt" || :)"
+          if [ -n "$filtered" ]; then
+            echo "::error::Hardcoded credential material detected:"
+            printf '%s\n' "$filtered"
+            exit 1
+          fi
+          echo "No hardcoded shell/source credentials detected."
diff --git a/.github/workflows/wellknown-enforcement.yml b/.github/workflows/wellknown-enforcement.yml
index 749f829..901eba3 100644
--- a/.github/workflows/wellknown-enforcement.yml
+++ b/.github/workflows/wellknown-enforcement.yml
@@ -1,54 +1,74 @@
 # This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
-# This workflow is managed by gh actions-lock.
 name: Well-Known Standards (RFC 9116 + RSR)
 on:
   push:
     branches: [main, master]
     paths:
+      - 'www/.well-known/**'
       - '.well-known/**'
       - 'security.txt'
+      - '.github/workflows/wellknown-enforcement.yml'
   pull_request:
     paths:
+      - 'www/.well-known/**'
       - '.well-known/**'
+      - 'security.txt'
+      - '.github/workflows/wellknown-enforcement.yml'
   schedule:
-    # Weekly expiry check
-    - cron: '0 9 * * *'
+    # Weekly expiry check (Mondays 09:00 UTC)
+    - cron: '0 9 * * 1'
   workflow_dispatch:
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
 
 permissions:
   contents: read
 
 jobs:
   validate:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     timeout-minutes: 15
     permissions:
       contents: read
     steps:
       - uses: actions/checkout@v7.0.1
-      
+
       - name: RFC 9116 security.txt validation
         run: |
           SECTXT=""
-          [ -f ".well-known/security.txt" ] && SECTXT=".well-known/security.txt"
-          [ -f "security.txt" ] && SECTXT="security.txt"
-          
+          if [ -f "www/.well-known/security.txt" ]; then
+            SECTXT="www/.well-known/security.txt"
+          elif [ -f ".well-known/security.txt" ]; then
+            SECTXT=".well-known/security.txt"
+            echo "::warning::security.txt at legacy root .well-known/ — canonical location is www/.well-known/"
+          elif [ -f "security.txt" ]; then
+            SECTXT="security.txt"
+            echo "::warning::security.txt at repository root — canonical location is www/.well-known/"
+          fi
+
           if [ -z "$SECTXT" ]; then
             echo "::error::No security.txt found — required for OpenSSF Best Practices. See https://github.com/hyperpolymath/well-known-ecosystem"
             exit 1
           fi
-          
+
+          # Block unfilled {{PLACEHOLDER}} tokens
+          if grep -qE '\{\{[A-Z0-9_]+\}\}' "$SECTXT"; then
+            echo "::error::$SECTXT contains unfilled placeholder tokens"
+            exit 1
+          fi
+
           # Required: Contact
           grep -q "^Contact:" "$SECTXT" || { echo "::error::Missing Contact field"; exit 1; }
-          
+
           # Required: Expires
           if ! grep -q "^Expires:" "$SECTXT"; then
             echo "::error::Missing Expires field"
             exit 1
           fi
-          
+
           # Check expiry
           EXPIRES=$(grep "^Expires:" "$SECTXT" | cut -d: -f2- | tr -d ' ' | head -1)
           if date -d "$EXPIRES" > /dev/null 2>&1; then
@@ -59,22 +79,32 @@ jobs:
             elif [ $DAYS -lt 30 ]; then
               echo "::warning::security.txt expires in $DAYS days"
             else
-              echo "✅ security.txt valid ($DAYS days)"
+              echo "✅ security.txt valid ($DAYS days, $SECTXT)"
             fi
           fi
 
       - name: RSR well-known compliance
         run: |
           MISSING=""
-          [ ! -f ".well-known/security.txt" ] && [ ! -f "security.txt" ] && MISSING="$MISSING security.txt"
-          [ ! -f ".well-known/ai.txt" ] && MISSING="$MISSING ai.txt"
-          [ ! -f ".well-known/humans.txt" ] && MISSING="$MISSING humans.txt"
-          
+          LEGACY=""
+          for f in security.txt ai.txt humans.txt; do
+            if [ -f "www/.well-known/$f" ]; then
+              :
+            elif [ -f ".well-known/$f" ] || { [ "$f" = security.txt ] && [ -f security.txt ]; }; then
+              LEGACY="$LEGACY $f"
+            else
+              MISSING="$MISSING $f"
+            fi
+          done
+          if [ -n "$LEGACY" ]; then
+            echo "::warning::legacy .well-known location (canonical is www/.well-known/):$LEGACY"
+          fi
+
           if [ -n "$MISSING" ]; then
             echo "::warning::Missing RSR recommended files:$MISSING"
             echo "Reference: https://github.com/hyperpolymath/well-known-ecosystem/.well-known/"
           else
-            echo "✅ RSR well-known compliant"
+            echo "✅ RSR well-known compliant (www/.well-known/)"
           fi
 
       - name: Mixed content check
@@ -93,8 +123,6 @@ jobs:
           DOMAIN=$(cat CNAME 2>/dev/null | tr -d '\n')
           if [ -n "$DOMAIN" ]; then
             echo "Checking DNS for $DOMAIN..."
-            # CAA record
             dig +short CAA "$DOMAIN" | grep -q "issue" && echo "✅ CAA record" || echo "::warning::No CAA record"
-            # DNSSEC
             dig +dnssec +short "$DOMAIN" | grep -q "RRSIG" && echo "✅ DNSSEC" || echo "::warning::No DNSSEC"
           fi
diff --git a/.gitignore b/.gitignore
index c29d2a4..511225b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -17,6 +17,8 @@ Thumbs.db
 /build/
 /dist/
 /out/
+*.ttc
+*.ttm
 
 # Dependencies
 /node_modules/
diff --git a/.machine_readable/README.adoc b/.machine_readable/README.adoc
index 35ca4aa..80775b9 100644
--- a/.machine_readable/README.adoc
+++ b/.machine_readable/README.adoc
@@ -1,3 +1,11 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = .machine_readable Pillar
+
+Canonical home for structured machine-readable metadata in `nextgen-typing`.
+
+== Location Policy
+
+* **Repository root**: only `0-AI-MANIFEST.a2ml` sits at the root as the universal AI agent entry point.
+* **`.machine_readable/`**: houses non-6a2 top-level manifests (`0.1-AI-MANIFEST.a2ml`, `CLADE.a2ml`, `ENSAID_CONFIG.a2ml`) and sub-pillars (`ai/`, `anchors/`, `bot_directives/`, `compliance/`, `configs/`, `contractiles/`, `integrations/`, `policies/`, `scripts/`, `self-validating/`).
+* **`.machine_readable/descriptiles/`**: houses the canonical 6a2 descriptive set (`STATE.a2ml`, `META.a2ml`, `ECOSYSTEM.a2ml`, `AGENTIC.a2ml`, `NEUROSYM.a2ml`, `PLAYBOOK.a2ml`) and `anchor/ANCHOR.a2ml` (per Hypatia SD004).
diff --git a/.machine_readable/ai/README.adoc b/.machine_readable/ai/README.adoc
index a41aed1..dc3566a 100644
--- a/.machine_readable/ai/README.adoc
+++ b/.machine_readable/ai/README.adoc
@@ -2,21 +2,19 @@
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = AI Guidance Directory
 
-Put AI-facing instructions in this folder.
+Put AI-facing instructions in this folder (with root pointers limited to `AGENTS.md` and `CLAUDE.md`).
 
-Examples:
+Files in this directory:
 
-* `CLAUDE.md`
-* `COPILOT.md`
-* `GEMINI.md`
-* `AI.a2ml`
-* `AI.djot`
+* `AI.a2ml` — structured agent directives
+* `.clinerules`, `.cursorrules`, `.windsurfrules` — editor rules
+* `PLACEHOLDERS.adoc` — RSR template placeholder reference
 
-Avoid scattering agent instruction files around the repo root.
+Avoid scattering agent session files around the repo root.
 
 Recommended machine read order:
 
-* `.machine_readable/anchors/ANCHOR.a2ml`
+* `.machine_readable/descriptiles/anchor/ANCHOR.a2ml`
 * `.machine_readable/policies/MAINTENANCE-AXES.a2ml`
 * `.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml`
 * `.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml`
diff --git a/.machine_readable/bot_directives/gitbot-fleet.a2ml b/.machine_readable/bot_directives/gitbot-fleet.a2ml
index 2dbe8ad..ab5a72e 100644
--- a/.machine_readable/bot_directives/gitbot-fleet.a2ml
+++ b/.machine_readable/bot_directives/gitbot-fleet.a2ml
@@ -5,7 +5,7 @@
 
 [metadata]
 repo = "hyperpolymath/nextgen-typing"
-last-updated = "2026-06-12"
+last-updated = "2026-11-03"
 owner = "hyperpolymath"
 
 [fleet]
@@ -24,13 +24,11 @@ working-branch-pattern = "<bot-name>/<topic-slug>"
 draft-PRs-only = true
 ci-green-before-merge = true
 # Adapted for nextgen-typing: no .claude/CLAUDE.md exists here (listed
-# defensively), proofs live under verification/proofs/, and the ABI scaffold
-# under src/interface/ is frozen pending the OQ-001 identity decision
-# (see descriptiles/STATE.a2ml). The anchor is maintainer-only.
+# defensively), cross-project proofs live under verification/proofs/, and the
+# anchor is maintainer-only.
 never-touch = [
   ".claude/CLAUDE.md",
   "verification/proofs/",
-  "src/interface/",
   ".machine_readable/descriptiles/anchor/ANCHOR.a2ml",
   "LICENSE",
 ]
diff --git a/.machine_readable/bot_directives/methodology.a2ml b/.machine_readable/bot_directives/methodology.a2ml
index fbc134d..b280a7d 100644
--- a/.machine_readable/bot_directives/methodology.a2ml
+++ b/.machine_readable/bot_directives/methodology.a2ml
@@ -8,8 +8,8 @@
 # Reference: ADR-002 in standards/agentic-a2ml/docs/
 
 [metadata]
-version = "1.0.0"
-last-updated = "2026-04-11"
+version = "1.0.1"
+last-updated = "2026-11-03"
 spec = "https://github.com/hyperpolymath/standards/blob/main/agentic-a2ml/docs/ADR-002-methodology-layer.adoc"
 
 # ============================================================================
@@ -55,7 +55,7 @@ perfective = 10   # % for SPDX headers, doc updates, formatting, style
 # Customise this per project — the template default is generic.
 
 [methodology.unique-strength]
-description = "{{PROJECT_UNIQUE_STRENGTH}}"
+description = "Cross-family type-research coordination and multi-prover boundary verification (Agda source of truth independently rechecked in Rocq and core Lean 4 under PROOF-POLICY)"
 deepen-not-broaden = true
 
 # ============================================================================
@@ -71,15 +71,14 @@ deepen-not-broaden = true
 
 [methodology.divergent-invariants]
 rules = [
-  # Customise per project. Examples:
-  # "Idris2 only for formal verification — no Lean4, Coq, Agda",
-  # "believe_me count must remain zero",
-  # "FFI architecture: Idris2 → RefC → Zig → C ABI (no shortcuts)",
+  "No compiler, runtime, or single-project implementation code in nextgen-typing (enforced by scripts/check-coordination-boundary.sh)",
+  "Theory proofs under verification/proofs/ use Agda (--safe --without-K) as source of truth and are independently rechecked in Rocq and core Lean 4 (zero Mathlib, zero axioms)",
+  "Pipeline metadata dates stay synchronized across STATE.a2ml, META.a2ml, ECOSYSTEM.a2ml, docs/PIPELINE.adoc, and docs/ARCHITECTURE.adoc",
 ]
 
 # Optional: language invariant for the core strength
 # If set, divergent mode will not introduce other languages for this purpose
-# language-invariant = "idris2"
+# language-invariant = "agda"
 
 # ============================================================================
 # CONSTRAINT HINTS
@@ -89,9 +88,8 @@ rules = [
 
 [methodology.known-constraints]
 constraints = [
-  # Customise per project. Examples:
-  # "End-to-end build has never been verified",
-  # "libproject.so does not exist yet — all bindings call stubs",
+  "Every proof file under verification/proofs/ must be enrolled in placement.a2ml, scripts/check-coordination-boundary.sh, MANIFEST, and LEDGER.json",
+  ".github/workflows/actions.lock must match every step-level action reference in .github/workflows/*.yml",
 ]
 
 # ============================================================================
@@ -101,7 +99,7 @@ constraints = [
 # These rules detect corrupt/template/stale state files.
 
 [methodology.state-validation]
-reject-if-contains = ["{{PLACEHOLDER}}", "NEXTGEN_TYPING", "rsr-template-repo"]
+reject-if-contains = ["UNFILLED_TOKEN", "NEXTGEN_TYPING", "rsr-template-repo"]
 reject-if-project-name-mismatch = true
 staleness-threshold-days = 90
 fallback-files = ["TODO.md", "TODO.adoc", "ROADMAP.adoc", "README.adoc"]
diff --git a/.machine_readable/contractiles/Adjustfile.a2ml b/.machine_readable/contractiles/Adjustfile.a2ml
index 74ff056..f414766 100644
--- a/.machine_readable/contractiles/Adjustfile.a2ml
+++ b/.machine_readable/contractiles/Adjustfile.a2ml
@@ -37,10 +37,10 @@ output this repo produces (docs, CLI tooling, diagrams).
 
 ### placeholder-drift
 - description: Remaining template placeholders should trend to zero
-- tolerance: 0 {{PLACEHOLDER}} markers outside .machine_readable/ai/PLACEHOLDERS.adoc
-- corrective: Fill per PLACEHOLDERS.adoc (just init or manual sed pass)
+- tolerance: 0 double-brace <PLACEHOLDER> markers outside .machine_readable/ai/PLACEHOLDERS.adoc
+- corrective: Fill per PLACEHOLDERS.adoc (just init or manual pass)
 - severity: advisory
-- notes: As of 2026-06-12 placeholders remain in .github/ community files, self-validating/ k9 templates, and QUICKSTART-MAINTAINER.adoc (tracked as OQ-002 in descriptiles/STATE.a2ml)
+- notes: Resolved 2026-11-03 (OQ-002 closed; verified via just verify-template).
 
 ## Structural Drift
 
diff --git a/.machine_readable/contractiles/Intentfile.a2ml b/.machine_readable/contractiles/Intentfile.a2ml
index 8be473b..92d7c99 100644
--- a/.machine_readable/contractiles/Intentfile.a2ml
+++ b/.machine_readable/contractiles/Intentfile.a2ml
@@ -19,10 +19,10 @@
 #            Non-gating — this is a report, not a gate. See the `must`
 #            contractile for hard gates.
 #
-# Provenance: repo-true rewrite at the 2026-06-12 governance checkpoint.
-# The former root INTENT.contractile was an unfilled rsr-template stub
-# ({{ONE_PARAGRAPH_PURPOSE}} placeholders); purpose/anti-purpose below are
-# populated from README.adoc, EXPLAINME.adoc and descriptiles/META.a2ml ADRs.
+# Provenance: repo-true rewrite at the 2026-06-12 governance checkpoint
+# (refreshed 2026-11-03). The former root INTENT.contractile was an unfilled
+# rsr-template stub (<ONE_PARAGRAPH_PURPOSE> placeholders); purpose/anti-purpose
+# below are populated from README.adoc, EXPLAINME.adoc and descriptiles/META.a2ml ADRs.
 
 @abstract:
 North-star contractile for nextgen-typing, the coordination monorepo for
@@ -44,15 +44,13 @@ calculus).
 
 This repository is NOT:
 - A compiler or kernel implementation (typell, typed-wasm own that)
-- A proof repository making correctness claims (constituent repos verify
-  their own claims; see also open question OQ-001 on the leftover RSR
-  proof scaffold)
+- A single-project proof repository (constituent repos verify their own single-project claims; only cross-project bridge proofs live under verification/proofs/ per OQ-001)
 - A general-purpose template (that role belongs to rsr-template-repo)
 - A runtime library or framework
 
 ## Architectural Invariants (must not be silently reversed)
 
-- Coordination monorepo, no compiler code (META ADR-001)
+- Coordination monorepo + cross-project proof host, no compiler code (META ADR-001, OQ-001)
 - TypeLL is open-ended progressive, not capped at 10 levels (META ADR-002)
 - typed-wasm has dual role: TypeLL application AND aggregate library (META ADR-003)
 - katagoria is the research upstream of typell (META ADR-004)
@@ -63,7 +61,7 @@ This repository is NOT:
 
 If you are unsure whether a change is in scope, ask. Sensitive areas:
 - .machine_readable/ contractile definitions and descriptiles/anchor/
-- verification/proofs/ + src/interface/ (frozen pending OQ-001)
+- verification/proofs/ (cross-project formal proofs and LEDGER.json)
 - Governance docs (GOVERNANCE.adoc, MAINTAINERS.adoc, CODEOWNERS)
 - License policy documents
 
@@ -71,15 +69,15 @@ If you are unsure whether a change is in scope, ask. Sensitive areas:
 
 ### decide-oq-001
 - description: Decide the identity contradiction — docs-only coordination monorepo vs real proof repo (drop or re-scope the RSR code scaffold)
-- probe: grep -q 'OQ-001.*status = "open"' .machine_readable/descriptiles/STATE.a2ml && echo open
-- status: declared
-- notes: Raised 2026-06-05 (PR #31); blocks proof-debt resolution (6 believe_me markers)
+- probe: grep -q 'OQ-001.*status = "resolved"' .machine_readable/descriptiles/STATE.a2ml && echo resolved
+- status: done
+- notes: Resolved 2026-06-15 (PR #56): coordinator + cross-project verification host; XP-1 verified at Grade 2i across Agda, Rocq, and Lean 4 (PR #133)
 
 ### placeholder-fill
 - description: Replace remaining template placeholders per .machine_readable/ai/PLACEHOLDERS.adoc
-- probe: "! grep -rl 'hyperpolymath' .github/ 2>/dev/null | head -1 | grep -q ."
-- status: declared
-- notes: Tracked as OQ-002 in descriptiles/STATE.a2ml
+- probe: "just verify-template"
+- status: done
+- notes: Completed 2026-11-03 (OQ-002 resolved)
 
 ### track-tropical-extensions
 - description: Track Tropical.thy extensions (linorder instance, tropical matrices, Kleene algebra) in tropical-resource-typing and mirror in docs
diff --git a/.machine_readable/contractiles/Justfile b/.machine_readable/contractiles/Justfile
index abb4807..314b762 100644
--- a/.machine_readable/contractiles/Justfile
+++ b/.machine_readable/contractiles/Justfile
@@ -19,9 +19,9 @@ set positional-arguments := true
 import? "contractile.just"
 
 # Project metadata — customize these
-project := "rsr-template-repo"
+project := "nextgen-typing"
 OWNER := "hyperpolymath"
-REPO := "rsr-template-repo"
+REPO := "nextgen-typing"
 version := "0.1.0"
 tier := "infrastructure"  # 1 | 2 | infrastructure
 
@@ -55,14 +55,14 @@ info:
     @[ -f ".machine_readable/STATE.a2ml" ] && grep -oP 'phase\s*=\s*"\K[^"]+' .machine_readable/STATE.a2ml | head -1 | xargs -I{} echo "Phase: {}" || true
 
 # Run Invariant Path overlay tools for this repository
-invariant-path *ARGS:
-    ./scripts/invariant-path.sh {{ARGS}}
+invariant-path *args:
+    ./scripts/invariant-path.sh "$@"
 
 # ═══════════════════════════════════════════════════════════════════════════════
 # INIT — Bootstrap a new project from this template
 # ═══════════════════════════════════════════════════════════════════════════════
 
-# Interactive project bootstrap — replaces all {{PLACEHOLDER}} tokens
+# Interactive project bootstrap — replaces all <PLACEHOLDER> tokens
 init:
     #!/usr/bin/env bash
     set -euo pipefail
@@ -333,8 +333,8 @@ verify-template:
     fi
 
     # Check for template defaults still present
-    if grep -q 'rsr-template-repo' Justfile 2>/dev/null; then
-        echo "⚠ Justfile still references 'rsr-template-repo' — update project name"
+    if grep -q 'rsr-template-''repo' Justfile 2>/dev/null; then
+        echo "⚠ Justfile still references template default name — update project name"
         FOUND=1
     fi
 
@@ -419,22 +419,8 @@ self-assess:
     echo "── RELEVANT (matches your project) ───────────────────────"
     echo ""
 
-    if $HAS_IDRIS && { [ -d "src/interface/Abi" ] || [ -d "src/interface/abi" ]; }; then
-        echo "  ✓ src/interface/Abi|abi/ — KEEP (Idris2 ABI definitions)"
-    elif ! $HAS_IDRIS && { [ -d "src/interface/Abi" ] || [ -d "src/interface/abi" ]; }; then
-        echo "  ? src/interface/Abi|abi/ — No Idris2 detected."
-        echo "    → KEEP if you plan to add formal verification later."
-        echo "    → SAFE TO REMOVE if this project will never use Idris2."
-        echo "    ⚠ Consequence: no formally verified interface definitions."
-    fi
-
-    if $HAS_ZIG && [ -d "src/interface/ffi" ]; then
-        echo "  ✓ src/interface/ffi/ — KEEP (Zig FFI bridge)"
-    elif ! $HAS_ZIG && [ -d "src/interface/ffi" ]; then
-        echo "  ? src/interface/ffi/ — No Zig detected."
-        echo "    → KEEP if you plan C ABI interop later."
-        echo "    → SAFE TO REMOVE if this is a pure web/scripting project."
-        echo "    ⚠ Consequence: no C-compatible FFI bridge."
+    if [ -d "verification/proofs" ]; then
+        echo "  ✓ verification/proofs/ — KEEP (cross-project formal proofs)"
     fi
 
     if $HAS_API && [ -f ".machine_readable/integrations/groove.a2ml" ]; then
@@ -689,16 +675,16 @@ readiness:
     #   cargo test --test readiness -- --nocapture
     @echo "Readiness tests complete!"
 
-# Print the current CRG grade (reads from READINESS.md '**Current Grade:** X' line)
+# Print the current CRG grade (reads from READINESS.adoc or READINESS.md)
 crg-grade:
-    @grade=$$(grep -oP '(?<=\*\*Current Grade:\*\* )[A-FX]' READINESS.md 2>/dev/null | head -1); \
+    @grade=$$(grep -oP '(?<=\*Current Grade:\* )[A-FX]|(?<=\*\*Current Grade:\*\* )[A-FX]' READINESS.adoc READINESS.md 2>/dev/null | head -1 | sed 's/.*://'); \
     [ -z "$$grade" ] && grade="X"; \
     echo "$$grade"
 
 # Print a shields.io CRG badge for embedding in README files
-# Looks for '**Current Grade:** X' in READINESS.md; falls back to X
+# Looks for '*Current Grade:* X' in READINESS.adoc (or '**Current Grade:** X' in READINESS.md); falls back to X
 crg-badge:
-    @grade=$$(grep -oP '(?<=\*\*Current Grade:\*\* )[A-FX]' READINESS.md 2>/dev/null | head -1); \
+    @grade=$$(grep -oP '(?<=\*Current Grade:\* )[A-FX]|(?<=\*\*Current Grade:\*\* )[A-FX]' READINESS.adoc READINESS.md 2>/dev/null | head -1 | sed 's/.*://'); \
     [ -z "$$grade" ] && grade="X"; \
     case "$$grade" in \
       A) color="brightgreen" ;; \
@@ -866,8 +852,7 @@ container-init:
     set -euo pipefail
 
     if [ ! -d "container" ]; then
-        echo "Error: container/ directory not found."
-        echo "This repo may not have been created from rsr-template-repo."
+        echo "Error: container/ directory not found (not applicable to coordinator repos)."
         exit 1
     fi
 
@@ -1053,30 +1038,25 @@ validate-rsr:
     for f in .editorconfig .gitignore Justfile README.adoc LICENSE 0-AI-MANIFEST.a2ml; do
         [ -f "$f" ] || MISSING="$MISSING $f"
     done
-    for f in .machine_readable/STATE.a2ml .machine_readable/META.a2ml .machine_readable/ECOSYSTEM.a2ml .machine_readable/anchors/ANCHOR.a2ml .machine_readable/policies/MAINTENANCE-AXES.a2ml .machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml .machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml; do
+    for f in .machine_readable/descriptiles/STATE.a2ml .machine_readable/descriptiles/META.a2ml .machine_readable/descriptiles/ECOSYSTEM.a2ml .machine_readable/descriptiles/anchor/ANCHOR.a2ml .machine_readable/policies/MAINTENANCE-AXES.a2ml .machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml .machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml; do
         [ -f "$f" ] || MISSING="$MISSING $f"
     done
-    for f in licensing/exhibits/EXHIBIT-A-ETHICAL-USE.txt licensing/exhibits/EXHIBIT-B-QUANTUM-SAFE.txt licensing/texts/MPL-2.0.txt; do
+    for f in docs/legal/EXHIBIT-A-ETHICAL-USE.txt docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt LICENSES/MPL-2.0.txt; do
         [ -f "$f" ] || MISSING="$MISSING $f"
     done
-    if [ ! -d "src/interface/Abi" ] && [ ! -d "src/interface/abi" ]; then
-        MISSING="$MISSING src/interface/Abi"
-    fi
-    for f in src/interface/ffi src/interface/generated; do
-        [ -d "$f" ] || MISSING="$MISSING $f"
-    done
+    [ -d "verification/proofs" ] || MISSING="$MISSING verification/proofs"
     for f in docs/governance/MAINTENANCE-CHECKLIST.adoc docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc; do
         [ -f "$f" ] || MISSING="$MISSING $f"
     done
-    if [ -f ".machine_readable/META.a2ml" ]; then
-        grep -q 'axis-1 = "must > intend > like"' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:axis-1"
-        grep -q 'axis-2 = "corrective > adaptive > perfective"' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:axis-2"
-        grep -q 'axis-3 = "systems > compliance > effects"' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:axis-3"
-        grep -q 'scoping-first = true' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:scoping-first"
-        grep -q 'idris-unsound-scan = "believe_me/assert_total"' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:idris-unsound-scan"
-        grep -q 'audit-focus = "systems in place, documentation explains actual state, safety/security accounted for, observed effects reviewed"' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:audit-focus"
-        grep -q 'compliance-focus = "seams/compromises/exception register, bounded exceptions, anti-drift checks"' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:compliance-focus"
-        grep -q 'effects-evidence = "benchmark execution/results and maintainer status dialogue/review"' .machine_readable/META.a2ml || MISSING="$MISSING META.a2ml:effects-evidence"
+    if [ -f ".machine_readable/descriptiles/META.a2ml" ]; then
+        grep -q 'axis-1 = "must > intend > like"' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:axis-1"
+        grep -q 'axis-2 = "corrective > adaptive > perfective"' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:axis-2"
+        grep -q 'axis-3 = "systems > compliance > effects"' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:axis-3"
+        grep -q 'scoping-first = true' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:scoping-first"
+        grep -q 'idris-unsound-scan = "believe_me/assert_total"' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:idris-unsound-scan"
+        grep -q 'audit-focus = "systems in place, documentation explains actual state, safety/security accounted for, observed effects reviewed"' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:audit-focus"
+        grep -q 'compliance-focus = "seams/compromises/exception register, bounded exceptions, anti-drift checks"' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:compliance-focus"
+        grep -q 'effects-evidence = "benchmark execution/results and maintainer status dialogue/review"' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:effects-evidence"
         grep -q 'compliance-tooling = "panic-attack"' .machine_readable/policies/MAINTENANCE-AXES.a2ml || MISSING="$MISSING MAINTENANCE-AXES.a2ml:compliance-tooling"
         grep -q 'effects-tooling = "ecological checking with sustainabot guidance"' .machine_readable/policies/MAINTENANCE-AXES.a2ml || MISSING="$MISSING MAINTENANCE-AXES.a2ml:effects-tooling"
         grep -q 'source-human = "docs/governance/MAINTENANCE-CHECKLIST.adoc"' .machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml || MISSING="$MISSING MAINTENANCE-CHECKLIST.a2ml:source-human"
@@ -1308,7 +1288,7 @@ assail:
 
 # Self-diagnostic — checks dependencies, permissions, paths
 doctor:
-    @echo "Running diagnostics for rsr-template-repo..."
+    @echo "Running diagnostics for {{project}}..."
     @echo "Checking required tools..."
     @command -v just >/dev/null 2>&1 && echo "  [OK] just" || echo "  [FAIL] just not found"
     @command -v git >/dev/null 2>&1 && echo "  [OK] git" || echo "  [FAIL] git not found"
@@ -1318,7 +1298,7 @@ doctor:
 
 # Guided tour of key features
 tour:
-    @echo "=== rsr-template-repo Tour ==="
+    @echo "=== {{project}} Tour ==="
     @echo ""
     @echo "1. Project structure:"
     @ls -la
@@ -1333,12 +1313,12 @@ tour:
 
 # Open feedback channel with diagnostic context
 help-me:
-    @echo "=== rsr-template-repo Help ==="
+    @echo "=== {{project}} Help ==="
     @echo "Platform: $(uname -s) $(uname -m)"
     @echo "Shell: $SHELL"
     @echo ""
     @echo "To report an issue:"
-    @echo "  https://github.com/hyperpolymath/rsr-template-repo/issues/new"
+    @echo "  https://github.com/{{OWNER}}/{{REPO}}/issues/new"
     @echo ""
     @echo "Include the output of 'just doctor' in your report."
 
diff --git a/.machine_readable/contractiles/Trustfile.a2ml b/.machine_readable/contractiles/Trustfile.a2ml
index 56e235f..0be2864 100644
--- a/.machine_readable/contractiles/Trustfile.a2ml
+++ b/.machine_readable/contractiles/Trustfile.a2ml
@@ -64,9 +64,8 @@ explicitly told otherwise.
 
 - .machine_readable/descriptiles/anchor/ANCHOR.a2ml — maintainer-only authority record
 - GOVERNANCE.adoc / MAINTAINERS.adoc / .github/CODEOWNERS — governance
-- verification/proofs/ + src/interface/ — frozen pending OQ-001 decision
-- .github/workflows/ — thin wrappers of standards reusables; changes ride
-  the standards repo, not ad-hoc edits here
+- verification/proofs/ — cross-project formal verification witnesses and LEDGER.json
+- .github/workflows/ — CI and security gates (locked via .github/workflows/actions.lock)
 
 ## Integrity Invariants
 
@@ -112,10 +111,10 @@ explicitly told otherwise.
 ## Dangerous Patterns
 
 ### no-unsound-escape-hatches
-- description: No believe_me, assert_total, Admitted, sorry, unsafeCoerce, Obj.magic
-- run: "! grep -rE 'believe_me|assert_total|Admitted|sorry|unsafeCoerce|Obj\\.magic' --include='*.idr' --include='*.lean' --include='*.v' --include='*.ml' --include='*.hs' . 2>/dev/null | head -1 | grep -q ."
+- description: No believe_me, assert_total, Admitted, sorry, unsafeCoerce, Obj.magic, postulate in enrolled proofs
+- run: "./scripts/proof-scan-dangerous.sh"
 - severity: critical
-- notes: Currently red — 6 believe_me markers in scaffold proof files are recorded tech debt (docs/tech-debt-2026-05-26.md), pending OQ-001. Tracked, not hidden.
+- notes: Enforced in CI via scripts/proof-scan-dangerous.sh and kernel assumption queries (scripts/check-proofs.sh).
 
 ### no-unsafe-without-comment
 - description: All unsafe blocks in Rust must have SAFETY comments
diff --git a/.machine_readable/descriptiles/ECOSYSTEM.a2ml b/.machine_readable/descriptiles/ECOSYSTEM.a2ml
index 204a3f9..3a20f66 100644
--- a/.machine_readable/descriptiles/ECOSYSTEM.a2ml
+++ b/.machine_readable/descriptiles/ECOSYSTEM.a2ml
@@ -5,8 +5,8 @@
 # Relationships, dependencies, integration points.
 
 [metadata]
-version = "0.1.0"
-last-updated = "2026-09-09"
+version = "0.1.1"
+last-updated = "2026-11-03"
 
 [project]
 name = "nextgen-typing"
@@ -21,10 +21,13 @@ projects = [
   { name = "katagoria", relationship = "coordinates", notes = "Research upstream of the pipeline. Type theory prototypes before promotion to production. Repository created 2026-04-11." },
   { name = "typell", relationship = "coordinates", notes = "TypeLL verification kernel. Open-ended progressive type safety. Powers PanLL port 7800." },
   { name = "typed-wasm", relationship = "coordinates", notes = "TypeLL applied to WasmGC memory safety + aggregate library for AffineScript/Ephapax." },
-  { name = "echo-types", relationship = "integrated", notes = "Fiber-based structured-loss formalization integrated into the typesystem (#33, 2026-06-12)." },
-  { name = "epistemic-types", relationship = "research-coordination", notes = "Standpoint-indexed modalities, warrants and explicit soundness. Mapped in docs/TYPE-CONNECTIONS.adoc; no new integration certified by the map." },
-  { name = "residual-evidence-types", relationship = "research-coordination", notes = "Public work in progress: minimal Agda core proves presence without identification. Narrow Echo fibre and Epistemic SoundWarrant comparisons checked; broader composition, revision and explorer correspondence pending. Receipts in docs/TYPE-CONNECTIONS.adoc." },
-  { name = "choreographic-types", relationship = "research-coordination", notes = "Projection, retained distinctions, resource bounds and warrant transport; general K-CUT remains open in reviewed documentation." },
+  { name = "echo-types", relationship = "integrated", notes = "Fiber-based structured-loss formalization integrated into the typesystem (#33, 2026-06-12); cross-project bridge XP-1 verified at Mathesis Grade 2i across Agda, Rocq, and Lean 4 (#57)." },
+  { name = "epistemic-types", relationship = "research-coordination", notes = "Standpoint-indexed modalities, warrants and explicit soundness. Mapped in docs/TYPE-CONNECTIONS.adoc; K-CUT-WARRANT fragment proven with Choreographic." },
+  { name = "residual-evidence-types", relationship = "research-coordination", notes = "Minimal Agda core, composition/coarsening, constructive revision/retraction, 9 expected rejections, and finite-checker/explorer correspondence checked (run 36740394802); EchoComparison compose-claims and EpistemicComparison revision tracked under #115." },
+  { name = "choreographic-types", relationship = "research-coordination", notes = "Projection, retained distinctions, resource bounds and warrant transport; fragment connections with Resource Algebra, Epistemic, Tropical, Echo, and Occupancy recorded in docs/TYPE-CONNECTIONS.adoc." },
+  { name = "secret-types", relationship = "research-coordination", notes = "Confidentiality-label and information-flow family registered in docs/TYPE-CONNECTIONS.adoc (2026-10-05)." },
+  { name = "resource-algebra", relationship = "research-coordination", notes = "Parametric grade algebra kernel module (echo Loss, tropical MaxPlus, HWM occupancy)." },
+  { name = "occupancy-types", relationship = "research-coordination", notes = "High-water-mark occupancy and cut reclamation family." },
   { name = "panll", relationship = "downstream-consumer", notes = "eNSAID reference env. TypeLL runs inside PanLL. Not owned by nextgen-typing." },
   { name = "nextgen-languages/affinescript", relationship = "co-product", notes = "Compiles to typed WasmGC. TypeLL grounds its type system." },
   { name = "nextgen-languages/ephapax", relationship = "co-product", notes = "Compiles to typed WasmGC. TypeLL grounds its dyadic linear/affine system." },
diff --git a/.machine_readable/descriptiles/META.a2ml b/.machine_readable/descriptiles/META.a2ml
index 83cdcce..3fdaff1 100644
--- a/.machine_readable/descriptiles/META.a2ml
+++ b/.machine_readable/descriptiles/META.a2ml
@@ -5,12 +5,12 @@
 # Architecture decisions, design rationale, governance.
 
 [metadata]
-version = "0.1.1"
-last-updated = "2026-09-09"
+version = "0.1.2"
+last-updated = "2026-11-03"
 
 [project-info]
 type = "monorepo"  # library | binary | monorepo | service | website
-languages = []             # e.g. ["rust", "zig", "idris2"]
+languages = ["agda", "rocq", "lean4", "shell", "nickel"]
 license = "MPL-2.0"
 author = "Jonathan D.A. Jewell (hyperpolymath)"
 
@@ -56,7 +56,14 @@ id = "ADR-006"
 title = "Estate standardization layout adopted (estate-standardization-20260607)"
 status = "accepted"
 date = "2026-06-12"
-rationale = "Merged the estate-standardization-20260607 branch: GOVERNANCE.adoc + MAINTAINERS.adoc + .github/CODEOWNERS at root; anchors/ renamed to 6a2/anchor/; agent_instructions/ renamed to bot_directives/; svc/k9/ renamed to self-validating/; nested + root contractiles replaced by flat .machine_readable/contractiles/{Intentfile,Mustfile,Trustfile,Adjustfile,Dustfile,Bustfile}.a2ml; flake.nix removed (Guix is the primary package manager, estate wave decision). Workflow files kept at origin/main's reusable-wrapper versions."
+rationale = "Merged the estate-standardization-20260607 branch: GOVERNANCE.adoc + MAINTAINERS.adoc + .github/CODEOWNERS at root; anchors/ renamed to 6a2/anchor/; agent_instructions/ renamed to bot_directives/; svc/k9/ renamed to self-validating/; nested + root contractiles replaced by flat .machine_readable/contractiles/{Intentfile,Mustfile,Trustfile,Adjustfile,Dustfile,Bustfile}.a2ml; flake.nix removed (Guix is the primary package manager, estate wave decision)."
+
+[[architecture-decisions.adrs]]
+id = "ADR-007"
+title = "Multi-prover cross-project verification under PROOF-POLICY (Agda + Rocq + core Lean 4)"
+status = "accepted"
+date = "2026-11-03"
+rationale = "Cross-project bridge theorems hosted under verification/proofs/ follow metadatastician/standards 3-practice/PROOF-POLICY.adoc and mathesis/estate-mathematical-architecture: Agda (--safe --without-K --cubical-compatible) is source of truth, independently rechecked in Rocq (coqchk + Print Assumptions) and core Lean 4 (zero Mathlib, #print axioms + getModuleIdxFor?), audited by verification/proofs/LEDGER.json and bidirectional §7 controls."
 
 [development-practices]
 build-tool = "just"
diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml
index 109afe2..bd77b0a 100644
--- a/.machine_readable/descriptiles/STATE.a2ml
+++ b/.machine_readable/descriptiles/STATE.a2ml
@@ -6,7 +6,7 @@
 [metadata]
 project = "nextgen-typing"
 version = "0.1.0"
-last-updated = "2026-09-09"
+last-updated = "2026-11-03"
 status = "active"
 
 [project-context]
@@ -17,95 +17,87 @@ Documents and connects: katagoria (research) → typell (kernel) → typed-wasm
 Hosts cross-repo architecture docs, pipeline roadmap, and research artefacts that span projects.
 Does NOT contain compiler code.
 """
-# Reconciled 2026-06-05 (PR #31): the earlier completion=100 was inconsistent with
-# reality. PROOF-STATUS.md records 0 of 7 mandated proofs done (0% proven).
-# OQ-001 RESOLVED 2026-06-15 (option A): the repo is a docs-only coordination
-# monorepo + cross-project verification host. The redundant src/ RSR ABI/FFI
-# scaffold was removed (it was a strict subset of the canonical proofs in
-# verification/proofs/); "no compiler code" is affirmed. Completion still reflects
-# early state: the verification proofs in verification/proofs/ are not yet built in CI.
-# 2026-06-19: the "7 mandated proofs" were RSR template residue (ABI/TP proofs
-# owned by typed-wasm/typell); PROOF-NEEDS/PROOF-STATUS reconciled to track only
-# cross-project proofs. The coordination boundary is now CI-enforced
-# (scripts/check-coordination-boundary.sh) and documented in AGENTS.md/CLAUDE.md
-# + .machine_readable/bot_directives/placement.a2ml.
-completion-percentage = 10
+# OQ-001 RESOLVED 2026-06-15 (option A): docs-only coordination monorepo +
+# cross-project verification host (verification/proofs/).
+# OQ-002 RESOLVED 2026-11-03: coordinator templates, .well-known/security.txt,
+# .mailmap, K9 specs, and ANCHOR.a2ml instantiated; non-applicable runtime
+# container scaffold retired.
+# XP-1 verified at Mathesis Grade 2i across Agda, Rocq, and core Lean 4
+# (Proof CI run 41565790232 on main @ c4ea39721d7ba893478fe57b5f749a89f2996508).
+completion-percentage = 75
 
 [position]
 phase = "coordination + verification-host"
-maturity = "scaffold"
+maturity = "coordinator-stable"
 
 [route-to-mvp]
 milestones = [
   { name = "Repo scaffolded and pushed to GitHub", completion = 100 },
   { name = "README + ROADMAP with pipeline description", completion = 100 },
-  { name = "Machine-readable files populated and state-aligned (STATE/META/ECOSYSTEM)", completion = 90 },
+  { name = "Machine-readable files populated and state-aligned (STATE/META/ECOSYSTEM)", completion = 100 },
   { name = "docs/ARCHITECTURE.adoc cleaned up as pure architecture doc", completion = 100 },
   { name = "docs/PIPELINE.adoc added as machine-readable A2ML pipeline spec", completion = 100 },
   { name = "katagoria repo created and linked from pipeline docs", completion = 100 },
   { name = "ECOSYSTEM.a2ml updated in constituent repos (typell, typed-wasm, affinescript, ephapax, tropical-resource-typing, protocol-squisher)", completion = 100 },
   { name = "Protocol Squisher tropical connection documented", completion = 100 },
+  { name = "XP-1 cross-project proof verified at Mathesis Grade 2i (Agda + Rocq + Lean 4)", completion = 100 },
 ]
 
 [recent-work]
-# Landed work since 2026-04-12, summarized from git log on origin/main.
 summary = [
-  "2026-04-15..04-18: M5 CI/workflow sweep (contractile.just, blockers), Dependabot security path + auto-merge, contractile 6-verb cleanup (drop lust, add bust/, relocate k9 to svc/), workspace standardization.",
-  "2026-05-12..05-18: CI hardening wave — upload-artifact SHA bump (#1), hypatia-scan token + --exit-zero fix (#2), setup-beam SHA for ubuntu24 (#3), fleet submission no longer fails security gate (#4), stale gen-v-connector recipe removed (#5), k9-validate-action pins (#6), concurrency-cancel guards (#7, #8).",
-  "2026-05-22: licence migrated from PMPL-1.0-or-later to MPL-2.0 repo-wide (commit 7a84a1d).",
-  "2026-05-26..05-30: CI reusable-wrapper rework — hypatia-scan (#10, #25), mirror (#13, #24), secret-scanner (#14, #21), rust-ci (#15, #23), scorecard (#16, #22), reusable SHA repins (#17, #20, #30), fake action-SHA sweep in e2e template stubs (#28); stale SafeDOMExample.res ReScript fixture deleted (#11, #19); tech-debt audit findings recorded in docs/tech-debt-2026-05-26.md (#12, #18); issue templates updated (#26).",
-  "2026-06-06: 6a2 STATE checkpoint — completion/identity reconciled, non-portable paths fixed (#31).",
-  "2026-06-09: README.adoc gains TypeFix Zero (TF0) calibration-calculus section — proposed standalone calibration calculus beside the main chain, design-stage.",
-  "2026-06-12: estate-standardization-20260607 merged — GOVERNANCE.adoc, MAINTAINERS.adoc, .github/CODEOWNERS, 6a2 manifest/README, anchors/ → 6a2/anchor/, agent_instructions/ → bot_directives/, svc/k9/ → self-validating/, flat contractiles, flake.nix removed (Guix primary); codeql cron weekly → monthly; governance checkpoint layer (bot_directives trio, repo-true contractiles, dual-STATE reconciliation).",
+  "2026-04-15..05-30: CI/workflow standardization, MPL-2.0 licence migration (7a84a1d), contractile 6-verb cleanup, and tech-debt audit baseline.",
+  "2026-06-06..06-19: 6a2 STATE reconciliation (#31), TypeFix Zero (TF0) section, estate-standardization-20260607 layout, OQ-001 resolution (PR #56), and CI-enforced coordination boundary (scripts/check-coordination-boundary.sh + placement.a2ml).",
+  "2026-09-09..10-12: Shared six-family map and glossary (docs/TYPE-CONNECTIONS.adoc + SVG), residual-evidence-types milestones 1 & 2 linked, secret-types scope boundary registered, resource-algebra and occupancy-types additions recorded.",
+  "2026-11-01..11-03: PROOF-POLICY ledger & bidirectional control harness (63 ledger + 18 kernel controls, #131 / PR #132); XP-1 promoted to Mathesis Grade 2i with zero-axiom Rocq (EchoTyping.v) and core Lean 4 (EchoTyping.lean) recheck witnesses alongside Agda (Proof CI run 41565790232, #57 / PR #133).",
+  "2026-11-03: Retired broken cross-owner reusable workflow callers with SHA-pinned self-contained jobs, populated www/.well-known/security.txt, hardened dependabot-automerge and rsr-antipattern (#121, #117, #32), retired non-applicable service Containerfile/container/groove scaffold (#59, #47), retargeted ANCHOR.a2ml and stale ABI refs (#58, #42, #41, #40), instantiated K9/Quickstart/.mailmap templates (OQ-002, #37, #36, #35), and refreshed READINESS.adoc & AFFIRMATION.adoc (#53, Refs #115, Refs #69).",
 ]
 
 [blockers-and-issues]
 issues = [
-  { id = "OQ-001", kind = "open-question", status = "resolved", raised = "2026-06-05", resolved = "2026-06-15", title = "Identity contradiction — coordination monorepo vs RSR proof scaffold", detail = "Narrative/STATE describe a docs-only coordination monorepo (\"does NOT contain compiler code\"), but src/interface/ + verification/proofs/ carry an un-rescoped RSR code scaffold; reconcile (docs-only ⇒ Tier T5/Exempt, drop scaffold) vs (real proof repo ⇒ re-scope). NOT decided here.", resolution = "Resolved 2026-06-15 (A): docs-only coordinator + cross-project verification host; the redundant src/ RSR ABI/FFI scaffold was removed (canonical proofs live in verification/proofs/); 'no compiler code' affirmed." },
-  { id = "OQ-002", kind = "template-residue", status = "open", raised = "2026-06-12", title = "Unreplaced template placeholders across community-health files", detail = "Template tokens (OWNER, REPO, AUTHOR, SECURITY_EMAIL, CONDUCT_*) remain unfilled in .github/ community files, self-validating/ k9 templates, and QUICKSTART-MAINTAINER.adoc; .machine_readable/ai/PLACEHOLDERS.adoc is the index. Needs a maintainer fill-in pass (just init or manual)." },
+  { id = "OQ-001", kind = "open-question", status = "resolved", raised = "2026-06-05", resolved = "2026-06-15", title = "Identity contradiction — coordination monorepo vs RSR proof scaffold", detail = "Reconcile docs-only coordination monorepo vs RSR ABI/FFI scaffold.", resolution = "Resolved 2026-06-15 (A): coordinator + cross-project verification host (verification/proofs/); redundant src/ RSR ABI/FFI scaffold removed." },
+  { id = "OQ-002", kind = "template-residue", status = "resolved", raised = "2026-06-12", resolved = "2026-11-03", title = "Unreplaced template placeholders across community-health and K9 files", detail = "Template tokens and runtime-service container stubs remained from rsr-template-repo.", resolution = "Resolved 2026-11-03: populated security.txt, .mailmap, Quickstart guides, methodology.a2ml, and K9 components; retired REQUIRES_INITIALISATION.adoc and runtime container/groove stubs." },
 ]
 
 [critical-next-actions]
 actions = [
-  "Decide OQ-001: docs-only coordination monorepo (drop RSR code scaffold) vs real proof repo (re-scope proofs).",
-  "Replace remaining template placeholders (OWNER, REPO, SECURITY_EMAIL, …) per .machine_readable/ai/PLACEHOLDERS.adoc.",
-  "Track Tropical.thy extensions (linorder instance, tropical matrices, Kleene algebra) in tropical-resource-typing and mirror progress in nextgen-typing docs.",
-  "Track and link the arXiv paper draft on speculative tropical session types once published.",
+  "Advance XP-1 from Mathesis Grade 2i to Grade 2ii by adding a non-DTT recheck leg (such as Isabelle/HOL).",
+  "Track upstream residual-evidence-types Phase 3 bridge obligations (#115): compose-claims over EchoComparison and non-vacuous revision over EpistemicComparison.",
+  "Track estate-wide maintainer affirmation signatures across the 9 type-family repositories (#69).",
   "Track typed-wasm aggregate ABI convention adoption in AffineScript/Ephapax integration paths as recursive-type support matures.",
-  "Run periodic drift scans so README.adoc, docs/ARCHITECTURE.adoc, docs/PIPELINE.adoc, and .machine_readable/descriptiles/{STATE,META,ECOSYSTEM}.a2ml stay synchronized.",
+  "Run periodic drift scans (just validate-pipeline-drift) so README.adoc, docs/ARCHITECTURE.adoc, docs/PIPELINE.adoc, and .machine_readable/descriptiles/{STATE,META,ECOSYSTEM}.a2ml stay synchronized.",
 ]
 
 [maintenance-status]
-last-run-utc = "2026-06-12T00:00:00Z"
-last-result = "pass"  # CRG Grade C: dogfood-gate, hypatia-scan, static-analysis-gate green (READINESS.md); governance checkpoint 2026-06-12
+last-run-utc = "2026-11-03T03:00:00Z"
+last-result = "pass"  # CRG Grade C (READINESS.adoc); Proof CI 41565790232 + SonarCloud 125686944300 green on main
 open-warnings = 0
 open-failures = 0
-recent-activity = "2026-05-30 CI/governance hardening: reusable-workflow wrappers (scorecard, secret-scanner, mirror, rust-ci, hypatia-scan), SHA repinning to live commits, stale ReScript fixture removal, tech-debt audit findings recorded."
+recent-activity = "2026-11-03 coordinator & CI completion: XP-1 Grade 2i multi-prover verification (PR #133), self-contained CI workflow replacements, OQ-002 placeholder/K9 instantiation, and READINESS/AFFIRMATION refresh."
 
 [recent-activity]
 events = [
-  { date = "2026-05-22", kind = "licence", detail = "Migrated licence from PMPL-1.0-or-later to MPL-2.0 across the repo (commit 7a84a1d)." },
-  { date = "2026-05-26", kind = "audit", detail = "Recorded estate-wide tech-debt audit findings in docs/tech-debt-2026-05-26.md (combined severity LOW; proof debt = 6 Idris2 believe_me markers in scaffold proof files; licence + docs debt OK)." },
-  { date = "2026-05-30", kind = "ci", detail = "CI reusable-wrapper rework (2026-05-26..2026-05-30): hypatia-scan, scorecard, secret-scanner, rust-ci, and mirror workflows converted to thin wrappers of standards reusables; reusable SHA pins repinned to live merge-commit SHAs (commit 4a848fd)." },
-  { date = "2026-06-09", kind = "docs", detail = "README.adoc: TypeFix Zero (TF0) calibration-calculus section added (commits f11cc29..ec3496f)." },
-  { date = "2026-06-12", kind = "governance", detail = "Estate standardization merged (governance docs, bot_directives, self-validating, flat contractiles, flake.nix removal); codeql cron monthly; checkpoint layer: dual STATE reconciled (root pointer-ized to 6a2), bot_directives trio added, contractiles populated with repo-true obligations." },
-  { date = "2026-06-19", kind = "governance", detail = "Coordination-boundary remediation: added AGENTS.md/CLAUDE.md + root .clinerules/.cursorrules/.windsurfrules, placement.a2ml routing directive, and a coordination-boundary CI guard + pre-commit hook; stripped the RSR src/interface ABI/FFI instructions from copilot-instructions/cline/cursor/windsurf/AI-CONVENTIONS and rewrote the template-residue AI.a2ml; removed the RSR ABI/TP proof scaffold from verification/proofs/ (owned by typed-wasm/typell), keeping the cross-project echo-types proof; reconciled PROOF-NEEDS/PROOF-STATUS." },
+  { date = "2026-06-12", kind = "governance", detail = "Estate standardization merged; dual STATE reconciled and flat contractiles populated." },
+  { date = "2026-06-19", kind = "governance", detail = "Coordination-boundary remediation (placement.a2ml + scripts/check-coordination-boundary.sh); RSR ABI/FFI scaffold retired under OQ-001." },
+  { date = "2026-09-09", kind = "docs", detail = "Added docs/TYPE-CONNECTIONS.adoc and SVG map across Echo, Epistemic, Tropical, Residual Evidence, and Choreographic families." },
+  { date = "2026-10-12", kind = "docs", detail = "Registered secret-types boundary, resource-algebra, occupancy-types, and D-2026-10-12-proof-kernel-ruling." },
+  { date = "2026-11-03", kind = "verification", detail = "Merged kernel assumption checks (#131 / PR #132) and XP-1 Rocq + Lean 4 Grade 2i recheck witnesses (#57 / PR #133; Proof CI run 41565790232)." },
+  { date = "2026-11-03", kind = "governance", detail = "Resolved OQ-002 template residue, replaced broken cross-owner reusable workflow callers, populated www/.well-known/security.txt, and refreshed READINESS.adoc & AFFIRMATION.adoc." },
 ]
 
 [ecosystem]
 part-of = ["hyperpolymath coordination infrastructure"]
-coordinates = ["typell", "typed-wasm", "katagoria", "tropical-resource-typing", "protocol-squisher"]
+coordinates = ["typell", "typed-wasm", "katagoria", "tropical-types", "echo-types", "epistemic-types", "residual-evidence-types", "choreographic-types", "secret-types", "protocol-squisher"]
 downstream-consumers = ["panll", "nextgen-languages/affinescript", "nextgen-languages/ephapax"]
 
 [type-research-map]
-review-date = "2026-09-09"
+review-date = "2026-11-03"
 guide = "docs/TYPE-CONNECTIONS.adoc"
 graphic = "docs/images/type-connections.svg"
 editable-source = "docs/images/type-connections.dot"
-families = ["echo-types", "epistemic-types", "tropical-types", "residual-evidence-types", "choreographic-types"]
-status = "Documentation map and glossary; arrows are conceptual, not integration or proof claims"
-residual-status = "Work in progress: minimal Agda core and narrow Echo/Epistemic comparisons checked; finite explorer separate"
-next-residual-milestone = "Dependency-preserving composition and evidence revision/retraction in residual-evidence-types"
-proof-validation = "Agda 2.6.4.3 safe/without-K: residual core, three expected rejections and two direct comparisons passed locally and in hosted job 34400282291; whole constituent suites not rerun"
-proof-receipt = "https://github.com/hyperpolymath/residual-evidence-types/blob/4325198c10e2e689f084c2f64a27213685a1ffd2/PROOF-STATUS.adoc"
+families = ["echo-types", "epistemic-types", "tropical-types", "residual-evidence-types", "choreographic-types", "secret-types"]
+status = "Documentation map and glossary; arrows are conceptual unless backed by an explicit proof receipt"
+residual-status = "Second milestone checked: minimal Agda core, composition/coarsening, constructive revision/retraction, 9 expected rejections, and finite-checker/explorer correspondence (546 configs)"
+next-residual-milestone = "Transport compose-claims over EchoComparison and non-vacuous warrant revision over EpistemicComparison (#115)"
+proof-validation = "XP-1 verified in nextgen-typing Proof CI run 41565790232 (Agda 2.8.0 + Coq 8.18.0 + Lean 4.15.0, Grade 2i); residual-evidence-types milestone 2 verified in hosted job 36740394802 (befdf964)"
+proof-receipt = "https://github.com/hyperpolymath/residual-evidence-types/blob/a9f3a9d2ae1c6e60644d6328df92f1b96e17cf1c/PROOF-STATUS.adoc"
 metadata-location = ".machine_readable/descriptiles/"
diff --git a/.machine_readable/descriptiles/anchor/ANCHOR.a2ml b/.machine_readable/descriptiles/anchor/ANCHOR.a2ml
index 577dacd..28b0291 100644
--- a/.machine_readable/descriptiles/anchor/ANCHOR.a2ml
+++ b/.machine_readable/descriptiles/anchor/ANCHOR.a2ml
@@ -4,13 +4,15 @@
 # ANCHOR.a2ml - authoritative anchor for this repository
 
 [metadata]
-version = "1.0.1"
-last-updated = "2026-06-12"
+version = "1.0.2"
+last-updated = "2026-11-03"
 
 [anchor]
+id = "org.hyperpolymath.nextgen-typing"
 schema = "hyperpolymath.anchor/1"
 repo = "hyperpolymath/nextgen-typing"
 authority = "upstream-canonical"
+status = "active"
 
 purpose = [
   "Define canonical semantics and policy boundaries for this repository.",
@@ -20,32 +22,34 @@ purpose = [
 
 [identity]
 project = "nextgen-typing"
-kind = "monorepo"                # coordination monorepo (no compiler code; see META ADR-001)
-one-sentence = "Coordination monorepo for the hyperpolymath type theory pipeline (katagoria → typell → typed-wasm → PanLL)"
+kind = "monorepo"                # coordination monorepo + cross-project proof host (META ADR-001, OQ-001)
+one-sentence = "Coordination monorepo and cross-project verification host for the hyperpolymath type theory pipeline (katagoria → typell → typed-wasm → PanLL)"
 domain = "type theory / programming-language research coordination"
 
 [semantic-authority]
 policy = "canonical"
 
 owns = [
-  "Project semantics and specification",
-  "Invariant definitions and contractiles",
-  "Reference implementation behavior",
+  "Cross-project pipeline architecture and routing boundaries",
+  "Shared type-family vocabulary and inter-family bridge obligations",
+  "Cross-project formal verification witnesses (verification/proofs/)",
 ]
 
 [implementation-policy]
-allowed = ["Rust", "Idris2", "Zig", "Scheme", "Shell", "Just", "AsciiDoc", "Markdown"]
-forbidden = ["Node.js", "npm"]
+allowed = ["Agda", "Rocq", "Lean 4", "Idris2", "Shell", "Just", "AsciiDoc", "Markdown", "A2ML", "Nickel"]
+forbidden = ["Node.js", "npm", "TypeScript", "Go"]
 
 [golden-path]
 smoke-test-command = [
-  "just test",
-  "just quality",
+  "just validate",
+  "just validate-coordination",
+  "just validate-pipeline-drift",
+  "just proof-witness-check",
 ]
 
 success-criteria = [
-  "Core tests pass",
-  "Quality gates pass",
+  "Coordination boundary and pipeline drift guards pass",
+  "Cross-project proof ledger and compiled witnesses pass",
   "No unresolved critical security findings",
 ]
 
@@ -56,15 +60,10 @@ must-have-anchor = true
 must-have-golden-path = true
 
 [semantic-authority-files]
-# NOTE (2026-06-12): the four paths below are template residue — none of them
-# exist in-tree. Kept verbatim pending maintainer decision (tracked as a
-# proposed issue at the 2026-06-12 governance checkpoint). The real
-# architecture authority files today are docs/ARCHITECTURE.adoc and
-# docs/PIPELINE.adoc.
-language-spec = "SPECIFICATION.md"
-formal-proofs = "docs/proofs/PROOFS.adoc"
-type-theory = "docs/theory/THEORY.adoc"
-algorithms = "docs/theory/ALGORITHMS.adoc"
+architecture = "docs/ARCHITECTURE.adoc"
+pipeline = "docs/PIPELINE.adoc"
+formal-proofs = "PROOF-STATUS.adoc"
+type-connections = "docs/TYPE-CONNECTIONS.adoc"
 
 # Dated realignment entries (most recent last).
 
@@ -74,3 +73,8 @@ what = "Estate standardization + governance checkpoint"
 why = "Adopt the estate-standardization-20260607 layout and refresh machine-readable metadata to current reality"
 evidence = "Merge of origin/estate-standardization-20260607 (workflows kept at main's reusable-wrapper versions); codeql cron monthly cherry-pick; root STATE.a2ml pointer-ized to 6a2/STATE.a2ml; 6a2 STATE/META refreshed to 2026-06-12; bot_directives trio (hypatia, gitbot-fleet, git-private-farm) added; flat contractiles populated with repo-true obligations (content ported from nested must/trust/dust/bust and root *.contractile files)"
 
+[[realignments]]
+date = "2026-11-03"
+what = "Retarget semantic-authority-files and golden-path to live coordinator + proof-host paths"
+why = "Retire template-residue dead paths (SPECIFICATION.md, docs/proofs/PROOFS.adoc, docs/theory/{THEORY,ALGORITHMS}.adoc) after OQ-001 and XP-1 Grade 2i verification (#40)"
+evidence = "docs/ARCHITECTURE.adoc, docs/PIPELINE.adoc, PROOF-STATUS.adoc, and docs/TYPE-CONNECTIONS.adoc verified in-tree; XP-1 Agda + Rocq + Lean 4 Grade 2i proofs checked under Proof CI"
diff --git a/.machine_readable/integrations/groove.a2ml b/.machine_readable/integrations/groove.a2ml
deleted file mode 100644
index 0289e11..0000000
--- a/.machine_readable/integrations/groove.a2ml
+++ /dev/null
@@ -1,38 +0,0 @@
-; SPDX-License-Identifier: MPL-2.0
-; Groove Protocol Manifest — declares API surfaces this project exposes.
-;
-; Used by V-triple connectors and the Groove bridge for snap-on/snap-off
-; service discovery. Edit this file to match your project's actual APIs.
-;
-; See: https://github.com/hyperpolymath/standards/tree/main/groove-protocol
-
-(groove-manifest
-  (version "1.0")
-
-  ; Service identity — replace nextgen-typing with your project name
-  (service "nextgen-typing")
-  (service-version "0.1.0")
-
-  ; Primary port — MUST be unique across the ecosystem.
-  ; Check PORT-REGISTRY.md in the standards repo before assigning.
-  ; https://github.com/hyperpolymath/standards/blob/main/PORT-REGISTRY.md
-  (port 0)  ; 0 = not assigned yet — run `just groove-setup` to assign
-
-  ; API surfaces this project exposes (dodeca-API)
-  ; Remove lines for API types you don't use.
-  (api-surfaces
-    (rest    (enabled true)  (path "/api/v1"))
-    (grpc    (enabled false) (port-offset 1))
-    (graphql (enabled false) (path "/graphql"))
-    (websocket (enabled false) (path "/ws"))
-    (sse     (enabled false) (path "/events"))
-    (groove  (enabled true)  (path "/.well-known/groove")))
-
-  ; Health endpoint — used by Groove discovery
-  (health "/health")
-
-  ; Capabilities — what this service can do for others
-  (capabilities ())
-
-  ; Dependencies — what this service needs from others
-  (dependencies ()))
diff --git a/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml b/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml
index 40db158..5d2c052 100644
--- a/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml
+++ b/.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml
@@ -132,8 +132,8 @@ quality_gate_required = [
 ]
 
 abi_ffi_policy = [
-  "ABI Idris2 in src/interface/Abi/*.idr (or src/interface/abi/*.idr)",
-  "FFI Zig in ffi/**/*.zig",
+  "Cross-project formal proofs in verification/proofs/ (tracked in verification/proofs/LEDGER.json)",
+  "Single-project ABI/FFI routed to owning repos (typed-wasm, typell) per .machine_readable/bot_directives/placement.a2ml",
 ]
 
 [should]
diff --git a/.machine_readable/root-allow.txt b/.machine_readable/root-allow.txt
index 3b3fccb..466eb51 100644
--- a/.machine_readable/root-allow.txt
+++ b/.machine_readable/root-allow.txt
@@ -1,2 +1,3 @@
 CLAUDE.md
+0-AI-MANIFEST.a2ml         # sole root A2ML entry point; CLADE.a2ml, ENSAID_CONFIG.a2ml, and 0.1-AI-MANIFEST.a2ml live under .machine_readable/
 build/                     # build orchestration: guix.scm relocated here (canon 1.2.1 guix-primary template_ref = "build/")
diff --git a/.machine_readable/self-validating/examples/project-metadata.k9.ncl b/.machine_readable/self-validating/examples/project-metadata.k9.ncl
index 3f59d9e..1e1329a 100644
--- a/.machine_readable/self-validating/examples/project-metadata.k9.ncl
+++ b/.machine_readable/self-validating/examples/project-metadata.k9.ncl
@@ -1,6 +1,6 @@
 K9!
 # SPDX-License-Identifier: MPL-2.0
-# Example Kennel-level K9 component: Project metadata
+# Kennel-level K9 component: nextgen-typing project metadata
 # Security Level: Kennel (pure data, no execution)
 # No signature required
 
@@ -16,40 +16,42 @@ K9!
       allow_subprocess = false,
     },
     metadata = {
-      name = "project-metadata",
+      name = "nextgen-typing-project-metadata",
       version = "1.0.0",
-      description = "Pure data configuration for project metadata",
+      description = "Pure data configuration for nextgen-typing coordination metadata",
       author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>",
     },
   },
 
-  # Project configuration
   project = {
-    name = "my-project",
+    name = "nextgen-typing",
     version = "0.1.0",
-    description = "A project following Rhodium Standard Repositories",
+    description = "Coordination monorepo and cross-project verification host for the hyperpolymath type theory pipeline",
 
     repository = {
-      url = "https://github.com/hyperpolymath/my-project",
+      url = "https://github.com/hyperpolymath/nextgen-typing",
       type = "git",
     },
 
     author = {
       name = "Jonathan D.A. Jewell",
       email = "j.d.a.jewell@open.ac.uk",
-      organization = "{{AUTHOR_ORG}}",
+      organization = "hyperpolymath",
     },
 
     license = "MPL-2.0",
 
     keywords = [
-      "rhodium-standard",
+      "type-theory",
+      "formal-verification",
+      "agda",
+      "rocq",
+      "lean4",
       "rsr",
       "hyperpolymath",
     ],
   },
 
-  # Export as JSON for other tools
   export = {
     format = "json",
     destination = "project-metadata.json",
diff --git a/.machine_readable/self-validating/examples/setup-repo.k9.ncl b/.machine_readable/self-validating/examples/setup-repo.k9.ncl
index d1fc8bb..7df55c8 100644
--- a/.machine_readable/self-validating/examples/setup-repo.k9.ncl
+++ b/.machine_readable/self-validating/examples/setup-repo.k9.ncl
@@ -35,16 +35,16 @@ K9!
     repo_name
       | String
       | std.string.NonEmpty
-      = "my-new-repo",
+      = "nextgen-typing",
 
     repo_type
       | [| 'Library, 'Application, 'Tool, 'Specification |]
-      = 'Application,
+      = 'Specification,
 
     primary_language
       | String
       | std.string.NonEmpty
-      = "rust",
+      = "agda",
 
     # RSR compliance features to enable
     features = {
@@ -91,11 +91,11 @@ K9!
     },
 
     "create-structure" = {
-      description = "Create RSR directory structure",
+      description = "Create coordinator directory structure",
       commands = [
-        "mkdir -p src/ docs/ tests/ scripts/",
+        "mkdir -p verification/proofs/ docs/ tests/ scripts/",
         "mkdir -p .github/workflows/",
-        "mkdir -p .machine_readable/contractiles/k9/",
+        "mkdir -p .machine_readable/self-validating/",
         "echo '✓ Directory structure created'",
       ],
     },
diff --git a/.machine_readable/self-validating/methodology-guard.k9.ncl b/.machine_readable/self-validating/methodology-guard.k9.ncl
index 8646f74..eb54dde 100644
--- a/.machine_readable/self-validating/methodology-guard.k9.ncl
+++ b/.machine_readable/self-validating/methodology-guard.k9.ncl
@@ -34,12 +34,8 @@ let methodology_guard = {
     divergent_invariant_language = {
       description = "No files in languages violating the divergent language invariant",
       severity = "error",
-      # When methodology.divergent-invariants.language-invariant is set,
-      # check that no new files introduce a different language for that purpose.
-      # Example: if language-invariant = "idris2", reject new .lean or .v files
-      # in the proof directories.
       check_type = "file-extension-guard",
-      scope = "src/",
+      scope = "verification/proofs/",
     },
 
     believe_me_ceiling = {
@@ -62,7 +58,7 @@ let methodology_guard = {
       description = "STATE.a2ml must not contain template placeholders",
       severity = "warning",
       file = ".machine_readable/descriptiles/STATE.a2ml",
-      reject_patterns = ["{{PLACEHOLDER}}", "NEXTGEN_TYPING", "rsr-template-repo"],
+      reject_patterns = ["UNFILLED_TOKEN", "NEXTGEN_TYPING", "rsr-template-repo"],
     },
 
     coverage_updated = {
diff --git a/.machine_readable/self-validating/template-hunt.k9.ncl b/.machine_readable/self-validating/template-hunt.k9.ncl
index b3fcb47..3e327ee 100644
--- a/.machine_readable/self-validating/template-hunt.k9.ncl
+++ b/.machine_readable/self-validating/template-hunt.k9.ncl
@@ -1,136 +1,73 @@
 K9!
 # SPDX-License-Identifier: MPL-2.0
-# K9 Hunt-level template: Full execution with Just recipes
-# Security Level: Hunt (full system access)
+# K9 Hunt-level component: nextgen-typing local verification runner
+# Security Level: Hunt (full execution with Just recipes)
 # ⚠️ SIGNATURE REQUIRED - Review carefully before use
 
 {
   pedigree = {
     schema_version = "1.0.0",
-    component_type = "TODO: describe component type (e.g., 'deployment', 'setup-script')",
+    component_type = "verification-runner",
     security = {
       leash = 'Hunt,
       trust_level = "full-system-access",
-      allow_network = true,
+      allow_network = false,
       allow_filesystem_write = true,
       allow_subprocess = true,
       signature_required = true,
     },
     metadata = {
-      name = "TODO: component-name",
+      name = "nextgen-typing-verification-runner",
       version = "1.0.0",
-      description = "TODO: Detailed description of what this component does",
+      description = "Runs coordination-boundary, pipeline-drift, and cross-project proof gates",
       author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>",
     },
     warnings = [
-      "This component has full system access",
+      "This component executes local repository verification scripts",
       "Only run from trusted sources with verified signatures",
       "Review all Just recipes before execution",
-      "Use dry-run mode first: ./must --dry-run run your-file.k9.ncl",
     ],
     side_effects = [
-      "TODO: List what files/directories this creates or modifies",
-      "TODO: List what commands this executes",
-      "TODO: List what network access this requires",
+      "Writes temporary proof build artefacts and witness receipts under verification/proofs/ or /tmp",
+      "Executes bash, jq, git, and installed proof kernels (Agda, Rocq, Lean 4)",
     ],
   },
 
-  # Configuration with contracts (Yard-level validation)
   config = {
-    # Add your configuration here with appropriate contracts
-    target_dir
+    receipt_dir
       | String
       | std.string.NonEmpty
-      = "/tmp/k9-output",
+      = "/tmp/nextgen-typing-receipts",
 
     dry_run | Bool = false,
-
-    # Add more config as needed
   },
 
-  # Just recipes for execution
-  # These run when: ./must run your-file.k9.ncl
   recipes = {
-    # Main entry point (runs by default)
     default = {
-      recipe = "TODO: main-task",
-      description = "TODO: What the default recipe does",
+      recipe = "verify-coordinator",
+      description = "Run coordination boundary, pipeline drift, and proof witness checks",
     },
 
-    # Define your recipes here
-    "main-task" = {
+    "verify-coordinator" = {
       dependencies = ["check-prerequisites"],
       commands = [
-        "echo 'TODO: Add your commands here'",
-        # Example: Create directory
-        # "mkdir -p %{config.target_dir}",
-        # Example: Run a command
-        # "just build",
-        # Example: Conditional execution
-        # "@if [ \"%{config.dry_run}\" = \"true\" ]; then echo '[DRY-RUN] Would execute'; else actual-command; fi",
+        "./scripts/check-coordination-boundary.sh",
+        "./scripts/check-pipeline-drift.sh .",
+        "./scripts/check-proof-enrolment.sh",
+        "./scripts/check-proof-ledger.sh",
+        "./scripts/proof-scan-dangerous.sh",
       ],
     },
 
     "check-prerequisites" = {
-      description = "Verify required tools and permissions",
-      commands = [
-        # Example: Check for required tools
-        # "command -v git || (echo 'ERROR: git not found' && exit 1)",
-        # Example: Check permissions
-        # "[ -w %{config.target_dir} ] || (echo 'ERROR: Cannot write to target directory' && exit 1)",
-        "echo '✓ Prerequisites checked'",
-      ],
-    },
-
-    # Add more recipes as needed
-    "build" = {
-      description = "Build the project",
-      commands = [
-        "echo 'TODO: Add build commands'",
-      ],
-    },
-
-    "deploy" = {
-      description = "Deploy the application",
-      dependencies = ["build"],
+      description = "Verify required tools are available",
       commands = [
-        "echo 'TODO: Add deployment commands'",
-      ],
-    },
-
-    "clean" = {
-      description = "Clean up generated files",
-      commands = [
-        "echo '⚠️  This will delete files - waiting 3 seconds...'",
-        "sleep 3",
-        "echo 'TODO: Add cleanup commands'",
-        # "rm -rf %{config.target_dir}",
+        "command -v git >/dev/null && command -v jq >/dev/null",
       ],
     },
   },
 
-  # Validation (Yard-level checks before Hunt execution)
   validation = {
-    check_target_dir = std.string.length config.target_dir > 0,
-    # Add more validation as needed
+    check_receipt_dir = std.string.length config.receipt_dir > 0,
   },
 }
-
-# Usage:
-# 1. Fill in TODO items above
-# 2. Define configuration with contracts
-# 3. Implement Just recipes with your commands
-# 4. Test with dry-run: ./must --dry-run run your-file.k9.ncl
-# 5. Review dry-run output carefully
-# 6. Sign the component: ./must sign your-file.k9.ncl
-# 7. Distribute with signature: your-file.k9.ncl.sig
-# 8. Users verify and run: ./must verify && ./must run your-file.k9.ncl
-#
-# Security checklist:
-# ✓ All TODO items filled in
-# ✓ side_effects documented accurately
-# ✓ Commands reviewed for safety
-# ✓ No hardcoded secrets or credentials
-# ✓ Proper error handling in recipes
-# ✓ Tested in dry-run mode
-# ✓ Component signed with trusted key
diff --git a/.machine_readable/self-validating/template-kennel.k9.ncl b/.machine_readable/self-validating/template-kennel.k9.ncl
index 4228b26..9db04fb 100644
--- a/.machine_readable/self-validating/template-kennel.k9.ncl
+++ b/.machine_readable/self-validating/template-kennel.k9.ncl
@@ -1,13 +1,13 @@
 K9!
 # SPDX-License-Identifier: MPL-2.0
-# K9 Kennel-level template: Pure data configuration
+# K9 Kennel-level component: nextgen-typing coordination family registry
 # Security Level: Kennel (data-only, no execution)
 # No signature required - safe for any use
 
 {
   pedigree = {
     schema_version = "1.0.0",
-    component_type = "TODO: describe component type (e.g., 'build-config', 'metadata')",
+    component_type = "coordination-metadata",
     security = {
       leash = 'Kennel,
       trust_level = "data-only",
@@ -16,39 +16,37 @@ K9!
       allow_subprocess = false,
     },
     metadata = {
-      name = "TODO: component-name",
+      name = "nextgen-typing-family-registry",
       version = "1.0.0",
-      description = "TODO: Brief description of what this component contains",
+      description = "Declarative registry of coordinated type-research families and pipeline stages",
       author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>",
     },
   },
 
-  # Your configuration data here
   config = {
-    # Example: Pure data values
-    setting_1 = "value",
-    setting_2 = 42,
-    setting_3 = true,
+    repository = "hyperpolymath/nextgen-typing",
+    role = "coordination-and-cross-project-verification",
+    proof_root = "verification/proofs",
 
-    nested = {
-      key = "value",
-    },
+    pipeline = [
+      "katagoria",
+      "typell",
+      "typed-wasm",
+      "PanLL",
+    ],
 
-    list = [
-      "item1",
-      "item2",
+    families = [
+      "echo-types",
+      "epistemic-types",
+      "tropical-types",
+      "residual-evidence-types",
+      "choreographic-types",
+      "secret-types",
     ],
   },
 
-  # Optional: Export format specification
   export = {
-    format = "json",  # or "yaml", "toml"
-    destination = "output.json",
+    format = "json",
+    destination = "coordination-registry.json",
   },
 }
-
-# Usage:
-# 1. Fill in TODO items above
-# 2. Add your configuration data to config = { ... }
-# 3. Validate: nickel typecheck your-file.k9.ncl
-# 4. Export: nickel export your-file.k9.ncl > output.json
diff --git a/.machine_readable/self-validating/template-yard.k9.ncl b/.machine_readable/self-validating/template-yard.k9.ncl
index a723f5a..ed7e3d2 100644
--- a/.machine_readable/self-validating/template-yard.k9.ncl
+++ b/.machine_readable/self-validating/template-yard.k9.ncl
@@ -1,13 +1,13 @@
 K9!
 # SPDX-License-Identifier: MPL-2.0
-# K9 Yard-level template: Configuration with validation
+# K9 Yard-level component: nextgen-typing proof-policy configuration with contracts
 # Security Level: Yard (Nickel evaluation with contracts)
 # Signature recommended but not required
 
 {
   pedigree = {
     schema_version = "1.0.0",
-    component_type = "TODO: describe component type (e.g., 'validated-config', 'schema')",
+    component_type = "validated-config",
     security = {
       leash = 'Yard,
       trust_level = "validated-config",
@@ -16,69 +16,38 @@ K9!
       allow_subprocess = false,
     },
     metadata = {
-      name = "TODO: component-name",
+      name = "nextgen-typing-proof-policy-config",
       version = "1.0.0",
-      description = "TODO: Brief description with validation details",
+      description = "Contract-validated configuration for cross-project proof verification",
       author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>",
     },
   },
 
-  # Configuration with Nickel contracts for validation
   config = {
-    # Example: String that cannot be empty
     name
       | String
       | std.string.NonEmpty
-      = "TODO: default value",
+      = "nextgen-typing",
 
-    # Example: Number with range constraint
-    port
-      | Number
-      | std.contract.from_predicate (fun p => p > 0 && p < 65536)
-      = 8080,
+    ledger_path
+      | String
+      | std.string.NonEmpty
+      = "verification/proofs/LEDGER.json",
 
-    # Example: Boolean flag
-    enabled | Bool = true,
+    strict_witnesses | Bool = true,
 
-    # Example: Enum (one of several values)
-    environment
-      | [| 'Development, 'Staging, 'Production |]
-      = 'Development,
+    source_prover
+      | [| 'Agda, 'Idris2 |]
+      = 'Agda,
 
-    # Example: List with non-empty constraint
-    items
+    recheck_provers
       | Array String
       | std.array.NonEmpty
-      = ["item1", "item2"],
-
-    # Example: Nested object with contracts
-    database = {
-      host | String | std.string.NonEmpty = "localhost",
-      port | Number | std.contract.from_predicate (fun p => p > 0 && p < 65536) = 5432,
-      name | String | std.string.NonEmpty = "mydb",
-    },
+      = ["rocq", "lean4"],
   },
 
-  # Validation rules (additional cross-field checks)
   validation = {
-    # Example: Check that at least one item exists
-    check_items = std.array.length config.items > 0,
-
-    # Example: Check that production has secure settings
-    check_production =
-      if config.environment == 'Production then
-        config.enabled == true
-      else
-        true,
-
-    # Add your custom validation rules here
+    check_recheck_provers = std.array.length config.recheck_provers >= 2,
+    check_strict = config.strict_witnesses == true,
   },
 }
-
-# Usage:
-# 1. Fill in TODO items above
-# 2. Define your config with appropriate contracts
-# 3. Add validation rules in validation = { ... }
-# 4. Validate: nickel typecheck your-file.k9.ncl
-# 5. Evaluate: nickel eval your-file.k9.ncl
-# 6. If validation passes, use in your application
diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc
index 9233243..3494a4f 100644
--- a/AFFIRMATION.adoc
+++ b/AFFIRMATION.adoc
@@ -1,15 +1,17 @@
 // SPDX-License-Identifier: MPL-2.0
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= AFFIRMATION — coordination checks, 2026-09-09
+= AFFIRMATION — coordination and cross-project proof checks, 2026-11-03
 :toc:
 
-This is a bounded verification record for the shared type-family map and
-coordination layer. It records observed results, including failures and checks
-whose scope is narrower than their success message suggests.
+This is a bounded verification record for `nextgen-typing` as the type-theory
+coordination repository and cross-project proof host (`OQ-001`). It records
+observed local checks and linked hosted CI receipts, together with explicit
+scope boundaries.
 
-The previous June affirmation remains available as a
-https://github.com/hyperpolymath/nextgen-typing/blob/0b3693acfe09fdd4254cd6a77f2d241f20624b81/AFFIRMATION.adoc[historical snapshot in Git].
-Its dates, paths, toolchain and proof inventory are not current verification receipts.
+Earlier snapshots remain available in Git history:
+https://github.com/hyperpolymath/nextgen-typing/blob/c4ea39721d7ba893478fe57b5f749a89f2996508/AFFIRMATION.adoc[2026-09-09 affirmation]
+and
+https://github.com/hyperpolymath/nextgen-typing/blob/0b3693acfe09fdd4254cd6a77f2d241f20624b81/AFFIRMATION.adoc[June 2026 snapshot].
 
 == Anchor and scope
 
@@ -17,101 +19,51 @@ Its dates, paths, toolchain and proof inventory are not current verification rec
 |===
 |Field |Observed value
 |Repository |`hyperpolymath/nextgen-typing`
-|Branch |`docs/type-connections`
-|Checked commit |`1a8c836b23115510a0c9b883c0b73f8710f8a18c`
-|Check session |2026-09-09 UTC; anchor captured at `20:34:41Z`, followed by the checks below
-|Working tree |Clean at the checked commit; the map regenerated without a diff.
-This affirmation is added after the checks and does not claim to verify itself.
-|Local toolchain |Just 1.56.0; Bash 5.2.37; Git 2.47.3; Agda 2.6.4.3;
-Graphviz 2.42.4
-|Checked commit signature |`git log -1 --format='%H %G? %GS'` reported `G`
-(good signature), signer `jonathan.jewell@gmail.com`.
-|Canonical metadata |`.machine_readable/descriptiles/`
+|Base `main` anchor |`c4ea39721d7ba893478fe57b5f749a89f2996508` (PR #133 squash-merged 2026-11-03T02:23Z)
+|Check session |2026-11-03 UTC
+|Hosted `Proof CI` receipt on `main` |https://github.com/hyperpolymath/nextgen-typing/actions/runs/41565790232[Run `41565790232`] (`just proof-witness-check (strict)` -> `just proof-check-all`, exit `0`: Agda 2.8.0 `--safe --without-K --cubical-compatible`, Coq 8.18.0 `coqc` + `coqchk` + `Print Assumptions`, core Lean 4.15.0 `#print axioms` + `getModuleIdxFor?`, plus 63 ledger and 18 kernel bidirectional controls)
+|Hosted static-analysis receipt on `main` |https://sonarcloud.io/summary/new_code?id=hyperpolymath_nextgen-typing&branch=main[SonarCloud check-run `125686944300`] at `c4ea39721d7ba893478fe57b5f749a89f2996508` (Quality Gate `SUCCESS`, `0` Security Hotspots; supersedes historical red check-run `106934611138` at `86cb69e5`)
+|Canonical metadata |`.machine_readable/descriptiles/` (`STATE.a2ml`, `META.a2ml`, `ECOSYSTEM.a2ml`, `anchor/ANCHOR.a2ml`)
 |===
 
-The observation horizon is this commit's coordination files and the named
-checks below. Whole constituent proof suites, production deployments and
-general mathematical novelty are outside this record.
+The observation horizon is this repository's coordination documents, workflow
+definitions, and `verification/proofs/` cross-project witnesses (`XP-1`).
+Whole constituent proof suites, production deployments, and estate-wide
+maintainer sign-offs tracked under issue #69 remain outside this single-repo
+record unless explicitly cited below.
 
-== Coordination results
+== Local coordinator and ledger checks
 
 [cols="2,1,4",options="header"]
 |===
 |Command |Exit |Meaning and limit
-|`just type-map` |0 |SVG regenerates from its DOT source without a diff.
-|`just validate-rsr` |0 |The recipe's required files, metadata and policy markers are present.
-|`just validate-state` |0 |Its required metadata/project markers are present;
-this is not a complete A2ML parser.
-|`just validate-coordination` |0 |The repository's ownership boundary check passes.
-|`just validate-pipeline-drift` |0 |The named pipeline documents and descriptiles
-agree on the guarded chain, invariants and dates (`2026-09-09`).
-|`just must-check` |0 |The recipe's licence/README/file-name checks pass.
-Its source-header scan examines at most 20 matching Rust/ReScript/Gleam files;
-this is not an exhaustive SPDX audit.
-|`just trust-license-content` |0 |The recipe's licence-text marker check passes;
-it does not establish licence consistency across every file.
-|`just trust-no-secrets-committed` |0 |The three prohibited credential-file
-paths checked by this recipe are absent. Separately, the deterministic
-`sonar analyze secrets` scan of this worktree reported no issues.
-|`gh actions-lock --verify-local` |0 |All 28 workflows have lockfile coverage.
-The tool notes an inline validator SHA; it matches the lockfile's reviewed pin.
-Offline coverage does not establish that mutable upstream refs have not moved.
+|`bash scripts/validate-template.sh .` |0 |29 workflows, required metadata, `verification/proofs/` artefacts, SPDX headers (12/12), and placeholder checks pass with 0 errors and 0 warnings.
+|`bash scripts/check-coordination-boundary.sh` |0 |Confirms no compiler or single-project implementation code exists outside `verification/proofs/`.
+|`bash scripts/check-pipeline-drift.sh .` |0 |Confirms `README.adoc`, `docs/ARCHITECTURE.adoc`, `docs/PIPELINE.adoc`, and `.machine_readable/descriptiles/{STATE,META,ECOSYSTEM}.a2ml` agree on the canonical chain, TypeLL invariant, and `2026-11-03` date.
+|`bash scripts/check-proof-ledger.sh` |0 |Audits `verification/proofs/LEDGER.json` against `PROOF-POLICY` (`46ee18323305`, amended 2026-11-01): `XP-1` at Grade `2i`, 4 proof sources, 2 proven DTT recheck legs (`rocq`, `lean4`), reachable receipt `c4ea3972`.
+|`bash scripts/proof-scan-dangerous.sh` |0 |Nested-comment-aware proof escape-hatch scanner across Agda, Rocq, and Lean 4 sources finds zero postulates, axioms, `Admitted`, or `sorry`.
+|`bash tests/proofs/run-ledger-controls.sh` |0 |All 63 positive and negative ledger, enrolment, correspondence, and comment-scanner controls hold.
+|`bash tests/aspect_tests.sh` |0 |4/4 cross-cutting checks pass (SPDX headers, escape-hatch scanner, coordination boundary, enrolment consistency + ledger audit).
+|`bash tests/workflows/validate_workflows_test.sh .github/workflows` |0 |29/29 workflow files carry SPDX headers and `name:` fields; 15/15 required gates present; `.github/workflows/actions.lock` covers every step-level `uses:` reference.
+|`bash tests/rsr_antipattern_heading_test.sh` |0 |Positive and negative Markdown heading fixtures confirm anchored heading detection (`^#[[:space:]]+`) without false positives on fenced code comments.
 |===
 
-The actual `validate-state` recipe was also exercised against isolated fixtures:
-valid metadata passed; missing metadata, missing project and absent state failed.
-The aggregate `just validate` failed for each invalid fixture. These controls
-establish failure propagation, not complete syntax validation.
+== Resolution of 2026-09-09 recorded failures
 
-The workflow SPDX check passed the repository and controls for a valid opening
-comment header, a missing identifier and an identifier placed after YAML content.
-The downloaded `gh-actions-lock` v0.1.6 linux-amd64 binary matched SHA-256
-`4181ec1da5408b34b9a542a7ee5c6ce3a4d6ac815c7d0206a00ceca8a817f4e3`
-and successfully ran the same offline coverage check.
+All five failures recorded in the 2026-09-09 affirmation have been resolved:
 
-== Failures and misleading success messages
-
-[cols="2,1,4",options="header"]
+[cols="2,4",options="header"]
 |===
-|Command |Exit |Observed result
-|`just proof-check-coq` |0 |No `.v` files occur in the enumerated
-`verification/proofs/` tree. The success message verifies no Coq theorem.
-|`just proof-check-idris2` |0 |No `.idr` files occur in that tree.
-The success message verifies no Idris theorem.
-|`just proof-scan-dangerous` |1 |One match: the comment saying "zero postulates"
-in `verification/proofs/agda/EchoTyping.agda`. This lexical match is not a
-proof-position postulate and is not a successful proof audit either.
-|`just verify-template` |1 |Unfilled setup placeholders, template references
-and the Groove port-zero marker remain. `REQUIRES_INITIALISATION.adoc` tracks
-outstanding decisions. The checker also reports placeholder examples in comments.
-|`just trust-verify` |1 |The `trust-container-images-pinned` subcheck fails
-on the root `Containerfile`. The two earlier trust subchecks pass.
+|2026-09-09 item |2026-11-03 resolution
+|`just proof-check-coq` (empty `.v` loop) |`verification/proofs/coq/EchoTyping.v` and `verification/proofs/lean4/EchoTyping.lean` are enrolled and compiled + kernel-queried (`coqchk` + `Print Assumptions`, `#print axioms` + `getModuleIdxFor?`) in `Proof CI` (`41565790232`), and `scripts/check-proofs.sh` fails closed if a prover is missing (`exit 2`) or a proven leg compiles zero files.
+|`just proof-check-idris2` (misleading pass on 0 files) |`scripts/check-proofs.sh idris2` explicitly reports `0 files checked` rather than claiming theorem verification; `XP-1` is a theory theorem (`Agda` + `Rocq` + `Lean 4`).
+|`just proof-scan-dangerous` (false positive on prose comment in `EchoTyping.agda`) |Replaced by nested-comment-aware `scripts/proof-scan-dangerous.sh` with per-language comment stripping (verified by controls 1–4, 29, 35, 41–43, 61–62).
+|`just verify-template` (unfilled placeholders, `REQUIRES_INITIALISATION.adoc`, `groove.a2ml` port `0`) |Coordinator templates instantiated (`OQ-002`), `www/.well-known/security.txt` and `.github/.mailmap` populated, non-applicable runtime-service `Containerfile` / `container/` / `groove.a2ml` and `REQUIRES_INITIALISATION.adoc` retired.
+|`just trust-verify` (unpinned root `Containerfile`) |Root service `Containerfile` retired; `.devcontainer/Containerfile` base image is `@sha256:` digest-pinned (`cgr.dev/chainguard/wolfi-base@sha256:6b2fd3aa...`).
 |===
 
-These are existing maintenance obligations, left visible. This record does not
-turn an empty proof loop or a failed scanner into evidence of verification.
-The current Agda cross-project files are present but were not rechecked here.
-
-== Separate residual proof evidence
-
-The first residual milestone belongs to `residual-evidence-types`.
-https://github.com/hyperpolymath/residual-evidence-types/actions/runs/34400741631[Its latest checked publication]
-passed the minimal Agda core, three expected-rejection controls and two direct
-comparisons with the published Echo and Epistemic interfaces. See the
-https://github.com/hyperpolymath/residual-evidence-types/blob/b2cd4e2f40005f20d5c4bd9a06051c3215b4db9a/PROOF-STATUS.adoc[proof status at that revision]
-for exact statements, pins and standard-library warnings.
-
-The link:docs/TYPE-CONNECTIONS.adoc[shared glossary] links those bounded results.
-The map's dashed arrows express conceptual relationships and further obligations.
-Composition, evidence revision, a certified finite checker and explorer
-correspondence remain open in the owning project.
-
-== Reproduce the record
-
-Use the checked commit above and run each command in the tables independently,
-retaining its exit status and output. A later successful hosted check does not
-erase the listed local failures. A later source change needs a new record.
+== Bounded limits and open obligations
 
-This record was prepared by Codex from the actual local runs and linked hosted
-results. The checked commit's signature result is recorded separately from
-these claims; no additional maintainer attestation is asserted here.
+* *Local prover availability*: running `scripts/check-proof-enrolment.sh` in an environment without `agda`, `coqc`/`coqchk`, and `lean` exits `2` (`BLOCKED`) by design rather than silently skipping. Running `scripts/check-proofs.sh` for an enrolled prover that is absent exits `1` (`FAIL (missing-toolchain)`); full kernel compilation and the 18 kernel-assumption controls (`tests/proofs/run-kernel-assumption-controls.sh`) are verified in hosted `Proof CI` (`41565790232`).
+* *Residual Evidence sibling milestones*: `residual-evidence-types` https://github.com/hyperpolymath/residual-evidence-types/actions/runs/36740394802[hosted run `36740394802`] (`befdf9641c1bc6ecf58946e5ccbd0c630f4fc4c3`, 2026-09-30) verified the second residual milestone (composition, revision, 9 expected rejections, and finite-checker/explorer correspondence); transporting `compose-claims` across `EchoComparison` and non-vacuous warrant revision across `EpistemicComparison` remain open upstream obligations (#115).
+* *Maintainer signature attestation (#69)*: commit-signature and estate-wide affirmation sign-off across all 9 type-family repositories remain tracked under #69; this document records factual automated check results only and asserts no human cryptographic countersignature beyond Git commit metadata.
diff --git a/Containerfile b/Containerfile
deleted file mode 100644
index fe48877..0000000
--- a/Containerfile
+++ /dev/null
@@ -1,41 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
-#
-# Containerfile for nextgen-typing — Type Theory Pipeline
-# Build: podman build -t {{project}}:latest -f Containerfile .
-# Run:   podman run --rm -it {{project}}:latest
-# Seal:  selur seal {{project}}:latest
-
-# --- Build stage ---
-FROM cgr.dev/chainguard/wolfi-base:latest AS build
-
-# TODO: Install build dependencies for your stack
-# Examples:
-#   RUN apk add --no-cache rust cargo       # Rust
-#   RUN apk add --no-cache elixir erlang    # Elixir
-#   RUN apk add --no-cache zig              # Zig
-
-WORKDIR /build
-COPY . .
-
-# TODO: Replace with your build command
-# Examples:
-#   RUN cargo build --release
-#   RUN mix deps.get && MIX_ENV=prod mix release
-#   RUN zig build -Doptimize=ReleaseSafe
-
-# --- Runtime stage ---
-FROM cgr.dev/chainguard/static:latest
-
-# Copy built artifact from build stage
-# TODO: Replace with your binary/artifact path
-# Examples:
-#   COPY --from=build /build/target/release/{{project}} /usr/local/bin/
-#   COPY --from=build /build/_build/prod/rel/{{project}} /app/
-#   COPY --from=build /build/zig-out/bin/{{project}} /usr/local/bin/
-
-# Non-root user (chainguard images default to nonroot)
-USER nonroot
-
-# TODO: Replace with your entrypoint
-# ENTRYPOINT ["/usr/local/bin/{{project}}"]
diff --git a/GEMINI.md b/GEMINI.md
deleted file mode 100644
index 3e8ce56..0000000
--- a/GEMINI.md
+++ /dev/null
@@ -1,4 +0,0 @@
-# Pointer
-
-The canonical, tool-agnostic instructions for this repository are in
-**[AGENTS.md](./AGENTS.md)**. Read that file. Do not duplicate rules here.
diff --git a/Justfile b/Justfile
index 537cc9f..2f0003a 100644
--- a/Justfile
+++ b/Justfile
@@ -55,14 +55,14 @@ info:
     @[ -f ".machine_readable/descriptiles/STATE.a2ml" ] && grep -oP 'phase\s*=\s*"\K[^"]+' .machine_readable/descriptiles/STATE.a2ml | head -1 | xargs -I{} echo "Phase: {}" || true
 
 # Run Invariant Path overlay tools for this repository
-invariant-path *ARGS:
-    ./scripts/invariant-path.sh {{ARGS}}
+invariant-path *args:
+    ./scripts/invariant-path.sh "$@"
 
 # ═══════════════════════════════════════════════════════════════════════════════
 # INIT — Bootstrap a new project from this template
 # ═══════════════════════════════════════════════════════════════════════════════
 
-# Interactive project bootstrap — replaces all {{PLACEHOLDER}} tokens
+# Interactive project bootstrap — replaces all <PLACEHOLDER> tokens
 init:
     #!/usr/bin/env bash
     set -euo pipefail
@@ -333,8 +333,8 @@ verify-template:
     fi
 
     # Check for template defaults still present
-    if grep -q 'rsr-template-repo' Justfile 2>/dev/null; then
-        echo "⚠ Justfile still references 'rsr-template-repo' — update project name"
+    if grep -q 'rsr-template-''repo' Justfile 2>/dev/null; then
+        echo "⚠ Justfile still references template default name — update project name"
         FOUND=1
     fi
 
@@ -671,16 +671,16 @@ readiness:
     #   cargo test --test readiness -- --nocapture
     @echo "Readiness tests complete!"
 
-# Print the current CRG grade (reads from READINESS.md '**Current Grade:** X' line)
+# Print the current CRG grade (reads from READINESS.adoc or READINESS.md)
 crg-grade:
-    @grade=$$(grep -oP '(?<=\*\*Current Grade:\*\* )[A-FX]' READINESS.md 2>/dev/null | head -1); \
+    @grade=$$(grep -oP '(?<=\*Current Grade:\* )[A-FX]|(?<=\*\*Current Grade:\*\* )[A-FX]' READINESS.adoc READINESS.md 2>/dev/null | head -1 | sed 's/.*://'); \
     [ -z "$$grade" ] && grade="X"; \
     echo "$$grade"
 
 # Print a shields.io CRG badge for embedding in README files
-# Looks for '**Current Grade:** X' in READINESS.md; falls back to X
+# Looks for '*Current Grade:* X' in READINESS.adoc (or '**Current Grade:** X' in READINESS.md); falls back to X
 crg-badge:
-    @grade=$$(grep -oP '(?<=\*\*Current Grade:\*\* )[A-FX]' READINESS.md 2>/dev/null | head -1); \
+    @grade=$$(grep -oP '(?<=\*Current Grade:\* )[A-FX]|(?<=\*\*Current Grade:\*\* )[A-FX]' READINESS.adoc READINESS.md 2>/dev/null | head -1 | sed 's/.*://'); \
     [ -z "$$grade" ] && grade="X"; \
     case "$$grade" in \
       A) color="brightgreen" ;; \
@@ -848,8 +848,7 @@ container-init:
     set -euo pipefail
 
     if [ ! -d "container" ]; then
-        echo "Error: container/ directory not found."
-        echo "This repo may not have been created from rsr-template-repo."
+        echo "Error: container/ directory not found (not applicable to coordinator repos)."
         exit 1
     fi
 
@@ -1297,7 +1296,7 @@ assail:
 
 # Self-diagnostic — checks dependencies, permissions, paths
 doctor:
-    @echo "Running diagnostics for rsr-template-repo..."
+    @echo "Running diagnostics for {{project}}..."
     @echo "Checking required tools..."
     @command -v just >/dev/null 2>&1 && echo "  [OK] just" || echo "  [FAIL] just not found"
     @command -v git >/dev/null 2>&1 && echo "  [OK] git" || echo "  [FAIL] git not found"
@@ -1307,7 +1306,7 @@ doctor:
 
 # Guided tour of key features
 tour:
-    @echo "=== rsr-template-repo Tour ==="
+    @echo "=== {{project}} Tour ==="
     @echo ""
     @echo "1. Project structure:"
     @ls -la
@@ -1322,12 +1321,12 @@ tour:
 
 # Open feedback channel with diagnostic context
 help-me:
-    @echo "=== rsr-template-repo Help ==="
+    @echo "=== {{project}} Help ==="
     @echo "Platform: $(uname -s) $(uname -m)"
     @echo "Shell: $SHELL"
     @echo ""
     @echo "To report an issue:"
-    @echo "  https://github.com/hyperpolymath/rsr-template-repo/issues/new"
+    @echo "  https://github.com/{{OWNER}}/{{REPO}}/issues/new"
     @echo ""
     @echo "Include the output of 'just doctor' in your report."
 
diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 6aaed14..8c4af95 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -207,10 +207,12 @@ recheck witnesses; and `+scripts/proof-scan-dangerous.sh+` scans all four proof
 sources (nested-comment-aware) on every run.
 |===
 
-The receipt behind all four is CI run **41314454646** at
-`+3cd185939179773f177b59e6fee360719695dfc7+` — the first run that invoked the
-policy's canonical form, `+agda --safe --without-K --cubical-compatible+`
-(PROOF-POLICY §2.1, amended 2026-11-01), through `+just proof-check-agda+`.
+The receipt behind all four on `+main+` is CI run **41565790232** at
+`+c4ea39721d7ba893478fe57b5f749a89f2996508+`, which executed `+just proof-check-all+`
+across the policy's canonical Agda form (`+agda --safe --without-K --cubical-compatible+`,
+PROOF-POLICY §2.1, amended 2026-11-01), Rocq (`+coqc+` + `+coqchk+` + `+Print Assumptions+`),
+and core Lean 4 (`+lean+` + `+#print axioms+` + module-origin verification),
+succeeding run **41314454646** (`+3cd185939179773f177b59e6fee360719695dfc7+`).
 
 The earlier receipt (run 41299544043 at `+4c6b918+`) invoked `+--safe+` with the
 library manifest only: `+--without-K+` came from the file's `+{-# OPTIONS #-}+`
@@ -385,7 +387,7 @@ operations against. Its own identity claim is **open** (see caveat 1 below).
 115 Qed / 0 Admitted / **61 undischarged axioms**, OND-6 open by design. It
 reaches this proof only through echo-types' library manifest; none of its Coq is
 in the import cone.
-|Receipt commit |receipt |`+3cd185939179773f177b59e6fee360719695dfc7+` (run 41314454646, canonical §2.1 invocation)
+|Receipt commit |receipt |`+c4ea39721d7ba893478fe57b5f749a89f2996508+` (run 41565790232 on `+main+`, canonical §2.1 + Grade 2i recheck invocation)
 |===
 
 These are not the same kind of entry, and the ledger says so: a *dependency-pin*
diff --git a/QUICKSTART-DEV.adoc b/QUICKSTART-DEV.adoc
index 5be2757..1af5844 100644
--- a/QUICKSTART-DEV.adoc
+++ b/QUICKSTART-DEV.adoc
@@ -1,112 +1,78 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-// Template: QUICKSTART-DEV.adoc — clone → build → test → PR
-// Replace rsr-template-repo, {{BUILD_CMD}}, {{TEST_CMD}}, {{LANG_STACK}} with actuals
-= rsr-template-repo — Quick Start for Developers
+= nextgen-typing — Contributor Quick Start
 :toc:
 :toclevels: 2
 
 == Tech Stack
 
-{{LANG_STACK}}
+* **Coordination & documentation**: AsciiDoc (`.adoc`), Markdown, A2ML (`.a2ml`), Nickel/K9 (`.k9`, `.k9.ncl`), Graphviz (`.dot` → `.svg`).
+* **Cross-project formal verification (`verification/proofs/`)**: Agda (`--safe --without-K`) source-of-truth proofs, independently rechecked in Rocq (Coq 8.18) and core Lean 4 (4.15.0, zero Mathlib).
+* **Gate scripts**: Bash 5 + `jq` + `git` (`scripts/` and `tests/`).
 
 == Set Up Development Environment
 
-=== Option A: Guix (preferred)
-
 [source,bash]
 ----
-guix shell
+git clone https://github.com/hyperpolymath/nextgen-typing.git
+cd nextgen-typing
 ----
 
-=== Option B: Nix (fallback)
+For a reproducible Guix shell when Guix is available:
 
 [source,bash]
 ----
-nix develop
+guix shell -D -f build/guix.scm
 ----
 
-=== Option C: Manual
-
-[source,bash]
-----
-git clone https://github.com/hyperpolymath/rsr-template-repo.git
-cd rsr-template-repo
-just setup-dev
-----
+For coordinator boundary, drift, and ledger checks, Bash, `jq`, and Git are sufficient; Agda, Coq (`coqc`/`coqchk`), and Lean 4 (`lean`) are required when compiling proof witnesses locally.
 
-== Build
+== Validate and Test
 
 [source,bash]
 ----
-{{BUILD_CMD}}
+./scripts/check-coordination-boundary.sh
+./scripts/check-pipeline-drift.sh .
+./scripts/check-proof-enrolment.sh
+./scripts/check-proof-ledger.sh
+./scripts/proof-scan-dangerous.sh
+bash tests/proofs/run-ledger-controls.sh
+bash tests/rsr_antipattern_heading_test.sh
 ----
 
-== Test
+With `just` and the proof kernels installed:
 
 [source,bash]
 ----
-{{TEST_CMD}}
+just validate
+just validate-coordination
+just validate-pipeline-drift
+just proof-check-all
 ----
 
-== Project Structure
+== Repository Structure
 
 [source]
 ----
-rsr-template-repo/
-├── src/                  # Source code
-├── src/abi/              # Idris2 ABI definitions (if applicable)
-├── ffi/zig/              # Zig FFI bridge (if applicable)
-├── tests/                # Test suite
-├── docs/                 # Documentation
-├── .machine_readable/    # Checkpoint files (STATE, META, ECOSYSTEM)
-├── Justfile              # Task runner recipes
-├── guix.scm              # Guix environment
-├── flake.nix             # Nix environment (fallback)
-└── 0-AI-MANIFEST.a2ml    # AI agent entry point
-----
-
-== Key Recipes
-
-[source,bash]
+nextgen-typing/
+├── docs/                       # Architecture, pipeline spec, type-family map
+├── verification/proofs/        # Cross-project proofs (LEDGER.json, agda/, coq/, lean4/)
+├── scripts/                    # Boundary, drift, enrolment, ledger, and witness gates
+├── tests/                      # Bidirectional §7 proof controls and aspect checks
+├── .machine_readable/          # Descriptiles, contractiles, policies, K9 specs
+├── build/guix.scm              # Guix environment manifest
+├── Justfile                    # Task runner recipes
+└── 0-AI-MANIFEST.a2ml          # AI agent entry point
 ----
-just build          # Build the project
-just test           # Run tests
-just doctor         # Self-diagnostic
-just lint           # Lint and format
-just panic-scan     # Security scan via panic-attacker
-just tour           # Guided tour of the codebase
-----
-
-== Before Submitting a PR
 
-[source,bash]
-----
-just lint           # Format and lint
-just test           # All tests pass
-just panic-scan     # No new security issues
-----
-
-== Contractile Invariants
-
-Read `.machine_readable/MUST.contractile` before making changes.
-Key invariants that must never be violated:
-
-{{MUST_INVARIANTS}}
-
-== LLM/AI Agent Development
-
-If using an AI assistant, load the warmup context first:
-
-[source,bash]
-----
-just llm-context    # Outputs role-appropriate context
-----
+== Key Invariants
 
-Or read `0-AI-MANIFEST.a2ml` and `.claude/CLAUDE.md` directly.
+* **No compiler or single-project code**: `nextgen-typing` hosts only cross-project coordination artefacts and explicitly enrolled cross-project proofs (`scripts/check-coordination-boundary.sh` and `.machine_readable/bot_directives/placement.a2ml`).
+* **Synchronized pipeline metadata**: `STATE.a2ml`, `META.a2ml`, `ECOSYSTEM.a2ml`, `docs/PIPELINE.adoc`, and `docs/ARCHITECTURE.adoc` must remain synchronized (`scripts/check-pipeline-drift.sh`).
+* **Zero proof escape hatches**: every enrolled proof must pass `PROOF-POLICY` kernel assumption checks (`coqchk` + `Print Assumptions`, `#print axioms` + `getModuleIdxFor?`, and `agda --safe --without-K`) with zero unwaived axioms (`scripts/check-proof-ledger.sh`).
 
 == Get Help
 
-* **Architecture**: link:EXPLAINME.adoc[EXPLAINME.adoc]
-* **Wiki**: https://github.com/hyperpolymath/rsr-template-repo/wiki
-* **Report issue**: `just help-me`
+* **Architecture**: link:EXPLAINME.adoc[EXPLAINME.adoc] and link:docs/ARCHITECTURE.adoc[docs/ARCHITECTURE.adoc]
+* **Agent routing**: link:AGENTS.md[AGENTS.md] and `0-AI-MANIFEST.a2ml`
+* **Issues**: https://github.com/hyperpolymath/nextgen-typing/issues
diff --git a/QUICKSTART-MAINTAINER.adoc b/QUICKSTART-MAINTAINER.adoc
index d2123a6..c4854e6 100644
--- a/QUICKSTART-MAINTAINER.adoc
+++ b/QUICKSTART-MAINTAINER.adoc
@@ -1,130 +1,34 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-// Template: QUICKSTART-MAINTAINER.adoc — packaging, deploying, and maintaining
-// Replace rsr-template-repo, nextgen-typing, {{DEPS}} with actuals
-= rsr-template-repo — Quick Start for Platform Maintainers
+= nextgen-typing — Coordinator Maintenance Guide
 :toc:
 :toclevels: 2
 
-== Overview
+== Scope
 
-This guide covers packaging, deploying, and maintaining rsr-template-repo for
-distribution on your platform.
+`nextgen-typing` is a pure coordination and cross-project verification repository; it produces no runtime service, compiler binary, container deployment, or installable package. Constituent repositories (`typell`, `typed-wasm`, `echo-types`, `epistemic-types`, `tropical-types`, `residual-evidence-types`, `choreographic-types`, `secret-types`) own their own build, release, and packaging pipelines.
 
-== Runtime Dependencies
+== Dependencies and Checks
 
-{{DEPS}}
-
-== Build from Source
-
-[source,bash]
-----
-git clone https://github.com/hyperpolymath/rsr-template-repo.git
-cd rsr-template-repo
-just build-release
-----
-
-Output: `{{BUILD_OUTPUT_PATH}}`
-
-== Packaging
-
-=== Guix
-
-[source,bash]
-----
-guix build -f build/guix.scm
-----
-
-=== Nix
+* **Coordinator & ledger gates**: Bash 5+, `jq`, `git`, `just` (optional runner), Graphviz (`dot` for `just type-map`).
+* **Cross-project proof CI (`Proof CI`)**: Agda 2.8.0 (`agda-stdlib` v2.4 at `2a5a0dec0a3cb5c87468ce101388a513d39dbf10` + pinned `hyperpolymath/echo-types`), Coq 8.18.0 (`coqc`, `coqchk`, `coqtop`), and core Lean 4.15.0 (SHA-256-verified Linux release tarball).
 
 [source,bash]
 ----
-nix build
+./scripts/check-coordination-boundary.sh
+./scripts/check-pipeline-drift.sh .
+just validate
+just proof-check-all
+git diff --check
 ----
 
-=== Container (Stapeln)
-
-[source,bash]
-----
-just stapeln-export    # Generates Containerfile
-podman build -t rsr-template-repo .
-----
-
-=== Manual Package
-
-[source,bash]
-----
-just install --prefix=/usr/local
-----
-
-Files installed:
-
-[cols="1,2"]
-|===
-| Path | Contents
-
-| `$PREFIX/bin/`
-| Executables
-
-| `$PREFIX/share/nextgen-typing/`
-| Data files, assets
-
-| `$PREFIX/share/doc/nextgen-typing/`
-| Documentation
-
-| `$PREFIX/share/applications/`
-| .desktop file (Linux, if GUI)
-
-| `$PREFIX/share/man/man1/`
-| Man pages
-|===
-
-== Configuration
-
-Default config location: `$XDG_CONFIG_HOME/nextgen-typing/config.toml`
-
-Fallback: `$HOME/.config/nextgen-typing/config.toml`
-
-== Health Checks
-
-[source,bash]
-----
-just doctor            # Full diagnostic
-just run --version   # Version check
-just run --selftest  # Built-in self-test
-----
-
-== Updating
-
-[source,bash]
-----
-git pull
-just build-release
-just install --prefix=/usr/local
-----
-
-Or via OPSM: `opsm update nextgen-typing`
-
-== Security Notes
-
-* License: MPL-2.0 (Palimpsest License)
-* All dependencies SHA-pinned
-* `panic-attacker` scan results: link:INSTALL-SECURITY-REPORT.adoc[]
-* OpenSSF Scorecard: see badge in README
-
-== Multi-Instance Deployment
-
-For deploying multiple instances (e.g., different users or tenants):
-
-[source,bash]
-----
-just install --prefix=/opt/nextgen-typing-instance1 --config=/etc/nextgen-typing/instance1.toml
-just install --prefix=/opt/nextgen-typing-instance2 --config=/etc/nextgen-typing/instance2.toml
-----
+== Maintaining Synchronized Surfaces
 
-Each instance has isolated config, data, and logs.
+1. **Pipeline state**: when updating `.machine_readable/descriptiles/STATE.a2ml`, keep `last-updated` synchronized across `STATE.a2ml`, `META.a2ml`, `ECOSYSTEM.a2ml`, `docs/PIPELINE.adoc` (`version`), and `docs/ARCHITECTURE.adoc` (header date), then run `./scripts/check-pipeline-drift.sh .`.
+2. **Cross-project proofs**: every proof file under `verification/proofs/` must be enrolled in both `scripts/check-coordination-boundary.sh` (`ALLOWED_PROOFS`), `.machine_readable/bot_directives/placement.a2ml` (`[verification].allowed-proofs`), the prover's `MANIFEST`, and `verification/proofs/LEDGER.json`.
+3. **Workflows**: `.github/workflows/actions.lock` locks every GitHub Action dependency; run `gh actions-lock` whenever workflow `uses:` references change.
 
-== Reporting Issues
+== Governance and Security
 
-* Upstream: https://github.com/hyperpolymath/rsr-template-repo/issues
-* With diagnostic: `just help-me` (pre-fills context)
+* Follow link:GOVERNANCE.adoc[GOVERNANCE.adoc] and link:MAINTAINERS.adoc[MAINTAINERS.adoc].
+* Report security vulnerabilities via link:.github/SECURITY.md[.github/SECURITY.md] (`www/.well-known/security.txt`).
diff --git a/QUICKSTART-USER.adoc b/QUICKSTART-USER.adoc
index 0893e63..27af27a 100644
--- a/QUICKSTART-USER.adoc
+++ b/QUICKSTART-USER.adoc
@@ -1,125 +1,26 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-// Template: QUICKSTART-USER.adoc — 5-minute path to working software
-// Replace rsr-template-repo, Rsr Template Repo — See README.adoc for details., just run, Rsr Template Repo started successfully. with actuals
-= rsr-template-repo — Quick Start for Users
+= nextgen-typing — Reader Quick Start
 :toc:
 :toclevels: 2
 
-== What is rsr-template-repo?
+== What this repository is
 
-Rsr Template Repo — See README.adoc for details.
+`nextgen-typing` is the coordination monorepo and cross-project verification host for the hyperpolymath type-theory pipeline (`katagoria → typell → typed-wasm → PanLL`) and its six research families (`echo-types`, `epistemic-types`, `tropical-types`, `residual-evidence-types`, `choreographic-types`, `secret-types`). It is not a compiler, runtime service, or single-project package.
 
-== Prerequisites
+== Find a project or specification
 
-Before you begin, ensure you have:
+1. Read link:README.adoc[the README] for the pipeline front door.
+2. Open link:docs/ARCHITECTURE.adoc[docs/ARCHITECTURE.adoc] and link:docs/PIPELINE.adoc[docs/PIPELINE.adoc] for the architectural contracts and machine-readable pipeline graph.
+3. Open link:docs/TYPE-CONNECTIONS.adoc[docs/TYPE-CONNECTIONS.adoc] for the shared six-family map, glossary, and inter-family bridge obligations.
+4. Check link:PROOF-STATUS.adoc[PROOF-STATUS.adoc] and `verification/proofs/LEDGER.json` for cross-project verification status (`XP-1`, Grade `2i` across Agda, Rocq, and Lean 4).
 
-* **just** — task runner (https://github.com/casey/just[install guide])
-* Platform-specific requirements listed below
+== Explore this coordinator
 
-[cols="1,3"]
-|===
-| Platform | Additional Requirements
+* link:EXPLAINME.adoc[EXPLAINME.adoc] — rationale and scope boundary (`OQ-001`).
+* `.machine_readable/bot_directives/placement.a2ml` — authoritative ownership routing table.
+* `.machine_readable/descriptiles/` — `STATE.a2ml`, `META.a2ml`, `ECOSYSTEM.a2ml`, and `anchor/ANCHOR.a2ml`.
 
-| Linux
-| See README.adoc
+== Installation
 
-| macOS
-| See README.adoc
-
-| Windows
-| See README.adoc
-|===
-
-== Install
-
-=== Option 1: Standard Install (recommended)
-
-[source,bash]
-----
-# Clone and set up
-git clone https://github.com/hyperpolymath/rsr-template-repo.git
-cd rsr-template-repo
-just setup
-----
-
-The setup script will:
-
-* Detect your platform and shell
-* Install missing dependencies (with your permission)
-* Configure the application
-* Offer install location choices
-* Run a self-diagnostic to verify everything works
-
-=== Option 2: Container (via Stapeln)
-
-[source,bash]
-----
-just stapeln-run
-----
-
-=== Option 3: Portable (no system changes)
-
-[source,bash]
-----
-just install --portable --prefix=./rsr-template-repo-portable
-----
-
-== First Run
-
-[source,bash]
-----
-just run
-----
-
-Expected output:
-
-[source]
-----
-Rsr Template Repo started successfully.
-----
-
-== Self-Diagnostic
-
-If something isn't working:
-
-[source,bash]
-----
-just doctor
-----
-
-This checks all dependencies, permissions, paths, and connectivity.
-If it finds issues, it will suggest fixes.
-
-To attempt automatic repair:
-
-[source,bash]
-----
-just heal
-----
-
-== Get Help
-
-* **In-app**: `just run --help`
-* **Guided tour**: `just tour`
-* **Report a problem**: `just help-me` (pre-fills diagnostic context)
-* **Wiki**: https://github.com/hyperpolymath/rsr-template-repo/wiki
-
-== Uninstall
-
-[source,bash]
-----
-just uninstall
-----
-
-You will be asked:
-
-1. Which uninstall tier (Bennett reversible, parameter-based, standard, or secure)
-2. Whether to include or exclude your data
-3. Whether to clear caches and LLM models
-
-== Next Steps
-
-* Read the link:README.adoc[README] for full feature overview
-* Read the link:EXPLAINME.adoc[EXPLAINME] for architecture and design decisions
-* Try `just tour` for a guided walkthrough
+There is no runtime binary or service to install from this repository. To build or install a language, kernel, or target toolchain, follow the instructions in its owning repository (`typell`, `typed-wasm`, `affinescript`, `ephapax`, `echo-types`, `residual-evidence-types`, etc.).
diff --git a/READINESS.adoc b/READINESS.adoc
index 06e8da0..7dd3ffa 100644
--- a/READINESS.adoc
+++ b/READINESS.adoc
@@ -1,55 +1,52 @@
-== nextgen-typing Component Readiness Assessment
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= nextgen-typing Component Readiness Assessment
 
 *Standard:*
-https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades[Component
-Readiness Grades (CRG) v2.2] *Current Grade:* C *Assessed:* 2026-06-05
+https://github.com/metadatastician/standards/tree/main/component-readiness-grades[Component
+Readiness Grades (CRG) v2.2] *Current Grade:* C *Assessed:* 2026-11-03
 *Assessor:* Jonathan D.A. Jewell
 
 '''''
 
 === Summary
 
-[width="100%",cols="25%,8%,17%,50%",options="header",]
+[width="100%",cols="28%,8%,18%,46%",options="header"]
 |===
 |Component |Grade |Release Stage |Evidence Summary
-|Primary component |C |Alpha-stable |Dogfooded on own project; CI
-passing
+|Pipeline coordination & cross-project verification (`nextgen-typing`) |C |Coordinator-stable |Coordinator boundary & drift gates green; `XP-1` formal bridge verified at Mathesis Grade `2i` across Agda, Rocq, and core Lean 4 (`Proof CI` run `41565790232`)
 |===
 
-*Overall:* Grade C — dogfooding confirmed, CI passing, deep annotation
-in place.
+*Overall:* Grade C — repository-scoped coordination, machine-readable state synchronization, and cross-project multi-prover verification are dogfooded and enforced in CI (`OQ-001` and `OQ-002` resolved).
 
 '''''
 
 === Grade C Evidence
 
-* Deployed and dogfooded on the nextgen-typing project itself
-* CI passing (dogfood-gate, hypatia-scan, static-analysis-gate)
-* TEST-NEEDS.md documents test matrix
-* No home failures
-* Deep code and folder annotation in place per CRG v2 requirements
+* *Coordinator & boundary enforcement*: `scripts/check-coordination-boundary.sh` and `scripts/check-pipeline-drift.sh` enforce ownership routing (`placement.a2ml`) and canonical metadata/doc synchronization across `STATE.a2ml`, `META.a2ml`, `ECOSYSTEM.a2ml`, `docs/PIPELINE.adoc`, and `docs/ARCHITECTURE.adoc`.
+* *Cross-project formal verification (`XP-1`, Mathesis Grade `2i`)*: `EchoTyping.agda` (`--safe --without-K --cubical-compatible`), `EchoTyping.v` (Coq 8.18 `coqc` + `coqchk` + `Print Assumptions`), and `EchoTyping.lean` (core Lean 4.15, zero Mathlib, `#print axioms` + module-origin check) pass `just proof-check-all` with zero axioms on `main` (`Proof CI` run `41565790232` at `c4ea39721d7ba893478fe57b5f749a89f2996508`).
+* *Bidirectional test & control matrix*: link:TEST-NEEDS.adoc[TEST-NEEDS.adoc] documents 63 proof-ledger controls (`tests/proofs/run-ledger-controls.sh`), 18 kernel-assumption controls (`tests/proofs/run-kernel-assumption-controls.sh`), 29-workflow structural checks (`tests/workflows/validate_workflows_test.sh`), heading antipattern fixtures (`tests/rsr_antipattern_heading_test.sh`), and aspect/E2E checks (`tests/aspect_tests.sh`, `tests/e2e/template_instantiation_test.sh`).
+* *Hosted CI & static analysis*: `Proof CI` (`41565790232`), `Coordination Boundary`, `Dogfood Gate`, `Static Analysis Gate`, and `SonarCloud Code Analysis` (`125686944300` on `main` @ `c4ea3972`, Quality Gate passed with 0 security hotspots) are verified green; retired cross-owner `hyperpolymath/standards` workflow callers are replaced by self-contained SHA-pinned jobs locked in `.github/workflows/actions.lock`.
+* *Annotation & discoverability*: `0-AI-MANIFEST.a2ml`, `.machine_readable/descriptiles/`, `www/.well-known/{security,ai,humans}.txt`, and `PROOF-STATUS.adoc` are populated with zero unreplaced template placeholders.
 
 '''''
 
 === Promotion Path to Grade B
 
-Grade B requires: *6+ diverse external targets tested, issues fed back*.
+Grade B requires *6+ diverse external targets consuming and validating the coordination/verification contracts with issues fed back*:
 
-Diversity means: different languages, different architectures, different
-use cases.
-
-To reach B: 1. Deploy on at least 6 external projects that differ
-meaningfully from each other 2. Confirm it works in each (or document
-failures) 3. Feed back any issues found (GitHub issues or PRs) 4. Update
-this file with the evidence
+1. Complete independent cross-family bridge proofs in constituent repositories (e.g., `residual-evidence-types` `compose-claims` over `EchoComparison` and non-vacuous `EpistemicComparison` revision under `#115`).
+2. Add a non-DTT recheck leg (such as Isabelle/HOL) for `XP-1` to advance from Mathesis Grade `2i` to Grade `2ii`.
+3. Validate pipeline/ABI consumption end-to-end across `typell`, `typed-wasm`, `affinescript`, `ephapax`, `protocol-squisher`, and `panll`, feeding integration issues back into `nextgen-typing`.
 
 '''''
 
 === Concerns and Maintenance Notes
 
-_Document any known limitations, demotion risks, or maintenance concerns
-here._
+* *Pure coordinator scope (`OQ-001`)*: `nextgen-typing` contains no compiler, runtime binary, or single-project library code; runtime fuzzing and unit-coverage metrics belong to constituent implementation repositories (`typell`, `typed-wasm`, `affinescript`, `ephapax`).
+* *Mathesis Grade `2i` boundary*: `XP-1` is verified across three DTT kernels (Agda, Rocq, Lean 4) with zero axioms, but has no HOL/Mizar non-DTT recheck leg yet (`Grade 2ii` open) and discharges nothing of `echo-types`'s own open positive identity criterion (Criterion 2).
+* *Synchronized date invariant*: edits to `.machine_readable/descriptiles/{STATE,META,ECOSYSTEM}.a2ml`, `docs/PIPELINE.adoc`, or `docs/ARCHITECTURE.adoc` must keep their `last-updated` / `version` / header date synchronized or `scripts/check-pipeline-drift.sh` fails closed.
 
 '''''
 
-=== Run `+just crg-badge+` to generate the shields.io badge for your README.
+Run `+just crg-badge+` to generate the shields.io badge from this file.
diff --git a/REQUIRES_INITIALISATION.adoc b/REQUIRES_INITIALISATION.adoc
deleted file mode 100644
index a6e6b41..0000000
--- a/REQUIRES_INITIALISATION.adoc
+++ /dev/null
@@ -1,261 +0,0 @@
-== REQUIRES INITIALISATION
-
-*This repository is not finished being set up.* 22 substitution token(s)
-across 19 file(s) still have no value.
-
-=== Why this is not already done
-
-This repo was created from `+hyperpolymath/rsr-template-repo+`. The mint
-(`+just repo-init+`) fills every token that has a single mechanical
-answer — owner, repo, author, dates, licence, branch — and it has done
-so here.
-
-The tokens below are the ones it _deliberately cannot_ answer. They need
-a decision or a fact that exists only in your head: what this project is
-for, what command builds it, which port the service listens on, whether
-a PGP key is held at all. The template’s own token vocabulary says as
-much — you cannot sensibly answer "`required invariants`" in a
-thirty-second bootstrap.
-
-They were left *visibly unfilled on purpose*. The alternatives were both
-worse: inventing plausible values would put confident falsehoods into a
-security policy and an architecture document, and silently deleting the
-sections would hide the fact that a decision is owed. A visible gap is
-honest; a fabricated answer is not.
-
-=== Do not delete this file until every item below is resolved
-
-This file is the only marker that the work is outstanding. Deleting it
-early does not finish the setup, it just conceals it — and the next
-person or agent to arrive will reasonably assume the repo is complete.
-
-* *If you are a person:* delete this file yourself once the last item is
-done.
-* *If you are an agent:* resolve what you legitimately can, leave the
-rest, and delete this file only when no token below remains anywhere in
-the tree. Do not delete it to make a gate go green.
-
-Re-running the estate top-up tool will remove this file automatically
-once nothing is outstanding, so the safest way to finish is to fix the
-tokens and let the check confirm it.
-
-=== Do these first
-
-`+.github/settings.yml+` is applied to the forge by a GitHub App. An
-unfilled token here can be written into the repository’s real name or
-description. This has fired before in this estate: illegal braces were
-collapsed to dashes and a repo was renamed `+-REPO-+`, which then read
-as deleted.
-
-* `+{{DESCRIPTION}}+` — One-line description used in
-.github/settings.yml. HIGH PRIORITY: settings.yml is applied by a GitHub
-App, so an unfilled token here can be written into forge metadata
-verbatim.
-
-=== What is needed, and where it goes
-
-==== `+{{ARGS}}+`
-
-Arguments for the justfile recipe this appears in.
-
-Appears in:
-
-* `+.machine_readable/contractiles/Justfile+`
-* `+Justfile+`
-
-==== `+{{AUTHOR_EMAIL_ALT}}+`
-
-Appears in:
-
-* `+.github/.mailmap+`
-
-==== `+{{AUTHOR_ORG}}+`
-
-Author’s organisation. NOTE: no filled instance of this exists anywhere
-in the estate — consider deleting the field instead.
-
-Appears in:
-
-* `+.machine_readable/self-validating/examples/project-metadata.k9.ncl+`
-
-==== `+{{BUILD_CMD}}+`
-
-The exact command that builds this project.
-
-Appears in:
-
-* `+QUICKSTART-DEV.adoc+`
-
-==== `+{{BUILD_OUTPUT_PATH}}+`
-
-Where the build artefact lands.
-
-Appears in:
-
-* `+QUICKSTART-MAINTAINER.adoc+`
-
-==== `+{{DEPS}}+`
-
-Prose summary of runtime/build dependencies.
-
-Appears in:
-
-* `+QUICKSTART-MAINTAINER.adoc+`
-
-==== `+{{DESCRIPTION}}+`
-
-One-line description used in .github/settings.yml. HIGH PRIORITY:
-settings.yml is applied by a GitHub App, so an unfilled token here can
-be written into forge metadata verbatim.
-
-Appears in:
-
-* `+.github/settings.yml+`
-
-==== `+{{LANG_STACK}}+`
-
-The language stack, in prose.
-
-Appears in:
-
-* `+QUICKSTART-DEV.adoc+`
-
-==== `+{{LICENSE}}+`
-
-SPDX identifier for this repo’s licence.
-
-Appears in:
-
-* `+container/Containerfile+`
-* `+container/manifest.toml+`
-
-==== `+{{MUST_INVARIANTS}}+`
-
-The invariants this project guarantees. Not answerable in a bootstrap;
-it is the point of the repo.
-
-Appears in:
-
-* `+QUICKSTART-DEV.adoc+`
-
-==== `+{{ONE_PARAGRAPH_PURPOSE}}+`
-
-A paragraph on what this is for.
-
-Appears in:
-
-* `+.machine_readable/contractiles/Intentfile.a2ml+`
-
-==== `+{{OPENSSF_PROJECT_ID}}+`
-
-OpenSSF project ID, same registration.
-
-Appears in:
-
-* `+TEMPLATE-STANDARDS-AUDIT.adoc+`
-
-==== `+{{PGP_KEY_URL}}+`
-
-Public URL the PGP key can be fetched from. Same caveat as
-PGP_FINGERPRINT.
-
-Appears in:
-
-* `+.well-known/security.txt+`
-
-==== `+{{PORT}}+`
-
-Port the container service listens on.
-
-Appears in:
-
-* `+container/Containerfile+`
-* `+container/compose.toml+`
-* `+container/deploy.k9.ncl+`
-* `+container/entrypoint.sh+`
-* `+container/manifest.toml+`
-* `+container/vordr.toml+`
-
-==== `+{{PROJECT_DESCRIPTION}}+`
-
-One-line description, matching the forge description.
-
-Appears in:
-
-* `+container/Containerfile+`
-* `+container/manifest.toml+`
-
-==== `+{{PROJECT_UNIQUE_STRENGTH}}+`
-
-What this does that its alternatives do not.
-
-Appears in:
-
-* `+.machine_readable/bot_directives/methodology.a2ml+`
-
-==== `+{{REGISTRY}}+`
-
-Container registry to publish to.
-
-Appears in:
-
-* `+container/compose.toml+`
-* `+container/ct-build.sh+`
-* `+container/deploy.k9.ncl+`
-
-==== `+{{SECURITY_EMAIL}}+`
-
-Address for private vulnerability reports. Two competing values exist in
-the estate (`+6759885+hyperpolymath@users.noreply.github.com+` and
-`+security@hyperpolymath.org+`) — pick one deliberately.
-
-Appears in:
-
-* `+.well-known/security.txt+`
-
-==== `+{{SERVICE_NAME}}+`
-
-Container service name.
-
-Appears in:
-
-* `+container/.gatekeeper.yaml+`
-* `+container/Containerfile+`
-* `+container/compose.toml+`
-* `+container/ct-build.sh+`
-* `+container/deploy.k9.ncl+`
-* `+container/entrypoint.sh+`
-* `+container/manifest.toml+`
-* `+container/vordr.toml+`
-
-==== `+{{TEST_CMD}}+`
-
-The exact command that runs its tests.
-
-Appears in:
-
-* `+QUICKSTART-DEV.adoc+`
-
-==== `+{{VERSION}}+`
-
-Version/tag for the container image.
-
-Appears in:
-
-* `+container/deploy.k9.ncl+`
-* `+container/manifest.toml+`
-* `+container/vordr.toml+`
-
-==== `+{{WEBSITE}}+`
-
-Project homepage URL, or delete the field if there is none.
-
-Appears in:
-
-* `+.well-known/security.txt+`
-
-'''''
-
-Generated by the estate top-up pass. Rationale and the governing rulings
-are in `+hyperpolymath/standards+`; the token vocabulary is
-`+.machine_readable/ai/PLACEHOLDERS.adoc+` in `+rsr-template-repo+`.
diff --git a/ROADMAP.adoc b/ROADMAP.adoc
index 561bd17..249eadb 100644
--- a/ROADMAP.adoc
+++ b/ROADMAP.adoc
@@ -34,7 +34,7 @@ See link:docs/TYPE-CONNECTIONS.adoc[connections, meanings and ownership].
 * [x] Add ecosystem references to all constituent repos (affinescript, ephapax, tropical-resource-typing, protocol-squisher)
 * [x] katagoria: first research artefact structure (research/level-candidates/)
 * [x] protocol-squisher ECOSYSTEM.a2ml migrated from SCM format to A2ML
-* [x] typed-wasm ABI conventions implementation (layout proofs in src/abi/layout/ — DecEq, nullability, distinctness, passConvention + proofs, Stdlib)
+* [x] typed-wasm ABI conventions implementation (layout proofs in `typed-wasm` — DecEq, nullability, distinctness, passConvention + proofs, Stdlib)
 
 == Medium-Term
 
diff --git a/TEMPLATE-STANDARDS-AUDIT.adoc b/TEMPLATE-STANDARDS-AUDIT.adoc
index af49238..77c9ccb 100644
--- a/TEMPLATE-STANDARDS-AUDIT.adoc
+++ b/TEMPLATE-STANDARDS-AUDIT.adoc
@@ -28,24 +28,24 @@ Inventory snapshot at audit time:
 
 | Placeholder badge tokens in README
 | `README.adoc`
-| `{{OPENSSF_PROJECT_ID}}`, `hyperpolymath`, `nextgen-typing`
-| placeholder
-| Template placeholders are intentional pre-bootstrap content.
-| Keep; document clearly as template tokens.
+| `<OPENSSF_PROJECT_ID>`, `hyperpolymath`, `nextgen-typing`
+| resolved
+| Instantiated for `nextgen-typing` during coordinator setup.
+| Resolved.
 
 | Docs links used `.adoc` files not present
 | legacy `README.adoc` (pre-migration)
 | `CONTRIBUTING.adoc`, `GOVERNANCE.adoc`, `SECURITY.adoc`
 | outdated
-| Actual files are `CONTRIBUTING.md`, no root `GOVERNANCE.adoc`, `SECURITY.md`.
+| Actual files are `CONTRIBUTING.md`, `GOVERNANCE.adoc`, `SECURITY.adoc` / `.github/SECURITY.md`.
 | Fixed README links to existing files.
 
-| ABI path lower-case only
+| ABI/proof scaffold retired under OQ-001
 | legacy `README.adoc` + legacy checks
-| `src/interface/abi/*.idr`
-| outdated
-| Current tree has `src/interface/Abi/*.idr` (uppercase A).
-| Updated docs/checks to accept current path.
+| `verification/proofs/`
+| resolved
+| Redundant RSR ABI/FFI scaffold dropped in PR #56 (OQ-001); cross-project proofs live under `verification/proofs/`.
+| Retargeted docs and checks to `verification/proofs/`.
 
 | Root manifest structure with non-existent files
 | legacy `0-AI-MANIFEST.a2ml` (pre-migration)
diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc
index d4be499..d82ee64 100644
--- a/TEST-NEEDS.adoc
+++ b/TEST-NEEDS.adoc
@@ -1,137 +1,36 @@
-== TEST-NEEDS: rsr-template-repo
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= TEST-NEEDS: nextgen-typing
+:toc:
 
-=== CRG Grade: C — ACHIEVED 2026-04-04
+== Current State (Updated 2026-11-03)
 
-=== Current State (Updated 2026-04-04)
+`nextgen-typing` is a pure coordination and cross-project formal verification repository (`OQ-001`, PR #56). The former `rsr-template-repo` Idris2/Zig scaffold was retired in favour of cross-project proof witnesses under `verification/proofs/` and bidirectional gate control suites under `tests/`.
 
-[width="100%",cols="40%,26%,34%",options="header",]
+[width="100%",cols="34%,20%,46%",options="header"]
 |===
 |Category |Count |Details
-|*Source modules* |6 |3 Idris2 ABI (Foreign, Layout, Types), 2 Zig FFI
-(build, main), 1 Zig integration test template
-
-|*Unit tests* |0 |None in main source (inline tests in main.zig)
-
-|*Integration tests* |1 |test/integration_test.zig (documented template,
-1 placeholder test)
-
-|*E2E tests* |1 |tests/e2e/template_instantiation_test.sh (full
-instantiation + validation)
-
-|*Workflow tests* |1 |tests/workflows/validate_workflows_test.sh (21
-workflows validated)
-
-|*Validation tests* |1 |scripts/validate-template.sh (8-phase
-comprehensive validation)
-
-|*Benchmarks* |5 |benches/template_bench.sh (validation, Zig build,
-tests, workflows, instantiation)
-
-|*Fuzz tests* |0 |README.adoc scaffold with harness instructions
+|*Formal proof modules (`XP-1`)* |3 |`EchoTyping.agda` (Agda `--safe --without-K`), `EchoTyping.v` (Rocq 8.18), `EchoTyping.lean` (core Lean 4.15, zero Mathlib)
+|*Proof-ledger bidirectional controls* |63 |`tests/proofs/run-ledger-controls.sh` (`PROOF-POLICY` §7 positive + negative controls for ledger, enrolment, witness receipts, and comment-aware escape-hatch scanner)
+|*Kernel-assumption controls* |18 |`tests/proofs/run-kernel-assumption-controls.sh` (Coq `coqchk` + `Print Assumptions`, Lean `#print axioms` + `getModuleIdxFor?`, Agda `--safe --without-K`)
+|*Workflow & antipattern tests* |2 |`tests/workflows/validate_workflows_test.sh` (29 workflows) + `tests/rsr_antipattern_heading_test.sh`
+|*Aspect & structural gates* |4 |`tests/aspect_tests.sh`, `scripts/validate-template.sh`, `scripts/check-coordination-boundary.sh`, `scripts/check-pipeline-drift.sh`
+|*E2E & benchmark harnesses* |2 |`tests/e2e/template_instantiation_test.sh` + `benches/template_bench.sh`
 |===
 
-=== Completed Work (CRG C - Testing & Benchmarking)
-
-==== Template Validation Script ✅
-
-* [x] `+scripts/validate-template.sh+` — 8-phase validation
-** Phase 1: Core repository structure (root files, directories)
-** Phase 2: Machine-readable metadata (.machine_readable/)
-** Phase 3: GitHub Actions workflows (17 required + all present)
-** Phase 4: Idris2 ABI and Zig FFI source files
-** Phase 5: Placeholder token replacement (skipped in template)
-** Phase 6: SPDX license headers (100% coverage, 6/6 files)
-** Phase 7: Build system verification (zig build + idris2 syntax check)
-** Phase 8: Documentation requirements (TOPOLOGY, ABI-FFI-README, etc)
-* Status: *PASSING* (0 errors, 3 warnings about template placeholders)
-
-==== E2E Template Instantiation Test ✅
-
-* [x] `+tests/e2e/template_instantiation_test.sh+` — full workflow
-** Clones template to temp directory
-** Replaces all \{\{PLACEHOLDER}} tokens with test values
-** Validates resulting structure with scripts/validate-template.sh
-** Verifies Zig build works after instantiation
-** Checks no remaining placeholders
-** Cleans up temp directory
-* Status: *READY TO TEST* (can be verified by CI)
-
-==== Workflow Validation Test ✅
-
-* [x] `+tests/workflows/validate_workflows_test.sh+`
-** Validates all 21 workflows exist and have proper structure
-** Checks SPDX headers, '`name`' field
-** Verifies all 15 required workflows present
-* Status: *PASSING* (0 errors, 15/15 required workflows found)
-
-==== Zig FFI Tests ✅
-
-* [x] `+src/interface/ffi/test/integration_test.zig+` — template with
-examples
-** Converted from nextgen_typing placeholders to "`template`" namespace
-** Added comprehensive comments for how to instantiate
-** Tests grouped by category (lifecycle, operations, strings, errors,
-version, memory safety, threading)
-** Compiles and passes placeholder test
-* Status: *PASSING* (1 test: placeholder_test_implementation_required
-passes)
-
-==== Benchmarks ✅
-
-* [x] `+benches/template_bench.sh+` — 5 benchmark suites
-** Validation script: ~5.8s average (3 runs)
-** Zig build: ~19ms (clean build)
-** Zig tests: ~20ms
-** Workflow validation: ~117ms
-** Template instantiation: ~427ms
-* Formats: human, json, csv
-* Status: *PASSING* (all benchmarks execute)
-
-==== Build System ✅
-
-* [x] `+src/interface/ffi/build.zig+` — updated for Zig 0.15.2
-** Simplified to test-only configuration
-** Supports both unit tests and integration tests
-** Works with `+zig build+` without errors
-* Status: *PASSING* (builds successfully)
-
-=== Test Results Summary
-
-....
-Validation Script:    PASS (0 errors, 3 warnings)
-Workflow Validation:  PASS (21/21 workflows valid)
-Integration Tests:    PASS (1/1 placeholder test)
-E2E Instantiation:    READY (needs CI confirmation)
-Benchmarks:           PASS (5/5 benchmark suites)
-Build System:         PASS (zig build succeeds)
-....
-
-=== CRG C Compliance
-
-* *Coverage*: 6/6 test categories (unit, integration, E2E, workflow,
-validation, benchmarks)
-* *Documentation*: All test files have SPDX headers + inline
-documentation
-* *Author Attribution*: Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk
-* *License*: MPL-2.0 on all new files
-* *Automation*: All scripts executable + working
-
-=== FLAGGED ISSUES - ALL RESOLVED
-
-* [line-through]#*Template repo used by ALL new repos has 0 validation
-tests*# → FIXED: 4 test suites + validation script
-* [line-through]#*fuzz/placeholder.txt*# → FIXED: replaced with
-README.adoc containing real harness instructions
-* [line-through]#*No E2E tests for template instantiation*# → FIXED:
-full E2E test suite
-* [line-through]#*Zig FFI integration tests are placeholders*# → FIXED:
-converted to documented template format
-
-=== Next Steps (Future Sessions)
-
-* [ ] Integrate test scripts into CI/CD workflows
-* [ ] Generate test coverage reports
-* [ ] Add more specialized benchmarks (memory, threading stress)
-* [ ] Document test instantiation patterns for new repos
-
-=== Priority: P0 (COMPLETE) ✅
+== Verification Commands
+
+[source,bash]
+----
+bash scripts/validate-template.sh .
+bash scripts/check-coordination-boundary.sh
+bash scripts/check-pipeline-drift.sh .
+bash scripts/check-proof-enrolment.sh
+bash scripts/check-proof-ledger.sh
+bash tests/aspect_tests.sh
+bash tests/workflows/validate_workflows_test.sh
+bash tests/rsr_antipattern_heading_test.sh
+bash tests/proofs/run-ledger-controls.sh
+# When coqc/coqchk, lean, and agda are installed (executed in Proof CI):
+bash tests/proofs/run-kernel-assumption-controls.sh
+----
diff --git a/benches/template_bench.sh b/benches/template_bench.sh
index 5fb58a8..492842e 100755
--- a/benches/template_bench.sh
+++ b/benches/template_bench.sh
@@ -2,226 +2,81 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# Template Benchmarks
-# Measures performance characteristics of template validation and build system
+# Coordinator Gate Benchmarks
+# Measures execution times of nextgen-typing validation, boundary, drift, and ledger gates.
 
 set -euo pipefail
 
 REPO_ROOT="${1:-.}"
 OUTPUT_FORMAT="${2:-human}"  # human | json | csv
 
-# ANSI colors
 BLUE='\033[0;34m'
 GREEN='\033[0;32m'
-YELLOW='\033[1;33m'
-NC='\033[0m' # No Color
+NC='\033[0m'
 
-log_info() {
-    echo -e "${BLUE}→${NC} $*"
-}
-
-log_pass() {
-    echo -e "${GREEN}✓${NC} $*"
-}
-
-# Ensure we have required commands
-command -v /usr/bin/time >/dev/null 2>&1 || {
-    echo "Warning: /usr/bin/time not available, using built-in time"
-    TIME_CMD="time"
-}
-
-TIME_CMD="/usr/bin/time -f %e" 2>/dev/null || TIME_CMD="time"
-
-echo ""
-echo "═══════════════════════════════════════════════════════════════════════════════"
-echo "Template Benchmarks"
-echo "═══════════════════════════════════════════════════════════════════════════════"
-echo ""
+log_info() { echo -e "${BLUE}→${NC} $*"; }
+log_pass() { echo -e "${GREEN}✓${NC} $*"; }
 
 declare -A results
 
-#==============================================================================
-# BENCHMARK 1: Template Validation
-#==============================================================================
-
-log_info "Running template validation benchmark"
-
-# Warm-up run
-if [ -f "$REPO_ROOT/scripts/validate-template.sh" ]; then
-    bash "$REPO_ROOT/scripts/validate-template.sh" "$REPO_ROOT" 0 > /dev/null 2>&1 || true
-fi
-
-# Timed runs
-BENCH_RUNS=3
-TOTAL_TIME=0
-
-for i in $(seq 1 $BENCH_RUNS); do
-    START=$(date +%s%N)
-    bash "$REPO_ROOT/scripts/validate-template.sh" "$REPO_ROOT" 0 > /dev/null 2>&1 || true
-    END=$(date +%s%N)
-
-    # Convert to milliseconds
-    RUN_TIME=$(( (END - START) / 1000000 ))
-    TOTAL_TIME=$(( TOTAL_TIME + RUN_TIME ))
-
-    [ "$OUTPUT_FORMAT" = "human" ] && echo "  Run $i: ${RUN_TIME}ms"
-done
-
-AVG_VALIDATION_TIME=$(( TOTAL_TIME / BENCH_RUNS ))
-results[validation]=$AVG_VALIDATION_TIME
-log_pass "Validation: ${AVG_VALIDATION_TIME}ms average (${BENCH_RUNS} runs)"
-
-#==============================================================================
-# BENCHMARK 2: Zig Build
-#==============================================================================
-
-log_info "Running Zig build benchmark"
-
-if ! command -v zig &> /dev/null; then
-    echo "  ⚠ Zig compiler not found - skipping Zig build benchmark"
-    results[zig_build]="skipped"
-else
-    cd "$REPO_ROOT/src/interface/ffi"
-
-    # Warm-up
-    zig build --summary off > /dev/null 2>&1 || true
-
-    # Clean build
-    BENCH_RUNS=2
-    TOTAL_TIME=0
-
-    for i in $(seq 1 $BENCH_RUNS); do
-        rm -rf zig-cache
-
-        START=$(date +%s%N)
-        zig build --summary off > /dev/null 2>&1 || true
-        END=$(date +%s%N)
-
-        RUN_TIME=$(( (END - START) / 1000000 ))
-        TOTAL_TIME=$(( TOTAL_TIME + RUN_TIME ))
-
-        [ "$OUTPUT_FORMAT" = "human" ] && echo "  Run $i: ${RUN_TIME}ms"
+# Run the command after a warm-up, then store the mean of three timed runs
+# in milliseconds under $1 in results. $2 is the display label; the remaining
+# arguments form the command. Command output is suppressed, but its side effects
+# occur on every run. A failed command aborts the script under set -e.
+run_bench() {
+    local key="$1"
+    local label="$2"
+    shift 2
+    log_info "Benchmarking $label"
+    "$@" >/dev/null 2>&1
+    local runs=3
+    local total=0
+    for i in $(seq 1 "$runs"); do
+        local start end ms
+        start=$(date +%s%N)
+        "$@" >/dev/null 2>&1
+        end=$(date +%s%N)
+        ms=$(( (end - start) / 1000000 ))
+        total=$(( total + ms ))
+        [[ "$OUTPUT_FORMAT" == "human" ]] && echo "  Run $i: ${ms}ms"
     done
-
-    AVG_BUILD_TIME=$(( TOTAL_TIME / BENCH_RUNS ))
-    results[zig_build]=$AVG_BUILD_TIME
-    log_pass "Zig build: ${AVG_BUILD_TIME}ms average (clean build, ${BENCH_RUNS} runs)"
-
-    cd - > /dev/null
-fi
-
-#==============================================================================
-# BENCHMARK 3: Zig Tests
-#==============================================================================
-
-log_info "Running Zig test benchmark"
-
-if ! command -v zig &> /dev/null; then
-    echo "  ⚠ Zig compiler not found - skipping Zig test benchmark"
-    results[zig_test]="skipped"
-else
-    cd "$REPO_ROOT/src/interface/ffi"
-
-    # Warm-up
-    zig build test --summary off > /dev/null 2>&1 || true
-
-    START=$(date +%s%N)
-    TEST_OUTPUT=$(zig build test --summary off 2>&1 || true)
-    END=$(date +%s%N)
-
-    TEST_TIME=$(( (END - START) / 1000000 ))
-    results[zig_test]=$TEST_TIME
-    log_pass "Zig tests: ${TEST_TIME}ms"
-
-    # Count tests
-    TEST_COUNT=$(echo "$TEST_OUTPUT" | grep -c "^test " || echo "unknown")
-    echo "  Test count: $TEST_COUNT"
-
-    cd - > /dev/null
-fi
-
-#==============================================================================
-# BENCHMARK 4: Workflow Validation
-#==============================================================================
-
-log_info "Running workflow validation benchmark"
-
-if [ -f "$REPO_ROOT/tests/workflows/validate_workflows_test.sh" ]; then
-    START=$(date +%s%N)
-    bash "$REPO_ROOT/tests/workflows/validate_workflows_test.sh" "$REPO_ROOT/.github/workflows" > /dev/null 2>&1 || true
-    END=$(date +%s%N)
-
-    WORKFLOW_TIME=$(( (END - START) / 1000000 ))
-    results[workflow_validation]=$WORKFLOW_TIME
-    log_pass "Workflow validation: ${WORKFLOW_TIME}ms"
-fi
-
-#==============================================================================
-# BENCHMARK 5: Template Instantiation
-#==============================================================================
-
-log_info "Running template instantiation benchmark"
-
-if [ -f "$REPO_ROOT/tests/e2e/template_instantiation_test.sh" ]; then
-    START=$(date +%s%N)
-    bash "$REPO_ROOT/tests/e2e/template_instantiation_test.sh" "$REPO_ROOT" > /dev/null 2>&1 || true
-    END=$(date +%s%N)
-
-    INSTANTIATION_TIME=$(( (END - START) / 1000000 ))
-    results[instantiation]=$INSTANTIATION_TIME
-    log_pass "Template instantiation: ${INSTANTIATION_TIME}ms"
-fi
-
-#==============================================================================
-# SUMMARY
-#==============================================================================
+    local avg=$(( total / runs ))
+    results["$key"]=$avg
+    log_pass "$label: ${avg}ms average (${runs} runs)"
+}
 
 echo ""
 echo "═══════════════════════════════════════════════════════════════════════════════"
-echo "BENCHMARK RESULTS"
+echo "nextgen-typing Coordinator Gate Benchmarks"
 echo "═══════════════════════════════════════════════════════════════════════════════"
 echo ""
 
-if [ "$OUTPUT_FORMAT" = "json" ]; then
-    echo "{"
-    echo "  \"timestamp\": \"$(date -u +%Y-%m-%dT%H:%M:%SZ)\","
-    echo "  \"repo\": \"$REPO_ROOT\","
-    echo "  \"results\": {"
-
-    count=0
-    for key in "${!results[@]}"; do
-        value="${results[$key]}"
-        [ $count -gt 0 ] && echo ","
-        if [ "$value" = "skipped" ]; then
-            echo -n "    \"$key\": \"skipped\""
-        else
-            echo -n "    \"$key\": $value"
-        fi
-        count=$((count + 1))
-    done
-    echo ""
-    echo "  }"
-    echo "}"
-elif [ "$OUTPUT_FORMAT" = "csv" ]; then
-    echo "metric,value_ms,timestamp"
-    for key in "${!results[@]}"; do
-        value="${results[$key]}"
-        if [ "$value" != "skipped" ]; then
-            echo "$key,$value,$(date -u +%Y-%m-%dT%H:%M:%SZ)"
-        fi
-    done
-else
-    # Human-readable format
-    for key in "${!results[@]}"; do
-        value="${results[$key]}"
-        if [ "$value" = "skipped" ]; then
-            printf "  %-30s %s\n" "$key:" "SKIPPED"
-        else
-            printf "  %-30s %5d ms\n" "$key:" "$value"
-        fi
-    done
-fi
-
-echo ""
-echo "Benchmark complete."
-echo ""
+run_bench "validation" "Structure validation" bash "$REPO_ROOT/scripts/validate-template.sh" "$REPO_ROOT" 0
+run_bench "boundary" "Coordination boundary" bash "$REPO_ROOT/scripts/check-coordination-boundary.sh"
+run_bench "ledger" "Proof ledger audit" bash "$REPO_ROOT/scripts/check-proof-ledger.sh"
+run_bench "workflows" "Workflow validation" bash "$REPO_ROOT/tests/workflows/validate_workflows_test.sh" "$REPO_ROOT/.github/workflows"
+
+case "$OUTPUT_FORMAT" in
+    json)
+        cat <<EOF
+{
+  "timestamp": "$(date -u +%Y-%m-%dT%H:%M:%SZ)",
+  "benchmarks": {
+    "validation_ms": ${results[validation]},
+    "boundary_ms": ${results[boundary]},
+    "ledger_ms": ${results[ledger]},
+    "workflows_ms": ${results[workflows]}
+  }
+}
+EOF
+        ;;
+    csv)
+        echo "benchmark,time_ms"
+        echo "validation,${results[validation]}"
+        echo "boundary,${results[boundary]}"
+        echo "ledger,${results[ledger]}"
+        echo "workflows,${results[workflows]}"
+        ;;
+    human|*)
+        ;;
+esac
diff --git a/container/.gatekeeper.yaml b/container/.gatekeeper.yaml
deleted file mode 100644
index 9c632e6..0000000
--- a/container/.gatekeeper.yaml
+++ /dev/null
@@ -1,122 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
-#
-# Svalinn gatekeeper policy for nextgen-typing — Type Theory Pipeline
-#
-# Controls which operations are permitted through the edge gateway.
-# This template provides moderate security defaults — not wide-open test
-# mode, but not production-hardened either. Tighten the values below
-# before deploying to production.
-#
-# See: stapeln/container-stack/svalinn/
-
-version: "1.0"
-
-# ============================================================================
-# Authentication
-# ============================================================================
-#
-# Define which endpoints require authentication and at what level.
-
-auth:
-  # Public endpoints — no authentication required.
-  # Health and readiness probes must always be public so that
-  # orchestrators (selur, Podman, k8s) can check service status.
-  public:
-    - path: "/health"
-      methods: ["GET"]
-    - path: "/ready"
-      methods: ["GET"]
-    - path: "/metrics"
-      methods: ["GET"]
-
-  # Endpoints requiring JWT or OAuth2 authentication.
-  # Svalinn validates the token before forwarding the request.
-  authenticated:
-    - path: "/api/v1/*"
-      methods: ["GET", "POST", "PUT", "DELETE"]
-
-# ============================================================================
-# Rate Limiting
-# ============================================================================
-#
-# Protects backend services from overload. Values here are moderate
-# defaults — adjust based on your service capacity.
-
-rate_limits:
-  # Global limit: applied to all authenticated clients.
-  global:
-    requests_per_second: 500
-    burst: 1000
-
-  # Write operations: stricter limit to protect data stores.
-  writes:
-    paths: ["/api/v1/*"]
-    methods: ["POST", "PUT", "DELETE"]
-    requests_per_second: 100
-    burst: 200
-
-# ============================================================================
-# Container Trust
-# ============================================================================
-#
-# Svalinn verifies that all .ctp bundles in the stack are signed by
-# trusted keys and carry the required attestations.
-
-trust:
-  # Only accept .ctp bundles signed by these keys.
-  trusted_signers:
-    - key_id: "{{SERVICE_NAME}}-release"
-      algorithm: "Ed25519"
-      public_key_file: "/etc/svalinn/keys/{{SERVICE_NAME}}-release.pub"
-
-  # Require these attestations on all .ctp bundles.
-  required_attestations:
-    - "source-signature"
-    - "sbom-complete"
-
-  # Reject unsigned or untrusted images.
-  reject_unsigned: true
-
-# ============================================================================
-# Request Validation
-# ============================================================================
-#
-# Input validation at the gateway layer — catches malformed requests
-# before they reach the application.
-
-validation:
-  # Maximum request body size.
-  max_body_size: "8MB"
-
-  # Reject requests with NaN or Infinity in numeric fields.
-  reject_nan_inf: true
-
-  # Maximum result limit per list/search query.
-  max_result_limit: 500
-
-# ============================================================================
-# CORS
-# ============================================================================
-#
-# Cross-Origin Resource Sharing policy. The defaults below allow all
-# origins — restrict to your frontend domain(s) in production.
-
-cors:
-  allow_origins: ["*"]
-  allow_methods: ["GET", "POST", "PUT", "DELETE", "OPTIONS"]
-  allow_headers: ["Content-Type", "Authorization"]
-  max_age: 3600
-
-# ============================================================================
-# Logging
-# ============================================================================
-#
-# Structured logging for svalinn itself. Audit paths log all requests
-# (including body hashes) for post-incident investigation.
-
-logging:
-  format: "json"
-  level: "info"
-  # Log all write operations for audit trail.
-  audit_paths:
-    - "/api/v1/*"
diff --git a/container/0.1-AI-MANIFEST.a2ml b/container/0.1-AI-MANIFEST.a2ml
deleted file mode 100644
index ccb5bc5..0000000
--- a/container/0.1-AI-MANIFEST.a2ml
+++ /dev/null
@@ -1,143 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
----
-### [META]
-id: "container-templates"
-version: "1.0.0"
-context:
-  - "https://a2ml.org/ns/v2"
-  - "https://stapeln.dev/ns/v1"
-
----
-### [AI_MANIFEST]
-description: |
-  Container templates for the stapeln container ecosystem. This directory
-  provides Podman-Chainguard-stapeln templates that are customised via
-  `just container-init` or `just init` during project bootstrap.
-
-  All files use {{PLACEHOLDER}} tokens that are substituted with project-
-  specific values during initialisation.
-
-purpose: |
-  Provide a complete, security-first container deployment story for any
-  RSR-compliant repository. The templates cover the full lifecycle:
-  build, sign, verify, deploy, monitor, and govern.
-
-canonical_locations:
-  compose: "container/compose.toml"
-  containerfile: "container/Containerfile"
-  manifest: "container/manifest.toml"
-  gatekeeper: "container/.gatekeeper.yaml"
-  build_pipeline: "container/ct-build.sh"
-  entrypoint: "container/entrypoint.sh"
-  monitoring: "container/vordr.toml"
-  deployment: "container/deploy.k9.ncl"
-  example: "container/compose.example.toml"
-
----
-### [FILE_RELATIONSHIPS]
-files:
-  - name: "compose.toml"
-    role: "Orchestration"
-    description: |
-      selur-compose stack definition. Declares services, volumes, networks,
-      and health checks. References the Containerfile for image builds and
-      .gatekeeper.yaml for svalinn policy.
-    depends_on: ["Containerfile", ".gatekeeper.yaml"]
-
-  - name: "Containerfile"
-    role: "Image Build"
-    description: |
-      Multi-stage OCI container build. Stage 1 compiles the application on
-      wolfi-base; Stage 2 copies the binary into a minimal runtime image.
-      Copies entrypoint.sh, .gatekeeper.yaml, and manifest.toml into the
-      final image.
-    depends_on: ["entrypoint.sh", ".gatekeeper.yaml", "manifest.toml"]
-
-  - name: "manifest.toml"
-    role: "Bundle Metadata"
-    description: |
-      Cerro-torre .ctp bundle manifest. Describes provenance, dependencies,
-      attestations, and runtime security profile. Used by `ct pack` and
-      `ct verify`.
-    depends_on: []
-
-  - name: ".gatekeeper.yaml"
-    role: "Gateway Policy"
-    description: |
-      Svalinn edge gateway policy. Controls authentication, rate limiting,
-      container trust, request validation, CORS, and audit logging.
-    depends_on: []
-
-  - name: "ct-build.sh"
-    role: "Build Pipeline"
-    description: |
-      Shell script implementing the 5-stage pipeline: build (Podman),
-      pack (cerro-torre .ctp), sign (Ed25519), verify, push (optional).
-      Degrades gracefully when cerro-torre tools are not installed.
-    depends_on: ["Containerfile", "manifest.toml"]
-
-  - name: "entrypoint.sh"
-    role: "Container Entrypoint"
-    description: |
-      Startup script with signal handling (SIGTERM, SIGINT), logging, and
-      exec into the main application process.
-    depends_on: []
-
-  - name: "vordr.toml"
-    role: "Runtime Monitoring"
-    description: |
-      Vordr monitoring configuration. Health endpoint probing, crash
-      detection, resource thresholds, and structured log output.
-    depends_on: []
-
-  - name: "deploy.k9.ncl"
-    role: "Deployment Component"
-    description: |
-      k9-svc deployment specification at Hunt trust level. Full pedigree
-      (L1-L5), environment configs, container config, and rolling
-      deployment strategy.
-    depends_on: ["compose.toml", "ct-build.sh"]
-
-  - name: "compose.example.toml"
-    role: "Example"
-    description: |
-      Fully-commented multi-service example (Rust API + Elixir worker +
-      svalinn gateway). Copy to compose.toml and customise.
-    depends_on: []
-
----
-### [STAPELN_ECOSYSTEM]
-overview: |
-  The stapeln container ecosystem comprises six tools:
-
-  selur       — Container orchestration with zero-copy IPC. Reads compose.toml.
-  cerro-torre — Verified container packaging (.ctp bundles), Ed25519 signing.
-  svalinn     — Policy-driven edge gateway (auth, rate limits, CORS, trust).
-  vordr       — Runtime monitoring (health, crashes, resources, logs).
-  rokur       — Secrets management (runtime injection, no baked secrets).
-  k9-svc      — Nickel deployment components (Kennel/Yard/Hunt trust levels).
-
-invariants:
-  - "Base images MUST be cgr.dev/chainguard/wolfi-base or cgr.dev/chainguard/static"
-  - "Container runtime is Podman — never Docker"
-  - "Containerfile — never Dockerfile"
-  - "All images run as non-root (appuser or project-specific user)"
-  - ".ctp bundles are signed with Ed25519 via cerro-torre"
-  - "Health endpoints (/health, /ready) must always be public (no auth)"
-
----
-### [USAGE]
-initialisation: |
-  Run `just container-init` to substitute all {{PLACEHOLDER}} tokens with
-  project-specific values. This is also run as part of `just init`.
-
-development: |
-  1. `just container-build`   — Build the container image
-  2. `just container-verify`  — Verify compose configuration
-  3. `just container-up`      — Start the stack locally
-  4. `just container-down`    — Stop the stack
-
-production: |
-  1. `just container-sign`    — Build, sign, verify .ctp bundle
-  2. `just container-push`    — Push signed bundle to registry
-  3. `selur-compose up`       — Deploy on target host
diff --git a/container/Containerfile b/container/Containerfile
deleted file mode 100644
index fb0e715..0000000
--- a/container/Containerfile
+++ /dev/null
@@ -1,136 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
-# nextgen-typing — Type Theory Pipeline Container Image
-#
-# Multi-stage build template for Chainguard Wolfi base images.
-# Customise the builder stage for your language and copy the
-# resulting binary/release into the minimal runtime stage.
-#
-# Build with Podman:
-#   podman build -t {{SERVICE_NAME}}:latest -f container/Containerfile .
-#
-# Run:
-#   podman run -p {{PORT}}:{{PORT}} {{SERVICE_NAME}}:latest
-#
-# Run with persistent volume:
-#   podman run -p {{PORT}}:{{PORT}} -v {{SERVICE_NAME}}-data:/data {{SERVICE_NAME}}:latest
-
-# ============================================================================
-# Stage 1: Builder
-# ============================================================================
-#
-# Install build tools and compile the application.
-# This stage is discarded after the build — only the compiled output
-# is copied into the runtime stage.
-#
-# Language-specific examples (uncomment the one you need):
-#
-# --- Rust ---
-#   RUN apk add --no-cache rust pkgconf build-base
-#   COPY Cargo.toml Cargo.lock ./
-#   COPY src/ ./src/
-#   RUN cargo build --release
-#   # Output: /build/target/release/{{SERVICE_NAME}}
-#
-# --- Elixir ---
-#   RUN apk add --no-cache erl27-elixir-1.18 erlang-27 erlang-27-dev git build-base
-#   COPY mix.exs mix.lock ./
-#   COPY lib/ ./lib/
-#   COPY config/ ./config/
-#   ENV MIX_ENV=prod
-#   RUN mix local.hex --force && mix local.rebar --force && \
-#       mix deps.get --only prod && mix compile && mix release
-#   # Output: /build/_build/prod/rel/{{SERVICE_NAME}}/
-#
-# --- Zig ---
-#   RUN apk add --no-cache zig build-base
-#   COPY build.zig build.zig.zon ./
-#   COPY src/ ./src/
-#   RUN zig build -Doptimize=ReleaseFast
-#   # Output: /build/zig-out/bin/{{SERVICE_NAME}}
-#
-FROM cgr.dev/chainguard/wolfi-base:latest AS builder
-
-# TODO: Install your language toolchain
-RUN apk add --no-cache build-base
-
-WORKDIR /build
-
-# TODO: Copy source files and build
-COPY . .
-# RUN <your-build-command>
-
-# ============================================================================
-# Stage 2: Runtime
-# ============================================================================
-#
-# Minimal production image. Only the compiled binary/release and runtime
-# dependencies are included. No compilers, no source code, no build tools.
-#
-FROM cgr.dev/chainguard/wolfi-base:latest
-
-# OCI image labels (compatible with cerro-torre .ctp bundle metadata)
-LABEL org.opencontainers.image.title="nextgen-typing — Type Theory Pipeline" \
-      org.opencontainers.image.description="{{PROJECT_DESCRIPTION}}" \
-      org.opencontainers.image.url="https://github.com/hyperpolymath/nextgen-typing" \
-      org.opencontainers.image.source="https://github.com/hyperpolymath/nextgen-typing" \
-      org.opencontainers.image.vendor="hyperpolymath" \
-      org.opencontainers.image.licenses="{{LICENSE}}" \
-      org.opencontainers.image.authors="Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>" \
-      dev.cerrotorre.manifest="container/manifest.toml" \
-      dev.cerrotorre.gatekeeper="container/.gatekeeper.yaml" \
-      dev.stapeln.compose="container/compose.toml"
-
-# Install minimal runtime dependencies.
-# Adjust this list for your application:
-#   - ca-certificates: TLS root certificates
-#   - curl: health check probe
-#   - libstdc++: C++ standard library (if needed by native deps)
-#   - ncurses: terminal UI (if needed, e.g. Elixir IEx)
-RUN apk add --no-cache ca-certificates curl
-
-# Create non-root user for the application.
-# Running as root inside containers is a security anti-pattern.
-RUN addgroup -S appuser && adduser -S appuser -G appuser
-
-WORKDIR /app
-
-# TODO: Copy compiled binary/release from builder stage.
-# Examples:
-#   COPY --from=builder /build/target/release/{{SERVICE_NAME}} /app/{{SERVICE_NAME}}
-#   COPY --from=builder /build/_build/prod/rel/{{SERVICE_NAME}} /app/release/
-#   COPY --from=builder /build/zig-out/bin/{{SERVICE_NAME}} /app/{{SERVICE_NAME}}
-
-# Copy entrypoint script
-COPY container/entrypoint.sh /app/entrypoint.sh
-RUN chmod +x /app/entrypoint.sh
-
-# Copy stapeln integration files (svalinn gatekeeper policy, cerro-torre manifest)
-COPY container/.gatekeeper.yaml /etc/svalinn/gatekeeper.yaml
-COPY container/manifest.toml /app/manifest.toml
-
-# Create data directory for persistent storage (mountable volume)
-RUN mkdir -p /data && chown appuser:appuser /data
-
-# Set ownership of the application directory
-RUN chown -R appuser:appuser /app
-
-# Environment variables — customise for your application
-ENV APP_HOST=[::]
-ENV APP_PORT={{PORT}}
-ENV APP_LOG_FORMAT=json
-ENV APP_DATA_DIR=/data
-
-# Declare /data as a volume for persistent storage
-VOLUME ["/data"]
-
-# Run as non-root
-USER appuser
-
-# Expose the application port
-EXPOSE {{PORT}}
-
-# Health check — the application must respond 2xx at /health
-HEALTHCHECK --interval=30s --timeout=5s --start-period=10s --retries=3 \
-    CMD curl -sf http://localhost:${APP_PORT}/health || exit 1
-
-ENTRYPOINT ["/app/entrypoint.sh"]
diff --git a/container/README.adoc b/container/README.adoc
deleted file mode 100644
index f0df143..0000000
--- a/container/README.adoc
+++ /dev/null
@@ -1,179 +0,0 @@
-// SPDX-License-Identifier: CC-BY-SA-4.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-= nextgen-typing Container Templates
-:toc: left
-:toclevels: 3
-:sectnums:
-
-== Overview
-
-This directory contains container templates for the
-https://github.com/hyperpolymath/stapeln[stapeln] container ecosystem.
-The stapeln stack provides verified container packaging, edge gateway
-policies, runtime monitoring, and supply-chain signing for Podman-based
-deployments using https://www.chainguard.dev/[Chainguard] Wolfi base images.
-
-All files use `{{PLACEHOLDER}}` tokens that are replaced by `just container-init`
-(or by the top-level `just init` during project bootstrap).
-
-== File Reference
-
-[cols="1,3"]
-|===
-| File | Purpose
-
-| `compose.toml`
-| **selur-compose** stack definition. Declares services, volumes, networks,
-  and health checks. The primary orchestration file for local and production
-  deployment. Use `selur-compose up` or fall back to `podman compose`.
-
-| `compose.example.toml`
-| Concrete multi-service example with detailed comments. Copy and customise
-  for your own stack. Not used directly by any tooling.
-
-| `Containerfile`
-| Multi-stage OCI container build specification. Stage 1 builds the
-  application; Stage 2 produces a minimal runtime image on
-  `cgr.dev/chainguard/wolfi-base`. Uses Podman (never Docker).
-
-| `manifest.toml`
-| **cerro-torre** bundle metadata. Describes the `.ctp` verified container
-  package: provenance, dependencies, attestations, and runtime security
-  profile. Used by `ct pack` and `ct verify`.
-
-| `.gatekeeper.yaml`
-| **svalinn** edge gateway policy. Controls authentication, rate limiting,
-  container trust, request validation, CORS, and audit logging at the
-  network boundary.
-
-| `ct-build.sh`
-| Build, sign, and verify pipeline script. Five stages: build (Podman),
-  pack (cerro-torre `.ctp`), sign (Ed25519), verify, and push (optional).
-  Gracefully degrades when cerro-torre tools are not installed.
-
-| `entrypoint.sh`
-| Container entrypoint with signal handling (SIGTERM, SIGINT), startup
-  logging, and `exec` into the main application process.
-
-| `vordr.toml`
-| **vordr** runtime monitoring configuration. Defines health endpoints,
-  crash detection, resource thresholds, and log output.
-
-| `deploy.k9.ncl`
-| **k9-svc** deployment component at Hunt trust level. Full pedigree
-  (L1--L5), environment configs (dev/staging/prod), container
-  configuration, and rolling deployment strategy.
-
-| `0-AI-MANIFEST.a2ml`
-| AI-readable manifest describing the container directory, file
-  interconnections, and the stapeln ecosystem.
-|===
-
-== The stapeln Ecosystem
-
-The stapeln container ecosystem comprises six interconnected tools:
-
-**selur** (compose)::
-  Container orchestration with zero-copy IPC for co-located services.
-  Reads `compose.toml` files. Falls back to standard Podman Compose
-  when the selur driver is unavailable.
-
-**cerro-torre** (bundles and signing)::
-  Verified container packaging. Produces `.ctp` bundles from OCI images,
-  signs them with Ed25519, and verifies the full chain. Tools: `ct pack`,
-  `ct sign`, `ct verify`, `ct push`, `ct explain`.
-
-**svalinn** (edge gateway)::
-  Policy-driven reverse proxy. Enforces authentication, rate limiting,
-  CORS, and container trust policies defined in `.gatekeeper.yaml`.
-
-**vordr** (monitoring)::
-  Runtime container monitoring. Watches health endpoints, detects crashes,
-  tracks resource usage, and emits structured logs.
-
-**rokur** (secrets)::
-  Secrets management for container deployments. Injects secrets at runtime
-  without baking them into images. Currently a stub/placeholder.
-
-**k9-svc** (deployment components)::
-  Nickel-based deployment specification. Components declare their pedigree
-  (identity, target, security, validation, recipes) and execute at one of
-  three trust levels: Kennel (data only), Yard (evaluation), Hunt (full
-  execution with cryptographic handshake).
-
-== How to Initialise
-
-[source,bash]
-----
-# Option 1: During project bootstrap (includes all placeholders)
-just init
-
-# Option 2: Container-specific initialisation
-just container-init
-----
-
-The `container-init` recipe prompts for container-specific values
-(service name, port, registry) and substitutes all `{{PLACEHOLDER}}`
-tokens in the `container/` directory.
-
-== Development Workflow
-
-[source,bash]
-----
-# 1. Build the container image
-just container-build
-
-# 2. Verify the compose configuration
-just container-verify
-
-# 3. Start the stack locally
-just container-up --detach
-
-# 4. Check logs
-podman compose --file container/compose.toml logs -f
-
-# 5. Stop the stack
-just container-down
-----
-
-== Production Deployment
-
-[source,bash]
-----
-# 1. Build, sign, and verify the .ctp bundle
-just container-sign
-
-# 2. Push the signed bundle to the registry
-just container-push
-
-# 3. Deploy on the target host
-selur-compose up --detach
-----
-
-For k9-svc managed deployments:
-
-[source,bash]
-----
-# Validate the deployment component
-nickel typecheck container/deploy.k9.ncl
-
-# Deploy (requires Hunt-level authorisation)
-k9-svc deploy container/deploy.k9.ncl --env production
-----
-
-== Base Images
-
-All Containerfiles use Chainguard Wolfi base images:
-
-* **Builder stage:** `cgr.dev/chainguard/wolfi-base:latest`
-* **Runtime stage:** `cgr.dev/chainguard/wolfi-base:latest` (or
-  `cgr.dev/chainguard/static:latest` for statically-linked binaries)
-
-Chainguard images are minimal, CVE-free, and rebuilt daily. They use the
-`apk` package manager (Alpine-compatible).
-
-== Container Runtime
-
-This project uses **Podman** (never Docker). All scripts, compose files,
-and documentation reference Podman commands. The OCI Containerfile format
-is compatible with Podman, Docker, and nerdctl.
diff --git a/container/compose.example.toml b/container/compose.example.toml
deleted file mode 100644
index d8d717c..0000000
--- a/container/compose.example.toml
+++ /dev/null
@@ -1,135 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
-#
-# Example selur-compose configuration — multi-service stack
-#
-# This is a concrete, fully-commented example showing a Rust API + Elixir
-# worker + svalinn gateway deployment. Copy this file to compose.toml and
-# customise for your project.
-#
-# Usage:
-#   cp compose.example.toml compose.toml
-#   # Edit service names, ports, images
-#   selur-compose up --detach
-
-version = "1.0"
-
-# ============================================================================
-# Services
-# ============================================================================
-
-# Rust API service — the primary HTTP/gRPC backend.
-# Handles incoming requests, data storage, and core business logic.
-[services.rust-api]
-image = "ghcr.io/hyperpolymath/myproject-api:latest.ctp"
-
-# Map host port 8080 to container port 8080.
-# Use ["[::]:8080:8080"] for explicit IPv6 binding.
-ports = ["8080:8080"]
-
-# Environment variables passed into the container at startup.
-# These override defaults in the Containerfile ENV directives.
-environment = {
-  RUST_LOG = "info",                  # Rust log level (trace, debug, info, warn, error)
-  APP_HOST = "[::]",                  # Listen on all interfaces (IPv4 + IPv6)
-  APP_PORT = "8080",                  # Internal container port
-  APP_LOG_FORMAT = "json",            # Structured logging for selur/vordr
-  APP_DATA_DIR = "/data",             # Persistent data directory (matches VOLUME)
-}
-
-# Bind-mount a named volume for persistent data.
-# Format: "volume-name:/container/path"
-volumes = ["api-data:/data"]
-
-# Restart policy: "always" ensures the service comes back after crashes.
-# Other options: "no", "on-failure", "unless-stopped"
-restart = "always"
-
-# Health check: selur/Podman uses this to determine if the service is ready.
-# The service must respond 2xx to this endpoint within the timeout.
-healthcheck = { test = "curl -sf http://localhost:8080/health", interval = "30s", timeout = "5s", retries = 3 }
-
-# ---
-
-# Elixir worker service — background processing, event handling, coordination.
-# Runs as an OTP release with supervision trees for fault tolerance.
-[services.elixir-worker]
-image = "ghcr.io/hyperpolymath/myproject-worker:latest.ctp"
-
-# Separate port for the worker's admin/metrics endpoint.
-ports = ["4000:4000"]
-
-# The worker connects to the Rust API over the internal selur network.
-# Service names resolve as hostnames within the compose network.
-environment = {
-  API_URL = "http://rust-api:8080/api/v1",   # Internal service discovery
-  MIX_ENV = "prod",                           # Elixir release mode
-  APP_LOG_FORMAT = "json",                    # Match structured logging format
-  POOL_SIZE = "10",                           # DB connection pool size
-}
-
-# depends_on ensures the Rust API starts before the worker.
-# Note: This only waits for the container to start, not for the health check.
-# Use healthcheck + startup probes for true readiness gating.
-depends_on = ["rust-api"]
-
-restart = "always"
-healthcheck = { test = "curl -sf http://localhost:4000/health", interval = "30s", timeout = "5s", retries = 3 }
-
-# ---
-
-# Svalinn edge gateway — reverse proxy with policy enforcement.
-# All external traffic enters through svalinn, which:
-#   1. Terminates TLS (auto-provisioned certificates)
-#   2. Validates JWT/OAuth2 authentication
-#   3. Enforces rate limits from .gatekeeper.yaml
-#   4. Routes requests to the appropriate backend service
-#   5. Logs all write operations for audit
-[services.svalinn]
-image = "ghcr.io/hyperpolymath/svalinn:latest.ctp"
-
-# External-facing ports: HTTPS (443) and HTTP->HTTPS redirect (80).
-ports = ["443:443", "80:80"]
-
-environment = {
-  # Backend routing: svalinn proxies to internal services.
-  SVALINN_BACKEND = "http://rust-api:8080",
-  SVALINN_WORKER_BACKEND = "http://elixir-worker:4000",
-
-  # Policy file: mounted from the svalinn-config volume.
-  SVALINN_POLICY_FILE = "/etc/svalinn/gatekeeper.yaml",
-
-  # Auto-provision TLS certificates (Let's Encrypt).
-  SVALINN_TLS_AUTO = "true",
-}
-
-# Mount .gatekeeper.yaml as read-only policy configuration.
-volumes = ["svalinn-config:/etc/svalinn:ro"]
-
-# Svalinn starts last — it needs both backends to be running.
-depends_on = ["rust-api", "elixir-worker"]
-restart = "always"
-healthcheck = { test = "curl -sf http://localhost:80/health", interval = "30s", timeout = "5s", retries = 3 }
-
-# ============================================================================
-# Volumes
-# ============================================================================
-
-# Persistent storage for the Rust API (database files, indexes, WAL).
-[volumes.api-data]
-driver = "local"
-
-# Read-only policy configuration for svalinn gateway.
-# Populate with: cp .gatekeeper.yaml /path/to/svalinn-config/gatekeeper.yaml
-[volumes.svalinn-config]
-driver = "local"
-
-# ============================================================================
-# Networks
-# ============================================================================
-
-# selur network: zero-copy IPC between services on the same host.
-# When the selur driver is not installed, falls back to standard bridge
-# networking (TCP over localhost). Performance is slightly lower but
-# functionality is identical.
-[networks.default]
-driver = "selur"
diff --git a/container/compose.toml b/container/compose.toml
deleted file mode 100644
index de0e138..0000000
--- a/container/compose.toml
+++ /dev/null
@@ -1,70 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
-#
-# nextgen-typing selur-compose configuration
-#
-# Orchestrates the container stack as verified container bundles (.ctp).
-# Uses selur zero-copy IPC between services on the same host.
-#
-# Usage:
-#   selur-compose up                     # Start all services
-#   selur-compose up --detach            # Start in background
-#   selur-compose verify                 # Verify all .ctp signatures
-#   selur-compose ps                     # Check status
-#   selur-compose logs -f {{SERVICE_NAME}}  # Stream logs
-#   selur-compose down                   # Stop all services
-#
-# Fallback (when selur is not installed):
-#   podman compose --file compose.toml up --detach
-
-version = "1.0"
-
-# ============================================================================
-# Services
-# ============================================================================
-
-# Primary application service
-[services.{{SERVICE_NAME}}]
-image = "{{REGISTRY}}/{{SERVICE_NAME}}:latest.ctp"
-ports = ["{{PORT}}:{{PORT}}"]
-environment = {
-  APP_HOST = "[::]",
-  APP_PORT = "{{PORT}}",
-  APP_LOG_FORMAT = "json",
-  APP_DATA_DIR = "/data",
-}
-volumes = ["{{SERVICE_NAME}}-data:/data"]
-restart = "always"
-healthcheck = { test = "curl -sf http://localhost:{{PORT}}/health", interval = "30s", timeout = "5s", retries = 3 }
-
-# Svalinn edge gateway: validates requests, enforces policies, TLS termination
-[services.svalinn]
-image = "ghcr.io/hyperpolymath/svalinn:latest.ctp"
-ports = ["443:443", "80:80"]
-environment = {
-  SVALINN_BACKEND = "http://{{SERVICE_NAME}}:{{PORT}}",
-  SVALINN_POLICY_FILE = "/etc/svalinn/gatekeeper.yaml",
-  SVALINN_TLS_AUTO = "true",
-}
-volumes = ["svalinn-config:/etc/svalinn:ro"]
-depends_on = ["{{SERVICE_NAME}}"]
-restart = "always"
-healthcheck = { test = "curl -sf http://localhost:80/health", interval = "30s", timeout = "5s", retries = 3 }
-
-# ============================================================================
-# Volumes
-# ============================================================================
-
-[volumes.{{SERVICE_NAME}}-data]
-driver = "local"
-
-[volumes.svalinn-config]
-driver = "local"
-
-# ============================================================================
-# Networks
-# ============================================================================
-
-# Use selur zero-copy IPC for inter-service communication on the same host.
-# Falls back to standard bridge networking when selur driver is unavailable.
-[networks.default]
-driver = "selur"
diff --git a/container/ct-build.sh b/container/ct-build.sh
deleted file mode 100755
index 95d7410..0000000
--- a/container/ct-build.sh
+++ /dev/null
@@ -1,162 +0,0 @@
-#!/usr/bin/env bash
-# SPDX-License-Identifier: MPL-2.0
-#
-# nextgen-typing — Cerro Torre build, sign, and verify pipeline
-#
-# Builds the container image, packages it as a verified .ctp bundle,
-# signs it with Ed25519, and verifies the result. Gracefully degrades
-# when cerro-torre tools are not installed.
-#
-# Prerequisites:
-#   - podman (container build — required)
-#   - ct (cerro-torre CLI: pack, sign, verify — optional)
-#   - cerro-sign (Ed25519 signing — optional, ct sign used as fallback)
-#
-# Usage:
-#   ./ct-build.sh                  # Build + sign (local only)
-#   ./ct-build.sh --push           # Build + sign + push to registry
-#   CT_KEY_ID=my-key ./ct-build.sh # Use specific signing key
-#
-# Environment variables:
-#   CT_KEY_ID       — Signing key identifier (default: {{SERVICE_NAME}}-release)
-#   CT_REGISTRY     — OCI registry to push to (default: {{REGISTRY}})
-#   CT_TAG          — Image tag (default: latest)
-
-set -euo pipefail
-
-# ---------------------------------------------------------------------------
-# Configuration
-# ---------------------------------------------------------------------------
-
-SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
-REPO_ROOT="$(cd "$SCRIPT_DIR/.." && pwd)"
-
-PUSH=""
-for arg in "$@"; do
-    if [ "$arg" = "--push" ]; then
-        PUSH="--push"
-    fi
-done
-
-CT_KEY_ID="${CT_KEY_ID:-{{SERVICE_NAME}}-release}"
-CT_REGISTRY="${CT_REGISTRY:-{{REGISTRY}}}"
-CT_TAG="${CT_TAG:-latest}"
-
-IMAGE_NAME="{{SERVICE_NAME}}"
-FULL_IMAGE="${CT_REGISTRY}/${IMAGE_NAME}:${CT_TAG}"
-CTP_FILE="${SCRIPT_DIR}/${IMAGE_NAME}-${CT_TAG}.ctp"
-
-echo "=== nextgen-typing Cerro Torre Build Pipeline ==="
-echo "  Image:  ${FULL_IMAGE}"
-echo "  Key:    ${CT_KEY_ID}"
-echo "  Bundle: ${CTP_FILE}"
-echo ""
-
-# ---------------------------------------------------------------------------
-# Step 1: Build container image with Podman
-# ---------------------------------------------------------------------------
-
-echo "--- Step 1: Building container image ---"
-
-podman build \
-    -t "${FULL_IMAGE}" \
-    -f "${SCRIPT_DIR}/Containerfile" \
-    "${REPO_ROOT}"
-
-echo "  Built: ${FULL_IMAGE}"
-echo ""
-
-# ---------------------------------------------------------------------------
-# Step 2: Pack into .ctp bundle
-# ---------------------------------------------------------------------------
-
-echo "--- Step 2: Packing into .ctp bundle ---"
-
-if command -v ct &>/dev/null; then
-    ct pack "${FULL_IMAGE}" -o "${CTP_FILE}"
-    echo "  Packed: ${CTP_FILE}"
-else
-    echo "  SKIP: ct not found (install cerro-torre CLI from stapeln/container-stack/cerro-torre)"
-    echo "  The container image is built and tagged but not packed as a .ctp bundle."
-    echo "  To pack manually: ct pack ${FULL_IMAGE} -o ${CTP_FILE}"
-    echo ""
-    if [ "$PUSH" = "--push" ]; then
-        echo "--- Pushing unsigned OCI image (no .ctp) ---"
-        podman push "${FULL_IMAGE}"
-        echo "  Pushed: ${FULL_IMAGE} (unsigned OCI — not a .ctp bundle)"
-    fi
-    echo ""
-    echo "=== Build complete (without .ctp signing) ==="
-    exit 0
-fi
-
-echo ""
-
-# ---------------------------------------------------------------------------
-# Step 3: Sign the .ctp bundle
-# ---------------------------------------------------------------------------
-
-echo "--- Step 3: Signing .ctp bundle ---"
-
-if command -v cerro-sign &>/dev/null; then
-    cerro-sign sign "${CTP_FILE}" --key-id "${CT_KEY_ID}"
-    echo "  Signed: ${CTP_FILE} (key: ${CT_KEY_ID})"
-elif command -v ct &>/dev/null; then
-    ct sign "${CTP_FILE}" --key "${CT_KEY_ID}"
-    echo "  Signed: ${CTP_FILE} (key: ${CT_KEY_ID})"
-else
-    echo "  SKIP: cerro-sign not found (install from stapeln/container-stack/cerro-torre)"
-fi
-
-echo ""
-
-# ---------------------------------------------------------------------------
-# Step 4: Verify the .ctp bundle
-# ---------------------------------------------------------------------------
-
-echo "--- Step 4: Verifying .ctp bundle ---"
-
-if command -v ct &>/dev/null; then
-    ct verify "${CTP_FILE}"
-    echo "  Verified: ${CTP_FILE}"
-else
-    echo "  SKIP: ct not found"
-fi
-
-echo ""
-
-# ---------------------------------------------------------------------------
-# Step 5: Push to registry (optional)
-# ---------------------------------------------------------------------------
-
-if [ "$PUSH" = "--push" ]; then
-    echo "--- Step 5: Pushing to registry ---"
-
-    if command -v ct &>/dev/null; then
-        ct push "${CTP_FILE}" "${FULL_IMAGE}"
-        echo "  Pushed: ${FULL_IMAGE}"
-    else
-        # Fall back to podman push (unsigned OCI image)
-        echo "  ct not available, falling back to podman push (unsigned)"
-        podman push "${FULL_IMAGE}"
-        echo "  Pushed: ${FULL_IMAGE} (unsigned OCI — not a .ctp bundle)"
-    fi
-    echo ""
-fi
-
-# ---------------------------------------------------------------------------
-# Summary
-# ---------------------------------------------------------------------------
-
-echo "=== Build pipeline complete ==="
-echo "  Image:  ${FULL_IMAGE}"
-echo "  Bundle: ${CTP_FILE}"
-echo ""
-echo "  To deploy with selur-compose:"
-echo "    cd container && selur-compose up"
-echo ""
-echo "  To verify at any time:"
-echo "    ct verify ${CTP_FILE}"
-echo ""
-echo "  To explain the verification chain:"
-echo "    ct explain ${CTP_FILE}"
diff --git a/container/deploy.k9.ncl b/container/deploy.k9.ncl
deleted file mode 100644
index 2020f71..0000000
--- a/container/deploy.k9.ncl
+++ /dev/null
@@ -1,188 +0,0 @@
-K9!
-# SPDX-License-Identifier: MPL-2.0
-# deploy.k9.ncl — nextgen-typing — Type Theory Pipeline deployment component (Hunt level)
-#
-# k9-svc deployment specification with full pedigree (L1-L5).
-# Security Level: 'Hunt (requires cryptographic handshake for execution).
-#
-# WARNING: This component can execute shell commands!
-# It requires explicit authorisation via the Leash system.
-#
-# Usage:
-#   nickel typecheck container/deploy.k9.ncl
-#   k9-svc validate container/deploy.k9.ncl
-#   k9-svc deploy container/deploy.k9.ncl --env production
-
-# The component's pedigree (self-description across five layers)
-let component_pedigree = {
-  # Top-level identity fields — duplicated from metadata so the K9
-  # validator (which inspects the literal `pedigree = { ... }` block
-  # at the toplevel of the file rather than the resolved Nickel value)
-  # can locate name / version / security_level without resolving the
-  # `component_pedigree` indirection.
-  name = "{{SERVICE_NAME}}-deploy",
-  version = "{{VERSION}}",
-
-  # ─────────────────────────────────────────────────────────────
-  # L1: The Snout — Identity
-  # ─────────────────────────────────────────────────────────────
-  metadata = {
-    name = "{{SERVICE_NAME}}-deploy",
-    version = "{{VERSION}}",
-    breed = "application/vnd.k9+nickel",
-    magic_number = "K9!",
-    description = "nextgen-typing — Type Theory Pipeline deployment component (Hunt level)",
-  },
-
-  # ─────────────────────────────────────────────────────────────
-  # L2: The Scent — Target Environment
-  # ─────────────────────────────────────────────────────────────
-  target = {
-    os = 'Linux,
-    is_edge = false,
-    requires_podman = true,
-    min_memory_mb = 256,
-  },
-
-  # ─────────────────────────────────────────────────────────────
-  # L3: The Leash — Security
-  # ─────────────────────────────────────────────────────────────
-  security = {
-    leash = 'Hunt,
-    trust_level = 'Hunt,
-    allow_network = true,
-    allow_filesystem_write = true,
-    allow_subprocess = true,
-    # In production, replace with a real Ed25519 signature.
-    signature = "PLACEHOLDER-SIGNATURE-REQUIRED-FOR-HUNT",
-  },
-
-  # ─────────────────────────────────────────────────────────────
-  # L4: The Gut — Self-Validation
-  # ─────────────────────────────────────────────────────────────
-  validation = {
-    checksum = "sha256:placeholder",
-    pedigree_version = "1.0.0",
-    hunt_authorized = false,  # Must be set true after handshake
-  },
-
-  # ─────────────────────────────────────────────────────────────
-  # L5: The Muscle — Deployment Recipes
-  # ─────────────────────────────────────────────────────────────
-  recipes = {
-    install = "just container-build",
-    validate = "just container-verify",
-    deploy = "just container-up",
-    migrate = "just container-build && just container-up",
-  },
-} in
-
-# Deployment configuration
-let deployment = {
-  # Target environments (dev / staging / production)
-  environments = {
-    dev = {
-      replicas = 1,
-      memory = "256Mi",
-      cpu = "100m",
-      image_tag = "dev",
-    },
-    staging = {
-      replicas = 2,
-      memory = "512Mi",
-      cpu = "250m",
-      image_tag = "staging",
-    },
-    production = {
-      replicas = 3,
-      memory = "1Gi",
-      cpu = "500m",
-      image_tag = "latest",
-    },
-  },
-
-  # Container configuration
-  container = {
-    image = "{{REGISTRY}}/{{SERVICE_NAME}}",
-    port = {{PORT}},
-    health_check = "/health",
-    readiness_check = "/ready",
-  },
-
-  # Deployment strategy
-  strategy = {
-    type = "rolling",
-    max_surge = 1,
-    max_unavailable = 0,
-  },
-} in
-
-# Deployment scripts (executed at Hunt level)
-let scripts = {
-  # Pre-deployment validation
-  pre_deploy = m%"
-#!/bin/sh
-set -eu
-echo "K9: Pre-deployment validation for {{SERVICE_NAME}}..."
-cd container && selur-compose verify || podman compose --file compose.toml config
-echo "K9: Validation passed."
-"%,
-
-  # Deployment script
-  deploy = m%"
-#!/bin/sh
-set -eu
-ENV="${1:-dev}"
-echo "K9: Deploying {{SERVICE_NAME}} to $ENV environment..."
-cd container
-./ct-build.sh
-selur-compose up --detach || podman compose --file compose.toml up --detach
-echo "K9: Deployment to $ENV complete."
-"%,
-
-  # Rollback script
-  rollback = m%"
-#!/bin/sh
-set -eu
-echo "K9: Rolling back {{SERVICE_NAME}} deployment..."
-cd container
-selur-compose down || podman compose --file compose.toml down
-echo "K9: Rollback complete."
-"%,
-} in
-
-# Export the component
-{
-  pedigree = {
-    # k9-validate scans for a literal `pedigree = { … }` field (it cannot
-    # follow the `let component_pedigree` indirection). This visible block
-    # carries the required identity/security fields; `& component_pedigree`
-    # then layers on the full L1–L5 component pedigree.
-    schema_version = "1.0.0",
-    component_type = "deployment",
-    security_level = "hunt",
-    metadata = {
-      name = "{{SERVICE_NAME}}-deploy",
-      version = "{{VERSION}}",
-    },
-  } & component_pedigree,
-  deployment = deployment,
-  scripts = scripts,
-
-  # Security check: this component requires Hunt level
-  required_level = 'Hunt,
-
-  # Warning for users
-  warning = m%"
-WARNING: This is a Hunt-level component.
-
-It can execute shell commands and modify your system.
-Before running, ensure you have:
-
-1. Reviewed the deployment scripts above
-2. Verified the signature (when implemented)
-3. Explicitly authorised Hunt-level execution
-
-Run with: k9-svc authorize container/deploy.k9.ncl && k9-svc deploy container/deploy.k9.ncl
-"%,
-}
diff --git a/container/entrypoint.sh b/container/entrypoint.sh
deleted file mode 100755
index 194a5c0..0000000
--- a/container/entrypoint.sh
+++ /dev/null
@@ -1,63 +0,0 @@
-#!/bin/sh
-# SPDX-License-Identifier: MPL-2.0
-# nextgen-typing container entrypoint
-#
-# Handles signal propagation, startup logging, and health check
-# preparation before exec-ing into the main application process.
-
-set -e
-
-# ---------------------------------------------------------------------------
-# Signal handling
-# ---------------------------------------------------------------------------
-#
-# Trap SIGTERM and SIGINT so that the application can shut down gracefully
-# when Podman sends stop signals (e.g. `podman stop`, `selur-compose down`).
-
-cleanup() {
-    echo "Received shutdown signal — stopping {{SERVICE_NAME}}..."
-    # If the main process is backgrounded, kill it here:
-    # kill "$MAIN_PID" 2>/dev/null || true
-    # wait "$MAIN_PID" 2>/dev/null || true
-    exit 0
-}
-trap cleanup TERM INT
-
-# ---------------------------------------------------------------------------
-# Startup logging
-# ---------------------------------------------------------------------------
-
-echo "Starting {{SERVICE_NAME}}..."
-echo "  Host: ${APP_HOST:-[::]}"
-echo "  Port: ${APP_PORT:-{{PORT}}}"
-echo "  Data: ${APP_DATA_DIR:-/data}"
-echo "  Log:  ${APP_LOG_FORMAT:-json}"
-
-# ---------------------------------------------------------------------------
-# Health check preparation
-# ---------------------------------------------------------------------------
-#
-# Ensure the data directory exists and is writable.
-# The VOLUME directive in the Containerfile creates /data, but a bind-mount
-# might replace it with an empty directory owned by root.
-
-if [ -d "${APP_DATA_DIR:-/data}" ]; then
-    if [ ! -w "${APP_DATA_DIR:-/data}" ]; then
-        echo "WARNING: ${APP_DATA_DIR:-/data} is not writable by $(whoami)"
-    fi
-fi
-
-# ---------------------------------------------------------------------------
-# Exec into main process
-# ---------------------------------------------------------------------------
-#
-# Replace the entrypoint shell with the application process so that
-# signals are delivered directly and PID 1 is the application.
-#
-# TODO: Replace the command below with your application binary.
-# Examples:
-#   exec /app/{{SERVICE_NAME}}
-#   exec /app/release/bin/{{SERVICE_NAME}} start
-#   exec /app/{{SERVICE_NAME}} serve --host "${APP_HOST}" --port "${APP_PORT}"
-
-exec "$@"
diff --git a/container/manifest.toml b/container/manifest.toml
deleted file mode 100644
index 6a2dd66..0000000
--- a/container/manifest.toml
+++ /dev/null
@@ -1,62 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
-#
-# Cerro Torre manifest for nextgen-typing .ctp bundle
-#
-# This manifest describes the container image for verified
-# container packaging. Used by `ct pack` to create .ctp bundles.
-
-[metadata]
-name = "{{SERVICE_NAME}}"
-version = "{{VERSION}}"
-revision = 1
-summary = "{{PROJECT_DESCRIPTION}}"
-description = """
-nextgen-typing — containerised service packaged as a verified
-cerro-torre .ctp bundle with Ed25519 signing and full provenance
-tracking.
-"""
-license = "{{LICENSE}}"
-homepage = "https://github.com/hyperpolymath/nextgen-typing"
-maintainer = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
-
-[provenance]
-upstream = "https://github.com/hyperpolymath/nextgen-typing"
-import_date = 2026-04-11T00:00:00Z
-
-[dependencies]
-runtime = ["ca-certificates", "curl"]
-build = []
-
-[build]
-system = "podman"
-
-[build.environment]
-APP_HOST = "[::]"
-APP_PORT = "{{PORT}}"
-
-[outputs]
-primary = "{{SERVICE_NAME}}"
-split = []
-
-[attestations]
-require = ["source-signature", "sbom-complete"]
-recommend = ["security-audit", "reproducible-build"]
-
-# Runtime security profile
-[security]
-user = "appuser"
-group = "appuser"
-read_only_root = false
-no_new_privileges = true
-
-[security.capabilities]
-drop = ["ALL"]
-add = ["NET_BIND_SERVICE"]
-
-[security.network]
-listen_tcp = [{{PORT}}]
-
-[security.filesystem]
-read = ["/app/", "/data/"]
-write = ["/data/", "/tmp/"]
-execute = ["/app/entrypoint.sh"]
diff --git a/container/vordr.toml b/container/vordr.toml
deleted file mode 100644
index e12022f..0000000
--- a/container/vordr.toml
+++ /dev/null
@@ -1,100 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
-#
-# Vordr runtime monitoring configuration for nextgen-typing
-#
-# Vordr watches container health, detects crashes, tracks resource usage,
-# and emits structured logs. It runs alongside the application stack and
-# provides runtime observability without requiring in-process agents.
-#
-# Usage:
-#   vordr watch --config container/vordr.toml
-#   vordr status
-#   vordr report
-
-[metadata]
-name = "{{SERVICE_NAME}}"
-version = "{{VERSION}}"
-
-# ============================================================================
-# Health Monitoring
-# ============================================================================
-#
-# Vordr periodically probes these endpoints. If a probe fails beyond the
-# failure_threshold, vordr emits an alert and (optionally) restarts the
-# container via Podman.
-
-[health]
-# Primary health endpoint — must return 2xx.
-endpoint = "http://localhost:{{PORT}}/health"
-interval = "30s"
-timeout = "5s"
-failure_threshold = 3
-
-# Readiness endpoint — checked during startup and after restarts.
-readiness_endpoint = "http://localhost:{{PORT}}/ready"
-readiness_timeout = "10s"
-
-# Action on failure: "alert" (log + notify) or "restart" (alert + podman restart).
-on_failure = "alert"
-
-# ============================================================================
-# Crash Detection
-# ============================================================================
-#
-# Monitors container state via Podman. Detects OOM kills, segfaults,
-# and unexpected exits.
-
-[crash_detection]
-enabled = true
-# Maximum restarts within the window before vordr stops restarting.
-max_restarts = 5
-restart_window = "10m"
-
-# ============================================================================
-# Resource Thresholds
-# ============================================================================
-#
-# Alert when resource usage exceeds these thresholds. Values are percentages
-# of the container's cgroup limits (or host limits if uncapped).
-
-[resources]
-cpu_warn = 80       # Percentage — warn at 80% sustained CPU.
-cpu_critical = 95   # Percentage — critical alert at 95%.
-memory_warn = 75    # Percentage of memory limit.
-memory_critical = 90
-disk_warn = 80      # Percentage of volume usage.
-disk_critical = 95
-
-# Sample interval for resource metrics.
-sample_interval = "15s"
-
-# ============================================================================
-# Log Output
-# ============================================================================
-#
-# Vordr emits its own logs (not the application's) in structured format.
-
-[logging]
-format = "json"
-level = "info"
-# Write vordr logs to stdout (captured by Podman) and optionally to file.
-output = "stdout"
-# file = "/var/log/vordr/{{SERVICE_NAME}}.log"
-
-# ============================================================================
-# Notifications (optional)
-# ============================================================================
-#
-# Uncomment and configure to receive alerts via webhook or email.
-
-# [notifications.webhook]
-# url = "https://example.com/hooks/vordr"
-# method = "POST"
-# headers = { "Content-Type" = "application/json" }
-# on = ["failure", "recovery", "resource_critical"]
-
-# [notifications.email]
-# to = "j.d.a.jewell@open.ac.uk"
-# from = "vordr@{{SERVICE_NAME}}.local"
-# smtp = "smtp://localhost:25"
-# on = ["failure", "resource_critical"]
diff --git a/docs/ARCHITECTURE.adoc b/docs/ARCHITECTURE.adoc
index e35cd67..6dad2cf 100644
--- a/docs/ARCHITECTURE.adoc
+++ b/docs/ARCHITECTURE.adoc
@@ -2,7 +2,7 @@
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = nextgen-typing: Pipeline Architecture
 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-2026-09-09
+2026-11-03
 :toc:
 :icons: font
 
diff --git a/docs/PIPELINE.adoc b/docs/PIPELINE.adoc
index 19c31b3..554238a 100644
--- a/docs/PIPELINE.adoc
+++ b/docs/PIPELINE.adoc
@@ -2,7 +2,7 @@
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = nextgen-typing: Pipeline Spec (A2ML)
 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-2026-09-09
+2026-11-03
 :toc:
 :icons: font
 
@@ -16,7 +16,7 @@ tooling and AI agents. Human-oriented architectural narrative remains in
 ----
 [pipeline]
 id = "hyperpolymath-type-theory-main-chain"
-version = "2026-09-09"
+version = "2026-11-03"
 coordination = "nextgen-typing"
 chain = "katagoria → typell → typed-wasm → PanLL"
 invariant = "TypeLL is open-ended progressive; L1-L10 is an initial checked set, not a ceiling."
diff --git a/docs/QUICKSTART.adoc b/docs/QUICKSTART.adoc
index f72fe10..45f069c 100644
--- a/docs/QUICKSTART.adoc
+++ b/docs/QUICKSTART.adoc
@@ -3,24 +3,27 @@
 = Quickstart
 :toc: preamble
 
-Get up and running in 60 seconds.
+Clone and run the `nextgen-typing` coordination and proof-ledger checks in 60 seconds.
 
 == Prerequisites
 
 * Git 2.40+
-* just (command runner)
-* Your language toolchain (see Justfile for details)
+* Bash 5+ and `jq`
+* `just` (optional command runner)
+* Agda, Coq (`coqc`/`coqchk`), and Lean 4 (only when compiling proof witnesses locally)
 
-== From Template (New Project)
+== Clone and Verify
 
 [source,bash]
 ----
-git clone https://github.com/hyperpolymath/rsr-template-repo my-project
-cd my-project
-rm -rf .git && git init -b main
-just init       # interactive placeholder replacement
+git clone https://github.com/hyperpolymath/nextgen-typing.git
+cd nextgen-typing
+./scripts/check-coordination-boundary.sh
+./scripts/check-pipeline-drift.sh .
+./scripts/check-proof-enrolment.sh
+./scripts/check-proof-ledger.sh
 ----
 
 == Project Structure
 
-See README.adoc in the root for the Dual-Track architecture summary.
+See link:../README.adoc[README.adoc] and link:ARCHITECTURE.adoc[docs/ARCHITECTURE.adoc] for the pipeline summary and ownership boundaries.
diff --git a/docs/RSR_OUTLINE.adoc b/docs/RSR_OUTLINE.adoc
index 5230bee..db493ee 100644
--- a/docs/RSR_OUTLINE.adoc
+++ b/docs/RSR_OUTLINE.adoc
@@ -103,14 +103,11 @@ just validate-rsr
 |`AI.a2ml`
 |Claude-specific instructions
 
-|`src/interface/Abi/`
-|Idris2 ABI definitions (Types, Layout, Foreign)
+|`verification/proofs/`
+|Cross-project formal proofs (Agda source + Rocq and Lean 4 recheck legs) and `LEDGER.json`
 
-|`ffi/zig/`
-|Zig FFI implementation
-
-|`generated/abi/`
-|Auto-generated C headers from Idris2 ABI
+|`.machine_readable/bot_directives/placement.a2ml`
+|Ownership routing rules between `nextgen-typing` and constituent repos
 |===
 
 == Justfile Features
@@ -176,23 +173,17 @@ project/
 │       ├── must/Mustfile      # Invariant checks
 │       └── trust/Trustfile.hs # Cryptographic verification
 ├── docs/                      # Documentation
-│   ├── CITATIONS.adoc
-│   ├── TOPOLOGY-GUIDE.adoc
-│   ├── generated/
-│   └── man/
-├── src/interface/Abi/         # Idris2 ABI definitions
-│   ├── Types.idr
-│   ├── Layout.idr
-│   └── Foreign.idr
-├── ffi/zig/                   # Zig FFI implementation
-│   ├── build.zig
-│   ├── src/main.zig
-│   └── test/integration_test.zig
-├── generated/abi/             # Auto-generated C headers
-├── examples/                  # Example code
-├── guix.scm                   # Guix package
+│   ├── ARCHITECTURE.adoc
+│   ├── PIPELINE.adoc
+│   └── TYPE-CONNECTIONS.adoc
+├── verification/proofs/       # Cross-project formal verification
+│   ├── LEDGER.json            # Theorem & recheck ledger
+│   ├── agda/                  # Agda source-of-truth proofs
+│   ├── coq/                   # Rocq (Coq) recheck witnesses
+│   └── lean4/                 # Core Lean 4 recheck witnesses
+├── scripts/                   # Boundary, drift, and proof gates
+├── build/guix.scm             # Guix package
 ├── Justfile                   # Task runner
-├── Containerfile              # Container build
 ├── LICENSE                    # MPL-2.0
 ├── EXHIBIT-A-ETHICAL-USE.txt  # Ethical use guidelines
 ├── EXHIBIT-B-QUANTUM-SAFE.txt # Quantum-safe provenance
diff --git a/docs/TYPE-CONNECTIONS.adoc b/docs/TYPE-CONNECTIONS.adoc
index 0003625..597d92b 100644
--- a/docs/TYPE-CONNECTIONS.adoc
+++ b/docs/TYPE-CONNECTIONS.adoc
@@ -130,13 +130,20 @@ domain. Equal measured values need not mean equal retained information.
 |The first core checks an encoding into `Echo.Echo` and both round trips.
 The residual core now also checks dependency-preserving composition and
 coarsening on its own side (`compose-claims`, `coarsen-claim`); whether
-these laws transport to Echo has not been compared.
+these laws transport to Echo has not been compared. *Acceptance criterion
+(#115):* `ResidualEvidence.Composition` states and proves `compose-claims`
+over `EchoComparison`, with a corresponding negative/reject module rejected
+in CI.
 |Epistemic → Residual Evidence
 |Make the meaning and evidence obligations of candidate-wide claims explicit.
 |The first core checks a `SoundWarrant` for a candidate-wide claim, with an
 inhabited case and explicit actual-world premises. The residual core now also
 checks evidence revision and retraction (`survives-retraction`, `revise`);
 their relation to warrant revision in Epistemic has not been compared.
+*Acceptance criterion (#115):* `ResidualEvidence.Revision` makes retraction
+constructive and `EpistemicComparison` proves non-vacuous warrant preservation
+/ revision beyond surface typing (explicitly discharging or bounding vacuous
+candidate paths).
 |Echo → Choreographic
 |Track the distinctions retained by projection to participants.
 |A projection model and correspondence theorem. An informal loss number
diff --git a/docs/developer/ABI-FFI-README.adoc b/docs/developer/ABI-FFI-README.adoc
index 5ac2241..c0dd632 100644
--- a/docs/developer/ABI-FFI-README.adoc
+++ b/docs/developer/ABI-FFI-README.adoc
@@ -2,21 +2,19 @@
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 = ABI/FFI — not defined in this repo
 
-nextgen-typing is a *coordination repo*: it documents and connects the
-type-theory pipeline and holds no compiler or application code, so it defines
-no ABI and no FFI of its own.
+`nextgen-typing` is a *coordination and cross-project verification repo*: it
+documents and connects the type-theory pipeline, hosts cross-project formal
+proofs under `verification/proofs/`, and holds no compiler or application code,
+so it defines no ABI and no FFI of its own.
 
-NOTE: the previous content here was RSR-template residue describing a
-`src/interface/Abi/` + `ffi/zig/` + `generated/abi/` layout that this repo does
-not have and never will. It was removed because it misled both humans and
-agents into adding ABI/FFI code to the coordination layer.
+NOTE: the previous RSR-template scaffold describing an Idris2 ABI and Zig FFI
+directory tree was removed under OQ-001 (PR #56) because this repository does
+not host single-project ABI/FFI implementations.
 
-== Where the ABI actually lives
-
-The estate's *verified convergence ABI* — the binary contract that independent
-WasmGC languages (AffineScript, Ephapax) agree on — and the aggregate-library
-binary conventions live in *typed-wasm*:
+== Where the ABI and proofs actually live
 
+* Cross-project formal verification witnesses: `verification/proofs/`
+  (tracked in `verification/proofs/LEDGER.json` and `PROOF-STATUS.adoc`)
 * WasmGC memory-safety proofs + convergence ABI: `hyperpolymath/typed-wasm`
 * Aggregate-library conventions (ADR-004): `hyperpolymath/typed-wasm`
 
diff --git a/docs/governance/CRG-CRITERIA.adoc b/docs/governance/CRG-CRITERIA.adoc
index 4b51a26..fd07550 100644
--- a/docs/governance/CRG-CRITERIA.adoc
+++ b/docs/governance/CRG-CRITERIA.adoc
@@ -38,4 +38,4 @@ This document defines the quality assessment criteria for individual project com
 6. Has it been tested on 6+ diverse external targets? (Broad → **B**)
 7. Do external users confirm it works and is useful? (Field-proven → **A**)
 
-See link:../../READINESS.md[READINESS.md] for the current project assessment.
+See link:../../READINESS.adoc[READINESS.adoc] for the current project assessment.
diff --git a/docs/governance/MAINTENANCE-CHECKLIST.a2ml b/docs/governance/MAINTENANCE-CHECKLIST.a2ml
index 17b6b96..53d2b95 100644
--- a/docs/governance/MAINTENANCE-CHECKLIST.a2ml
+++ b/docs/governance/MAINTENANCE-CHECKLIST.a2ml
@@ -133,8 +133,8 @@ quality_gate_required = [
 ]
 
 abi_ffi_policy = [
-  "ABI Idris2 in src/interface/Abi/*.idr (or src/interface/abi/*.idr)",
-  "FFI Zig in ffi/**/*.zig",
+  "Cross-project formal proofs in verification/proofs/ (tracked in verification/proofs/LEDGER.json)",
+  "Single-project ABI/FFI routed to owning repos (typed-wasm, typell) per .machine_readable/bot_directives/placement.a2ml",
 ]
 
 [should]
diff --git a/docs/governance/MAINTENANCE-CHECKLIST.adoc b/docs/governance/MAINTENANCE-CHECKLIST.adoc
index 10c4849..8711cd7 100644
--- a/docs/governance/MAINTENANCE-CHECKLIST.adoc
+++ b/docs/governance/MAINTENANCE-CHECKLIST.adoc
@@ -105,9 +105,9 @@ Run this pass at the end of a corrective/adaptive/perfective cycle:
 - [ ] Keep docs and navigation coherent:
   - single navigation entry point in root (`NAVIGATION.adoc` or equivalent)
   - no duplicate conflicting docs for same purpose (for example both `.md` and `.adoc` in root unless intentionally required)
-- [ ] Enforce ABI/FFI purity where the policy applies:
-  - ABI definitions in Idris2 (`src/interface/Abi/*.idr`)
-  - FFI implementations in Zig (`ffi/**/*.zig`)
+- [ ] Enforce verification and coordination-boundary purity:
+  - Cross-project formal proofs in `verification/proofs/` (tracked in `verification/proofs/LEDGER.json`)
+  - Single-project ABI/FFI implementations routed to their owning repositories (`typed-wasm`, `typell`) per `.machine_readable/bot_directives/placement.a2ml`
 - [ ] Ensure quality gate includes: formatting, lint, unit/integration tests, p2p/e2e checks, benchmark smoke, docs checks, security scan.
 
 ### Should
diff --git a/scripts/validate-template.sh b/scripts/validate-template.sh
index f053202..9142614 100755
--- a/scripts/validate-template.sh
+++ b/scripts/validate-template.sh
@@ -2,13 +2,9 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# RSR Template Validation Script
-# Verifies that a repository follows the RSR template structure and contains all required files
-#
-# Exit codes:
-#   0 = validation passed
-#   1 = validation failed with errors
-#   2 = validation failed with warnings (but can proceed)
+# RSR Coordinator & Verification Structure Validation Script for nextgen-typing
+# Verifies that the repository satisfies RSR structural, metadata, workflow,
+# proof-host (OQ-001), placeholder, and SPDX requirements.
 
 set -euo pipefail
 
@@ -17,37 +13,25 @@ VERBOSE="${2:-0}"
 ERRORS=0
 WARNINGS=0
 
-# ANSI colors
 RED='\033[0;31m'
 GREEN='\033[0;32m'
 YELLOW='\033[1;33m'
 BLUE='\033[0;34m'
-NC='\033[0m' # No Color
-
-# Helper functions
-log_error() {
-    echo -e "${RED}ERROR${NC}: $*" >&2
-    ERRORS=$((ERRORS + 1))
-}
-
-log_warning() {
-    echo -e "${YELLOW}WARN${NC}: $*" >&2
-    WARNINGS=$((WARNINGS + 1))
-}
-
-log_info() {
-    echo -e "${BLUE}INFO${NC}: $*" >&2
-}
+NC='\033[0m'
 
-log_pass() {
-    echo -e "${GREEN}PASS${NC}: $*" >&2
-}
+log_error() { echo -e "${RED}ERROR${NC}: $*" >&2; ERRORS=$((ERRORS + 1)); }
+log_warning() { echo -e "${YELLOW}WARN${NC}: $*" >&2; WARNINGS=$((WARNINGS + 1)); }
+log_info() { echo -e "${BLUE}INFO${NC}: $*" >&2; }
+log_pass() { echo -e "${GREEN}PASS${NC}: $*" >&2; }
 
+# Check a file path relative to REPO_ROOT. The optional second argument is a
+# description for a missing-file error. Return 1 and increment ERRORS if the
+# path is not a regular file; otherwise return 0.
 check_file_exists() {
     local file="$1"
     local description="${2:-}"
-    if [ -f "$REPO_ROOT/$file" ]; then
-        [ "$VERBOSE" = "1" ] && log_pass "File exists: $file"
+    if [[ -f "$REPO_ROOT/$file" ]]; then
+        [[ "$VERBOSE" == "1" ]] && log_pass "File exists: $file"
         return 0
     else
         log_error "Required file missing: $file ${description:+(${description})}"
@@ -55,11 +39,14 @@ check_file_exists() {
     fi
 }
 
+# Check a directory path relative to REPO_ROOT. The optional second argument is
+# a description for a missing-directory error. Return 1 and increment ERRORS if
+# the path is not a directory; otherwise return 0.
 check_dir_exists() {
     local dir="$1"
     local description="${2:-}"
-    if [ -d "$REPO_ROOT/$dir" ]; then
-        [ "$VERBOSE" = "1" ] && log_pass "Directory exists: $dir"
+    if [[ -d "$REPO_ROOT/$dir" ]]; then
+        [[ "$VERBOSE" == "1" ]] && log_pass "Directory exists: $dir"
         return 0
     else
         log_error "Required directory missing: $dir ${description:+(${description})}"
@@ -67,31 +54,17 @@ check_dir_exists() {
     fi
 }
 
+# Check the first ten lines for an SPDX identifier. Return a non-zero status if
+# none is found or the read/search pipeline fails.
 has_spdx_header() {
-    local file="$1"
-    if head -10 "$file" | grep -q "SPDX-License-Identifier"; then
-        return 0
-    fi
-    return 1
+    local target_file="$1"
+    head -10 "$target_file" | grep -q "SPDX-License-Identifier"
 }
 
-has_placeholder() {
-    local file="$1"
-    if grep -q "{{REPO\|{{OWNER\|{{FORGE\|{{PROJECT\|{{project\|{{AUTHOR" "$file" 2>/dev/null; then
-        return 0
-    fi
-    return 1
-}
-
-#==============================================================================
-# VALIDATION PHASE 1: CORE STRUCTURE
-#==============================================================================
-
 echo ""
-log_info "Phase 1: Core repository structure"
+log_info "Phase 1: Core coordinator repository structure"
 echo ""
 
-# Root files
 check_file_exists "0-AI-MANIFEST.a2ml" "AI manifest (universal entry point)"
 check_file_exists "README.adoc" "High-level pitch"
 check_file_exists "EXPLAINME.adoc" "Developer deep-dive"
@@ -99,32 +72,21 @@ check_file_exists "LICENSE" "License file"
 check_file_exists "Justfile" "Task runner"
 check_file_exists "AUDIT.adoc" "Release audit gate"
 
-# Directories
 check_dir_exists ".machine_readable" "Machine-readable metadata"
 check_dir_exists ".github" "GitHub community metadata"
-check_dir_exists "src/interface/abi" "Idris2 ABI definitions"
-check_dir_exists "src/interface/ffi" "Zig FFI implementation"
-check_dir_exists "src/interface/generated/abi" "Generated C headers"
+check_dir_exists "verification/proofs" "Cross-project formal proofs (OQ-001)"
 check_dir_exists "docs" "Documentation"
 
-#==============================================================================
-# VALIDATION PHASE 2: MACHINE-READABLE METADATA
-#==============================================================================
-
 echo ""
 log_info "Phase 2: Machine-readable metadata (.machine_readable/)"
 echo ""
 
-check_file_exists ".machine_readable/STATE.a2ml" "Project state"
-check_file_exists ".machine_readable/META.a2ml" "Architecture decisions"
-check_file_exists ".machine_readable/ECOSYSTEM.a2ml" "Ecosystem position"
-check_file_exists ".machine_readable/anchors/ANCHOR.a2ml" "Semantic boundary anchor"
+check_file_exists ".machine_readable/descriptiles/STATE.a2ml" "Project state"
+check_file_exists ".machine_readable/descriptiles/META.a2ml" "Architecture decisions"
+check_file_exists ".machine_readable/descriptiles/ECOSYSTEM.a2ml" "Ecosystem position"
+check_file_exists ".machine_readable/descriptiles/anchor/ANCHOR.a2ml" "Semantic boundary anchor"
 check_file_exists ".machine_readable/policies/MAINTENANCE-AXES.a2ml" "Maintenance axes"
 
-#==============================================================================
-# VALIDATION PHASE 3: REQUIRED WORKFLOWS (17 minimum)
-#==============================================================================
-
 echo ""
 log_info "Phase 3: GitHub Actions workflows"
 echo ""
@@ -141,180 +103,98 @@ REQUIRED_WORKFLOWS=(
     "security-policy.yml"
     "wellknown-enforcement.yml"
     "workflow-linter.yml"
-    "npm-bun-blocker.yml"
-    "ts-blocker.yml"
-    "scorecard-enforcer.yml"
     "secret-scanner.yml"
+    "proof-ci.yml"
+    "coordination-boundary.yml"
+    "dogfood-gate.yml"
+    "openssf-compliance.yml"
+    "governance.yml"
 )
 
-# Check required workflows
 for workflow in "${REQUIRED_WORKFLOWS[@]}"; do
-    if [ -f "$REPO_ROOT/.github/workflows/$workflow" ]; then
-        [ "$VERBOSE" = "1" ] && log_pass "Workflow found: $workflow"
+    if [[ -f "$REPO_ROOT/.github/workflows/$workflow" ]]; then
+        [[ "$VERBOSE" == "1" ]] && log_pass "Workflow found: $workflow"
     else
         log_error "Required workflow missing: $workflow"
     fi
 done
 
-# Verify all workflows have SPDX headers and proper structure
 WORKFLOW_FILES=$(find "$REPO_ROOT/.github/workflows" -name "*.yml" -type f 2>/dev/null || true)
 WORKFLOW_COUNT=$(echo "$WORKFLOW_FILES" | grep -c "." || true)
-
-if [ "$WORKFLOW_COUNT" -ge 15 ]; then
+if [[ "$WORKFLOW_COUNT" -ge 15 ]]; then
     log_pass "Found $WORKFLOW_COUNT workflows (>= 15 expected)"
 else
     log_warning "Found only $WORKFLOW_COUNT workflows (expected >= 15)"
 fi
 
-# Spot-check workflow files for issues
 while IFS= read -r workflow_file; do
-    if [ -z "$workflow_file" ]; then continue; fi
-
-    # Check for SPDX header (optional in YAML workflows, but best practice)
+    [[ -z "$workflow_file" ]] && continue
     if ! head -5 "$workflow_file" | grep -q "SPDX-License-Identifier"; then
         log_warning "Workflow missing SPDX header: $(basename "$workflow_file")"
     fi
-
-    # Check for proper YAML structure
     if ! grep -q "^name:" "$workflow_file"; then
         log_error "Workflow missing 'name' field: $(basename "$workflow_file")"
     fi
 done <<< "$WORKFLOW_FILES"
 
-#==============================================================================
-# VALIDATION PHASE 4: ABI/FFI SOURCE FILES
-#==============================================================================
-
 echo ""
-log_info "Phase 4: Idris2 ABI and Zig FFI source files"
+log_info "Phase 4: Cross-project formal verification (verification/proofs/)"
 echo ""
 
-# Idris2 ABI files
-check_file_exists "src/interface/abi/Types.idr" "Core type definitions"
-check_file_exists "src/interface/abi/Layout.idr" "Memory layout specifications"
-check_file_exists "src/interface/abi/Foreign.idr" "FFI foreign declarations"
-
-# Zig FFI files
-check_file_exists "src/interface/ffi/build.zig" "Zig build configuration"
-check_file_exists "src/interface/ffi/src/main.zig" "Zig implementation"
-check_file_exists "src/interface/ffi/test/integration_test.zig" "Integration tests"
-
-#==============================================================================
-# VALIDATION PHASE 5: PLACEHOLDER TOKENS
-#==============================================================================
+check_file_exists "verification/proofs/LEDGER.json" "Proof policy ledger"
+check_file_exists "verification/proofs/agda/EchoTyping.agda" "Agda source proof (XP-1)"
+check_file_exists "verification/proofs/coq/EchoTyping.v" "Rocq recheck witness (XP-1)"
+check_file_exists "verification/proofs/lean4/EchoTyping.lean" "Lean 4 recheck witness (XP-1)"
 
 echo ""
-log_info "Phase 5: Placeholder token replacement (skipped in template repo)"
+log_info "Phase 5: Placeholder token replacement"
 echo ""
 
-# Note: Template repo is allowed to have placeholders
-# For derived repos, we'd check that placeholders are replaced
-if [ "$(basename "$REPO_ROOT")" = "rsr-template-repo" ]; then
-    log_pass "Skipping placeholder check for template repo"
-else
-    # Check that key files don't have unresolved placeholders
-    for file in "$REPO_ROOT/README.adoc" "$REPO_ROOT/Justfile" "$REPO_ROOT/.machine_readable/STATE.a2ml"; do
-        if [ -f "$file" ]; then
-            if has_placeholder "$file"; then
-                log_warning "File contains unresolved placeholders: $(basename "$file")"
-            fi
-        fi
-    done
+for file in "$REPO_ROOT/README.adoc" "$REPO_ROOT/.machine_readable/descriptiles/STATE.a2ml" "$REPO_ROOT/www/.well-known/security.txt"; do
+    if [[ -f "$file" ]] && grep -qE '\{\{[A-Z0-9_]+\}\}' "$file" 2>/dev/null; then
+        log_error "File contains unresolved placeholders: $(basename "$file")"
+    fi
+done
+if [[ -f "$REPO_ROOT/Justfile" ]] && grep -q 'rsr-template-''repo' "$REPO_ROOT/Justfile" 2>/dev/null; then
+    log_error "Justfile still references template default repository name"
 fi
-
-#==============================================================================
-# VALIDATION PHASE 6: SPDX LICENSE HEADERS
-#==============================================================================
+log_pass "Key files checked for unresolved placeholders"
 
 echo ""
 log_info "Phase 6: SPDX License Headers"
 echo ""
 
-# Check source files for SPDX headers (excluding build artifacts)
-SOURCE_FILES=$(find "$REPO_ROOT/src" -type f \( -name "*.idr" -o -name "*.zig" \) \
-              ! -path "*/.zig-cache/*" ! -path "*/zig-cache/*" 2>/dev/null || true)
+SOURCE_FILES=$(find "$REPO_ROOT/verification/proofs" "$REPO_ROOT/scripts" -type f \( -name "*.agda" -o -name "*.v" -o -name "*.lean" -o -name "*.idr" -o -name "*.sh" \) 2>/dev/null || true)
 SOURCE_COUNT=$(echo "$SOURCE_FILES" | grep -c "." || true)
 SPDX_COUNT=0
-
 while IFS= read -r src_file; do
-    if [ -z "$src_file" ]; then continue; fi
+    [[ -z "$src_file" ]] && continue
     if has_spdx_header "$src_file"; then
         SPDX_COUNT=$((SPDX_COUNT + 1))
     else
-        log_warning "Source file missing SPDX header: $(basename "$src_file")"
+        log_warning "Source file missing SPDX header: $src_file"
     fi
 done <<< "$SOURCE_FILES"
 
-if [ "$SOURCE_COUNT" -gt 0 ]; then
+if [[ "$SOURCE_COUNT" -gt 0 ]]; then
     PERCENT=$((SPDX_COUNT * 100 / SOURCE_COUNT))
     log_pass "SPDX headers: $SPDX_COUNT/$SOURCE_COUNT ($PERCENT%)"
-    if [ "$PERCENT" -lt 100 ]; then
-        log_warning "Not all source files have SPDX headers"
-    fi
 fi
 
-#==============================================================================
-# VALIDATION PHASE 7: BUILD VERIFICATION
-#==============================================================================
-
 echo ""
-log_info "Phase 7: Build system verification"
+log_info "Phase 7: Documentation requirements"
 echo ""
 
-# Check Zig build
-if [ -f "$REPO_ROOT/src/interface/ffi/build.zig" ]; then
-    if command -v zig &> /dev/null; then
-        cd "$REPO_ROOT/src/interface/ffi"
-        if zig build 2>&1 | grep -q "error"; then
-            log_error "Zig build failed"
-        else
-            log_pass "Zig build successful"
-        fi
-        cd - > /dev/null
-    else
-        log_warning "Zig compiler not found - skipping Zig build check"
-    fi
+check_file_exists "docs/ARCHITECTURE.adoc" "Pipeline architecture"
+check_file_exists "docs/PIPELINE.adoc" "Machine-readable pipeline spec"
+check_file_exists "docs/TYPE-CONNECTIONS.adoc" "Type-family connections guide"
+check_file_exists "docs/developer/ABI-FFI-README.adoc" "ABI/FFI routing note"
+if [[ -f "$REPO_ROOT/.github/CONTRIBUTING.md" ]] || [[ -f "$REPO_ROOT/CONTRIBUTING.md" ]]; then
+    [[ "$VERBOSE" == "1" ]] && log_pass "Contribution guide found"
 else
-    log_error "Zig build.zig not found"
+    log_error "Required file missing: .github/CONTRIBUTING.md (Contribution guide)"
 fi
-
-# Check Idris2 syntax (if available)
-if command -v idris2 &> /dev/null; then
-    IDS_FILES=$(find "$REPO_ROOT/src/interface/abi" -name "*.idr" -type f 2>/dev/null || true)
-    while IFS= read -r ids_file; do
-        if [ -z "$ids_file" ]; then continue; fi
-        if ! idris2 --check "$ids_file" 2>&1 | grep -q "Error"; then
-            log_pass "Idris2 syntax OK: $(basename "$ids_file")"
-        else
-            log_warning "Idris2 syntax issue: $(basename "$ids_file")"
-        fi
-    done <<< "$IDS_FILES"
-else
-    log_warning "Idris2 compiler not found - skipping Idris2 syntax checks"
-fi
-
-#==============================================================================
-# VALIDATION PHASE 8: DOCUMENTATION
-#==============================================================================
-
-echo ""
-log_info "Phase 8: Documentation requirements"
-echo ""
-
-check_file_exists "docs/developer/ABI-FFI-README.adoc" "ABI/FFI documentation"
-check_file_exists "TOPOLOGY.md" "Architecture topology" || check_file_exists "docs/architecture/TOPOLOGY.md" "Architecture topology (in docs)"
-check_file_exists "CONTRIBUTING.md" "Contribution guide"
-
-# Governance can be at root or in docs/governance/
-if [ -f "$REPO_ROOT/GOVERNANCE.adoc" ] || [ -f "$REPO_ROOT/GOVERNANCE.md" ] || [ -d "$REPO_ROOT/docs/governance" ]; then
-    [ "$VERBOSE" = "1" ] && log_pass "Governance files found"
-else
-    log_warning "Governance documentation not found"
-fi
-
-#==============================================================================
-# VALIDATION SUMMARY
-#==============================================================================
+check_file_exists "GOVERNANCE.adoc" "Governance documentation"
 
 echo ""
 echo "═══════════════════════════════════════════════════════════════════════════════"
@@ -325,12 +205,10 @@ echo -e "Errors:   ${RED}${ERRORS}${NC}"
 echo -e "Warnings: ${YELLOW}${WARNINGS}${NC}"
 echo ""
 
-if [ "$ERRORS" -eq 0 ]; then
+if [[ "$ERRORS" -eq 0 ]]; then
     echo -e "${GREEN}✓ Validation PASSED${NC}"
-    [ "$WARNINGS" -gt 0 ] && echo -e "  (with $WARNINGS warnings)"
     exit 0
 else
     echo -e "${RED}✗ Validation FAILED${NC}"
-    echo "  Please fix the errors above."
     exit 1
 fi
diff --git a/setup.sh b/setup.sh
index f69d2a9..ba93530 100755
--- a/setup.sh
+++ b/setup.sh
@@ -1,6 +1,6 @@
 #!/bin/sh
 # SPDX-License-Identifier: MPL-2.0
-# setup.sh — Universal setup script for rsr-template-repo
+# setup.sh — Universal setup script for nextgen-typing
 #
 # Detects your shell, platform, and installs prerequisites.
 # Then hands off to `just setup` for project-specific configuration.
@@ -127,7 +127,7 @@ detect_platform() {
 }
 
 # ── Verified just install ──
-# Replaces `curl https://just.systems/install.sh | bash`: piping a remote script
+# Replaces unverified remote install-script execution: piping a remote script
 # into a shell runs whatever the server returns, with no chance to check it.
 # A pinned RELEASE BINARY is fetched instead and its digest checked before use
 # (ported from hyperpolymath/standards setup.sh, 3079bc12). Digests computed
diff --git a/tests/aspect_tests.sh b/tests/aspect_tests.sh
index 797b688..fcbe2a9 100755
--- a/tests/aspect_tests.sh
+++ b/tests/aspect_tests.sh
@@ -2,22 +2,11 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# RSR Standard Aspect Test Template
-#
-# Aspect tests validate cross-cutting architectural invariants that span
-# the entire codebase. These are NOT functional tests — they verify that
-# coding standards, safety rules, and structural contracts hold.
-#
-# Usage:
-#   bash tests/aspect_tests.sh
-#   just aspect
-#
-# Standard aspects (enable what applies to your project):
-#   1. SPDX compliance — all source files have license headers
-#   2. Dangerous patterns — no believe_me, assert_total, sorry, unsafeCoerce, etc.
-#   3. ABI/FFI contract — declarations match exports
-#   4. Thread safety — mutex in FFI modules
-#   5. Error handling — no panic/unreachable in production paths
+# Aspect tests for nextgen-typing (cross-cutting architectural invariants):
+#   1. SPDX compliance — all verification proofs and gate scripts have SPDX headers
+#   2. Dangerous proof escape hatches — scripts/proof-scan-dangerous.sh passes
+#   3. Coordination boundary — scripts/check-coordination-boundary.sh passes
+#   4. Proof enrolment & ledger — scripts/check-proof-enrolment.sh & check-proof-ledger.sh pass
 
 set -euo pipefail
 
@@ -39,96 +28,51 @@ fail() { red "  FAIL: $1"; FAIL=$((FAIL + 1)); }
 warn() { yellow "  WARN: $1"; WARN=$((WARN + 1)); }
 
 echo "═══════════════════════════════════════════════════════════════"
-echo "  NEXTGEN_TYPING — Aspect Tests (Cross-Cutting Concerns)"
+echo "  nextgen-typing — Aspect Tests (Cross-Cutting Concerns)"
 echo "═══════════════════════════════════════════════════════════════"
 echo ""
 
-# ═══════════════════════════════════════════════════════════════════════
-# Aspect 1: SPDX License Headers
-# ═══════════════════════════════════════════════════════════════════════
 bold "Aspect 1: SPDX license headers"
-
 MISSING_SPDX=0
 while IFS= read -r -d '' f; do
     if ! head -5 "$f" | grep -q "SPDX-License-Identifier"; then
         warn "Missing SPDX header: $f"
         MISSING_SPDX=$((MISSING_SPDX + 1))
     fi
-done < <(find src/ -type f \( -name "*.rs" -o -name "*.zig" -o -name "*.res" -o -name "*.ex" -o -name "*.exs" -o -name "*.gleam" -o -name "*.idr" -o -name "*.sh" \) -print0 2>/dev/null)
+done < <(find scripts/ verification/proofs/ -type f \( -name "*.agda" -o -name "*.v" -o -name "*.lean" -o -name "*.idr" -o -name "*.sh" \) -print0 2>/dev/null)
 
-if [ "$MISSING_SPDX" -eq 0 ]; then
-    pass "All source files have SPDX headers"
+if [[ "$MISSING_SPDX" -eq 0 ]]; then
+    pass "All verification proofs and gate scripts carry SPDX headers"
 else
-    fail "$MISSING_SPDX files missing SPDX headers"
+    fail "$MISSING_SPDX file(s) missing SPDX headers"
 fi
 
-# ═══════════════════════════════════════════════════════════════════════
-# Aspect 2: Dangerous Patterns (BANNED)
-# ═══════════════════════════════════════════════════════════════════════
-bold "Aspect 2: Dangerous patterns"
-
-# Idris2 dangerous patterns
-DANGEROUS_IDRIS=$(grep -rn 'believe_me\|assert_total\|really_believe_me' src/abi/ 2>/dev/null | grep -v "^Binary" | grep -v "test" || true)
-if [ -n "$DANGEROUS_IDRIS" ]; then
-    fail "Dangerous Idris2 patterns found:"
-    echo "$DANGEROUS_IDRIS" | head -5
+bold "Aspect 2: Dangerous proof escape hatches"
+if ./scripts/proof-scan-dangerous.sh >/dev/null; then
+    pass "Comment-aware proof escape-hatch scanner clean"
 else
-    pass "No dangerous Idris2 patterns (believe_me, assert_total)"
+    fail "scripts/proof-scan-dangerous.sh reported dangerous proof tokens"
 fi
 
-# Coq/Lean dangerous patterns
-DANGEROUS_PROOF=$(grep -rn '\bAdmitted\b\|\bsorry\b\|\bunsafeCoerce\b\|\bObj\.magic\b' src/ verification/ 2>/dev/null | grep -v "test" | grep -v "comment" || true)
-if [ -n "$DANGEROUS_PROOF" ]; then
-    fail "Dangerous proof patterns found:"
-    echo "$DANGEROUS_PROOF" | head -5
+bold "Aspect 3: Coordination boundary"
+if ./scripts/check-coordination-boundary.sh >/dev/null; then
+    pass "Coordination boundary intact (verification/proofs/ only)"
 else
-    pass "No dangerous proof patterns (Admitted, sorry, unsafeCoerce)"
+    fail "scripts/check-coordination-boundary.sh failed"
 fi
 
-# ═══════════════════════════════════════════════════════════════════════
-# Aspect 3: ABI/FFI Contract (if applicable)
-# ═══════════════════════════════════════════════════════════════════════
-# Uncomment if your project has Idris2 ABI + Zig FFI:
-
-# bold "Aspect 3: ABI/FFI contract"
-# if [ -d "src/abi" ] && [ -d "ffi/zig" ]; then
-#     # Check that every exported function in Idris2 ABI has a Zig FFI implementation
-#     ABI_EXPORTS=$(grep -h 'export' src/abi/*.idr 2>/dev/null | wc -l)
-#     FFI_EXPORTS=$(grep -h 'pub export fn' ffi/zig/src/*.zig 2>/dev/null | wc -l)
-#     if [ "$ABI_EXPORTS" -gt 0 ] && [ "$FFI_EXPORTS" -gt 0 ]; then
-#         pass "ABI ($ABI_EXPORTS exports) and FFI ($FFI_EXPORTS exports) both present"
-#     else
-#         fail "ABI/FFI mismatch: $ABI_EXPORTS ABI exports, $FFI_EXPORTS FFI exports"
-#     fi
-# else
-#     pass "ABI/FFI not applicable (no src/abi or ffi/zig)"
-# fi
-
-# ═══════════════════════════════════════════════════════════════════════
-# Aspect 4: Error Handling (no raw panic in production code)
-# ═══════════════════════════════════════════════════════════════════════
-# Uncomment for Rust projects:
-
-# bold "Aspect 4: Error handling"
-# UNWRAP_COUNT=$(grep -rn '\.unwrap()' src/ 2>/dev/null | grep -v "test" | grep -v "example" | wc -l)
-# if [ "$UNWRAP_COUNT" -gt 20 ]; then
-#     warn "$UNWRAP_COUNT .unwrap() calls in src/ — consider replacing with ? or expect()"
-# else
-#     pass "Acceptable unwrap count: $UNWRAP_COUNT"
-# fi
+bold "Aspect 4: Proof enrolment & ledger integrity"
+ENROL_RC=0
+./scripts/check-proof-enrolment.sh >/dev/null 2>&1 || ENROL_RC=$?
+if [[ "$ENROL_RC" -eq 0 || "$ENROL_RC" -eq 2 ]] && ./scripts/check-proof-ledger.sh >/dev/null; then
+    pass "Proof enrolment consistent and LEDGER.json audit passed"
+else
+    fail "Proof enrolment (rc=$ENROL_RC) or LEDGER.json check failed"
+fi
 
-# ═══════════════════════════════════════════════════════════════════════
-# Summary
-# ═══════════════════════════════════════════════════════════════════════
 echo ""
 echo "═══════════════════════════════════════════════════════════════"
-printf "  Results: "
-green "PASS=$PASS" | tr -d '\n'
-echo -n "  "
-if [ "$FAIL" -gt 0 ]; then red "FAIL=$FAIL" | tr -d '\n'; else echo -n "FAIL=0"; fi
-echo -n "  "
-if [ "$WARN" -gt 0 ]; then yellow "WARN=$WARN"; else echo "WARN=0"; fi
-echo ""
+printf "  Results: PASS=%d  FAIL=%d  WARN=%d\n" "$PASS" "$FAIL" "$WARN"
 echo "═══════════════════════════════════════════════════════════════"
 
-exit "$FAIL"
+[[ "$FAIL" -eq 0 ]]
diff --git a/tests/e2e/template_instantiation_test.sh b/tests/e2e/template_instantiation_test.sh
index 591f20f..f81ff2e 100755
--- a/tests/e2e/template_instantiation_test.sh
+++ b/tests/e2e/template_instantiation_test.sh
@@ -2,269 +2,36 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# E2E Test: Template Instantiation
-# Verifies that the template can be cloned and instantiated into a working project
-#
-# This test:
-# 1. Clones the template to a temp directory
-# 2. Replaces all placeholder tokens with test values
-# 3. Validates the resulting repository structure
-# 4. Verifies builds work after instantiation
-# 5. Cleans up
+# E2E Test: Coordinator Repository Integrity
+# Copies the repository into a clean temporary working tree and runs all
+# structural, coordination-boundary, workflow, and proof-ledger checks.
 
 set -euo pipefail
 
-# Test configuration
-TEMPLATE_ROOT="${1:-.}"
-TEST_DIR="${TMPDIR:-/tmp}/rsr-template-test-$$"
-TEST_REPO_NAME="test-instantiated-repo"
-TEST_OWNER="test-owner"
-TEST_FORGE="github"
-TEST_AUTHOR="Test Author"
-TEST_AUTHOR_EMAIL="test@example.com"
-TEST_PROJECT_NAME="Test Project"
-TEST_DESCRIPTION="A test project instantiated from the RSR template"
-TEST_PRIMARY_LANGUAGE="Rust"
-
-# ANSI colors
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[1;33m'
-BLUE='\033[0;34m'
-NC='\033[0m' # No Color
-
-# Helper functions
-log_step() {
-    echo ""
-    echo -e "${BLUE}→${NC} $*"
-}
-
-log_pass() {
-    echo -e "${GREEN}✓${NC} $*"
-}
-
-log_error() {
-    echo -e "${RED}✗${NC} $*" >&2
-}
+REPO_SOURCE="${1:-.}"
+TEMP_DIR="$(mktemp -d)"
+TEST_REPO_PATH="$TEMP_DIR/nextgen-typing-e2e"
 
 cleanup() {
-    if [ -d "$TEST_DIR" ]; then
-        log_step "Cleaning up test directory: $TEST_DIR"
-        rm -rf "$TEST_DIR"
-        log_pass "Cleanup complete"
-    fi
+    rm -rf "$TEMP_DIR"
 }
-
 trap cleanup EXIT
 
-#==============================================================================
-# PHASE 1: SETUP
-#==============================================================================
-
-echo ""
-echo "═══════════════════════════════════════════════════════════════════════════════"
-echo "E2E TEST: Template Instantiation"
-echo "═══════════════════════════════════════════════════════════════════════════════"
-echo ""
-
-log_step "Creating test directory: $TEST_DIR"
-mkdir -p "$TEST_DIR"
-log_pass "Test directory created"
-
-#==============================================================================
-# PHASE 2: CLONE TEMPLATE
-#==============================================================================
-
-log_step "Cloning template from $TEMPLATE_ROOT"
-
-# Copy template to test location (simulating git clone)
-TEST_REPO_PATH="$TEST_DIR/$TEST_REPO_NAME"
-cp -r "$TEMPLATE_ROOT" "$TEST_REPO_PATH"
-log_pass "Template cloned to $TEST_REPO_PATH"
-
-# Remove .git directory for clean state
-if [ -d "$TEST_REPO_PATH/.git" ]; then
-    rm -rf "$TEST_REPO_PATH/.git"
-    log_pass ".git directory removed (fresh clone)"
-fi
-
-#==============================================================================
-# PHASE 3: PLACEHOLDER REPLACEMENT
-#==============================================================================
-
-log_step "Replacing placeholder tokens"
-
-# Function to replace all occurrences of a placeholder in a file
-replace_placeholder() {
-    local file="$1"
-    local placeholder="$2"
-    local value="$3"
-
-    if [ ! -f "$file" ]; then
-        return 0
-    fi
-
-    # Use sed to replace (platform-portable)
-    if grep -q "$placeholder" "$file" 2>/dev/null; then
-        sed -i "s|$placeholder|$value|g" "$file"
-        echo "  Replaced $placeholder in $(basename "$file")"
-    fi
-}
-
-# Replace in all text files
-export TEST_REPO_NAME TEST_OWNER TEST_FORGE TEST_PROJECT_NAME \
-    TEST_DESCRIPTION TEST_PRIMARY_LANGUAGE TEST_AUTHOR TEST_AUTHOR_EMAIL
-find "$TEST_REPO_PATH" -type f \
-    \( -name "*.md" -o -name "*.adoc" -o -name "*.a2ml" -o -name "*.zig" -o -name "*.idr" \
-       -o -name "Justfile" -o -name "Containerfile" -o -name "*.yml" -o -name "*.yaml" \
-       -o -name "*.json" -o -name "*.scm" -o -name "contractile" \) \
-    -exec bash -c '
-        file="$1"
-        placeholder_pairs=(
-            "nextgen-typing|$TEST_REPO_NAME"
-            "hyperpolymath|$TEST_OWNER"
-            "github.com|$TEST_FORGE"
-            "NEXTGEN_TYPING|$TEST_PROJECT_NAME"
-            "nextgen_typing|'"${TEST_REPO_NAME//-/_}"'"
-            "{{REPO_DESCRIPTION}}|$TEST_DESCRIPTION"
-            "{{PRIMARY_LANGUAGE}}|$TEST_PRIMARY_LANGUAGE"
-            "Jonathan D.A. Jewell|$TEST_AUTHOR"
-            "j.d.a.jewell@open.ac.uk|$TEST_AUTHOR_EMAIL"
-            "2026-04-11|2026-04-04"
-        )
-
-        for pair in "${placeholder_pairs[@]}"; do
-            IFS="|" read -r placeholder value <<< "$pair"
-            if grep -q "$placeholder" "$file" 2>/dev/null; then
-                sed -i "s|$placeholder|$value|g" "$file"
-            fi
-        done
-    ' _ {} \;
+cp -r "$REPO_SOURCE" "$TEST_REPO_PATH"
 
-log_pass "All placeholder tokens replaced"
-
-#==============================================================================
-# PHASE 4: VALIDATE STRUCTURE
-#==============================================================================
-
-log_step "Validating instantiated repository structure"
-
-# Run validation script on the instantiated repo
-if [ -f "$TEMPLATE_ROOT/scripts/validate-template.sh" ]; then
-    bash "$TEMPLATE_ROOT/scripts/validate-template.sh" "$TEST_REPO_PATH" 0
-    log_pass "Repository structure validation passed"
-else
-    log_error "Validation script not found"
-    exit 1
-fi
-
-#==============================================================================
-# PHASE 5: VERIFY BUILD
-#==============================================================================
-
-log_step "Verifying build system works after instantiation"
-
-if [ -f "$TEST_REPO_PATH/src/interface/ffi/build.zig" ]; then
-    if command -v zig &> /dev/null; then
-        cd "$TEST_REPO_PATH/src/interface/ffi"
-        if zig build 2>&1; then
-            log_pass "Zig build successful"
-        else
-            log_error "Zig build failed"
-            exit 1
-        fi
-        cd - > /dev/null
-    else
-        log_error "Zig compiler not found - cannot verify build"
+(
+    cd "$TEST_REPO_PATH"
+    bash scripts/validate-template.sh . 0
+    bash scripts/check-coordination-boundary.sh
+    ENROL_RC=0
+    bash scripts/check-proof-enrolment.sh >/dev/null 2>&1 || ENROL_RC=$?
+    if [[ "$ENROL_RC" -ne 0 ]]; then
+        echo "check-proof-enrolment.sh failed with rc=$ENROL_RC" >&2
         exit 1
     fi
-fi
-
-#==============================================================================
-# PHASE 6: VERIFY NO REMAINING PLACEHOLDERS
-#==============================================================================
-
-log_step "Checking for remaining placeholders"
-
-REMAINING_PLACEHOLDERS=$(
-    find "$TEST_REPO_PATH" -type f \
-        \( -name "*.md" -o -name "*.adoc" -o -name "*.a2ml" -o -name "*.zig" -o -name "*.idr" \
-           -o -name "Justfile" -o -name "*.yml" \) \
-        -exec grep -l "{{[A-Z_]*}}" {} \; 2>/dev/null || true
+    bash scripts/check-proof-ledger.sh
+    bash tests/workflows/validate_workflows_test.sh .github/workflows
+    bash tests/aspect_tests.sh
 )
 
-if [ -z "$REMAINING_PLACEHOLDERS" ]; then
-    log_pass "No remaining placeholders found"
-else
-    log_error "Found remaining placeholders in:"
-    echo "$REMAINING_PLACEHOLDERS" | sed 's/^/  /'
-    exit 1
-fi
-
-#==============================================================================
-# PHASE 7: VERIFY CRITICAL FILES ARE NOT TEMPLATES
-#==============================================================================
-
-log_step "Verifying critical files have been instantiated"
-
-CRITICAL_FILES=(
-    "README.adoc"
-    "EXPLAINME.adoc"
-    "Justfile"
-)
-
-for file in "${CRITICAL_FILES[@]}"; do
-    if [ -f "$TEST_REPO_PATH/$file" ]; then
-        # Check that it's not just a template (contains some actual content)
-        if grep -q "$TEST_PROJECT_NAME\|$TEST_AUTHOR\|$TEST_REPO_NAME" "$TEST_REPO_PATH/$file" 2>/dev/null || \
-           [ $(wc -l < "$TEST_REPO_PATH/$file") -gt 10 ]; then
-            log_pass "File instantiated: $file"
-        else
-            log_error "File appears to be a template: $file"
-            exit 1
-        fi
-    else
-        log_error "Critical file missing: $file"
-        exit 1
-    fi
-done
-
-#==============================================================================
-# PHASE 8: VERIFY METADATA
-#==============================================================================
-
-log_step "Verifying machine-readable metadata"
-
-METADATA_FILES=(
-    ".machine_readable/STATE.a2ml"
-    ".machine_readable/META.a2ml"
-)
-
-for file in "${METADATA_FILES[@]}"; do
-    if [ -f "$TEST_REPO_PATH/$file" ]; then
-        log_pass "Metadata file exists: $file"
-    else
-        log_error "Metadata file missing: $file"
-        exit 1
-    fi
-done
-
-#==============================================================================
-# SUMMARY
-#==============================================================================
-
-echo ""
-echo "═══════════════════════════════════════════════════════════════════════════════"
-echo -e "${GREEN}✓ E2E TEMPLATE INSTANTIATION TEST PASSED${NC}"
-echo "═══════════════════════════════════════════════════════════════════════════════"
-echo ""
-echo "Summary:"
-echo "  - Template cloned successfully"
-echo "  - All placeholders replaced"
-echo "  - Repository structure valid"
-echo "  - Build system works"
-echo "  - No remaining placeholders"
-echo "  - Metadata intact"
-echo ""
-echo "Test repository: $TEST_REPO_PATH (will be cleaned up)"
-echo ""
+echo "✓ E2E coordinator repository integrity test PASSED"
diff --git a/tests/rsr_antipattern_heading_test.sh b/tests/rsr_antipattern_heading_test.sh
new file mode 100755
index 0000000..1ed7677
--- /dev/null
+++ b/tests/rsr_antipattern_heading_test.sh
@@ -0,0 +1,80 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
+#
+# Positive and negative fixture controls for `.github/workflows/rsr-antipattern.yml`
+# Markdown heading detection (#121 AC 3):
+#   1. Positive fixture: a real `## TypeScript Exemptions` heading enables
+#      parsing of its Markdown table rows and stops at the next heading.
+#   2. Negative fixture: a prose mention of `TypeScript Exemptions` followed
+#      by an unrelated Markdown table must NOT match or ingest rows.
+
+set -euo pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+REPO_ROOT="$(cd "$SCRIPT_DIR/.." && pwd)"
+WORKFLOW="$REPO_ROOT/.github/workflows/rsr-antipattern.yml"
+
+python3 - "$WORKFLOW" <<'PYEOF'
+import pathlib, re, sys
+
+wf_text = pathlib.Path(sys.argv[1]).read_text(encoding="utf-8")
+
+# Extract the live heading-detection regex directly from rsr-antipattern.yml so
+# any drift in the workflow is tested rather than a copy-pasted regex.
+m_open = re.search(r"re\.search\(r'([^']*TypeScript \[Ee\]xemptions[^']*)',\s*line\)", wf_text)
+assert m_open is not None, "Could not locate TypeScript Exemptions heading regex in rsr-antipattern.yml"
+heading_pattern = re.compile(m_open.group(1))
+assert m_open.group(1).startswith(r"^#{1,4}\s+"), (
+    f"Heading regex is not anchored to ^#{{1,4}}\\s+: {m_open.group(1)!r}"
+)
+
+def parse_exemptions(markdown_text: str) -> list[str]:
+    found = []
+    in_table = False
+    for line in markdown_text.splitlines():
+        if heading_pattern.search(line):
+            in_table = True
+            continue
+        if in_table and re.match(r"^#{1,4}\s+", line):
+            break
+        if in_table and line.startswith("|"):
+            m = re.match(r"\|\s*`([^`]+)`", line)
+            if m:
+                found.append(m.group(1))
+    return found
+
+# 1. Positive fixture: real Markdown `## TypeScript Exemptions` heading matches,
+#    and parsing stops cleanly at the next section heading.
+positive_doc = """# Project Instructions
+
+## TypeScript Exemptions
+
+| Path | Rationale |
+|------|-----------|
+| `bridges/demo/*.ts` | Permitted interop bridge |
+
+## Unrelated Table
+
+| Path | Notes |
+|------|-------|
+| `forbidden/sneak.ts` | Must not be parsed |
+"""
+pos_rows = parse_exemptions(positive_doc)
+assert pos_rows == ["bridges/demo/*.ts"], f"Positive fixture failed: got {pos_rows!r}"
+
+# 2. Negative fixture: prose line mentioning `TypeScript Exemptions` does NOT
+#    match even when followed by a backticked Markdown table.
+negative_doc = """# Project Instructions
+
+Do not add entries to the TypeScript Exemptions table without maintainer review.
+
+| Column | Example |
+|--------|---------|
+| `forbidden/prose_leak.ts` | Unrelated prose table row |
+"""
+neg_rows = parse_exemptions(negative_doc)
+assert neg_rows == [], f"Negative fixture matched prose mention: got {neg_rows!r}"
+
+print("PASS: rsr-antipattern heading regex passed positive and negative fixtures.")
+PYEOF
diff --git a/tests/workflows/validate_workflows_test.sh b/tests/workflows/validate_workflows_test.sh
index 614bb5a..4bf2bf4 100755
--- a/tests/workflows/validate_workflows_test.sh
+++ b/tests/workflows/validate_workflows_test.sh
@@ -100,9 +100,9 @@ REQUIRED_WORKFLOWS=(
     "security-policy.yml"
     "wellknown-enforcement.yml"
     "workflow-linter.yml"
-    "npm-bun-blocker.yml"
-    "ts-blocker.yml"
-    "scorecard-enforcer.yml"
+    "proof-ci.yml"
+    "coordination-boundary.yml"
+    "governance.yml"
     "secret-scanner.yml"
 )
 
diff --git a/verification/proofs/LEDGER.json b/verification/proofs/LEDGER.json
index 49a2e2e..a3aca63 100644
--- a/verification/proofs/LEDGER.json
+++ b/verification/proofs/LEDGER.json
@@ -19,7 +19,7 @@
         "clause": "§6 (toolchains)",
         "subject": "CI install path for Rocq and Lean 4",
         "deviation": "installed in .github/workflows/proof-ci.yml from the Ubuntu package index (coq 8.18.0, version asserted) and from the official Lean 4 release archive (4.15.0, sha256-verified before extraction and version asserted) — not through a Guix manifest or through container/",
-        "reason": "container/ is the development environment and does not carry the proof toolchains; pinning them through Guix or the container is a separate change with its own review",
+        "reason": ".devcontainer/ is the editor development environment and does not carry the proof toolchains; pinning them through Guix or a dedicated proof container is a separate change with its own review",
         "state": "open",
         "note": "Recorded as a deviation, not a waiver: §4 is a capability exception for a proof leg, not a bootstrap exception for how a toolchain is installed."
       }
@@ -69,14 +69,23 @@
         ],
         "evidence": {
           "kind": "ci-receipt",
-          "commit": "3cd185939179773f177b59e6fee360719695dfc7",
-          "date": "2026-11-01",
-          "run": "https://github.com/hyperpolymath/nextgen-typing/actions/runs/41314454646",
-          "invocation": "agda --safe --without-K --cubical-compatible verification/proofs/agda/EchoTyping.agda and .../Verification.agda, via `just proof-check-agda` -> scripts/check-proofs.sh agda, with the standard-library, echo-types and absolute-zero library manifests registered",
+          "commit": "c4ea39721d7ba893478fe57b5f749a89f2996508",
+          "date": "2026-11-03",
+          "run": "https://github.com/hyperpolymath/nextgen-typing/actions/runs/41565790232",
+          "invocation": "agda --safe --without-K --cubical-compatible verification/proofs/agda/EchoTyping.agda and .../Verification.agda, via `just proof-check-all` -> `just proof-check-agda` -> scripts/check-proofs.sh agda, with the standard-library, echo-types and absolute-zero library manifests registered",
           "observed_result": "PASS — 2 gated modules typecheck, 0 failures, 0 quarantined; manifest coverage 2/2 files accounted for",
-          "checked_by": "proof-ci.yml, Agda 2.8.0, agda-stdlib v2.4 @2a5a0dec0a3cb5c87468ce101388a513d39dbf10, echo-types b0982c44f36133acd2d0e1d4e03cf031fff7a470, absolute-zero f486c29903434589117fa0662c6f29b0f17d1d5f",
-          "note": "PROOF-POLICY §2.1 (2026-11-01) makes the canonical invocation `agda --safe --without-K --cubical-compatible` and says a prior `--safe` or `--safe --without-K` success is historical evidence rather than a receipt for that combined profile. This receipt is the first canonical one; the earlier receipt is kept below as historical, not as evidence.",
+          "checked_by": "proof-ci.yml on main, Agda 2.8.0, agda-stdlib v2.4 @2a5a0dec0a3cb5c87468ce101388a513d39dbf10, echo-types b0982c44f36133acd2d0e1d4e03cf031fff7a470, absolute-zero f486c29903434589117fa0662c6f29b0f17d1d5f",
+          "note": "PROOF-POLICY §2.1 (2026-11-01) makes the canonical invocation `agda --safe --without-K --cubical-compatible`. Run 41565790232 on main (c4ea3972) verified Agda alongside Rocq and Lean 4 via `just proof-check-all`; superseded pre-merge receipts are retained below.",
           "historical_evidence": [
+            {
+              "state": "superseded",
+              "kind": "ci-receipt",
+              "commit": "3cd185939179773f177b59e6fee360719695dfc7",
+              "date": "2026-11-01",
+              "run": "https://github.com/hyperpolymath/nextgen-typing/actions/runs/41314454646",
+              "checked_by": "proof-ci.yml, Agda 2.8.0, agda-stdlib v2.4 @2a5a0dec0a3cb5c87468ce101388a513d39dbf10, echo-types b0982c4, absolute-zero f486c29",
+              "why_not_current": "superseded on main by squash-merged commit c4ea39721d7ba893478fe57b5f749a89f2996508 (run 41565790232)"
+            },
             {
               "state": "superseded",
               "kind": "ci-receipt (historical under §2.1)",
@@ -238,9 +247,9 @@
           "statement_compared": "Compared anchor-by-anchor against verification/proofs/agda/EchoTyping.agda (PROOF-POLICY §2.2): Echo f y := { x : A & f x = y } (Type-valued sigT, never Prop-truncated ex, preserving projT1 witness projection); EchoR Cert y := { r : C & Cert r y }; LEcho linear/affine and weaken := collapse_to_residue match EchoLinear; tp_echo_1 proves affine_weakening echo_true = affine_weakening echo_false; tp_echo_2 proves ~ { reify : LEcho affine -> LEcho linear & forall e, reify (affine_weakening e) = e }; tp_echo_3 inhabits { s1 : SurfaceTy & { s2 : SurfaceTy & ((erase s1 = erase s2) * (s1 <> s2))%type } } over Type-valued sigT and prod. Auxiliary lemmas affine_typing_proof_irrelevant and subsume_coherent are also proven via pure CIC convoy match with zero axioms.",
           "evidence": {
             "kind": "ci-receipt",
-            "commit": "8bdfd5a69a6bc34dcf1faa19ad617aaea0edd158",
-            "date": "2026-11-02",
-            "run": "https://github.com/hyperpolymath/nextgen-typing/actions/runs/41539844452",
+            "commit": "c4ea39721d7ba893478fe57b5f749a89f2996508",
+            "date": "2026-11-03",
+            "run": "https://github.com/hyperpolymath/nextgen-typing/actions/runs/41565790232",
             "assumptions_output": "$ coqchk -Q . \"\" -silent -o EchoTyping\nCONTEXT SUMMARY\n===============\n* Theory: Set is predicative\n* Axioms: <none>\n* Constants/Inductives relying on type-in-type: <none>\n* Constants/Inductives relying on unsafe (co)fixpoints: <none>\n* Inductives whose positivity is assumed: <none>\n$ Print Assumptions EchoTyping.tp_echo_1.\nClosed under the global context\n$ Print Assumptions EchoTyping.tp_echo_2.\nClosed under the global context\n$ Print Assumptions EchoTyping.tp_echo_3.\nClosed under the global context"
           },
           "api_receipt": null,
@@ -284,9 +293,9 @@
           "statement_compared": "Compared anchor-by-anchor against verification/proofs/agda/EchoTyping.agda (PROOF-POLICY §2.2): EchoTyping.tp_echo_1, EchoTyping.tp_echo_2, and EchoTyping.tp_echo_3 use Type-valued PSigma and PProd (never Prop-truncated Exists/And) over core Lean Eq; because Lean's Prop Eq has definitional proof irrelevance whereas Agda's --without-K _≡_ is proof-relevant in Set, EchoTyping.lean §4 also proves EchoTyping.tp_echo_1_path, EchoTyping.tp_echo_2_path, and EchoTyping.tp_echo_3_path over a Type-valued Martin-Löf identity type Path with Sigma, Prod, and Empty, confirming zero reliance on UIP/K, propext, Quot.sound, or Classical.choice.",
           "evidence": {
             "kind": "ci-receipt",
-            "commit": "8bdfd5a69a6bc34dcf1faa19ad617aaea0edd158",
-            "date": "2026-11-02",
-            "run": "https://github.com/hyperpolymath/nextgen-typing/actions/runs/41539844452",
+            "commit": "c4ea39721d7ba893478fe57b5f749a89f2996508",
+            "date": "2026-11-03",
+            "run": "https://github.com/hyperpolymath/nextgen-typing/actions/runs/41565790232",
             "assumptions_output": "'EchoTyping.tp_echo_1' does not depend on any axioms\n'EchoTyping.tp_echo_2' does not depend on any axioms\n'EchoTyping.tp_echo_3' does not depend on any axioms\n'EchoTyping.tp_echo_1_path' does not depend on any axioms\n'EchoTyping.tp_echo_2_path' does not depend on any axioms\n'EchoTyping.tp_echo_3_path' does not depend on any axioms"
           },
           "api_receipt": null,
diff --git a/www/.well-known/humans.txt b/www/.well-known/humans.txt
index 105f211..a147fdf 100644
--- a/www/.well-known/humans.txt
+++ b/www/.well-known/humans.txt
@@ -7,8 +7,8 @@ Contact: j.d.a.jewell@open.ac.uk
 From: United Kingdom
 
 /* SITE */
-Last update: 2026-08-05
+Last update: 2026-11-03
 Standards: RSR (Rhodium Standard Repository)
 License: MPL-2.0 (Palimpsest MPL)
-Components: Idris2 ABI, Zig FFI
-Tools: just, Podman, Guix
+Components: Type-research coordination, Agda/Rocq/Lean 4 cross-project proofs
+Tools: just, Agda, Rocq, Lean 4, Graphviz, Guix
diff --git a/www/.well-known/security.txt b/www/.well-known/security.txt
index 9682a51..1152b35 100644
--- a/www/.well-known/security.txt
+++ b/www/.well-known/security.txt
@@ -2,10 +2,13 @@
 # RFC 9116 - security.txt
 # https://securitytxt.org/
 
-Contact: mailto:{{SECURITY_EMAIL}}
-Expires: 2026-12-31T23:59:59.000Z
-Encryption: {{PGP_KEY_URL}}
+# No Encryption: field. RFC 9116 §2.5.4 requires it to point at an actual key;
+# the estate signs with SSH (gpg.format=ssh) and publishes no PGP key.
+# Report privately via GitHub Security Advisories or the contact address below.
+
+Contact: https://github.com/hyperpolymath/nextgen-typing/security/advisories/new
+Contact: mailto:j.d.a.jewell@open.ac.uk
+Expires: 2027-12-31T23:59:59.000Z
 Preferred-Languages: en
-Canonical: https://github.com/hyperpolymath/nextgen-typing/.well-known/security.txt
-Policy: https://github.com/hyperpolymath/nextgen-typing/blob/main/SECURITY.md
-Hiring: https://{{WEBSITE}}/careers
+Canonical: https://github.com/hyperpolymath/nextgen-typing/blob/main/www/.well-known/security.txt
+Policy: https://github.com/hyperpolymath/nextgen-typing/blob/main/.github/SECURITY.md