null_ray_diagonal
plain-language theorem explainer
If three equal spatial components satisfy 3a² = 1, the four-vector (1, a, a, a) lies on the Minkowski light cone. Anyone checking the continuum causal structure or the c = 1 voxel/tick speed limit cites this. The proof reduces lightlikeness to the quadratic form and closes by linear arithmetic from the hypothesis.
Claim. Let $a \in \mathbb{R}$ satisfy $3a^2 = 1$. Then the displacement $(t,x,y,z) = (1,a,a,a)$ is lightlike: its Minkowski quadratic form vanishes, $-1^2 + a^2 + a^2 + a^2 = 0$.
background
This 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 $\eta$ on $\mathbb{R}^{1,3}$ by $s^2 = -t^2 + x^2 + y^2 + z^2$; steps 2–4 establish Lorentzian signature, the timelike/spacelike/lightlike trichotomy, and the light-cone speed limit $c = 1$ voxel per tick.
Lightlike separation is defined by vanishing of that form: a four-vector is lightlike precisely when $\mathrm{minkowski_form}(t,x,y,z) = 0$. The present lemma sits among the signature and cone lemmas (temporal and spatial signature signs, causal trichotomy, light-cone speed limit) that make the continuum causal structure unconditional before the $N\to\infty$ lattice limit begins.
proof idea
Term-mode proof. Rewrite the goal via the definition of lightlike separation as equality of the Minkowski form at $(1,a,a,a)$ to zero. Unfold the form to $-1^2 + a^2 + a^2 + a^2$. Discharge with nlinarith from the hypothesis $3a^2 = 1$, which forces $-1 + 3a^2 = 0$. No external lemmas beyond the local form and lightlike definitions.
why it matters
The module claims Lorentzian signature, light cone, and causal structure as unconditional. This lemma supplies an explicit null generator along the equal-spatial diagonal: the ray that advances one tick and equal steps in $x,y,z$ with $a = 1/\sqrt{3}$. That is the continuum image of isotropic one-voxel-per-tick propagation forced by the tick/voxel asymmetry and $D = 3$ (DimensionForcing, T8).
It anchors the light-cone $\leftrightarrow$ speed-limit story ($c = \ell_0/\tau_0 = 1$ in RS units) before finite $N$-site lattices and Laplacian convergence. No downstream dependents are recorded yet; the natural consumers are causal-trichotomy corollaries, cone geometry, and any continuum certificate that needs a concrete null direction in three equal spatial components.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.