Registry · Proposition IV.P60 tau-effective formalized

IV.P60 — Z Field Composition

Z_mu = W^3_mu cos(theta_W) - B_mu sin(theta_W): mixed mode seeing both lobes simultaneously. Contains SU(2) (lobe-distinguishing) and U(1) (uniform) components. Heavier than W by factor 1/cos(theta_W).

Book IV Part 4 Ch. 31

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookIV.Electroweak.WeakHolonomy2

Symbol: Tau.BookIV.Electroweak.ZFieldComposition