christoffel_symmetric
plain-language theorem explainer
Physicists deriving the Levi-Civita connection cite this result to confirm that Christoffel symbols are symmetric in the lower indices. The symmetry follows directly from the metric tensor's symmetry under index exchange. The proof reduces the equality via unfolding the definition, applying summation congruence, ring normalization, and a rewrite that invokes the metric's built-in symmetry.
Claim. For a metric tensor $g$, point $x : Fin 4 → ℝ$, and indices $ρ, μ, ν$, the Christoffel symbol satisfies $Γ^ρ_{μν}(x) = Γ^ρ_{νμ}(x)$.
background
The module derives Christoffel symbols from the metric tensor in four-dimensional spacetime. MetricTensor supplies a local bilinear form $g : (Fin 4 → ℝ) → (Fin 4 → ℝ) → (Fin 2 → Fin 4) → ℝ$. The upstream christoffel definition in Action.EulerLagrange gives the explicit one-dimensional Hessian case $Γ = -3/(2x)$, while the present declaration generalizes the torsion-free property to the four-index setting. The local theoretical setting is the extraction of curvature quantities from the metric in the relativity layer.
proof idea
The tactic proof unfolds the christoffel definition, applies congr 1 followed by Finset.sum_congr over the summation index lambda, normalizes the resulting expression with ring_nf, constructs an auxiliary hypothesis h_sym that swaps the mu and nu slots inside the metric function via g.symmetric, and finishes with a rewrite.
why it matters
This theorem supplies the torsion-free property required by Gravity.Connection.connection_cert and LeviCivitaTheorem.levi_civita_torsion_free. It feeds directly into RiemannSymmetries.christoffel_torsion_free and partialDeriv_christoffel_sym, closing the torsion-free step toward the Riemann tensor and Einstein tensor. The result realizes the torsion-free axiom in the Recognition Science derivation of the metric-compatible connection, consistent with the eight-tick octave and the forcing of spatial dimension D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.