HolonomyDefect
plain-language theorem explainer
The holonomy defect predicate holds for a metric tensor, closed loop, and initial vector precisely when there exists a smooth parallel transport solution along the loop whose endpoint vector differs from the initial one. General relativists and Recognition Science researchers cite this when interpreting the Riemann tensor as the generator of holonomy around closed paths. The definition is realized directly by an existential quantifier over the parallel transport solution type.
Claim. The holonomy defect for metric tensor $g$, closed loop $l$, and initial vector $V_0$ is the proposition asserting existence of a parallel transport solution along the curve of $l$ starting at $V_0$ such that the vector field is smooth and its value at the endpoint differs from $V_0$.
background
The module formalizes parallel transport in 4D spacetime via the Levi-Civita connection. A closed loop is a spacetime curve with coinciding start and end points. The metric tensor supplies the inner product structure at each point. Parallel transport preserves the inner product along the curve but, in the presence of curvature, fails to return the original vector after a closed path. This failure is the holonomy defect, whose infinitesimal form is given by the Riemann tensor acting on the enclosed area element. The module notes that in Recognition Science this defect manifests the ledger imbalance from non-uniform J-cost defect density. Upstream results include the defect functional equal to J for positive arguments, and various metric tensor interfaces used across gravity and cosmology modules.
proof idea
The definition is a direct existential statement: there exists a parallel transport solution for the given metric and curve starting at the initial vector, such that the vector field is smooth and the endpoint value differs from the initial vector. No further lemmas are applied; it is the defining property.
why it matters
This definition is invoked by the theorem establishing that vanishing Riemann curvature implies no holonomy defect around any closed loop. It supplies the geometric content of the Riemann tensor as the source of parallel transport failure, consistent with the module's physical interpretation that curvature arises from J-cost defects. The declaration closes the link between the algebraic defect in the recognition ledger and the differential geometry of spacetime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.