Motivation

Discrete arbitrage-free valuation makes insurance and pension investment guarantees amenable to exact replication arguments. A contingent payment can be financed by trading in the underlying risky asset and a risk-free bank account when the market contains a complete two-state one-period set of securities. The corresponding values can be calculated through risk-neutral expectations. This mission develops the explicit share and cash positions and verifies that one strategy replicates both possible obligations. It extends these identities to a two-period option tree and immediate-exercise decisions while keeping market completeness and the appropriate no-arbitrage assumptions visible. The book is S. David Promislow, Fundamentals of Actuarial Mathematics, Third Edition (2015), chapters 20.1–20.11. The independently published supporting research reference is available here.

Setting

At time zero, the stock price is s>0. At time one it becomes either su or sd, where u and d are gross stock-return factors. A bank account grows by the strictly positive factor R. A viable two-state frictionless market with strict full-support risk-neutral probabilities requires d<R<u. A European claim pays xu in the up state and xd in the down state, with currency units consistent across both states. The hedge holds Δ shares and a cash bank deposit b from time zero until expiration without any intermediate external cash injection. Replication means both terminal payoffs coincide in the same two-state market. For the multiperiod extension, individual tree nodes have their own exercise and continuation values; immediate exercise is available only at eligible American nodes.

The central actuarial model can be written

$$q=\frac{R-d}{u-d},\quad \Delta=\frac{x_u-x_d}{s(u-d)},\quad b=\frac{u x_d-d x_u}{R(u-d)}.$$

Formalization targets

One-period market no-arbitrage and risk-neutral probability

First construct the unique risk-neutral probability and its complementary down-state weight using the bank return and the two possible stock returns. Establish strict bounds zero less than q less than one when the bank return lies strictly between the stock outcomes. Risk-neutral valuation is linear in the payoff and positive on nonnegative claims. The discounted expected stock price equals today's stock price, which is the defining one-step martingale restriction. The boundary cases q=0 or q=1 are algebraically valid but no longer correspond to a full-support equivalent martingale measure.

Explicit self-financing hedge and European option replication

Next construct the actual hedge shares and bank investment. The same positions must deliver the specified payoff in both states, with s, R and u-d explicitly nonzero. The cost of replication then agrees with risk-neutral discounted expected payoff. Theorems handle deterministic payments, zero risky exposure, linearity and one-step put-call parity for a common strike and expiry. The stock/call/put payoff relation is pathwise, including the stock-price-equals-strike boundary; it therefore does not rely on an assumed lognormal distribution or on any incomplete market theorem.

Two-period binomial recursion and American option exercise

Finally the two-step binomial model calculates the expectation over all four ordered movement paths, preserving separate path-dependent middle cashflows if specified. Backward induction discounts from terminal nodes to time one, then discounts again to issue. An American contract replaces European continuation with the maximum of immediate exercise and expected continuation. The graph includes the fundamental domination of a corresponding European price by an American price when gross bank return is positive and risk-neutral probabilities are valid. Statewise replication at each node is the building block for multistage self-financing hedges.

Capstone theorem

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

$$\Delta su+bR=x_u,\quad \Delta sd+bR=x_d,\quad \Delta s+b=\frac{q x_u+(1-q)x_d}{R}.$$

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 explicit two-asset hedge is useful for formalising investment-linked policy guarantees, embedded options, financial market valuations and replicated hedging of insurer liabilities. The original binomial option framework is published by Cox, Ross and Rubinstein (1979). A separate published Lean 4 formalisation of the broad Fundamental Theorem of Asset Pricing exists: Raphael Coelho (2026), https://arxiv.org/abs/2606.28990. This mission's incremental scope is the explicit binomial hedge, two-period recursion and American exercise boundary rather than a claim to newly establish all finite-market arbitrage theory.

Difficulty

Replication needs a nonsingular two-state payoff matrix and a positive bank numeraire. Different payoff dates cannot be mixed in a single price equation without discounting. Recombining trees can be represented by ordered movement paths without forcing equal middle payoffs for a path-dependent option. American early exercise requires a node-specific immediate payoff and comparison with the discounted continuation; using terminal exercise value prematurely changes the contract. All independent proofs must retain the strict no-arbitrage hypothesis and the role of risk-neutral probabilities. The capstone is a constructive theorem about a particular self-financing portfolio, with actual terminal state equations.

Formalization scope

The proposed definitions cover risk-neutral weights, expected payoff, discounted price, share-and-bank hedge, European call and put payoffs, a two-period tree and an American exercise operator. The intended capstone proves existence of the exact replication holdings and equality of hedging cost and risk-neutral valuation. Further research could add a complete finite filtration, dynamic hedging rebalancing, conditional risk-neutral measures and general finite-market completeness, reusing rather than duplicating existing formal work. Every proof target remains open until an authoritative remote compiler accepts an actual Lean proof. The staged inventory comprises 16 definitions and 36 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 20.1–20.11. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
• John C. Cox, Stephen A. Ross and Mark Rubinstein (1979), Option Pricing: A Simplified Approach, Journal of Financial Economics 7, 229–263. https://doi.org/10.1016/0304-405X(79)90015-1

Motivation

The deterministic claims-development model estimates future claim amounts but does not quantify reserve uncertainty. Thomas Mack's distribution-free standard error framework in ASTIN Bulletin (1993) introduces conditional moments, volume-weighted development, process variability and factor estimation uncertainty. The process uncertainty of future claims and parameter uncertainty from fitted factors must be distinguished. This mission supplies original finite Lean identities corresponding to those actuarial building blocks, without claiming a proof of Mack's full reserve mean-square-error theorem.

The published source supplies the publicly verifiable actuarial context. Original finite Lean formalisation of the corresponding identities remains an open mathematical task; existing actuarial theory is not by itself an accepted formal proof. The input conventions and hypotheses should be compared to the source by an independent human reviewer.

Setting

A finite observed paid-claims triangle has common pairs of cumulative claims C(i,j) and C(i,j+1) for origin cohorts i below m. The Mack link factor is f_j=sum C(i,j+1)/sum C(i,j). A predicted next-age amount is C*f_j, and paid-to-ultimate reserve equals predicted amount minus current paid claims. Weighted squared residuals are deviations squared divided by strictly positive cumulative claims. An estimated sigma-squared divides aggregate weighted squared residual by positive degrees of freedom. Under a stated one-step variance model, process variability takes sigma-squared times current claims and estimation variability takes sigma-squared times squared current claims divided by observed development exposure.

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.

Development factors and volume-weighted exposure

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

$$\widehat C(C+D)=\widehat C(C)+\widehat C(D)$$

One common factor distributes over aggregated claims.

Residual dispersion and one-step uncertainty

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

$$V=0\Rightarrow\hat\sigma^2=0$$

No residual variation means zero estimated variance.

Process error, estimation error and reserve variance

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

$$fD=N,\;v_p,v_e,MSE\ge0,\;C+R=U$$

The capstone combines observed factor calibration, separate nonnegative process and estimation variance terms, and claims reserve reconciliation.

Capstone theorem

The main target is `ActuarialValuation.mackReserveVariance_fundamental`. The capstone combines observed factor calibration, separate nonnegative process and estimation variance terms, and claims reserve reconciliation.

$$fD=N,\;v_p,v_e,MSE\ge0,\;C+R=U$$

Significance

Mack (1993) derives the full distribution-free standard error of chain-ladder reserve estimates from conditional development assumptions. The finite results here are algebraic audit invariants, intended to be reused in a later proof of those conditional-moment claims. The capstone checks that process and factor-estimation error terms are individually nonnegative and reconcile with the selected development factor and reserve. These results support future uncertainty decomposition, diagnostics and coherent reserve modelling.

Difficulty

A Mack residual statistic is not a conditional random variable until a stochastic development model is explicitly established. The factor's denominator must include exactly the cohorts for which the next development observation exists. Strictly positive observed claim amounts are essential for scaled residuals. The process variance and estimated factor variance terms are distinct and must be justified by separate modelling assumptions for a full stochastic theorem. The chosen positive degrees of freedom is an input to the algebraic dispersion estimator; a specific m-minus-one estimator requires enough observed cohorts. The staged capstone does not silently assert unbiasedness or independence.

The original Mack distribution-free method distinguishes model process noise from sampling or parameter estimation uncertainty. The original 1993 paper includes conditional assumptions and a reserve mean-square error derivation; these staged identities prove only algebraic invariants before constructing that complete stochastic theory. For a published actuarial result to be claimed as proved in Lean, corresponding random variables, sigma algebras, conditional expectations and associated independence or uncorrelatedness conditions would all need authoritative formal statements and proofs. This package makes no such claim, and sample residual calculations or a successfully elaborated open theorem do not amount to a stochastic proof.

Formalization scope

All staged theorem targets are finite deterministic real-algebraic components motivated by Mack's published reserving model. They do not constitute the full distribution-free stochastic proof, a confidence interval, a tail extrapolation or a quantile estimation result. The Lean source specifies nonzero denominators, finite index sets and valuation units precisely. The nontrivial root assembles calibration, two distinct variance charges and reserve valuation without collapsing either variance term into a tautological special case.

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

• Thomas Mack, Distribution-free Calculation of the Standard Error of Chain Ladder Reserve Estimates (1993), ASTIN Bulletin 23(2), pp. 213–225. https://www.casact.org/sites/default/files/database/astin_vol23no2_213.pdf
• Thomas Mack, The Standard Error of Chain Ladder Reserve Estimates: Recursive Calculation and Inclusion of a Tail Factor (1999), ASTIN Bulletin 29(2), pp. 361–366. https://www.casact.org/sites/default/files/database/astin_vol29no2_361.pdf

Motivation

Stochastic survival distributions provide the probability-theoretic foundation for mortality-based insurance and pension valuation. They describe the actual random duration until failure, its probability distribution and the conditional risk faced by someone still alive at a particular time. Promislow (2015), especially Chapter 14, presents discrete and continuous lifetime distributions, survival functions and hazard rates, building on the continuous mortality material in Chapter 8 and probability foundations in Appendix A.

The established mathematical ideas are available in published literature, and Mathlib has general measure-theoretic infrastructure for probability measures. This mission proposes a bridge between that genuine probability structure and concrete actuarial lifetime calculations. Earlier actuarial work contains life-table and parametric mortality results, but this mission separately constructs a measurable lifetime event model. Every new theorem remains an open Lean target until an authoritative proof is accepted.

Setting

Let Ω be the underlying outcome space with a measurable structure, μ a probability measure on that space, and T : Ω → ℝ a measurable lifetime random variable. For a threshold t, define the failure CDF by the probability of T ≤ t and survival by the probability of T > t. This strict-versus-nonstrict distinction is essential when the lifetime law has atoms:

$$F_T(t)=\mathbb P(T\le t),\quad S_T(t)=\mathbb P(T>t),\quad F_T(t)+S_T(t)=1.$$

Both quantities are represented by extended nonnegative-real measures. For an economic lifetime model, additional hypotheses specify nonnegative durations and probability normalisation. A lifetime with an atom at issue need not satisfy S_T(0)=1. A lifetime that is only almost surely nonnegative is mathematically sufficient for many distributional identities, although some finite initial targets state stronger pointwise assumptions.

For positive integer k, the discrete failure mass is p_k=P(T=k). The discrete hazard is conditional on surviving beyond k-1:

$$h_k=\frac{\mathbb P(T=k)}{\mathbb P(T>k-1)}.$$

This ratio is defined operationally only if the at-risk denominator is strictly positive. The underlying Lean division remains total, so the cancellation theorem must explicitly exclude zero and infinite denominators.

Formalization targets

Measurable lifetime distributions and conditional survival

The first supporting group formalises survival and CDF monotonicity, event partition, survival before time zero, failure atoms, conditional ratios and residual lifetimes. The residual lifetime after time s is represented by the shifted random variable T-s, while the conditional law of that random variable given T>s is represented separately by a survival ratio. This distinction prevents silently treating an unconditional time shift as conditional survival.

The conditional identity to establish, for a positive survival denominator, is

$$\mathbb P(T>s+t\mid T>s) =\frac{S_T(s+t)}{S_T(s)}.$$

It applies for nonnegative additional duration t when the numerator event is contained in the conditioning event. The algebraic quotient may also be defined at other real inputs, but its interpretation as a conditional probability requires these event conditions.

Discrete failure masses and finite life expectancy

A finite probability mass model on durations zero through n supplies explicit sums for expected lifetime and discrete strict-tail survival. The intended tail-sum identity is

$$\sum_{k=0}^{n} k p_k =\sum_{j=0}^{n-1}\sum_{k=j+1}^{n}p_k.$$

This finite identity holds without convergence issues. Probability normalisation and nonnegative mass are additional hypotheses required when interpreting the identity as a lifetime expectation. Discrete term-insurance valuation also appears as a death-year-weighted sum, with death in year k paid at the end of that year. These finite constructions give checkable links from distributional quantities to insurance cashflows.

Exponential, Gompertz and Makeham hazards and insurance valuation

