TimelikeGeodesic
plain-language theorem explainer
A structure defining timelike geodesics on the RS-derived metric tensor. GR modelers working with particle worldlines in the unified spacetime would cite it to select negative-interval paths. The definition extends RealGeodesic by adjoining the explicit negative quadratic form condition on the four-velocity.
Claim. A timelike geodesic relative to metric tensor $g$ is a path $x:ℝ→ℝ^4$ obeying the geodesic equation with real Christoffel symbols of $g$ and satisfying $g_{μν}(x(λ))ẋ^μ(λ)ẋ^ν(λ)<0$ for every $λ$.
background
The module establishes equivalence between the Minkowski metric derived from the Recognition Science forcing chain and the standard metric tensor used in the IndisputableMonolith relativity stack. Key definitions include MetricTensor as a local bilinear form on spacetime indices, and RealGeodesic as a structure specifying a path satisfying the geodesic equation with Christoffel symbols from the curvature module. From the module doc the RS derivation proceeds from RCL through J-uniqueness (T5), eight-tick octave (T7), to D=3 yielding the diagonal metric η = diag(−1, +1, +1, +1). Upstream results provide the MetricTensor interface from Hamiltonian and Gravity modules.
proof idea
This is a structure definition that extends RealGeodesic by adjoining the timelike_condition predicate. The condition sums the metric components weighted by velocity products and requires the result to be negative, directly encoding the negative interval for timelike paths.
why it matters
This declaration supplies the timelike case for geodesic motion in the RS-unified metric, enabling application of GR results such as geodesic deviation to RS-derived spacetimes. It completes the bridge described in the module for downstream theorems on Christoffel symbols and curvature. It touches the T8 step fixing D=3 and the emergence of the Minkowski metric from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.