Complete Life Assurances, Lump Sums and Insurance–Annuity Identities

Motivation

A life assurance pays a contingent lump sum under a policy-defined event, rather than a sequence of survivor-contingent instalments. A benefit paid at the end of the policy year of death has a different value from one paid immediately on death. A pure endowment pays instead when the insured survives to maturity, while an endowment assurance combines cover for death before maturity with a maturity payment to survivors. For these products, the event partition, contractual recipient and payment instant must be explicit before an expected present value is calculated.

Promislow (2015, Chapter 5, sections 5.1–5.8) derives a general annual insurance–annuity relationship from benefit vectors. Dickson, Hardy and Waters (2020, Chapter 4) develops the corresponding conventional life insurance factors. The mission makes the death, survival and maturity events visible as actual random cashflows, then derives the classical identities without taking the desired identities as assumptions.

Setting

Let the lifetime-state variable $K$ take values $0,\ldots,h$. For $j<h$, state $K=j$ represents death during the policy year whose start is anniversary $j$ and whose end is anniversary $j+1$. State $K=h$ represents survival at the model's right-censoring anniversary. Nonnegative probabilities $p_j$ satisfy $\sum_{j=0}^{h}p_j=1$. The anniversary survival probability is $S(j)=\sum_{k=j}^{h}p_k$, for $0\le j\le h$. The annual discount factor $v$ satisfies $0<v\le1$, and all values are expressed at policy commencement, time zero.

For an amount schedule $b_j$ in money per death claim, the random present value of a death benefit payable at the end of the death year is

$$Z(K)=\sum_{j=0}^{h-1}v^{j+1}b_j\mathbf{1}_{\{K=j\}}.$$

A temporary assurance of duration $n$ includes deaths in policy years $0,\ldots,n-1$. A deferred term assurance adds a waiting period $a$ and covers deaths in years $a,\ldots,a+n-1$. A pure endowment is triggered by $K\ge n$ and pays at time $n$. The term and maturity components are disjoint for $0\le n\le h$. The specific settlement recipient can be identified contractually; if recipient survival or eligibility changes the payment event, that condition requires an additional model variable.

Formalization targets

Realised insurance values

The foundational result is a reconciliation between the expectation of the realised random present value $Z$ and a separate valuation made from the probability of death in each covered policy year. For a unit sum assured, both routes must produce an actuarial value from exactly the same state law. The analogous pure-endowment reconciliation averages realised survivor payments and independently discounts the survival tail.

Maturity-event partition and annuity identity

The next result establishes the endowment decomposition from disjoint actual payment events, including the zero-term boundary and a terminal survivor who must not receive a fictitious death claim. The year-end-of-death benefit and the maturity benefit are valued separately. Their combination is then reconciled with a survival-contingent annuity paid in advance at anniversaries $0,\ldots,n-1$.

Writing $d=1-v$ for the annual effective discount rate, the central finite relationship for unit death and maturity benefits is

$$A_n^{1}+v^nS(n)+d\ddot a_n=1, \qquad \ddot a_n=\sum_{j=0}^{n-1}v^jS(j).$$

Here $A_n^{1}$ includes deaths before maturity and settlement at the following policy-year end. The maturity mass $v^nS(n)$ captures those alive at $n$. The formula is derived by telescoping discounted survival decrements. When the horizon is right-censored, a whole-horizon death-only assurance omits terminal survivors and requires a residual term. A familiar whole-life identity without that term needs certain death by the terminal horizon or an expressly defined terminal benefit.

Variable benefits and moments

The source also defines arithmetic increasing and decreasing insured amounts, geometric escalation and minimum-benefit floors. It constructs the second moment of the actual claim present value by squaring its realised value and compares it to a separate squared-benefit death-mass sum. Distinct death years are mutually exclusive, so mixed claim terms vanish. A variance is meaningful only with a normalised, nonnegative probability law. Additional families cover insurance-term extensions, the split of a deferred term, exact commutation recursions and benefit or discount ordering.

The principal capstone starts with a single finite lifetime law and one annual discount basis. It simultaneously derives the death-claim expectation, the pure-endowment expectation, the disjoint endowment decomposition, the finite insurance–annuity conservation identity and the independent second-moment formula. The conservation equation is the substantive conclusion rather than a restated hypothesis. Each item remains an open theorem statement until a valid Prove2Me proof is separately accepted.

