physical_interval_temporal
plain-language theorem explainer
Purely temporal displacements on the lattice carry a negative physical interval: a² s² < 0 whenever the spacing a and the time coordinate t are nonzero. Anyone checking that the continuum limit keeps Lorentzian signature cites this. The proof multiplies the positive square a² by the already-proved negative temporal Minkowski form.
Claim. For lattice spacing $a \neq 0$ and time coordinate $t \neq 0$, the physical interval $a^{2}\,s^{2}$ of the pure time displacement $(t,0,0,0)$ is strictly negative: $a^{2}\,\eta(t,0,0,0) < 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 metrics from defect. Architecture step 2 is the Lorentzian signature itself: temporal directions negative, spatial directions positive.
The Minkowski form on $\mathbb{R}^{1,3}$ is $s^{2} = -t^{2} + x^{2} + y^{2} + z^{2}$. The physical interval scales that form by the squared lattice spacing: $\mathrm{ds}^{2} = a^{2},s^{2}$. Upstream, signature_temporal already shows that a pure time displacement has $s^{2} < 0$ whenever $t \neq 0$ ("encodes the NEGATIVE signature of the time direction").
This lemma lifts that sign statement from the dimensionless form to the dimensionful physical interval used when the continuum limit $N\to\infty$ is taken with spacing $a = L/N$.
proof idea
One short term proof. Unfold the physical interval to $a^{2}\cdot\eta(t,0,0,0)$. Apply mul_neg_of_pos_of_neg: the first factor is $a^{2} > 0$ by sq_pos_of_ne_zero on $a\neq 0$; the second factor is $\eta(t,0,0,0) < 0$ by the upstream theorem signature_temporal on $t\neq 0$. Product of a positive and a negative is negative.
why it matters
Preserving Lorentzian signature under the physical (lattice-scaled) interval is part of the module's unconditional core: "Lorentzian signature, light cone, causal structure" and "Flat-space limit = Minkowski." Without the temporal sign staying negative after multiplying by $a^{2}$, the continuum limit would not be Lorentzian spacetime.
The module contrasts this zero-parameter forcing with the phenomenological ILG time-kernel: signature here is forced by tick/voxel asymmetry, not fit to data. Framework landmarks in play are the eight-tick temporal structure and $D=3$ spatial dimensions already forced upstream; this lemma is the temporal half of the signature check that feeds causal trichotomy and the light-cone speed limit $c=1$ voxel/tick.
No downstream uses are recorded yet; it sits as a signature lemma available to later continuum and weak-field arguments in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.