source_equiv
plain-language theorem explainer
The theorem equates the direct ILG effective source 4π G a² ρ W(k,a) δ with its pressure-rewritten form that substitutes p := ρ · W(k,a) · δ. Modelers rewriting the Poisson or growth source term in ILG would cite this for display equivalence. The proof is a one-line reflexivity that holds because the two definitions expand to identical expressions.
Claim. Let $P$ be a structure containing gravitational constant $G$ and let $W : ℝ → ℝ → ℝ$ be the kernel. For real parameters $k,a,ρ,δ$, the source term $4π G a² ρ W(k,a) δ$ equals the pressure-displayed source $4π G a² p$ where $p = ρ · W(k,a) · δ$.
background
The ILG.PressureForm module presents an algebraic scaffold for rewriting the effective source term of the Poisson or growth equation using a pressure variable. Phys is the structure holding only the constant G. Kernel is the abbreviation for the two-argument function w(k,a). The upstream definitions effectiveSource and effectiveSource_pressure both expand to the same product 4π G a² ρ w δ, with the latter inserting the pressure product explicitly.
proof idea
The proof is a term-mode reflexivity. The two sides are definitionally equal once pressure is substituted for the product ρ · W(k,a) · δ inside the common prefactor 4π G a².
why it matters
This theorem closes the display-equivalence scaffold in the ILG pressure-form section, allowing the source term to be written indifferently in density or pressure variables. It supplies the algebraic identity needed before any dynamical use of the rewritten source, consistent with the Recognition Science emphasis on equivalent representations. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.