wealthDistributionCert
The wealth distribution certificate certifies that the Pareto exponent of wealth equals the golden ratio φ and lies in (1.61, 1.62), together with the identity 1/φ = φ - 1. Economists modeling scale-free wealth tails under sigma conservation would cite it to anchor the RS prediction α = 1 + 1/φ ≈ 1.618. The definition is assembled by direct field assignment from three supporting theorems on the exponent equality, numerical band, and inverse-phi relation.
claimThe wealth distribution certificate is the structure asserting that the Pareto exponent equals the golden ratio φ, satisfies 1.61 < Pareto exponent < 1.62, and obeys the identity φ^{-1} = φ - 1.
background
The module formalizes wealth distribution under sigma conservation in the Recognition Science framework. It treats the complementary cumulative distribution P(W > w) ∝ w^{-α} and derives the RS prediction that the Pareto exponent α equals 1 + 1/φ ≈ 1.618 (equivalently φ, since 1/φ = φ - 1). The local setting is F3 Economics Depth, which also notes the Zipf exponent 1/φ ≈ 0.618 and the Gini ceiling 1/φ proved elsewhere.
proof idea
The definition constructs the certificate by assigning the three fields of the WealthDistributionCert structure. It sets the exponent-equality field to the theorem that unfolds the Pareto exponent definition and reduces via the inverse-phi identity, the band field to the theorem that rewrites the equality and applies the golden-ratio bounds, and the inverse-phi field to the direct algebraic proof from the square equation.
why it matters in Recognition Science
This definition supplies the certified object that closes the Lean claim 1 + 1/φ ∈ (1.61, 1.63) with zero sorry, as stated in the module documentation. It realizes the RS prediction for Pareto tails in wealth and network degree distributions, linking directly to the phi-ladder and the eight-tick octave structure. No downstream uses are recorded yet, leaving open its integration into broader inequality or sigma-conservation theorems.
scope and limits
- Does not derive the Pareto form from sigma conservation axioms.
- Does not compute explicit wealth quantiles or sample distributions.
- Does not address empirical deviations from pure power-law tails.
- Does not prove that φ is the unique exponent compatible with the model.
formal statement (Lean)
51noncomputable def wealthDistributionCert : WealthDistributionCert where
52 exponent_eq_phi := paretoExponent_eq_phi
proof body
Definition body.
53 exponent_band := paretoExponent_band
54 inv_phi := inv_phi_eq
55
56end IndisputableMonolith.Economics.WealthDistributionFromSigma