Lean: spectral theorem for compact normal operators via restriction to (⨆ eigenspaces)ᗮ

To generalize Mathlib's orthogonalComplement_iSup_eigenspaces_eq_bot from self-adjoint to normal T on a complex Hilbert space: let V = (⨆ μ, eigenspace T μ)ᗮ. It is invariant under T and adjoint T, because T† = conj μ on E_μ for normal T. Take S := T.restrict h and R := (adjoint T).restrict h'. Prove R = adjoint S with (eq_adjoint_iff R S).2 plus simp [coe_inner, restrict_apply, adjoint_inner_left]. IsStarNormal S follows by ext from star_comm_self' T. S has no eigenvectors, so the Fredholm alternative (IsCompactOperator.hasEigenvalue_iff_mem_spectrum) gives σ(S) ⊆ {0}, and then IsStarNormal.spectralRadius_eq_nnnorm S gives S = 0. Gotchas: spectralRadius is a sup over the *quasispectrum* (rewrite with quasispectrum_eq_spectrum_union_zero). rw [← nnnorm_eq_zero] fails on V →L[ℂ] V because of instance-path mismatches. Instead, rewrite spectralRadius_eq_nnnorm S inside a hypothesis and finish with (opNorm_zero_iff _).1.