Registry · Proposition IV.P44 tau-effective formalized

IV.P44 — Current Conservation from Gauge Invariance

The source equation d*F = *J implies partial_mu J^mu = 0 (continuity equation) as an algebraic identity from d^2 = 0.

Book IV Part 4 Ch. 28

Dependency Graph

Depends on (1)

IV.T54

Lean Formalization

Module: TauLib.BookIV.Electroweak.TauMaxwell

Symbol: Tau.BookIV.Electroweak.CurrentConservationFromGaugeInvariance