pith. sign in
module module high

IndisputableMonolith.ILG.PoissonKernel

show as:
view Lean formalization →

The module defines the operator mapping source density perturbations to gravitational potentials via the modified Poisson equation in Fourier space, incorporating the ILG kernel. Cosmologists studying scale-dependent gravity modifications would cite it for potential calculations in structure formation. The module consists entirely of definitions that import and apply the kernel without any proofs.

claimThe module introduces the operator mapping such that $-k^2 Φ(k,a) = 4πG · w(k,a) · δρ(k,a)$, where the kernel takes the form $w(k,a) = 1 + C (a/(k τ₀))^α$.

background

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

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the operator definition that enables sibling declarations such as poisson_operator and poisson_operator_solves to establish solvability and boundedness properties. It operationalizes the ILG kernel for the modified Poisson equation within the framework.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (14)