TaxType
The declaration enumerates five canonical tax categories for the Recognition Science treatment of public finance. Researchers applying J-cost minimization to Laffer-curve problems cite it to fix the configuration dimension at five. The definition introduces the constructors by direct listing and derives the required typeclass instances in one step.
claimLet $T$ be the inductive type whose constructors are the five tax categories: income, corporate, capital-gains, consumption, and wealth.
background
The module interprets the Laffer curve through the J-cost function on the compliance ratio $r$, with the optimal rate minimizing $J(r)$ and the disruption band located at $J(phi)$. The inductive type supplies the discrete set of instruments that realizes configDim $D=5$. It draws on the CanonicalJBand import for the underlying J-band constants and on the general Recognition Science forcing chain that fixes phi and the eight-tick octave.
proof idea
The declaration is an inductive definition that lists the five constructors explicitly and attaches the deriving clause for DecidableEq, Repr, BEq, and Fintype.
why it matters in Recognition Science
TaxOptimizationCert depends on this enumeration to populate its five_types field and thereby certify configDim = 5. The definition therefore supplies the concrete carrier set over which the J-cost optimization theorem operates. It extends the T5–T8 forcing chain into the economics tier by fixing the number of tax instruments to the canonical band size.
scope and limits
- Does not assign numerical rates or revenue functions to any constructor.
- Does not prove optimality or compute a minimum of J.
- Does not model avoidance dynamics or behavioral responses.
- Does not relate the five types to spatial dimension D=3.
formal statement (Lean)
24inductive TaxType where
25 | income | corporate | capitalGains | consumption | wealth
26 deriving DecidableEq, Repr, BEq, Fintype
27