All missions

Motivation

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

Setting

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

Formalization targets

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

Bivariate joint distribution and boundary constraints

Two exchangeable uniform loss lines have symmetric FGM dependence.

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

Rectangle probability, Fréchet bounds and copula construction

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

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

Independent and dependent upper-tail co-exceedance

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

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

Capstone theorem

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

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

Significance

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

Difficulty

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

Formalization scope

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

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

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

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

Motivation

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

Setting

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

Formalization targets

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

Entry age, attained age and liability allocation

Annual attained normal cost equals rate times current pensionable earnings.

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

Aggregate funding and deficit amortisation

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

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

Fund asset rollforward and exact surplus attribution

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

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

Capstone theorem

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

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

Significance

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

Difficulty

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

Formalization scope

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

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

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

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

Motivation

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

Setting

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

The central actuarial model can be written

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

Formalization targets

Actual joint-lifetime events and cause partition

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

Independent-shock Marshall–Olkin survivor law

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

Cause-contingent actuarial benefits and dependence

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

Capstone theorem

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

Setting

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

Formalization targets

Aggregate loss and the net profit condition

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

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

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

Exponential claim transform and adjustment coefficient

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

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

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

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

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

Candidate ruin function and renewal equation

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

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

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

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

Motivation

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

Setting

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

Formalization targets

Conservative three-state transition rates

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

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

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

Exact continuous-time survival

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

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

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

Prospective reserve and Thiele equation

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

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

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

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

This entry lowers the sufficient exponent cutoff for the sharp diagonal Hlawka formula from 63 to 62. For every real $p\ge 62$, the foundation's unchanged cyclic constant is the least constant comparing the triple deficit with the pair-deficit sum for every complex coordinate triple in every finite dimension.

The statement includes unequal and zero input vectors and dimension zero. It concerns complex diagonal matrices through their coordinate norms. It does not settle the conjectured cutoff 2 or the full noncommutative matrix problem.

Goal and companion

• Exact complex cutoff 62 goal, proved.
• Real coordinate bound for $p\ge 62$, the supporting milestone, proved.

The confinement radius on this integer is $3643/10000$. The accepted cutoff-$63$ theorem remains the tail this argument calls. Cutoffs 64, 65, 66, and 70 stay proved and are not restated here.

This is the last integer this confinement argument reaches. At $p=61$ every radius whose tangent model stays positive already makes the budget-$7$ box factor larger than $1$.

Motivation

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

Setting

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

Formalization targets

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

Premium and claim surplus cash-flow recursion

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

Representative theorem `ActuarialValuation.ruNetClaimTotal_reconcile`:

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

Surplus is opening capital minus cumulative net claims.

First passage and deficit at ruin

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

Representative theorem `ActuarialValuation.ruCumulativeMargin_eq_surplus`:

$$M_n=U_n$$

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

Stop-loss reinsurance, retained deficit and pathwise capital

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

Representative theorem `ActuarialValuation.ruRuinDeficit_fundamental`:

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

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

Capstone theorem

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

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

Significance

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

Difficulty

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

Formalization scope

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

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

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

Motivation

Multi-state actuarial models capture payments depending on whether an insured person is active, disabled or exited, and on transitions between these statuses. Promislow's Fundamentals of Actuarial Mathematics (2015), Chapter 19 studies nonstationary Markov chains, continuous transition forces, reserve equations and semi-Markov models. Dickson, Hardy and Waters (2009), Chapter 8 provides an actuarial multiple-state foundation. Earlier formal missions cover finite transition recursions and disability-state benefit valuation; this extension concentrates on transition-mass conservation, two-period nonstationary composition and explicit sojourn-duration resets needed for semi-Markov policies.

Setting

A three-state transition model represents active, disabled and exited statuses, with finite conditional matrix T(i,j) and beginning-of-year state mass p(i). The outgoing row mass must be one and probabilities nonnegative for a valid stochastic model; the total state mass is preserved when these assumptions hold. A second transition matrix U may differ from T, allowing a nonstationary model. The Chapman-Kolmogorov two-period distribution is (pT)U=p(TU). Benefits may depend on the destination state or the exact ordered pair of origin and destination states. The one-period actuarial reserve comprises current-year state benefit plus a discounted conditional mean of next-period liabilities.

Formalization targets

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

Finite-state transition and probability conservation

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

Representative theorem `ActuarialValuation.msApplyTwo_mass`:

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

Two successive stochastic transition years conserve total cohort probability.

Transition benefits, annual reserve values and profit

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

Representative theorem `ActuarialValuation.msNetProfit_reconcile`:

