Registry · Proposition IV.P40 tau-effective formalized

IV.P40 — Observable Hierarchy

EM observables form a strict hierarchy: A_mu (gauge-dependent) -> F_mu_nu (locally invariant) -> Wilson loops (globally invariant).

Book IV Part 4 Ch. 27

Dependency Graph

Depends on (2)

IV.D92 IV.D108

Lean Formalization

Module: TauLib.BookIV.Electroweak.GaugeInvariance2

Symbol: Tau.BookIV.Electroweak.ObservableHierarchy