Continuous and fractional-time valuation

The additional model uses an actual real future lifetime T with a specified probability measure μ supported on nonnegative times. It does not infer a continuous death-time distribution from annual mortality probabilities. At nonnegative maturity n, death in 0≤T<n triggers an immediately paid claim. Death at T=n instead belongs to the pure-endowment event T≥n, even if the probability law has an atom there.

At constant force of interest δ, put U=min(T,n). A continuously paid unit annuity has realised present value Y=(1−exp(−δU))/δ when δ≠0, and Y=U when δ=0. An immediate death benefit or maturity benefit pays exp(−δU) under exactly one of the two events. Therefore its pathwise conservation law is

$$\exp(-\delta U)+\delta Y=1.$$

Taking expectations under the same μ produces the distinct continuous insurance–annuity identity

$$\overline A_n^1+\exp(-\delta n)\Pr(T\ge n)+\delta\overline a_n=1.$$

Fractional-time results specify m>0 annual instalment periods, each ending at (r+1)/m. A death in [r/m,(r+1)/m) is payable at the following subperiod end, without ambiguity at exact grid instants. At nonnegative force, immediate payment is at least as valuable as m-thly payment, which is at least as valuable as year-end payment. Supporting results cover cashflow moments, settlement lag, escalation and UDD-versus-constant-force survival. The annual–continuous bridge equates year-end claim values under matched policy-year death masses.

Significance

This event-level basis, grounded in the insurance benefit conventions of Dickson, Hardy and Waters (2020, Chapter 4), supports analyses of death-in-service benefits, death-in-deferment cover, pension-scheme lump sums, term life protection and survival maturity benefits. It also makes transparent why the expected value of a lump-sum death claim can be represented using an annuity schedule only after the schedules and discounting are related mathematically. The annuity correspondence reflects an exact payment-mass identity, and a denominator used for recurring premiums needs strict positivity before division.

These reusable cashflow models can support future dependent-beneficiary and pension-scheme guarantees, but true survivor entitlement requires an additional joint-life state.

Difficulty

Careful classification at anniversaries is essential. In the annual model, a death allocated to the policy year following maturity cannot generate both the pre-maturity death benefit and the maturity benefit. Terminal censoring distinguishes survival observed at the end of a finite table from guaranteed eventual death. The conservation identity should remain valid at zero interest and zero term; when no covered deaths occur, its insurance component must vanish. Later death-year payments also make valuation sensitive to the chosen discount factor.

Death-claim second moments require exclusive event indicators, not independence. The capstones derive values from cashflows rather than commutation-table definitions. These constraints exclude vacuous premises and cosmetic equalities.

Formalization scope

The private formal development contains two distinct models: a finite annual right-censored K-model with discount factor v and an actual real-lifetime T-model with exponential discounting at force δ. The annual root remains the main theorem, while the continuous insurance–annuity result is a separate supporting capstone. Targeted Mathlib imports encode a probability measure, real claim instants, fractional settlement and cashflow moments.

The classical actuarial identities are already established in the literature. The Draft contains 119 open theorem statements, including seven explicitly formulated reusable root-support lemmas, with no accepted mission proofs. Pinned-revision private Lean checks have verified 85 distinct theorem statements, including the complete 12-conjunct finite annual root, distribution-level insurance–annuity conservation and the annual–continuous settlement bridge. These are private compiler diagnostics, not accepted proofs of published mission targets.

Annual discount d=1−v differs from continuous force δ. The fractional branch models UDD and finite constant-force survival and bridges half-year survival to the payment grid. General-duration inequalities, death-time density valuation, select tables, dependent-survivor eligibility and infinite-horizon convergence remain open. A time-dependent recipient multiplier does not establish joint-life entitlement.

Selected references

• David C. M. Dickson, Mary R. Hardy and Howard R. Waters (2020), Actuarial Mathematics for Life Contingent Risks, third edition, Chapter 4, Cambridge University Press. https://doi.org/10.1017/9781108784184
• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapters 5 and 7, and Chapter 8, section 8.8, Wiley, ISBN 9781118782460. https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782521