P04: add portable Mathlib search skill

[akiezun]

Scope

• add one portable mathlib-search skill shared by roadmap and review work
• add a read-only helper with stable autoform-mathlib-search/v1 JSON
• search project sources and the checked-out pinned Mathlib tree
• optionally invoke an already-installed Loogle with index writes disabled
• verify every Loogle result against local source before reporting it
• classify results as exact, partial, or missing
• update Roadmap, Agent Review, host manifests, and server documentation

Non-goals

• no Loogle installation, network search, or dependency update
• no claim that a name match proves type compatibility; selected candidates still require #check
• no execution-branch proof automation

Dependency

Stacked on P00 (upstream facebookresearch#9), whose manifest authorizes the independent reimplementation and assigns archived Loogle behavior to this single owner. This branch is independent of P01–P03.

Validation

• focused mathlib-search/plugin/skill tests — 23 passed
• make lint — passed
• make test — 550 passed, 1 skipped
• make check-example — passed, including strict MkDocs build
• Mathlib Search skill validator — passed
• plugin validator — passed

Tests cover local project and pinned-Mathlib search, exact/partial/missing outcomes, ambiguous suffixes, Loogle present, absent and failed fallback, deterministic JSON, read-only behavior, and rejection of invented Loogle names.

Risks and migration

The fallback is lexical name search, not type-shape search; shape queries require an installed Loogle. The helper scans local source trees and can be slower than Loogle on a full checkout, but it never installs or writes indexes.

Rollback

Revert commit a44577d; existing Lean LSP/REPL and roadmap behavior are unchanged.