governance: enforce coordination-repo boundary so bots stop dumping project code

nextgen-typing is the coordination monorepo (no compiler/application code), but
its bot-facing steering still carried RSR-template instructions to put ABI/FFI
code in src/interface/ and to "add proofs here". The repo's identity files said
one thing while the files agents actually read said another, so agents kept
landing typing-project content here instead of in the constituent repos.

Prevention (correct boundary at every surface agents actually read):
- add root AGENTS.md + CLAUDE.md and root .clinerules/.cursorrules/.windsurfrules
  carrying the placement boundary + a routing table (none existed before)
- add .machine_readable/bot_directives/placement.a2ml as the authoritative,
  machine-readable routing table; reference it from 0-AI-MANIFEST.a2ml,
  AI-CONVENTIONS.adoc, AGENTIC.a2ml and bot_directives/README.adoc
- strip the src/interface ABI/FFI instructions from copilot-instructions.md,
  the .machine_readable/ai/ rule files and AI-CONVENTIONS.adoc
- rewrite the template-residue AI.a2ml (it still called the repo rsr-template-repo)

Enforcement:
- add scripts/check-coordination-boundary.sh + the coordination-boundary.yml
  workflow + a pre-commit hook: fail when project code or a non-allowlisted
  proof appears in the coordination repo

Resite / cleanup:
- remove the RSR ABI/TP proof scaffold from verification/proofs/ (those
  obligations belong in typed-wasm/typell); keep the genuinely cross-project
  echo-types proof (EchoTyping + Verification aggregator)
- reconcile PROOF-NEEDS.md, PROOF-STATUS.md and verification/proofs/README.adoc
  to coordination reality; record the change in STATE.a2ml

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X2UKV63H4584CQ66qdgxZy

Author: claude

.clinerules

@@ -0,0 +1,24 @@
+# SPDX-License-Identifier: MPL-2.0
+# Cline rules for nextgen-typing. Full rules: AGENTS.md / CLAUDE.md.
+
+# ⛔ COORDINATION REPO — NOT A CODE REPO.
+# nextgen-typing documents and connects the type-theory pipeline
+# (katagoria → typell → typed-wasm → PanLL). It does NOT hold compiler,
+# kernel, language, or single-project code — including single-project proofs,
+# benchmarks, and tests.
+#
+# Before creating ANY implementation file or single-project proof here: STOP.
+# Put it in the owning repo. Routing table:
+#   .machine_readable/bot_directives/placement.a2ml   (authoritative)
+#   AGENTS.md                                          (human-readable)
+# CI enforces this: scripts/check-coordination-boundary.sh
+#
+# Only these belong here: coordination/architecture docs, .machine_readable/
+# state, estate governance/CI scaffold, and CROSS-project proofs in
+# verification/proofs/ that import >=2 constituent repos (e.g. agda/EchoTyping.agda).
+
+# Then: read 0-AI-MANIFEST.a2ml, then .machine_readable/6a2/STATE.a2ml.
+# Licence MPL-2.0 (never AGPL) + SPDX header on every file.
+# Banned langs: TypeScript->ReScript, npm/Node->Deno, Go->Rust, Python->Julia/Rust.
+# Containers: Podman + Containerfile. Build via just.
+# No believe_me / assert_total / postulate / sorry / Admitted / unsafeCoerce.

.cursorrules

@@ -0,0 +1,24 @@
+# SPDX-License-Identifier: MPL-2.0
+# Cursor rules for nextgen-typing. Full rules: AGENTS.md / CLAUDE.md.
+
+# ⛔ COORDINATION REPO — NOT A CODE REPO.
+# nextgen-typing documents and connects the type-theory pipeline
+# (katagoria → typell → typed-wasm → PanLL). It does NOT hold compiler,
+# kernel, language, or single-project code — including single-project proofs,
+# benchmarks, and tests.
+#
+# Before creating ANY implementation file or single-project proof here: STOP.
+# Put it in the owning repo. Routing table:
+#   .machine_readable/bot_directives/placement.a2ml   (authoritative)
+#   AGENTS.md                                          (human-readable)
+# CI enforces this: scripts/check-coordination-boundary.sh
+#
+# Only these belong here: coordination/architecture docs, .machine_readable/
+# state, estate governance/CI scaffold, and CROSS-project proofs in
+# verification/proofs/ that import >=2 constituent repos (e.g. agda/EchoTyping.agda).
+
+# Then: read 0-AI-MANIFEST.a2ml, then .machine_readable/6a2/STATE.a2ml.
+# Licence MPL-2.0 (never AGPL) + SPDX header on every file.
+# Banned langs: TypeScript->ReScript, npm/Node->Deno, Go->Rust, Python->Julia/Rust.
+# Containers: Podman + Containerfile. Build via just.
+# No believe_me / assert_total / postulate / sorry / Admitted / unsafeCoerce.

.github/copilot-instructions.md

@@ -7,6 +7,18 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 # Copilot Instructions
 
