docs: corpus subsystem guide + 2026-04-28 ADR + 6a2 sync + Justfile recipes

Closing the documentation arc on the N-dim corpus push. Files:

* `docs/CORPUS.md` — user-facing guide for the corpus subsystem:
  CLI surface, query DSL, octad shape, cross-prover semantics,
  limitations, end-to-end verified fixtures.
* `docs/decisions/2026-04-28-corpus-and-design-search.md` — ADR-style
  record covering D1–D7: design problems vs tactic problems, SA →
  swarm progression, the honest-energy lesson, capability-first
  ordering, the 6-step N-dim plan, hashing-trick → GNN trade-off,
  Bennettian/Landauer caveat with the cross-reference to echo-types'
  own thermo work.
* `.machine_readable/6a2/STATE.a2ml` — appended
  `[session-2026-04-28-corpus-and-design-search]` block recording
  commits, modules, CLI verbs, design-problems, recommendations,
  fixtures, test posture, remaining-open. The full proof-direction
  log lives there + in the ADR.
* `.machine_readable/6a2/META.a2ml` — version 2.1.1 → 2.2.0,
  last-updated → 2026-04-28, completion 92% → 94%, phase line
  reflects the new corpus + design-search + swarm.
* `.machine_readable/6a2/ECOSYSTEM.a2ml` — version 0.2.0 → 0.3.0;
  `verisimdb` upgraded from `planned-integration` to
  `active-integration` (octad emit verified); added `echo-types` as
  `active-consumer`, `januskey/reversible-core` as
  `planned-integration`, `jtv` and `eclexia` as `indexed`.
* `.machine_readable/contractiles/intend/Intentfile.a2ml` — Purpose
  block extended with the corpus + 8-modality octad + design-search
  + swarm declaration so `intend` reflects current scope.
* `.gitignore` — added `data/corpus/*.octads.jsonl` (regenerable from
  the JSON index via `corpus export-octads`).
* `Justfile` — added `corpus-ingest-{agda,coq,lean,idris}`,
  `corpus-impact`, `corpus-near`, `corpus-cross`, `corpus-octads`,
  `design-search`, `design-swarm` recipes.

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

Author: hyperpolymath

.gitignore

