flat_christoffel_vanish
plain-language theorem explainer
In Minkowski spacetime the Christoffel symbols derived from the inverse metric and zero metric derivatives are identically zero. General-relativity calculations in inertial frames rely on this reduction of the covariant derivative to the ordinary partial derivative. The proof proceeds by direct substitution of the explicit Minkowski inverse into the Christoffel formula followed by normalization.
Claim. For the Minkowski inverse metric with constant components and vanishing partial derivatives of the metric, the Christoffel symbols satisfy $Γ^ρ_{μν}=0$ for all indices $ρ,μ,ν∈{0,1,2,3}$.
background
The module works in local coordinates on a 4-dimensional spacetime patch where the metric is a smooth matrix-valued function. Idx is the finite index set Fin 4. The construction christoffel_from_metric assembles the symbols via the standard summation (1/2) g^{ρσ}(∂_μ g_νσ + ∂_ν g_μσ − ∂_σ g_μν) once an inverse metric and a derivative tensor are supplied. The Minkowski inverse is the explicit diagonal matrix with entries (−1,1,1,1).
proof idea
The proof is a direct term-mode simplification. After introducing the three indices, simp unfolds the definition of christoffel_from_metric and substitutes the concrete components of minkowski_inverse; norm_num then reduces the resulting arithmetic expression to zero.
why it matters
This supplies the flat-spacetime case required by the downstream connection_cert theorem, which packages both torsion-freeness and vanishing symbols into a single certificate. It confirms that the Levi-Civita connection reduces to the ordinary derivative when curvature vanishes, consistent with the Recognition Science flat-limit requirement before curvature or mass terms are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.