docs(er): formal VeriSim E-R schema + CORPUS-ADAPTERS index + saturation ADR

Three new docs landing the schema + indexes for the saturation
campaign:

- docs/architecture/VERISIM-ER-SCHEMA.md — 12 entities (Octad +
  8 modalities + ProofAttempt + CertificateBlob + ProverBinaryIntegrity)
  and 7 relationships (composition / cross-prover identity / attempt /
  certificate / binary-integrity / depends-on / evolved-from). Crosswalk
  Rust struct ↔ Cap'n Proto schema ↔ ClickHouse table. Replaces the
  aspirational design/ECHIDNA-VERISIM-TRIANGULATION-2026-04-17.adoc
  as the formal data-model spec. Drift-detection plan + open
  migrations tracked inline.

- docs/CORPUS-ADAPTERS.md — index of all 17 corpus adapters with
  hazard-flag inventory + canonical source URLs + open backlog
  (naproche/mathcomp/iris/cubical_agda/tlaps/pvs/naturalproofs/
  alphaproof) for future waves.

- docs/decisions/2026-06-01-saturation-campaign.md — ADR for the
  whole campaign: context, decision, consequences, what this campaign
  did NOT do, alternatives considered.

Lane: prover-corpus-saturation.

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

Author: hyperpolymath

docs/CORPUS-ADAPTERS.md

