signature_temporal
plain-language theorem explainer
Purely temporal displacements in the Minkowski quadratic form are strictly negative: s²(t,0,0,0) = −t² < 0 whenever t ≠ 0. Anyone assembling the Lorentzian signature of the continuum limit cites this. The proof unfolds the form and applies positivity of squares.
Claim. For every real $t \neq 0$, the Minkowski quadratic form satisfies $s^2(t,0,0,0) = -t^2 < 0$.
background
This module builds the zero-parameter bridge from discrete RS ledger sites to Lorentzian spacetime: J-cost lattice to quadratic cost to Laplacian to Lorentzian interval to Minkowski flat limit, then curved metric from defect and Einstein equations. Lorentzian signature is forced by tick/voxel asymmetry; spatial metric by $J''(1)=1$; $c=\ell_0/\tau_0$ by one voxel per tick; $D=3$ by DimensionForcing.
The Minkowski form on $\mathbb{R}^{1,3}$ is defined by $s^2(t,x,y,z)=-t^2+x^2+y^2+z^2$. Architecture step 2 isolates the signature: temporal directions negative, spatial directions positive. This theorem is the temporal half of that split; the three spatial siblings handle the positive axes.
Upstream, minkowski_form is the bare quadratic form used here. The continuum-limit certificate later packages temporal negativity with spatial positivity and causal trichotomy as proved fields.
proof idea
Term-mode, three tactics. Unfold minkowski_form to $-t^2+0+0+0$. Simplify to $-t^2$. Then nlinarith with sq_pos_of_ne_zero ht closes $-t^2<0$ from $t\neq 0$ implying $t^2>0$.
why it matters
Without temporal negativity there is no Lorentzian continuum limit, only a Euclidean one. The master certificate continuum_limit_certificate wires this lemma in as temporal_negative, alongside the three spatial signature theorems and causal trichotomy. Downstream, physical_interval_temporal lifts the same fact to scaled physical intervals: $a^2\cdot s^2(t,0,0,0)<0$ for $a\neq 0$, preserving Lorentzian signature under the lattice-to-continuum scaling.
In the module architecture this is architecture item 2 (Lorentzian signature), feeding the causal trichotomy, light-cone speed limit $c=1$ voxel/tick, and eventually the flat Minkowski limit before defect curvature. It is unconditional (proved, no sorry), matching the module claim that signature and causal structure are fully forced rather than phenomenological ILG bridges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.