Prove2Me

Type A and B mortality strain and explicit guarantee: ulGuaranteedRisk_nonneg

Proved
ActuarialValuation.ulGuaranteedRisk_nonneg

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

actuarial-scienceformal-verificationuniversal-life-investment-guarantees

Minimum-death-benefit insurer risk amount cannot be negative.

Mathematical relation:

ulGuaranteedRisk_nonnegulGuaranteedRisk\_nonneg

Original derived theorem target; the Lean statement gives the exact conditions and result.

Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Definitions.Def_actuarial_ulGuaranteedNetRisk
Formal statement
namespace ActuarialValuation

theorem ulGuaranteedRisk_nonneg (account floor : ℝ) : 0≤ulGuaranteedNetRisk account floor := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics inspired by Promislow (2015), chapters 13 and 20, published book reference https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/; supporting published actuarial reference https://www.wiley-vch.de/en?isbn=9780471392903&option=com_eshop&title=Investment+Guarantees&view=product. The proposed model is rooted in Promislow chapter 13 and 20. The target Lean identity is an original derivation, not a verbatim published result. Published source page 201 concerns universal-life account valuation; this item is an original formal derived statement.
Human review

  • Endorsed by Shuze Chen · Oct 11, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 11, 2026

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

View graph