pure_spatial_is_spacelike
plain-language theorem explainer
A nonzero four-vector with support only in one spatial direction has positive Lorentzian interval and is therefore spacelike. Researchers verifying the emergence of Lorentzian geometry from the J-cost functional and the T0-T8 chain would cite this when confirming the positive-definite spatial metric. The proof is a direct algebraic reduction that rewrites interval positivity via the superluminal equivalence and applies the positivity of squares of nonzero reals.
Claim. For any nonzero real number $x$, the four-vector $v$ with components $(0,x,0,0)$ satisfies $0 < I(v)$, where $I(v) = v_1^2 + v_2^2 + v_3^2 - v_0^2$ is the Lorentzian interval, so $v$ is spacelike.
background
The SpacetimeEmergence module derives 4D Lorentzian spacetime with signature $(- , + , + , +)$ from the J-cost functional via the forcing chain T0-T8. The interval function encodes the associated quadratic form on vectors indexed by Fin 4, with index 0 temporal and indices 1-3 spatial. The module states that the full structure (light cone, Lorentz factor, arrow of time) is forced by J-uniqueness, the eight-tick octave, and D=3 spatial dimensions. Upstream results supply the active-edge count A and collision-free structures used to anchor the cost accounting, but the immediate prior fact is the equivalence relating interval positivity to the superluminal inequality.
proof idea
The proof rewrites the goal with the equivalence that converts interval positivity into the strict inequality between the squared temporal component and the sum of squared spatial components. Specializing the vector to zero time component and value $x$ in the first spatial slot, norm_num reduces the inequality to $0 < x^2$. The final step applies the lemma that the square of any nonzero real is positive.
why it matters
This result confirms the positive-definite spatial metric required by the central theorem of the module: Lorentzian spacetime is forced by J-cost minimization with no free parameters. It aligns with the derivation RCL to J''(1)=1 for spatial directions plus the eight-tick temporal operator and D=3 from T8, yielding diag(-1,+1,+1,+1). Although no downstream theorems depend on it in the current graph, it closes part of the verification that pure spatial displacements lie outside the light cone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.