Registry · Definition IV.D84 tau-effective formalized

IV.D84 — Electric Charge

Electric charge is the winding number n_B of the U(1) holonomy around the B-sector cycle on T^2, giving Q = n_B * e with n_B in Z.

Book IV Part 4 Ch. 26

Dependency Graph

Depends on (1)

Depended on by (5)

Lean Formalization

Module: TauLib.BookIV.Electroweak.PhotonMode

Symbol: Tau.BookIV.Electroweak.ElectricCharge