Motivation

The stochastic approach to insurance pricing treats discounted benefit payments and premium receipts as random variables driven by the policyholder's lifetime and contract cashflow design. This approach makes it possible to study expected insurance losses, second moments, tail probabilities and the adequacy of different premium rates. Promislow (2015), Chapters 15 and 16, develops insurance and annuity random present values, loss distributions, the equivalence principle and percentile premiums.

Earlier Prove2Me actuarial missions have considered expectations, moment identities and reserve recursions. This mission proposes a coherent additional distributional layer using genuinely random, state-dependent present values and finite scenario probabilities. Published mathematical methods already establish the underlying theory, but all of the Lean statements here remain original derived open theorem targets. None is a claim that a remote definition compilation supplies an accepted proof.

Setting

The outcome space is a finite set of insured lifetime scenarios indexed by Fin n. Each scenario i has probability mass p(i), discounted benefit B(i) in currency units and discounted unit-premium annuity A(i) in years or in the adopted unit-premium scaling. Valid probabilities satisfy

$$p(i)\ge 0,\qquad \sum_{i\in \operatorname{Fin}(n)}p(i)=1.$$

The index n=0 has no scenarios and cannot support a normalised probability law. Mathematical empty-sum identities remain useful for checking boundary behaviour, while actuarial interpretations require a nonempty normalised scenario space.

At annual premium rate P, the random prospective loss at issue is

$$L_P(i)=B(i)-P A(i).$$

Each component is evaluated on the same realised scenario, preserving the correlation induced by common survival time. Whole-life, endowment, and term insurance can be represented through the scenario benefit schedule. A term policy covers specified death years k < N; covered death benefits are paid at k+1 and a death at or after the term boundary receives no term death benefit. A separate endowment benefit may be payable at maturity.

Formalization targets

Finite random present values of insurance benefits and premium streams

The first group defines benefit PV, premium stream PV, scenario loss, term-cover PV and an endowment event split. The resulting identities relate prospective loss to the benefit and premium cashflows path by path. They include zero-benefit, zero-premium and scaling checks to preserve monetary units and exclude temporal ambiguity.

The key pathwise accounting identity is

$$L_P(i)+P A(i)=B(i).$$

While algebraically transparent, this equality determines which realised random variables must subsequently be used when constructing the loss distribution and its expectation.

Equivalence premiums and loss variance

Define finite expectation and second raw moment by

$$\mathbb E[L]=\sum_i p(i)L(i),\quad \mathbb E[L^2]=\sum_i p(i)L(i)^2,$$

and define variance as E[L²]-(E[L])². Under nonnegative, normalised scenario masses, the variance theorem must prove nonnegativity by a genuine weighted convexity argument. There is no assumption that loss has only nonnegative support; negative losses correspond to profitable realised outcomes.

The equivalence-principle premium, under nonzero expected premium annuity E[A], is

$$P_{\mathrm{EP}}=\frac{\mathbb E[B]}{\mathbb E[A]},\qquad \mathbb E[L_{P_{\mathrm{EP}}}]=0.$$

The denominator condition is essential. Expense loading is explicitly separated as a monetary surcharge or premium margin. An additional group of identities handles finite portfolio expected values and their linearity. An additive variance model for genuinely independent portfolio losses requires independent stochastic assumptions and is not asserted automatically by the finite arithmetic expression.

Actual loss distribution and percentile premium adequacy

The loss CDF is constructed from realised values, rather than introduced as an uninterpreted function:

$$F_{L_P}(z)=\sum_{i:L_P(i)\le z}p(i).$$

It includes atoms exactly at the threshold. The exact mass at z is the sum over scenarios whose loss equals that value. Separate targets establish CDF nonnegativity, monotonicity, normalisation above the maximum of finite support and vanishing mass below its minimum. Every assertion that a weighted sum represents a probability includes nonnegative mass conditions.

Premium adequacy at annual rate P is

$$\Pr(L_P\le0) =\sum_{i:B(i)\le P A(i)}p(i).$$

This is the actual probability that realised discounted premium income covers the realised discounted claims obligation. For a required solvency probability α, a percentile premium must satisfy Pr(L_P≤0)≥α. The probability level is prescribed explicitly, with meaningful economic values lying between zero and one. Where scenario annuity values are nonnegative, increasing the premium cannot reduce adequacy probability. Boundary equality is included in the adequately funded event.

For constant unit premium annuity, the premium-adequacy probability is the benefit CDF evaluated at the proposed premium. With variable annuity values, the full loss distribution must be used instead.

Capstone theorem

The theorem ActuarialValuation.pvRiskPremium_fundamental establishes three linked statements: the equivalence premium produces zero expected prospective loss, actual adequacy probability equals the CDF of realised loss at zero, and a premium increase preserves an explicitly stipulated percentile adequacy threshold. The first statement alone provides no claim that a given high percentile target is met. The capstone requires normalised nonnegative probability weights, nonnegative scenario premium annuity values, a nonzero expected annuity and an ordered comparison of premium rates.

Significance

The finite random-loss model provides a reusable way to distinguish pricing by expected cost from pricing by an insurance-loss tail constraint. These are central actuarial techniques documented by Promislow's stochastic insurance chapters. It also supplies a prospective bridge to a more general measurable lifetime and present-value integral model, compound aggregate insurance loss, reserve distributions and market risk allowances. The distinction between expectation, event probability and required percentile is preserved directly in Lean target types.

Difficulty

Positive expected-value pricing can coexist with a substantial probability of loss. For example, a two-scenario benefit distribution with mass two-thirds at zero and one-third at three has expected benefit one under a unit premium annuity. An equivalence premium of one covers claims in only two-thirds of scenarios, well below a ninety per cent adequacy threshold. This is a direct mathematical counterexample to treating an equivalence premium as universally percentile-adequate.

The assumptions that probabilities sum to one, that scenario masses are nonnegative, and that the premium annuity is nonnegative matter to the capstone. A zero denominator invalidates the equivalence funding equation. The CDF includes equality at its threshold, and scenario indices need not identify distinct loss values because separate scenarios may produce the same loss. Variance proof needs the actual normalised distribution.

Formalization scope

There are 18 reusable definitions, 40 open theorem targets and 39 supporting milestone descriptions. The mission operates on a finite probability mass model with scenario-dependent discounted benefits and premium annuities. This provides exact finite loss distributions and mathematical endpoint handling without inventing a density for a discrete variable. Term benefits, endowment-event selection, expected benefits, second moments, loadings and percentile adequacy appear in the target graph.

Continuous loss distributions under exponential lifetime, nontrivial portfolio dependence, conditional reserve-loss distributions, general law-invariant risk measures and asymptotic aggregate premium principles require further work. This mission does not claim these general results, and no open sorry stub represents a verified theorem proof. Numerical examples are independent sanity checks, with the remote compiler serving solely as an authoritative declaration-elaboration validator.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Third Edition, Wiley, Chapters 15–16. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
• Society of Actuaries (2006), Education Catalog: Actuarial Mathematics, Life Contingencies and Loss Distributions, Society of Actuaries. https://www.soa.org/globalassets/assets/files/edu/fall2006webcatalog.pdf