+## ⛔ Before Writing Anything — Placement Boundary
+
+`nextgen-typing` is a **coordination repo**, not a code repo. Do NOT add
+compiler/application code or single-project proofs here. If content implements
+or proves something about ONE project, put it in that project's repo. Routing
+table: `.machine_readable/bot_directives/placement.a2ml` (enforced in CI by
+`scripts/check-coordination-boundary.sh`). Full guidance: `AGENTS.md`.
+
+Only these belong here: coordination/architecture docs, `.machine_readable/`
+state, estate governance/CI scaffold, and CROSS-project proofs (importing ≥2
+constituent repos) under `verification/proofs/`.
+
 ## Before Writing Code
 
 - Read `0-AI-MANIFEST.a2ml` in the repo root for canonical file locations.
@@ -47,12 +59,6 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 - Name the file `Containerfile`, never `Dockerfile`.
 - Base image: `cgr.dev/chainguard/wolfi-base:latest`.
 
-## ABI/FFI
-
-- ABI definitions in Idris2 (`src/interface/abi/`).
-- FFI implementations in Zig (`src/interface/ffi/`).
-- Generated C headers in `src/interface/generated/`.
-
 ## State Files
 
 Never create these in the repo root:

.github/workflows/coordination-boundary.yml

@@ -0,0 +1,32 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Coordination-boundary guard: nextgen-typing must stay docs + machine-readable
+# state + estate scaffold + CROSS-project proofs only — no compiler/application
+# code and no single-project proofs. Routing table:
+#   .machine_readable/bot_directives/placement.a2ml
+name: Coordination Boundary
+
+on:
+  push:
+    branches: [main, master, develop]
+  pull_request:
+    branches: [main, master, develop]
+
+permissions:
+  contents: read
+
+concurrency:
+  group: coord-boundary-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  boundary:
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    permissions:
+      contents: read
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - name: Enforce coordination boundary
+        run: bash scripts/check-coordination-boundary.sh

.machine_readable/6a2/AGENTIC.a2ml

@@ -22,6 +22,10 @@ can-create-files = true
 # - Never use banned languages (TypeScript, Python, Go, etc.)
 # - Never place state files in repository root (must be in .machine_readable/)
 # - Never use AGPL license (use MPL-2.0)
+# - Never add compiler/application code or single-project proofs to this
+#   coordination repo; route them to the owning repo per
+#   .machine_readable/bot_directives/placement.a2ml (CI-enforced by
+#   scripts/check-coordination-boundary.sh).
 
 [maintenance-integrity]
 fail-closed = true

.machine_readable/6a2/STATE.a2ml

@@ -6,7 +6,7 @@
 [metadata]
 project = "nextgen-typing"
 version = "0.1.0"
-last-updated = "2026-06-15"
+last-updated = "2026-06-19"
 status = "active"
 
 [project-context]
@@ -24,6 +24,11 @@ Does NOT contain compiler code.
 # 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
 
 [position]
