IV.R372 — Lean verification

The spectral formula and its numerical bounds are verified in the Lean 4 module TauLib.BookIV.Sectors.FineStructure; the theorem alpha_spectral_inverse_in_range proves 137 < alpha_spec^{-1} < 139, bracketing the experimental value with machine-checked rigor.