feat(corpus): multi-axis query DSL — N-dim plan capstone

Adds `corpus/query.rs` with `CorpusQuery`, a builder API that
composes filters, similarity-near, ordering, and limit into a single
surface over the multi-modal index.

## Surface

```rust
let hits = corpus.query()
    .where_kind(DeclKind::Function)
    .where_axiom_free()
    .where_recursive()
    .near_text("WellFounded _<_")
    .order_by(SortKey::Similarity)
    .limit(10)
    .run();
```

## Filter axes (composable)

* `where_kind(DeclKind)` / `where_kind_in(&[DeclKind])`
* `where_axiom_free()` — exclude any hazard
* `where_no_hazards()` — exclude hazards but keep declared postulates
* `where_recursive()` / `where_non_recursive()` — from metrics
* `where_structural()` — structural-induction shape detection
* `where_name_contains(s)` / `where_qualified_contains(s)`
* `where_head_symbol(s)` — exact match on metrics.head_symbol
* `where_adapter(s)` — restrict to one prover
* `where_has_reverse_deps()` — non-leaf entries
* `where_custom(fn(&Entry, &Metrics) -> bool)` — escape hatch

## Similarity (Vector octad)

* `near_text("…")` — embed via HashEmbedder, cosine-rank
* `near_vector(Vec<f32>)` — pre-computed embeddings (e.g. GNN)
* Both implicitly set `SortKey::Similarity` unless overridden.

## Ordering (Tensor octad metrics)

* `Default` (corpus order)
* `Similarity` (descending; needs near_query)
* `StatementSize`, `ProofDepth` (ascending)
* `Fanin`, `Fanout` (descending — most-depended-on first)

## What this closes

Replaces the ad-hoc `find` / `closure` / `reverse_deps` /
`nearest_neighbours` methods with a unified query surface. The SA
energy in `learning/buchholz_rank.rs::blockers()` was hand-coded
predicates over hardcoded lemma names; with this DSL it becomes a
data-driven query over the corpus's metrics and graph octads, e.g.

  corpus.query()
      .where_qualified_contains("osuc-mono")
      .where_axiom_free()
      .run()
      .is_empty()  // → "this lemma is missing"

That refactor is its own PR; this commit lands the DSL substrate.

## Tests

6 new query tests covering kind filter, axiom-free filter,
recursive filter, similarity ordering, fanin ordering, and a
compositional end-to-end query that returns wf-< as the unique
top hit. 1059 total lib tests pass (16 added across Steps 1–5 +
capstone).

## End state of the N-dim plan

  Step 1: reverse-dep index             [completed]
  Step 2: Coq + Lean 4 + Idris 2        [completed]
  Step 3: 8-modality octad storage      [completed]
  Step 4: tensor metrics                [completed]
  Step 5: vector embeddings             [completed]
  Capstone: multi-axis query DSL        [completed]

Six commits, ~6,000 LoC, 16 unit tests added. The corpus is now an
N-dimensional, octad-shaped, content-addressed, history-preserving,
query-able index across four provers — ready to be the substrate
for SA-from-data, MCTS priors, and the actual Phase 1.3 / unbudgeted
wf-<ᵇʳᶠ_ proof work that this whole campaign is in service of.

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

Author: hyperpolymath

src/rust/corpus/mod.rs

@@ -40,6 +40,7 @@ pub mod idris2;
 pub mod lean;
 pub mod metrics; // Per-entry metrics tensor (Step 4)
 pub mod octad; // 8-modality octad emission for VeriSim integration (Step 3)
+pub mod query; // Multi-axis query DSL (capstone)
 
 use std::collections::HashMap;
 use std::path::{Path, PathBuf};