ClosedLoop

formal source

 174/-! ## §4 Holonomy: Curvature as Parallel Transport Failure -/
 175
 176/-- A closed loop in spacetime, parameterized by λ ∈ [0, 1] with γ(0) = γ(1). -/
 177structure ClosedLoop extends SpacetimeCurve where
 178  closed : path 0 = path 1
 179
 180/-- The holonomy defect: the difference between a vector and its parallel
 181    transport around a closed loop.
 182
 183    For an infinitesimal loop enclosing area δA^{μν}, the defect is:
 184    δV^ρ = R^ρ_{σμν} V^σ δA^{μν}
 185
 186    This is the geometric meaning of the Riemann tensor. -/
 187def HolonomyDefect (g : MetricTensor) (loop : ClosedLoop) (V_init : Fin 4 → ℝ) : Prop :=
 188  ∃ (sol : ParallelTransportSolution g loop.toSpacetimeCurve ⟨0, V_init⟩),
 189    SmoothField sol.V ∧ sol.V 1 ≠ V_init
 190
 191/-- Vanishing Riemann implies zero holonomy: no defect around any closed loop. -/
 192theorem no_holonomy_if_flat (loop : ClosedLoop) (V_init : Fin 4 → ℝ) :
 193    ¬ HolonomyDefect minkowski_tensor loop V_init := by
 194  intro ⟨sol, h_smooth, h_ne⟩
 195  apply h_ne
 196  -- In flat spacetime, parallel transport keeps V constant
 197  have h_const := parallel_transport_flat loop.toSpacetimeCurve sol.V sol.is_parallel
 198  -- V is constant, so V(1) = V(0) = V_init
 199  have h_zero : ∀ l μ, deriv (fun l' => sol.V l' μ) l = 0 := h_const
 200  -- V(0) = V_init by initial condition
 201  have h_ic : sol.V 0 = V_init := sol.initial_condition
 202  -- V(1) = V(0) since all derivatives vanish (V is constant)
 203  have h_eq_comp : ∀ μ, sol.V 1 μ = sol.V 0 μ := by
 204    intro μ
 205    have hconst := is_const_of_deriv_eq_zero (h_smooth μ) (fun l => h_zero l μ)
 206    exact hconst 1 0
 207  have h_eq : sol.V 1 = sol.V 0 := by