Probability

Motivation

Large technology firms often buy small startups mainly to hire their staff, a practice known as acquihiring. Antitrust authorities review acquisitions that may reduce competition in product markets, but an acquihire can instead reduce competition in the labour market: a firm that buys the employer of a scarce worker no longer has to outbid that employer for her. Bar-Isaac, Johnson and Nocke study this effect in a three-player model: a startup, its essential employee, and a potential acquirer (CRC TR 224 Discussion Paper No. 500, 2024; published in Management Science, 2025, doi:10.1287/mnsc.2024.04604).

In the paper's baseline model (Proposition 1) the acquirer, whenever it hires the employee, does so by buying the startup, and the employee always prefers direct wage competition. This mission formalizes §6, where the employee's private benefit from staying at the startup is her private information. That uncertainty softens wage competition, so acquihiring is no longer always chosen, and the paper derives the exact threshold at which the acquirer switches.

Setting

An employee produces value $v_a$ if she works for the acquirer and $v_s$ if she works for the startup. At the startup she also enjoys a private benefit $b$, which only she observes and which is uniformly distributed on $[0,B]$. She has an outside option worth $0$, and wages are unrestricted real numbers. The standing assumptions of §6 are

$$0 < B < \min\{v_a, v_s\}, \qquad v_s - B < v_a < v_s + 2B .$$

The acquirer chooses between two modes.

• Direct hiring. The acquirer and the startup make simultaneous wage offers $w_a$ and $w_s$. A type-$b$ employee joins the acquirer when $w_a > w_s + b$ and $w_a \ge 0$, and stays at the startup when $w_s + b \ge w_a$ and $w_s + b \ge 0$. Expected profits are averages over $b \sim U[0,B]$, for example

$$\pi_a(w_a, w_s) = \frac1B \int_0^B (v_a - w_a)\,\mathbf 1\{\text{type } b \text{ joins the acquirer}\}\,db .$$

A pair $(w_a, w_s)$ is an equilibrium of this wage game when each offer is a best response to the other over all real wages.

• Acquihiring. The acquirer bids for the startup. A startup that is a monopsonist pays wage $0$ and earns $v_s$, so the acquisition succeeds at price $v_s$ exactly when $v_a > v_s$, and the acquirer then pays the employee $0$. The acquirer's acquihiring profit is $\max\{0, v_a - v_s\}$ (Lemma 2 of the paper with wage floor $0$).

The quantities named in the statements are Lemma 5's wages

$$w_a^* = \frac{2v_a + v_s - B}{3}, \qquad w_s^* = \frac{2v_s + v_a - 2B}{3},$$

the indifferent type $b^* = (v_a - v_s + B)/3 = w_a^* - w_s^*$, and the threshold

$$\hat v_a = v_s + \frac{7 - 3\sqrt5}{2}\,B .$$

Formalization targets

Goal: Proposition 5

Under the standing assumptions, $\hat v_a > v_s$, $(w_a^*, w_s^*)$ is a direct-hiring equilibrium, and

$$v_a > \hat v_a \;\Longrightarrow\; \pi_a(w_a^*, w_s^*) < \max\{0, v_a - v_s\},$$ $$v_a < \hat v_a \;\Longrightarrow\; \max\{0, v_a - v_s\} < \pi_a(w_a^*, w_s^*) \ \text{ and the poaching probability is } \frac{v_a - v_s + B}{3B}.$$

In addition, every type $b \in [0,B]$ of employee is strictly better off under direct hiring than under acquihiring.

Milestones

1. A monopsonistic startup sets wage $0$ and earns $v_s$; a monopsonistic acquirer sets wage $0$ (§6, p. 15).
2. Lemma 5: the direct-hiring wages, the poaching probability $(v_a - v_s + B)/(3B) \in (0,1)$, and the acquirer's profit $(v_a - v_s + B)^2/(9B)$.
3. The two values of $v_a$ at which the profits are equal, $\hat v_a$ and $v_s + (7 + 3\sqrt5)B/2$, and the fact that the second lies above $v_s + 2B$.
4. The welfare display in the proof of Corollary 4, and Corollary 4 itself: acquihiring is more efficient than direct hiring exactly when $v_a > v_s + \tfrac45 B$, so on $\tfrac{7-3\sqrt5}{2} < (v_a - v_s)/B < \tfrac45$ the acquirer acquihires although direct hiring yields more surplus.

Significance

The proposition separates two effects that coincide in the baseline model. Without private information, wage competition is Bertrand-like: the winning firm must match the losing firm's full willingness to pay, so buying the competitor is always cheaper. With a privately known benefit, competition between the two employers resembles product differentiation, and each offers less than the employee's productive value. Direct hiring then becomes profitable when $v_a$ is close to $v_s$, and acquihiring is chosen only when $v_a - v_s$ exceeds $\frac{7-3\sqrt5}{2}B \approx 0.146\,B$. Corollary 4 compares this threshold with the efficiency threshold $\frac45 B$ and finds a band of parameters in which acquihiring occurs although it lowers total surplus. That band is the paper's case for labour-market scrutiny of acquisitions.

The results are proved on paper, by first-order conditions and a quadratic comparison. None of them has a machine-checked proof, and the platform has no prior formalization of wage competition, monopsony or acquisitions. The mission adds an explicit Bayesian wage game with expected profits written as integrals over the type distribution, with global best responses rather than first-order conditions. The objects are small enough to be reused for other two-firm wage-posting models with a uniformly distributed taste shock.

Difficulty

The algebra of Proposition 5 is a quadratic inequality in $(v_a - v_s)/B$. The work is in Lemma 5. The page solves first-order conditions inside the region $w_a \ge 0$, $0 < w_a - w_s < B$, where both expected profits are concave quadratics. An equilibrium, however, requires that no deviation pays anywhere on the real line, including offers so low that no type accepts and offers so high that every type accepts. Outside the interior region the profit functions are piecewise (zero below, linear above), and each piece has to be compared with the interior optimum. The expected profits are interval integrals of indicator functions, so evaluating them requires the measure of the set of accepting types. Ties between the two offers occur with probability zero, and the statements are insensitive to how they are broken.

Formalization scope

All quantities are real numbers. The parameters $v_a$, $v_s$, $B$ form a structure, and the five standing inequalities form a predicate that every theorem except the pure-algebra milestone takes as a hypothesis (that milestone needs only $B > 0$). Expected profits, the poaching probability and direct-hiring welfare are $\frac1B \int_0^B$ of bounded, piecewise-constant integrands, hence interval integrable. A verification file evaluates the acquirer's profit at Lemma 5's wages to its closed form on one instance, and exhibits instances of both branches of the proposition and of the window in Corollary 4. Ties $b = w_a - w_s$ go to the startup.

Conventions committed to:

• best responses range over all real wages, which is stronger than the page's first-order conditions;
• the direct-hiring branch is evaluated at Lemma 5's wages, and Lemma 5's uniqueness clause is claimed only within the interior region where the page derives it; uniqueness among all equilibria is not on the page and is not claimed;
• the acquihiring profit $\max\{0, v_a - v_s\}$ and the employee's acquihiring payoff ($0$ if $v_a > v_s$, otherwise her benefit $b$) are Lemma 2's outcomes with wage floor $0$, as §6 states; the milestone on the monopsonistic wage justifies this, and at $v_a = v_s$ the acquisition is taken to fail;
• surplus under acquihiring is $v_a$, the allocation with the employee at the acquirer, as in Corollary 4.

The direct-hiring profit is an integral over the type distribution evaluated at wages that are proved to be an equilibrium. It is not a closed-form payoff taken as a definition. Dropping any standing inequality would change Lemma 5 (the poaching probability leaves $(0,1)$) or Proposition 5 (the second root comes back into range). The employee-preference clause is part of the goal, and no equilibrium is claimed unique beyond what the page derives.

Contributions welcome: the interval-integral evaluations of step functions, the global best-response argument for Lemma 5, and the quadratic comparison with $\sqrt5$.

Selected references

• H. Bar-Isaac, J. P. Johnson, V. Nocke, Acquihiring for Monopsony Power, CRC TR 224 Discussion Paper No. 500, January 2024 (the version formalized here; journal version below).
• H. Bar-Isaac, J. P. Johnson, V. Nocke, Acquihiring for Monopsony Power, Management Science, 2025. https://doi.org/10.1287/mnsc.2024.04604

Motivation

A sequence of real numbers $(m_0, m_1, m_2, \dots)$ often arrives as a list of moments: averages $\mathbb E[X^n]$ of powers of a random variable, traces $\langle T^n e, e\rangle$ of powers of a self-adjoint operator, or coefficients of a continued fraction. The Hamburger moment problem, named after Hans Ludwig Hamburger (1920–21), asks when such a list really comes from a measure on the whole real line, and, when it does, whether the measure is determined by its moments. The question sits at the junction of probability (the method of moments, identification of limit laws), spectral theory of symmetric operators and Jacobi matrices, and the theory of orthogonal polynomials; standard monographs include Shohat–Tamarkin (1943) and Schmüdgen (2017).

Timeline (as summarized in the source article and its references):

