Jphi_penalty_eq_phi_minus_three_halves
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value of phi or its continued-fraction approximants.
- Does not extend the penalty formula to rungs beyond the first.
- Does not address the derivation of the kernel exponent alpha.
- Does not incorporate higher-order corrections from multi-channel factorization.
Lean usage
rw [Jphi_penalty_eq_phi_minus_three_halves, C_kernel_eq_two_minus_phi]formal statement (Lean)
144theorem Jphi_penalty_eq_phi_minus_three_halves :
145 Jphi_penalty = phi - 3 / 2 := rfl
proof body
Term-mode proof.
146
147/-- The first-rung J-cost penalty equals the J-cost evaluated at φ. -/