ilg_spatial_kernel_one_statement
plain-language theorem explainer
The theorem establishes that the ILG spatial kernel amplitude C equals 2 minus phi, satisfies the half-rung budget identity J(phi) plus C equals one half, factors as the square of the channel weight, lies in the interval from 0.380 to 0.390, and excludes the competing amplitude phi to the minus three halves. Gravity modelers would cite it to fix the kernel amplitude from the Recognition cost structure. The proof is a one-line term wrapper that assembles six prior lemmas on the closed form, positivity, budget identity, numerical band, three-chan
Claim. Let $C = ϕ^{-2}$, $J = ϕ - 3/2$, $C' = ϕ^{-3/2}$, and $w = ϕ^{-1}$. Then $C = 2 - ϕ$, $0 < C$, $J + C = 1/2$, $0.380 < C < 0.390$, $C = w · w$, and $J + C' > 1/2$.
background
The Information-Limited Gravity framework modifies the Newton-Poisson source-potential relation in Fourier space as $w_{ker}(k) = 1 + C · (k_0/k)^α$ with exponent α already fixed near 0.191. The amplitude C is derived from the half-rung budget identity $J(ϕ) + C = 1/2$, which follows from $ϕ^2 = ϕ + 1$ alone. J(phi) is the first-rung J-cost penalty $ϕ - 3/2$, and C is defined as $ϕ^{-2}$. The module contrasts this with a competing value $ϕ^{-3/2}$ from an earlier account. The structural core is the algebraic identity $J(ϕ) + ϕ^{-2} = 1/2$, which says the cost penalty for crossing one phi-rung plus the cost-saving from finite-latency closure equals the half-rung interval.
proof idea
The proof is a one-line wrapper that applies the six lemmas C equals two minus phi, C positive, half-rung budget, the two parts of the numerical band, three-channel factorization, and competing violates budget.
why it matters
This declaration resolves the prior ambiguity between two accounts of the kernel amplitude by selecting C = phi^{-2} via the half-rung budget identity from the Recognition Science cost structure. It directly implements the structural core described in the module documentation. The result sits inside the ILG gravity construction and is consistent with the J-uniqueness and phi fixed-point steps of the forcing chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.