no_holonomy_if_flat
plain-language theorem explainer
In Minkowski spacetime, parallel transport of any initial vector around a closed loop returns exactly the initial value, so the holonomy defect is absent. General relativists and Recognition Science workers cite this when confirming that zero Riemann tensor produces no net rotation on closed paths. The tactic proof assumes a defect solution exists, invokes the flat-transport lemma to force constancy, then derives V(1) equals V(0) from vanishing derivatives and the initial condition.
Claim. Let $g$ be the Minkowski metric. For any closed loop (a curve with identified endpoints) and any initial vector $V_0$, every solution of the parallel-transport equation along the loop satisfies $V(1) = V_0$.
background
ClosedLoop is a spacetime curve whose path satisfies path(0) = path(1). HolonomyDefect(g, loop, V_init) asserts the existence of a ParallelTransportSolution whose vector field is smooth yet satisfies V(1) ≠ V_init. The module formalizes parallel transport via the Levi-Civita connection of the metric and states that, in Recognition Science, curvature arises from non-uniform J-cost defect density; parallel-transport failure around loops is the geometric signature of that imbalance. The key upstream lemma parallel_transport_flat asserts that, when the metric is Minkowski, every parallel-transported vector field is constant along the curve.
proof idea
Assume for contradiction that a HolonomyDefect exists, yielding a solution sol together with smoothness and V(1) ≠ V_init. Apply parallel_transport_flat to obtain that all derivatives of sol.V vanish. Use is_const_of_deriv_eq_zero on each component to conclude sol.V(1) = sol.V(0). The initial-condition field of the solution supplies sol.V(0) = V_init, producing the required equality and the contradiction.
why it matters
The result supplies the flat-space half of the holonomy-curvature correspondence stated in the module documentation. It confirms that Minkowski geometry (zero Riemann) produces no net defect, consistent with the Recognition Science claim that curvature requires non-uniform J-cost defects. No downstream theorems are recorded yet; the declaration closes one direction of the equivalence holonomy_vanishes_iff_flat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.