phi_plus_inv
The golden ratio φ satisfies φ + φ^{-1} = √5. Researchers deriving J-costs or mass ladders in Recognition Science cite this algebraic identity to simplify expressions at the self-similar fixed point. The proof is a short tactic sequence that unfolds the definition of φ, applies field simplification and ring normalization, then invokes the square-root squaring identity to reach equality.
claimLet φ denote the golden ratio. Then φ + 1/φ = √5.
background
The Inequalities module collects fundamental algebraic lemmas that support the Recognition Science framework. The golden ratio φ is the positive fixed point of the self-similar forcing step (T6) and enters the J-cost definition J(x) = (x + x^{-1})/2 - 1. Upstream structures include the Constants bundle from CPM.LawOfExistence, which packages RS-native constants, and the cost functions from MultiplicativeRecognizerL4 and ObserverForcing that derive recognition costs from positive-ratio comparators.
proof idea
The proof unfolds the definition of φ from Constants. It introduces positivity of 5 and a non-zero denominator via norm_num and linarith. Field_simp and ring_nf reduce the expression, after which rw [Real.sq_sqrt] followed by ring closes the equality.
why it matters in Recognition Science
This identity is applied directly by J_cost_phi to obtain J(φ) = (√5 - 2)/2 and by the YangMillsMassGap theorems Jcost_phi_exact and phi_plus_inv for the exact closed form. It supplies the algebraic step required for T5 J-uniqueness and the phi fixed point, enabling the eight-tick octave and the mass formula on the phi-ladder.
scope and limits
- Does not prove uniqueness of the golden ratio among quadratic irrationals.
- Does not extend the identity to complex or negative arguments.
- Does not supply numerical bounds or approximation error estimates.
- Does not connect the identity to empirical measurements or physical units.
Lean usage
rw [phi_plus_inv]formal statement (Lean)
109theorem phi_plus_inv : φ + 1/φ = Real.sqrt 5 := by
proof body
Tactic-mode proof.
110 unfold φ Constants.phi
111 have hroot_pos : (0 : ℝ) < 5 := by norm_num
112 have hroot_ne : Real.sqrt 5 + 1 ≠ 0 := by
113 have := Real.sqrt_nonneg 5
114 linarith
115 field_simp
116 ring_nf
117 rw [Real.sq_sqrt (le_of_lt hroot_pos)]
118 ring
119
120/-- J-cost of φ -/