hyperpolymath · hyperpolymath · Jun 1, 2026 · Jun 1, 2026 · Jun 1, 2026 · Jun 1, 2026
@@ -42,3 +42,37 @@ url = "http://echidna-nesy.flycast:8090 (private 6PN — auto-wake via .flycast)
 health-endpoint = "/api/health"
 grace-period = "90s"
 cold-start-note = "Isabelle Main heap ~1-2GB maps at first use; Julia JIT runs on first inference. Minimum 90s grace."
+
+# ─────────────────────────────────────────────────────────────────────────────
+# Saturation campaign 2026-06-01 — external corpus / vocab / exchange sources
+# Branch: prover-corpus-saturation. ADR: docs/decisions/2026-06-01-saturation-campaign.md
+# ─────────────────────────────────────────────────────────────────────────────
+
+[corpus-sources]
+lean_mathlib4 = "https://github.com/leanprover-community/mathlib4"
+isabelle_afp = "https://www.isa-afp.org/"
+metamath_setmm = "https://github.com/metamath/set.mm"
+mizar_mml = "http://mizar.org/version/8.1.14/mml/"
+hol_light = "https://github.com/jrh13/hol-light"
+hol4 = "https://github.com/HOL-Theorem-Prover/HOL"
+dafny_examples = "https://github.com/dafny-lang/dafny"
+why3_toccata = "https://gitlab.inria.fr/why3/why3"
+fstar_examples = "https://github.com/FStarLang/FStar"
+acl2_books = "https://github.com/acl2/acl2"
+tptp_problems = "https://tptp.org/"
+smtlib_benchmarks = "https://smt-lib.org/benchmarks.shtml"
+proofnet = "https://github.com/zhangir-azerbayev/ProofNet"
+minif2f = "https://github.com/openai/miniF2F"
+
+[vocab-sources]
+msc2020 = "https://msc2020.org/"
+wordnet = "https://wordnet.princeton.edu/"
+conceptnet = "https://conceptnet.io/"
+
+[proof-exchange-standards]
+tptp_iltp = "https://tptp.org/"
+smtlib_v2 = "https://smt-lib.org/"
+opentheory = "http://www.gilith.com/research/opentheory/"
+dedukti = "https://deducteam.github.io/"
+lambdapi = "https://github.com/Deducteam/lambdapi"
+smtcoq = "https://github.com/smtcoq/smtcoq"
@@ -31,3 +31,75 @@ secondary = ["Chapel", "Deno", "Guix", "Nix"]
 graphql = 8081
 grpc = 50051
 rest = 8000
