Prove2Me

Zero cover and zero premium payments produce zero expected loss

Proved
actuarial_c_zero_term_zero_loss

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

actuarial-scienceinsurancelife-contingency

Zero cover and zero premium payments produce zero expected loss.

Mathematical relation:

E[L0(0)]=0\mathbb E[L_0(0)]=0

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_alive
import Definitions.Def_actuarial_c_death
import Definitions.Def_actuarial_c_termPath
import Definitions.Def_actuarial_c_premiumPath
import Definitions.Def_actuarial_c_lossPath
import Definitions.Def_actuarial_c_expectedLoss

open ActuarialAssurances
Formal statement
theorem actuarial_c_zero_term_zero_loss (h : ℕ) (v : ℝ) (b p : ℕ → ℝ) : expectedLoss h 0 v 0 b p=0 := by sorry
Source
Original derived finite life-contingency specification; S. David Promislow (2015), Fundamentals of Actuarial Mathematics, 3rd edition, Chapter 5, Section 5.2, net premium ratio and premium stream, printed p. 63. 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