Motivation

This work is motivated by the IFoA CM1 financial and life-contingent mathematics syllabus (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). Financial mathematics provides the time-value backbone of actuarial pricing and pension liability management. The CM1 formula sheet records effective interest and discount rates, annuity-certain relationships, loan amortisation and bond duration. These should be proved as one connected mathematical construction culminating in the local Redington immunisation conditions, rather than as separate missions of two-line rearrangements. A correct proof handles actual discounted dated cashflows and the consistency of their rate derivatives. The IFoA 2026 CM1 financial mathematics syllabus provides the subject boundaries.

Setting

The established CM1 modelling conventions and previously known actuarial identities provide the conceptual background, while the following larger original-derived Lean results still need accepted proofs. The stated nontrivial capstone excludes vacuous equal cashflow or zero-duration substitutes. Each accepted module could become reusable infrastructure for future actuarial formalisation missions.

Real-valued effective annual interest i is restricted to i greater than minus one where cashflow discount factors need to remain positive. A finite dated cashflow c(k) is payable at time k+1. The annual discount factor is (1+i) raised to the negative integer horizon, implemented as a reciprocal of an accumulated factor. Unit annuities in advance and arrears use dates k and k+1 respectively. The cashflow valuation V(i) is a finite weighted sum. A loan balance at t is the present value of remaining loan installments. Duration and convexity numerators aggregate discounted times and squared-time coefficients of cashflows. Asset and liability streams are compared at a single flat effective rate, so rate derivatives are well-defined on the positive accumulation domain.

Formalization targets

All declarations below are original derived CM1-style formal results. The supporting milestone order builds an intentional mathematical chain to a single root theorem.

Interest rate algebra

This block contributes 10 theorem targets and 4 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.

Representative theorem ActuarialValuation.cm1NominalInterest_scale:

$$j^{(m)}=mj$$

Nominal rate scales the periodic effective interest input.

Annuity certain identities

This block contributes 11 theorem targets and 3 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.

Representative theorem ActuarialValuation.cm1IncreasingImmediate_succ:

$$(Ia)_{n+1}=(Ia)_n+(n+1)v^{n+1}$$

Increasing annuity recurrence uses the next arithmetically increasing payment.

General cashflows and loan balances

This block contributes 10 theorem targets and 2 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.

Representative theorem ActuarialValuation.cm1LoanBalance_nonneg:

$$B_t\ge0$$

Remaining positive scheduled loan payments have nonnegative prospective value.

Bond pricing and immunisation

This block contributes 12 theorem targets and 4 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.

Representative theorem ActuarialValuation.cm1RedingtonImmunisation_fundamental:

$$S(i_0)=S'(i_0)=0,\ S''(i_0)>0 \Longrightarrow S(i)\ge0\text{ locally}$$

The genuine Redington second-derivative test gives a local surplus minimum at the matching effective yield; it does not assert global or arbitrary curve immunisation.

Capstone theorem

The main target is ActuarialValuation.cm1RedingtonImmunisation_fundamental. The genuine Redington second-derivative test gives a local surplus minimum at the matching effective yield; it does not assert global or arbitrary curve immunisation.

$$S(i_0)=S'(i_0)=0,\ S''(i_0)>0 \Longrightarrow S(i)\ge0\text{ locally}$$

Significance

The established actuarial syllabus identifies the relevant relationships and applications (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). Matching current assets and liabilities without checking interest-rate sensitivity is inadequate. A valuation system should reconcile cashflow present values, annuities, prospective loan balances, duration and convexity, and verify that asset surplus cannot turn negative under sufficiently small yield movements when Redington's strictly positive second-derivative condition holds. These equations are reused in actuarial annuity and pension schemes. The mission formalises genuine financial relationships as a graph: compound accumulation leads to discount factors, then discounted cashflow valuation and rate derivatives, ending with a strict local minimum argument. The latter is more substantial than algebraic definition expansion.

Difficulty

Theorems must preserve distinctions between interest and discount rates and between annuities in advance and arrears. Positive accumulation is essential where inverse factors are cancelled or differentiated. Loan prospective value must include only payments remaining after the valuation date. Duration is a ratio whose denominator must be nonzero. Redington immunisation is a genuinely local twice-differentiable result requiring matched PV, first derivative and strictly positive second derivative at an interior yield. It does not provide protection from arbitrary nonparallel yield-curve shifts or sufficiently large interest-rate movements. A proof must establish smoothness of the finite rational cashflow surplus near i₀, rather than assuming local minimisation as a hidden premise.

Formalization scope

The model is deterministic finite cashflow financial mathematics. Mortality-weighted uncertain payments can later be inserted as expected cashflow amounts. Explicit coupon, redemption, loan and annuity terms share the same discounting convention. The capstone uses the actual finite asset-minus-liability discounted cashflows. This is a flat-yield Redington local test only. It is mathematically strong and may be difficult to complete because the second derivative theorem requires calculus and finite-sum differentiability, but no artificial axiom or proof placeholder may count as a solved result.

These are original derived finite/analytic CM1 formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

• Institute and Faculty of Actuaries, CM1 Actuarial Mathematics Syllabus (2026). https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf
• David C. M. Dickson, Mary R. Hardy and Howard R. Waters, Actuarial Mathematics for Life Contingent Risks (2009). https://www.cambridge.org/core/books/actuarial-mathematics-for-life-contingent-risks/51C0B04099D4DE1D1DDEF9551024133B/listing
• F. M. Redington, Review of the Principles of Life-Office Valuations (1952); contextual discussion and institutional course treatment in CM1 Actuarial Mathematics Syllabus (2026). https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf