CausalityBoundsPoissonCert
CausalityBoundsPoissonCert packages the three homogeneity properties of the ILG-modified Poisson operators. Cosmologists checking consistency of the kernel modification with standard FRW would cite it to confirm that the perturbation sector vanishes when the density contrast is zero. The structure is realized by direct substitution of the operator definitions into each field.
claimA record type whose fields require: for all kernel parameters $P$, scale factor $a$ and background density $bar rho$, the full operator (background plus perturbation) at zero contrast equals the background operator; the perturbation operator itself returns zero at zero contrast; and the full operator at zero contrast reduces to the background operator.
background
The module defines the modified Poisson equation as a Fourier-space multiplier and establishes basic stability bounds relative to standard GR. KernelParams is the ILG parameter bundle carrying the RS-derived exponent alpha = (1 - 1/phi)/2, amplitude C and reference time scale tau_0. The background operator is the standard FRW source term 4 pi a^2 bar rho / 3. The perturbation operator multiplies the density contrast by the kernel with explicit IR cutoff k_min to remove the k=0 divergence. The full operator is their direct sum.
proof idea
The declaration defines a record type collecting the three homogeneity statements. The concrete instance is supplied downstream by direct application of the three supporting lemmas: background independence of the kernel, homogeneity of the perturbation operator, and homogeneity of the full operator.
why it matters in Recognition Science
This structure is the master certificate for the causality-bound Poisson layer. It is instantiated by the definition that feeds into higher-level stability and scaling bounds for the modified gravity model. The properties guarantee that the ILG kernel modification preserves the homogeneous sector of the Poisson equation, ensuring consistency with the Recognition Science forcing chain before perturbation analysis proceeds.
scope and limits
- Does not derive the explicit kernel form or its Fourier multiplier.
- Does not establish operator-norm bounds or coercivity estimates.
- Does not treat time-dependent or nonlinear extensions of the equation.
- Does not link the operators to the full T0-T8 forcing chain.
formal statement (Lean)
136structure CausalityBoundsPoissonCert where
137 background_indep : ∀ (P : KernelParams) (a ρ_bar : ℝ),
138 poisson_operator_full P 0 0 a ρ_bar 0
139 = poisson_operator_background a ρ_bar
140 perturbation_homogeneous : ∀ (P : KernelParams) (k_min k a : ℝ),
141 poisson_operator_perturbation P k_min k a 0 = 0
142 full_homogeneous : ∀ (P : KernelParams) (k_min k a ρ_bar : ℝ),
143 poisson_operator_full P k_min k a ρ_bar 0
144 = poisson_operator_background a ρ_bar
145