All missions

Motivation and actuarial context

A net premium is usually set at policy inception. As an insured life survives and the remaining insurance term shortens, the expected future claim outgo and future premium income change. A prospective policy value measures the expected present value of the insurer's future loss on a policy that is still in force at the valuation date. This is the natural next stage after the equivalence principle of Actuarial Mathematics VIII. Dickson, Hardy and Waters provide the insurer's future-loss definition and the annual-cashflow policy-value framework in Actuarial Mathematics for Life Contingent Risks (2009), Chapter 7, §§7.3.1–7.3.3 [1]. Promislow covers both deterministic reserve recursions and the stochastic approach to reserves [2].

This mission formalises a finite-term life-assurance reserve at an integer valuation duration. Its central feature is survival conditioning: the reserve is a liability per surviving in-force policy, rather than the unconditional present value of the original contract. Separating these quantities avoids a common modelling error in stochastic policy values.

Model, contract timing and in-force event

Let $K:\Omega\to\mathbb N$ be measurable curtate future lifetime under a probability measure $P$. Let $n\in\mathbb N$ denote the term, $t\in\mathbb N$ the valuation duration, $v\in\mathbb R$ a fixed per-period discount factor, $b\in\mathbb R$ the death benefit and $\pi\in\mathbb R$ the annual level premium.

Premiums are payable in advance at integer times $j<n$ while the life is alive. The benefit, if payable, occurs at the end of the year of death, at date $K+1$. Only cashflows on or after duration $t$ enter the reserve, with discount exponents measured from $t$.

The in-force survival event is

$$S_t=\{\omega\in\Omega:K(\omega)\ge t\}.$$

When $P(S_t)>0$, conditioning on this event gives the valuation basis for policies in force at $t$. A statement about reserves conditional on survival must not silently assume that $P(S_t)>0$.

Future benefit, premium and loss values

The remaining unit term-assurance benefit present value is

$$B_{n,t}(\omega)= \mathbf1_{\{t\le K(\omega)<n\}}\,v^{K(\omega)+1-t}.$$

The remaining premium-annuity present value is

$$Y_{n,t}(\omega)= \sum_{t\le j<n} v^{j-t} \mathbf1_{\{K(\omega)\ge j\}}.$$

The realised future net loss is therefore

$$L_{n,t}(\omega;b,\pi)= bB_{n,t}(\omega)-\pi Y_{n,t}(\omega).$$

These finite expressions make it explicit whether a premium due at the valuation instant is included. Here $t$ is immediately before the premium at time $t$, consistent with an annual premium payable in advance. The choice is essential when comparing reserve formulas across valuation conventions.

At $t=0$ the in-force event is certain. At or after $t=n$, both remaining cashflow components vanish because the contract's coverage and premium period have ended.

Prospective reserve and normalisation

For positive survival probability, the prospective term-policy reserve per in-force policy is

$$V_{n,t} =\mathbb E_P[L_{n,t}\mid S_t] =\frac{\mathbb E_P[L_{n,t}]}{P(S_t)}.$$

The second equality holds because the model defines the realised future loss as zero outside $S_t$. It is a conditional-event expectation, rather than an unrestricted claim about conditional expectation with respect to an arbitrary sigma-algebra. The formal quotient definition makes the denominator explicit, and the principal reserve interpretation and capstone theorem retain $P(S_t)>0$ as a hypothesis.

Linearity separates the reserve into benefit and premium components:

$$V_{n,t}= b\,\mathbb E_P[B_{n,t}\mid S_t] -\pi\,\mathbb E_P[Y_{n,t}\mid S_t].$$

In particular, multiplying both cashflow amounts by $c\in\mathbb R$ gives

$$V_{n,t}(cb,c\pi)=cV_{n,t}(b,\pi).$$

The finite payment period ensures integrability for any fixed real discount factor. When studying economic reserve properties, a nonnegative or positive discount factor can be imposed separately. No assumption of independence between survival indicators, benefits and premiums is made.

Boundary cases and formalisation strategy

The principal boundary checks are survival at inception, $t=0$; exhaustion of cover at $t\ge n$; finite sums with $n=0$; and zero in-force probability. The total real-valued quotient happens to evaluate to zero when both its numerator and denominator are zero in Lean, but this does not create an actuarially meaningful conditional reserve for an impossible in-force event. The descriptive and main conditional theorems are explicitly scoped to positive probability.

Five definitions provide the in-force event, future benefit PV, future premium PV, future loss PV and the prospective reserve. Supporting theorems develop survival-event measurability, cashflow boundaries, nonnegativity where applicable, integrability, inception valuation, benefit–premium decomposition and scaling. The capstone combines the survival-normalised expected-loss identity, valuation decomposition and scaling.

The formalisation is deliberately self-contained at the level of future cashflow definitions so the owner Draft does not depend on the unconfirmed publication of any Mission VIII declarations. The intended later bridge is an exact identity between the duration-zero future loss and the loss-at-issue formula from Mission VIII, once those definitions are published. All theorems are proposed proof targets, not assertions of accepted proofs.

Gerber [4, §§6.3 and 6.5] provides an independent treatment of net premium reserves and annual reserve recursions. Its equation (6.5.6) expresses a whole-life net reserve through the premium difference, illustrating the same prospective viewpoint but not asserting the more general term-reserve theorem of this mission.

References

[1] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 7, Policy Values, Cambridge University Press. Relevant sections: §7.3.1 (future loss), §7.3.2 (policy values for annual cashflows) and §7.3.3 (recursive policy values), printed pages 176–195.

[2] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, ISBN 9781118782460. In particular §6.3 (reserve recursion) and §15.5 (stochastic reserves).

[3] Dickson, Hardy and Waters (2009), Chapter 6, §6.5.1, equation (6.1), on the equivalence principle at policy inception, publisher book record.

[4] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, Net Premium Reserves, §6.3 and §6.5, including the premium-difference reserve formula (6.5.6).

Motivation and actuarial context

The equivalence principle is one of the foundational methods of setting premiums for life-contingent contracts. It requires that the insurer's expected present value of future benefits equal the expected present value of future net premium income at policy inception. As a result, the expected present value of the net future-loss random variable is zero. Dickson, Hardy and Waters define the net future-loss random variable in Actuarial Mathematics for Life Contingent Risks (2009), §6.4, and state the equivalence principle in §6.5.1, equation (6.1) [1]. Promislow develops the corresponding stochastic premium principle in Fundamentals of Actuarial Mathematics (2015), §15.6.1 [2].

This mission makes that principle a rigorous theorem for a finite-term life assurance financed by level premiums payable annually in advance. It proves that a unique net premium exists when at least one premium is due and nonnegative discount factors are used, and it separately addresses the zero-term case where uniqueness fails. The formal treatment distinguishes realised loss from expected loss, keeps mortality and discounting assumptions explicit, and avoids treating survival-contingent benefits and premiums as independent.

Insurance contract, premium dates and realised loss

Let $(\Omega,P)$ represent the probability space, with a measurable natural-valued curtate future lifetime $K$. Let $n\in\mathbb N$ denote the policy term, $v\in\mathbb R$ the annual discount factor, $b\in\mathbb R$ a deterministic death benefit and $\pi\in\mathbb R$ a level premium.

A unit $n$-year term assurance pays once, at the end of the year of death, if death occurs within the covered term. Its realised benefit present value is $A_n$, reusing the published definition from Actuarial Mathematics II. In conventional cashflow notation,

$$A_n(\omega)= \sum_{0\le k<n}v^{k+1}\mathbf 1_{\{K(\omega)=k\}}.$$

This is the discrete term-assurance structure from [3, §3.2.2, equation (3.8)]. Premiums are due at the start of each covered year while the insured remains alive. The realised present value of unit premium income is

$$Y_n(\omega)= \sum_{0\le k<n}v^k\mathbf 1_{\{K(\omega)\ge k\}}.$$

The insurer's discounted net future loss at inception is then

$$L_n(\omega;\pi,b) =bA_n(\omega)-\pi Y_n(\omega).$$

The same curtate lifetime determines both premium income and death benefit outgo. No independence assumption is made between these two random variables.

The equivalence-principle premium

Because the sums are finite, their measurability and integrability can be established from measurability of $K$ for any finite real $v$. Linearity of expectation gives

$$\mathbb E_P[L_n(\pi,b)] =b\mathbb E_P[A_n]-\pi\mathbb E_P[Y_n].$$

For a positive term $n\ge1$ and $v\ge0$, the first premium at time zero is certain: $v^0=1$. All subsequent premium present values are nonnegative. Consequently,

$$Y_n(\omega)\ge1, \qquad \mathbb E_P[Y_n]\ge1>0.$$

The denominator in the premium formula is therefore strictly positive. Solving the linear expected-loss equation leads to the net level premium

$$\pi^*(b)= \frac{b\mathbb E_P[A_n]}{\mathbb E_P[Y_n]}, \qquad \mathbb E_P[L_n(\pi^*(b),b)]=0.$$

The theorem also proves uniqueness: any real premium $\pi$ satisfying $\mathbb E_P[L_n(\pi,b)]=0$ must equal $\pi^*(b)$. This is the formal analogue of the equivalence premium calculation in [1, equation (6.1)]. As a related worked example, [1, equation (6.2)] gives a net premium for an endowment contract using the ratio of benefit and premium-annuity values. The mission specialises the general principle to an $n$-year term assurance.

Scaling, boundaries and assumptions

Linearity yields the scaling identity

$$\pi^*(cb)=c\pi^*(b)$$

for any constant $c$. In particular, a zero benefit produces a zero premium under the ratio definition. A nonnegative benefit gives a nonnegative premium when $0\le v$, although the core algebraic scaling theorem does not require positive $b$.

The boundary $n=0$ is deliberately distinct. Neither a term-assurance benefit nor a premium can occur, so $A_0=Y_0=L_0=0$. Every quoted level premium has zero expected loss in this empty contract, and uniqueness does not follow. The ratio definition is therefore paired with explicit theorem hypotheses rather than falsely suggesting a unique zero-term premium.

At $v=0$ and $n\ge1$, the certain initial premium remains payable at inception, while all covered death benefits are paid at strictly positive times and have zero discounted value. The net premium is zero. At $v=1$, all payment sums remain finite and integrable for fixed $n$, so no artificial upper bound $v<1$ is needed for these finite-term results.

