no_holonomy_if_flat
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.