FundamentalTheoremUniqueness
plain-language theorem explainer
The uniqueness part of the fundamental theorem of pseudo-Riemannian geometry asserts that any torsion-free metric-compatible connection on a 4D spacetime with metric g has lowered Christoffel symbols given by the Koszul formula. Differential geometers and general relativists cite this to guarantee a unique Levi-Civita connection. The declaration is a structure definition whose single field encodes the explicit formula recovered from the lowered identity and torsion-freeness.
Claim. For a metric tensor $g$, any connection coefficients $Γ$ that are torsion-free and satisfy the lowered connection identity $Γ_{ρμν} + Γ_{νρμ} = ∂_μ g_{ρν}$ at each point $x$ obey $Γ_{ρμν} = ½(∂_μ g_{ρν} + ∂_ν g_{ρμ} - ∂_ρ g_{μν})$.
background
The module establishes the Fundamental Theorem of Pseudo-Riemannian Geometry on a pseudo-Riemannian manifold (M, g): there exists a unique torsion-free metric-compatible connection whose coefficients are the Christoffel symbols. ConnectionCoeffs is the type of connection coefficients Γ^ρ_μν on 4D spacetime. IsTorsionFree requires Γ^ρ_μν = Γ^ρ_νμ. LoweredConnectionIdentity encodes metric compatibility in lowered form as Γ_{ρμν} + Γ_{νρμ} = ∂μ g{ρν}, matching Wald equation (3.1.18). MetricTensor supplies the local bilinear form, while partialDeriv_v2 stands for the partial derivative operator.
proof idea
This is a structure definition that directly packages the uniqueness property. The containing theorem fundamental_theorem_uniqueness is a one-line wrapper that applies connection_uniqueness_lowered to the hypotheses IsTorsionFree and LoweredConnectionIdentity, recovering the explicit Koszul expression for the lowered coefficients.
why it matters
This uniqueness result completes the Fundamental Theorem alongside FundamentalTheoremExistence to form the LeviCivitaCertificate. It is invoked by DiscreteContinuumBridge to conclude that the coarse-graining limit of the J-cost lattice produces the Einstein equations. The module cites Wald Theorem 3.1.1 and do Carmo Theorem 2.3. In the Recognition Science setting it fixes the geometric connection for the metric arising from the phi-ladder in the relativity domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.