All missions

Motivation

A gauge theory can be formulated in several mathematically different ways: with potentials (connections), with field strengths (curvature), or with holonomies, the parallel transports around closed loops. Philosophers and physicists ask whether these formulations say the same thing, and which one carries "surplus structure".

Category theory makes the question precise. Each formulation is a category of models, and each translation between formulations is a functor. A functor that is faithful and essentially surjective but not full forgets structure. One that is full and faithful but not essentially surjective forgets properties. One that is full and essentially surjective but not faithful forgets stuff. One that is all three forgets nothing and is an equivalence. This taxonomy is due to Baez, Bartels and Dolan (Baez–Shulman, §2.4).

Weatherall (2016) applied it to electromagnetism. Potentials without gauge arrows forget structure relative to field strengths (Proposition 1). The erratum in arXiv v2 (p. 15) corrects his Proposition 2: the principal-bundle formulation, whose arrows include gauge transformations, forgets only stuff, not nothing. Nguyen, Teh and Wells obtain the same verdict for the gauge-orbit functor (their Proposition 3.2.3). In their footnote 26 they identify the forgotten stuff as the constant ("global") gauge transformations. All of this is abelian, U(1) on a contractible spacetime.

The non-abelian counterpart is the holonomy formulation. Barrett's reconstruction and representation theorems, and their categorical upgrade by Rosenstock and Weatherall (Theorem 2), show that on a connected manifold, principal connections and generalized holonomy maps form equivalent categories. On the topological side, Freed and Quinn (eqs. 3.11–3.13) identify the automorphisms of a finite-group gauge field with a centralizer.

This mission states these results for an arbitrary group $G$ on a finite graph. There the smooth and topological subtleties disappear, but the categorical content survives intact.

Setting

A finite directed graph $X$ has vertices $\mathrm{Fin}\,n_V$, edges $\mathrm{Fin}\,n_E$, and maps $\mathrm{src},\mathrm{tgt}$. A step is an edge traversed forwards or backwards, and a walk $x \to y$ is a list of steps whose endpoints chain. $X$ is connected from $x$ if every vertex is reached by a walk from $x$.

• A connection is $A : E \to G$. Its holonomy along a walk is the ordered product of $A(e)$ (forwards) and $A(e)^{-1}$ (backwards), as in Baez (1996), §2.
• A gauge transformation is $g : V \to G$, acting by $(g\cdot A)(e) = g(\mathrm{src}\,e)\,A(e)\,g(\mathrm{tgt}\,e)^{-1}$.
• $\mathsf{PotG}$: objects are connections, and arrows $A \to B$ are gauge transformations with $g\cdot A = B$. This is the discrete analogue of the groupoid $C_A$ of Nguyen–Teh–Wells.
• $\mathsf{HolMap}_x$: a holonomy map at $x$ assigns a group element to each walk. It is multiplicative on loops at $x$ and unchanged when a backtrack $s, \bar s$ is inserted into a loop at $x$; this is the discrete form of thin equivalence. Arrows $H \to H'$ are elements $h$ with $H'(\gamma) = h\,H(\gamma)\,h^{-1}$ on every loop at $x$. Only values on loops at $x$ matter.
• Functors. $\mathrm{hol}_x : \mathsf{PotG} \to \mathsf{HolMap}_x$ sends $A \mapsto \mathrm{hol}_A$ and $g \mapsto g(x)$. $\mathrm{orbit}$ sends $\mathsf{PotG}$ to the discrete category of gauge orbits.
• Curvature. On a 2-complex, each face has a base vertex and a boundary loop. The curvature functor sends $A$ to the family of conjugacy classes of its face holonomies, which is the gauge-invariant non-abelian field strength.

Formalization targets

Goal: the holonomy functor is an equivalence

$$X \text{ connected from } x \;\Longrightarrow\; \mathrm{hol}_x \text{ is full, faithful and essentially surjective.}$$

This is the discrete, fixed-base-point form of Rosenstock–Weatherall's Theorem 2. In the taxonomy above, potentials-with-gauge and holonomies forget nothing relative to each other. The statement holds for every group $G$, finite or not. The base-point-changing arrows of Rosenstock–Weatherall are not included.

Milestones

1. Faithful. A gauge arrow between two connections is determined by its value at $x$.
2. Full. Every conjugation relating the holonomy maps of $A$ and $B$ is realized by a gauge transformation.
3. Barrett reconstruction. Every holonomy map at $x$ equals $\mathrm{hol}_A$ on all loops at $x$, for some connection $A$.
4. Barrett representation. $\mathrm{hol}_A = \mathrm{hol}_B$ on loops at $x$ iff $B = g\cdot A$ for a gauge transformation with $g(x) = 1$, and that $g$ is unique.
5. Stabilizer = centralizer. Evaluation at $x$ is a bijection from the gauge stabilizer of $A$ onto the centralizer of its holonomies at $x$. This is the non-abelian $H^0$, the discrete form of Freed–Quinn (3.11)–(3.13).
6. The orbit functor forgets only stuff. It is full and essentially surjective. It is faithful iff $X$ has no vertices or $G$ is trivial. This is the discrete form of Nguyen–Teh–Wells Proposition 3.2.3 and of Weatherall's corrected Proposition 2.
7. Aharonov–Bohm. Take $G$ nontrivial, abelian or not. On the boundary of a triangle, which has no faces, the curvature functor is not full: flat connections with different holonomy are not gauge-equivalent. On the filled triangle the curvature functor is full and essentially surjective but not faithful.

Significance

• Equivalence of formulations. The goal says that, once gauge transformations are arrows, the potential and holonomy formulations of non-abelian lattice gauge theory are categorically equivalent. This is the precise sense in which "the physics is in the holonomies".
• Stuff and global symmetry. Milestones 5–6 locate the forgotten stuff exactly. When potentials are compared with gauge-invariant data that lacks arrows, the stuff is the centralizer of the holonomy group, the global gauge symmetry that survives a choice of connection. In the abelian case this is Nguyen–Teh–Wells' footnote 26. In general it is the automorphism group that weights the Dijkgraaf–Witten / Freed–Quinn sum.
• Topology. Milestone 7 shows that on a non-simply-connected graph the curvature formulation also forgets structure. Weatherall's footnote 9 sets this situation aside for Minkowski space.
• Novelty. Each ingredient is classical in some setting. A machine-checked statement of the non-abelian classification on finite graphs, in the language of forgetful functors, does not appear to exist. It is a step towards treating the theories-as-categories programme formally.

Difficulty

• Combinatorics of walks. Lists of steps, their endpoint conditions, and the interaction of concatenation with backtracking all have to be handled explicitly. The goal and Milestones 1–4 need statements about walks between arbitrary vertices, not only loops.
• Essential surjectivity. Reconstruction has to produce a connection from data that is only constrained on loops at one vertex. Connectivity enters non-trivially.
• Faithfulness versus fullness. These use the hypotheses differently, and the boundary cases (empty graph, trivial group) have to be tracked.
• Milestone 7 needs explicit non-equivalences, and so a gauge invariant separating gauge orbits.

Formalization scope

• Graphs. These are finite directed graphs with Fin-indexed cells and are not required to be simple. Loops and multiple edges are allowed. A 2-complex adds faces with a base vertex and a boundary walk proved to be a loop.
• Groups. $G$ is any Group; finiteness is not assumed.
• Holonomy maps. These are functions on all lists of steps whose axioms only constrain loops at $x$. Two maps agreeing on loops are isomorphic in $\mathsf{HolMap}_x$ (via $h = 1$) but need not be equal. Reconstruction is therefore stated on loops.
• Functor properties. These are Mathlib's Functor.Full, Functor.Faithful and Functor.EssSurj. The goal is their conjunction, not an explicitly constructed inverse.
• Excluded. Spacetime symmetries (graph automorphisms), base-point-changing holonomy isomorphisms, and smooth or continuum statements are left out.
• Proved in the definitions. Gauge covariance of holonomy along walks is proved in the definitions file, because the functors require it.

Selected references

• J. O. Weatherall, "Understanding Gauge", Philosophy of Science 83 (2016) 1039–1049. arXiv:1505.02229. arXiv v2 includes the erratum to Proposition 2 (p. 15).
• J. Nguyen, N. J. Teh, L. Wells, "Why surplus structure is not superfluous", British Journal for the Philosophy of Science 71 (2020). arXiv:1712.01228
• S. Rosenstock, J. O. Weatherall, "A categorical equivalence between generalized holonomy maps on a connected manifold and principal connections on bundles over that manifold", J. Math. Phys. 57 (2016) 102902. arXiv:1504.02401
• D. S. Freed, F. Quinn, "Chern–Simons theory with finite gauge group", Comm. Math. Phys. 156 (1993) 435–472. arXiv:hep-th/9111004
• J. C. Baez, M. Shulman, "Lectures on n-categories and cohomology", in Towards Higher Categories, Springer (2010) 1–68. arXiv:math/0608420
• J. C. Baez, "Spin network states in gauge theory", Adv. Math. 117 (1996) 253–272. arXiv:gr-qc/9411007

Motivation

The established IFoA actuarial mathematics syllabus discusses the relevant mathematics (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). CM1 actuarial foundations form the mathematical background. Continuous-time reserves connect mortality and financial discounting to the dynamics of insurance liabilities. The standard Thiele differential equation is a recognised result in actuarial mathematics and describes the effect of mortality death strain, premium income and interest force on prospective policy reserves. A significant missing foundation of the preceding primarily discrete-time missions is the exact analytic relationship between a closed-form constant-force reserve and its differential equation. The Oxford actuarial reserve lectures and the Encyclopedia of Mathematics give independent descriptions of the equation.

Setting

Exact actuarial equivalence is conditional on the stated model assumptions. The previously known actuarial mathematics in the published textbooks motivates these original-derived Lean targets. They remain unproved until real theorem solutions are accepted. Nontrivial cashflow and probability examples exclude vacuous zero-benefit substitutes, and the resulting identities can support future actuarial missions.

An insured is alive at valuation time t, with term insurance expiring at time T. A death benefit B is payable immediately upon death within the contract term. Continuous premiums arrive at annual rate P while the insured is alive. The mortality force μ and financial interest force δ are constant. Survival over u years is exp(-μu), financial discount is exp(-δu), and their product discounts by exp(-(δ+μ)u). The combined force k=δ+μ must be strictly positive for the capstone's conventional closed-form quotient. The prospective reserve at time t is V(t)=(μB-P)(1-exp(-k(T-t)))/k for 0≤t≤T.

Formalization targets

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

Continuous survival and discount

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

$$\delta,t\ge0\Rightarrow v(t)\le1$$

Nonnegative interest force implies ordinary discount factors no greater than one.

Insurance net outgo and prospective reserves

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

$$B=0\Rightarrow V'=(\delta+\mu)V+P$$

Without insurance benefit, reserve drift includes only premium and liability unwind.

Valuation of continuous benefits

This block contributes 11 theorem targets and 2 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.cm1ThieleContinuousValuation_fundamental:

$$V(T)=0,\quad V(0)=PV_B-PV_P,\quad V(t)\ge0,\quad V'=P+\delta V-\mu(B-V)$$

The capstone proves the exact continuous term reserve issue value, terminal zero, nonnegative on the term and the actual Thiele ODE, not merely a definitional rewriting.

Capstone theorem

The main target is ActuarialValuation.cm1ThieleContinuousValuation_fundamental. The capstone proves the exact continuous term reserve issue value, terminal zero, nonnegative on the term and the actual Thiele ODE, not merely a definitional rewriting.

$$V(T)=0,\quad V(0)=PV_B-PV_P,\quad V(t)\ge0,\quad V'=P+\delta V-\mu(B-V)$$

Significance

The professional actuarial syllabus provides the background to this reusable work (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). The closed form reserve formula can be verified independently through expected benefit and premium present values, and must satisfy the continuous-time insurance reserve balance at every intermediate time. Thiele's equation states V'(t)=P+δV(t)-μ(B-V(t)), where B−V is the death strain at risk. The terminal reserve vanishes at expiry of the pure term insurance. Proving all conditions together guards against wrong signs in mortality costs, incorrect interest accumulation, and omitting the premium stream. This formal special case may be reusable for continuous-time multi-state reserves or variable force extensions, provided their assumptions are stated explicitly.

Difficulty

The formula is valid under a constant mortality force and a constant financial force and is not a universal solution of a time-varying Thiele equation. Real exp differentiation and finite-term time inversion require correct signs. The quotient involves k=δ+μ, so algebraic cancellation requires k nonzero. For nonnegative reserves one additionally needs μB≥P and t≤T. At t=T the closed form vanishes, but no positive term must be inferred after expiry. The ODE must be established by differentiating the actual prospective reserve, not inserting it as an extra axiom. Zero mortality and zero premiums provide legitimate boundary cases.

Formalization scope

The model describes a pure continuous term insurance with immediate death benefit and continuous premium income. Expenses, profit margins, maturity endowments, lapses and stochastic changing forces are excluded. Financial force δ need not individually be nonnegative if the combined k is positive, but for a mortality probability interpretation μ must be nonnegative. The closed-form expected claim and premium PV definitions use the same integrated combined discount factor. The capstone is a nontrivial analytic theorem joining boundary values, PV valuation, reserve nonnegativity and Thiele's linear ODE and is suitable for reuse in richer insurance reserve models.

These are original derived finite/analytic CM1 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

• Encyclopedia of Mathematics, Thiele Differential Equation (2012). https://encyclopediaofmath.org/wiki/Thiele_differential_equation
• University of Oxford Department of Statistics, Actuarial Reserves and Thiele's Differential Equation (2020), lecture notes. https://www.stats.ox.ac.uk/~winkel/bs4b11.pdf
• David C. M. Dickson, Mary R. Hardy and Howard R. Waters, Actuarial Mathematics for Life Contingent Risks (2020), Chapter 7. https://www.kriso.ee/actuarial-mathematics-life-contingent-risks-3rd-db-9781108478083.html
• Institute and Faculty of Actuaries, CM1 Actuarial Mathematics Syllabus (2026). https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf

Motivation

