Prove2Me

Risk guarantees, surrender payments and reserve strain: ulDeathCost_nonneg

Proved
ActuarialValuation.ulDeathCost_nonneg

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

actuarial-scienceformal-verificationunit-linked-profit-charges

Expected non-unit death cost is nonnegative at a valid mortality rate. This original derived actuarial relation uses the parameter restrictions, endpoints and units stated in the separate formal theorem or definition.

Mathematical relation:

Btdeath=max⁡(Ft,Gt),Rt=(Gt−Ft)+B_t^{\text{death}}=\max(F_t,G_t),\quad R_t=(G_t-F_t)^+
Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Order.Group.MinMax
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Definitions.Def_actuarial_ulDeathCost
Formal statement
namespace ActuarialValuation

theorem ulDeathCost_nonneg (q fund guarantee : ℝ) (hq : 0≤q) : 0≤ulDeathCost q fund guarantee := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 16. FCA, Unit-linked pensions and savings price and value practices, https://www.fca.org.uk/publications/multi-firm-reviews/unit-linked-pensions-and-savings-multi-firm-review-consumer-duty-price-and-value-practices; FCA TR16/2 Fair treatment of long-standing customers, https://www.fca.org.uk/your-fca/documents/thematic-reviews/tr16-02. Parent topic: Allocated premium, offer and bid unit prices, cost of allocation spread, fund charges, net amount at risk, policy expenses and discounted expected non-unit profit. The particular Lean formula is a new finite/real-algebraic formalisation and remains an unproved theorem target if labelled theorem. Relevant published actuarial derivation: https://www.fca.org.uk/your-fca/documents/thematic-reviews/tr16-02
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