Documentation

Lean 4 Proof

theorem capital_stock_reduction :
    -- ΔK/Y ≈ -σ · τ_B / (1 - τ_B) for bequest tax τ_B
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:402

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file