chore: remove arghda-core/ subtree + cross-refs (extracted to standalone repo per #159) (#160)

## Summary

Per owner directive 2026-05-30, \`arghda-core\` is not close enough to
echo-types' logic to justify being in-tree. It's been extracted to its
own repo at https://github.com/hyperpolymath/arghda-core with full git
history preserved via \`git subtree split --prefix=arghda-core HEAD\`.

This PR completes the move on the echo-types side: delete the subtree +
the spec doc + update all 8 cross-references.

## Counterpart on the new repo

Already landed on https://github.com/hyperpolymath/arghda-core/main:

- 4 commits of historical arghda-core history preserved (subtree-split
from echo-types)
- Bootstrap: standalone-repo plumbing (Cargo.toml repo URL fixed,
.gitignore, README rewritten, smoke tests rewritten from
echo-types-relative integration to self-contained fixtures)
- CI: self-contained Rust workflow (cargo fmt + build + test + clippy -D
warnings) — verified green at
https://github.com/hyperpolymath/arghda-core/actions/runs/26684219505
- \`docs/arghda-spec.adoc\` imported from echo-types verbatim

## What this PR does

| File | Change |
|---|---|
| \`arghda-core/\` (12 files, ~1450 LOC) | Delete subtree |
| \`docs/arghda-spec.adoc\` | Delete (moved to new repo) |
| \`.gitignore\` | Drop \`arghda-core/target/\` |
| \`0-AI-MANIFEST.a2ml\` | Drop \`arghda-core/\` from agent-may
allowlist |
| \`QUICKSTART-DEV.adoc\` | Drop \`rust (for arghda-core/)\` dev-dep |
| \`TOPOLOGY.adoc\` | Drop \`arghda-core/\` tree-diagram line |
| \`CLAUDE.md\` ecosystem block | Point at new repo URL + record
2026-05-30 extraction |
| \`flake.nix\` | Drop \`pkgs.{rustc,cargo,rustfmt,clippy}\` from
devShell; PINNING-DECISION block records the extraction |
| \`docs/echo-types/MAP.adoc\` §Tooling | Replace in-tree ArghDA block
with external pointer |
| \`contractiles/Mustfile.a2ml\` | Drop \`rust-compiles\` must; narrow
\`spdx-headers\` to Agda-only |
| \`contractiles/Dustfile.a2ml\` | Drop \`rm -rf arghda-core/target\`
from \`clean-build\` |
| \`audits/assail-classifications.a2ml\` | Drop the now-stale
UnboundedAllocation entry for the orphan_module.rs file; rewrite
metadata notes; keep flake.nix SupplyChain entry |

## What this PR deliberately leaves

Four \`arghda\` mentions remain in the tree — all extraction-record
breadcrumbs by design:

- \`flake.nix\` PINNING-DECISION comment — historical context
- \`CLAUDE.md\` ecosystem-context block — points future agents at the
new repo
- \`audits/assail-classifications.a2ml\` metadata — records why the
orphan_module.rs entry left
- \`docs/echo-types/MAP.adoc\` §Tooling — external pointer

## Test plan

- [x] Agda suite unaffected — no Agda files moved. Verified clean
against post-#158 main earlier this session (All.agda + Smoke.agda +
characteristic + examples all exit 0 under \`--safe --without-K\`;
kernel-guard + check-guardrails both pass).
- [x] Narrowed \`spdx-headers\` must rule still passes (Agda-only
scope).
- [x] New repo's CI green:
https://github.com/hyperpolymath/arghda-core/actions/runs/26684219505

## Refs

- Closes #159
- New repo: https://github.com/hyperpolymath/arghda-core
- Spec moved to: \`arghda-core/docs/arghda-spec.adoc\` in the new repo

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

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

Author: hyperpolymath

.gitignore

@@ -1,5 +1,4 @@
 *.agdai
-arghda-core/target/
 .claude/
 .agda/
 

0-AI-MANIFEST.a2ml

@@ -3,7 +3,7 @@
 
 [ai-contract]
 purpose = "Constructive Agda formalisation of echo types — proof-relevant fibers / loss-with-residue. Foundation library."
-agent-may = "edit proofs/agda/, arghda-core/, docs/, CHANGELOG.md, contractiles/, .machine_readable/6a2/"
+agent-may = "edit proofs/agda/, docs/, CHANGELOG.md, contractiles/, .machine_readable/6a2/"
 agent-may-not = "edit LICENSE / SECURITY.md / [security.signing] without explicit user confirmation; introduce believe_me/assert_total/postulate/sorry/Admitted/unsafeCoerce/Obj.magic; reopen EI-2 under any framing in .machine_readable/6a2/STATE.a2ml § forbidden-rebrandings; rename ModeGraded -> ModeGrade (the trailing d is canonical)"
 agent-must-after = "code-edit -> 'just verify'"
 

CLAUDE.md

@@ -33,11 +33,13 @@ Adjacent projects, in one line each, for session bootstrapping:
   for automatic detection and integration (e.g. discipline-specific
   analyzers becoming visible to PanLL without manual wiring).
   See GROOVE_PANLL_RESEARCH_SUMMARY.md in panll.
-- ArghDA (planned) — lightweight proof-workspace manager for Agda;
+- ArghDA — lightweight proof-workspace manager for Agda;
   triage folders (inbox → working → proven/rejected), linter, DAG view.
-  Split as `arghda-core` (language-agnostic engine) + `arghda-panll`
-  (Gossamer/ReScript presentation). See docs/buchholz-plan.adoc appendix
-  for the motivating proof pipeline.
+  Split as `arghda-core` (language-agnostic engine, separate repo at
+  https://github.com/hyperpolymath/arghda-core, extracted from this
+  repo 2026-05-30 — see echo-types#159) + `arghda-panll`
+  (Gossamer/ReScript presentation, planned). See docs/buchholz-plan.adoc
+  appendix for the motivating proof pipeline.
 
 # This repo
 

QUICKSTART-DEV.adoc

@@ -9,7 +9,6 @@ Required:
 * `just`
 * `agda` (per `.tool-versions` — currently floats; pinning pending)
 * `ghc` + `cabal` (Agda runtime)
-* `rust` (for `arghda-core/`)
 * `podman` (for container builds, when `stapeln.toml` is wired)
 
 == First build

TOPOLOGY.adoc

@@ -16,7 +16,6 @@ echo-types/
 │       ├── Ordinal/             # Buchholz / Veblen track
 │       ├── examples/            # concrete usage demos
 │       └── characteristic/      # characteristic-style results (RoleGraded, etc.)
-├── arghda-core/                 # Rust crate — companion tooling (TBD scope)
 ├── docs/                        # supplementary documentation
 │   ├── EI2_REPORT.adoc          # investigation EI-2 working record
 │   ├── gate-1-distinct-phenomenon.adoc