is_timelike
plain-language theorem explainer
Timelike separation on ℝ^{1,3} is the open set where the Minkowski quadratic form is strictly negative: s² = −t² + x² + y² + z² < 0. Continuum-limit and causal-structure arguments cite this predicate as the interior of the light cone. It is a one-line definition wrapping the Minkowski form.
Claim. A displacement $(t,x,y,z)\in\mathbb{R}^{1,3}$ is timelike when its Minkowski interval satisfies $s^2=-t^2+x^2+y^2+z^2<0$ (strictly inside the light cone).
background
The module builds the zero-parameter bridge from discrete RS ledger sites to a Lorentzian continuum: J-cost lattice to quadratic cost to Laplacian to Lorentzian interval, then Minkowski flat limit and weak-field curvature. Architecture step 1 fixes the Minkowski form η on ℝ^{1,3} by s²(t,x,y,z) = −t² + x² + y² + z²; step 3 packages the causal trichotomy (timelike / spacelike / lightlike).
The upstream definition of the Minkowski quadratic form is exactly that expression. Signature lemmas already record that pure temporal displacements give s² < 0 and pure spatial ones give s² > 0. The present predicate simply names the open set {s² < 0}, i.e. the interior of the light cone in the (−,+,+,+) convention used throughout the module.
Local conventions: c = 1 (one voxel per tick), D = 3 spatial dimensions forced upstream, and the continuum limit is the N → ∞ lattice scaling with spacing a = L/N.
proof idea
Pure definition: unfold the Minkowski form and assert strict negativity. No tactics, no lemmas. Equivalent content is s²(t,x,y,z) < 0 with s² = −t² + x² + y² + z².
why it matters
This predicate is the first leg of the causal package that the continuum-emergence certificate must export. Downstream, causal trichotomy proves every displacement is exactly one of timelike, spacelike, or lightlike by case-splitting the real trichotomy of s² against 0. The equivalence theorem rewrites timelike as t² > x² + y² + z² (temporal component dominates). The master ContinuumLimitCert structure records temporal_negative as a Tier-1 forced fact: pure time intervals stay negative under the Minkowski form, and the weak-field Lorentzian-signature theorem reuses the same sign convention.
In the RS forcing chain this sits after T8 (D = 3) and the tick/voxel asymmetry that forces Lorentzian signature: the definition is the concrete open set on which those forced signs act. It is not phenomenological; it is the named interior used by every later light-cone and speed-limit statement in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.