192theorem no_holonomy_if_flat (loop : ClosedLoop) (V_init : Fin 4 → ℝ) : 193 ¬ HolonomyDefect minkowski_tensor loop V_init := by
proof body
Tactic-mode proof.
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. -/
depends on (25)
Lean names referenced from this declaration's body.