weak_field_spatial_positive
plain-language theorem explainer
Under a weak gravitational potential with |Φ| < 1/2, any pure spatial displacement with nonzero x-component has strictly positive weak-field interval. Cited when checking that the weak-field metric retains Lorentzian spatial signature. The proof unfolds the interval, gets 1−2Φ > 0 from the bound on Φ, and multiplies by x² > 0.
Claim. Let $\Phi, x \in \mathbb{R}$ with $|\Phi| < 1/2$ and $x \neq 0$. Then the weak-field spacetime interval at the pure spatial event $(t,x,y,z)=(0,x,0,0)$ is strictly positive: $0 < s^2_{\mathrm{wf}}(\Phi;0,x,0,0)$.
background
The module builds the zero-parameter bridge from discrete RS ledger sites to a Lorentzian continuum: J-cost lattice to quadratic cost to Laplacian to Lorentzian interval, then weak-field curvature and Einstein equations. Architecture step 9 is the weak-field regime, where a defect potential Φ perturbs the flat Minkowski form.
Sibling material fixes the Minkowski quadratic form $s^2 = -t^2 + x^2 + y^2 + z^2$, with temporal signature negative and each spatial axis positive, plus the causal trichotomy and light-cone speed limit $c = 1$ voxel per tick. The weak-field interval is the first-order deformation of that form by Φ (schematically factors like $1 \pm 2\Phi$ on the temporal and spatial blocks).
Upstream constants fix the tick $\tau_0 = 1$ and spatial dimension $D = 3$ (T8/DimensionForcing), so the ambient space is $\mathbb{R}^{1,3}$. The present lemma is the spatial half of the weak-field signature check along a single axis.
proof idea
Tactic proof. Unfold weak_field_interval and simplify; the pure-spatial evaluation reduces to a product $(1-2\Phi),x^2$. From $|\Phi| < 1/2$, abs_lt and linarith give the bracket inequality $0 < 1-2\Phi$. Then mul_pos with sq_pos_of_ne_zero hx yields strict positivity. No external lemmas beyond core real arithmetic.
why it matters
Closes the spatial-positivity half of Lorentzian signature in the weak-field sector of ContinuumManifoldEmergence. The module's claim is that Lorentzian signature is forced by tick/voxel asymmetry and $J''(1)=1$, not fitted; this lemma is the elementary real-analysis check that the spatial block stays positive when $|\Phi|<1/2$.
It sits next to the flat-signature siblings (signature_spatial_x/y/z, signature_temporal) and the causal trichotomy, and supports the later curved-metric / EFE step in the same file. Framework landmarks: D = 3 from DimensionForcing (T8), c forced as one voxel per tick, and the zero-parameter gravity coupling from ZeroParameterGravity. No downstream uses are recorded yet; the lemma is local infrastructure for the master continuum certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.