paretoExponent
plain-language theorem explainer
The definition sets the Pareto exponent α for wealth distributions to 1 plus the reciprocal of the golden ratio. Modelers of inequality or scale-free networks in Recognition Science cite it to obtain the predicted value near 1.618. It is introduced as a direct abbreviation that later algebraic steps reduce to phi itself.
Claim. The Pareto exponent is defined by α := 1 + φ^{-1}.
background
The module treats wealth as following a Pareto distribution whose complementary cumulative satisfies P(W > w) ∝ w^{-α}. The golden ratio φ obeys φ² = φ + 1, which rearranges to the identity 1/φ = φ - 1. This definition therefore places α at 1 + 1/φ. The local setting is sigma conservation in an economic network, which the module links to the same exponent that appears for degree distributions in scale-free graphs.
proof idea
The declaration is a direct noncomputable definition. No lemmas or tactics are invoked; the body simply equates the symbol to the expression 1 + φ^{-1}.
why it matters
The definition supplies the base quantity used by paretoExponent_eq_phi to prove equality with phi, by paretoExponent_band to establish the interval (1.61, 1.62), and by the WealthDistributionCert structure to certify the full set of distribution properties. It realizes the Recognition Science prediction α = 1 + 1/φ inside the F3 Economics depth and connects to the phi-ladder fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.