spacelike_iff_superluminal
plain-language theorem explainer
The biconditional equating a positive spacetime interval to the spatial quadratic form exceeding the temporal one for any four-vector displacement is established in the emergence module. Researchers deriving causal structure from J-cost minimization would cite this when confirming the light-cone geometry. The proof rewrites the interval definition then dispatches both directions of the biconditional with linear arithmetic.
Claim. For a displacement $v : Fin 4 → ℝ$, $0 < interval(v) ↔ temporal_sq(v) < spatial_norm_sq(v)$, where $interval(v)$ is the spacetime interval $ds^2$, $temporal_sq(v)$ the squared time component, and $spatial_norm_sq(v)$ the sum of squared spatial components.
background
The Spacetime Emergence module derives the full 4D Lorentzian structure from the J-cost functional and the T0-T8 forcing chain. A Displacement is the abbrev Fin 4 → ℝ representing the four-vector (Δt, Δx₁, Δx₂, Δx₃). The interval function is the quadratic form whose sign distinguishes timelike, lightlike, and spacelike vectors; the module states that this form is forced to be spatial minus temporal, producing the signature (−,+,+,+).
proof idea
One-line wrapper that rewrites interval via interval_eq_spatial_minus_temporal, then applies constructor to split the biconditional and linarith to close both implications by arithmetic on the reals.
why it matters
This equivalence is invoked by the downstream theorem pure_spatial_is_spacelike to confirm that purely spatial displacements are spacelike. It completes the light-cone subsection of the central theorem that Lorentzian geometry, including the causal speed c=1 and the arrow of time, is forced by J-cost together with the eight-tick octave (T7) and D=3 spatial dimensions (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.