phi_inv_eq
plain-language theorem explainer
The golden ratio reciprocal satisfies φ⁻¹ = φ − 1 for φ = (1 + √5)/2. Interval bounds and mass-gap calculations cite the identity to obtain 0.618 < φ⁻¹ < 0.6186 and to sum the geometric series. A one-line term proof rewrites the Mathlib inverse definition, unfolds goldenRatio and goldenConj, then reduces by ring.
Claim. Let $φ = (1 + √5)/2$. Then $φ^{-1} = φ - 1$.
background
The module supplies algebraic bounds on the golden ratio using the quadratic relation φ² = φ + 1. It starts from the concrete inequalities 2.236² < 5 < 2.237² to locate √5 and hence φ in (1.618, 1.6185), with tighter decimal versions obtained by the same method. The local setting is therefore numeric verification of the exact algebraic identities needed for the phi-ladder.
proof idea
The term proof first rewrites with inv_goldenRatio, unfolds the Mathlib definitions of goldenRatio and goldenConj, then closes the equality by ring.
why it matters
The identity is invoked by phi_inv_gt and phi_inv_lt to close the interval (0.618, 0.6186) and by phi_series_sum to evaluate the geometric sum to φ. It supplies the exact algebraic step required for the phi-ladder mass formula and for the J-uniqueness property T5 in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.