Prove2Me

No in-force indicator beyond death year

Proved
ActuarialValuation.finiteLifeInForceIndicator_after_death

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

actuarial-sciencehattendorffprospective-reserves

Once time t strictly exceeds the curtate death year K, the in-force indicator vanishes.

Mathematical statement

t>K  ⟹  St(K)=0t>K\implies S_t(K)=0
Preamble
import Mathlib
import Definitions.Def_actuarial_finiteLifeInForceIndicator
open MeasureTheory
Formal statement
namespace ActuarialValuation

theorem finiteLifeInForceIndicator_after_death (K t : ℕ) (h : K < t)
  :
  finiteLifeInForceIndicator K t = 0 := by sorry

end ActuarialValuation
Source
Shiu and Xiong (2021), An elementary derivation of Hattendorff's theorem, European Actuarial Journal 11 319-323, especially equations (1), (3)-(5), https://doi.org/10.1007/s13385-020-00256-9; Gerber (1997), Life Insurance Mathematics, third ed., Chapter 6 section 6.7, https://doi.org/10.1007/978-3-662-03460-6
Read-back

What the Lean code literally says, in plain math · gpt-6

Independent mathematical reading. If the current policy-year index t is strictly greater than the realised death year K, the condition t≤K is false. Consequently the in-force indicator is zero. This does not require any financial parameters or stochastic death rate.

Human review

  • Endorsed by Shuze Chen · Oct 9, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 9, 2026

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

View graph