The golden ratio obeys the reciprocal identity φ^{-1} = φ - 1. Researchers on self-similar discrete ledgers with J-cost cite it when simplifying scale ratios or deriving costs. The tactic proof starts from the quadratic φ² = φ + 1, divides by φ, and closes with field simplification plus linear arithmetic.
claimThe reciprocal of the golden ratio satisfies $φ^{-1} = φ - 1$.
background
The PhiForcing module shows that self-similarity of a discrete ledger under J-cost forces the scale ratio to be the golden ratio. J is the cost function J(x) = (x + x^{-1})/2 - 1 drawn from the Law of Existence. The upstream theorem phi_equation supplies the defining relation φ² = φ + 1.
proof idea
The proof invokes phi_equation to obtain φ² = φ + 1, divides both sides by φ, applies field_simp to reach φ = 1 + φ^{-1}, and finishes with linarith.
why it matters in Recognition Science
This identity is invoked directly in J_phi to obtain J(φ) = φ - 3/2 and reappears in PhiEmergence and lexicon-ratio calculations. It realizes the self-similar fixed point (T6) that selects φ in the forcing chain.
scope and limits
Does not prove existence or positivity of φ.
Applies only to the golden ratio root of x² = x + 1.
Does not address negative or complex arguments.
Lean usage
rw [phi_inv]
formal statement (Lean)
110theorem phi_inv : φ⁻¹ = φ - 1 := by
proof body
Tactic-mode proof.
111 have hphi_ne : φ ≠ 0 := phi_pos.ne' 112 have h := phi_equation 113 -- From φ² = φ + 1, divide by φ: φ = 1 + 1/φ, so 1/φ = φ - 1 114 have h1 : φ^2 / φ = (φ + 1) / φ := by rw [h] 115 have h2 : φ = 1 + φ⁻¹ := by 116 field_simp at h1 117 field_simp 118 nlinarith [phi_pos] 119 linarith 120 121/-- J(φ) = (2φ - 1)/2 - 1 = φ - 3/2 (cost of the golden ratio). 122 Note: J(φ) ≠ 0 because φ ≠ 1. -/
used by (15)
From the project-wide theorem graph. These declarations reference this one in their body.