signature_spatial_z
plain-language theorem explainer
Purely spatial displacements along the z-axis yield a strictly positive Minkowski interval. Anyone assembling the Lorentzian signature of the RS continuum limit cites this (with the matching x/y and temporal lemmas). The proof unfolds the quadratic form and applies positivity of squares for nonzero reals.
Claim. For every real $z \neq 0$, the Minkowski interval $s^2 = -t^2 + x^2 + y^2 + z^2$ at $(t,x,y,z)=(0,0,0,z)$ satisfies $s^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 curved metric from defect. Architecture step 1 defines the Minkowski form $\eta$ on $\mathbb{R}^{1,3}$ by $s^2 = -t^2 + x^2 + y^2 + z^2$; step 2 asserts Lorentzian signature (temporal negative, spatial positive).
In RS-native units the tick $\tau_0$ and voxel $\ell_0$ are both 1, so $c = \ell_0/\tau_0 = 1$. The continuum certificate packages four signature facts plus causal trichotomy. This lemma is the z-axis spatial half of that package: a pure $z$-displacement must be spacelike.
Upstream constants fix the discrete units; the form itself is the local definition minkowski_form. Dimension forcing (T8) already supplies $D=3$, so three spatial axes appear.
proof idea
Term-mode, three steps. Unfold minkowski_form to $-0^2+0^2+0^2+z^2$. simp reduces the goal to $0 < z^2$. nlinarith closes with Mathlib's sq_pos_of_ne_zero on the hypothesis $z \neq 0$. No RS-specific lemmas beyond the form definition.
why it matters
Feeds directly into continuum_limit_certificate as the field spatial_positive_z, alongside temporal negativity and the x/y spatial lemmas. That certificate is the master stamp that Lorentzian signature, light cone, and causal structure are proved unconditionally in the continuum bridge.
Framework role: the module claims Lorentzian signature is forced by tick/voxel asymmetry, not fitted. This lemma is one atomic half of that claim (spatial positivity on the third axis). It sits under the flat Minkowski limit before defect curvature and Einstein equations. Landmarks: T8 ($D=3$) justifies three spatial axes; $c=1$ voxel/tick sets the cone that this signature supports. No open scaffold: status is proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.