def growthDrag (g₀ β : ℝ) : ℝ := g₀ * β
thesis/CESProofs/Macro/GrowthTax.lean:67
Growth and Dynamic Tax Revenue (Layer 4-5 of Macro Extension)