HolonomyCurvatureCorrespondence
plain-language theorem explainer
The HolonomyCurvatureCorrespondence encodes the leading-order defect in parallel transport of a vector around an infinitesimal parallelogram as the Riemann tensor contracted with the vector and the area bivector. A relativist deriving curvature from transport failure in Recognition Science would cite this when linking the geometric Riemann tensor to the J-cost ledger imbalance. The definition directly equates the summed defect to the standard contraction without invoking additional lemmas.
Claim. For a metric tensor $g$, the correspondence holds when, for every point $x_0$, vector $V_0$, displacements $δx$ and $δy$, and index $ρ$, there exists a real defect equal to the sum over $σ,μ,ν$ of the Riemann component $R^ρ_{σμν}(g,x_0)$ times $V_0^σ δx^μ δy^ν$.
background
Parallel transport along curves uses the Levi-Civita connection from the metric to move vectors while preserving inner products. The module works in 4D spacetime, where closed-loop failure of transport defines curvature via the Riemann tensor. Upstream, MetricTensor supplies the local bilinear form on Fin 4 indices, while riemann_tensor computes the curvature from Christoffel symbols and derivatives as $R^ρ_{σμν} = ∂μ Γ^ρ{νσ} - ∂ν Γ^ρ{μσ} + Γ$ terms.
proof idea
This is a definition that directly encodes the infinitesimal holonomy identity. It applies the riemann_tensor function at $x_0$ with the supplied index selector, then contracts against $V_0$, $δx$, and $δy$ via the triple sum over Fin 4 indices.
why it matters
The definition supplies the geometric content that curvature equals parallel-transport failure around loops, matching the module's physical interpretation and the Recognition Science forcing of curvature from non-uniform defect density. It fills the step from the Riemann tensor (upstream in Gravity.RiemannTensor and Relativity.Geometry.Curvature) to holonomy statements, though no downstream theorems yet consume it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.