null_ray_x
plain-language theorem explainer
The four-vector (1,1,0,0) is null for the Minkowski form on ℝ^{1,3}. Anyone assembling the light-cone or causal trichotomy in the continuum limit cites this elementary witness. The proof unfolds the lightlike predicate and the quadratic form, then closes by ring.
Claim. The displacement $(t,x,y,z)=(1,1,0,0)$ is lightlike: its Minkowski quadratic form vanishes, $-1^{2}+1^{2}+0^{2}+0^{2}=0$.
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 curved metric from defect. Architecture step 1 fixes the Minkowski form on ℝ^{1,3} by $s^{2}(t,x,y,z)=-t^{2}+x^{2}+y^{2}+z^{2}$.
Lightlike (null) separation is the predicate $s^{2}=0$, i.e. the event lies on the light cone. Sibling definitions supply the matching timelike and spacelike predicates and the causal trichotomy. The continuum limit forces $c=1$ voxel per tick, so a unit time step with unit spatial step along one axis is the canonical null generator.
proof idea
One-line tactic proof: unfold the lightlike predicate (equality of the Minkowski form to zero) and the definition of the Minkowski form, then ring evaluates $-1^{2}+1^{2}+0^{2}+0^{2}=0$.
why it matters
This is a concrete null-ray witness inside the proved causal-structure block of ContinuumManifoldEmergence (Lorentzian signature, light cone, trichotomy). It anchors the geometric meaning of $c=1$ forced by one voxel per tick, before the N→∞ Laplacian limit and the weak-field defect → Einstein path. Downstream siblings such as the light-cone speed-limit statement and the 45° multi-axis null ray sit in the same cluster; the module doc lists Lorentzian signature and light cone as unconditional. Framework landmarks: continuum bridge after T7 (eight-tick) and T8 (D=3), with spatial metric fixed by J''(1)=1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.