feat(suggest): implement echidna suggest CLI verb — mechanical tactic-variant finder

Closes §4.1+§4.3 from ECHIDNA-NOTES-2026-04-27.md.  New `echidna suggest
<file>:<lemma> --prover <P>` verb extracts a named lemma, identifies tactic
sites, looks up alternatives in data/synonyms/<prover>.toml, re-runs the
prover on each single-site substitution, and prints a ranked Markdown table.

Module layout:
  src/rust/suggest/
    mod.rs      — SuggestConfig, run() entry point, parse_target, detect_prover
    extractor.rs — Probe + TacticSite; per-prover line-based extractors for
                   Isabelle/HOL, Coq, Lean4, Idris2, Agda
    synonyms.rs  — SynonymTable + SynonymEntry (TOML deserialisation, by_name index)
    variant.rs   — Variant generation (single-site substitutions, Levenshtein ranking)
    tester.rs    — VariantOutcome; concurrent JoinSet-based variant testing
    report.rs    — Markdown table printer (closes > fails > timeout > syntax; edit asc)

26 new unit tests across 5 files; lib test count 972 → 998.  All 998 pass.

Does NOT call ProverBackend::suggest_tactics (that is the §4.4 GNN layer).
Acceptance criteria covered: parse_target, detect_prover, synonym alternatives,
word-boundary substitution, Levenshtein, dry-run, empty-result paths.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

src/rust/lib.rs

@@ -35,6 +35,7 @@ pub mod parsers;
 pub mod proof_encoding; // CBOR encoding + proof identity hashing
 pub mod proof_search; // Chapel parallel proof search (optional feature)
 pub mod provers;
+pub mod suggest; // Mechanical tactic-variant finder (echidna suggest verb)
 pub mod vcl_ut;
 pub mod verification;
 #[cfg(feature = "verisim")]

src/rust/main.rs

@@ -174,6 +174,37 @@ enum Commands {
 
     /// Interactive diagnostics REPL for health monitoring
     Diagnostics,
+
+    /// Suggest tactic variants that close a failing lemma
+    Suggest {
+        /// Target in `<file>:<lemma>` form, e.g. `Foo.thy:bar`
+        #[arg(value_name = "TARGET")]
+        target: String,
+
+        /// Prover to use (auto-detected from file extension if absent)
+        #[arg(short, long)]
+        prover: Option<ProverKind>,
+
+        /// Time budget per variant attempt in seconds
+        #[arg(long, default_value_t = 60)]
+        budget: u64,
+
+        /// Maximum number of variants to report
+        #[arg(long, default_value_t = 10)]
+        top: usize,
+
+        /// Synonym table directory (defaults to `data/synonyms/`)
+        #[arg(long)]
+        synonyms_dir: Option<PathBuf>,
+
+        /// Don't run the prover; just print candidate variants
+        #[arg(long)]
+        dry_run: bool,
+
+        /// Maximum concurrent variant tests
+        #[arg(long, default_value_t = 4)]
+        max_parallel: usize,
+    },
 }
 
 #[tokio::main]
@@ -254,6 +285,27 @@ async fn main() -> Result<()> {
         Commands::Diagnostics => {
             diagnostics_command().await?;
         },
+        Commands::Suggest {
+            target,
+            prover,
+            budget,
+            top,
+            synonyms_dir,
+            dry_run,
+            max_parallel,
+        } => {
+            let synonyms_dir = synonyms_dir.unwrap_or_else(|| PathBuf::from("data/synonyms"));
+            let config = echidna::suggest::SuggestConfig {
+                target,
+                prover,
+                budget: std::time::Duration::from_secs(budget),
+                top,
+                synonyms_dir,
+                dry_run,
+                max_parallel,
+            };
+            echidna::suggest::run(config).await?;
+        },
     }
 
     Ok(())