Documentation

Lean 4 Proof

theorem no_inheritance_tradeoff {ρ : ℝ} {N₁ N₂ : ℕ}
    (hρ : ρ < 1) (hN₁ : 0 < N₁) (hN₂ : 0 < N₂) (h : N₁ < N₂) :
    -- (a) More heirs → lower Herfindahl (more equal)
    bequestHerfindahl N₂ < bequestHerfindahl N₁
    -- (b) More heirs → higher curvature gain (more efficient)
    ∧ concentrationWelfareCost ρ N₁ < concentrationWelfareCost ρ N₂ := by
  exact ⟨more_heirs_lower_herfindahl hN₁ h,
         dispersion_raises_curvature hρ hN₁ hN₂ h⟩

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:203

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file