IV.R256 — Lean verification

The spectral formula and its numerical bounds are verified in TauLib.BookIV.Sectors.FineStructure. The theorem alpha_spectral_inverse_in_range proves 137 < alpha_spec^(-1) < 139, bracketing the experimental value with zero sorry terms.