Complete Single-Life Annuity Valuation, Payment Timing and Relationships

Motivation

A life annuity pays instalments conditional on an annuitant surviving to specified instants. As discussed in Dickson, Hardy and Waters (2020), actuarial value depends on the exact timing of the payments. For a pension payable in arrears, the payment event is at the end of the period. A contractual guarantee can preserve payments for the estate after death, but only once the entitlement has commenced. Those conditions must be explicitly modelled before calculating actuarial factors.

Setting

Take a finite distribution over last survived anniversaries $K=0,\ldots,h$ with nonnegative probabilities $p_k$ summing to one. The final state is right-censored: it does not assert death at the terminal age. Define $S(t)=\sum_{k=t}^{h}p_k$. A schedule has its first index $a$, up to $n$ instalments, an amount $b_j$ for each instalment, and an annual discount factor $v$ with $0<v\le1$. Advance instalments fall at $j$ and arrears instalments at $j+1$.

The first $g$ scheduled instalments are guaranteed only when survival to commencement $a$ activates the annuity. They continue to the estate after death during that period. Later instalments depend on survival at their actual payment instant. No spouse benefit is assumed.

Formalization targets

Payment events and survival

Define the realised random variable $Z(K)$ by summing actual payment indicators across the finite schedule. Derive its expectation independently from the lifetime-state mass function. Define a second valuation using survival to each payment instant, and prove the equivalence by interchanging finite sums.

$$\mathbb{E}[Z]=\sum_{k=0}^{h}p_kZ(k)= \sum_{j=a}^{a+n-1} b_j v^{j+\delta} \begin{cases} S(a),&j<a+g,\\ S(j+\delta),&j\ge a+g. \end{cases}$$

The instalment sum is truncated at the finite horizon. The timing offset $\delta$ equals zero for advance and one for arrears.

Duration, guarantee and varying benefits

Partition a non-guaranteed whole-horizon annuity into temporary and deferred periods. For a guaranteed annuity, split payments into the activated period-certain amount and the strictly later survival-contingent amount. If $g\ge n$, its entire value is survival to commencement multiplied by the corresponding annuity-certain present value. The benefit kernel supports level, arithmetic increasing or decreasing, geometric and piecewise step-up instalments.

Arrears, fractional survival and moments

The exact finite level-annuities relationship includes the terminal payment:

$$\ddot a_{\overline{h}|}-a_{\overline{h}|}=1-v^hS(h).$$

Expected squares of realised present values yield second moments and variance. The uniform distribution of deaths (UDD) provides a separate linear interpolation of observed annual survival probabilities at fractional instants.

Continuous survival laws and a controlled limit

At a fixed payment frequency, split each annual death-state mass equally across its subperiods under UDD. The same resulting micro-lifetime distribution can be used for fractional instalments and continuous benefit-rate integrals, so their actual cashflow representations share exact event boundaries. The construction agrees with annual survival at integer anniversaries. Placing the unsplit annual masses directly at integer death times would give a different, stepwise survival model within a year.

The zero-interest level annuity has an exact finite correction to the integral of linearly interpolated UDD survival. If $C$ is that integral, $S$ annual absolute survival and $m>0$, the due value equals $C+(S(0)-S(h))/(2m)$, and the arrears value equals $C-(S(0)-S(h))/(2m)$. Both have an explicit $O(1/m)$ error and converge to $C$. Under the fixed micro-atom lifetime law, continuously paid GBP 1 per year instead equals the same-frequency arrears value at zero interest, because the real-time survival indicator is constant between atom times. The limit of these finite-atom laws recovers the UDD linear-survival valuation.

A separate real-time lifetime-state model represents a continuous benefit rate in money per year rather than discrete money per instalment. Its actual realised annuity present value is integrated across the entitlement interval, with a guarantee activated by survival at commencement and payments then continuing to the estate before expiry. A finite probability expectation of the realised integral is reconciled with independently integrated survival weights. The continuous certain value is a comparison under the same deterministic discount force.

