Registry · Definition IV.D103 tau-effective formalized

IV.D103 — Electromagnetic Current 4-Vector

The EM current 4-vector J^mu = sum_a q_a n_a u_a^mu is the B-sector component of the total defect density, with charges from U(1) winding numbers.

Book IV Part 4 Ch. 28

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookIV.Electroweak.TauMaxwell

Symbol: Tau.BookIV.Electroweak.ElectromagneticCurrent4vector