no_holonomy_if_flat
Vanishing Riemann curvature on Minkowski spacetime forces parallel transport around any closed loop to return the initial vector unchanged. Relativists and differential geometers cite this to confirm holonomy measures curvature alone. The tactic proof assumes a defect solution, invokes the flat-transport lemma to obtain constancy, then applies zero-derivative constancy and the initial-condition equality to reach a contradiction.
claimLet $g$ be the Minkowski metric tensor. For any closed loop $C$ (a curve with $C(0)=C(1)$) and any initial vector $V_0$, the holonomy defect predicate does not hold: there is no parallel-transport solution $V$ along $C$ such that $V$ is smooth and $V(1)neq V_0$.
background
ClosedLoop extends a spacetime curve by the endpoint condition path(0)=path(1). HolonomyDefect(g, loop, V_init) is the proposition that a parallel-transport solution exists whose vector field is smooth yet satisfies V(1) ≠ V_init; the defect is the geometric signature of the Riemann tensor contracted with the enclosed area bivector. The module develops parallel transport via the Levi-Civita connection on 4D spacetime, proving that transport preserves inner products and that flat transport yields constant vectors. The local setting states that curvature arises from non-uniform J-cost defect density, so parallel-transport failure around loops manifests ledger imbalance.
proof idea
The proof is by contradiction in tactic mode. It intros the defect witness (sol, h_smooth, h_ne), applies h_ne, then calls parallel_transport_flat to obtain that all derivatives of sol.V vanish. It next invokes is_const_of_deriv_eq_zero on each component together with the initial-condition equality sol.V(0)=V_init to conclude sol.V(1)=sol.V(0), yielding the required contradiction.
why it matters in Recognition Science
The declaration supplies one direction of the holonomy-curvature equivalence (holonomy_vanishes_iff_flat) listed among the module's main results. It thereby anchors the geometric claim that curvature is precisely parallel-transport failure. Within Recognition Science this fits the forcing chain in which non-uniform J-cost produces curvature, with the eight-tick octave and D=3 emerging from the same ledger structure; the result closes the infinitesimal-loop side of that correspondence.
scope and limits
- Does not prove the converse that zero holonomy implies vanishing Riemann tensor.
- Does not treat non-Minkowski metrics or non-Levi-Civita connections.
- Does not quantify finite-size holonomy or higher-order curvature corrections.
- Does not address global topology or non-simply-connected spacetimes.
formal statement (Lean)
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. -/