feat(lexicon): echidna lexicon scan + canonicaliser completeness (stage 6c PR 3)

CHANGELOG.adoc

@@ -8,6 +8,64 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== Added — `echidna lexicon scan`, 2026-10-27
+
+* *`+echidna lexicon scan+`* (`+src/rust/lexicon/scan.rs+`,
+  `+just lexicon-scan+`) — compares `+training_data/+` corpora by theorem
+  name and by canonical statement shape, and writes cognates, false-friend
+  and specialisation candidates, and synonym candidates (joined by
+  identical text, shape or skeleton) as JCS JSON Lines with UUIDv8 pair
+  ids. Flag-only: every record carries `+evidence = none+`, and
+  `+data/synonyms/+` is never written. Presets `+learning+`,
+  `+spanning+` (one corpus per prover family), `+in-family+` and `+full+`.
+  Per-corpus coverage and key-collision samples are written alongside.
+  Whitespace runs collapse to one space, or to a newline when they hold
+  one, so a line comment cannot swallow the rest of a statement. A re-run
+  removes only the file names the scan writes.
+  The per-name cap (`+--max-pairs-per-name+`) bounds folded-name pairs
+  across a whole folded group, not per raw-name pair. Corpus keys may not
+  start or end with `+_+`, so pair file names stay unambiguous; a hyphen is
+  allowed, so the shipped `+2026-03-20+` corpus can be scanned.
+  Anonymous names (`+_+`) are indexed like any other, so
+  `+--keep-generic+` now joins them. A bare signature over any type names
+  (`+Tree -> Tree -> Tree+`) no longer proposes a synonym. With the global
+  `+--format json+`, the scan prints one JCS summary object on stdout.
+
+==== Fixed — canonicaliser, 2026-10-27
+
+* *`+corpus::canonical+` no longer panics* on a statement whose last
+  token is an unbalanced opening bracket (eight `+open + 1..close+` slices
+  are now guarded). `+structural_key+` reaches this from `+corpus ingest+`
+  and the octad identity keys. No key changes.
+* *String literals are opaque atoms.* A quoted span is lexed as a formula
+  only where it wraps one: at the start of a statement, after `+:+`, or
+  after an Isabelle statement keyword. Elsewhere (`+s = "a//b"+`, ACL2
+  `+"Goal"+` hints, Why3 `+meta "…"+`) it is one constant, so its contents
+  are no longer read as comments, operators or variables, and a backslash
+  escapes the next character. A quote opens a formula only when its close
+  also ends the statement (or meets another quote or an Isabelle keyword),
+  and a quote right after an unwrapped formula is the next proposition,
+  so `+"a" == "z"+` keeps its leading literal. *Key change*: statements with such a literal
+  get new keys; distinct literals no longer share one. On
+  `+training_data/+` this splits a dozen Mizar and seven Why3 key
+  collisions; coverage moves by at most 0.1 point per corpus.
+* *`+StructuralKey::complete+`* (new, `+#[serde(default)]+`) reports
+  whether the shape accounts for the whole statement: false when the
+  parser stops early, invents a missing operand, gives a binary-only
+  prefix operator one operand (`+(= (+ x 1))+`), or the input ends inside
+  an open bracket, a quoted statement or a block comment; when a closer
+  meets a group of another kind; when the statement meets
+  notation `+dk-shape-v1+` has no rule for (HOL binders, `+~+`, `+==>+`,
+  Isabelle `+\<…>+` escapes), drops a statement's own leading tokens as a
+  "header", misreads a leading group as a telescope, or cuts off a tree
+  deeper than 256 levels, counting bracket groups and infix operators
+  (the parser is now bounded, so neither deep nesting nor a long flat
+  chain such as `+a -> a -> …+` can overflow a caller's stack).
+  `+corpus identity+` skips incomplete declarations and says how many. No key changes.
+  Measured on `+training_data/+`, 0.4 %–94 % of a corpus is read
+  completely; the rule-level causes are recorded for a `+dk-shape-v2+`
+  decision in `+docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc+`.
+
 ==== Added — structural cross-prover identity keys, 2026-10-22
 
 * *`+src/rust/corpus/canonical.rs+`* — normalises a declaration's *type*

Justfile

@@ -1163,6 +1163,14 @@ lexicon-check:
     scripts/lexicon-check.sh
     cargo test --locked --test lexicon_v2_test
 
+# Mine lexicon candidates across training_data/ corpora: cognates, false
+# friends and synonym candidates as JCS JSON Lines under target/lexicon-scan.
+# Flag-only (evidence = none); never edits data/synonyms/. Presets: learning,
+# spanning, in-family, full.
+lexicon-scan preset="learning":
+    cargo run --locked --bin echidna -- lexicon scan --preset {{preset}}
+    cargo test --locked --test lexicon_scan_test
+
 # Run the saturation-campaign cargo tests only (139 cases + 1 ignored).
 test-saturation:
     cargo test --lib -- \

data/synonyms/README.adoc

@@ -219,6 +219,42 @@ Nickel contract `schema.ncl`; `scripts/lexicon-check.sh` (or
 Corpus-mined candidates (owner decision D4) are flag-only: they carry
 `evidence = { kind = "none" }` and never set `semantic_class` on their own.
 
+=== Mining candidates: `echidna lexicon scan`
+
+`echidna lexicon scan --preset learning` (or `just lexicon-scan`) compares
+`training_data/proof_states_<corpus>.jsonl` corpora on two axes, the theorem
+*name* and the canonical *shape* of its statement (`dk-shape-v1`,
+`src/rust/corpus/canonical.rs`), and writes review candidates as JCS JSON
+Lines under `target/lexicon-scan/`. It never edits this directory.
+
+[cols="1,2,2"]
+|===
+| | same shape | different shape
+
+| *same name*
+| cognate (`cognate_exact`, `cognate_shape`)
+| false friend or specialisation (`cognate_skeleton`, `differs`)
+
+| *different name*
+| synonym candidate (joins `text`, `shape`, `skeleton`)
+| unrelated, not reported
+|===
+
+A pair is `unparsed` when either statement was not read completely by the
+canonicaliser (`StructuralKey::complete`): its key is then a prefix that
+other statements share, so it says nothing. Joins between different names
+also skip shapes too thin to identify anything (`informative`: a variable in
+function position, fewer than three constants, or a bare type signature).
+Every skip is counted in `summary.jsonl`; `coverage.jsonl` reports, per
+corpus, how much the canonicaliser read and how often distinct statements
+share a key. Each candidate's `id` is the UUIDv8 content id of the
+statement pair, independent of scan direction and normaliser version, so a
+review decision survives a re-scan.
+
+A candidate becomes a row here only by curation: a person writes the row
+with `evidence = curated` (or `probe` / `kernel` once that evidence exists),
+and the Nickel contract checks it like any other.
+
 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`).
@@ -242,8 +278,9 @@ prover no longer accepts (or never accepted in this version).
 - Cross-prover synonym graph (Isabelle `le_trans` ↔ Coq `Rle_trans` ↔
   Lean `le_trans`) is intentionally **out of scope** here — that's
   `echidna port`, not `echidna suggest`.
-- ML-driven synonym discovery from the corpus (mining
-  `training_data/`) is in §4.4 of the notes, not this layer.
+- ML-driven synonym discovery from the corpus is in §4.4 of the notes,
+  not this layer. Syntactic mining of `training_data/` is
+  `echidna lexicon scan` (above); it proposes, it never writes here.
 
 == Maintenance
 

docs/CORPUS.adoc

@@ -242,6 +242,22 @@ Isabelle writes the same fact without binders and Why3 states it over
 therefore *tiered*: exact structural key first, skeleton key second. Any
 consumer that only compares one field should compare both.
 
+A key is only as good as the parse behind it. `+StructuralKey::complete+`
+says whether the canonicaliser read the *whole* statement; when it did not
+(its parser stopped early, invented an operand or found a relation with one
+operand, the input ended inside an
+open bracket, quote or comment, a closer met a group of another kind, it
+met notation it has no rule for — HOL's `+!+` and `+?+` binders, Isabelle's
+`+\<…>+` escapes — or a header drop discarded the statement's own leading
+tokens), the key is still reported at the
+structural tier but is a *prefix* that other statements share. Treat an
+incomplete key as no identity at all: `+corpus identity+` skips such
+declarations and reports how many it skipped. Measured on `+training_data/+`, the
+share of statements read completely ranges from under 1% (Isabelle/ZF) to
+over 90% (λProlog); see
+`+docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc+`
+(PR 3 results) and `+echidna lexicon scan+`.
+
 The CLI surfaces it directly:
 
 [source,bash]