effectiveSource
plain-language theorem explainer
The effectiveSource definition supplies the ILG source term as the product 4π G a² ρ w(k,a) δ. Workers on gravitational growth equations or Poisson sources in the Recognition framework cite it when shifting to pressure variables p := ρ w δ. The definition is a direct algebraic expression matching the standard source form with the kernel inserted.
Claim. The effective source term is defined by $S = 4π G a^2 ρ w(k,a) δ$, where $G$ is the gravitational constant from the Phys structure, $w$ is the ILG kernel function of type Kernel, $a$ is the scale factor, $ρ$ the density, and $δ$ the defect parameter.
background
The ILG.PressureForm module presents ILG as a pressure display scaffold. Phys is a structure containing the gravitational constant G; Kernel is the abbreviation for the two-argument function type ℝ → ℝ → ℝ that stands for the ILG kernel w(k,a). The module documentation states that this permits rewriting the source using the pressure variable p := ρ · w(k,a) · δ while leaving the physics unchanged.
proof idea
Direct definition. The body is the single expression 4 * Real.pi * P.G * (a ^ 2) * ρ * (W k a) * δ, which inserts the kernel evaluation into the standard 4π G a² ρ δ form.
why it matters
This definition is used by the source_equiv theorem, which proves equality to the pressure-form version by reflexivity. It completes the algebraic display scaffold for ILG pressure in the Recognition framework and connects to the upstream derivation of G in Constants.G together with the J-cost inflaton potential. It supports the T8 step on spatial dimensions by supplying the source term for growth equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.