HolonomyDefect
plain-language theorem explainer
HolonomyDefect asserts existence of a smooth parallel transport solution along a closed loop whose endpoint vector differs from the initial vector. Curvature modelers in general relativity cite it to connect Riemann curvature to observable vector rotation after transport. The definition is introduced directly as an existential predicate over ParallelTransportSolution instances satisfying the endpoint mismatch.
Claim. For metric tensor $g$, closed loop $C$, and initial vector $V_0$, the holonomy defect holds when there exists a parallel transport solution along the curve of $C$ starting at $V_0$ such that the transported vector field is smooth and its value at parameter 1 differs from $V_0$.
background
ClosedLoop is a spacetime curve parameterized on $[0,1]$ with endpoints identified. MetricTensor supplies the local symmetric bilinear form used to define the Levi-Civita connection. ParallelTransportSolution encodes solutions of the first-order transport ODE along the curve with the given initial vector at parameter 0. SmoothField requires the transported components to be differentiable. The module sets parallel transport in 4D spacetime via the Christoffel symbols of Curvature.christoffel and interprets failure around loops as the geometric signature of non-uniform J-cost defect density. Upstream MetricTensor structures appear in Gravity.Connection, Foundation.Hamiltonian, and Meta.Homogenization; the defect functional from LawOfExistence equals J for positive arguments.
proof idea
Direct definition expressing the holonomy defect via existential quantification over ParallelTransportSolution with added smoothness and inequality conditions on the endpoint value.
why it matters
The definition supplies the predicate used by the downstream theorem no_holonomy_if_flat, which proves vanishing Riemann curvature implies no holonomy defect. It encodes the module doc-comment statement that the defect satisfies $δV^ρ = R^ρ_{σμν} V^σ δA^{μν}$ and thereby links curvature to the Recognition Science claim that curvature is forced by non-uniform J-cost defect density. It touches the open question of how defect inhomogeneities source the gravitational field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.