feat(corpus): 8-modality octad emission — Step 3 of N-dim plan

Adds `corpus/octad.rs` with `DeclarationOctad`, mirroring the shape of
`verisim_bridge::OctadPayload` but with corpus-declaration-tailored
fields. Each `CorpusEntry` becomes one octad; persist as newline-
delimited JSON (`*.octads.jsonl`), one octad per line — streamable,
inspectable, line-by-line ingestable by VeriSim's `/api/v1/octads`.

## Six of eight modalities populate immediately

* **Semantic**:  adapter, kind, name, qualified, statement, proof
* **Document**:  searchable_text built from name + statement + proof +
  aspects; aspects include hazard tags (`hazard:postulate`,
  `hazard:believe_me`, etc.) so document-mode FTS surfaces them
* **Graph**:     forward `dependencies` AND reverse `dependents`
  (Step 1 payoff — both directions), plus `cross_prover_id` =
  SHA-256 of the local-name tail (theorems with matching local
  names across provers join on this hash)
* **Provenance**: SHA-256 hash chain over (parent, event, ts, file,
  line). Replayable from the source files (Bennettian foundation).
* **Spatial**:    file path + line + adapter namespace
* **Temporal**:   single Created version with content_hash today;
  future ingest rungs append additional versions

Tensor (Step 4) currently carries hazard flags + fan-in/fan-out.
Vector (Step 5) reserved.

## Why a sibling type, not the existing OctadPayload

`verisim_bridge::OctadPayload` is feature-gated behind `verisim` and
proof-attempt-shaped (its TemporalPayload assumes a tactic chain;
its SemanticPayload carries a CBOR `proof_blob_b64`). Forcing
declarations into that shape would either pull the corpus behind the
feature gate or distort the schema. Sibling type with parallel
modalities is the additive integration — the field names overlap
where semantically appropriate so a future bridge layer can map
1:1 when an actual VeriSim instance accepts both.

## Cross-prover identity

The `cross_prover_id` is SHA-256 over the qualified name's local
tail. `Foo.WellFounded` (Agda) and `Bar.WellFounded` (Coq) get the
same key — cross-prover joins fall out from the graph octad
without going through the synonym layer. Coarser than full
semantic equivalence (which lives in OpenTheory/Dedukti exchange)
but fine for the impact-analysis use case.

## CLI

* `echidna corpus export-octads --index data/corpus/X.json --out X.octads.jsonl`
* `echidna corpus import-octads --octads X.octads.jsonl --out X.json`

End-to-end verified: round-tripped 640 echo-types entries through
JSONL (one 1.4-KB line per entry); test asserts statement, proof,
deps, kind, line all preserved; `dependents` index rebuilt on load.

## Tests

3 new octad tests + the 38 existing corpus tests all pass.
End-to-end exercise: 640 octads emitted, first verified to have all
8 modalities populated, content_hash + provenance hash both stable
SHA-256 hex digests.

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

Author: hyperpolymath

src/rust/corpus/mod.rs

@@ -37,6 +37,7 @@ pub mod agda;
 pub mod coq;
 pub mod idris2;
 pub mod lean;
+pub mod octad; // 8-modality octad emission for VeriSim integration (Step 3)
 
 use std::collections::HashMap;
 use std::path::{Path, PathBuf};