Zero-horizon loss is exactly the opening reserve
ProvedActuarialValuation.finiteReserveLossAtIssue_zeroactuarial-sciencehattendorffprospective-reserves
With no covered years, the premium and death-benefit sums are empty, and all that remains is the current reserve.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_finiteReserveLossAtIssue open MeasureTheory
Formal statement
namespace ActuarialValuation theorem finiteReserveLossAtIssue_zero (K : ℕ) (v : ℝ) (premium benefit reserve : ℕ → ℝ) : finiteReserveLossAtIssue K 0 v premium benefit reserve = reserve 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. At horizon n=0 the finite year range contains no premiums or death benefits. The terminal reserve is V_0 times the inception in-force indicator, equal to one for all natural K. Hence the insurer loss definition reduces precisely to opening reserve V_0, not to zero.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.