Registry · Proposition IV.P45 tau-effective formalized

IV.P45 — Charge Density as Winding-Number Density

Charge density rho(x) = e * sum_a n_a^(wind) * n_a(x); charge quantization is automatic since winding numbers are integers.

Book IV Part 4 Ch. 28

Dependency Graph

Depends on (2)

IV.D114 IV.D84

Lean Formalization

Module: TauLib.BookIV.Electroweak.TauMaxwell

Symbol: Tau.BookIV.Electroweak.ChargeDensityAsWindingnumberDensity