newtonian_positive_source
plain-language theorem explainer
Positive mass density forces a strictly positive right-hand side in the Newtonian Poisson equation ∇²Φ = 4πGρ, using the RS-native gravitational coupling. Anyone checking the continuum Newtonian limit of the cubic-lattice J-cost Regge action needs this sign fact. The proof is a four-factor positivity product: 4 > 0, π > 0, G > 0, and ρ > 0.
Claim. If $\rho \in \mathbb{R}$ satisfies $\rho > 0$, then $4\pi G\rho > 0$, where $G$ is the RS-native gravitational coupling (projected through the recognition/Planck bridge).
background
The module gives a direct continuum limit for J-cost Regge calculus on the cubic lattice $\mathbb{Z}^D$, replacing the general Cheeger–Müller–Schrader axiom by an RS-specific argument. The cost is the forced J-function $J(e^\varepsilon)=\cosh\varepsilon-1$; its Euler–Lagrange equation linearizes to the lattice Laplacian, which converges to $\nabla^2$ at order $a^2$.
In the Newtonian regime the continuum equation is Poisson’s equation $\nabla^2\Phi=4\pi G\rho$. Here $G$ is the RS-native coupling $G=\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$ (equivalently $G=\varphi^5/\pi$ in RS units), not a fitted SI constant. The companion lemma $G>0$ is already proved from positivity of $\lambda_{\mathrm{rec}}$, $c$, and $\hbar$.
This declaration isolates the elementary sign statement: a positive source density yields positive potential curvature on the right-hand side of Poisson’s equation.
proof idea
Term-mode proof by iterated mul_pos. Factor the product as $(((4\cdot\pi)\cdot G)\cdot\rho)$. The constant $4$ is positive by norm_num; $\pi>0$ is Real.pi_pos; $G>0$ is Constants.G_pos; $\rho>0$ is the hypothesis. Each successive product of positives is positive.
why it matters
In the cubic-lattice Regge program the continuum limit of the J-cost variational principle is the linearized Einstein equation, whose Newtonian reduction is $\nabla^2\Phi=4\pi G\rho$ with the forced coupling $G=\varphi^5/\pi$. The sign of the source term is part of that identification: positive density must produce positive curvature of $\Phi$.
The declaration sits in the Newtonian-limit block of Gravity.CubicReggeProof, after EL linearization and before the cubic-lattice geometry section (flat $\mathbb{Z}^3$ has vanishing deficit). It has no recorded downstream dependents yet; it is a local hygiene lemma that any later uniqueness or maximum-principle argument for the continuum potential can invoke without reopening the definition of $G$.
Framework landmarks: T5 forces $J$, the continuum tier recovers $\nabla^2$, and the RS value of $G$ is already fixed by the recognition/Planck bridge rather than by fit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.