LoweredConnectionIdentity
plain-language theorem explainer
LoweredConnectionIdentity encodes the metric-compatibility condition on lowered Christoffel symbols for a connection in four-dimensional spacetime. General relativists cite it when verifying that a candidate connection satisfies ∇g = 0. The declaration is a direct packaging of the Wald coordinate identity as a reusable Prop for uniqueness arguments.
Claim. Let Γ be a connection and g a metric tensor at spacetime point x. Then Γ_{ρμν} + Γ_{νρμ} = ∂_μ g_{ρν} for all indices ρ, μ, ν.
background
ConnectionCoeffs is the type of maps assigning Christoffel symbols Γ^ρ_μν at each point of four-dimensional spacetime. MetricTensor supplies the components of the pseudo-Riemannian metric g_αβ. The lowered_connection operation contracts the upper index of Γ with g to obtain the fully covariant coefficients, while partialDeriv_v2 supplies the coordinate partial derivative ∂_μ.
proof idea
The declaration is a definition whose body is the single universal quantifier stating the required symmetry on the lowered coefficients. No lemmas are applied; the body directly transcribes the metric-compatibility identity.
why it matters
This definition supplies the hypothesis interface for connection_uniqueness_lowered and for the FundamentalTheoremUniqueness structure. Together they establish the uniqueness half of the Fundamental Theorem of Pseudo-Riemannian Geometry, showing that any torsion-free connection obeying the identity must reproduce the Christoffel symbols of Curvature.christoffel, as required by Wald Theorem 3.1.1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.