partialDeriv_christoffel_sym
plain-language theorem explainer
Partial derivatives of Christoffel symbols with respect to any coordinate commute with interchange of the final two indices. Curvature calculations in general relativity cite this helper when expanding the Riemann tensor definition. The term proof reduces the claim to the pointwise symmetry of the Christoffel symbols by congruence and function extensionality.
Claim. For a metric tensor $g$, point $x : Fin 4 → ℝ$, and indices $a,b,c,d : Fin 4$, the partial derivative $∂_d Γ^a_{bc}(x)$ equals $∂_d Γ^a_{cb}(x)$, where $Γ$ denotes the Christoffel symbols of $g$.
background
The module proves symmetry properties of the Riemann curvature tensor built from Christoffel symbols. MetricTensor supplies the local non-sealed bilinear form on $Fin 4$. partialDeriv_v2 provides the placeholder partial derivative operator. christoffel computes the connection coefficients from the metric. The local setting is the standard derivation of Riemann symmetries in general relativity, with references to Wald Eq. (3.2.14) and MTW Chapter 13.
proof idea
Term-mode proof. congr 1 matches the outer equality structure. funext reduces to pointwise equality of the functions. The final step applies the Christoffel symmetry lemma directly.
why it matters
This helper is invoked by the first Bianchi identity theorem in the same module, which states the cyclic sum of the Riemann tensor vanishes. It supports the algebraic derivation of pair-exchange symmetry for the Riemann tensor, consistent with the torsion-free Levi-Civita connection used throughout the Recognition Science geometry layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.