Registry · Theorem IV.T40 tau-effective formalized

IV.T40 — AB Phase Quantization

The AB phase is a root of unity iff the enclosed magnetic flux is a rational multiple of the flux quantum Phi_0 = 2pi*hbar/e.

Book IV Part 4 Ch. 27

Dependency Graph

Depends on (1)

IV.D93

Depended on by (2)

IV.R23 IV.T52

Lean Formalization

Module: TauLib.BookIV.Electroweak.GaugeInvariance2

Symbol: Tau.BookIV.Electroweak.AbPhaseQuantization