IV.R253 — Lean formalization

Lean verification: em_is_weak_squared and weak_strong_power_formula in TauLib.BookIV.Sectors.CouplingFormulas, proved by ring and field_simp. The power ladder is the unique monotone sequence compatible with depth grading, polarity, and kappa(A) + kappa(D) = 1.