inv_phi_eq
plain-language theorem explainer
The golden ratio satisfies 1/φ = φ - 1. Economists deriving the Pareto exponent for wealth distributions under sigma conservation cite this algebraic identity. The proof reduces the claim to the quadratic φ² = φ + 1 by field simplification and linear arithmetic.
Claim. The golden ratio satisfies $1/φ = φ - 1$.
background
The module derives Pareto wealth distributions from sigma conservation, predicting the exponent α = 1 + 1/φ. The golden ratio φ is the positive root of x² - x - 1 = 0, so φ² = φ + 1 holds by the upstream lemma phi_sq_eq in Constants and in PhiLadderLattice. The module also imports phi_ne_zero to guarantee the reciprocal is well-defined. This identity supplies the exact algebraic link between the self-similar fixed point and the predicted Pareto exponent.
proof idea
The term proof invokes phi_sq_eq to obtain φ² = φ + 1, applies field_simp with phi_ne_zero to clear the denominator, and closes with linarith.
why it matters
The result is used by paretoExponent_eq_phi to conclude that the Pareto exponent equals φ and by the certificate wealthDistributionCert. It supplies the missing algebraic step that converts the golden-ratio fixed point (T5-T6) into the concrete prediction α = 1 + 1/φ ≈ 1.618 inside the economics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.