An exponential lifetime with constant hazard λ has model survival exp(-λt)) and cumulative hazard λt. A **Gompertz** model uses hazard b exp(ct), and a **Makeham** model adds an age-independent force a. Their cumulative hazard formulae are valid under their stated parameter conditions. In particular, the standard integrated Gompertz expression divides by c; when c=0`, its expression must be treated separately as the constant-hazard limit rather than used through division by zero.

General survival and cumulative hazard satisfy, for appropriately regular and nonnegative force of mortality,

$$S_T(t)=\exp\!\left(-\int_0^t h(u)\,du\right).$$

This mission stages finite parametric hazard identities and a genuine insurance present-value expectation, rather than claiming the full general theorem without the necessary absolute continuity and integrability formalisation. The expectation of a unit claim payable at the realised lifetime under interest force δ is represented as

$$\mathbb E[\exp(-\delta T)] =\int_\Omega\;\exp(-\delta T(\omega))\,d\mu(\omega).$$

The zero-interest and deterministic-lifetime special cases are explicitly targeted.

Capstone theorem

ActuarialValuation.svSurvivalHazardInsurance_fundamental connects the event-defined CDF of a measurable lifetime with a stipulated exponential survivor law, the corresponding cumulative hazard representation and the genuine measure-integral expected discounted insurance value at zero force of interest. The model-law hypothesis is explicit. The theorem therefore retains stochastic semantics while providing a solvable initial path to a broader general hazard calculus.

Significance

Actuarial tables, conditional survivor calculations and life insurance prices can be checked against a consistent random-lifetime model instead of relying solely on formal algebra involving survival symbols. Mathlib's probability-measure library provides a verified environment for event probabilities, with related integration foundations available for subsequent extensions. This builds a reusable formal bridge to mortality projection, multiple-decrement valuation, insurance-loss distributions and the pricing mission LXIV.

Difficulty

The distinction between strict survival and nonstrict failure probability governs boundary atoms. Conditional hazard ratios are meaningful only when the at-risk population has nonzero measure. Continuity, absolute continuity, differentiability and density-based hazard formulae are genuinely additional hypotheses; their absence cannot be repaired by simply assuming exponential survival. General integrated hazard reconstruction will require a later properly regularised theorem. The integral at a nonzero discount rate also needs integration and sign assumptions to justify pricing.

An event-defined random variable has materially different proof obligations from a deterministic model formula. The graph includes nontrivial probability event partitions, monotonicity and conditional mass inequalities, a finite tail-sum expectation identity and a measure-integral valuation. The open declarations are not accepted results.

Formalization scope

The staged inventory contains 17 reusable definitions, 36 open theorem targets and 35 supporting milestone specifications. Its finite and continuous-like model families are carefully separated. The capstone is intentionally conditional on a named exponential survival hypothesis and has an actual measure-theoretic loss valuation. Discrete failure times, finite support, residual-life shift, cumulative hazard and time-zero present values are included as individual targets.

Excluded future extensions include general Radon-Nikodym hazard construction, an absolute-continuity theorem for arbitrary lifetime distributions, differentiability of log survival, almost-everywhere equality of densities and insurance PV identities at arbitrary interest forces. These are genuine mathematical next steps, not already established by the initial capstone. Private declaration compilation and any numerical sampling evidence remain separate from accepted proof status.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Third Edition, Wiley, Chapters 8 and 14 and Appendix A. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
• Lean community (2026), Mathlib MeasureTheory: Probability Measure Classes, mathematical formalisation documentation. https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/Typeclasses/Probability.html

Motivation

Fractional-duration life contingencies arise when contractual cashflows are paid more frequently than annually and when valuations occur between policy anniversaries. The frequency of annuity payments, the timing of a death benefit and the assumption used to interpolate survival between integral ages each affect the expected present value. S. David Promislow's Fundamentals of Actuarial Mathematics, third edition (2015), particularly Chapter 7, develops these relationships alongside its treatment of life annuities (Chapter 4) and continuous payments (Chapter 8). This mission constructs independent, explicitly timed Lean 4 definitions and original theorem targets that can be reused in later insurance, pension and reserve formalisation.

The foundational mathematics is already established in the actuarial literature. Its corresponding Lean declarations in this mission are open proof targets. The existing Prove2Me actuarial collection already contains annual annuities, life-table identities and constant-force mortality examples, but these do not by themselves establish the new m-thly cashflow and within-year reserve results. Relevant published material includes Promislow (2015) and Society of Actuaries actuarial work on uniform mortality interpolation.

Setting

Time is measured in years after issue. Policy year k is a natural number, payment frequency m is a positive number of instalments per year, and j ranges from zero through m-1. A benefit amount c(k) has currency units per year. A normalised annual payment stream has cash amount c(k)/m at each instalment. Discount D(t) and unconditional survival p(k) are dimensionless. Annual mortality q(k) belongs to the interval from zero to one when interpreted as a valid probability.

An annuity-due payment in subperiod j occurs at k+j/m; an annuity-immediate payment occurs at k+(j+1)/m. The final immediate instalment therefore requires survival to the following policy anniversary. In each policy year, uniform distribution of deaths (UDD) specifies

$$S_{\mathrm{UDD}}(s\mid k)=1-s q(k),\qquad 0\le s\le 1,$$

whereas constant force of mortality specifies

$$S_{\mathrm{CF}}(s)=\exp(-\mu s).$$

The exponential model assumes a constant force mu over the relevant duration; it is not silently identified with UDD. Constant force of interest delta yields D(t)=exp(-delta*t), but the finite annuity definitions also permit an arbitrary discount function with explicit nonnegativity hypotheses when required.

Formalization targets

Within-year survival and discount timing

Construct separate linear and exponential survival models, conditional UDD survival after fraction s, a constant-interest discount factor and the exact indexed instalment time. Establish the zero-duration and full-year boundaries, positivity and monotonicity under justified probability assumptions, conditional-survival multiplication, exponential multiplicativity, and a discount-factor splitting identity. The conditional UDD formula divides by survival at s; a zero-survival endpoint requires an explicit exclusion.

The within-year decomposition is

$$S_{\mathrm{UDD}}(s+t\mid k) = S_{\mathrm{UDD}}(s\mid k)-tq(k),$$

and the conditional expression divides the left-hand side by S_UDD(s|k) when this is positive.

Frequency-dependent annuity cashflow valuation

Define a finite n-year annuity-due as the discounted weighted double sum

$$V^{(m)}_{\mathrm{due}} =\sum_{k=0}^{n-1}\sum_{j=0}^{m-1} \frac{c(k)}{m}D\!\left(k+\frac{j}{m}\right) p(k)\left(1-\frac{j}{m}q(k)\right).$$

Define immediate valuation by changing both the payment time and within-year survival exposure to (j+1)/m. These definitions specify exact UDD actuarial values under the stated unconditional annual survivor weights, rather than using an approximation to annual payments. Establish zero-year and zero-benefit boundaries, linearity, scaling, positivity, and the reduction to annual due valuation for m=1.

For the annual immediate reduction, require the annual survival recurrence p(k+1)=p(k)(1-q(k)). This is necessary because an immediate payment at the annual boundary is conditioned on survival through the full policy year. The case m=0 is retained as an empty finite-sum identity solely to check mathematical totality; it is excluded from economic payment-frequency interpretation.

Fractional premiums and policy reserves

The equivalence principle premium rate is the expected discounted benefits divided by the present value of a unit-premium annuity. The associated balance is

$$\pi A=B,\qquad \pi=\frac{B}{A},\qquad A\ne0.$$

Here A is a dimensionless instalment-weighted annuity value, B is in currency and pi is currency per year of nominal premium rate. The denominator is required to be nonzero for the funding identity, and positive if the quantity is interpreted as an economically valid payment stream.

For a death benefit payable at the end of the policy year, a retrospective fractional survivor reserve, measured at s after that year's premium has been received, satisfies the conditional balance

$$V_s (1-sq)+sq\,b\,D_{s,1} =(V_0+\pi)G_{0,s},$$

where G_{0,s} is accumulation from the anniversary to s, and D_{s,1} discounts an end-year death payment back to s. The reserve is conditioned on survival to s; require 1-sq\ne0. Prove the opening, zero-mortality, end-year and zero-death-benefit boundary identities. These statements do not assert that all deaths occur at an anniversary.

Capstone theorem

ActuarialValuation.frFractionalValuation_fundamental connects annual reduction for a single due instalment, equivalence-premium funding, exact conditional within-year reserve reconciliation, and positivity of finite-time constant-force survival. The theorem keeps the two mortality assumptions in separate propositions.

Significance

As described in Promislow (2015), fractional valuation provides a common time axis. The graph establishes a common, formally stated time axis for fractional pension and life-insurance cashflows. It distinguishes the recipient's conditional survival at payment from the insurer's future death-benefit payment obligation. The finite indexed formulation supports later derivation of m-thly life-contingent premium conversion, changes in reserving basis and comparison with continuous annuity integrals. The theorem graph can also be composed with existing annual actuarial-valuation work once published theorem identities and exact dependencies have been independently verified.

Difficulty

The main sources of mathematical risk are year-end payment conventions, the survival status of an annuitant exactly at an instalment boundary, the difference between UDD and constant force, and division by the probability of being alive at the valuation duration. The initial model is finite and avoids an unjustified assertion that every m-thly sum converges to a continuous value. Such limiting claims require a further integrability and regularity layer and are reserved for an explicitly justified extension.

The graph includes actual mathematical content beyond zero and cancellation identities: conditional-survival reconciliation, exact change of payment frequency, additivity of survival-discounted cashflows and survivor-weighted reserve funding. The numerical checks and remote declaration checks should be reviewed independently. A successfully elaborated sorry declaration remains unproved.

Formalization scope

There are 15 proposed definitions, 38 open theorem targets and 37 subordinate milestone descriptions. The mathematical objects include finite event-weighted cashflow sums, an explicit discount factor, UDD and constant-force survival, and retrospective fractional-duration reserves. The item specifications are the authoritative proposed Lean propositions. Hypotheses on q, s, m, the annual survivor recursion and the premium annuity denominator are present only where required for a proposition.

The mission does not yet include Woolhouse asymptotic expansions, rigorous m\to\infty convergence, a general interest-rate term structure or non-UDD reserve interpolation. Those are identifiable continuation targets rather than presumed established results. No owner item is to be confirmed and no proposal submitted for moderation without human source and mathematical review.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Third Edition, John Wiley & Sons, Chapters 4, 7 and 8. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
• Society of Actuaries (2018), Life & Annuity Symposium, session 033, UDD interpolation and exposure conventions. https://www.soa.org/498941/globalassets/assets/files/e-business/pd/events/2018/las/pd-2018-05-las-session-033.pdf

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Finite random present values of insurance benefits and premium streams

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

The key pathwise accounting identity is

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

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

Equivalence premiums and loss variance

Define finite expectation and second raw moment by

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

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

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

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

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

Actual loss distribution and percentile premium adequacy

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

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

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

Premium adequacy at annual rate P is

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

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

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

Capstone theorem

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

Significance

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

Motivation

Actuaries graduate crude observed mortality rates to remove sampling noise while retaining meaningful age-related mortality structure. Whittaker-Henderson graduation expresses the trade-off between goodness of fit to exposure-weighted crude experience and smoothness of the fitted series through successive finite differences. A 1968 Casualty Actuarial Society account of graduation describes the fit-plus-smoothness criterion. These public actuarial ideas motivate new Lean finite identities for mortality curves, rather than a claim to reprove the original general constrained optimisation theory.

The published source supplies the publicly verifiable actuarial context. Original finite Lean formalisation of the corresponding identities remains an open mathematical task; existing actuarial theory is not by itself an accepted formal proof. The input conventions and hypotheses should be compared to the source by an independent human reviewer.

Setting

At ages i the crude empirical rate q(i), graduated rate g(i) and nonnegative reliability weight w(i) define weighted squared error F=sum w(i)(g(i)-q(i))². Adjacent differences are Delta g(i)=g(i+1)-g(i); second differences are Delta²g(i)=g(i+2)-2g(i+1)+g(i). The first and second order roughness measures are finite sums of squared differences. A nonnegative chosen smoothing coefficient lambda yields a composite objective F+lambda S. Uniformly shifting graduated rate levels leaves first and second differences unchanged, though its fit to unchanged crude rates changes.

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.

Observed crude rates and exposure-weighted fitting

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

$$g_i=q_i\Rightarrow F=0$$

No data fidelity loss arises when graduated values exactly equal crude rates.

First and second finite difference smoothness

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

Representative theorem `ActuarialValuation.whSecondDifference_linear`:

$$\Delta^2(a+bi)=0$$

An affine age trend has exactly zero second finite difference.

Composite graduation objective and invariance

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

$$F\ge0,\;S_2\ge0,\;F+\lambda S_2\ge0,\;S_2(g+c)=S_2(g)$$

The capstone proves a nonnegative exposure-weighted mortality graduation criterion and exact curvature shift invariance under explicit weighting assumptions.

Capstone theorem

The main target is `ActuarialValuation.whMortalityGraduation_fundamental`. The capstone proves a nonnegative exposure-weighted mortality graduation criterion and exact curvature shift invariance under explicit weighting assumptions.

$$F\ge0,\;S_2\ge0,\;F+\lambda S_2\ge0,\;S_2(g+c)=S_2(g)$$

Significance

The Casualty Actuarial Society graduation discussion describes a formal balance between smoothness and fidelity. The staged theorem chain provides reusable mortality graduation quality-control identities: exact finite-difference stencils, nonnegative penalised objective, zero second-difference penalty for affine curves and invariance of smoothing to a uniform level shift. These underlie future actuarial model verification and penalised optimisation work.

Difficulty

The two finite difference orders are not interchangeable. A first difference of an affine age pattern is constant but is not necessarily zero; a second difference of that same pattern vanishes. The fit statistic must account for exposure or credibility weights that cannot be negative when nonnegative loss is asserted. Penalty invariance under adding a constant does not imply that the whole fit-plus-smoothing objective is invariant, because observed crude rates are held fixed. An unconstrained fitted mortality curve may fall outside the unit interval, so future operational graduation must constrain rates appropriately. This mission has no unproved claim of existence or uniqueness of an optimal graduated curve.

The smoothness weight controls the model's balance between observed experience and regularity, and its selection is not proved optimal by the finite arithmetic identities here. An affine age curve has zero second difference but can have a positive first-difference roughness sum. Shifting all estimated rates changes residual fit against unchanged crude rates even as it leaves smoothness unchanged. A realistic actuarial graduation may need constraints on graduated rates, tail-age behaviour and end-condition conventions; these need separate explicit mathematical and administrative specifications. The open theorem set makes these distinctions visible.

Formalization scope

Lean formalisation uses finite deterministic age-indexed functions, nonnegative observation weights, squared error and one- or two-step finite differences. The main theorem is the conjunction of exact penalty properties, not a statistical estimator bias theorem or an optimisation convergence theorem. It leaves endpoint boundary conditions and monotonicity constraints for later missions. A genuinely nontrivial result is the simultaneous control of weighted fit and roughness plus invariance of curvature to mortality-level translation.

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

• Casualty Actuarial Society, Proceedings of the Casualty Actuarial Society, Volume LV (1968), graduation discussion, https://www.casact.org/sites/default/files/database/proceed_proceed68_1968.pdf
• Nels M. Valerius, Notes on Whittaker-Henderson Formula A (1967), Proceedings of the Casualty Actuarial Society LIV, pp. 218–230. https://www.casact.org/sites/default/files/database/proceed_proceed67_67218.pdf

Motivation

Insurance solvency capital requires aggregating standalone module risk charges while acknowledging diversification. The EU Solvency II Directive Article 104 and Annex IV prescribe a correlation aggregation formula; the UK Prudential Regulation Authority's standard formula annexes likewise contain explicit correlation matrices. This mission formalises original exact finite-risk mathematical identities behind the quadratic calculation rather than attempting to certify a particular insurer's regulatory solvency position.

The published source supplies the publicly verifiable actuarial context. Original finite Lean formalisation of the corresponding identities remains an open mathematical task; existing actuarial theory is not by itself an accepted formal proof. The input conventions and hypotheses should be compared to the source by an independent human reviewer.

Setting

For insurance risk modules i and j, standalone charges are nonnegative real capital amounts C_i and correlation coefficients rho_ij. The squared correlation-based aggregation is Q=sum over ordered i,j of rho_ij C_i C_j. For exactly two risks and symmetric common pairwise rho, the calculation reduces to C_1 squared plus C_2 squared plus twice rho C_1 C_2. Squared capital before diversification is (C_1+C_2)^2. The difference equals 2(1-rho)C_1 C_2, which is nonnegative when rho is at most one and both standalone charges are nonnegative.

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.

Two-module capital charges and correlation cross terms

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

$$C_1^2+C_2^2\ge0$$

Zero-correlation squared risk capital is nonnegative.

Diversification gains and pairwise correlation bounds

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

$$Q(C_1+0,C_2)=Q(C_1,C_2)$$

A zero change in module capital leaves aggregate squared risk unchanged.

Finite-dimensional standard formula quadratic aggregation

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

$$Q_\rho\ge0,\;D^2\ge0,\;Q_\rho+D^2=(C_1+C_2)^2$$

The capstone proves nonnegative two-module correlation aggregation, exact squared diversification reconciliation and the full-correlation limit.

Capstone theorem

The main target is `ActuarialValuation.scrSolvencyDiversification_fundamental`. The capstone proves nonnegative two-module correlation aggregation, exact squared diversification reconciliation and the full-correlation limit.

$$Q_\rho\ge0,\;D^2\ge0,\;Q_\rho+D^2=(C_1+C_2)^2$$

Significance

The Solvency II legislative Annex IV gives a source-defined matrix arrangement for module capital aggregation. Exact factor-of-two handling of off-diagonal cross terms is a crucial capital calculation audit. The capstone proves the squared two-risk diversification identity, boundedness under nonnegative coefficients and the perfect positive correlation limit. These results are reusable for portfolio risk controls and independent testing of actuarial capital spreadsheets.

Difficulty

A symmetric numerical matrix of pairwise values in [-1,1] is not automatically positive semidefinite. Nonnegative quadratic aggregation of arbitrary signed real vectors requires matrix PSD or a suitable structural hypothesis; the finite portfolio theorem instead explicitly restricts all charges and coefficients to be nonnegative. For two positive risk charges, rho must not exceed one for the usual diversification inequality, and it is only the squared capital that is compared. Cross terms are counted for both ordered pairs. The regulatory total may include operational risk, intangible risk, tax-loss absorption and other adjustments beyond basic quadratic capital, so their signs cannot be invented.

The correlation matrix in a published regulatory formula must be distinguished from an arbitrary symmetric matrix. Two at-most-unit correlated modules with nonnegative standalone risk values enjoy the displayed squared diversification relation; negative or inconsistent correlation matrices can invalidate unsupplemented general positivity assumptions. In actual Solvency II reporting, the calculation depends on rule jurisdiction, date, calibration and other adjustments. The theorem graph is a source-grounded mathematical component, not a regulatory determination or an audit opinion about an individual insurer.

Formalization scope

The Lean formalisation is finite real algebra for risk charges and selected correlation weights, with a two-module squared capital capstone. It does not assert unconditional positivity for a non-PSD arbitrary coefficient matrix or identify the square root with regulatory capital without establishing nonnegative Q. Published correlation matrices and applicable UK or EU dates must be checked independently when the formula is deployed operationally. The theorem statements concern a nontrivial parametric diversification identity, not a preselected numerical example.

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

• European Parliament and Council, Directive 2009/138/EC on the Taking-up and Pursuit of the Business of Insurance and Reinsurance (2009), Article 104 and Annex IV. https://eur-lex.europa.eu/legal-content/EN/TXT/?uri=CELEX:32009L0138
• Bank of England, Prudential Regulation Authority, Standard Formula Annexes (2024), Annex IV, pp. 3–5. https://www.bankofengland.co.uk/-/media/boe/files/prudential-regulation/policy-statement/2024/november/ps1524app7.pdf

Motivation

Lee-Carter mortality projection is a standard demographic approach for age-specific death rates. The original paper by Ronald Lee and Lawrence Carter represents mortality's logarithm by age effects and a common period index. The Social Security Administration working paper explains this decomposition and the identifiability of its components. Existing actuarial literature establishes the parametric modelling framework; these are original formal finite-period Lean identities, not claims that the statistical model has been estimated from historical data.

The published reference identifies the actuarial basis for this work. Finite source-specific formalisation in Lean remains open, while the motivating mathematical identities and technical conventions have been established in the literature. No compiler check or numerical example is an accepted proof.

Setting

At attained age x and calendar year t, the central death rate is m(x,t)=exp(a_x+b_xk_t), with a_x a real age intercept, b_x real age sensitivity and k_t a real period-mortality index. A deterministic index drift evolves k_(t+n)=k_t+ndelta. The ratio of death rates at the same age across two periods equals exp(b_x*(k_2-k_1)). With a nonnegative constant annual mortality force m, one-year survival is exp(-m) and the one-year death probability equals one minus survival. A cohort receives a possibly age- and calendar-dependent sequence of valid annual death probabilities q(t).

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.

Age-period Lee-Carter log mortality and drift

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

$$m_{x,t}=e^{a_x}\text{ if }\kappa_t=0$$

Zero index gives the exponential age baseline.

Mortality rate ratios and force-to-probability conversion

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

Representative theorem `ActuarialValuation.lcDeathProb_partition`:

$$q+p=1$$

One-year death and survival are complementary under a constant-force basis.

Projected cohort survival and one-period insured loss

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

Representative theorem `ActuarialValuation.lcLeeCarterCohort_fundamental`:

$$m_{x,2}=m_{x,1}R,\;m_{x,2}>0,\;0\le S_{n+1}\le S_n,\;E[C]\ge0$$

The comprehensive mortality capstone links Lee-Carter rate ratios with a valid bounded cohort survival law and the nonnegative one-year insured death outgo.

Capstone theorem

The main target is `ActuarialValuation.lcLeeCarterCohort_fundamental`. The comprehensive mortality capstone links Lee-Carter rate ratios with a valid bounded cohort survival law and the nonnegative one-year insured death outgo.

$$m_{x,2}=m_{x,1}R,\;m_{x,2}>0,\;0\le S_{n+1}\le S_n,\;E[C]\ge0$$

Significance

The original Lee-Carter work provides a tractable time trend at each age. The proposed mathematical capstone relates positive death-rate projections and exact age-specific rate ratios to bounded multi-year cohort survival and nonnegative expected death benefit cost. These are reusable model-validation invariants for actuarial mortality improvement projections. Unlike a fitted SVD or time-series forecast, a deterministic rate ratio and finite survival-product identity can be verified without probabilistic estimation assumptions.

Difficulty

A central death rate is not automatically an annual death probability. Converting an annual nonnegative force of mortality to a death probability is a modelling assumption that holds with constant force during the year. The one-year mortality intensities for ages x+n along a cohort differ from fixed-attained-age period ratios. The survival product must use each cohort-year probability exactly once, with half-open endpoints. Negative annual force values would yield death probabilities outside the unit interval and are ruled out where probabilities are asserted. The Lee-Carter age and period parameters have a scale identifiability ambiguity unless normalisation constraints are imposed; the current mission asserts algebraic properties at fixed parameters, not unique statistical identification.

An age-period mortality rate for the same age in two calendar years is not the same as the sequence of annual death probabilities experienced by a cohort ageing through consecutive calendar years. The first is represented as a ratio of positive central mortality intensities; the second is a product of annual survival complements. The conversion from a rate to an annual probability assumes a constant mortality force within the relevant year. That is distinct from mere exponential positivity and must be explained in review. A parameter-normalisation condition would be necessary for identification from experience data, but fixed-parameter algebraic rate-ratio statements do not require identifying the historical fit.

Formalization scope

The nontrivial root combines exact exponential rate-ratio reconstruction with independent multi-year cohort survival bounds and expected assurance claims, rather than using degenerate zero mortality or zero benefits. It does not prove statistical estimation, covariance forecasts, stochastic longevity risk, or maximum likelihood fit. The formalisation uses Lean real arithmetic, exp, finite products and model-specific definitions, preserving positivity assumptions. Future missions can reuse the established identities for age-calendar time series and annuity valuation of projected cohorts.

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

• Ronald D. Lee and Lawrence R. Carter, Modeling and Forecasting U.S. Mortality (1992), Journal of the American Statistical Association 87, pp. 659–671. https://doi.org/10.1080/01621459.1992.10475265
• U.S. Social Security Administration, The Out-of-Sample Performance of Stochastic Methods in Forecasting Age-Specific Mortality Rates (2008), Working Paper No. 111. https://www.ssa.gov/policy/docs/workingpapers/wp111.html

Motivation

Actuarial insurance ratemaking links expected claims to a measurable risk exposure base. The Actuarial Standards Board's adopted ASOP No. 53 discusses prospective risk-transfer cost estimation, exposure data and risk classification. Pure premium is cost per earned exposure and class relativity describes relative risk classification in a common basis. The already established actuarial pricing framework is conceptual; the new Lean statements are independent original finite proofs.

The published reference identifies the actuarial basis for this work. Finite source-specific formalisation in Lean remains open, while the motivating mathematical identities and technical conventions have been established in the literature. No compiler check or numerical example is an accepted proof.

Setting

A finite set of insured risk classes has real earned exposures e(i), loss costs L(i), and selected dimensionless relativity r(i). A common base pure rate b charges technical class premium e(i)br(i), summed over n disjoint classes. The relativity-weighted exposure W equals the sum of e(i)r(i). A projected aggregate claim cost T is financed by the uniquely calibrated b=T/W, provided W is strictly positive. Historical observed pure premium L/E is distinct from the future indicated base price.

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.

Exposure, observed claims and indicated pure premiums

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

$$f=0\Rightarrow c=0$$

No expected frequency leads to zero prospective claim cost.

Class relativities and aggregate technical premium

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

$$P=bW$$

The class-by-class technical premium sum factors as base rate times weighted exposure.

Base rate calibration and technical premium adequacy

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

Representative theorem `ActuarialValuation.ratExposureRatemaking_fundamental`:

$$P(b^*)=T,\;b^*\ge0,\;S(b^*)=0,\;b\ge b^*\Rightarrow S(b)\ge0$$

The substantive pricing capstone establishes unique expected-cost calibration and technical premium adequacy across arbitrary finite risk-class exposures and relativities.

Capstone theorem

The main target is `ActuarialValuation.ratExposureRatemaking_fundamental`. The substantive pricing capstone establishes unique expected-cost calibration and technical premium adequacy across arbitrary finite risk-class exposures and relativities.

$$P(b^*)=T,\;b^*\ge0,\;S(b^*)=0,\;b\ge b^*\Rightarrow S(b)\ge0$$

Significance

The ASOP No. 53 actuarial source distinguishes the estimate of future insured losses from an actual insurance selling price. This formal capstone proves a finite technical income reconciliation and a nonnegative adequacy margin at every higher base rate. These equalities form reusable verification invariants for actuarial pricing spreadsheets and downstream portfolio studies. It does not assert legally required rates, premium tax calculations, competitive prices or expense allocation.

Difficulty

Class exposures must be measured on consistent earned-exposure units. Multiplying a base rate by class relativity differs from taking an unweighted arithmetic average of class premiums. If weighted exposure vanishes, a positive target cannot be financed by the formula T/W. Positivity of weighted exposure is needed for uniqueness and increasing-rate adequacy; aggregate exposure alone may be positive even when all relativity weights are zero. A risk class's exposure may be zero without invalidating the rest of the portfolio. A zero-cost portfolio is a legitimate boundary, but an all-zero exposure scenario cannot establish the general theorem.

A pure indicated base premium in this finite model covers only the agreed future claim-cost total. It is not a retail premium including expense, profit, risk or market pricing provisions. The same class relati­vity and earned exposure basis must be applied to the projected loss cost and to the pricing denominator. An independent actuarial reviewer can identify a rate-mix error through the exact aggregate reconstruction identity. Positive aggregate unweighted exposure alone does not ensure a viable technical rate when all class multipliers vanish. The central root is therefore a financial reconciliation theorem with an explicit strictly positive relativity-weighted exposure base.

Formalization scope

The formal verification uses finite indexed class data and real-valued expected costs, independent of claim arrival distributions or stochastic credibility assumptions. The results prove exact identities over a fixed prospective insurance coverage basis. A loading for acquisition costs, handling expenses, reinsurance and capital is not automatically contained in the technical pure premium. The nontrivial root quantifies over every alternative higher rate and proves genuine fiscal sufficiency, rather than only simplifying an illustrative numeric case.

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

• Actuarial Standards Board, ASOP No. 53: Estimating Future Costs for Prospective Property/Casualty Risk Transfer and Risk Retention (2017), Section 3, https://www.actuarialstandardsboard.org/asops/estimating-future-costs-prospective-propertycasualty-risk-transfer-risk-retention/
• Casualty Actuarial Society, Basic Ratemaking presentation (2012), https://www.airc.org.tw/newsfiles/BasicRatemakingI.pdf

Motivation

Insurers price retention layers and assess high-loss capital needs using distributions of losses rather than only expected claim frequency. The Rockafellar and Uryasev paper introduces an auxiliary loss-threshold objective for conditional value-at-risk (CVaR). Its central mathematical construction uses expected positive-part loss in excess of a threshold. The existing core relationship is established in published research; this mission develops an original exact finite-scenario Lean formalisation and its necessary boundary lemmas.

The published reference identifies the actuarial basis for this work. Finite source-specific formalisation in Lean remains open, while the motivating mathematical identities and technical conventions have been established in the literature. No compiler check or numerical example is an accepted proof.

Setting

A finite lattice has loss outcomes 0 through n with nonnegative scenario weights p(k); it represents a genuine probability distribution only when their total mass equals one. The scenario-weighted excess above deductible t is SL_n(t)=sum p(k) max(k-t,0), which is an expected excess under unit total probability mass. For a conventional confidence alpha in the interval from zero to one, excluding one, the tail fraction 1-alpha is positive and the Rockafellar-Uryasev objective equals F_alpha(t)=t+SL_n(t)/(1-alpha). The lower cumulative weight includes outcomes less than or equal to an integer threshold, while upper mass includes only strictly larger losses. Both parts partition the original finite weight. The Lean identities hold more generally for nonnegative weights without asserting that unnormalised weights define a probability distribution or that a fixed threshold minimises the CVaR objective.

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 scenario probabilities, losses and positive-part payouts

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

$$t\le u\Rightarrow(x-u)_+\le(x-t)_+$$

Increasing retention cannot increase payment for any insured loss.

Finite stop-loss and Rockafellar-Uryasev threshold objective

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

$$SL\ge0,\tau>0\Rightarrow K\ge0$$

Nonnegative expected excess and positive tail mass make a valid nonnegative scaling.

Discrete cumulative tails, thresholds and monetary shifts

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

$$SL(t)\ge0,\;F_\alpha(t)\ge t,\;F_\alpha^{X+s}(t+s)=F_\alpha^X(t)+s$$

The root joins tail-stop-loss nonnegativity, a valid finite CVaR objective, monetary translation equivalence and the complete lower/upper finite loss partition.

Capstone theorem

The main target is `ActuarialValuation.tailTailRisk_fundamental`. The root joins tail-stop-loss nonnegativity, a valid finite CVaR objective, monetary translation equivalence and the complete lower/upper finite loss partition.

$$SL(t)\ge0,\;F_\alpha(t)\ge t,\;F_\alpha^{X+s}(t+s)=F_\alpha^X(t)+s$$

Significance

A scenario version of the original threshold-objective formula is suitable for rigorous deterministic actuarial software tests. Exact stop-loss monotonicity and positive-part partition results are reusable in reinsurance, capital modelling and future optimisation research. The root proves meaningful financial invariants: nonnegative ceded loss, a lower bound on the objective, and translation equivariance. It does not claim the objective at an arbitrary threshold equals optimised CVaR: that requires minimising over all thresholds.

Difficulty

The confidence parameter alpha must remain below one, otherwise dividing by 1-alpha is meaningless and positivity assertions fail. An insurance loss scenario at the deductible does not generate ceded payout. Discrete distributions may have atoms at a quantile: the conditional tail mean needs partial quantile mass, not a careless conditional expectation over all values greater than or equal to VaR. The auxiliary objective is defined for all real thresholds, whereas finite lower/upper tails at integer thresholds have disjoint endpoints. Zero-weight degenerate examples cannot establish the universal finite-scenario results.

The Rockafellar-Uryasev expression represents an auxiliary objective at each fixed threshold, with the conditional value-at-risk corresponding to its minimum across thresholds. This proposal does not assume that any arbitrary deductible minimises the objective. It distinguishes a discrete lattice distribution from a continuous loss density and preserves the mass at the chosen deductible in the lower tail. Taking a retention greater than every possible loss yields zero ceded premium but does not prove a zero capital risk measure. Translation equivariance follows from shifting the distribution of losses and the monetary threshold together, so the excess layer itself remains unchanged.

Formalization scope

This is finite-scenario algebraic formal verification of a classic CVaR optimisation building block, not a continuous-distribution conditional expectation theorem or an assertion of existence/uniqueness of the minimising quantile. No distributional normalisation is inferred from truncated mass. The meaningful root relates insurance payouts, risk objective and monetary translation across arbitrary finite nonnegative-weight scenarios, preserving explicit denominator restrictions. This supports independent future research on convexity, optimum threshold and subadditive coherent measures.

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. Tyrrell Rockafellar and Stanislav Uryasev, Optimization of Conditional Value-at-Risk (1999 preprint; Journal of Risk 2000), Equation (4), p. 5. https://sites.math.washington.edu/~rtr/papers/rtr179-CVaR1.pdf
• Rockafellar and Uryasev, Optimization of Conditional Value-at-Risk (2000), Journal of Risk 2, pp. 21–42. https://econpapers.repec.org/RePEc:rsk:journ4:2161159

Motivation

Actuarial collective risk models represent total insured losses as a random sum of claim amounts. Panjer's 1981 recursive method provides a tractable recurrence for aggregate probabilities when claim number frequencies belong to a specified recursive family. This mission uses the compound Poisson special case and formalises the positive integer severity setting, its unique recursive aggregate law and finite premium and stop-loss valuations.

Finite actuarial valuation follows published literature, including the principal source. Definitions of finite event counts, valuation factors and cashflow conventions must be treated as precise mathematical inputs. Established actuarial formulae motivate the work; the resulting Lean statements are newly proposed, open proof obligations. The formal verification of these identities is distinct from the existing published mathematical development. No numerical tests or private declaration compilation constitute accepted proofs.

Setting

For intensity lambda at least zero, individual claims take strictly positive integer sizes with nonnegative severity weights f(j) and f(0)=0. The Poisson zero-claims probability is exp(-lambda). The aggregate loss lattice masses g(k) satisfy, for positive k, kg(k)=lambdasum from j=1 to k of j*f(j)*g(k-j). A finite probability prefix through n gives G(n), and 1-G(n) denotes its modelled tail complement. Finite expected aggregate loss and stop-loss premiums use sums over outcomes 0 through n.

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 claim-size severity and convolution

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

$$f_k\ge0\Rightarrow kf_k\ge0$$

Nonnegative severity weights yield nonnegative weighted claims.

Compound Poisson Panjer recurrence

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

Representative theorem `ActuarialValuation.panjerRecurrence_nonneg`:

$$\lambda,f\ge0\Rightarrow g_k\ge0$$

The uniquely generated compound Poisson aggregate coefficients are nonnegative for nonnegative severity probabilities.

Finite aggregate loss reserve and stop-loss valuation

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

Representative theorem `ActuarialValuation.panjerAggregateClaims_fundamental`:

$$g=h,\;g_k\ge0,\;G_n+T_n=1,\;SL_n(d)\ge0,\;\lambda\mu_n\ge0$$

The compound aggregate-claims capstone combines genuine uniqueness of forward Panjer probabilities, nonnegative aggregate coefficients, and finite claim-payment cost controls.

Capstone theorem

The main target is `ActuarialValuation.panjerAggregateClaims_fundamental`. The compound aggregate-claims capstone combines genuine uniqueness of forward Panjer probabilities, nonnegative aggregate coefficients, and finite claim-payment cost controls.

$$g=h,\;g_k\ge0,\;G_n+T_n=1,\;SL_n(d)\ge0,\;\lambda\mu_n\ge0$$

Significance

The core mathematical target proves that the forward recurrence with initial mass exp(-lambda) uniquely fixes all aggregate coefficients, and nonnegative intensity and severities imply all generated probabilities are nonnegative. It reconciles finite cumulative mass, a tail complement, expected aggregate costs and a ceded stop-loss value in one theorem. The recursion is independent of the earlier negative-binomial frequency moment mission and leaves full normalisation to separate infinite-series proofs.

The importance of the formal result is the availability of reusable, source-explicit lemmas for actuarial software audit and subsequent independent mathematical work, as described in the published literature. It goes beyond an elementary reformulation of a single definition: the capstone simultaneously connects different construction stages with monetary or probability reconciliation and precise boundary hypotheses. A vacuous zero-data specialisation cannot establish these relationships across arbitrary finite schedules.

Difficulty

The Panjer recurrence requires positive severity weights indexed by j at least one: allowing mass at zero without changing the denominator and initial atom would make its stated form incorrect. For each target k only lower aggregate coefficients occur, permitting ordinary induction. Natural index subtraction is safe within the finite sum. Intensity positivity, exp(-lambda), natural-to-real index coercions and finite sums need careful attention. This mission deliberately does not claim that a truncated mass automatically sums to one or that a sequence satisfying the recurrence is normalised without additional assumptions.

The recurrence's fundamental mathematical content is the coefficient-by-coefficient relationship: the coefficient at aggregate loss k depends only on previously calculated coefficients for aggregate losses strictly below k. This well-founded structure supports a strong induction proof of uniqueness and a separate positivity induction. The initial mass exp(-lambda) applies only when each individual claim has strictly positive loss. A severity law admitting zero-sized claims would require a corrected initial atom and a denominator involving zero-severity mass. A finite prefix of recursive probabilities is not, by itself, an exhaustive law. Further work can add total normalisation and full expectation formulas.

Formalization scope

The model is the lattice compound Poisson special case, not the full (a,b,0) family. It distinguishes algebraic consistency of a recursively specified sequence from measure-theoretic construction of an independent compound random sum. Stop-loss results are finite truncation values and do not by themselves control omitted large losses. All theorems are original derived 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

• H. H. Panjer, Recursive Evaluation of a Family of Compound Distributions, ASTIN Bulletin 12 (1981), pp. 22–26. https://www.casact.org/sites/default/files/database/astin_vol12no1_22.pdf
• Sundt and Jewell, Further Results on Recursive Evaluation of Compound Distributions, ASTIN Bulletin 12 (1981), pp. 27–39. https://www.casact.org/sites/default/files/database/astin_vol12no1_27.pdf

Motivation

Insurance mortality investigations must estimate survival probabilities from observed death times when some policyholders leave the observation period alive or are otherwise censored. Kaplan-Meier product-limit estimation accounts for changing risk sets without misclassifying censoring as mortality. Greenwood's formula provides the standard plug-in variance. This mission formalises a finite death-event calculation, risk-set conservation, survival probability bounds, and variance bookkeeping.

Finite actuarial valuation follows published literature, including the principal source. Definitions of finite event counts, valuation factors and cashflow conventions must be treated as precise mathematical inputs. Established actuarial formulae motivate the work; the resulting Lean statements are newly proposed, open proof obligations. The formal verification of these identities is distinct from the existing published mathematical development. No numerical tests or private declaration compilation constitute accepted proofs.

Setting

At event index t, the observed risk set r_t is positive immediately before deaths d_t and censoring exits c_t. Deaths and censors are disjoint exits, so the next risk set is r_t-d_t-c_t under a closed cohort. The estimated event-time mortality fraction is d_t/r_t, and Kaplan-Meier survival through n events is the product of 1-d_t/r_t. The complement gives cumulative failure. With 0<=d_t<r_t, the Greenwood term is d_t/[r_t(r_t-d_t)] and the plug-in variance equals squared Kaplan-Meier survival times the accumulated terms. Restricted expected lifetime is a finite sum of discrete event-time survival values.

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.

Observed risk sets and interval exits

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

$$d/r+c/r=(d+c)/r$$

Death and censoring hazards sum to the total observed exit fraction, without equating censoring to mortality.

Kaplan-Meier product-limit survival

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

$$S_{n+1}=S_np_n$$

An actuarial one-step survival update reproduces the exact finite product-limit estimate.

Greenwood uncertainty and finite restricted survival

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

Representative theorem `ActuarialValuation.kmSurvivalGreenwood_fundamental`:

$$0\le S_{n+1}\le S_n,\;S_{n+1}+F_{n+1}=1,\;V_{n+1}\ge0,\;RMST_{n+1}\ge0$$

The survival-estimation capstone proves the complete finite product-limit probability bounds, failure partition, nonnegative Greenwood plug-in variance and nonnegative restricted expected lifetime under strict risk-set conditions.

Capstone theorem

The main target is `ActuarialValuation.kmSurvivalGreenwood_fundamental`. The survival-estimation capstone proves the complete finite product-limit probability bounds, failure partition, nonnegative Greenwood plug-in variance and nonnegative restricted expected lifetime under strict risk-set conditions.

$$0\le S_{n+1}\le S_n,\;S_{n+1}+F_{n+1}=1,\;V_{n+1}\ge0,\;RMST_{n+1}\ge0$$

Significance

The capstone formally guarantees nonnegative and nonincreasing estimated survival, a complementary failure estimate, a nonnegative Greenwood plug-in variance and a nonnegative finite restricted survival integral under actual risk-set constraints. These are foundational actuarial quality-control properties and provide reusable results for experience investigations. Censoring changes future exposures but never directly counts as a death.

The importance of the formal result is the availability of reusable, source-explicit lemmas for actuarial software audit and subsequent independent mathematical work, as described in the published literature. It goes beyond an elementary reformulation of a single definition: the capstone simultaneously connects different construction stages with monetary or probability reconciliation and precise boundary hypotheses. A vacuous zero-data specialisation cannot establish these relationships across arbitrary finite schedules.

Difficulty

The denominator must be the individuals under observation immediately before the death time. Event times with r_t=0 cannot identify a mortality fraction. The Greenwood variance denominator requires r_t>d_t, so a complete mortality exhaustion creates a boundary where the usual finite formula is undefined. Event-time product-limit survival does not imply unbiasedness under informative censoring; external independent/non-informative censoring assumptions are needed for statistical interpretations. A finite restricted sum is not an unrestricted life expectancy.

The survival estimator is indexed by actual ordered death-event intervals. People censored without dying should remain at risk up to the censoring time and leave the risk set before later events. At a death time the product decreases by a factor determined by deaths divided by lives currently exposed. At an interval containing no death the factor is one. The standard Greenwood approximation is only defined when positive risk remains after each included set of deaths. At complete exhaustion the finite variance expression must not divide by zero, and the usual delta-method approximation should not be silently extrapolated. Results are deterministic algebra conditional on observed counts, not a theorem of statistical consistency.

Formalization scope

The formal model is a finite discrete event-time product-limit calculation, not an asymptotic proof of the Kaplan-Meier central limit theorem. Greenwood's plug-in formula is defined explicitly; the proof obligations concern its algebra, positivity and consistency under stated boundaries, not an estimator-unbiasedness claim. Definitions and milestones are original derived Lean results based on published survival-method principles.

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

• Society of Actuaries, Mortality Differences by Handedness, Transactions of the Society of Actuaries 45 (1993), p. 267, on product-limit estimation and Greenwood variance. https://www.soa.org/globalassets/assets/library/research/transactions-of-society-of-actuaries/1990-95/1993/january/tsa93v459.pdf
• Kaplan and Meier, Nonparametric Estimation from Incomplete Observations (1958), Journal of the American Statistical Association 53, pp. 457–481. https://doi.org/10.1080/01621459.1958.10501452

Motivation

Paid claims triangles are essential to general insurance reserving. A volume-weighted chain-ladder link factor projects mature cohorts and less developed cohorts to a common ultimate basis, while the Bornhuetter-Ferguson approach apportions expected remaining development to an externally selected prior ultimate. This research mission formalises their finite algebra and reconciliation without asserting stochastic unbiasedness or any distributional variance result.

Finite actuarial valuation follows published literature, including the principal source. Definitions of finite event counts, valuation factors and cashflow conventions must be treated as precise mathematical inputs. Established actuarial formulae motivate the work; the resulting Lean statements are newly proposed, open proof obligations. The formal verification of these identities is distinct from the existing published mathematical development. No numerical tests or private declaration compilation constitute accepted proofs.

Setting

For origin cohort i and development period j, C(i,j) denotes cumulative paid claims and C(i,j+1)-C(i,j) the incremental payment. A selected rectangular subset with m fully observed adjacent development points gives volume-weighted factor f_j=Sum_i C(i,j+1)/Sum_i C(i,j), defined when denominator nonzero. The remaining development factor F is the finite product of selected nonnegative age-to-age factors. Latest cumulative paid claims C yield chain-ladder ultimate CF and reserve C(F-1). With a priori ultimate E, the Bornhuetter-Ferguson unpaid reserve is E(1-1/F), and ultimate is C plus this reserve.

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.

Cumulative triangles and selected development factors

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

$$N_j\ge0,D_j>0\Rightarrow f_j\ge0$$

Nonnegative claims and positive exposure make the factor nonnegative.

Development to ultimate and outstanding reserve

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

$$C+R=U$$

The ultimate estimate is reconciled exactly to paid claims and outstanding reserve.

Prior expected ultimate and Bornhuetter-Ferguson reconciliation

This block contributes 14 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.clClaimsDevelopment_fundamental`:

