pressure
plain-language theorem explainer
Pressure in the ILG effective source is defined as the product of density ρ, the kernel weight evaluated at wavenumber k and scale factor a, and defect factor δ. Cosmologists and flight dynamics researchers cite it when converting the Poisson source term into pressure variables while preserving the 4π G a² prefactor. The definition is a direct algebraic substitution from the kernel abbreviation with no lemmas applied.
Claim. The pressure satisfies $p = ρ · w(k,a) · δ$, where $w$ is the effective source kernel mapping wavenumber $k$ and scale factor $a$ to a dimensionless weight, $ρ$ is mass density, and $δ$ is a defect parameter.
background
The ILG.PressureForm module supplies an algebraic display equivalence that rewrites the effective gravitational source using a pressure variable. The Kernel abbreviation stands for the weight function in the Poisson or growth equation source, given explicitly as 4π G a² ρ w δ. This definition sets p equal to ρ times the kernel evaluation at (k,a) times δ, leaving the underlying physics unchanged.
proof idea
The declaration is a one-line definition performing the multiplication ρ * (W k a) * δ. No lemmas or tactics are invoked; it directly encodes the pressure substitution stated in the module documentation.
why it matters
This definition feeds downstream results including darkEnergyDensity in Cosmology.CosmologicalConstant and PressureDropFromVorticity in Flight.Pressure. It completes the scaffold step for rewriting the ILG source in pressure variables, linking to the Recognition Science derivation of G from the Constants module and the J-cost inflaton potential. It enables consistent pressure treatment across cosmological and propulsion contexts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.