interval_eq_spatial_minus_temporal
The theorem states that the spacetime interval for any 4-vector displacement equals the squared spatial norm minus the squared temporal component under metric signature (−,+,+,+). Researchers deriving emergent Lorentzian geometry from J-cost minimization would cite this when classifying causal structure. The proof is a direct algebraic reduction that unfolds the three quadratic definitions and applies the explicit diagonal metric values.
claimFor a displacement $v = (v_0, v_1, v_2, v_3)$ the spacetime interval satisfies $I(v) = v_1^2 + v_2^2 + v_3^2 - v_0^2$, where $I(v) = -v_0^2 + v_1^2 + v_2^2 + v_3^2$.
background
The Spacetime Emergence module derives 4D Lorentzian geometry from the J-cost functional and forcing chain T0–T8. A Displacement is the 4-vector abbrev Fin 4 → ℝ with index 0 temporal and indices 1–3 spatial. The interval is the quadratic form ∑ η_ii v_i² with η = diag(−1, +1, +1, +1). Spatial norm squared isolates the three spatial components while temporal squared isolates the time component. The module states: “The complete structure of 4D Lorentzian spacetime — metric signature (−,+,+,+), causal light-cone, Lorentz factor, arrow of time — is FORCED by the J-cost functional and the forcing chain T0–T8.” Upstream definitions supply the three quadratic forms used in the identity.
proof idea
The term proof unfolds interval, spatial_norm_sq and temporal_sq, then applies simp over the Fin 4 sum. It rewrites the four diagonal metric entries η_00 = −1, η_11 = η_22 = η_33 = +1 and finishes with the ring tactic to obtain the algebraic identity.
why it matters in Recognition Science
This identity supplies the explicit Minkowski form required by the downstream light-cone theorems (lightlike_iff_speed_c, timelike_iff_subluminal, spacelike_iff_superluminal, equal_displacement_is_lightlike, proper_time_sq_eq_neg_interval). It realizes the metric signature forced by J''(1) = 1 for spatial directions and the 8-tick operator for the temporal direction, completing the chain RCL → T5–T8 → η = diag(−1, +1, +1, +1) inside the Recognition framework.
scope and limits
- Does not derive the metric components η from the J-cost; those are supplied upstream.
- Does not extend to curved spacetimes or general relativity.
- Does not address quantum corrections or higher-dimensional cases.
- Does not prove uniqueness of the signature; it assumes the forced diagonal values.
Lean usage
rw [interval_eq_spatial_minus_temporal]formal statement (Lean)
195theorem interval_eq_spatial_minus_temporal (v : Displacement) :
196 interval v = spatial_norm_sq v - temporal_sq v := by
proof body
Term-mode proof.
197 unfold interval spatial_norm_sq temporal_sq
198 simp only [Fin.sum_univ_four]
199 rw [η_00, η_11, η_22, η_33]; ring
200
201/-- **Light cone condition**: ds² = 0 iff |Δx|² = (Δt)². -/