interval_eq_spatial_minus_temporal
plain-language theorem explainer
The equality states that the spacetime interval for any 4-vector displacement equals the squared spatial norm minus the squared temporal component under the (−,+,+,+) metric. Researchers deriving causal structure from J-cost minimization would reference this identity to connect interval signs to speed regimes. The proof proceeds by direct expansion of the summed metric terms followed by algebraic simplification.
Claim. For a displacement 4-vector $v = (Δt, Δx_1, Δx_2, Δx_3)$, the spacetime interval satisfies interval$(v) = |Δx|^2 - (Δt)^2$, where interval is the quadratic form with metric diag(−1, +1, +1, +1).
background
In the Spacetime Emergence module, spacetime geometry is derived from the J-cost functional via the forcing chain T0–T8. Displacement denotes a 4-vector in Fin 4 → ℝ. The interval is defined as ∑{i:Fin 4} η{ii} v_i². spatial_norm_sq sums the three spatial components squared, while temporal_sq isolates the time component squared. The module establishes that the Lorentzian signature (−,+,+,+) emerges from J''(1)=1 for space and the 8-tick operator for time. This identity is the explicit translation of that signature into component form.
proof idea
The proof unfolds the three definitions, applies the sum over four indices, substitutes the metric values η_00 = −1 and η_11=η_22=η_33=+1, then simplifies the resulting expression by ring.
why it matters
This identity underpins the light-cone theorems in the same module, including lightlike_iff_speed_c and timelike_iff_subluminal, which classify displacements by whether interval is zero, negative, or positive. It fills the step from the forced metric η = diag(−1,+1,+1,+1) in the derivation chain RCL → J unique (T5) → ... → η to the explicit interval formula. The result supports the claim that spacetime structure, including the arrow of time, follows from cost minimization without background assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.