physical_interval
plain-language theorem explainer
Defines the physical spacetime interval on a lattice of spacing a as ds² = a²(−t² + x² + y² + z²). Anyone working the continuum limit from discrete ledger sites to Minkowski spacetime cites this scaling. It is a one-line product of a² with the dimensionless Minkowski quadratic form.
Claim. For lattice spacing $a \in \mathbb{R}$ and coordinates $(t,x,y,z) \in \mathbb{R}^{1,3}$, the physical interval is $ds^2(a;t,x,y,z) := a^2(-t^2 + x^2 + y^2 + z^2)$.
background
The module builds the zero-parameter bridge from discrete RS ledger sites to a Lorentzian manifold: J-cost lattice to quadratic cost to Laplacian to Lorentzian interval, then Minkowski flat limit and curved metric from defect. Lorentzian signature is forced by tick/voxel asymmetry; the spatial metric by $J''(1)=1$; $c=\ell_0/\tau_0$ by one voxel per tick; $D=3$ by DimensionForcing.
The dimensionless Minkowski form on $\mathbb{R}^{1,3}$ is $s^2(t,x,y,z)=-t^2+x^2+y^2+z^2$. A related unification-layer interval sums $\eta_{ii}v_i^2$ over a four-component displacement. Here the continuum picture uses a finite $N$-site box of side $L$ with spacing $a=L/N$; physical lengths are lattice units times $a$, so the interval must carry $a^2$.
proof idea
Pure definition: multiply the squared lattice spacing by the already-defined Minkowski quadratic form. No tactics or lemmas; the body is the product $a^2\cdot s^2(t,x,y,z)$. Downstream lemmas unfold this and the Minkowski form, then finish by ring or sign facts on the signature.
why it matters
Places the continuum interval at the correct physical scale so signature and causal structure survive the $N\to\infty$ limit. Feeds three immediate parents: the expansion identity $ds^2=-(at)^2+(ax)^2+(ay)^2+(az)^2$; the temporal sign lemma (physical temporal intervals stay negative for $a\neq 0$); and the spatial sign lemma (physical spatial intervals stay positive). Those close architecture steps 1–3 of the module (Minkowski form, Lorentzian signature, causal trichotomy) and underwrite the flat-space limit claimed as proved. In the RS chain this is the Lorentzian-interval node between Laplacian continuum limit and weak-field Einstein equations, with $\kappa=8\varphi^5$ from ZeroParameterGravity kept separate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.