Prove2Me

The survivor-tail cohort decreases by exactly the corresponding death-year probability

Proved
actuarial_c_mass_cohort_decrement

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

actuarial-scienceinsurancelife-contingency

The survivor-tail cohort decreases by exactly the corresponding death-year probability.

Mathematical relation:

S(j)−S(j+1)=pj,j<hS(j)-S(j+1)=p_j,\quad j<h

The declared assumptions restrict the life law, discount and coverage exactly as required. This is an open actuarial theorem, derived from realised claim events or their expected values.

Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Definitions.Def_actuarial_c_alive
import Definitions.Def_actuarial_c_surv
import Definitions.Def_actuarial_c_massCohort

open ActuarialAssurances
Formal statement
theorem actuarial_c_mass_cohort_decrement (h j : ℕ) (p : ℕ → ℝ) (hj : j < h) : massCohort h p j-massCohort h p (j+1)=p j := by sorry
Source
Original derived finite life-contingency specification; S. David Promislow (2015), Fundamentals of Actuarial Mathematics, 3rd edition, Chapter 5, Section 5.7, general identity and actuarial notation, printed p. 71. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml. The cited material establishes actuarial context and payment conventions. This particular finite Lean declaration is not a verbatim published theorem.
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 13, 2026

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

View graph