Prove2Me

At each realised lifetime state a deterministic extra settlement lag multiplies the claim PV

Proved
actuarial_c_delay_path_factor

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

actuarial-scienceinsurancelife-contingency

At each realised lifetime state a deterministic extra settlement lag multiplies the claim PV.

Mathematical relation:

Zrdelay(K)=vrZ(K)Z^{\text{delay}}_{r}(K)=v^{r}Z(K)

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_death
import Definitions.Def_actuarial_c_path
import Definitions.Def_actuarial_c_delayPath

open ActuarialAssurances
Formal statement
theorem actuarial_c_delay_path_factor (h lag k : ℕ) (v : ℝ) (b : ℕ → ℝ) : delayPath h lag v b k=v^lag*path h v b k := by sorry
Source
Original derived finite life-contingency specification; S. David Promislow (2015), Fundamentals of Actuarial Mathematics, 3rd edition, Chapter 5, Section 5.1, claim processing and payment timing, printed p. 61. 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