half_rung_budget
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 in Recognition Science
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.
scope and limits
- Does not derive the kernel exponent α.
- Does not extend the budget identity to higher rungs.
- Does not incorporate the three-channel factorization argument.
- Does not address empirical fitting beyond the structural constraint.
Lean usage
have h := half_rung_budget; linarithformal statement (Lean)
159theorem half_rung_budget : Jphi_penalty + C_kernel = 1 / 2 := by
proof body
Term-mode proof.
160 rw [Jphi_penalty_eq_phi_minus_three_halves, C_kernel_eq_two_minus_phi]
161 ring
162
163/-- Equivalent form: `2 J(φ) + 2 C = 1`. -/