ConnectionCoeffs
ConnectionCoeffs supplies the function type for Christoffel symbols Γ^ρ_μν(x) on 4D spacetime. Researchers stating the Fundamental Theorem of pseudo-Riemannian geometry cite this type when quantifying torsion-free or metric-compatible connections. The declaration is a direct type abbreviation with no further computation or proof obligations.
claimA connection on 4-dimensional spacetime is a map assigning to each point $x : Fin 4 → ℝ$ and index triple $ρ,μ,ν$ the real coefficient $Γ^ρ_{μν}(x)$.
background
The module proves the Fundamental Theorem of Pseudo-Riemannian Geometry: on any pseudo-Riemannian manifold (M, g) there exists a unique torsion-free, metric-compatible connection ∇ whose coefficients are the Christoffel symbols. ConnectionCoeffs is the type used to represent these coefficients Γ^ρ_μν at each point x in ℝ^4. The module doc states: 'On any pseudo-Riemannian manifold (M, g) there exists a unique torsion-free, metric-compatible connection ∇. Its coefficients are the Christoffel symbols Γ^ρ_μν defined in Curvature.lean.' Sibling definitions introduce IsTorsionFree (Γ^ρ_μν = Γ^ρ_νμ) and IsMetricCompatible (covariant derivative of g vanishes). Upstream imports supply the 4D index set and partial derivative operators from the Calculus and Tensor modules.
proof idea
This is a one-line type abbreviation that directly names the space of all possible connection coefficient functions on 4D spacetime.
why it matters in Recognition Science
The definition anchors the uniqueness and existence statements that follow in the same module. It is used by connection_uniqueness_lowered, FundamentalTheoremUniqueness, IsTorsionFree, IsMetricCompatible, and lowered_connection. These establish that any torsion-free metric-compatible connection equals the Christoffel connection, matching Wald Theorem 3.1.1. In the Recognition Science setting the 4D index set is consistent with T8 (D = 3 spatial dimensions) and the eight-tick octave. No open scaffolding questions are attached to this declaration.
scope and limits
- Does not impose torsion-freeness or metric compatibility on the coefficients.
- Does not encode the explicit Koszul formula for Christoffel symbols.
- Does not define covariant derivatives or curvature tensors.
- Does not restrict the metric signature to Lorentzian (1,3).
formal statement (Lean)
40abbrev ConnectionCoeffs := (Fin 4 → ℝ) → Fin 4 → Fin 4 → Fin 4 → ℝ
proof body
Definition body.
41
42/-- A connection is torsion-free iff Γ^ρ_μν = Γ^ρ_νμ. -/