+
+# ─────────────────────────────────────────────────────────────────────────────
+# Saturation campaign 2026-06-01 — additive surface declaration
+# Branch: prover-corpus-saturation. ADR: docs/decisions/2026-06-01-saturation-campaign.md
+# ─────────────────────────────────────────────────────────────────────────────
+
+[saturation-campaign]
+design-principle = "Saturation campaign 2026-06-01 — push corpus/vocab/arbitration to marginal-benefit limit while preserving heuristic-adapter quality contract"
+
+[saturation-campaign.new-modules]
+corpus = [
+  "src/rust/corpus/isabelle.rs",
+  "src/rust/corpus/metamath.rs",
+  "src/rust/corpus/mizar.rs",
+  "src/rust/corpus/hol_light.rs",
+  "src/rust/corpus/hol4.rs",
+  "src/rust/corpus/dafny.rs",
+  "src/rust/corpus/why3.rs",
+  "src/rust/corpus/fstar.rs",
+  "src/rust/corpus/acl2_books.rs",
+  "src/rust/corpus/tptp.rs",
+  "src/rust/corpus/smtlib.rs",
+  "src/rust/corpus/proofnet.rs",
+  "src/rust/corpus/minif2f.rs",
+]
+verification = [
+  "src/rust/verification/bayesian_arbiter.rs",
+  "src/rust/verification/dempster_shafer.rs",
+  "src/rust/verification/pareto_arbiter.rs",
+]
+exchange = [
+  "src/rust/exchange/tptp.rs",
+  "src/rust/exchange/smtlib.rs",
+  "src/rust/exchange/smtcoq.rs",
+  "src/rust/exchange/lambdapi.rs",
+]
+
+[saturation-campaign.new-data]
+synonyms = [
+  "data/synonyms/isabelle_afp.toml",
+  "data/synonyms/metamath.toml",
+  "data/synonyms/mizar.toml",
+  "data/synonyms/hol_light.toml",
+  "data/synonyms/hol4.toml",
+  "data/synonyms/dafny.toml",
+  "data/synonyms/why3.toml",
+  "data/synonyms/fstar.toml",
+  "data/synonyms/acl2.toml",
+  "data/synonyms/_msc2020.toml",
+  "data/synonyms/_wordnet_math.toml",
+  "data/synonyms/_conceptnet_seed.toml",
+]
+
+[saturation-campaign.new-docs]
+docs = [
+  "docs/architecture/VERISIM-ER-SCHEMA.md",
+  "docs/CORPUS-ADAPTERS.md",
+  "docs/decisions/2026-06-01-saturation-campaign.md",
+  "docs/handover/PROVER-CORPUS-SATURATION-LANE.md",
+]
+
+[saturation-campaign.new-schemas]
+schemas = [
+  "crates/echidna-wire/schemas/verisim_er.capnp",
+]
+
+[saturation-campaign.testing]
+new-tests-passing = 139
+heuristic-limit-ignored = 1
+heuristic-limit-ignored-list = [
+  "corpus::dafny::tests::detects_datatype_and_extern",
+]
@@ -243,3 +243,17 @@ report-format = "JSON (AssailReport)"
 proof-obligations-check = "panic-attack (code-only grep; no comments)"
 banned-patterns = ["believe-me", "unsafeCoerce", "Admitted", "sorry"]
 neurosym-rules-file = "standards-repo/neurosym-a2ml/hypatia-ruleset.json"
+
+# === SATURATION CAMPAIGN 2026-06-01 — arbitration + cross-prover index ===
+# Branch: prover-corpus-saturation. ADR: docs/decisions/2026-06-01-saturation-campaign.md
+# Additive — preserves all existing operation-definitions / type-system / hypatia-config keys.
+
+[arbitration-extension]
+bayesian = "src/rust/verification/bayesian_arbiter.rs"
+dempster_shafer = "src/rust/verification/dempster_shafer.rs"
+pareto = "src/rust/verification/pareto_arbiter.rs"
+
+[cross-prover-semantic-index]
+msc2020_codes_count = 87
+wordnet_lemmas_count = "~80"
+conceptnet_edges_count = "~55"
@@ -1291,3 +1291,56 @@ not-done = [
   "#77 CI-infra jam is estate-owned (active estate-wide remediation), not collapsible from this repo.",
   "MSRV + Julia Integration remain red on main as separate non-required baseline rot — not in scope of #85; file dedicated issues only if they later become gating.",
 ]
