FundamentalTheoremUniqueness
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove existence of a torsion-free metric-compatible connection.
- Does not specify the metric signature.
- Does not address global topology or curvature tensors.
- Does not extend beyond local coordinate charts on 4D spacetime.
formal statement (Lean)
187structure FundamentalTheoremUniqueness (g : MetricTensor) : Prop where
188 unique : ∀ (Γ : ConnectionCoeffs) (x : Fin 4 → ℝ),
189 IsTorsionFree Γ →
190 LoweredConnectionIdentity Γ g x →
191 ∀ ρ μ ν, lowered_connection Γ g x ρ μ ν =
192 (1/2 : ℝ) * (
193 partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then ρ else ν)) μ x +
194 partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then ρ else μ)) ν x -
195 partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then μ else ν)) ρ x)
196
197/-- The Fundamental Theorem holds for all metrics. -/