diff --git a/.github/workflows/dogfood-proofs-ci.yml b/.github/workflows/dogfood-proofs-ci.yml
index e2f91f3a..141953ff 100644
--- a/.github/workflows/dogfood-proofs-ci.yml
+++ b/.github/workflows/dogfood-proofs-ci.yml
@@ -219,7 +219,11 @@ jobs:
 
   agda:
     name: Agda
-    runs-on: ubuntu-latest
+    # Pinned: ubuntu-latest moved to 26.04, whose apt agda 2.8.0 rejects the
+    # options agda-stdlib v1.7.3 sets ("Unrecognized option:
+    # --warn=noUserWarning"). 24.04 ships agda 2.6.3, the version the corpus
+    # is verified against. Unpin when the stdlib moves to a 2.8-compatible tag.
+    runs-on: ubuntu-24.04
     timeout-minutes: 20
     steps:
       - uses: actions/checkout@v7.0.1
diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml
index 3d9b71f1..ec9b65c7 100644
--- a/.github/workflows/rust-ci.yml
+++ b/.github/workflows/rust-ci.yml
@@ -77,6 +77,20 @@ jobs:
           repository: ${{ github.repository }}
           ref: ${{ github.ref }}
 
+      - name: Lexicon v2 contract (Nickel)
+        # data/synonyms/schema.ncl applied to every shipped table, plus the
+        # accept/reject fixtures that prove the contract still bites.
+        # Nickel is a pinned release binary checked by SHA-256 (no action, so
+        # no actions.lock record). Bump both lines together.
+        env:
+          NICKEL_VERSION: 1.12.2
+          NICKEL_SHA256: dae58ae8a96bbcacf141d61a5f93a971c89341f9d7164f763aa170459336ea46
+        run: |
+          curl -sSfL -o "$RUNNER_TEMP/nickel" "https://github.com/tweag/nickel/releases/download/${NICKEL_VERSION}/nickel-x86_64-linux"
+          echo "${NICKEL_SHA256}  $RUNNER_TEMP/nickel" | sha256sum -c -
+          chmod +x "$RUNNER_TEMP/nickel"
+          NICKEL="$RUNNER_TEMP/nickel" scripts/lexicon-check.sh
+
       - name: Install Rust toolchain
         # `toolchain:` is mandatory because the ref is `@v1` (pinned to a commit
         # through actions.lock), not a toolchain name:
diff --git a/Justfile b/Justfile
index 207cfb06..d6921d1d 100644
--- a/Justfile
+++ b/Justfile
@@ -1138,6 +1138,12 @@ corpus-stats-all:
 synonym-load-test:
     cargo test --lib --quiet suggest::synonyms 2>&1 | tail -20
 
+# Lexicon v2: apply the Nickel contract (data/synonyms/schema.ncl) to every
+# synonym table and to the accept/reject fixtures. Needs nickel >= 1.12.
+lexicon-check:
+    scripts/lexicon-check.sh
+    cargo test --locked --test lexicon_v2_test
+
 # Run the saturation-campaign cargo tests only (139 cases + 1 ignored).
 test-saturation:
     cargo test --lib -- \
diff --git a/data/synonyms/README.adoc b/data/synonyms/README.adoc
index cdfa8cbc..99cd3fd3 100644
--- a/data/synonyms/README.adoc
+++ b/data/synonyms/README.adoc
@@ -51,7 +51,7 @@ Each `[[synonym]]` entry has:
 
 | `aliases`
 | yes
-| Array of equivalent names.  Order is *not* significant.
+| Array of non-empty names; `relation` says how they relate to `canonical`.  Order is *not* significant.
 
 | `tactic_class`
 | no
@@ -68,6 +68,63 @@ Each `[[synonym]]` entry has:
 | Version range over which the alias applies.  Empty means "always".
 |===
 
+== Lexicon v2 fields
+
+Owner decisions 2026-10-19 (D2, D4) in
+`docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc`.
+All fields are optional; v1 rows load unchanged. The schema of record is the
+Nickel contract `schema.ncl`; `scripts/lexicon-check.sh` (or
+`just lexicon-check`) applies it to every table here and to the fixtures in
+`tests/lexicon_fixtures/`, and CI runs it in the `rust-ci` check job.
+
+[cols="1,3"]
+|===
+| Field | Meaning
+
+| `relation`
+| How `aliases` relate to `canonical`: `synonym` (default, interchangeable),
+  `specialisation` (each alias is a special case), `generalisation`,
+  `false_friend` (looks alike, is not; never substituted) or `phrase`
+  (`canonical` is a multi-token idiom). Only `synonym` and `phrase` rows feed
+  the variant tester; the others are reported by `SynonymTable::related`.
+  Phrase substitution runs one way for now: an alias at a tactic site can be
+  replaced by the phrase spelling, but the extractors see single identifiers,
+  so a canonical phrase in a proof is not yet replaced by an alias.
+
+| `phrase`
+| Token list of a multi-token idiom. Required with, and only allowed with,
+  `relation = "phrase"`.
+
+| `false_friends`
+| Look-alike names in other tables, each `{ name, table }` where `table` is
+  the other file's stem.
+
+| `evidence`
+| The witness behind the row: `{ kind = "none" }` (default), `"curated"`,
+  `"probe"` with `tests` and `failures`, or `"kernel"` with `format`,
+  `checked_by` and a 64-hex BLAKE3 `term_hash`; counts are integers that fit
+  a u32. Evidence attests the row's relation, whatever it is, but lifts into
+  the arbiter's `FidelityEvidence` (`SynonymEntry::fidelity_evidence`) only
+  for an identity claim: a `synonym` or `phrase` row that is not `lossy`.
+  There `probe` lifts to `DeclaredCorrespondence` and `kernel` to
+  `KernelTranslation`; `none`, `curated` (provenance, not fidelity
+  evidence) and every other row lift to `None`. A lexicon row never raises
+  a verdict above its own evidence.
+
+| `fidelity`, `residue`
+| `exact` or `lossy`; a lossy row must say what is lost in `residue`.
+
+| `scope`
+| `{ library, version }` the relation holds in.
+|===
+
+Corpus-mined candidates (owner decision D4) are flag-only: they carry
+`evidence = { kind = "none" }` and never set `semantic_class` on their own.
+
+Nickel checks shape and the cross-field rules; serde checks that
+`checked_by` names a `ProverKind` and `format` an `ExchangeFormat` when Rust
+loads a table (`tests/lexicon_v2_test.rs`).
+
 == Variant-tester contract
 
 When `echidna suggest` encounters a tactic name in a failing proof, it:
diff --git a/data/synonyms/hol4.toml b/data/synonyms/hol4.toml
index b8d80a99..b5d9c0ef 100644
--- a/data/synonyms/hol4.toml
+++ b/data/synonyms/hol4.toml
@@ -108,7 +108,7 @@ aliases      = ["Induct_on", "recInduct", "completeInduct_on"]
 tactic_class = "induction"
 notes        = """
 `Induct` does induction on the *outermost* universally-quantified
-variable. `Induct_on \`x\`` picks the variable explicitly.
+variable. `Induct_on `x`` picks the variable explicitly.
 `recInduct` uses the recursion induction principle generated from a
 `Define`. `completeInduct_on` is strong (course-of-values) induction.
 """
@@ -128,7 +128,7 @@ canonical    = "Cases"
 aliases      = ["Cases_on", "FULL_CASES_TAC"]
 tactic_class = "case"
 notes        = """
-Case split on the outermost universal. `Cases_on \`x\`` picks the
+Case split on the outermost universal. `Cases_on `x`` picks the
 variable. `FULL_CASES_TAC` is the legacy form that also splits
 hypotheses by case.
 """
