causalityBoundsPoissonCert
plain-language theorem explainer
The definition causalityBoundsPoissonCert assembles the master certificate for the causality-bound Poisson layer by direct assignment of three homogeneity theorems. Researchers modeling modified gravity with ILG kernels would cite it to confirm that the kernel leaves the homogeneous FRW background invariant. The construction is a record wrapper that supplies the background independence theorem, the perturbation homogeneity theorem, and the full operator homogeneity theorem to the respective structure fields.
Claim. The master certificate for the causality-bound Poisson layer is the structure containing three properties: background independence, which states that for all kernel parameters $P$, scale factor $a$ and background density $bar rho$, the full Poisson operator at zero wavenumbers and zero perturbation equals the background operator; perturbation homogeneity, which states that for all $P$, $k_{min}$, $k$ and $a$, the perturbation operator vanishes at zero density perturbation; and full homogeneity, which states that for all $P$, $k_{min}$, $k$, $a$ and $bar rho$, the full operator at zero perturbation equals the background operator.
background
The ILG.PoissonKernel module expresses the modified Poisson equation as a Fourier-space multiplier and establishes basic stability and scaling bounds relative to standard GR. The structure CausalityBoundsPoissonCert collects the invariance properties that certify the ILG kernel respects causality bounds. Its background independence field asserts that the full operator reduces exactly to the standard background operator when both wavenumbers and perturbations vanish. The perturbation homogeneity field asserts that the perturbation term is identically zero for homogeneous configurations, leaving only the FRW background. The full homogeneity field follows by substitution of the perturbation result into the full operator.
proof idea
This is a one-line wrapper that directly supplies the three component theorems to the fields of the CausalityBoundsPoissonCert structure. It assigns poisson_background_independent_of_kernel to the background independence field, poisson_operator_perturbation_homogeneous to the perturbation homogeneity field, and poisson_operator_full_homogeneous to the full homogeneity field. The upstream theorems are invoked by name with no further rewriting or case analysis required.
why it matters
This certificate supplies the operator-level invariance statements required for the Poisson-with-kernel formulation to remain consistent with standard cosmology in the homogeneous limit. It supports the module's target of proving basic stability and scaling bounds relative to GR by guaranteeing that the ILG kernel introduces no effect on the background mode. No downstream results are recorded yet, so its role in full inhomogeneous solutions or explicit scaling bounds remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.