@@ -0,0 +1,108 @@
+<!--
+SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+SPDX-License-Identifier: MPL-2.0
+-->
+
+# Corpus Adapters — Index
+
+**Status**: canonical. Updated 2026-06-01 as part of the saturation campaign
+(see `docs/decisions/2026-06-01-saturation-campaign.md`).
+
+Each adapter is a `pub fn ingest(root: &Path) -> Result<Corpus>` in
+`src/rust/corpus/<name>.rs`, structurally indexing a proof tree into
+`Corpus` (`src/rust/corpus/mod.rs:138`). Hazards (axioms, sorry,
+believe_me, cheat, …) populate `AxiomUsage` per entry.
+
+## Adapter table
+
+| Adapter | File extensions | Canonical source URL | Hazard flags surfaced | Status |
+|---|---|---|---|---|
+| **agda** | `*.agda` | <https://github.com/agda/agda> | postulate, believe_me, assert_total, sorry, trustme | shipped pre-2026-04 |
+| **coq** | `*.v` | <https://github.com/coq/coq> | Axiom, Parameter, Admitted | shipped pre-2026-04 |
+| **lean** | `*.lean` | <https://github.com/leanprover-community/mathlib4> | sorry, axiom, admit | shipped pre-2026-04 |
+| **idris2** | `*.idr` / `*.ipkg` | <https://github.com/idris-lang/Idris2> | believe_me, assert_total, postulate | shipped pre-2026-04 |
+| **isabelle** | `*.thy` | <https://www.isa-afp.org/> | axiomatization, axiom, sorry, oops, consts, nitpick, quickcheck | **NEW 2026-06-01** |
+| **metamath** | `*.mm` | <https://github.com/metamath/set.mm> | `$a` axiom usage, `?` admitted in proof | **NEW 2026-06-01** |
+| **mizar** | `*.miz`, `*.abs` | <http://mizar.org/version/8.1.14/mml/> | `@proof` sketch, commented-theorem, consider-without-proof | **NEW 2026-06-01** |
+| **hol_light** | `*.ml` (HOL Light filter) | <https://github.com/jrh13/hol-light> | new_axiom, mk_thm, free ASSUME, failwith "not yet" | **NEW 2026-06-01** |
+| **hol4** | `*Script.sml` | <https://github.com/HOL-Theorem-Prover/HOL> | new_axiom, mk_thm, cheat, CHEAT_TAC | **NEW 2026-06-01** |
+| **dafny** | `*.dfy` | <https://github.com/dafny-lang/dafny> | assume, `:axiom`, extern, expect, `:fuel 0` | **NEW 2026-06-01** |
+| **why3** | `*.mlw`, `*.why` | <https://gitlab.inria.fr/why3/why3> | axiom, val function (uninterpreted), val lemma, assume, absurd | **NEW 2026-06-01** |
+| **fstar** | `*.fst`, `*.fsti` | <https://github.com/FStarLang/FStar> | assume, admit, magic, Obj.magic, unsafe_coerce, admit_smt_queries | **NEW 2026-06-01** |
+| **acl2_books** | `*.lisp`, `*.acl2` | <https://github.com/acl2/acl2> | defaxiom, defstub, skip-proofs (top-level surfaced), ld-skip-proofsp, local-in-theory-nil | **NEW 2026-06-01** |
+| **tptp** | `*.p`, `*.tptp` | <https://tptp.org/> | no_conjecture (axiom-only file), TFF/THF dialects not fully supported | **NEW 2026-06-01** |
+| **smtlib** | `*.smt2`, `*.smt` | <https://smt-lib.org/benchmarks.shtml> | status_unknown, uninterpreted (declared-not-defined), unnamed_bang_pattern | **NEW 2026-06-01** |
+| **proofnet** | `*.jsonl` | <https://github.com/zhangir-azerbayev/ProofNet> | sorry, admit, axiom, no_formal_proof | **NEW 2026-06-01** |
+| **minif2f** | `*.lean`, `*.thy`, `*.ml`, `*.mm`, `*.v` (multi) | <https://github.com/openai/miniF2F> | sorry, admit, Admitted, empty_body, todo | **NEW 2026-06-01** |
+
+## Coverage summary
+
+**Pre-2026-04**: 4 adapters (agda, coq, lean, idris2).
+**Post-2026-06-01**: 17 adapters — 4.25× expansion.
+
+## Test fixtures
+
+Every adapter has a minimal smoke fixture under
+`tests/corpus_fixtures/<adapter>/`. Fixtures cover the
+happy-path decl parse plus at least one hazard-detection case.
+They are intentionally tiny — the goal is "compile + smoke
+correctness", not "extensive coverage". Larger evaluation corpora
+live outside the repo (mathlib4 etc. are fetched at training time
+via `just provision-corpora`).
+
+## Cross-prover synonyms
+
+Every adapter has a corresponding per-prover synonyms TOML at
+`data/synonyms/<adapter>.toml` listing tactic / decl / hazard
+vocabulary with canonical-and-aliases form. Plus three cross-prover
+taxonomic dictionaries (underscore-prefix; merged into
+`SynonymTable` via `merge_external()`):
+
+- `_msc2020.toml` — 87 MSC2020 codes for cross-domain classification
+- `_wordnet_math.toml` — ~80 lemmas from WordNet 3.1 math sub-hierarchy
+- `_conceptnet_seed.toml` — ~55 pre-fetched ConceptNet 5.7 edges
+  for offline-resilient semantic_class resolution
+
+## Wiring into downstream consumers
+
+1. **suggest**: `src/rust/suggest/synonyms.rs::SynonymTable::load_all()`
+   reads per-prover TOMLs. The cross-prover dictionaries are loaded
+   via `with_msc2020()` / `with_wordnet()` / `with_conceptnet()` (new
+   methods landing in the same campaign).
+
+2. **octad emission**: `src/rust/corpus/octad.rs::Corpus::emit_octads()`
+   walks any `Corpus` produced by any adapter and emits 8-modality
+   octads into VeriSimDB (see `docs/architecture/VERISIM-ER-SCHEMA.md`).
+
+3. **GNN training**: `src/julia/training/train.jl` consumes
+   `premises_<adapter>.jsonl` files under `training_data/`. The new
+   adapters can produce these files via
+   `cargo run --bin corpus-emit -- --adapter <name> --output training_data/premises_<name>.jsonl`
+   (TODO — wire CLI).
+
+## When to add a new adapter
+
+- Upstream proof library has > 100 declarations AND
+- The library has a stable file format (not a daily-changing CI artifact) AND
+- A real prover backend exists in `src/rust/provers/` OR
+  it's a recognised ML evaluation set (ProofNet, MiniF2F, NaturalProofs, …).
+
+Drop the new file under `src/rust/corpus/<name>.rs`, add it to
+`mod.rs`, write at least 2 unit tests, add a fixture under
+`tests/corpus_fixtures/<name>/`, add an entry to this index, and
+add the per-prover synonyms TOML at `data/synonyms/<name>.toml`
+(omit if it's a format like TPTP/SMT-LIB rather than a prover).
+
+## Open backlog (next saturation wave)
+
+- `src/rust/corpus/naproche.rs` (Naproche-SAD)
+- `src/rust/corpus/mathcomp.rs` (Coq MathComp — distinct from generic coq.rs)
+- `src/rust/corpus/iris.rs` (Coq Iris separation logic)
+- `src/rust/corpus/cubical_agda.rs` (Cubical Agda stdlib)
+- `src/rust/corpus/tlaps.rs` (TLA+ Proofs)
+- `src/rust/corpus/pvs.rs` (PVS theories)
+- `src/rust/corpus/naturalproofs.rs` (Bobrow et al. NL→Coq dataset)
+- `src/rust/corpus/alphaproof.rs` (DeepMind 2024 olympiad set)
+
+Drop here as upstream URLs are confirmed and at least one production
+consumer needs each.