Prove2Me

Conservative multi-state intensity matrices and forward Euler transition: ctEuler_row_one

Proved
ActuarialValuation.ctEuler_row_one

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

actuarial-sciencectmc-generator-thieleformal-verification

The short-step transition approximation conserves unit row mass. The exact assumptions, units and boundary conventions are recorded separately in the formal statement.

Mathematical relation:

The short-step transition approximation conserves unit rowmass.\begin{aligned}\text{The short-step transition approximation conserves unit row} \\ \text{mass.}\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_ctEuler
Formal statement
namespace ActuarialValuation

theorem ctEuler_row_one (r : Fin 3 → Fin 3 → ℝ) (h : ℝ) (i : Fin 3) : (∑ j : Fin 3, ctEuler r h i j) = 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