@@ -161,7 +161,7 @@ canonical    = "EXISTS_TAC"
 aliases      = ["Q.EXISTS_TAC", "qexists_tac", "MAP_EVERY EXISTS_TAC"]
 tactic_class = "structural"
 notes        = """
-Witness an existential. `Q.EXISTS_TAC \`t\`` accepts a quotation
+Witness an existential. `Q.EXISTS_TAC `t`` accepts a quotation
 (parses `t` in the current goal's context). `qexists_tac` is the
 modern lower-case alias.
 """
@@ -172,7 +172,7 @@ aliases      = ["Q.SPECL", "ISPEC", "SPEC"]
 tactic_class = "lemma"
 notes        = """
 Specialise a universally-quantified theorem to a quoted term.
-`Q.SPECL [\`a\`,\`b\`]` does multiple at once. `ISPEC` infers the type
+`Q.SPECL [`a`,`b`]` does multiple at once. `ISPEC` infers the type
 from the term; bare `SPEC` requires a term of the matching type.
 """
 
@@ -230,7 +230,7 @@ canonical    = "Definition"
 aliases      = ["Define", "tDefine", "Hol_reln"]
 tactic_class = "term_builder"
 notes        = """
-`Definition name: eqn End` (modern) / `Define \`eqn\`` (classic).
+`Definition name: eqn End` (modern) / `Define `eqn`` (classic).
 `tDefine` accepts a termination-measure annotation for definitions
 whose termination isn't structural. `Hol_reln` is the inductive-
 relation variant (corresponds to `Inductive`).
@@ -315,7 +315,7 @@ canonical    = "by"
 aliases      = ["sg", "SUBGOAL_THEN", "qsuff_tac"]
 tactic_class = "structural"
 notes        = """
-HOL4 modern Theorem syntax: `\`stmt\` by tac` proves a side-lemma
+HOL4 modern Theorem syntax: ``stmt` by tac` proves a side-lemma
 and adds it as a hypothesis. `qsuff_tac` is the "it-suffices-to-show"
 form (turns the current goal into the lemma + a discharge step).
 """
@@ -325,7 +325,7 @@ canonical    = "first_assum"
 aliases      = ["pop_assum", "qpat_assum", "Q.PAT_ASSUM"]
 tactic_class = "structural"
 notes        = """
