fix: code-review findings in local-search caching + fuzzy

[KrystianNowakowski]

Addresses the high-effort code review of the WS1+WS2 local-search work. Fixes the three substantive findings plus two cheap ones; the rest were lower-severity (and the reported str.format brace crash was refuted — str.format does not re-scan replacement values).

• Fix list declarations bug #1 char-cap break→continue (accumulate_used_definitions): an over-budget definition no longer aborts the loop, so smaller later definitions the proof used still get cached.
• Anthropic "incomplete" nodes in LangSmith trace leads to full incomplete ax-prover runs #2 ambiguous bare-name precision (_used_in_code + _AMBIGUOUS_BARE_NAMES): a local decl with a ubiquitous simple name (min/map/insert/…) is cached only when its qualified name appears in the code — avoids caching Foo.min just because the proof used Mathlib's min. Distinctive names (e.g. extract_min) still cache from a bare reference, preserving recall for opened names.
• Detect axioms and search tactics public #4 budget the injected block (_render_used_definitions): the <local-definitions> block is bounded to a fraction of the model's input window, dropping whole trailing entries (verbatim Lean source is never chopped) with an omission note — consistent with the existing build-output truncation.
• Add commands to submit batch jobs #7 silent no-op log (_find_local_searcher): warns when the local-search tool is configured but its searcher can't be recovered, so the caching feature degrading to a no-op is visible.
• Add support for Qwen 3.5 and initial testing #8 hoist query normalization (_score_name): the fuzzy query is normalized once per search instead of once per declaration.

392 unit tests pass (7 new), ruff clean. New tests cover the continue-not-break cap, the ambiguous-vs-qualified-vs-distinctive caching cases, and the injection budget (drop-trailing / keep-all / empty).

🤖 Generated with Claude Code

---

Note

Medium Risk
Changes what definitions are cached and how much context the proposer sees each iteration; behavior is intentional but can affect proof quality on name collisions or large caches.

Overview
Hardens local-search used-definition caching and how those definitions are fed back into the proposer.

Caching (accumulate_used_definitions) now uses _used_in_code instead of bare identifier matching: ubiquitous simple names (min, map, insert, …) are cached only when the qualified name appears in the proof, while distinctive names still match bare references. When the char budget is exceeded, an oversized entry is skipped (continue) rather than stopping the loop, so later smaller defs can still be added.

Proposer prompt: _render_used_definitions caps the <local-definitions> block to roughly ¼ of max_input_tokens (char proxy), dropping whole trailing entries with an omission note instead of dumping the full cache.

Ops / perf: _find_local_searcher logs a warning if the local-search tool is configured but the LocalLeanSearcher instance cannot be recovered. Fuzzy search normalizes the query once per file scan via _score_name.

Unit tests cover budget rendering, continue-on-oversize, and ambiguous vs qualified caching.

^{Reviewed by Cursor Bugbot for commit 95413be. Bugbot is set up for automated code reviews on this repo. Configure here.}