phi_inv
plain-language theorem explainer
The identity 1/φ = φ − 1 holds for the golden ratio satisfying φ² = φ + 1. Researchers deriving J-costs or scale ratios in self-similar discrete ledgers cite this algebraic step. The proof is a short tactic sequence that invokes the defining quadratic, applies field simplification, and closes with linear arithmetic under positivity.
Claim. For the golden ratio φ satisfying φ² = φ + 1, the reciprocal satisfies φ^{-1} = φ − 1.
background
The module shows that self-similarity on a discrete ledger with J-cost forces the scale ratio to φ. J(x) is the cost (x + x^{-1})/2 − 1. The upstream theorem phi_equation states φ² = φ + 1 and is the sole algebraic input here.
proof idea
The tactic proof invokes phi_equation, rewrites the quadratic divided by φ, applies field_simp twice to isolate the reciprocal, then uses nlinarith with positivity and linarith to finish.
why it matters
This identity is applied directly in the same module to obtain J(φ) = φ − 3/2 and is reused in PhiEmergence and lexicon-ratio calculations. It supplies the algebraic simplification required for T6, the self-similar fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.