$$Π+E+C=P$$

Premium allocation exactly partitions earnings, expenses and expected claims.

Duration-dependent semi-Markov disability and exit valuations

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

Representative theorem `ActuarialValuation.msMultiStateReserves_fundamental`:

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

The capstone couples exact stochastic population conservation, the full non-stationary Chapman-Kolmogorov identity, origin-state prospective reserve valuation and the duration-sensitive semi-Markov specialisation.

Capstone theorem

The main target is `ActuarialValuation.msMultiStateReserves_fundamental`. The capstone couples exact stochastic population conservation, the full non-stationary Chapman-Kolmogorov identity, origin-state prospective reserve valuation and the duration-sensitive semi-Markov specialisation.

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

Significance

The published semi-Markov insurance model emphasises duration dependence, surrender and paid-up transitions rather than forcing every policyholder into a Markov model. The mission introduces sojourn duration d explicitly: remaining in state i gives d+1, while entering a different state resets duration to zero. This changes which next-period reserve V(j,d') should be valued. A precise difference theorem shows how changing elapsed duration changes actuarial reserves through a changed conditional transition law. The fixed-duration Markov case is recovered without assuming all semi-Markov contracts have duration-independent cash flows.

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

Difficulty

A complete row stochastic matrix is necessary for mass conservation, and each conditional transition probability is separately nonnegative. Chapman-Kolmogorov must sum over all intermediate states, including absorbing exits, without assuming T=U. The reserve is sensitive to payment timing: a current cashflow at the valuation instant is not discounted but future continuation reserves are. Disability benefits can vary with duration; reset occurs on actual state change rather than at every new policy year. Continuous-time generator differential equations are intentionally not claimed by this discrete-time Lean 4 model. This is a formal finite base for downstream generator and Thiele analysis with targeted Mathlib finite-sum imports.

Formalization scope

The mission formalizes finite nonstationary three-state Markov and duration-dependent semi-Markov one-step reserve relations with genuine probability-weighted cashflows. It excludes the vacuous substitution of a claimed identity as a model assumption: mass preservation is derived from row normalisation, and two-step propagation is reconciled by rearranging real finite sums. The theorem graph does not assert that disability and recovery rates can be recovered from incomplete cohort tables without assumptions or that a discrete reserve equation proves a continuous Thiele ODE. It prepares such future stochastic extensions with explicit sojourn-duration changes.

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

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

Motivation

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

Setting

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

Formalization targets

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

Finite count, severity and convolution transforms

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

Representative theorem `ActuarialValuation.cxSecondMoment_succ`:

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

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

Bernoulli claim counts, zero claims and aggregate moments

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

Representative theorem `ActuarialValuation.cxTwoClaimMoment_two_decomposition`:

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

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

Panjer adjustment with mass at zero

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

Representative theorem `ActuarialValuation.cxCompoundRisk_fundamental`:

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

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

Capstone theorem

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

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

Motivation

Kramers–Wannier duality was found in 1941 as a map between the high- and low-temperature phases of the two-dimensional Ising model (Kramers–Wannier 1941). In its quantum form it exchanges the transverse field $X_j$ and the nearest-neighbour coupling $Z_{j-1}Z_j$ of the transverse-field Ising chain, and it fixes the critical point. In conformal field theory it is implemented by a topological defect line (Fröhlich–Fuchs–Runkel–Schweigert 2004), the prototypical non-invertible symmetry: its fusion with itself is a sum of operators, not a single invertible one (Shao, TASI lectures 2023).

On a finite periodic chain the duality cannot be a unitary operator, because it maps the $\mathbb Z_2$-even sector to itself and annihilates the odd sector. Seiberg–Shao 2023 and Seiberg–Seifnashri–Shao 2024 wrote the exact lattice operator $\mathsf D$ on the tensor-product Hilbert space $(\mathbb C^2)^{\otimes L}$. They showed that its algebra closes only after the lattice translation is included: $\mathsf D^2=(1+\eta)T^{-1}$. This is a lattice relation that a fusion category does not describe, since the continuum fusion rule $\mathcal N^2=1+\eta$ appears only at low energy. The same identity drives the LSM-type constraint proved in that paper.

Timeline. 1941: Kramers and Wannier find the duality of the 2D Ising model. 2004: Fröhlich, Fuchs, Runkel and Schweigert realise it as a conformal defect. 2016: Aasen–Mong–Fendley construct the lattice defects. 2023–2024: Seiberg, Seifnashri and Shao find the exact operator algebra on the tensor-product Hilbert space, including the translation factor.

Setting

Fix $L\ge1$ qubits on a ring, with site indices in $\mathbb Z/L$ (Fin L with modular arithmetic). A computational-basis state is labelled by a configuration $s=(s_0,\dots,s_{L-1})\in(\mathbb Z/2)^L$ (Config L). Operators are complex $2^L\times2^L$ matrices indexed by configurations (Op L). Write $\operatorname{sgn}(a)=(-1)^a$.

• Pauli operators. $X_j|s\rangle=|s+e_j\rangle$ flips spin $j$ (pauliX), and $Z_j|s\rangle=(-1)^{s_j}|s\rangle$ (pauliZ).
• $\mathbb Z_2$ symmetry. $\eta=\prod_j X_j$ flips every spin (eta).
• Translation. $T|s\rangle=|s'\rangle$ with $s'_k=s_{k-1}$ (transl), so that $TX_jT^{-1}=X_{j+1}$.
• Kramers–Wannier operator (kwD):

$$\langle t|\,\mathsf D\,|s\rangle \;=\; 2^{-L/2}\,(-1)^{\sum_{k} t_k\,(s_k+s_{k+1})}.$$

This explicit formula is the definition used throughout. Relations (1.5) together with $\mathsf D\eta=\mathsf D$ determine $\mathsf D$ up to a scalar, and (1.4) fixes the scalar up to a sign. Every statement below is invariant under $\mathsf D\mapsto-\mathsf D$, so this is the operator of Seiberg–Seifnashri–Shao in that paper's normalisation (footnote 1). Its equality with their matrix-product presentation (2.64) is not formalised here.

Formalization targets

Goal: the non-invertible fusion rule (eqs. (1.4), (2.65), (F.18))

$$\mathsf D^2=(1+\eta)\,T^{-1}\qquad\text{for every }L\ge1 .$$

Milestones

1. Invertible algebra (eqs. (1.1)–(1.3), (2.10), (2.65)): $\eta^2=1$, $T\eta=\eta T$, $T^L=1$, $TX_jT^{-1}=X_{j+1}$, $TZ_jT^{-1}=Z_{j+1}$, $\eta X_j=X_j\eta$, $\eta Z_j=-Z_j\eta$.
2. Duality on $X$ (eq. (1.5)): $\mathsf D X_j=Z_{j-1}Z_j\,\mathsf D$.
3. Duality on $ZZ$ (eq. (1.5)): $\mathsf D Z_{j-1}Z_j=X_{j-1}\,\mathsf D$.
4. Absorbing $\eta$ (eqs. (1.4), (2.65)): $\mathsf D\eta=\eta\mathsf D=\mathsf D$.
5. Translation and adjoint (eq. (2.65), Table 1): $T\mathsf D=\mathsf DT$ and $\mathsf D^\dagger=\mathsf DT$.
6. Non-invertibility (§1.1): $\mathsf D$ is not a unit, and $\ker\mathsf D\neq0$.

Significance

The result. The goal identity is the defining relation of the lattice Kramers–Wannier symmetry. Together with milestones 4–5 it shows that $\mathsf D/\sqrt2$ restricted to the $\eta$-even sector squares to a translation, so $\mathsf D$ is a square root of $T^{-1}$ there. The paper uses this to derive its LSM-type constraint, and also to show that the lattice symmetry is not a fusion category, because the continuum rule $\mathcal N^2=1+\eta$ only emerges at low energy. Milestones 2–3 are the lattice Kramers–Wannier map on $\mathbb Z_2$-invariant operators, so $\mathsf D$ commutes with the critical Ising Hamiltonian $H=-\sum_j(Z_{j-1}Z_j+X_j)$.

Formalizing it. The identities are proved in the physics literature by tensor-network manipulations ((F.14)–(F.18)) and checked numerically, but none of this is machine-checked. This mission produces a reusable Lean setup for qubit chains: Pauli strings on $(\mathbb Z/2)^L$, $\mathbb Z_2$ and translation symmetries, and an exact non-invertible operator with its full operator algebra for every chain length. No mission on the platform or file in Mathlib currently formalizes a non-invertible lattice symmetry.

Difficulty

Each identity is easy to check for a fixed small $L$ by brute force. The content is that it holds for all $L$ at once, on a $2^L$-dimensional space. The difficulty is bookkeeping with periodic indices: sums over $(\mathbb Z/2)^L$ of characters $(-1)^{\langle t,\,\cdot\rangle}$, reindexing $k\mapsto k\pm1$ in Fin L (including $L=1$, where $k+1=k$, and $L=2$, where $k+1=k-1$), and the exact normalisation $2^{-L/2}$, so that the right-hand side carries no stray factor $2^L$. The goal also involves the matrix inverse $T^{-1}$, so a proof must establish that $T$ is invertible rather than rely on Lean's junk value.

Formalization scope

• Representation. Operators are Matrix (Fin L → ZMod 2) (Fin L → ZMod 2) ℂ; products are matrix products; $T^{-1}$ is Mathlib's matrix inverse (transl L)⁻¹; $\dagger$ is conjTranspose. Every theorem assumes [NeZero L], i.e. $L\ge1$.
• Conventions committed to. $Z_j=(-1)^{s_j}$ on basis states, translation to the right ($s'_k=s_{k-1}$), and $\mathsf D$ normalised by $2^{-L/2}$ as in eqs. (1.4)/(2.65). Other conventions (left translation, unnormalised $\mathsf D$) change the statements to $T$ instead of $T^{-1}$ or add a factor $2^L$; the conventions here reproduce the paper's equations verbatim.
• No trivialisation. kwD is an explicit formula, not a hypothesis. The goal fixes both sides completely, and milestone 1 pins the translation convention against eq. (2.10).
• Out of scope. The defect Hamiltonians, the MPO presentation (2.64) itself, the $\mathbb Z_2$- and duality-twisted operators of §§2.3.3–2.3.4, and the LSM constraint of §4.
• Reusable. Pauli operators, translation and $\eta$ on qubit chains; character-sum lemmas over $(\mathbb Z/2)^L$. Contributions of general Mathlib lemmas on Walsh–Hadamard-type sums are welcome.

Selected references

• H. A. Kramers, G. H. Wannier, Statistics of the Two-Dimensional Ferromagnet. Part I, Phys. Rev. 60, 252–262 (1941). doi:10.1103/PhysRev.60.252
• J. Fröhlich, J. Fuchs, I. Runkel, C. Schweigert, Kramers–Wannier duality from conformal defects, Phys. Rev. Lett. 93, 070601 (2004). arXiv:cond-mat/0404051
• D. Aasen, R. S. K. Mong, P. Fendley, Topological Defects on the Lattice I: The Ising model, J. Phys. A 49, 354001 (2016). arXiv:1601.07185
• N. Seiberg, S.-H. Shao, Majorana chain and Ising model – (non-invertible) translations, anomalies, and emanant symmetries, SciPost Phys. 16, 064 (2024). arXiv:2307.02534
• S.-H. Shao, What's Done Cannot Be Undone: TASI Lectures on Non-Invertible Symmetries (2023). arXiv:2308.00747
• Source: N. Seiberg, S. Seifnashri, S.-H. Shao, Non-invertible symmetries and LSM-type constraints on a tensor product Hilbert space, SciPost Phys. 16, 154 (2024). arXiv:2401.12281

Motivation

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

Setting

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

The central actuarial model can be written

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

Formalization targets

Deterministic zero-coupon bonds and forward discounts

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

Coupon-bond cashflows duration and flat yield

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

Finite-state stochastic discount factors and arbitrage-free valuation

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

Capstone theorem

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

Setting

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

Formalization targets

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

Salary scales, average pay and fractional service

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

Representative theorem `ActuarialValuation.pen9MidyearPension_delta`:

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

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

DC accumulation and replacement-ratio annuity funding

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

Representative theorem `ActuarialValuation.pen9TargetCapital_annuity_monotone`:

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

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

Service-table exits, survivor and deferred benefits

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

Representative theorem `ActuarialValuation.pen9AnnualExitPV_nonneg`:

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

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

Projected versus traditional unit credit and reserve recursion

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

Representative theorem `ActuarialValuation.pen9PensionFunding_fundamental`:

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

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

Capstone theorem

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

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

Significance

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

Difficulty

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

Formalization scope

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

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

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

Motivation

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

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

Setting

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

Let the pre-insurance earned account be

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

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

Formalization targets

Monthly account premium expenses and insurance charges

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

Type A and B mortality strain and explicit guarantee

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

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

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

Path-dependent account evolution and stochastic guarantee pricing

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

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

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

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

Capstone theorem

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

Significance

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

Formalization targets

Actual finite loss distributions and scenario ambiguity

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

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

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

Coherent worst-case actuarial premium and portfolio

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

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

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

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

Stop-loss risk comparison and limitations of floored risk principles

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

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

Capstone theorem

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

Significance

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

Motivation

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

Setting

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

The central actuarial model can be written

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

Formalization targets

Finite probability martingales and bounded stopping

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

Actuarial surplus and exponential supermartingale

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

Ruin events and finite-horizon Lundberg bound

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

Capstone theorem

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

Selected references

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

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