factored split_outcome out into reusable lemma; defined wd_payments here for now; more outline for proof of wd_outcome
oops → qed