minkowski_real_christoffel_zero
plain-language theorem explainer
Minkowski spacetime has vanishing Christoffel symbols under the standard metric tensor. This fact is invoked when deriving straight-line geodesics and when confirming that the zero-valued scaffold matches the real curvature computation. The proof is a one-line wrapper that directly applies the proper vanishing theorem from the Curvature module.
Claim. For the Minkowski metric tensor, the Christoffel symbols vanish identically: for every point $x : Fin 4 → ℝ$ and indices $ρ, μ, ν : Fin 4$, the connection coefficient $Γ^ρ_{μν}(x)$ computed from the metric equals zero.
background
The module unifies the Recognition Science-derived Minkowski metric (obtained from the forcing chain RCL → T5 J-uniqueness → T7 eight-tick octave → T8 D=3) with the standard MetricTensor used in the relativity stack. The Christoffel symbol is the standard connection coefficient obtained from the metric and its first partial derivatives; the Minkowski tensor is the diagonal form diag(−1, +1, +1, +1). The upstream result minkowski_christoffel_zero_proper in Curvature already establishes the vanishing by unfolding the definitions and simplifying with the fact that all metric derivatives are zero.
proof idea
One-line wrapper that applies the theorem minkowski_christoffel_zero_proper from the Curvature module. That theorem unfolds christoffel and minkowski_tensor, then invokes dsimp followed by simp using eta_deriv_zero to reduce every term to zero.
why it matters
The result is used by minkowski_straight_line_geodesic (which constructs straight-line paths as geodesics under the real Christoffel symbols) and by scaffold_agrees_on_minkowski (which confirms the old zero scaffold matches the computed curvature). It completes the bridge from the RS forcing chain landmarks (T5, T7, T8 yielding η) to downstream GR theorems that now operate on the RS-derived metric without duplication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.