ILGSpatialKernelCert
plain-language theorem explainer
ILGSpatialKernelCert packages six phi-derived properties of the ILG spatial-kernel amplitude C into one structure. Gravity modelers cite it to fix C at phi inverse squared and exclude the competing phi to the minus three-halves value. The structure is a direct definition that assembles the six fields from already-proved sibling lemmas on the closed forms and inequalities.
Claim. The structure asserts that the spatial-kernel amplitude $C = varphi^{-2}$ satisfies the closed form $C = 2 - varphi$, positivity $0 < C$, the half-rung budget $J(varphi) + C = 1/2$, the numerical band $0.380 < C < 0.390$, the factorization $C = w^2$ with channel weight $w = varphi^{-1}$, and that the competing amplitude $C' = varphi^{-3/2}$ violates the budget.
background
In the ILG framework the Fourier-space modification of the Newton-Poisson relation is written $w_{ker}(k) = 1 + C (k_0/k)^alpha$ with amplitude $C = varphi^{-2}$. The module defines C_kernel as phi to the minus two and Jphi_penalty as phi minus three halves; these enter the half-rung budget identity $J(varphi) + C = 1/2$ which follows from $varphi^2 = varphi + 1$ alone. Upstream results supply channel_weight as phi inverse and confirm the competing value phi to the minus three-halves.
proof idea
The structure is a definition that directly assembles six fields from sibling lemmas: closed_form from C_kernel_eq_two_minus_phi, positivity from C_kernel_pos, budget from half_rung_budget, band from C_kernel_band, factorization from three_channel_factorization, and competing_excluded from the corresponding inequality on the competing amplitude.
why it matters
This certificate fixes the kernel amplitude at phi inverse squared, resolving the ambiguity between the entropy paper value and the competing phi to the minus three-halves. It feeds the inhabited certificate ilgSpatialKernelCert used downstream in gravity derivations. The half-rung budget identity is the key structural constraint from the phi ladder and RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.