IsHighMobilityRegime
plain-language theorem explainer
This definition classifies an economy as high-mobility when its Gini proxy falls strictly below the J-cost evaluated at the golden ratio. Economists working on intergenerational mobility and the Great Gatsby Curve would cite it to separate regimes in sigma-budget models. The definition is a direct one-line comparison to the precomputed MobilityThreshold.
Claim. An economy with Gini proxy $g$ is in the high-mobility regime if and only if $g < J(φ)$, where $J$ is the J-cost function and $φ$ the golden ratio.
background
The module derives Lorenz curves and Gini coefficients from per-decile J-costs on deviation ratios $r_k =$ observed decile share over equal share. The Gini coefficient equals the integral of these J-costs across deciles. The high-mobility versus trapped-underclass boundary is set at the canonical value $J(φ) ∈ (0.11, 0.13)$, the same quantum that bounds pathology thresholds in other Recognition Science domains. Upstream, MobilityThreshold is defined as the J-cost of $φ$, described as the high-mobility/trapped boundary equal to the canonical golden-section quantum.
proof idea
One-line definition that directly compares the input Gini proxy against the MobilityThreshold constant.
why it matters
This definition supplies the predicate used in LorenzCurveCert to certify the threshold band $0.11 <$ MobilityThreshold $< 0.13$ and in regimes_exclusive to prove the two regimes are mutually exclusive. It applies the Recognition Science J-cost (T5) to economics, reproducing the structural prediction that Gini ≤ J(φ) yields higher mobility, consistent with Nordic versus US/UK observations. The declaration closes the regime separation step in the sigma-budget conservation argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.