feat: add Burnside normal p-complement theorem eval problem

[kim-em]

This PR adds Burnside's normal p-complement theorem (1911): if a Sylow p-subgroup P of a finite group G is central in its normalizer, then G has a normal p-complement. The prototype transfer-based local-to-global argument and the seed of fusion theory.

Mathlib already contains the underlying construction MonoidHom.ker_transferSylow_isComplement'; the eval problem is to assemble the named theorem statement from that machinery.

🤖 Prepared with Claude Code

[kim-em]

Closing: this statement is essentially already in Mathlib via MonoidHom.ker_transferSylow_isComplement' and MonoidHom.not_dvd_card_ker_transferSylow in Transfer.lean. The full proof is just 5 lines assembling those existing lemmas — see the spelled-out proof for the witness. As a benchmark this is an "API discovery" exercise rather than a theorem-proving challenge. Closing in favour of stronger results not in Mathlib (Hall's theorem for solvable groups, Frobenius's p-nilpotence, etc.) in a future PR.