The established IFoA actuarial mathematics syllabus discusses the relevant mathematics (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). CM1 actuarial foundations form the mathematical background. Salary growth, defined contribution funding and defined benefit pension accrual are usually treated in separate actuarial calculations, even though they can be joined through a coherent finite cashflow model. The standard pension formula B=alpha times years of service times pensionable salary and the distinction between final salary and career-average revalued earnings are explained by Dickson, Hardy and Waters. A larger formal mission can prove the exact deterministic contribution rate that finances a salary-linked CARE pension, rather than stopping at a definition of accrued pension. This fills a gap not addressed by earlier tranche factor and commutation missions.

Setting

Exact actuarial equivalence is conditional on the stated model assumptions. The previously known actuarial mathematics in the published textbooks motivates these original-derived Lean targets. They remain unproved until real theorem solutions are accepted. Nontrivial cashflow and probability examples exclude vacuous zero-benefit substitutes, and the resulting identities can support future actuarial missions.

At service year t, salary S(t) is annual pensionable pay. Annual benefit accrual at rate alpha is alpha S(t). The CARE retirement benefit revalues each year's accrual with a tranche-specific real factor R(t), giving B=alpha sum S(t)R(t) over the service period. A pension capitalisation factor a at retirement converts this annual pension to liability L=aB. A DC member or sponsor contributes a fixed fraction c of salary each year, with terminal growth multiplier G(t), producing assets A(c)=c sum S(t)G(t). The relevant salary contribution base F is the last sum. All monetary quantities and multipliers must use the same common terminal valuation date.

Formalization targets

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

Salary scales and cumulative service

This block contributes 9 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.cm1FinalSalaryPension_nonneg:

$$B_{\rm FS}\ge0$$

Nonnegative service, salary and accrual rate produce a nonnegative final-salary pension.

Pension accrual and valuation

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

Representative theorem ActuarialValuation.cm1CARELiability_add_last:

$$L_{n+1}=L_n+\alpha S_n R_n a_R$$

An additional year of pension accrual adds its own capitalised liability slice.

DC contribution accumulation and matching

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

Representative theorem ActuarialValuation.cm1SalaryPensionFunding_fundamental:

$$c^*\ge0,\quad A_n(c^*)=L,\quad c\ge c^*\Rightarrow A_n(c)\ge L$$

Capstone proves the unique actuarially consistent contribution threshold funding a CARE pension, with nonnegative surplus for rates above the threshold.

Capstone theorem

The main target is ActuarialValuation.cm1SalaryPensionFunding_fundamental. Capstone proves the unique actuarially consistent contribution threshold funding a CARE pension, with nonnegative surplus for rates above the threshold.

$$c^*\ge0,\quad A_n(c^*)=L,\quad c\ge c^*\Rightarrow A_n(c)\ge L$$

Significance

The professional actuarial syllabus provides the background to this reusable work (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). The formal result makes the relation between salary-linked pension promises and their financing explicit. An increasing final-salary pension need not equal a career-average pension, and a DC accumulated account value is not directly an annual pension. CARE revaluation and contribution fund growth can differ significantly, so the unique equivalent rate c=L/F must use the separately defined factors rather than an arbitrary average. The equations can support pension valuation controls, funding reconciliations and salary projection sensitivities. They can become reusable infrastructure for subsequent UK defined benefit funding and DC pension options.

Difficulty

The common time origin for earnings, CARE revaluation and contribution accumulation must be maintained. Each cashflow slice is counted exactly once and the result is not a closed-form salary sum unless growth is genuinely constant. The rate c=L/F is only actuarially meaningful if the accumulation base F is positive; division by zero must not make a false equivalence claim. Zero service, negative growth, increasing salary and nonnegative annuity factors are genuine boundary cases. The capstone must prove monetary matching and the threshold property, not assume either as an axiom.

Formalization scope

The model is finite and deterministic. Salary projection uses a constant growth special case, while salary and revaluation cashflow schedules can vary arbitrarily. It does not pretend that a matching terminal DC fund guarantees an identical DB pension after retirement: the annuity capitalisation factor must be agreed and both schemes may have different risk allocation. The final salary formula is a separate valuation component. The nontrivial root proves a contribution-rate funding threshold and is reusable in future stochastic contribution and employer covenant extensions.

These are original derived finite/analytic CM1 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

• David C. M. Dickson, Mary R. Hardy and Howard R. Waters, Actuarial Mathematics for Life Contingent Risks (2009), Chapter 9. https://doi.org/10.1017/CBO9780511800146
• Cambridge University Press, Actuarial Mathematics for Life Contingent Risks: Pensions (2020), Chapter 1. https://api.pageplace.de/preview/DT0400.9781108787406_A49239377/preview-9781108787406_A49239377.pdf
• Institute and Faculty of Actuaries, CM1 Actuarial Mathematics Syllabus (2026). https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf

Motivation

The established IFoA actuarial mathematics syllabus discusses the relevant mathematics (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). CM1 actuarial foundations form the mathematical background. A pension service table projects active members through competing causes of leaving employment, including retirement, death, disability and withdrawal. A comprehensive valuation must account for those mutually exclusive events without creating or destroying pension scheme members. Dickson, Hardy and Waters Chapter 9 discusses pension service tables and Chapter 8 introduces multiple decrement models. Earlier missions consider a single-year decrement law and mortality variance; this mission develops multi-year cohort conservation and a complete reconciliation between two implementations of cause-specific pension benefit valuation.

Setting

Exact actuarial equivalence is conditional on the stated model assumptions. The previously known actuarial mathematics in the published textbooks motivates these original-derived Lean targets. They remain unproved until real theorem solutions are accepted. Nontrivial cashflow and probability examples exclude vacuous zero-benefit substitutes, and the resulting identities can support future actuarial missions.

An initial active-service cohort l(0) is projected to year N. For each year t, d(t,j) records the nonnegative number of scheme members leaving active service due to cause j during that year, where causes are mutually exclusive. The service-table accounting law is l(t+1)+sum_j d(t,j)=l(t). Individual cause probabilities conditional on active membership are q(t,j)=d(t,j)/l(t) when l(t)>0. The probability of remaining active at year t is l(t)/l(0). The unconditional probability of a specified exit is d(t,j)/l(0). A benefit amount b(t,j) and a discount factor v(t) attach to that exit event. The expected present value can be constructed either directly from unconditional cause exit mass or by multiplying active survival and conditional cause probability.

Formalization targets

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

Pension cohort accounting

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

$$\sum_{t<N}\sum_jd_{t,j}+l_N=l_0$$

All exits during the horizon plus active lives at its end exactly reconcile to the initial cohort.

Cause probabilities and transitions

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

$$P(\mathrm{active\ at\ }N)+P(\mathrm{exit\ before\ }N)=1$$

The full pension cohort partitions into all competing causes of exit and eventual continued active service.

Benefit cashflows and service value

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

Representative theorem ActuarialValuation.cm1ServiceCohortValuation_fundamental:

$$P(\mathrm{stay})+\sum_{t,j}P(\mathrm{exit}_{t,j})=1,\quad V_{\rm unconditional}=V_{\rm conditional}\ge0$$

The nontrivial capstone simultaneously proves full multi-year service-table probability conservation, consistent cause-specific pension benefit PV and nonnegative liability.

Capstone theorem

The main target is ActuarialValuation.cm1ServiceCohortValuation_fundamental. The nontrivial capstone simultaneously proves full multi-year service-table probability conservation, consistent cause-specific pension benefit PV and nonnegative liability.

$$P(\mathrm{stay})+\sum_{t,j}P(\mathrm{exit}_{t,j})=1,\quad V_{\rm unconditional}=V_{\rm conditional}\ge0$$

Significance

The professional actuarial syllabus provides the background to this reusable work (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). A service table must reconcile deaths, retirements, withdrawals and remaining active membership throughout the projection. The multi-period accounting result says cumulative decrement counts plus terminal active count equal the original cohort; after normalisation, the corresponding probabilities sum to one. This provides an important actuarial QC invariant. The same model supplies a direct payment valuation and a survival-conditioned valuation, which must match if probability denominators and calendar payment dates are consistently defined. Both the conservation invariant and cashflow equality can be reused for scheme funding, actuarial gain analysis and member-level pension cost models.

Difficulty

Each decrement cause must form a disjoint partition and the yearly cohort equation has no additional inflow from new entrants. To divide by remaining active service, survivor counts must be nonzero in each year where conditional rates are used. At the terminal horizon no more cause payment years are included. The exact finite-sum telescope must account for every annual exit once and only once. Negative claim sizes, negative exit counts or zero initial cohorts cannot support the probability interpretation. The capstone deliberately validates both valuation routes rather than obtaining equality by defining the two formulas identically.

Formalization scope

The results model a closed, finite cohort with given competing decrement counts. They do not infer cause-specific hazards from observed data or assume independent causes. Causes are disjoint observed outcomes; the conditional exit probabilities sum with the surviving-in-service probability to one. The service table can later be enhanced by new entrants, state transitions and pension commencement options, but these are outside this precise closed-cohort theorem. The calculations retain common valuation dates and financial units for all benefits. The root establishes probability conservation, PV equivalence and nonnegativity, and is reusable in other pension missions.

These are original derived finite/analytic CM1 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

• David C. M. Dickson, Mary R. Hardy and Howard R. Waters, Actuarial Mathematics for Life Contingent Risks (2009), Chapters 8 and 9. https://www.cambridge.org/core/books/abs/actuarial-mathematics-for-life-contingent-risks/multiple-state-models/BFEB2CD04A3EA012FCB1C7E3A326E9A0
• Institute and Faculty of Actuaries, CM1 Actuarial Mathematics Syllabus (2026). https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf
• Institute and Faculty of Actuaries, CM1 Actuarial Mathematics Syllabus (2026). https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf

Motivation

This work is motivated by the IFoA CM1 financial and life-contingent mathematics syllabus (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). A life-table survival model underpins almost every actuarial life contingent assurance, annuity and pensions result. The earlier actuarial missions concentrate on valuation of given death and survival probabilities. CM1_new_formula.pdf sections on life-table identities, select mortality, fractional-year assumptions, joint lives and contingent annuities motivate a larger proof mission establishing those foundations rather than restating assurance formulas already formalised. The principal application is the correct value of a spouse's reversionary annuity when the original member dies while the beneficiary survives.

Setting

The established CM1 modelling conventions and previously known actuarial identities provide the conceptual background, while the following larger original-derived Lean results still need accepted proofs. The stated nontrivial capstone excludes vacuous equal cashflow or zero-duration substitutes. Each accepted module could become reusable infrastructure for future actuarial formalisation missions.

A life table l(x) records survivor counts at integer ages. Conditional survival and death probabilities divide later survivor counts by a nonzero starting cohort. Select rates use within an explicit initial select period, with ultimate rates from the boundary onwards. Within an integer year UDD fractional survival is linear in elapsed fraction, whereas constant force of mortality gives an exponential survival model; neither assumption can be inferred from the other. For two lifetimes, pX(t) and pY(t) are marginal survival probabilities and pBoth(t) is the joint probability of both lives surviving. A valid joint model obeys 0 ≤ pBoth ≤ each marginal probability, but does not need independence. The difference pY(t)−pBoth(t) is the probability of y surviving while x has died. Finite annuity present values sum positive discount factors multiplied by appropriate survival-event indicators.

Formalization targets

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

Life tables and survival composition

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

$${}_{k|n}q_x\ge0$$

Valid cohort life counts yield a nonnegative deferred mortality probability.

Select, UDD and constant force

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

Representative theorem ActuarialValuation.cm1SelectUltimateRate_zero_select:

$$k=0\Longrightarrow q=q^U$$

A select period of zero years uses ultimate rates immediately.

Joint, last-survivor and reversionary benefits

This block contributes 18 theorem targets and 7 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.cm1ReversionaryValue_fundamental:

$$a_{x|y}\ge0,\ a_{x|y}+a_{xy}=a_y,\ a_{\rm last}+a_{xy}=a_x+a_y$$

The genuine contingent annuity capstone combines positivity, reversionary partition and inclusion-exclusion for any valid dependent joint survival model, not just independent lives.

Capstone theorem

The main target is ActuarialValuation.cm1ReversionaryValue_fundamental. The genuine contingent annuity capstone combines positivity, reversionary partition and inclusion-exclusion for any valid dependent joint survival model, not just independent lives.

$$a_{x|y}\ge0,\ a_{x|y}+a_{xy}=a_y,\ a_{\rm last}+a_{xy}=a_x+a_y$$

Significance

The established actuarial syllabus identifies the relevant relationships and applications (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). Pension spouse benefits, contingent pensions, first death and last survivor assurance contracts all depend on correctly partitioning joint and marginal survival events. Using pX pY for all joint probabilities would silently impose independence, which is neither universally correct nor necessary for the most important reversionary identity. The capstone shows a contingent pension to y can be computed as the y-only annuity minus the joint-life annuity, with correct survival-event assumptions and finite payment dates. It also proves the separate last-survivor inclusion-exclusion relation. These foundational results can serve as accepted dependencies for detailed UK DB spouse entitlement and guarantee missions.

Difficulty

Conditional life-table quotients require a positive or nonzero cohort count at the reference age and intermediate age. A monotone life table is needed for probabilities to lie within zero and one. A survival decomposition cannot assume independence across adjoining conditional periods without precise population conditioning, and multiplicativity of constant-force survival cannot be falsely attributed to UDD within the year. Select and ultimate mortality require disjoint endpoints. The reversionary decomposition must keep both-alive and y-alone events distinct and retain the correct payment dates, while allowing arbitrary joint lifetime dependence. The full capstone is the exact conjunction of substantive annuity identities and a meaningful positivity inequality.

Formalization scope

The model is a finite discrete collection of integer-age and payment-date statements augmented by separate algebraic fractional-age rules. The UDD and constant-force models are explicitly assumed and are not asserted as general mortality laws. Annuities are generic finite discounted expected payments; contract guaranteed payments or calendar pension increases would enter through schedule-specific weights in a later mission. The theorem capstone does not impose independent lifetimes, and the independent product model is kept as an optional separate special case. There is no double-counting of survivor states or need to invent an average life expectancy.

