christoffel_symmetric
plain-language theorem explainer
The declaration proves that Christoffel symbols computed from an inverse metric and its first partial derivatives are symmetric in the lower two indices whenever those derivatives inherit the symmetry of the metric tensor. Relativists working in local coordinates would cite the result to confirm that the Levi-Civita connection is torsion-free. The argument substitutes the explicit summation formula for the symbols, applies the derivative symmetry hypothesis four times inside the sum, and finishes by ring simplification.
Claim. Let $g^{ρσ}$ be the components of the inverse metric and let $∂_λ g_{μν}$ be the partial derivatives of the metric components. Assume $∂_μ g_{νσ} = ∂_μ g_{σν}$ for all indices. Then the Christoffel symbols defined by $Γ^ρ_{μν} = ½ g^{ρσ} (∂_μ g_{νσ} + ∂_ν g_{μσ} - ∂_σ g_{μν})$ satisfy $Γ^ρ_{μν} = Γ^ρ_{νμ}$ for all indices.
background
In the Gravity.Connection module spacetime indices are elements of Idx := Fin 4. InverseMetric is the structure holding a symmetric bilinear form ginv : Idx → Idx → ℝ that satisfies ginv μ ρ · g_{ρ ν} = δ^μ_ν. The function christoffel_from_metric assembles the symbols from ginv and the derivative tensor dg : Idx → Idx → Idx → ℝ whose components are the partial derivatives of the metric.
proof idea
The proof introduces the free indices rho, mu, nu, simplifies the definition of christoffel_from_metric, and reduces the equality to a summed expression by congruence. A Finset.sum_congr tactic isolates each summand sigma. Four rewrites with the hypothesis dg_metric_sym on the appropriate index pairs, followed by the ring tactic, establish the required cancellation.
why it matters
The result supplies the torsion_free field of the downstream connection_cert theorem that packages both symmetry of the Christoffel symbols and vanishing of the flat-space symbols. It is reused verbatim in the Levi-Civita theorem, RiemannSymmetries, and Curvature modules to establish that the metric-derived connection is torsion-free. Within the Recognition framework this step confirms the unique torsion-free, metric-compatible connection required for the Levi-Civita property in four-dimensional spacetime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.