geodesic_uses_real_christoffel
plain-language theorem explainer
RealGeodesic structures satisfy the standard geodesic equation using Christoffel symbols derived from the metric tensor itself. Physicists bridging Recognition Science to general relativity cite this to ensure consistency with classical GR on the RS-derived Minkowski metric. The proof consists of a single application of the geodesic_equation axiom in the RealGeodesic definition.
Claim. For a metric tensor $g$ and a real geodesic $geo$ in $g$, at any affine parameter $lam$ and coordinate index $mu$, the second derivative of the path component plus the double sum over Christoffel symbols times the two velocity components equals zero.
background
MetricTensor supplies the local bilinear form interface for the relativity stack. RealGeodesic is the structure whose geodesic_equation field encodes the second-order ODE with Christoffel symbols taken from Curvature.christoffel. The module unifies the RS-derived eta metric (obtained via the forcing chain RCL to J-uniqueness at T5, eight-tick octave at T7, and D=3 at T8) with the IndisputableMonolith Minkowski tensor so that standard GR operators apply directly without duplication.
proof idea
The proof is a one-line wrapper that directly invokes the geodesic_equation field of the RealGeodesic structure at the supplied lam and mu.
why it matters
This declaration confirms that geodesics in the unified metric employ the physical Christoffel symbols rather than any scaffold version. It supports the module's bridge from the forcing chain (T5 through T8) to classical GR structures, enabling downstream results on Riemann curvature and Einstein equations to operate on the RS eta. No open questions are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.