$$fD=N,\;C+R_{CL}=U_{CL},\;U_{BF}=wU_{CL}+(1-w)E,\;R_{CL},R_{BF}\ge0$$

The substantive capstone reconciles a volume-selected development factor, chain-ladder valuation, and prior-informed Bornhuetter-Ferguson valuation under economically meaningful positivity assumptions.

Capstone theorem

The main target is `ActuarialValuation.clClaimsDevelopment_fundamental`. The substantive capstone reconciles a volume-selected development factor, chain-ladder valuation, and prior-informed Bornhuetter-Ferguson valuation under economically meaningful positivity assumptions.

$$fD=N,\;C+R_{CL}=U_{CL},\;U_{BF}=wU_{CL}+(1-w)E,\;R_{CL},R_{BF}\ge0$$

Significance

The main formal result reconciles numerator and denominator on the same observed cohorts, the paid-plus-reserve valuation identity, and the exact BF weighted-average identity. It distinguishes development-based estimation from prior-informed estimation. These results establish algebraic control checks for finite claims triangles and reserve reconciliation, while reserving model predictive uncertainty for subsequent work.

The importance of the formal result is the availability of reusable, source-explicit lemmas for actuarial software audit and subsequent independent mathematical work, as described in the published literature. It goes beyond an elementary reformulation of a single definition: the capstone simultaneously connects different construction stages with monetary or probability reconciliation and precise boundary hypotheses. A vacuous zero-data specialisation cannot establish these relationships across arbitrary finite schedules.

