christoffel_torsion_free
plain-language theorem explainer
The declaration establishes symmetry of Christoffel symbols in the lower indices for any metric tensor, confirming the torsion-free Levi-Civita connection. Researchers constructing discrete-to-continuum bridges cite it to match lattice connections to standard general relativity. The proof is a direct one-line application of the upstream symmetry result for metric-derived Christoffel symbols.
Claim. Let $g$ be a metric tensor. For any point $x : Fin 4 → ℝ$ and indices $ρ, μ, ν$, the Christoffel symbol satisfies $Γ^ρ_{μν}(x) = Γ^ρ_{νμ}(x)$.
background
The RiemannSymmetries module derives algebraic properties of the Riemann tensor from Christoffel symbols of the metric. MetricTensor supplies a local symmetric bilinear form on four-dimensional spacetime. Christoffel symbols are the standard connection coefficients built from metric derivatives, as defined in the imported Connection module.
proof idea
The proof is a one-line wrapper that applies the upstream theorem christoffel_symmetric, which encodes symmetry of the lower indices because metric derivatives are symmetric under interchange of the last two slots.
why it matters
This supplies the torsion-free property required by DiscreteContinuumBridge, which packages the certificate that N → ∞ J-cost lattice sites yield the Einstein equations under coarse-graining. It fills the classical Levi-Civita step referenced to Wald and MTW, closing one link from the Recognition Composition Law to geometric symmetries in the relativity sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.