phi_inv_eq
plain-language theorem explainer
The golden ratio satisfies the algebraic identity 1/φ = φ - 1. Researchers deriving series sums or mass-gap expressions in Recognition Science cite this relation when working with the phi-ladder. The proof is a one-line wrapper that invokes the phi_inv theorem from the Inequalities module.
Claim. $1/φ = φ - 1$
background
The PhiEmergence module derives φ from J-cost minimization, where J(x) = (x + x^{-1})/2 - 1 is the recognition cost. The golden ratio is the positive self-similar fixed point satisfying φ² = φ + 1. Upstream results in Inequalities.phi_inv and PhiForcing.phi_inv establish the identity from this quadratic equation together with φ > 0.
proof idea
This is a one-line wrapper that applies Inequalities.phi_inv. The underlying lemma starts from φ² = φ + 1, multiplies through by 1/φ, and rearranges to obtain the reciprocal form.
why it matters
The identity feeds phi_series_sum, which evaluates the geometric series of powers of 1/φ as equaling φ. It is also invoked in YangMillsMassGap.phi_inv_eq and phi_plus_inv for the mass-gap calculation. It supplies the basic algebraic step supporting the self-similar fixed point (T6) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.