From eb5d5817e3d2d81b7008ca890a1b6007c470b1ad Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Mon, 19 Oct 2026 22:14:34 +0000 Subject: [PATCH 1/4] 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 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) += 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) +# +# false_friend_scan.sh — lexical cognate / false-friend / homonym census over +# training_data/proof_states_.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 "namegoal" 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" Date: Mon, 19 Oct 2026 22:27:41 +0000 Subject: [PATCH 2/4] 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 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/4] 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 "namegoal" 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" Date: Mon, 19 Oct 2026 22:43:37 +0000 Subject: [PATCH 4/4] 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 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 "namegoal" with whitespace normalised, one row per -# distinct (name, goal) pair, sorted on the name for join(1). +# prover -> TSV "namegoal": 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 }