mobility_threshold_band
plain-language theorem explainer
The theorem establishes that the mobility threshold J(φ) lies in the open interval (0.11, 0.13). Economists modeling intergenerational mobility and the Great Gatsby Curve would cite it to fix the structural boundary between high-mobility and trapped-underclass regimes. The proof is a short tactic sequence that substitutes the squared form of the J-cost function and applies the tight numerical bounds on φ with linear arithmetic.
Claim. $0.11 < J(φ) < 0.13$, where $J(x) = (x-1)^2 / (2x)$ and $φ$ is the golden ratio.
background
The module derives Lorenz curves and Gini coefficients from sigma-budget conservation by assigning a J-cost to each decile based on its share ratio relative to equal division. The Gini coefficient equals the integral of these J-costs over the deciles. MobilityThreshold is introduced as the J-cost evaluated at the golden ratio φ, serving as the canonical quantum that marks the transition from high-mobility to trapped-underclass regimes.
proof idea
The proof unfolds the definition of MobilityThreshold, applies the lemma Jcost_eq_sq using phi_ne_zero, inserts the bounds phi_gt_onePointSixOne and phi_lt_onePointSixTwo, and concludes the two inequalities via lt_div_iff₀ followed by nlinarith.
why it matters
This result populates the threshold_band component of lorenzCurveCert, which assembles the full certificate for Lorenz-curve inequality properties. It supplies the quantitative anchor for the module's claim that Gini values below J(φ) correspond to structurally higher mobility, consistent with the observed Great Gatsby Curve. The declaration closes one link in the chain connecting the J-cost function to economic observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.