taxTypeCount
The theorem establishes that the set of canonical tax types has cardinality exactly five. Economists applying J-cost minimization to Laffer-curve problems would cite this result to fix the configuration dimension of the tax space. The proof is a one-line decision procedure that exploits the Fintype instance generated by the five-constructor inductive definition.
claimThe cardinality of the set of canonical tax types is five: $|TaxType| = 5$.
background
The module models tax optimization by minimizing the J-cost function on the compliance ratio r. Five canonical tax types are introduced as the inductive type TaxType with constructors income, corporate, capitalGains, consumption, and wealth; this type carries DecidableEq, Repr, BEq, and Fintype instances. The module documentation states that these five types realize configDim D = 5 and thereby ground the Laffer-curve analysis in Recognition Science.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the goal Fintype.card TaxType = 5. The tactic succeeds because the Fintype instance for TaxType is derived automatically from its five constructors.
why it matters in Recognition Science
The result populates the five_types field of the downstream taxOptimizationCert definition, which certifies the tax-optimization structure. It directly implements the module claim that five tax types equal configDim D = 5, extending the Recognition Science framework in which spatial dimension is fixed at three while configuration dimensions are chosen per domain. No open scaffolding questions are closed by this declaration.
scope and limits
- Does not derive any optimal tax rate from the J-cost function.
- Does not assign J-values or disruption bands to individual tax types.
- Does not prove that the five-type classification is unique or exhaustive.
Lean usage
example : Fintype.card TaxType = 5 := taxTypeCountformal statement (Lean)
28theorem taxTypeCount : Fintype.card TaxType = 5 := by decide
proof body
29