Difficulty

Carefully distinguish incremental and cumulative claims, the latest paid amount and ultimate, and an age-to-age factor from the full age-to-ultimate product. The volume-weighted ratio must use identical origin-cohort exposure in numerator and denominator. A zero denominator does not identify a meaningful observed development factor. The BF interpretation requires strictly positive F, and nonnegative future emergence requires F at least one. Deterministic algebra is not an assertion of unbiased predictive reserves without statistical assumptions.

An age-to-age ratio represents an explicitly selected rectangular cohort of observed cumulative values. It is not interchangeable with the arithmetic average of individual ratios, nor with an extrapolated tail factor after the final observed maturity. Where paid and incurred development patterns differ, separate sets of factors must be selected. In the Bornhuetter-Ferguson setting the chosen external expectation must correspond to the same basis as the observed cumulative paid claims: mixing paid claims and reported case estimates invalidates the interpretation. The final theorem therefore tests linked monetary identities rather than asserting an objective optimal reserve.

Formalization scope

The task is finite deterministic paid-claims reserving in a single currency and valuation date, with nonnegative selected cumulative development under hypotheses of each theorem. It formalises no future-tail extrapolation or reserve variability, and no stochastic independence or Mack conditional unbiasedness. Every theorem is an original derived Lean goal requiring an accepted proof.

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

