WealthDistributionCert
plain-language theorem explainer
WealthDistributionCert bundles three properties for the Pareto exponent in wealth distributions: equality to phi, membership in the open interval (1.61, 1.62), and the relation phi inverse equals phi minus one. Modelers of scale-free networks or empirical wealth tails would cite it to anchor the RS prediction alpha equals 1 plus 1 over phi. The declaration is a direct record definition that packages the upstream paretoExponent value with the inv_phi relation.
Claim. A record certifying that the Pareto exponent satisfies $1 + 1/phi = phi$, $1.61 < 1 + 1/phi < 1.62$, and $phi^{-1} = phi - 1$.
background
The module treats wealth as following a Pareto complementary CDF with exponent alpha approximately 1.5 to 2. Recognition Science fixes this exponent at 1 plus 1 over phi, which equals phi from the quadratic phi squared equals phi plus one. The upstream paretoExponent definition sets the value to 1 plus phi inverse, and the supplied relation 1 over phi equals phi minus 1 follows immediately from that quadratic.
proof idea
Structure definition that directly assembles the three fields from the paretoExponent definition and the inv_phi_eq relation. No tactics or reductions are applied; it functions as a bundling record for the downstream wealthDistributionCert instance.
why it matters
The structure supplies the certified properties consumed by wealthDistributionCert, which constructs the concrete instance. It encodes the RS prediction for the Pareto exponent in the economics module, consistent with the self-similar fixed point phi and the forcing chain landmarks. It closes the band check for the interval around 1.618 while leaving empirical matching to separate validation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.