Formalisation and dependency structure

The mission introduces three definitions: the realised finite premium annuity-due present value, the realised term-policy loss, and the equivalence net premium. Supporting theorems establish the initial premium lower bound, measurability and integrability, positivity of the expected premium annuity, linearity of expected loss, existence and uniqueness of the equivalence premium, benefit scaling, and the zero-term and zero-discount boundaries. The capstone combines positivity, zero expected loss, uniqueness and benefit scaling.

The only previously published actuarial definition imported is the $n$-year term-assurance present value from Mission II. The mathematical arguments use finite sums and integration under a probability measure, rather than relying on unproved statements from other draft missions. All declarations in this owner Draft are mathematical proof targets. Their presence in a proposal does not mean that their proofs have been accepted.

Gerber [4, §5.3.1] independently develops annual-premium term insurance, including its realised loss and the net premium equations (5.3.9)–(5.3.11). Those results corroborate the payment timing and the equivalence-premium construction adopted here.

References

[1] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Cambridge University Press, book DOI 10.1017/CBO9780511800146. See §6.4, The present value of future loss random variable, and §6.5.1, Net premiums, particularly equations (6.1)–(6.2).

[2] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, ISBN 9781118782460. See §15.6.1, The equivalence principle, and §15.6, The stochastic approach to premiums.

[3] Open Actuarial Textbooks Project, Life Contingencies, Chapter 3, Basic Life Contingent Benefits, §3.2.2, equation (3.8), finite term assurance.

[4] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 5, Net Premiums, particularly §5.3.1, equations (5.3.9)–(5.3.11), on finite term insurance and net annual premiums.

Motivation and actuarial context

Whole-life assurance and a whole-life annuity-due are two fundamental life-contingent contracts. The assurance provides one unit of benefit at the end of the year of death, whereas the annuity-due provides one unit at the start of each year that the life is still eligible for payment, including time zero. Under a constant positive effective annual interest rate, their realised present values satisfy an exact finite-geometric-series identity. This provides an unusually direct connection between insurance benefits, annuity values and the distribution of curtate future lifetime. The relationship and its expected-value and variance consequences are stated in Life Contingencies, Chapter 3, equations (3.13)–(3.14) [1].

This mission formally develops that equivalence in Lean, starting from the individual cashflows and ending with a capstone theorem that combines the pointwise, expectation and variance results. It also isolates the assumptions needed for these results, supplies reusable bounds and integrability lemmas, and treats the zero-interest boundary separately. Related treatments of whole-life insurance and life annuities are available in the actuarial textbooks of Promislow [2] and Dickson, Hardy and Waters [3]. The mission's declarations are proposed proof obligations, not claims that every theorem has already been proved.

Contracts and notation

Let $K:\Omega\to\mathbb N$ be the natural-valued curtate future lifetime of the insured life. In outcome $\omega$, death occurs during policy year $K(\omega)+1$. Let $i>0$ be a flat, deterministic annual effective interest rate and define

$$v=\frac{1}{1+i},\qquad 0<v<1.$$

The unit whole-life assurance, payable at the end of the year of death, has realised present value

$$Z_A(\omega)=v^{K(\omega)+1}.$$

This is the assurance contract defined in [1, §3.2.1, equation (3.7)]. The unit whole-life annuity-due makes payments at dates $0,1,\ldots,K(\omega)$ and therefore has realised present value

$$Z_D(\omega)=\sum_{k=0}^{K(\omega)}v^k.$$

The annuity cashflow and the flat-interest specialisation are discussed in [1, §3.3.1, equations (3.11) and (3.13)]. The difference in timing is essential: the assurance payment occurs at $K+1$, one year after the last annuity-due payment at $K$.

Pointwise assurance–annuity equivalence

For $i>0$, the finite geometric sum gives

$$\begin{aligned} Z_D(\omega) &=\frac{1-v^{K(\omega)+1}}{1-v}\\ &=\frac{1+i}{i}\bigl(1-Z_A(\omega)\bigr). \end{aligned}$$

Equivalently, writing $d=i/(1+i)=1-v$ for the annual effective rate of discount,

$$Z_A(\omega)+dZ_D(\omega)=1.$$

These are pathwise statements. They hold for every realised natural-valued lifetime and require no assumptions about a mortality law or independence between annual survival events. They formalise the finite-series relationship in [1, equation (3.13)], rather than relying on an approximation or a selected life table.

Expected present values and variance

Now let $P$ be a probability measure on $\Omega$ and suppose that $K$ is measurable. The assumption $i>0$ implies $0<v<1$, and the realised values obey

$$0<Z_A(\omega)\le 1, \qquad 0\le Z_D(\omega)\le\frac{1+i}{i}.$$

These deterministic bounds establish integrability, including the required second moments, even where $K$ has unbounded support across outcomes. Taking expectations of the pointwise identity yields

$$\mathbb E_P[Z_D] =\frac{1+i}{i}\left(1-\mathbb E_P[Z_A]\right).$$

If $A_x=\mathbb E_P[Z_A]$ and $\ddot a_x=\mathbb E_P[Z_D]$ denote the corresponding actuarial values for a life aged $x$, then

$$\ddot a_x=\frac{1+i}{i}(1-A_x).$$

Translation by a constant leaves variance unchanged, and scaling multiplies variance by the square of the factor. Thus

$$\operatorname{Var}_P(Z_D) =\left(\frac{1+i}{i}\right)^2 \operatorname{Var}_P(Z_A).$$

The EPV and variance identities are stated in [1, equation (3.14)]. In particular, the variance factor is squared. No independence assumption is imposed: the assurance and annuity values are functions of the same lifetime, and the variance identity follows from their exact affine relationship.

Interest-rate boundary and scope

At zero interest, $v=1$, the whole-life annuity-due has realised value

$$Z_D(\omega)=\sum_{k=0}^{K(\omega)}1=K(\omega)+1.$$

This is a separate pointwise theorem. The expression $(1+i)/i$ is undefined at $i=0$, and an arbitrary distribution of $K$ need not give a finite undiscounted expected payment count or a finite variance. An expectation theorem at zero interest would require a suitable first-moment assumption on $K$, while a finite variance requires a second moment.

The simple assurance–annuity equivalence also relies on a flat deterministic interest basis. Under a non-flat yield curve the discounted cashflow series has varying discount factors and the same fixed geometric multiplier does not generally exist. The source expressly makes this limitation in [1, §3.3.1].

Formalisation and proof structure

The mission adds one definition, the whole-life assurance realised present value, together with eleven supporting theorems and one capstone. The supporting graph establishes discount-factor positivity, the finite geometric sum, assurance positivity, the pointwise and unit identities, a boundedness lemma, integrability of both contracts, and their expected-value and variance relationships. A separate theorem handles zero interest. The capstone combines the key pathwise identity, expected-value relation, variance scaling and unit identity.

The only imported published actuarial definition is the existing whole-life annuity-due present-value definition from the earlier mission. The assurance definition is introduced here. The proposed proofs should use the appropriate finite-sum and probability-measure results from the pinned Mathlib, and no unproved theorem from another actuarial mission should be treated as an available proof dependency. These formal dependencies are distinct from the published textbook references below.

References

[1] Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, Basic Life Contingent Benefits. Principal results: §3.3.1, equations (3.13)–(3.14), on the flat-interest annuity identity, EPV and variance. Assurance definition: §3.2.1, equation (3.7). Whole-life annuities: §3.3.1, equations (3.11)–(3.12).

[2] Promislow, S. David (2010), Fundamentals of Actuarial Mathematics, Wiley. Publisher book record, particularly Chapters 4, Life Annuities, and 5, Life Insurance. This provides wider actuarial background rather than an attribution of equations (3.13)–(3.14) to Promislow.

[3] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2019), Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, particularly Chapters 4, Insurance Benefits, 5, Annuities, and 12, Yield Curves and Non-Diversifiable Risk. These chapters provide context for contract valuation and the distinction between flat and varying interest rates.

Motivation and actuarial context

A whole-life annuity provides payments contingent on the annuitant remaining alive. A guaranteed life annuity adds a minimum number of payments, irrespective of early death. This alters the insurer's cashflows, since payments during the guarantee period are certain and subsequent payments depend on survival. It is an important contract structure for retirement income and provides a natural bridge between annuities certain, whole-life annuities and deferred life annuities. The payment definitions and expected present values are given in the Open Actuarial Textbooks Project's Life Contingencies, Chapter 3, §3.3.4, equations (3.19) and (3.20) [1]. Guaranteed payments are also covered within the broader treatments of life annuities in [2] and [3].

The objective of this mission is to formalise both annuities payable in advance (due) and annuities payable in arrears (immediate), including their exact cashflow decompositions, expected values and variances. It develops the mathematical justification for infinite survival-weighted sums when the distribution of lifetime is not bounded above. These are formal theorem targets to be proved, rather than results already established merely by publishing the statements.

Contract definition and payment timing

Let $K:\Omega\to\mathbb N$ be curtate future lifetime, where $K(\omega)$ is the number of complete future years lived in outcome $\omega$. Let $n\in\mathbb N$ be the number of guaranteed annual payments and let $v\in\mathbb R$ be a constant per-period discount factor. Each payment has unit amount, and an empty sum has value zero.

For an annuity-due, payments occur at times $0,1,\ldots$. The first $n$ payments at times $0,\ldots,n-1$ are certain. Additional payments occur at times $n,\ldots,K(\omega)$, if any.

For an annuity-immediate, payments occur at times $1,2,\ldots$. The first $n$ payments at times $1,\ldots,n$ are certain. Additional payments occur at times $n+1,\ldots,K(\omega)$, if any. The separate timing conventions are essential to the guaranteed-period boundary cases.

Realised present-value identities

The guaranteed annuity-due has realised present value

$$\begin{aligned} Z_{G,\mathrm{due}}(\omega) &=\sum_{0\le k<\max\{K(\omega)+1,n\}}v^k\\ &=\underbrace{\sum_{0\le k<n}v^k}_{C_{\mathrm{due}}} +\underbrace{\sum_{n\le k\le K(\omega)}v^k}_{D_{\mathrm{due}}(\omega)}. \end{aligned}$$

For an annuity-immediate, the corresponding identity is

