minkowski_christoffel_zero_proper
plain-language theorem explainer
The Minkowski metric has vanishing Christoffel symbols at every point and for every index combination. Workers on flat-spacetime limits, discrete bridges, or parallel transport in Recognition Science cite the result to close curvature calculations. The proof is a term-mode reduction that unfolds the general Christoffel definition, substitutes the constant Minkowski tensor, and applies the derivative-vanishing lemma together with arithmetic zero rules to obtain the zero expression.
Claim. For the Minkowski metric tensor $eta$, the Christoffel symbol $Gamma^rho_{mu nu}(x)$ equals zero for every spacetime point $x in R^4$ and every index triple $rho, mu, nu in {0,1,2,3}$.
background
Christoffel symbols are obtained from the standard formula that contracts the inverse metric with first partial derivatives of the metric components. The module supplies the four-dimensional version as a sum over an auxiliary index of the inverse metric times the combination of two positive and one negative partial derivative. The Minkowski tensor is introduced as the constant diagonal metric with signature (+,-,-,-). Its partial derivatives are identically zero by the upstream lemma eta_deriv_zero, which applies the constant-function derivative rule after unfolding the metric definition. Basic arithmetic facts (addition by zero and multiplication by zero) are imported to clear remaining terms.
proof idea
The term proof unfolds the Christoffel definition and the Minkowski tensor, then applies dsimp followed by simp using eta_deriv_zero to replace every derivative by zero. The arithmetic lemmas add_zero and mul_zero together with the constant-zero sum rule finish the reduction to the literal zero value.
why it matters
The result is invoked directly by minkowski_riemann_zero to establish that the Riemann tensor vanishes on Minkowski space, by flat_chain_holds to assemble the complete flat-curvature package, and by parallel_transport_flat to conclude that vectors are constant along curves. It also supplies the concrete instance used in MetricUnification to equate the scaffolded zero Christoffel with the real definition. Within the Recognition framework the vanishing confirms that the flat metric (the base case of the forcing chain) carries no curvature, consistent with the eight-tick octave and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.