Jphi_penalty_eq_phi_minus_three_halves
plain-language theorem explainer
The first-rung J-cost penalty equals φ minus three-halves. Workers deriving the ILG spatial kernel amplitude cite this closed form to close the half-rung budget identity. The proof is a one-line reflexivity that matches the definition directly.
Claim. The first-rung J-cost penalty equals $φ - 3/2$.
background
The ILG spatial kernel module derives the amplitude C in the Fourier modification w_ker(k) = 1 + C · (k₀/k)^α from the half-rung budget. The first-rung J-cost penalty is the J-cost incurred when crossing one φ-rung on the ladder. Upstream results define cost as the J-cost of a recognition event and set rung to 1 in the relevant anchor and fermion contexts. The module document states that J(φ) + φ^{-2} = 1/2 follows from φ² = φ + 1 alone, with the penalty term written explicitly as φ - 3/2.
proof idea
This is a one-line wrapper that applies reflexivity to the definition of the first-rung J-cost penalty.
why it matters
The identity supplies the left-hand side of the half-rung budget theorem, which forces C = φ^{-2} as the unique amplitude consistent with the first-rung penalty. It completes the structural step that selects the entropy-paper value over the alternative φ^{-3/2} in the ILG derivation, aligning with the Recognition Science phi-ladder and the T5 J-uniqueness landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.