pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.ILG.PoissonKernel

show as:
view Lean formalization →

The ILG.PoissonKernel module formalizes the modified Poisson equation in Fourier space for Infra-Luminous Gravity, defining an operator that maps density perturbations to gravitational potentials via the ILG kernel. Cosmologists studying modified gravity and structure formation would cite it when deriving potentials under scale-dependent corrections. The module supplies the core definitions and basic solvability statements for the poisson_operator and its properties, building directly on the imported kernel.

claimThe operator satisfies $-k^2 Φ(k,a) = 4πG · w(k,a) · δρ(k,a)$, where the ILG kernel is $w(k,a) = 1 + C (a/(k τ₀))^α$.

background

The Infra-Luminous Gravity (ILG) model augments Newtonian gravity with a scale-dependent kernel in the Poisson equation. The upstream ILG.Kernel module supplies the explicit form $w(k,a) = 1 + C · (a/(k τ₀))^α$. This module recasts the equation $-k² Φ = 4πG w δρ$ as an operator mapping from source density to potential in Fourier space, within the setting of linear cosmological perturbations.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the operator that connects the ILG kernel to gravitational potentials, enabling downstream ILG calculations of structure growth and potential-density relations. It implements the Fourier-space form of the modified Poisson equation required by the broader Recognition Science gravity framework.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (14)