1. 1894 — Stieltjes treats the analogous problem on $[0,+\infty)$ (the Stieltjes moment problem).
2. 1920–21 — Hamburger extends the theory to the whole real line: solvability is equivalent to positivity of the Hankel kernel $(m_{j+k})$.
3. 1920s — Carleman gives a growth condition on the moments guaranteeing uniqueness (Carleman's condition); the factorial growth bound $|m_n| \le C D^n n!$ is a special case (Reed–Simon 1975, p. 205).
4. Later — the operator-theoretic treatment through self-adjoint extensions of the shift operator and its spectral measure becomes standard (Reed–Simon 1975, p. 145).

Setting

Let $m = (m_n)_{n \ge 0}$ be a sequence of real numbers. A solution of the Hamburger moment problem for $m$ is a positive Borel measure $\mu$ on $\mathbb R$ such that every power $x^n$ is $\mu$-integrable and

$$m_n = \int_{-\infty}^{\infty} x^n \, d\mu(x) \qquad (n = 0, 1, 2, \dots).$$

The sequence $m$ is a moment sequence if at least one solution exists.

The Hankel kernel of $m$ is the infinite matrix $A = (m_{j+k})_{j,k \ge 0}$. It is positive definite (in the sense of the source) if

$$\sum_{j,k \ge 0} m_{j+k}\, c_j \overline{c_k} \;\ge\; 0$$

for every finitary complex sequence $(c_j)_{j \ge 0}$, i.e. $c_j = 0$ for all but finitely many $j$. Its finite sections are the $(n+1)\times(n+1)$ Hankel matrices

$$\Delta_n = (m_{i+j})_{0 \le i,j \le n}.$$

In the Lean development these objects are IsMomentMeasure m μ, IsMomentSequence m, hankelForm m c, HankelPosDef m and hankelMatrix m n, all in the namespace HamburgerMoment.

Formalization targets

Goal — Hamburger's characterization

$$m \text{ is a moment sequence} \iff \sum_{j,k \ge 0} m_{j+k} c_j \overline{c_k} \ge 0 \text{ for every finitary } (c_j) \subset \mathbb C.$$

Milestones

1. The identity $\sum_{j,k} m_{j+k} c_j \overline{c_k} = \int |\sum_j c_j x^j|^2 \, d\mu(x)$ for any solution $\mu$, and the resulting "only if" direction.
2. The "if" direction: a positive definite Hankel kernel is the kernel of a moment sequence.
3. The solution set is convex; hence a solvable problem has either a unique solution or infinitely many.
4. Positivity of $A$ gives $\det \Delta_n \ge 0$ for all $n$; if $\det \Delta_n = 0$ for some $n$, the solution is unique and finitely supported.
5. Uniqueness under the growth bound $|m_n| \le C D^n n!$.
6. Existence of moment sequences with more than one solution.
7. The real-polynomial identity $\int p^2 \, d\mu = \sum_{j,k} a_j a_k m_{j+k} \ge 0$, and the characterization of moment sequences by positive semidefiniteness of all real Hankel matrices $\Delta_n$.

Significance

The result. Hamburger's theorem turns an existence question about measures into a family of finite-dimensional positivity conditions that can be checked on the data. It is the basic tool behind the method of moments in probability (identifying a distribution from its moments, when the problem is determinate), behind the spectral theory of Jacobi matrices, and behind Gauss quadrature and orthogonal polynomials on the line. The uniqueness criteria decide when moments determine a law; the non-uniqueness examples (for instance the log-normal distribution) show that they do not always do so.

Formalizing it. All results here are classical and proved in the literature; to the best of the captain's knowledge none of them is currently available as a formal statement in Mathlib, which has neither moment problems nor Hankel kernels. The mission produces a reusable vocabulary (moment measures, Hankel forms and matrices) and machine-checked versions of the existence theorem, the uniqueness criteria and the non-uniqueness phenomenon.

Difficulty

The "only if" direction is a direct computation. The converse is the substance: from positivity of countably many finite quadratic forms one must produce a countably additive measure on a non-compact space with all moments matching. Compactness arguments on finite sections give measures whose low-order moments match, but mass can escape to infinity and higher moments need not converge; the source's route instead goes through the Hilbert space completion of finitary sequences, self-adjoint extensions of the (generally unbounded) shift operator and the spectral theorem for unbounded self-adjoint operators — machinery that is only partly present in Mathlib. An alternative route via positive linear functionals on polynomials (M. Riesz extension, Riesz–Markov–Kakutani) has to control the same escape of mass. The uniqueness criterion requires quasi-analyticity or Carleman-type estimates.

Formalization scope

1. Sequences are m : ℕ → ℝ; measures are Measure ℝ on the Borel σ-algebra of $\mathbb R$. A solution must have every power $x^n$ integrable, so in particular $\mu$ is finite with total mass $m_0$.
2. Finitary complex sequences are finitely supported functions ℕ →₀ ℂ, and the Hankel form is the finite double sum over the support. "$\ge 0$" is the order on $\mathbb C$ (the value is a nonnegative real number), matching the source.
3. $\Delta_n$ is the real matrix indexed by Fin (n + 1); positive semidefiniteness is Mathlib's Matrix.PosSemidef.
4. Uniqueness statements quantify over all solutions; finite support means the solution vanishes outside a finite set.

Needed infrastructure and welcome contributions: polynomial integrability under finite moments, positive linear functionals on $\mathbb R[x]$, a Riesz–Markov or spectral-measure construction on $\mathbb R$, Vandermonde arguments for finitely supported measures, and Carleman / quasi-analyticity estimates. The definitions of moment measures and Hankel kernels are reusable for the Stieltjes and Hausdorff moment problems.

Selected references

• Wikipedia, Hamburger moment problem, revision oldid=1356180072, https://en.wikipedia.org/w/index.php?title=Hamburger_moment_problem&oldid=1356180072
• H. Hamburger, Über eine Erweiterung des Stieltjesschen Momentenproblems, Math. Ann. 81 (1920), 235–319; 82 (1921), 120–164, 168–187.
• M. Reed, B. Simon, Methods of Modern Mathematical Physics II: Fourier Analysis, Self-Adjointness, Academic Press, 1975, pp. 145, 205.
• T. S. Chihara, An Introduction to Orthogonal Polynomials, Gordon and Breach, 1978, pp. 56, 73.
• K. Schmüdgen, The Moment Problem, Graduate Texts in Mathematics 277, Springer, 2017. https://doi.org/10.1007/978-3-319-64546-9
• J. A. Shohat, J. D. Tamarkin, The Problem of Moments, AMS, 1943.

Motivation

The secretary problem is the standard example of an optimal stopping problem with partial information. It is also known as the marriage problem, the sultan's dowry problem, the fussy suitor problem, the googol game and the best choice problem. It is studied in applied probability, statistics and decision theory. Its solution is often called the 37% rule: a simple rule picks the single best of $n$ applicants with probability about $1/e \approx 0.368$, whether there are 100 or 100 million applicants (Wikipedia: Secretary problem). The problem is a standard example of the exploration–exploitation dilemma.

Timeline (as recounted in the Wikipedia article's History section, following Ferguson 1989):

• 1949: Merrill M. Flood introduces the problem (as the "fiancée problem") in a lecture. It then spreads as folklore through the 1950s.
• 1958: Flood circulates a letter outlining a proof of the optimal strategy. Its appendix by R. Palermo proves that every strategy is dominated by one of the form "reject the first $p$ unconditionally, then accept the next candidate who is better".
• 1960: First publication, in Martin Gardner's Scientific American column (February 1960), with the analysis supplied by Leo Moser and J. R. Pounder.
• 1966: Gilbert and Mosteller, "Recognizing the maximum of a sequence", a detailed study of the problem and many variants.
• 1989: Ferguson, "Who solved the secretary problem?", a historical survey.
• 2000: Bruss's odds theorem, which the article calls the shortest rigorous proof known.

Setting

There is a single position and there are $n$ applicants, where $n$ is known. If seen together, the applicants can be ranked from best to worst with no ties. They are interviewed one at a time in a uniformly random order: each of the $n!$ orders is equally likely. Right after each interview the applicant is either accepted, which ends the process, or rejected for good. The decision may depend only on the relative ranks of the applicants interviewed so far. The objective is to maximize the probability of selecting the best applicant of the whole group.

An order is a permutation $\sigma$ of $\{0,\dots,n-1\}$. The applicant interviewed at time $i$ has quality $\sigma(i)$, where larger means better. The relative rank of the applicant interviewed at time $j$ is the number of applicants interviewed before time $j$ who are worse than them. A stopping rule $s$ maps the list of relative ranks observed so far to "accept" or "reject". Its success probability $P_n(s)$ is the fraction of the $n!$ orders on which the applicant accepted by $s$ is the overall best. A rule that never accepts anyone fails. The optimal success probability is

$$V_n = \sup_s P_n(s).$$

A candidate is an applicant who is better than every applicant interviewed before them. The cutoff rule with cutoff $r$ rejects the first $r-1$ applicants and then accepts the first candidate after that point.

Formalization targets

Goal: the 37% rule

$$\lim_{n\to\infty} V_n = \frac1e .$$

Milestones (following the article's derivation)

1. $P_n(\text{cutoff } 1) = 1/n$.
2. For $2\le r\le n$: $P_n(\text{cutoff } r) = \dfrac{r-1}{n}\displaystyle\sum_{i=r}^{n}\frac{1}{i-1}$.
3. Some cutoff rule with $1\le r\le n$ is optimal among all rank-based stopping rules.
4. The table of optimal cutoffs and optimal success probabilities for $n=1,\dots,10$.
5. If $r_n/n\to x\in[0,1]$, then $P_n(\text{cutoff } r_n)\to x\int_x^1 \frac{dt}{t} = -x\log x$.
6. On $[0,1]$ the function $-x\log x$ has maximum value $1/e$, attained only at $x=1/e$.
7. Optimal cutoffs satisfy $r_n/n\to 1/e$.
8. $V_n \ge 1/e$ for every $n\ge 1$.

Significance

The result. The 37% rule is the classical result of optimal stopping. It shows that a fixed fraction of the best possible success probability survives as the number of options grows without bound, and that a simple threshold policy achieves it. The structure of its solution has three parts: optimal rules may be taken to be threshold rules, there is an exact formula in terms of the records of a uniformly random permutation, and a limit turns a harmonic sum into an integral. This structure recurs throughout the best-choice literature, including the prophet-secretary and multi-choice secretary problems.

Formalizing it. The result has been proved since the late 1950s and early 1960s. The remaining work is to formalize the known proof: a model of rank-based stopping rules over uniformly random permutations, the exact success probability of cutoff rules, the optimality of cutoff rules among all rank-based rules, and the asymptotics.

Difficulty

The success probability of a fixed cutoff rule and the calculus limit are elementary. The central step is the optimality of cutoff rules (Milestone 3). A stopping rule may depend arbitrarily on the whole history of relative ranks, and one has to show that no such rule beats the best cutoff rule. Evaluating cutoff rules alone does not prove the goal, because $V_n$ is a supremum over all rank-based rules. A second, smaller difficulty is that the limit statements need control of the harmonic sums along a varying cutoff $r_n$, not only along a fixed ratio.

Formalization scope

• The sample space is the finite set Equiv.Perm (Fin n) with uniform weights. successProb n s is the ratio (number of winning permutations) / $n!$ in $\mathbb R$.
• A stopping rule is a deterministic function List ℕ → Bool, applied to the list of relative ranks observed so far. Through the length of the list it also knows the current time. It never sees absolute qualities. Randomized rules are not modelled. A randomized rule is a mixture of deterministic ones, so it cannot do better.
• optimalProb n is the real supremum of successProb n s over all such rules. The values lie in $[0,1]$, so the supremum is the usual least upper bound.
• Times are 0-based in Lean (Fin n). Cutoffs $r$ are 1-based, as in the article: cutoffRule r accepts at time $i$ exactly when $i+1 \ge r$ and the current applicant is a candidate.
• $1/e$ is written Real.exp (-1).
• The 1/e-law of best choice (unknown number of applicants, Bruss 1984), the odds algorithm, cardinal-payoff variants and the other generalizations in the article are outside this mission.

All declarations live in the namespace ClassicalSecretary. Reusable contributions are welcome, in particular facts about records of uniformly random permutations (independence of relative ranks, the probability that position $i$ is a record) and a backward-induction principle for finite-horizon stopping problems.

Selected references

• Wikipedia contributors, Secretary problem, sections "Formulation" and "Deriving the optimal policy". https://en.wikipedia.org/wiki/Secretary_problem
• T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 282–289, 1989. https://doi.org/10.1214/ss/1177012493
• J. Gilbert, F. Mosteller, Recognizing the maximum of a sequence, Journal of the American Statistical Association 61(313), 35–73, 1966. https://doi.org/10.2307/2283044
• F. T. Bruss, Sum the odds to one and stop, Annals of Probability 28(3), 1384–1391, 2000. https://doi.org/10.1214/aop/1019160340

Motivation

Uncertain financial returns affect funded pensions, DC saving and endowment adequacy. A single investment rate selected once and held fixed for the full projection is fundamentally different from a genuinely independent sequence of annual investment returns. The former produces expected powers of a single random variable while the latter factorises independent annual gross-return moments. These distinctions underpin the financial risk assumptions in stochastic finance models. Existing actuarial missions cover discounted deterministic cashflows but not these stochastic accumulation and contributions.

Setting

Annual gross returns equal one plus their annual net investment returns. A finite probability space has actual scenario masses with total one, so expectation and variance are weighted finite sums. The fixed-rate accumulation raises the same scenario gross factor to the investment horizon. For independent years the model explicitly constructs a product joint mass p(a)q(b) and verifies the first and second product moments. A real pension fund receives a contribution at the beginning of the year before earning its realised gross return.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Finite-scenario investment returns and fixed random rates

A finite discrete fixed-rate model begins at a sure one.

$$S_n=(1+I)^n,\quad \mathbb{E}[S_n]=\sum_{\omega}p_{\omega}(1+I_{\omega})^n$$

Independent annual returns on actual product scenarios

Actual joint product probability laws establish two independent annual accumulation moments.

$$\mathbb{E}[G_1G_2]=\mathbb{E}[G_1]\mathbb{E}[G_2]$$

Regular contributions and fund first/second-moment recursions

The independent-return pension accumulation recursions reconcile first and second fund moments including contribution cross terms.

$$A_{n+1}=(A_n+c)G_{n+1},\quad m_{n+1}=(m_n+c)\bar G$$

Capstone theorem

The independent-return pension accumulation recursions reconcile first and second fund moments including contribution cross terms.

$$A_{n+1}=(A_n+c)G_{n+1},\quad m_{n+1}=(m_n+c)\bar G$$

Significance

As discussed in Shreve's stochastic-finance treatment, The capstones distinguish random fixed returns from actually independent annual returns without presupposing a target identity. For the latter, the true two-year joint probability law factorises the expected growth and its second moment. Under subsequent iid moment factorisation, a multi-year first and second return moment model yields an exact variance recursion. The fund valuation then derives consistent one-step mean, second-moment and variance formulae with contributions, including the cross-term from previously accumulated assets. The model is useful for genuine stochastic saving, actuarial adequacy and projected pension risk.

Difficulty

It is mathematically false in general that expected compound returns equal the power of the expected rate for a fixed but random interest assumption. Genuine product probability weights, not a definition of independence as the desired conclusion, support the two-year factorisation. For a regular savings fund, the contribution is invested with the previous fund, so the second moment includes a cross term twice the contribution times the prior expected fund. The variance has to be derived from the two independently defined moments with positive gross-return second-moment bounds. All signs and independence restrictions should be preserved at every step.

Formalization scope

Fixed stochastic-rate model and independent annual returns are distinct mathematical constructs in this model. A future substantial probability model could construct fully independent n-year return families and an exact savings accumulation probability distribution, rather than stopping at the two-year product law. The present source has nontrivial results because it independently calculates both moments of an actual joint scenario distribution and reconciles the cross terms in the savings fund variance. Existing stochastic insurance claims calculations alone do not provide an investment growth scenario model. This finite product model and fund recursion are reusable for defined contribution pensions, insurance asset adequacy testing and later cashflow simulations.

For a random interest rate sampled once at issue and held fixed, the expected n-year accumulation is an expectation of a random power, not generally a power of the expected return. If annual investment returns instead vary independently, the gross growth factors are multiplied across years and their expected product factorises. This mission proves the two-year factorisation from genuine independent finite product-state probability masses, without taking independence to mean the target moment identity by definition. For regular savings, contribution timing matters because a beginning-of-period contribution earns that period's return. The second-moment recursion must therefore contain the mixed term twice the contribution times the previous expected fund. These identities provide an actuarial basis for testing pension fund accumulation and capital adequacy, but do not justify a normal or lognormal fund distribution merely from calculated means and variances.

The principal independence derivation is from an actual finite two-year product scenario model, while the general n-year variance is stated as an explicit algebraic moment-factorisation law. Deriving n-way stochastic independence under a full probability measure, lognormal approximate fund distribution and path-dependent contributions remains work for subsequent substantial probability theory. No normal approximation or lognormality is assumed from mean and variance alone. These open theorem targets are not accepted proofs.

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.

Selected references

• S. E. Shreve (2004), Stochastic Calculus for Finance I: The Binomial Asset Pricing Model, Springer. https://link.springer.com/book/10.1007/978-0-387-22527-2
• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Wiley, accumulation and stochastic investment model chapters. https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782521

Motivation

Unit-linked life and pension policies require careful accounting for where gross premiums go, which underlying fund units are purchased and which charges are received by the insurer. The FCA's unit-linked review identifies allocation, management, surrender and other policy charges as distinct insurer cashflows. Earlier actuarial missions XLVI and LXIX already formalise simple unit funds and guarantees, but lack explicit offer/bid unit pricing and a fully reconciled insurer non-unit profit signature.

Setting

A policyholder pays a gross premium, of which an allocation percentage is invested at the offer price and the remainder is retained by the insurer. Unit-holders value their existing holdings using the bid price. Management and fixed administration charges reduce fund assets; a guaranteed minimum death benefit creates an insurer mortality risk above the unit-linked fund. The insurer's non-unit account collects charges and premium differences and separately pays expenses, commissions and mortality guarantee strain.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Premium allocation, bid and offer prices and fund charges

Cancelling no more units than held retains a nonnegative unit account.

$$U_t=U_{t-1}+\frac{a_t P_t}{O_t}-\frac{C_t}{B_t}$$

Risk guarantees, surrender payments and reserve strain

A nonnegative surrender charge cannot increase the positive fund value.

$$B_t^{\text{death}}=\max(F_t,G_t),\quad R_t=(G_t-F_t)^+$$

Non-unit profit signatures and discounted insurer margins

Actual unit premium allocation and bid-offer cost reconcile with the insurer's separate death guarantee obligations and complete non-unit cashflow profit account.

$$\Pi=\sum_t v^t p_t\left(\text{income}_t-\text{outgo}_t\right)$$

Capstone theorem

Actual unit premium allocation and bid-offer cost reconcile with the insurer's separate death guarantee obligations and complete non-unit cashflow profit account.

$$\Pi=\sum_t v^t p_t\left(\text{income}_t-\text{outgo}_t\right)$$

Significance

As discussed in the FCA's unit-linked review, The target reconciles every gross premium unit purchase and retained amount; it values immediate bid-offer spread costs, decomposes guaranteed death benefits into the invested fund plus net insurer amount at risk, and establishes an independent non-unit profit cashflow balance. Additional supporting theorems make the risk discount present value additive across the profit signature, with correct timing of beginning-year premium allocations and end-year fund costs. This provides an exact starting point for insurance policy profit testing and the analysis of charge sensitivity.

Difficulty

Bid and offer prices cannot be interchanged: a unit bought at offer is valued at bid and a positive spread produces a real cost even with unchanged market prices. A premium allocation percentage is not identical to the percentage of bid value created. Death insurance cost is the excess guaranteed benefit above the fund, rather than the total benefit, because fund assets already cover the remainder. The non-unit income and the actual expenses/commission/insurance risk must be kept separate rather than silently netted inside fund performance. The proof must impose suitable positivity on offer prices and fund values.

Formalization scope

Bid-offer spread and non-unit profit signature are distinct mathematical constructs in this model. A future extension will include surrender probabilities, partial withdrawal, guaranteed annuity options and stochastic policyholder behaviour, together with a non-unit reserve liability under the prospective profit-testing basis. The current identities are nontrivial because they distinguish bid-valued units bought at an offer price, actual management charges, underlying expenses and the top-up death cost. Existing unit account and zeroisation missions do not include all these separate components in one coherent insurer profit signature. The explicit fund and charge functions are reusable for product pricing sensitivities, reserve testing and financial reporting.

Insurance premiums credited to unit-linked funds are converted into units at the offer price, but the policyholder's fund is valued using the bid price. A positive spread therefore creates an immediate difference even when financial markets have not moved. Management fees and policy administration charges reduce the unit fund, whereas amounts charged to policyholders generate insurer non-unit income and are not synonymous with the actual expenses incurred. A guaranteed death benefit creates mortality cost only on the positive excess above the linked fund value; it would double-count fund assets to charge the full guaranteed amount as non-unit insurer cost. The non-unit profit signature then recognises unallocated premiums, spreads and management and administration charges less commission, expenses, additional death cover and any guarantee cost. Future cashflows are discounted year by year. These identities form a precise accounting model, not a regulatory determination of fair consumer value.

The mission develops one-period unit accounting and finite annual expected profit signatures. It is not a market conduct or compliance assessment of a particular insurer. Fund return and projected mortality are explicit model inputs and do not assert a complete stochastic-policy profit distribution. Complex paid-up terms, partial surrender and non-unit reserve zeroisation have related earlier mission infrastructure and require further integration. Every Lean theorem remains open.

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.

Selected references

• Financial Conduct Authority (2026), Unit-linked pensions and savings: price and value practices. https://www.fca.org.uk/publications/multi-firm-reviews/unit-linked-pensions-and-savings-multi-firm-review-consumer-duty-price-and-value-practices
• Financial Conduct Authority (2016), Fair treatment of long-standing customers in the life insurance sector, TR16/2. https://www.fca.org.uk/your-fca/documents/thematic-reviews/tr16-02

Motivation

General-insurance reserving methods must distinguish development of claim payments from changes in their price level. The IFoA inflation reserving guidance distinguishes implicit and explicit inflation adjustments. Its earlier claims reserving report identifies inflation and average cost per claim methods alongside standard chain ladder. Earlier actuarial missions LIII and LIX cover volume chain ladder and reserve variances but not these two methods.

Setting

Incremental claims are paid in calendar years determined by accident year plus development year. A strictly positive index converts nominal claims into a constant valuation-year price level before applying development factors. The projected real future claim payment is then reinflated to its expected future calendar-year cost. Separately, an average cost per claim development triangle and a count triangle project ultimate claim frequency and mean severity.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Inflation indices and real-claims transformations

A price index remains positive for growth greater than minus one.

$$C^{\text{real}}_{i,j}=C_{i,j}\frac{I_{\text{base}}}{I_{i+j}}$$

Incremental triangles and cumulative development

Sufficient projected ultimate value gives nonnegative outstanding reserve.

$$C_{i,j}=\sum_{k=0}^{j}X_{i,k},\quad U_i=C_{i,j}f_j$$

Average-cost-per-claim projection and reserve reconciliation

The inflation-adjusted chain-ladder projection and the independently developed average-cost claim reserve both reconcile nominal cashflows, real development and ultimate claims without treating the projection as an observed fact.

$$U_i=N_i^{\text{ult}}A_i^{\text{ult}},\quad R_i=U_i-P_i$$

Capstone theorem

The inflation-adjusted chain-ladder projection and the independently developed average-cost claim reserve both reconcile nominal cashflows, real development and ultimate claims without treating the projection as an observed fact.

$$U_i=N_i^{\text{ult}}A_i^{\text{ult}},\quad R_i=U_i-P_i$$

Significance

As discussed in the IFoA claims-reserving literature, The target establishes exact no-loss conversion between nominal and real claims, proper telescoping between incremental and cumulative triangles, the composition of real development factors, and the multiplication of projected ultimate claim numbers by projected average severity. It then reconciles both ultimate and outstanding amounts in an independent combined capstone. A payment-year inflation assumption is distinguishable from a development-year link factor, which guards against projecting historical calendar-year inflation twice.

Difficulty

The proof must preserve accident-year, development-year and calendar-year indexing and impose positivity on every ratio's index, claim count and growth denominator before invoking any reconstruction identity. The dollar value of a claim that has already been paid must never be reinflated as if it were a future payment. Volume development and average-cost development use different denominators and cannot be conflated in a single grossing-up factor without an additional model assumption. The capstone reconciles separately constructed projections rather than defining reserves by the desired equality.

Formalization scope

Historical inflation adjustment and claim-development factors are distinct mathematical constructs in this model. A future extension could integrate stochastic calendar-year inflation factors, accident-year trends, and parameter-estimation uncertainty into a single insurer liability distribution. The current exact algebraic target is nontrivial because it reconstructs nominal cashflows after applying conversion and development operations to independently constructed real and count-based projections. Known chain-ladder methods do not eliminate the need to prove that the resulting factors and projected reserve components reconcile. The finite triangle definitions and their transformations are reusable for other claims reserving methods, including tail development and multiple accident years.

A loss development triangle involves three separate notions of time: accident-year origin, settlement development lag and payment calendar year. Past inflation must be removed according to the actual payment year before development is extrapolated. Only after the real-valued development has been projected should future expected payment-year inflation be reinstated, and only once. A claim volume development factor does not represent a price inflation rate. The average-cost-per-claim method separately projects ultimate claim numbers and average claim sizes, then multiplies them. This decomposition distinguishes frequency development from claim inflation and severity development. The actuarial motivation is substantial, as long-tailed insured losses can have irregular calendar-year price patterns. The mathematical statements in this source are exact projection identities, not claims that past development patterns predict future claim payments without residual risk.

This is a mathematically exact deterministic claims triangle and projected cashflow formalisation, not a claim that chain-ladder assumptions hold for a particular line of business or that the selected inflation index is statistically correct. The index rate and link factors are model inputs, and the full stochastic process/reserve estimation error remains covered only in related Mack mission LIX. Interactions of separate inflation by payment type and stochastic calendar effects are future research problems. All Lean theorem bodies are open.

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.

Selected references

• Institute and Faculty of Actuaries (2025), High-level Methods for Incorporating Changing Inflation into Claims Reserve Estimates. https://vle.actuaries.org.uk/pluginfile.php/168696/mod_resource/content/1/Reserving%20During%20Volatile%20Inflation%20v1.9.pdf
• Institute and Faculty of Actuaries (2004), Claims reserving, §5. https://www.actuaries.org.uk/system/files/documents/pdf/0353-0413.pdf

Motivation

The Cramér–Lundberg model describes insurer capital invested in premium revenue while discrete random claims are paid at unpredictable arrival times. The model's classical adjustment coefficient and ruin probability are treated in risk theory and in modern ruin-probability bounds. Earlier mission LXXVIII derives a candidate ruin formula satisfying a renewal equation, but does not model the actual first-passage event. This mission supplies genuine stochastic first passage and measurable ruin events with an explicit stopped exponential-moment route to a rigorous bound.

Setting

Let W_j and Y_j be random waiting times and severities on a measurable probability space. At n-th claim arrival, cumulative elapsed time is the sum of W_0 through W_{n−1}, aggregate paid claims are the corresponding sum of Y_j, and the surplus is initial capital plus premium rate c times elapsed time minus claims. Ruin means surplus strictly less than zero and is only tested at claim boundaries, where a positive continuous premium slope allows a crossing to occur. The first-hit event excludes every earlier ruin, and its union over n is ultimate ruin.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Embedded Poisson-arrival capital paths and first-passage partition

Larger capital cannot create pathwise ruin.

$$U_n=u+c\sum_{j<n}W_j-\sum_{j<n}Y_j$$

Probability of ruin, monotonicity and severity overshoot

Observation of more arrivals can only increase probability of ruin.

$$\psi_N(u)=\mathbb{P}(\min_{n\le N}U_n<0)$$

Stopped exponential-loss process and conditional Lundberg capital bound

The actual stochastic first-passage event and stopped exponential moment condition derive a nonvacuous ultimate Lundberg capital bound.

$$\mathbb{E}[M_{\tau\wedge N}]\le1\ \Longrightarrow\ \psi_N(u)\le e^{-Ru}$$

Capstone theorem

The actual stochastic first-passage event and stopped exponential moment condition derive a nonvacuous ultimate Lundberg capital bound.

$$\mathbb{E}[M_{\tau\wedge N}]\le1\ \Longrightarrow\ \psi_N(u)\le e^{-Ru}$$

Significance

The mission establishes a real measured probability of ultimate ruin, monotonicity under capital and arrival horizon, and a disjoint partition by the first claim causing ruin. It then uses a stopped exponential loss process and an explicit moment upper bound to derive a Lundberg inequality for finite and ultimate ruin probabilities. The auxiliary stopped expectation condition is an independent martingale-style hypothesis, not an assumption of the desired probability bound. This helps distinguish authentic probability claims from an explicit exponential candidate whose equation has been verified. The risk-theory literature motivates the exponential-capital tail.

Difficulty

Nontrivial probability analysis is required to link a finite first-passage indicator to a stopped exponential transform. The first-hit sum cannot count multiple ruin dates on the same path, and the no-ruin terminal term must appear exactly once. Strict ruin, equality at zero and an observed negative surplus require distinct treatment. The finite-horizon inequality then uses measurability, positivity of exponential loss and a moment expectation hypothesis. Passing to ultimate ruin requires the countable union of nested ruin events and probability measure continuity, without assuming the theorem's conclusion.

Formalization scope

Existing actuarial theory establishes the analytical principle, whereas the formal work here must prove the stated identities in Lean using the true distribution and event definitions. Some prior mission targets describe finite distributions or a candidate valuation, but they do not establish these stronger infinite-support or measured first-passage results. The boundary assumptions are part of each mathematical statement and cannot be replaced by a tautological definition. A complete proof requires independent source lemmas, explicit handling of the limiting case and verification of every transformation before concluding the capstone.

The pathwise event uses a strict negative surplus, not failure on equality at zero. The first-passage index is a disjoint union of finite-arrival failure events, and the increasing union gives ultimate ruin. A conditional moment hypothesis provides a nontrivial route to an exponential capital inequality. It is not the same assertion as the inequality on the ultimate ruin probability. The model does not claim to establish the Poisson arrival distribution or full independence of exponential severities from this conditional input. Those must be proved in a later, more elaborate stochastic source model.

The capstone proves the conditional stopped-moment Lundberg inequality for an actual measurable first-passage event, not yet the complete exponential-claims distributional identification. Independent exponential waiting times and independent claim severities supply the classical route to the stopped moment hypothesis but are not themselves constructed or verified in this graph. A future mission should derive that moment condition from fully specified iid waiting and severity distributions and prove uniqueness of the exact ruin probability. The pathwise framework is reusable for continuous-time embedding, overshoot losses, first-passage service tables and capital assessment. All Lean proof obligations remain open.

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.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 23. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml
• Hanspeter Schmidli (2017), Risk Theory, first edition, Springer. https://link.springer.com/book/10.1007/978-3-319-72005-0
• Bounds for the Ruin Probability in the Sparre–Andersen Model (2024), Risks 12(2), 28. https://www.mdpi.com/2227-9091/12/2/28

Motivation

Continuous-time multi-state life insurance uses a generator of competing decrement intensities and prospective reserves for status-dependent benefits. The time-dependent state equations appear in multi-state insurance research; Promislow (2015), Chapter 19, provides actuarial fundamentals. The existing LXXVI mission constructs general conservative generator rows but only solves the stationary alive/dead reserve. This mission adds time-varying competing risks and derives a genuine contingent-payment reserve from its cashflows.

Setting

Three mutually exclusive states consist of active insurance, termination by cause one and termination by cause two. The latter are absorbing. The common exit intensity is a nonstationary force λ(t)=a+bt with cumulative hazard H(t)=at+bt²/2. A fixed proportion p of the exit force belongs to the first cause; 1−p belongs to the second. Nonnegative a, b and future dates and p in the unit interval make the transition probabilities stochastic. The model admits two distinct termination payments, one for each cause, and a separately specified maturity endowment.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Nonstationary intensity, exact absorption and generator conservation

Generator no-exit diagonal is minus total force.

$$\lambda(t)=a+bt,\quad H(t)=at+\frac{bt^2}{2}$$

Three-state transition probabilities and Chapman–Kolmogorov

Forward cause-two flow equals complementary hazard share times active membership.

$$P_{00}(s,t)=e^{-(H(t)-H(s))},\quad P_{01}(s,t)=p(1-P_{00}(s,t))$$

Cause-contingent insurance and integral Thiele reserves

A genuinely nonstationary three-state absorbing model conserves probability and its independently integral-defined prospective liability obeys the cause-contingent Thiele equation.

$$V'(t)=(\delta+\lambda(t))V(t)-\lambda(t)\bigl(pB_1+(1-p)B_2\bigr)$$

Capstone theorem

A genuinely nonstationary three-state absorbing model conserves probability and its independently integral-defined prospective liability obeys the cause-contingent Thiele equation.

$$V'(t)=(\delta+\lambda(t))V(t)-\lambda(t)\bigl(pB_1+(1-p)B_2\bigr)$$

Significance

The prospective reserve is an independently defined sum of a terminal-survival present value and a bona fide interval integral of the time-discounted, competing-exit claim intensity. The capstone proves its terminal boundary and differentiates it to obtain a nonstationary, three-status Thiele ODE, with an explicit cause-mix death strain. The result includes complete Chapman–Kolmogorov composition and transition normalisation for two absorbing exits. Research on multi-state actuarial equations explains how these equations fit into the broader general reserve framework.

Difficulty

The proof must establish a nontrivial inhomogeneous probability structure, not simply define reserve cashflows by the desired ODE. The cumulative-force derivative must be combined with the exponential survival chain rule, and the transition matrix must be composed across different calendar intervals. The integral of discounted cause-specific benefits must then be differentiated with a moving lower endpoint and a valuation-date-dependent exponential factor. Several steps rely on genuine interval integral differentiation and the finite-timestamp boundary conventions; no closed-form fixed-intensity substitution is assumed.

Formalization scope

The model imposes fixed cause allocation while the total force changes with time. It therefore admits a genuine conditional transition matrix with two absorbing states. This provides a nonstationary counterexample to treating all transition intensities as constant; forcing an arbitrary time-dependent kernel to satisfy the desired generator equation by assumption would be vacuous. The interval-integral benefit value is independently defined before differentiating it. Its terminal boundary depends on the maturity payment, and no death benefit is payable at maturity beyond the contractual endpoint. The formalisation does not assume a general matrix-exponential formula for time-dependent noncommuting generators.

The mission establishes a nonstationary three-state absorbing competing-decrement model, not an arbitrary intercommunicating time-dependent finite-state generator or a semi-Markov duration-reset model. This restriction is important because its exact transition matrix and reserve integrals can be constructed without assuming the answer. Later actuarial missions can reuse the resulting conditional survivor functions and Thiele equation as a basis for disability recovery and wider inter-state transfers. Lean statements are open research targets, not accepted formal proofs, and the mathematical identity must be obtained from the originally defined valuation.

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.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 19. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml
• Multi-state modeling in the mathematics of life insurance: meditations and applications (2020), research thesis, pp. 17–35. https://www.math.ku.dk/bibliotek/arkivet/phd-theses/phd20cf.pdf
• Kristian Buchardt, Thomas Møller and Kristian Bjerre Schmidt (2015), Cash flows and policyholder behaviour in the semi-Markov life insurance setup. https://doi.org/10.1080/03461238.2013.879919

Motivation

Actual insurer mortality and withdrawal observations are censored and may differ systematically with explanatory covariates. Cox's original 1972 proportional-hazards paper treats an arbitrary baseline hazard combined with covariate-relative-risk multipliers and constructs a conditional partial likelihood. Existing actuarial missions cover lifetimes, Kaplan–Meier/Greenwood and mortality graduation, but not regression risk-set estimation.

Setting

A life with scalar covariate z and regression parameter beta has hazard λ0(t) exp(beta z). The cumulative baseline hazard determines the survival function. At each distinct observed failure time there is a finite nonempty at-risk set, including the life that died, and censoring removes deaths that are not observed without treating them as failures. This mission assumes no tied failures in its conditional likelihood graph; more general Efron and Breslow ties require a separate coherent treatment.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Positive proportional hazards and cumulative survival

A zero covariate reduces to baseline survival.

$$\lambda(t\mid z)=\lambda_0(t)e^{\beta z},\quad S(t\mid z)=e^{-\Lambda_0(t)e^{\beta z}}$$

Censored risk sets and event conditional likelihood

A censored observation must not simultaneously be a failure contribution.

$$L(\beta)=\prod_{i\in D}\frac{e^{\beta z_i}}{\sum_{j\in R(t_i)}e^{\beta z_j}}$$

Log-partial likelihood, weighted risk scores and inference

Cox covariates alter baseline hazard multiplicatively, survival stays within probability bounds, and the nontrivial risk-set score is derived as the derivative of the conditional partial likelihood.

$$U(\beta)=\sum_{i\in D}\left(z_i-\frac{\sum_{j\in R_i}z_je^{\beta z_j}}{\sum_{j\in R_i}e^{\beta z_j}}\right)$$

Capstone theorem

Cox covariates alter baseline hazard multiplicatively, survival stays within probability bounds, and the nontrivial risk-set score is derived as the derivative of the conditional partial likelihood.

$$U(\beta)=\sum_{i\in D}\left(z_i-\frac{\sum_{j\in R_i}z_je^{\beta z_j}}{\sum_{j\in R_i}e^{\beta z_j}}\right)$$

Significance

The mission formally separates a common arbitrary baseline hazard from the relative hazard of each observed insured life. The partial likelihood uses event-specific risk sets, not a single fixed cohort denominator, and the model derives the true conditional event probabilities and analytic score from the independently defined likelihood. As in the original Cox model, the mathematical outcome provides essential foundations for credible, covariate-sensitive life contingent predictions and statistical mortality investigations.

Difficulty

The risk sets must remain nonempty and include observed failures when interpreting their shares as probabilities. Finite products with changing risk sets combine with a log-likelihood that is differentiated using an exponential weighted denominator. The central theorem must obtain the score from a derivative and must not define score equality as a model axiom. Positive covariate multipliers and boundary survival values are derived separately. The model does not assert a numerical maximum likelihood estimator exists without concavity or identifiability conditions.

Formalization scope

The conditional partial likelihood is based on one observed failure at a time. Each event has its own finite risk set. A life censored before the event time is excluded from that later set, but an individual censored after the time remains exposed at that instant. Censoring patterns therefore change the risk sets, even though the baseline force drops out of the conditional event ratio. With a scalar coefficient, this model is an actuarially meaningful specialisation of the Cox regression formulation. The score derivative is substantive because its risk-weighted average contains the current coefficient in both the numerator and denominator. The numerator and denominator must each be differentiated, the denominator must remain strictly positive and the log derivative must not assume the target identity. Only after these facts have been proved can the formula for the score be justified. Extending the analysis to a score vector and information matrix would involve covariance matrices weighted by dynamic risk sets, and the nonnegativity of observed information is not a pointwise algebraic identity without proper hypotheses. Reusable consequences of this foundation include estimation with life-assurance underwriting covariates, statistical investigation of pensioner mortality, cause-specific decrements and a later treatment of time-dependent covariates. This graph deliberately treats distinct failure times rather than asserting a tied-events formula that has not yet been formally justified; Efron and Breslow corrections motivate future work, not assumptions of the current model.

The model treats a single scalar covariate and untied observed failures. It neither assumes a parametric distribution for the baseline mortality force nor confuses censored lives with observed deaths. It does not prove martingale asymptotics, proportional-hazard diagnostics, time-varying regression coefficients or Efron tied-event corrections. These are legitimate larger follow-on missions. Its theorem statements and source are unproved formal targets.

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.

Selected references

• D. R. Cox (1972), Regression Models and Life-Tables, JRSS Series B 34, 187–202. https://doi.org/10.1111/j.2517-6161.1972.tb00899.x
• D. R. Cox (1975), Partial Likelihood, Biometrika 62, 269–276. https://doi.org/10.1093/biomet/62.2.269

Motivation

Panjer recursions allow compound claim distributions to be computed without enumerating many severity convolutions. The original Panjer paper and the Sundt–Jewell family extension establish the actuarial context. The previous LXXVII mission covers finite-support frequency distributions with zero claim amounts. Here the claim count ranges over all nonnegative integers, so correct series convergence and coefficient interchange become new formal obligations.

Setting

Let N be Poisson with claim count intensity λ≥0 or geometric with parameter q in [0,1). Independently distributed claim severities are nonnegative integer valued, with pmf f_j and possibly f_0>0. For each claim count n, the distribution f^{*n} is formed using genuine convolution; the empty portfolio assigns mass one to zero. The compound mass g_k is defined as the infinite sum of p_n times the n-fold convolution coefficient, independently of any Panjer formula.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Countably infinite count laws and convolution powers

True infinite aggregate mass is nonnegative.

$$p_n^{\mathrm{Poi}}=e^{-\lambda}\frac{\lambda^n}{n!}$$

Probability generating functions, mass normalisation and zero atoms

Compound Poisson zero mass comes from thinning.

$$g_k=\sum_{n=0}^{\infty}p_n(f^{*n})_k,\quad g_0=G_N(f_0)$$

Full Poisson and geometric infinite Panjer recurrence

The genuinely infinite Poisson and geometric aggregates obey their independently derived corrected Panjer laws.

$$(1-qf_0)g_k=q\sum_{j=1}^kf_jg_{k-j}$$

Capstone theorem

The genuinely infinite Poisson and geometric aggregates obey their independently derived corrected Panjer laws.

$$(1-qf_0)g_k=q\sum_{j=1}^kf_jg_{k-j}$$

Significance

The capstone derives both infinite frequency families' entire positive-aggregate recurrence. For Poisson frequency the kernel includes a severity-size factor λj/k; for geometric frequency it contains an essential zero-claim correction 1−qf_0. The zero aggregate mass itself is the count PGF evaluated at severity f_0, not merely the probability of having no claims. The 1981 ASTIN literature underpins these equations, while a countably supported Lean formalisation makes their analytic conditions explicit.

Difficulty

Unlike the finite claim count in LXXVII, an infinite frequency model requires genuine convergence before double series may be rearranged. Proving the Poisson and geometric frequency normalisations is distinct from proving convergence of the actual aggregate pmf. At a fixed amount k a finite inner convolution remains, but summation over the count n is infinite. The nontrivial step is justifying probability-generating function composition and extracting the correct severity coefficients without assuming the desired recurrence or silently truncating Poisson claims. Special cases with all claim sizes zero are included.

Formalization scope

Existing actuarial theory establishes the analytical principle, whereas the formal work here must prove the stated identities in Lean using the true distribution and event definitions. Some prior mission targets describe finite distributions or a candidate valuation, but they do not establish these stronger infinite-support or measured first-passage results. The boundary assumptions are part of each mathematical statement and cannot be replaced by a tautological definition. A complete proof requires independent source lemmas, explicit handling of the limiting case and verification of every transformation before concluding the capstone.

The generating-function series is defined from the probability mass of each count; the count law is genuinely infinite, not a finite upper cutoff with a hidden tail. In particular, the positive Panjer recursion cannot be used to define its own aggregate coefficients: the aggregate mass must first be constructed from convolution powers and the count weights. At claim size zero, the event of positive frequency with all zero-valued claims contributes to the true aggregate zero probability. Geometric count and Poisson count require distinct coefficient functions, even though they share the same actuarial notation for the severity distribution.

This mission addresses actual infinite Poisson and geometric count laws, with arbitrary properly normalised discrete severities. It does not cover noninteger-shape negative-binomial frequency, complex-domain analytic continuation or continuous claim sizes. The formal target makes probability nonnegativity and summed severity mass explicit, and all Lean proofs remain open. The resulting count/compound transforms can be reused in later collective-risk, stop-loss and capital modelling applications. It deliberately excludes vacuous proof strategies that define the aggregate distribution as the recurrence answer.

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.

Selected references

• Harry H. Panjer (1981), Recursive Evaluation of a Family of Compound Distributions, ASTIN Bulletin 12(1), pp. 22–26. https://doi.org/10.1017/S0515036100006796
• Bjørn Sundt and William S. Jewell (1981), Further Results on Recursive Evaluation of Compound Distributions, ASTIN Bulletin 12(1), pp. 27–39. https://doi.org/10.1017/S0515036100006802
• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 21. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml

Motivation

Actuarial claim counts and average costs depend on policy exposure, customer characteristics and risk-factor selection. The foundational Nelder–Wedderburn GLM formulation derives exponential-family maximum likelihood through a predictor and link, including Poisson count and Gamma response examples. Existing actuarial missions cover finite exposures and rating relativities, but not a unified log-likelihood score, information and deviance calculation.

Setting

An exposed group contributes E positive insured person-years. The count predictor η produces expected claims μ=E exp η, so log exposure is a compulsory offset rather than a fitted regression coefficient. The model defines observed claims per exposure, the Poisson log-likelihood up to a response-only factorial constant, its scalar score, expected information and saturated deviance. A separate Gamma mean and variance model describes positive insurance severity.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Positive claim rates, log links and exposure offsets

Nonnegative frequency and severity produce nonnegative pure premium.

$$\mu=E e^\eta,\quad \log \mu=\log E+\eta$$

Poisson log-likelihood, score and information

Poisson log-likelihood attains a global maximum at the fitted canonical count for strictly positive observations.

$$\ell(\eta)=y\log(Ee^\eta)-Ee^\eta,\quad U(\eta)=y-Ee^\eta$$

Claims deviance, premium relativity and model comparison

A genuine positive-exposure Poisson GLM has the correct canonical offset, score and Fisher derivative, nonnegative saturated deviance and consistent severity-loaded insurance premium.

$$D_{\text{Poi}}=2\left[y\log\left(\frac{y}{\mu}\right)-(y-\mu)\right]$$

Capstone theorem

A genuine positive-exposure Poisson GLM has the correct canonical offset, score and Fisher derivative, nonnegative saturated deviance and consistent severity-loaded insurance premium.

$$D_{\text{Poi}}=2\left[y\log\left(\frac{y}{\mu}\right)-(y-\mu)\right]$$

Significance

Following Nelder–Wedderburn, the capstone derives the Poisson model's canonical offset, identifies the score as a genuine derivative of the log-likelihood, and proves that its derivative is negative Fisher information. A nonnegative deviance measures disagreement with saturated data and integrates with multiplication of expected frequency and severity to obtain the insurer's pure premium. This is the mathematical basis for estimating tariff frequency relativities and verifying model fit.

Difficulty

A real-valued logarithm is not automatically the log of a positive expected count: exposure positivity must be explicit. Count zero is handled with a separate non-log-deviance expression, avoiding undefined logarithmic ratios. The score and information identities must follow by differentiation rather than by an assumed GLM normal equation. It is a nontrivial analytic task: a vacuous definition of a zero score would not establish any likelihood derivative. The deviance inequality uses the logarithmic convexity inequality and requires positive expected and observed claims, while the finite exposure boundary avoids any mistaken claim of an informative zero-exposure observation.

Formalization scope

The Poisson GLM score is the derivative of a log-likelihood rather than an arbitrary residual statistic. The exposure offset shifts the logarithm of expected claim counts, so changing exposed policy-years modifies the fitted expected count without changing the per-exposure class rate. This is a defining issue in insurance rating where two policyholders with the same expected annual frequency can have different months insured. The score derivative gives the negative Fisher information, leading to the familiar concavity of the scalar canonical log-likelihood under positive exposures. Identifying a maximum-likelihood estimate, however, also requires adequate observed data and a nondegenerate model: at zero observed claims, the MLE can be approached only as the predicted rate tends to zero, not necessarily at a finite linear predictor. The scaled deviance measures disagreement with saturated data; it is nonnegative by the logarithmic inequality when observed and fitted counts are strictly positive. The zero-count case has to be handled by a limiting convention outside the positive-count formula. This is actuarially material in sparse claim classes and high-frequency policy segments. Gamma severity uses a different conditional variance function, so its dispersion and positivity conditions are not inherited directly from the Poisson count model. This graph is a reusable foundation for multivariate tariff construction, fitted pure premiums, exposure offsets and later iterative weighted regression algorithms. Its source model follows Nelder and Wedderburn while making every claim-count positivity hypothesis explicit.

This is the scalar Poisson frequency and Gamma severity foundation, not a full numerical fitting algorithm or a general matrix-valued IRLS solver. The categorical design matrix, multivariate coefficient normal equations, dispersion estimation, residual-based diagnostics and parameter-inference asymptotics are reserved for follow-on missions. There is no assertion that positive claims always exist or that every rate model is identifiable. All Lean proof statements remain open.

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.

Selected references

• J. A. Nelder and R. W. M. Wedderburn (1972), Generalized Linear Models, JRSS A 135(3), 370–384. https://doi.org/10.2307/2344614
• Casualty Actuarial Society, Generalized Linear Models for Insurance Rating, https://www.casact.org/sites/default/files/2021-03/05-Goldburd-Khare-Tevet.pdf

Motivation

Extreme insurance severity and catastrophe accumulation require models whose tails are not dictated by a Gaussian or ordinary exponential claim law. The NIST generalized Pareto reference provides a tail model for excess claim payments over a high threshold, while NIST maximum-type Gumbel models describe maxima of repeated extreme events. Existing actuarial risk missions cover limited stop-loss expectations and tail risk measures, but not the extreme-value distribution families themselves.

Setting

For positive shape ξ and scale σ, an exceedance amount x≥0 has GPD survival (1+ξx/σ) to the power minus one over shape. The distribution has an explicit actuarial claim density, hazard and percentile quantile. Its upper excess distribution retains the same shape while the scale increases linearly with the threshold. For ξ below one the conditional tail expectation is finite and can be expressed in terms of its loss quantile. A separate positive-shape GEV and maximum-type Gumbel distribution model extreme maxima.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Positive-shape generalized Pareto survival and severity density

The GPD density is minus the actual survival derivative.

$$S(x)=\left(1+\frac{\xi x}{\sigma}\right)^{-1/\xi}$$

Extreme claim quantiles, threshold stability and expected shortfall

GPD tail expectation follows the actuarial excess-loss identity.

$$q_p=\frac{\sigma}{\xi}\left((1-p)^{-\xi}-1\right),\quad \text{ES}_p=\frac{q_p+\sigma}{1-\xi}$$

Gumbel and generalized extreme-value maxima

An actual positive-shape GPD combines a valid percentile inverse, threshold-stable excess distribution and coherent expected shortfall, alongside a genuine extreme-maximum CDF.

$$G_{\xi}(x)=\exp\left[-\left(1+\xi\frac{x-\mu}{\sigma}\right)^{-1/\xi}\right]$$

Capstone theorem

An actual positive-shape GPD combines a valid percentile inverse, threshold-stable excess distribution and coherent expected shortfall, alongside a genuine extreme-maximum CDF.

$$G_{\xi}(x)=\exp\left[-\left(1+\xi\frac{x-\mu}{\sigma}\right)^{-1/\xi}\right]$$

Significance

The capstone connects the actual GPD distribution function, quantile inversion, excess-threshold stability and analytical expected shortfall. These are independent mathematical constructions, not labels attached to the target identities. This is a foundation for setting catastrophe attachment points, deriving economic capital quantiles and analysing sensitivity of retained high losses as severity tail shape changes. The extreme-value literature also explains why the GP exceedance approximation complements the family of limiting extreme maxima.

Difficulty

Power-law transformations are valid only where the base and denominators are strictly positive. Shape ξ=0 is a separate exponential limit and must not be quietly substituted into a nonzero-shape power expression. Valid quantile inversion needs a probability below one, a positive scale and a positive shape. The conditional excess calculation requires exact cancellation of two power-law tails with different scales. The expected-shortfall identity needs the finite-mean restriction ξ<1, while finite variance needs ξ<1/2. The maximum CDF uses nonnegative integer powers and genuine probability bounds.

Formalization scope

The generalised Pareto excess distribution is most naturally expressed as an actual conditional survival function above a high loss threshold. Its threshold stability property says that when the threshold rises, the shape remains fixed and the excess scale changes linearly. The proof must use the quotient of two survival probabilities and factor the two scale-dependent power-law terms. A mere definition of the updated scale would not establish the identity. This gives an analytic foundation for excess-of-loss reinsurance attachment and severity tail risk. The capital quantile inverts the GPD CDF using a real power; the definition is meaningful only with the probability strictly below one and a positive scale and shape. Expected shortfall requires stronger tail integrability than a simple high quantile. A positive shape at or above one produces a distribution with infinite mean, so a finite closed-form conditional tail expectation must be restricted to shape below one. A finite second moment requires shape below one half. These parameter boundaries are central to actuarial capital stress testing. Maximum-type Gumbel and GEV distributions arise from the theory of sample extremes and use distinct parameterisations from the excess-loss distribution. The GEV expression implemented here is intentionally limited to the valid positive-shape support and does not assert the universal asymptotic convergence theorem. The NIST severity model supplies the distributional formula, and the NIST Gumbel model supplies the maximum-type reference. The resulting identities can be reused in future high-quantile capital and retention-optimisation missions without assuming that all insurance losses follow the Pareto family.

The mission formalises positive-shape heavy-tailed GPD and GEV and ordinary maximum-type Gumbel models. It does not claim the full three-regime extreme-value convergence theorem or derive the Pickands–Balkema–de Haan asymptotic result from arbitrary parent claims. The zero-shape GPD limit and bounded negative-shape Weibull branch are future extensions. The tail expected value is a defined closed-form functional; a further probability-integration theorem would be needed to prove equality with a conditional expectation integral. Lean theorem statements remain open.

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.

Selected references

• NIST (accessed 2026), Conditional Mean Exceedance, including the GPD CDF. https://itl.nist.gov/div898/software/dataplot/refman1/auxillar/cme.htm
• NIST (accessed 2026), Extreme Value Type I Distribution, maximum Gumbel. https://www.itl.nist.gov/div898/handbook/eda/section3/eda366g.htm
• Natalia Nolde and Chen Zhou (2021), Extreme Value Analysis for Financial Risk Management, Annual Review of Statistics and Its Application. https://doi.org/10.1146/annurev-statistics-042720-015705

Motivation

As shown in crop insurance dependence studies, insurance risks share systemic mortality, climate, market and catastrophe drivers, so their aggregate extremes cannot always be modelled as independent. Copulas combine marginal loss distributions with their dependence structure. Actuarial empirical studies demonstrate that lower and upper joint-tail dependence can materially change high-quantile capital estimates. Existing Prove2Me missions cover risk measures and finite dependent lifetimes, but not copula margins, rectangle probability conditions or insurance co-exceedance.

Setting

A bivariate copula is a two-dimensional distribution function with uniform margins. Its cumulative joint probability on any rectangle must be nonnegative, so mere pointwise bounds are not sufficient to define a valid copula. The model independently defines product independence, comonotonic and countermonotonic Fréchet couplings, an FGM dependent family, and convex mixtures of copulas, with explicit parameter restrictions.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Bivariate joint distribution and boundary constraints

Two exchangeable uniform loss lines have symmetric FGM dependence.

$$C(u,0)=0,\quad C(1,v)=v,\quad C(u,1)=u$$

Rectangle probability, Fréchet bounds and copula construction

All valid bivariate uniform joint risks satisfy the upper Fréchet bound.

$$\max(0,u+v-1)\le C(u,v)\le\min(u,v)$$

Independent and dependent upper-tail co-exceedance

FGM joint insurance dependence obeys genuine copula axioms, universally valid Fréchet limits and an exact analytic capital tail correction.

$$\Pr(U>u,V>v)=1-u-v+C(u,v)$$

Capstone theorem

FGM joint insurance dependence obeys genuine copula axioms, universally valid Fréchet limits and an exact analytic capital tail correction.

$$\Pr(U>u,V>v)=1-u-v+C(u,v)$$

Significance

As the crop insurance dependence study demonstrates, the capstone proves a genuinely bivariate dependence family has uniform margins and nonnegative rectangle masses, satisfies universal Fréchet bounds, and produces the exact difference between two-line capital exceedance probability and the independent baseline. The function used in the tail calculation is constructed independently of the conclusion and must meet the full two-increasing criterion. The mathematics isolates dependence risk from marginal expected losses and supports subsequent high-quantile capital analysis.

Difficulty

The two-increasing property is a nontrivial rectangular inequality, not a claim that a function happens to take values in the unit interval. The FGM copula must satisfy this criterion for its full allowed parameter range, and the Fréchet bounds must be proved for any separately certified copula. Tail co-exceedance combines survival complements and the joint cumulative distribution without assuming independence. Correct parameter and threshold restrictions are crucial.

Formalization scope

The Fréchet–Hoeffding bounds arise from nonnegative masses of carefully chosen rectangles within the unit square and the uniform marginal constraints. Their proof uses the full two-increasing property, not merely pointwise nonnegativity of the joint CDF. It is possible to construct a function that has plausible one-dimensional boundaries but produces a negative rectangle mass, so boundary checks alone do not establish a copula. Convex mixtures preserve the genuine constraints because rectangle probability is linear in the dependence function and mixture weights are nonnegative. The FGM dependence family supplies a parameterised example where the entire copula proof is nontrivial yet algebraically accessible. Its parameter range must be restricted to preserve all rectangle masses. The joint exceedance probability then follows from inclusion-exclusion: capital thresholds correspond to upper tails of the marginal uniform transforms. This is an important distinction from simply computing the probability that at least one line exceeds its threshold. The same margins can coexist with different joint capital requirements, so portfolio dependence cannot generally be recovered from marginal loss expectations. This development is reusable when analysing risk aggregation and diversification under copula uncertainty. The crop-insurance dependence study illustrates the sensitivity of high-quantile risk to the dependence family. Gaussian, Clayton and Gumbel copulas require careful domain, monotonicity and tail-limit results and should be additional substantial targets rather than names appended to an unverified bivariate function.

This is the complete bivariate Fréchet/independence/FGM finite-copula foundation. The full Sklar representation theorem for arbitrary marginal distributions and Gaussian, Clayton and Gumbel parameter families require substantial measure-theoretic and analytic extensions and remain future work. The real-valued percentage thresholds must lie in the unit interval; conditional ratios are claimed only away from zero denominators. Theorem statements remain open.

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.

Selected references

• R. B. Nelsen, An Introduction to Copulas, 2nd ed., Springer, 2006. https://doi.org/10.1007/0-387-28678-0
• Value-at-Risk and Models of Dependence in the U.S. Federal Crop Insurance Program. https://www.mdpi.com/1911-8074/12/2/65
• R. L. Gudmundarson, M. Guerra and A. B. Moura (2022), On some effects of dependencies on an insurer’s risk exposure. https://doi.org/10.1007/s13385-022-00326-0

Motivation

Defined benefit funding involves a mathematical choice about when benefits are recognised and how contributions relate to prospective projected payroll. The IFoA's historical GN26 distinguishes entry-age, attained-age and aggregate methods. Existing actuarial missions cover projected/current unit credit and prospective reserve cashflows; they do not derive the wider standard contribution rate and exact actuarial surplus decomposition in the same theorem graph. This mission formalises the distinct valuation equations rather than repeating the projected unit method.

Setting

Write B for actuarial present value of total prospective benefits, P for the present value of projected future earnings, A for fund assets and L for accrued actuarial liability. An entry-age rate is calibrated when the member joins; an attained-age rate covers the total projected benefits net of the accrued projected-unit liability; the aggregate rate credits assets directly. Deficit payments are discounted over an explicit recovery annuity, and current assets and liabilities each evolve by actual monetary cashflows and assumption changes.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Entry age, attained age and liability allocation

Annual attained normal cost equals rate times current pensionable earnings.

$$r_{\text{entry}}=\frac{B_e}{P_e},\qquad L_x=B_x-r_{\text{entry}}P_x$$

Aggregate funding and deficit amortisation

Under the mathematical total-function convention, zero payroll cannot define a useful rate; the model therefore makes no recovery claim at that boundary.

$$r_{\text{agg}}=\frac{B_x-A_x}{P_x},\qquad r_{\text{modified}}=r_{\text{normal}}+\frac{L_x-A_x}{a}$$

Fund asset rollforward and exact surplus attribution

The three genuinely distinct DB funding methods reconcile projected liabilities while deficit contributions and complete one-year experience movements reconcile surplus.

$$S_{t+1}-S_t=(A_{t+1}-A_t)-(L_{t+1}-L_t)$$

Capstone theorem

The three genuinely distinct DB funding methods reconcile projected liabilities while deficit contributions and complete one-year experience movements reconcile surplus.

$$S_{t+1}-S_t=(A_{t+1}-A_t)-(L_{t+1}-L_t)$$

Significance

The capstone reconciles entry-age funding, attained-age future-service financing, aggregate funding and modified deficit contribution rates with an exact opening-to-closing surplus movement. In particular, the attained-age rate is derived from future-service value and the aggregate rate is derived from total prospective benefits less existing assets. The objective respects the OECD comparison of pension funding methods and does not conflate entry-age accrued liability with projected-unit accrued benefits.

Difficulty

The mathematical work must keep different cost allocations separate and exclude undefined zero-payroll or zero-amortisation denominators wherever contribution recovery is claimed. It must distinguish the actuarial liability from fund assets and preserve the signs of benefit outgo, administration expenses, interest unwind and changes in assumptions. The surplus capstone combines several independently defined rollforwards and excludes artificial circular definitions of a fully funded position.

Formalization scope

The normal cost and accrued liability need different interpretations across the three prospective methods. For the entry-age model, future contributions use a rate calibrated on original entrant benefits and entrant payroll, whereas the current accrued liability subtracts the value of future payments at that inherited rate. For attained age, a separate projected unit past-service valuation is the liability, so only future-service benefits enter the prospective contribution rate. These two normal rates cannot be asserted equal without assumptions on salary progression, cohort service and entrance dates. The aggregate method deliberately credits existing scheme assets against all projected benefits when calculating a single funding rate, rather than reporting the past-service liability and deficit as distinct parts. The difference has real consequences for an open or closed scheme in surplus. This distinction is discussed in the IFoA terminology. The experience surplus reconciliation treats actuarial assets, cash contributions, actual investment gain, pensions paid and expense outgo separately from unwinding accrued liabilities, service cost, liability benefit releases and assumption changes. An investment gain and an investment assumption revision are not the same cashflow and must not be silently combined. The capstone derives both sides from the separately defined asset and liability rolls, so it does not assume their equality through the definition of surplus. These equations provide reusable inputs for later pension funding projections, deficit-recovery schedules, capital adequacy and sensitivity analysis. The chosen real-valued model does not itself make an actuarial statement about prudence, solvency regulations or a chosen best-estimate basis.

This is a precise real-valued funding reconciliation, not an assertion that a particular funding method is appropriate for a specific pension scheme. Discounted future benefits and payroll are model inputs, not a new probabilistic pension cashflow engine, and no universal claim of a positive contribution rate is made when assets exceed liabilities. The model's zero-denominator branches are mathematical total-function conventions only; normal recovery assertions require nonzero annuity and payroll inputs. Existing projected unit, early/late factors and cohort service models are reused conceptually without duplicating their theorem graphs. The statements remain open proof obligations.

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.

Selected references

• Institute and Faculty of Actuaries (2000), GN26 Pension Fund Terminology, §§4.5–4.9. https://www.actuaries.org.uk/system/files/documents/pdf/gn26v2-0.pdf
• OECD, Funding Rules and Actuarial Methods, §§74–76. https://www.oecd.org/content/dam/oecd/en/publications/reports/2006/10/funding-rules-and-actuarial-methods_g17a1941/274307371724.pdf
• Actuarial Standards Board (2023), Measuring Pension Obligations and Determining Pension Plan Costs or Contributions. https://www.actuarialstandardsboard.org/asops/measuring-pension-obligations-determining-pension-plan-costs-contributions/

Motivation

Dependent competing risks arise when more than one cause can terminate a pension or insurance status, and when a single event can terminate several lives simultaneously. A traditional independent-life calculation can materially understate the probability of joint survival and misunderstand the probability of simultaneous failure. Promislow's account of minimum failure times, competing causes, common shock and multi-state modelling is the conceptual guide. The Marshall–Olkin model is an independently published stochastic model of linked exponential lifetimes. This mission formalises the actual underlying failure events and their resulting actuarial benefits; its proposed Lean theorem declarations are new mathematical targets, not claims of already accepted proofs. The book is S. David Promislow, Fundamentals of Actuarial Mathematics, Third Edition (2015), chapters 11, 17 and 19. The independently published supporting research reference is available here.

Setting

On a measurable outcome space Ω with probability measure μ, take three real-valued primitive failure times U, V and Z. U and V represent idiosyncratic risks for the two lives; Z is a common shock. The observed times are T₁=min(U,Z) and T₂=min(V,Z). An earliest Z causes both observed lives to fail together, even when U,V and Z have no primitive ties. Survival means strictly exceeding a stated duration. Failure by a horizon includes equality with that endpoint. For probabilistic interpretation, primitive times should be nonnegative and measurable. Pairwise independence is inadequate to justify multiplying three primitive survivor probabilities, so the joint product identity requires suitable mutual independence assumptions. Full parametric expressions require independent primitive exponential waiting times.

The central actuarial model can be written

$$S_{12}(s,t)=\Pr(T_1>s,T_2>t)=\exp[-as-bt-c\max(s,t)],\quad s,t\ge0.$$

Formalization targets

Actual joint-lifetime events and cause partition

The first block uses the actual probability measure of lifetime events. It distinguishes first idiosyncratic cause, second idiosyncratic cause, common-shock cause and primitive ties. The probabilities of the strict first-cause events add to one only if ties have zero probability. A positive common-shock event still produces a genuine observed joint-failure atom. Conditional survival and the monotonicity of joint survival at increasing deadlines are not inferred from deterministic symbols. The event partition provides a reusable bridge to multistate transition structures and group-life payment obligations.

Independent-shock Marshall–Olkin survivor law

The second block introduces the Marshall–Olkin parametric survivor law with nonnegative primitive exponential hazard rates a,b,c. Joint survivor at two different horizons depends on the maximum horizon because the shock affects both lives. Separate the independent-case boundary c=0 from the strictly dependent case c>0. Theorems on marginal survivors, diagonal joint survival, normalisation, positivity and the comparison with independently multiplied observed marginal survivors quantify exactly how the shared hazard creates dependence. This is a model-specific calculation, not an assertion that arbitrary observed lifetimes have independent components.

Cause-contingent actuarial benefits and dependence

The third block prices cause-contingent insurance benefits by multiplying actual measured first-cause probabilities by separately specified amounts and a common deterministic discount. Benefit amounts are in currency; discount factors are dimensionless; failure times are in years. A three-way benefit schedule must specify an explicit common-shock payment amount because simultaneous failure cannot be assigned to only one idiosyncratic cause without a contractual rule. Scaling, additivity, positivity and the full-first-cause partition provide actuarial accounting results. The capstone connects the joint model's strict dependence with real cause-event probabilities and nonnegative expected claim value.

Capstone theorem

The proposed root is the principal actuarial theorem. Its intended actuarial mathematical relationship is illustrated by

$$S_{12}(t,t)=e^{-(a+b+c)t}>e^{-(a+b+2c)t}=S_1(t)S_2(t),\qquad c,t>0.$$

This is a substantive nontrivial model commitment that excludes degenerate substitutes. This formula is stated only under the hypotheses and timing conventions of the actual Lean target. Subordinate theorem declarations provide the named formal prerequisites in the local source inventory. Each supporting milestone requires its own genuine proof rather than a textual assertion that an identity is obvious.

Significance

The results supply a reusable mathematical foundation for joint-life and last-survivor annuities, cause-specific death benefits and pensions involving disability, death and retirement triggers. They expose why observed first-failure data alone cannot determine every latent competing-risk dependence structure, a limitation studied by Tsiatis (1975). The Marshall–Olkin published shock model supports the probabilistic modelling motivation. The event formulation can later be joined with formal survival distributions, conditional hazards and reserve calculations while preserving simultaneous-event conventions.

Difficulty

The major proof obligations concern event measurability, countable additivity, event partition exhaustiveness and strict versus non-strict comparisons. Algebraic exponential survivor formulas do not by themselves establish independence of primitive failure times or the distribution of the first-cause variable. A genuine random-shock claim requires an actual probability measure and events. The capstone's source model is deliberately finite and avoids declaring a general copula representation without its full distributional hypotheses. A published source on competing-risk nonidentifiability, Tsiatis (1975), https://pmc.ncbi.nlm.nih.gov/articles/PMC432231/, describes why additional identifying assumptions are necessary.

Formalization scope

This graph contains formal definitions of observed times and cause probabilities, supporting theorem targets for disjoint probability partitions and the Marshall–Olkin family, and one main actuarial claim-value capstone. General copulas, a fully general conditional joint-lifetime distribution and parametric shock-cause probability from three genuinely independent exponential random variables are natural extensions. The proposed current theorem graph is fully specified in the local dependency inventory. A remote declaration check with sorry placeholders validates only elaboration. Accepted proofs and a moderator-published mission are separate future stages. The staged inventory comprises 14 definitions and 34 open theorem targets. It uses the pinned Mathlib revision and a guarded remote private compiler. The proposed definitions also provide reusable results for future actuarial missions and downstream applications. The planned graph is recorded independently of theorem proof acceptance. The mathematical identities are already established in published actuarial or probability literature; the proposed Lean results remain new unproved formal targets. Every target remains open until an accepted proof is verified, and no owner item is to be confirmed or submitted for moderator review without human assessment.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Third Edition, John Wiley & Sons, chapters 11, 17 and 19. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
• Albert W. Marshall and Ingram Olkin (1967), A Multivariate Exponential Distribution, Journal of the American Statistical Association 62, 30–44. https://doi.org/10.1080/01621459.1967.10482885

Motivation

The Cramér–Lundberg surplus model values how initial risk capital and premiums absorb claims arriving according to a Poisson process. Under exponential claim severities it admits an explicit ruin formula and Lundberg exponent. Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 23, covers martingales, adjustment coefficients and the compound Poisson surplus model. Rather than reproduce an elementary bounded gambler's-ruin recursion from previous missions, we formalise the distinctive exponential-severity transform and the actual renewal convolution integral required by the classical model.

Setting

Assume claim-count intensity lambda>0, premium rate c>0, independent claim amounts with Exp(beta) rate beta>0, and the net profit condition c beta>lambda. The expected aggregate loss over t is lambda t/beta. The risk adjustment coefficient R=beta-lambda/c is then strictly between zero and beta. The exponential severity MGF is beta/(beta-r) only for r<beta. Its net-loss exponent λ(M_X(r)-1)-cr vanishes at R. Define the explicit candidate ψ(u)=(lambda/(c beta))*exp(-R u) and the actual convolution ∫_0^u ψ(u-x) beta exp(-beta x) dx.

Formalization targets

Aggregate loss and the net profit condition

Let $\lambda>0$ be the Poisson claim-arrival intensity, $c>0$ the premium income per year and $\beta>0$ the rate of independent exponential claim sizes. The expected claim amount is $1/\beta$; consequently, the expected aggregate loss over duration $t$ is $\lambda t/\beta$. The expected surplus accounting identity is

$$\mathbb{E}[U(t)]=u+ \left(c-\frac{\lambda}{\beta}\right)t.$$

The strict net profit condition $c\beta>\lambda$ makes the expected rate of capital accumulation positive.

Exponential claim transform and adjustment coefficient

For a severity with an exponential distribution, the moment generating function is finite only for $r<\beta$:

$$M_X(r)=\frac{\beta}{\beta-r},\qquad r<\beta.$$

The Lundberg equation compares the exponential claim cost with the premium contribution. Under the net profit condition, its nonzero adjustment root is

$$\lambda\bigl(M_X(R)-1\bigr)=cR,\qquad R=\beta-\frac{\lambda}{c}>0.$$

The theorem targets establish the necessary denominator and sign restrictions, together with the corresponding exponential transform identity.

Candidate ruin function and renewal equation

Define the classical exponential-severity ruin candidate for initial capital $u\ge0$ by

$$\psi(u)=\frac{\lambda}{c\beta}e^{-Ru}.$$

The capstone verifies both the derivative of this function and the genuine convolution with the exponential severity density. The resulting integro-differential identity is

$$c\psi'(u)=\lambda\left[ \psi(u)- \int_0^u\psi(u-x)\beta e^{-\beta x}\,dx -e^{-\beta u}\right].$$

Proving that the candidate satisfies this equation is a nontrivial analytic step. Identifying it with the probability of the actual stochastic first-passage ruin event requires a separately constructed Poisson surplus process and appropriate renewal uniqueness or stopping-time arguments, which remain outside this mission.

Significance

The classical Lundberg risk-model literature motivates this setup. The capstone proves that an authentic positive adjustment root exists under stated assumptions, that the analytically defined net-loss moment transform is one at the adjustment root, and that the candidate function differentiates and solves the compound Poisson renewal differential/integral equation using the integral defined in Lean. This is substantially stronger than proving the algebraic exponential ansatz alone, and its boundary ψ(0)=lambda/(c beta) and capital monotonicity are separately covered. Existing missions establish finite-horizon ruin and bounded stopping ingredients. This mission goes beyond them by requiring the actual convolution integral with exponential severities, rather than postulating a renewal formula. All the new formal targets remain open Lean declarations, not accepted proofs. The stochastic identification of this unique analytic solution with the infinite-horizon ruin probability is a further theorem, not asserted without probabilistic martingale or renewal uniqueness hypotheses.

Difficulty

The exponential moment generating function exists for r<beta, not at r=beta; strict positive intensity, net profit and nonzero denominators are enforced. The ruin differential equation has an integral convolution and a remaining severity-tail term, and the sign is sensitive to whether the surplus decreases at claim arrivals. The candidate is only defined as the proposed analytic ruin function; an equation-satisfying candidate alone cannot be claimed to equal the actual stopping-time ruin event probability. Lean differentiability and interval integration are checked remotely against a pinned revision, never via local Lean.

Formalization scope

The formal target covers expected compound Poisson loss and premium cashflows, the exponential severity transform, adjustment equation, renewal convolution and candidate solution for strictly positive exponential severities and premium rate, with u≥0 for probability interpretations. It does not directly construct a Poisson stochastic process, prove an exponential martingale from its probability law or prove uniqueness of a renewal equation solution. Those are explicit future reusable probability-theory extensions; the finite positive capital formula is formalised as a candidate until supported by a stochastic theorem.

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.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 23, Sections 23.3–23.7. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml
• Hanspeter Schmidli (2017), Risk Theory, first edition, classical collective risk and adjustment coefficients. https://link.springer.com/book/10.1007/978-3-319-72005-0
• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 23. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml

Motivation

The transition-intensity generator and prospective reserve equation are the key bridge between finite actuarial multi-state valuations and continuous-time life-contingency models. Promislow (2015), Chapter 19, and the research article Markov models and Thiele's integral equations for the prospective reserve establish the broader context. LXXV treats discrete-time state and duration resets; this mission creates genuinely continuous-time transition and actuarial reserve targets.

Setting

Three finite employment/life statuses admit a time-local generator Q with off-diagonal rates r_ij≥0 and diagonal Q_ii equal to minus the total rate of leaving state i. The short-period matrix I+hQ is stochastic only under a step-size condition, and no Euler approximation is misrepresented as the exact matrix exponential. A separate exact two-status alive/dead model at constant mortality intensity mu has survival exp(-mu t) and an absorbing death row. For this analytically solvable submodel, a finite-term prospective reserve incorporates continuous running payments, a death benefit and a discount force delta.

Formalization targets

Conservative three-state transition rates

Let $r_{ij}$ denote the annualised instantaneous rate of moving from state $i$ to a different state $j$. The model begins with three states and constructs the generator $Q=(q_{ij})$ from nonnegative off-diagonal rates, rather than assuming that the transition matrix already has the desired properties.

$$q_{ij}=r_{ij}\quad(i\ne j),\qquad q_{ii}=-\sum_{j\ne i}r_{ij},\qquad \sum_jq_{ij}=0.$$

For a time increment $h$, the Euler approximation $I+hQ$ retains unit row sums. Its entries represent valid nonnegative transition weights only when $h\ge0$ and $h\sum_{j\ne i}r_{ij}\le1$. This step-size condition is part of the mathematical result.

Exact continuous-time survival

The next group treats an insured person who is alive initially and whose death state is absorbing. With constant mortality intensity $\mu$, the probabilities of remaining alive and having died by duration $t$ are

$$p_{00}(t)=e^{-\mu t},\qquad p_{01}(t)=1-e^{-\mu t},\qquad p_{11}(t)=1.$$

The targets establish nonnegativity, normalisation, the Chapman–Kolmogorov semigroup law and the derivatives of survival and death probabilities. This exact exponential model is distinct from the finite-step Euler approximation above.

Prospective reserve and Thiele equation

Let $b$ be a continuous benefit outgo rate, $B$ the benefit on death, $\delta$ the force of interest and $T$ the contract maturity. For $t\le T$, the constant-intensity prospective reserve is

$$V(t)=\frac{b+\mu B}{\delta+\mu} \left(1-e^{-(\delta+\mu)(T-t)}\right).$$

The capstone derives its terminal condition and differentiates this defined reserve to obtain

$$V'(t)=(\delta+\mu)V(t)-b-\mu B,\qquad V(T)=0.$$

This is an exact alive/dead actuarial result. A general nonstationary three-state reserve differential system requires further transition-kernel and differentiability hypotheses and is not claimed here.

Significance

As explained in the continuous-time reserve literature, the main target derives the conservation property of Q and its short-step transition matrix, exact exponential Chapman–Kolmogorov for the alive/dead process, and a derivative identity for an explicit prospective reserve, namely V'(t)=(delta+mu)V(t)-b-mu B, V(T)=0. This is a mathematically defensible continuous-time stepping stone toward full time-inhomogeneous three-state reserve systems. It does not take the desired ODE as a premise.

Difficulty

Conservativity requires cancelling the generator diagonal against all off-diagonal exit rates. Euler steps require nonnegative h and h times the total departure rate at most one for nonnegative stay probability. Exponential semigroup identities require correct absorbing death treatment. Derivative calculations combine the exponential chain rule and nonzero delta+mu, with negative time-to-maturity kept outside the physical future-time domain when discussing positivity. Previously established actuarial models have described finite state-transition accounting and single-state Thiele expressions, while all new theorems in the current formalisation remain open. The generator and transition operators in this mission are independently specified, so row conservation and the ODE are proof obligations rather than assumed axioms. Nonstationary general-state Kolmogorov equations remain separate open mathematical work and are not asserted by this special constant-rate capstone.

Formalization scope

A three-status arbitrary conservative generator with valid Euler short-step and a continuous-time two-status exponential Markov insurance submodel. The Thiele result is derived for an absorbing-life special case, not a general three-state nonstationary Thiele system and not a semi-Markov duration-dependent forward integro-differential law. The nontrivial capstone must substantively differentiate a reserve derived from dated benefits, not merely rename a differential equation or assume the desired target. The generalised setting is supported by explicit structural lemmas but needs further probability and differentiability formalisation before a complete multi-state ODE can be asserted. All targets are original formal derived claims; the declarations are not accepted proofs.

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.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapter 19, sections 19.3–19.6. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml
• Markov models and Thiele's integral equations for the prospective reserve, Insurance: Mathematics and Economics 19(3) (1997), 187–235. https://doi.org/10.1016/S0167-6687(97)00020-6
• Buchardt, Møller and Schmidt (2015), Cash flows and policyholder behaviour in the semi-Markov life insurance setup. https://doi.org/10.1080/03461238.2013.879919

Motivation

Ruin theory connects claim arrival, premium receipts and capital sufficiency with path-dependent insurer solvency events. Chapter 23 of Promislow's Fundamentals of Actuarial Mathematics explicitly covers the distribution of deficit at ruin, recursions and the compound Poisson surplus process. The 2018 study of discrete-time ruin recursions illustrates the importance of distinguishing a classical first passage event from delayed Parisian ruin. Existing actuarial missions handle expected aggregate claims and some ruin probability inequalities; this new mission supplies exact finite pathwise accounting and deficit-at-first-ruin lemmas rather than repeating those earlier targets.

Setting

At integer time n, capital U_n equals initial monetary reserve u plus n premiums of amount c less all n claims X_k settled in periods 0 through n-1. The ruin event is U_n<0, with strict inequality; equality to zero is solvent for this model. Finite-horizon ruin is the union of ruin observations up to n, and a first-ruin event at n excludes every earlier negative surplus. Deficit D_n=max(0,-U_n) is positive precisely when the period-n surplus is negative. Claims can recover the portfolio after an early ruin event, so period-end ruin and by-horizon ruin are not identical.

Formalization targets

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

Premium and claim surplus cash-flow recursion

This block contributes 16 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.ruNetClaimTotal_reconcile`:

$$U_n=u-Σ(X-c)$$

Surplus is opening capital minus cumulative net claims.

First passage and deficit at ruin

This block contributes 12 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.ruCumulativeMargin_eq_surplus`:

$$M_n=U_n$$

Independent premium/claim accounting agrees with the period-end surplus calculation.

Stop-loss reinsurance, retained deficit and pathwise capital

This block contributes 15 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.ruRuinDeficit_fundamental`:

$$U_{n+1}=U_n+c-X_n;D_n=-U_n;U^R=U+Y$$

The capstone derives the surplus recursion, genuine positive deficit on the first-ruin event, and the pathwise reinsurance gain, with original capital and premium unchanged.

Capstone theorem

The main target is `ActuarialValuation.ruRuinDeficit_fundamental`. The capstone derives the surplus recursion, genuine positive deficit on the first-ruin event, and the pathwise reinsurance gain, with original capital and premium unchanged.

$$U_{n+1}=U_n+c-X_n;D_n=-U_n;U^R=U+Y$$

Significance

The published ruin-theory treatment motivates conditional deficits at failure. A first-passage deficit is a cash shortfall conditional on ruin occurring at that exact time; the mission proves positivity and exact magnitude from the surplus path independently of any loss distribution. It then integrates an excess-of-loss treaty that splits claims into retained min(X,d) and ceded max(0,X-d). This financial identity shows when cumulative reinsurance recoveries improve the surplus path, assuming the same premium rate: U^R=U+ceded. Any later premium ceded to reinsurers must be explicitly modelled before calling that comparison an economic gain. The result provides a reusable basis for subsequent ruin probabilities, stochastic aggregate processes and formal reinsurance contracts.

Difficulty

The deficit at ruin is defined at the first passage, not arbitrarily at a later negative-surplus period. The first-passage event makes ruin time unique and requires quantification over all previous observations. The insurer may emerge from negative surplus at a later period, so no implication from solvency at n to absence of earlier ruin is valid. All finite sums respect half-open settlement times; adding the new year must not double count claims. The ceded premium, reinsurer credit risk and interest are excluded from the explicitly fixed-premium comparison. Lean 4 uses finite sums and arithmetic with targeted Mathlib imports; no local Lean compilation occurs.

Formalization scope

The theorem graph is a discrete-time finite-horizon surplus and first-ruin model, not a claim of the infinite-horizon Cramér-Lundberg or Pollaczek-Khinchine formula. It includes a two-scenario probability mixture only as an elementary example of genuine probability-weighted ruin events. No adjustment coefficient or optional-stopping theorem is assumed for the pathwise capstone, thereby excluding a vacuous claim of infinite-horizon ruin bounds without stochastic hypotheses. The finite formalization prepares those future theorems while retaining genuine nontrivial first-event quantifiers and reinsurance identities.

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.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapter 23, Sections 23.4–23.6. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml
• Zbigniew Palmowski, Lewis Ramsden, Apostolos D. Papaioannou (2018), Parisian ruin for the dual risk process in discrete-time, European Actuarial Journal. https://link.springer.com/article/10.1007/s13385-018-0172-8

Motivation

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.

Setting

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.

Formalization targets

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

Finite-state transition and probability conservation

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`:

$$M((pT)U)=M(p)$$

Two successive stochastic transition years conserve total cohort probability.

Transition benefits, annual reserve values and profit

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`:

$$Π+E+C=P$$

Premium allocation exactly partitions earnings, expenses and expected claims.

Duration-dependent semi-Markov disability and exit valuations

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`:

$$ΣpT=Σp;(pT)U=p(TU);V_i(d)=b_i+vΣ_jT_ij(d)V_j$$

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.

Capstone theorem

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.

$$ΣpT=Σp;(pT)U=p(TU);V_i(d)=b_i+vΣ_jT_ij(d)V_j$$

Significance

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.

Difficulty

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.

Formalization scope

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.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapter 19, Sections 19.2–19.6. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml
• David Dickson, Mary Hardy and Howard Waters (2009), Actuarial Mathematics for Life Contingent Risks, Chapter 8. https://www.cambridge.org/core/books/abs/actuarial-mathematics-for-life-contingent-risks/multiple-state-models/BFEB2CD04A3EA012FCB1C7E3A326E9A0
• Kristian Buchardt, Thomas Møller and Kristian Bjerre Schmidt (2015), Cash flows and policyholder behaviour in the semi-Markov life insurance setup, Scandinavian Actuarial Journal. https://www.tandfonline.com/doi/full/10.1080/03461238.2013.879919

Motivation

The collective risk model uses a random count of insurance claims and a severity distribution to obtain an aggregate loss law. Promislow's Fundamentals of Actuarial Mathematics, Chapter 21, discusses compound distributions, generating functions and the distinctive recurrence when individual claim amounts may be zero. The book's publisher contents identify the specialised zero-amount section. Published actuarial work also analyses the Panjer recurrence family. Prior actuarial missions address aggregate loss and some recursions; this extension connects generating transforms directly to an explicit count/severity model where zero-size claims occur.

Setting

A claim severity X takes nonnegative integer values with finite probability mass f_k, explicitly allowing f_0>0. A compound total S is the sum of N independent severities. The mission proves a product-transform identity for two independent severities with finite support and a composition identity for Bernoulli N in {0,1}. It separately records the first two raw aggregate moments when N is supported on {0,1,2}; this relies on identically distributed and independent severities, so the cross term is 2p_2(E[X])². For Panjer's (a,b,0) count family, Bernoulli frequency has a=-p_1/p_0 and b=2p_1/p_0 for p_0 nonzero. Its zero-size correction is (1-a f_0). All probabilities and denominator restrictions are explicit.

Formalization targets

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

Finite count, severity and convolution transforms

This block contributes 20 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.cxSecondMoment_succ`:

$$m_{2,n+1}=m_{2,n}+n² f_n$$

The new claim-size category contributes its squared severity times probability.

Bernoulli claim counts, zero claims and aggregate moments

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.cxTwoClaimMoment_two_decomposition`:

$$m_{2,S}=E[N]m_{2,X}+2p_2μ²$$

The two-claim cross product adds twice the product of the severity means.

Panjer adjustment with mass at zero

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.cxCompoundRisk_fundamental`:

$$G_S=G_N(G_X);(1-af_0)g_1=(a+b)f_1g_0$$

The compound-risk capstone reconciles independent frequency/severity generating functions, probability normalisation, the aggregate zero atom, and the nontrivial Panjer zero-severity correction to the first positive aggregate mass.

Capstone theorem

The main target is `ActuarialValuation.cxCompoundRisk_fundamental`. The compound-risk capstone reconciles independent frequency/severity generating functions, probability normalisation, the aggregate zero atom, and the nontrivial Panjer zero-severity correction to the first positive aggregate mass.

$$G_S=G_N(G_X);(1-af_0)g_1=(a+b)f_1g_0$$

Significance

A nonzero count of zero-sized claims is a different event from zero claims. The original published Panjer analysis confirms that the general recursion involves the denominator 1-a f_0. We prove a concrete nontrivial Bernoulli first-positive-atom instance from the independently defined compound mass rather than defining the answer equal to its recurrence. This provides a reusable exact boundary case for larger frequency families while also proving the proper generating-function composition and normalisation invariants.

Previously established actuarial theory supplies the probability and valuation setting; this mission proposes additional original derived formal theorems whose Lean proofs remain open.

Difficulty

The zero aggregate mass is p_0+p_1 f_0, not p_0 unless zero-sized claims are excluded. PGF multiplication requires explicit independent product masses and correct truncation of each finite support. The zero-size Panjer factor requires a denominator nonzero and a valid Bernoulli count law with p_0>0. The full infinite Poisson/negative-binomial Panjer recursion is outside the formal scope, and the finite Bernoulli boundary case is deliberately not described as that general result. The source is a finite real-algebraic Lean 4 model using targeted Mathlib sum imports and no local Lean compilation.

Formalization scope

The formalization targets use finite sums of real probability weights on nonnegative integer claim sizes and a Bernoulli frequency model. They exclude degenerate statements that introduce the target recurrence as an assumed equality. The genuine proof goal is to derive the adjusted recurrence from independently defined aggregate probabilities. A separate count support {0,1,2} provides a raw-moment calculation for independent severities. No theorem here asserts the general arbitrary (a,b,0) recurrence or a distributional equality for unconstrained unbounded claim counts.

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.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapter 21, Sections 21.10-21.11. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml
• Harry H. Panjer (1981), Recursive Evaluation of a Family of Compound Distributions, ASTIN Bulletin 12(1), pp. 22–26. https://doi.org/10.1017/S0515036100006796

Motivation

Term-structure valuation represents the price of a certain unit payment at each future maturity using a zero-coupon discount curve. This produces cashflow valuation, bond duration and implied forward discount factors. Bond prices at future dates may be random, even though redemption is certain at maturity. Promislow develops fixed-income valuation in Chapter 2 and the arbitrage-free stochastic bond-market extension in Chapter 20. The central distinction is between multiplying known deterministic discount ratios and pricing uncertain future bond prices using an appropriate stochastic discount factor or risk-neutral valuation rule. Both conventions are made explicit in the new Lean targets. The book is S. David Promislow, Fundamentals of Actuarial Mathematics, Third Edition (2015), chapters 2.12–2.13 and 20.13. The independently published supporting research reference is available here.

Setting

At issue, D(t) is the deterministic price in currency of a unit default-free zero-coupon maturity payment at integer date t. Normalise D(0)=1 for the usual spot-discount interpretation and require strictly positive D(t) before dividing by it. A bond paying face F at T has price F D(T). If a forward contract settles at s and redeems at t, its deterministic implied discount is D(t)/D(s), with 0≤s≤t for an economic forward period. Gross forward accumulation is its reciprocal; effective single-interval interest is gross return minus one. Fixed bond coupons are paid at integer year ends and a redemption payment can be included in the final cashflow. Stochastic one-period claims are represented by a finite scenario distribution and a positive state-dependent deflator.

The central actuarial model can be written

$$P(0,T)=D(T),\quad P(s,T)=\frac{D(T)}{D(s)},\quad P(0,T)=P(0,s)P(s,T)\ \text{for deterministic discount curves}.$$

Formalization targets

Deterministic zero-coupon bonds and forward discounts

The first group formalises spot zero-coupon bond values, deterministic forward discounts, forward gross returns, effective forward interest and a flat annually compounded term structure. Discount factors across an intermediate settlement time compose multiplicatively when the denominator bond prices are nonzero. The forward bond value times the discounted settlement price reconstructs the present value of the maturity redemption. Positive prices ensure that inversion and the implied one-year forward are mathematically and economically meaningful. The curve may change shape with maturity; flat rates form one explicitly controlled special case.

Coupon-bond cashflows duration and flat yield

The second group handles a complete set of finite annual coupon cashflows, with payment k made at k+1 years. It defines the bond's present value, first time-weighted moment, Macaulay duration, convexity time moment and the coupon that prices a unit-redemption bond at par. Linear cashflow valuation, addition of a coupon, positivity and the weighted-time accounting identity follow under correct nonzero denominators. Monetary amounts and dates carry distinct units: duration is measured in years, market value in currency and discount factors are dimensionless. The scope is fixed scheduled cashflows without mortality or credit dependence.

Finite-state stochastic discount factors and arbitrage-free valuation

The third group prices a genuine finite-state random bond delivery using state probabilities and stochastic discount factors. Under positive and normalised state weights the price of a certain unit maturity payment is the weighted expectation of the deflator, while an uncertain delivery is priced using the weighted deflated payoff. A zero-value forward delivery price is the ratio of these two state prices when the unit-bond denominator is nonzero. The theorem graph establishes its uniqueness. This formalism avoids claiming that an unobserved future stochastic discount factor is equal to a deterministic ratio of today's bond prices path by path.

Capstone theorem

The proposed root is ActuarialValuation.bdForwardBond_fundamental. Its intended actuarial mathematical relationship is illustrated by

$$\frac{D(u)}{D(s)}\frac{D(T)}{D(u)}=\frac{D(T)}{D(s)},\qquad F\frac{D(T)}{D(s)}D(s)=FD(T).$$

This is a substantive nontrivial model commitment that excludes degenerate substitutes. This formula is stated only under the hypotheses and timing conventions of the actual Lean target. Subordinate theorem declarations provide the named formal prerequisites in the local source inventory. Each supporting milestone requires its own genuine proof rather than a textual assertion that an identity is obvious.

Significance

The resulting formalisation is directly relevant to pension liability cashflows, bulk annuity asset valuation, investment guarantees and interest-rate hedging. A stochastic term-structure modelling framework with arbitrage restrictions was developed by Heath, Jarrow and Morton (1992), whereas the proposed deterministic forward identities are elementary building blocks. Formal separation of spot curves, forward prices and state-contingent valuation should make it easier to audit inconsistent maturity dates, discount-curve interpolation assumptions and unsupported arbitrage conclusions.

Difficulty

The major issue is maturity timing and conditional valuation. A certain redemption has an unknown market price before maturity if discount rates are stochastic. The deterministic multiplicative relationship is valid for time-zero discount curves; it cannot be imposed on random future bond-price processes without a sufficiently strong assumption. A genuine risk-neutral martingale statement also needs a numeraire and filtration. Nonzero forward-price denominators and nonnegative state deflators matter to financial interpretation. A bond duration formula is undefined economically at zero present value, even though Lean's real division is total. The proposed capstone carefully stays within explicitly deterministic forward funding identity.

Formalization scope

Definitions span deterministic bond curves, annual forwards, flat gross-return curves, coupon present values, duration, convexity and par coupon, together with finite-state stochastic claim discounting. The main theorem establishes multiplicative deterministic forward discount consistency and a forward bond funding identity. The stochastic state-price results form a separate cluster for subsequent risk-neutral bond-market integration. Full short-rate models, adapted random term structures, conditional martingales, forward-measure changes and HJM drift restrictions require substantial additional probability theory and remain future targets. The staged inventory comprises 16 definitions and 35 open theorem targets. It uses the pinned Mathlib revision and a guarded remote private compiler. The proposed definitions also provide reusable results for future actuarial missions and downstream applications. The planned graph is recorded independently of theorem proof acceptance. The mathematical identities are already established in published actuarial or probability literature; the proposed Lean results remain new unproved formal targets. Every target remains open until an accepted proof is verified, and no owner item is to be confirmed or submitted for moderator review without human assessment.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Third Edition, John Wiley & Sons, chapters 2.12–2.13 and 20.13. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
• David Heath, Robert Jarrow and Andrew Morton (1992), Bond Pricing and the Term Structure of Interest Rates: A New Methodology for Contingent Claims Valuation, Econometrica 60, 77–105. https://www.jstor.org/stable/2951677

Motivation

Pension plan valuation requires three distinct operations: measuring benefits acquired during service, pricing the probability and timing of exit benefits, and funding those liabilities with contributions. Dickson, Hardy and Waters, Actuarial Mathematics for Life Contingent Risks (2009), Chapter 9, treat salary scales, DC contribution rates, the pension service table, benefit valuation and funding in one coherent mathematical sequence. Existing actuarial Prove2Me missions formalise salary-linked pensions, competing decrements and projected unit credit separately. This research extension fills the remaining foundational connections: explicit salary interpolation and final-average windows, DC replacement targets including spouse reversions, deferral and death-in-service contingent benefits, traditional versus projected unit credit, and the annual funded-service reserve balance.

Setting

An employee earns annual salary scale S_t, credited annual pension accrual fraction alpha, and completed service n. A finite final-average salary is the arithmetic mean over a nonempty window of annual salary observations, with a stated zero convention for an empty one. Within-year salary is interpolated linearly and a mid-year service exit can earn an additional one-half year of pension accrual. For DC funding, salary-proportional contributions are paid at each year end, accumulated at multiplier j, and converted at retirement into a target pension replacement ratio tau times retirement salary. The annuity factor includes a spouse reversion valued contingently on the member dying first. Active DB members face mutually exclusive withdrawal, death, disability and retirement transitions, producing probability-weighted pension costs and a survivor continuation reserve. The simplified PUC model values completed service at projected salary while TUC values the same service at current salary under a common retirement factor.

Formalization targets

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

Salary scales, average pay and fractional service

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.pen9MidyearPension_delta`:

$$B_{n+1/2}-B_n=\alpha S/2$$

Within-year exits credit one half-year under the stated service convention.

DC accumulation and replacement-ratio annuity funding

This block contributes 12 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.pen9TargetCapital_annuity_monotone`:

$$a_1\le a_2\implies K_1\le K_2$$

More expensive annuity pricing cannot reduce the target DC pension capital.

Service-table exits, survivor and deferred benefits

This block contributes 11 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.pen9AnnualExitPV_nonneg`:

$$p_t,v_t,B_t\ge0\implies EPV_n\ge0$$

Valid finite exit-survival and payment assumptions preserve nonnegative valuations.

Projected versus traditional unit credit and reserve recursion

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.pen9PensionFunding_fundamental`:

$$A(c^*)=K,\quad AL^{PUC}_{n+1}=AL^{PUC}_n+NC,\quad AL^{PUC}-AL^{TUC}=\alpha n\Delta S f,\quad V_t+C_t=E_t+vp^aV_{t+1}$$

A combined pension valuation and funding theorem: DC accumulation finances a salary-replacement pension including survivor annuity; DB projected service cost adds to PUC liability; the TUC difference is the projected salary revaluation; and the annual contribution uniquely balances exit benefits with the continuation reserve.

Capstone theorem

The main target is `ActuarialValuation.pen9PensionFunding_fundamental`. A combined pension valuation and funding theorem: DC accumulation finances a salary-replacement pension including survivor annuity; DB projected service cost adds to PUC liability; the TUC difference is the projected salary revaluation; and the annual contribution uniquely balances exit benefits with the continuation reserve.

$$A(c^*)=K,\quad AL^{PUC}_{n+1}=AL^{PUC}_n+NC,\quad AL^{PUC}-AL^{TUC}=\alpha n\Delta S f,\quad V_t+C_t=E_t+vp^aV_{t+1}$$

Significance

The IAS 19 funding and valuation framework informs the actuarial attribution assumptions. The mathematical funding identities explain where projected salary changes affect attributed DB pension liability, and why traditional unit cost and projected unit cost may differ even when they share the same mortality, discount and annuity assumptions. The salary and exit definitions also make payment timing explicit rather than hiding different conventions inside a pension factor. The DC funding calculation models a target rather than a guarantee: contributions achieve the target only if the assumed investment growth, salary pattern and annuity price materialise. The reserve recursion is a genuine unique contribution balance, not a tautology about the definition of benefits. This is a reusable finite mathematical foundation for subsequent multi-year DB funding and experience analysis.

Difficulty

A withdrawal-deferred pension requires both withdrawal probability and survival between withdrawal and retirement. The spouse reversionary annuity factor must be contingent on member death to avoid paying two independent ordinary annuities. An exit in the middle of a service year changes credited pension service; half-year accrual is not justified if the scheme only credits whole years. Distinguishing an investment accumulation multiplier from a discount factor is essential for DC targets. In PUC and TUC, salary repricing is separated from the cost of earning one further unit of service; positive salary growth alone cannot establish monotonic liabilities without nonnegative accrual and factor assumptions. The active-continuation coefficient in the reserve recursion must already contain time discounting, whereas competing-decrement probabilities are undiscounted.

Formalization scope

The Lean statements are self-contained finite sums, arithmetic recursions, and salary-proportional valuation identities. Probabilities, survival terms, annuity factors, contribution rates, salary and benefit amounts are explicit independent inputs with assumptions applied where bounds are claimed. We do not claim that a positive DC investment fund guarantees a target realisation or that the accounting method chosen implies scheme-specific statutory funding. The capstone is nontrivial because the DC and DB formulae have distinct time horizons and financial units; it excludes the vacuous substitute of assuming the desired reserve-balance identity as an unproved hypothesis. This mission complements but does not duplicate the previously published salary/pension and multiple-decrement missions or the pending projected-unit-credit mission. No local Lean or Mathlib compilation is run; authoritative Prove2Me remote elaboration is required before owner Draft creation.

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.

Selected references

• Dickson, D. C. M., Hardy, M. R., and Waters, H. R. (2009), Actuarial Mathematics for Life Contingent Risks, Chapter 9, Pension Mathematics. Cambridge University Press. https://www.cambridge.org/core/books/abs/actuarial-mathematics-for-life-contingent-risks/pension-mathematics/E935265B9EFB465A282DE1BD6254B67A
• IFRS Foundation (accessed 2026), IAS 19 Employee Benefits, paragraphs 67–74 (projected unit credit and allocation of benefits to periods of service). https://www.ifrs.org/issued-standards/list-of-standards/ias-19-employee-benefits/
• Actuarial Standards Board (accessed 2026), Unit Credit Actuarial Cost Method, glossary (normal cost and accrued liability). https://www.actuarialstandardsboard.org/glossary/unit-credit-actuarial-cost-method/
• Institute and Faculty of Actuaries (accessed 2026), GN26 Pension Fund Terminology, section 3. https://www.actuaries.org.uk/system/files/documents/pdf/GN26V1-0.pdf

Motivation

Universal-life policies maintain a distinct policyholder account that receives premiums, incurs explicit expense charges, is credited investment interest and finances the cost of life insurance. Unlike a traditional fixed-premium product, account returns and mortality charges can change over time, and an investment-linked contract can contain additional embedded guarantees. Promislow's Fundamentals of Actuarial Mathematics, Third Edition (2015), Chapter 13, develops account recursions, alternative death-benefit structures, credited-interest mechanisms and variable-annuity guarantees. Mary Hardy's Investment Guarantees (2003) provides an independently published actuarial treatment of insurance investment guarantees.

The established mathematical basis covers account balances, insurance pricing and financial option guarantees. Existing Prove2Me actuarial missions contain gross premiums, prospective reserves, investment valuation and option replication, but their theorem inventories do not yet provide the exact universal-life account recursion and guarantee decomposition addressed here. This new mission constructs explicit policy-account mathematics and scenario-based guarantee valuation with original unproved Lean declarations.

Setting

Time is indexed by policy period k, typically months, and all monetary variables are currency amounts at their stipulated valuation instant. An initial account A at the start of a period receives a cash premium π, from which a percentage expense r is deducted, together with a flat expense e. The resulting amount earns credited rate i through the period. A death claim associated with this period is payable at the end of the period. The insured mortality charge is the cost-of-insurance rate q multiplied by the relevant end-period net amount at risk. The conventional economic basis requires 0≤r≤1, 0≤q<1 and 1+i>0 where cancellation and nonnegative accumulation are invoked.

Let the pre-insurance earned account be

$$E=(A+\pi(1-r)-e)(1+i).$$

For a Type B death benefit, the amount in excess of account value at death is the fixed additional face amount b, and the closing account is E-qb. For a Type A structure, b is the fixed total death benefit and the net amount at risk is b minus the end-period account in the covered region. The implicit survivor-account equation therefore requires q<1 and the appropriate benefit-dominance condition. A separate guarantee may instead pay the larger of the investment account and a specified floor.

Formalization targets

Monthly account premium expenses and insurance charges

The first group states the premium allocation π(1-r), the post-premium account A+π(1-r)-e, credited accumulation E, and the start-period cost-of-insurance equivalent qη/(1+i), where η is the period-end amount at risk. If insurance charges use a separate discount rate j, the adjusted effective mortality charge is q(1+i)/(1+j). An explicit reserve recursion then accounts for the different investment and mortality-charge bases. Theorems establish exact charge reconciliation, nonnegative allocations under appropriate expense rates, monotonicity of charged premiums and equivalence when the two discount bases agree. A credited-rate floor, cap and participation fraction are represented using an explicit clamp with the floor no higher than the cap for valid contractual interpretation.

Type A and B mortality strain and explicit guarantee

The Type B closing account is defined by a direct subtraction of q times the additional face amount. The Type A solution accounts for the dependence of insured risk on its own closing balance:

$$A_{B}=E-qb,\qquad A_{A}=\frac{E-qb}{1-q},\qquad q\ne1.$$

These equations require different interpretations of b and hence are treated as separate contracts. The Lean statements specify the algebraic balance for each and the admissible region of the Type A net amount at risk. A death benefit equal to max(account, floor) is also considered. When the guarantee binds, its survivor account is solved by the Type A equation with the floor. When the earned balance exceeds that floor, the extra death benefit strain is zero. Subordinate results verify the branches and the assumptions which make the piecewise survivor account self-consistent. No reserve identity is asserted when the survival denominator vanishes.

Path-dependent account evolution and stochastic guarantee pricing

An actual policy path is generated recursively from the initial account, period-indexed premiums, charge rates, expenses, credited rates and face amounts. This builds a genuine multi-period monetary ledger, rather than a single-period formula masquerading as a trajectory. Pathwise zero-charge boundaries and a successor equation link the recursion to Type B period values.

An investment guarantee pays the greater of the realised account and a guaranteed floor at death or maturity. Its embedded insurer liability is the positive shortfall max(floor-account,0). The identity

$$\max(A,G)=A+\max(G-A,0)$$

holds on each realised scenario. To value the genuine stochastic guarantee, take a finite probability mass p(ω), a scenario-dependent discount factor d(ω), an account A(ω) and guarantee floor G(ω). Expected discounted benefit is the weighted sum over those states, with p≥0 and Σp=1 required for a valid probability law. The value of the full benefit decomposes into discounted account value plus the insurer's embedded guarantee liability. Theorems establish positivity and monotonicity as the contractual guarantee floor increases.

Capstone theorem

The main theorem ActuarialValuation.ulUniversalGuarantee_fundamental connects the exact Type A and Type B account-funding equations, with nonzero survivor denominator, to the stochastic account-plus-guarantee decomposition. This capstone preserves the difference between the account owned by the insured and the additional option-like obligation borne by the insurer, and follows the actual timing of premium receipts and mortality charges.

Significance

A reusable, explicit account recursion provides a foundation for later development of variable-annuity death and maturity guarantees, secondary no-lapse guarantees, investment-crediting corridors and stochastic profit testing. Hardy (2003) discusses the broader mathematics and risk management of equity-linked guarantees, while the proposed results formalise precise finite contracts with identified payment dates. The scenario-dependent valuation can subsequently connect to the completed binomial hedge proposal and to genuine survival-conditioned insurance cashflow expectations.

Difficulty

The implicit Type A recursion contains the end-period reserve on both sides; division by 1-q therefore has to be justified, and the fixed-total-benefit interpretation applies only while the guaranteed face remains above account value. Type B adds its stated face benefit and uses a different charge. The floor-and-cap crediting mechanism has a contractual ordering assumption, and distinct mortality/interest discount rates cannot be cancelled without a nonzero gross return. Under a negative reserve, policies may lapse unless an explicit secondary guarantee overrides the restriction; an account computation alone does not model the lapse decision.

Stochastic guarantee pricing requires actual scenario probabilities, discount factors and benefit realisations. Theorems concerning a positive option-like liability require nonnegative probabilities and discounts. This nontrivial setting excludes a degenerate zero-payment substitute. The current graph formalises conditional algebra and exact scenario valuation rather than asserting that any arbitrary investment law admits a unique arbitrage-free guarantee price.

Formalization scope

The graph contains 18 proposed reusable definitions and 41 open Lean theorem targets. It comprises monthly or period-indexed account mechanics, implicit and explicit mortality risk structures, interest rate corridors, a genuine multistep account path and the finite stochastic valuation of an investment guarantee. Its proposed capstone is supported by separate funding and stochastic valuation identities. The source inventory, dependency graph, published reference crosswalk and private compiler receipts are retained for human review.

Extensions include lapse guarantees, bid–offer spreads, withdrawals, surrender charges, a full asset-price driven account with a risk-neutral measure, minimum withdrawal guarantees and an explicit benefit date random variable. Those require additional stochastic assumptions. Declaration elaboration with sorry establishes a syntactically and mathematically well-typed proposition, subject to authoritative compiler outcomes; none of these targets is considered proved until an actual accepted proof exists. No owner Draft item should be confirmed or submitted for moderator review without human assessment.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Third Edition, John Wiley & Sons, Chapter 13 and related Chapter 20. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
• Mary R. Hardy (2003), Investment Guarantees: Modeling and Risk Management for Equity-Linked Life Insurance, John Wiley & Sons. https://www.wiley-vch.de/en?isbn=9780471392903&option=com_eshop&title=Investment+Guarantees&view=product

Motivation

Coherent risk measures provide a systematic method of comparing uncertain insurer losses and choosing a capital or premium requirement. Expected loss under one probability distribution is a linear valuation, while uncertain mortality, claims and market assumptions can make several distributions plausible. A conservative insurer may require a price sufficient under each admissible scenario model. Promislow's Fundamentals of Actuarial Mathematics, Third Edition (2015), Chapter 22, develops utility theory, Jensen inequalities, stop-loss risk comparison, capital risk measures and Value-at-Risk and Tail-Value-at-Risk principles. Artzner, Delbaen, Eber and Heath (1999) established the axiomatic coherent risk framework.

The existing Prove2Me actuarial theorem inventories include an entropic premium principle, actuarial stop-loss identities, finite tail value-at-risk and loss distributions. This mission develops a distinct robust expected-loss capital functional over two genuine candidate probability laws, and proves its coherent properties, attainment, conservatism across distribution mixtures and interaction with joint portfolio losses. The results provide reusable mathematical infrastructure for future actuarial solvency and pricing missions.

Setting

Take a finite outcome space indexed by Fin n, on which two candidate probability mass functions p and q satisfy nonnegative weights and total mass one. Let X(ω) and Y(ω) denote real-valued insurer losses in currency units on the same sample scenarios. The model deliberately allows different dependence, mortality or claim-probability assumptions without changing the realised payoff functions. Larger values of X represent larger claim outgo, so capital functions are monotone increasing in X. Expected loss under p is a finite weighted sum. The worst-case premium is

$$\rho_{p,q}(X)=\max\{\mathbb E_p[X],\mathbb E_q[X]\}.$$

For λ in [0,1], define the mixed candidate law r(ω)=λp(ω)+(1-λ)q(ω). Both p and q must be valid probability laws for cash translation invariance and a conventional premium interpretation. Requiring n greater than zero is implicit in probability normalisation, since an empty sample space cannot support a total mass of one. Losses can be negative when outcomes are profitable.

Formalization targets

Actual finite loss distributions and scenario ambiguity

Construct scenario expectations, their linearity and monotonicity, nonnegative-loss valuation, mixtures of the candidate mass functions and the expected premium difference between two models. Show that the mixture has normalised probability mass and remains nonnegative when λ belongs to the unit interval. The main mixture relation is

$$\mathbb E_{\lambda p+(1-\lambda)q}[X] =\lambda\mathbb E_p[X]+(1-\lambda)\mathbb E_q[X].$$

This exact statement makes the uncertainty set mathematically meaningful. Each candidate distribution remains tied to the same scenario-specific insurance loss, preventing accidental replacement of distribution ambiguity with arbitrary deterministic adjustments. A shared scenario space also means two insured portfolio losses may be dependent. Expected aggregate claims still add due to linear expectation.

Coherent worst-case actuarial premium and portfolio

The second group proves the following four coherence properties for ρ with losses interpreted as outgo. For any realised X no greater than Y, ρ(X)≤ρ(Y); for certain monetary shift k, ρ(X+k)=ρ(X)+k; for c≥0, ρ(cX)=cρ(X); and for aggregate losses, ρ(X+Y)≤ρ(X)+ρ(Y). Their simultaneous validity requires nonnegative, normalised scenario weights where appropriate. The subadditivity theorem is a genuine diversification property, because the worst-case candidate distribution may differ for the individual risks:

$$\max(E_p[X+Y],E_q[X+Y]) \le\max(E_p[X],E_q[X])+\max(E_p[Y],E_q[Y]).$$

The mission also proves the envelope dominates the expected loss under every convex mixture of p and q, and one of the original models attains the envelope. The robust loading relative to the first candidate model and the worst-to-best expectation spread are therefore nonnegative, while a singleton ambiguity set recovers the equivalence premium.

The model's functional need not be law-invariant relative to one distinguished reference measure: different scenario payoffs that share a distribution under p can produce different robust premiums if they are weighted differently under q. A concrete two-state counterexample is included to expose that consequence explicitly.

Stop-loss risk comparison and limitations of floored risk principles

The third group formalises an actual loss-excess random variable max(X-d,0) at deductible d and its expected value under a finite probability mass. Stop-loss premiums are nonnegative under valid masses, decrease as the deductible increases and are monotone in losses. A formal stop-loss order compares two loss distributions by the inequality at every deductible, with reflexivity, transitivity and pointwise sufficiency results. A robust stop-loss envelope takes the larger of the two candidate-law expected stop-loss costs.

Some pricing practices impose a separate floor at zero on the coherent robust capital. This creates a nonnegative functional max(0,ρ(X)) but generally breaks cash translation invariance. The target graph contains a simple exact counterexample: a certain loss of negative one requires zero floored capital, and adding one unit of certain loss still requires zero. A genuinely cash-additive risk measure would instead increase by one. The nontrivial mathematical distinction prevents treating an intuitively appealing floor as another coherent premium principle without checking its axioms.

Capstone theorem

ActuarialValuation.crRobustCapital_fundamental establishes, within one source-checked Lean proposition, monotonicity, translation invariance, nonnegative positive homogeneity, subadditivity for combined portfolios and dominance over all convex mixtures of the two candidate probability laws. The capstone refers to the actual finite-scenario expectations and joint portfolio payoff. It does not assume the axioms as hypotheses, and is therefore a substantive proof target.

Significance

A distributionally robust premium formalisation clarifies the mathematical responsibilities of a capital measure and gives a reusable construction for comparing heterogeneous insurance bases. Artzner and co-authors (1999) develop the rigorous coherent risk axioms for insurance and market risks, and their scenario-based interpretation motivates this envelope construction. The stop-loss order provides another basis for assessing which losses generate greater insurer tail payments. Later actuarial applications include premium loadings, reserve uncertainty, portfolio risk aggregation and valuation-basis selection.

Difficulty

The key distinction is between robust expected loss, expected positive loss, a quantile-based capital requirement and a floored capital requirement. Each functional can satisfy different axioms and should not be labelled coherent without verification. Translation invariance requires the candidate distributions both have unit total mass. Monotonicity requires nonnegative mass, while the robust expectation of a negative cashflow may legitimately be negative. Positive homogeneity is asserted only for nonnegative scaling. Stop-loss retention and loss amounts share currency units, and the equality boundary is included in the nonnegative excess definition.

The main capstone must reconcile all four properties and the model-mixture upper bound simultaneously. Algebraic examples and numerical tests can expose mathematical defects, but passing those checks does not establish a Lean theorem proof. The proposal keeps the actual probability distributions and contract losses explicit and excludes a vacuous assignment of coherence to an uninterpreted symbol.

Formalization scope

There are 15 proposed definitions and 42 open theorem targets. The model covers exact finite-scenario probability mixtures, robust premiums and margins, aggregate insurance losses with dependence, a selected worst-case distribution, stop-loss contracts and risk ordering, together with counterexamples to careless capital-principle generalisation. The intended theorem graph is locally recorded, and source provenance distinguishes published theory from original derived Lean statements. Individual private declaration compilation with sorry placeholders and genuine accepted Lean proofs remain separate stages.

Extensions include countably infinite ambiguity sets, a distributionally robust Tail-Value-at-Risk representation, coherent spectral risk measures with general measurable losses and a convex-order implication for all suitable convex payoff functions. Existing finite Tail-Value-at-Risk and entropic premium results are candidates for reuse in those extensions. No new item should be confirmed and no Draft should be submitted for moderator review before human mathematical review.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Third Edition, Wiley, Chapter 22. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
• Philippe Artzner, Freddy Delbaen, Jean-Marc Eber and David Heath (1999), Coherent Measures of Risk, Mathematical Finance 9, pp. 203–228. https://doi.org/10.1111/1467-9965.00068

Motivation

Martingales and stopping times link the evolution of an insurer's random capital to finite-horizon ruin probabilities. At issue the insurer holds initial surplus u. Premiums and claims make its later surplus stochastic. A positive exponential transformation of the surplus can become a supermartingale under an appropriate model of premium income, independent claims and an adjustment coefficient. Optional stopping then bounds the probability of negative capital when the contract stops at ruin or at a finite horizon. Promislow develops this connection between probability theory and ruin models in Chapters 18 and 23. This mission states finite probability and stopped-increment hypotheses explicitly. The book is S. David Promislow, Fundamentals of Actuarial Mathematics, Third Edition (2015), chapters 18 and 23. The independently published supporting research reference is available here.

Setting

A finite scenario space has nonnegative probability weights p indexed by Fin m and total probability mass one. Net cashflow G(k,ω) is a random realised premium less claim at policy anniversary k, in currency units. The capital process starts at u and accumulates increments up to time k. A scenario-dependent integer stopping time τ is assumed bounded by N. Genuine adaptedness relative to a filtration is mathematically separate and must be checked before asserting that a particular random τ is an admissible stopping time. The stopped process at time k is X(min(k,τ),ω). The exponential transform is exp(-R U(k,ω)), with positive adjustment coefficient R measured in reciprocal currency units. Ruin occurs at strict negative surplus, rather than merely touching zero.

The central actuarial model can be written

$$U_k(\omega)=u+\sum_{j<k}G_j(\omega),\quad M_k(\omega)=e^{-R U_k(\omega)},\quad X^{\tau}_k=X_{\min(k,\tau)}.$$

Formalization targets

Finite probability martingales and bounded stopping

The finite probability block defines an actual weighted expectation, a stopped random process, and the expected increments after stopping. Linearity and positivity of expectation are proved over the concrete scenario distribution. A bounded optional stopping theorem follows from summing the stopped increments when each such increment has zero expected value. The supermartingale inequality follows under nonpositive expected stopped increments. Such restrictions are useful explicit finite conditional consequences of genuine martingale models, while their derivation from a more general filtration is a separate mathematical task. The theorem types therefore avoid assuming the desired optional stopping conclusion outright.

Actuarial surplus and exponential supermartingale

The surplus and exponential block defines insurer capital as initial funds plus realised net increments. The surplus recursion is verified path by path. Exponential functions convert additive capital changes into multiplicative factors, and under positive adjustment coefficient the transform decreases as capital increases. The intended later dependence on the claim distribution enters through expected exponential increments. The model does not assert that any arbitrary premium-minus-claim process has the required supermartingale property. This prevents a false blanket application of the Lundberg bound and distinguishes positive initial capital from a possibly negative terminal surplus.

Ruin events and finite-horizon Lundberg bound

The ruin block introduces an actual event probability, monotonicity of ruin with respect to horizon and capital, and the deficit conditional on negative terminal funds. At a ruined path, exp(-R U)>1 when R>0, so the ruined-path indicator can be bounded by the exponential transform. The nonpositive stopped-increment hypothesis bounds its expectation by the initial exponential reserve. These two independent mathematical steps combine in a finite-horizon exponential bound for genuine ruin events. The initial condition, finite sample weights, and bounded stopping time are all explicit in the capstone.

Capstone theorem

The proposed root is ActuarialValuation.ruBoundedStoppingRuin_fundamental. Its intended actuarial mathematical relationship is illustrated by

$$\mathbb E[M_{\tau\wedge N}]\le e^{-Ru},\qquad \Pr(U_{\tau\wedge N}<0)\le e^{-Ru}.$$

This is a substantive nontrivial model commitment that excludes degenerate substitutes. This formula is stated only under the hypotheses and timing conventions of the actual Lean target. Subordinate theorem declarations provide the named formal prerequisites in the local source inventory. Each supporting milestone requires its own genuine proof rather than a textual assertion that an identity is obvious.

Significance

The finite-horizon result is a reusable first formalisation of the reasoning behind adjustment-coefficient solvency bounds. It aligns actuarial capital and stochastic stopping mathematics while making model assumptions auditable. MIT OpenCourseWare's optional stopping notes provide an independent probability reference, and classical actuarial risk theory treats analogous exponential surplus transformations. An ultimate infinite-horizon ruin probability needs additional convergence and stopping-time controls, and the finite bound alone does not establish a limiting probability statement.

Difficulty

The key condition is mathematical rather than syntactic: an arbitrary stopped process need not preserve mean and an exponential of an arbitrary reserve need not be a supermartingale. The finite expected-increment constraints are stated as proof hypotheses; linking them to a filtration and an actuarial claim model is future work. All sums require valid nonnegative weights, and the total weight must equal one to interpret expectations. The proof must use strict negative surplus, R positive, and explicit boundedness of τ. Passing remote declaration elaboration with sorry proves no stochastic result.

Formalization scope

The graph includes weighted expectations, stopped processes, a finite optional stopping identity, a discrete actuarial surplus process, exponential transforms, ruin event and deficit definitions, and an exponential upper-bound capstone. Full optional stopping for a measurable filtration, adjusted compound Poisson reserves, deficit-at-ruin distributions and ultimate ruin probabilities remain extensions. The capstone is finite-horizon by construction and carries the assumptions needed to justify it. Detailed dependency graph, exact Lean target types and independent finite probability checks are maintained as distinct artefacts. The staged inventory comprises 13 definitions and 38 open theorem targets. It uses the pinned Mathlib revision and a guarded remote private compiler. The proposed definitions also provide reusable results for future actuarial missions and downstream applications. The planned graph is recorded independently of theorem proof acceptance. The mathematical identities are already established in published actuarial or probability literature; the proposed Lean results remain new unproved formal targets. Every target remains open until an accepted proof is verified, and no owner item is to be confirmed or submitted for moderator review without human assessment.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Third Edition, John Wiley & Sons, chapters 18 and 23. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
• Scott Sheffield (2014), Martingales and the Optional Stopping Time Theorem, Massachusetts Institute of Technology OpenCourseWare. https://ocw.mit.edu/courses/18-440-probability-and-random-variables-spring-2014/resources/mit18_440s14_lecture35/