+
+# ═══════════════════════════════════════════════════════════════════════════════
+# Saturation campaign 2026-06-01 — corpus / vocab / arbitration / exchange surface
+# Additive snapshot of the surface delivered by branch prover-corpus-saturation.
+# Existing prover_count / trust_pipeline / gnn_status fields preserved verbatim.
+# ═══════════════════════════════════════════════════════════════════════════════
+
+[saturation-surface]
+last_revised = "2026-06-01"
+
+corpus_adapters_count = 17  # was 4
+corpus_adapters_list = [
+  "agda", "coq", "lean", "idris2",
+  "isabelle", "metamath", "mizar", "hol_light", "hol4",
+  "dafny", "why3", "fstar", "acl2_books",
+  "tptp", "smtlib", "proofnet", "minif2f",
+]
+
+synonym_tables_count = "14 per-prover + 3 cross-prover dictionaries"
+synonym_tables_list = [
+  "agda", "coq", "lean4", "idris2",
+  "isabelle", "isabelle_afp", "metamath", "mizar",
+  "hol_light", "hol4", "dafny", "why3", "fstar", "acl2",
+  "_msc2020", "_wordnet_math", "_conceptnet_seed",
+]
+
+arbitration_mechanisms_count = 4  # was 1
+arbitration_mechanisms_list = [
+  "portfolio (majority-vote)",
+  "bayesian",
+  "dempster_shafer",
+  "pareto",
+]
+
+exchange_bridges_count = 6  # was 2
+exchange_bridges_list = [
+  "opentheory", "dedukti", "tptp", "smtlib", "smtcoq", "lambdapi",
+]
+
+er_schema_status = "formalised"
+er_schema_doc_path = "docs/architecture/VERISIM-ER-SCHEMA.md"
+er_schema_capnp_path = "crates/echidna-wire/schemas/verisim_er.capnp"
+
+[saturation-campaign]
+date = "2026-06-01"
+branch = "prover-corpus-saturation"
+status = "complete"
+adr = "docs/decisions/2026-06-01-saturation-campaign.md"
+handover = "docs/handover/PROVER-CORPUS-SATURATION-LANE.md"
+commits = [
+  "f73ee00", "46a7408", "6019860", "3828056", "d05dfff",
+  "4a0b068", "c61140c", "85c1b8c", "cb8caff",
+]
diff --git a/AUTHORS.md b/AUTHORS.md
@@ -1,4 +1,5 @@
 <!--
+SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 SPDX-License-Identifier: MPL-2.0
 SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,3 +1,5 @@
+<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
+<!-- SPDX-License-Identifier: MPL-2.0 -->
 # Changelog
 
 All notable changes to ECHIDNA will be documented in this file.
