effectiveSource_pressure
plain-language theorem explainer
effectiveSource_pressure rewrites the ILG source term as 4π G a² times the pressure p = ρ W(k,a) δ. Cosmologists using Recognition Science models for structure formation cite this when recasting the Poisson source in pressure variables. The definition is a direct algebraic substitution that multiplies the supplied G by the kernel-derived pressure term.
Claim. Let $P$ be a structure containing the gravitational constant $G$, and let $W : ℝ → ℝ → ℝ$ be the ILG kernel. The pressure-form effective source is $4π G a² · p$, where $p = ρ · W(k,a) · δ$.
background
The ILG.PressureForm module supplies an algebraic scaffold for rewriting the effective source using a pressure variable p := ρ · w(k,a) · δ while leaving the physics unchanged. Phys is the structure holding G; Kernel is the abbreviation for the two-argument kernel function w(k,a). Upstream results supply G from the Recognition Science derivation in Constants, where G equals λ_rec² c³ / (π ℏ) in native units, and from the J-cost inflaton form G(t) = cosh(t) − 1.
proof idea
The definition is a direct one-line expression that multiplies 4π P.G a² by the pressure term computed from the kernel W at arguments k, a, ρ, δ. No lemmas or tactics are applied beyond the arithmetic and the referenced pressure function.
why it matters
This definition supplies the pressure-display form used by the downstream theorem source_equiv to prove algebraic identity with the standard effectiveSource via reflexivity. It completes the scaffold step in the ILG pressure display module, permitting equivalent presentation of the source term while preserving the forcing-chain landmarks T5–T8 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.