Prove2Me

Prospective reserve, death and running benefits: ctAliveReserve_zero_cashflow

Proved
ActuarialValuation.ctAliveReserve_zero_cashflow

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

actuarial-sciencectmc-generator-thieleformal-verification

There is no liability when both running and death cashflows vanish. The exact assumptions, units and boundary conventions are recorded separately in the formal statement.

Mathematical relation:

There is no liability when both running and death cashflowsvanish.\begin{aligned}\text{There is no liability when both running and death cashflows} \\ \text{vanish.}\end{aligned}
Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Definitions.Def_actuarial_ctAliveReserve
Formal statement
namespace ActuarialValuation

theorem ctAliveReserve_zero_cashflow (delta mu maturity t : ℝ) : ctAliveReserve delta mu 0 0 maturity t = 0 := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 324. Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 19, sections 19.3–19.6, https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml; Norberg and colleagues, Markov models and Thiele's integral equations for the prospective reserve (1997), https://doi.org/10.1016/S0167-6687(97)00020-6; Buchardt, Møller and Schmidt (2015), https://doi.org/10.1080/03461238.2013.879919. Parent topic: Finite actuarial multi-state generator conservation, continuous-time mortality transition matrices, and an analytically derived absorbing-state prospective reserve equation. The particular Lean formula is a new finite/real-algebraic formalisation and remains an unproved theorem target if labelled theorem. Relevant published actuarial derivation: https://www.sciencedirect.com/science/article/pii/S0167668797000206
Human review

  • Endorsed by Shuze Chen · Oct 11, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 11, 2026

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

View graph