RealNullGeodesic
plain-language theorem explainer
The declaration introduces the structure RealNullGeodesic, which classifies a path as a null geodesic when it obeys the real geodesic equation and the metric quadratic form vanishes on its tangent vector. Researchers deriving general relativity from the Recognition Science forcing chain would cite it when treating light-like trajectories. The definition is a direct extension of RealGeodesic that adds the null condition as a field.
Claim. Let $g$ be a metric tensor. A null geodesic is a path $x:ℝ→ℝ^4$ satisfying the geodesic equation with the real Christoffel symbols of $g$ and obeying $g_{μν}(x(λ)) (dx^μ/dλ)(dx^ν/dλ)=0$ for all $λ∈ℝ$.
background
The module unifies the Recognition Science Minkowski metric, obtained from the forcing chain RCL through J-uniqueness (T5), phi fixed point (T6), eight-tick octave (T7) and D=3 (T8), with the IndisputableMonolith MetricTensor. MetricTensor supplies the local bilinear form interface appearing in Hamiltonian, Gravity.Connection and Meta.Homogenization. RealGeodesic supplies the base structure whose path obeys the geodesic equation using real Christoffel symbols from Curvature.christoffel.
proof idea
The declaration is a structure definition that extends RealGeodesic by adding the null_condition field encoding the vanishing of the quadratic form along the path.
why it matters
This structure completes the set of geodesic types in the metric unification module, enabling consistent treatment of null paths in the RS-derived metric. It supports the module goal of allowing all downstream GR theorems on Christoffel symbols, Riemann tensor and Einstein equations to operate on the unified η without duplication. The definition aligns with T8 spatial dimensions and the eight-tick temporal structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.