• Klaus D. Schmidt, Methods and Models of Loss Reserving Based on Run-Off Triangles, CAS Forum (2006), especially section 4.3 and p. 283. https://www.casact.org/sites/default/files/database/forum_06fforum_273.pdf
• Schmidt and Zocher, The Bornhuetter-Ferguson Principle, Casualty Actuarial Society (2008). https://www.casact.org/sites/default/files/2021-07/Bornhuetter-Ferguson-Schmidt-Zocher.pdf

Motivation

Actuarial valuation of these claims follows published actuarial mathematics (https://www.actuaries.org.uk/system/files/documents/pdf/0042-0071.pdf). Actuarial commutation functions provide a classical exact connection between life-table survival and financial discounting. The Institute of Actuaries' International Actuarial Notation (1969–1971) records the discounted survivor and death columns and their accumulated insurance and annuity values. Dickson, Hardy and Waters' Actuarial Mathematics for Life Contingent Risks (2009), Chapter 5, explains valuation relationships between assurance and annuity payments. The objective is a connected proof of the finite-horizon assurance, annuity-due and pure endowment identity, rather than a cataloguing of conventional symbols.

Setting

Existing known actuarial results from the reference sources motivate these new original-derived theorem obligations. The actuarial formulae in published literature provide the mathematical background, while the proposed Lean theorem declarations are original derived results and remain unproved. A genuine nonzero mortality, service or insurance cashflow model is required rather than a vacuous zero-value special case. Accepted results will support more advanced actuarial valuation tasks.

An integer-age life table l(x) gives survivors at age x and decreases over the covered term. An annual discount factor v is strictly positive. The commutation functions are D_x=v^x l_x and C_x=v^(x+1)(l_x−l_(x+1)), where the second discounts a death claim payable at the end of the year. The finite sums N_(x:n)=sum_(k<n)D_(x+k) and M_(x:n)=sum_(k<n)C_(x+k) measure the temporary annuity-due and term assurance numerators. Terminal survival is D_(x+n), and the financial effective discount rate is d=1−v. Dividing the numerator sums by D_x gives the corresponding conditional actuarial present values, when D_x is nonzero.

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.

Discounted life table functions

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.commLocalDeathIdentity:

$$C_x+(1-v)D_x=D_x-D_{x+1}$$

One-year death and annuity-discount value telescope to the discounted decrement.

Finite commutation functions

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

$$M_{x:n}+dN_{x:n}+D_{x+n}=D_x$$

The full insurance-annuity-survival decomposition follows by telescoping annual differences.

Assurance and annuity monetary values

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

Representative theorem ActuarialValuation.commAssuranceAnnuity_fundamental:

$$M+dN+D_{x+n}=D_x,\quad A+d\ddot a+E=1$$

The capstone establishes both raw and conditional actuarial valuation identities and nonnegativity of term assurance and pure endowment for a valid life table.

Capstone theorem

The main target is ActuarialValuation.commAssuranceAnnuity_fundamental. The capstone establishes both raw and conditional actuarial valuation identities and nonnegativity of term assurance and pure endowment for a valid life table.

$$M+dN+D_{x+n}=D_x,\quad A+d\ddot a+E=1$$

Significance

The resulting formal identities will be reusable by future downstream pensions and insurance valuation missions. Formal actuarial modelling of these obligations follows the published valuation literature (https://www.actuaries.org.uk/system/files/documents/pdf/0042-0071.pdf). The one-year identity C_x+(1−v)D_x=D_x−D_(x+1) telescopes over successive payment years. The resulting finite equation M_(x:n)+dN_(x:n)+D_(x+n)=D_x reconciles three disjoint financially timed payment streams. Dividing by D_x yields A_(x:n)+d a_due_(x:n)+E_(x:n)=1, connecting term assurance, annuity due and survival to term expiration. This provides a powerful actuarial valuation consistency check: omitting a terminal survival payment or discounting deaths at the beginning rather than end of the year breaks the identity.

Difficulty

The annual life-table decrement l_x−l_(x+1) must not be confused with the financial discount d=1−v. The annuity-due includes the initial survivor payment at age x whereas the insurance claim is payable at the end of the death year. Each exponent and half-open finite sum endpoint must be exact. The main telescope holds without assumptions on real survivor counts, but financial probability interpretation requires nonnegative remaining lives and a nonincreasing table, plus positive valuation-age survivors. The conditional ratios require a nonzero D_x. A general theorem must not assume the result by defining the numerator balance identically equal to D_x.

Formalization scope

The model is a finite integer-age life table and a common annual interest basis with unit annuity payments, year-end unit death claims and a unit pure endowment at the terminal payment date. It makes no independence assumption about additional lives and introduces no continuous-time death benefits. The capstone proves the raw commutation identity, the actuarial present value identity and nonnegativity of its insurance and terminal survival components. All declarations are original Lean formalisation targets and should remain open until genuine accepted remote proofs exist.

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 of Actuaries, International Actuarial Notation and Commutation Functions (1969–1971). https://www.actuaries.org.uk/system/files/documents/pdf/0042-0071.pdf
• David C. M. Dickson, Mary R. Hardy and Howard R. Waters, Actuarial Mathematics for Life Contingent Risks: Annuities (2009). https://www.cambridge.org/core/books/abs/actuarial-mathematics-for-life-contingent-risks/annuities/6E4AF10872F5D04E3437447F025ECA97

Motivation

Actuarial valuation of these claims follows published actuarial mathematics (https://onlinelibrary.wiley.com/doi/10.1002/9781119971528.ch6). Life insurance policy alterations require a mathematically coherent link between reserves, remaining premium payments, reduced paid-up cover and cash surrender settlements. In Fundamentals of Actuarial Mathematics, S. David Promislow develops the premium difference and paid-up formulae in Chapter 6, Section 6.8 (2010/2015). Dickson, Hardy and Waters cover policy values and alterations within life-contingent reserve theory. The proposal creates a connected sequence of algebraic valuation results for these choices, without treating a surrender value as if it were always the prospective reserve.

Setting

Existing known actuarial results from the reference sources motivate these new original-derived theorem obligations. The actuarial formulae in published literature provide the mathematical background, while the proposed Lean theorem declarations are original derived results and remain unproved. A genuine nonzero mortality, service or insurance cashflow model is required rather than a vacuous zero-value special case. Accepted results will support more advanced actuarial valuation tasks.

At the policy alteration date, B denotes the complete present value of remaining insured benefits and a denotes the value of future unit premium payments. A level premium P leaves prospective policy reserve V=B−Pa. An equivalent newly repriced premium Ps=B/a is meaningful for nonzero a. A reserve-equivalent paid-up benefit amount b is V/Aunit for an explicitly positive unit insurance present value Aunit. A proportionally scaled paid-up policy uses z=V/B under nonzero B. Cash surrender value is the simplified payment SV=V−c, with a separate nonnegative surrender deduction c not exceeding V when positive surrender cash is required. All values are compared at the same time and on one consistent actuarial valuation basis.

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.

Prospective reserve and premium difference

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

$$V(P_2)-V(P_1)=(P_1-P_2)a$$

Change in future premiums shifts the actuarial reserve by the monetised payment difference.

Paid-up insurance and equivalent cover

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.alterationPaidUpScaledValue_add:

$$PV(f+g)=PV(f)+PV(g)$$

Paid-up proportional benefit values are additive over cover portions.

Surrender deductions and policy value comparisons

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

Representative theorem ActuarialValuation.alterationReservePaidUpSurrender_fundamental:

$$V=(P_s-P)a=b_{\rm PU}A_{\rm unit},\quad0\le SV\le V$$

Main policy alteration theorem reconciles prospective reserve, repriced premium difference and reserve-equivalent paid-up cover while bounding surrender cash by the reserve.

Capstone theorem

The main target is ActuarialValuation.alterationReservePaidUpSurrender_fundamental. Main policy alteration theorem reconciles prospective reserve, repriced premium difference and reserve-equivalent paid-up cover while bounding surrender cash by the reserve.

$$V=(P_s-P)a=b_{\rm PU}A_{\rm unit},\quad0\le SV\le V$$

Significance

Formal actuarial modelling of these obligations follows the published valuation literature (https://onlinelibrary.wiley.com/doi/10.1002/9781119971528.ch6). The premium difference theorem identifies reserve as the present value of the deficiency of original premiums relative to the equivalent premium currently required for remaining benefits. Paid-up insurance conversion substitutes a benefit without future premiums whose expected present value equals the original reserve. A surrender amount can differ from reserve when contractual charges apply. These three concepts reconcile actuarially while remaining different legal and financial benefit forms. The final theorem combines premium-difference equivalence, paid-up monetary equivalence, and the inequality between surrender value and reserve under explicit reserve and deduction constraints.

Difficulty

Divisions in reprice and paid-up formulae require nonzero insurance and premium annuity denominators, unlike Lean's totalised real division. A prospective reserve can be negative if future premiums exceed remaining insurance values, so nonnegative paid-up cover and cash surrender cannot be claimed without additional assumptions. An actual policy might use tax, expenses, guaranteed surrender values, bonus distributions or other legal terms not represented by a simple deduction. The model distinguishes a change in premium value from a change in benefit value, and the capstone cannot be established through a degenerate zero-cover simplification.

Formalization scope

The mathematical scope is a finite real-valued prospective valuation model supplied with consistent actuarial present-value factors. Benefit discounting, mortality basis and benefit dates are represented by B, a and Aunit rather than silently re-derived. Paid-up and surrender transformations are idealised actuarial alternatives and are not universal contractual entitlements. Asset share is a separate retrospective concept and is not asserted equal to prospective reserve without further matching assumptions. Every theorem remains an original derived obligation, suitable for subsequent extensions with expense-adjusted reserves and policyholder nonforfeiture terms.

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, Fundamentals of Actuarial Mathematics (2010), Chapter 6. https://onlinelibrary.wiley.com/doi/10.1002/9781119971528.ch6
• David C. M. Dickson, Mary R. Hardy and Howard R. Waters, Actuarial Mathematics for Life Contingent Risks (2009). https://www.cambridge.org/core/books/actuarial-mathematics-for-life-contingent-risks/51C0B04099D4DE1D1DDEF9551024133B/listing

Motivation

Actuarial valuation of these claims follows published actuarial mathematics (https://www.actuary.org/sites/default/files/pdf/pension/fundamentals_0704.pdf). Projected unit credit funding is a standard actuarial cost method that allocates pension retirement benefits to completed and future years of service. The American Academy of Actuaries describes actuarial accrued liability and normal cost under this method in its Fundamentals of Pension Accounting and Funding (2004). The Institute of Actuaries' GN26 Pension Fund Terminology (2006) likewise describes projected unit cost, standard contribution rates and amortisation. This formal research mission unites the benefit attribution and funding calculations in a single theorem graph; it goes beyond the separate salary-linked CARE/DC terminal equivalence already treated in the preceding mission.

Setting

The actuarial formulae in published literature provide the mathematical background, while the proposed Lean theorem declarations are original derived results and remain unproved. A genuine nonzero mortality, service or insurance cashflow model is required rather than a vacuous zero-value special case. Accepted results will support more advanced actuarial valuation tasks.

A finite salary-linked accrued annual pension is expressed as a sum of projected retirement benefit units b(t). Completed service years occupy the half-open index range zero through n−1, and m future years occupy n through n+m−1. An actuarial retirement factor f is a survival probability times an appropriate discount and pension annuity package. The accrued liability is AL=f sum of completed service units, and projected future normal costs equal f times the future-service units. Assets A are measured at the same valuation date. An unfunded liability UL=AL−A is financed by a constant contribution rate c applied to a strictly positive present value F of pensionable payroll, and S=A+cF−AL is the resulting simplified funding surplus.

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.

Projected service and accrued benefits

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.pucTotalBenefit_zero:

$$B_{0,0}=0$$

An empty past and future service ledger has zero pension.

Actuarial liability and normal cost

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.pucProjectedBenefitPV_add_future:

$$PVFB_{m+1}=PVFB_m+NC_{n+m}$$

Projected PV of benefits increases by the normal cost of the added service year.

Funding shortfall and contribution amortisation

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

Representative theorem ActuarialValuation.pucPensionFunding_fundamental:

$$PVFB=AL+PVFNC,\quad c^*F=UL,\quad c\ge c^*\Rightarrow S(c)\ge0$$

The pension funding capstone unites projected-unit service attribution with the exact amortisation contribution threshold and surplus monotonicity.

Capstone theorem

The main target is ActuarialValuation.pucPensionFunding_fundamental. The pension funding capstone unites projected-unit service attribution with the exact amortisation contribution threshold and surplus monotonicity.

$$PVFB=AL+PVFNC,\quad c^*F=UL,\quad c\ge c^*\Rightarrow S(c)\ge0$$

Significance

Formal actuarial modelling of these obligations follows the published valuation literature (https://www.actuary.org/sites/default/files/pdf/pension/fundamentals_0704.pdf). A sound pension valuation must reconcile the projected retirement benefit with both its accrued-service obligation and the cost of further service. The formal capstone proves that PVFB=AL+PVFNC under the same projected benefit assumptions. It additionally derives the unique amortisation percentage c*=UL/F required to extinguish a nonnegative valuation-date deficit and proves that every larger contribution percentage produces nonnegative surplus. This establishes a financial and actuarial accounting invariant across valuation and funding. It can support later analyses of demographic experience, recovery periods, employer contributions and aggregate scheme funding, but does not automatically impose any scheme-specific contribution rule.

Difficulty

The benefit units represent projected retirement benefits, not past salary amounts at historical ages. Past and future service must be disjoint and exhaustion of the projection horizon must be exact. The pension factor uses the same assumed retirement date, survival and payment schedule throughout each monetary reconciliation; changes in that basis are outside the elementary attribution equation. Zero service and zero accrued liability are meaningful. A nonzero payroll base is necessary to define the funding rate, and positive payroll PV is essential to monotonicity. Deficits and surpluses are financially different: the chosen capstone assumes a nonnegative unfunded deficit rather than assuming the same payment solves an overfunded scheme under all regulations.

Formalization scope

The formal results treat an individual or coherently aggregated finite service schedule under one actuarial pension valuation basis and a simplified fixed-rate contribution financing model. They do not assert that the selected funding contribution must be paid by law or accounting standards, nor do they value ancillary expenses, deferred pension increases or new entrants automatically. The main theorem combines independently defined actuarial benefit allocation, pension liability and funding surplus. Existing pension funding textbooks provide the conceptual derivations, while every proposed Lean statement is an original finite formalisation requiring a real proof.

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

• American Academy of Actuaries, Fundamentals of Pension Accounting and Funding (2004). https://www.actuary.org/sites/default/files/pdf/pension/fundamentals_0704.pdf
• Institute of Actuaries, GN26 Pension Fund Terminology (2006). https://www.actuaries.org.uk/system/files/documents/pdf/gn26v2-1.pdf
• International Monetary Fund, Conducting Stress Tests of Defined Benefit Pension Plans (2014). https://www.elibrary.imf.org/display/book/9781484368589/ch012.xml

Motivation

A life table summarises the survival of a cohort as ages advance, as developed in Promislow's life-table treatment. It provides an essential common language for life assurance, retirement pensions, annuities and reserves. A credible mathematical foundation must make precise when cohort counts define conditional probabilities, how death counts exhaust an assumed closed population, and why commutation-function ratios give the same values as discounted contractual payments. The classical notation is widely understood by actuaries but can conceal assumptions at terminal ages, when there are no remaining lives, and at fractional-year payment times. This formalisation specifies those assumptions so that later results can safely reuse them.

Setting

Consider an integer-age cohort with a finite terminal age, nonnegative numbers alive and nonincreasing numbers alive at successive ages. At the terminal age the remaining cohort is zero. Annual deaths are the change in cohort size over each year. Conditional survival starts only from an age with positive numbers alive. The model also has a strictly positive annual discount factor; when the corresponding effective interest rate is nonnegative, that factor is at most one. A due annuity pays on the integer anniversaries at which the insured life is alive. An annual death assurance pays at the end of the year of death. All financial amounts in the principal identities are per unit benefit, valued at the attained age of the insured life.

Formalization targets

Cohort probabilities and lifetime laws

The opening group establishes that successive survivor and decrement counts conserve population mass. Multi-year survival, conditional and deferred mortality must be derived from original counts and remain coherent under time shifts. A zero survivor count is an explicit boundary of the probability model. Curtate lifetime moments are obtained from the annual death distribution and its tail probabilities. Continuous survival and hazard relationships form an additional interface requiring a genuine measurable lifetime law. They cannot be inferred from the table's integer-age observations without an interpolation assumption.

Select and fractional-age assumptions

The next group distinguishes age at selection from time since selection and attained age. Ultimate mortality applies only after the selection period. Within a year, uniform distribution of deaths, constant force and Balducci interpolation share the annual survival endpoints but generally disagree between those endpoints. Each conditional fractional formula needs the corresponding survival denominator to be positive. These are alternative models, so the choice of interpolation must remain explicit.

Commutation columns and benefit timing

The commutation columns are defined from the same original survivor counts and a fixed annual discount factor. Discounted survivors and year-end deaths create the first-order columns. Their finite forward sums create the second-order columns, and sums of those forward sums create the increasing-benefit columns. In particular, for survivors the discounted payments begin at the valuation anniversary, whereas for deaths the benefit is payable on the next anniversary. The finite terminal convention is essential for the last year's assurance payment and the last available annuity instalment.

Principal finite-cohort capstone

The principal goal is the finite-cohort valuation reconciliation. Starting independently from annual numbers alive and numbers dying, it shows that total deaths exhaust the living cohort, actual survival-contingent payments agree with the annuity commutation ratio, actual annual death payments agree with the assurance commutation ratio, and the commutation sums satisfy their backward recursions. It also establishes the capital identity expressing unit present value as annual death assurance plus the discount loss on an annuity due. No commutation recurrence or present-value equivalence is assumed as an input.

At a valid attained age, the annuity and assurance are independently valued from the original cohort:

$$\ddot a_x=\frac{N_x}{D_x},\qquad A_x=\frac{M_x}{D_x},\qquad A_x+(1-v)\ddot a_x=1.$$

Significance

As in the classical actuarial notation, the resulting interfaces separate cohort mass from conditional probability and separate mortality from the economic discounting basis. This allows a later actuarial mission to combine them only where the required regularity and positivity assumptions are available. The commutation functions supply a transparent independent valuation route alongside direct finite cashflow sums. Their ratios remain useful as a reference calculation even when production models value very large pension populations by member-level cashflow projection. Higher-order commutation functions are also the natural algebraic representation of benefits that increase by one unit at each subsequent anniversary.

This foundation is reusable across future mortality and valuation missions. A foundational namespace is particularly important where related existing missions already use different local definitions. The present work provides a compatibility design and a proposed canonical public vocabulary. Publishing an older equivalent definition does not automatically establish a safe imported interface: exact source, revision, visibility, and declaration signatures must match. The programme therefore retains existing mission objects and develops explicit crosswalks, rather than silently replacing earlier results.

Difficulty

The mathematical difficulty centres on conditioning, index shifts and independent routes to the same financial result. At an age with no survivors, a formal programming language may return a totalised value for division by zero even though no conditional mortality probability exists. A common off-by-one error values a death at the beginning of its year or includes a due annuity payment after the terminal age. Another error confuses discounting to time zero with discounting to the current valuation age. Select mortality requires careful handling of attained age at the exact selection-duration boundary. Continuous lifetime hazard and moment formulas additionally need probability, measurability and integrability assumptions that finite cohort counts alone cannot supply.

The double-sum commutation identities require a finite discrete summation argument and must use published survivor and assurance conventions consistently. The goal compares separate original definitions of payment cashflows, the population exit distribution, and commutation columns under one valid finite life table. The capstone is nonvacuous: a positive starting cohort and positive discount factor exclude empty-cohort substitutions and make its conditional cashflows meaningful. Its assumptions impose cohort validity and positive discounting; they do not contain the desired present-value identities as hypotheses.

Formalization scope

The initial formalisation supplies a canonical finite discrete cohort and annual cashflow basis. The continuous-law, hazard, select and fractional-age results are separately specified mathematical interfaces and are admitted into the formal theorem inventory only when remote declaration checks establish valid Lean signatures. For nonnegative effective interest the annual discount is in the interval from zero excluded to one included. More general deterministic term structures and stochastic discount factors require separate cashflow definitions. Joint-life and competing-decrement extensions must identify any independence or mutually exclusive decrement assumptions explicitly.

No assertion is made about mortality being stationary across calendar years or about the validity of a specific mortality table for a real population. The terminal-age assumption imposes certain death before the finite horizon. It is unsuitable without modification for a lifetime distribution with unbounded support. A lifetime with an atom at an integer boundary requires separate weak and strict survival events; interpreting a one-year death count as the hazard at the death instant is unjustified without further assumptions. Open formal statements remain proof obligations, and passing a declaration check would establish only well-formed Lean, not the mathematical truth of the intended result.

The finite-cohort valuation targets also include independently defined one-year and multi-year mortality probabilities, temporary and deferred annuities, term and endowment assurances, pure endowments, annuities in arrears and increasing finite-term cashflows. The expanded candidate graph has 26 definitions and 48 open theorem obligations in a coherent reconciliation programme. New results require independently derived cashflow-to-commutation identities.

Related proposals LII (commutation functions and finite-term benefits) and LXII (fractional-duration valuation) are in review, not public importable dependencies. Existing published life-table theorems in XLV must be reused where signatures match. The fractional-age and continuous-law interfaces require separate hypotheses. All research targets remain provisional until their exact published-name overlap checks, authoritative declaration elaboration and dependency links are validated. No private diagnostic is counted as a proved theorem.

The increasing-insurance commutation column requires the relative-duration or absolute-age convention to be declared explicitly. Annual UDD includes certain year-end death, but constant-force and Balducci interpolation require annual death probability strictly below one.

Selected references

• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, Chapters 2–5, 7, 9 and 13–14. https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782521
• David C. M. Dickson, Mary R. Hardy and Howard R. Waters (2020), Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, Chapters 2–5. https://doi.org/10.1017/9781108784184

Motivation

The Black–Scholes model (Black and Scholes, 1973; Merton, 1973) is the reference model for pricing European options. Its closed-form price, the Black–Scholes formula, is quoted daily by options markets, its partial derivatives (the Greeks) are the standard risk measures that trading desks limit and hedge, and the Black–Scholes equation is the prototype of the parabolic pricing PDEs that are solved numerically when no closed form exists. Merton and Scholes received the 1997 Nobel Memorial Prize in Economic Sciences for this work.

Timeline. Bachelier (1900) first applied Brownian motion to option pricing. In the 1960s Sprenkle, Boness, Samuelson and Merton refined the theory. Black and Scholes found the risk-neutral hedging argument in 1968 and published the formula in The Pricing of Options and Corporate Liabilities (Journal of Political Economy, 1973); Merton's paper of the same year extended the mathematical framework and coined the name.

Setting

Fix a strike $K>0$, an expiry $T$, a constant risk-free rate $r\in\mathbb R$ and a constant volatility $\sigma>0$. At time $t<T$ the time to maturity is $\tau=T-t>0$ and the spot price of the (non-dividend-paying) stock is $S>0$. Let

$$N(x)=\frac1{\sqrt{2\pi}}\int_{-\infty}^x e^{-z^2/2}\,dz,\qquad N'(x)=\frac1{\sqrt{2\pi}}e^{-x^2/2}$$

be the standard normal distribution and density functions, and set

$$d_+=\frac{1}{\sigma\sqrt{\tau}}\Big[\ln\frac SK+\Big(r+\frac{\sigma^2}2\Big)\tau\Big],\qquad d_-=d_+-\sigma\sqrt\tau .$$

The Black–Scholes call and put prices are

$$C(S,t)=N(d_+)S-N(d_-)Ke^{-r\tau},\qquad P(S,t)=N(-d_-)Ke^{-r\tau}-N(-d_+)S .$$

In the alternative (Black '76) parametrisation one uses the discount factor $D=e^{-r\tau}$ and the forward price $F=e^{r\tau}S$, with $d_\pm=\frac1{\sigma\sqrt\tau}\big[\ln\frac FK\pm\frac12\sigma^2\tau\big]$, and $C=D[N(d_+)F-N(d_-)K]$. Under the risk-neutral measure the terminal price is $S_T=S\exp\big((r-\tfrac12\sigma^2)\tau+\sigma\sqrt\tau\,Z\big)$ with $Z$ standard normal.

Formalization targets

Goal: the formula solves the Black–Scholes equation

On the domain $\{S>0,\ t<T\}$ the call price $C$ is $C^\infty$ and satisfies

$$\frac{\partial C}{\partial t}+\frac12\sigma^2S^2\frac{\partial^2C}{\partial S^2}+rS\frac{\partial C}{\partial S}-rC=0,$$

together with the boundary and terminal conditions $C(S,t)\to0$ as $S\to0^+$, $C(S,t)-(S-Ke^{-r(T-t)})\to0$ as $S\to\infty$, and $C(S,t)\to\max\{S-K,0\}$ as $t\to T^-$.

Milestones

1. The density $N'$ is the derivative of $N$.
2. The alternative (forward) formulation of the call and put prices.
3. Put–call parity, $P=Ke^{-r\tau}-S+C$, and its forward form $C-P=D(F-K)$.
4. The Greeks table: Delta, Gamma, Vega, Theta and Rho for calls and puts.
5. Risk-neutral pricing: $C=e^{-r\tau}\,\mathbb E[\max(S_T-K,0)]$.
6. Binary options: cash-or-nothing values $e^{-r\tau}N(\pm d_-)$ and asset-or-nothing values $SN(\pm d_+)$.

Significance

The result. The goal is the statement that ties the model's two faces together: the closed-form price is a classical solution of the pricing PDE with the payoff as terminal datum. The Greeks are what hedging strategies are built from (delta hedging is the core of the model's replication argument), put–call parity is the basic no-arbitrage relation, and the risk-neutral and binary-option identities are the probabilistic reading of the two terms in the formula.

Formalizing it. All results here are classical and proved in textbooks (e.g. Hull, Options, Futures, and Other Derivatives). The work is formalization: building a reusable, machine-checked library for the normal distribution function, the Black–Scholes price and its sensitivities, and Gaussian expectations of log-normal payoffs, on top of Mathlib's real analysis and its Gaussian measure gaussianReal.

Difficulty

Each identity is elementary on paper, but the calculus is long: every Greek requires differentiating $N\circ d_\pm$ through a logarithm, a square root and a quotient, and the simplifications rest on the identity $SN'(d_+)=Ke^{-r\tau}N'(d_-)$. The limits in the goal need Gaussian tail estimates (e.g. $SN(-d_+)\to0$ as $S\to\infty$, where $S$ grows while $N(-d_+)$ decays). The risk-neutral identities require computing Gaussian integrals over half-lines with an exponential weight, i.e. a change of variables shifting the mean of the normal distribution.

Formalization scope

All objects are real-valued and deterministic: $N$ is defined by the integral formula above (a Lebesgue integral over $(-\infty,x]$), $N'$ by its closed form, and prices by the formulas, as functions of $(S,t)$ with parameters $(K,r,\sigma,T)$. Partial derivatives are stated with HasDerivAt (genuine differentiability plus the value), except in the goal's PDE, where deriv is used together with an explicit $C^\infty$ clause on the open domain. Each theorem carries the standing assumptions $K>0$, $\sigma>0$, $S>0$, $t<T$ where they are needed; the parity identities hold without them and are stated unconditionally. At $S=0$ and $t=T$ the formula is undefined in the source, so the boundary and terminal conditions are stated as one-sided limits rather than values. Risk-neutral expectations are integrals against the standard Gaussian gaussianReal 0 1 of an explicit log-normal terminal price; no stochastic calculus (Itô integrals, SDEs, Girsanov, Feynman–Kac) is required or formalized. The dividend-paying extensions, American options and the perpetual put are out of scope; binary options are formalized for the non-dividend case $q=0$.

Contributions of reusable lemmas (derivative of $N$, symmetry $N(x)+N(-x)=1$, limits of $N$ at $\pm\infty$, Gaussian half-line integrals) are welcome.

Selected references

• F. Black, M. Scholes, The Pricing of Options and Corporate Liabilities, Journal of Political Economy 81(3), 1973. https://doi.org/10.1086/260062
• R. C. Merton, Theory of Rational Option Pricing, Bell Journal of Economics and Management Science 4(1), 1973. https://doi.org/10.2307/3003143
• J. C. Hull, Options, Futures, and Other Derivatives, Pearson.
• Wikipedia, Black–Scholes model. https://en.wikipedia.org/wiki/Black%E2%80%93Scholes_model

Motivation

Zipf's law is the empirical observation that when a set of measured values is sorted in decreasing order, the value of the $n$-th entry is often approximately inversely proportional to $n$. Its best-known instance is word frequency in natural language: in the Brown Corpus the most frequent word, "the", accounts for nearly $7\%$ of all word occurrences, the second, "of", for slightly over $3.5\%$, and so on. The same rank–size relation has been reported for city populations (Auerbach 1913), firm sizes (Axtell 2001), and many other data sets; it is named after the linguist George Kingsley Zipf (1932, 1935, 1949) and remains a central concept of quantitative linguistics (Piantadosi 2014).

In mathematical statistics the law is formalized as the Zipf distribution, a family of discrete probability distributions whose rank–frequency relation is an inverse power law, together with its relatives: the zeta distribution (Lotka's law), the Zipf–Mandelbrot law and the Yule–Simon distribution. Several generative explanations — random typing (Miller 1957, Li 1992) and preferential attachment — produce power laws by provable mechanisms.

Timeline of the results formalized here:

• 1913–1932 — Auerbach (city sizes), Estoup (1916), Dewey (1923), Condon (1928) and Zipf (1932) observe the inverse rank–frequency relation.
• 1957 — Miller: a power law emerges in randomly generated texts (doi:10.2307/1419346).
• 1992 — Li: in random texts with equiprobable letters, word frequency follows Zipf's macro-trend (doi:10.1109/18.165464).

Setting

For a real exponent $s$ and an integer $N \ge 1$, the generalized harmonic number is

$$H_{N,s} = \sum_{k=1}^{N}\frac{1}{k^s}, \qquad H_N = H_{N,1}.$$

The Zipf distribution on $N$ elements with exponent $s$ assigns to the element of rank $k \in\{1,\dots,N\}$ the probability

$$f(k;N,s) = \frac{1}{H_{N,s}}\,\frac{1}{k^{s}} .$$

The classical Zipf law is $s=1$. The source lists the parameter range $s\ge0$, $N\in\{1,2,3,\dots\}$.

The Riemann zeta function is $\zeta(s)=\sum_{k\ge1}k^{-s}$ for $s>1$. The Hurwitz zeta function is $\zeta(s,a)=\sum_{n\ge0}(n+a)^{-s}$. The Zipf–Mandelbrot law on ranks $k=1,2,\dots$ with shift $q$ and exponent $s$ is $f(k;q,s)=\frac{1}{C}\frac{1}{(k+q)^s}$ with $C=\zeta(s,q+1)$. The Yule–Simon distribution with parameter $\rho>0$ is $f(k;\rho)=\rho\,B(k,\rho+1)=\rho\,\Gamma(k)\Gamma(\rho+1)/\Gamma(k+\rho+1)$, $k = 1, 2, \dots$.

Formalization targets

Goal — the infinite-item extension

For $s \ge 0$:

$$\sum_{k\ge1}\frac1{k^s}<\infty \iff s>1;\qquad s>1 \implies H_{N,s}\xrightarrow[N\to\infty]{}\zeta(s);\qquad s\le1 \implies H_{N,s}\xrightarrow[N\to\infty]{}\infty .$$

That is, the generalized Zipf distribution extends to infinitely many items exactly when $s>1$, in which case the normalizing constant becomes Riemann's zeta function.

Milestones

1. Normalization: $\sum_{k=1}^N f(k;N,s)=1$.
2. CDF: $\sum_{k=1}^n f(k;N,s)=H_{n,s}/H_{N,s}$ for $n\le N$.
3. Mean: $\sum_{k} k\,f(k;N,s)=H_{N,s-1}/H_{N,s}$.
4. Variance: $\frac{H_{N,s-2}}{H_{N,s}}-\frac{H_{N,s-1}^2}{H_{N,s}^2}$.
5. Entropy: $\frac{s}{H_{N,s}}\sum_{k=1}^N\frac{\ln k}{k^s}+\ln H_{N,s}$.
6. Mode: rank $1$ is a most probable element (for $s \ge 0$).
7. Ratio: $f(1;N,s)/f(n;N,s)=n^s$ — "the most common word occurs about $n$ times the $n$-th most common one" when $s = 1$.
8. Log–log linearity: $\ln f(k;N,s) = -s\ln k-\ln H_{N,s}$, an affine function of $\ln k$ with slope $-s$.
9. Zipf–Mandelbrot: with $C=\zeta(s,q+1)$ the law is a probability distribution ($s>1$, $q\ge0$).
10. Yule–Simon tail: $f(k;\rho)\sim C/k^{\rho+1}$ for some constant $C>0$.
11. Random typing (Li): word probability is bounded above and below by a power of the rank.
12. Benford connection: the leading digits of a Zipf ($s=1$) random rank follow Benford's law as $N\to\infty$.

Significance

The goal pins down exactly when "Zipf's law with infinitely many items" makes sense, and identifies the resulting distribution (the zeta distribution) with Riemann's zeta function. The milestones are the infobox facts that statisticians use when fitting Zipf models (CDF, mean, variance, entropy, mode), the log–log diagnostic used to test data against the law, two of the related laws the source lists (Zipf–Mandelbrot, Yule–Simon), one of the generative explanations (random typing), and the stated link to Benford's law.

The results are classical; the work is formalizing them. Most milestones are finite algebra about $H_{N,s}$; the goal, the Yule–Simon tail, the random-typing bound and the Benford connection need analysis.

Difficulty

The finite identities are routine once the support conventions are fixed. The analytic content is concentrated in four places. The goal needs the $p$-series test and the identification of the limit with Mathlib's complex riemannZeta, which is defined by analytic continuation rather than by the series. The Yule–Simon tail needs the asymptotics $\Gamma(k)/\Gamma(k+a)\sim k^{-a}$. The random-typing bound requires controlling the rank of a word through the number of strictly shorter words, uniformly over every rank order compatible with the probabilities. The Benford connection requires comparing the harmonic sums over each block of integers with a fixed leading digit with $\ln(1+1/d)$, with an error that is negligible against $H_N\sim\ln N$.

Formalization scope

• $H_{N,s}$ uses a real exponent (Real.rpow); $H_{0,s}=0$.
• zipfPMF N s k is defined for every natural $k$ and is $0$ outside the support $\{1,\dots,N\}$. Statements that need a nonempty support assume $N\ge1$.
• The goal states convergence to the complex number riemannZeta s of the real partial sums viewed as complex numbers, and divergence as Tendsto … atTop atTop. The source's parameter range $s\ge0$ is kept as a hypothesis.
• The Hurwitz zeta function is defined by its series (value $0$ when the series diverges); the Zipf–Mandelbrot law is the infinite-item version on ranks $k\ge1$, with $q\ge0$.
• The Yule–Simon distribution is defined through the Gamma function; the tail statement asserts existence of a positive constant, matching the source's "[constant]".
• Random typing is formalized in Li's equiprobable model: $m\ge2$ letters each typed with probability $q>0$, a space with probability $1-mq>0$, and a word $w$ has probability $q^{|w|}(1-mq)$. "Sorted by rank" means any bijection $e$ from $\mathbb N$ onto the nonempty words along which the probability is non-increasing; the conclusion is a two-sided power-law bound with exponent $\log_m(1/q)$.
• The Benford connection uses the leading decimal digit of the rank $k$, with $k$ drawn from the Zipf distribution with $s=1$.
• Not formalized: the empirical claims (word, city, income data), the atlas-model result, Belevitch's Taylor-series argument, the parabolic fractal distribution and the Pareto exchange of variables; their statements in the source are not precise enough to formalize faithfully.

Selected references

• G. K. Zipf, Human Behavior and the Principle of Least Effort, Addison-Wesley, 1949. https://archive.org/details/in.ernet.dli.2015.90211
• E. U. Condon, Statistics of vocabulary, Science 67 (1928), 300. https://doi.org/10.1126/science.67.1733.300
• G. A. Miller, Some effects of intermittent silence, American Journal of Psychology 70 (1957), 311–314. https://doi.org/10.2307/1419346
• W. Li, Random texts exhibit Zipf's-law-like word frequency distribution, IEEE Trans. Inform. Theory 38 (1992), 1842–1845. https://doi.org/10.1109/18.165464
• B. Conrad, M. Mitzenmacher, Power laws for monkeys typing randomly: the case of unequal probabilities, IEEE Trans. Inform. Theory 50 (2004), 1403–1414. https://doi.org/10.1109/TIT.2004.830752
• R. L. Axtell, Zipf distribution of U.S. firm sizes, Science 293 (2001), 1818–1820. https://doi.org/10.1126/science.1062081
• M. E. J. Newman, Power laws, Pareto distributions and Zipf's law, Contemporary Physics 46 (2005), 323–351. https://arxiv.org/abs/cond-mat/0412004
• S. T. Piantadosi, Zipf's word frequency law in natural language: a critical review and future directions, Psychon. Bull. Rev. 21 (2014), 1112–1130. https://doi.org/10.3758/s13423-014-0585-6
• Wikipedia, Zipf's law. https://en.wikipedia.org/wiki/Zipf%27s_law

Motivation

Benford's law (also the Newcomb–Benford law, or first-digit law) is the observation that in many real-life collections of numbers the leading significant digit is small far more often than a uniform guess would suggest: the digit $1$ leads about $30.1\%$ of the time and the digit $9$ less than $5\%$ of the time. Simon Newcomb noticed in 1881 that the early pages of logarithm tables were more worn than the later ones and proposed that digit $d$ leads with probability $\log_{10}(d+1)-\log_{10} d$ (Newcomb 1881); Frank Benford rediscovered the law in 1938 and tested it on 20,229 observations from 20 domains (Benford 1938). The law is used today as a screening statistic in forensic accounting, election forensics and the detection of fabricated scientific data.

Beyond empirical data, many classical integer sequences satisfy the law exactly, in the asymptotic sense: the powers of $2$, the powers of any integer $k$ with $\log_{10} k$ irrational, the Fibonacci numbers and the factorials. These are theorems, and they are the core of this mission.

Timeline of the mathematical results formalized here:

• 1881 — Newcomb states the first-digit law (doi:10.2307/2369148).
• 1938 — Benford's empirical study (JSTOR 984802).
• 1961 — Pinkham: a scale-invariant first-digit law must be logarithmic (doi:10.1214/aoms/1177704862).
• 1967, 1981 — Duncan and Washington: the Fibonacci numbers are Benford (doi:10.1080/00150517.1967.12431312, doi:10.1080/00150517.1981.12430109).
• 1976 — Raimi's survey "The first digit problem" (doi:10.2307/2319349).
• 1995 — Hill: base invariance and a statistical derivation; the distribution of digits beyond the first (doi:10.1214/ss/1177009869, doi:10.1080/00029890.1995.11990578).

Setting

Fix an integer base $b \ge 2$. Every real $x \neq 0$ can be written uniquely as $|x| = m \cdot b^{e}$ with significand $m \in [1, b)$ and $e \in \mathbb{Z}$. The leading digit of $x$ is $D_b(x) = \lfloor m \rfloor \in \{1,\dots,b-1\}$. Equivalently, with $\{t\} = t - \lfloor t \rfloor$ the fractional part,

$$D_b(x) = \left\lfloor b^{\{\log_b |x|\}} \right\rfloor .$$

More generally, the integer formed by the first $k$ significant digits is $\lfloor b^{\{\log_b|x|\} + k - 1}\rfloor$, and the $n$-th significant digit is that integer for $k=n$ reduced modulo $b$.

The Benford probabilities are

$$P_b(d) = \log_b(d+1) - \log_b d = \log_b\!\left(1 + \frac1d\right), \qquad d = 1, \dots, b-1 .$$

A real sequence $(a_n)_{n \ge 0}$ satisfies Benford's law in base $b$ if for every digit $d \in \{1,\dots,b-1\}$

$$\lim_{N\to\infty} \frac{\#\{0 \le n < N : D_b(a_n) = d\}}{N} = P_b(d).$$

A positive random variable $X$ satisfies the strong form of the law if $\{\log_b X\}$ is uniformly distributed on $[0,1)$.

Formalization targets

Goal — powers of $k$ (Note 3 of the source)

For every natural number $k$ such that $\log_{10} k$ is irrational, the sequence $k^1, k^2, k^3, \dots$ satisfies Benford's law in base $10$:

$$\lim_{N\to\infty}\frac{\#\{1\le n\le N : D_{10}(k^n)=d\}}{N}=\log_{10}\!\left(1+\frac1d\right)\quad (d=1,\dots,9).$$

Milestones

1. The Benford probabilities in base $b$ sum to $1$.
2. $D_b(x) = d$ if and only if $\log_b d \le \{\log_b x\} < \log_b (d+1)$.
3. Strong form $\Rightarrow$ first-digit law, in every base $b \ge 2$.
4. In base $2$ every nonzero number has leading digit $1$.
5. The powers of $2$ satisfy Benford's law.
6. The Fibonacci numbers satisfy Benford's law.
7. The factorials satisfy Benford's law.
8. Exponential growth or decay $C e^{rt}$ ($r\ne 0$) spends an asymptotic fraction $\log_{10}(1+1/d)$ of its time with leading digit $d$.
9. A scale-invariant first-digit distribution is the Benford distribution.
10. Under the strong form, the first $k$ digits form the integer $n$ with probability $\log_{10}(1+1/n)$.
11. Under the strong form, the $n$-th digit ($n \ge 2$) equals $d$ with probability $\sum_{k=10^{n-2}}^{10^{n-1}-1}\log_{10}\!\left(1+\frac{1}{10k+d}\right)$.
12. That $n$-th-digit probability tends to $1/10$.
13. The Benford first-digit distribution has mean $3.440$ and variance $6.057$ (to three decimals).
14. The reciprocals $1/n$ and the square roots $\sqrt n$ of the natural numbers do not satisfy Benford's law.

Significance

The goal is the cleanest instance of the mechanism behind Benford's law: a sequence obeys the law exactly when the fractional parts of its base-$10$ logarithms are equidistributed modulo $1$, and for $k^n$ those fractional parts are the multiples $n\log_{10}k$ reduced modulo $1$. The milestones cover the rest of the mathematical content of the article: the definition and normalization of the law, the derivation from a log-uniform significand, the generalization to several leading digits and to the $n$-th digit, scale invariance, the continuous-time exponential case, and the negative results for $1/n$ and $\sqrt n$.

All of these results are classical and proved in the literature cited above; the work here is formalizing the known proofs. Related entries already on the platform (a leading-digit / fractional-part characterization and an equidistribution-based Benford criterion, stated with different definitions) may be reusable by solvers.

Difficulty

The goal and milestones 5–7 reduce to equidistribution of a sequence modulo $1$. For $k^n$ and Fibonacci numbers this is Weyl's equidistribution theorem for irrational rotations (Fibonacci additionally needs Binet's formula and an error term that vanishes). Factorials are harder: $\log_{10} n!$ is not a linear sequence, and the classical proof combines Stirling's formula with an equidistribution criterion for sequences whose differences vary slowly. The scale-invariance theorem requires a Fourier-analytic argument on the circle $\mathbb{R}/\mathbb{Z}$. The negative results require showing that a counting ratio oscillates, which needs explicit lower and upper estimates along two subsequences.

Formalization scope

• Digits are defined through real logarithms: $D_b(x) = \lfloor b^{\{\log_b x\}} \rfloor$. Lean's Real.logb takes $\log_b|x|$, so negative numbers get the leading digit of their absolute value, and the junk value $D_b(0) = 1$ occurs. Every statement either restricts to positive (or nonzero) inputs or only uses positive sequences.
• Sequences are indexed from $n=0$; "the sequence $k^1, k^2, \dots$" is encoded as $a_n = k^{n+1}$, the Fibonacci numbers as $F_{n+1}$ and the factorials as $(n+1)!$.
• The asymptotic frequency is a natural density over $\{0,\dots,N-1\}$; "satisfies Benford's law" requires convergence for every digit $1\le d<b$.
• The strong form is encoded as: $X$ measurable, $X>0$ almost surely, and the pushforward of the probability measure under $\omega \mapsto \{\log_b X(\omega)\}$ equals Lebesgue measure restricted to $[0,1)$ (this forces the underlying measure to have total mass $1$).
• Moments are stated to three decimals, matching the source's rounding: $|\mathrm{mean} - 3.440| < 0.0005$ and $|\mathrm{variance} - 6.057| < 0.0005$.
• Not formalized: the empirical claims (tables, applications, statistical tests), Hill's 1995 theorem on random mixtures of distributions, and the Krieger–Kafri entropy explanation; their statements in the source are not precise enough to formalize faithfully.

Reusable infrastructure: leading-digit and significand API, equidistribution of $n\alpha$ modulo $1$ (Weyl), Benford criteria via equidistribution. Contributions toward a general "equidistributed $\{\log_{10} a_n\}$ $\Rightarrow$ Benford" lemma are welcome.

Selected references

• S. Newcomb, Note on the frequency of use of the different digits in natural numbers, American Journal of Mathematics 4 (1881), 39–40. https://doi.org/10.2307/2369148
• F. Benford, The law of anomalous numbers, Proc. Amer. Philos. Soc. 78 (1938), 551–572. https://www.jstor.org/stable/984802
• R. S. Pinkham, On the distribution of first significant digits, Ann. Math. Statist. 32 (1961), 1223–1230. https://doi.org/10.1214/aoms/1177704862
• R. L. Duncan, An application of uniform distribution to the Fibonacci numbers, Fibonacci Quarterly 5 (1967), 137–140. https://doi.org/10.1080/00150517.1967.12431312
• L. C. Washington, Benford's law for Fibonacci and Lucas numbers, Fibonacci Quarterly 19 (1981), 175–177. https://doi.org/10.1080/00150517.1981.12430109
• R. A. Raimi, The first digit problem, American Mathematical Monthly 83 (1976), 521–538. https://doi.org/10.2307/2319349
• T. P. Hill, A statistical derivation of the significant-digit law, Statistical Science 10 (1995), 354–363. https://doi.org/10.1214/ss/1177009869
• T. P. Hill, The significant-digit phenomenon, American Mathematical Monthly 102 (1995), 322–327. https://doi.org/10.1080/00029890.1995.11990578
• A. Berger, T. P. Hill, The mathematics of Benford's law: a primer, Stat. Methods Appl. 30 (2021), 779–795. https://arxiv.org/abs/1909.07527
• Wikipedia, Benford's law. https://en.wikipedia.org/wiki/Benford%27s_law

Motivation

Value-at-Risk (VaR) is the regulatory risk measure for banking and insurance capital: it is the quantile of a loss distribution at a fixed tail probability. Two questions arise when several agents use it. First, risk sharing: if an aggregate loss $X$ is split among agents $i=1,\dots,n$, each measuring its share with its own risk measure, what is the smallest total risk the group can achieve and which split achieves it? Second, model uncertainty: an agent rarely knows the distribution of a loss exactly, and a common response is to evaluate the worst case over all distributions close to an estimate, here in the sense of the Wasserstein distance used in distributionally robust optimization (Esfahani and Kuhn, 2018).

F. Liu, T. Mao, R. Wang and L. Wei, Inf-Convolution, Optimal Allocations, and Model Uncertainty for Tail Risk Measures (Mathematics of Operations Research, 2022; the version used here is the authors' SSRN copy 3490348 of January 16, 2022, ssrn.com/abstract=3490348), combine the two questions. When each agent uses a Wasserstein-robust VaR and the split must be comonotonic (every share increases with the total, the usual requirement in insurance), their Theorem 6 gives the optimal total risk in closed form and shows that one agent should carry the entire loss.

Setting

Fix an atomless probability space $(\Omega,\mathcal F,\mathbb P)$: every event of positive probability contains an event of strictly smaller positive probability. A random variable $X$ is a loss, with distribution function $F_X(x)=\mathbb P(X\le x)$. The domain is $\mathcal X=L^\infty$, the essentially bounded measurable random variables.

For $\alpha\in(0,1)$ the left and right Value-at-Risk are

$$\mathrm{VaR}^L_\alpha(X)=\inf\{x: F_X(x)\ge1-\alpha\},\qquad \mathrm{VaR}^R_\alpha(X)=\inf\{x: F_X(x)>1-\alpha\},$$

so a small $\alpha$ looks far into the tail of the loss. $\Lambda\in\{L,R\}$ selects one of the two.

The Wasserstein metric of order $k\ge1$ between $X$ and $Y$ with quantile functions $F^{-1}$ and $G^{-1}$ is

$$W_k(X,Y)=\Big(\int_0^1|F^{-1}(x)-G^{-1}(x)|^k\,\mathrm dx\Big)^{1/k},$$

and the robust version of a risk measure $\rho$ at radius $\delta>0$ is

$$[\rho]^k_\delta(X)=\sup\{\rho(Y): Y\in L^\infty,\ W_k(Y,X)\le\delta\}.$$

Two random variables $X,Y$ are comonotonic if $(X(\omega)-X(\omega'))(Y(\omega)-Y(\omega'))\ge0$ for all $\omega,\omega'$ in an event of probability one. The comonotonic allocations of $X$ among $n$ agents are

$$\mathbb A^+_n(X)=\{(X_1,\dots,X_n)\in(L^\infty)^n: X_1+\dots+X_n=X,\ X_i \text{ comonotonic with } X\},$$

and the constrained inf-convolution of $\rho_1,\dots,\rho_n$ is $\boxplus_{i=1}^n\rho_i(X)=\inf\{\sum_i\rho_i(X_i):(X_1,\dots,X_n)\in\mathbb A^+_n(X)\}$. An allocation attaining the infimum is optimal.

Formalization targets

Goal: Theorem 6 (p. 31)

Let $X\in L^\infty$ and $\Lambda\in\{L,R\}$.

(i) If $0<\delta_1\le\dots\le\delta_n$ and $\alpha\in(0,1)$, then

$$\mathop{\boxplus}_{i=1}^n[\mathrm{VaR}^\Lambda_\alpha]^1_{\delta_i}(X)=[\mathrm{VaR}^\Lambda_\alpha]^1_{\delta_1}(X)+\sum_{i=2}^n\frac{\delta_i}{\alpha}.$$

(ii) If $1>\alpha_1\ge\dots\ge\alpha_n>0$ and $\delta>0$, then

$$\mathop{\boxplus}_{i=1}^n[\mathrm{VaR}^\Lambda_{\alpha_i}]^1_{\delta}(X)=[\mathrm{VaR}^\Lambda_{\alpha_1}]^1_{\delta}(X)+\sum_{i=2}^n\frac{\delta}{\alpha_i}.$$

In either case $(X,0,\dots,0)$ is an optimal comonotonic allocation.

Milestones

1. Proposition 4(iii), (34)–(35), p. 30. For $k\ge1$, $\delta>0$, $\alpha\in(0,1)$: $[\mathrm{VaR}^L_\alpha]^k_\delta(X)=[\mathrm{VaR}^R_\alpha]^k_\delta(X)=x$, where $x$ is the unique solution of $\int_0^\alpha(x-\mathrm{VaR}^R_u(X))_+^k\,\mathrm du=\delta^k$, and $[\mathrm{VaR}^R_\alpha]^k_\delta(X)\ge\mathrm{VaR}^R_\alpha(X)+\delta/\alpha^{1/k}$.
2. (40), p. 31. With $V_\delta=[\mathrm{VaR}^L_\alpha]^1_\delta$: $V_\delta(Y)\le0$ if and only if $\int_0^\alpha(-\mathrm{VaR}^L_u(Y))_+\,\mathrm du\ge\delta$.
3. (39), p. 31. For $\delta_1\le\delta_2$: $V_{\delta_1}\boxplus V_{\delta_2}(X)\le V_{\delta_1}(X)+\delta_2/\alpha$, through the allocation $(X+\delta_2/\alpha,\,-\delta_2/\alpha)$.
4. (38), p. 31. For $\delta_1\le\delta_2$: $V_{\delta_1}\boxplus V_{\delta_2}(X)=V_{\delta_1}(X)+\delta_2/\alpha$.
5. (41), p. 33. For $\lambda\ge1$ with $\lambda\alpha<1$: $[\mathrm{VaR}^\Lambda_\alpha]^1_\delta\ge[\mathrm{VaR}^\Lambda_{\lambda\alpha}]^1_{\lambda\delta}$ on $L^\infty$.

Significance

The theorem is one of the few explicit solutions of a risk-sharing problem with model uncertainty and non-convex agents. Without uncertainty, the inf-convolution of VaRs is a VaR at the summed level (Theorem 1 of the same paper), and its optimal allocations split the tail of the loss across agents. Under Wasserstein uncertainty and a comonotonicity constraint the structure changes: the optimum concentrates the whole loss on the agent least sensitive to uncertainty when the levels agree, or least sensitive to risk when the radii agree, and the remaining agents hold only cash. In particular the equal split $(X/n,\dots,X/n)$, optimal for identical convex risk measures, is in general not optimal here. Proposition 4(iii) is independently useful: it computes the worst-case VaR over a one-dimensional Wasserstein ball of any order and shows that left and right VaR coincide after robustification.

The results are proved in the paper. As far as is known, none of them has a machine-checked proof; this mission produces the first formal statements and, eventually, proofs. The quantile-based Wasserstein metric, the robust risk measure and the comonotonic inf-convolution are reusable objects for further work on robust risk measures.

Difficulty

The upper bound is a direct computation with one explicit allocation. The lower bound is the hard part. VaR is not convex, so the duality arguments that solve the inf-convolution of convex risk measures do not apply, and the robust VaR is not a distortion risk measure to which the Expected Shortfall formula of Proposition 4(ii) applies. The paper itself notes (p. 30) that the inf-convolution of robust VaRs over all allocations is hard to compute because VaR lacks convexity, and obtains only two-sided bounds there, which are generally not sharp. The explicit formula of Theorem 6 depends on the comonotonicity constraint, on the order $k=1$, and on the agents sharing either the level or the radius; the paper states it only under these assumptions, and the ordering of the radii or levels is necessary for the identity as written, since it singles out the agent who carries the loss. For Proposition 4(iii), the supremum over the ball is a supremum over distributions, and identifying it with a real number requires realising worst-case distributions as random variables on the given space, which is where atomlessness is used.

Formalization scope

Random variables are functions $\Omega\to\mathbb R$; $L^\infty$ is the set of measurable, almost surely bounded functions, with no quotient. The probability measure is atomless in the splitting sense. The quantile function is $F^{-1}_X(x)=\mathrm{VaR}^L_{1-x}(X)$, and the Wasserstein integral is the interval integral over $[0,1]$; for $X,Y\in L^\infty$ its integrand is bounded and monotone on $(0,1)$, so the integral is the paper's. The supremum in the robust measure ranges over $Y\in L^\infty$ only, as in the paper. It is a real supremum: the set is nonempty since it contains $\rho(X)$, and for VaR its boundedness from above is part of the statement of Proposition 4(iii), so no junk value enters. Allocation constraints $\sum_iX_i=X$ hold pointwise. The constrained inf-convolution is valued in the extended reals. The $n=m+1$ agents are indexed by Fin (m+1), so $n\ge1$; the orderings of the radii and of the levels are hypotheses, since without them the identities fail. Theorem 6 is stated for order $k=1$; Proposition 4(iii) for every real $k\ge1$. The single implicit hypothesis made explicit is $\lambda\alpha<1$ in (41), which keeps the VaR level in $(0,1)$.

A formalization in which the robust supremum ranges over all measurable functions, or over an unbounded set where the real supremum is $0$, would make the identities trivial or false; both are excluded by the definitions above.

The development needs: quantile functions of bounded random variables and their monotonicity; the existence on an atomless space of a random variable with a prescribed quantile function; comonotonic additivity of VaR; and the interval-integral calculus for monotone integrands. Contributions of general lemmas on quantile functions and on one-dimensional Wasserstein distances are welcome and reusable beyond this mission.

Selected references

• F. Liu, T. Mao, R. Wang, L. Wei, Inf-Convolution, Optimal Allocations, and Model Uncertainty for Tail Risk Measures, Mathematics of Operations Research, 2022; SSRN version of January 16, 2022. https://ssrn.com/abstract=3490348 , https://doi.org/10.1287/moor.2021.1217
• P. Embrechts, H. Liu, R. Wang, Quantile-based risk sharing, Operations Research 66(4), 2018. https://doi.org/10.1287/opre.2017.1716
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1
• J. Dhaene, S. Vanduffel, M. Goovaerts, R. Kaas, Q. Tang, D. Vyncke, Risk measures and comonotonicity: a review, Stochastic Models 22(4), 2006. https://doi.org/10.1080/15326340600878016