physical_interval_spatial
plain-language theorem explainer
Purely spatial physical intervals are strictly positive whenever the lattice scale and the nonzero spatial displacement are nonzero, so the Lorentzian signature stays intact on spatial axes. Cite this when checking continuum emergence of Minkowski signature from the ledger. The proof multiplies a^{2} > 0 by the spatial-signature positivity lemma after unfolding the interval.
Claim. For all real $a,x$ with $a \neq 0$ and $x \neq 0$, the physical spacetime interval at scale $a$ with pure $x$-displacement (vanishing $t,y,z$) is strictly positive: $0 < I_{\mathrm{phys}}(a;\,0,x,0,0)$.
background
This module builds the zero-parameter bridge from discrete Recognition Science ledger sites to a Lorentzian continuum: J-cost lattice to quadratic cost to Laplacian, then Lorentzian interval, Minkowski flat limit, and eventually curved metrics from defects. Architecture step 2 is the Lorentzian signature itself: temporal components negative, spatial components positive.
The Minkowski form on $\mathbb{R}^{1,3}$ is $s^2 = -t^2 + x^2 + y^2 + z^2$. Sibling lemmas establish the four signature signs and the causal trichotomy (timelike / spacelike / lightlike). The physical interval scales that quadratic form by a nonzero lattice factor $a$, so positivity of pure spatial displacements is exactly spacelike signature at finite scale.
Upstream forcing supplies $D = 3$ (T8/T9 dimension forcing) and the log-coordinate cost $J_{\log}(t) = \cosh t - 1$, whose second derivative at the identity normalizes the spatial metric later in the module. Here only the signature half of that story is needed.
proof idea
Term-mode, two steps. Unfold the definition of the physical interval (scale factor times the Minkowski quadratic form). The pure-$(x)$ case factors as $a^2$ times the spatial $x$-signature value. Apply mul_pos to (i) sq_pos_of_ne_zero on $a \neq 0$, giving $a^2 > 0$, and (ii) the sibling lemma that the spatial $x$-component of the signature is positive for $x \neq 0$. No further rewriting.
why it matters
Preserving positive spatial intervals is half of the forced Lorentzian signature in the continuum bridge (the other half is negative temporal intervals). The module doc lists Lorentzian signature, light cone, and causal structure among the unconditional proved items; this lemma is the $x$-axis spatial half of that certificate.
Framework landmarks: T8 forces $D = 3$ spatial dimensions, and the later J-cost section uses $J''(1) = 1$ plus $J_{\log}(\varepsilon) = J_{\log}(-\varepsilon)$ to get full Euclidean spatial metric and SO(3) isotropy. Without spatial positivity at finite scale, the Minkowski flat limit and the light-cone speed limit ($c = 1$ voxel/tick) would not sit on a Lorentzian form.
No downstream uses are recorded yet; the natural consumers are the causal trichotomy, spacelike predicate, and master continuum-emergence certificate in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.