Prove2Me

Policy in force at inception

Proved
ActuarialValuation.finiteLifeInForceIndicator_zero

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

actuarial-sciencehattendorffprospective-reserves

Every curtate lifetime is at least zero, so the policy is in force at issue.

Mathematical statement

S0(K)=1S_0(K)=1
Preamble
import Mathlib
import Definitions.Def_actuarial_finiteLifeInForceIndicator
open MeasureTheory
Formal statement
namespace ActuarialValuation

theorem finiteLifeInForceIndicator_zero (K : ℕ)
  :
  finiteLifeInForceIndicator K 0 = 1 := 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. For any natural curtate future lifetime K, zero is at most K. Therefore the in-force indicator at policy inception t=0 is one. This is a simple boundary for the original policy issued in force, regardless of whether death occurs during the first policy year.

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