Formalize the McKay conjecture statement

[Vilin97]

What changed

• Adds a new self-contained mckay-conjecture Lean 4 package.
• Pins the package to mathlib commit 9cebae57f419f984d008f357605b2621a1d9f13b and Lean v4.33.0-rc1, the current mathlib head at project creation.
• Defines ordinary irreducible complex characters as character functions with certified natural degree and a simple FDRep ℂ G witness.
• Defines the p'-degree subtype, the Sylow normalizer N_G(P), and McKayConjecture.Statement as the corresponding cardinal equality.
• Adds identity-value and extensionality lemmas proving that the certified degree does not overcount a character function.
• Adds a path-scoped CI workflow and a root README entry.

Why

This establishes a precise, reproducible, axiom-free formal target for the full McKay theorem before proof engineering begins. Cardinal.mk is used instead of Nat.card, avoiding the latter's silent value 0 on infinite types while finiteness of the new character wrapper has not yet been formalized.

Statement audit

Two independent adversarial reviewer agents compiled and inspected the statement. Both returned FAITHFUL, specifically checking character-versus-representation counting, uniqueness of degree, p'-degree divisibility in ℕ, the Sylow and normalizer encodings, prime/finite-group assumptions, and universe behavior.

Validation

• lake build — succeeds (2,329 jobs)
• repository scan — no sorry, axiom, admit, or heartbeat override in the new package
• git diff --check — clean
• CI workflow YAML parse — succeeds