$$\begin{aligned} Z_{G,\mathrm{imm}}(\omega) &=\sum_{0\le k<\max\{K(\omega),n\}}v^{k+1}\\ &=\underbrace{\sum_{0\le k<n}v^{k+1}}_{C_{\mathrm{imm}}} +\underbrace{\sum_{n\le k<K(\omega)}v^{k+1}}_{D_{\mathrm{imm}}(\omega)}. \end{aligned}$$

Here $C$ is the deterministic annuity-certain prefix and $D$ is the survival-dependent deferred continuation. The equations reproduce the underlying payment timing of [1, equations (3.19)–(3.20)]. They also connect to the deferred-annuity formulas in [1, equations (3.17)–(3.18)]. Additional pointwise theorems express each guaranteed value as its corresponding whole-life value plus the extra payments required when death occurs during the guarantee.

Expected values and variance

Let $P$ be a probability measure and assume that $K$ is measurable. For the analytical theorems, impose $0\le v<1$. Write $\Pr(K\ge k)=P(\{\omega:K(\omega)\ge k\})$. The expected present values are

$$\mathbb E_P[Z_{G,\mathrm{due}}] =\sum_{0\le k<n}v^k +\sum_{k=n}^{\infty}v^k\Pr(K\ge k)$$

and

$$\mathbb E_P[Z_{G,\mathrm{imm}}] =\sum_{0\le k<n}v^{k+1} +\sum_{k=n}^{\infty}v^{k+1}\Pr(K\ge k+1).$$

The fixed prefix and survival-weighted tail are those in the guaranteed-annuity textbook formulas [1]. A formal proof must establish measurability and integrability and justify taking expectation through the infinite sum. The geometric bound supplied by $0\le v<1$ makes these conclusions possible for a natural-valued lifetime distribution with unbounded support. No maximum attainable lifetime is assumed.

Since $C_{\mathrm{due}}$ and $C_{\mathrm{imm}}$ are deterministic, adding them changes the expected values but does not change the variances:

$$\begin{aligned} \operatorname{Var}_P(Z_{G,\mathrm{due}}) &=\operatorname{Var}_P(D_{\mathrm{due}}),\\ \operatorname{Var}_P(Z_{G,\mathrm{imm}}) &=\operatorname{Var}_P(D_{\mathrm{imm}}). \end{aligned}$$

These variance equalities are derived theorems, based on translation invariance of variance, rather than separate numbered statements in §3.3.4. The general survival-cashflow moment framework in [1, §3.1.1, equations (3.3), (3.5)–(3.6)] supplies background. No independence assumption between annual survival events is introduced.

Boundary cases and formal proof structure

When $n=0$, both guaranteed annuities reduce to their corresponding whole-life annuities. When $K(\omega)=n$, the due annuity can still pay at time $n$, while the immediate deferred continuation is empty and the $n$ guaranteed immediate payments remain. When $K(\omega)=0$, the due contract has its time-zero payment, and an immediate contract with $n>0$ still pays the $n$ certain instalments.

The finite realised-value identities hold algebraically for every real $v$, including zero, one and negative values. The stated integrability, infinite expected-value and variance theorems deliberately use $0\le v<1$. In particular, an arbitrary undiscounted lifetime distribution need not have a finite expected payment count.

The mission introduces four definitions, fourteen supporting theorems and one capstone. The intended proof path establishes cashflow decompositions and zero-guarantee identities, develops geometric bounds and measurable survival events, proves the expected-value and variance relations, and then assembles the capstone from the supporting results.

The formal dependency graph reuses six published Prove2Me declarations: the curtate-survival event and its measurability theorem, together with whole-life and deferred present-value definitions for due and immediate annuities. These are technical dependencies, distinct from the bibliographic sources below. An unproved theorem from an earlier mission is not treated as an available proof dependency.

References

[1] Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, Basic Life Contingent Benefits. Principal source: §3.3.4, equations (3.19)–(3.20). Related foundations: §3.3.1 (3.11)–(3.12), §3.3.3 (3.17)–(3.18), and §3.1.1 (3.3), (3.5)–(3.6). The explanatory sentence after (3.20) calls the contract deferred, although the section heading and displayed expressions describe a guaranteed annuity.

[2] Promislow, S. David (2010), “Life Annuities”, Chapter 4 of Fundamentals of Actuarial Mathematics, Wiley, DOI: 10.1002/9781119971528.ch4. The chapter's published summary includes guaranteed payments.

[3] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2019), Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, Chapter 5, Annuities. General context for life-annuity valuation.

Motivation

Whole-life and deferred life annuities extend survival-contingent payments beyond a fixed policy term. A whole-life annuity may pay on each eligible anniversary until death, while a deferred annuity begins after a specified waiting period. Both are standard components of pension and life-contingency valuation.

Actuarial Mathematics I established how to value finite cashflows. Missions III and IV provide curtate survival events and temporary annuity schedules. This mission develops the infinite-horizon valuation step: it justifies the lifetime payment series and its expected present value, including the conditions under which expectation can be exchanged with the discounted survival series.

The mortality and discount model

Let $(\Omega,\mathcal F,P)$ be a probability space and let $K:\Omega\to\mathbb N$ be a measurable curtate future lifetime. Define the survival event at time $k$ by

$$S_k=\{\omega:K(\omega)\ge k\}.$$

For expected present value statements, assume a deterministic annual discount factor $v$ satisfying

$$0\le v<1.$$

This condition provides a geometric bound on the payments and justifies exchanging expectation with the discounted survival series. No particular life table or independence between survival dates is assumed, and $K$ need not have a finite upper bound.

Whole-life annuities

With unit payments in advance, a life with realised curtate lifetime $K(\omega)$ receives a payment at time zero and at each subsequent beginning-of-year date through time $K(\omega)$. Its present value can be written

$$Z_{\mathrm{WL,due}}(\omega)=\sum_{k=0}^{K(\omega)}v^k =\sum_{k=0}^{\infty}v^k\mathbf1_{\{K(\omega)\ge k\}}.$$

Its expected present value, given by equation (3.11), is

$$\mathbb E_P[Z_{\mathrm{WL,due}}] =\sum_{k=0}^{\infty}v^kP(S_k).$$

A whole-life annuity in arrears pays at times $1,\ldots,K(\omega)$, with no payment at time zero:

$$Z_{\mathrm{WL,immediate}}(\omega) =\sum_{k=0}^{\infty}v^{k+1}\mathbf1_{\{K(\omega)\ge k+1\}}.$$

Equation (3.12) gives its expected present value:

$$\mathbb E_P[Z_{\mathrm{WL,immediate}}] =\sum_{k=0}^{\infty}v^{k+1}P(S_{k+1}).$$

The payment in advance at time zero is certain, and the remaining payments match the arrears stream. Thus their pointwise and expected values satisfy

$$Z_{\mathrm{WL,immediate}}=Z_{\mathrm{WL,due}}-1.$$

Deferred life annuities

For a deferral period $n\in\mathbb N$, a deferred annuity in advance has its first possible payment at time $n$, with no payments before then. Equation (3.17) gives its indicator representation:

$$Z_{\mathrm{deferred,due}} =\sum_{k=n}^{\infty}v^k\mathbf1_{\{K\ge k\}},$$

and its expected present value is

$$\mathbb E_P[Z_{\mathrm{deferred,due}}] =\sum_{k=n}^{\infty}v^kP(S_k).$$

A deferred annuity in arrears starts at time $n+1$ and requires survival to that date. Equation (3.18) gives

$$Z_{\mathrm{deferred,immediate}} =\sum_{k=n}^{\infty}v^{k+1}\mathbf1_{\{K\ge k+1\}},$$

with expected present value

$$\mathbb E_P[Z_{\mathrm{deferred,immediate}}] =\sum_{k=n}^{\infty}v^{k+1}P(S_{k+1}).$$

The timing conditions matter. If $K=n$, there is a due payment at time $n$, but no immediate payment at time $n+1$. When $n=0$, each deferred annuity is its corresponding whole-life annuity.

Whole-life values minus temporary annuities

The discounted cashflows in equations (3.17) and (3.18) are the corresponding whole-life streams with the first $n$ potential payment dates removed. Pointwise, this gives

$$Z_{\mathrm{deferred,due}} =Z_{\mathrm{WL,due}} -\sum_{k=0}^{n-1}v^k\mathbf1_{S_k},$$

and

$$Z_{\mathrm{deferred,immediate}} =Z_{\mathrm{WL,immediate}} -\sum_{k=0}^{n-1}v^{k+1}\mathbf1_{S_{k+1}}.$$

Taking expectations gives the source's deferred-annuity valuation differences: each deferred annuity's expected present value is the corresponding whole-life expected present value less that of the temporary annuity.

The finite prefix sums reproduce the temporary-annuity schedules from Mission IV without importing its unpublished declarations. Mission IV remains a Draft, so its new theorems are not available as published imports. The two published curtate survival results from Mission III can be used.

Formalisation and analytical scope

The four new definitions use a finite payment sum for each realised natural-valued lifetime. Each realised cashflow therefore has finite support, even when the possible lifetimes are unbounded. The milestones connect these finite realised sums with infinite survival-indicator series, prove the deferred and initial-payment decompositions, establish integrability under the geometric discount condition, and derive four infinite expected-value formulas.

The capstone combines these formulas and decompositions for the same probability measure, curtate lifetime, discount factor and deferral period. The measure need not arise from a particular mortality model.

The condition $0\le v<1$ applies to the expected present value claims. Pointwise present value identities hold for any real $v$, since each realised natural-valued lifetime is finite and so produces only finitely many payments. At $v=1$, an arbitrary lifetime distribution can have infinite expectation, so finite expected values cannot be assumed. The condition used here is sufficient; it is not claimed to be the sharpest possible condition under the source's financial discount assumptions.

Source and dependencies

The primary source is Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3 §3.3.1 equations (3.11)–(3.12) and §3.3.3 equations (3.17)–(3.18). The temporary prefixes are the payment schedules from §3.3.2 equations (3.15)–(3.16), and the general expectation-of-cashflows step is equation (3.3).

• https://openacttextdev.github.io/LifeCon/C-SimpleBenefit.html
• https://openacttextdev.github.io/LifeCon/C-ModelingLifeTimes.html

This mission covers whole-life and deferred annuities. Guaranteed-period benefits, flat-interest assurance–annuity equivalence and continuous-time intensity-based valuations are separate later projects.

Motivation

