IsHighInequalityRegime
plain-language theorem explainer
An economy enters the trapped-underclass regime once its Gini proxy reaches or exceeds the MobilityThreshold value J(φ). Researchers analyzing intergenerational mobility via the Great Gatsby Curve would cite this boundary to distinguish high-mobility from trapped states. The declaration encodes the comparison directly from the pre-defined threshold obtained by evaluating the J-cost at the golden ratio.
Claim. An economy is in the high-inequality regime if and only if its Gini proxy $g$ satisfies $g ≥ J(φ)$, where $J$ denotes the recognition cost function and $φ$ the golden ratio.
background
In this module the Gini coefficient arises as the integral of per-decile J-costs, with each decile ratio defined as observed share divided by equal share. The module document states that the critical value for high-mobility versus trapped-underclass corresponds to Gini ≈ J(φ) in (0.11, 0.13), the same quantum bounding pathology thresholds in other domains. This yields the structural prediction that countries with Gini ≤ J(φ) have higher intergenerational mobility, matching observations for Nordic countries and East Asia below the band and the US, UK, Brazil above it. The MobilityThreshold is set to the J-cost evaluated at φ, providing the canonical golden-section quantum as the regime boundary.
proof idea
This definition is a one-line wrapper that applies the MobilityThreshold constant, which equals the J-cost at the golden ratio.
why it matters
The definition feeds the LorenzCurveCert structure, which certifies equal-zero, reciprocal symmetry, nonnegativity, and the threshold band 0.11 < MobilityThreshold < 0.13, and the regimes_exclusive theorem proving the regimes cannot overlap. It implements the module's core claim linking sigma-budget conservation to the Great Gatsby Curve. The threshold connects to the Recognition Science framework through the J-uniqueness property and the self-similar fixed point φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.