is_spacelike
plain-language theorem explainer
Spacelike separation on ℝ^{1,3} is the open set where the Minkowski quadratic form is strictly positive: s² = −t² + x² + y² + z² > 0 (outside the light cone). Anyone building causal structure, light-cone bounds, or continuum-limit certificates in the RS gravity bridge cites this predicate. It is a one-line definitional abbreviation of the sign of the Minkowski form.
Claim. A displacement $(t,x,y,z)\in\mathbb{R}^{1,3}$ is spacelike when its Minkowski interval is strictly positive: $s^2(t,x,y,z)=-t^2+x^2+y^2+z^2>0$ (equivalently, the event lies outside the light cone).
background
The module ContinuumManifoldEmergence is the zero-parameter bridge from discrete RS ledger sites to Lorentzian spacetime: J-cost lattice → quadratic cost → Laplacian → Lorentzian interval → Minkowski flat limit → curved metric from defect → Einstein equations. Lorentzian signature is forced by tick/voxel asymmetry; c = ℓ₀/τ₀ by one voxel per tick; D = 3 by DimensionForcing.
The basic quadratic form is the Minkowski form on ℝ^{1,3}: $s^2(t,x,y,z)=-t^2+x^2+y^2+z^2$. Sibling predicates split the real line of $s^2$ into timelike ($s^2<0$), spacelike ($s^2>0$), and lightlike ($s^2=0$). The present definition is the middle case: outside the light cone, where spatial components dominate.
Upstream, the form itself is the homogeneous degree-2 object used throughout the signature lemmas (temporal negative, spatial positive on each axis).
proof idea
Pure definition: unfold to the strict inequality $0 < \mathrm{minkowski_form}(t,x,y,z)$, i.e. $0 < -t^2+x^2+y^2+z^2$. No tactics or lemmas; the body is the Prop itself.
why it matters
This predicate is one leg of the causal trichotomy: every displacement is exactly one of timelike, spacelike, or lightlike (proved by real trichotomy on the Minkowski form). It also feeds the equivalence spacelike ↔ $t^2 < x^2+y^2+z^2$, which makes the geometric content of "outside the cone" explicit, and appears in the ContinuumLimitCert bundle that packages forced Lorentzian signature for the N→∞ limit.
In the RS forcing chain this sits under the continuum bridge after T7 (eight-tick octave) and T8 (D = 3): once the Minkowski form is in place, causal structure and the light-cone speed limit c = 1 voxel/tick are definitional consequences rather than phenomenological inputs. The module contrasts this zero-parameter path with the ILG time-kernel, which still fits galaxy data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.