feat(corpus): vector-octad embeddings — Step 5 of N-dim plan

Adds `corpus/embed.rs` with the `Embedder` trait and a default
`HashEmbedder` (offline feature-hashing-trick at 32 dimensions to
match the GNN local-embedding `FEATURE_DIM`). Wires embeddings into
`octad.rs::save_octads_jsonl` so the Vector modality populates with
each entry's vector, model name, and dimensions.

## Why hashing-trick first

`gnn::GnnClient::embed` is the proper backend but the Julia ML
server at port 8090 is currently scaffold-only (per CLAUDE.md:
`models/neural/` doesn't exist; cosine fallback returns zero vectors).
Hashing-trick is offline, deterministic, free, and at 32 dimensions
gives meaningful cosine similarity over shared vocabulary. Drop-in
replacement when the GNN server is primed: implement `Embedder` for
a `GnnEmbedder` and swap one trait usage in the corpus emit path.

## CLI

`echidna corpus near <query> [--index <path>] [--top K]` — embeds the
query with the same hasher, computes cosine similarity against every
entry, prints top-K by score. Verified end-to-end on echo-types:
`corpus near "WellFounded" --top 5` returns a plausible neighbourhood
(CNO-Echo entries score 0.85, declining ranks below). At 32 dims
collisions are common; real GNN embeddings will sharpen this.

## What this unblocks

* SA / MCTS priors: `learning::buchholz_rank::initial` could now seed
  the search from "the K entries nearest to the goal", instead of a
  hard-coded baseline.
* Cross-prover similarity: same vocabulary in Coq, Lean, Idris 2,
  Agda all hash into the same 32 buckets, so the Vector octad joins
  them transparently.
* The capstone DSL (Step 6 / task #11) gets `near_vector` as a
  query primitive.

## Tests

3 new embed tests + 44 existing corpus tests all pass.
* Verifies dimension stability across entries
* Verifies cosine well-definedness for shared vocabulary
* Verifies self-cosine = 1.0 (top NN of any entry is itself)

## Known limitations

* 32-dim feature hashing has plenty of bucket collisions on large
  corpora (echo-types' 640 entries × ~10 tokens/entry hits the
  birthday bound easily). For impact-analysis use cases that's fine;
  for fine-grained similarity, swap in the GNN backend.
* `Embedder` trait isn't currently object-safe (`embed` takes
  `&CorpusEntry` directly); converting to `dyn Embedder` is a
  one-line change when needed.

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

Author: hyperpolymath

src/rust/corpus/embed.rs

@@ -0,0 +1,257 @@
+// SPDX-FileCopyrightText: 2026 ECHIDNA Project Team
+// SPDX-License-Identifier: PMPL-1.0-or-later
+
+//! Vector-octad embeddings for the corpus — Step 5 of the N-dim
+//! VeriSim plan.
+//!
+//! Two backends:
+//!
+//! 1. **Hashing-trick** (default, offline): tokenise statement +
+//!    proof on whitespace + Agda-syntax separators, hash each token
+//!    into one of 32 buckets, accumulate L2-normalised counts. Free,
+//!    deterministic, no network. Good enough for cosine-similarity
+//!    nearest-neighbour queries over shared vocabulary, which is
+//!    exactly what the SA / MCTS prior layer needs.
+//!
+//! 2. **GNN client** (future, online): for when the Julia server at
+//!    `/gnn/embed` is primed against real proof corpora (Wave-3 ML
+//!    work tracked in `docs/handover/TODO.md`). The trait `Embedder`
+//!    abstracts the choice; replacing the default `HashEmbedder`
+//!    with a `GnnEmbedder` is one-line.
+//!
+//! The corpus's `compute_embeddings` returns `Vec<Vec<f32>>` parallel
+//! to `entries`; `octad.rs::save_octads_jsonl` populates each Vector
+//! modality from this. Cosine-similarity helper lives here too.
+
+#![allow(dead_code)]
+
+use serde::{Deserialize, Serialize};
+
+use super::{Corpus, CorpusEntry};
+
+/// Embedding dimension used by the default hashing-trick embedder.
+/// Chosen to match the 32-dim GNN local-term embeddings already
+/// shipped in `src/rust/gnn/embeddings.rs` (`FEATURE_DIM = 32`), so
+/// stored octads can be later re-embedded from the GNN client without
+/// changing dimensions.
+pub const HASH_EMBED_DIM: usize = 32;
+
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct EmbedderInfo {
+    pub model: String,
+    pub dimensions: usize,
+}
+
+pub trait Embedder {
+    fn info(&self) -> EmbedderInfo;
+    fn embed(&self, entry: &CorpusEntry) -> Vec<f32>;
+}
+
+/// Default offline embedder: hashing-trick over the entry's
+/// statement + proof tokens, with L2 normalisation.
+#[derive(Debug, Clone, Default)]
+pub struct HashEmbedder;
+
+impl Embedder for HashEmbedder {
+    fn info(&self) -> EmbedderInfo {
+        EmbedderInfo {
+            model: "echidna-corpus-hash-v1".to_string(),
+            dimensions: HASH_EMBED_DIM,
+        }
+    }
+
+    fn embed(&self, entry: &CorpusEntry) -> Vec<f32> {
+        let mut buckets = vec![0.0_f32; HASH_EMBED_DIM];
+        let mut text = entry.statement.clone();
+        if let Some(p) = &entry.proof {
+            text.push(' ');
+            text.push_str(p);
+        }
+        for tok in tokenise(&text) {
+            let idx = bucket_for(tok);
+            buckets[idx] += 1.0;
+        }
+        l2_normalise(&mut buckets);
+        buckets
+    }
+}
+
+fn tokenise(s: &str) -> impl Iterator<Item = &str> {
+    s.split(|c: char| {
+        c.is_whitespace()
+            || matches!(
+                c,
+                '(' | ')' | '[' | ']' | '{' | '}' | ',' | ';' | '=' | ':' | '"' | '|'
+            )
+    })
+    .filter(|t| !t.is_empty())
+}
+
+/// FxHash-style fast hash; we only need stable bucketing, not crypto.
+fn bucket_for(tok: &str) -> usize {
+    let mut h: u64 = 0xcbf29ce484222325; // FNV-1a offset
+    for b in tok.as_bytes() {
+        h ^= *b as u64;
+        h = h.wrapping_mul(0x100000001b3);
+    }
+    (h as usize) % HASH_EMBED_DIM
+}
+
+fn l2_normalise(v: &mut [f32]) {
+    let norm: f32 = v.iter().map(|x| x * x).sum::<f32>().sqrt();
+    if norm > 1e-9 {
+        for x in v.iter_mut() {
+            *x /= norm;
+        }
+    }
+}
+
+/// Cosine similarity between two vectors of the same dimension.
+/// Returns 0.0 if either is zero.
+pub fn cosine(a: &[f32], b: &[f32]) -> f32 {
+    if a.len() != b.len() {
+        return 0.0;
+    }
+    let dot: f32 = a.iter().zip(b.iter()).map(|(x, y)| x * y).sum();
+    let na: f32 = a.iter().map(|x| x * x).sum::<f32>().sqrt();
+    let nb: f32 = b.iter().map(|x| x * x).sum::<f32>().sqrt();
+    if na < 1e-9 || nb < 1e-9 {
+        0.0
+    } else {
+        dot / (na * nb)
+    }
+}
+
+impl Corpus {
+    /// Compute embeddings for every entry using the default
+    /// `HashEmbedder`. Result is parallel to `self.entries`.
+    pub fn compute_embeddings(&self) -> Vec<Vec<f32>> {
+        let embedder = HashEmbedder;
+        self.entries.iter().map(|e| embedder.embed(e)).collect()
+    }
+
+    /// Embed a free-form text query using the same default
+    /// embedder. Used for `corpus query --near <text>`.
+    pub fn embed_query(&self, query: &str) -> Vec<f32> {
+        let synthetic = CorpusEntry {
+            name: String::new(),
+            qualified: String::new(),
+            module_idx: 0,
+            kind: super::DeclKind::Function,
+            statement: query.to_string(),
+            proof: None,
+            line: 0,
+            dependencies: vec![],
+            axiom_usage: super::AxiomUsage::default(),
+        };
+        HashEmbedder.embed(&synthetic)
+    }
+
+    /// Top-k nearest entries to `query_vec` by cosine similarity.
+    /// Each tuple is `(entry-index, similarity)`, sorted descending.
+    pub fn nearest_neighbours(&self, query_vec: &[f32], k: usize) -> Vec<(usize, f32)> {
+        let embeddings = self.compute_embeddings();
+        let mut scored: Vec<(usize, f32)> = embeddings
+            .iter()
+            .enumerate()
+            .map(|(i, v)| (i, cosine(query_vec, v)))
+            .collect();
+        scored.sort_by(|a, b| b.1.partial_cmp(&a.1).unwrap_or(std::cmp::Ordering::Equal));
+        scored.truncate(k);
+        scored
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::corpus::{AxiomUsage, DeclKind, ModuleEntry};
+    use std::path::PathBuf;
+
+    fn sample_corpus() -> Corpus {
+        let mut c = Corpus {
+            adapter: "agda".into(),
+            ..Default::default()
+        };
+        c.modules.push(ModuleEntry {
+            name: "M".into(),
+            path: PathBuf::from("M.agda"),
+            options: vec![],
+            imports: vec![],
+            entries: vec![0, 1, 2],
+        });
+        c.entries.push(CorpusEntry {
+            name: "wf-<".into(),
+            qualified: "M.wf-<".into(),
+            module_idx: 0,
+            kind: DeclKind::Function,
+            statement: "WellFounded _<_".into(),
+            proof: Some("acc lambda".into()),
+            line: 1,
+            dependencies: vec![],
+            axiom_usage: AxiomUsage::default(),
+        });
+        c.entries.push(CorpusEntry {
+            name: "Acc".into(),
+            qualified: "M.Acc".into(),
+            module_idx: 0,
+            kind: DeclKind::Data,
+            statement: "Acc R x".into(),
+            proof: None,
+            line: 5,
+            dependencies: vec![],
+            axiom_usage: AxiomUsage::default(),
+        });
+        c.entries.push(CorpusEntry {
+            name: "Nat".into(),
+            qualified: "M.Nat".into(),
+            module_idx: 0,
+            kind: DeclKind::Data,
+            statement: "data Nat where zero suc".into(),
+            proof: None,
+            line: 10,
+            dependencies: vec![],
+            axiom_usage: AxiomUsage::default(),
+        });
+        c.reindex();
+        c
+    }
+
+    #[test]
+    fn hash_embedder_dimensions() {
+        let c = sample_corpus();
+        let embeds = c.compute_embeddings();
+        assert_eq!(embeds.len(), 3);
+        for v in &embeds {
+            assert_eq!(v.len(), HASH_EMBED_DIM);
+        }
+    }
+
+    #[test]
+    fn cosine_similar_for_shared_vocab() {
+        let c = sample_corpus();
+        let embeds = c.compute_embeddings();
+        // wf-< (mentions WellFounded + _<_) and Acc (mentions R + x)
+        // should both be non-zero similar to a query about
+        // well-foundedness.
+        let q = c.embed_query("WellFounded _<_");
+        let s_wf = cosine(&q, &embeds[0]);
+        let s_acc = cosine(&q, &embeds[1]);
+        let s_nat = cosine(&q, &embeds[2]);
+        assert!(s_wf > 0.0, "wf-< should be similar to WellFounded query");
+        assert!(s_wf >= s_nat, "wf-< should beat Nat for WF query");
+        // Acc may or may not beat Nat depending on hash collisions;
+        // the assertion is just that similarity is well-defined.
+        assert!(s_acc.is_finite());
+    }
+
+    #[test]
+    fn nearest_neighbours_top1_is_self() {
+        let c = sample_corpus();
+        let embeds = c.compute_embeddings();
+        let nn = c.nearest_neighbours(&embeds[0], 1);
+        assert_eq!(nn.len(), 1);
+        assert_eq!(nn[0].0, 0);
+        assert!((nn[0].1 - 1.0).abs() < 1e-5, "self-cosine should be 1.0");
+    }
+}

src/rust/corpus/mod.rs

@@ -35,6 +35,7 @@
 
 pub mod agda;
 pub mod coq;
+pub mod embed; // Vector-octad embeddings (Step 5)
 pub mod idris2;
 pub mod lean;
 pub mod metrics; // Per-entry metrics tensor (Step 4)

src/rust/corpus/octad.rs

@@ -407,9 +407,13 @@ impl Corpus {
         } else {
             timestamp
         };
-        // Compute the rich metrics tensor once for the whole corpus
-        // (Step 4); attach to each octad's Tensor modality.
+        // Compute the rich metrics tensor + embeddings once for the
+        // whole corpus (Steps 4, 5). Tensor → tensor.metrics; vectors
+        // → vector.goal_embedding.
         let metrics_per_entry = self.compute_metrics();
+        let embedder = super::embed::HashEmbedder;
+        let info = <super::embed::HashEmbedder as super::embed::Embedder>::info(&embedder);
+        let embeddings = self.compute_embeddings();
         let mut out = String::new();
         for (i, entry) in self.entries.iter().enumerate() {
             let module = &self.modules[entry.module_idx];
@@ -421,6 +425,9 @@ impl Corpus {
             let mut octad =
                 DeclarationOctad::from_entry(entry, module, &self.adapter, &rev, ts);
             octad.tensor.metrics = metrics_per_entry[i].as_metric_map();
+            octad.vector.goal_embedding = embeddings[i].clone();
+            octad.vector.model = info.model.clone();
+            octad.vector.dimensions = info.dimensions;
             let line = serde_json::to_string(&octad).context("serialise octad")?;
             out.push_str(&line);
             out.push('\n');

src/rust/main.rs

@@ -273,6 +273,17 @@ enum CorpusOp {
         synonyms_dir: Option<PathBuf>,
     },
 
+    /// Find the K nearest-neighbour entries to a free-form text
+    /// query by cosine similarity over the Vector octad embeddings.
+    /// Useful for "find lemmas semantically near `WellFounded _<_`".
+    Near {
+        query: String,
+        #[arg(short, long)]
+        index: Option<PathBuf>,
+        #[arg(short, long, default_value_t = 10)]
+        top: usize,
+    },
+
     /// Convert a JSON corpus index into 8-modality octad JSONL
     /// (one DeclarationOctad per line). Streamable; compatible with
     /// VeriSim's `/api/v1/octads` endpoint when posted line-by-line.
@@ -1307,6 +1318,39 @@ fn corpus_command(op: CorpusOp, formatter: &OutputFormatter) -> Result<()> {
             }
         }
 
+        CorpusOp::Near { query, index, top } => {
+            let path = match index {
+                Some(p) => p,
+                None => {
+                    let basename = std::env::current_dir()?
+                        .file_name()
+                        .map(|s| s.to_string_lossy().into_owned())
+                        .unwrap_or_else(|| "project".to_string());
+                    default_index(&basename)
+                }
+            };
+            let corpus = Corpus::load_json(&path)
+                .with_context(|| format!("load corpus index {}", path.display()))?;
+            let q_vec = corpus.embed_query(&query);
+            let nn = corpus.nearest_neighbours(&q_vec, top);
+            if nn.is_empty() {
+                formatter.info(&format!(
+                    "no entries near '{}' (corpus has {} entries)",
+                    query,
+                    corpus.entries.len()
+                ))?;
+                return Ok(());
+            }
+            for (idx, sim) in &nn {
+                let entry = &corpus.entries[*idx];
+                println!(
+                    "{:.3}  {}  [{:?}]",
+                    sim, entry.qualified, entry.kind
+                );
+                println!("       : {}", entry.statement);
+            }
+        }
+
         CorpusOp::ExportOctads { index, out } => {
             let corpus = Corpus::load_json(&index)
                 .with_context(|| format!("load corpus index {}", index.display()))?;