weak_field_correction_bound
plain-language theorem explainer
The absolute gap between the weak-field interval (Newtonian potential Φ) and the flat Minkowski form is at most 2|Φ| times the Euclidean displacement norm-squared. Continuum-gravity analysts cite it to control metric perturbations before proving Lorentzian signature survives. The proof is pure algebra: the difference equals −2Φ‖v‖², so the claimed bound is equality after absolute values.
Claim. For all real $\Phi,t,x,y,z$, $\bigl|s_{\mathrm{wf}}(\Phi;t,x,y,z)-\eta(t,x,y,z)\bigr|\le 2|\Phi|(t^2+x^2+y^2+z^2)$, where $s_{\mathrm{wf}}$ is the weak-field interval and $\eta(t,x,y,z)=-t^2+x^2+y^2+z^2$ is the Minkowski quadratic form.
background
This module is the zero-parameter bridge from discrete RS ledger sites to a Lorentzian continuum: J-cost lattice → quadratic cost → Laplacian → Lorentzian interval → Minkowski flat limit → curved metric from defect → Einstein equations. Lorentzian signature, light-cone structure, and $c=1$ voxel/tick are forced upstream; $D=3$ comes from DimensionForcing and $\kappa=8\varphi^5$ from ZeroParameterGravity.
The Minkowski form on $\mathbb{R}^{1,3}$ is $\eta=-t^2+x^2+y^2+z^2$. The weak-field interval inserts a first-order defect potential $\Phi$, classically $s_{\mathrm{wf}}=-(1+2\Phi)t^2+(1-2\Phi)(x^2+y^2+z^2)$. Sibling definitions in the same file supply both forms. The next theorem in the file uses the present bound to keep signature Lorentzian whenever $|\Phi|<1/2$.
proof idea
The argument first upgrades the inequality to an equality of absolute values. Unfolding both interval forms and simplifying by ring gives the exact identity
$s_{\mathrm{wf}}-\eta=-2\Phi(t^2+x^2+y^2+z^2)$.
Absolute values then yield $|-2\Phi S|=2|\Phi|S$ with $S=t^2+x^2+y^2+z^2\ge 0$ (positivity). The remaining rewrites factor the product via abs_mul and discharge non-negativity of the constant 2 and of $S$ by abs_of_nonneg. No external gravity lemmas are required; the whole proof is elementary real arithmetic.
why it matters
In the continuum-emergence chain this is the quantitative control step for weak-field curvature: ledger defects produce a metric correction bounded by $2|\Phi|$ times displacement norm-squared. That bound is the hypothesis fuel for the immediately following “Weak-Field is Lorentzian” theorem in the same module, which needs $|\Phi|<1/2$ to keep temporal intervals negative and spatial intervals positive.
Architecturally it occupies step 9 of ContinuumManifoldEmergence (weak-field defect → curved Lorentzian → EFE), after Minkowski form, causal trichotomy, and light-cone speed limit. It is unconditional (proved, zero sorry). The dependency graph currently lists no downstream users, so it remains a local lemma awaiting the Einstein-equation closure of the module. Ambient RS landmarks are $D=3$ (T8) and the derived coupling $\kappa=8\varphi^5$; the bound itself is pure analysis on the interval forms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.