-Hypothesis lookup. `qpat_assum \`pat\` f` finds the first hypothesis
+Hypothesis lookup. `qpat_assum `pat` f` finds the first hypothesis
 matching `pat` and applies `f`. `pop_assum f` pops the most-recent
 hypothesis and applies `f` (typical use: `pop_assum mp_tac`).
 """
diff --git a/data/synonyms/schema.ncl b/data/synonyms/schema.ncl
new file mode 100644
index 00000000..d9ce06b8
--- /dev/null
+++ b/data/synonyms/schema.ncl
@@ -0,0 +1,166 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Lexicon v2 — the normative schema for every `data/synonyms/*.toml` table.
+#
+# Owner decision 2026-10-19 (D2): the lexicon schema is written in Nickel.
+# The tables stay TOML so the Rust loader (`src/rust/suggest/synonyms.rs`)
+# and the Julia mirror (`src/julia/saturation_synonyms.jl`) read them
+# unchanged; Nickel imports each table and applies `Table` to it.
+# Check one table:   nickel export <<< '(import "data/synonyms/coq.toml") | (import "data/synonyms/schema.ncl").Table'
+# Check all tables:  scripts/lexicon-check.sh
+#
+# Division of labour: this contract checks shape and the cross-field rules
+# below. Enum membership of `checked_by` (a `ProverKind` variant name) and
+# `format` (an `ExchangeFormat`) is checked by serde when Rust loads the
+# table (`tests/lexicon_v2_test.rs` loads every table), so neither list is
+# duplicated here.
+#
+# Design: docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc
+
+let fail = fun msg => 'Error { message = msg } in
+
+let is_nonempty_string = fun v => std.is_string v && v != "" in
+
+let all_nonempty_strings = fun v =>
+  std.is_array v && std.array.all is_nonempty_string v
+in
+
+# `LexiconEvidence::Probe` holds u32 counts; the contract must not certify
+# a count the Rust loader rejects.
+let is_u32 = fun v =>
+  std.is_number v && std.number.is_integer v && v >= 0 && v <= 4294967295
+in
+
+let only_fields = fun allowed r =>
+  std.array.all (fun f => std.array.elem f allowed) (std.record.fields r)
+in
+
+let unknown_fields = fun allowed r =>
+  std.array.filter (fun f => !(std.array.elem f allowed)) (std.record.fields r)
+in
+
+# How `aliases` relate to `canonical`.
+#   synonym         interchangeable names (the v1 meaning; the default)
+#   specialisation  each alias is a special case of `canonical`
+#   generalisation  each alias generalises `canonical`
+#   false_friend    each alias looks like `canonical` and is NOT it; the
+#                   variant tester never substitutes it
+#   phrase          `canonical` is a multi-token idiom spelled out in `phrase`
+let relations = ["synonym", "specialisation", "generalisation", "false_friend", "phrase"] in
+
+# The witness behind a row, mirroring the ECH-05 `FidelityEvidence` shapes.
+# Evidence attests the row's relation, whatever it is. It lifts to the
+# arbiter only for an identity claim: a `synonym` or `phrase` row whose
+# fidelity is not `lossy` (`SynonymEntry::fidelity_evidence` in Rust).
+# There `probe` lifts to `DeclaredCorrespondence` and `kernel` to
+# `KernelTranslation`; `none` and `curated` (provenance, not fidelity
+# evidence) lift to `FidelityEvidence::None`, as does every row that is
+# not an identity claim.
+let evidence_check = fun value =>
+  if !(std.is_record value) || !(std.record.has_field "kind" value) then
+    fail "evidence must be a table with a `kind` field"
+  else
+    let k = value.kind in
+    if k == "none" || k == "curated" then
+      if only_fields ["kind"] value then 'Ok value
+      else fail "evidence `%{k}` takes no other field"
+    else if k == "probe" then
+      if !(only_fields ["kind", "tests", "failures"] value)
+        || !(std.record.has_field "tests" value)
+        || !(std.record.has_field "failures" value) then
+        fail "probe evidence needs exactly `tests` and `failures`"
+      else if !(is_u32 value.tests) || !(is_u32 value.failures) then
+        fail "probe evidence `tests` and `failures` must be integers from 0 to 4294967295"
+      else if value.tests < 1 || value.failures > value.tests then
+        fail "probe evidence needs tests >= 1 and 0 <= failures <= tests"
+      else 'Ok value
+    else if k == "kernel" then
+      if !(only_fields ["kind", "format", "checked_by", "term_hash"] value)
+        || !(std.record.has_field "format" value)
+        || !(std.record.has_field "checked_by" value)
+        || !(std.record.has_field "term_hash" value) then
+        fail "kernel evidence needs exactly `format`, `checked_by` and `term_hash`"
+      else if !(is_nonempty_string value.format) || !(is_nonempty_string value.checked_by) then
+        fail "kernel evidence `format` and `checked_by` must be non-empty strings"
+      else if !(std.is_string value.term_hash)
+        || !(std.string.is_match "^[0-9a-f]{64}$" value.term_hash) then
+        fail "kernel evidence `term_hash` must be 64 lowercase hex digits (BLAKE3)"
+      else 'Ok value
+    else
+      fail "evidence kind must be one of none, curated, probe, kernel"
+in
+
+let evidence_contract = std.contract.custom (fun _label value => evidence_check value) in
+
+let entry_fields = [
+  "canonical", "aliases", "tactic_class", "semantic_class", "notes", "since", "until",
+  "relation", "phrase", "false_friends", "evidence", "fidelity", "residue", "scope",
+] in
+
+let optional_strings = ["tactic_class", "semantic_class", "notes", "since", "until"] in
+
+let entry_contract = std.contract.custom (fun _label e =>
+  if !(std.is_record e) then fail "each [[synonym]] must be a table"
+  else if !(only_fields entry_fields e) then
+    fail "unknown field(s): %{std.string.join ", " (unknown_fields entry_fields e)}"
+  else if !(std.record.has_field "canonical" e) || !(is_nonempty_string e.canonical) then
+    fail "`canonical` must be a non-empty string"
+  else if !(std.record.has_field "aliases" e) || !(all_nonempty_strings e.aliases) then
+    fail "`%{e.canonical}`: `aliases` must be an array of non-empty strings"
+  else if !(std.array.all
+      (fun f => !(std.record.has_field f e) || std.is_string (std.record.get f e))
+      optional_strings) then
+    fail "`%{e.canonical}`: tactic_class, semantic_class, notes, since and until must be strings"
+  else
+    let relation = if std.record.has_field "relation" e then e.relation else "synonym" in
+    if !(std.array.elem relation relations) then
+      fail "`%{e.canonical}`: relation must be one of %{std.string.join ", " relations}"
+    else if relation == "phrase" && !(std.record.has_field "phrase" e) then
+      fail "`%{e.canonical}`: relation `phrase` needs a `phrase` token list"
+    else if std.record.has_field "phrase" e && relation != "phrase" then
+      fail "`%{e.canonical}`: `phrase` is only allowed with relation `phrase`"
+    else if std.record.has_field "phrase" e
+      && (!(all_nonempty_strings e.phrase) || std.array.length e.phrase < 2) then
+      fail "`%{e.canonical}`: `phrase` must list at least two non-empty tokens"
+    else if relation != "synonym" && relation != "phrase" && std.array.length e.aliases == 0 then
+      fail "`%{e.canonical}`: relation `%{relation}` needs at least one alias to relate"
+    else if std.record.has_field "false_friends" e
+      && !(std.is_array e.false_friends
+        && std.array.all
+          (fun ff => std.is_record ff && only_fields ["name", "table"] ff
+            && std.record.has_field "name" ff && is_nonempty_string ff.name
+            && std.record.has_field "table" ff && is_nonempty_string ff.table)
+          e.false_friends) then
+      fail "`%{e.canonical}`: each false_friends item needs exactly a non-empty `name` and `table`"
+    else if std.record.has_field "fidelity" e && !(std.array.elem e.fidelity ["exact", "lossy"]) then
+      fail "`%{e.canonical}`: fidelity must be `exact` or `lossy`"
+    else if std.record.has_field "fidelity" e && e.fidelity == "lossy"
+      && !(std.record.has_field "residue" e && is_nonempty_string e.residue) then
+      fail "`%{e.canonical}`: a lossy correspondence must say what is lost in `residue`"
+    else if std.record.has_field "residue" e
+      && !(std.record.has_field "fidelity" e && e.fidelity == "lossy") then
+      fail "`%{e.canonical}`: `residue` is only allowed with fidelity `lossy`"
+    else if std.record.has_field "scope" e
+      && !(std.is_record e.scope && only_fields ["library", "version"] e.scope
+        && std.record.has_field "library" e.scope && is_nonempty_string e.scope.library
+        && (!(std.record.has_field "version" e.scope) || is_nonempty_string e.scope.version)) then
+      fail "`%{e.canonical}`: scope needs a non-empty `library` and optionally a `version`"
+    else
+      if std.record.has_field "evidence" e then
+        evidence_check e.evidence
+        |> match {
+          'Ok _ => 'Ok e,
+          'Error err => fail "`%{e.canonical}`: %{err.message}",
+        }
+      else
+        'Ok e
+)
+in
+
+{
+  Relation = std.contract.from_predicate (fun r => std.array.elem r relations),
+  Evidence = evidence_contract,
+  Entry = entry_contract,
+  Table = { synonym | Array entry_contract },
+}
diff --git a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc
index b754948d..30b4c41b 100644
--- a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc
+++ b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc
@@ -2,7 +2,7 @@
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 = ADR: lexicon v2 (false friends, phrases, equivalences) and hub-and-probe identity arbitration (stage 6c)
 :revdate: 2026-10-19
-:status: proposed — owner decisions D1–D5 in §7 are open; nothing below is ruled
+:status: accepted in part — D1, D2 and D4 ruled 2026-10-19 (§7); D3 and D5 open
 
 == Context (measured on `main` at `ed6ef60`, 2026-10-19)
 
@@ -294,16 +294,20 @@ re-running `metrics/run_all.jl` to re-baseline `oov_rate` and
   verdict's `level` should surface in its trust bridge once dispatch attaches
   evidence.
 
-== Open owner decisions (the selector questions this session could not ask)
+== Owner decisions
 
-[cols="1,5,3",options="header"]
+Ruled 2026-10-19 through the selector: D1, D2 and D4. D3 and D5 remain open.
+The owner also ruled the pacing: PRs 1 and 3 proceed now; PRs 4–6 (arbiter
+and ABI changes, kernel translation) wait for the stronger model.
+
+[cols="1,5,3,3",options="header"]
 |===
-| # | Question | Recommended
-| D1 | Architecture for identity arbitration: hub and probe (A + B), super-language (C), or pairwise only (D)? | A + B
-| D2 | Lexicon v2 format: extend the TOML tables in place (loader-compatible) or move `data/synonyms/` to Nickel or deed? | TOML in place
-| D3 | First consequence-probe pair: Z3 ↔ CVC5 (runs in CI today) alongside the HOL4 ↔ HOL Light hub pilot, or wait for HOL binaries in CI? | Z3 ↔ CVC5 now
-| D4 | May corpus-mined candidates set `semantic_class` automatically? | No: `evidence = none`, flag-only until curated or probe-tested
-| D5 | Open the verisimdb consonance-subject issue (option E) now? | Yes
+| # | Question | Recommended | Ruling
+| D1 | Architecture for identity arbitration: hub and probe (A + B), super-language (C), or pairwise only (D)? | A + B | A + B (hub and probe)
+| D2 | Lexicon v2 format: extend the TOML tables in place (loader-compatible) or move `data/synonyms/` to Nickel or deed? | TOML in place | Nickel. Read as: the schema is a Nickel contract (`data/synonyms/schema.ncl`) applied to the TOML tables, which stay the data so the Rust and Julia loaders are unchanged. Converting the tables themselves to `.ncl` remains open.
+| D3 | First consequence-probe pair: Z3 ↔ CVC5 (runs in CI today) alongside the HOL4 ↔ HOL Light hub pilot, or wait for HOL binaries in CI? | Z3 ↔ CVC5 now | open
+| D4 | May corpus-mined candidates set `semantic_class` automatically? | No: `evidence = none`, flag-only until curated or probe-tested | as recommended
+| D5 | Open the verisimdb consonance-subject issue (option E) now? | Yes | open
 |===
 
 == Non-claims
diff --git a/scripts/lexicon-check.sh b/scripts/lexicon-check.sh
new file mode 100755
index 00000000..1052ce59
--- /dev/null
+++ b/scripts/lexicon-check.sh
@@ -0,0 +1,67 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# lexicon-check.sh — apply the lexicon v2 Nickel contract
+# (data/synonyms/schema.ncl) to every shipped table, and prove the contract
+# still bites: every fixture under tests/lexicon_fixtures/accept/ must pass
+# and every fixture under tests/lexicon_fixtures/reject/ must fail.
+#
+# Usage: scripts/lexicon-check.sh        (from the repository root)
+# Needs: nickel (>= 1.12) on PATH, or NICKEL=/path/to/nickel.
+set -euo pipefail
+
+nickel="${NICKEL:-nickel}"
+command -v "$nickel" >/dev/null || { echo "lexicon-check: nickel not found (set NICKEL)" >&2; exit 2; }
+root="$(pwd)"
+schema="$root/data/synonyms/schema.ncl"
+[ -f "$schema" ] || { echo "lexicon-check: run from the repository root" >&2; exit 2; }
+
+# check FILE -> exit status of applying the contract to FILE.
+check() {
+  printf '(import "%s") | (import "%s").Table\n' "$1" "$schema" \
+    | "$nickel" export --format json >/dev/null 2>"$errfile"
+}
+
+errfile="$(mktemp)"
+trap 'rm -f "$errfile"' EXIT
+bad=0 n=0
+
+# An unmatched glob must not pass as a file (it would "fail" to load and so
+# count as a rejection), and an empty set must not pass silently.
+shopt -s nullglob
+tables=("$root"/data/synonyms/*.toml)
+accepts=("$root"/tests/lexicon_fixtures/accept/*.toml)
+rejects=("$root"/tests/lexicon_fixtures/reject/*.toml)
+shopt -u nullglob
+for set in tables accepts rejects; do
+  declare -n files="$set"
+  if [ "${#files[@]}" -eq 0 ]; then
+    echo "lexicon-check: no $set found; refusing to pass an empty set" >&2
+    exit 1
+  fi
+  unset -n files
+done
+
+for f in "${tables[@]}" "${accepts[@]}"; do
+  n=$((n + 1))
+  if ! check "$f"; then
+    echo "FAIL (must pass): ${f#"$root"/}"
+    sed -n '1,12p' "$errfile"
+    bad=$((bad + 1))
+  fi
+done
+
+for f in "${rejects[@]}"; do
+  n=$((n + 1))
+  if check "$f"; then
+    echo "FAIL (must be rejected): ${f#"$root"/}"
+    bad=$((bad + 1))
+  fi
+done
+
+if [ "$bad" -ne 0 ]; then
+  echo "lexicon-check: $bad of $n files failed"
+  exit 1
+fi
+echo "lexicon-check: $n files, all as expected"
diff --git a/src/julia/saturation_synonyms.jl b/src/julia/saturation_synonyms.jl
index 3a22681f..7abb6bd7 100644
--- a/src/julia/saturation_synonyms.jl
+++ b/src/julia/saturation_synonyms.jl
@@ -24,7 +24,7 @@ dictionaries (`_msc2020`, `_wordnet_math`, `_conceptnet_seed`) added in
 the saturation campaign.
 
 Each entry exposes `(canonical, aliases, tactic_class, semantic_class,
-notes, since, until)`. The cross-prover lookup `by_semantic_class`
+notes, since, until, relation)`. The cross-prover lookup `by_semantic_class`
 mirrors `src/rust/suggest/synonyms.rs::SynonymTable::by_semantic_class`
 and is the load-bearing primitive for cross-corpus equivalence in the
 S5 verification gate.
@@ -44,6 +44,12 @@ export load_prover_synonyms,
        by_semantic_class,
        expand_aliases
 
+# Lexicon v2 relations whose aliases are interchangeable with the
+# canonical name. Mirrors `Relation::interchangeable` in
+# `src/rust/suggest/synonyms.rs`: specialisations, generalisations and
+# false friends are never expanded as synonyms.
+const INTERCHANGEABLE_RELATIONS = ("synonym", "phrase")
+
 # ----------------------------------------------------------------------
 # Per-prover loader
 # ----------------------------------------------------------------------
@@ -53,7 +59,8 @@ export load_prover_synonyms,
 
 Load `dir/<prover>.toml` and return a `Dict{String, NamedTuple}` keyed
 by the canonical name. Each value is a NamedTuple with fields
-`(:aliases, :tactic_class, :semantic_class, :notes, :since, :until)`.
+`(:aliases, :tactic_class, :semantic_class, :notes, :since, :until,
+:relation)`; `relation` defaults to `"synonym"` as in the Rust loader.
 
 The TOML schema is `[[synonym]]` rows, each with the same fields as
 `src/rust/suggest/synonyms.rs::SynonymEntry`. Missing optional fields
@@ -85,6 +92,7 @@ function load_prover_synonyms(prover::Symbol, dir::String)
             notes = _opt_string(get(row, "notes", nothing)),
             since = _opt_string(get(row, "since", nothing)),
             until = _opt_string(get(row, "until", nothing)),
+            relation = String(get(row, "relation", "synonym")),
         )
     end
     return table
@@ -185,6 +193,9 @@ end
 
 Given a name (canonical or alias), return every OTHER name in the same
 entry. Mirrors `src/rust/suggest/synonyms.rs::SynonymTable::alternatives`.
+Only `synonym` and `phrase` rows are expanded (lexicon v2): a false friend,
+specialisation or generalisation is not a synonym and must not reach the
+GNN training data as one.
 
 Returns an empty vector if `name` is not present in `table`. The result
 is sorted and de-duplicated to match the Rust contract.
@@ -193,6 +204,7 @@ function expand_aliases(name::String, table::Dict)
     out = String[]
     for (canonical, entry) in table
         entry isa NamedTuple || continue
+        get(entry, :relation, "synonym") in INTERCHANGEABLE_RELATIONS || continue
         if String(canonical) == name
             for alias in entry.aliases
                 alias == name || push!(out, alias)
@@ -238,6 +250,7 @@ function _load_underscore_table(dir::String, filename::String)
             notes = _opt_string(get(row, "notes", nothing)),
             since = _opt_string(get(row, "since", nothing)),
             until = _opt_string(get(row, "until", nothing)),
+            relation = String(get(row, "relation", "synonym")),
         )
     end
     return table
diff --git a/src/rust/suggest/synonyms.rs b/src/rust/suggest/synonyms.rs
index 6902809e..6f4ec3ff 100644
--- a/src/rust/suggest/synonyms.rs
+++ b/src/rust/suggest/synonyms.rs
@@ -9,17 +9,139 @@ use std::collections::HashMap;
 use std::path::Path;
 
 use anyhow::{Context, Result};
-use serde::Deserialize;
+use serde::{Deserialize, Serialize};
 
+use crate::exchange::ExchangeFormat;
+use crate::verification::FidelityEvidence;
 use crate::ProverKind;
 
-#[derive(Debug, Clone, Deserialize)]
+/// How a row's `aliases` relate to its `canonical` name (lexicon v2).
+///
+/// The schema of record is `data/synonyms/schema.ncl`; see
+/// `docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc`.
+#[derive(
+    Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default, Deserialize, Serialize,
+)]
+#[serde(rename_all = "snake_case")]
+pub enum Relation {
+    /// Interchangeable names (the v1 meaning).
+    #[default]
+    Synonym,
+    /// Each alias is a special case of `canonical`.
+    Specialisation,
+    /// Each alias generalises `canonical`.
+    Generalisation,
+    /// Each alias looks like `canonical` and is not it. Never substituted.
+    FalseFriend,
+    /// `canonical` is a multi-token idiom spelled out in `phrase`.
+    ///
+    /// Substitution runs one way today: an alias found at a tactic site
+    /// can be replaced by the phrase spelling, but the extractors record
+    /// single identifiers, so a canonical phrase in a proof is never a
+    /// site and is not replaced by an alias. That direction needs
+    /// phrase-aware site detection.
+    Phrase,
+}
+
+impl Relation {
+    /// Whether the variant tester may substitute an alias for the
+    /// canonical name (and back). Only synonyms and phrase spellings are
+    /// interchangeable; specialisations, generalisations and false friends
+    /// are reported by [`SynonymTable::related`] instead.
+    pub fn interchangeable(self) -> bool {
+        matches!(self, Relation::Synonym | Relation::Phrase)
+    }
+}
+
+/// The witness behind a lexicon row. Mirrors the ECH-05
+/// [`FidelityEvidence`] shapes. It attests the row's relation, whatever
+/// that is; only [`SynonymEntry::fidelity_evidence`] lifts it to the arbiter.
+#[derive(Debug, Clone, PartialEq, Eq, Default, Deserialize, Serialize)]
+#[serde(tag = "kind", rename_all = "snake_case", deny_unknown_fields)]
+pub enum LexiconEvidence {
+    /// No evidence (the default, and the only value a corpus-mined
+    /// candidate may carry: owner decision D4).
+    #[default]
+    None,
+    /// A person curated the row. Provenance only, not fidelity evidence.
+    Curated,
+    /// Consequence-tested correspondence.
+    Probe { tests: u32, failures: u32 },
+    /// Kernel-checked translation through the exchange layer.
+    Kernel {
+        format: ExchangeFormat,
+        checked_by: ProverKind,
+        term_hash: String,
+    },
+}
+
+impl LexiconEvidence {
+    /// The shape-for-shape lift, without the row's context. Private: a
+    /// probe on a false friend or a lossy row must not reach the arbiter
+    /// as identity evidence, so callers go through
+    /// [`SynonymEntry::fidelity_evidence`].
+    fn lift(&self) -> FidelityEvidence {
+        match self {
+            LexiconEvidence::None | LexiconEvidence::Curated => FidelityEvidence::None,
+            LexiconEvidence::Probe { tests, failures } => {
+                FidelityEvidence::DeclaredCorrespondence {
+                    consequence_tests: *tests,
+                    failures: *failures,
+                }
+            },
+            LexiconEvidence::Kernel {
+                format,
+                checked_by,
+                term_hash,
+            } => FidelityEvidence::KernelTranslation {
+                format: *format,
+                checked_by: *checked_by,
+                term_hash: term_hash.clone(),
+            },
+        }
+    }
+}
+
+/// A name in another table that looks like this entry and is not it.
+#[derive(Debug, Clone, PartialEq, Eq, Deserialize, Serialize)]
+#[serde(deny_unknown_fields)]
+pub struct FalseFriend {
+    pub name: String,
+    /// The other table's file stem, e.g. `"lean4"` or `"metamath"`.
+    pub table: String,
+}
+
+/// Whether a correspondence loses information, after echo-types'
+/// loss-with-residue formalism.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Deserialize, Serialize)]
+#[serde(rename_all = "snake_case")]
+pub enum Fidelity {
+    Exact,
+    /// Lossy: the row's `residue` says what is lost.
+    Lossy,
+}
+
+/// The library (and optionally version) a relation holds in.
+#[derive(Debug, Clone, PartialEq, Eq, Deserialize, Serialize)]
+#[serde(deny_unknown_fields)]
+pub struct Scope {
+    pub library: String,
+    #[serde(default)]
+    pub version: Option<String>,
+}
+
+#[derive(Debug, Clone, Default, Deserialize)]
+#[serde(deny_unknown_fields)]
 pub struct SynonymEntry {
     pub canonical: String,
     pub aliases: Vec<String>,
+    #[serde(default)]
     pub tactic_class: Option<String>,
+    #[serde(default)]
     pub notes: Option<String>,
+    #[serde(default)]
     pub since: Option<String>,
+    #[serde(default)]
     pub until: Option<String>,
     /// Cross-prover semantic class. Two entries (potentially from
     /// different prover synonym tables) sharing the same
@@ -30,6 +152,53 @@ pub struct SynonymEntry {
     /// Dedukti exchange layer (`src/rust/exchange/`).
     #[serde(default)]
     pub semantic_class: Option<String>,
+    // ---- lexicon v2 (all optional; v1 rows load unchanged) ----
+    /// How `aliases` relate to `canonical`; defaults to `synonym`.
+    #[serde(default)]
+    pub relation: Relation,
+    /// Token spelling of a multi-token idiom (relation `phrase`).
+    #[serde(default)]
+    pub phrase: Option<Vec<String>>,
+    /// Look-alike names in other tables that are not this entry.
+    #[serde(default)]
+    pub false_friends: Vec<FalseFriend>,
+    #[serde(default)]
+    pub evidence: LexiconEvidence,
+    #[serde(default)]
+    pub fidelity: Option<Fidelity>,
+    /// What a lossy correspondence loses.
+    #[serde(default)]
+    pub residue: Option<String>,
+    #[serde(default)]
+    pub scope: Option<Scope>,
+}
+
+impl SynonymEntry {
+    /// Whether the row claims identity: its aliases are interchangeable
+    /// with `canonical` ([`Relation::interchangeable`]) and nothing is
+    /// lost between them (fidelity not [`Fidelity::Lossy`]).
+    pub fn claims_identity(&self) -> bool {
+        self.relation.interchangeable() && self.fidelity != Some(Fidelity::Lossy)
+    }
+
+    /// The arbiter's evidence for this row.
+    ///
+    /// Only an identity claim ([`Self::claims_identity`]) lifts its
+    /// evidence: probe to [`FidelityEvidence::DeclaredCorrespondence`],
+    /// kernel to [`FidelityEvidence::KernelTranslation`]. Every other row
+    /// gives [`FidelityEvidence::None`], whatever it carries: a probe on a
+    /// false friend, a specialisation or a lossy row attests that
+    /// relation, not identity, and must not raise an attempt's
+    /// fidelity level. `none` and `curated` also give
+    /// [`FidelityEvidence::None`]. Field values are carried over without
+    /// validation.
+    pub fn fidelity_evidence(&self) -> FidelityEvidence {
+        if self.claims_identity() {
+            self.evidence.lift()
+        } else {
+            FidelityEvidence::None
+        }
+    }
 }
 
 /// Parsed and indexed synonym table for a single prover.
@@ -48,15 +217,52 @@ struct RawTable {
 
 impl SynonymTable {
     /// Load the table for `prover` from `dir/<prover-name>.toml`.
+    ///
+    /// Returns an empty table if the path is missing or its existence
+    /// cannot be checked.
+    ///
+    /// # Errors
+    ///
+    /// If the path exists, propagates the read and parse errors from
+    /// [`Self::load_path`].
     pub fn load(prover: ProverKind, dir: &Path) -> Result<Self> {
         let filename = prover_table_filename(prover);
         let path = dir.join(&filename);
         if !path.exists() {
             return Ok(Self::default());
         }
-        let raw = crate::provers::bounded_read_corpus_file(&path)?;
+        Self::load_path(&path)
+    }
+
+    /// Load one table file, whatever its name (per-prover or an
+    /// underscore-prefixed cross-prover dictionary).
+    ///
+    /// Indexes canonical names and aliases. The Nickel contract's
+    /// cross-field rules are not checked here.
+    ///
+    /// # Errors
+    ///
+    /// Returns an error if the file cannot be opened or read as UTF-8,
+    /// exceeds 64 MiB, cannot be deserialised as a synonym table, or has
+    /// a row with an empty canonical name or alias.
+    pub fn load_path(path: &Path) -> Result<Self> {
+        let raw = crate::provers::bounded_read_corpus_file(path)?;
         let parsed: RawTable =
             toml::from_str(&raw).with_context(|| format!("Failed to parse {}", path.display()))?;
+        // An empty name would be offered as a replacement that deletes
+        // the matched tactic. The contract refuses it too; this keeps an
+        // unchecked table from reaching the variant tester.
+        if let Some(entry) = parsed
+            .synonyms
+            .iter()
+            .find(|e| e.canonical.is_empty() || e.aliases.iter().any(String::is_empty))
+        {
+            anyhow::bail!(
+                "{}: row `{}` has an empty canonical name or alias",
+                path.display(),
+                entry.canonical
+            );
+        }
         Ok(Self::from_entries(parsed.synonyms))
     }
 
@@ -71,7 +277,15 @@ impl SynonymTable {
         SynonymTable { entries, by_name }
     }
 
-    /// All names in the same entry as `name`, excluding `name` itself.
+    /// All names interchangeable with `name`, excluding `name` itself.
+    ///
+    /// Only rows whose [`Relation`] is interchangeable (synonym, phrase)
+    /// contribute: a false friend, specialisation or generalisation is
+    /// never offered as a drop-in replacement. Use [`Self::related`]
+    /// for those.
+    ///
+    /// Matches names exactly and returns sorted, deduplicated names.
+    /// Returns an empty vector if `name` is unknown.
     pub fn alternatives(&self, name: &str) -> Vec<String> {
         let indices = match self.by_name.get(name) {
             Some(v) => v,
@@ -80,6 +294,9 @@ impl SynonymTable {
         let mut out = Vec::new();
         for &i in indices {
             let entry = &self.entries[i];
+            if !entry.relation.interchangeable() {
+                continue;
+            }
             if entry.canonical != name {
                 out.push(entry.canonical.clone());
             }
@@ -94,6 +311,41 @@ impl SynonymTable {
         out
     }
 
+    /// Names related to `name` by a non-interchangeable [`Relation`],
+    /// each with the relation read from `name`'s side: if `name` is the
+    /// canonical of a `specialisation` row, every alias is a
+    /// specialisation of it; if `name` is one of those aliases, the
+    /// canonical is its generalisation. False friends are symmetric.
+    ///
+    /// Matches names exactly and returns sorted, deduplicated pairs.
+    /// An alias lookup returns only the canonical name from each row,
+    /// not the other aliases. The separate `false_friends` metadata is
+    /// not searched. Returns an empty vector if `name` is unknown.
+    pub fn related(&self, name: &str) -> Vec<(String, Relation)> {
+        let mut out = Vec::new();
+        for &i in self.by_name.get(name).map(Vec::as_slice).unwrap_or(&[]) {
+            let entry = &self.entries[i];
+            if entry.relation.interchangeable() {
+                continue;
+            }
+            if entry.canonical == name {
+                for alias in &entry.aliases {
+                    out.push((alias.clone(), entry.relation));
+                }
+            } else {
+                let inverse = match entry.relation {
+                    Relation::Specialisation => Relation::Generalisation,
+                    Relation::Generalisation => Relation::Specialisation,
+                    other => other,
+                };
+                out.push((entry.canonical.clone(), inverse));
+            }
+        }
+        out.sort();
+        out.dedup();
+        out
+    }
+
     pub fn is_empty(&self) -> bool {
         self.entries.is_empty()
     }
@@ -242,6 +494,7 @@ mod tests {
                 since: None,
                 until: None,
                 semantic_class: None,
+                ..Default::default()
             },
             SynonymEntry {
                 canonical: "linarith".to_string(),
@@ -251,6 +504,7 @@ mod tests {
                 since: None,
                 until: None,
                 semantic_class: None,
+                ..Default::default()
             },
         ])
     }
diff --git a/src/rust/suggest/variant.rs b/src/rust/suggest/variant.rs
index 98197b10..aa52b47a 100644
--- a/src/rust/suggest/variant.rs
+++ b/src/rust/suggest/variant.rs
@@ -183,6 +183,7 @@ mod tests {
             since: None,
             until: None,
             semantic_class: None,
+            ..Default::default()
         }])
     }
 
diff --git a/tests/lexicon_fixtures/accept/v2_all_fields.toml b/tests/lexicon_fixtures/accept/v2_all_fields.toml
new file mode 100644
index 00000000..38417db1
--- /dev/null
+++ b/tests/lexicon_fixtures/accept/v2_all_fields.toml
@@ -0,0 +1,32 @@
+# SPDX-License-Identifier: MPL-2.0
+# Every lexicon v2 field, valid. Must pass data/synonyms/schema.ncl.
+[[synonym]]
+canonical = "omega"
+aliases = ["lia"]
+
+[[synonym]]
+canonical = "NN"
+aliases = ["NN0"]
+relation = "false_friend"
+false_friends = [{ name = "Nat", table = "lean4" }]
+evidence = { kind = "curated" }
+
+[[synonym]]
+canonical = "le_trans"
+aliases = ["Rle_trans"]
+relation = "specialisation"
+fidelity = "lossy"
+residue = "Rle_trans fixes the carrier to R"
+scope = { library = "Coq.Reals", version = "8.18" }
+evidence = { kind = "probe", tests = 12, failures = 0 }
+
+[[synonym]]
+canonical = "then thus"
+aliases = ["hence"]
+relation = "phrase"
+phrase = ["then", "thus"]
+
+[[synonym]]
+canonical = "add_comm"
+aliases = ["Nat.add_comm"]
+evidence = { kind = "kernel", format = "dedukti", checked_by = "Dedukti", term_hash = "af1349b9f5f9a1a6a0404dea36dcc9499bcb25c9adc112b7cc9a93cae41f3262" }
diff --git a/tests/lexicon_fixtures/reject/bad_relation.toml b/tests/lexicon_fixtures/reject/bad_relation.toml
new file mode 100644
index 00000000..024c6e8f
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/bad_relation.toml
@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Must be rejected by data/synonyms/schema.ncl: a relation outside the closed set
+[[synonym]]
+canonical = "x"
+aliases = ["y"]
+relation = "antonym"
diff --git a/tests/lexicon_fixtures/reject/curated_with_counts.toml b/tests/lexicon_fixtures/reject/curated_with_counts.toml
new file mode 100644
index 00000000..aaba544e
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/curated_with_counts.toml
@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Must be rejected by data/synonyms/schema.ncl: curated evidence carrying probe counts
+[[synonym]]
+canonical = "x"
+aliases = ["y"]
+evidence = { kind = "curated", tests = 3, failures = 0 }
diff --git a/tests/lexicon_fixtures/reject/empty_alias.toml b/tests/lexicon_fixtures/reject/empty_alias.toml
new file mode 100644
index 00000000..a3dc0f23
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/empty_alias.toml
@@ -0,0 +1,5 @@
+# SPDX-License-Identifier: MPL-2.0
+# An empty alias would be offered as a replacement that deletes the tactic.
+[[synonym]]
+canonical = "omega"
+aliases = ["lia", ""]
diff --git a/tests/lexicon_fixtures/reject/empty_canonical.toml b/tests/lexicon_fixtures/reject/empty_canonical.toml
new file mode 100644
index 00000000..9665b852
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/empty_canonical.toml
@@ -0,0 +1,5 @@
+# SPDX-License-Identifier: MPL-2.0
+# Must be rejected by data/synonyms/schema.ncl: an empty canonical name
+[[synonym]]
+canonical = ""
+aliases = ["y"]
diff --git a/tests/lexicon_fixtures/reject/false_friend_item_shape.toml b/tests/lexicon_fixtures/reject/false_friend_item_shape.toml
new file mode 100644
index 00000000..0fbc9762
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/false_friend_item_shape.toml
@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Must be rejected by data/synonyms/schema.ncl: a false_friends item without its table
+[[synonym]]
+canonical = "x"
+aliases = ["y"]
+false_friends = [{ name = "Nat" }]
diff --git a/tests/lexicon_fixtures/reject/false_friend_no_alias.toml b/tests/lexicon_fixtures/reject/false_friend_no_alias.toml
new file mode 100644
index 00000000..42ba4e81
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/false_friend_no_alias.toml
@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Must be rejected by data/synonyms/schema.ncl: a false-friend row with nothing to relate
+[[synonym]]
+canonical = "x"
+aliases = []
+relation = "false_friend"
diff --git a/tests/lexicon_fixtures/reject/kernel_short_hash.toml b/tests/lexicon_fixtures/reject/kernel_short_hash.toml
new file mode 100644
index 00000000..c9b7cd80
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/kernel_short_hash.toml
@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Must be rejected by data/synonyms/schema.ncl: kernel evidence with a hash that is not BLAKE3 hex
+[[synonym]]
+canonical = "x"
+aliases = ["y"]
+evidence = { kind = "kernel", format = "dedukti", checked_by = "Dedukti", term_hash = "abc" }
diff --git a/tests/lexicon_fixtures/reject/kernel_without_checker.toml b/tests/lexicon_fixtures/reject/kernel_without_checker.toml
new file mode 100644
index 00000000..ef87a710
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/kernel_without_checker.toml
@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Must be rejected by data/synonyms/schema.ncl: kernel evidence missing checked_by
+[[synonym]]
+canonical = "x"
+aliases = ["y"]
+evidence = { kind = "kernel", format = "dedukti", term_hash = "af1349b9f5f9a1a6a0404dea36dcc9499bcb25c9adc112b7cc9a93cae41f3262" }
diff --git a/tests/lexicon_fixtures/reject/lossy_without_residue.toml b/tests/lexicon_fixtures/reject/lossy_without_residue.toml
new file mode 100644
index 00000000..3f2bcc4c
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/lossy_without_residue.toml
@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Must be rejected by data/synonyms/schema.ncl: a lossy correspondence that does not say what is lost
+[[synonym]]
+canonical = "x"
+aliases = ["y"]
+fidelity = "lossy"
diff --git a/tests/lexicon_fixtures/reject/phrase_on_synonym.toml b/tests/lexicon_fixtures/reject/phrase_on_synonym.toml
new file mode 100644
index 00000000..b4028fe1
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/phrase_on_synonym.toml
@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Must be rejected by data/synonyms/schema.ncl: a phrase list on a non-phrase row
+[[synonym]]
+canonical = "x"
+aliases = ["y"]
+phrase = ["a", "b"]
diff --git a/tests/lexicon_fixtures/reject/phrase_without_tokens.toml b/tests/lexicon_fixtures/reject/phrase_without_tokens.toml
new file mode 100644
index 00000000..edcc0129
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/phrase_without_tokens.toml
@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Must be rejected by data/synonyms/schema.ncl: relation phrase without a phrase list
+[[synonym]]
+canonical = "then thus"
+aliases = ["hence"]
+relation = "phrase"
diff --git a/tests/lexicon_fixtures/reject/probe_fractional.toml b/tests/lexicon_fixtures/reject/probe_fractional.toml
new file mode 100644
index 00000000..45bb28b6
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/probe_fractional.toml
@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Probe counts are u32 in Rust; a fractional count must not pass the contract.
+[[synonym]]
+canonical = "omega"
+aliases = ["lia"]
+evidence = { kind = "probe", tests = 1.5, failures = 0 }
diff --git a/tests/lexicon_fixtures/reject/probe_more_failures.toml b/tests/lexicon_fixtures/reject/probe_more_failures.toml
new file mode 100644
index 00000000..f855221b
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/probe_more_failures.toml
@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Must be rejected by data/synonyms/schema.ncl: more failures than tests
+[[synonym]]
+canonical = "x"
+aliases = ["y"]
+evidence = { kind = "probe", tests = 2, failures = 3 }
diff --git a/tests/lexicon_fixtures/reject/probe_over_u32.toml b/tests/lexicon_fixtures/reject/probe_over_u32.toml
new file mode 100644
index 00000000..2483f82e
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/probe_over_u32.toml
@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Probe counts are u32 in Rust; 2^32 is out of range.
+[[synonym]]
+canonical = "omega"
+aliases = ["lia"]
+evidence = { kind = "probe", tests = 4294967296, failures = 0 }
diff --git a/tests/lexicon_fixtures/reject/probe_zero_tests.toml b/tests/lexicon_fixtures/reject/probe_zero_tests.toml
new file mode 100644
index 00000000..60cc32a8
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/probe_zero_tests.toml
@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Must be rejected by data/synonyms/schema.ncl: a probe with no tests
+[[synonym]]
+canonical = "x"
+aliases = ["y"]
+evidence = { kind = "probe", tests = 0, failures = 0 }
diff --git a/tests/lexicon_fixtures/reject/residue_on_exact.toml b/tests/lexicon_fixtures/reject/residue_on_exact.toml
new file mode 100644
index 00000000..c40b6d9a
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/residue_on_exact.toml
@@ -0,0 +1,7 @@
+# SPDX-License-Identifier: MPL-2.0
+# Must be rejected by data/synonyms/schema.ncl: a residue on an exact correspondence
+[[synonym]]
+canonical = "x"
+aliases = ["y"]
+fidelity = "exact"
+residue = "nothing"
diff --git a/tests/lexicon_fixtures/reject/unknown_field.toml b/tests/lexicon_fixtures/reject/unknown_field.toml
new file mode 100644
index 00000000..ade20225
--- /dev/null
+++ b/tests/lexicon_fixtures/reject/unknown_field.toml
@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Must be rejected by data/synonyms/schema.ncl: a misspelt field
+[[synonym]]
+canonical = "x"
+aliases = []
+relaton = "phrase"
diff --git a/tests/lexicon_v2_test.rs b/tests/lexicon_v2_test.rs
new file mode 100644
index 00000000..2099ae3c
--- /dev/null
+++ b/tests/lexicon_v2_test.rs
@@ -0,0 +1,211 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+//! Lexicon v2: every shipped table loads, v2 fields parse, false friends
+//! are never offered as substitutes, and lexicon evidence lifts to the
+//! arbiter's fidelity evidence only for an identity claim.
+//!
+//! The normative shape check is the Nickel contract
+//! `data/synonyms/schema.ncl` (`scripts/lexicon-check.sh`); this suite
+//! covers what Nickel does not: enum membership of `checked_by` /
+//! `format` (serde), and the loader's behaviour.
+
+use std::path::{Path, PathBuf};
+
+use echidna::exchange::ExchangeFormat;
+use echidna::provers::ProverKind;
+use echidna::suggest::synonyms::{
+    load_all, load_cross_prover_dicts, LexiconEvidence, Relation, SynonymTable,
+};
+use echidna::verification::FidelityEvidence;
+
+fn synonyms_dir() -> PathBuf {
+    Path::new(env!("CARGO_MANIFEST_DIR")).join("data/synonyms")
+}
+
+#[test]
+fn every_shipped_table_loads() {
+    let mut loaded = 0;
+    for entry in std::fs::read_dir(synonyms_dir()).unwrap() {
+        let path = entry.unwrap().path();
+        if path.extension().and_then(|e| e.to_str()) != Some("toml") {
+            continue;
+        }
+        let table =
+            SynonymTable::load_path(&path).unwrap_or_else(|e| panic!("{}: {e:#}", path.display()));
+        assert!(!table.is_empty(), "{} has no rows", path.display());
+        loaded += 1;
+    }
+    assert!(
+        loaded >= 18,
+        "expected the 18 shipped tables, found {loaded}"
+    );
+}
+
+#[test]
+fn load_all_and_cross_prover_dicts_succeed() {
+    let tables = load_all(&synonyms_dir()).expect("load_all");
+    assert!(tables.contains_key(&ProverKind::HOL4), "HOL4 table missing");
+    load_cross_prover_dicts(&synonyms_dir()).expect("cross-prover dicts");
+}
+
+const V2_TABLE: &str = r#"
+[[synonym]]
+canonical = "omega"
+aliases = ["lia"]
+
+[[synonym]]
+canonical = "NN"
+aliases = ["NN0"]
+relation = "false_friend"
+false_friends = [{ name = "Nat", table = "lean4" }]
+evidence = { kind = "curated" }
+
+[[synonym]]
+canonical = "le_trans"
+aliases = ["Rle_trans"]
+relation = "specialisation"
+fidelity = "lossy"
+residue = "Rle_trans fixes the carrier to R"
+scope = { library = "Coq.Reals", version = "8.18" }
+evidence = { kind = "probe", tests = 12, failures = 0 }
+
+[[synonym]]
+canonical = "then thus"
+aliases = ["hence"]
+relation = "phrase"
+phrase = ["then", "thus"]
+
+[[synonym]]
+canonical = "add_comm"
+aliases = ["Nat.add_comm"]
+evidence = { kind = "kernel", format = "dedukti", checked_by = "Dedukti", term_hash = "0000000000000000000000000000000000000000000000000000000000000000" }
+
+[[synonym]]
+canonical = "lt_irrefl"
+aliases = ["Nat.lt_irrefl"]
+evidence = { kind = "probe", tests = 8, failures = 0 }
+
+[[synonym]]
+canonical = "Rplus_comm"
+aliases = ["plus_comm_R"]
+fidelity = "lossy"
+residue = "Rplus_comm fixes the carrier to R"
+evidence = { kind = "kernel", format = "dedukti", checked_by = "Dedukti", term_hash = "1111111111111111111111111111111111111111111111111111111111111111" }
+"#;
+
+fn v2_table() -> SynonymTable {
+    #[derive(serde::Deserialize)]
+    struct Raw {
+        synonym: Vec<echidna::suggest::synonyms::SynonymEntry>,
+    }
+    let raw: Raw = toml::from_str(V2_TABLE).expect("v2 fixture parses");
+    SynonymTable::from_entries(raw.synonym)
+}
+
+#[test]
+fn false_friends_are_never_alternatives() {
+    let t = v2_table();
+    assert!(t.alternatives("NN").is_empty());
+    assert!(t.alternatives("NN0").is_empty());
+    assert_eq!(
+        t.related("NN"),
+        vec![("NN0".to_string(), Relation::FalseFriend)]
+    );
+    // v1 rows keep their meaning.
+    assert_eq!(t.alternatives("omega"), vec!["lia".to_string()]);
+}
+
+#[test]
+fn specialisation_is_related_not_substituted_and_inverts() {
+    let t = v2_table();
+    assert!(t.alternatives("le_trans").is_empty());
+    assert_eq!(
+        t.related("le_trans"),
+        vec![("Rle_trans".to_string(), Relation::Specialisation)]
+    );
+    assert_eq!(
+        t.related("Rle_trans"),
+        vec![("le_trans".to_string(), Relation::Generalisation)]
+    );
+}
+
+#[test]
+fn phrase_spellings_are_interchangeable() {
+    let t = v2_table();
+    assert_eq!(t.alternatives("hence"), vec!["then thus".to_string()]);
+}
+
+#[test]
+fn only_identity_claims_lift_their_evidence() {
+    let t = v2_table();
+    let by = |c: &str| t.entries.iter().find(|e| e.canonical == c).unwrap();
+    assert_eq!(by("omega").evidence, LexiconEvidence::None);
+    assert_eq!(by("omega").fidelity_evidence(), FidelityEvidence::None);
+    // Curated is provenance, not fidelity evidence.
+    assert_eq!(by("NN").fidelity_evidence(), FidelityEvidence::None);
+    // A failure-free probe on a lossy specialisation attests that
+    // relation, not identity: it is kept but never reaches the arbiter.
+    assert_eq!(
+        by("le_trans").evidence,
+        LexiconEvidence::Probe {
+            tests: 12,
+            failures: 0
+        }
+    );
+    assert!(!by("le_trans").claims_identity());
+    assert_eq!(by("le_trans").fidelity_evidence(), FidelityEvidence::None);
+    // The same probe on an exact synonym lifts.
+    assert_eq!(
+        by("lt_irrefl").fidelity_evidence(),
+        FidelityEvidence::DeclaredCorrespondence {
+            consequence_tests: 8,
+            failures: 0
+        }
+    );
+    // A kernel check on a lossy synonym does not lift either.
+    assert!(!by("Rplus_comm").claims_identity());
+    assert_eq!(by("Rplus_comm").fidelity_evidence(), FidelityEvidence::None);
+    match by("add_comm").fidelity_evidence() {
+        FidelityEvidence::KernelTranslation {
+            format, checked_by, ..
+        } => {
+            assert_eq!(format, ExchangeFormat::Dedukti);
+            assert_eq!(checked_by, ProverKind::Dedukti);
+        },
+        other => panic!("expected a kernel translation, got {other:?}"),
+    }
+}
+
+/// The contract and the loader must agree: what Nickel refuses for a
+/// probe count or an empty name, the loader refuses too, and the u32
+/// boundary passes both.
+#[test]
+fn loader_agrees_with_contract_on_counts_and_empty_names() {
+    let fixtures = Path::new(env!("CARGO_MANIFEST_DIR")).join("tests/lexicon_fixtures/reject");
+    for name in ["empty_alias", "probe_fractional", "probe_over_u32"] {
+        let path = fixtures.join(format!("{name}.toml"));
+        assert!(
+            SynonymTable::load_path(&path).is_err(),
+            "{name} must not load"
+        );
+    }
+    let boundary = "[[synonym]]\ncanonical = \"a\"\naliases = [\"b\"]\nevidence = { kind = \"probe\", tests = 4294967295, failures = 4294967295 }\n";
+    SynonymTable::load_path(&write_tmp("boundary.toml", boundary)).expect("u32::MAX loads");
+}
+
+#[test]
+fn unknown_fields_and_prover_names_are_rejected() {
+    let typo = "[[synonym]]\ncanonical = \"x\"\naliases = []\nrelaton = \"phrase\"\n";
+    assert!(SynonymTable::load_path(&write_tmp("typo.toml", typo)).is_err());
+    let bad_prover = "[[synonym]]\ncanonical = \"x\"\naliases = []\nevidence = { kind = \"kernel\", format = \"dedukti\", checked_by = \"NoSuchProver\", term_hash = \"00\" }\n";
+    assert!(SynonymTable::load_path(&write_tmp("prover.toml", bad_prover)).is_err());
+}
+
+fn write_tmp(name: &str, body: &str) -> PathBuf {
+    let dir = std::env::temp_dir().join(format!("echidna-lexicon-v2-{}", std::process::id()));
+    std::fs::create_dir_all(&dir).unwrap();
+    let path = dir.join(name);
+    std::fs::write(&path, body).unwrap();
+    path
+}