Registry · Proposition
IV.P32
tau-effective
formalized
IV.P32 — No Rest Frame
The photon has no rest frame: a Lorentz boost cannot bring it to v=0 since p=0 implies E=0.
Dependency Graph
Depends on (1)
Depended on by (1)
Lean Formalization
Module: TauLib.BookIV.Electroweak.PhotonMode
Symbol: Tau.BookIV.Electroweak.NoRestFrame