@@ -199,3 +199,4 @@ dist/
 
 # Generated corpus indices (rebuilt with `echidna corpus ingest`)
 data/corpus/*.json
+data/corpus/*.octads.jsonl

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -4,8 +4,8 @@
 # ECOSYSTEM.a2ml — Ecosystem position for echidna
 
 [metadata]
-version = "0.2.0"
-last-updated = "2026-04-11"
+version = "0.3.0"
+last-updated = "2026-04-28"
 project = "echidna"
 ecosystem = "hyperpolymath"
 
@@ -26,9 +26,13 @@ type = "component"
 projects = [
   { name = "proven-servers (nesy-solver-api)", relationship = "consumer", notes = "nesy-solver-api calls /api/verify on echidna-nesy.flycast:8090. Cold-start grace 90s." },
   { name = "hypatia", relationship = "sibling-neurosym", notes = "Hypatia performs neurosymbolic CI scanning; echidna does theorem proving. Both are Tier 2 formal verification tools." },
-  { name = "verisimdb", relationship = "planned-integration", notes = "Proof attempt results should feed VeriSimDB for longitudinal tracking." },
+  { name = "verisimdb", relationship = "active-integration", notes = "Corpus emits 8-modality octads (corpus/octad.rs) compatible with /api/v1/octads. Round-trip verified; HTTP push deferred." },
   { name = "neural-foundations", relationship = "monorepo-satellite", notes = "echidna is mirrored as a submodule/satellite inside neural-foundations." },
   { name = "maa-framework", relationship = "sibling", notes = "Absolute-zero and related MA/ML tools in same neurosymbolic tier." },
+  { name = "echo-types", relationship = "active-consumer", notes = "Echidna's design-search drove the Phase 1.3 _≤_ redesign + unbudgeted wf-<ᵇʳᶠ rank-function recommendations. Handoff document at echo-types/docs/echidna-design-search-2026-04-28.adoc. 640 entries indexed." },
+  { name = "januskey/reversible-core", relationship = "planned-integration", notes = "Bennettian reversibility substrate for the SA annealer trace ledger. Not yet wired." },
+  { name = "jtv (Lean 4)", relationship = "indexed", notes = "147 entries verified during Lean adapter rollout." },
+  { name = "eclexia (Idris 2 ABI)", relationship = "indexed", notes = "93 entries verified during Idris 2 adapter rollout." },
 ]
 
 [deployment]

.machine_readable/6a2/META.a2ml

@@ -8,14 +8,20 @@ full-name = "Extensible Cognitive Hybrid Intelligence for Deductive Neural Assis
 author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
 license = "PMPL-1.0-or-later"
 standard = "RSR 2026"
-version = "2.1.1"
-last-updated = "2026-04-20"
+version = "2.2.0"
+last-updated = "2026-04-28"
 status = "active"
 
 [project-context]
 name = "echidna"
-completion-percentage = 92
-phase = "v2.1.1 - Production Ready"
+completion-percentage = 94
+phase = "v2.2.0 — N-dim corpus + design-search + swarm landed"
+notes = """
+2026-04-28: corpus subsystem expanded into an N-dimensional / 8-
+modality / cross-prover index, with simulated-annealing design-search
+and 007 swarm dispatcher driving it. See docs/CORPUS.md and
+docs/decisions/2026-04-28-corpus-and-design-search.md.
+"""
 
 [dependencies]
 primary = ["Rust", "Julia", "ReScript", "Idris2", "Zig"]

.machine_readable/6a2/STATE.a2ml

@@ -1112,3 +1112,77 @@ remaining-open = [
   "Stage 1c extractor premise gaps (28/50, in-flight)",
   "Stage 8 E10-E13 proofs + SPARK kernel (Opus design session needed)",
 ]
+
+[session-2026-04-28-corpus-and-design-search]
+date = "2026-04-28"
+summary = """
+Built the project-corpus indexer + simulated-annealing design-search +
+007 swarm dispatcher + rank-function search, then expanded the corpus
+into an N-dimensional / 8-modality / cross-prover index per the
+VeriSim octad shape. Eleven commits in echidna; one in echo-types
+(handoff document for the Phase 1.3 + unbudgeted wf-<ᵇʳᶠ proof
+campaign).
+"""
+commits-pushed = [
+  "85c2b55 feat(corpus): project-corpus indexer + Agda adapter + ordinal/WF synonyms",
+  "ae68579 feat(learning): SA design-search — proof-design space, not tactic space",
+  "fca18d5 feat(agent): swarm dispatcher + SA energy refinement",
+  "ca56b96 feat(learning): rank-function search for unbudgeted wf-<ᵇʳᶠ_",
+  "e599868 feat(corpus): reverse-dep index — Step 1 of N-dim VeriSim plan",
+  "572b9b7 feat(corpus): Coq + Lean 4 + Idris 2 adapters; cross-prover semantic classes",
+  "8604909 feat(corpus): 8-modality octad emission — Step 3 of N-dim plan",
+  "3148d14 feat(corpus): tensor-octad metrics — Step 4 of N-dim plan",
+  "4558e61 feat(corpus): vector-octad embeddings — Step 5 of N-dim plan",
+  "8265f9b feat(corpus): multi-axis query DSL — N-dim plan capstone",
+]
+new-modules = [
+  "src/rust/corpus/{mod,agda,coq,lean,idris2,metrics,embed,octad,query}.rs",
+  "src/rust/learning/{design_search,buchholz_rank}.rs",
+  "src/rust/agent/swarm.rs",
+]
+new-cli-verbs = [
+  "echidna corpus ingest --root <path> --adapter <agda|coq|lean|idris2>",
+  "echidna corpus query <pattern> [--deps] [--reverse-deps] [--reverse-closure]",
+  "echidna corpus near \"<text>\" [--top N]",
+  "echidna corpus crossquery <semantic-class>",
+  "echidna corpus export-octads --index <X.json> --out <X.octads.jsonl>",
+  "echidna corpus import-octads --octads <X.octads.jsonl> --out <X.json>",
+  "echidna corpus stats [--index <X.json>]",
+  "echidna design search <problem> [--iterations N] [--top K]",
+  "echidna design swarm <problem> [--agents N] [--broadcast-every N]",
+]
+design-problems-available = [
+  "brouwer-leq — Phase 1.3 _≤_ redesign",
+  "buchholz-rank — unbudgeted wf-<ᵇʳᶠ rank function",
+]
+recommendations-issued = """
+Phase 1.3: switch Ordinal.Brouwer._≤_ to a recursive definition.
+Energy [0, 0, 1, 0]; SA + 4-agent swarm both unanimous.
+
+Unbudgeted wf-<ᵇʳᶠ_: rank shape
+  rank bzero        = oz
+  rank (bOmega ν)   = ω-rank ν
+  rank (bplus x y)  = rank x ⊕ rank y
+  rank (bpsi ν α)   = psi-rank ν (rank α)
+Energy [3, 0, 1]; three downstream blockers (Phase-2.2 rank-mono-<ᵇ,
+⊕-mono-<-right twice). Closes via Subrelation.wellFounded chain.
+
+Handoff document: echo-types/docs/echidna-design-search-2026-04-28.adoc
+"""
+verified-fixtures = [
+  "echo-types/proofs/agda — 57 modules / 640 entries (Agda)",
+  "echidna/proofs/coq — 5 modules / 108 entries (Coq)",
+  "jtv/jtv_proofs — 7 modules / 147 entries (Lean 4)",
+  "eclexia/src/abi — 4 modules / 93 entries (Idris 2)",
+]
+test-posture = "1059 lib tests pass (16 added). 0 failures, 2 ignored (pre-existing)."
+remaining-open = [
+  "Apply recommendation to Agda — Phase 1.3 redesign + Σ-elim rewrite (multi-session)",
+  "Wire SA energy in learning/buchholz_rank::blockers to consume the corpus query DSL (~1d)",
+  "Reversibility integration with januskey/reversible-core::ContentStore for SA trace ledger",
+  "GNN embeddings via Julia /gnn/embed (deferred ML training column)",
+]
+new-docs = [
+  "docs/CORPUS.md — user-facing guide for the corpus subsystem",
+  "docs/decisions/2026-04-28-corpus-and-design-search.md — ADR record",
+]

.machine_readable/contractiles/intend/Intentfile.a2ml

@@ -9,8 +9,17 @@ Declared intent and purpose for Echidna.
 ## Purpose
 
 Echidna is a trust-hardened neurosymbolic theorem proving platform.
-It supports 48 prover backends, records every proof attempt to VeriSimDB,
-and feeds the Hypatia learning loop so the fleet gets smarter over time.
+It supports 128 prover backends, records every proof attempt to
+VeriSimDB, and feeds the Hypatia learning loop so the fleet gets
+smarter over time.
+
+As of 2026-04-28, Echidna also operates a project-corpus indexer with
+adapters for Agda, Coq, Lean 4, and Idris 2; emits 8-modality
+declaration octads compatible with VeriSim's `/api/v1/octads`; and
+runs simulated-annealing design-search + 007-style swarm dispatchers
+over candidate axiomatisations and rank functions. See
+`docs/CORPUS.md` and `docs/decisions/2026-04-28-corpus-and-design-
+search.md`.
 
 ## Anti-Purpose
 

Justfile

@@ -830,3 +830,48 @@ crg-badge:
       D) color="orange" ;; E) color="red" ;; F) color="critical" ;; \
       *) color="lightgrey" ;; esac; \
     echo "[![CRG $$grade](https://img.shields.io/badge/CRG-$$grade-$$color?style=flat-square)](https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades)"
+
+
+# ────────────────────────────────────────────────────────────────────
+# Corpus + design-search (added 2026-04-28)
+# ────────────────────────────────────────────────────────────────────
+
+# Ingest an Agda project into the corpus
+corpus-ingest-agda root:
+    cargo run --bin echidna -- corpus ingest --root {{root}} --adapter agda
+
+# Ingest a Coq project into the corpus
+corpus-ingest-coq root:
+    cargo run --bin echidna -- corpus ingest --root {{root}} --adapter coq
+
+# Ingest a Lean 4 project into the corpus
+corpus-ingest-lean root:
+    cargo run --bin echidna -- corpus ingest --root {{root}} --adapter lean
+
+# Ingest an Idris 2 project into the corpus
+corpus-ingest-idris root:
+    cargo run --bin echidna -- corpus ingest --root {{root}} --adapter idris2
+
+# Query the corpus by name with full reverse-dep impact set
+corpus-impact name index="data/corpus/agda.json":
+    cargo run --bin echidna -- corpus query "{{name}}" --index {{index}} --reverse-closure
+
+# Cosine-similarity nearest-neighbour query
+corpus-near query index="data/corpus/agda.json" top="10":
+    cargo run --bin echidna -- corpus near "{{query}}" --index {{index}} --top {{top}}
+
+# Cross-prover semantic-class lookup
+corpus-cross class:
+    cargo run --bin echidna -- corpus crossquery {{class}}
+
+# Export a JSON index as 8-modality octad JSONL (VeriSim-compatible)
+corpus-octads in="data/corpus/agda.json" out="data/corpus/agda.octads.jsonl":
+    cargo run --bin echidna -- corpus export-octads --index {{in}} --out {{out}}
+
+# Run the SA design-search on a named problem
+design-search problem="brouwer-leq" iterations="2000" top="10":
+    cargo run --bin echidna -- design search {{problem}} --iterations {{iterations}} --top {{top}}
+
+# Run the parallel-swarm design-search
+design-swarm problem="brouwer-leq" agents="4" iterations="800":
+    cargo run --bin echidna -- design swarm {{problem}} --agents {{agents}} --iterations {{iterations}} --broadcast-every 50