Kerr-Newman

A standalone Lean 4 proof of the local equivalence between Kerr–Newman perturbation systems (1) and (7), for both spin signs, with reproducible source and an axiom audit.