Motivation

A life table summarises the survival of a cohort as ages advance, as developed in Promislow's life-table treatment. It provides an essential common language for life assurance, retirement pensions, annuities and reserves. A credible mathematical foundation must make precise when cohort counts define conditional probabilities, how death counts exhaust an assumed closed population, and why commutation-function ratios give the same values as discounted contractual payments. The classical notation is widely understood by actuaries but can conceal assumptions at terminal ages, when there are no remaining lives, and at fractional-year payment times. This formalisation specifies those assumptions so that later results can safely reuse them.

Setting

Consider an integer-age cohort with a finite terminal age, nonnegative numbers alive and nonincreasing numbers alive at successive ages. At the terminal age the remaining cohort is zero. Annual deaths are the change in cohort size over each year. Conditional survival starts only from an age with positive numbers alive. The model also has a strictly positive annual discount factor; when the corresponding effective interest rate is nonnegative, that factor is at most one. A due annuity pays on the integer anniversaries at which the insured life is alive. An annual death assurance pays at the end of the year of death. All financial amounts in the principal identities are per unit benefit, valued at the attained age of the insured life.

Formalization targets

Cohort probabilities and lifetime laws

The opening group establishes that successive survivor and decrement counts conserve population mass. Multi-year survival, conditional and deferred mortality must be derived from original counts and remain coherent under time shifts. A zero survivor count is an explicit boundary of the probability model. Curtate lifetime moments are obtained from the annual death distribution and its tail probabilities. Continuous survival and hazard relationships form an additional interface requiring a genuine measurable lifetime law. They cannot be inferred from the table's integer-age observations without an interpolation assumption.

Select and fractional-age assumptions

The next group distinguishes age at selection from time since selection and attained age. Ultimate mortality applies only after the selection period. Within a year, uniform distribution of deaths, constant force and Balducci interpolation share the annual survival endpoints but generally disagree between those endpoints. Each conditional fractional formula needs the corresponding survival denominator to be positive. These are alternative models, so the choice of interpolation must remain explicit.

Commutation columns and benefit timing

The commutation columns are defined from the same original survivor counts and a fixed annual discount factor. Discounted survivors and year-end deaths create the first-order columns. Their finite forward sums create the second-order columns, and sums of those forward sums create the increasing-benefit columns. In particular, for survivors the discounted payments begin at the valuation anniversary, whereas for deaths the benefit is payable on the next anniversary. The finite terminal convention is essential for the last year's assurance payment and the last available annuity instalment.

Principal finite-cohort capstone

The principal goal is the finite-cohort valuation reconciliation. Starting independently from annual numbers alive and numbers dying, it shows that total deaths exhaust the living cohort, actual survival-contingent payments agree with the annuity commutation ratio, actual annual death payments agree with the assurance commutation ratio, and the commutation sums satisfy their backward recursions. It also establishes the capital identity expressing unit present value as annual death assurance plus the discount loss on an annuity due. No commutation recurrence or present-value equivalence is assumed as an input.

At a valid attained age, the annuity and assurance are independently valued from the original cohort:

$$\ddot a_x=\frac{N_x}{D_x},\qquad A_x=\frac{M_x}{D_x},\qquad A_x+(1-v)\ddot a_x=1.$$

Significance

As in the classical actuarial notation, the resulting interfaces separate cohort mass from conditional probability and separate mortality from the economic discounting basis. This allows a later actuarial mission to combine them only where the required regularity and positivity assumptions are available. The commutation functions supply a transparent independent valuation route alongside direct finite cashflow sums. Their ratios remain useful as a reference calculation even when production models value very large pension populations by member-level cashflow projection. Higher-order commutation functions are also the natural algebraic representation of benefits that increase by one unit at each subsequent anniversary.

This foundation is reusable across future mortality and valuation missions. A foundational namespace is particularly important where related existing missions already use different local definitions. The present work provides a compatibility design and a proposed canonical public vocabulary. Publishing an older equivalent definition does not automatically establish a safe imported interface: exact source, revision, visibility, and declaration signatures must match. The programme therefore retains existing mission objects and develops explicit crosswalks, rather than silently replacing earlier results.

Difficulty

The mathematical difficulty centres on conditioning, index shifts and independent routes to the same financial result. At an age with no survivors, a formal programming language may return a totalised value for division by zero even though no conditional mortality probability exists. A common off-by-one error values a death at the beginning of its year or includes a due annuity payment after the terminal age. Another error confuses discounting to time zero with discounting to the current valuation age. Select mortality requires careful handling of attained age at the exact selection-duration boundary. Continuous lifetime hazard and moment formulas additionally need probability, measurability and integrability assumptions that finite cohort counts alone cannot supply.

The double-sum commutation identities require a finite discrete summation argument and must use published survivor and assurance conventions consistently. The goal compares separate original definitions of payment cashflows, the population exit distribution, and commutation columns under one valid finite life table. The capstone is nonvacuous: a positive starting cohort and positive discount factor exclude empty-cohort substitutions and make its conditional cashflows meaningful. Its assumptions impose cohort validity and positive discounting; they do not contain the desired present-value identities as hypotheses.

Formalization scope

The initial formalisation supplies a canonical finite discrete cohort and annual cashflow basis. The continuous-law, hazard, select and fractional-age results are separately specified mathematical interfaces and are admitted into the formal theorem inventory only when remote declaration checks establish valid Lean signatures. For nonnegative effective interest the annual discount is in the interval from zero excluded to one included. More general deterministic term structures and stochastic discount factors require separate cashflow definitions. Joint-life and competing-decrement extensions must identify any independence or mutually exclusive decrement assumptions explicitly.

No assertion is made about mortality being stationary across calendar years or about the validity of a specific mortality table for a real population. The terminal-age assumption imposes certain death before the finite horizon. It is unsuitable without modification for a lifetime distribution with unbounded support. A lifetime with an atom at an integer boundary requires separate weak and strict survival events; interpreting a one-year death count as the hazard at the death instant is unjustified without further assumptions. Open formal statements remain proof obligations, and passing a declaration check would establish only well-formed Lean, not the mathematical truth of the intended result.

The finite-cohort valuation targets also include independently defined one-year and multi-year mortality probabilities, temporary and deferred annuities, term and endowment assurances, pure endowments, annuities in arrears and increasing finite-term cashflows. The expanded candidate graph has 26 definitions and 48 open theorem obligations in a coherent reconciliation programme. New results require independently derived cashflow-to-commutation identities.

Related proposals LII (commutation functions and finite-term benefits) and LXII (fractional-duration valuation) are in review, not public importable dependencies. Existing published life-table theorems in XLV must be reused where signatures match. The fractional-age and continuous-law interfaces require separate hypotheses. All research targets remain provisional until their exact published-name overlap checks, authoritative declaration elaboration and dependency links are validated. No private diagnostic is counted as a proved theorem.

The increasing-insurance commutation column requires the relative-duration or absolute-age convention to be declared explicitly. Annual UDD includes certain year-end death, but constant-force and Balducci interpolation require annual death probability strictly below one.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, Chapters 2–5, 7, 9 and 13–14. 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 (2020), Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, Chapters 2–5. https://doi.org/10.1017/9781108784184