Jphi_penalty
plain-language theorem explainer
Jphi_penalty defines the first-rung J-cost penalty as phi minus 3/2. Researchers deriving the ILG spatial kernel amplitude cite this when establishing the half-rung budget identity J(phi) + C = 1/2. The definition is a direct assignment from the closed-form evaluation of the J-function at the golden ratio.
Claim. The first-rung J-cost penalty is defined by $J_φ := φ - 3/2$, where $φ$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The ILG module formalizes the spatial-kernel amplitude $C = φ^{-2}$ in the Fourier modification $w_{ker}(k) = 1 + C · (k_0/k)^α$. The half-rung budget identity states that the cost penalty for crossing one φ-rung plus the cost-saving from finite-latency closure equals 1/2. Jphi_penalty supplies the explicit value of that penalty as φ - 3/2.
proof idea
This declaration is a direct definition setting Jphi_penalty equal to phi minus 3/2. No lemmas or tactics are applied; the form follows immediately from the J-function evaluated at phi.
why it matters
This supplies the J(φ) term required by the half-rung budget theorem, which forces C = 2 - phi as the unique kernel amplitude. It appears in half_rung_budget, C_is_complement_of_Jphi, and the master certificate ILGSpatialKernelCert. In the Recognition Science framework it connects to J-uniqueness (T5) and the phi fixed point (T6), closing the structural ambiguity between prior accounts of C.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.