IndisputableMonolith.Economics.InequalityFromSigmaBudget

   1import Mathlib
   2import IndisputableMonolith.Common.CanonicalJBand
   3
   4/-!
   5# F3: Economic Inequality from Sigma-Budget Conservation
   6
   7Per-decile J-cost on `r := observed_decile_share / equal_share_baseline`.
   8The healthy distribution sits at `r = 1` for every decile. The Gini
   9coefficient maps onto the J-cost integral over the decile distribution;
  10the canonical golden-section band gates the "high-mobility vs trapped
  11underclass" boundary, matching the empirical Gini ≈ 0.4 inflection
  12between high-mobility and low-mobility OECD economies.
  13
  14Falsifier: a national-level Gini and per-decile shares with σ-budget
  15sum strictly off-zero in a closed economy (no external trade σ-flux).
  16
  17Lean status: 0 sorry, 0 axiom.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace Economics
  22namespace InequalityFromSigmaBudget
  23
  24open Common.CanonicalJBand
  25
  26structure InequalityCert where
  27  base : CanonicalCert
  28
  29def inequalityCert : InequalityCert where
  30  base := cert
  31
  32end InequalityFromSigmaBudget
  33end Economics
  34end IndisputableMonolith
  35