paretoExponent_band
plain-language theorem explainer
The Pareto exponent α in the Recognition Science wealth distribution satisfies 1.61 < α < 1.62. Economists fitting power-law tails to wealth data would cite this interval to anchor the prediction α = 1 + φ^{-1}. The proof is a term reduction that substitutes the equality α = φ and invokes the pre-established numerical bounds on the golden ratio.
Claim. $1.61 < 1 + φ^{-1} < 1.62$, where φ is the golden ratio satisfying φ² = φ + 1.
background
The module WealthDistributionFromSigma derives Pareto wealth tails from sigma conservation. The Pareto exponent is defined as α := 1 + φ^{-1}. The upstream theorem paretoExponent_eq_phi shows this equals φ itself via the identity 1/φ = φ - 1. Module documentation states the RS prediction α ≈ 1.618 and requires a Lean proof that 1 + 1/φ lies in (1.61, 1.63); the present result tightens the upper bound. Upstream lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo establish the numerical bounds on φ by direct comparison with √5.
proof idea
The term proof first rewrites the target using paretoExponent_eq_phi to replace the exponent with φ. It then discharges the conjunction by applying the pair of lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo.
why it matters
This theorem supplies the exponent_band field inside the wealthDistributionCert certificate that packages the RS wealth prediction. It closes the numerical verification step requested in the module documentation for the interval around 1 + 1/φ. The bound links the economic application to the phi-ladder constants and the self-similar fixed point forced by the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.