J_cost_phi
plain-language theorem explainer
The equality establishes that the J-cost at the golden ratio equals (√5 − 2)/2. Researchers anchoring the phi-ladder or computing base costs in Recognition Science cite this identity. The proof is a direct algebraic reduction that substitutes the φ-sum identity and simplifies.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. Then $J(φ) = (√5 - 2)/2$, where $φ$ satisfies $φ + φ^{-1} = √5$.
background
The Inequalities module supplies basic lemmas for the Recognition Science derivations. The J-cost is the function $J(x) = (x + x^{-1})/2 - 1$. The upstream theorem phi_plus_inv states that $φ + 1/φ = √5$.
proof idea
The term proof applies the phi_plus_inv lemma to replace $φ + 1/φ$ by √5, then uses the ring tactic to confirm the arithmetic identity.
why it matters
J_at_phi in PhiEmergence invokes this result to fix the J-cost at the self-similar point. It supports T5 J-uniqueness and T6 forcing of phi as the fixed point in the UnifiedForcingChain. The negative value aligns with the Berry creation threshold at $φ^{-1}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.