C_kernel_lt_half
plain-language theorem explainer
The spatial-kernel amplitude C in the ILG gravity model satisfies C < 1/2. Gravity modelers cite this to confirm the kernel amplitude remains below the half-rung budget when modifying the Newton-Poisson relation in Fourier space. The proof rewrites C via its closed form 2 - phi, invokes the lemma phi > 1.5, and closes the inequality with linear arithmetic.
Claim. $C < 1/2$, where $C = 2 - 1/2$ is the ILG spatial-kernel amplitude derived from the half-rung budget identity.
background
The module formalizes the ILG spatial-kernel amplitude as $C = phi^{-2}$ in the Fourier-space modification $w_ker(k) = 1 + C (k_0/k)^alpha$ with alpha approximately 0.191. The structural core is the half-rung budget identity $J(phi) + phi^{-2} = 1/2$, which follows from the quadratic relation phi^2 = phi + 1 and selects C = phi^{-2} over the alternative phi^{-3/2} value. Upstream results include the lemma phi > 1.5 (from sqrt(5) > 2) and the equality theorem C_kernel = 2 - phi.
proof idea
The proof is a one-line wrapper that rewrites C_kernel using the equality C_kernel = 2 - phi, applies the upstream lemma phi > 1.5, and closes via linarith.
why it matters
This bound confirms the kernel amplitude lies strictly below the half-rung budget, supporting the structural identity J(phi) + C = 1/2 that resolves the prior ambiguity between C = phi^{-2} and C = phi^{-3/2} in the Recognition Science framework. It belongs to the numerical band section that follows the derivation of C from first principles and aligns with the entropy paper's three-channel factorization. The declaration closes a concrete inequality needed for the ILG kernel to remain consistent with the eight-tick octave and D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.