Documentation

Lean 4 Proof

theorem trust_irrelevance {τ_R W : ℝ} {N : ℕ} (hN : 0 < N) :
    -- Revenue when trust distributes to N recipients
    recipientTaxRevenue τ_R W N
    -- equals revenue from direct bequest
    = estateTaxRevenue τ_R W :=
  revenue_equivalence hN

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:313

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file