taxOptimizationCert
plain-language theorem explainer
taxOptimizationCert supplies the concrete TaxOptimizationCert instance for the J-cost Laffer model by populating the tax-type cardinality field from the decidable count theorem and the threshold field from the canonical certificate. Public-finance researchers working inside the Recognition Science monolith would cite it when formalizing compliance-ratio optimization across the five canonical tax types. The construction is a direct structure instantiation that wires the upstream count result into the required certificate record.
Claim. The tax-optimization certificate is the structure whose first field asserts that the set of tax types has cardinality five and whose second field supplies the canonical certificate as threshold.
background
The module interprets the Laffer curve via the J-cost function J(r) on the compliance ratio r = actual revenue / maximum possible revenue, with the optimum at r=1 where J=0 and the disruption band beginning at J(phi). Five canonical tax types (income, corporate, capital gains, consumption, wealth) are identified with configDim D=5. The structure TaxOptimizationCert packages these requirements as the pair of fields five_types : Fintype.card TaxType = 5 and threshold : CanonicalCert.
proof idea
The definition is a direct structure construction that assigns the five_types field the value of the upstream theorem taxTypeCount and the threshold field the value of the canonical certificate cert.
why it matters
This definition closes the certificate interface required by the Tax Optimization from J-Cost layer, supplying the five-type count that aligns with the framework's D=5 configuration for public-finance models. It feeds any later theorem that invokes TaxOptimizationCert to derive J-minimizing rates or to connect the Laffer optimum to the Recognition Composition Law. The construction touches the open question of how the canonical threshold cert is itself obtained from the J-band axioms imported via CanonicalJBand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.