A life annuity pays a series of amounts while its recipient survives. A term assurance pays at most once during the policy term, whereas a temporary life annuity may pay several times. The indicators for its payments can therefore overlap, so a correct second-moment calculation must retain the dependence between them.

This mission formalises temporary life annuities payable in advance and in arrears, using the finite contingent-cashflow framework established in Actuarial Mathematics I. It reuses the curtate survival-event definition from Actuarial Mathematics III.

Survival events and dependence

Let $(\Omega,\mathcal F,P)$ be a probability space, and let $K:\Omega\to\mathbb N$ be the measurable curtate future lifetime, counting completed years. The event that the life survives to time $k$ is

$$S_k=\{\omega:K(\omega)\ge k\}.$$

These events are nested. For all $i,j\in\mathbb N$,

$$S_i\cap S_j=S_{\max(i,j)}.$$

Consequently their indicators satisfy

$$\mathbf1_{S_i}(\omega)\mathbf1_{S_j}(\omega)=\mathbf1_{S_{\max(i,j)}}(\omega).$$

This matters for second moments: survival to one payment date and survival to another are not mutually exclusive. Their intersection is survival to the later date. No independence assumption is made.

Temporary life annuity payable in advance

A unit temporary life annuity payable in advance makes up to $n$ payments, at times $k=0,\dots,n-1$. The payment at time $k$ is made if $K\ge k$. With deterministic annual discount factor $v$, its random present value is

$$Z_{\mathrm{due}}=\sum_{k=0}^{n-1}v^k\mathbf1_{S_k}.$$

The expected present value is

$$\mathbb E_P[Z_{\mathrm{due}}]=\sum_{k=0}^{n-1}v^kP(S_k).$$

These are the temporary-annuity-in-advance identities in Chapter 3, equation (3.15). The first payment, at time zero, is certain whenever $n\ge1$.

Temporary life annuity payable in arrears

A unit temporary life annuity payable in arrears has potential payments at times $k+1$, for $k=0,\dots,n-1$. A payment is made only if $K\ge k+1$:

$$Z_{\mathrm{immediate}}=\sum_{k=0}^{n-1}v^{k+1}\mathbf1_{S_{k+1}}.$$

Its expected present value is

$$\mathbb E_P[Z_{\mathrm{immediate}}]=\sum_{k=0}^{n-1}v^{k+1}P(S_{k+1}).$$

These are the corresponding payment-in-arrears identities in equation (3.16). In particular, a life with $K=0$ can receive the first payment of the annuity in advance, but no payment from the annuity in arrears.

Second moments and variance

The general moment calculations in Section 3.1.1 apply to the payment schedules in equations (3.15) and (3.16). Intersections of survival events reduce to the requirement to survive to the later date.

For payments in advance, the finite double-sum second moment is

$$\mathbb E_P[Z_{\mathrm{due}}^2]= \sum_{i=0}^{n-1}\sum_{j=0}^{n-1}v^{i+j}P(S_{\max(i,j)}).$$

For payments in arrears, it is

$$\mathbb E_P[Z_{\mathrm{immediate}}^2]= \sum_{i=0}^{n-1}\sum_{j=0}^{n-1} v^{i+j+2}P(S_{\max(i+1,j+1)}).$$

These are ordered double sums. Every ordered pair of payment dates contributes, including the diagonal terms and both orders of each off-diagonal pair. The corresponding variances are

$$\operatorname{Var}_P(Z_{\mathrm{due}})= \mathbb E_P[Z_{\mathrm{due}}^2]-\bigl(\mathbb E_P[Z_{\mathrm{due}}]\bigr)^2,$$ $$\operatorname{Var}_P(Z_{\mathrm{immediate}})= \mathbb E_P[Z_{\mathrm{immediate}}^2]-\bigl(\mathbb E_P[Z_{\mathrm{immediate}}]\bigr)^2.$$

The double-sum second-moment results are formal specialisations of the general moment equations (3.5)–(3.6). They are not additional numbered results in Section 3.3.2, which gives the expectation and present-value identities in equations (3.15) and (3.16).

Formalisation goal

The main theorem packages the expected values, second moments and variances of both annuities under the same $P$, $K$, $v$ and $n$. Its supporting milestones establish the nesting of survival events and the products of their indicators, the finite payment schedules, and the successive valuation identities.

Both definitions are instances of the generic finite present-value construction from Actuarial Mathematics I. The curtate survival event is imported from Actuarial Mathematics III. Together, these provide reusable foundations for later missions on deferred and guaranteed life annuities.

The finite sums cover $n=0$, when both annuities have zero present value, and $n=1$, when the advance annuity includes the certain payment at time zero and the arrears annuity pays only if the life has completed at least one year. Algebraically, the identities allow any real $v$. In actuarial applications, $v$ is normally positive. This mission asserts neither convergence of an infinite whole-life annuity nor statistical independence of survival payments.

Source references

The primary source is Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Open Actuarial Textbooks Project, Chapter 3 §3.1.1 equations (3.5)–(3.6) and §3.3.2 equations (3.15)–(3.16).

• https://openacttextdev.github.io/LifeCon/C-SimpleBenefit.html
• https://openacttextdev.github.io/LifeCon/C-ModelingLifeTimes.html
• https://prove2.me/missions/Actuarial_Mathematics_I%3A_Present_Values_of_Contingent_Cashflows

This is a draft mission and has not yet been published. It formalises finite-term annual payments. Continuous payment timing, deferred whole-life payments, guaranteed-period annuities and infinite valuation are planned separately.

Motivation

An endowment assurance pays a fixed benefit either when the policyholder dies during the policy term or when the policy reaches its maturity date. It therefore brings death-contingent and survival-contingent payments together in one valuation framework.

Actuarial Mathematics I established general identities for valuing finite contingent cashflows. Mission II formalised unit term assurance and the mutually exclusive events of death in different policy years. This mission extends those foundations to pure endowments and endowment assurances, covering payment dates, expected present values, second moments and variances.

Exact lifetime and curtate lifetime

Let $(\Omega,\mathcal F,P)$ be a probability space. The exact future lifetime $T$ takes nonnegative real values, while the curtate future lifetime $K$ records completed years. Their relationship is

$$K(\omega)\le T(\omega)<K(\omega)+1.$$

For a term $n\in\mathbb N$, the textbook's pure-endowment payment in equation (3.9) depends on strict survival:

$$E_n^{>}=\{\omega:T(\omega)>n\}.$$

The endowment-assurance formula in equation (3.10), by contrast, uses a maturity payment when $K+1>n$, equivalently when $K\ge n$. Define

$$E_n^{\ge}=\{\omega:K(\omega)\ge n\}.$$

These events differ if death occurs exactly at time $n$. Given the relationship between exact and curtate lifetime,

$$E_n^{\ge}=E_n^{>}\cup\{\omega:T(\omega)=n\}.$$

Thus equation (3.9) uses exact lifetime and excludes death at $T=n$, whereas equation (3.10) uses curtate lifetime and includes it, since then $K=\lfloor T\rfloor=n$. This endpoint identity clarifies the textbook's conventions; it is not itself a numbered textbook result. No assumption is made that death at a policy anniversary has probability zero.

Pure-endowment benefit

Under the strict exact-lifetime convention, a unit pure endowment payable at time $n$ has random present value

$$Z_{\mathrm{pure}}=v^n\mathbf1_{\{T>n\}}.$$

Equation (3.9) gives its expected value and variance:

$$\mathbb E_P[Z_{\mathrm{pure}}]=v^nP(T>n),$$ $$\operatorname{Var}_P(Z_{\mathrm{pure}}) =v^{2n}P(T>n)\bigl(1-P(T>n)\bigr).$$

Here $v$ is a deterministic annual discount factor. The Lean algebra permits any real $v$, including the conventional case of a positive discount factor.

Endowment-assurance benefit

The endowment assurance pays a unit benefit at the end of the policy year of death if death occurs within the first $n$ years. Otherwise, it pays at time $n$. As in equation (3.10), its present value is defined by

$$Z_{\mathrm{endow}}(\omega)=v^{\min(K(\omega)+1,n)}.$$

The theorem expresses this value as the sum of the unit term assurance from Mission II and the curtate maturity payment:

$$Z_{\mathrm{endow}} =\sum_{k=0}^{n-1}v^{k+1}\mathbf1_{\{K=k\}} +v^n\mathbf1_{\{K\ge n\}}.$$

The death benefit and maturity benefit are mutually exclusive. This gives the expected value and second moment:

$$\mathbb E_P[Z_{\mathrm{endow}}] =\sum_{k=0}^{n-1}v^{k+1}P(K=k)+v^nP(K\ge n),$$ $$\mathbb E_P[Z_{\mathrm{endow}}^2] =\sum_{k=0}^{n-1}v^{2(k+1)}P(K=k)+v^{2n}P(K\ge n).$$

The variance is then

$$\operatorname{Var}_P(Z_{\mathrm{endow}}) =\mathbb E_P[Z_{\mathrm{endow}}^2] -\bigl(\mathbb E_P[Z_{\mathrm{endow}}]\bigr)^2.$$

Formalisation goals and milestones

The formalisation proves measurability of the strict and curtate survival events, the exact boundary-event bridge, disjointness of death during the term from survival to maturity, and the pure-endowment expectation and variance. It also proves the endowment decomposition, expectation, second moment and variance. The formal capstone brings these results together under one probability measure, using the same exact and curtate lifetimes, term and discount factor. It states the boundary bridge explicitly and includes the pure-endowment mean and variance, along with the endowment present value, mean, second moment and variance.

The formalisation reuses Mission II's definition of term-assurance present value rather than reconstructing it. The main namespace remains ActuarialValuation, so later life-annuity missions can use the survival-event lemmas.

The edge cases require care. When $n=0$, the endowment assurance pays immediately. The strict pure endowment, however, still depends on whether $T>0$. Death at exactly $T=n$ is represented separately and is never excluded by an unstated continuity assumption. The finite real-valued Lean identities permit negative or zero discount factors as a mathematical generalisation, although ordinary actuarial applications use positive discount factors.

Source and scope

The primary source is the Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 2 §2.4.3, Chapter 3 §3.2.3 equation (3.9) and §3.2.4 equation (3.10).

• https://openacttextdev.github.io/LifeCon/C-ModelingLifeTimes.html
• https://openacttextdev.github.io/LifeCon/C-SimpleBenefit.html
• https://prove2.me/missions/Actuarial_Mathematics_I%3A_Present_Values_of_Contingent_Cashflows

