IndisputableMonolith.Economics.LaborEconomicsFromRS

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Labor Economics from RS — C Economics
   6
   7Five canonical labor market theories (human capital, search, efficiency
   8wages, insider-outsider, implicit contracts) = configDim D = 5.
   9
  10In RS: labor equilibrium = J = 0 (wage = marginal recognition cost).
  11Labor market frictions: J > 0 (recognition mismatch).
  12
  13Lean: 5 theories.
  14
  15Lean status: 0 sorry, 0 axiom.
  16-/
  17
  18namespace IndisputableMonolith.Economics.LaborEconomicsFromRS
  19open Cost
  20
  21inductive LaborMarketTheory where
  22  | humanCapital | searchFriction | efficiencyWages | insiderOutsider | implicitContracts
  23  deriving DecidableEq, Repr, BEq, Fintype
  24
  25theorem laborMarketTheoryCount : Fintype.card LaborMarketTheory = 5 := by decide
  26
  27/-- Labor equilibrium: J = 0. -/
  28theorem labor_equilibrium : Jcost 1 = 0 := Jcost_unit0
  29
  30/-- Market friction: J > 0. -/
  31theorem market_friction {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  32    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  33
  34structure LaborEconomicsCert where
  35  five_theories : Fintype.card LaborMarketTheory = 5
  36  equilibrium : Jcost 1 = 0
  37  friction : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  38
  39def laborEconomicsCert : LaborEconomicsCert where
  40  five_theories := laborMarketTheoryCount
  41  equilibrium := labor_equilibrium
  42  friction := market_friction
  43
  44end IndisputableMonolith.Economics.LaborEconomicsFromRS
  45