spacelike_iff_superluminal
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.
claimFor 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 in Recognition Science
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).
scope and limits
- Does not define interval, temporal_sq or spatial_norm_sq.
- Does not address curved or quantum-corrected metrics.
- Does not prove existence of superluminal displacements.
- Does not extend the equivalence beyond four dimensions.
Lean usage
rw [spacelike_iff_superluminal]formal statement (Lean)
212theorem spacelike_iff_superluminal (v : Displacement) :
213 0 < interval v ↔ temporal_sq v < spatial_norm_sq v := by
proof body
Term-mode proof.
214 rw [interval_eq_spatial_minus_temporal]; constructor <;> intro h <;> linarith
215
216/-! ## §6 Light Cone Structure -/
217
218/-- A purely temporal displacement is timelike. -/