feat(corpus): tensor-octad metrics — Step 4 of N-dim plan

Adds `corpus/metrics.rs` with `EntryMetrics`, a fixed-shape per-entry
metrics tuple covering size / connectivity / shape / hazards / K-elim
risk / head-symbol class. Computed by `Corpus::compute_metrics()`
after `reindex` populates dependency tables; consumed by both the
Tensor octad (string-keyed map for VeriSim wire compat) and any
downstream Rust caller (typed `EntryMetrics` for the SA energy in
`learning/buchholz_rank.rs`).

## Metric families

* **Size**: statement_tokens, proof_tokens, statement_chars
* **Connectivity**: dep_fanout, dep_fanin, proof_depth (longest
  forward dep-chain to a leaf, capped at 32, cycle-stable via seen
  set)
* **Shape**: recursive (self-reference detection),
  structural_induction (constructor-pattern heuristic),
  pattern_match_clauses (clause count from owns-prefix matches),
  has_where_block
* **Hazards**: one bool per AxiomUsage class
  (postulate/believe_me/admitted/sorry/assert_total/trustme) + count
  of `other` entries
* **K-elim risk** (Agda-only): conservative-positive on
  `refl`-pattern-match shapes that classically violate `--without-K`
* **Head-symbol class**: first top-level identifier in the statement
  (skipping leading binders / parens / `∀` / `Π`); coarse semantic
  class fallback when no `synonyms.semantic_class` is set

## Tensor octad now populates

`octad.rs::save_octads_jsonl` now calls `compute_metrics()` once per
ingest and attaches the resulting map to each octad's
`tensor.metrics`. Downstream consumers reading the octad stream get
the rich tensor without re-parsing source files.

## SA-from-data is now possible

`learning/buchholz_rank.rs::blockers` currently hardcodes its
predicates. With this commit the corpus exposes the data those
predicates would consume — proof_depth, dep_fanout, hazard flags,
head_symbol, recursive-vs-structural. The capstone DSL (Step
6/task#11) will rewrite the SA energy as queries over this tensor;
this commit lays the substrate.

## Tests

3 new metrics tests + 33 existing corpus tests all pass. Verified:
* `_<_` (leaf) → fanout 0, fanin N (depending on graph)
* `pred` (depends on `_<_`) → fanout 1, depth 1, multi-clause body
  detected
* `wf` (recursive on itself) → `recursive` flagged true; depth 2

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

Author: hyperpolymath