weak_field_flat_limit
plain-language theorem explainer
Vanishing Newtonian potential reduces the weak-field isotropic interval exactly to the Minkowski quadratic form on ℝ^{1,3}. Anyone citing the zero-parameter continuum bridge from discrete ledger sites to Lorentzian spacetime uses this as the flat-space anchor. The proof is a pure algebraic identity: unfold both definitions and ring.
Claim. For all real $t,x,y,z$, the weak-field isotropic interval at zero potential equals the Minkowski form: $-(1+2\cdot 0)\,t^2+(1-2\cdot 0)(x^2+y^2+z^2)=-t^2+x^2+y^2+z^2$. Equivalently, $\Phi=0$ recovers $s^2=-t^2+x^2+y^2+z^2$.
background
This module builds the foundational continuum bridge from discrete RS ledger sites to a Lorentzian manifold: J-cost lattice to quadratic cost to Laplacian to Lorentzian interval, then the Minkowski flat limit, then curved metric from defect and Einstein equations. Unlike the phenomenological ILG time-kernel, the bridge is zero-parameter: Lorentzian signature from tick/voxel asymmetry, spatial metric from $J''(1)=1$, $c=\ell_0/\tau_0$ from one voxel per tick, and $D=3$ from DimensionForcing.
The Minkowski quadratic form is $s^2(t,x,y,z)=-t^2+x^2+y^2+z^2$. The weak-field isotropic interval is the standard linearized ansatz $ds^2=-(1+2\Phi),dt^2+(1-2\Phi)(dx^2+dy^2+dz^2)$, with $\Phi$ the Newtonian potential. The module lists the flat-space limit as unconditionally proved.
proof idea
One-line algebraic identity. Unfold the definitions of the weak-field interval and the Minkowski form, substitute $\Phi=0$, and finish with ring. No external lemmas are required; the equality is immediate from the coefficient arithmetic $1\pm 2\cdot 0=1$.
why it matters
Anchors step 9 of the module architecture (weak-field defect perturbation to curved Lorentzian) by fixing the $\Phi=0$ base case as exact Minkowski. Downstream it is consumed by the continuum limit certificate, which packages signature, causal trichotomy, and related facts into a single ContinuumLimitCert. In the Recognition chain this is the flat limit on the path from discrete ledger to continuum gravity: without it the weak-field curved metric has no calibrated Minkowski background. It sits under the zero-parameter gravity program (coupling $\kappa=8\varphi^5$ derived elsewhere) and under the forcing landmarks $D=3$ and the eight-tick octave that fix the discrete substrate before the $N\to\infty$ limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.