half_rung_budget_doubled
plain-language theorem explainer
The doubled half-rung budget identity states that twice the first-rung J-cost penalty plus twice the spatial-kernel amplitude equals one. Researchers modeling Information-Limited Gravity Fourier kernels cite this when normalizing the modification to the Newtonian source term. The proof is a one-line wrapper that scales the base half-rung budget by two and closes with linear arithmetic.
Claim. $2J(φ) + 2C = 1$, where $J(φ) = φ - 3/2$ is the first-rung cost penalty and $C = φ^{-2}$ is the kernel amplitude.
background
The ILG module formalizes the Fourier-space kernel $w_ker(k) = 1 + C (k_0/k)^α$ with amplitude $C = φ^{-2} ≈ 0.382$ and exponent $α ≈ 0.191$. Jphi_penalty is defined as $φ - 3/2$, the cost penalty for crossing the first φ-rung. C_kernel is defined as $φ^{-2}$, the spatial-kernel amplitude that supplies the complementary saving from finite-latency closure. The module states that the algebraic identity $J(φ) + φ^{-2} = 1/2$ follows from $φ^2 = φ + 1$ alone, making the two terms complementary contributions to the half-rung interval.
proof idea
The proof invokes the sibling half_rung_budget lemma establishing the undoubled form Jphi_penalty + C_kernel = 1/2, then applies linarith to obtain the doubled identity.
why it matters
This identity selects $C = φ^{-2}$ as the structurally forced value inside the half-rung budget, resolving the factor-of-$φ^{1/2}$ discrepancy between the entropy-paper value and the earlier $φ^{-3/2}$ account. It supplies the normalization for the ILG spatial kernel and aligns with the Recognition Science forcing chain in which phi is the self-similar fixed point. The declaration closes the structural core of the module without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.