Mission
Actuarial Mathematics XLVI: Gross Premiums, Reserve Recursions, Profit Testing and Minimal Zeroisation
Log in to contributeGoal
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). Actuarial life insurance pricing is incomplete without the link between gross premiums, future reserve liabilities, emerging cashflow profits and risk capital requirements. The IFoA CM1 syllabus explicitly includes gross prospective and retrospective reserves, death strain, mortality profit, profit signatures, profit testing for unit-linked business and elimination of negative non-unit profit cashflows by reserve zeroisation. Dickson, Hardy and Waters (2009), Chapter 11 (Emerging costs for traditional life insurance) supplies the broader profit testing theory. We combine these elements into one connected mission with an optimisation property as its capstone.
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.
A contract has dated benefit payments, expenses, premiums and probability/discounter weights over a finite horizon N. Gross level premium divides the total expected benefit and expense PV by a nonzero premium annuity factor. A prospective reserve equals expected future outgo less future premiums, and a retrospective reserve uses prior accumulated premiums less outgo on the same valuation basis. Death strain at risk measures the claim amount net of the next reserve release. For unit-linked products the unit fund develops through allocation, charges and investment returns. Non-unit projected cashflow c(t) combines premium and charges less expenses and claims. The non-unit reserve R(t), growth factor g(t)>0 and survival/continuation weight s(t)≥0 determine projected profit Π(t)=c(t)+g(t)R(t)-s(t)R(t+1), with terminal reserve R(N)=0.
All declarations below are original derived CM1-style formal results. The supporting milestone order builds an intentional mathematical chain to a single root theorem.
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.cm1ExpectedBenefitPV_add_last:
Finite expected benefit PV recurses correctly when one extra payment term is appended.
This block contributes 11 theorem targets and 5 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.cm1MortalityProfit_favourable:
With positive death strain, fewer actual deaths than expected produce favourable mortality profit.
This block contributes 10 theorem targets and 5 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.cm1ProfitMargin_nonneg:
Profit margin is nonnegative if projected profit is nonnegative and the premium base positive.
This block contributes 12 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.cm1ZeroisationOptimality_fundamental:
The finite-horizon capstone proves that a backwards-zeroised reserve produces nonnegative projected profits and is pointwise minimal among all nonnegative feasible reserve paths with the same terminal boundary.
The main target is ActuarialValuation.cm1ZeroisationOptimality_fundamental. The finite-horizon capstone proves that a backwards-zeroised reserve produces nonnegative projected profits and is pointwise minimal among all nonnegative feasible reserve paths with the same terminal boundary.
The established actuarial syllabus identifies the relevant relationships and applications (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). The zeroisation recursion can be used to eliminate projected negative future non-unit profits while avoiding excessive reserve financing. It is valuable to show that the backwards reserve is not only feasible but pointwise minimal among all competing nonnegative reserve profiles satisfying the same profit and terminal constraints. Such a theorem is an auditable dynamic optimisation guarantee, not merely a spreadsheet check. It also provides a bridge from earlier finite cashflow PV and insurance reserve missions to modern policy profit testing. The intermediate theorem groups separate gross premium equivalence, death strain, reserve valuation, unit funds, discounted profit signatures and zeroisation.
The formal model carefully distinguishes net benefit cashflows and reserve-adjusted profit, and never calls a gross premium formula universally correct without its equivalence assumptions. In zeroisation, g(t) must be strictly positive before division and multiplication inequalities can be reversed, while s(t)≥0 is necessary to compare different next-year reserve requirements. The floor max(0,(sRnext-c)/g) is a genuine feasibility threshold. The minimality result needs backward induction from the same terminal reserve, not a false forward monotonicity argument. Negative non-unit cashflows and zero survival are meaningful cases. The result does not equate the risk discount rate used for net present value with the investment growth rate g(t).
This is a finite-horizon deterministic expected-cashflow model rather than a fully stochastic regulatory reserve basis. Probability, benefit and expenses schedules enter as given finite arrays. Gross premiums use the simplified actuarial equivalence principle and not arbitrary commission or investment-profit target structures. The non-unit zeroisation capstone is conditional on a reserve path satisfying the specified backward recursion; its existence can be constructed by a later recurrence theorem and should not be replaced by a hidden axiom. All explicitly stated profit constraints and nonnegative reserve bounds are maintained for each pre-terminal valuation date. The theorem is meaningful even when cashflow c(t) is negative.
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.
namespace ActuarialValuation theorem cm1ZeroisationOptimality_fundamental (c s g R Q : ℕ → ℝ) (N : ℕ) (hR : cm1ZeroReserveCondition c s g R N) (hg : ∀ j ∈ Finset.range N, 0 < g j) (hs : ∀ j ∈ Finset.range N, 0 ≤ s j) (hQend : Q N = 0) (hQpos : ∀ j, j ≤ N → 0 ≤ Q j) (hQprof : ∀ j ∈ Finset.range N, 0 ≤ cm1ReserveYearProfit c s g Q j) : (∀ t ∈ Finset.range N, 0 ≤ cm1ReserveYearProfit c s g R t) ∧ (∀ t, t ≤ N → R t ≤ Q t) := by sorry end ActuarialValuation
The finite-horizon capstone proves that a backwards-zeroised reserve produces nonnegative projected profits and is pointwise minimal among all nonnegative feasible reserve paths with the same terminal boundary. The full Lean declaration specifies the finite boundaries, exact units and any positivity, independence or regularity assumptions. This is an original derived CM1 mathematical statement, not a claim of a numbered previously published theorem.
Mathematical relation:
No open leaves. Every sub-goal is proved or awaiting decomposition.