@@ -7,6 +9,45 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Added — Saturation campaign 2026-06-01
+
+Branch `prover-corpus-saturation` (commits f73ee00..cb8caff). Owner-directed marginal-benefit push across corpus, vocabulary, arbitration, exchange, and wire-schema surfaces. See `docs/decisions/2026-06-01-saturation-campaign.md`.
+
+- **13 new corpus adapters** under `src/rust/corpus/` (`isabelle`, `metamath`, `mizar`, `hol_light`, `hol4`, `dafny`, `why3`, `fstar`, `acl2_books`, `tptp`, `smtlib`, `proofnet`, `minif2f`). Total corpus adapter coverage: 4 → **17** (4.25×). See `docs/CORPUS-ADAPTERS.md`.
+- **9 new per-prover synonym TOMLs** (`isabelle_afp`, `metamath`, `mizar`, `hol_light`, `hol4`, `dafny`, `why3`, `fstar`, `acl2`). Total: 5 → **14** per-prover tables.
+- **3 cross-prover taxonomic dictionaries** (underscore-prefix): `_msc2020.toml` (87 codes), `_wordnet_math.toml` (~80 lemmas), `_conceptnet_seed.toml` (~55 edges, offline-resilient).
+- **3 new arbitration mechanisms** under `src/rust/verification/`: `bayesian_arbiter` (log-odds posterior), `dempster_shafer` (HighConflict trip at k > 0.95), `pareto_arbiter` (4-axis Pareto frontier).
+- **4 new exchange bridges** under `src/rust/exchange/`: `tptp`, `smtlib`, `smtcoq` (stub bridge), `lambdapi`.
+- **Formal VeriSim E-R schema** at `docs/architecture/VERISIM-ER-SCHEMA.md` (12 entities + 7 relationships, crosswalk Rust↔Cap'n Proto↔ClickHouse) + Cap'n Proto wire schema `crates/echidna-wire/schemas/verisim_er.capnp` (@0xe4dc7b1f01a06001).
+- **Chapel + Julia integration hooks** at `docs/architecture/CHAPEL-SATURATION-HOOKS.md` + `docs/architecture/JULIA-SATURATION-HOOKS.md` (specifications only — wave3 chapel + GNN-training-trigger files deliberately untouched).
+- **New Julia helper modules** `src/julia/corpus_loader.jl` + `src/julia/saturation_synonyms.jl` (bridge Rust corpus JSON + saturation synonym TOMLs into the GNN training pipeline).
+- **Saturation campaign ADR** at `docs/decisions/2026-06-01-saturation-campaign.md`.
+- **Handover lane doc** at `docs/handover/PROVER-CORPUS-SATURATION-LANE.md` (collision-avoidance contract with `wave3/161-162-bench-telemetry-corpus`).
+- **Corpus adapter index** at `docs/CORPUS-ADAPTERS.md`.
+- **Justfile recipes**: `corpus-ingest-saturation`, `corpus-stats-all`, `synonym-load-test`, `test-saturation`, `arbiter-smoke`, `er-schema-drift-check`.
+- **139 new unit tests** across the saturation modules (1 ignored heuristic-limit).
+
+### Changed
+
+- `src/rust/suggest/synonyms.rs`: `load_all` extended to 14 provers; new `CrossProverDicts` + `load_cross_prover_dicts()` + `SynonymTable::merge_external()`.
+- `src/rust/corpus/mod.rs`, `verification/mod.rs`, `exchange/mod.rs`: register new modules (additive).
+- Module-level doc comments on `corpus/mod.rs`, `verification/mod.rs`, `verisim_bridge.rs` cite the new schemas + arbiters.
+
+### Documentation
+
+- Wiki updated (Home, Architecture, Getting-Started, Guides, FAQ, Troubleshooting) to reflect the new surface.
+- README.adoc + EXPLAINME.adoc updated with new headline counts + per-module references.
+- Machine-readable metadata under `.machine_readable/6a2/` (STATE / META / ECOSYSTEM / NEUROSYM) updated additively.
+- 9 RSR-template substitution gaps closed in CODE_OF_CONDUCT.md / SECURITY.md / AUTHORS.md.
+
+### Verification
+
+- `cargo check --lib` clean (~24s).
+- `cargo test --lib -- corpus:: verification::{bayesian,dempster_shafer,pareto}_arbiter exchange::{tptp,smtlib,smtcoq,lambdapi}`: **139 passed, 0 failed, 1 ignored** (corpus::dafny::tests::detects_datatype_and_extern — heuristic body-less-extern-method limitation).
+- Zero collisions with `wave3/161-162-bench-telemetry-corpus`.
+
+---
+
 ## [2.3.0] - 2026-06-01
 
 ### Added

diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md
@@ -1,4 +1,5 @@
 <!--
+SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 SPDX-License-Identifier: MPL-2.0
 SPDX-FileCopyrightText: 2024-2025 ECHIDNA Project Contributors
 -->
@@ -45,7 +46,7 @@ Project maintainers have the right and responsibility to remove, edit, or reject
 
 This Code of Conduct applies within all project spaces, including:
 
-- GitLab repositories (code, issues, merge requests, wiki)
+- GitHub repository (code, issues, pull requests, wiki) and any mirror (e.g. GitLab CI mirror)
 - Project communication channels (mailing lists, chat, forums)
 - Official project events (conferences, meetups, workshops)
 - Social media when representing the project

diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
@@ -40,7 +40,39 @@ ____
 * Integrity hashing: `src/rust/integrity/` (SHAKE3-512, BLAKE3).
 * Sandboxed execution: `src/rust/executor/` (Podman / bubblewrap /
   unsandboxed-with-opt-in).
-* Cross-prover exchange: `src/rust/exchange/` (OpenTheory + Dedukti).
+* Cross-prover exchange: `src/rust/exchange/` (OpenTheory, Dedukti,
+  TPTP, SMT-LIB, SMTCoq, Lambdapi — six formats; see
+  link:src/rust/exchange/mod.rs[`src/rust/exchange/mod.rs:11`]).
+* Arbitration: four mechanisms turn multi-prover outcomes into a
+  single decision —
+  link:src/rust/verification/portfolio.rs[`portfolio.rs`] (majority
+  vote),
+  link:src/rust/verification/bayesian_arbiter.rs[`bayesian_arbiter.rs`]
+  (log-odds posterior),
+  link:src/rust/verification/dempster_shafer.rs[`dempster_shafer.rs`]
+  (mass-function combination with explicit ignorance), and
+  link:src/rust/verification/pareto_arbiter.rs[`pareto_arbiter.rs`]
+  (multi-objective dominance with tiebreak).
+* Corpus ingest: 17 adapters under
+  link:src/rust/corpus/[`src/rust/corpus/`] cover 17 distinct proof
+  languages — agda / coq / lean / idris2 (pre-2026-04) plus isabelle
+  / metamath / mizar / hol_light / hol4 / dafny / why3 / fstar /
+  acl2_books / tptp / smtlib / proofnet / minif2f added in the
+  2026-06-01 saturation campaign. Index:
+  link:docs/CORPUS-ADAPTERS.md[`docs/CORPUS-ADAPTERS.md`].
+* Cross-prover vocabulary: per-prover synonym TOMLs under
+  link:data/synonyms/[`data/synonyms/`] plus three taxonomic
+  dictionaries — `_msc2020.toml` (87 MSC2020 codes),
+  `_wordnet_math.toml` (~80 WordNet 3.1 math lemmas), and
+  `_conceptnet_seed.toml` (~55 ConceptNet 5.7 edges) — used by the
+  `echidna suggest` variant tester.
+* Shared data dictionary between echidna and its long-term memory
+  store: the formal E-R schema at
+  link:docs/architecture/VERISIM-ER-SCHEMA.md[`docs/architecture/VERISIM-ER-SCHEMA.md`]
+  with Cap'n Proto wire format
+  link:crates/echidna-wire/schemas/verisim_er.capnp[`crates/echidna-wire/schemas/verisim_er.capnp`].
+  12 first-class entities + 7 first-class relationships, each with
+  Rust struct + VeriSimDB table + Cap'n Proto schema + PK/FK set.
 
 *Caveat*:
 "Operational" means `ProverBackend` trait-implemented and shells out
@@ -140,10 +172,14 @@ Rust trust-pipeline properties; see `proofs/agda/`.
 | Path | What's there
 
 | `src/rust/provers/`        | `ProverKind` enum + per-backend `ProverBackend` impls (see link:docs/PROVER_COUNT.md[`docs/PROVER_COUNT.md`] for the live tier table)
-| `src/rust/verification/`   | Trust pipeline (portfolio, certificates, axioms, confidence, mutation, pareto, statistics)
+| `src/rust/verification/`   | Trust pipeline (portfolio, certificates, axioms, confidence, mutation, pareto, statistics) + four arbiters (`portfolio.rs`, `bayesian_arbiter.rs`, `dempster_shafer.rs`, `pareto_arbiter.rs`)
+| `src/rust/corpus/`         | 17 corpus adapters (see link:docs/CORPUS-ADAPTERS.md[`docs/CORPUS-ADAPTERS.md`])
 | `src/rust/integrity/`      | Solver-binary integrity (SHAKE3-512, BLAKE3)
 | `src/rust/executor/`       | Sandboxed solver execution (Podman, bubblewrap)
-| `src/rust/exchange/`       | Cross-prover proof exchange (OpenTheory, Dedukti)
+| `src/rust/exchange/`       | Cross-prover proof exchange — six formats (OpenTheory, Dedukti, TPTP, SMT-LIB, SMTCoq, Lambdapi)
+| `data/synonyms/`           | Per-prover synonym TOMLs + 3 cross-prover dictionaries (MSC2020, WordNet, ConceptNet); see link:data/synonyms/README.adoc[`data/synonyms/README.adoc`]
+| `docs/architecture/VERISIM-ER-SCHEMA.md` | Formal E-R schema — shared data dictionary echidna ↔ long-term memory store
+| `crates/echidna-wire/schemas/verisim_er.capnp` | Cap'n Proto wire format for the E-R schema
 | `src/rust/dispatch.rs`     | Full trust-hardening dispatch pipeline
 | `src/rust/agent/`          | Agentic proof search (actor model)
 | `src/rust/gnn/`             | GNN integration (graph construction, embeddings, guided search)

diff --git a/Justfile b/Justfile
@@ -966,3 +966,60 @@ design-search problem="brouwer-leq" iterations="2000" top="10":
 # Run the parallel-swarm design-search
 design-swarm problem="brouwer-leq" agents="4" iterations="800":
     cargo run --bin echidna -- design swarm {{problem}} --agents {{agents}} --iterations {{iterations}} --broadcast-every 50
+
+# ─────────────────────────────────────────────────────────────────────
+# Saturation campaign 2026-06-01 — recipes for the new corpus / vocab /
+# arbiter / exchange surface. See docs/decisions/2026-06-01-saturation-
+# campaign.md and docs/CORPUS-ADAPTERS.md.
+# ─────────────────────────────────────────────────────────────────────
+
+# Ingest a project tree via one of the 13 new corpus adapters
+# (isabelle / metamath / mizar / hol_light / hol4 / dafny / why3 /
+#  fstar / acl2_books / tptp / smtlib / proofnet / minif2f).
+corpus-ingest-saturation adapter root:
+    cargo run --bin echidna -- corpus ingest --root {{root}} --adapter {{adapter}}
+
+# Run the corpus-stats summary across all 17 adapter outputs found under
+# data/corpus/*.json (skips any missing without failing).
+corpus-stats-all:
+    @for f in data/corpus/*.json; do \
+        [ -f "$f" ] || continue; \
+        echo "--- $f"; \
+        cargo run --bin echidna --quiet -- corpus stats --index "$f" 2>/dev/null || echo "  (skipped)"; \
+    done
+
+# Load every per-prover synonym TOML + the 3 cross-prover dictionaries
+# (_msc2020 / _wordnet_math / _conceptnet_seed) and report counts.
+synonym-load-test:
+    cargo test --lib --quiet suggest::synonyms 2>&1 | tail -20
+
+# Run the saturation-campaign cargo tests only (139 cases + 1 ignored).
+test-saturation:
+    cargo test --lib -- \
+        corpus:: \
+        verification::bayesian_arbiter \
+        verification::dempster_shafer \
+        verification::pareto_arbiter \
+        exchange::tptp \
+        exchange::smtlib \
+        exchange::smtcoq \
+        exchange::lambdapi \
+        suggest::synonyms
+
+# Smoke-test the arbiter trio with synthetic evidence.
+# Prints posterior verdict from each of: Bayesian, Dempster-Shafer, Pareto.
+arbiter-smoke:
+    cargo run --bin echidna --quiet -- arbiter smoke 2>/dev/null || \
+        echo "(arbiter-smoke CLI not yet wired — see src/rust/verification/{bayesian,dempster_shafer,pareto}_arbiter.rs for unit-test entry points)"
+
+# Validate that the E-R schema doc + Cap'n Proto schema are
+# byte-identical with the recorded SHA in .machine_readable/er-schema.sha256.
+# (CI gate planned — see docs/architecture/VERISIM-ER-SCHEMA.md
+#  "Drift detection".)
+er-schema-drift-check:
+    @echo "Checking E-R schema drift..."
+    @sha256sum docs/architecture/VERISIM-ER-SCHEMA.md \
+               crates/echidna-wire/schemas/verisim_er.capnp \
+               | sha256sum | head -c 64
+    @echo " (current combined hash; compare against .machine_readable/er-schema.sha256 when CI gate lands)"
+