No death-year event after actual death
ProvedActuarialValuation.finiteLifeDeathIndicator_after_deathactuarial-sciencehattendorffprospective-reserves
The death-year indicator for later years is zero.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_finiteLifeDeathIndicator open MeasureTheory
Formal statement
namespace ActuarialValuation theorem finiteLifeDeathIndicator_after_death (K t : ℕ) (h : K < t) : finiteLifeDeathIndicator 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. When t exceeds the actual curtate death year K, the equality K=t is false, so the indicator for death in year t vanishes. This guards against counting repeated claim payments in later years after the actual death.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.