Registry · Theorem
IV.T139
tau-effective
formalized
IV.T139 — NLO from EW Projection
Bridge: NLO numerator 5 = |V_EW|, denominator 7 = |V_complement|.
Book IV
Part 4
Ch. 31
Dependency Graph
Depends on (1)
Lean Formalization
Module: TauLib.BookIV.Electroweak.WeinbergNLO
Symbol: nlo_from_ew_projection