is_lightlike
plain-language theorem explainer
Lightlike (null) separation on Minkowski space is the predicate that s² = −t² + x² + y² + z² vanishes. Anyone citing the continuum-limit bridge from discrete ledger sites to Lorentzian spacetime uses it for causal trichotomy and the light-cone speed limit. It is a one-line definition equating the Minkowski quadratic form to zero.
Claim. A displacement $(t,x,y,z)\in\mathbb{R}^{1,3}$ is lightlike when its Minkowski quadratic form vanishes: $-t^{2}+x^{2}+y^{2}+z^{2}=0$ (null separation, on the light cone).
background
The module ContinuumManifoldEmergence is the zero-parameter bridge from discrete RS ledger sites to Lorentzian spacetime. Its architecture starts from the Minkowski form on $\mathbb{R}^{1,3}$, then Lorentzian signature, then the causal trichotomy (timelike / spacelike / lightlike), then the light cone as the speed limit $c=1$ (one voxel per tick).
The upstream Minkowski quadratic form is $s^{2}(t,x,y,z)=-t^{2}+x^{2}+y^{2}+z^{2}$. Sibling predicates mark the other two causal classes: timelike when $s^{2}<0$, spacelike when $s^{2}>0$. Lightlike is the remaining case $s^{2}=0$, i.e. null separation on the cone.
Signature and flat Minkowski limit are listed as unconditional in the module: forced by tick/voxel asymmetry and by $J''(1)=1$ for the spatial metric, with $D=3$ from DimensionForcing.
proof idea
One-line definition (no proof body): the predicate holds exactly when the Minkowski quadratic form equals zero. Downstream proofs unfold it and reduce with linarith, ring, or nlinarith against the expanded form $-t^{2}+x^{2}+y^{2}+z^{2}$.
why it matters
This predicate is the null leg of the causal structure that the continuum bridge must export. Parent results that apply it directly: causal trichotomy (every displacement is exactly one of timelike, spacelike, or lightlike); light-cone speed limit (on $s^{2}=0$ one has $t^{2}=x^{2}+y^{2}+z^{2}$, i.e. $c=1$ voxel/tick); explicit null rays along the $x$-axis and the equal-spatial diagonal; and the master ContinuumLimitCert, which packages Lorentzian signature as a Tier-1 forced fact.
In the RS forcing chain this sits after T7 (eight-tick octave) and T8 ($D=3$), and after the J-cost lattice has produced a quadratic spatial metric. It is definitional scaffolding for the proved light-cone and flat-limit claims, not a phenomenological fit (contrast the ILG time-kernel $w_t$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.