Motivation

Universal-life policies maintain a distinct policyholder account that receives premiums, incurs explicit expense charges, is credited investment interest and finances the cost of life insurance. Unlike a traditional fixed-premium product, account returns and mortality charges can change over time, and an investment-linked contract can contain additional embedded guarantees. Promislow's Fundamentals of Actuarial Mathematics, Third Edition (2015), Chapter 13, develops account recursions, alternative death-benefit structures, credited-interest mechanisms and variable-annuity guarantees. Mary Hardy's Investment Guarantees (2003) provides an independently published actuarial treatment of insurance investment guarantees.

The established mathematical basis covers account balances, insurance pricing and financial option guarantees. Existing Prove2Me actuarial missions contain gross premiums, prospective reserves, investment valuation and option replication, but their theorem inventories do not yet provide the exact universal-life account recursion and guarantee decomposition addressed here. This new mission constructs explicit policy-account mathematics and scenario-based guarantee valuation with original unproved Lean declarations.

Setting

Time is indexed by policy period k, typically months, and all monetary variables are currency amounts at their stipulated valuation instant. An initial account A at the start of a period receives a cash premium π, from which a percentage expense r is deducted, together with a flat expense e. The resulting amount earns credited rate i through the period. A death claim associated with this period is payable at the end of the period. The insured mortality charge is the cost-of-insurance rate q multiplied by the relevant end-period net amount at risk. The conventional economic basis requires 0≤r≤1, 0≤q<1 and 1+i>0 where cancellation and nonnegative accumulation are invoked.

Let the pre-insurance earned account be

$$E=(A+\pi(1-r)-e)(1+i).$$

For a Type B death benefit, the amount in excess of account value at death is the fixed additional face amount b, and the closing account is E-qb. For a Type A structure, b is the fixed total death benefit and the net amount at risk is b minus the end-period account in the covered region. The implicit survivor-account equation therefore requires q<1 and the appropriate benefit-dominance condition. A separate guarantee may instead pay the larger of the investment account and a specified floor.

Formalization targets

Monthly account premium expenses and insurance charges

The first group states the premium allocation π(1-r), the post-premium account A+π(1-r)-e, credited accumulation E, and the start-period cost-of-insurance equivalent qη/(1+i), where η is the period-end amount at risk. If insurance charges use a separate discount rate j, the adjusted effective mortality charge is q(1+i)/(1+j). An explicit reserve recursion then accounts for the different investment and mortality-charge bases. Theorems establish exact charge reconciliation, nonnegative allocations under appropriate expense rates, monotonicity of charged premiums and equivalence when the two discount bases agree. A credited-rate floor, cap and participation fraction are represented using an explicit clamp with the floor no higher than the cap for valid contractual interpretation.

Type A and B mortality strain and explicit guarantee

The Type B closing account is defined by a direct subtraction of q times the additional face amount. The Type A solution accounts for the dependence of insured risk on its own closing balance:

$$A_{B}=E-qb,\qquad A_{A}=\frac{E-qb}{1-q},\qquad q\ne1.$$

These equations require different interpretations of b and hence are treated as separate contracts. The Lean statements specify the algebraic balance for each and the admissible region of the Type A net amount at risk. A death benefit equal to max(account, floor) is also considered. When the guarantee binds, its survivor account is solved by the Type A equation with the floor. When the earned balance exceeds that floor, the extra death benefit strain is zero. Subordinate results verify the branches and the assumptions which make the piecewise survivor account self-consistent. No reserve identity is asserted when the survival denominator vanishes.

Path-dependent account evolution and stochastic guarantee pricing

An actual policy path is generated recursively from the initial account, period-indexed premiums, charge rates, expenses, credited rates and face amounts. This builds a genuine multi-period monetary ledger, rather than a single-period formula masquerading as a trajectory. Pathwise zero-charge boundaries and a successor equation link the recursion to Type B period values.

An investment guarantee pays the greater of the realised account and a guaranteed floor at death or maturity. Its embedded insurer liability is the positive shortfall max(floor-account,0). The identity

$$\max(A,G)=A+\max(G-A,0)$$

holds on each realised scenario. To value the genuine stochastic guarantee, take a finite probability mass p(ω), a scenario-dependent discount factor d(ω), an account A(ω) and guarantee floor G(ω). Expected discounted benefit is the weighted sum over those states, with p≥0 and Σp=1 required for a valid probability law. The value of the full benefit decomposes into discounted account value plus the insurer's embedded guarantee liability. Theorems establish positivity and monotonicity as the contractual guarantee floor increases.

Capstone theorem

The main theorem ActuarialValuation.ulUniversalGuarantee_fundamental connects the exact Type A and Type B account-funding equations, with nonzero survivor denominator, to the stochastic account-plus-guarantee decomposition. This capstone preserves the difference between the account owned by the insured and the additional option-like obligation borne by the insurer, and follows the actual timing of premium receipts and mortality charges.

Significance

A reusable, explicit account recursion provides a foundation for later development of variable-annuity death and maturity guarantees, secondary no-lapse guarantees, investment-crediting corridors and stochastic profit testing. Hardy (2003) discusses the broader mathematics and risk management of equity-linked guarantees, while the proposed results formalise precise finite contracts with identified payment dates. The scenario-dependent valuation can subsequently connect to the completed binomial hedge proposal and to genuine survival-conditioned insurance cashflow expectations.

Difficulty

The implicit Type A recursion contains the end-period reserve on both sides; division by 1-q therefore has to be justified, and the fixed-total-benefit interpretation applies only while the guaranteed face remains above account value. Type B adds its stated face benefit and uses a different charge. The floor-and-cap crediting mechanism has a contractual ordering assumption, and distinct mortality/interest discount rates cannot be cancelled without a nonzero gross return. Under a negative reserve, policies may lapse unless an explicit secondary guarantee overrides the restriction; an account computation alone does not model the lapse decision.

Stochastic guarantee pricing requires actual scenario probabilities, discount factors and benefit realisations. Theorems concerning a positive option-like liability require nonnegative probabilities and discounts. This nontrivial setting excludes a degenerate zero-payment substitute. The current graph formalises conditional algebra and exact scenario valuation rather than asserting that any arbitrary investment law admits a unique arbitrage-free guarantee price.

Formalization scope

The graph contains 18 proposed reusable definitions and 41 open Lean theorem targets. It comprises monthly or period-indexed account mechanics, implicit and explicit mortality risk structures, interest rate corridors, a genuine multistep account path and the finite stochastic valuation of an investment guarantee. Its proposed capstone is supported by separate funding and stochastic valuation identities. The source inventory, dependency graph, published reference crosswalk and private compiler receipts are retained for human review.

Extensions include lapse guarantees, bid–offer spreads, withdrawals, surrender charges, a full asset-price driven account with a risk-neutral measure, minimum withdrawal guarantees and an explicit benefit date random variable. Those require additional stochastic assumptions. Declaration elaboration with sorry establishes a syntactically and mathematically well-typed proposition, subject to authoritative compiler outcomes; none of these targets is considered proved until an actual accepted proof exists. No owner Draft item should be confirmed or submitted for moderator review without human assessment.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Third Edition, John Wiley & Sons, Chapter 13 and related Chapter 20. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
• Mary R. Hardy (2003), Investment Guarantees: Modeling and Risk Management for Equity-Linked Life Insurance, John Wiley & Sons. https://www.wiley-vch.de/en?isbn=9780471392903&option=com_eshop&title=Investment+Guarantees&view=product