spacelike_iff
plain-language theorem explainer
Spacelike separation on ℝ^{1,3} is exactly the region outside the light cone: the spatial quadratic form strictly exceeds t². Anyone working the continuum bridge from ledger sites to Lorentzian geometry cites this as the coordinate form of the spacelike predicate. The proof unfolds the Minkowski form and closes both directions by linear arithmetic.
Claim. For all real $t,x,y,z$, the event $(t,x,y,z)$ is spacelike if and only if $t^2 < x^2 + y^2 + z^2$. Equivalently, the Minkowski quadratic form $s^2 = -t^2 + x^2 + y^2 + z^2$ is strictly positive precisely when the spatial part dominates the temporal part.
background
This module builds the zero-parameter bridge from discrete Recognition Science ledger sites to a Lorentzian continuum. The architecture starts from the Minkowski quadratic form on $\mathbb{R}^{1,3}$,
$$s^2(t,x,y,z) = -t^2 + x^2 + y^2 + z^2,$$
and derives signature, causal trichotomy, and the light-cone speed limit before taking the $N\to\infty$ continuum limit.
Spacelike separation is defined by positivity of that form: $s^2 > 0$ (outside the light cone). Timelike and lightlike are the complementary cases $s^2 < 0$ and $s^2 = 0$. The module already records that Lorentzian signature is forced by tick/voxel asymmetry, the spatial metric by $J''(1)=1$, and $c=1$ voxel per tick by the discrete posting cadence. This lemma is the elementary coordinate translation of the spacelike predicate into an inequality on the components.
proof idea
One short tactic proof. Unfold is_spacelike (defined as $0 < s^2$) and minkowski_form ($-t^2+x^2+y^2+z^2$). Split the biconditional; each direction is an intro followed by linarith, which rewrites $0 < -t^2 + x^2+y^2+z^2$ into $t^2 < x^2+y^2+z^2$ and conversely. No external lemmas are required beyond the two local definitions.
why it matters
Causal structure is step 3 of the continuum-emergence architecture: after the Minkowski form and Lorentzian signature, the module needs a clean trichotomy (timelike / spacelike / lightlike) and the light-cone speed limit. This iff statement is the coordinate face of the spacelike half of that trichotomy, matching the paper claim "Spacelike ↔ Outside Cone."
It sits inside the unconditional block of the module (signature, light cone, causal structure, flat Minkowski limit). Downstream siblings such as causal_trichotomy and light_cone_speed_limit rely on the same vocabulary; even with no recorded used_by edges yet, the lemma is the standard rewrite target when a proof needs the geometric inequality rather than the $s^2>0$ packaging. In the broader RS chain it supports the forced $D=3$ spatial sector and the continuum limit that eventually feeds weak-field Einstein equations from ledger defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.