signature_spatial_y
plain-language theorem explainer
Along a pure y-displacement with nonzero coordinate, the Minkowski quadratic form is strictly positive. Gravity and continuum-limit arguments cite this as one of the three spatial signature legs that force Lorentzian signature (+,+,+) on space. The proof unfolds the form, simplifies, and applies positivity of squares.
Claim. For every real $y \neq 0$, the Minkowski interval $s^2(0,0,y,0) = -0^2 + 0^2 + y^2 + 0^2$ satisfies $s^2 > 0$.
background
The module ContinuumManifoldEmergence builds the zero-parameter bridge from discrete RS ledger sites to Lorentzian spacetime: J-cost lattice to quadratic cost to Laplacian to Lorentzian interval, then Minkowski flat limit and curved metrics from defects.
The Minkowski quadratic form on $\mathbb{R}^{1,3}$ is defined by $s^2(t,x,y,z) = -t^2 + x^2 + y^2 + z^2$. Lorentzian signature means the pure-time ray is negative and each pure-space axis is positive. This theorem is the y-axis half of that spatial positivity package (siblings cover $x$ and $z$).
Upstream, the form itself is the local definition minkowski_form. The broader architecture ties spatial metric normalization to $J''(1)=1$ and $D=3$ from DimensionForcing; here only the algebraic signature fact is needed.
proof idea
Term-mode tactic proof: unfold the Minkowski form definition, simplify the zeros, then finish by nlinarith using sq_pos_of_ne_zero on the hypothesis $y \neq 0$. No external continuum or gravity lemmas are invoked; it is pure real arithmetic on $y^2 > 0$.
why it matters
Feeds directly into continuum_limit_certificate, which packages temporal negativity and all three spatial positivities plus causal trichotomy as the Continuum Limit Certificate. That certificate is the proved half of the module's foundational claim: Lorentzian signature is forced (not fitted), completing the chain from discrete ledger to Minkowski flat limit before defect curvature and Einstein equations.
In the RS forcing picture this sits under the continuum bridge after T8 ($D=3$) and the eight-tick/voxel asymmetry that separates the time axis from space. Without each spatial leg, the master certificate cannot assert full Lorentzian signature on $\mathbb{R}^{1,3}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.