lowered_connection
plain-language theorem explainer
lowered_connection defines the lowered Christoffel coefficients by contracting a general connection with the metric tensor at a spacetime point. It is referenced in uniqueness arguments for the Levi-Civita connection in pseudo-Riemannian geometry. The definition is realized as an explicit finite sum over the repeated index that lowers the first slot of the connection coefficients.
Claim. For a connection with coefficients $Γ^σ_{μν}$ and metric tensor $g_{ρσ}$, the lowered coefficients are given by $Γ_{ρμν}(x) = g_{ρσ}(x) Γ^σ_{μν}(x)$, where summation over $σ$ is understood.
background
The module establishes the Fundamental Theorem of Pseudo-Riemannian Geometry: on any pseudo-Riemannian 4-manifold there exists a unique torsion-free, metric-compatible connection whose coefficients are the Christoffel symbols. ConnectionCoeffs is the type of a general connection supplying components $Γ^ρ_{μν}$ at each point $x ∈ ℝ^4$. MetricTensor supplies the components of the metric $g_{μν}$ as a symmetric bilinear form. The lowered form converts the metric-compatibility condition into an algebraic relation on the lowered coefficients.
proof idea
The declaration is a direct definition. It evaluates the metric component $g_{ρσ}$ at $x$ via the supplied indexing convention and multiplies by the connection coefficient $Γ^σ_{μν}$, then sums over the dummy index $σ$ using Finset.univ.
why it matters
This definition supplies the lowered coefficients that appear in the uniqueness statement connection_uniqueness_lowered and the structure FundamentalTheoremUniqueness. Those results show that any torsion-free metric-compatible connection must reproduce the same lowered coefficients as the Christoffel connection, completing the uniqueness half of the fundamental theorem (Wald, Theorem 3.1.1). It directly implements the lowered identity $Γ_{ρμν} + Γ_{νρμ} = ∂μ g{ρν}$ used in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.