SpacelikeGeodesic
plain-language theorem explainer
The structure for a spacelike geodesic defines a curve obeying the second-order geodesic equation under real Christoffel symbols together with the requirement that the metric quadratic form on its tangent vector remains strictly positive. Workers unifying Recognition Science metrics with general relativity would reference this when partitioning geodesics by interval signature. The declaration is realized as a direct structural extension of the real geodesic record by a single inequality predicate.
Claim. A spacelike geodesic relative to metric tensor $g$ consists of a path $x:ℝ→(Fin 4→ℝ)$ satisfying the geodesic equation $d²x^μ/dλ² + Γ^μ_{ρσ}(x) (dx^ρ/dλ)(dx^σ/dλ)=0$ for each component μ together with the condition that $g_{μν}(x(λ)) (dx^μ/dλ)(dx^ν/dλ)>0$ holds for every real parameter λ.
background
RealGeodesic supplies the base record: a path field together with the geodesic equation that inserts the Christoffel symbols taken from the Curvature module rather than any scaffold construction. MetricTensor is the local bilinear form interface appearing in Hamiltonian, Gravity.Connection and Meta.Homogenization, here specialized to four-dimensional index sets. The module itself derives the Minkowski metric η from the Recognition Science forcing chain (RCL to J-uniqueness to eight-tick octave to D=3) and proves its identity with the IndisputableMonolith stack so that all subsequent curvature and geodesic constructions operate on the same object.
proof idea
The declaration is a pure structure definition; it inherits the path and geodesic_equation fields verbatim from RealGeodesic and adjoins only the spacelike_condition predicate expressed as a double Finset sum of g contracted with the two velocity components.
why it matters
It supplies the missing spacelike case in the geodesic classification required once the RS-derived η is installed as the base metric. The module doc-comment states that this bridge lets all downstream GR theorems (Christoffel, Riemann, geodesics) run on the forcing-chain metric without duplication. No used-by edges appear yet, indicating the structure is placed for later use in interval-specific conservation laws or deviation equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.