weak_field_temporal_negative
plain-language theorem explainer
In the weak-field isotropic metric with Newtonian potential Φ, pure temporal intervals stay strictly negative whenever |Φ| < 1/2 and the time separation is nonzero. Researchers checking that the continuum limit keeps Lorentzian signature under small gravitational perturbations would cite this. The argument is a short algebraic inequality from the absolute-value bound and positivity of t².
Claim. If $|\Phi| < 1/2$ and $t \neq 0$, then the weak-field interval $-(1+2\Phi)t^{2}+(1-2\Phi)(x^{2}+y^{2}+z^{2})$ at $(t,0,0,0)$ is strictly negative.
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 Minkowski flat limit, curved metric from defect, and Einstein equations. Lorentzian signature is forced by tick/voxel asymmetry; the spatial metric by J''(1)=1; c by one voxel per tick; D=3 by DimensionForcing.
The weak-field isotropic interval is the standard linearized form $ds^{2}=-(1+2\Phi),dt^{2}+(1-2\Phi)(dx^{2}+dy^{2}+dz^{2})$, with Φ the Newtonian potential. At Φ=0 this collapses to Minkowski $s^{2}=-t^{2}+x^{2}+y^{2}+z^{2}$. The present claim is the temporal half of the statement that this form remains Lorentzian for small Φ.
proof idea
Unfold the weak-field interval at pure time separation $(t,0,0,0)$, which simplifies to $-(1+2\Phi)t^{2}$. From $|\Phi|<1/2$ extract $1+2\Phi>0$ via the absolute-value characterization and linear arithmetic. Then nonlinear arithmetic with $t^{2}>0$ (from $t\neq 0$) yields the strict inequality $-(1+2\Phi)t^{2}<0$.
why it matters
Doc-comment frames this as half of "Weak-Field is Lorentzian": temporal intervals remain negative (spatial positivity is the companion). In the module architecture it sits under step 9 (weak-field defect perturbation yields a curved Lorentzian metric en route to the EFE) and supports the proved block on Lorentzian signature, light cone, and causal structure. It anchors the claim that the continuum limit is not a phenomenological fit (unlike the ILG time-kernel) but a forced signature from the discrete ledger. No downstream users are wired yet; the natural parents are the master continuum-emergence certificate and any ADM or EFE assembly that needs the weak-field form to stay Lorentzian inside the Newtonian band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.