J_at_phi
plain-language theorem explainer
The equality shows that J-cost at the golden ratio φ equals (√5 - 2)/2. Researchers modeling self-similar recognition systems cite this to fix the minimal nonzero coherence cost on the φ-ladder. The proof is a direct one-line wrapper invoking the J_cost_phi lemma from Inequalities.
Claim. The J-cost at the golden ratio φ satisfies $J(φ) = (φ + φ^{-1})/2 - 1 = (√5 - 2)/2$.
background
The φ-Emergence module derives the golden ratio from J-cost minimization under self-similarity. J-cost is the function J(x) = (x + x^{-1})/2 - 1 for positive x, which quantifies the coherence cost of a recognition event as defined via ObserverForcing.cost and the derivedCost on multiplicative recognizers. The local setting is the emergence of φ as the fixed point that minimizes nonzero J-cost on the ladder of self-similar ratios.
proof idea
The proof is a one-line wrapper that applies the J_cost_phi theorem from the Inequalities module. That lemma rewrites the left-hand side using phi_plus_inv and closes the identity by ring normalization.
why it matters
This result supplies the exact value of J(φ) that feeds into canonicalLayerSysPlus in RecognitionCategory and the H_StableIffPhiLadder hypothesis asserting stable positions coincide with the φ-ladder. It realizes the T6 step in the forcing chain where φ is forced as the self-similar fixed point, bridging the Recognition Composition Law to discrete quantization on the φ-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.