Sections / Section 14: Macro -- Two-Factor CES, Growth, Tax / corporate_tax_revenue

Corporate Tax Revenue

theoremprovedMacroeconomics

Documentation

Lean 4 Proof

theorem corporate_tax_revenue {τ_corp Y Jσ : ℝ} :
    τ_corp * corporateProfit Y Jσ = τ_corp * Y / Jσ := by
  simp only [corporateProfit]; ring

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:190

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file

taxRevenue taxRevenueShare corporateProfit profitShare lafferRevenue lafferPeak lafferMaxRevenue saezTopRate primaryDeficit debtDynamics debtSustainable taxRevenue_zero_rates taxRevenue_scale taxRevenue_additive taxRevenue_increasing_in_τL taxRevenue_increasing_in_τK taxRevenue_increasing_in_τC taxRevenue_increasing_in_τcorp corporateProfit_pos corporateProfit_increasing_in_Y