Registry · Definition IV.D116 tau-effective formalized

IV.D116 — Weak Isospin Generators

T_i := (1/2) sigma_i (Pauli matrices). T_3 measures lobe eigenvalue (isospin projection), T_1 and T_2 exchange lobes (polarity-switching), T_pm = T_1 pm iT_2 are raising/lowering operators.

Book IV Part 4 Ch. 31

Dependency Graph

Depends on (1)

Depended on by (2)

Lean Formalization

Module: TauLib.BookIV.Electroweak.WeakHolonomy

Symbol: Tau.BookIV.Electroweak.WeakIsospinGenerators