Mission II, Actuarial Mathematics II: Term Assurance Present Values and Moments, is under moderator review at drafting time. Its relevant published definitions and theorem IDs are referenced directly.

This mission formalises unit benefits over a finite term with deterministic annual discounting. It establishes a finite-horizon result, not an infinite-horizon theorem. It does not cover immediate death benefits, arbitrary benefit scales, lifetime-dependent interest, infinite whole-life present values or the full continuous-time theory of mortality.

Why single-use information can underestimate communication

A sender can encode a classical message in a quantum state, transmit that state through a noisy quantum channel, and let a receiver measure the output. For researchers studying classical communication over quantum systems, the question is whether evaluating one channel use captures the benefit of encoding across several uses. Hastings established that the relevant information quantity can violate additivity when joint inputs are allowed. Hastings, 2009.

The result contributed here concerns the size of that discrepancy in finite dimensions. It gives channels for which positive single-use information is arbitrarily small while both the absolute two-use additivity gap and the relative benefit of two uses are arbitrarily large. The paper's introduction states the gap, capacity, and separation consequences; the released Lean theorem packages the small-information, gap, and ratio conclusions into one common-witness statement. Revised manuscript, Section 1, headline Lean theorem.

Channels, states, and information in bits

A finite-dimensional quantum channel $T:M_a(\mathbb C)\to M_b(\mathbb C)$ is a completely positive, trace-preserving linear map on complex matrices, where the positive integers $a,b$ are its input and output dimensions. A density matrix $\rho$ is a positive semidefinite matrix with trace one. Such matrices represent the possible input states. The released development represents a channel by finitely many rectangular Kraus matrices $A_k$, satisfying $\sum_k A_k^*A_k=I_a$, with action $T(X)=\sum_k A_kXA_k^*$. Concrete channel definitions.

The von Neumann entropy in bits is $S(\rho)=-\sum_j\lambda_j\log_2\lambda_j$, where $\lambda_j$ are the eigenvalues of $\rho$, using $0\log 0=0$. A finite ensemble consists of density matrices $\rho_x$ and real probabilities $p_x\ge0$ with $\sum_xp_x=1$. The Holevo quantity is

$$\chi(T)=\sup_{\{p_x,\rho_x\}} \left[S\!\left(\sum_xp_xT(\rho_x)\right) -\sum_xp_xS(T(\rho_x))\right].$$

The supremum includes all normalized finite ensembles. For two uses, $T^{\otimes2}$ acts on joint inputs, including states entangled between the uses. Write $\chi_2(T)=\chi(T^{\otimes2})$, $\Delta_\chi(T)=\chi_2(T)-2\chi(T)$, and, when $\chi(T)>0$, $r_2(T)=\chi_2(T)/(2\chi(T))$. These are the released definitions chi, chiTwo, gap, and twoUseRatio. Definitions.

The broader release also studies operational classical capacity $C(T)$: the supremum of achievable classical message rates in bits per use. Its independent definition uses actual density-matrix codewords, a normalized positive-operator-valued measurement decoder, and average Born decoding error tending to zero over all positive block lengths. Arbitrary block inputs and joint decoding are allowed. That coding development provides context for the result; it is a separate released branch outside this contribution's initial import. Released operational definition.

Formalization targets

Simultaneous small information, large absolute gap, and large ratio

The headline statement is

$$\forall\varepsilon>0\;\forall A,R\in\mathbb R\;\exists T: \quad 0<\chi(T)\le\varepsilon,\qquad \Delta_\chi(T)\ge A,\qquad r_2(T)\ge R.$$

One channel witnesses every inequality. The lower-bound thresholds $A,R$ are arbitrary real numbers; they are not restricted to positive values in the Lean statement. Input and output dimensions may depend on the thresholds. The goal imposes no hard-coded dimension bound or numerical constant. It is the exact statement of Nonadditivity.DeterministicConsequences.exists_small_chi_large_gap_and_ratio. Source.

The supporting separation statement uses a sequence of genuine finite channels $T^{(K)}$ with

$$\chi(T^{(K)})\longrightarrow0,\qquad \frac{\chi_2(T^{(K)})}{2}\longrightarrow+\infty.$$

The separation statement is already proved for the selected deterministic family. It gives the two information limits asserted in the manuscript's Corollary 1.3, with no analytic channel-existence assumption. The formal family is totalized at its first two indices by the one-dimensional identity channel; this finite prefix does not affect either limit. Its members have positive single-use Holevo information for every $K\ge2$. Released family, positivity, and limits.

What the result and its formal proofs provide

The theorem gives unbounded absolute Holevo additivity gaps and unbounded two-use ratios for the same witnesses, even while their single-use information is arbitrarily small. This supplies an existence result rather than an efficient method for finding small channels with practical parameters. The manuscript separately proves explicit sufficient input dimensions; those bounds are not conclusions of the headline theorem. Manuscript, Corollaries 1.2–1.3.

The mathematical result is proved, and its principal endpoints already have machine-checked Lean proofs in release v1.0.0. This contribution imports the existing deterministic separation theorem and its dependency library, preserving their source provenance and proofs. The reusable material includes density matrices, concrete channels, entropy, finite ensembles, tensor products, and the finite-channel construction. Independent review of the correspondence between the formal statements and the manuscript remains useful. Release and verification scope.

The broader release additionally proves $C(T)=\sup_{m\ge1}\chi(T^{\otimes m})/m$ from independently defined physical codes, implying $C(T)-\chi(T)\ge\Delta_\chi(T)/2$. It also proves a common-witness theorem combining small positive information with arbitrary capacity gain and two-use ratio. Those operational results are separate released context, rather than targets or imported milestones of this contribution. They concern unassisted memoryless communication and do not assert distinct-channel capacity nonadditivity or a strong converse. Released coding identity, released operational consequence.

Why the uniform bounds matter

A separate information estimate for each channel factor does not control inputs entangled across an entire block. The construction needs bounds valid for every such joint input, while retaining the favorable two-use behavior. Likewise, convergence of averaged matrix moments alone need not control exceptional eigenvalues and therefore cannot replace the needed norm control. These are substantive uniformity requirements in the paper's construction. Manuscript, Section 1.

Regrouping tensor powers of one fixed channel is insufficient for a gap linear in the regrouping length: the manuscript shows $\Delta_\chi(T^{\otimes m})/m\to0$ for a fixed $T$. The existential goal instead allows channel dimensions and the channel itself to vary. Fixed-channel limitation.

Formalization scope and conventions

The imported representation is ActualConsequences.FiniteQuantumChannel: finite, nonempty input and output index types, a finite environment index type, and a concrete Kraus channel. Entropy is computed spectrally with natural logarithms internally; holevoBits divides by $\ln2$. Supremum and infimum uses are accompanied by the developed nonemptiness and boundedness results. Positive tensor powers are indexed by a natural number $n$ meaning $n+1$ uses. Strict positivity of the goal's $\chi(T)$ prevents division-by-zero interpretations of its ratio. The channel and information quantities must retain these physical definitions; numerical records assigned the desired values would not formalize the result. Formal representation, bit conversion.

The headline proof uses the alternate deterministic finite-channel construction. It does not assert the prescribed-dimension result. The imported library provides complex matrix analysis, positivity and trace normalization, tensor products, entropy inequalities, finite ensembles, and the construction's finite group and moment infrastructure. The full manuscript remains outside the completed formalization: general Haar convergence interfaces and the broader finite-dimensional realization statement retain their documented limitations. The release's correspondence findings remain qualified; no complete semantic audit or independent human certification is claimed. Formalization status, statement review.

Selected references

• Jinzhao Wang, Unbounded Holevo additivity gaps in finite dimensions, arXiv preprint, 2026. arXiv:2609.18222v2; revised manuscript retained in the formalization release.
• M. B. Hastings, Superadditivity of communication capacity using entangled inputs, Nature Physics 5, 255–257, 2009. arXiv:0809.3972.
• A. S. Holevo, The capacity of the quantum channel with general signal states, IEEE Transactions on Information Theory 44, 269–273, 1998. DOI:10.1109/18.651037.
• B. Schumacher and M. D. Westmoreland, Sending classical information via noisy quantum channels, Physical Review A 56, 131–138, 1997. DOI:10.1103/PhysRevA.56.131.
• P. W. Shor, Equivalence of additivity questions in quantum information theory, Communications in Mathematical Physics 246, 453–472, 2004. arXiv:quant-ph/0305035.
• Nonadditivity project contributors, Holevo Additivity Gap: Lean certificates, software release v1.0.0, 2026. Release, source commit 635aa93eb3a2310b79fd5371e2ce311914ec5887.

Motivation: comparing quantum processes

A quantum channel describes a physical process that transforms a quantum state into another state. Comparing two channels means comparing their possible outputs, including outputs obtained when the input is entangled with a reference system. This distinction matters in quantum information: an experiment can retain a reference while sending the other part of an entangled state through an unknown process. The resulting measure of distinguishability should account for that experiment.

For states, several divergence measures approach relative entropy when their order parameter approaches one. For channels, optimization over inputs and arbitrarily many channel uses introduces an additional question: does this continuity survive those optimizations? Jinzhao Wang and Yuxiang Yang answer that question for the regularized, stabilized sandwiched Rényi divergence in Continuity of Regularized Channel Rényi Divergences, arXiv:2609.28635v1, Theorem 1. This mission contributes the completed result and its supporting formal infrastructure.

Setting: states, references, and repeated uses

Let $H$ and $K$ be nonzero finite-dimensional complex Hilbert spaces. A density operator is a positive operator with trace one. Two channels $N,M:\mathcal L(H)\to\mathcal L(K)$ are completely positive, trace-preserving linear maps with the same input and output spaces.

The relative entropy $D(\rho\Vert\sigma)$ compares density operators $\rho$ and $\sigma$. The sandwiched Rényi divergence $\widetilde D_\alpha(\rho\Vert\sigma)$ is an order-dependent comparison, defined for $\alpha\ge\tfrac12$, $\alpha\ne1$. The state, channel, and regularized divergences are measured in bits. Operator-level analytic lemmas may use natural logarithms; the state wrappers divide by $\log 2$. Singular states are allowed; the support conventions retain infinite values rather than assigning a finite substitute. These are the state quantities in the paper's equations (1.2)–(1.3).

