phi_inv
plain-language theorem explainer
The golden ratio satisfies the reciprocal identity 1/φ = φ - 1. Researchers deriving J-costs along the phi-ladder or simplifying self-similar fixed-point expressions cite this identity repeatedly. The proof unfolds the explicit definition of φ as (1 + sqrt(5))/2, confirms the denominator is nonzero via positivity of sqrt(5), and closes the equation with field simplification plus linear arithmetic.
Claim. $1/φ = φ - 1$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The PhiRing module defines φ explicitly as (1 + Real.sqrt 5)/2 and develops its algebraic closure properties inside Z[φ]. The upstream lemma sqrt5_pos states that sqrt(5) > 0, which is invoked to guarantee φ > 0 and to rule out division by zero. Parallel statements of the same identity appear in Inequalities.phi_inv and PhiForcing.phi_inv, each derived from the quadratic relation φ² = φ + 1.
proof idea
The tactic proof first unfolds the definition of φ. It then constructs a subproof that the denominator (1 + sqrt(5))/2 is nonzero by appealing to sqrt5_pos and linarith. After recording (sqrt 5)² = 5, the script applies field_simp on the cleared equation and finishes with nlinarith.
why it matters
This identity is applied directly in PhiForcing.J_phi to obtain J(φ) = φ - 3/2 and in LexiconRatio to express the active fraction as phi_inv. It supports the self-similar fixed-point step (T6) in the forcing chain and the J-uniqueness formula (T5). Downstream results in PhiEmergence and Linguistics reuse it for conservation identities on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.