HealthEconomicAnalysis
plain-language theorem explainer
HealthEconomicAnalysis enumerates five standard health economic evaluation methods as an inductive type. Researchers mapping Recognition Science to health metrics would cite it to equate the number of canonical analyses with configuration dimension D. The declaration is a direct inductive enumeration deriving Fintype to support immediate cardinality results.
Claim. The inductive type of health economic analyses consists of five variants: cost-effectiveness analysis, cost-benefit analysis, cost-utility analysis, budget impact analysis, and return on investment.
background
Recognition Science equates the quality-adjusted life year to the time integral of J-cost. Perfect health corresponds to J-cost equal to zero while disease states produce positive J-cost and lower QALY weights. The module identifies five analysis types with configuration dimension D equals five, parallel to five healthcare financing models.
proof idea
The declaration is a direct inductive definition that introduces five constructors and derives DecidableEq, Repr, BEq, and Fintype automatically.
why it matters
This definition supplies the five analysis types required by HealthEconomicsCert, which asserts Fintype.card HealthEconomicAnalysis equals five together with the perfect-health condition Jcost 1 equals zero. It realizes the E4/E1 application by setting the count of standard health economic methods equal to configDim D equals five.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.