The stabilized channel divergence optimizes the state divergence over normalized pure inputs on $H\otimes R$, where $R$ is a copy of $H$. The channel acts on $H$ and the identity acts on $R$. Writing $\psi=|\psi\rangle\langle\psi|$, the convention is

$$\mathbb D(N\Vert M)=\sup_{\|\psi\|=1} \mathbb D\bigl((N\otimes\operatorname{id}_R)(\psi) \Vert(M\otimes\operatorname{id}_R)(\psi)\bigr),$$

where $\mathbb D$ denotes either state divergence. The paper places the reference first; the formalization places it second and proves the tensor-factor convention agrees. A block of $n$ uses employs $N^{\otimes n},M^{\otimes n}$ and a reference copy of $H^{\otimes n}$. Its pure input may be entangled across every use. Equation (1.4) specifies this stabilization.

Formalization targets

The regularized divergences are defined independently as positive-block suprema:

$$\widetilde D_\alpha^{\mathrm{reg}}(N\Vert M) =\sup_{n\ge1}\frac{\widetilde D_\alpha(N^{\otimes n}\Vert M^{\otimes n})}{n}, \qquad D^{\mathrm{reg}}(N\Vert M) =\sup_{n\ge1}\frac{D(N^{\otimes n}\Vert M^{\otimes n})}{n}.$$

Two supporting targets establish that these definitions are the actual asymptotic limits in equation (1.5). For every fixed $\alpha\ge\tfrac12$, $\alpha\ne1$,

$$\lim_{n\to\infty}\frac{\widetilde D_\alpha(N^{\otimes n}\Vert M^{\otimes n})}{n} =\widetilde D_\alpha^{\mathrm{reg}}(N\Vert M),$$

and

$$\lim_{n\to\infty}\frac{D(N^{\otimes n}\Vert M^{\otimes n})}{n} =D^{\mathrm{reg}}(N\Vert M).$$

The main goal is Theorem 1:

$$\lim_{\alpha\to1,\,\alpha\ne1} \widetilde D_\alpha^{\mathrm{reg}}(N\Vert M) =D^{\mathrm{reg}}(N\Vert M).$$

This is convergence from both sides. Each target includes infinite divergence. The block identities are supporting identifications, rather than extra premises of the main theorem.

Significance: continuity after optimization

The main result identifies a single limit after optimization over entangled inputs and unbounded block lengths. It permits near-one regularized Rényi quantities to approach regularized relative entropy for arbitrary channel pairs in the stated finite-dimensional setting. When the latter is infinite, the conclusion is convergence to positive infinity. The paper discusses applications to discrimination and asymptotic approximation; those operational conclusions are beyond this mission's targets. Wang–Yang, arXiv:2609.28635v1.

This is a contribution of a known, formally proved result, rather than an unsolved conjecture. The original public Lean development includes proofs of the definitions' supporting properties and both block identities. Its recorded verification reports Lean checking with a transitive axiom audit, Comparator statement comparison and Lean kernel replay, and independent Nanoda kernel checking. These records concern the original pinned development. They are unsigned and do not establish independent human review of correspondence to the paper. The converted contribution uses Lean 4.30.0 and Mathlib c5ea003. Its 95 Definition bundles and 27 theorem nodes have been published; every theorem has an ACCEPTED proof and public Proved status. Before upload, the exact statement and solution files compiled locally, their types and transparent definition values were compared with the frozen compatibility port, and a transitive axiom audit of every generated declaration found only propext, Classical.choice, and Quot.sound. These new checks are separate from the original Comparator and Nanoda records. Human review of correspondence to the paper is still required.

Difficulty: optimization and singular inputs

Pointwise continuity for a fixed pair of output states does not justify interchanging a limit with the supremum over all block inputs. That domain includes every positive block length, so finite-dimensionality of each block does not itself supply a uniform conclusion. The right-hand limit is particularly sensitive to the order of these operations. Singular inputs introduce a separate issue: support mismatch can force genuine infinity, and converting all expressions to ordinary real numbers would discard that case. The formalization must preserve these domains and conventions throughout, as documented in the paper-to-Lean mapping.

Formalization scope

The Lean representation uses actual positive density operators, CPTP maps, reference systems, and tensor powers. State divergences have extended-real values; channel and regularized divergences take values in $[0,+\infty]$. Nonnegativity is proved for the admissible orders, so conversion to nonnegative extended reals preserves those values. Supremum definitions quantify over positive block lengths. The normalized block sequences are total at $n=0$, which is irrelevant to convergence as $n\to\infty$.

The main formal statement uses a punctured neighborhood of one. A sufficiently small such neighborhood lies within $\alpha>\tfrac12$, so totalized definitions at other real orders impose no assertion about their divergence interpretation outside the admissible range. No support inclusion, finite max-relative entropy, filter estimate, or Schatten estimate is assumed by the main theorem. Defining the limiting value to equal the desired conclusion, or replacing arbitrary channels by an easy special family, would not meet these targets.

The development builds on Mathlib and Lean-Quantum. Reusable components include extended-valued Fekete convergence, channel tensor identities, quantum testing quantities, prescribed-dilation approximation, and finite-dimensional Schatten bounds. The scope mapping records that the supporting decomposition estimate is formalized for $1<\alpha\le2$, sufficient near one; it does not claim the paper's entire all-orders version. Contributions that improve reuse, verify the converted dependency graph, or extend separately stated results are welcome. The paper's later operational corollaries are excluded.

Selected references

• Jinzhao Wang and Yuxiang Yang, Continuity of Regularized Channel Rényi Divergences, arXiv preprint, 2026, version 1. Paper and versioned source.
• Jinzhao Wang, Continuity of regularized channel Rényi divergence: Lean formalization, public software repository, 2026; development assisted by Codex. Source commit e29274a, v1.1.0 verification release.
• Hayata–Yamasaki Group, Lean-Quantum, formalization library, pinned revision bf1c4f6, 2026. Dependency source.
• Lean community, Mathlib4, mathematical library for Lean 4, 2026. Converted contribution's selected revision c5ea003.

Motivation

An $n$-year term assurance pays a benefit if the insured person dies in one of the first $n$ policy years. It can pay only once. This matters when calculating the second moment: claims in different years cannot both occur, so the cross-products between them are zero.

Actuarial Mathematics I established finite expected present values, second moments and variances for general collections of contingent payments. This mission applies those results to one life and a fixed-term death benefit. It proves the familiar term-assurance formulas from reusable death-year events, rather than treating them as isolated actuarial notation.

Mathematical setting

Let $(\Omega,\mathcal F,P)$ be a probability space and let $K:\Omega\to\mathbb N$ be a measurable curtate future lifetime: the number of complete future years lived before death. For $k\in\mathbb N$, define the event of death during policy year $k+1$ by

$$D_k=\{\omega\in\Omega:K(\omega)=k\}.$$

Each event $D_k$ is measurable. The events are pairwise disjoint: if $i\ne j$, then $D_i\cap D_j=\varnothing$.

Fix a policy term $n\in\mathbb N$ and a constant annual discount factor $v$. A unit benefit is payable at time $k+1$ if death occurs during year $k+1$, for $0\leq k<n$. Its random present value is

$$Z_n(\omega)=\sum_{k=0}^{n-1}v^{k+1}\mathbf1_{D_k}(\omega).$$

When $n=0$, the sum is zero. The implementation uses the previously published `ActuarialValuation.presentValue` definition with the schedule of death-year events, reusing the general valuation machinery. The theorem statements allow any real $v$, so the finite algebra also holds beyond the economic setting $0<v\leq1$. The positive discount factors customary in the source are a special case.

Main theorem

The capstone proves these three identities together.

Expected present value:

$$\mathbb E_P[Z_n]=\sum_{k=0}^{n-1}v^{k+1}P(D_k).$$

Second moment:

$$\mathbb E_P[Z_n^2]=\sum_{k=0}^{n-1}v^{2(k+1)}P(D_k).$$

Variance:

$$\operatorname{Var}_P(Z_n)= \sum_{k=0}^{n-1}v^{2(k+1)}P(D_k) -\left(\sum_{k=0}^{n-1}v^{k+1}P(D_k)\right)^2.$$

The second-moment simplification comes from the mutual exclusivity of distinct death-year events, not from independence. In the general double sum from Actuarial Mathematics I, every off-diagonal intersection of death-year events is empty, leaving a single sum.

Formalisation milestones

The milestones proceed from measurability of each death-year event to disjointness across years, vanishing products of distinct death-year indicators, the finite present-value representation, the expected value, the second moment and the variance. The proposal gives each mathematical statement and Lean target type separately. The capstone combines the three moment identities for the same $K$, $v$, $n$ and $P$.

The project uses the existing `ActuarialValuation` namespace and imports published Mission I results where they apply. All dates are annual, and benefits are payable at the end of the year of death. Multiple lives, benefits payable immediately on death, stochastic discounts, select-life models and whole-of-life infinite sums are outside the scope of this capstone.

Why these results matter

A complete proof provides a reusable one-life mortality event model and a verified finite-term insurance valuation formula. The model can support a later mission on pure endowments and endowment assurances, where survival-to-term events complement death-in-term events, and another on temporary annuities, where survival events are nested rather than disjoint.

The results also make it straightforward to compare the traditional actuarial single-sum variance formula with the general dependent-cashflow theorem proved in Mission I.

Source and scope

The main mathematical source is Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 2 §2.4.3 for curtate future lifetime, Chapter 3 §3.1.1 equation (3.4) for disjoint-event moments, and §3.2.2 equation (3.8) for term-assurance present value, mean and variance.

• https://openacttextdev.github.io/LifeCon/C-ModelingLifeTimes.html
• https://openacttextdev.github.io/LifeCon/C-SimpleBenefit.html
• https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf (CM1 2026, life-contingency valuation objectives)
• Actuarial Mathematics I: Present Values of Contingent Cashflows

These established actuarial formulas are not new mathematical conjectures. The contribution is a precise formal link in Lean from a curtate-lifetime model to the general contingent-payment valuation layer.

Formalisation challenges

The death-year set must be shown measurable from the measurability of $K$. The disjointness arguments must also cover degenerate cases such as $n=0$. The generic second-moment theorem uses an ordered double sum. The proof must remove only terms justified by $D_i\cap D_j=\varnothing$, retain the diagonal terms and use the correct end-of-year exponent $k+1$.

