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

Per owner directive 2026-05-30, arghda-core is not close enough to
echo-types' logic to justify living in-tree. 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`.

What this PR does
=================

* Delete arghda-core/ (12 files, ~1450 LOC of Rust).
* Delete docs/arghda-spec.adoc — moved to the new repo at
  docs/arghda-spec.adoc (same content; verbatim copy committed
  there separately).
* Drop the in-tree integration trail in 7 supporting files:
  * .gitignore — drop the `arghda-core/target/` line
  * 0-AI-MANIFEST.a2ml — drop `arghda-core/` from the agent-may
    edit allowlist
  * QUICKSTART-DEV.adoc — drop the `rust (for arghda-core/)`
    dev-dependency
  * TOPOLOGY.adoc — drop the `arghda-core/` tree-diagram line
  * CLAUDE.md ecosystem block — point at the new repo URL +
    note the 2026-05-30 extraction date
  * flake.nix — drop pkgs.{rustc,cargo,rustfmt,clippy} from the
    devShell (no Rust crate remains in this repo); update the
    PINNING DECISION block to record the extraction
  * docs/echo-types/MAP.adoc §Tooling — replace the in-tree
    ArghDA `[REAL*]` block with an external pointer to the new
    repo
  * contractiles/Mustfile.a2ml — drop the `rust-compiles` must
    rule; narrow the `spdx-headers` must rule from
    `find proofs arghda-core ... '*.agda' -o '*.rs'` to
    `find proofs ... '*.agda'`
  * contractiles/Dustfile.a2ml — narrow the `clean-build`
    command to drop the `rm -rf arghda-core/target` half
  * audits/assail-classifications.a2ml — drop the now-stale
    UnboundedAllocation entry for
    arghda-core/src/lint/orphan_module.rs (the file no longer
    lives here); rewrite the metadata `notes` to record the
    extraction; keep the `flake.nix` SupplyChain entry
    untouched

What this PR deliberately leaves
=================================

The four remaining `arghda` mentions in the tree are 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
=========

* Agda suite unaffected — no Agda files moved. Verified clean
  against post-#158 main tip earlier this session.
* `find proofs -name '*.agda' | xargs grep -L 'SPDX-License-Identifier'`
  still passes (the narrowed spdx-headers must rule).
* Devshell `rustc` / `cargo` no longer present — anyone working on
  Rust would do so in the standalone arghda-core repo, which has
  its own flake/CI.

Refs
====

* Extraction record: echo-types#159
* New repo: https://github.com/hyperpolymath/arghda-core
* Spec moved to: arghda-core/docs/arghda-spec.adoc (in the new repo)

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