christoffel_from_metric
plain-language theorem explainer
The definition constructs the Levi-Civita Christoffel symbols in local coordinates from the inverse metric and partial derivatives of the metric components. Researchers formalizing general relativity within the Recognition Science gravity module cite it when deriving geodesic equations or torsion-free properties. It is realized as a direct structural definition that transcribes the classical summation formula without invoking additional lemmas.
Claim. $Gamma^rho_{mu nu} := (1/2) g^{rho sigma} (partial_mu g_{nu sigma} + partial_nu g_{mu sigma} - partial_sigma g_{mu nu})$, where $g^{rho sigma}$ denotes the inverse metric satisfying $g^{rho sigma} g_{sigma nu} = delta^rho_nu$ and $partial_mu g_{nu sigma}$ is the partial derivative of the metric component with respect to the mu-th coordinate.
background
The module works in a coordinate patch on 4-dimensional spacetime where the metric is a smooth matrix-valued function, bypassing the lack of abstract manifold connections in Mathlib. Key structures are the inverse metric (a symmetric bilinear form satisfying the delta contraction), the index set Idx as Fin 4, and ChristoffelData as the function returning the triple-indexed symbols. The local setting is the standard Levi-Civita connection expressed componentwise: Gamma^rho_{mu nu} equals one-half the inverse metric contracted against the combination of metric derivatives.
proof idea
The definition is a direct one-line implementation of the classical Christoffel formula, summing over the repeated index sigma with the inverse metric contracted against the symmetrized combination of metric derivatives.
why it matters
This supplies the coordinate expression for the connection that feeds the symmetry theorem christoffel_symmetric, the ConnectionCert structure, and the flat spacetime vanishing result. It is used downstream to construct null geodesics and to certify torsion-free properties. In the Recognition Science framework it bridges the metric to the covariant derivative in the gravity sector, consistent with the eight-tick octave while remaining in standard 4D spacetime coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.