All formal declarations are written for Prove2Me's pinned Mathlib revision `0df444a360eaa60ab8c11dca51a86af692955474`. No local Lean compiler is used. Any private preflight compilation, if needed, is performed through Prove2Me's remote system.

Motivation

Life insurers and pension schemes promise cashflows whose payment depends on future events. A term assurance pays if the insured dies within a stated period. A pension pays when a member survives to an instalment date. A contingent survivor pension may continue after the member dies. These liabilities differ in the events triggering payment, but share one mathematical operation: discount the amounts payable and aggregate them to obtain a random present value. Expected present value is used in premium setting and liability valuation, while the second moment and variance quantify how much the discounted liability can vary.

The open textbook Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, §3.1, introduces uncertain discounted cashflows using indicators, and derives their expected values in equation (3.3). Its treatment also distinguishes independent indicators from indicators connected through death or survival. This mission establishes a finite-horizon generalisation of those identities that handles arbitrary dependencies among payment-triggering events.

Setting

Fix a measurable sample space $(\Omega,\mathcal F)$ with a probability measure $P$. A finite set $I$ indexes distinct payment obligations. Each obligation $i\in I$ has a non-negative integer payment date $t_i\in\mathbb N$, a deterministic cashflow amount $c_i\in\mathbb R$, and a measurable event $A_i\in\mathcal F$ that triggers payment. The deterministic discount function $d:\mathbb N\to\mathbb R$ assigns a multiplier to each date. Write $\mathbf 1_{A_i}(\omega)$ for the real-valued event indicator, equal to one on $A_i$ and zero otherwise.

The random present value is

$$Z(\omega)=\sum_{i\in I}d(t_i)c_i\mathbf 1_{A_i}(\omega).$$

The same date can support multiple obligations with distinct contingencies, such as member and survivor payments, pension tranches and expenses. The index distinguishes obligations even when their payment times coincide. Amounts may be positive, zero or negative and triggering events can be mutually exclusive, nested, independent or arbitrarily dependent. Finite schedules also allow no obligations. Each present value is bounded and has finite first and second moments because the schedule is finite, amounts are deterministic real numbers, and indicators are bounded.

Formalisation targets

The capstone theorem proves the expected present value, second moment and variance identities for the same random variable $Z$. The expected present value is

$$\mathbb E_P[Z]=\sum_{i\in I}d(t_i)c_iP(A_i).$$

The second moment retains all dependence terms, including pairs of different obligations payable on the same date:

$$\mathbb E_P[Z^2]=\sum_{i\in I}\sum_{j\in I} d(t_i)c_i\,d(t_j)c_j\,P(A_i\cap A_j).$$

Consequently,

$$\operatorname{Var}_P(Z)=\sum_{i\in I}\sum_{j\in I} d(t_i)c_i\,d(t_j)c_j\, \left(P(A_i\cap A_j)-P(A_i)P(A_j)\right).$$

The finite identity for expected present value specialises the textbook's equation (3.3). The general joint-event second-moment identity extends its §3.1.1 discussion to arbitrary dependence. The goal combines all three formulas in a single result, with supporting milestone theorems for integrability, square-integrability, one-event expectation, the finite-schedule expectation formula, pairwise event interactions, the second moment and the variance.

Significance

A single reusable statement should allow a future mission to specify the trigger events and payment schedule of a policy and immediately obtain its discounted mean and variance. A life assurance can use disjoint death-year events, and an annuity can use nested survival-to-payment events. A guaranteed pension, deferred benefit, survivor pension or multiple-decrement model can use more general indicators. Later missions can also specialise the variance expression when events are known to be independent or mutually exclusive.

Examples of why the dependence assumptions matter. Write $w_i=d(t_i)c_i$ for each discounted obligation amount:

• Mutually exclusive death-year benefits: If $A_i\cap A_j=\varnothing$ for every distinct pair $i\ne j$, the general second moment simplifies to $\mathbb E_P[Z^2]=\sum_{i\in I}w_i^2P(A_i)$. This is the event structure behind term-assurance death-year payments.
• Nested survival payments: For an annuity whose $A_i$ denotes survival to time $t_i$, whenever $t_i\leq t_j$ we have $A_j\subseteq A_i$, and hence $P(A_i\cap A_j)=P(A_j)$. The later-survival probability therefore appears in the cross-term.
• Different benefits at the same date: Two obligations indexed $1$ and $2$ may both have payment time $5$, while depending on different events. Their second moment includes the cross-term $2w_1w_2P(A_1\cap A_2)$, even though $t_1=t_2$.

These specialisations use the same capstone rather than different definitions of actuarial present value.

The mathematical identities are established results of elementary probability and financial mathematics. The formalisation contribution is a stable actuarial cashflow interface connecting the relevant Lean measure-theoretic and probability results. It does not assert that the classical equations are newly discovered, or that general insurance reserving, stochastic interest rates or continuous-time survival models have already been formalised.

Difficulty

The event indicator is a bounded random variable, but its mathematical expectation is represented in Lean by integration against a measure. The development must reconcile the real-valued integrals with event probabilities represented as extended non-negative reals. Moreover, expanding the square of a finite random cashflow sum requires pairwise intersections without adding an independence assumption. The usual simplification that removes cross-terms is invalid for nested survival events or arbitrary dependent payment events.

The target also uses the real-valued variance from Mathlib. Its general API permits variables outside $L^2$, so a faithful proof must establish square-integrability for the finite event-based present value rather than use any default value for an undefined or infinite variance.

Formalisation scope

The initial development is discrete-time and finite-horizon, with distinct payment obligations indexed by a finite set. Each obligation has a nonnegative integer payment time. Different obligations may have the same payment time. Discount multipliers and payments are deterministic real values; no positivity assumption is needed for the algebraic identities. Each trigger is a measurable event and the underlying measure is a probability measure. Empty index sets and zero or negative payments are included. The joint-event formula remains valid when the same outcome triggers more than one payment.

Use Mathlib's existing MeasureTheory.Measure, MeasurableSet, integration and ProbabilityTheory.variance rather than redefining them. A lightweight namespace ActuarialValuation should define the random present value and retain clear time and cashflow parameter names. Supporting results should be small and import only genuine mathematical dependencies. The formalisation uses a generic obligation index type and a payment-time function into the natural numbers. The event family and amounts are indexed by obligations rather than by time.

There is no finite-to-infinite inference in the target; infinite sums require separate convergence results. There are no mortality rates, hazard functions, Markov transition kernels or stochastic discount factors in this mission. Those are targets for later missions, building on the valuation layer.

Selected references

• Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, §3.1, equations (3.1)–(3.3) and §3.1.1, https://openacttextdev.github.io/LifeCon/C-SimpleBenefit.html.
• Lean community, Mathlib 4: ProbabilityTheory.variance, https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Moments/Variance.html.
• Prove2Me, Captain tour, https://prove2.me/tour/mission-captain.

Prove Lieb’s concavity theorem (Theorem 8.1.1, also stated as Theorem 3.4.1): for fixed Hermitian H, the function A ↦ tr exp(H + log A) is concave on positive-definite matrices. This is the deterministic foundation of Chapter 3’s probabilistic argument.

Milestones follow the book’s route through generalized Klein, relative-entropy nonnegativity, variational trace formulas, operator Jensen, matrix perspectives, and joint convexity of relative entropy. Logarithm and trace-exponential monotonicity are included as reusable comparisons. The domain allows noncommuting positive-definite matrices without trace normalization.

Source: Tropp, January 2015 version, Chapter 8. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Control the spectral norm of a matrix series with independent standard Gaussian or Rademacher coefficients. The goal is Theorem 4.1.1, including its variance identity, expected-norm estimate, and tail bound for rectangular complex matrices.

Milestones are the Gaussian and Rademacher matrix mgf/cgf estimates (Lemmas 4.6.2–3) and the Hermitian series bound (Theorem 4.6.1). The formulation keeps the source’s constants, both coefficient laws, and the zero-variance case. The shared Chapter 3 tools connect these transform estimates to concentration.

Source: Tropp, January 2015 version, Chapter 4. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Replace ambient matrix dimension by intrinsic dimension, the ratio of trace to spectral norm. The goal is intrinsic Matrix Bernstein (Theorem 7.3.1). Intrinsic Matrix Chernoff (Theorem 7.2.1) is a second major target within the mission.

Supporting milestones include the generalized Laplace bound, intrinsic-dimension trace estimate, block-diagonal identities, Hermitian Bernstein, and the expected-norm corollary. The statements retain the source’s constants, threshold restrictions, and matrix-valued mean or variance bounds. Nonzero proxies keep intrinsic dimension well-defined; the expectation constant is universal.

Source: Tropp, January 2015 version, Chapter 7. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Control the spectral norm of a sum of independent, centered, bounded rectangular random matrices. The goal is Matrix Bernstein (Theorem 6.1.1), including the variance identity and both expected-norm and tail estimates.

Milestones cover Hermitian dilation, variance additivity, the bounded-summand mgf/cgf estimate (Lemma 6.6.2), and Hermitian Bernstein (Theorem 6.6.1). Chapter 3 supplies the general Laplace-transform machinery. The formulation uses the Euclidean operator norm, preserves the one-sided eigenvalue assumption in the Hermitian result, and includes deterministic zero sums.

Source: Tropp, January 2015 version, Chapter 6. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Bound the extreme eigenvalues of a sum of independent positive-semidefinite random matrices. The goal is the complete Matrix Chernoff theorem (Theorem 5.1.1): both expectation estimates, both tails, and the identities for the mean’s extreme eigenvalues.

The supporting milestone is the matrix mgf/cgf estimate (Lemma 5.4.1); Chapter 3 supplies the master bounds. The Lean statement retains the different lower- and upper-tail deviation ranges, permits zero mean eigenvalues, and handles a zero summand bound explicitly.

Source: Tropp, January 2015 version, Chapter 5. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Develop the reusable matrix Laplace-transform method behind Tropp’s concentration inequalities. The goal is Theorem 3.6.1: upper and lower tail and expectation bounds for sums of independent Hermitian random matrices, expressed through their matrix cumulant-generating functions.

Milestones cover the eigenvalue tail and expectation bounds (Propositions 3.2.1–2), probabilistic Lieb inequality (Corollary 3.4.2), and trace-cgf subadditivity (Lemma 3.5.1). This mission also supplies the series’ shared spectral, probability, and dilation definitions. Lieb’s underlying concavity theorem is the Chapter 8 goal.

