Mission
Actuarial Mathematics LXXV: Multi-State Transition Values and Duration-Dependent Reserves
Log in to contributeGoal
Multi-state actuarial models capture payments depending on whether an insured person is active, disabled or exited, and on transitions between these statuses. Promislow's Fundamentals of Actuarial Mathematics (2015), Chapter 19 studies nonstationary Markov chains, continuous transition forces, reserve equations and semi-Markov models. Dickson, Hardy and Waters (2009), Chapter 8 provides an actuarial multiple-state foundation. Earlier formal missions cover finite transition recursions and disability-state benefit valuation; this extension concentrates on transition-mass conservation, two-period nonstationary composition and explicit sojourn-duration resets needed for semi-Markov policies.
A three-state transition model represents active, disabled and exited statuses, with finite conditional matrix T(i,j) and beginning-of-year state mass p(i). The outgoing row mass must be one and probabilities nonnegative for a valid stochastic model; the total state mass is preserved when these assumptions hold. A second transition matrix U may differ from T, allowing a nonstationary model. The Chapman-Kolmogorov two-period distribution is (pT)U=p(TU). Benefits may depend on the destination state or the exact ordered pair of origin and destination states. The one-period actuarial reserve comprises current-year state benefit plus a discounted conditional mean of next-period liabilities.
All declarations below are original derived actuarial formal results. The supporting milestone order builds an intentional mathematical chain to a single root theorem.
This block contributes 17 theorem targets and 6 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.msApplyTwo_mass`:
Two successive stochastic transition years conserve total cohort probability.
This block contributes 17 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.msNetProfit_reconcile`:
Premium allocation exactly partitions earnings, expenses and expected claims.
This block contributes 13 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.msMultiStateReserves_fundamental`:
The capstone couples exact stochastic population conservation, the full non-stationary Chapman-Kolmogorov identity, origin-state prospective reserve valuation and the duration-sensitive semi-Markov specialisation.
The main target is `ActuarialValuation.msMultiStateReserves_fundamental`. The capstone couples exact stochastic population conservation, the full non-stationary Chapman-Kolmogorov identity, origin-state prospective reserve valuation and the duration-sensitive semi-Markov specialisation.
The published semi-Markov insurance model emphasises duration dependence, surrender and paid-up transitions rather than forcing every policyholder into a Markov model. The mission introduces sojourn duration d explicitly: remaining in state i gives d+1, while entering a different state resets duration to zero. This changes which next-period reserve V(j,d') should be valued. A precise difference theorem shows how changing elapsed duration changes actuarial reserves through a changed conditional transition law. The fixed-duration Markov case is recovered without assuming all semi-Markov contracts have duration-independent cash flows.
Previously established actuarial theory supplies the probability and valuation setting; this mission proposes additional original derived formal theorems whose Lean proofs remain open.
A complete row stochastic matrix is necessary for mass conservation, and each conditional transition probability is separately nonnegative. Chapman-Kolmogorov must sum over all intermediate states, including absorbing exits, without assuming T=U. The reserve is sensitive to payment timing: a current cashflow at the valuation instant is not discounted but future continuation reserves are. Disability benefits can vary with duration; reset occurs on actual state change rather than at every new policy year. Continuous-time generator differential equations are intentionally not claimed by this discrete-time Lean 4 model. This is a formal finite base for downstream generator and Thiele analysis with targeted Mathlib finite-sum imports.
The mission formalizes finite nonstationary three-state Markov and duration-dependent semi-Markov one-step reserve relations with genuine probability-weighted cashflows. It excludes the vacuous substitution of a claimed identity as a model assumption: mass preservation is derived from row normalisation, and two-step propagation is reconciled by rearranging real finite sums. The theorem graph does not assert that disability and recovery rates can be recovered from incomplete cohort tables without assumptions or that a discrete reserve equation proves a continuous Thiele ODE. It prepares such future stochastic extensions with explicit sojourn-duration changes.
These are original derived finite/analytic Actuarial 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 msMultiStateReserves_fundamental (p b V : Fin 3 → ℝ) (T U : Fin 3 → Fin 3 → ℝ) (discount : ℝ) (duration : ℕ) (Td : ℕ → Fin 3 → Fin 3 → ℝ) (hT : ∀ i, msRowMass T i=1) (hU : ∀ i, msRowMass U i=1) : (msMass (fun j => msStep p T j)=msMass p) ∧ (∀ k : Fin 3, msApplyTwo p T U k=msStep p (msTwoStep T U) k) ∧ (∀ i : Fin 3, msReserveOne b T V discount i=b i+msTransitionCost T V discount i) ∧ (∀ i : Fin 3, msSemiReserve b Td V discount duration i = msReserveOne b (Td duration) V discount i) := by sorry end ActuarialValuation
The capstone couples exact stochastic population conservation, the full non-stationary Chapman-Kolmogorov identity, origin-state prospective reserve valuation and the duration-sensitive semi-Markov specialisation. The full Lean declaration specifies the finite boundaries, exact units and any positivity, independence or regularity assumptions. This is an original derived Actuarial mathematical statement, not a claim of a numbered previously published theorem.
Mathematical relation:
No open leaves. Every sub-goal is proved or awaiting decomposition.