IndisputableMonolith.Economics.HealthEconomicsFromRS

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Health Economics from RS — E4 / E1 Applied
   6
   7Five canonical health economic analysis types (CEA, CBA, CUA, BIA, ROI)
   8= configDim D = 5.
   9
  10In RS: QALY (quality-adjusted life year) = J-cost integrated over time.
  11Perfect health: J = 0 (QALY weight = 1).
  12Disease: J > 0 (QALY weight < 1).
  13
  14Five canonical healthcare financing models (Beveridge, Bismarck, national
  15health insurance, out-of-pocket, mixed) = configDim D.
  16
  17Lean: 5 analysis types + 5 financing models.
  18
  19Lean status: 0 sorry, 0 axiom.
  20-/
  21
  22namespace IndisputableMonolith.Economics.HealthEconomicsFromRS
  23open Cost
  24
  25inductive HealthEconomicAnalysis where
  26  | cea | cba | cua | bia | roi
  27  deriving DecidableEq, Repr, BEq, Fintype
  28
  29theorem healthEconomicAnalysisCount : Fintype.card HealthEconomicAnalysis = 5 := by decide
  30
  31inductive HealthcareFinancingModel where
  32  | beveridge | bismarck | nationalHealthInsurance | outOfPocket | mixed
  33  deriving DecidableEq, Repr, BEq, Fintype
  34
  35theorem healthcareFinancingModelCount : Fintype.card HealthcareFinancingModel = 5 := by decide
  36
  37/-- Perfect health: J = 0 (QALY = 1). -/
  38theorem perfect_health : Jcost 1 = 0 := Jcost_unit0
  39
  40structure HealthEconomicsCert where
  41  five_analyses : Fintype.card HealthEconomicAnalysis = 5
  42  five_models : Fintype.card HealthcareFinancingModel = 5
  43  perfect : Jcost 1 = 0
  44
  45def healthEconomicsCert : HealthEconomicsCert where
  46  five_analyses := healthEconomicAnalysisCount
  47  five_models := healthcareFinancingModelCount
  48  perfect := perfect_health
  49
  50end IndisputableMonolith.Economics.HealthEconomicsFromRS
  51