RealGeodesic
plain-language theorem explainer
RealGeodesic packages a curve whose second derivatives satisfy the geodesic equation built from the real Christoffel symbols of a given MetricTensor. Researchers extending the RS-derived Minkowski metric into general relativity cite it to guarantee that all subsequent geodesic structures inherit the physically correct connection. The declaration is a direct structure definition that records the path function together with the component-wise differential equation.
Claim. A curve $x:ℝ→ℝ^4$ is a RealGeodesic for metric $g$ when, for every parameter value $λ$ and index $μ$, the second derivative satisfies $d²x^μ/dλ² + Γ^μ_{ρσ}(x(λ)) (dx^ρ/dλ)(dx^σ/dλ) = 0$, where the Christoffel symbols $Γ$ are those supplied by the real curvature module applied to $g$.
background
MetricTensor supplies a local bilinear form on 4D index space; several sibling modules define variants, all of which are treated as symmetric (0,2) tensors in the unification layer. The christoffel function imported from Curvature computes the standard connection coefficients for any such metric. Module MetricUnification establishes that the RS forcing chain (RCL through T5–T8) produces the same η = diag(−1,+1,+1,+1) that the IndisputableMonolith relativity stack already uses, thereby allowing all downstream GR objects to operate on the RS metric without duplication.
proof idea
This is a structure definition; it simply records the two fields (path and the geodesic_equation predicate) with no further reduction or tactic steps.
why it matters
RealGeodesic is the common base extended by TimelikeGeodesic, SpacelikeGeodesic and RealNullGeodesic, and is invoked by geodesic_uses_real_christoffel and minkowski_straight_line_geodesic. It therefore closes the bridge stated in the module doc-comment: once rs_minkowski is shown equal to the canonical Minkowski tensor, every geodesic theorem downstream inherits the RS-derived η without re-deriving the connection. The declaration touches the T7–T8 segment of the forcing chain by ensuring the eight-tick temporal structure and D=3 spatial dimensions are respected in the geodesic equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.