The discrete and real-time laws are connected at annual and fractional instalment boundaries through exact survivor-event identities. A bounded continuous payment-rate function admits an appropriate Riemann-sum limit under the specific regularity assumptions in the formal declaration. A twice differentiable integrand with uniformly bounded second derivative admits the two-term Woolhouse-type endpoint correction with a finite-horizon quadrature error bound. These limiting and approximation statements remain open formal theorem obligations, with no universal error claim for arbitrary discontinuous mortality laws.

Capstone

The unified capstone reconciles actual annual advance and arrears payments and UDD subperiod payments with independent survival-weighted sums. It also reconciles the same finite lifetime-state law with real-time survival at anniversaries and continuous integrated benefit valuations, including an activated guarantee. Separate milestones handle second moments, terminal-censored assurance-annuity identity, Riemann convergence and the explicit quadrature error bound. The earlier finite due-minus-arrears relationship remains a supporting target. These obligations follow from the separately defined probability masses and cashflow events, rather than assuming any valuation equality.

Significance

The classical distinction between annuity-certain and life-annuity present values is explained by Promislow (2015) through an explicit interest-and-survivorship discount mechanism. The present model makes this accounting precise at the level of individual payment events. It is consequently possible to compare a certain payment stream with a contingent one using exactly the same instalment schedule. It is also possible to alter the instalment amount without silently altering the survival law or guarantee entitlement.

The resulting mathematical foundation is suitable for retirement income and defined benefit pension cashflows where timing and benefit continuation clauses materially affect value. It separates annual unit amount from each instalment, and survival at commencement from survival at later payment events.

Difficulty

A death before commencement cannot activate a deferred guarantee. A death during the guarantee permits payments to the estate. An arrears instalment requires survival at the subsequent instant and the final one cannot silently disappear. Proving these relationships from true payment indicators is harder than defining annuity factors so the desired equations hold automatically. Finite lifetime censoring and the last surviving anniversary must remain visible in all derivations.

Formalization scope

The proposed Lean representation is an indexed real-valued finite probability mass function, a survival indicator and Finset-based cashflow sums. The canonical scope is a single namespace and targeted imports of Mathlib's real-number and finite-big-operator files. The environment revision is pinned in the manifest, but remains subject to live remote verification. Periods are integer anniversaries, amounts are per actual instalment, and the valuation origin is zero. Only finite sums are asserted without convergence hypotheses. The existing classical annuity formulae appear in the cited books. Their underlying mathematics is known, while the original finite cashflow encoding and its Lean theorem obligations are open and unproved.

These primitives are intended to supply later work on DB pension guarantee periods, future life-insurance premium annuities and pension escalation. A future separate mission could reuse the actual realised-cashflow event semantics to value survival-contingent spouse benefits with a two-life entitlement law, while keeping spouse entitlement fixed at the policyholder's death under the scheme rules. The current work limits itself to the single-life estate-continuation benefit and therefore does not risk silently importing joint-life assumptions.

The extended finite discrete formalisation constructs an actual UDD subperiod death-state law. Its fractional annuity valuations follow from realised subperiod payment events, with each instalment equal to the nominal annual pension divided by frequency. Separate theorems reconcile second moments with pairwise survival-event intersections, derive the incremental value of guarantees and reconcile finite annual assurance with the life-annuity due while retaining the terminal censored-state residual. The separate continuous law and a quantitative two-term Woolhouse-type error inequality are now included as remotely elaborated open theorem declarations, still requiring genuine proofs. General commutation-column identities, noninteger-year deferrals under arbitrary interpolation, unbounded whole-life convergence and classical higher-order Woolhouse estimates need further formal models. An unconfirmed Foundation A owner Draft is not an importable dependency. Every theorem declaration is an open proof obligation and no accepted proofs are asserted.

Selected references

• David C. M. Dickson, Mary R. Hardy and Howard R. Waters (2020), Actuarial Mathematics for Life Contingent Risks, third edition, Chapters 4–5, Cambridge University Press. https://doi.org/10.1017/9781108784184
• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapter 4, Wiley, https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782521
• David C. M. Dickson, Mary R. Hardy and Howard R. Waters (2013), Actuarial Mathematics for Life Contingent Risks, second edition, Chapter 5, sections 5.3–5.13. https://assets.cambridge.org/97811070/44074/frontmatter/9781107044074_frontmatter.pdf