IsTorsionFree
plain-language theorem explainer
A connection on 4D spacetime is torsion-free when its coefficients are symmetric under interchange of the lower indices at every point. This predicate is required in statements of the fundamental theorem of pseudo-Riemannian geometry. The definition is a direct universal quantification over the symmetry condition on the coefficients.
Claim. A connection $Γ$ is torsion-free if $Γ^ρ_{μν}(x) = Γ^ρ_{νμ}(x)$ for all points $x$ and indices $ρ, μ, ν$.
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 of such a connection, represented as a map from points in Fin 4 to coefficients $Γ^ρ_{μν}$. The local setting quotes Wald Theorem 3.1.1 and do Carmo Theorem 2.3 for the classical statement. Upstream structures supply J-cost minimization and the emergence of exactly three spatial dimensions that constrain the geometry.
proof idea
The definition directly encodes the torsion-free condition as equality of the connection coefficients under swap of the final two indices.
why it matters
This definition supplies the torsion-free hypothesis for FundamentalTheoremExistence and FundamentalTheoremUniqueness, which together recover the Levi-Civita connection. It is used in the DiscreteContinuumBridge that derives the Einstein equations from J-cost lattice dynamics in the continuum limit. The predicate closes the torsion-free step in the Recognition Science derivation of general relativity from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.