These are original derived finite/analytic CM1 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, CM1 Actuarial Mathematics Syllabus (2026). https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf
• David C. M. Dickson, Mary R. Hardy and Howard R. Waters, Actuarial Mathematics for Life Contingent Risks (2009), chapters on mortality and joint lives. https://www.cambridge.org/core/books/actuarial-mathematics-for-life-contingent-risks/51C0B04099D4DE1D1DDEF9551024133B/listing

Motivation

This work is motivated by the IFoA CM1 financial and life-contingent mathematics syllabus (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). Actuarial life insurance pricing is incomplete without the link between gross premiums, future reserve liabilities, emerging cashflow profits and risk capital requirements. The IFoA CM1 syllabus explicitly includes gross prospective and retrospective reserves, death strain, mortality profit, profit signatures, profit testing for unit-linked business and elimination of negative non-unit profit cashflows by reserve zeroisation. Dickson, Hardy and Waters (2009), Chapter 11 (Emerging costs for traditional life insurance) supplies the broader profit testing theory. We combine these elements into one connected mission with an optimisation property as its capstone.

Setting

The established CM1 modelling conventions and previously known actuarial identities provide the conceptual background, while the following larger original-derived Lean results still need accepted proofs. The stated nontrivial capstone excludes vacuous equal cashflow or zero-duration substitutes. Each accepted module could become reusable infrastructure for future actuarial formalisation missions.

A contract has dated benefit payments, expenses, premiums and probability/discounter weights over a finite horizon N. Gross level premium divides the total expected benefit and expense PV by a nonzero premium annuity factor. A prospective reserve equals expected future outgo less future premiums, and a retrospective reserve uses prior accumulated premiums less outgo on the same valuation basis. Death strain at risk measures the claim amount net of the next reserve release. For unit-linked products the unit fund develops through allocation, charges and investment returns. Non-unit projected cashflow c(t) combines premium and charges less expenses and claims. The non-unit reserve R(t), growth factor g(t)>0 and survival/continuation weight s(t)≥0 determine projected profit Π(t)=c(t)+g(t)R(t)-s(t)R(t+1), with terminal reserve R(N)=0.

Formalization targets

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

Gross premium equivalence

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

$$B_{N+1}=B_N+b_Nv_Np_N$$

Finite expected benefit PV recurses correctly when one extra payment term is appended.

Prospective reserve and mortality profit

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

$$a\le e,\ DSAR\ge0\Longrightarrow M\ge0$$

With positive death strain, fewer actual deaths than expected produce favourable mortality profit.

Projected profits and unit-linked funds

This block contributes 10 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.cm1ProfitMargin_nonneg:

$$NPV\ge0,\ PV(P)>0\Longrightarrow m\ge0$$

Profit margin is nonnegative if projected profit is nonnegative and the premium base positive.

Backwards non-unit zeroisation

This block contributes 12 theorem targets and 2 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.cm1ZeroisationOptimality_fundamental:

$$(\forall t<N:\ \Pi_t(R)\ge0)\ \land\ (\forall t\le N:\ R_t\le Q_t)$$

The finite-horizon capstone proves that a backwards-zeroised reserve produces nonnegative projected profits and is pointwise minimal among all nonnegative feasible reserve paths with the same terminal boundary.

Capstone theorem

The main target is ActuarialValuation.cm1ZeroisationOptimality_fundamental. The finite-horizon capstone proves that a backwards-zeroised reserve produces nonnegative projected profits and is pointwise minimal among all nonnegative feasible reserve paths with the same terminal boundary.

$$(\forall t<N:\ \Pi_t(R)\ge0)\ \land\ (\forall t\le N:\ R_t\le Q_t)$$

Significance

The established actuarial syllabus identifies the relevant relationships and applications (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). The zeroisation recursion can be used to eliminate projected negative future non-unit profits while avoiding excessive reserve financing. It is valuable to show that the backwards reserve is not only feasible but pointwise minimal among all competing nonnegative reserve profiles satisfying the same profit and terminal constraints. Such a theorem is an auditable dynamic optimisation guarantee, not merely a spreadsheet check. It also provides a bridge from earlier finite cashflow PV and insurance reserve missions to modern policy profit testing. The intermediate theorem groups separate gross premium equivalence, death strain, reserve valuation, unit funds, discounted profit signatures and zeroisation.

Difficulty

The formal model carefully distinguishes net benefit cashflows and reserve-adjusted profit, and never calls a gross premium formula universally correct without its equivalence assumptions. In zeroisation, g(t) must be strictly positive before division and multiplication inequalities can be reversed, while s(t)≥0 is necessary to compare different next-year reserve requirements. The floor max(0,(sRnext-c)/g) is a genuine feasibility threshold. The minimality result needs backward induction from the same terminal reserve, not a false forward monotonicity argument. Negative non-unit cashflows and zero survival are meaningful cases. The result does not equate the risk discount rate used for net present value with the investment growth rate g(t).

Formalization scope

This is a finite-horizon deterministic expected-cashflow model rather than a fully stochastic regulatory reserve basis. Probability, benefit and expenses schedules enter as given finite arrays. Gross premiums use the simplified actuarial equivalence principle and not arbitrary commission or investment-profit target structures. The non-unit zeroisation capstone is conditional on a reserve path satisfying the specified backward recursion; its existence can be constructed by a later recurrence theorem and should not be replaced by a hidden axiom. All explicitly stated profit constraints and nonnegative reserve bounds are maintained for each pre-terminal valuation date. The theorem is meaningful even when cashflow c(t) is negative.

These are original derived finite/analytic CM1 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, CM1 Actuarial Mathematics Syllabus (2026). https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf
• David C. M. Dickson, Mary R. Hardy and Howard R. Waters, Actuarial Mathematics for Life Contingent Risks: Emerging Costs for Traditional Life Insurance (2009), Chapter 11. https://doi.org/10.1017/CBO9780511800146.012

Motivation

This work is motivated by the IFoA CM1 financial and life-contingent mathematics syllabus (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). Financial mathematics provides the time-value backbone of actuarial pricing and pension liability management. The CM1 formula sheet records effective interest and discount rates, annuity-certain relationships, loan amortisation and bond duration. These should be proved as one connected mathematical construction culminating in the local Redington immunisation conditions, rather than as separate missions of two-line rearrangements. A correct proof handles actual discounted dated cashflows and the consistency of their rate derivatives. The IFoA 2026 CM1 financial mathematics syllabus provides the subject boundaries.

Setting

The established CM1 modelling conventions and previously known actuarial identities provide the conceptual background, while the following larger original-derived Lean results still need accepted proofs. The stated nontrivial capstone excludes vacuous equal cashflow or zero-duration substitutes. Each accepted module could become reusable infrastructure for future actuarial formalisation missions.

Real-valued effective annual interest i is restricted to i greater than minus one where cashflow discount factors need to remain positive. A finite dated cashflow c(k) is payable at time k+1. The annual discount factor is (1+i) raised to the negative integer horizon, implemented as a reciprocal of an accumulated factor. Unit annuities in advance and arrears use dates k and k+1 respectively. The cashflow valuation V(i) is a finite weighted sum. A loan balance at t is the present value of remaining loan installments. Duration and convexity numerators aggregate discounted times and squared-time coefficients of cashflows. Asset and liability streams are compared at a single flat effective rate, so rate derivatives are well-defined on the positive accumulation domain.

Formalization targets

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

Interest rate algebra

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

$$j^{(m)}=mj$$

Nominal rate scales the periodic effective interest input.

Annuity certain identities

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

Representative theorem ActuarialValuation.cm1IncreasingImmediate_succ:

$$(Ia)_{n+1}=(Ia)_n+(n+1)v^{n+1}$$

Increasing annuity recurrence uses the next arithmetically increasing payment.

General cashflows and loan balances

This block contributes 10 theorem targets and 2 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.cm1LoanBalance_nonneg:

$$B_t\ge0$$

Remaining positive scheduled loan payments have nonnegative prospective value.

Bond pricing and immunisation

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

$$S(i_0)=S'(i_0)=0,\ S''(i_0)>0 \Longrightarrow S(i)\ge0\text{ locally}$$

The genuine Redington second-derivative test gives a local surplus minimum at the matching effective yield; it does not assert global or arbitrary curve immunisation.

Capstone theorem

The main target is ActuarialValuation.cm1RedingtonImmunisation_fundamental. The genuine Redington second-derivative test gives a local surplus minimum at the matching effective yield; it does not assert global or arbitrary curve immunisation.

$$S(i_0)=S'(i_0)=0,\ S''(i_0)>0 \Longrightarrow S(i)\ge0\text{ locally}$$

Significance

The established actuarial syllabus identifies the relevant relationships and applications (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). Matching current assets and liabilities without checking interest-rate sensitivity is inadequate. A valuation system should reconcile cashflow present values, annuities, prospective loan balances, duration and convexity, and verify that asset surplus cannot turn negative under sufficiently small yield movements when Redington's strictly positive second-derivative condition holds. These equations are reused in actuarial annuity and pension schemes. The mission formalises genuine financial relationships as a graph: compound accumulation leads to discount factors, then discounted cashflow valuation and rate derivatives, ending with a strict local minimum argument. The latter is more substantial than algebraic definition expansion.

Difficulty

Theorems must preserve distinctions between interest and discount rates and between annuities in advance and arrears. Positive accumulation is essential where inverse factors are cancelled or differentiated. Loan prospective value must include only payments remaining after the valuation date. Duration is a ratio whose denominator must be nonzero. Redington immunisation is a genuinely local twice-differentiable result requiring matched PV, first derivative and strictly positive second derivative at an interior yield. It does not provide protection from arbitrary nonparallel yield-curve shifts or sufficiently large interest-rate movements. A proof must establish smoothness of the finite rational cashflow surplus near i₀, rather than assuming local minimisation as a hidden premise.

Formalization scope

The model is deterministic finite cashflow financial mathematics. Mortality-weighted uncertain payments can later be inserted as expected cashflow amounts. Explicit coupon, redemption, loan and annuity terms share the same discounting convention. The capstone uses the actual finite asset-minus-liability discounted cashflows. This is a flat-yield Redington local test only. It is mathematically strong and may be difficult to complete because the second derivative theorem requires calculus and finite-sum differentiability, but no artificial axiom or proof placeholder may count as a solved result.

These are original derived finite/analytic CM1 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, CM1 Actuarial Mathematics Syllabus (2026). https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf
• David C. M. Dickson, Mary R. Hardy and Howard R. Waters, Actuarial Mathematics for Life Contingent Risks (2009). https://www.cambridge.org/core/books/actuarial-mathematics-for-life-contingent-risks/51C0B04099D4DE1D1DDEF9551024133B/listing
• F. M. Redington, Review of the Principles of Life-Office Valuations (1952); contextual discussion and institutional course treatment in CM1 Actuarial Mathematics Syllabus (2026). https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf

Motivation

A defined benefit pension commencement lump sum cannot generally be determined by multiplying the pre-commutation pension by a cash conversion factor without considering the remaining pension. HMRC's Pensions Tax Manual PTM063240 (https://www.gov.uk/hmrc-internal-manuals/pensions-tax-manual/ptm063240) establishes the applicable amount for a DB arrangement and gives a simplified exact solution 20fg/(20+3f) when the pension is partially surrendered at commutation factor f. PTM063230 (https://www.gov.uk/hmrc-internal-manuals/pensions-tax-manual/ptm063230) identifies other statutory allowance restrictions. This mission formalises the HMRC arithmetic under explicit assumptions, and then extends the model to separate pension tranche reductions rather than pretending all pensions must use a single commutation factor.

Setting

Let g denote the annual pension before commutation, L the pension commencement cash and f the cash paid per pound of annual pension surrendered. The remaining annual pension is P_B=g−L/f. For the simplified DB arrangement with no disqualifying pension credit and no other relevant linked lump sum, the statutory test becomes 3L≤20P_B. Solving this with f>0 gives the maximum applicable cash L_max=20fg/(20+3f). A real value A can represent an externally determined available allowance, giving the capped amount min(L_max,A). For a collection of tranches, annual reduction x(i) and individual cash factor f(i) generate cash contributions f(i)x(i). The residual annual pension is the sum of P(i)−x(i).

Formalization targets

The following declarations are original derived results, not direct quotations of numbered textbook or statutory theorems. Exact hypotheses and corner cases are fixed by the formal Lean statements.

Fundamental boundary

The named result ActuarialValuation.dbCommutedPension_zero_cash captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. If no pension is commuted, the original annual DB pension remains unchanged. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.

$$L=0\Longrightarrow P_B=g$$

Intermediate valuation relation

The named result ActuarialValuation.dbCappedPCLS_le_max captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The allowance cap cannot increase cash above the base applicable amount. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.

$$L_{\rm cap}\le L_{\max}$$

Main actuarial capstone

The named result ActuarialValuation.dbPCLSMaximum_fundamental captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The capstone proves the attained basic HMRC cash limit, verifies the allowance-limited cash remains admissible, and retains a nonnegative pension tax headroom. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.

$$H(L_{\max})=0,\quad0\le L_{\rm cap}\le\min(L_{\max},A),\quad H(L_{\rm cap})\ge0$$

Additional supporting theorems establish cancellations, finite-sum identities, positivity and uniqueness. In all cases the generated formal theorem type rather than an informal diagram is authoritative.

Significance

