paretoExponent_eq_phi
plain-language theorem explainer
The declaration proves that the Pareto exponent in wealth distributions equals the golden ratio φ. Econophysicists modeling scale-free networks or inequality ceilings would cite this equality to anchor RS predictions. The proof is a one-line algebraic reduction that unfolds the definition and applies the inverse-phi identity followed by ring simplification.
Claim. The Pareto exponent defined by $1 + 1/φ$ equals $φ$.
background
The module Wealth Distribution from Sigma Conservation models Pareto tails P(W > w) ∝ w^(-α) with α ≈ 1.5-2. Recognition Science predicts α = 1 + 1/φ ≈ 1.618, which is the complementary-CDF form of the Zipf exponent 1/φ and matches the Gini ceiling proved elsewhere. The local definition sets paretoExponent := 1 + phi^{-1}. The upstream lemma inv_phi_eq states that 1/φ = φ - 1, obtained from the quadratic phi_sq_eq by field simplification and linear arithmetic.
proof idea
The term proof unfolds paretoExponent to expose 1 + phi^{-1}, rewrites the inverse term via inv_phi_eq to reach 1 + (phi - 1), and closes with ring to obtain phi.
why it matters
This supplies the exact value used by paretoExponent_band to certify the interval (1.61, 1.62) and by wealthDistributionCert to package the full certificate. It realizes the RS prediction for the Pareto exponent under sigma conservation, consistent with the self-similar fixed point T6 and the phi-ladder mass formula. No open scaffolding remains in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.