no_holonomy_if_flat

formal source

 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
 208    funext μ
 209    exact h_eq_comp μ
 210  simpa [h_ic] using h_eq
 211
 212/-- The holonomy-curvature correspondence for infinitesimal loops.
 213
 214    For a parallelogram loop with sides δx^μ and δy^ν, the holonomy defect
 215    of a vector V^σ is:
 216    δV^ρ = R^ρ_{σμν} V^σ δx^μ δy^ν + O(|δx|²|δy| + |δx||δy|²)
 217
 218    This is the defining property of the Riemann tensor from the geometric
 219    viewpoint: curvature IS parallel transport failure.
 220
 221    The leading-order defect equals the Riemann contraction with the
 222    enclosed area bivector. -/