From eb5d5817e3d2d81b7008ca890a1b6007c470b1ad Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <j.d.a.jewell@open.ac.uk>
Date: Mon, 19 Oct 2026 22:14:34 +0000
Subject: [PATCH 1/9] docs(decisions): lexicon v2 and hub-and-probe identity
 arbitration ADR, with the false-friend census
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Propose the next step past per-prover synonyms: a lexicon schema that can
record false friends, phrases, specialisations and equivalences with a
witness, and an identity-arbitration architecture (λΠ hub for `sound`,
consequence-partition probes for `epi`) that maps onto the two ECH-05
fidelity constructors without arbiter or ABI changes.

Add scripts/false_friend_scan.sh, a deterministic jq + coreutils census over
training_data/proof_states_*.jsonl. On the owner's first stage-6a pair
(HOL4 ↔ HOL Light) it finds 5,060 shared theorem names, 1,030 cognate
statements and 10,460 differing statement pairs, most of them type
generalisations rather than synonyms or contradictions; the within-prover
census shows a name is not an identity even inside one corpus.

Status: proposed. Owner decisions D1–D5 are listed in the ADR instead of
being asked, because the session was ending.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
---
 ...9-lexicon-v2-and-identity-arbitration.adoc | 288 ++++++++++++++++++
 scripts/false_friend_scan.sh                  |  72 +++++
 2 files changed, 360 insertions(+)
 create mode 100644 docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc
 create mode 100755 scripts/false_friend_scan.sh

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
new file mode 100644
index 00000000..1aedef2b
--- /dev/null
+++ b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc
@@ -0,0 +1,288 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// 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
+
+== Context (measured on `main` at `ed6ef60`, 2026-10-19)
+
+The owner asked for two things at once: push the saturation levers again
+(provers, corpora, vocabulary, synonyms) and go past lexical synonymy toward
+*phrases*, *equivalent expressions*, *false friends*, and ultimately a way to
+arbitrate proofs across prover families by establishing what mathematical
+object each system is talking about — "feeling our way around mathematical
+objects" rather than only checking the same text in many kernels.
+
+What the tree already has:
+
+* *Exchange bridges*: six (`src/rust/exchange/`: OpenTheory, Dedukti,
+  Lambdapi, TPTP, SMT-LIB, SMTCoq). All work on rendered text. None produces a
+  kernel-checked translation; `term_hash` is taken over the rendering, with no
+  α-normalisation (roadmap 6c), so α-equivalent terms hash apart. The failure
+  direction is safe (a missed `sound`, never a false one).
+* *Arbitration*: four fusion mechanisms behind `ResultArbiter`, and since
+  2026-10-14 (ECH-05, #430) a fidelity level `belief` / `epi` / `sound` set by
+  per-attempt `FidelityEvidence` (`KernelTranslation` /
+  `DeclaredCorrespondence` / `None`), with the Idris2 statement in
+  `src/abi/EchidnaABI/Arbitration.idr`. Dispatch attaches no evidence yet, so
+  every dispatched verdict is `belief`. The owner's first kernel-translation
+  target is HOL4 ↔ HOL Light through OpenTheory (6a), then Lean 4 ↔ Rocq
+  through Dedukti (6b). Issue #429 asks to *consume* fidelity evidence (fibre
+  coverage, round trips, cross-prover agreement from one kernel plus
+  independent standpoints) rather than collect N re-proofs.
+* *Lexicon*: `data/synonyms/` holds 14 per-prover tables (343 `[[synonym]]`
+  rows) and 4 cross-prover dictionaries (`_msc2020`, `_wordnet_math`,
+  `_conceptnet_seed`, `_disciplines`; 262 rows). `semantic_class`, the only
+  cross-prover join key, is present on 61 of the 343 per-prover rows, 40 of
+  them in `mizar.toml`; nine tables have none. The schema can say "these names
+  are interchangeable" and nothing else: no way to record a *false friend*
+  (same name, different object), a *phrase* (a multi-token idiom that is one
+  tactic or one concept), a *specialisation* (same theorem at a narrower
+  type), or an *equivalence with a witness* (and which kind of witness).
+* *Corpus*: `training_data/` is uneven. Over thirty provers have empty
+  `premises_*` / `tactics_*` files; HOL Light alone contributes 328,825
+  premise rows. `models/premise_vocab.txt` has 1,311,903 lines, which already
+  exceeds the roadmap's "~1 M canonical tokens" target as a raw count; the
+  metric that matters is `metrics/oov_rate.jl` (≤ 3 %), unmeasured since the
+  saturation campaign.
+* *Toolchain in the session container*: Rust only. No prover, no Julia, no
+  Idris2. Everything measured below is lexical; no kernel was consulted.
+
+=== Experiment 1 — the owner's first pair, HOL4 ↔ HOL Light
+
+`scripts/false_friend_scan.sh training_data hol4 hol_light` (this PR;
+deterministic, jq + coreutils, under a minute):
+
+[cols="3,1",options="header"]
+|===
+| Quantity | Value
+| HOL4 distinct (name, statement) rows / distinct names | 95,740 / 90,170
+| HOL Light distinct (name, statement) rows / distinct names | 43,937 / 42,456
+| Theorem names shared by both corpora | 5,060
+| Shared-name statement pairs | 11,490
+| … with byte-identical statement text (cognates) | 1,030
+| … with differing statement text | 10,460
+|===
+
+Reading the differing pairs in order shows the dominant pattern is *not*
+contradiction and *not* synonymy. It is type generalisation: HOL4's
+`!f:real->real …` against HOL Light's `!f:real^M->real^N …`, `abs` against
+`norm`, `0` against `vec 0` (HOL Light's multivariate library is the
+n-dimensional generalisation of the shared ancestor). Those are
+*specialisation* pairs: the HOL4 statement is an instance of the HOL Light
+one. A lexicon with only `synonym` cannot express that, and an arbiter that
+accepted them as "the same theorem" would be wrong in one direction and
+right in the other. Genuine false friends also exist in the same list: the
+name `lemma` carries unrelated statements in each corpus.
+
+=== Experiment 2 — within-prover homonymy
+
+Same script, census rows (one name, more than one distinct statement):
+
+[cols="2,1,1,1,1",options="header"]
+|===
+| Corpus | Rows | Names | Homonymous names | Rate
+| hol4 | 95,740 | 90,170 | 3,755 | 4.2 %
+| hol_light | 43,937 | 42,456 | 1,218 | 2.9 %
+| lean3 | 92,680 | 68,823 | 13,213 | 19.2 %
+| mizar | 76,522 | 18,795 | 340 | 1.8 %
+| agda | 46,028 | 36,936 | 3,178 | 8.6 %
+| afp | 102,685 | 100,116 | 2,077 | 2.1 %
+| acl2 | 135,964 | 118,117 | 9,438 | 8.0 %
+| why3 | 25,183 | 15,396 | 3,368 | 21.9 %
+| dafny | 10,487 | 7,551 | 920 | 12.2 %
+| fstar | 9,386 | 6,367 | 1,216 | 19.1 %
+| lambda_prolog | 24,970 | 15,263 | 7,628 | 50.0 %
+|===
+
+The Mizar figure is an artefact of the extractor keying on article-local
+labels (`Th1`, `Th2`, …): 76,522 rows collapse onto 18,795 names, so the
+corpus is nearly all homonyms *by construction*, and the low rate means the
+extractor dropped most of them. Lean 3 and Why3 are genuinely namespace-heavy
+(`add_comm` in dozens of structures). Both facts matter for anything that
+joins corpora by name: a name is not an identity, even inside one prover.
+
+=== What the numbers establish
+
+. Lexical alignment is unsafe as *evidence*, which ECH-05 already assumes; the
+  experiment quantifies how unsafe (nine in ten shared-name pairs differ).
+. Lexical alignment is a high-yield *candidate generator*: 1,030 exact
+  cognates and roughly ten thousand specialisation candidates fall out of the
+  first pair for free, before any kernel runs.
+. The relation the lexicon most needs next is not more synonyms but
+  `specialisation` / `generalisation`, then `false_friend`, then `phrase`.
+
+== Options
+
+Rated first for elegance and correctness, then for dependability and
+security. Aspects noted where relevant.
+
+=== A. Logical-framework hub (λΠ-modulo as the lingua franca)
+
+Dedukti / Lambdapi as the single exchange target; prover-specific encoders do
+the work (the Dedukti ecosystem ships them: OpenTheory → Dedukti, Coq →
+Dedukti, Agda → Dedukti, Isabelle → Dedukti, Lean partial). Identity of two
+statements is identity of their λΠ terms after normalisation, which the
+arbiter already names as `KernelTranslation { term_hash }` and already proves
+cannot fuse a collision to `sound`.
+
+* Elegance / correctness: highest. One hub, kernel-checked, matches roadmap
+  6b and #191 exactly, and the arbiter's `sound` level is already defined
+  over it.
+* Dependability / security: high once an encoder exists; each encoder is a
+  research-grade artefact and the set of provers it covers is bounded.
+* Aspect: this is the *only* route to `sound`. Everything else tops out at
+  `epi`.
+
+=== B. Behavioural identity by consequence partitions ("feeling our way around")
+
+Identify an object by what it does, not by its term: fix a shared probe set
+(consequences, instances, counter-instances), have each prover decide the
+probes for its candidate statement, and call two candidates the same object
+when they induce the same partition of the probe set. This is the standpoint
+in `hyperpolymath/autoformal-fidelity` (two target standpoints; agreement is
+identical partitions; convergence is evidence only under independence) and it
+is what #429 asks ECHIDNA to consume. It is neurosymbolic in the intended
+sense: the neural layer proposes alignments from corpus embeddings and
+lexical candidates (Experiment 1); the symbolic layer tests them; the result
+lands in the existing `DeclaredCorrespondence { consequence_tests, failures }`
+constructor and yields `epi`, never `sound`.
+
+* Elegance / correctness: high; reuses the ECH-05 vocabulary unchanged.
+  Correctness is bounded by the probe set and by independence, which must be
+  recorded (same kernel, same library, same author all reduce it).
+* Dependability / security: high. Probes are ordinary prover invocations and
+  run inside the existing sandbox and integrity checks.
+* Aspect: this is the route that handles *false friends* natively (different
+  partitions) and *specialisation* (one partition refines the other), neither
+  of which a term hash can express.
+
+=== C. An in-house super-language or universal IR
+
+A new estate language in which every prover's statements are written.
+Rated lowest: it reinvents MMT / Dedukti, needs the same per-prover encoders
+as A, and adds a kernel nobody has checked. The useful kernel of the idea is
+already in the tree: `core::Term` in `crates/echidna-core/src/core.rs` is a
+small dependent-type IR (Var, Const, App, Lambda, Pi, Sigma, universes, Let).
+The elegant move is to make `core::Term` the α-normalised *projection target*
+that renders to λΠ (6c), not to invent a language around it. KYAML, deed and
+System-ET are serialisation surfaces, not logics: they can carry the lexicon
+and the certificates, and they cannot carry identity.
+
+=== D. Pairwise translators (Mathport-style)
+
+Lean 3 → Lean 4, HOL Light → HOL4 via OpenTheory, and so on. Pragmatic where
+a mature tool exists; quadratic in the number of provers; keeps every pair as
+its own special case. Kept as *feeders* into A, never as the architecture.
+
+=== E. Identity as a VeriSimDB consonance subject (alternative framing, cross-repo)
+
+`hyperpolymath/verisimdb` already defines exactly this problem for data:
+one identity maintained across modal witnesses, with drift detection and the
+verbs `MERGE` / `SPLIT` / `RETRACT`. Treat each prover as a modal witness of
+one mathematical object: a cognate is consonance, a false friend is drift,
+curation is `MERGE` or `SPLIT`, retraction of a backend
+(`ResultArbiter::retract`) is `RETRACT`. This is not a competitor to A + B;
+it is where the identity lives between runs, and it is the estate trope the
+owner asked to look for. It belongs in verisimdb, not here.
+
+== Recommendation
+
+*Hub and probe*: A for `sound` where an encoder exists (6a OpenTheory on the
+owner's HOL4 ↔ HOL Light pair first, 6b Dedukti next), B for `epi` everywhere
+else, D as feeders, C rejected, E as the persistence layer, filed against
+verisimdb. The hybrid is the elegant option because it maps one-to-one onto
+the two evidence constructors ECH-05 already proves properties about, so no
+arbiter or ABI change is needed to adopt it; it departs from nothing the
+owner has ruled.
+
+== Decision (proposed; lands only after D1–D5)
+
+. *Lexicon v2 schema*, additive and loader-compatible (serde defaults), on
+  every `[[synonym]]` row:
+  * `relation`: one of `synonym` (default), `specialisation`,
+    `generalisation`, `false_friend`, `phrase`.
+  * `phrase`: ordered token list for a multi-token idiom (for example
+    Mizar's `then thus`, Coq's `apply … ; auto`, Isabelle's `by (simp add:`).
+  * `false_friends`: names that *look* like this entry in other tables and
+    are not it, with the other table named.
+  * `evidence`: `none` (default), `curated`, `probe { tests, failures }`,
+    `kernel { format, term_hash }` — the same three shapes as
+    `FidelityEvidence`, so a lexicon row can be lifted straight into an
+    attempt's fidelity.
+  * `fidelity`: `exact` or `lossy` with a `residue` note, after echo-types'
+    loss-with-residue formalism, so a lossy correspondence says what is lost.
+  * `scope`: library and version the relation holds in (the existing `since`
+    / `until` cover the prover version only).
+. *Candidate generation from corpora*: `scripts/false_friend_scan.sh` now; a
+  Rust `echidna lexicon scan` later that emits v2 rows with
+  `evidence = none`. Candidates never set `semantic_class` on their own.
+. *Consequence probes*: a `verification/consequence_probe.rs` that takes a
+  probe set per pair, runs it through the existing dispatcher and sandbox,
+  records independence, and produces `DeclaredCorrespondence`. First probe
+  pair: the SMT-LIB pair Z3 ↔ CVC5, because both binaries already install in
+  `live-provers.yml` Tier 1, so the probe loop is testable in CI today.
+. *Hub*: 6a real OpenTheory (article reader and writer against the real
+  stack-machine format, compatible with the OpenTheory → Dedukti encoder),
+  with the CR-8 round-trip test from `standards`
+  `3-practice/testing-and-benchmarking/TESTING-TAXONOMY.adoc`.
+. *6c*: α-normalised projection of `core::Term` to λΠ; `term_hash` over the
+  canonical form; property tests that α-equivalent terms hash equal.
+. *Dispatch attaches evidence* (closes "every verdict is `belief`"), then
+  #429's ingestion.
+
+== Work breakdown (stacked PRs, each independently reviewable)
+
+[cols="1,4,2",options="header"]
+|===
+| PR | Content | Depends on
+| 0 (this) | This ADR + `scripts/false_friend_scan.sh` | —
+| 1 | Lexicon v2 schema in `src/rust/suggest/synonyms.rs` + `data/synonyms/README.adoc` + tests; existing tables load unchanged | D2
+| 2 | Fill `semantic_class` on the 282 per-prover rows that lack it, curated, with `evidence = curated`; relations added from the scan where the owner's reading confirms them | 1, D4
+| 3 | `echidna lexicon scan`: Rust port of the census, emits v2 candidate rows across all corpus pairs; cognate and specialisation candidates for HOL4 ↔ HOL Light as fixtures | 1
+| 4 | `consequence_probe.rs` + `DeclaredCorrespondence` producer + CI job on Z3 ↔ CVC5 | D3
+| 5 | 6a OpenTheory real + CR-8 round-trip test (#190) | —
+| 6 | 6c α-normalised λΠ projection; canonical `term_hash` | 5
+| 7 | Dispatch attaches fidelity; #429 ingestion | 4, 6
+|===
+
+Saturation levers that need no decision and can run alongside: synonym
+tables for the Tier-1 provers that still have none (Z3, CVC5, PVS), filling
+the empty `premises_*` files for Tier-2 provers whose extractor exists, and
+re-running `metrics/run_all.jl` to re-baseline `oov_rate` and
+`alignment_rate` (needs Julia; not possible in the session container).
+
+== Beyond this repository
+
+* `hyperpolymath/verisimdb`: map cross-prover object identity onto a
+  consonance subject (option E); one issue to open.
+* `hyperpolymath/standards`: CR-8 names the round-trip pairs; the FRG grades'
+  "cross-prover replication ≥ 2 / ≥ 3" (V2 / V3) should require `epi` or
+  better, not lexical agreement, once this lands.
+* `hyperpolymath/autoformal-fidelity` and `hyperpolymath/nextgen-typing`
+  (`docs/TYPE-CONNECTIONS.adoc`): the partition-agreement statement B
+  implements; cite, do not re-derive.
+* `hyperpolymath/echo-types`: the residue of a lossy correspondence
+  (`fidelity = lossy`) is an echo-types L3 object; the lexicon should cite the
+  loss taxonomy rather than invent names for kinds of loss.
+* `hyperpolymath/echidnabot`: consumes `echidna.prove.result/1`; the
+  verdict's `level` should surface in its trust bridge once dispatch attaches
+  evidence.
+
+== Open owner decisions (the selector questions this session could not ask)
+
+[cols="1,5,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
+|===
+
+== Non-claims
+
+No prover ran during the measurement. Every number above is lexical. Nothing
+in this ADR raises any verdict above `belief`; the ECH-05 regression and
+fidelity tests are untouched.
diff --git a/scripts/false_friend_scan.sh b/scripts/false_friend_scan.sh
new file mode 100755
index 00000000..8de2a3c4
--- /dev/null
+++ b/scripts/false_friend_scan.sh
@@ -0,0 +1,72 @@
+#!/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>
+#
+# false_friend_scan.sh — lexical cognate / false-friend / homonym census over
+# training_data/proof_states_<prover>.jsonl for one prover pair.
+#
+# Evidence class: LEXICAL ONLY. Nothing here is fidelity evidence in the
+# ECH-05 sense (src/rust/verification/result_arbiter.rs); the output is a
+# candidate list for lexicon curation and for consequence probing. See
+# docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc.
+#
+# Usage:  scripts/false_friend_scan.sh [TRAINING_DIR] [PROVER_A] [PROVER_B]
+# Default: training_data hol4 hol_light   (the stage-6a first pair)
+# Needs:   jq + coreutils (sort, join, comm, awk, cut, uniq). Deterministic.
+set -euo pipefail
+
+dir="${1:-training_data}"
+a="${2:-hol4}"
+b="${3:-hol_light}"
+tab="$(printf '\t')"
+work="$(mktemp -d)"
+trap 'rm -rf "$work"' EXIT
+
+# prover -> TSV "name<TAB>goal" with whitespace normalised, one row per
+# distinct (name, goal) pair, sorted on the name for join(1).
+extract() {
+  local f="$dir/proof_states_$1.jsonl"
+  [ -s "$f" ] || { echo "no records: $f" >&2; return 1; }
+  jq -r 'select(.theorem != null and .goal != null)
+         | [.theorem, (.goal | gsub("[[:space:]]+"; " ") | gsub("^ | $"; ""))]
+         | @tsv' "$f" | LC_ALL=C sort -u | LC_ALL=C sort -t "$tab" -k1,1 -s
+}
+
+# prover tsv -> one census row: records, distinct names, homonymous names
+# (one name, more than one distinct goal), homonym rate.
+census() {
+  local r n h
+  r=$(wc -l < "$2")
+  n=$(cut -f1 "$2" | LC_ALL=C sort -u | wc -l)
+  h=$(cut -f1 "$2" | LC_ALL=C sort | uniq -d | wc -l)
+  awk -v p="$1" -v r="$r" -v n="$n" -v h="$h" \
+    'BEGIN { printf "%-14s %9d %9d %9d %6.1f%%\n", p, r, n, h, (n ? 100*h/n : 0) }'
+}
+
+extract "$a" > "$work/a.tsv"
+extract "$b" > "$work/b.tsv"
+
+echo "== within-prover census"
+printf "%-14s %9s %9s %9s %7s\n" prover records names homonyms rate
+census "$a" "$work/a.tsv"
+census "$b" "$work/b.tsv"
+
+cut -f1 "$work/a.tsv" | LC_ALL=C sort -u > "$work/na"
+cut -f1 "$work/b.tsv" | LC_ALL=C sort -u > "$work/nb"
+echo
+echo "== cross-prover name overlap: $a vs $b"
+echo "shared names: $(LC_ALL=C comm -12 "$work/na" "$work/nb" | wc -l)"
+echo "$a-only: $(LC_ALL=C comm -23 "$work/na" "$work/nb" | wc -l)"
+echo "$b-only: $(LC_ALL=C comm -13 "$work/na" "$work/nb" | wc -l)"
+
+LC_ALL=C join -t "$tab" "$work/a.tsv" "$work/b.tsv" > "$work/joined.tsv"
+echo
+echo "== shared names, statement text agreement (name-pairs: $(wc -l < "$work/joined.tsv"))"
+awk -F'\t' '{ if ($2 == $3) s++; else d++ }
+  END { printf "cognate (identical statement text): %d\ndiffering statement text (false-friend or specialisation candidates): %d\n", s, d }' \
+  "$work/joined.tsv"
+echo
+echo "== first differing name-pairs (deterministic order)"
+awk -F'\t' -v A="$a" -v B="$b" '$2 != $3 {
+  printf "%s\n  %s: %s\n  %s: %s\n", $1, A, substr($2, 1, 100), B, substr($3, 1, 100) }' \
+  "$work/joined.tsv" | head -24

From 38c986fd370268e19c619b927c6a2c101939cd60 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <j.d.a.jewell@open.ac.uk>
Date: Mon, 19 Oct 2026 22:27:41 +0000
Subject: [PATCH 2/9] fix(scripts): false_friend_scan exits 0 after its sample;
 ADR states the measured property
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Review findings on #443 (CodeRabbit), each reproduced before the change:

- The final `awk … | head -24` made head close the pipe while awk was still
  writing; under `set -o pipefail` the finished scan exited 141 (SIGPIPE).
  awk now stops itself after eight pairs and head is gone. Exit is 0.
- `$2 == $3` compared numeric-looking goals numerically (`01` == `1`); both
  comparisons now force string comparison.
- `uniq -d` inherited the caller's locale while `sort` ran under LC_ALL=C;
  uniq runs under LC_ALL=C too.
- The ADR called the 1,030 cognates "byte-identical"; the script compares
  after whitespace normalisation, so the ADR now says that.
- The lexicon v2 `evidence` field: `curated` is provenance only and lifts to
  `FidelityEvidence::None`; `kernel` needs `checked_by`; only `probe` and a
  complete `kernel` lift to the arbiter's constructors.

The counts are unchanged (95,740/90,170/3,755; 43,937/42,456/1,218; 5,060
shared; 11,490 pairs; 1,030 cognate; 10,460 differing).

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
---
 ...-19-lexicon-v2-and-identity-arbitration.adoc | 17 ++++++++++-------
 scripts/false_friend_scan.sh                    | 16 +++++++++-------
 2 files changed, 19 insertions(+), 14 deletions(-)

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 1aedef2b..a4939272 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
@@ -60,7 +60,7 @@ deterministic, jq + coreutils, under a minute):
 | HOL Light distinct (name, statement) rows / distinct names | 43,937 / 42,456
 | Theorem names shared by both corpora | 5,060
 | Shared-name statement pairs | 11,490
-| … with byte-identical statement text (cognates) | 1,030
+| … with equal statement text after whitespace normalisation (cognates) | 1,030
 | … with differing statement text | 10,460
 |===
 
@@ -106,9 +106,9 @@ joins corpora by name: a name is not an identity, even inside one prover.
 
 . Lexical alignment is unsafe as *evidence*, which ECH-05 already assumes; the
   experiment quantifies how unsafe (nine in ten shared-name pairs differ).
-. Lexical alignment is a high-yield *candidate generator*: 1,030 exact
-  cognates and roughly ten thousand specialisation candidates fall out of the
-  first pair for free, before any kernel runs.
+. Lexical alignment is a high-yield *candidate generator*: 1,030
+  whitespace-normalised cognates and roughly ten thousand specialisation
+  candidates fall out of the first pair for free, before any kernel runs.
 . The relation the lexicon most needs next is not more synonyms but
   `specialisation` / `generalisation`, then `false_friend`, then `phrase`.
 
@@ -207,9 +207,12 @@ owner has ruled.
   * `false_friends`: names that *look* like this entry in other tables and
     are not it, with the other table named.
   * `evidence`: `none` (default), `curated`, `probe { tests, failures }`,
-    `kernel { format, term_hash }` — the same three shapes as
-    `FidelityEvidence`, so a lexicon row can be lifted straight into an
-    attempt's fidelity.
+    `kernel { format, checked_by, term_hash }`. `curated` records provenance
+    only and lifts to `FidelityEvidence::None` until probe or kernel evidence
+    is attached; `probe` lifts to `DeclaredCorrespondence`, and `kernel` to
+    `KernelTranslation` only when every field, `checked_by` included, is
+    present. A lexicon row therefore never raises an attempt's fidelity
+    above what its own evidence carries.
   * `fidelity`: `exact` or `lossy` with a `residue` note, after echo-types'
     loss-with-residue formalism, so a lossy correspondence says what is lost.
   * `scope`: library and version the relation holds in (the existing `since`
diff --git a/scripts/false_friend_scan.sh b/scripts/false_friend_scan.sh
index 8de2a3c4..b3627ff0 100755
--- a/scripts/false_friend_scan.sh
+++ b/scripts/false_friend_scan.sh
@@ -38,7 +38,7 @@ census() {
   local r n h
   r=$(wc -l < "$2")
   n=$(cut -f1 "$2" | LC_ALL=C sort -u | wc -l)
-  h=$(cut -f1 "$2" | LC_ALL=C sort | uniq -d | wc -l)
+  h=$(cut -f1 "$2" | LC_ALL=C sort | LC_ALL=C uniq -d | wc -l)
   awk -v p="$1" -v r="$r" -v n="$n" -v h="$h" \
     'BEGIN { printf "%-14s %9d %9d %9d %6.1f%%\n", p, r, n, h, (n ? 100*h/n : 0) }'
 }
@@ -62,11 +62,13 @@ echo "$b-only: $(LC_ALL=C comm -13 "$work/na" "$work/nb" | wc -l)"
 LC_ALL=C join -t "$tab" "$work/a.tsv" "$work/b.tsv" > "$work/joined.tsv"
 echo
 echo "== shared names, statement text agreement (name-pairs: $(wc -l < "$work/joined.tsv"))"
-awk -F'\t' '{ if ($2 == $3) s++; else d++ }
-  END { printf "cognate (identical statement text): %d\ndiffering statement text (false-friend or specialisation candidates): %d\n", s, d }' \
+awk -F'\t' '{ if (($2 "") == ($3 "")) s++; else d++ }
+  END { printf "cognate (equal after whitespace normalisation): %d\ndiffering statement text (false-friend or specialisation candidates): %d\n", s, d }' \
   "$work/joined.tsv"
 echo
-echo "== first differing name-pairs (deterministic order)"
-awk -F'\t' -v A="$a" -v B="$b" '$2 != $3 {
-  printf "%s\n  %s: %s\n  %s: %s\n", $1, A, substr($2, 1, 100), B, substr($3, 1, 100) }' \
-  "$work/joined.tsv" | head -24
+echo "== first differing name-pairs (deterministic order, at most 8)"
+# awk stops itself after eight pairs; truncating with head(1) would close
+# the pipe early and, under pipefail, turn a finished scan into exit 141.
+awk -F'\t' -v A="$a" -v B="$b" '($2 "") != ($3 "") {
+  printf "%s\n  %s: %s\n  %s: %s\n", $1, A, substr($2, 1, 100), B, substr($3, 1, 100)
+  if (++shown >= 8) exit }' "$work/joined.tsv"

From 5be5583ee9a7a47456e76b6989b4de42db084524 Mon Sep 17 00:00:00 2001
From: "coderabbitai[bot]"
 <136622811+coderabbitai[bot]@users.noreply.github.com>
Date: Mon, 19 Oct 2026 22:35:07 +0000
Subject: [PATCH 3/9] docs(scripts): document extract and census contracts in
 false_friend_scan

---
 scripts/false_friend_scan.sh | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/scripts/false_friend_scan.sh b/scripts/false_friend_scan.sh
index b3627ff0..9685c66d 100755
--- a/scripts/false_friend_scan.sh
+++ b/scripts/false_friend_scan.sh
@@ -24,6 +24,11 @@ trap 'rm -rf "$work"' EXIT
 
 # prover -> TSV "name<TAB>goal" with whitespace normalised, one row per
 # distinct (name, goal) pair, sorted on the name for join(1).
+# $1 is the prover key for "$dir/proof_states_$1.jsonl"; output goes to stdout.
+# Rows with a missing or null theorem or goal are omitted; goal whitespace is
+# collapsed to single spaces and trimmed. Missing or empty input returns 1
+# with a diagnostic on stderr; read, JSON and processing errors propagate a
+# non-zero status.
 extract() {
   local f="$dir/proof_states_$1.jsonl"
   [ -s "$f" ] || { echo "no records: $f" >&2; return 1; }
@@ -34,6 +39,9 @@ extract() {
 
 # prover tsv -> one census row: records, distinct names, homonymous names
 # (one name, more than one distinct goal), homonym rate.
+# $1 labels the prover; $2 is a TSV file of distinct (name, goal) pairs, as
+# produced by extract. Writes to stdout; the rate is a percentage, or 0 when
+# there are no names. File read and processing failures abort the scan.
 census() {
   local r n h
   r=$(wc -l < "$2")

From 4486d2d55abfaf3a31b894a790d511d441ed0620 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <j.d.a.jewell@open.ac.uk>
Date: Mon, 19 Oct 2026 22:43:37 +0000
Subject: [PATCH 4/9] fix(scripts): drop empty names and statements from the
 census; ADR carries independence and injectivity
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Codex review findings on #443:

- The extractor admitted rows with an empty theorem name or an empty goal
  (three in HOL4, twelve in Why3, more in lambda_prolog), which could join
  as "cognates" with nothing to compare. Rows whose trimmed name or
  whitespace-normalised goal is empty are now dropped before the TSV is
  written. The affected census rows move by a few units (HOL4 95,738 /
  90,168; AFP, ACL2, Why3, lambda_prolog likewise); the HOL4 ↔ HOL Light
  overlap and agreement counts are unchanged.
- The ADR claimed the exchange renderings fail safe. They do not: the
  OpenTheory renderer collapses unsupported terms to one opaque constant
  and drops binder types, so distinct terms can hash alike. The ADR now
  says so and requires an injective rendering with unsupported terms
  rejected before any KernelTranslation is built (decision 5, PR 6).
- The ADR claimed no arbiter or ABI change was needed, yet asked for probe
  independence that DeclaredCorrespondence cannot carry and fidelity_level
  does not check. It now specifies a standpoint record on
  DeclaredCorrespondence, an Epi lift only when standpoints differ, and the
  matching Arbitration.idr argument (option B, decision 3, PR 4), and calls
  the change what it is: additive.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
---
 ...9-lexicon-v2-and-identity-arbitration.adoc | 62 +++++++++++++------
 scripts/false_friend_scan.sh                  |  9 ++-
 2 files changed, 48 insertions(+), 23 deletions(-)

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 a4939272..b754948d 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
@@ -18,8 +18,13 @@ What the tree already has:
 * *Exchange bridges*: six (`src/rust/exchange/`: OpenTheory, Dedukti,
   Lambdapi, TPTP, SMT-LIB, SMTCoq). All work on rendered text. None produces a
   kernel-checked translation; `term_hash` is taken over the rendering, with no
-  α-normalisation (roadmap 6c), so α-equivalent terms hash apart. The failure
-  direction is safe (a missed `sound`, never a false one).
+  α-normalisation (roadmap 6c), so α-equivalent terms hash apart. Worse, the
+  renderings are lossy: `term_to_opentheory` collapses every term outside
+  Var / Const / App / Lambda to `const "echidna_opaque"` and drops binder
+  types, so two different source terms can render, and hash, alike. Nothing
+  fuses on these hashes today because dispatch attaches no evidence; once it
+  does, a `KernelTranslation` may only come from an injective rendering of a
+  supported fragment, with unsupported terms rejected, never collapsed (§5).
 * *Arbitration*: four fusion mechanisms behind `ResultArbiter`, and since
   2026-10-14 (ECH-05, #430) a fidelity level `belief` / `epi` / `sound` set by
   per-attempt `FidelityEvidence` (`KernelTranslation` /
@@ -51,12 +56,13 @@ What the tree already has:
 === Experiment 1 — the owner's first pair, HOL4 ↔ HOL Light
 
 `scripts/false_friend_scan.sh training_data hol4 hol_light` (this PR;
-deterministic, jq + coreutils, under a minute):
+deterministic, jq + coreutils, under a minute; rows with an empty name or
+statement are dropped, which removes three HOL4 rows):
 
 [cols="3,1",options="header"]
 |===
 | Quantity | Value
-| HOL4 distinct (name, statement) rows / distinct names | 95,740 / 90,170
+| HOL4 distinct (name, statement) rows / distinct names | 95,738 / 90,168
 | HOL Light distinct (name, statement) rows / distinct names | 43,937 / 42,456
 | Theorem names shared by both corpora | 5,060
 | Shared-name statement pairs | 11,490
@@ -77,22 +83,23 @@ name `lemma` carries unrelated statements in each corpus.
 
 === Experiment 2 — within-prover homonymy
 
-Same script, census rows (one name, more than one distinct statement):
+Same script, census rows (one name, more than one distinct statement; rows
+with an empty name or statement dropped):
 
 [cols="2,1,1,1,1",options="header"]
 |===
 | Corpus | Rows | Names | Homonymous names | Rate
-| hol4 | 95,740 | 90,170 | 3,755 | 4.2 %
+| hol4 | 95,738 | 90,168 | 3,755 | 4.2 %
 | hol_light | 43,937 | 42,456 | 1,218 | 2.9 %
 | lean3 | 92,680 | 68,823 | 13,213 | 19.2 %
 | mizar | 76,522 | 18,795 | 340 | 1.8 %
 | agda | 46,028 | 36,936 | 3,178 | 8.6 %
-| afp | 102,685 | 100,116 | 2,077 | 2.1 %
-| acl2 | 135,964 | 118,117 | 9,438 | 8.0 %
-| why3 | 25,183 | 15,396 | 3,368 | 21.9 %
+| afp | 102,683 | 100,116 | 2,075 | 2.1 %
+| acl2 | 135,963 | 118,117 | 9,437 | 8.0 %
+| why3 | 25,180 | 15,395 | 3,368 | 21.9 %
 | dafny | 10,487 | 7,551 | 920 | 12.2 %
 | fstar | 9,386 | 6,367 | 1,216 | 19.1 %
-| lambda_prolog | 24,970 | 15,263 | 7,628 | 50.0 %
+| lambda_prolog | 24,897 | 15,232 | 7,615 | 50.0 %
 |===
 
 The Mizar figure is an artefact of the extractor keying on article-local
@@ -149,8 +156,16 @@ lands in the existing `DeclaredCorrespondence { consequence_tests, failures }`
 constructor and yields `epi`, never `sound`.
 
 * Elegance / correctness: high; reuses the ECH-05 vocabulary unchanged.
-  Correctness is bounded by the probe set and by independence, which must be
-  recorded (same kernel, same library, same author all reduce it).
+  Correctness is bounded by the probe set and by independence (same kernel,
+  same library, same author all reduce it). The current
+  `DeclaredCorrespondence { consequence_tests, failures }` has no place to
+  carry independence, and `fidelity_level` lifts any tested, failure-free
+  correspondence to `Epi`, so independence must travel inside the evidence:
+  `DeclaredCorrespondence` gains a standpoint record (kernel, library and
+  authorship of each side), `fidelity_level` lifts to `Epi` only when the
+  standpoints differ, and the `Arbitration.idr` constructor takes the same
+  argument. That is an additive arbiter and ABI change, and the one this
+  proposal needs.
 * Dependability / security: high. Probes are ordinary prover invocations and
   run inside the existing sandbox and integrity checks.
 * Aspect: this is the route that handles *false friends* natively (different
@@ -191,10 +206,12 @@ owner asked to look for. It belongs in verisimdb, not here.
 *Hub and probe*: A for `sound` where an encoder exists (6a OpenTheory on the
 owner's HOL4 ↔ HOL Light pair first, 6b Dedukti next), B for `epi` everywhere
 else, D as feeders, C rejected, E as the persistence layer, filed against
-verisimdb. The hybrid is the elegant option because it maps one-to-one onto
-the two evidence constructors ECH-05 already proves properties about, so no
-arbiter or ABI change is needed to adopt it; it departs from nothing the
-owner has ruled.
+verisimdb. The hybrid is the elegant option because it maps onto the two
+evidence constructors ECH-05 already proves properties about: the fusion
+mechanisms are untouched, and the arbiter and ABI changes it needs are
+additive (the standpoint record on `DeclaredCorrespondence`, option B, and
+the injectivity requirement on `KernelTranslation` renderings, option A).
+It departs from nothing the owner has ruled.
 
 == Decision (proposed; lands only after D1–D5)
 
@@ -222,7 +239,9 @@ owner has ruled.
   `evidence = none`. Candidates never set `semantic_class` on their own.
 . *Consequence probes*: a `verification/consequence_probe.rs` that takes a
   probe set per pair, runs it through the existing dispatcher and sandbox,
-  records independence, and produces `DeclaredCorrespondence`. First probe
+  and produces `DeclaredCorrespondence` with its standpoint record;
+  `fidelity_level` and `Arbitration.idr` are extended in the same PR so that
+  correlated probes cannot reach `Epi`. First probe
   pair: the SMT-LIB pair Z3 ↔ CVC5, because both binaries already install in
   `live-provers.yml` Tier 1, so the probe loop is testable in CI today.
 . *Hub*: 6a real OpenTheory (article reader and writer against the real
@@ -230,7 +249,10 @@ owner has ruled.
   with the CR-8 round-trip test from `standards`
   `3-practice/testing-and-benchmarking/TESTING-TAXONOMY.adoc`.
 . *6c*: α-normalised projection of `core::Term` to λΠ; `term_hash` over the
-  canonical form; property tests that α-equivalent terms hash equal.
+  canonical form; the renderer rejects terms outside the supported fragment
+  instead of collapsing them to an opaque constant; property tests that
+  α-equivalent terms hash equal and that distinct terms in the fragment never
+  share a hash.
 . *Dispatch attaches evidence* (closes "every verdict is `belief`"), then
   #429's ingestion.
 
@@ -243,9 +265,9 @@ owner has ruled.
 | 1 | Lexicon v2 schema in `src/rust/suggest/synonyms.rs` + `data/synonyms/README.adoc` + tests; existing tables load unchanged | D2
 | 2 | Fill `semantic_class` on the 282 per-prover rows that lack it, curated, with `evidence = curated`; relations added from the scan where the owner's reading confirms them | 1, D4
 | 3 | `echidna lexicon scan`: Rust port of the census, emits v2 candidate rows across all corpus pairs; cognate and specialisation candidates for HOL4 ↔ HOL Light as fixtures | 1
-| 4 | `consequence_probe.rs` + `DeclaredCorrespondence` producer + CI job on Z3 ↔ CVC5 | D3
+| 4 | `consequence_probe.rs` + `DeclaredCorrespondence` producer with the standpoint record + `fidelity_level` and `Arbitration.idr` extension + CI job on Z3 ↔ CVC5 | D3
 | 5 | 6a OpenTheory real + CR-8 round-trip test (#190) | —
-| 6 | 6c α-normalised λΠ projection; canonical `term_hash` | 5
+| 6 | 6c α-normalised λΠ projection; unsupported terms rejected; canonical `term_hash`; injectivity property test | 5
 | 7 | Dispatch attaches fidelity; #429 ingestion | 4, 6
 |===
 
diff --git a/scripts/false_friend_scan.sh b/scripts/false_friend_scan.sh
index b3627ff0..0b569969 100755
--- a/scripts/false_friend_scan.sh
+++ b/scripts/false_friend_scan.sh
@@ -22,13 +22,16 @@ tab="$(printf '\t')"
 work="$(mktemp -d)"
 trap 'rm -rf "$work"' EXIT
 
-# prover -> TSV "name<TAB>goal" with whitespace normalised, one row per
-# distinct (name, goal) pair, sorted on the name for join(1).
+# prover -> TSV "name<TAB>goal": name trimmed, goal whitespace-normalised, rows
+# with an empty name or goal dropped, one row per distinct pair, sorted on the
+# name for join(1).
 extract() {
   local f="$dir/proof_states_$1.jsonl"
   [ -s "$f" ] || { echo "no records: $f" >&2; return 1; }
   jq -r 'select(.theorem != null and .goal != null)
-         | [.theorem, (.goal | gsub("[[:space:]]+"; " ") | gsub("^ | $"; ""))]
+         | [(.theorem | gsub("^[[:space:]]+|[[:space:]]+$"; "")),
+            (.goal | gsub("[[:space:]]+"; " ") | gsub("^ | $"; ""))]
+         | select(.[0] != "" and .[1] != "")
          | @tsv' "$f" | LC_ALL=C sort -u | LC_ALL=C sort -t "$tab" -k1,1 -s
 }
 

From 0fbb7f9366e8b24f4d223ecdcd3273a889f31acb Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <j.d.a.jewell@open.ac.uk>
Date: Mon, 19 Oct 2026 23:36:43 +0000
Subject: [PATCH 5/9] feat(lexicon): lexicon v2 schema as a Nickel contract;
 loader learns relations and evidence

Stage 6c, PR 1 of the stack in
docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc, after
the owner's rulings D1 (hub and probe), D2 (Nickel) and D4 (mined
candidates flag-only), recorded in the ADR.

- data/synonyms/schema.ncl: the schema of record. Nickel imports each TOML
  table and applies `Table`; the tables stay TOML, so the Rust and Julia
  loaders are unchanged. It checks shape and the cross-field rules
  (phrase <=> relation phrase, lossy => residue, evidence shapes, closed
  field set).
- scripts/lexicon-check.sh + tests/lexicon_fixtures/: the gate applies the
  contract to all 18 shipped tables and to fixtures; 1 accept fixture must
  pass and 14 planted defects must be rejected. The reject set caught a bug
  in the first draft (lazy evaluation skipped the evidence check).
- rust-ci check job runs the gate with a SHA-256-pinned Nickel release (a
  run step, so no actions.lock change); `just lexicon-check` runs it locally.
- src/rust/suggest/synonyms.rs: Relation, LexiconEvidence (lifts to
  FidelityEvidence: none/curated -> None, probe -> DeclaredCorrespondence,
  kernel -> KernelTranslation), FalseFriend, Fidelity, Scope; unknown fields
  are rejected. alternatives() offers only synonym and phrase rows, so a
  false friend is never substituted; related() reports the rest, with
  specialisation and generalisation inverted from the alias side.
- fix(data): hol4.toml used the escape \` seven times, which TOML rejects.
  load_all() therefore failed and `echidna corpus crossquery` crashed on
  main; it now runs. Found by the contract on its first run.

Tests: tests/lexicon_v2_test.rs (7, both load tests failed before the
hol4.toml fix), suggest:: unit tests (26), arbitration_fidelity_test (4);
clippy -D warnings and rustfmt clean.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
---
 .github/workflows/rust-ci.yml                 |  14 ++
 Justfile                                      |   6 +
 data/synonyms/README.adoc                     |  51 +++++
 data/synonyms/hol4.toml                       |  14 +-
 data/synonyms/schema.ncl                      | 157 +++++++++++++++
 ...9-lexicon-v2-and-identity-arbitration.adoc |  22 ++-
 scripts/lexicon-check.sh                      |  51 +++++
 src/rust/suggest/synonyms.rs                  | 187 +++++++++++++++++-
 src/rust/suggest/variant.rs                   |   1 +
 .../accept/v2_all_fields.toml                 |  32 +++
 .../lexicon_fixtures/reject/bad_relation.toml |   6 +
 .../reject/curated_with_counts.toml           |   6 +
 .../reject/empty_canonical.toml               |   5 +
 .../reject/false_friend_item_shape.toml       |   6 +
 .../reject/false_friend_no_alias.toml         |   6 +
 .../reject/kernel_short_hash.toml             |   6 +
 .../reject/kernel_without_checker.toml        |   6 +
 .../reject/lossy_without_residue.toml         |   6 +
 .../reject/phrase_on_synonym.toml             |   6 +
 .../reject/phrase_without_tokens.toml         |   6 +
 .../reject/probe_more_failures.toml           |   6 +
 .../reject/probe_zero_tests.toml              |   6 +
 .../reject/residue_on_exact.toml              |   7 +
 .../reject/unknown_field.toml                 |   6 +
 tests/lexicon_v2_test.rs                      | 166 ++++++++++++++++
 25 files changed, 765 insertions(+), 20 deletions(-)
 create mode 100644 data/synonyms/schema.ncl
 create mode 100755 scripts/lexicon-check.sh
 create mode 100644 tests/lexicon_fixtures/accept/v2_all_fields.toml
 create mode 100644 tests/lexicon_fixtures/reject/bad_relation.toml
 create mode 100644 tests/lexicon_fixtures/reject/curated_with_counts.toml
 create mode 100644 tests/lexicon_fixtures/reject/empty_canonical.toml
 create mode 100644 tests/lexicon_fixtures/reject/false_friend_item_shape.toml
 create mode 100644 tests/lexicon_fixtures/reject/false_friend_no_alias.toml
 create mode 100644 tests/lexicon_fixtures/reject/kernel_short_hash.toml
 create mode 100644 tests/lexicon_fixtures/reject/kernel_without_checker.toml
 create mode 100644 tests/lexicon_fixtures/reject/lossy_without_residue.toml
 create mode 100644 tests/lexicon_fixtures/reject/phrase_on_synonym.toml
 create mode 100644 tests/lexicon_fixtures/reject/phrase_without_tokens.toml
 create mode 100644 tests/lexicon_fixtures/reject/probe_more_failures.toml
 create mode 100644 tests/lexicon_fixtures/reject/probe_zero_tests.toml
 create mode 100644 tests/lexicon_fixtures/reject/residue_on_exact.toml
 create mode 100644 tests/lexicon_fixtures/reject/unknown_field.toml
 create mode 100644 tests/lexicon_v2_test.rs

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..c6c72db2 100644
--- a/data/synonyms/README.adoc
+++ b/data/synonyms/README.adoc
@@ -68,6 +68,57 @@ 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`
+| 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`. It lifts into the
+  arbiter's `FidelityEvidence`: `none` and `curated` lift to `None`
+  (curation is provenance, not fidelity evidence), `probe` to
+  `DeclaredCorrespondence`, `kernel` to `KernelTranslation`. 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..dbb4d4ca
--- /dev/null
+++ b/data/synonyms/schema.ncl
@@ -0,0 +1,157 @@
+# 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
+
+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.
+# `none` and `curated` lift to `FidelityEvidence::None` (curated is
+# provenance, not fidelity evidence); `probe` lifts to
+# `DeclaredCorrespondence`; `kernel` lifts to `KernelTranslation`.
+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 !(std.is_number value.tests) || !(std.is_number value.failures)
+        || value.tests < 1 || value.failures < 0
+        || 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) || !(std.is_array e.aliases)
+    || !(std.array.all std.is_string e.aliases) then
+    fail "`%{e.canonical}`: `aliases` must be an array of 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..ed8b588b
--- /dev/null
+++ b/scripts/lexicon-check.sh
@@ -0,0 +1,51 @@
+#!/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
+
+for f in "$root"/data/synonyms/*.toml "$root"/tests/lexicon_fixtures/accept/*.toml; 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 "$root"/tests/lexicon_fixtures/reject/*.toml; 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/rust/suggest/synonyms.rs b/src/rust/suggest/synonyms.rs
index 6902809e..5581d2eb 100644
--- a/src/rust/suggest/synonyms.rs
+++ b/src/rust/suggest/synonyms.rs
@@ -9,17 +9,131 @@ 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`.
+    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; see [`LexiconEvidence::to_fidelity`].
+#[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 {
+    /// Lift to the arbiter's evidence. `none` and `curated` lift to
+    /// [`FidelityEvidence::None`], so a lexicon row never raises an
+    /// attempt's fidelity above what its own evidence carries.
+    pub fn to_fidelity(&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 +144,25 @@ 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>,
 }
 
 /// Parsed and indexed synonym table for a single prover.
@@ -54,7 +187,13 @@ impl SynonymTable {
         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).
+    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()))?;
         Ok(Self::from_entries(parsed.synonyms))
@@ -71,7 +210,12 @@ 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.
     pub fn alternatives(&self, name: &str) -> Vec<String> {
         let indices = match self.by_name.get(name) {
             Some(v) => v,
@@ -80,6 +224,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 +241,36 @@ 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.
+    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 +419,7 @@ mod tests {
                 since: None,
                 until: None,
                 semantic_class: None,
+                ..Default::default()
             },
             SynonymEntry {
                 canonical: "linarith".to_string(),
@@ -251,6 +429,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_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_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_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..8f2b8261
--- /dev/null
+++ b/tests/lexicon_v2_test.rs
@@ -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: every shipped table loads, v2 fields parse, false friends
+//! are never offered as substitutes, and lexicon evidence lifts to the
+//! arbiter's fidelity evidence without raising it.
+//!
+//! 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" }
+"#;
+
+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 evidence_lifts_without_raising_fidelity() {
+    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").evidence.to_fidelity(), FidelityEvidence::None);
+    assert_eq!(by("NN").evidence.to_fidelity(), FidelityEvidence::None);
+    assert_eq!(
+        by("le_trans").evidence.to_fidelity(),
+        FidelityEvidence::DeclaredCorrespondence {
+            consequence_tests: 12,
+            failures: 0
+        }
+    );
+    match by("add_comm").evidence.to_fidelity() {
+        FidelityEvidence::KernelTranslation {
+            format, checked_by, ..
+        } => {
+            assert_eq!(format, ExchangeFormat::Dedukti);
+            assert_eq!(checked_by, ProverKind::Dedukti);
+        },
+        other => panic!("expected a kernel translation, got {other:?}"),
+    }
+}
+
+#[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
+}

From ac318fc167ccd21335c009b8265c54139651ec0f Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <j.d.a.jewell@open.ac.uk>
Date: Mon, 19 Oct 2026 23:44:20 +0000
Subject: [PATCH 6/9] fix(scripts): lexicon-check refuses an empty fixture or
 table set

Review finding on #444 (CodeRabbit): with no reject fixtures, Bash passed
the unmatched `reject/*.toml` pattern through as a literal path; Nickel
failed to load it, and the gate counted that as an expected rejection and
exited 0. Reproduced with an empty reject directory (exit 0, "20 files,
all as expected"). The three sets are now expanded under nullglob and an
empty set fails the gate (exit 1); with the real fixtures it still reports
33 files, all as expected.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
---
 scripts/lexicon-check.sh | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

diff --git a/scripts/lexicon-check.sh b/scripts/lexicon-check.sh
index ed8b588b..1052ce59 100755
--- a/scripts/lexicon-check.sh
+++ b/scripts/lexicon-check.sh
@@ -27,7 +27,23 @@ errfile="$(mktemp)"
 trap 'rm -f "$errfile"' EXIT
 bad=0 n=0
 
-for f in "$root"/data/synonyms/*.toml "$root"/tests/lexicon_fixtures/accept/*.toml; do
+# 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"/}"
@@ -36,7 +52,7 @@ for f in "$root"/data/synonyms/*.toml "$root"/tests/lexicon_fixtures/accept/*.to
   fi
 done
 
-for f in "$root"/tests/lexicon_fixtures/reject/*.toml; do
+for f in "${rejects[@]}"; do
   n=$((n + 1))
   if check "$f"; then
     echo "FAIL (must be rejected): ${f#"$root"/}"

From d631f1040955991620edf330100a7951af50ef40 Mon Sep 17 00:00:00 2001
From: "coderabbitai[bot]"
 <136622811+coderabbitai[bot]@users.noreply.github.com>
Date: Tue, 20 Oct 2026 00:31:14 +0000
Subject: [PATCH 7/9] docs(suggest): clarify synonym lookup, loading errors,
 and evidence conversion

---
 src/rust/suggest/synonyms.rs | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/src/rust/suggest/synonyms.rs b/src/rust/suggest/synonyms.rs
index 5581d2eb..8b9151dc 100644
--- a/src/rust/suggest/synonyms.rs
+++ b/src/rust/suggest/synonyms.rs
@@ -72,6 +72,9 @@ impl LexiconEvidence {
     /// Lift to the arbiter's evidence. `none` and `curated` lift to
     /// [`FidelityEvidence::None`], so a lexicon row never raises an
     /// attempt's fidelity above what its own evidence carries.
+    /// Probe evidence becomes [`FidelityEvidence::DeclaredCorrespondence`];
+    /// kernel evidence becomes [`FidelityEvidence::KernelTranslation`].
+    /// Field values are carried over without validation.
     pub fn to_fidelity(&self) -> FidelityEvidence {
         match self {
             LexiconEvidence::None | LexiconEvidence::Curated => FidelityEvidence::None,
@@ -181,6 +184,14 @@ 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);
@@ -192,6 +203,14 @@ impl SynonymTable {
 
     /// 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, or cannot be deserialised as a synonym table.
     pub fn load_path(path: &Path) -> Result<Self> {
         let raw = crate::provers::bounded_read_corpus_file(path)?;
         let parsed: RawTable =
@@ -216,6 +235,9 @@ impl SynonymTable {
     /// 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,
@@ -246,6 +268,11 @@ impl SynonymTable {
     /// 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(&[]) {

From cb9607ec2a0fe6254f5d1a7b6419e5b732e3e8bd Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 20 Oct 2026 11:36:29 +0000
Subject: [PATCH 8/9] fix(lexicon): only identity claims lift evidence; tighten
 names and probe counts

Addresses the Codex review of #444.

- Fidelity lifting is entry-aware. `SynonymEntry::fidelity_evidence`
  lifts probe/kernel evidence only for an identity claim (a synonym or
  phrase row that is not lossy); every other row gives
  `FidelityEvidence::None`. The context-free `LexiconEvidence::to_fidelity`
  is now private, so a probe on a false friend, specialisation or lossy
  row can no longer promote an attempt to Epi or Sound. Evidence is kept
  on those rows: it attests their relation, not identity.
- The Julia mirror (`saturation_synonyms.jl`) carries `relation` and
  `expand_aliases` expands only synonym and phrase rows, matching
  `Relation::interchangeable`. Untested: no Julia toolchain is reachable
  from the build environment and no CI job runs this module.
- The contract refuses empty alias strings, and probe counts that are not
  integers in the u32 range; the Rust loader refuses empty names too.
  Three new reject fixtures; a test checks the loader agrees with the
  contract on them and that u32::MAX passes both.
- Phrase substitution is documented as one-way (alias -> phrase) until
  phrase-aware site detection exists.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
---
 data/synonyms/README.adoc                     | 18 +++--
 data/synonyms/schema.ncl                      | 27 +++++---
 src/julia/saturation_synonyms.jl              | 17 ++++-
 src/rust/suggest/synonyms.rs                  | 66 ++++++++++++++++---
 .../lexicon_fixtures/reject/empty_alias.toml  |  5 ++
 .../reject/probe_fractional.toml              |  6 ++
 .../reject/probe_over_u32.toml                |  6 ++
 tests/lexicon_v2_test.rs                      | 59 +++++++++++++++--
 8 files changed, 171 insertions(+), 33 deletions(-)
 create mode 100644 tests/lexicon_fixtures/reject/empty_alias.toml
 create mode 100644 tests/lexicon_fixtures/reject/probe_fractional.toml
 create mode 100644 tests/lexicon_fixtures/reject/probe_over_u32.toml

diff --git a/data/synonyms/README.adoc b/data/synonyms/README.adoc
index c6c72db2..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
@@ -87,6 +87,9 @@ Nickel contract `schema.ncl`; `scripts/lexicon-check.sh` (or
   `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,
@@ -99,11 +102,14 @@ Nickel contract `schema.ncl`; `scripts/lexicon-check.sh` (or
 | `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`. It lifts into the
-  arbiter's `FidelityEvidence`: `none` and `curated` lift to `None`
-  (curation is provenance, not fidelity evidence), `probe` to
-  `DeclaredCorrespondence`, `kernel` to `KernelTranslation`. A lexicon row
-  never raises a verdict above its own evidence.
+  `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`.
diff --git a/data/synonyms/schema.ncl b/data/synonyms/schema.ncl
index dbb4d4ca..d9ce06b8 100644
--- a/data/synonyms/schema.ncl
+++ b/data/synonyms/schema.ncl
@@ -26,6 +26,12 @@ 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
@@ -44,9 +50,13 @@ in
 let relations = ["synonym", "specialisation", "generalisation", "false_friend", "phrase"] in
 
 # The witness behind a row, mirroring the ECH-05 `FidelityEvidence` shapes.
-# `none` and `curated` lift to `FidelityEvidence::None` (curated is
-# provenance, not fidelity evidence); `probe` lifts to
-# `DeclaredCorrespondence`; `kernel` lifts to `KernelTranslation`.
+# 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"
@@ -60,9 +70,9 @@ let evidence_check = fun value =>
         || !(std.record.has_field "tests" value)
         || !(std.record.has_field "failures" value) then
         fail "probe evidence needs exactly `tests` and `failures`"
-      else if !(std.is_number value.tests) || !(std.is_number value.failures)
-        || value.tests < 1 || value.failures < 0
-        || value.failures > value.tests then
+      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
@@ -96,9 +106,8 @@ let entry_contract = std.contract.custom (fun _label e =>
     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) || !(std.is_array e.aliases)
-    || !(std.array.all std.is_string e.aliases) then
-    fail "`%{e.canonical}`: `aliases` must be an array of strings"
+  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
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 8b9151dc..6f4ec3ff 100644
--- a/src/rust/suggest/synonyms.rs
+++ b/src/rust/suggest/synonyms.rs
@@ -34,6 +34,12 @@ pub enum Relation {
     /// 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,
 }
 
@@ -48,7 +54,8 @@ impl Relation {
 }
 
 /// The witness behind a lexicon row. Mirrors the ECH-05
-/// [`FidelityEvidence`] shapes; see [`LexiconEvidence::to_fidelity`].
+/// [`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 {
@@ -69,13 +76,11 @@ pub enum LexiconEvidence {
 }
 
 impl LexiconEvidence {
-    /// Lift to the arbiter's evidence. `none` and `curated` lift to
-    /// [`FidelityEvidence::None`], so a lexicon row never raises an
-    /// attempt's fidelity above what its own evidence carries.
-    /// Probe evidence becomes [`FidelityEvidence::DeclaredCorrespondence`];
-    /// kernel evidence becomes [`FidelityEvidence::KernelTranslation`].
-    /// Field values are carried over without validation.
-    pub fn to_fidelity(&self) -> FidelityEvidence {
+    /// 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 } => {
@@ -168,6 +173,34 @@ pub struct SynonymEntry {
     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.
 #[derive(Debug, Clone, Default)]
 pub struct SynonymTable {
@@ -210,11 +243,26 @@ impl SynonymTable {
     /// # Errors
     ///
     /// Returns an error if the file cannot be opened or read as UTF-8,
-    /// exceeds 64 MiB, or cannot be deserialised as a synonym table.
+    /// 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))
     }
 
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/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_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_v2_test.rs b/tests/lexicon_v2_test.rs
index 8f2b8261..2099ae3c 100644
--- a/tests/lexicon_v2_test.rs
+++ b/tests/lexicon_v2_test.rs
@@ -3,7 +3,7 @@
 
 //! 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 without raising it.
+//! 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
@@ -80,6 +80,18 @@ phrase = ["then", "thus"]
 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 {
@@ -125,20 +137,36 @@ fn phrase_spellings_are_interchangeable() {
 }
 
 #[test]
-fn evidence_lifts_without_raising_fidelity() {
+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").evidence.to_fidelity(), FidelityEvidence::None);
-    assert_eq!(by("NN").evidence.to_fidelity(), FidelityEvidence::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.to_fidelity(),
+        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: 12,
+            consequence_tests: 8,
             failures: 0
         }
     );
-    match by("add_comm").evidence.to_fidelity() {
+    // 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, ..
         } => {
@@ -149,6 +177,23 @@ fn evidence_lifts_without_raising_fidelity() {
     }
 }
 
+/// 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";

From 0b4f98a6dd1d0870d53ee464ce833a48147e3e94 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 20 Oct 2026 12:27:10 +0000
Subject: [PATCH 9/9] ci(agda): pin the Agda proofs job to ubuntu-24.04

ubuntu-latest is now 26.04, whose apt agda 2.8.0 rejects the options
agda-stdlib v1.7.3 sets ("Unrecognized option: --warn=noUserWarning"),
so the job fails on main and on every PR that touches its path filter.
24.04 ships agda 2.6.3, the version the corpus is verified against.
The lasting fix is moving the stdlib to a 2.8-compatible tag; unpin then.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
(cherry picked from commit 3716a1162afed8ec5103b13c1436ce81312970b7)
---
 .github/workflows/dogfood-proofs-ci.yml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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