poisson_operator_perturbation_kernel_bounded
plain-language theorem explainer
The theorem establishes an upper bound on the perturbation kernel multiplier in the modified Poisson operator for ILG models, ensuring it stays finite as the wave number approaches zero. Researchers studying infrared stability of Fourier-space perturbations in modified gravity or kernel-based cosmologies would cite this to control low-k runaway behavior. The proof is a direct one-line term application of the auxiliary boundedness lemma for the kernel perturbation function.
Claim. Let $P$ be kernel parameters containing positive constants $C$, fundamental tick duration $τ_0$, and exponent $α$. For $k_{min}>0$, $a>0$, and any wave number $k$, the perturbation kernel satisfies $κ(P,k_{min},k,a) ≤ 1 + C · (max(0.01, a/(k_{min} τ_0)))^α$, where $κ$ is the multiplier in front of $δρ/k²$.
background
The ILG.PoissonKernel module expresses the modified Poisson equation as a Fourier-space multiplier and derives stability/scaling bounds relative to standard GR. Kernel parameters $P$ encode scaling factors including $C$, the fundamental time unit $τ_0$ (duration of one tick in RS-native units), and the exponent $α$. Upstream constants supply $τ_0$ as the placeholder tick duration and the fine-structure constant definition used in the exponent.
proof idea
The proof is a term-mode one-line wrapper that directly invokes the prior lemma establishing the upper bound on the perturbation kernel for the supplied parameters $P$, $k_{min}$, $a$, and $k$. No further reductions or case splits are performed.
why it matters
This declaration supplies the infrared saturation bound required for the perturbation component of the Poisson-with-kernel statement. It guarantees the multiplier in front of $δρ/k²$ cannot diverge at small $k$, thereby supporting background-mode invariance where the homogeneous FRW solution remains untouched by the ILG kernel. The result closes one stability gap in the module's target of proving basic bounds relative to GR.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.