@@ -84,6 +89,7 @@ events = [
   { 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." },
 ]
 
 [ecosystem]

.machine_readable/ai/.clinerules

@@ -34,10 +34,11 @@
 # File: Containerfile (never Dockerfile).
 # Base: cgr.dev/chainguard/wolfi-base:latest or cgr.dev/chainguard/static:latest.
 
-# ABI/FFI
-# ABI: Idris2 with dependent types (src/interface/abi/).
-# FFI: Zig with C ABI (src/interface/ffi/).
-# Headers: src/interface/generated/.
+# COORDINATION REPO — NO PROJECT CODE
+# nextgen-typing is coordination-only: docs, .machine_readable/ state, estate
+# scaffold, and CROSS-project proofs (>=2 constituent repos) in
+# verification/proofs/. Do NOT add compiler/app code or single-project proofs.
+# Route per .machine_readable/bot_directives/placement.a2ml (CI-enforced).
 
 # BUILD: Use just (justfile) for all tasks.
 # STYLE: Descriptive names. Document all files. SPDX headers everywhere.

.machine_readable/ai/.cursorrules

@@ -33,10 +33,11 @@
 # File: Containerfile (never Dockerfile)
 # Base: cgr.dev/chainguard/wolfi-base:latest
 
-# ABI/FFI STANDARD
-# ABI definitions: Idris2 with dependent types (src/interface/abi/)
-# FFI implementation: Zig with C ABI (src/interface/ffi/)
-# Generated C headers: src/interface/generated/
+# COORDINATION REPO — NO PROJECT CODE
+# nextgen-typing is coordination-only: docs, .machine_readable/ state, estate
+# scaffold, and CROSS-project proofs (>=2 constituent repos) in
+# verification/proofs/. Do NOT add compiler/app code or single-project proofs.
+# Route per .machine_readable/bot_directives/placement.a2ml (CI-enforced).
 
 # BUILD SYSTEM
 # Use just (justfile) for all build, test, lint, and format tasks.

.machine_readable/ai/.windsurfrules

@@ -34,10 +34,11 @@
 # File: Containerfile (never Dockerfile).
 # Base: cgr.dev/chainguard/wolfi-base:latest or cgr.dev/chainguard/static:latest.
 
-# ABI/FFI
-# ABI: Idris2 with dependent types (src/interface/abi/).
-# FFI: Zig with C ABI (src/interface/ffi/).
-# Headers: src/interface/generated/.
+# COORDINATION REPO — NO PROJECT CODE
+# nextgen-typing is coordination-only: docs, .machine_readable/ state, estate
+# scaffold, and CROSS-project proofs (>=2 constituent repos) in
+# verification/proofs/. Do NOT add compiler/app code or single-project proofs.
+# Route per .machine_readable/bot_directives/placement.a2ml (CI-enforced).
 
 # BUILD: Use just (justfile) for all tasks.
 # STYLE: Descriptive names. Document all files. SPDX headers everywhere.

.machine_readable/ai/AI.a2ml

@@ -1,38 +1,38 @@
 # SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
-# AI Assistant Instructions
+# AI Assistant Instructions — nextgen-typing
 
-## Repository Focus
-- `rsr-template-repo` is treated as a Rhodium Standard Repository; obey the Rhodium policies and keep `.machine_readable/` authoritative.
-- All machine-readable content lives under `.machine_readable/` — state files (a2ml), bot directives, and contractiles.
-- Prefer to keep generated files out of source control, and regenerate them with the documented commands before committing.
+## ⛔ Placement Boundary (read first)
+
+nextgen-typing is the **coordination repo** for the type-theory pipeline
+(katagoria → typell → typed-wasm → PanLL). It is NOT a code repo: no compiler,
+kernel, language, or single-project code — and no single-project proofs,
+benchmarks, or tests.
+
+If content implements or proves something about ONE project, it belongs in that
+project's repo. Use the routing table:
+- `.machine_readable/bot_directives/placement.a2ml` (authoritative, CI-enforced)
+- `AGENTS.md` / `CLAUDE.md` (human-readable)
+
+Only these belong here: coordination/architecture docs, `.machine_readable/`
+state, estate governance/CI scaffold, and CROSS-project proofs (importing ≥2
+constituent repos) under `verification/proofs/`.
 
 ## Workflow
-1. Inspect `.machine_readable/6a2/STATE.a2ml` for blockers and next actions.
-2. Respect any constraints listed inside `.machine_readable/AGENTIC.a2ml` when tooling changes are requested.
-3. After finishing edits, update STATE with your outcomes and commit with a concise, imperative message.
-
-## Delivery Promises
-- Mention in summaries whether STATE, `.machine_readable/contractiles/`, or `.machine_readable/bot_directives/` changed.
-- Keep this file in sync with the repository's status; update it if the governance changes.
-
-[foundational-integrations]
-# These tools form the architectural floor for all hyperpolymath repos.
-# Integrate them incrementally as the project matures.
-
-proven = "Formally verified safety library — replace raw string/JSON/URL/crypto ops"
-panic-attacker = "Static analysis — run `just assail` before every commit"
-feedback-o-tron = "Autonomous bug filing — auto-report upstream dependency failures"
-verisimdb = "Cross-repo analytics — emit scan results and build metrics"
-vexometer = "Irritation surface analysis — measure friction in CLI/UI tools"
-hypatia = "Neurosymbolic CI/CD — safety-triangle routing for automated fixes"
-boj-server = "MCP gateway — all external service integrations route through BoJ"
-
-[floor-raise-checklist]
-step-1 = "Ensure 0-AI-MANIFEST.a2ml exists at repo root"
-step-2 = "Ensure Mustfile.a2ml + Trustfile.a2ml + Dustfile.a2ml in .machine_readable/contractiles/"
-step-3 = "Add `assail` recipe to Justfile and wire into pre-commit hook"
-step-4 = "Add proven integration reference in .machine_readable/integrations/"
-step-5 = "Add verisimdb feed configuration"
-step-6 = "Add feedback-o-tron integration for upstream reporting"
-step-7 = "Add vexometer hooks for friction measurement (CLI/UI repos)"
+
+1. Read `0-AI-MANIFEST.a2ml`, then `.machine_readable/6a2/STATE.a2ml` for
+   blockers and next actions.
+2. Respect `.machine_readable/6a2/AGENTIC.a2ml` constraints.
+3. Before creating any file, confirm placement against `placement.a2ml`.
+4. After edits, update STATE with outcomes; commit with a concise message.
+
+## Conventions
+
+- Licence MPL-2.0 + SPDX header on every file (never AGPL).
+- `.a2ml` state files live in `.machine_readable/` only, never the repo root.
+- Banned languages: TypeScript→ReScript, npm/Node→Deno, Go→Rust, Python→Julia/Rust.
+- Containers: Podman + `Containerfile`. Build/test via `just`.
+- No unsound escape hatches: believe_me, assert_total, postulate, sorry,
+  Admitted, unsafeCoerce, Obj.magic.
+- Full rules: `docs/practice/AI-CONVENTIONS.adoc`.