Registry · Proposition IV.P38 tau-effective formalized

IV.P38 — Parallel Transport is Gauge-Covariant

The parallel transport operator is gauge-covariant for open paths and gauge-invariant for closed loops.

Book IV Part 4 Ch. 27

Dependency Graph

Depends on (1)

Lean Formalization

Module: TauLib.BookIV.Electroweak.GaugeInvariance

Symbol: Tau.BookIV.Electroweak.ParallelTransportIsGaugecovariant