HealthcareFinancingModel
plain-language theorem explainer
The declaration introduces an inductive type enumerating the five canonical healthcare financing models in the Recognition Science health economics setting. Researchers modeling policy configurations under RS would reference it to establish the finite set of options matching configuration dimension five. The definition proceeds by direct enumeration of constructors with derived instances for equality and finiteness.
Claim. The healthcare financing models form the finite set $M = B, Bi, N, O, M$ where $B$ denotes Beveridge, $Bi$ Bismarck, $N$ national health insurance, $O$ out-of-pocket, and $M$ mixed, equipped with decidable equality and Fintype structure.
background
Recognition Science models health economics by equating five analysis types (CEA, CBA, CUA, BIA, ROI) and five financing models to the configuration dimension D = 5. Quality-adjusted life years arise as the integral of the J-cost function over time, with perfect health at J-cost zero and disease states at positive J-cost. The module imports the Cost definitions to ground Jcost in the recognition framework.
proof idea
The declaration is a direct inductive definition listing five constructors and deriving DecidableEq, Repr, BEq, and Fintype from the Mathlib library.
why it matters
This supplies the five_models component of the HealthEconomicsCert structure and supports the cardinality result in healthcareFinancingModelCount. It instantiates the D = 5 assignment for the economics application, consistent with the broader Recognition Science use of configuration dimension to organize domains. The definition closes the enumeration needed for the certification theorem without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.