physical_interval_expand
plain-language theorem explainer
The lattice-scaled spacetime interval equals the expanded Minkowski quadratic form with each coordinate multiplied by the spacing a. Anyone working the continuum limit from discrete ledger sites to Lorentzian geometry will cite this identity. The proof is a one-line unfold of the two definitions followed by ring normalization.
Claim. For all real $a,t,x,y,z$, the physical interval at lattice spacing $a$ satisfies $$\mathrm{ds}^2(a;t,x,y,z)=-(at)^2+(ax)^2+(ay)^2+(az)^2.$$
background
This module builds the zero-parameter bridge from discrete Recognition Science ledger sites to a Lorentzian continuum. The chain runs J-cost lattice → quadratic cost → Laplacian → Lorentzian interval → Minkowski flat limit, then curved metrics from defect and Einstein equations. Signature, light cone, and $c=1$ voxel per tick are forced rather than fitted.
The Minkowski form on $\mathbb{R}^{1,3}$ is $s^2(t,x,y,z)=-t^2+x^2+y^2+z^2$. The physical interval multiplies that form by the squared lattice spacing: $\mathrm{ds}^2=a^2,s^2$. Here $a=L/N$ is the spacing of an $N$-site box of side $L$, so the identity simply rewrites the scaled interval in the familiar expanded coordinates used later for causal trichotomy and the light-cone speed limit.
proof idea
One-line term proof. Unfold the definitions of the physical interval ($a^2$ times the Minkowski form) and of the Minkowski form itself, then apply ring to rewrite $a^2(-t^2+x^2+y^2+z^2)$ as $-(at)^2+(ax)^2+(ay)^2+(az)^2$. No external lemmas are required.
why it matters
The expanded form is the working expression for Lorentzian intervals on the lattice before the $N\to\infty$ continuum limit. It sits in the proved block of ContinuumManifoldEmergence: Lorentzian signature, light cone, and flat-space Minkowski limit. Downstream siblings (timelike/spacelike/lightlike predicates, causal trichotomy, light-cone speed limit) read intervals in this expanded shape. In the RS forcing chain it supports the claim that $c=\ell_0/\tau_0$ is forced by one voxel per tick and that $D=3$ spatial dimensions (T8) enter the continuum metric with the correct signature, without phenomenological ILG kernels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.