fundamental_theorem_uniqueness
plain-language theorem explainer
The uniqueness half of the fundamental theorem of pseudo-Riemannian geometry asserts that any torsion-free metric-compatible connection on a pseudo-Riemannian manifold coincides with the Levi-Civita connection defined by the Christoffel symbols. General relativists and differential geometers cite this result when establishing the uniqueness of the covariant derivative compatible with the metric. The Lean proof is a one-line wrapper that invokes the lowered-connection uniqueness lemma.
Claim. For any metric tensor $g$, every torsion-free connection coefficients field $Γ$ that satisfies the lowered connection identity with $g$ at a point $x$ has lowered coefficients identical to the Christoffel symbols: lowered_connection$(Γ, g, x, ρ, μ, ν) = ½(∂_μ g_{ρν} + ∂_ν g_{ρμ} - ∂_ρ g_{μν})$.
background
The module proves the fundamental theorem of pseudo-Riemannian geometry on any pseudo-Riemannian manifold $(M, g)$: existence of a torsion-free metric-compatible connection together with its uniqueness. MetricTensor supplies the local bilinear form $g$; IsTorsionFree encodes vanishing torsion; LoweredConnectionIdentity equates the lowered connection coefficients to the indicated partial derivatives of metric components. The uniqueness statement is the third of the three listed claims in the module documentation, which also cites Wald Theorem 3.1.1 and do Carmo Theorem 2.3.
proof idea
Term-mode proof consisting of a single lambda that directly applies the sibling lemma connection_uniqueness_lowered to the supplied connection coefficients, evaluation point, torsion-freeness hypothesis, and lowered-identity hypothesis.
why it matters
This uniqueness result completes the fundamental theorem and is invoked inside levi_civita_certificate to produce the combined certificate. The certificate in turn feeds DiscreteBridge.bridge_certificate, which records the discrete-to-continuum bridge under the Regge hypothesis. The result therefore supplies the geometric uniqueness step required for the Recognition Science treatment of curvature and connection structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.