Jphi_penalty_eq_Jcost_phi
plain-language theorem explainer
The theorem shows that the first-rung J-cost penalty equals the J-cost function evaluated at the golden ratio φ. Researchers deriving the Information-Limited Gravity spatial kernel would cite this to fix the amplitude C at φ^{-2}. The proof is a short algebraic reduction that unfolds both sides and applies field simplification together with the quadratic identity for φ.
Claim. $J_1 = J(φ)$ where $J_1 := φ - 3/2$ is the first-rung J-cost penalty and $J(x) = (x + x^{-1})/2 - 1$ is the J-cost function.
background
The module derives the ILG spatial-kernel amplitude from the Recognition framework. The Fourier modification takes the form $w_ker(k) = 1 + C (k_0/k)^α$ with $α = (1 - φ^{-1})/2$. The first-rung J-cost penalty is defined directly as $Jphi_penalty := φ - 3/2$. This quantity satisfies the half-rung budget identity $J(φ) + φ^{-2} = 1/2$, which forces $C = φ^{-2} = 2 - φ$ once the quadratic relation $φ^2 = φ + 1$ is used. The upstream lemma phi_sq_eq supplies exactly that quadratic identity.
proof idea
The term proof unfolds the definitions of Jphi_penalty and Cost.Jcost, records that φ is nonzero, invokes the upstream lemma phi_sq_eq, then applies field_simp followed by nlinarith on the positive square and the square identity.
why it matters
The result selects $C = φ^{-2}$ over the competing value $φ^{-3/2}$ by exhibiting the complementary half-rung budget $J(φ) + C = 1/2$. It therefore anchors the spatial-kernel amplitude inside the Recognition Science forcing chain (T5–T8) and supplies the concrete value used by the sibling identities C_kernel_eq_two_minus_phi and C_is_complement_of_Jphi. The declaration closes one source of prior ambiguity between the entropy-paper and Gravity_From_Recognition accounts of the kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.