equal_displacement_is_lightlike
plain-language theorem explainer
A four-vector with equal nonzero components in the temporal and one spatial slot has vanishing interval, hence is lightlike. Workers deriving Lorentzian structure from J-cost minimization cite this when confirming the light cone emerges without background assumptions. The proof is a one-line wrapper that rewrites via the spatial-minus-temporal identity then cancels algebraically with norm_num.
Claim. For any real number $a$, the spacetime interval of the displacement vector with components $(a,a,0,0)$ in the metric signature $(-,+,+,+)$ is zero: $-a^2 + a^2 = 0$.
background
The module derives 4D Lorentzian geometry from the J-cost functional and the T0–T8 forcing chain. The spacetime interval is defined as the quadratic form $interval(v) = sum_{i=0}^3 η_{ii} v_i^2$ with $η = diag(-1,1,1,1)$. An upstream lemma states that this equals the squared spatial norm minus the squared temporal component. The vector in question places equal amplitude $a$ on the temporal slot and the first spatial slot, with the remaining two spatial components zero.
proof idea
The proof applies the upstream identity interval = spatial_norm_sq minus temporal_sq. It then expands the three spatial squares and the single temporal square, yielding $a^2 + 0 + 0 - a^2$. The final norm_num tactic reduces the expression to zero.
why it matters
The result verifies that equal temporal and spatial displacements are null, a direct consequence of the metric signature forced by J-cost and the eight-tick octave (T7) together with D=3 spatial dimensions (T8). It sits inside the Spacetime Emergence derivation of the light cone, proper time, and Lorentz factor; the module doc-comment notes that every step is parameter-free. No downstream uses are recorded yet, but the lemma closes one concrete check on the emergent causal structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.