HolonomyDefect
HolonomyDefect asserts existence of a parallel transport solution along a closed loop whose smooth vector field returns a value different from the initial vector, encoding curvature via the Riemann tensor. General relativists and Recognition Science researchers cite it when linking holonomy failure to non-uniform J-cost defect density. The definition is a direct existential predicate over ParallelTransportSolution with smoothness and inequality conditions.
claimFor 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 starting at $V_0$ such that the transported vector field is smooth yet differs from $V_0$ at the endpoint.
background
The module formalizes parallel transport on 4D spacetime via the Levi-Civita connection from the metric. ClosedLoop extends SpacetimeCurve by the condition that the path satisfies path 0 = path 1. MetricTensor supplies the local symmetric bilinear form used to define the connection and inner products. Upstream, defect from LawOfExistence equals the J functional, while V from InflatonPotentialFromJCost gives the potential on the recognition manifold as J(1 + phi_inf). The module doc states that curvature arises from non-uniform J-cost defect density and that parallel transport failure manifests ledger imbalance.
proof idea
This is a definition that directly encodes the existential claim: there exists a ParallelTransportSolution for the supplied metric and loop starting from the initial vector, conjoined with the requirements that the solution's vector field is smooth and that its value at parameter 1 differs from the initial vector. No lemmas are applied; the body is the predicate itself.
why it matters in Recognition Science
The definition supplies the predicate used by the downstream theorem no_holonomy_if_flat, which proves that vanishing Riemann curvature implies no holonomy defect on any closed loop. It supplies the geometric interpretation step in the parallel transport module, where the doc-comment identifies the defect with the Riemann tensor action on an infinitesimal area. In the Recognition Science framework this corresponds to the emergence of curvature from J-cost defect density, consistent with the eight-tick octave and D=3 spatial dimensions forced earlier in the chain.
scope and limits
- Does not compute an explicit numerical value for the defect.
- Does not restrict the metric tensor to Minkowski or any fixed signature.
- Does not address finite-size loops beyond the infinitesimal Riemann limit.
- Does not derive the connection coefficients or Christoffel symbols.
formal statement (Lean)
187def HolonomyDefect (g : MetricTensor) (loop : ClosedLoop) (V_init : Fin 4 → ℝ) : Prop :=
proof body
Definition body.
188 ∃ (sol : ParallelTransportSolution g loop.toSpacetimeCurve ⟨0, V_init⟩),
189 SmoothField sol.V ∧ sol.V 1 ≠ V_init
190
191/-- Vanishing Riemann implies zero holonomy: no defect around any closed loop. -/