resolve OQ-001 (A): coordinator + verification host — drop redundant src/ ABI/FFI scaffold (#56)

## Summary — resolves OQ-001 (option A)

nextgen-typing's long-standing identity contradiction (OQ-001:
"docs-only coordinator, no compiler code" **vs** an in-tree RSR ABI/FFI
scaffold) is resolved as **coordination monorepo + cross-project
verification host** — *not* an ABI/compiler repo.

The evidence made the call clear:
`src/interface/Abi/{Types,Layout,Foreign}.idr` was a strict **subset**
of the fuller canonical `verification/proofs/idris2/ABI/`
(Compliance/Platform/Pointers/Layout/Foreign + Types), plus a redundant
`src/interface/ffi/` Zig duplicate and **committed Idris build
artifacts** (`src/interface/build/ttc/…`). So the scaffold was redundant
template residue.

## Changes
- **Dropped the `src/` RSR scaffold** (45 files): redundant ABI subset,
Zig FFI duplicate, committed `.ttc`/`.ttm` build artifacts, and
`src/{aspects,bridges,contracts,core,definitions,errors}` manifest
stubs. The canonical proofs in `verification/proofs/` are untouched.
- **Justfile**: removed the `src/interface/{Abi,ffi,generated}`
existence checks from `validate-rsr` and the `self-assess` structure
report. Bonus: fixed stale root→`6a2/` paths in `validate-rsr`'s
required-file + META-axis checks (left dead by the #34 migration).
`proof-check-idris2` already targets `verification/proofs/` — untouched.
- **`.gitignore`**: added `*.ttc`, `*.ttm`, `zig-out/`.
- **Identity reconciled**: README.adoc + EXPLAINME.adoc now state "does
not contain compiler or application code; it documents and coordinates
the pipeline, and hosts the cross-project formal-verification proofs in
`verification/proofs/`." STATE.a2ml marks **OQ-001 resolved**, `phase =
"coordination + verification-host"`.

## Safety
No CI workflow or Justfile recipe executes the dropped `src/` paths
(verified — `e2e.yml`/`workflow-linter.yml` only use `src/**` as benign
trigger/lang-detection globs). `.claude/` doesn't exist in this repo.
STATE parses as TOML.

## Follow-ups (filed as issues, not in this PR)
1. **Proof-CI**: nothing currently builds `verification/proofs/` — a
real proof-CI needs agda+stdlib (+echo-types lib), lean4, coq, idris2
toolchains. This is the key next step to make the "verification host"
identity enforced rather than asserted.
2. **Doc sweep**: 6 docs (e.g. `docs/developer/ABI-FFI-README.adoc` — a
stale stub with an unfilled `{{~ ~}}` token) still mention
`src/interface/Abi`; retarget to `verification/proofs/` or drop the
ABI/FFI authoring docs.

🤖 Draft — opened for review.

https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ

---
_Generated by [Claude
Code](https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.gitignore

@@ -112,3 +112,8 @@ deps/
 .cache/
 build/
 dist/
+
+# Idris2 compiled artifacts (verification/proofs/idris2) + Zig build output
+*.ttc
+*.ttm
+zig-out/

.machine_readable/6a2/STATE.a2ml

@@ -6,7 +6,7 @@
 [metadata]
 project = "nextgen-typing"
 version = "0.1.0"
-last-updated = "2026-06-12"
+last-updated = "2026-06-15"
 status = "active"
 
 [project-context]
@@ -18,15 +18,16 @@ Hosts cross-repo architecture docs, pipeline roadmap, and research artefacts tha
 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), and the
-# repo still carries an un-rescoped RSR code scaffold (src/interface/,
-# verification/proofs/). Maturity reflects scaffold/early state, not a finished
-# coordination layer. Recalibration retained at the 2026-06-12 checkpoint: work
-# landed since #31 is CI/governance/docs only — it does not move the scaffold needle.
+# 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.
 completion-percentage = 10
 
 [position]
-phase = "scaffold"
+phase = "coordination + verification-host"
 maturity = "scaffold"
 
 [route-to-mvp]
@@ -55,7 +56,7 @@ summary = [
 
 [blockers-and-issues]
 issues = [
-  { id = "OQ-001", kind = "open-question", status = "open", raised = "2026-06-05", 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." },
+  { 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)." },
 ]
 

EXPLAINME.adoc

@@ -8,7 +8,9 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 == What This Is
 
 `nextgen-typing` is the **coordination monorepo** for the hyperpolymath type
-theory pipeline.  It does not contain compiler code.  It documents, connects,
+theory pipeline.  It does not contain compiler or application code; it
+documents and coordinates the pipeline, and hosts the cross-project
+formal-verification proofs in `verification/proofs/`.  It documents, connects,
 and tracks the pipeline:
 
 ----

Justfile

@@ -419,24 +419,6 @@ 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."
-    fi
-
     if $HAS_API && [ -f ".machine_readable/integrations/groove.a2ml" ]; then
         PORT=$(grep '(port ' .machine_readable/integrations/groove.a2ml 2>/dev/null | sed 's/.*(port \([0-9]*\)).*/\1/')
         if [ "$PORT" = "0" ]; then
@@ -1053,30 +1035,24 @@ 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/6a2/STATE.a2ml .machine_readable/6a2/META.a2ml .machine_readable/6a2/ECOSYSTEM.a2ml .machine_readable/6a2/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
         [ -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
     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/6a2/META.a2ml" ]; then
+        grep -q 'axis-1 = "must > intend > like"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:axis-1"
+        grep -q 'axis-2 = "corrective > adaptive > perfective"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:axis-2"
+        grep -q 'axis-3 = "systems > compliance > effects"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:axis-3"
+        grep -q 'scoping-first = true' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:scoping-first"
+        grep -q 'idris-unsound-scan = "believe_me/assert_total"' .machine_readable/6a2/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/6a2/META.a2ml || MISSING="$MISSING META.a2ml:audit-focus"
+        grep -q 'compliance-focus = "seams/compromises/exception register, bounded exceptions, anti-drift checks"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:compliance-focus"
+        grep -q 'effects-evidence = "benchmark execution/results and maintainer status dialogue/review"' .machine_readable/6a2/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"

README.adoc

@@ -16,7 +16,9 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 `nextgen-typing` is the coordination monorepo for the hyperpolymath type
 theory research and production pipeline.  It does not contain compiler
-code.  It documents relationships between type-theoretic repos, tracks
+or application code; it documents and coordinates the pipeline, and hosts
+the cross-project formal-verification proofs in `verification/proofs/`.
+It documents relationships between type-theoretic repos, tracks
 the pipeline roadmap, and hosts research artefacts that span multiple projects.
 
 == The Main Chain