LoweredConnectionIdentity
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.
claimLet Γ 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 in Recognition Science
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.
scope and limits
- Does not prove existence of a torsion-free metric-compatible connection.
- Does not incorporate the torsion-free condition IsTorsionFree.
- Does not derive the explicit Koszul formula for the coefficients.
- Does not extend the identity beyond the four-dimensional coordinate chart.
formal statement (Lean)
128def LoweredConnectionIdentity (Γ : ConnectionCoeffs) (g : MetricTensor)
129 (x : Fin 4 → ℝ) : Prop :=
proof body
Definition body.
130 ∀ ρ μ ν,
131 lowered_connection Γ g x ρ μ ν + lowered_connection Γ g x ν ρ μ =
132 partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then ρ else ν)) μ x
133
134/-- Uniqueness: any torsion-free, metric-compatible connection has lowered coefficients
135 uniquely determined by the metric. The Koszul formula gives:
136
137 Γ_{ρμν} = (1/2)(∂_μ g_{ρν} + ∂_ν g_{ρμ} - ∂_ρ g_{μν})
138
139 which, after raising the index with g^{ρσ}, yields `Curvature.christoffel`. -/