Prove2Me

Second-death order and tie partition

Proved
actuarial_d_second_order_partition

by WillR · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

actuarial-sciencejoint-lifelife-contingencymultiple-lives

Second-death order and tie partition. The second claim allocates to the later death or simultaneous death, when both deaths are observed. The settlement date, survivor entitlement, financial discount and relevant joint-law assumptions are those declared in the formal model.

Mathematical relation:

C2=Cx≻y(2)+Cy≻x(2)+CtieC_2=C_{x\succ y}^{(2)}+C_{y\succ x}^{(2)}+C_{\text{tie}}
Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Definitions.Def_actuarial_d_firstPath
import Definitions.Def_actuarial_d_secondPath
import Definitions.Def_actuarial_d_xFirstPath
import Definitions.Def_actuarial_d_yFirstPath
import Definitions.Def_actuarial_d_xSecondPath
import Definitions.Def_actuarial_d_ySecondPath
import Definitions.Def_actuarial_d_tiePath

open ActuarialJointD
Formal statement
theorem actuarial_d_second_order_partition (h i j : ℕ) (d : ℕ → ℝ) : secondPath h d i j = xSecondPath h d i j + ySecondPath h d i j + tiePath h d i j := by sorry
Source
Originally derived two-life finite-grid definition or theorem, motivated by S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapter 10, Section 10.8.2, p. 154. The published reference supplies actuarial context, while the formal statement and joint-law conventions are new. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
Human review

  • Endorsed by Shuze Chen · Oct 16, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 16, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph