FieldConfig

formal source

 107/-! ## Local vs Global Gauge Symmetry -/
 108
 109/-- A field configuration is a function from spacetime to the ledger. -/
 110def FieldConfig (X : Type*) := X → ℂ
 111
 112/-- Global gauge transformation: same phase everywhere. -/
 113noncomputable def globalGauge (θ : ℝ) (ψ : FieldConfig X) : FieldConfig X :=
 114  fun x => U1Transform θ (ψ x)
 115
 116/-- Local gauge transformation: phase depends on position.
 117
 118    This is the key upgrade that requires introducing gauge fields! -/
 119noncomputable def localGauge (θ : X → ℝ) (ψ : FieldConfig X) : FieldConfig X :=
 120  fun x => U1Transform (θ x) (ψ x)
 121
 122/-- Local gauge invariance requires introducing a connection (gauge field).
 123    The covariant derivative D_μ ψ = ∂_μ ψ - i A_μ ψ transforms properly.
 124    This is a fundamental principle encoded in the structure of the theory. -/
 125def localGaugeDescription : String :=
 126  "D_μ ψ = ∂_μ ψ - i A_μ ψ transforms covariantly under local gauge"
 127
 128/-! ## The Gauge Field (Connection) -/
 129
 130/-- A gauge field (connection 1-form) transforms as:
 131    A_μ → A_μ + ∂_μ θ
 132
 133    This compensates for the phase gradient in local gauge transformations. -/
 134structure GaugeField (X : Type*) where
 135  components : Fin 4 → X → ℝ
 136
 137/-- **THEOREM**: A gauge field has 4 components (one per spacetime dimension). -/
 138theorem gauge_field_components (X : Type*) (A : GaugeField X) :
 139    ∃ (comps : Fin 4 → X → ℝ), A.components = comps := ⟨A.components, rfl⟩
 140