weak_field_interval
plain-language theorem explainer
The weak-field isotropic interval is the standard linearized line element ds² = −(1+2Φ)dt² + (1−2Φ)d𝐱² on ℝ^{1,3}. Continuum-limit and gravity proofs cite it to recover Minkowski at Φ = 0, bound the metric correction by 2|Φ|, and keep Lorentzian signature for |Φ| < 1/2. It is a pure definition of that quadratic form.
Claim. For a real potential $\Phi$ and coordinates $(t,x,y,z)\in\mathbb{R}^4$, the weak-field isotropic interval is $-(1+2\Phi)t^2+(1-2\Phi)(x^2+y^2+z^2)$, i.e. $ds^2=-(1+2\Phi)\,dt^2+(1-2\Phi)\,d\mathbf{x}^2$.
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 curved metric from defect and Einstein equations. Architecture steps include the Minkowski form $\eta$ on $\mathbb{R}^{1,3}$, forced Lorentzian signature from tick/voxel asymmetry, causal trichotomy, light-cone speed limit $c=1$ voxel/tick, and ADM-style weak-field deformation.
Sibling notation fixes the flat background as $s^2=-t^2+x^2+y^2+z^2$, with temporal rays negative and spatial rays positive. The weak-field object inserts a single isotropic Newtonian potential $\Phi$ as a first-order conformal split between the time and space blocks, matching the classical GR isotropic gauge.
Downstream theorems treat this form as the curved interval whose $\Phi=0$ slice is Minkowski and whose signature stays Lorentzian for $|\Phi|<1/2$.
proof idea
Pure definition (no proof obligations). The body is the five-argument real quadratic form $-(1+2\Phi)t^2+(1-2\Phi)(x^2+y^2+z^2)$, written to match the classical isotropic weak-field line element. Callers unfold it and simplify or ring-reduce against the Minkowski form.
why it matters
This is the curved interval in the module's weak-field tier (architecture step 9): defect perturbation to curved Lorentzian toward the Einstein equations. It is the common substrate for the flat-limit identity ($\Phi=0$ recovers Minkowski), the perturbation bound (correction $\le 2|\Phi|$ times displacement norm-squared), and the signature lemmas that temporal intervals stay negative and spatial intervals stay positive when $|\Phi|<1/2$.
Those facts feed the master ContinuumLimitCert structure, which packages forced Lorentzian signature and related continuum claims. In the RS chain this sits after D=3 forcing and J''(1)=1 spatial metric, and before zero-parameter coupling $\kappa=8\varphi^5$; it is definitional scaffolding for the proved continuum bridge, not a phenomenological ILG kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.