connection_uniqueness_lowered
plain-language theorem explainer
Any torsion-free metric-compatible connection on a 4D pseudo-Riemannian manifold has its lowered Christoffel symbols uniquely fixed by the metric via the Koszul formula. General relativists and differential geometers cite this when establishing the uniqueness half of the fundamental theorem. The proof takes three cyclic permutations of the lowered identity, symmetrizes via torsion-freeness, equates two derivative terms by metric symmetry, and solves the linear system by arithmetic.
Claim. Suppose a connection on 4-dimensional spacetime is torsion-free and satisfies the lowered identity that the sum of two lowered coefficients equals the partial derivative of the metric component at point $x$. Then the lowered coefficient equals one-half times the sum of the partial derivative with respect to the second index of the metric component with first and third indices, plus the partial with respect to the third index of the metric component with first and second indices, minus the partial with respect to the first index of the metric component with second and third indices.
background
A connection assigns coefficients at each spacetime point. Torsion-freeness requires symmetry in the last two indices. The lowered connection identity encodes metric compatibility by equating the sum of two lowered coefficients to the partial derivative of the corresponding metric component, as in Wald equation (3.1.18). This lemma sits inside the uniqueness direction of the Fundamental Theorem of Pseudo-Riemannian Geometry. The module proves torsion-freeness of the Christoffel symbols, metric compatibility, and uniqueness of any such connection on pseudo-Riemannian manifolds, citing Wald Theorem 3.1.1 and do Carmo Theorem 2.3. It draws on the metric tensor structure and partial derivative interface.
proof idea
The tactic proof introduces the three cyclic permutations of the lowered identity. It builds a symmetry lemma for the lowered coefficients from torsion-freeness and applies it to align terms across the three equations. Metric symmetry equates two partial derivative expressions. The linear combination of the three equations isolates twice the target coefficient, which linarith resolves directly.
why it matters
This uniqueness result supplies the unique direction for the bundled fundamental theorem uniqueness theorem. It completes the Fundamental Theorem of Pseudo-Riemannian Geometry in the module. Within the Recognition Science framework it fixes the canonical connection on the metric before curvature is defined in the relativity geometry layer, consistent with the eight-tick octave and spatial dimension three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.