Document the McKay proof and formalization blueprint

[Vilin97]

What

• adds a detailed natural-language proof certificate for the McKay equality, following the exact Cabanes–Späth/IMN/Rossi theorem chain
• expands the final type-D argument through the doubly regular case, Lemma 5.8, the twisted Frobenius subgroup, stable transversals, extension maps, and Theorem 6.12
• records the search for a simpler proof and distinguishes the general theorem from p-solvable special cases
• audits current mathlib, odd-order, Qiuzhen CFSG, TauCeti, lean-pool, and TNLean at reproducible commits
• adds a file-by-file Lean blueprint, exact missing obligations, latest-mathlib port boundaries, and a heartbeat-clean import plan

Why

This is the second stacked milestone after #32. It turns the literature proof and the current Lean ecosystem into an auditable implementation plan without disguising CFSG or the finite-reductive character theory as assumptions.

Checks

• lake build (2329 jobs)
• latexmk -pdf -interaction=nonstopmode -halt-on-error for both documents
• no unresolved references, overfull boxes, or LaTeX errors/warnings in the final logs
• rendered and visually inspected all 10 proof pages and all 17 blueprint pages
• adversarial source audit against arXiv 2410.20392v2/Annals theorem numbering
• Lean source scan found no sorry, axiom, admit, heartbeat, or recursion-depth overrides