Jphi_penalty_eq_Jcost_phi
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 in Recognition Science
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.
scope and limits
- Does not derive the kernel exponent α.
- Does not address higher-rung penalties or multi-rung sums.
- Does not incorporate observational data or numerical fitting.
- Does not prove uniqueness of the kernel form beyond the half-rung budget.
formal statement (Lean)
148theorem Jphi_penalty_eq_Jcost_phi :
149 Jphi_penalty = Cost.Jcost phi := by
proof body
Term-mode proof.
150 unfold Jphi_penalty Cost.Jcost
151 have h_phi_ne : phi ≠ 0 := ne_of_gt phi_pos
152 have h_sq := phi_sq_eq
153 field_simp
154 nlinarith [sq_pos_of_pos phi_pos, h_sq]
155
156/-- **THE HALF-RUNG BUDGET IDENTITY.** `J(φ) + C = 1/2`, the structural
157 forcing of `C = φ⁻²` as the unique spatial-kernel amplitude
158 consistent with the first-rung cost penalty. -/