TaxOptimizationCert
plain-language theorem explainer
TaxOptimizationCert encodes a minimal certificate for J-cost tax optimization by requiring exactly five tax types and an instance of the canonical J-band threshold. Public-finance analysts working in the Recognition Science framework cite it when minimizing J(r) on the compliance ratio to locate the Laffer optimum. The declaration is a direct record construction that pairs the Fintype cardinality of TaxType with a CanonicalCert instance.
Claim. A record whose fields are the assertion that the set of tax types has cardinality five, i.e., $ |$ {income, corporate, capital gains, consumption, wealth} $ | = 5 $, together with a six-clause certificate satisfying $ J(1) = 0 $, $ J(x) = J(1/x) $ for $ x ≠ 0 $, $ J(ϕ) > 0 $, $ 0.11 < J(ϕ) < 0.13 $, and $ J(1/ϕ^2) > 0 $.
background
The module treats tax optimization through the J-cost functional on the compliance ratio r = actual revenue / maximum possible revenue. The Laffer curve is recovered by minimizing J(r); the optimum occurs at r = 1 where J vanishes, while the disruption band is marked by J(ϕ). Five canonical tax types are identified with configuration dimension D = 5. The TaxType inductive enumerates income, corporate, capital gains, consumption and wealth, each deriving Fintype, DecidableEq and Repr. The upstream CanonicalCert structure supplies the six properties that certify the J-band: matched zero at unity, reciprocity under inversion, positivity at ϕ, the numerical interval (0.11, 0.13), and positivity at the reciprocal square.
proof idea
The declaration is a structure definition with an empty proof body. It is a direct record bundling the cardinality fact supplied by the Fintype instance of TaxType and an instance of CanonicalCert.
why it matters
The structure supplies the certificate constructed by the downstream taxOptimizationCert definition, which populates five_types via taxTypeCount and threshold via an instance of CanonicalCert. It encodes the five-type configuration required by the module's Laffer analysis and thereby connects J-cost minimization to the canonical band properties established in CanonicalJBand. In the Recognition Science chain it realizes the configDim = 5 step for the economics domain while inheriting the J-uniqueness and phi fixed-point landmarks from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.