signature_spatial_x
plain-language theorem explainer
For any nonzero real x-displacement with vanishing time and other spatial coordinates, the Minkowski quadratic form is strictly positive. Continuum-limit and gravity arguments cite this as the x-axis half of Lorentzian spatial signature. The proof unfolds the form to x² and finishes by positivity of nonzero squares.
Claim. If $x \in \mathbb{R}$ and $x \neq 0$, then the Minkowski quadratic form satisfies $s^2(0,x,0,0) > 0$, i.e. $-0^2 + x^2 + 0^2 + 0^2 > 0$.
background
The module constructs the zero-parameter bridge from discrete Recognition Science ledger sites to Lorentzian spacetime: J-cost lattice to quadratic cost to Laplacian to Lorentzian interval, then Minkowski flat limit, curved metric from defect, and Einstein equations. Unlike the phenomenological ILG time-kernel, signature here is forced by tick/voxel asymmetry, the spatial metric by $J''(1)=1$, $c$ by one voxel per tick, and $D=3$ by DimensionForcing.
The Minkowski form on $\mathbb{R}^{1,3}$ is $s^2(t,x,y,z)=-t^2+x^2+y^2+z^2$. Lorentzian signature means temporal rays give $s^2<0$ and pure spatial rays give $s^2>0$. This lemma is the pure x-axis case of that spatial positivity, sibling to the y- and z-axis statements and to temporal negativity.
proof idea
Short tactic proof. Unfold the Minkowski form at $(0,x,0,0)$ to $-0^2+x^2+0^2+0^2$. Simplify away the zero terms, leaving $x^2$. Close with nonlinear arithmetic, feeding Mathlib's fact that a nonzero real has strictly positive square. No intermediate RS lemmas; pure algebra on the definition.
why it matters
Feeds the continuum limit certificate, which packages temporal negativity and all three spatial positivities plus causal trichotomy as the proved fields of the continuum-limit certificate structure. Also used by the physical-interval spatial theorem: a nonzero scale factor times this positive x-signature stays positive, so Lorentzian signature survives the physical interval map.
In the Recognition chain this is unconditional infrastructure for the N→∞ ledger-to-manifold bridge (module architecture steps 1–2): Lorentzian signature forced, not fitted. It sits under the flat Minkowski limit and upstream of light-cone speed limit, ADM decomposition, and weak-field defect-to-Einstein steps. Landmark contact: D=3 spatial dimensions (T8) and the forced continuum geometry rather than a free metric ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.