ci: check Lean snippets in released READMEs

[kim-em]

Summary

• pin a tested lean-readme revision and check every released README source in the existing CI job
• check displayed theorem quotations definitionally against explicit, fully qualified imported declarations with lean recall Fully.Qualified.name
• collect imports from checked command blocks before validation, so later examples can stay self-contained while recall fences reuse earlier imports
• keep the recall implementation independent of Mathlib and avoid ambiguous suffix matching
• preserve concrete factorization, irreducibility, and evaluation examples; hidden native-runtime prefixes execute examples backed by precompiled implementations
• correct stale quoted signatures and document the convention

The general recall checker and import handling are proposed independently as david-christiansen/lean-readme#1 and david-christiansen/lean-readme#2. This PR pins a tested private-fork commit that combines them with the explicit-target extension, so it does not wait for either upstream PR.

Validation

• all 115 README Lean blocks pass lean-readme, including 44 explicitly targeted theorem-signature blocks and the concrete Berlekamp–Zassenhaus examples
• all recall blocks omit repeated import and open setup
• zero lean nocheck blocks
• the pinned lean-readme revision passes lake build, lake test, lake shake, and its self-check
• lake build
• lake build HexAggregateCheck lean-readme
• python3 scripts/check_copyright_headers.py
• python3 scripts/release/check_released_manifest.py
• python3 scripts/bench/check_factor_sweep_freshness.py
• git diff --check