IndisputableMonolith.Economics.LorenzCurveFromSigmaBudget

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Lorenz Curve and Gini from Sigma-Budget Conservation
   7
   8Per-decile J-cost on `r_k := observed_decile_k_share / equal_share`.
   9The Gini coefficient is structurally the integral of J-costs across
  10deciles. The critical value for high-mobility vs trapped-underclass
  11corresponds to Gini ≈ `J(φ) ∈ (0.11, 0.13)` on the income-share
  12deviation ratio — the same canonical quantum that bounds pathology
  13thresholds across every other domain.
  14
  15The structural prediction: countries with Gini ≤ J(φ) have structurally
  16higher intergenerational mobility than those with Gini > J(φ). This
  17matches the empirical Great Gatsby Curve (Krueger 2012; Chetty 2014):
  18the US, UK, Brazil, Mexico all sit above the canonical band; the Nordic
  19countries and much of East Asia sit at or below it.
  20
  21Lean status: 0 sorry, 0 axiom.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Economics
  26namespace LorenzCurveFromSigmaBudget
  27
  28open Constants Cost
  29
  30noncomputable section
  31
  32/-- Per-decile J-cost on the income-share ratio. -/
  33def decileCost (r : ℝ) : ℝ := Cost.Jcost r
  34
  35theorem decileCost_zero_at_equal : decileCost 1 = 0 := Cost.Jcost_unit0
  36
  37theorem decileCost_reciprocal_symm {r : ℝ} (hr : 0 < r) :
  38    decileCost r = decileCost r⁻¹ := Cost.Jcost_symm hr
  39
  40theorem decileCost_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ decileCost r :=
  41  Cost.Jcost_nonneg hr
  42
  43theorem decileCost_pos_off_equal {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  44    0 < decileCost r := Cost.Jcost_pos_of_ne_one r hr hne
  45
  46/-- High-mobility/trapped boundary = canonical golden-section quantum. -/
  47def MobilityThreshold : ℝ := Cost.Jcost phi
  48
  49/-- A country economy is in the trapped-underclass regime iff its
  50inequality-adjusted decile cost (Gini proxy) meets or exceeds the threshold. -/
  51def IsHighInequalityRegime (gini_proxy : ℝ) : Prop :=
  52  MobilityThreshold ≤ gini_proxy
  53
  54/-- A country economy is in the high-mobility regime iff it sits below. -/
  55def IsHighMobilityRegime (gini_proxy : ℝ) : Prop :=
  56  gini_proxy < MobilityThreshold
  57
  58theorem regimes_exclusive {g : ℝ} :
  59    ¬ (IsHighMobilityRegime g ∧ IsHighInequalityRegime g) := by
  60  rintro ⟨h_lt, h_ge⟩
  61  exact (lt_irrefl _) (lt_of_lt_of_le h_lt h_ge)
  62
  63theorem mobility_threshold_band :
  64    0.11 < MobilityThreshold ∧ MobilityThreshold < 0.13 := by
  65  unfold MobilityThreshold
  66  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  67  rw [Cost.Jcost_eq_sq hphi_ne]
  68  have h_lo : (1.61 : ℝ) < phi := Constants.phi_gt_onePointSixOne
  69  have h_hi : phi < (1.62 : ℝ) := Constants.phi_lt_onePointSixTwo
  70  have hpos : (0 : ℝ) < 2 * phi := by
  71    have : (0 : ℝ) < phi := Constants.phi_pos
  72    linarith
  73  refine ⟨?lo, ?hi⟩
  74  · rw [lt_div_iff₀ hpos]; nlinarith [h_lo, h_hi]
  75  · rw [div_lt_iff₀ hpos]; nlinarith [h_lo, h_hi]
  76
  77structure LorenzCurveCert where
  78  equal_zero : decileCost 1 = 0
  79  reciprocal_symm : ∀ {r : ℝ}, 0 < r → decileCost r = decileCost r⁻¹
  80  cost_nonneg : ∀ {r : ℝ}, 0 < r → 0 ≤ decileCost r
  81  threshold_band :
  82    0.11 < MobilityThreshold ∧ MobilityThreshold < 0.13
  83  regimes_exclusive :
  84    ∀ {g : ℝ}, ¬ (IsHighMobilityRegime g ∧ IsHighInequalityRegime g)
  85
  86/-- Lorenz-curve inequality certificate. -/
  87def lorenzCurveCert : LorenzCurveCert where
  88  equal_zero := decileCost_zero_at_equal
  89  reciprocal_symm := decileCost_reciprocal_symm
  90  cost_nonneg := decileCost_nonneg
  91  threshold_band := mobility_threshold_band
  92  regimes_exclusive := regimes_exclusive
  93
  94end
  95end LorenzCurveFromSigmaBudget
  96end Economics
  97end IndisputableMonolith
  98