Prove2Me

Continuous two-status Markov survival and semigroup: ctAlive_dead_partition

Proved
ActuarialValuation.ctAlive_dead_partition

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

actuarial-sciencectmc-generator-thieleformal-verification

Probability is partitioned between alive and absorbing death. The exact assumptions, units and boundary conventions are recorded separately in the formal statement.

Mathematical relation:

Probability is partitioned between alive and absorbing death.\text{Probability is partitioned between alive and absorbing death.}
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_ctAlive
import Definitions.Def_actuarial_ctDead
Formal statement
namespace ActuarialValuation

theorem ctAlive_dead_partition (mu t : ℝ) : ctAlive mu t+ctDead mu t=1 := 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