minkowski_straight_line_geodesic
plain-language theorem explainer
Straight lines satisfy the geodesic equation in Minkowski spacetime when equipped with the real Christoffel symbols. Researchers unifying Recognition Science derivations with standard relativity would cite this to confirm inertial trajectories remain geodesics under the RS-derived metric. The proof proceeds by explicit construction of the linear path followed by direct verification that the equation holds once Christoffel symbols vanish.
Claim. In Minkowski spacetime with metric tensor $η$, for any initial position $x_0$ and four-velocity $v$ in $ℝ^4$, there exists a geodesic $γ$ such that $γ(λ)^μ = x_0^μ + λ v^μ$ for all $λ ∈ ℝ$ and $μ ∈ {0,1,2,3}$.
background
This module unifies the Recognition Science-derived Minkowski metric (from the forcing chain RCL → T5 J-uniqueness → T7 eight-tick octave → T8 D=3 yielding η = diag(−1,+1,+1,+1)) with the IndisputableMonolith relativity stack's Geometry.eta and minkowski_tensor. RealGeodesic is the structure whose path is a map ℝ → (Fin 4 → ℝ) and whose geodesic_equation requires the second derivative plus the double sum over Christoffel symbols contracted with first derivatives to vanish. Upstream results include the definition of minkowski_tensor as the eta matrix and the theorem minkowski_real_christoffel_zero establishing that all real Christoffel symbols on this metric are identically zero.
proof idea
The proof is a term-mode construction that refines a RealGeodesic record whose path is the explicit affine map λ ↦ x₀ + λv. The geodesic_equation obligation is discharged by simp using minkowski_real_christoffel_zero, which replaces the Christoffel sum by zero and leaves only the second derivative (itself zero for linear paths). The path-equality obligation is discharged by reflexivity.
why it matters
This theorem anchors the geodesic sector of the metric unification, confirming that the RS-derived Minkowski metric reproduces the expected flat-spacetime geodesics. It supports the bridge to GR theorems on Christoffel symbols, Riemann curvature, and Einstein equations as described in the module documentation. No downstream uses are recorded yet, but the result closes the consistency check for inertial motion within the unified RS-to-GR framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.