Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Library primary source: S. David Promislow, Fundamentals of Actuarial Mathematics (third edition, 2015), Chapter 21, sections 21.8.1–21.9, PDF pages 411–413, particularly formula (21.9), Poisson thinning discussion on page 412 and claim-type joint mass factorisation and superposition on page 413. Further open teaching source: SCMA469 Actuarial Statistics, Chapter 5.6, Poisson process superposition and thinning, https://pairote-sat.github.io/SCMA469/poisson-processes.html. These sources distinguish single-stream thinning, independence of split streams and combination of already independent processes. The new Lean targets give explicit finite count-probability identities rather than claiming a general measure-theoretic process theorem.
For a Poisson claim frequency , define the mass at integer claim count by
A frequency class selected with probability , independently for every original claim, receives intensity ; the other class receives intensity . Their intensities must sum to . A total of claims has count probability . Given that count, exactly marked claims and unmarked claims occur with conditional binomial probability . Thus the joint count mass is
The splitting identity is the exact factorisation
This product shows independence of the two count variables, rather than deriving independence merely from matching their marginal Poisson distributions. Cases , , and count zero are included.
For independent Poisson claim-frequency streams with rates , superposition gives
The identity uses a finite convolution coefficient for each total claim count. The total-rate parameter is additive. Algebraic theorems can allow signed real parameters, while the actuarial probability interpretation requires nonnegative rates and valid marking probabilities.
Five definitions introduce Poisson count mass, count convolution, selected intensity, split count joint mass and superposed intensity. Twelve supporting theorems include the factorial count recursion, zero-count probabilities, rate partition, nonnegativity, convolution at zero, the binomial superposition identity, marked mass factorisation and zero-rate boundary. The thirteenth theorem combines exact superposition and splitting.
The substantial algebraic steps use the factorial ratio , the binomial theorem and , with all denominators equal to positive natural factorials. Count variables are nonnegative integers and finite coefficient identities do not themselves assert a construction of continuous-time Poisson processes. That stronger stochastic process claim is outside this mission.
An independent 80-digit decimal evaluation verified 1,968 count-convolution and split-joint identities, including , , , mixed rates and both zero and positive counts.
This Draft is formally self-contained. It does not import the unpublished aggregate-claims theorems from XXVII and never claims that a proof is accepted simply because an open Lean proposition elaborates in a private authoring check.
Harry H. Panjer (1980), The Aggregate Claims Distribution and Stop-Loss Reinsurance, Transactions of the Society of Actuaries 32, 523–535, examines aggregate distributions and stop-loss reinsurance. Panjer and Willmot (1982), Recursions for Compound Distributions, ASTIN Bulletin, connects efficient compound-claim recursion to net stop-loss premium calculations. Gordon E. Willmot, Steve Drekic and Jun Cai (2005), Equilibrium compound distributions and stop-loss moments, Scandinavian Actuarial Journal, DOI https://doi.org/10.1080/03461230510009691, studies tail/integrated-tail representations relevant to stop-loss valuation.
The mission gives a deliberately finite, integer-lattice and exact version of stop-loss valuation. It works on probability mass coefficients for integer aggregate losses . Some algebraic identities are true even for unnormalised real coefficients; this distinction is retained in the formal theorem types rather than assuming a distribution without stating it.
The attachment is the insurer's retained limit, with reinsurer payment at the claim settlement date of
A claim exactly equal to d pays zero excess. The expected net stop-loss premium does not contain expense or variance loading:
The insurer's retained limited expected loss is
The pointwise cashflow partition gives the actuarial bridge . It is valid for any real mass coefficients by linearity of the finite sum.
Let the strict loss tail be
when the coefficients form a normalised probability law. Raising the attachment from d to d+1 changes the payout by one unit on exactly the event . Consequently
for , and the last difference is zero outside the grid.
Because at , the adjacent recurrence telescopes into the finite discrete tail-sum identity
With nonnegative probability coefficients, tails are nonnegative and decrease with attachment. It follows that is nonnegative, nonincreasing and discretely convex:
The term at attachment B in the tail sum is zero. Deductibles above B also produce zero premium. The zero-attachment premium equals the full gross expected aggregate claim .
Five local definitions cover the nonnegative excess payment, bounded expected excess premium, strict aggregate tail, retained limited mean and gross aggregate expected claim. Fourteen supporting milestone theorems establish individual claim boundaries, payment partition, zero/full attachments, nonnegativity, one-step premium and tail differences, monotonicity, discrete convexity, the limited-mean bridge and exact tail-sum valuation.
The capstone combines in one target theorem:
An independent exact-rational verification checked 72 bounded grid/attachment cases, including deductibles above the maximum loss and unnormalised nonnegative coefficient arrays. The cashflow, increment, tail-sum and convexity identities all passed.
The bounded-grid model can be populated by Actuarial XXVI's finite individual-risk aggregate PMF. Actuarial XXVII's compound Poisson model is generally unbounded, so its full stop-loss premium requires infinite-sum convergence and cannot be treated as if it shared this finite maximum B. Such a limit and numerical truncation-error guarantee would be a separate mission.
The formal source is self-contained until earlier definitions are actually published, and never imports a theorem merely because a prior mission was drafted. All supporting and capstone theorems are open Lean proof obligations.
R. J. Verrall (1989), The individual risk model: a compound distribution, Journal of the Institute of Actuaries, volume 116(1), pages 101–107, DOI https://doi.org/10.1017/S0020268100036465, develops the connection between individual and collective aggregate-risk modelling. Nelson De Pril (1989), The Aggregate Claims Distribution in the Individual Model with Arbitrary Positive Claims, ASTIN Bulletin, volume 19(1), pages 9–24, DOI https://doi.org/10.2143/AST.19.1.2014913, develops exact aggregate-distribution recursion for the individual-risk model.
The present mission is a finite, integer-lattice, independent Bernoulli-policy formalisation. It derives probability-mass support, nonnegativity and normalisation from convolution, rather than claiming that either author already supplied these exact Lean theorem types.
Policy pays a fixed nonnegative integer benefit with probability , where . It pays nothing otherwise. The Bernoulli policy's payment distribution, as opposed to its event distribution, is
A zero-benefit policy has both events paying zero. Therefore its single payment coefficient at is , not . This corner case is explicitly retained, rather than assuming every is strictly positive.
The total loss over n independent policies is , with independent Bernoulli indicators . Its maximum possible loss is .
For coefficient arrays , define their discrete convolution by
With no policies the payment mass is . Each additional policy is introduced by
A bound-aware mass operator is . If the first distribution vanishes above B and the second above C, convolution satisfies , even for unnormalised intermediate coefficient arrays.
The companion algebraic lemmas establish convolution identity, commutativity and associativity. A distributional lemma establishes that nonnegative component masses imply nonnegative convolution coefficients.
Under for every included policy, the portfolio aggregate is a valid bounded probability mass function:
These are three distinct requirements: nonnegativity, normalisation on the exact finite benefit bound and zero support above that bound. All must be proved, including empty portfolios and policies whose benefit is zero. Independence is encoded by the convolution construction, not inferred from unrelated marginal Bernoulli probabilities.
Five new definitions introduce convolution, one-policy Bernoulli mass, bounded total mass, maximum possible claim and recursive portfolio probability mass. Fourteen supporting milestones prove convolution identities and support/mass preservation, the policy recursion, and bounded portfolio mass and nonnegativity; the fifteenth theorem is the capstone.
An independent exact-rational benchmark enumerated all binary claim/no-claim events across 1,365 distinct heterogeneous policy configurations, with zero and repeated benefits and probabilities at 0, 1/4, 1/2 and 1. Direct event enumeration agreed exactly with recursive convolution, giving nonnegative coefficients and unit total mass.
The source uses natural-valued grid claims, not continuous severities, and finite portfolios only. It does not assume any unpublished other mission's definitions exist in the Lean environment. Imported Lean definitions are local within this mission, with all imports before namespaces. Every theorem remains an open proof obligation until proved on the authoritative Prove2Me remote compiler.
Harry H. Panjer (1981), Recursive Evaluation of a Family of Compound Distributions, ASTIN Bulletin 12(1), 22–26, DOI https://doi.org/10.1017/S0515036100006796, proves a recursion for aggregate-claim distributions with suitable claim-frequency laws. The original paper treats a wider class than Poisson claim counts. Sundt and Jewell (1981), Further Results on Recursive Evaluation of Compound Distributions, ASTIN Bulletin 12(1), 27–39, DOI https://doi.org/10.1017/S0515036100006802, develops its extensions.
This mission formalises the positive-integer-severity compound Poisson case. The restriction on zero-sized claims is essential to the exact finite-count mixture used by the Lean definitions. It does not claim that a finite truncated Poisson mixture is automatically a probability distribution if zero severity has positive mass.
Let with . Its count probabilities are
Each claim has a positive integer severity with mass . The key support condition is . The usual stochastic interpretation additionally requires and total severity mass one, although the algebraic Panjer theorem itself works for arbitrary real satisfying .
For exactly m independent claims, is the m-fold discrete convolution, with and . Each positive claim contributes at least one unit, hence
It follows that the compound Poisson coefficient at aggregate loss s can be written as an exact finite sum, despite the count distribution being unbounded:
At , the distribution is . When , the zero-loss aggregate mass equals .
Panjer's recursion for this model is
It can be derived by combining the Poisson count ratio with the convolution-power coefficients. The zero-severity term has a factor j=0 and vanishes. Consequently the right-hand side at s depends only on the earlier aggregate coefficients . A separate theorem asserts that the initial mass and this recurrence uniquely determine the aggregate mass sequence.
The main Lean theorem is a conjunction of the no-claim initial value, the one-step recursion for every , and uniqueness for any real sequence satisfying those identities. It is an exact theorem about coefficients, not a numerical approximation or an unsupported claim of convergence of a severity generating function.
Five local definitions represent severity convolution, m-claim convolution powers, Poisson frequency mass, the aggregate mixture and the Panjer coefficient update. Thirteen supporting theorems include power recursion, support, count ratio, zero rate, nonnegative coefficients, the Panjer identity and uniqueness. The fourteenth is the capstone.
The independent high-precision benchmark compared two implementations: (i) direct Poisson-weighted convolution powers and (ii) the Panjer recurrence. They agreed to better than across 264 rate, severity and aggregate-size combinations using 70-digit decimal arithmetic, including zero frequency, fixed unit severity, two-point severity and a three-point severity with a gap.
The positive integer severity condition cannot simply be dropped: when zero-valued claims occur, can still contribute to aggregate loss s, and the true Poisson initial value becomes . That more general form, and arbitrary Panjer (a,b,0) counting laws, are explicitly out of scope.
No unpublished definitions are imported from Actuarial XXVI. The problem is mathematically linked but formally self-contained while XXVI is still a Draft. The theorem targets remain unproved until valid Lean submissions are accepted by Prove2Me.
Marek Kaluszka (2001), Optimal reinsurance under mean-variance premium principles, Insurance: Mathematics and Economics 28(1), 61–67, https://doi.org/10.1016/S0167-6687(00)00066-4, examines optimal retention when the reinsurance premium depends on claim mean and variance. Manuel Guerra and Maria de Lourdes Centeno (2010), Optimal Reinsurance for Variance Related Premium Calculation Principles, ASTIN Bulletin 40(1), 97–121, https://doi.org/10.2143/AST.40.1.2049220, studies the effect of variance-based loading on reinsurance decisions.
This mission isolates a clean Bernoulli claim and continuous quota-share specialisation, with a closed-form optimum and a finite-menu alternative. It does not assert the general optimal-retention functional results or the VaR/CVaR optimisations in the cited papers.
Let , where is a Bernoulli indicator with . Its claim amount is and the claim probability satisfies . A quota share is the insurer's retained proportion of each realised claim:
The reinsurer receives a fixed premium at policy inception that is an expected-value premium plus a loading on ceded variance. Using parameters and , where each variance coefficient has reciprocal currency units, define
The insurer's objective adds expected retained claims, the reinsurance premium and a variance-based risk-capital charge on retained loss:
For any real , the relevant expectation and variance formulas yield
The premium is deterministic once the contract and model are fixed, so it does not contribute additional random loss variance. A quota-share arrangement may change both the expected ceded premium and the variance of retained claims; both effects are included.
Assume in addition to nonnegative coefficients. Completing the square gives
It follows that the optimal insurer retention, not the ceded proportion, is
The solution can be at a boundary. If the insurer fully cedes the claim, . If , it retains everything, . If both coefficients vanish, all retentions have the same objective and the displayed ratio is undefined: this case is explicitly excluded. With , nonzero claim amount and positive total coefficient, is unique. For zero variance, for example or , every retention has the same variance component, so uniqueness does not follow and is not asserted.
A real insurer may instead face a finite menu of quoted retentions . Since is nonempty and finite, a cost-minimising member always exists, but there is no promise that .
The five definitions represent retained claim, ceded claim, variance premium, insurer capital objective and closed-form continuous retention. Twelve intermediate theorem obligations establish cashflow conservation, claim nonnegativity, full retention and full cession boundaries, objective expansion, admissibility of the candidate, quadratic square completion, global optimality, strict uniqueness when appropriate and finite-menu attainment. The capstone combines with for every real alternative.
The proof uses elementary real algebra and finite-set minimum selection. It requires neither local stochastic simulation nor a limit-of-policy-years theorem. The Bernoulli setup is deliberate, making the mean/variance premium principle analytically exact and testable before attempting general loss distributions.
Annual claim occurrence is a single Bernoulli event. Multiple correlated claims, expense loadings, default, credit risk, taxes, multi-period dynamic adjustment and Solvency II regulatory capital are not modelled. The capital coefficient is a chosen deterministic variance penalty rather than a regulatory capital formula. An optimal in this model should not be confused with an optimal excess-of-loss attachment point or with the entropic risk-sensitive optimum in Missions XXI–XXII.
All displayed theorem targets are unproved obligations until the authoritative Prove2Me compiler accepts a valid Lean proof. The owner Draft is for captain confirmation and moderator review, not an accepted theorem library.
Shiu and Xiong (2021), An elementary derivation of Hattendorff's theorem, European Actuarial Journal 11, 319–323, https://doi.org/10.1007/s13385-020-00256-9, derives the fully discrete mortality variance formula using reserve differences and summation by parts. The present mission develops the multiple-decrement extension on a countable lifetime space, keeping the covariance of different termination causes in the same policy year. This is a new derived formalisation rather than a claim that Shiu and Xiong printed these exact competing-risk theorems.
The earlier Actuarial XIV mission considers multiple-decrement valuation and premium recursion, while XVI investigates yearly mortality innovation orthogonality. Neither automatically supplies the countable competing-cause variance theorem, particularly when the net amount at risk is different for each decrement cause.
The termination year is a natural number . Its cause belongs to a finite type . For every policy year and cause , write . Causes are mutually exclusive: exactly one cause is realised on termination.
Require , and a strictly positive in-force mass at every policy year:
The cause probabilities do not have to be equal. Their sum is at most one because survival through the year remains possible. The realised cause has no independent probability after termination: this is one joint time-and-cause categorical distribution, not a collection of independent single-decrement lives.
For a realised scenario , define the year , cause surprise:
All these innovations vanish when . At termination , the cause-c innovation is . The innovation of any other cause in the same year equals . Therefore treating the cause indicators as independent would be wrong.
Let be the discounted cause-specific net amount at risk payable at the end of year . With cause-dependent death benefits and an appropriate prospective reserve , a typical amount is . The finite-horizon centred reserve surprise is
The mission defines this random variable directly. A cashflow-specific reserve recursion would be a further theorem, not a hidden hypothesis.
Cause-specific innovations from different years are orthogonal. At the same year, however, distinct causes have negative weighted cross moments:
The full annual Hattendorff contribution is therefore
This subtracts the square of the aggregate weighted amount at risk, rather than subtracting separate squares for individual causes. It is the unconditional variance contribution from one year's categorical decrement shock. The assumptions , and imply by weighted Cauchy–Schwarz.
The capstone asserts
It works with an arbitrary finite cause set and a countably infinite possible termination-year set. It does not yet claim an infinite-horizon limit, which can be developed by applying XXIII-style summability to these .
There are five new definitions, ten supporting milestone theorems and one capstone. The supporting obligations establish nonnegative year masses, exact observed/other-cause innovation values, zero horizon, the successor-year identity, nonnegative annual variance, scaling of risk exposure, and the negative cross-cause moment before proving the full year-by-year allocation.
The proof must distinguish the finite inner cause sum from the infinite outer lifetime sum; nonnegative mass and summability are explicitly required for countable expectation manipulations. The formal model allows zero annual incidence for a particular cause, but demands positive aggregate survival tails so the conditional fractions are defined. All proof obligations use the pinned Mathlib version and require authoritative Prove2Me remote compilation and accepted Lean proofs.
The AdS/CFT correspondence relates a theory of quantum gravity in anti-de Sitter space (the bulk) to a quantum field theory without gravity on its boundary (the CFT). A central question is how a local field operator deep in the bulk is represented by boundary operators. Almheiri, Dong and Harlow (JHEP 04 (2015) 163) pointed out a puzzle.
Their resolution is that the bulk effective theory is a quantum error-correcting code. Bulk operators are logical operators acting on a code subspace of the CFT Hilbert space. Different boundary representations agree only on that subspace, as one logical operator of an erasure-correcting code can be implemented on different subsets of qubits.
The mathematical backbone of that resolution is a finite-dimensional criterion for when a logical operator can be implemented on a given subsystem. This mission formalizes it (Appendix B of the paper), with the examples and corollaries of Section 3.
Timeline.
The physical Hilbert space is a tensor product of finite-dimensional spaces. is the part that may be erased (lost), and is the part that remains. A code subspace is a subspace .
An operator acts within the code subspace if both and map into itself. Such an operator has a representation on if there is an operator acting only on , that is of the form , with
Representations on are defined in the same way, with operators .
The three-qutrit code (Section 3.1) encodes one qutrit into three via
that is, and so on (Eq. (3.3)).
For an operator acting within ,
The result. The goal theorem characterizes, by a checkable commutation condition, which logical operators survive the loss of ; milestone 4 is its specialization to full erasure correction. Milestone 6 explains why a non-commuting algebra of bulk operators cannot be represented on two complementary boundary regions at once, so reconstructions of on different regions are distinct operators that agree only on the code subspace. The three-qutrit code models this: every logical operator is realized on any two qutrits, and no single qutrit carries information.
Formalizing it. All statements are proved in the source, or cited there from standard references, and are finite-dimensional. This mission produces machine-checked versions and a reusable vocabulary of code subspaces, logical operators and subsystem representations. That vocabulary is the starting point for formalizing the later results it underlies, in particular the subsystem and operator-algebra theorems of Harlow's derivation of the Ryu–Takayanagi formula (arXiv:1607.03901).
Status honesty. The mathematics is unconditional finite-dimensional linear algebra. The application to AdS/CFT rests on the conjectured duality and on bulk effective field theory, and is context only; none of it enters the hypotheses. The appendix proof is the authors' own, and the theorem is a special case of the results of Bény, Kempf and Kribs. The equivalence of (3.19) with correctability of the erasure (the existence of a recovery unitary, Eqs. (3.14)–(3.18)) is cited in the source from Schumacher–Nielsen and Grassl–Beth–Pellizzari, and is not part of this mission. No machine-checked proof of any of these statements is known. Neither Mathlib nor Physlib (including its quantum-information library) formalizes code subspaces, erasure correction or operator-algebra quantum error correction.
The forward direction of the goal is a direct computation. The converse is an existence statement: an operator has to be produced from a hypothesis that constrains only the matrix elements of between code states. That hypothesis says nothing about how acts off the code subspace, and generally acts nontrivially on . So no candidate for can be read off from itself.
Milestone 4 has the same character in both directions. One direction must produce a representation on for every operator acting within the code subspace, starting from the scalar condition (3.19), which concerns operators on alone. The other direction is a non-existence claim about operators on , to be derived from a property quantified over all logical operators.
The explicit-code milestones are finite but involve the irrational normalization and a -dimensional space.
⊗ₖ, is the conjugate transpose, and is star w ⬝ᵥ u.Submodule ℂ). It is described without a basis: " for all " is stated for all pairs of code vectors, which is equivalent by sesquilinearity.(A ⊗ₖ B) *ᵥ v), conjugate transposes of Kronecker products, orthogonal projection onto a Submodule, and partial traces. These are reusable; stand-alone contributions are welcome.An insurer choosing a retention or other reinsurance action in one year may affect both the immediate net claim cost and the distribution of liabilities in the following year. When the insurer values uncertainty using an exponential risk measure, the relevant policy objective applies the same conditional risk valuation recursively across policy years. A finite-horizon state-and-action model makes the timing, transition probabilities and policy optimality statement mathematically explicit.
This mission studies a finite-state, finite-action, discrete-time cost minimisation problem. Actions may represent a menu of excess-of-loss retention levels, but the formal statements allow any finite action menu and any state-dependent insurer cost schedule. It extends the cost-control ideas in prior actuarial missions into an explicitly risk-sensitive dynamic model. The result is a specialisation of finite-horizon recursive risk-sensitive Markov decision theory, with its own finite real-valued hypotheses and theorem proof obligations.
Let be the finite collection of financial, underwriting or liability states and a finite nonempty set of insurance actions. At the beginning of a policy year the insurer observes the current state and selects an action . At the end of that year, the state becomes with conditional transition probability .
We require, for each current state and action,
An individual destination is allowed to have probability zero. The annual real-valued cost includes the insurer's net premium, claim and treaty cashflows for the covered year, with its sign convention chosen so that larger positive values mean higher losses. A deterministic terminal amount values residual liabilities when the chosen finite horizon ends. With consistent payment-date conventions, let be the factor applied to the next year's continuation cost and the entropic risk-aversion parameter for costs.
The real-valued stage costs are finite by construction. Hence, because the transition row is a genuine probability law, the exponential moment defined below is strictly positive.
For any future state-value function , define
and the one-year risk-sensitive insurer cost
The cost and continuation value are included in one conditional exponential moment. The former is paid or valued within the current period, and the latter carries the next-year discount factor. The same chosen action changes both the costs and the transition row.
If every destination has the identical current-period cost and continuation , then probability normalisation implies . If every annual cost is increased by a fixed , the stage value increases by under the unit-mass probability row. With nonnegative transition probabilities, and , increasing either annual costs or future costs cannot decrease the entropic stage value.
For an annual cost independent of the next state, the expression simplifies to
Writing , the continuation term for is . In general it differs from . Entropic risk valuation is cash-additive and monotone under the stated conditions, but it is not generally homogeneous in the random cost. For , continuation costs make no contribution and no division by is performed.
This matters in actuarial applications: transplanting an expectation-based Bellman formula and simply replacing each conditional expectation with a fixed-parameter entropic premium would alter the intended discounted model.
Let denote the number of policy years remaining. A deterministic nonstationary Markov policy selects action when years remain and the current state is .
Its recursively valued insurer cost is
Define the finite-action entropic Bellman minimum by . Its finite-horizon optimum satisfies
At horizon zero the terminal amount is the entire valuation. At each successor horizon, the minimum is attained because the action set is finite and nonempty. Positive risk aversion, nonnegative discounting and a stochastic transition row make the entropic stage map monotone in its continuation argument. Those properties support induction from the terminal year backwards.
For the finite model above, the capstone combines domination of every deterministic nonstationary Markov policy with existence of an attaining Markov policy:
The second line asserts a single policy that works simultaneously for all starting states. Its state- and remaining-horizon-dependent actions may be obtained by selecting a minimiser at each finite Bellman step.
The formal graph contains definitions for the transition exponential moment, entropic stage valuation, finite-action minimum, fixed-policy value and Bellman value. The supporting theorem targets establish strict positivity, deterministic-value reduction, monotonicity, cash additivity, minimum comparison and attainment, the base and successor horizon identities, policy cost domination and an attaining policy. The capstone joins the latter optimality statements.
All probability distributions here have finite support in a finite state space, and the horizon is finite. Stochastic rows are required only where a conditional cost interpretation or positivity is used. Zero transition probabilities for particular destinations cause no division-by-zero problem. A zero-horizon value is exactly its terminal cost; removes future exposure from each one-step valuation. The type-level definition permits an empty state type, for which assertions at each starting state are vacuous, while the action type remains nonempty.
The positive-risk-aversion assumption excludes . Any analytical expected-value limit as would require a separate result. Negative gamma is outside the proposed monotone insurer-cost interpretation.
The capstone is stated for deterministic nonstationary Markov policies only. It does not formally establish comparison with all randomised or history-dependent strategies, optimality for infinite horizons or an HJB verification theorem for continuous-time stochastic factors. A finite treaty price from other actuarial missions may later be substituted into , after its own publication and consistency checks. No additional imported theorem dependencies are assumed here.
The source declarations have been checked by Prove2Me's private remote Lean compiler at the pinned Mathlib revision. The remote compiler's overall failure is deliberately caused by the incomplete proof bodies and a terminal type-mismatch sentinel; there were no unexpected declaration elaboration errors. This validates the proposed types and definitions, not any Lean proof. Independent high-precision finite model evaluation supports the mathematical direction, subject to the limitations of numerical evidence. The listed mathematical results remain proof obligations until accepted proof submissions exist.
[1] Bäuerle, Nicole and Glauner, Alexander (2022), Markov decision processes with recursive risk measures, European Journal of Operational Research, 296(3), 953–966. In the author preprint, Definition 4.6 states the one-step recursive risk operators, Theorem 4.7 establishes the finite-horizon Bellman value and existence of Markov optimal policies under Assumptions 3.1 and 4.2, and equation (4.2) is the one-step minimisation in the backward-induction proof. This mission explicitly specialises the framework to finite insurance costs and entropic valuation.
[2] Bäuerle, Nicole and Jaśkiewicz, Anna (2024), Markov decision processes with risk-sensitive criteria: an overview, Mathematical Methods of Operations Research, 99, 141–178. Example 1(a), equation (2) gives an entropic certainty equivalent in reward convention. The sign has been translated to an insurer cost/loss convention here.
[3] Actuarial Mathematics XVII: Finite-Horizon Markov Decision and Optimal Policy Valuation, previously published finite-state/action Markov recursion declarations. The present mission uses a distinct cost-minimising entropic stage operator, so it does not import XVII's reward-maximising Bellman definitions.
[4] Actuarial Mathematics XXI: Finite Exponential Premiums and Risk-Sensitive Retention, an earlier owner Draft concerning one-period entropic reinsurance premiums. Its unpublished declarations are not imported as available source modules.
An excess-of-loss reinsurance treaty divides each insurance claim between the insurer and a reinsurer at an agreed retention. The cedant retains the first portion of the claim while the reinsurer pays the excess. The decision to purchase reinsurance trades off the reinsurer's premium against the insurer's retained claims and risk-capital requirement.
Bäuerle and Glauner [1, §6] discuss the classic expected-value premium principle for reinsurance,
where is the ceded claim amount and is the reinsurer's safety loading. Their paper develops a broader discrete-time dynamic reinsurance application under risk measures. Glauner [2] develops a risk-sensitive Markov decision formulation for dynamic reinsurance with general premium principles. Brachetta and Ceci [3] provide the related continuous-time stochastic-factor excess-of-loss problem, which includes a more complicated HJB verification theorem.
This mission establishes a finite-scenario, single-period insurance cost and finite-retention optimisation layer. It makes the expected-value premium algebra precise, shows how the safety loading changes expected insurer cost, and introduces an illustrative, transparently specified variance-based capital add-on. The finite optimum is then attained by one of a nonempty set of allowable retentions. This mathematical bridge can later be incorporated into Mission XVII's finite-horizon optimal policy recursion.
Let be a realised gross insurance claim and the retention limit. The actuarial interpretation concerns , ; the Lean definitions extend the formulas to all reals for algebraic convenience.
The retained and ceded claims are respectively
Consequently
The insurer cannot retain more than either the original claim or its chosen retention. The ceded amount is nonnegative and decreases, or stays constant, as the retention is increased. These results follow directly from the minimum function without needing a particular claim distribution.
Let be a finite set of claim scenarios, with weights summing to one, and gross claim function . Define
The expected retained loss is , while the reinsurer's premium for the ceded part, under the expected-value premium principle with loading , is
The insurer's expected cost, comprising retained claims plus reinsurance premium, is
Because retained and ceded claims add to gross claims, linearity gives the useful exact identity
If , total expected cost equals gross expected claims and is independent of retention. If and scenario weights are nonnegative, increasing retention reduces the expected ceded amount and therefore cannot increase this pure expected cost:
This is not a general claim that greater retention is better for an insurer. It shows precisely why a risk criterion is needed when retention involves a trade-off: expected-value pricing with a nonnegative loading alone rewards retaining more risk.
To introduce a simple finite model of capital cost, define the retained-claim variance
For nonnegative weights this variance is nonnegative. Let be an illustrative cost per unit of retained variance and define
The functional is an explicit modelling choice for this mission, not a formula attributed directly to Bäuerle and Glauner. Their paper uses more general risk measures and cost-of-capital principles, which motivate the need for a risk-sensitive criterion. A variance charge is a mathematically simple finite-scenario proxy rather than the complete dynamic capital methodology of [1–2].
Under and nonnegative scenario weights,
At , the added capital cost disappears. Unlike pure expected cost, the variance-adjusted objective need not be monotone in retention. The optimum can depend on the distribution, reinsurer loading and variance charge.
Let be a finite nonempty set of permissible treaty choices, and let give the retention level associated with each choice. For an actuarial contract assume , though the Lean maximum/minimum existence theorems need only finiteness and nonemptiness.
Define the best achievable risk-adjusted cost
The supporting theorems establish that every candidate has cost at least , and some admissible choice achieves equality:
This result is finite-action existence, not a claimed optimal continuous stochastic control. If the chosen retention menu and claim process become state dependent, this one-step reward or cost can be fed into the finite-horizon dynamic programming model of Mission XVII, subject to an appropriate specification of state transitions.
The draft has seven definitions: retained claim, ceded claim, finite weighted expectation, loaded expected premium cost, retained variance, risk-adjusted objective and finite optimal retention cost. Fourteen supporting theorem targets prove split and bounds, the monotone ceded claim, premium decomposition, zero loading, monotonic pure expected cost, nonnegative retained variance, zero variance-charge limit and finite argmin existence. The capstone combines universal optimal-cost lower bounds and an attaining retention choice.
The algebraic identities hold for arbitrary real weights and monetary amounts, with nonnegative weights required for probability inequalities and variance nonnegativity. A unit-sum condition is necessary for interpreting weights as a probability law, although the core finite-sum identities remain true without it. The actuarial discussion assumes nonnegative claims and retention, and nonnegative loading and capital coefficient where specified.
No Monte Carlo approximation, continuous-time wealth process, ruin probability, stochastic premium model or HJB partial differential equation is asserted. The mission is a finite expected-cost and finite risk-penalty formalisation, designed as a controlled predecessor to more complex dynamic reinsurance.
All Lean statements are proposed proof obligations. A private declaration-compilation check, even if all statements elaborate, is not an accepted proof, and unpublished local definitions cannot be treated as already importable in individual theorem files.
[1] Bäuerle, Nicole and Glauner, Alexander (2021), “Minimizing spectral risk measures applied to Markov decision processes”, Mathematical Methods of Operations Research, Section 6, Dynamic optimal reinsurance, particularly equation (6.1), the premium-principle discussion and the discrete-time risk-sensitive optimisation context.
[2] Glauner, Alexander (2022), “Dynamic reinsurance in discrete time minimizing the insurer's cost of capital”, Scandinavian Actuarial Journal, pp. 279–306. Establishes a broader discrete-time reinsurance/Markov decision framework with general risk measures and premium principles; it does not specifically prescribe the variance-only charge chosen here.
[3] Brachetta, Matteo and Ceci, Claudia (2019), “Optimal Excess-of-Loss Reinsurance for Stochastic Factor Risk Models”, Risks 7(2), article 48, and open preprint. Motivates the retained claim function and later continuous-time control research, not a direct derivation of this finite-stage capital add-on.
Insurance premiums are commonly calculated from an expected claim with a safety loading, but this approach does not by itself distinguish risks having the same mean and different tail behaviour. A classical alternative is the exponential premium principle, also known as the entropic certainty equivalent. It charges for the full distribution of a loss through the expectation of an exponential transformation. Tsanakas and Desli [1] explain how the exponential premium principle arises from expected utility theory, and compare its properties with other premium and risk-measure principles.
Bäuerle and Glauner [2–3] study risk-sensitive Markov decision processes, including recursively applied risk measures and the entropic functional. This motivates a later dynamic reinsurance programme. The present mission deliberately formalises the finite-scenario, one-step algebra: positivity of the exponential moment, cash additivity and monotonicity of the premium, and attainment of a risk-sensitive choice from a finite menu of reinsurance retentions. It is not a theorem about general stochastic processes, asymptotic ruin probabilities or continuous-time optimal control.
Let be a finite set of insurance-claim scenarios, a loss amount, and the weight of each scenario. For a probability law assume
The positive risk-sensitivity parameter is . Define the exponential moment
For a nonnegative unit-sum weight law, for every real , since at least one scenario has positive weight and every exponential factor is positive. This guarantees that the real logarithm is applied to a strictly positive number.
The entropic insurance premium is
For any with positive exponential moment this is a well-defined finite certainty equivalent. The formal Lean definition uses real division for every , which is totalised at zero, but the actuarial interpretation and monotonicity theorem use strictly positive sensitivity. The formalisation does not assert that the formula is the limiting expected-value premium: proving that limit requires a separate analytic theorem.
If in every scenario, then
In particular, zero claims have zero premium. The key cash-additivity or translation-invariance identity is
and consequently, whenever and ,
Thus a known extra expense of is added directly to the premium, rather than changing how stochastic variability is priced. This monetary risk-measure property is one of the central axioms discussed by Tsanakas and Desli [1].
For two scenario claim amounts satisfying for every , positive sensitivity , and nonnegative probability weights, exponential and logarithmic monotonicity give
The supporting theorems prove the exponential-moment ordering first, then transfer it through the increasing logarithm and division by . The formal source does not assume the two risks are independent or that a moment-generating function exists outside the finite scenario model.
Suppose the cedant chooses an excess-of-loss retention . For a realised gross claim , the amount retained by the insurer is
Conventional insurance interpretation requires nonnegative claims and retention. The underlying Lean function is real-valued on all arguments so algebraic order properties can be stated without additional domain restrictions.
Let be a deterministic reinsurance premium quoted for retention . The combined risk-sensitive cost of the retention choice is
This is a model choice: the insurer adds the quoted cost of its treaty to the entropic valuation of the stochastic losses it still retains. The quoted premium is an arbitrary input function. The mission does not assume it decreases with higher retention, or that it has been calculated by the reinsurer using the same exponential premium principle.
Let be a finite, nonempty set of allowed treaty choices, with mapping each choice to a retention level. The optimal cost is
Since the action set is finite and nonempty, the minimum is attained. The capstone establishes that every menu action has cost at least , and there is an action satisfying
This is finite-menu optimisation. It does not by itself establish a finite-horizon optimal policy, solve a risk-sensitive Bellman equation, or prove optimality over a continuous retention interval. Those extensions require explicit state transitions and additional regularity or compactness assumptions.
Five definitions establish the finite exponential moment, entropic premium, retained claim, risk-sensitive one-period reinsurance cost, and finite-menu optimal cost. Thirteen supporting theorems establish nonnegative and positive exponential moments, constant-claim cases, factorisation and cash additivity, exponential and premium monotonicity, monotonic retained claim, and finite argmin bounds and attainment. The capstone combines finite-menu domination and an attaining retention.
The definitions and theorem statements apply to arbitrary finite types and real weights where algebraically meaningful; the probabilistic interpretation needs nonnegative weights of total one. Finite moments are automatically finite for real-valued scenarios, but the logarithm requires a positive moment for the usual risk valuation. The proof of cash additivity uses . The monotonicity theorem uses and nonnegative scenario weights.
This draft is a finite actuarial risk-valuation precursor. The literature includes further results, such as comparisons with expected value, convexity and recursion of risk measures. They are not declared proved by this mission. Neither a successfully elaborated Lean statement nor an independent arithmetic test constitutes an accepted Lean proof.
[1] Tsanakas, Andreas and Desli, Evangelia (2003), “Risk measures and theories of choice”, British Actuarial Journal, 9(4), pp. 959–991. Discusses exponential premium calculation, expected utility and the monetary properties and limitations of different risk measures. Open academic record.
[2] Bäuerle, Nicole and Glauner, Alexander (2021), “Minimizing spectral risk measures applied to Markov decision processes”, Mathematical Methods of Operations Research. Introduces the entropic certainty equivalent as when discussing risk-sensitive decision processes.
[3] Bäuerle, Nicole and Glauner, Alexander (2022), “Markov decision processes with recursive risk measures”, European Journal of Operational Research, 296(3), pp. 953–966. Develops recursive risk-sensitive Bellman equations and optimal Markov policies under suitable assumptions; the present mission only proves the simpler one-period finite-scenario predecessor.
A prospective insurance reserve is an actuarial estimate of future net obligations conditional on the policy being in force. A realised claim can differ from this estimate because death may occur earlier or later than expected. For a fully discrete life insurance contract, Hattendorff's theorem allocates the variance of the insurer's loss to individual policy years. A decisive preliminary identity is that the realised insurer loss at issue, after subtracting the opening reserve, equals a sum of discounted net amounts at risk multiplied by centred mortality innovations.
Shiu and Xiong [1] express loss at issue in their equation (1), derive a one-year reserve finite-difference identity in equation (3), and sum the resulting reserve changes in equations (4)–(5). This mission makes the corresponding finite-horizon, pathwise reserve-loss identity precise, including a terminal prospective reserve for policies still in force when the chosen horizon ends. It is the cashflow side of the finite-scenario innovation analysis proposed in Mission XVI.
The central distinction is important: the mission proves a deterministic identity for each possible curtate death year, provided the annual conditional rates and reserve recurrence are consistent. It does not itself construct the mortality probability distribution, derive conditional rates from a measure, prove annual orthogonality, or establish the final variance formula. Those tasks belong to the probabilistic components in XVI and their eventual integration.
Let denote curtate future lifetime. The event means the insured dies during policy year , with the associated benefit paid at time . Define the real-valued indicators
These satisfy the disjoint partition
Let be the finite valuation horizon, a per-year discount factor, the premium at the start of policy year , the death benefit at its end, and the prospective reserve at time on the in-force basis.
The finite-horizon net insurer loss, including the reserve required at the horizon for a policy still in force, is
The first term values year-end death benefits, the second subtracts premiums paid at the beginning of each covered year only while the policy remains in force, and the third carries forward the continuing liability.
For no premium or death benefit is included and . If , the insurer has not paid a death benefit during the chosen horizon, and the value includes . Therefore the mission does not assume that everyone dies before the selected horizon, nor does it discard an outstanding terminal liability.
Let denote the conditional probability of death during policy year , given the policy is still in force at its start, and let denote conditional survival through that year. Their one-year normalisation is
Let the annual prospective reserve balance be
This is the discrete one-year recurrence appearing in [1, equation (3)] before multiplication by and rearrangement. The source has an annual premium paid at the beginning and a death benefit at the end. The rates , benefit , premium and reserve sequence are inputs to the formal statement. Their actuarial origin is not silently assumed.
The formalisation deliberately permits arbitrary real quantities for the algebra. The usual probability interpretation additionally requires , and the conventional financial interpretation requires a valid positive discount factor. These stronger conditions are not needed for the pathwise identity itself once the two recurrence equalities are assumed.
The year- realised mortality surprise is
This equals on death in year , when the insured survives through year , and zero after the policy has ended. It is a pointwise cashflow expression here; statistical centring requires a later assumption that the supplied is the correct conditional death probability.
Define the discounted net amount at risk and its annual contribution:
The finite innovation value is
Unlike the more general mortality innovation mission, this draft explicitly connects the coefficient to the death benefit and prospective reserve rather than treating it as an arbitrary monetary sequence.
To see the mechanism, consider the change in the reserve-adjusted insurer loss when the horizon increases from to :
Substituting , the one-year reserve balance, and reduces that entire expression to
Sum this identity from to . All intermediate reserve balances cancel, leaving the capstone:
This equality holds for every and finite provided the year-by-year normalisation and reserve balance hold on the relevant years. It includes without a special artificial convention and it retains the terminal liability already included in . Neither nor is required.
When later coupled to a genuine mortality distribution and the statistical identities in Mission XVI, the representation provides the missing bridge for a finite-horizon discrete Hattendorff variance theorem. Such a coupling must explicitly reconcile the probability model, its conditional rates, and the definition of weighted variance. No published theorem is treated as a proved dependency merely because it has appeared as an Open Prove2Me target.
Six definitions introduce the in-force and death-year indicators, the realised finite loss with terminal reserve, an annual reserve balance predicate, a centred mortality surprise and the discounted net-at-risk innovation sum. Twelve supporting theorems establish time-zero and after-death indicators, the disjoint event partition, the zero-horizon loss and innovation, realised death/survival shock cases, finite-sum successor identities and the pivotal one-year reserve-adjusted loss identity. The capstone proves the finite pathwise equality for every curtate death year under annual assumptions for all years .
All source declarations use correct leading Lean imports. Every local definition import is required by the declaration it uses; the dependency graph must remain acyclic. Preliminary private remote elaboration checks only statement syntax and types. It is not an accepted Lean proof, nor does it show that not-yet-published definition modules are individually importable.
[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), (3), (4) and (5). In particular, their one-year reserve recurrence and summation-by-parts argument motivate the loss-to-innovation representation.
[2] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, §6.7, allocation of the overall life-insurance loss to individual 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. Supports the indicator-based perspective and the relationship between mortality surprises and annual loss allocation.
An insurer can transfer part of an unusually large claim to a reinsurer using an excess-of-loss contract. The insurer chooses a retention amount and remains liable for each claim only up to that amount, while the reinsurer covers the excess. A retention strategy trades off the cost of reinsurance protection against the amount of insurance loss retained.
Brachetta and Ceci (2019) investigate optimal excess-of-loss retention under a stochastic environment which affects claim frequency, claim severity and reinsurance premiums [1]. Their actual results use a marked point process, an exogenous diffusion factor, terminal exponential utility, a Hamilton–Jacobi–Bellman equation and a continuous-time verification theorem. This mission is not a purported proof of that stochastic HJB result.
Instead, it creates a rigorous finite-scenario, finite-action precursor: exact excess-of-loss claim sharing, weighted retained-claim valuation and the Bellman optimisation operator for a finite collection of actions. The direct source for discrete finite-horizon optimality is Puterman, Markov Decision Processes, Chapter 4 [2], which develops dynamic programming and the existence of deterministic optimal actions. A genuine stochastic reinsurance-control model can later replace the discrete scenario assumptions, construct the controlled wealth process and address the full HJB theorem of [1].
Let be a gross claim amount and be the retention threshold. The insured-life/non-life interpretation requires and , but the Lean functions themselves are defined algebraically on all real numbers.
The insurer retains
and cedes to the reinsurer
Consequently the claim is allocated without double counting:
The supporting theorems show that retained loss cannot exceed either the original claim or the retention limit, that ceded loss is nonnegative, and that raising the retention threshold cannot reduce the retained loss. For nonnegative claims, setting leaves no retained loss. If , no excess is ceded.
The division of claim amounts follows the surplus decomposition in Brachetta and Ceci [1, §2], where the retained claim is expressed by the minimum of the claim size and the control.
Let be a finite set of claim scenarios. For scenario , let be the gross claim and a probability weight. Probability interpretation requires
The expected retained claim amount for retention is
Let be the reinsurance premium charged for that retention. The one-period expected insurance and reinsurance cost is
This simple expected-cost criterion captures the basic trade-off: a lower retention reduces claims retained, generally at the cost of a higher reinsurance premium. The theorem definitions impose no monotonicity on the premium function ; if actuarial monotonicity is required, it must be included as a separate hypothesis.
The finite expected-loss function is nonnegative under nonnegative scenarios, retentions and weights. It is increasing in retention when the weights are nonnegative. These are algebraic checks, not a claim that minimising this expected cost is equivalent to maximising exponential terminal utility in [1]. The source article uses the latter, more sophisticated objective.
To prepare for multi-year optimal reinsurance, let be a finite state space, a nonempty finite admissible action set, and the one-step transition weight from state to when action is selected. Let be the one-period reward, a deterministic discount factor and a next-period value.
The return associated with one action is
The finite-action Bellman operator is
Since is nonempty and finite, the maximum is attained. The capstone formally targets
This is the finite-horizon principle of selecting an optimal discrete action, not continuous-time HJB verification. Puterman [2, Chapter 4] discusses the Bellman recursion and the existence of deterministic Markov policies for finite-horizon decision problems. To model reinsurance with this operator, later theorems must specialise to admissible retention limits, define state-dependent premium and claim distributions, and prove row-stochasticity and any desired utility assumptions.
The draft intentionally does not claim that arbitrary matrix entries define a valid probability law. The finite Bellman maximum and the two capstone inequalities are algebraically meaningful for arbitrary real weights; a controlled Markov-process interpretation requires additional conditions.
Five definitions introduce gross claim retention, ceded claim, finite weighted retained loss, one-year reinsurance cost and the finite-action Bellman operator. Twelve supporting theorems cover the claim split, nonnegative and monotone retention results, expected retained-loss monotonicity, stage cost and Bellman lower bounds. The capstone packages upper domination and attainment of the Bellman maximum.
All local imports appear before other Lean commands. Every theorem is currently a proposed proof obligation; the source-elaboration checks are private and do not constitute accepted proofs. Definitions that are not yet published cannot be assumed importable in the production theorem preview.
This is a foundations mission for a later reinsurance-control programme. A credible subsequent research mission will need the full conditional marked-point-process model, wealth dynamics, admissible adapted controls, exponential utility and the analytic regularity assumptions of [1] before attempting its backward-PDE verification result.
[1] Brachetta, Matteo and Ceci, Claudia (2019), “Optimal Excess-of-Loss Reinsurance for Stochastic Factor Risk Models”, Risks, 7(2), article 48. The claim process and retention control are in §2, the HJB formulation in §3, optimal strategies in §4 and the verification argument in §5. This article motivates the reinsurance problem but its continuous-time verification theorem is outside the present draft.
[2] Puterman, Martin L. (1994), Markov Decision Processes: Discrete Stochastic Dynamic Programming, Chapter 4, “Finite-Horizon Markov Decision Processes”, Wiley, pp. 74–118. Includes finite-horizon policy evaluation, optimality equations, deterministic Markov policies and backward induction. This is the direct source for the discrete Bellman stage.
[3] Brachetta and Ceci (2019), open preprint, arXiv:1904.05422. Independent accessible source for the original stochastic-factor control problem and its distinct continuous-time assumptions.
A prospective life insurance reserve describes the expected remaining loss on a policy at a valuation date. An alternative way to understand the insurer's total future loss is to allocate it between individual policy years. Each year produces an insurance cashflow and a change in the reserve needed to support future benefits. When properly centred by the reserve balance, the resulting annual gains have expectation zero. Hattendorff's theorem connects this allocation to the striking result that losses for distinct years are uncorrelated and the variance of total discounted loss is the sum of their individual discounted variances.
The classical finite annual result is covered by Gerber, Life Insurance Mathematics, third edition, §6.7, particularly equations (6.7.3) and (6.7.6)–(6.7.10) [1]. A modern actuarial derivation is developed in the European Actuarial Journal article An elementary derivation of Hattendorff's theorem [2]. The connection to martingale increments is emphasised by Norberg [3] and by Gerber, Leung and Shiu [4].
This mission formalises a finite-scenario annual-loss allocation and Hattendorff-style variance identity. It makes the distinction between a proved algebraic decomposition and the deeper stochastic theorem explicit: annual orthogonality is a hypothesis of the capstone, with its derivation from conditional mortality and reserve dynamics reserved for a subsequent extension. Thus the mission does not claim that an arbitrary pair of yearly cashflows is uncorrelated.
Let be a finite sample space, and let denote the probability assigned to scenario . A valid scenario probability law has nonnegative weights summing to one. The mission defines the finite weighted expectation
Its supporting results establish expected values of constants and linear combinations. For scenario cashflows and , weighted variance and covariance are defined by
The definitions work for arbitrary real arrays of weights, while the actuarial probability interpretation assumes valid scenario probabilities. Finite sums avoid moment-integrability issues without imposing an artificial condition such as independence between years.
Let be the net insurer cash outgo during policy year , measured at that year's start, and let be the deterministic opening prospective reserve under a given in-force valuation basis. With per-year discount factor , define the annual gain or loss component
The term represents the discounted liability carried into the next year, while is the reserve released from the opening position. The sign convention is insurer loss, so positive values represent net outgo or an adverse change.
If the annual reserve balance is
then linearity gives
This is the first actuarial component of Hattendorff's framework: properly reserved annual losses are centred under the valuation basis. The finite scenario weights need to sum to one, and the reserve balance must be assumed or established. Merely defining does not give it zero mean.
The total discounted annual gain through years is
Expanding the annual gain definition and telescoping the reserve terms gives the pathwise identity
The terminal reserve is retained explicitly. It must not be assumed zero for an arbitrary incomplete policy horizon. This exact finite-period formula corresponds to the annual allocation of loss and reserve changes discussed in [1, §6.7, equation (6.7.3)], with the horizon and terminal liability clearly stated.
The empty-term case has . Increasing the horizon from to adds precisely . These boundary and recursion lemmas form a useful independent verification layer for the finite sum.
When distinct annual gains have zero covariance,
their discounted aggregate variance has no cross-year terms:
Importantly, uncorrelated does not mean independent. Annual losses are linked by the same insured life, survival history and reserve process. Hattendorff's theorem establishes the required uncorrelatedness from the correct conditional insurance model; the zero-covariance condition is an explicit hypothesis in this mission's finite-scenario algebraic capstone. This distinction is important for the formalisation and is consistent with [1, equations (6.7.6)–(6.7.8)] and the martingale explanation in [3–4].
The supporting theorem on variance of a sum, variance scaling and covariance symmetry makes the algebra behind the annual allocation explicit. Zero-mean gain and zero-covariance assumptions must be separately justified when moving from this finite abstract setting to a particular mortality model.
The capstone assumes a finite scenario law whose weights sum to one, a sequence of yearly cashflows , deterministic reserves , a reserve balance for each year , and pairwise zero covariance of the resulting annual gains. It then proves three statements together: each year's gain is centred, the discounted variance splits additively by year, and the discounted sum telescopes to net cashflows plus the terminal reserve less opening reserve.
Five definitions establish weighted expectation, annual reserve gain, discounted aggregate gain, variance and covariance. Thirteen supporting theorem targets handle elementary expectation algebra, finite-year telescoping, zero-mean reserve gains, covariance symmetry and orthogonal variance decomposition. A capstone combines these results.
This is explicitly the finite algebraic and reserve-accounting stage, not a complete proof of Hattendorff's theorem for arbitrary life insurance contracts. A later mission should construct the curtate-lifetime annual innovations using the published reserve recursions of Mission XI, establish the conditional mean-zero property from survival information and derive cross-year orthogonality without assuming it. Only that later bridge will discharge the substantive stochastic obligation. No independence claim is made.
Every item is a proposed Lean statement. The isolated-module imports appear before other Lean commands, and no unpublished definition is treated as already available to the live compiler.
[1] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, §6.7, Allocation of the Overall Loss to Policy Years, equations (6.7.3)–(6.7.10). Publisher book record.
[2] An elementary derivation of Hattendorff's theorem, European Actuarial Journal (2021), DOI: 10.1007/s13385-020-00256-9. Develops the annual insurer-loss formula using the prospective reserve recurrence.
[3] Norberg, Ragnar (1992), “Hattendorff's theorem and Thiele's differential equation generalized”, Scandinavian Actuarial Journal, pp. 2–14. Places the annual uncorrelated-loss principle in a broader stochastic and martingale setting.
[4] 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 the actuarial theorem to uncorrelated martingale increments.
A traditional life-insurance model may have one way of exiting the insured state, namely death. Many actuarial contracts instead allow multiple mutually exclusive decrements. A policyholder might exit through death, disability, withdrawal or retirement, and different causes may trigger different benefits. A net premium reserve must therefore allow one-year payments that vary by the cause of exit, as well as the liability continuing for policies that do not exit.
Gerber, Life Insurance Mathematics, third edition, Chapter 7 §7.5 [1], derives the multiple-decrement reserve and its one-year recursion, followed by a decomposition of premium into reserve accumulation and the expected cost of the net amounts at risk. The same models are related to the broader multiple-state framework developed in Dickson, Hardy and Waters (2009), Chapter 8, including §8.8 on multiple decrements [2].
This mission formalises the one-year multiple-decrement reserve balance and premium decomposition for a finite set of causes. It is a deliberately local actuarial model: it handles one policy year and deterministic opening and closing reserves, without assuming that the complete lifetime-dependent reserve functions from Missions XI or XII have already been published.
Let be a finite set of mutually exclusive causes of exit. Fix a policy in force at the start of the year. Let denote the conditional probability of surviving in force to the following year, and the conditional probability of decrement cause during the year.
The one-year decrement law is valid when
The possible decrement causes are alternative outcomes of the same year. Their probabilities are added because the causes are mutually exclusive; they are not independent risks. The survival probability refers to remaining in force, rather than necessarily being alive in every possible post-decrement state.
The formal model treats as any finite type. No nonempty-type hypothesis is required: if is empty, the unit-probability law forces and reduces to certain survival, without exit benefits.
Let be the benefit payable at the end of the year following exit for cause . The conditional expected exit benefit before discounting is
Let be the reserve immediately before the current premium, let denote the reserve required at the next annual valuation for surviving policies, and let be the annual discount factor. Assume the year-end reserve for policies which exit is zero after payment of the cause-specific benefit. Under this timing, the expected present value of the following-year liability is
The required premium is defined by the annual reserve balance
Equivalently, the formula defines
This is the discrete conditional one-year multiple-decrement generalisation of the annual life-reserve recursion in [1, equation (7.5.2)]. It does not assert that the reserves and were derived from a complete prospective valuation, nor that an arbitrary premium chosen externally automatically satisfies the balance. Those tasks require a separate multi-year model.
The one-year required premium can be separated into two economically interpretable parts. The savings premium grows the opening reserve towards the next reserve:
The risk premium finances benefits above or below the amount of reserve that would otherwise remain at the next annual valuation:
Since the decrement law satisfies ,
Thus the principal premium decomposition is
This follows the savings and risk-premium interpretation of [1, equations (7.5.3)–(7.5.5)]. A negative risk premium is possible algebraically when cause benefits are lower than the continuing reserve. The formal theorem does not assume all monetary amounts are nonnegative.
If , every in-force policy exits during the year, and the continuing reserve term vanishes:
If no decrement can occur, and for every cause, the required premium reduces to the savings component alone,
If every cause of exit pays exactly the same amount as the following-year reserve, , the risk component is zero. Scaling all monetary benefits and reserve amounts by a common factor scales the premium by that factor.
The draft introduces five definitions: a valid annual decrement law, expected cause benefit, required annual premium, savings premium and risk premium. Eleven supporting theorems establish probability conditions, zero and scaled benefits, reserve balance, zero-survival and no-decrement limits, risk-free exits and the premium decomposition. The capstone combines the one-year reserve balance with the savings/risk identity.
The definitions and theorem types are independent of unconfirmed Prove2Me actuarial declarations from earlier missions. Imports of local definitions are explicitly placed at the beginning of each Lean file, and the proposed statements do not treat a Draft declaration as a published theorem. The proofs of the individual statements remain to be supplied after captain and moderator review.
[1] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 7, Multiple Decrements, §7.5, The Net Premium Reserve, equations (7.5.1)–(7.5.5). In particular (7.5.2) is the annual multiple-decrement recursion and (7.5.3)–(7.5.5) separate the savings and risk portions.
[2] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 8, Cambridge University Press, §8.8, Multiple Decrement Models.
[3] Dickson, Hardy and Waters (2009), Chapter 7, Policy Values, annual policy-value recursions. The one-cause formula provides the earlier special case from which the multiple-cause generalisation develops.
The expected error of the randomized SVD with a Gaussian test matrix is times the optimal error (Halko–Martinsson–Tropp 2011, Theorem 10.5). The factor is for a standard Gaussian matrix : the quality of every Gaussian sketching method is governed by inverse moments of a Gaussian matrix — moments of its pseudoinverse, equivalently of the inverse of the Wishart matrix . The expected spectral error uses instead (Tropp–Webber 2023, Lemmas B.2–B.3), and deviation bounds use tail estimates for both norms (HMT Proposition 10.4). None of these inverse moments is available in Mathlib. This mission proves them.
A standard Gaussian matrix has independent entries; its law is . Throughout, is wide or square, , so that is almost surely invertible; is a Wishart matrix with degrees of freedom and is inverse-Wishart.
The pseudoinverse of a full-row-rank matrix is . Its norms are determined by the inverse Wishart matrix:
where is the Frobenius norm, the spectral norm (largest singular value) and the smallest of the singular values of . The letter denotes Euler's number.
For integer and ,
The case is , the spectral inverse moment at the heart of expected spectral-norm error bounds. It is the goal because it is the one inverse moment that is not an exact formula: its proof passes through Edelman's bound on the density of and an explicit integration, and it implies the expectation bound of HMT Proposition 10.2 by Jensen's inequality.
The results. Combined with the second-moment identity and block independence of Mission I, the Frobenius inverse moment gives the expected Frobenius error of the randomized SVD and of generalized Nyström; the spectral inverse moment gives the expected spectral error and the core-noise bounds of truncated sketching methods; the two tail bounds give the large-deviation statements of HMT §10.3. The second-order inverse-Wishart moments quantify the variance of , which Tropp–Webber use for concentration of the randomized SVD error.
Formalizing them. The inverse-Wishart mean and the second-order moments are classical multivariate-statistics formulas (Muirhead; von Rosen) with no Mathlib counterpart. The Chen–Dongarra tail requires the exact distribution of , or at least Edelman's density bound; the Frobenius tail is HMT's own argument through the bidiagonal (Householder) model of a Gaussian matrix and chi-square moment estimates. Every statement here is a proved theorem in the literature; none has a machine-checked proof.
There is no Wishart distribution in Mathlib. The direct approach — compute the density of and integrate — needs the Wishart density, a change of variables on the cone of positive-definite matrices, and the matrix-variate gamma function. The classical route to the mean avoids this: by rotational invariance has the same law as for every orthogonal , so its mean is a multiple of the identity, and the trace is -type quantities whose means are elementary; making "the diagonal entries of are reciprocals of variables" rigorous requires the Gram–Schmidt (QR) decomposition of a Gaussian matrix and the independence of its factors. The spectral inverse moment needs a lower-tail bound for of the exact order ; a union bound over rows loses a factor and does not give the stated constant. The naive attempt to bound by loses a factor as well.
is sampled from the product measure on arrays; is Mathlib's total matrix inverse, equal to on the null set where is singular, and is defined as (pinvR). Every inequality is stated together with integrability of its integrand, so the Lean convention that a non-integrable function integrates to cannot make a bound vacuous; identities with nonzero right-hand sides force integrability on their own but are also stated with it. The inverse-Wishart mean is stated entrywise. Tail bounds are inequalities between a measure in and of the real bound. Real powers with non-integer exponents are Mathlib's rpow; all bases are positive under the hypotheses. The spectral norm is Mathlib's operator norm. The sizes follow Tropp–Webber (); HMT's and conventions are translated in each item's source field.
Welcome contributions: a Wishart/inverse-Wishart library (QR decomposition of a Gaussian matrix, Bartlett decomposition, chi-square moments ), and the distribution of of a Gaussian matrix (Edelman).
Shared definitions: the items of this mission import Definitions.Def_GaussianMatrix_basic, a draft of Mission I; submit that proposal first so the import resolves at compile time.
Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.
Policy gradient methods are the main family of reinforcement learning algorithms that search directly over a parameterized class of stochastic policies , , by stochastic gradient ascent on the expected discounted return. They underlie REINFORCE, actor-critic methods and their deep-learning descendants. The return is a nonconvex function of , and the gradient is available only through Monte Carlo samples of trajectories, so the basic question is what the iterates of such a method converge to.
Classical analyses of actor-critic algorithms (Konda and Tsitsiklis, 2003) use the ODE method of stochastic approximation and assume that the gradient estimate is unbiased. In the infinite-horizon discounted setting, a trajectory of finite length cannot by itself produce an unbiased sample of the gradient. Zhang, Koppel, Zhu and Başar (arXiv:1906.08383, SIAM J. Control Optim. 58(6), 2020) resolve this with random horizons: drawing the trajectory lengths from geometric distributions makes the resulting estimate exactly unbiased and almost surely bounded. They then prove convergence of the resulting random-horizon policy gradient (RPG) algorithm with the supermartingale convergence theorem, an optimization argument that also yields rates. This mission formalizes that first part of the paper (§2–§4 and App. A.1–A.4). The paper's later results on escaping saddle points are not part of it.
A finite Markov decision process is a tuple : finite state and action sets, transition probabilities , rewards and a discount factor . A stochastic policy gives a probability vector on at each state. Its value and Q-function are the expected discounted returns from a state, respectively a state-action pair.
A parameterized policy assigns to each a policy . Fix an initial state . The objective is
The score function is . The discounted state-occupancy measure is , and .
Assumption 3.1 asks for and for a differentiable policy whose score exists, is -Lipschitz in and is bounded in norm by . Two constants recur below:
The RPG algorithm (Algorithm 3) works as follows at the current iterate :
Assumption 4.1 is the Robbins–Monro condition , .
Under Assumptions 3.1 and 4.1, almost surely
and almost surely every cluster point of satisfies . The page states the conclusion as "", where is the set of stationary points. Read literally, that asserts convergence of , which fails when has no stationary point at all (one state, two actions, a softmax policy). The goal states what the proof on p. 30 concludes.
With constant stepsize and Assumption 3.1 only, for every ,
The theorem shows that Monte Carlo policy gradient, with a sampling scheme that can be implemented from simulated trajectories alone, behaves like an exact stochastic gradient method on a smooth nonconvex objective. It needs no ODE approximation, no two-timescale critic and no assumption that the estimate is unbiased: unbiasedness is proved (Theorem 3.4). The same estimates give the finite-time bound of Corollary 4.4 and are the starting point of the paper's second part, which adds perturbations to escape saddle points.
To our knowledge none of these results has been machine-checked. The mission's work is to formalize the known proof: the infinite-horizon policy gradient theorem with a vector parameter, the smoothness bound with its explicit constant, the exact law of the random-horizon estimator and its moments, and the supermartingale argument. The formal statements also repair three misprints of the source: the conclusion of Theorem 4.2, the tail of (A.22), which is read as , and the of Corollary 4.4, which is replaced by its explicit form (A.37).
Each step of the argument is standard on paper. The work is in the parts that the paper treats in one line:
PolicyValue, QFunction, OccupationDist, IsPolicy, IsTransitionKernel). is EuclideanSpace ℝ (Fin d), and is Mathlib's gradient.rpgLaw θ is the law of , built from the geometric horizons, the trajectory probabilities and EstQ. A run is a filtered probability space carrying and with on every path, adapted, and the conditional law of given equal to rpgLaw θ_k.rpgLaw would assume Theorem 3.4 and turn the goal into generic SGD; that encoding is ruled out. A sorry-free example shows that the run hypothesis is satisfiable and that rpgLaw is a probability measure.Tendsto of the partial sums to . "Cluster point" is MapClusterPt.rpgLaw. These are reusable for every Monte Carlo policy gradient analysis.A chance-constrained program minimizes a cost over decisions subject to the requirement that a random constraint holds with probability at least : , where collects constraint functions and is a risk level. Such constraints model reliability requirements in power systems, finance and engineering design. They are hard to handle numerically: the probability is rarely available in closed form, its sample estimate is a step function of , and the feasible region is in general nonconvex.
Peña-Ordieres, Luedtke and Wächter (arXiv:1905.07377v2; SIAM J. Optim. 30(3), 2020, DOI 10.1137/19M1261985) replace the probability by a smoothed sample quantile, which turns the chance constraint into a single smooth nonlinear constraint, and solve the resulting problem with a trust-region method built on an exact penalty, in the spirit of the SQP method for regular nonlinear programs (Nocedal and Wright). This mission formalizes the analytic core of that method: the smoothed quantile is well defined and has a bounded, Lipschitz gradient, and the piecewise quadratic model used to compute trust-region steps agrees with the penalty function up to second order.
Fix . The smoothed indicator equals on , on , and a strictly decreasing function in between, chosen so that is differentiable (equation (2.2)). The concrete choice is the quartic kernel (2.6),
which makes twice continuously differentiable.
Fix a sample of the random vector. For , the smoothed -quantile is the number solving
It is applied to the vector with entries , and the smoothed sample problem requires .
With deterministic constraints and a penalty parameter , the exact penalty function is
The trust-region step at minimizes the model
where is a symmetric matrix, and .
If and have Lipschitz gradients, each is -Lipschitz with -Lipschitz gradient, is the quartic kernel and , then for fixed there is a constant with
The constant is not specified, so the goal survives any sharpening of the estimate.
Proposition 5.3 is the hypothesis under which the trust-region convergence theory of Conn, Gould and Toint (cited as Theorem 5.4, from their Theorem 11.2.5) applies: it guarantees that the method of §5 converges to stationary points of . Combined with the exact-penalty result of Curtis and Overton (cited as Theorem 5.2), which says that for large enough local minimizers of the smoothed problem are local minimizers of , this justifies solving the smoothed chance-constrained problem by minimizing . Proposition 4.1 is independently useful: it says that the smoothed quantile can be handed to any smooth nonlinear solver as a constraint with a bounded, Lipschitz gradient.
The results are proved in the paper. None of them has a machine-checked proof that this mission is aware of. A formalization would also settle two points the printed proofs leave thin: the uniform lower bound on the denominator in Proposition 4.1, which the paper asserts without argument, and the existence part of Lemma 2.1, whose printed proof argues only uniqueness.
The model error splits into three parts. The and parts are standard Taylor estimates. The quantile part is the substance. First, is defined only implicitly, so its differentiability needs the implicit function theorem, and its gradient bound needs a lower bound on that is uniform over all , not just pointwise. The pointwise statement is easy: some sample lies strictly inside the smoothing window. The uniform statement needs a quantitative version of that fact, which uses the fractional part of . Second, is a maximum of smooth functions and is not differentiable, so the model linearizes each before taking the maximum; one has to show this costs only , uniformly in .
All objects are defined in one module, SmoothCCP.PenaltyModel.Setting. Decisions and directions live in EuclideanSpace ℝ (Fin n), so gradients and are inner products. is a self-adjoint continuous linear operator and is its operator norm. Sample values are a fixed list ξs : Fin N → Ξ; this mission involves no probability. is a function on Fin N → ℝ (sup norm), defined as the least root of (2.3) via sInf. Its gradient is the Fréchet derivative. is deriv of the smoothed indicator, which is differentiable for the quartic kernel, including at . The maximum over uses Finset.sup' and needs (the paper's §5 has ). The Euclidean norm on appears explicitly only in milestone 5, where it is written to match the printed factor .
Standing hypotheses: , , , and . From Proposition 4.1 on, is the quartic kernel. Three readings are disclosed in the goal's statement. The Lipschitz hypotheses (5.4)–(5.5) are assumed on all of and per component , because the conclusion ranges over all . The quartic kernel and are assumed because the proof uses Proposition 4.1. The constant is quantified after all data and and before , , .
is the paper's quantile, defined from (2.3), not a function assumed to satisfy it. A statement in which the uniform constant may depend on , or , or in which (2.3) has no root, would be trivial and is excluded.
A complete development needs the implicit function theorem for (Mathlib's HasStrictFDerivAt.implicitFunction or a one-dimensional argument), first-order Taylor bounds for functions with Lipschitz gradients, and elementary facts about the quartic kernel. The Taylor bounds and the facts about maxima of linearizations are reusable beyond this mission. Proofs of any milestone are welcome independently.
Many problems in optimization, variational inequalities and saddle-point computation can be written as a monotone inclusion: find with , where is a set-valued maximally monotone operator (a subdifferential, a normal cone) and is single-valued (a gradient, a skew saddle operator). Splitting methods treat only through its resolvent and only through forward evaluations. The classical forward-backward method needs to be cocoercive, which rules out saddle-point operators; Tseng's forward-backward-forward method removes this but needs two evaluations of per step.
Malitsky and Tam (arXiv:1808.04162, SIAM J. Optim. 30(2), 2020) introduced the forward-reflected-backward method, which needs only monotonicity and Lipschitz continuity of and one new evaluation of per iteration. Its step size in Section 2 depends on a global Lipschitz constant of . Such a constant is often unknown, expensive to estimate, overly conservative, or nonexistent when is only locally Lipschitz. Section 3 of the paper replaces the fixed step by a linesearch (backtracking) and proves convergence for locally Lipschitz in finite dimensions. This mission formalizes that result.
Let be a finite-dimensional real inner product space. An operator is monotone if whenever , , and maximally monotone if moreover its graph is not properly contained in the graph of another monotone operator. For the resolvent is the map with for every . A map is monotone if , and locally Lipschitz if every point has a neighbourhood on which is Lipschitz. The zero set is .
Fix and . Given , and the previous step , the trial point at step is
Algorithm 1 starts from arbitrary and . In each iteration it chooses , sets with the smallest nonnegative integer for which
The choice of may change from one iteration to the next; allows the step to grow.
If is maximally monotone, is monotone and locally Lipschitz, and , then every sequence generated by Algorithm 1 satisfies
The statement fixes no constant: it holds for every , every , every initial pair and every sequence of choices of .
stated for (see Formalization scope). 3. The iterates are bounded and . 4. (33): there is with for all . 5. The step sizes are bounded away from zero.
The theorem makes the forward-reflected-backward method usable without any knowledge of a Lipschitz constant, and extends it to operators that are only locally Lipschitz, such as gradients of functions without globally Lipschitz gradient or saddle operators of smooth non-quadratic convex-concave functions. The linesearch costs one resolvent and one evaluation of per trial, and the adaptive factor lets the steps recover after a conservative phase. The same template (an energy inequality where the linesearch test stands in for the Lipschitz bound, followed by a lower bound on the step sizes) recurs in adaptive and backtracking variants of many first-order methods.
The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal account of Algorithm 1 including the minimality of the backtracking index, which is where informal accounts of linesearch methods tend to be imprecise. It also records one correction: Lemma 3.3 as printed asserts (32) for all , but at the bound concerns initial data that Algorithm 1 never tests, and it fails there. Theorem 3.4 is unaffected.
Two steps do not transfer directly from the constant-step analysis. First, termination of the linesearch requires the limit behaviour of resolvents as the step tends to zero (, Bauschke–Combettes, Theorem 23.47), combined with continuity of at the current point; local Lipschitz continuity enters only here and in the last step. Second, the step sizes must be bounded below. The obvious argument combines the accepted test (30) with the Lipschitz bound (33) along the iterates, but (33) concerns accepted points, while a rejected trial step concerns a trial point that is not an iterate. One must show that the rejected trial points also stay in a fixed bounded set, on which is Lipschitz. Finite dimensionality is used exactly to pass from local Lipschitz continuity to Lipschitz continuity on bounded sets.
is a type with [NormedAddCommGroup H] [InnerProductSpace ℝ H] [FiniteDimensional ℝ H]; it is never specialised to EuclideanSpace ℝ (Fin n). The operator vocabulary (monotone, maximally monotone, resolvent) is the published module ThreeOpSplitting.Accel.MonotoneOperators; local Lipschitz continuity is Mathlib's LocallyLipschitz. Conventions committed to:
J : ℝ → H → H with IsResolventFamily A J; for maximally monotone it exists (Minty) and is unique on . The goal keeps maximal monotonicity of as well.x j is and lam j is , so lam 0 . Algorithm 1's initialization also names a that the iteration never uses; it is not a parameter.IsLinesearchRun J B δ σ lam x requires at every iteration some and an index such that , is the trial point at , (30) holds, and (30) fails at every smaller index. Every sequence of choices is admitted.Filter.Tendsto x atTop (nhds xs).Trivializing encodings are ruled out: the resolvent is tied to by IsResolventFamily rather than left free; the minimality clause prevents arbitrarily small accepted steps; is not fixed; convergence is in norm, not weak; and a global Lipschitz hypothesis on , which would reduce the goal to mission 1 of this series in finite dimension, is not assumed. The hypotheses are satisfiable (a sanity file checks , , ).
A complete development needs: nonexpansiveness and continuity in the step of resolvents of maximally monotone operators, including the small-step limit to the projection onto ; Lipschitz continuity on compact sets of locally Lipschitz maps; the telescoping argument of Theorem 2.5; and a finite-dimensional closedness argument for the graph of . The resolvent facts are reusable well beyond this mission. Proofs of individual milestones, and of the resolvent lemmas as separate items, are welcome.
How many edges can a graph have if it contains no long cycle? This Turán-type question for the circumference goes back to Erdős and Gallai (1959), who showed that an -vertex graph with circumference has at most edges. For 2-connected graphs the answer is exact and the extremal graphs are known, so the natural next question is stability: what does a graph look like when its edge count is just below the extremal value? Such statements are the standard input for exact results via the stability method, and for counting and spectral variants of the original problem.
Timeline.
All graphs are finite and simple, with vertex set . The circumference is the length (number of edges) of a longest cycle. is 2-connected if it has at least three vertices and stays connected after deleting any one vertex. is the minimum degree and the number of edges.
For , the graph is a clique together with further vertices, each joined to the same vertices of the clique. It has vertices, minimum degree , circumference , and
edges. The graph is the union of a clique and cliques , any two of the cliques sharing the same two vertices. The families and consist of graphs on (resp. ) with a clique of size , stable and complete to . In every vertex of has exactly two neighbours, the same and . In , carries a star forest whose stars all attach to the same two vertices in a prescribed way.
The proof works with the -closure of a cycle . It is obtained by replacing by its -closure, which repeatedly joins non-adjacent pairs of whose degree sum is at least . A cycle is locally maximal if every longer cycle uses at least three edges between and the rest of the graph.
Let and let be 2-connected on vertices with and circumference , . If
then , or , or (, odd, and is a subgraph of a member of ), or ( and ).
For a longest cycle , the same hypotheses give one of four alternatives. Either ; or ; or the alternative holds; or and .
The milestones follow the paper's proof.
The theorem describes every 2-connected graph whose edge count comes within one step of Woodall's extremal bound in either parameter. At it recovers the theorem of Füredi, Kostochka, Luo and Verstraëte exactly. At it refines the Li–Ning / Füredi–Kostochka–Luo stability theorem for non-Hamiltonian 2-connected graphs. It also gives Corollary 1.8 for 3-connected graphs, where only the two graphs remain. Theorem 1.9 goes further and identifies the extremal configurations exactly, up to the closure.
On the formal side, Mathlib has walks, cycles, Hamiltonian paths and cycles, clique numbers and graph embeddings. It has no circumference theory, no Bondy–Chvátal closure, no Hamiltonian-connectedness and none of the classical extremal results the proof cites (Dirac, Bondy, Chvátal, Erdős–Gallai, Fan). No result of this mission is known to have a machine-checked proof. The mission asks for the paper's proof, or any other proof, of the goal; for its refinement, Theorem 1.9; and for the closure and attachment lemmas on the way.
The obvious approach is to delete a low-degree vertex and induct, as in the classical proofs of Erdős–Gallai type bounds. It does not reach stability. Deleting a vertex can destroy 2-connectivity, and the extremal family changes with : the threshold moves with the minimum degree, and the new graph appears only for .
The edges inside are the hard part. A longest cycle gives no direct control over . The paper's route needs two non-trivial reductions:
After that, Lemma 4.2 is four pages of degree-sequence casework, and Lemma 4.4 is a ten-claim structural argument.
Vertices are Fin n and graphs are Mathlib SimpleGraphs. Further conventions:
⊑, a subgraph up to relabelling), and "" or "" is a graph isomorphism.Added hypothesis: in Theorems 1.7, 1.9, 4.1 and Lemma 4.4. As printed, the theorems claim every , but they fail at : a member of with is 2-connected, has circumference and edges, yet lies in neither nor . also divides by . Lemma 4.3 has no minimum-degree hypothesis and is stated for every .
Trivializations ruled out.
Infrastructure. A complete development needs:
All of these are reusable well beyond this mission, and contributions of any of them are welcome. Theorem 1.12 is also the goal of the companion mission on the stability of Bondy's theorem.
Online matching models a platform that must commit resources to requests as they arrive, without knowing the future. In revenue management the resources are items in limited supply and the requests are customers, and the firm also chooses the price. Ma and Simchi-Levi (arXiv:1905.04770, Oper. Res. 2020, DOI 10.1287/opre.2019.1957) give algorithms whose worst-case guarantee depends on the set of prices each item can be sold at, and show that the guarantee is tight.
Timeline of the deterministic (matching) case:
A firm sells items, one unit of each. Item has a price set with , and . Customers arrive one at a time. In the deterministic case, customer either would or would not buy item at price : . Let be the largest with , or if there is none. Assigning item to customer earns . An online algorithm sees only when customer arrives.
The benchmark is the LP (5): maximize subject to , and , with optimal value . Its dual (19) minimizes subject to and . An algorithm is -competitive if for every arrival sequence.
Booking limits. By Proposition 1 there are unique positive that sum to and satisfy
Set and . For let be the segment containing . The value function is
It increases continuously from to and equals at .
Multi-price Ranking (Algorithm 2). Each item draws an independent seed . Customer is assigned an available item maximizing , provided the maximum is strictly positive. Ties are broken arbitrarily. The analysis uses dual variables: when is assigned to , and ; all other dual variables are .
For every setup in the deterministic case with , every arrival sequence, every tie-breaking rule and every feasible of (5),
The theorem shows that one randomized rule achieves the optimal guarantee for every price set, and that the guarantee depends only on the price ratios. For one price, and the classical vertex-weighted result is recovered. With several prices the benchmark (5) is stronger, because the offline optimum may also choose prices, and the guarantee degrades gracefully: lies in and depends only on how far apart the prices are. Theorem 3 of the same paper shows that no online algorithm does better than when every item has price set , so the ratio is tight.
The results are proved in the paper, in §4 and App. C. As far as the platform's records show, they have not been formalized. A formalization adds three things on top of the paper. It machine-checks a randomized primal–dual argument whose expectations are integrals over . It makes precise the measure-zero conventions the paper uses: ties in (23), and at segment borders. It also gives a Lean model of a ranking algorithm with continuous seeds that sees only the present customer, which could be reused for related online algorithms.
The pointwise part (Lemma 2) is a direct computation from the booking-limit identity (7). The difficulty is Lemma 3. The constraint for a pair needs , but on a single sample path can be far below this: item may be taken by an earlier customer, or customer may take another item. The bound only holds after conditioning on the other seeds and comparing two coupled runs, one with item and one without. That comparison needs an invariant that holds at every step: the set of items still available in the run with contains the set in the run without . The invariant fails when ties are broken differently in the two runs, so the measure-zero set of ties must be handled explicitly. The conditional expectation of is then an integral of , which is discontinuous at the segment borders.
Fin n and customers Fin T, both 0-based. Prices are 1-based within an item, with pr r 0 = 0 for . Data at indices outside are never read.IsBookingLimits, unique by Proposition 1); on ; . Weak duality is stated for any and any inventories.Strategic open pit mine planning decides which parts of an ore body are excavated, in which period, and where each block of material is sent: to a processing plant, a stockpile or a waste dump. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research 68(5), 2020) state the problem as a mixed-integer program, the precedence-constrained production scheduling problem with clusters (PCPSP-C), which extends the formulation of Bienstock and Zuckerberg (IPCO 2010) to clusters of blocks that are extracted together. The integer versions of this program have large integrality gaps on production scheduling instances (§5, p. 1432), so the authors derive problem-specific cutting planes. This mission concerns the variable-right-hand-side (VRHS) production cuts of §5.2. They combine the precedence order of the clusters with the capacity of a single destination: if a solution sends many blocks to a capacitated destination, the predecessors of those blocks must be fully extracted.
The VRHS cuts are introduced first on a one-period, two-destination set, the mode-knapsack set MK (§5.2.1), and then generalised to the full multi-period clustered model (§5.2.2). Disaggregated formulations with destination choices go back to Boland et al. (Comput. Oper. Res. 2009); cutting planes for the precedence-constrained knapsack structure of open pit scheduling were studied by Bley et al. (Comput. Oper. Res. 2010).
All page references are journal pages of the published Operations Research article.
An instance has finite sets of blocks, of destinations and of clusters, the latter a partition of , and periods . Block lies in cluster and has weight . A precedence relation on blocks induces one on clusters ( if some block of precedes some block of ), assumed to be a strict partial order. The arc set is its transitive reduction: when is an immediate predecessor of . The reverse closure of a cluster is , the cluster and everything that requires it; for a set of clusters, .
Variables give the fraction of cluster extracted in period , and the fraction of block sent to destination in period . The constraints (2)–(7) of p. 1427 are
together with an integrality condition: full integrality (10), , defines the PCPSP-F, and partial integrality (11), " implies for ", defines the PCPSP-P. The general rows include the destination capacity rows (9), . The cuts use the cumulative variables (17).
The mode-knapsack set MK (p. 1433) fixes a DAG , weights and a capacity , and consists of the vectors with
Fix , and clusters with . Let , for , and , . For constants (), the inequality
is valid for the PCPSP-F, and, when (33), for the PCPSP-P. The goal is the conjunction of the two validity claims.
A valid inequality removes fractional points of the linear relaxation while keeping every feasible schedule. The VRHS cuts are among the production cuts that the paper evaluates in its computational study (§8), alongside the extraction cuts and the hourglass cuts. Their right-hand side is not a constant but a combination of extraction variables along a chain, which is what lets them couple the destination capacity with the precedence order; the paper's Theorem 5 shows the mechanism on MK, Theorem 7 in the full model. The partial integrality regime, under which the second half of Theorem 7 holds, is the one used by commercial mine planning software (p. 1427).
The results are proved in the paper by case analysis on the first index with . None of them has a machine-checked proof. Formalizing them makes explicit which rows of the formulation each cut uses (the destination capacity (9) and the integrality condition), and what role the coefficient condition (33) plays in the partially integral case.
The proof uses that partition and are disjoint from , which requires along the chain. It uses that for every , and that forces all strict successors of to be unextracted; both chain the constraints (4) and (11) along covering arcs of a finite strict order, since the formulation constrains only the arcs of , not all of . A natural first attempt, arguing directly from , therefore does not apply. The counting step needs , which is not a constraint of the formulation but follows from , and the nonemptiness of clusters. In the partial integrality case a fractional is possible, and the bound on the term must come from (33) rather than from integrality.
Blocks, destinations and clusters are finite types; periods are Fin T, index standing for period . An instance carries the block-to-cluster map, the block precedence, values, discount rate, weights, capacities and side rows . Cluster precedence is derived from block precedence; is its covering relation, and constraints (4) and (11) range over only. The chain is a function on read at with , and condition 1 of Theorem 7 is stated for consecutive pairs. In (32), is taken at the single period and is cumulative.
The standing assumptions of §2.1 are hypotheses of every PCPSP-C statement: clusters cover (so each is nonempty), is a strict partial order on clusters, , and . A cut "valid for the PCPSP-F (PCPSP-P)" is stated as: at every point feasible for the formulation with full (partial) integrality whose destination capacity rows (9) hold, the inequality holds. The capacity rows enter as an explicit hypothesis because the paper assumes they are among the rows of ; without them the cut is false. Validity is never asserted for the LP relaxation, where (29) and (32) fail, so the integrality condition cannot be dropped. Conditions 2 and 3 of Theorem 7 are kept as on the page, although the proof does not use condition 3. In MK, the DAG property, and are hypotheses; an arc means that extracting forces , and collects and the blocks from which is reachable.
The development needs only finite sums, finite sets and orders from Mathlib. Contributions are welcome on the chaining lemma for covering relations of finite strict orders, on the nonnegativity and monotonicity of , and on the partition of , which the goal and the milestones share.
Many learning and estimation problems are solved by a network of agents: each agent holds part of the data, can talk only to its neighbours, and wants to compute the minimizer of the average of all agents' objectives. Examples are sensor networks, multi-robot systems, and data-parallel training without a central server (Nedić and Ozdaglar 2009; Lian et al. 2017). In these settings the agents rarely know their exact gradients; they sample them, one data point or one mini-batch at a time.
Gradient tracking methods let each agent keep, next to its estimate of the minimizer, a running estimate of the network-average gradient. With exact gradients they converge linearly with a constant stepsize (Qu and Li 2018; Nedić, Olshevsky and Shi 2017), which plain distributed gradient descent does not. S. Pu and A. Nedić (Math. Program. 187 (2021) 409–457) analysed the same scheme when every gradient is replaced by an unbiased noisy sample, and called it DSGT (distributed stochastic gradient tracking). This mission formalizes their constant-stepsize result, Theorem 1.
There are agents. Agent holds a cost , and the agents seek
Each is -strongly convex with -Lipschitz gradient: and .
Noisy gradients. At time agent draws a random sample and observes , with and ; the samples are independent.
The network. Agents are coupled by a nonnegative doubly stochastic matrix (rows and columns sum to ), with exactly when and communicate, some , and a connected undirected communication graph. The number
the spectral norm, measures how fast one round of averaging brings the agents together.
DSGT. Each agent keeps and a tracker . Stacking them as rows of and writing for the matrix with rows , the method with constant stepsize is
started from a deterministic and . The two error measures are the distance of the average to and the consensus error .
Fix and a stepsize below the explicit threshold (7) of the paper (a minimum of three expressions in , , , , ). Then a certain explicit matrix has spectral radius , and with ,
The constants are the paper's, so the goal is stated with them.
Under a further stepsize condition (13), .
The milestones follow the paper's proof: the tracking identity (6); Lemma 1 on ; the one-step conditional estimates of Lemmas 2–4 and the auxiliary Lemmas 8–9; the linear system of inequalities (21) and its iterate (22); the determinant criterion Lemma 5; the bound under the relations (23)–(25); and the lower bound (27) on the auxiliary parameter .
The first term of the bound on , up to the factor , is the error of centralized stochastic gradient descent that averages samples per step; it does not depend on the network. The network enters only through terms of order . So for small stepsizes a decentralized method with gradient tracking pays nothing in the limiting error for having no central server. Theorem 1 is one of the standard references for this statement in decentralized stochastic optimization.
The result is proved in the paper, with constants. It has no machine-checked proof that we know of. Formalizing it produces a checked development of the linear-system method for distributed algorithms: conditional moment bounds for coupled stochastic recursions, a linear system of inequalities between expectations, and a Perron–Frobenius criterion for its stability. The same pattern recurs in the analysis of many gradient-tracking and variance-reduced decentralized methods.
The obvious argument would bound each error by itself, but the three quantities , and feed into one another, and none of them contracts on its own. The tracker error in particular depends on the next iterate, which itself depends on the current noise, so the cross terms do not vanish in conditional expectation and must be estimated separately (Lemmas 8 and 9).
Once the coupled system is set up, its stability needs the spectral radius of a nonnegative matrix whose entries depend on all constants at once, and the explicit limiting bounds need its inverse. The determinant criterion of Lemma 5 rests on Perron–Frobenius theory, which Mathlib provides only in part.
Stacked variables are Fin n → EuclideanSpace ℝ (Fin p). Every matrix norm is written out: (Frobenius), is the Frobenius norm of the matrix, and is the operator norm of on Euclidean . Spectral radii are taken over , so complex eigenvalues count. Expectations are Bochner integrals, and every bounded expectation comes with an integrability conclusion. "" is stated as "for every , eventually ". is the σ-algebra generated by , and conditional statements hold almost surely.
Standing assumptions and additions, all stated in the items:
The goal speaks only about the DSGT iterates, and the matrix ; it does not assume the linear system (21), or any estimate of the proof. The clause of Theorem 1 that approaches the limsup at the rate carries an unquantified constant and is not formalized: the paper's proof yields only the envelope (22) and the limit of its right-hand side, not a rate at which reaches the limsup; the envelope (22) is a milestone. Theorem 2 (diminishing stepsizes) is the subject of the second mission of the series.
A complete development needs conditional expectations of functions of independent samples, a Frobenius-norm calculus for stacked vectors, the consensus contraction of Lemma 1, and the Perron–Frobenius facts behind Lemma 5. The last two are reusable beyond this mission. Proofs of any milestone, and of the deterministic matrix lemmas in particular, are welcome independently.
Many problems in convex optimization, variational inequalities and saddle-point computation can be written as a monotone inclusion: find in a real Hilbert space with
where is a set-valued maximally monotone operator (a subdifferential, a normal cone, a constraint) and is a single-valued monotone operator (a gradient, or the skew operator of a saddle-point problem). Splitting methods solve such problems using and separately: a backward step evaluates the resolvent , and a forward step evaluates .
The classical forward-backward method converges when is cocoercive, but can fail when is merely monotone and Lipschitz, which is the case for saddle-point operators such as . Tseng's forward-backward-forward method (Tseng 2000) removes the cocoercivity assumption at the price of two evaluations of per iteration. Malitsky and Tam (arXiv:1808.04162; SIAM J. Optim. 30(2), 2020) propose the forward-reflected-backward method, which needs one evaluation of and one resolvent of per iteration, reusing the previous value of .
Timeline of the relevant results:
is a real Hilbert space with inner product . A set-valued operator is monotone if whenever , , and maximally monotone if its graph is not properly contained in the graph of another monotone operator. Its resolvent is, for and maximally monotone, an everywhere defined single-valued map, characterised by . A map is -Lipschitz if , and monotone if .
The zero set is . Given initial points and step sizes , the forward-reflected-backward method is
A sequence converges weakly to if for every ; a sequential weak cluster point is the weak limit of a subsequence.
If is maximally monotone, is monotone and -Lipschitz, , and for some , then every sequence generated by (13) satisfies
In attack order:
Corollary 2.6, the constant-step case , is included as a companion theorem.
Theorem 2.5 shows that monotone inclusions with a Lipschitz, non-cocoercive single-valued part can be solved by a splitting method with the per-iteration cost of forward-backward splitting: one forward and one backward evaluation. For saddle-point problems, where each evaluation of is a pair of matrix–vector products, this halves the operator cost of Tseng's method. The method contains the projected reflected gradient method and, for , Popov's method and the optimistic gradient method used in training generative adversarial networks (Remark 2.1). The analysis of this section is reused for the linear rate, the linesearch, the inertial variant and the three-operator variant of later sections (missions 2–5 of this series).
The theorem is proved in the paper. Formalizing it requires a machine-checked Opial-type lemma and a machine-checked demiclosedness argument for maximally monotone operators perturbed by a continuous monotone map, both reusable well beyond this mission. To our knowledge no machine-checked proof of convergence of the forward-reflected-backward method exists.
The energy inequality of Lemma 2.4 is algebra plus monotonicity and the Lipschitz estimate, and it yields boundedness and . The difficulty lies in passing from these facts to weak convergence of the whole sequence. Norm convergence is false in general, so a Cauchy-sequence argument is unavailable. The energy is not Fejér monotone in alone, because of the cross term , so the standard Fejér/Opial lemma does not apply directly. Identifying weak cluster points as zeros requires the weak-strong closedness of the graph of , which in turn rests on maximal monotonicity of the sum: this is not a consequence of monotonicity of the two parts, and the inclusion (25) can be passed to the limit only because the step sizes stay above .
The Lean development uses a real inner product space H (InnerProductSpace ℝ H), complete wherever the page needs it, and the published operator vocabulary ThreeOpSplitting.Accel.MonotoneOperators (monotone and maximally monotone set-valued operators, monotone and Lipschitz single-valued maps, resolvents). Conventions:
x j is and lam j is ; the initial points are arbitrary.Three formalizations would trivialize the goal and are excluded:
A complete development needs the Opial-type Lemma 2.2, which in turn needs weak sequential compactness of bounded sets in Hilbert space, and maximal monotonicity of for continuous monotone (Bauschke–Combettes, Corollaries 20.25 and 24.4(i)) with its demiclosedness (Proposition 20.33). These are general results of monotone operator theory, and contributions of them as separate theorems are welcome.
Mean field games describe Nash equilibria of large populations in which every player interacts with every other player symmetrically, through the empirical distribution of all states. Many systems of interest are not of this kind: agents in a network interact only with their neighbours, and the interaction structure is a graph rather than a complete graph. Understanding when equilibria on large graphs behave like mean field equilibria, and when they do not, requires models in which the equilibrium on a finite graph can be computed exactly.
Lacker and Soret (arXiv:2005.14102v2, Math. Oper. Res. 2022) introduced such a model: a linear–quadratic flocking game on an arbitrary finite graph, in which each player steers a Brownian particle and pays a terminal penalty for being far from the average of her neighbours. For vertex-transitive graphs they solved the game in closed form, up to a scalar ODE, with an equilibrium that depends on the graph only through the spectrum of its Laplacian. This mission formalizes that finite-graph result, Theorem 2.5 of the paper. Its large-graph consequences are the subject of missions II and III of this series.
Let be a finite simple graph on vertices , with adjacency matrix and degree matrix . When has no isolated vertices its random-walk Laplacian is
is transitive if for every two vertices there is a graph automorphism mapping to . A transitive graph is regular, so its Laplacian is symmetric, with eigenvalues in .
Fix a horizon , a noise level and a cost constant . Each vertex is a player with state
driven by independent Brownian motions , from a non-random initial state . A Markovian control is a Borel function of time and the full state vector with at most linear growth. Player minimises
A profile is a Markovian Nash equilibrium if no player can lower her cost by switching unilaterally to another Markovian control.
The equilibrium is built from
For a finite transitive graph without isolated vertices:
All four parts are in the goal statement.
The milestones follow the paper's proof in §2.2, §3 and §4.
The result. Theorem 2.5 is one of the few explicit Nash equilibria of a stochastic differential game on a non-complete graph. Two features of it are not visible in mean field theory. The equilibrium controls are nonlocal: each player reacts to the whole state vector, not only to her neighbours. The whole equilibrium (law, value, controls) depends on the graph only through the spectrum of . The second feature drives the paper's later results. Weak convergence of the eigenvalue distributions yields limits of the equilibrium, and these separate the dense regime, where the mean field approximation is valid, from the sparse regime, where it is not.
Formalizing it. The result is proved in the paper; nothing here is open. No machine-checked version of it or of its ingredients exists: the random-walk Laplacian of a graph, linear–quadratic stochastic differential games, verification theorems for Nash systems, and Gaussian laws of linear SDEs with time-dependent coefficients. The mission produces a checked statement of the equilibrium together with reusable layers: spectral facts about , an ODE analysis for , and a Riccati reduction for quadratic Nash systems.
Three steps resist a direct approach.
Lean conventions:
Fin n, so the paper's become . The state space is the platform's EthierKurtz.SDEState n (Euclidean ).multivariateGaussian.A formalization that fixes , restricts deviations to linear controls, drops the existence of the equilibrium state process, or replaces by is not this theorem.
Infrastructure that a complete development needs:
The spectral, ODE and Riccati layers are reusable beyond this mission. Proofs of individual milestones are welcome; so are general verification theorems for linear–quadratic games.
The spectral radius of a graph, the largest eigenvalue of its adjacency matrix, measures how densely and how unevenly the edges of the graph are distributed. Asking which graph in a class maximizes it is a spectral analogue of the extremal question "which graph in the class has the most edges". For planar graphs the question has a long history in spectral graph theory, going back at least to Schwenk and Wilson. It also arose in geography, where the spectral radius serves as a measure of the connectivity of planar networks. To compare real networks with a theoretical upper bound, geographers wanted the planar graph of maximum spectral radius (arXiv:1606.01916v2, p. 3).
Timeline, as recorded by Tait and Tobin (pp. 1–3):
All graphs are finite and simple. A graph on vertices has vertex set . Its adjacency matrix is the real matrix with entry in position when and otherwise. Its eigenvalues are real, and the largest is the spectral radius .
A graph is planar if it can be drawn in the plane with vertices as distinct points and edges as simple arcs joining their ends, such that an arc meets no vertex other than its ends and two arcs meet only at common ends.
For graphs and on disjoint vertex sets, the join is the graph on the union of the two vertex sets that keeps every edge of and of and adds every edge between a vertex of and a vertex of . Write for a single edge, for the path on vertices, and for their join: two adjacent vertices, both joined to every vertex of a path on the remaining vertices. The paper also writes it .
A planar graph on vertices is a planar spectral maximizer if for every planar graph on the same vertices.
The milestones refer to a leading eigenvector of a maximizer, scaled so that every entry is positive and the largest entry is , and to a vertex with . For a parameter they use the sets and , the edge counts (edges inside ) and (edges between and ), and a second vertex with that is adjacent to all but vertices of .
The threshold is not fixed. The paper proves the statement only for beyond an unspecified bound, and the conjecture's bound remains open. The equivalence encodes "the unique maximizer is ": every maximizer is isomorphic to it, and it is itself a maximizer.
The result. Theorem 15 settles the Boots–Royle / Cao–Vince conjecture for all large . It identifies the planar graph of maximum spectral radius exactly, so the theoretical upper bound that the geographic application asks for is . Along the way, Lemmas 8–14 describe the eigenvector of the extremal graph: two vertices carry almost all of the eigenvector weight, and every other entry is below . The same method proves the outerplanar analogue (Theorem 7, the companion mission of this series).
Formalizing it. The theorem is proved on paper and has no machine-checked proof. Formalizing it needs several pieces that are absent from Mathlib or the platform and are reusable: the edge bound and the bipartite bound for topologically planar graphs, the non-planarity of and and of their subdivisions, Rayleigh-quotient comparison of spectral radii, and the face structure of maximal planar graphs. Each milestone is a self-contained target.
Counting edges does not separate the candidates. A maximizer can be taken to be a maximal planar graph, so it has exactly edges. Every maximal planar graph on vertices has the same number of edges, and the standard lower bound is the same for all of them. The extremal graph is pinned down only through its eigenvector. One has to show that the weight concentrates on two vertices, which are then forced to be adjacent to each other (Lemma 13) and to every other vertex (Lemma 14). Lemma 13 is the step specific to planarity. It uses the triangular faces of a maximal planar graph to find an edge switch that keeps the graph planar. In the formal setting, planarity is topological, so every planarity fact of the argument (the edge counts, the and obstructions, the faces of a triangulation) has to be derived from the drawing.
SimpleGraph (Fin n). " is " is a graph isomorphism G ≃g bookPath n, where bookPath n lives on Fin 2 ⊕ Fin (n - 2). It is not an equality on a fixed labelling.WangKangXue.SpectralTuran.specRad, the largest eigenvalue of the real adjacency matrix.RobertsonSeymour1986.GM5.IsPlanar: a drawing by simple arcs. It is not replaced by /-minor-freeness or by an edge count, either of which would change the class the maximum ranges over.IsSpecMax IsPlanar G: is planar and for every planar on Fin n. Every milestone from Lemma 8 to Lemma 14 assumes it. These lemmas are false for an arbitrary planar graph, so a statement that drops the hypothesis, or replaces it by a property implying the conclusion, is not acceptable.IsSecondHub), with the constants and .Bibliographic data as given in the bibliography of Tait and Tobin (pp. 21–23).