half_rung_budget
plain-language theorem explainer
The half-rung budget identity asserts that the first-rung J-cost penalty J(φ) together with the spatial-kernel amplitude C sums exactly to one half. Workers on the Information-Limited Gravity model cite this result to select C = φ^{-2} over competing values. The proof proceeds by direct substitution of the closed-form expressions for each summand followed by algebraic simplification.
Claim. $J(φ) + φ^{-2} = 1/2$, where $J(φ) := φ - 3/2$ is the first-rung cost penalty and $φ^{-2}$ is the spatial-kernel amplitude.
background
In the ILG framework the Fourier-space kernel takes the form $w_ker(k) = 1 + C (k_0/k)^α$ with amplitude C fixed by the half-rung budget. The first-rung J-cost penalty is defined as $J(φ) = φ - 3/2$. The spatial-kernel amplitude is defined as $C = φ^{-2}$. Upstream lemmas establish the closed forms $Jphi_penalty = φ - 3/2$ and $C_kernel = 2 - φ$.
proof idea
The proof is a one-line wrapper. It rewrites the left-hand side by substituting the equality theorems Jphi_penalty_eq_phi_minus_three_halves and C_kernel_eq_two_minus_phi, then normalizes the resulting expression with the ring tactic.
why it matters
This identity is the structural core of the ILG spatial-kernel module. It is invoked by the complement theorem C_is_complement_of_Jphi, the doubled form half_rung_budget_doubled, and the master certificate ilgSpatialKernelCert. The result selects C = φ^{-2} as the unique amplitude consistent with the first-rung cost penalty, closing the ambiguity noted in the module documentation between prior accounts of the kernel amplitude.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.