Registry · Definition IV.D95 tau-effective formalized

IV.D95 — Sigma-Equivariance

A U(1)-valued functional Phi on the EM loop space is sigma-equivariant if Phi(sigma o gamma) = conjugate(Phi(gamma)), respecting the bipolar involution.

Book IV Part 4 Ch. 27

Dependency Graph

Depends on (1)

IV.D94

Lean Formalization

Module: TauLib.BookIV.Electroweak.GaugeInvariance

Symbol: Tau.BookIV.Electroweak.Sigmaequivariance