The Lean statements give bounds for each admissible transform parameter, with explicit integrability hypotheses; optimization recovers the source’s infimum/supremum forms.

Source: Tropp, January 2015 version, Chapter 3. Lean statements compile; proofs remain open.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Symmetries of real plane curves

How many Euclidean symmetries can a real plane algebraic curve of degree $d$ have? Rotational symmetry of a curve is classically detected from the monomials $z^a\bar z^{\,b}$ of its equation in the complex coordinate $z=x+iy$: a rotation of order $N$ about the origin can preserve the curve only if the differences $a-b$ of the nonzero monomials satisfy a congruence modulo $N$ (Lebmeir and Richter-Gebert, Section 4; Lebmeir, Theorem 5.4). Bounds on the number of symmetries in terms of the degree enter symmetry detection algorithms (Alcázar, Lávička and Vršek) and incidence geometry: Pach and de Zeeuw, Lemma 2.6 use a bound of $4d$ on the number of isometries of a curve in a distinct-distances argument.

The note Sharp symmetry bounds for real algebraic curves (C. Perassi, 2026; PDF) determines the sharp bounds, classifies the curves attaining the rotation bound in degree $d\ge5$, and describes their Möbius geometry. This mission is the complete Lean formalization of that note.

Setting

Let $f\in\mathbb R[x,y]$ be irreducible in $\mathbb C[x,y]$, of total degree $d\ge2$, and let $C=\{(x,y)\in\mathbb R^2 : f(x,y)=0\}$, identified with a subset of $\mathbb C$ through $z=x+iy$. Assume that $C$ is infinite and is not a circle. Write $\operatorname{Sym}(C)$ for the group of Euclidean isometries $T$ of $\mathbb C$ with $T(C)=C$, and $\operatorname{Sym}^+(C)$ for its orientation-preserving subgroup (the rotations and translations preserving $C$).

For an integer $m\ge1$ and a nonreal $\alpha\in\mathbb C$ with $|\alpha|=1$, the extremal family is

$$C_{m,\alpha}=\{z\in\mathbb C : \operatorname{Re}\bigl(z^m(|z|^2+\alpha)\bigr)=0\},$$

a curve of degree $m+2$. Its closure $\widehat C_{m,\alpha}$ in the Riemann sphere $\widehat{\mathbb C}=\mathbb C\cup\{\infty\}$ is acted on by Möbius maps $z\mapsto (az+b)/(cz+d)$ and by anti-Möbius maps, a Möbius map composed with complex conjugation. In the coordinates $X=z$, $Y=\bar z$ the family has the equation $P_\alpha=X^m(\alpha+XY)+Y^m(\bar\alpha+XY)$, whose zero set $V_\alpha\subset\mathbb P^1\times\mathbb P^1$ has bidegree $(m+1,m+1)$.

Formalization targets

Goal: the bounds (Theorem 1)

$$\operatorname{Sym}(C)\ \text{and}\ \operatorname{Sym}^+(C)\ \text{are finite},\qquad |\operatorname{Sym}^+(C)|\le\max\{d,\,2d-4\},\qquad |\operatorname{Sym}(C)|\le 2d .$$

The goal asserts the bounds only; their sharpness and the equality case are milestones.

Milestones

1. Theorem 1, sharpness and equality. Both bounds are attained in every degree $d\ge2$. If $d\ge5$ and $|\operatorname{Sym}^+(C)|=2d-4$, an orientation-preserving similarity carries $C$ onto $C_{d-2,\alpha}$; conversely every $C_{m,\alpha}$ with $m\ge3$ has $2m$ rotations.
2. Equation (2). The quintic $\operatorname{Re}\bigl(z^3(|z|^2+i)\bigr)=0$ satisfies $f(e^{\pi i/3}z)=-f(z)$ and has exactly six rotations: a symmetry of a zero set need not fix its defining polynomial.
3. Lemma 3. Every $T\in\operatorname{Sym}(C)$ satisfies $f\circ T=\pm f$, with sign $+1$ for reflections.
4. Theorem 2. $C_{m,\alpha}$ ($m\ge2$) is infinite, geometrically irreducible, of degree $m+2$; the full ambient Möbius symmetry group of $\widehat C_{m,\alpha}$ is $\{z\mapsto cz : c^{2m}=1\}\cup\{z\mapsto c/z : c^{2m}=\bar\alpha^{\,2}\}$, dihedral of order $4m$, with no anti-Möbius symmetry; the Euclidean symmetries are the $2m$ rotations; and for fixed $m$, $\widehat C_{m,\alpha}$ and $\widehat C_{m,\beta}$ are Möbius equivalent if and only if $\beta=\alpha$, anti-Möbius equivalent if and only if $\beta=\bar\alpha$.
5. Lemma 4. $P_\alpha$ is irreducible (and so is $V_\alpha$), the only singular points of $V_\alpha$ are $(0,0)$ and $(\infty,\infty)$, both ordinary $m$-fold points, and its function field has genus $m$.
6. Remark 5. In degree four, $\operatorname{Re}(z^4)=1$ attains the rotation bound but is not similar to any $C_{2,\alpha}$: its function field has genus three, those of the family genus two. The parameters $e^{i\theta}$, $0<\theta<\pi$, give pairwise inequivalent curves, and for algebraic $\alpha$ all the maps in Theorem 2 have algebraic coefficients.

Significance

The result. The bounds $\max\{d,2d-4\}$ and $2d$ are attained in every degree, so they cannot be improved as functions of $d$ alone; for $d\ge5$ the curves attaining the rotation bound form one explicit family up to similarity, with a complete invariant. The bound $2d$ sharpens the auxiliary $4d$ estimate used by Pach and de Zeeuw (no improvement of their distance exponent is claimed), and the quintic of equation (2) contradicts the degree restriction stated in Lemma 9 of the arXiv version of Alcázar, Lávička and Vršek (the journal version has not been checked).

The formalization. Every statement of the note is proved in Lean 4 with Mathlib: 208 theorems and 12 definition files here, all proved, using only the axioms propext, Classical.choice and Quot.sound. It contains material that Mathlib does not have yet and that is reusable on its own: the genus of a function field over $\mathbb C$ defined through its places and holomorphic differentials, and its invariance under isomorphism; the places of quadratic covers $w^2=h(t)$ and Kummer covers $y^n=f(x)$, with uniformizers and local Kähler differentials; the classification of places of a Dedekind domain; the four-chart atlas of $\mathbb P^1\times\mathbb P^1$ with its Zariski topology; and Möbius and anti-Möbius maps acting on the Riemann sphere. Theorem 1 is also registered with the Palomar registry as PALOMAR-2026-09-18-000007. The Lean code was written by AI agents under the author's direction; the Lean kernel checks it. The results have not been reviewed by an independent human, and neither the kernel checks nor the registration certify novelty.

Difficulty

The first argument is Bézout: the images of a point of $C$ under the rotations about a common center are distinct points on one circle, so there are at most $2d$ of them. This gives $2d$ for $\operatorname{Sym}^+(C)$, not $\max\{d,2d-4\}$, and it says nothing about which curves are extremal. A second obstacle is that a symmetry of the zero set need only fix the polynomial up to sign, as equation (2) shows, so invariant-theoretic arguments that assume $f\circ T=f$ do not apply directly. For the Möbius statements the difficulty is that a Möbius map of the sphere does not act on the real equation; the curve must be compactified and its singular points identified. In the formalization, the genus comparison of Remark 5 needs a genus that does not depend on a chosen model, which Mathlib does not provide.

Formalization scope

• Curves are given by real polynomials in two variables (MvPolynomial (Fin 2) ℝ), and the curve is their real zero set as a subset of $\mathbb C$. Geometric irreducibility means irreducibility over $\mathbb C$.
• Symmetry groups are the actual groups of isometries ℂ ≃ᵢ ℂ preserving that subset. Group orders use Nat.card, which is $0$ for an infinite set, so finiteness is part of the statements.
• Several family statements need less than the note: $\alpha\notin\mathbb R$ without $|\alpha|=1$, or $m\ge1$; the statements say so.
• The Riemann sphere is OnePoint ℂ with the action of $\mathrm{GL}_2(\mathbb C)$.
• $V_\alpha$ is the bihomogeneous zero locus in $\mathbb P^1\times\mathbb P^1$, with the topology making the four standard affine Zariski charts open embeddings. These are classical complex points, not schemes.
• The genus is the dimension of the space of differentials of the function field that are regular at every place, a place being a proper valuation subring containing $\mathbb C$. A branch point is a point of the $t$-line with fewer than two places above it. Ramification indices and a divisor-level Riemann–Hurwitz formula are not formalized; the genus of Lemma 4 comes from an explicit basis of differentials.
• The hypotheses rule out trivial versions: the curve is infinite, irreducible over $\mathbb C$ and not a circle, and the groups are those of the zero set, not of the polynomial.
• Welcome contributions: moving the reusable parts into Mathlib, a divisor-level Riemann–Hurwitz statement, and a scheme-theoretic normalization of $V_\alpha$.

Selected references

• C. Perassi, Sharp symmetry bounds for real algebraic curves, note, 2026. PDF; Lean formalization: github.com/carlok/curve-symmetry-lean.
• P. Lebmeir and J. Richter-Gebert, Rotations, translations and symmetry detection for complexified curves, Computer Aided Geometric Design 25 (2008), 707–719. doi:10.1016/j.cagd.2008.09.004
• P. M. Lebmeir, Feature Detection for Real Plane Algebraic Curves, doctoral thesis, TU München, 2009. PDF
• J. Pach and F. de Zeeuw, Distinct distances on algebraic curves in the plane, 2014. arXiv:1308.0177v3
• J. G. Alcázar, M. Lávička and J. Vršek, Symmetries and similarities of planar algebraic curves using harmonic polynomials, 2018. arXiv:1801.09962v1; Journal of Computational and Applied Mathematics 357 (2019), 302–318, doi:10.1016/j.cam.2019.02.036.
• L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language, CADE 28, LNCS 12699, Springer, 2021, 625–635. doi:10.1007/978-3-030-79876-5_37
• The mathlib Community, The Lean mathematical library, CPP 2020, 367–381. doi:10.1145/3372885.3373824