hyperpolymath · hyperpolymath · Jun 19, 2026 · Jun 19, 2026
diff --git a/.clinerules b/.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.
diff --git a/.cursorrules b/.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.
diff --git a/.github/copilot-instructions.md b/.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:

diff --git a/.github/workflows/coordination-boundary.yml b/.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
diff --git a/.machine_readable/6a2/AGENTIC.a2ml b/.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

diff --git a/.machine_readable/6a2/STATE.a2ml b/.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]

diff --git a/.machine_readable/ai/.clinerules b/.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.
diff --git a/.machine_readable/ai/.cursorrules b/.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.

diff --git a/.machine_readable/ai/.windsurfrules b/.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.
diff --git a/.machine_readable/ai/AI.a2ml b/.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`.
diff --git a/.machine_readable/bot_directives/README.adoc b/.machine_readable/bot_directives/README.adoc
@@ -38,10 +38,17 @@ interactive agents.
 
 | `debt.a2ml`
 | Meander debt — things found but not fixed, carried between sessions
+
+| `placement.a2ml`
+| Content-routing directive — WHERE content belongs in the estate. What this
+  coordination repo accepts vs what must be routed to a constituent repo.
+  Authoritative source behind AGENTS.md and the coordination-boundary CI check.
 |===
 
 == How Agents Use These
 
+0. Consult `placement.a2ml` BEFORE creating any file — confirm it belongs in a
+   coordination repo; if it implements or proves one project, route it out.
 1. Read `methodology.a2ml` at session start — know mode, invariants, ceiling
 2. Read `coverage.a2ml` — know what was visited last time, what was skipped
 3. Read `debt.a2ml` — know what's outstanding from previous sessions

diff --git a/.machine_readable/bot_directives/placement.a2ml b/.machine_readable/bot_directives/placement.a2ml
@@ -0,0 +1,83 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# placement.a2ml — content-routing directive (authoritative)
+#
+# WHERE content belongs in the type-theory estate. This is the machine-readable
+# source of truth behind AGENTS.md / CLAUDE.md and the coordination-boundary CI
+# check (scripts/check-coordination-boundary.sh). Agents MUST consult this
+# before creating files in nextgen-typing.
+
+[metadata]
+version = "1.0.0"
+last-updated = "2026-06-19"
+applies-to = "nextgen-typing"
+precedence = "maintainer > this directive > bot defaults"
+
+[identity]
+repo = "nextgen-typing"
+role = "coordination-monorepo"
+rule = """
+nextgen-typing documents and connects the type-theory pipeline
+(katagoria -> typell -> typed-wasm -> PanLL). It contains NO compiler, kernel,
+language, or single-project code -- including single-project proofs, benchmarks,
+and tests. If content implements or proves something about ONE project, it
+belongs in that project's repo, not here.
+"""
+
+# What this repo accepts. Anything not matching belongs elsewhere (see [routing]).
+[accepts]
+allowed = [
+  "Coordination & architecture docs (README, ROADMAP, TOPOLOGY, docs/ARCHITECTURE, docs/PIPELINE, docs/decisions ADRs)",
+  "Machine-readable pipeline state (.machine_readable/)",
+  "Estate governance / CI scaffold",
+  "Cross-project formal proofs in verification/proofs/ that import or relate >=2 constituent repos",
+  "Research artefacts that genuinely span multiple projects",
+]
+
+# What this repo rejects -> route to the owning repo.
+[rejects]
+disallowed = [
+  "Compiler / kernel / language implementation code",
+  "Single-project formal proofs (proofs about exactly one constituent repo)",
+  "Single-project ABI/FFI definitions, benchmarks, or tests",
+  "A code scaffold (src/, crates/, Cargo.toml) of any kind",
+]
+
+# Routing table. `owns` = the canonical repo for that subject matter.
+[routing]
+rules = [
+  { subject = "type-theory research prototypes, Idris2/Lean PoCs, reading notes", owns = "kategoria" },
+  { subject = "TypeLL kernel: dependent/linear/session types, QTT, proof-carrying code, effects", owns = "typell" },
+  { subject = "WasmGC memory-safety proofs, verified convergence ABI, aggregate-library conventions", owns = "typed-wasm" },
+  { subject = "echo-types library: fiber-based structured loss (Echo/EchoLinear/EchoResidue/EchoCharacteristic)", owns = "echo-types", companion = "EchoTypes.jl" },
+  { subject = "choreographic / multiparty session types", owns = "choreographic-types" },
+  { subject = "TypeFix Zero / micro-Type-0 calibration calculus", owns = "typefix-zero" },
+  { subject = "AffineScript language code", owns = "affinescript" },
+  { subject = "Ephapax language code / region calculus", owns = "ephapax" },
+  { subject = "query-language type safety (SQL/GraphQL/Cypher/SPARQL/VQL)", owns = "typedqliser", also = "vcl-ut" },
+  { subject = "tropical / semiring type theory (Isabelle/Lean)", owns = "tropical-resource-typing" },
+  { subject = "transport-adapter / max-plus pathfinding", owns = "protocol-squisher" },
+  { subject = "eNSAID reference env (downstream consumer of TypeLL)", owns = "panll" },
+]
+
+# Cross-project proofs are the ONLY proofs allowed in verification/proofs/.
+# A proof qualifies only if it imports/relates >=2 constituent repos. New
+# entries require a conscious decision: add the path here AND to the allowlist
+# in scripts/check-coordination-boundary.sh.
+[verification]
+cross-project-only = true
+allowed-proofs = [
+  "verification/proofs/agda/EchoTyping.agda",   # relates echo-types <-> AffineScript/typed-wasm pipeline
+  "verification/proofs/agda/Verification.agda", # aggregator that typechecks the cross-project set
+  "verification/proofs/agda/nextgen-typing.agda-lib",
+]
+route-elsewhere = [
+  "ABI/FFI/memory-layout proofs -> typed-wasm",
+  "TypeLL kernel proofs -> typell",
+  "echo-types library proofs -> echo-types",
+  "single-project type-soundness proofs -> the owning repo",
+]
+
+[on-uncertainty]
+action = "Open an issue in nextgen-typing proposing where the content should live. Do NOT commit code or single-project proofs here on spec."
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
@@ -50,3 +50,13 @@ repos:
     rev: v8.24.3
     hooks:
       - id: gitleaks
+
+  # --- Coordination boundary (this repo is coordination-only) ---
+  - repo: local
+    hooks:
+      - id: coordination-boundary
+        name: Coordination boundary (no project code / single-project proofs)
+        entry: scripts/check-coordination-boundary.sh
+        language: script
+        pass_filenames: false
+        always_run: true