ChristoffelData
plain-language theorem explainer
ChristoffelData packages the three-index array of Levi-Civita connection coefficients Gamma^rho_mu nu in local coordinates on four-dimensional spacetime. Coordinate GR calculations cite it when the metric and its first derivatives are supplied to build the connection. The declaration is a direct record definition that stores the gamma function without invoking any lemmas or reductions.
Claim. A record holding the Christoffel symbols of the second kind as a map gamma from three indices in the set {0,1,2,3} to real numbers, where the components satisfy Gamma^rho_{mu nu} = (1/2) g^{rho sigma} (partial_mu g_{nu sigma} + partial_nu g_{mu sigma} - partial_sigma g_{mu nu}).
background
The module works in local coordinate patches on R^4, treating the metric as a smooth matrix-valued function to avoid the absence of abstract connections in the base library. Idx is the finite set Fin 4 indexing the four spacetime directions. MetricTensor is the symmetric nondegenerate bilinear form g_mu nu at each point, while InverseMetric supplies the raised-index components g^{rho sigma}.
proof idea
The declaration is a structure definition that directly introduces the gamma field as a three-argument function from Idx to real numbers. No tactics or upstream lemmas are applied; it functions as a plain data carrier for the two downstream constructions that populate and verify the symbols.
why it matters
It supplies the explicit connection data required by christoffel_from_metric, which assembles the symbols from the inverse metric and metric derivatives, and by metric_compatibility, which encodes the condition nabla g = 0. This places the Levi-Civita connection inside the Recognition Science gravity formalization, consistent with the eight-tick octave and the emergence of D = 3 spatial dimensions from the forcing chain. The structure closes the coordinate-level interface needed before curvature or geodesic results can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.