mobilityTransitionCost

formal source

  46theorem socialStratumCount_eq : socialStratumCount = 5 := rfl
  47
  48/-- J-cost on stratum mobility ratio. -/
  49def mobilityTransitionCost (achieved_status expected_status : ℝ) : ℝ :=
  50  Jcost (achieved_status / expected_status)
  51
  52theorem mobilityTransitionCost_at_stratum (s : ℝ) (h : s ≠ 0) :
  53    mobilityTransitionCost s s = 0 := by
  54  unfold mobilityTransitionCost; rw [div_self h]; exact Jcost_unit0
  55
  56theorem mobilityTransitionCost_nonneg (a e : ℝ) (ha : 0 < a) (he : 0 < e) :
  57    0 ≤ mobilityTransitionCost a e := by
  58  unfold mobilityTransitionCost; exact Jcost_nonneg (div_pos ha he)
  59
  60/-- One-step upward mobility cost (from rung k to k+1): J(φ). -/
  61def oneStepMobilityCost : ℝ := phi - 3 / 2
  62
  63theorem oneStepMobilityCost_eq_Jph : oneStepMobilityCost = Jcost phi :=
  64  Jcost_phi_val.symm
  65
  66theorem oneStepMobilityCost_pos : 0 < oneStepMobilityCost := by
  67  unfold oneStepMobilityCost; linarith [phi_gt_onePointSixOne]
  68
  69structure SocialStratificationCert where
  70  stratum_count : socialStratumCount = 5
  71  cost_at_stratum : ∀ s : ℝ, s ≠ 0 → mobilityTransitionCost s s = 0
  72  cost_nonneg : ∀ a e : ℝ, 0 < a → 0 < e → 0 ≤ mobilityTransitionCost a e
  73  mobility_cost_pos : 0 < oneStepMobilityCost
  74
  75noncomputable def cert : SocialStratificationCert where
  76  stratum_count := socialStratumCount_eq
  77  cost_at_stratum := mobilityTransitionCost_at_stratum
  78  cost_nonneg := mobilityTransitionCost_nonneg
  79  mobility_cost_pos := oneStepMobilityCost_pos