Motivation

Fractional-duration life contingencies arise when contractual cashflows are paid more frequently than annually and when valuations occur between policy anniversaries. The frequency of annuity payments, the timing of a death benefit and the assumption used to interpolate survival between integral ages each affect the expected present value. S. David Promislow's Fundamentals of Actuarial Mathematics, third edition (2015), particularly Chapter 7, develops these relationships alongside its treatment of life annuities (Chapter 4) and continuous payments (Chapter 8). This mission constructs independent, explicitly timed Lean 4 definitions and original theorem targets that can be reused in later insurance, pension and reserve formalisation.

The foundational mathematics is already established in the actuarial literature. Its corresponding Lean declarations in this mission are open proof targets. The existing Prove2Me actuarial collection already contains annual annuities, life-table identities and constant-force mortality examples, but these do not by themselves establish the new m-thly cashflow and within-year reserve results. Relevant published material includes Promislow (2015) and Society of Actuaries actuarial work on uniform mortality interpolation.

Setting

Time is measured in years after issue. Policy year k is a natural number, payment frequency m is a positive number of instalments per year, and j ranges from zero through m-1. A benefit amount c(k) has currency units per year. A normalised annual payment stream has cash amount c(k)/m at each instalment. Discount D(t) and unconditional survival p(k) are dimensionless. Annual mortality q(k) belongs to the interval from zero to one when interpreted as a valid probability.

An annuity-due payment in subperiod j occurs at k+j/m; an annuity-immediate payment occurs at k+(j+1)/m. The final immediate instalment therefore requires survival to the following policy anniversary. In each policy year, uniform distribution of deaths (UDD) specifies

$$S_{\mathrm{UDD}}(s\mid k)=1-s q(k),\qquad 0\le s\le 1,$$

whereas constant force of mortality specifies

$$S_{\mathrm{CF}}(s)=\exp(-\mu s).$$

The exponential model assumes a constant force mu over the relevant duration; it is not silently identified with UDD. Constant force of interest delta yields D(t)=exp(-delta*t), but the finite annuity definitions also permit an arbitrary discount function with explicit nonnegativity hypotheses when required.

Formalization targets

Within-year survival and discount timing

Construct separate linear and exponential survival models, conditional UDD survival after fraction s, a constant-interest discount factor and the exact indexed instalment time. Establish the zero-duration and full-year boundaries, positivity and monotonicity under justified probability assumptions, conditional-survival multiplication, exponential multiplicativity, and a discount-factor splitting identity. The conditional UDD formula divides by survival at s; a zero-survival endpoint requires an explicit exclusion.

The within-year decomposition is

$$S_{\mathrm{UDD}}(s+t\mid k) = S_{\mathrm{UDD}}(s\mid k)-tq(k),$$

and the conditional expression divides the left-hand side by S_UDD(s|k) when this is positive.

Frequency-dependent annuity cashflow valuation

Define a finite n-year annuity-due as the discounted weighted double sum

$$V^{(m)}_{\mathrm{due}} =\sum_{k=0}^{n-1}\sum_{j=0}^{m-1} \frac{c(k)}{m}D\!\left(k+\frac{j}{m}\right) p(k)\left(1-\frac{j}{m}q(k)\right).$$

Define immediate valuation by changing both the payment time and within-year survival exposure to (j+1)/m. These definitions specify exact UDD actuarial values under the stated unconditional annual survivor weights, rather than using an approximation to annual payments. Establish zero-year and zero-benefit boundaries, linearity, scaling, positivity, and the reduction to annual due valuation for m=1.

For the annual immediate reduction, require the annual survival recurrence p(k+1)=p(k)(1-q(k)). This is necessary because an immediate payment at the annual boundary is conditioned on survival through the full policy year. The case m=0 is retained as an empty finite-sum identity solely to check mathematical totality; it is excluded from economic payment-frequency interpretation.

Fractional premiums and policy reserves

The equivalence principle premium rate is the expected discounted benefits divided by the present value of a unit-premium annuity. The associated balance is

$$\pi A=B,\qquad \pi=\frac{B}{A},\qquad A\ne0.$$

Here A is a dimensionless instalment-weighted annuity value, B is in currency and pi is currency per year of nominal premium rate. The denominator is required to be nonzero for the funding identity, and positive if the quantity is interpreted as an economically valid payment stream.

For a death benefit payable at the end of the policy year, a retrospective fractional survivor reserve, measured at s after that year's premium has been received, satisfies the conditional balance

$$V_s (1-sq)+sq\,b\,D_{s,1} =(V_0+\pi)G_{0,s},$$

where G_{0,s} is accumulation from the anniversary to s, and D_{s,1} discounts an end-year death payment back to s. The reserve is conditioned on survival to s; require 1-sq\ne0. Prove the opening, zero-mortality, end-year and zero-death-benefit boundary identities. These statements do not assert that all deaths occur at an anniversary.

Capstone theorem

ActuarialValuation.frFractionalValuation_fundamental connects annual reduction for a single due instalment, equivalence-premium funding, exact conditional within-year reserve reconciliation, and positivity of finite-time constant-force survival. The theorem keeps the two mortality assumptions in separate propositions.

Significance

As described in Promislow (2015), fractional valuation provides a common time axis. The graph establishes a common, formally stated time axis for fractional pension and life-insurance cashflows. It distinguishes the recipient's conditional survival at payment from the insurer's future death-benefit payment obligation. The finite indexed formulation supports later derivation of m-thly life-contingent premium conversion, changes in reserving basis and comparison with continuous annuity integrals. The theorem graph can also be composed with existing annual actuarial-valuation work once published theorem identities and exact dependencies have been independently verified.

Difficulty

The main sources of mathematical risk are year-end payment conventions, the survival status of an annuitant exactly at an instalment boundary, the difference between UDD and constant force, and division by the probability of being alive at the valuation duration. The initial model is finite and avoids an unjustified assertion that every m-thly sum converges to a continuous value. Such limiting claims require a further integrability and regularity layer and are reserved for an explicitly justified extension.

The graph includes actual mathematical content beyond zero and cancellation identities: conditional-survival reconciliation, exact change of payment frequency, additivity of survival-discounted cashflows and survivor-weighted reserve funding. The numerical checks and remote declaration checks should be reviewed independently. A successfully elaborated sorry declaration remains unproved.

Formalization scope

There are 15 proposed definitions, 38 open theorem targets and 37 subordinate milestone descriptions. The mathematical objects include finite event-weighted cashflow sums, an explicit discount factor, UDD and constant-force survival, and retrospective fractional-duration reserves. The item specifications are the authoritative proposed Lean propositions. Hypotheses on q, s, m, the annual survivor recursion and the premium annuity denominator are present only where required for a proposition.

The mission does not yet include Woolhouse asymptotic expansions, rigorous m\to\infty convergence, a general interest-rate term structure or non-UDD reserve interpolation. Those are identifiable continuation targets rather than presumed established results. No owner item is to be confirmed and no proposal submitted for moderation without human source and mathematical review.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Third Edition, John Wiley & Sons, Chapters 4, 7 and 8. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
• Society of Actuaries (2018), Life & Annuity Symposium, session 033, UDD interpolation and exposure conventions. https://www.soa.org/498941/globalassets/assets/files/e-business/pd/events/2018/las/pd-2018-05-las-session-033.pdf