MobilityThreshold
plain-language theorem explainer
The declaration sets the mobility threshold to the J-cost evaluated at the golden ratio. Economists analyzing the Great Gatsby Curve would cite it as the structural boundary separating high-mobility economies from trapped-underclass regimes. The definition is a direct assignment of the J-cost function at phi with no additional steps.
Claim. Let the mobility threshold be the real number given by the J-cost function evaluated at the golden ratio: $J(φ)$.
background
The J-cost function measures the deviation cost for multiplicative recognizers on positive ratios and equals $(x + x^{-1})/2 - 1$. In this module the per-decile J-cost is computed on the ratio of observed income share to equal share, and the Gini coefficient arises as the integral of these J-costs. The module states that the critical value separating mobility regimes is $J(φ) ∈ (0.11, 0.13)$, matching the empirical Great Gatsby Curve reported by Krueger and Chetty.
proof idea
This is a one-line definition that directly assigns the value of the J-cost function at phi to the mobility threshold.
why it matters
The definition supplies the threshold used by the regime classifiers IsHighInequalityRegime and IsHighMobilityRegime and is certified inside LorenzCurveCert to lie in (0.11, 0.13). It fills the structural prediction that Gini ≤ J(φ) implies higher intergenerational mobility, invoking the J-uniqueness property and the self-similar fixed point phi from the forcing chain. It touches the open question of broader empirical validation across additional countries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.