timelike_iff_subluminal
plain-language theorem explainer
The equivalence states that a spacetime displacement has negative interval precisely when its squared spatial separation is smaller than its squared temporal separation. Researchers deriving Lorentzian geometry from J-cost minimization cite this when confirming the causal light-cone structure. The proof is a direct algebraic substitution of the interval decomposition followed by linear arithmetic on the resulting inequality.
Claim. For a spacetime displacement $v$, the interval satisfies $ds^2(v) < 0$ if and only if the squared Euclidean norm of the spatial components is strictly less than the square of the temporal component.
background
The Spacetime Emergence module derives 4D Lorentzian geometry from the J-cost functional and the T0-T8 forcing chain. A Displacement is the 4-vector map Fin 4 → ℝ representing (Δt, Δx₁, Δx₂, Δx₃). The interval is the quadratic form ∑ η_{ii} v_i² with signature (−,+,+,+), which expands explicitly to spatial_norm_sq v − temporal_sq v. This decomposition is supplied by the upstream theorem interval_eq_spatial_minus_temporal, which unfolds the definitions, applies the metric values η_{00} = −1 and η_{ii} = +1 for i=1,2,3, and simplifies by ring arithmetic.
proof idea
The term proof first rewrites the left-hand side via interval_eq_spatial_minus_temporal. It then splits the biconditional with constructor and dispatches both directions with linarith on the resulting arithmetic statement.
why it matters
The result is invoked by pure_temporal_is_timelike to show that nonzero time-only displacements are timelike and by spacetime_emergence_cert to certify the full Lorentzian structure. It completes the causal classification step in the module's derivation chain: RCL → J-uniqueness (T5) → 8-tick octave (T7) + D=3 (T8) → metric signature (−,+,+,+) → light cone. No open scaffolding remains for this fragment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.