The equations are financially useful because the HMRC basic limit depends on the annual pension remaining after cash has been commuted. Using the original pension instead of P_B would overstate the permitted amount. HMRC PTM063240 (https://www.gov.uk/hmrc-internal-manuals/pensions-tax-manual/ptm063240) gives the explicit formula and examples, while PTM063230 (https://www.gov.uk/hmrc-internal-manuals/pensions-tax-manual/ptm063230) explains the allowance components of the permitted maximum. The formal result provides a check of cash amount, pension reduction, binding constraint and residual HMRC headroom. Separate tranche cash and residual pension definitions are appropriate when benefit tranches have different commutation factors and noncommutable components. They will support more advanced finite optimisation and pension rights constraints.

Difficulty

Cross multiplication and the residual pension test require f strictly positive. Without this, division by f does not correspond to a legal pension surrender and reversed inequality steps are possible. The formula L_max is required to attain zero HMRC headroom in the simplified case, and every lower nonnegative cash amount must satisfy the same basic maximum relation. Allowance caps must themselves be nonnegative to preserve a nonnegative paid amount. An actual arrangement can also have disqualifying pension credits, other linked lump sums, protected rights, scheme minimum pensions or a finite available lump sum and death benefit allowance. The reduced mathematics must not be misrepresented as covering these cases automatically.

Formalization scope

The Lean model uses exact real arithmetic for the single-factor formula and finite sums for the separate-tranche amounts. It proves basic nonnegativity, monetary identities, headroom monotonicity, the cash upper bound and an allowance-capped admissible solution. Noncommutable GMP and scheme-specific rules are deliberately outside this first formal capstone, with reductions of zero available as an abstract representation of such tranches. The external allowance input does not calculate a member's statutory tax allowances. This limits the formal claims to the HMRC simplified applicable-amount formula, while providing separate tranche arithmetic that a subsequent mission can enrich with survivor minimums, GMP guarantees and more involved cash waterfalls.

Existing actuarial valuation theory gives the financial identities motivating these new formal obligations, but the exact original Lean declarations have no accepted proofs yet. The proposed capstone is nontrivial because arbitrary benefit dates, positivity hypotheses and boundary cases cannot be excluded or replaced with a degenerate zero-cashflow special case. The algebraic components are reusable in future UK scheme valuation and administration missions. For source interpretation, a valuation basis means the explicit package assumptions and a benefit constraint means a scheme-specific rule, not an implicit mathematical axiom.

The pinned Mathlib revision is 0df444a360eaa60ab8c11dca51a86af692955474. All source declarations use targeted imports, with no unrelated namespace opening. An authoring compilation with open sorry targets checks source elaboration but does not prove a mathematical statement. The full actuarial benefit schedule may require further scheme-specific data beyond this theorem graph.

Selected references

• HM Revenue & Customs, Pensions Tax Manual PTM063240, defined-benefit PCLS applicable amount, updated (2026). https://www.gov.uk/hmrc-internal-manuals/pensions-tax-manual/ptm063240
• HM Revenue & Customs, Pensions Tax Manual PTM063230, available allowances, updated (2026). https://www.gov.uk/hmrc-internal-manuals/pensions-tax-manual/ptm063230
• Dickson, Hardy and Waters, Actuarial Mathematics for Life Contingent Risks (2009). https://doi.org/10.1017/CBO9780511800146

Motivation

Defined benefit pension schemes may contain multiple legally different benefit tranches. Their pension increases, retirement ages, survivor benefits, guarantees and death-in-deferment provisions need not be identical. Applying one arithmetic average factor to a total pension would ignore differences in complete present value. The controlled UK DB Retirement Factors Mathematical Framework (2026, Chapter 18, equations 58–60) specifies a separately derived factor for each tranche, and treats a shared factor only when scheme provisions actually permit it. Dickson, Hardy and Waters (2009, Pension mathematics, Chapter 9, https://doi.org/10.1017/CBO9780511800146) explain pension cashflows and service-table valuation. This mission defines formal monetary equivalence for every tranche separately, retaining each actuarial package.

Setting

Take a finite number n of pension tranches. For each index i, P(i) denotes accrued annual pension measured in pounds per year, A(i) the complete early-date immediate retirement package value in annuity years, and D(i) the alternative normal-retirement comparator in the same units. Each package can itself be the sum of discounted expected payments at tranche-specific dates. The individual factor f(i)=D(i)/A(i) is applied only to the original pension in tranche i, giving R(i)=P(i)f(i). Its immediate monetary value is R(i)A(i). Total retirement pension and total actuarial liability must be formed by summing their respective tranche contributions. The model never substitutes a pension-only average factor.

Formalization targets

The following declarations are original derived results, not direct quotations of numbered textbook or statutory theorems. Exact hypotheses and corner cases are fixed by the formal Lean statements.

Fundamental boundary

The named result ActuarialValuation.trancheAnnuityLedgerValue_zero captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. A tranche with no ledger payment dates has zero immediate package value. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.

$$A_i(0)=0$$

Intermediate valuation relation

The named result ActuarialValuation.trancheSchemePension_zero captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. No tranches means no payable scheme pension. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.

$$P_{\rm total}(0)=0$$

Main actuarial capstone

The named result ActuarialValuation.separateTrancheFactors_fundamental captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The capstone asserts per-tranche and aggregate monetary equivalence simultaneously, without computing or applying a common averaged factor. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.

$$(\forall i<n:\ P_if_iA_i=P_iD_i)\land V_{\rm adjusted}=V_{\rm comparator}$$

Additional supporting theorems establish cancellations, finite-sum identities, positivity and uniqueness. In all cases the generated formal theorem type rather than an informal diagram is authoritative.

Significance

Tranche-specific monetary valuation is crucial for pension administration, where two pensions with identical nominal amounts may carry different spouse percentages, indexation and normal retirement dates. The actuarial cost of each unit of pension can consequently vary, and the conditions for equivalence differ. Dickson, Hardy and Waters, pension mathematics (2009, https://doi.org/10.1017/CBO9780511800146), provides the standard actuarial valuation background, while the UK retirement-factor framework 5.3.0 demonstrates the particular multi-tranche application. The resulting identity is useful in migration audits, administering benefit rectifications, reconciling aggregate valuation, and checking that rounding or source ordering has not silently changed benefit values. Separate original benefit rights remain authoritative.

Difficulty

The denominator A(i) must not vanish when cancelling the value ratio. In particular, the real-number convention that division by zero has a defined total Lean value does not make its ordinary actuarial quotient meaningful. Even when total monetary values happen to match, separate per-tranche equality cannot be inferred without additional assumptions. The formal task must retain all individual tranche indices and not count a benefit twice. Zero pension tranches, empty pension schedules and appending another tranche are meaningful cases, rather than mathematical errors. Every unit package must be valued on its own scheme-rule basis, including its relevant discount and contingent cashflows.

Formalization scope

The declarations use exact real arithmetic and finite sums. In particular, the discount, survival, pension increases, guarantee and survivor entitlement details may be assembled into each package ledger as inputs. Their stochastic derivation is an additional task and not silently asserted by a generic real-valued annuity factor. The central identity is P(i)f(i)A(i)=P(i)D(i), and the whole scheme result sums these monetary equivalence equations over finite tranches. The derived calculation remains exact before administration rounding, with no common average factor theorem and no claim that all tranches have the same normal retirement age. It is a reusable base for more detailed pension option missions.

Existing actuarial valuation theory gives the financial identities motivating these new formal obligations, but the exact original Lean declarations have no accepted proofs yet. The proposed capstone is nontrivial because arbitrary benefit dates, positivity hypotheses and boundary cases cannot be excluded or replaced with a degenerate zero-cashflow special case. The algebraic components are reusable in future UK scheme valuation and administration missions. For source interpretation, a valuation basis means the explicit package assumptions and a benefit constraint means a scheme-specific rule, not an implicit mathematical axiom.

The pinned Mathlib revision is 0df444a360eaa60ab8c11dca51a86af692955474. All source declarations use targeted imports, with no unrelated namespace opening. An authoring compilation with open sorry targets checks source elaboration but does not prove a mathematical statement. The full actuarial benefit schedule may require further scheme-specific data beyond this theorem graph.

Selected references

• Dickson, Hardy and Waters, Actuarial Mathematics for Life Contingent Risks, Cambridge University Press (2009). https://doi.org/10.1017/CBO9780511800146
• UK DB Retirement Factors Project, Mathematical Framework v5.3.0, controlled pension valuation manuscript (2026). Background: https://doi.org/10.1017/CBO9780511800146

Motivation

Retiring earlier changes the number of pension payments and may introduce payments before normal retirement age. Retiring later removes some payments but may entitle the member to an uplift and missed increases. A defensible actuarial equivalence calculation compares complete benefit packages, including contingent benefits, at the same valuation date. The UK DB Retirement Factors Mathematical Framework 5.3.0 (2026, Chapters 8 to 11) explicitly treats early and late benefit routes, guaranteed periods, pension increases and pre-commencement death. Dickson, Hardy and Waters (2009, Chapter 9, https://doi.org/10.1017/CBO9780511800146) provide independent actuarial pension valuation background. This mission first formalises a carefully delimited factor-independent death-benefit model and retains explicit differences between pure and total late-retirement factors.

Setting

For early retirement, A_E is the immediate retirement package, D_E the normal retirement comparator, and F_E=D_E/A_E the unrounded reduction factor. The comparator may contain a death-before-retirement component plus survival-to-normal-age probability p times an appropriate discount v and normal pension annuity A_N. For late retirement N is the value of the benefit package at normal retirement, D the value of death benefits payable while commencement is postponed, and A_L the immediate package at the late date. The positive multiplier m represents pension increases that would otherwise have accrued while in payment. The pure LRF F_L solves N=D+pvm A_L F_L. The total pension multiplier M_L=mF_L includes both late uplift and missed increases.

Formalization targets

The following declarations are original derived results, not direct quotations of numbered textbook or statutory theorems. Exact hypotheses and corner cases are fixed by the formal Lean statements.

Fundamental boundary

The named result ActuarialValuation.pensionEarlyComparator_nonneg captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. Nonnegative disjoint death and surviving deferred-annuity route values yield a nonnegative comparator. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.

$$D_E\ge0$$

Intermediate valuation relation

The named result ActuarialValuation.pensionLatePureFactor_nonneg captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The net value available for deferred pension is nonnegative once factor-independent death costs are deducted. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.

$$N\ge D,\ pv m A>0\Longrightarrow F_L\ge0$$

Main actuarial capstone

The named result ActuarialValuation.pensionRetirementEquivalence_fundamental captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The capstone validates both early and late monetary equivalence and proves that the pure factor and total missed-increase multiplier represent the same late pension liability. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.

$$F_E A_E=D_E,\quad D+pv\,m A_LF_L=N,\quad D+pv A_L M_L=N$$

Additional supporting theorems establish cancellations, finite-sum identities, positivity and uniqueness. In all cases the generated formal theorem type rather than an informal diagram is authoritative.

Significance

The distinction prevents a common implementation error: treating the total missed-increase pension multiplier as the pure actuarial LRF and then applying increases a second time. The financial basis and cashflow boundaries must be stated before taking an algebraic ratio. The UK retirement factor methodology v5.3.0 details the pension ledger and explicitly separates pure and total late multipliers. Pension mathematics and contingent annuities in Dickson, Hardy and Waters (2009, https://doi.org/10.1017/CBO9780511800146) explain the broader framework. The resulting small formal theorem can be combined with exact-dated benefit ledgers and numerical models to test early and late valuation reconciliation before rounding. That reuse is important when individual tranches have different dates and benefit conditions.

Difficulty

Both ratio definitions need nonzero annuity packages or survival-weighted denominators. If normal survival probability is zero, a late pension cannot compensate financially in the ordinary quotient model, and Lean division must not hide that failure. The death benefit during late postponement is assumed independent of the eventual pure factor, an explicit limitation. Factor-dependent death benefits require solving a different potentially nonlinear root equation; simply dividing a fixed numerator would be wrong. Increases accrued while waiting are distinct from in-payment increases already present in A_L. All route components are valued at a common date, and different death and survival outcomes are treated as disjoint events.

Formalization scope

The theorem graph establishes early comparator positivity, factor existence and uniqueness, and exact equivalence when an annuity denominator is nonzero. It separately proves late pension value and uniqueness under the corresponding nonzero survival-discount-increase-annuity product. The capstone reconciles the early option and the two equivalent late expressions: using the pure late factor and using the total multiplier mF_L. The underlying cashflow package values are abstract real inputs, which enables later missions to supply actual discounted mortality-weighted schedules. The current restricted identity does not claim to model every dependant, guarantee, calendar increase or factor-linked death benefit. Scheme-specific cashflow rights remain controlling.

Existing actuarial valuation theory gives the financial identities motivating these new formal obligations, but the exact original Lean declarations have no accepted proofs yet. The proposed capstone is nontrivial because arbitrary benefit dates, positivity hypotheses and boundary cases cannot be excluded or replaced with a degenerate zero-cashflow special case. The algebraic components are reusable in future UK scheme valuation and administration missions. For source interpretation, a valuation basis means the explicit package assumptions and a benefit constraint means a scheme-specific rule, not an implicit mathematical axiom.

The pinned Mathlib revision is 0df444a360eaa60ab8c11dca51a86af692955474. All source declarations use targeted imports, with no unrelated namespace opening. An authoring compilation with open sorry targets checks source elaboration but does not prove a mathematical statement. The full actuarial benefit schedule may require further scheme-specific data beyond this theorem graph.

Selected references

• Dickson, Hardy and Waters, Actuarial Mathematics for Life Contingent Risks, Cambridge University Press (2009). https://doi.org/10.1017/CBO9780511800146
• UK DB Retirement Factors Project, Mathematical Framework v5.3.0, controlled retirement factors manuscript (2026). Background: https://doi.org/10.1017/CBO9780511800146

Motivation

Philosophers of physics ask when a formulation of a theory carries excess structure: mathematical distinctions between models that make no physical difference. The standard example is electromagnetism written with a vector potential $A$. Potentials that differ by a gauge transformation $A \mapsto A + d\lambda$ have the same field strength $F = dA$, and on the usual view they represent the same physical situation.

Weatherall (2016) made this precise with category theory. Each formulation becomes a category of models, and a translation between formulations becomes a functor. A functor that is faithful and essentially surjective but not full forgets structure. One that is full and faithful but not essentially surjective forgets properties. One that is full and essentially surjective but not faithful forgets stuff. Weatherall's Proposition 1 says the functor $A \mapsto dA$ from potentials to field strengths forgets only structure, provided the arrows between potentials are spacetime symmetries that preserve $A$. His Proposition 2 says the principal-bundle formulation, whose arrows include gauge transformations, forgets nothing. His footnote 15 notes that adding gauge transformations as arrows between potentials yields a category equivalent to that of field strengths (Weatherall, arXiv:1411.5757).

These arguments work on Minkowski space, which is contractible. Weatherall's footnote 9 sets topology aside for that reason. The follow-up literature, for example Nguyen, Teh and Wells (2018), compares these and related functors further. This mission states the comparison exactly on a finite cell complex, where topology cannot be set aside. Each of the three ways a functor can forget information then corresponds to one cohomology group.

Setting

A finite oriented 2-complex $X$ has $n_V$ vertices, $n_E$ edges and $n_P$ faces, together with integer incidence numbers $\partial_1(e,v)$ and $\partial_2(p,e)$ satisfying $\sum_e \partial_2(p,e)\,\partial_1(e,v) = 0$ for every face $p$ and vertex $v$. Nothing beyond this identity is required, so the incidence data need not come from a geometric complex; all results hold for any such integer data. Fix an additive commutative group $K$ of coefficients, for example $\mathbb{Z}$, $\mathbb{R}$, or $\mathbb{Z}/n$ as a discrete stand-in for $U(1)$. The cochains are $C^0 = K^{V}$ (gauge parameters $\lambda$), $C^1 = K^{E}$ (potentials $A$) and $C^2 = K^{P}$ (field strengths $F$). The coboundaries are

$$(\delta^0\lambda)(e) = \sum_v \partial_1(e,v)\,\lambda(v), \qquad (\delta^1 A)(p) = \sum_e \partial_2(p,e)\,A(e),$$

and $\delta^1\delta^0 = 0$.

There are three categories, with spacetime symmetries taken to be trivial:

• $\mathsf{Fld}$ (Weatherall's EM1): its objects are the 2-cochains $F$, and its only arrows are identities.
• $\mathsf{Pot}_0$ (Weatherall's EM2): its objects are the 1-cochains $A$, and its only arrows are identities.
• $\mathsf{Pot}_G$ (potentials with gauge arrows): its objects are the 1-cochains $A$. An arrow $A \to A'$ is a gauge parameter $\lambda \in C^0$ with $A + \delta^0\lambda = A'$, and composition adds the parameters. Arrows are the parameters $\lambda$ themselves, so two parameters differing by an element of $\ker\delta^0$ (e.g. a constant) are distinct arrows, just as distinct vertical automorphisms are distinct arrows in Weatherall's bundle category EM3. This is the category of his footnote 15.

The field-strength functors $\mathsf{Pot}_0 \to \mathsf{Fld}$ and $\mathsf{Pot}_G \to \mathsf{Fld}$ send $A \mapsto \delta^1 A$. In the second functor every gauge arrow goes to an identity.

Cohomology vanishing is stated elementarily:

• $H^0 = 0$ means $\delta^0\lambda = 0 \Rightarrow \lambda = 0$.
• $H^1 = 0$ means every $A$ with $\delta^1 A = 0$ equals $\delta^0\lambda$ for some $\lambda$.
• $H^2 = 0$ means every $F$ equals $\delta^1 A$ for some $A$.

Formalization targets

Goal: the cohomological classification

For every finite 2-complex $X$ and coefficient group $K$, the functor $\mathsf{Pot}_G \to \mathsf{Fld}$ satisfies

$$\text{faithful} \iff H^0 = 0,\qquad \text{full} \iff H^1 = 0,\qquad \text{essentially surjective} \iff H^2 = 0.$$

Milestones

1. Proposition 1 analogue. If some $\delta^0\lambda \neq 0$, then $\mathsf{Pot}_0 \to \mathsf{Fld}$ is faithful and not full, and it is essentially surjective iff $H^2 = 0$.
2. Faithful iff $H^0 = 0$.
3. Full iff $H^1 = 0$.
4. Essentially surjective iff $H^2 = 0$.
5. Aharonov–Bohm. On the triangle boundary circle3 with $\mathbb{Z}$ coefficients, the potential equal to $1$ on one edge has the same field strength as $0$. No gauge arrow connects the two, so the functor is not full.
6. Forgetting only stuff. On the filled triangle with $\mathbb{Z}$ coefficients, the functor is full and essentially surjective but not faithful.

Significance

The result. The classification turns a qualitative philosophical diagnostic into a cohomological criterion.

• Structure: Weatherall's "forgets structure" verdict for potentials without gauge arrows is the statement that $\ker\delta^1 \neq 0$.
• Topology: once gauge arrows are added, whether any structure is still forgotten is exactly the question whether $H^1 \neq 0$. A nonzero $H^1$ is the Aharonov–Bohm situation, in which potentials with equal field strength differ by a gauge-invariant holonomy.
• Stuff: the clause $\text{faithful} \iff H^0 = 0$ shows that on a geometric complex (every edge has boundary head minus tail) with at least one vertex and $K \neq 0$, constant gauge parameters are non-identity automorphisms that the functor sends to identities. The functor therefore forgets stuff. This contrasts with the faithfulness clause of Weatherall's Proposition 2 for the bundle formulation, where the analogous constant vertical automorphisms are the subtle case.

Formalizing it. No machine-checked version of the theories-as-categories programme for gauge theory is known to the author of this mission. This mission is the base case of a planned discrete gauge-functor development: non-abelian groups, nontrivial symmetry groups, and holonomy-based equivalences.

Difficulty

The mathematics is elementary once stated. The work is in making the categorical notions line up with the cochain conditions. Three points need care:

• In a discrete category, an isomorphism is an equality.
• Fullness must be tested against arrows between arbitrary pairs of potentials, not only potentials with zero field strength.
• Faithfulness concerns parallel gauge arrows, which differ exactly by elements of $\ker\delta^0$.

The concrete milestones require computations on explicit complexes, including a gauge-invariant obstruction for the Aharonov–Bohm example.

Formalization scope

• Complexes. Cells are indexed by Fin types, and the incidence numbers are integer-valued. The complex is finite but may be empty in any dimension.
• Coefficients. $K$ is any AddCommGroup, and integers act on it by zsmul.
• Categories. Fld and Pot0 are Mathlib Discrete categories. PotG carries a hand-written Category instance whose arrows are the structure GaugeHom.
• Functor properties. Fullness, faithfulness and essential surjectivity are Mathlib's Functor.Full, Functor.Faithful and Functor.EssSurj.
• Symmetries. Spacetime symmetries are fixed to be trivial, so the results compare categories of potentials and fields over a fixed complex.
• Non-triviality. The cohomology conditions are explicit Props about the coboundaries, so none of them is a definition that makes a target hold trivially. The hypothesis of Milestone 1 excludes the degenerate case $\delta^0 = 0$, in which that functor is full.
• Infrastructure. The cochain API (delta0, delta1, $\delta^1\delta^0 = 0$) is proved in the definitions file and is reusable for discrete gauge theory and toric-code missions.

Selected references

• J. O. Weatherall, "Understanding Gauge", Philosophy of Science 83 (2016) 1039–1049. arXiv:1505.02229, doi:10.1086/687936
• J. O. Weatherall, "Are Newtonian Gravitation and Geometrized Newtonian Gravitation Theoretically Equivalent?". arXiv:1411.5757
• J. Nguyen, N. J. Teh, L. Wells, "Why surplus structure is not superfluous", British Journal for the Philosophy of Science 71 (2020). arXiv:1712.01228

Motivation

The Bühlmann–Straub credibility method allocates weight to individual observed claims experience according to total exposure and variability. It balances the expected value of process variance EPV with the variance of hypothetical means VHM. More exposure raises the statistical information carried by the policyholder's observed rate and should weakly improve the resulting optimal linear prediction error. The established credibility formula and its interpretation are developed in Loss Data Analytics (https://openacttexts.github.io/LDAVer2/ChapCredibility.html). The new mission formalises how these exact deterministic weight and risk formulae change with exposure.

Setting

Let P be a nonnegative real representing total risk exposure. EPV is strictly positive, while VHM is nonnegative and may equal zero for a homogeneous risk class. The credibility factor Z(P) is P times VHM divided by the sum of P times VHM and EPV. A credibility premium combines the policyholder's experience rate with the collective mean using weights Z(P) and 1-Z(P). A normalised optimal quadratic prediction error is EPV times VHM over the same positive denominator. A scaled quadratic expression captures the trade-off between random process noise and between-risk heterogeneity.

Formalization targets

The formal targets progress from structural boundary identities to financial sensitivity and the full capstone. Supporting theorems remain genuine Open declarations until accepted Lean proofs are submitted; no previously accepted proof is silently assumed.

Boundary identity

The exact theorem name is ActuarialValuation.exposureCredibilityWeight_zero. Without any exposure, the experience credibility weight must be zero, provided the process variance is strictly positive.

$$\mathrm{EPV}>0\Longrightarrow Z(0)=0$$

Structural intermediate target

The exact theorem name is ActuarialValuation.exposureCredibilityPremium_between. As the credibility weight lies in the unit interval, a lower observed claim rate produces a premium bounded by the observed and collective rates.

$$\bar x\le\mu\Longrightarrow \bar x\le\widehat\mu(P)\le\mu$$

Main capstone

The exact theorem name is ActuarialValuation.exposureCredibilityAccuracy_fundamental. The capstone reconciles exposure-driven increases in credibility with the monotone decline of minimum expected squared error, including the zero heterogeneity boundary.

$$Z(P_1)\le Z(P_2),\quad G(P_1,P_2)\ge0,\quad R_{\min}(P_2)\le R_{\min}(P_1)$$

The graph also contains separately stated supporting inequalities and exact definitions, with the intended original derived mathematical identity written out in every milestone.

Significance

Experience-rating systems can be checked for sensible monotonicity when an additional policy year or risk exposure enters the rating base. Larger exposure should not decrease the weight assigned to otherwise unchanged policy experience and should not increase the theoretically optimal error. The classical structure of Bühlmann credibility and its use of EPV and VHM are described by Loss Data Analytics (https://openacttexts.github.io/LDAVer2/ChapCredibility.html). These precise algebraic statements are reusable for downstream weighted risk models, rating systems and numerical sensitivity checks.

Difficulty

Credibility is a rational function whose denominator could vanish under an invalid zero-process-variance model. The hypotheses impose strictly positive EPV and retain zero VHM as a legitimate boundary. Monotonicity is therefore weak, not strict, since a homogeneous portfolio provides no justification for relying more on experience. Comparisons between two exposures must use the same structural parameters, otherwise a change of class could reverse the effect. The theorem relating quadratic risk and the credibility weight is a genuine completing-square identity, while the mission does not assert that an arbitrary Bayesian posterior has linear form.

Formalization scope

Lean uses exact real arithmetic for exposure, EPV, VHM, premium and risk formulae. The finite statistical model is reduced to its deterministic structural-parameter consequences; estimation of the parameters and robustness of individual claims are outside the scope. The theorem graph begins with positivity and zero-exposure boundaries, continues through weight and premium identities, and ends with a conjunction linking increasing credibility to decreasing minimal prediction error. The mathematical framework is known, but the newly stated Lean specialisations have to be proved and exclude vacuous denominator cases.

The pinned Mathlib revision and the precise Lean type of each definition or proposition are authoritative. The imported source must use targeted Mathlib modules; one large aggregate compiler check never substitutes for testing individual definition imports and obsolete namespace openings. The source-specific intermediate statements separate units and hypotheses. The finite index always counts claims, scenarios, or observations according to the declaration, not an implicit probability measure. In an insurance pricing setting the difference between a gross loss, a ceded payment, a net premium and a credibility risk estimate is financially important. A positive coefficient does not by itself imply the coefficients sum to one. Likewise a deterministic algebraic identity does not grant stochastic independence or a forecast model. These restrictions preserve the distinction between a purely algebraic result and a probabilistic interpretation. The formal theorem declarations have to maintain exactly the same quantifiers, arithmetic operations and endpoint conventions as the descriptions, including meaningful boundary cases. Future extensions can introduce richer distributions and dependence without altering the precise finite identities established here.

Selected references

• S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015, printed page 489. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/

• Frees and colleagues, Loss Data Analytics: Experience Rating Using Credibility Theory, 2024. https://openacttexts.github.io/LDAVer2/ChapCredibility.html

Motivation

The stop-loss transform is the expected value of the positive excess of a claim above an attachment, an important building block of actuarial risk ordering. Increasing retention should never increase an otherwise unchanged pure reinsurance premium. A second useful criterion is that the decrease in price should not exceed the increase in retention, once scenario probabilities are normalised. Insurance mathematics describes stop-loss premiums as decreasing functions of the deductible (https://www.researchgate.net/publication/4958878_The_Concept_of_Comonotonicity_in_Actuarial_Science_And_Finance_Theory). This mission additionally identifies their convexity in retention and develops finite verification targets for the exact bound.

Setting

A real loss X(s), a real attachment d and a real scenario weight w(s) determine a positive excess payment max(X(s)-d,0). The pure stop-loss premium at d is the weighted finite sum across s in the range from zero through bound B. Scenario weights are nonnegative for premium-order and convexity theorems. Their finite total W may be arbitrary, while W=1 expresses a genuine probability distribution and yields a sharp unit Lipschitz constant. Two attachments a and b can be combined by d(theta)=(1-theta)a+theta b, with interpolation weight theta between zero and one.

Formalization targets

The formal targets progress from structural boundary identities to financial sensitivity and the full capstone. Supporting theorems remain genuine Open declarations until accepted Lean proofs are submitted; no previously accepted proof is silently assumed.

Boundary identity

The exact theorem name is ActuarialValuation.retentionExcessPositive_nonneg. An excess loss payment cannot be negative even for signed real inputs, since the positive part is the maximum against zero.

$$(x-d)_+\ge0$$

Structural intermediate target

The exact theorem name is ActuarialValuation.retentionStopLossPremium_zero_weight. With no scenario mass, a finite net premium is zero regardless of loss amounts and attachment.

$$w_s\equiv0\Longrightarrow\Pi(d)=0$$

Main capstone

The exact theorem name is ActuarialValuation.retentionStopLossSensitivity_fundamental. The capstone states the three structural constraints on an actuarially valid premium curve, including convex interpolation, when finite scenario weights are normalized.

$$0\le\Pi(a)-\Pi(b)\le b-a,\qquad\Pi(d_\theta)\le(1-\theta)\Pi(a)+\theta\Pi(b)$$

The graph also contains separately stated supporting inequalities and exact definitions, with the intended original derived mathematical identity written out in every milestone.

Significance

These conditions provide powerful reasonableness checks for treaty pricing functions. An actuary can diagnose a premium that rises with retention, or an implausibly large fall inconsistent with maximum ceded-payment change, before relying on a stochastic model. The classical stop-loss transform is extensively studied in insurance finance (https://www.researchgate.net/publication/4958878_The_Concept_of_Comonotonicity_in_Actuarial_Science_And_Finance_Theory). The reusable finite inequalities connect claim severity, scenario weights and contract terms, and can support downstream optimisation, layered reinsurance sensitivity and refinement of discrete tail distributions.

Difficulty

The positive part is a maximum of two affine functions, which is convex but not differentiable when the claim equals the retention. The finite theorem must not assume every claim is above a or b: a distribution can straddle both attachment points. The premium derivative is not required, since pointwise algebraic inequalities suffice to justify convex interpolation and monotone order. The mass-dependent Lipschitz bound becomes one only when total mass is one, so probability normalisation must be stated. Claim severity need not be nonnegative for the algebraic result, while weights must be nonnegative for order preservation.

Formalization scope

The Lean representation uses real numbers for claim severities, deductibles, masses and convex interpolation. Finite scenarios are represented by natural indices and Finset.range. Positive excess is a maximum of two real numbers. All inequalities are original derived finite specialisations of well-known stop-loss facts, with explicit mathematical types and numerical boundary conventions. The formalisation intentionally excludes continuous distributions, derivatives, infinite-dimensional weak convergence and loaded commercial premium assumptions. The main goal is nontrivial because it demands the general weighted convexity and Lipschitz properties for an arbitrary finite loss table.

The pinned Mathlib revision and the precise Lean type of each definition or proposition are authoritative. The imported source must use targeted Mathlib modules; one large aggregate compiler check never substitutes for testing individual definition imports and obsolete namespace openings. The source-specific intermediate statements separate units and hypotheses. The finite index always counts claims, scenarios, or observations according to the declaration, not an implicit probability measure. In an insurance pricing setting the difference between a gross loss, a ceded payment, a net premium and a credibility risk estimate is financially important. A positive coefficient does not by itself imply the coefficients sum to one. Likewise a deterministic algebraic identity does not grant stochastic independence or a forecast model. These restrictions preserve the distinction between a purely algebraic result and a probabilistic interpretation. The formal theorem declarations have to maintain exactly the same quantifiers, arithmetic operations and endpoint conventions as the descriptions, including meaningful boundary cases. Future extensions can introduce richer distributions and dependence without altering the precise finite identities established here.

Selected references

• S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015, printed page 409. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/

• Denuit and colleagues, The Concept of Comonotonicity in Actuarial Science and Finance: Theory, 2002. https://www.researchgate.net/publication/4958878_The_Concept_of_Comonotonicity_in_Actuarial_Science_And_Finance_Theory

Motivation

Sampling an entire finite-state execution is a different computational task from recognizing a supplied word. A membership circuit must answer correctly on its given input. A sampler instead chooses the input together with its associated output, while preserving their joint distribution. This distinction is relevant when finite-state models describe allowable executions and when parallel generation should avoid a sequential pass through every transition. The source paper establishes constant-depth sampling results for regular languages and finite Markov chains in Appendix E (Zhang et al., 2026).

The mission concerns that appendix's finite-state sampling results. It formalizes all six numbered results E.1–E.6, together with the seed bounds stated in the surrounding text. Each milestone points to a published theorem with a separately checked proof. The objects to sample are complete words, word–acceptance pairs, and complete state trajectories. Sampling only the final state would lose the joint temporal information required by the targets.

Finite-state models and fair-bit circuits

A binary deterministic finite automaton has finitely many states, a designated start state, a transition for each state and bit, and a set of accepting states. Starting from its initial state, a binary word of length $n$ determines a run. Let $L$ be the set of words whose final state is accepting. Put $L_n=L\cap\{0,1\}^n$. An arbitrary such automaton represents an arbitrary binary regular language, with no assumption that membership belongs to $\mathrm{AC}^0$.

A finite Markov chain consists of a nonempty finite state set $Q$, an initial probability vector $\mu$, and a row-stochastic transition matrix $P$. Entries are nonnegative real numbers, not restricted to rational numbers. For $\gamma=(x_0,\ldots,x_n)$, its probability is $p_M(\gamma)=\mu(x_0)\prod_{i=1}^{n}P(x_{i-1},x_i)$. The distribution of all $n+1$ states is denoted $\mathrm{Path}_n(M)$. For $F\subseteq Q$, conditioning is allowed when the probability that $X_n\in F$ is positive.

A randomized $\mathrm{AC}^0$ sampler is a deterministic Boolean circuit supplied with independent, unbiased random bits. AND and OR gates have unbounded fan-in; NOT gates and Boolean constants are permitted. Its size is polynomial and its depth has a constant bound independent of trajectory length. Approximate families are nonuniform in both $n$ and their real error tolerance $\epsilon$: existence does not require efficiently computing circuit descriptions or numerical tables from a supplied transition matrix.

Formalization targets

The main goal is the conjunction of all results E.1–E.6, including the linear seed guarantee for E.5. This organizational theorem is not an additional numbered result attributed to the paper. All six milestones must be proved for the goal to hold. The exact Markov sampling criterion in Theorem E.5 is one component. A nonnegative real number is dyadic if it equals $a/2^k$ for natural numbers $a,k$, including zero. A chain is path-dyadic when every finite trajectory, including a trajectory of length zero, has a dyadic probability. The target is

$$\mathrm{Path}_n(M)\text{ has an exact randomized }\mathrm{AC}^0\text{ sampler family} \quad\Longleftrightarrow\quad \forall n\geq0\;\forall\gamma\in Q^{n+1},\ p_M(\gamma)\text{ is dyadic}.$$

On the left, the family has polynomial size in $n+1$ and depth bounded independently of $n$. A supporting target records the linear fair-bit budget $O_M(n+1)$ when path-dyadicity holds. Lemma E.4 supplies another target: every path-dyadic chain is the coordinatewise projection of a finite chain whose initial and transition probabilities are all dyadic. Path-dyadicity must not be replaced by the stronger requirement that the original transition matrix itself be dyadic (Appendix E.3).

Theorem E.1 concerns exact sampling of a uniformly random word together with its acceptance indicator:

$$(X,\mathbf 1[X\in L]),\qquad X\sim\operatorname{Unif}(\{0,1\}^n).$$

The sampler uses exactly $n$ fair bits, polynomial size, and depth depending only on the fixed automaton. This is a sampling assertion and does not assert that membership can be computed in constant depth on an arbitrary externally supplied word.

Theorem E.2 concerns the uniform law on nonempty $L_n$. For every $0<\epsilon\leq1/2$, the target is

$$d_{\mathrm{TV}}(Q_{n,\epsilon},\operatorname{Unif}(L_n))\leq\epsilon, \qquad r_{n,\epsilon}\leq n+C_L\log_2(1/\epsilon).$$

Every possible output is accepted. Size is polynomial in $n+1$ and $1/\epsilon$, and depth depends only on the fixed language or its automaton. In particular, the leading coefficient of the $n$ term in the random-bit bound is one (Appendix E.2).

Theorem E.6 is the corresponding approximate target for trajectories conditioned on $X_n\in F$. It requires total variation error at most $\epsilon$, only positive-probability outputs ending in $F$, $O_M(n+\log(1/\epsilon))$ fair bits, polynomial size in $n+1$ and $1/\epsilon$, and depth depending only on the chain. There is no lower bound on the conditioning probability beyond strict positivity (Appendix E.4).

Lemma E.3 supplies the exact representation used in the Markov construction. A transition-dyadic chain is represented by one binary DFA and a fixed state projection. On a uniform input of length $v+ns$, with positive constants $v,s$, the states observed after $v,v+s,\ldots,v+ns$ bits project to exactly the complete trajectory law of the chain. The same DFA and projection work for every length, including zero.

Significance of the targets

These results separate sampling an input together with its finite-state behavior from computing that behavior on a prescribed input. They also identify a precise obstruction to exact sampling with a finite fair-bit seed: each output probability must be dyadic. Approximate sampling allows arbitrary real transition probabilities while retaining the valid trajectory support. The complete trajectory requirement preserves correlations among all time coordinates.

The formalization makes the circuit model, seed accounting, support guarantees and asymptotic quantifiers explicit and reusable. The theorem statements and their separately submitted proofs have passed the platform verifier. The goal proof imports all six milestones; its E.5 milestone in turn imports both the equivalence and the linear seed theorem. Thus the platform dependency graph covers the entire appendix. Platform verification establishes the formal statements; semantic correspondence is documented in the statement descriptions and source references.

Difficulty

A literal step-by-step implementation of a run makes circuit depth grow with $n$, so it does not meet the constant-depth target. Recognition results alone do not furnish the required joint sampler. For approximate word sampling, an error estimate alone is insufficient: the output must remain in the accepted support, and the coefficient-one seed bound must also hold. For exact Markov sampling, unreachable states and non-dyadic individual transitions prevent identifying the desired criterion with entrywise dyadicity. Conditioning on a rare terminal event must not introduce an unstated dependence on its probability.

Formalization scope

States are indexed by finite types $\mathrm{Fin}(q)$. Binary words have type $\mathrm{Fin}(n)\to\mathrm{Bool}$; trajectories have $n+1$ coordinates. Markov vectors and matrices are real-valued and carry normalization and nonnegativity proofs. Sampling probabilities are defined by counting all seeds that give a particular encoded outcome and dividing by $2^r$. Total variation is half the finite sum of absolute probability differences.

The circuit representation is an explicit topologically ordered gate list with checked wire references. Size counts input bits, gates, gate-input wires and output wires; this yields the usual polynomial-size class. State trajectories use a fixed one-hot encoding at each time coordinate. The invalid-output predicate is checked over every seed, so neither arbitrary decoders nor unrepresented outcomes can satisfy an exact or support-preserving claim. The encodings used by the targets are injective. The circuit family is existentially quantified after the fixed finite-state model; the depth and polynomial constants precede $n$ and $\epsilon$.

Zero-length words and zero-transition Markov paths are included. The word target excludes empty accepted slices. The conditioned target excludes zero-probability conditioning events. Definitions of division by zero still exist as total Lean functions, but the hypotheses exclude those cases from approximate claims. Extensions of these results, reusable finite-state probability lemmas, and further circuit constructions are welcome. No sampler-existence axiom, vacuous model or final-state-only replacement is part of the interface.

Selected references

• Jiarui Zhang, Chengwei Liang, Haozhe Jiang, Binhang Yuan and Jingzhao Zhang. Revision Provably Reduces Sequential Computation in Diffusion Language Models. Zenodo preprint, 2026. DOI 10.5281/zenodo.23105365, Appendix E, Theorems E.1, E.2, E.5, E.6 and Lemmas E.3, E.4, printed pages 33–36.

Motivation

Per-occurrence excess and aggregate excess have different financial triggers. One aggregate deductible applies once to the sum of claims, while a per-risk retention is charged against each loss. Combining many small claims may exhaust an aggregate deductible without producing a payment under any separate per-claim policy. HMRC explains how non-proportional reinsurance differs across individual risks and catastrophe or aggregate protections (https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8060). The valuation question is how the ceded amounts and their pure expected costs are ordered when otherwise identical annual experience and deductibles are used.

Setting

The individual claims x(i), their finite number n, and the deductible d are natural-number monetary quantities. Gross aggregate loss S(n) is the sum of the first n claims. Aggregate recovery is positive excess of S(n) above d; separate per-claim recovery is the sum of each claim's positive excess over d. Finite scenario weights w(s) are real. A scenario maps to an entire loss sequence, and its total claim portfolio is evaluated consistently under both treaty designs. Weighted claims are aggregated for indices from zero to a finite bound B, allowing the scenario count itself to be zero or the probability weights to lack normalisation.

Formalization targets

The formal targets progress from structural boundary identities to financial sensitivity and the full capstone. Supporting theorems remain genuine Open declarations until accepted Lean proofs are submitted; no previously accepted proof is silently assumed.

Boundary identity

The exact theorem name is ActuarialValuation.aggregateLossTotal_zero. An empty collection of claims has zero gross claims and therefore defines the base case for deductible comparisons.

$$S_0=0$$

Structural intermediate target

The exact theorem name is ActuarialValuation.aggregateDeductibleCeded_zero_attachment. With attachment zero, the aggregate excess treaty covers every unit of gross annual claims.

$$C_{\mathrm{agg}}(0)=S_n$$

Main capstone

The exact theorem name is ActuarialValuation.aggregateVsPerClaim_fundamental. The capstone joins the nontrivial pointwise reinsurance coverage inequality to the same ordering of expected pure premiums, without conflating a whole-year treaty with a per-claim deductible.

$$C_{\mathrm{individual}}\le C_{\mathrm{agg}},\quad0\le\Pi_{\mathrm{agg}},\quad\Pi_{\mathrm{individual}}\le\Pi_{\mathrm{agg}}$$

The graph also contains separately stated supporting inequalities and exact definitions, with the intended original derived mathematical identity written out in every milestone.

Significance

The comparison can diagnose material pricing errors, since an aggregate deductible and a per-risk deductible with the same quoted monetary value should not normally have the same technical premium. HMRC's treatment of non-proportional reinsurance (https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8060) makes this distinction a contractual reality. The formal theorem is useful for ceded reserve reconciliation, claims-data audit, treaty design, and future models including several occurrence covers within a separate annual limit. In each case exact mathematical relationships are more valuable than approximate simulation agreement.

Difficulty

The algebra of positive-part natural subtraction differs from ordinary subtraction over integers or real values. The aggregate deductible is taken once, whereas the per-event premium subtracts the same amount separately from each positive claim. The theorem is a weak inequality and must remain valid even when every event is below the separate retention but the aggregate exceeds the annual attachment. The model explicitly includes zero claims, zero deductible, empty portfolios and nonnegative scenario weights. Signed weights would make the expectation order invalid and are not silently permitted in that result.

Formalization scope

Lean treats all claim amounts, event counts, attachment values and scenario bounds as natural numbers. Real numbers occur only in the finite expected ceded amounts. Each individual-claim sum uses Finset.range and the pure premium is a further finite sum over scenarios. This is an exact deterministic relationship between two reinsurance structures rather than an assumption of independence or identical event distributions. No catastrophe frequency model, claims adjustment expenses or risk load is included. The established contractual idea motivates original derived finite relations, and the formal statements remain open until proved.

The pinned Mathlib revision and the precise Lean type of each definition or proposition are authoritative. The imported source must use targeted Mathlib modules; one large aggregate compiler check never substitutes for testing individual definition imports and obsolete namespace openings. The source-specific intermediate statements separate units and hypotheses. The finite index always counts claims, scenarios, or observations according to the declaration, not an implicit probability measure. In an insurance pricing setting the difference between a gross loss, a ceded payment, a net premium and a credibility risk estimate is financially important. A positive coefficient does not by itself imply the coefficients sum to one. Likewise a deterministic algebraic identity does not grant stochastic independence or a forecast model. These restrictions preserve the distinction between a purely algebraic result and a probabilistic interpretation. The formal theorem declarations have to maintain exactly the same quantifiers, arithmetic operations and endpoint conventions as the descriptions, including meaningful boundary cases. Future extensions can introduce richer distributions and dependence without altering the precise finite identities established here.

Selected references

• S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015, printed page 389. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/

• HM Revenue & Customs, General Insurance Manual: Non-proportional reinsurance, GOV.UK, 2023. https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8060

Motivation

Hattendorff's theorem allocates the variance of an insurer's life-contingent loss to policy years. In a fully discrete life insurance model, each policy year's contribution depends on the discounted net amount at risk, the probability of dying in that year, and the conditional probability of surviving the year. Shiu and Xiong (1) derive the classical loss-at-issue formula and the corresponding discrete Hattendorff variance through reserve identities and a summation-by-parts argument. Gerber [2, §6.7] discusses the actuarial allocation of total loss to individual policy years.

The related Missions XVI and XIX address two complementary parts of that argument. XVI specifies death/survival masses for a finite lifetime distribution and proposes proofs of centred annual mortality innovations, cross-year orthogonality and variance. XIX describes a pathwise, year-by-year accounting identity expressing insurer loss, including the terminal reserve, as the opening reserve plus discounted mortality innovations. The present mission is the mathematical bridge combining these structures.

It targets the full finite-horizon reserve-loss expectation and variance theorem under consistent conditional mortality probabilities and the annual prospective reserve recurrence. Unlike a purely algebraic zero-covariance lemma, the mortality model supplies the orthogonality. Unlike a standalone cashflow telescoping lemma, the result calculates the variance of the insurer's actual policy loss.

Setting

Fix a finite scenario space $\Omega$, with nonnegative probabilities $w_\omega$ summing to one, and a curtate future lifetime $K:\Omega\to\mathbb N$. An insured with $K(\omega)=t$ dies during policy year $t$.

Define the in-force and death-year probability masses

$$S_t=\sum_{\omega\in\Omega}w_\omega\mathbf1_{\{K(\omega)\ge t\}}, \qquad D_t=\sum_{\omega\in\Omega}w_\omega\mathbf1_{\{K(\omega)=t\}}.$$

The disjoint survival/death partition gives $S_t=D_t+S_{t+1}$. For each year covered by the policy valuation horizon, assume positive in-force mass, $S_t>0$, so that the conditional death and survival rates are well-defined:

$$q_t=\frac{D_t}{S_t}, \qquad p_t=\frac{S_{t+1}}{S_t}, \qquad q_t+p_t=1.$$

These rates are derived from one joint lifetime distribution. The annual death indicators are therefore linked across years and are not independent. The zero-covariance result must be derived from the nested survival-event structure rather than assumed.

Let $n$ denote the finite number of years covered, $v$ a deterministic annual discount factor, $\pi_t$ the beginning-of-year premium, $b_{t+1}$ the death benefit payable at time $t+1$, and $V_t$ the prospective reserve at time $t$ for a policy still in force.

Assume that, for each year $0\le t<n$, the prospective reserve satisfies

$$\boxed{ V_t+\pi_t=v\left(p_tV_{t+1}+q_tb_{t+1}\right). }$$

The realised insurer loss, valued at issue, is

$$\begin{aligned} L_n(\omega) ={}&\sum_{0\le t<n}\left[ v^{t+1}b_{t+1}\mathbf1_{\{K(\omega)=t\}} -v^t\pi_t\mathbf1_{\{K(\omega)\ge t\}} \right]\\ &+v^nV_n\mathbf1_{\{K(\omega)\ge n\}}. \end{aligned}$$

The terminal reserve is explicitly included if the insured survives beyond the chosen horizon. Thus $L_0=V_0$, a life may remain insured after year $n$, and neither $V_0$ nor $V_n$ is assumed zero. The original Shiu–Xiong complete-life issue-loss formula is recovered only under appropriate terminal/residual liability conditions; the present finite-horizon formula is the reserve-inclusive extension needed for a finite theorem.

Formalization targets

Mortality innovation and pointwise reserve loss

The year-$t$ mortality innovation is

$$I_t(\omega)= \mathbf1_{\{K(\omega)=t\}} -q_t\mathbf1_{\{K(\omega)\ge t\}}.$$

The discounted net amount at risk is

$$\rho_t=v^{t+1}(b_{t+1}-V_{t+1}).$$

By the annual reserve recurrence and the in-force event partition, the change in the insurer's loss across a policy year equals $\rho_tI_t$. Summing over years gives the exact pathwise representation

$$\boxed{ L_n(\omega)=V_0+\sum_{0\le t<n}\rho_tI_t(\omega). }$$

Mission XIX describes this pointwise reserve-loss identity. The present formalisation must bridge XIX's realised-death-year indicator and reserve-derived innovation to XVI's scenario-based mortality innovation. They represent the same object when the death probabilities are calculated from the same $w,K$ model.

From the finite scenario lifetime law and $S_t>0$, the annual innovations satisfy

$$\mathbb E_w[I_t]=0,\qquad \mathbb E_w[I_iI_j]=0\quad(i\ne j),\qquad \mathbb E_w[I_t^2]=D_tp_t.$$

The final factor $p_t$ is the conditional one-year survival probability and is essential to the fully discrete variance formula. It must not be replaced by an assumed independence condition or omitted by importing a continuous-time formula.

Full expectation and variance capstone

Taking expectations of the pathwise identity, using $\sum_\omega{} w_\omega=1$, yields

$$\boxed{\mathbb E_w[L_n]=V_0.}$$

The variance of an insurer loss is unaffected by adding a deterministic opening reserve when the probability weights have unit total mass. Consequently,

$$\begin{aligned} \operatorname{Var}_w(L_n) &=\operatorname{Var}_w\left(\sum_{0\le t<n}\rho_tI_t\right)\\ &=\sum_{0\le t<n}\rho_t^2\mathbb E_w[I_t^2]\\ &=\boxed{\sum_{0\le t<n}v^{2(t+1)} (b_{t+1}-V_{t+1})^2D_tp_t}. \end{aligned}$$

The capstone combines these two results, with no unproved independence assumption. Its mathematical hypotheses explicitly include nonnegative, normalised scenario weights, positive in-force probability for every year in the range, and the one-year reserve recurrence with conditional rates computed from the given lifetime distribution.

The theorem remains valid at $n=0$: the insurer's finite-horizon loss is deterministically $V_0$, and the variance sum is empty and equals zero.

The exact final theorem is ActuarialValuation.finiteHattendorffReserveLoss_fundamental. This result is nontrivial at positive horizons. The formal model does not assert independence, fix the opening reserve to zero, or substitute a deterministic insurer loss.

Significance

The annual decomposition separates valuation assumptions from stochastic fluctuations in mortality. Shiu and Xiong's classical fully discrete treatment (https://doi.org/10.1007/s13385-020-00256-9) emphasises that a survival factor remains in each annual variance contribution. Preserving this factor makes the result useful for actuarial risk allocation and for reconciling the valuation reserve with actual finite-period insurer loss.

The finite-scenario definitions are reusable in downstream insurance valuation missions, for example multiple-decrement reserves and explicit conditional mortality shock models. The result also supplies finite boundary tests for nonzero opening reserves, death exactly at the horizon, and survival beyond the final premium year.

Difficulty

Annual death events arise from the same curtate lifetime, so their indicator variables have nested dependence. Their centred innovations have vanishing cross-year covariance only under the correct conditional in-force rates and probability-weighting conventions. Incorrect denominators or an unproved independence assumption would change the result.

The pathwise identity also accounts for different timing of premiums and benefits, and includes a terminal reserve for survivors. At the last covered year a policy death and survival are disjoint, so the last benefit and terminal reserve must not both be counted. The exact Lean imports must retain the definitions and parameter order of the previously published mortality and loss modules.

Formalization scope

The Lean 4 model uses a finite scenario type with Fintype, real-valued weights, a natural-number curtate lifetime, and the published definition modules from related actuarial missions. Four new definitions and 13 Open theorem obligations form the formal graph, including 12 supporting targets before the conjunction capstone. The accepted proof status of another theorem is never inferred merely from its publication.

The result is finite horizon, finite probability space and fully discrete. The source's complete-life identity would additionally require justified limiting arguments, the disappearance (or valuation) of terminal reserves, integrability and interchange of expectation, variance and limit. None of those conditions is silently assumed here. There is no continuous-time martingale or Lévy-process result in this mission.

The classical full-life result is known mathematically, while the specific finite-horizon Lean declarations remain open proof targets. A compiler-accepted declaration with a sorry body does not establish a proof.

Selected references

• [1] Shiu, Elias S. W. and Xiong, Xiaoyi (2021), “An elementary derivation of Hattendorff's theorem”, European Actuarial Journal, 11, pp. 319–323, equations (1)–(5). Source for the discrete variance survival factor and the reserve-based derivation.
• [2] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, §6.7, Allocation of the Overall Loss to Policy Years.
• [3] Gerber, Hans U., Leung, Bartholomew P. K. and Shiu, Elias S. W. (2003), “Indicator Function and Hattendorff Theorem”, North American Actuarial Journal, 7(1), pp. 38–47. Relates mortality indicator functions, actuarial loss variance and orthogonal yearly increments.

Motivation

A bounded linear operator $u : E \to F$ between Banach spaces is Fredholm if its kernel is finite-dimensional and its range is closed and of finite codimension. Its index

$$\operatorname{ind} u = \dim \operatorname{Ker} u - \dim \operatorname{Coker} u, \qquad \operatorname{Coker} u = F/\operatorname{Im} u,$$

is an integer that survives deformation: it does not change under small perturbations or under compact perturbations, and it is additive under composition. These properties make Fredholm operators the setting for index theorems. Elliptic differential operators on compact manifolds, Toeplitz operators, linearized Cauchy–Riemann operators in symplectic topology, and the linearizations of nonlinear Fredholm maps in transversality arguments (Sard–Smale) all rest on them. Atkinson's theorem characterizes Fredholm operators as those invertible modulo compact operators. For endomorphisms this says that the image in the Calkin algebra $\mathcal{L}(E)/\mathcal{K}(E)$ is invertible.

This mission formalizes the abstract theory on Banach spaces over $\mathbb{R}$ or $\mathbb{C}$, following N. Bourbaki, Théories spectrales, Chapitre III, §§ 3–5 (Springer, 2023). It builds on Mathlib's ContinuousLinearMap.IsFredholm, which already provides the definition and its equivalent descriptions on topological vector spaces. It adds the index and the results listed below.

Setting

$\mathbb{K}$ is $\mathbb{R}$ or $\mathbb{C}$. $E$, $F$, $G$ are Banach spaces over $\mathbb{K}$, and $\mathcal{L}(E;F)$ is the Banach space of bounded linear maps with the operator norm.

• Fredholm operator. $u \in \mathcal{L}(E;F)$ is Fredholm if $\operatorname{Ker} u$ is finite-dimensional and topologically complemented, $\operatorname{Im} u$ is closed and of finite codimension, and $u$ is a strict map (it induces a homeomorphism $E/\operatorname{Ker} u \to \operatorname{Im} u$). On Banach spaces this agrees with Bourbaki's Définition 1 (TS III.41): $u$ has a quasi-inverse $v \in \mathcal{L}(F;E)$, i.e. $1_E - v\circ u$ and $1_F - u\circ v$ have finite rank.
• Index. $\operatorname{ind} u = \dim \operatorname{Ker} u - \dim (F/\operatorname{Im} u) \in \mathbb{Z}$. Bourbaki (TS III.43, formula (1)) uses the opposite sign; this mission uses the sign above, which is the usual one in analysis and geometry.
• Compact operator. $h \in \mathcal{L}(E;F)$ is compact if it maps some neighbourhood of $0$ into a compact set (Mathlib's IsCompactOperator).

Formalization targets

Goal: Atkinson's theorem

$u \in \mathcal{L}(E;F)$ is Fredholm if and only if there is $v \in \mathcal{L}(F;E)$ such that $1_E - v\circ u$ and $1_F - u\circ v$ are compact (Bourbaki III, §5, Corollaire 1, TS III.74).

Milestones

1. Finite codimension gives closed range. If $F/\operatorname{Im} u$ is finite-dimensional, then $\operatorname{Im} u$ is closed and $u$ is strict (§3, Lemme 6, TS III.52).
2. Fredholm criterion. $u$ is Fredholm if and only if $\operatorname{Ker} u$ and $F/\operatorname{Im} u$ are finite-dimensional (§3, Proposition 11, TS III.52).
3. Composition. If $u : E \to F$ and $v : F \to G$ are Fredholm, so is $v\circ u$ (§3, Remarque 2, TS III.41).
4. Additivity of the index. $\operatorname{ind}(v\circ u) = \operatorname{ind} v + \operatorname{ind} u$ (§3, formula (2), TS III.43).
5. Restriction to subspaces of finite codimension. For closed subspaces $E_1 \subset E$, $F_1 \subset F$ of finite codimension with $u(E_1) \subset F_1$, $u$ is Fredholm if and only if its restriction $u_1 : E_1 \to F_1$ is, and then $\operatorname{ind} u - \operatorname{ind} u_1 = \operatorname{codim} E_1 - \operatorname{codim} F_1$ (§3, Proposition 3, TS III.44).
6. Index zero. A Fredholm operator of index $0$ that is injective or surjective is an isomorphism (§3, n° 3, TS III.44).
7. Openness and local constancy. The Fredholm operators form an open subset of $\mathcal{L}(E;F)$, and the index is locally constant on it (§4, Théorème 1, TS III.58).
8. Compact perturbation, kernel side. If $\operatorname{Ker} u$ is finite-dimensional, $\operatorname{Im} u$ is closed and $h$ is compact, then $\operatorname{Ker}(u+h)$ is finite-dimensional and $\operatorname{Im}(u+h)$ is closed (§5, Théorème 1, TS III.72).
9. Compact perturbation, cokernel side. If $\operatorname{Im} u$ has finite codimension and $h$ is compact, then $\operatorname{Im}(u+h)$ is closed and of finite codimension (§5, Théorème 2, TS III.73).
10. Compact perturbation of Fredholm operators. If $u$ is Fredholm and $h$ is compact, then $u+h$ is Fredholm and $\operatorname{ind}(u+h) = \operatorname{ind} u$ (§5, Théorème 3, TS III.73).
11. Index-zero characterization. $u$ is Fredholm of index $0$ if and only if $u$ is the sum of an isomorphism $E \to F$ and a finite-rank operator, if and only if it is the sum of an isomorphism and a compact operator (§5, Corollaire 2, TS III.74).

Significance

The result. Atkinson's theorem identifies the Fredholm operators with the units modulo the compact ideal. Together with the stability of the index under compact and small perturbations, it is the abstract input of every Fredholm index computation. Examples are the Fredholm alternative for integral equations, the index of Toeplitz operators, and the index of elliptic and Cauchy–Riemann operators on compact or punctured surfaces.

Formalizing it. Mathlib defines Fredholm operators on topological vector spaces (ContinuousLinearMap.IsFredholm) and proves that four descriptions agree (isFredholm_tfae). It has no index, no statement about compositions, and no perturbation theory. Its documentation lists the Banach-space criterion (milestone 2) and the restriction statement (milestone 5) as not yet formalized. The library built here is intended for reuse by any later index computation.

Difficulty

The statements combine linear algebra and topology. The index is a difference of dimensions of a subspace and a quotient space, and every statement about it carries a Fredholm hypothesis, since Module.finrank is $0$ on infinite-dimensional spaces. Openness and local constancy are statements about the operator-norm topology on $\mathcal{L}(E;F)$, and the perturbation statements involve operators that are compact but not necessarily of finite rank. The completeness hypotheses are part of the statements: over incomplete normed spaces, a range of finite codimension need not be closed.

Formalization scope

• Namespace FredholmBanach. The definition module FredholmBanach_Setting defines only index. Fredholm operators are Mathlib's ContinuousLinearMap.IsFredholm and compact operators are Mathlib's IsCompactOperator.
• Field and spaces. [RCLike 𝕜], [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E], and likewise for F and G. Bourbaki states several results for locally convex or Fréchet spaces; this mission specializes all of them to Banach spaces.
• Index. index u = finrank 𝕜 u.ker - finrank 𝕜 (F ⧸ u.range) in ℤ. Module.finrank is $0$ on infinite-dimensional spaces, so index is meaningful only for Fredholm u. Every statement about it assumes u.IsFredholm.
• Subspaces and quotients. The codimension of a subspace $E_1$ is finrank 𝕜 (E ⧸ E₁), and "finite codimension" is FiniteDimensional 𝕜 (E ⧸ E₁). The restriction in milestone 5 is ContinuousLinearMap.restrict.
• Isomorphisms are E ≃L[𝕜] F. "Finite rank" is FiniteDimensional 𝕜 (u - e).range.

Contributions welcome: reusable general-purpose lemmas about bounded and compact operators between Banach spaces.

Selected references

• N. Bourbaki, Théories spectrales, Chapitres III à V, Springer (2023), Chapitre III, §§ 3–5. https://doi.org/10.1007/978-3-031-19505-1
• F. V. Atkinson, The normal solubility of linear equations in normed spaces, Mat. Sb. (N.S.) 28(70):1 (1951), 3–14 (in Russian), MR0042059. https://mathnet.ru/eng/sm5589
• T. Kato, Perturbation Theory for Linear Operators, Springer (1995 reprint of the 2nd ed.). https://doi.org/10.1007/978-3-642-66282-9
• D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52 (2012). https://doi.org/10.1090/coll/052

Motivation

Let $S : S^1 \to \mathbb{R}^{2n\times 2n}$ be a loop of symmetric matrices. The asymptotic operator

$$A_S = -J_0\,\partial_t - S(t)$$

acts on loops $S^1 \to \mathbb{R}^{2n}$. It appears wherever a pseudoholomorphic curve approaches a periodic orbit. Near a puncture, a finite-energy curve in a symplectization converges to a Reeb orbit, and in a trivialization along that orbit the linearized Reeb flow is $\Psi' = J_0 S \Psi$. The operator $A_S$ is the Hessian of the action functional at that orbit. The rate of approach and the winding of the curve around the orbit come from its eigenfunctions (Hofer–Wysocki–Zehnder 1995). In Floer theory the operator $-J_0\partial_t - S$ is the Hessian of the symplectic action at a $1$-periodic orbit, and the gradient-flow operator $\partial_s + A_{S(s)}$ is the linearized Floer operator (Robbin–Salamon 1995).

The operator links functional analysis to the linear algebra of stage I. $A_S$ is nondegenerate, i.e. $0$ is not an eigenvalue, exactly when the time-one map $\Psi(1)$ of the linearized flow has no eigenvalue $1$. Then $\Psi|_{[0,1]}$ lies in $\mathrm{SP}(n)$ and has a Conley–Zehnder index. The Fredholm index formula for Cauchy–Riemann operators on punctured surfaces is written in terms of the Conley–Zehnder indices of the asymptotic operators at the punctures (Wendl, Lectures on SFT, Lecture 3).

This is stage II of a series that formalizes the Fredholm theory of linearized Cauchy–Riemann operators. Stage I (Conley–Zehnder Index I: Axiomatic Characterization on Paths of Symplectic Matrices) characterizes the Conley–Zehnder index on $\mathrm{SP}(n)$. This stage sets up the spectral theory of asymptotic operators: the operator itself, self-adjointness, discrete spectrum, compact resolvent, and the dictionary between the kernel of $A_S$ and the time-one map. Later stages are the Fredholm theory of $\partial_s + A_{S(s)}$ in Banach spaces, elliptic regularity for $\bar\partial$, and the index formula.

Setting

$S^1 = \mathbb{R}/\mathbb{Z}$ with its Haar probability measure. $\mathbb{R}^{2n}$ has coordinates $(q,p)$ and the Euclidean inner product, and

$$J_0 = \begin{pmatrix} 0 & -\mathrm{Id}\\ \mathrm{Id} & 0\end{pmatrix}.$$

$S : S^1 \to \mathbb{R}^{2n\times 2n}$ is continuous with $S(t)^{\mathsf T} = S(t)$ for every $t$.

• Fourier coefficients. For $f \in L^2(S^1,\mathbb{R}^{2n})$ and $k \in \mathbb{Z}$, $\hat f_k = \int_{S^1} e^{-2\pi i k t} f(t)\,dt \in \mathbb{C}^{2n}$.
• Domain. $W^{1,2}(S^1,\mathbb{R}^{2n})$ is the set of $f \in L^2$ with $\sum_{k\in\mathbb{Z}} (1+k^2)\,|\hat f_k|^2 < \infty$.
• The operator. For $f \in W^{1,2}$, $A_S f = g$ means $\hat g_k = -2\pi i k\,J_0 \hat f_k - (Sf)^\wedge_k$ for every $k$, i.e. $g = -J_0 f' - S f$ with the derivative taken in $L^2$. This is Wendl's (3.4) with period $1$.
• Fundamental solution. $\Psi : \mathbb{R} \to \mathbb{R}^{2n\times2n}$ with $\Psi(0) = \mathrm{Id}$ and $\Psi'(t) = J_0 S(t)\Psi(t)$. These are the solutions of $(-J_0\partial_t - S)\Psi = 0$. For constant $S$, $\Psi(t) = \exp(tJ_0S)$ is the path in the signature property of stage I.

Formalization targets

Goal: spectral theory of the asymptotic operator

For every continuous loop $S$ of symmetric matrices:

1. $A_S$ with domain $W^{1,2}$ is self-adjoint on $L^2(S^1,\mathbb{R}^{2n})$;
2. $L^2(S^1,\mathbb{R}^{2n})$ has an orthonormal basis of eigenvectors of $A_S$ lying in $W^{1,2}$; the eigenvalues are real, each has finite multiplicity, and they accumulate only at $\pm\infty$;
3. $\ker A_S \cong \ker(\Psi(1) - \mathrm{Id})$, where $\Psi$ is the fundamental solution.

Milestones

1. Well-defined operator. Exactly one partially defined linear map on $L^2$ has graph $\{(f, A_S f)\}$.
2. Domain. The domain of $A_S$ is $W^{1,2}$, and it is dense in $L^2$.
3. Symmetry. $\langle A_S f, g\rangle = \langle f, A_S g\rangle$ for $f, g \in W^{1,2}$.
4. Self-adjointness.
5. Discrete spectrum. An orthonormal eigenbasis exists, with eigenvalues of finite multiplicity tending to $\pm\infty$.
6. Compact resolvent. If $\mu \in \mathbb{R}$ is not an eigenvalue, $A_S - \mu : W^{1,2} \to L^2$ is bijective and its inverse is a compact operator on $L^2$.
7. Unbounded spectrum. For $n \geq 1$ there are eigenvalues of both signs with arbitrarily large absolute value.
8. The unperturbed operator. The eigenvalues of $-J_0\partial_t$ are exactly $2\pi k$, $k\in\mathbb{Z}$, and each eigenspace has dimension $2n$.
9. Fundamental solution. $\Psi$ exists and is unique for every continuous loop $S$.
10. Symplecticity. If $S$ is symmetric, $\Psi(t) \in \mathrm{Sp}(2n)$ for every $t$.
11. Kernel. $\ker A_S \cong \ker(\Psi(1) - \mathrm{Id})$.
12. Nondegeneracy. $0$ is not an eigenvalue of $A_S$ if and only if $\Psi|_{[0,1]} \in \mathrm{SP}(n)$.

Significance

The result. These are the analytic facts that every use of asymptotic operators relies on. Self-adjointness and the discrete spectrum define the eigenvalue branches and the spectral flow. The compact resolvent makes $A_S - \mu$ Fredholm of index $0$ for every real $\mu$, and the weighted Sobolev spaces of the later Fredholm theory are chosen with weights avoiding the spectrum. The kernel dictionary identifies nondegenerate asymptotic operators with the paths of stage I. It is the bridge through which Conley–Zehnder indices enter the index formula.

Formalizing it. All results here are classical. Mathlib has partially defined linear maps and their adjoints, the Fourier basis of $L^2$ on the circle, and compact operators. It has no Sobolev spaces on the circle, no unbounded operator with discrete spectrum beyond trivial cases, and no first-order differential operator treated as an unbounded operator. This stage builds the first such example. The same pattern applies to other first-order elliptic operators on $S^1$, and the library is reusable for spectral flow and for Floer-type operators.

Difficulty

$A_S$ is unbounded and not defined on all of $L^2$, so self-adjointness is a statement about the domain of the adjoint, not a symmetry identity. The spectral statements concern the resolvent of a first-order differential operator with non-constant coefficients, as an operator on $L^2$. The kernel dictionary relates $L^2$ classes, defined through Fourier coefficients, to classical solutions of a linear ODE. The statements about $\Psi$ concern linear ODEs whose coefficients are only continuous.

Formalization scope

• Namespace AsymptoticOperator; all definitions are in AsymptoticOperator_Setting, which imports stage I's ConleyZehnder_Setting (for Mat n, J₀, IsSymplectic and SP).
• The circle is UnitAddCircle ($\mathbb{R}/\mathbb{Z}$) with AddCircle.haarAddCircle. $L^2(S^1,\mathbb{R}^{2n})$ is Lp (EuclideanSpace ℝ (Fin n ⊕ Fin n)) 2 haarAddCircle, a real Hilbert space.
• Fourier coefficients are Mathlib's fourierCoeff, applied to the componentwise complexification $\mathbb{R}^{2n} \to \mathbb{C}^{2n}$. $J_0$ and $S(t)$ act on $\mathbb{C}^{2n}$ through the real-to-complex coercion.
• The operator is a LinearPMap, defined by choice as the map whose graph is the set of pairs $(f, g)$ satisfying the coefficient identity. The fallback is $0$, and milestone 1 makes it unreachable. Self-adjointness is Mathlib's IsSelfAdjoint for LinearPMap, and symmetry is IsFormalAdjoint.
• Eigenspaces are kernels of $A_S - \mu$ on the domain. The discrete spectrum is stated as a HilbertBasis of eigenvectors whose eigenvalues tend to $\infty$ in absolute value along the cofinite filter. This covers $n = 0$, where $L^2 = 0$.
• Regularity of $S$. Wendl assumes $S$ smooth; Hofer–Wysocki–Zehnder (§3, (35)) take $S$ continuous, as here. HWZ state self-adjointness, compact resolvent and discreteness of the spectrum for $n = 1$; this mission states them for all $n$.
• Sign conventions follow Wendl §3.2: $A_S = -J_0\partial_t - S$ and $\Psi' = J_0S\Psi$.

Contributions welcome: reusable lemmas on Sobolev spaces of vector-valued functions on the circle (Fourier characterization, continuity of $W^{1,2}$ functions), on unbounded self-adjoint operators with compact resolvent, and on linear ODEs with continuous periodic coefficients.

Selected references

• C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 3 (§§3.2–3.4). https://arxiv.org/abs/1612.01009
• H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations II: Embedding controls and algebraic invariants, Geom. Funct. Anal. 5 (1995), 270–328. https://doi.org/10.1007/BF01895669
• J. Robbin, D. Salamon, The spectral flow and the Maslov index, Bull. London Math. Soc. 27 (1995), 1–33. https://doi.org/10.1112/blms/27.1.1
• D. Salamon, Lectures on Floer homology, in: Symplectic Geometry and Topology, IAS/Park City Math. Ser. 7, AMS (1999), 143–229. https://doi.org/10.1090/pcms/007/05
• J. Gutt, Generalized Conley–Zehnder index, Ann. Fac. Sci. Toulouse Math. (6) 23 (2014), 907–932. https://doi.org/10.5802/afst.1430