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?
Online stochastic matching models display advertising and similar allocation problems in which requests arrive one at a time and must be served immediately. A bipartite graph links a set of advertisers to a set of impression types; requests arrive, each of a type drawn independently with , and each request must be assigned at once and irrevocably to an unmatched interested advertiser, or dropped. Performance is measured by the competitive ratio , where OPT is the maximum matching of the realized graph.
Without distributional knowledge the best possible ratio is (Karp, Vazirani and Vazirani, 1990). Knowing the type distribution allows more:
This mission concerns the analytic core of Theorem 3, the general-rates bound.
For an advertiser , let be the LP flow into . Its neighbours , which include a dummy advertiser with , are indexed by . For each neighbour, is the expected number of random lists , and is the neighbour's flow, so that . Write and .
Claim 2 of the paper introduces the functions
where is the probability that is matched through a list headed by . The per-advertiser bracket is
and the reduced function of three variables is
In Lean these are h, g, bracket f x y and R f β s in RandomListsMatching.GeneralRates.
For , any and reals with , and ,
The paper bounds below by (p. 15), so this inequality is the whole of what Theorem 3's numerical constant rests on.
The result. Theorem 3 gives for online stochastic matching with general (non-integral) arrival rates, improving the of Manshadi et al. The probabilistic half of its proof reduces matching probabilities to the closed forms and ; the paper then states that "in the remaining part of the section, we only use algebraic manipulations and the following properties of functions and ". That remaining part, posed here, is an exact real inequality, and it is where the constant is decided.
Formalizing it. The paper proves Claim 3 in one line ("can be easily verified by taking first and second order partial derivatives") and Claim 4 by a grid computation over cubes of side , with no recorded error analysis. A machine-checked proof replaces both. It also settles the regime of the constant: Claim 4 as printed, with the constraint "for ", is false, and the bound holds in the limit form stated here. None of these statements has a formal proof anywhere, to the extent of the search made for this mission.
The margin is small. The minimum of over the feasible region is about , attained near on the boundary ; the margin over is under . Any argument that loses a constant factor in the estimates of , or replaces by a rational bound that is not tight to five digits, fails. The bound is a three-variable statement with the minimum on a boundary face, so a one-variable monotonicity argument does not settle it.
The second difficulty is the function itself. Its two-case definition is continuous but the quotient form has a removable singularity at , which is exactly the end of the interval on which Claim 3 asserts convexity and concavity. Derivative computations that are routine away from the diagonal need care there.
The natural first idea for the goal, to apply Claim 4 directly to the bracket, does not type-check: the bracket depends on the whole family , and the reduction to three variables through the chord and cross-sum bounds is a separate step.
Real.exp 1, is Real.log 2, and is the exact rational (0.706 : ℝ).Fin k, and is allowed.MonotoneOn, AntitoneOn); convexity is ConvexOn ℝ (Set.Icc 0 y). The derivative in (5) is deriv (fun t => h y t) 0, the derivative in the second argument; the page's is a slip.A complete development needs the derivative calculus of on , including the diagonal, and certified interval bounds for and . The latter is reusable well beyond this mission. Proofs of Claim 3 or Claim 4 alone are welcome contributions.
A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. QCQPs contain max-cut, binary programming, the trust-region subproblem and many problems from signal processing and control, and are NP-hard in general. The standard convex approach is the Shor semidefinite relaxation, which lifts to the matrix and relaxes to an arbitrary positive semidefinite completion. Two questions decide how useful the relaxation is for a given QCQP: is its optimal value equal to the QCQP's (SDP exactness), and does its projected epigraph equal the convex hull of the QCQP's epigraph (convex hull exactness)?
A. L. Wang and F. Kılınç-Karzan (arXiv:1911.09195v3, Math. Program. 2021) give sufficient conditions for both, in terms of the faces of a dual set and a symmetry parameter , the quadratic eigenvalue multiplicity. Their Theorems 1 and 2 require to be polyhedral and on every semidefinite face . This mission formalizes §4.3 of the paper, which shows that neither hypothesis can be weakened on its own.
Timeline. Fujie and Kojima (1997) recorded the dual description of the SDP value used here. Ye and Zhang (2003) and Beck and Eldar (2006) gave sufficient conditions under which the trust-region subproblem with one additional quadratic inequality has a tight SDP relaxation; Locatelli (2016) gave an exactness condition for a variant of the trust-region subproblem, and Burer and Ye (2019) for diagonal QCQPs. Wang and Kılınç-Karzan (2020) unified these conditions through the facial structure of , and showed in their Propositions 2 and 3 that their own hypotheses are sharp.
A QCQP in variables with constraints, of them inequalities, is
with , . Its epigraph is . With and , the SDP relaxation minimizes subject to or and ; its value is , and is the set of for which some feasible has .
For write , and . The dual set is
Assumption 1: the QCQP is feasible and for some with on the inequalities. Assumption 2: is attained whenever it is finite. Assumption 3: is polyhedral. A face of is definite if some has , and semidefinite otherwise. The quadratic eigenvalue multiplicity is the largest such that every equals for some , .
The Lean development uses the same names: QCQP N m, Opt, OptSDP, D, DSDP, Gamma, bγ, qγ, Assumption1–Assumption3, IsSemidefiniteFace, IsQuadEigMult, affdim.
The milestones pin the paper's witness, the QCQP (13): .
There is a QCQP in variables with constraints satisfying Assumptions 1 and 2, with multiplicity and on every semidefinite face, but with . The companion items about its witness (14) state , , and .
The result. Theorems 1 and 2 of the paper are the general sufficient conditions behind many earlier exactness results for SDP relaxations. Propositions 2 and 3 show that the two hypotheses are each necessary in the sense that relaxing either one by the smallest possible amount produces a counterexample: lowering the multiplicity bound by one, or replacing polyhedrality by mere attainment of the dual supremum. Anyone trying to extend the theorems therefore has to change the form of the conditions, not just their constants.
Formalizing it. Both propositions are proved in the paper; none of this has been machine-checked. A formal proof requires Lemma 1, a strong-duality statement for a parametric SDP that is reusable across the whole paper, and explicit computations of faces, affine dimensions and multiplicities for two concrete families. The multiplicity claim in particular ("the largest ") is asserted but not argued on the page, and a formal proof must supply it.
The concrete computations for (13) and (14) are elementary in isolation; the work lies in three places. First, Lemma 1 is a conic duality statement, including attainment of the outer minimum, that depends on Assumption 1; it is the bridge from the SDP to the dual set, and Mathlib has no semidefinite duality theory to build on. Second, the face structure: one must show that the hyperplane is the only semidefinite face of the halfspace of (13), and that every face of the disk of (14) gives a single point . Third, "the multiplicity is " requires ruling out every larger block structure , not only exhibiting one of size . A naive witness with only shown would establish a lower bound on the multiplicity, which is not the statement.
Points of are Fin N → ℝ; the paper's constraint is index of Fin m, and constraint is an inequality exactly when its index is below mI. and are infima in EReal, so infeasible and unbounded programs take the values rather than a junk real. A supremum bound is written as for every . Faces are nonempty convex extreme subsets of . The quadratic eigenvalue multiplicity is the greatest admitting a block form, under the identification of block , entry with coordinate . Proposition 3 says " variables"; the construction lives in , so the formal statement uses .
The goal is existential, as on the page, and a solver may exhibit any witness; it cannot be met trivially, because the multiplicity must equal exactly, the dimensions , are fixed by the type, and both and are required.
The QCQP (13) is given in full: the page states only the matrices , and the linear terms encode the constraints as . Lemma 1 is the reusable piece, and proofs of it are welcome independently of this mission; so are general lemmas on faces of halfspaces and balls and on Kronecker block structure.
A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. QCQPs model trust-region subproblems, max-cut and other binary programs, phase retrieval, and many problems in signal processing and control; in general they are NP-hard. The standard tool for bounding and solving them is the Shor semidefinite relaxation (Shor 1990), which lifts the variable to a matrix and replaces every quadratic term by a linear function of . The relaxation is a convex program, so it can be solved efficiently, but it is only useful when one knows that it is tight: that its optimal value equals that of the QCQP, or, more strongly, that it describes the convex hull of the QCQP's epigraph.
Wang and Kılınç-Karzan (arXiv:1911.09195v3, Math. Program. 2021) give sufficient conditions for tightness. Section 6 of the paper concerns QCQPs with symmetry: when every quadratic form is identical copies of one smaller form, . Such problems arise as quadratic matrix programs in the sense of Beck 2007, where the variable is a matrix and the objective and constraints are traces of quadratic matrix expressions. Beck showed (Corollary 4.4) that gives value exactness under a regularity assumption; Theorem 7 of the paper gives the convex-hull result for ; this mission's Theorem 8 covers .
Fix variables and constraints. For let with symmetric, , . The QCQP is
and its epigraph is .
With , the SDP relaxation has value
and its projected epigraph is the set of for which some satisfies the constraints with . Always and .
For write and , and let . Assumption 1 requires that the QCQP be feasible and that some with on the inequalities have .
The quadratic eigenvalue multiplicity (Definition 3) is the largest integer such that and every , , equals for some . Finally,
is the hyperplane on which the SDP relaxation attains its value.
Under Assumption 1, if , then
Theorem 8 says that one copy of symmetry fewer than Theorem 7 requires still makes the SDP relaxation exact in value, and identifies the relaxation's optimal set: every optimal point of the relaxation, projected to , is a convex combination of optimal epigraph points of the QCQP. In particular the relaxation's optimal points can be decomposed into QCQP optima, which is what makes the relaxation a solution method and not only a bound. Remark 14 of the paper places the result between Beck's (only ) and Theorem 7's (the full convex hull), and records the conjecture that all three thresholds are sharp.
The theorem is proved in the paper (Appendix B). No machine-checked proof of it, or of the multiplicity results of Section 6, is known to exist. A formal proof needs a Lean development of the Shor relaxation, its Lagrangian dual, conic strong duality with dual attainment for an SDP with sign-constrained multipliers, and the Kronecker structure of the data.
The inclusion is routine. The converse needs, for an SDP-optimal point, a decomposition into feasible QCQP points that are themselves optimal. A rank-one decomposition of the SDP matrix does not suffice in general: its terms leave the feasible set unless the perturbation directions are orthogonal to all the linear parts , including the objective's. With multiplicity there is room for all orthogonality conditions; with only the constraint conditions can be imposed, and the objective condition has to come from elsewhere. The difficulty sits in that last condition and in the conic duality step, whose dual must attain its value under Assumption 1 alone (no polyhedrality of , no attainment assumption).
The Lean development lives in the namespace QCQPTightness.MultTight. The data are a structure QCQP N m with symmetric , constraints indexed by Fin m, and constraint i an inequality exactly when (i : ℕ) < mI (the paper's inequalities come first). Vectors are Fin N → ℝ; points of are pairs (x, t). and are infima in EReal, and is defined from that EReal value; this is why the goal states as a separate conjunct: if were , would be empty and the first conjunct trivial. is (Q * Y).trace; is PosSemidef; is y ⬝ᵥ y = 1. The identification sends block , entry to coordinate s + n * j.
Standing assumptions: the goal carries (p. 1) and Assumption 1. The multiplicity is the largest (IsGreatest), as on the page. The milestones take an explicit representation instead, which makes them apply to every representation, and drop and Assumption 1 where the step does not use them. The rank-induction milestone carries , which the page's sentence omits but its proof uses ("by minimality of "); without it the claim is false.
A trivializing formalization would assume system (19), or the vanishing of , in the goal; the goal assumes neither, and both are milestones to be proved.
Reusable infrastructure: the QCQP and Shor-relaxation definitions are shared with the other missions of this series, and a general SDP strong-duality statement exists on the platform (ConvexOptimization.sdp_strong_duality) in a different form (a minimization without sign-constrained variables). Contributions welcome: proofs of the milestones, a conic duality lemma with sign-constrained multipliers, and Kronecker-product lemmas such as .
The Frank-Wolfe algorithm (also called the conditional gradient method) minimizes a smooth convex function over a compact convex set using only a linear minimization oracle in place of a projection. Each step solves a linearized problem over the feasible set and moves toward its solution. This makes it the method of choice when projections are expensive but linear subproblems are cheap or have closed-form solutions: nuclear-norm balls, polytopes, and the semidefinite feasible sets that come up in distributionally robust estimation.
Nguyen, Shafieezadeh-Abadeh, Kuhn and Mohajerin Esfahani (arXiv:1911.03539v2, Math. Oper. Res. 48(1), 2023) need such a method for a nonlinear semidefinite program that computes Wasserstein minimax mean square error estimators. Its feasible set is not strongly convex in the traditional sense, and the linear subproblems can only be solved approximately. Section 6.1 of the paper analyses a fully adaptive Frank-Wolfe algorithm under these conditions: it uses an inexact oracle, a backtracking estimate of the smoothness constant, and a weakened, gradient-dependent notion of strong convexity of the feasible set. The section proves a linear convergence rate. This mission formalizes that rate and the lemmas of its proof.
Timeline. Frank and Wolfe (1956) introduced the method for quadratic programs. Levitin and Polyak (1966) proved linear convergence over strongly convex sets when the gradient is bounded away from zero, with the adaptive stepsize (6.4); Garber and Hazan (2015) revisited this regime. Pedregosa, Négiar, Askari and Jaggi (2020) introduced the backtracking line search with adaptive smoothness parameters β_t used here, and proved its sublinear rate. Section 6.1 combines that line search with inexact oracles and blockwise strong convexity with respect to .
The decision variable is with blocks , and carries the Euclidean norm . The problem is
where is a product of convex compact sets and is convex and differentiable on . The partial gradient with respect to block is .
An inexact oracle with precision is a map with
For it returns an exact solution of the linearized problem. At a point the search direction is and the surrogate duality gap is .
Assumption 6.1 consists of three conditions:
Algorithm 1 starts from with parameters , and . At iteration it sets and . It then picks as the smallest element of that passes the sufficient-decrease test
and moves to with that stepsize .
With , every run of Algorithm 1 satisfies
In the order the proof uses them:
The result. Theorem 6.2 gives a linear rate for a Frank-Wolfe method that never needs the global smoothness constant , that tolerates approximate linear subproblems, and that works on feasible sets which are strongly convex only in the weak, gradient-dependent sense of Assumption 6.1 (ii). In the paper it justifies the algorithm used to compute Nash equilibria of Wasserstein minimax MMSE estimation problems at dimensions where interior-point SDP solvers run out of memory. The analysis is generic and applies to any problem meeting Assumption 6.1.
Formalizing it. The result is proved in the paper, but the printed constant is wrong. In Lemma 6.3 (ii) the factor is maximized at , where it equals ; the page drops the square. Lemma 6.3 (ii), (6.12) and Theorem 6.2 are therefore false as printed for . A two-dimensional instance (unit disk, linear objective, ) violates the printed rate after one step. The printed and corrected rates agree for an exact oracle (). The mission states the corrected constant throughout and quotes the printed text in the milestones. No machine-checked proof of a linear rate for Frank-Wolfe with adaptive line search is known to us.
The obvious argument, "β-smoothness plus a contraction per step", does not go through directly. The line search may pick far below , so the contraction factor in case (ii) is controlled by and needs the separate fact that never exceeds . That fact depends on being the smallest accepted trial value, and it fails for an arbitrary accepted one. The lower bound of Lemma 6.3 (ii) comes from testing the oracle inequality against a point built from Assumption 6.1 (ii). That point is assembled block by block, and the step back to uses the Euclidean (not the sup) norm on the product space. The constant then comes from an explicit one-variable optimization, which is where the printed proof errs.
The space is PiLp 2 (fun k : Fin K => EuclideanSpace ℝ (Fin (d k))), so ‖·‖ is Euclidean and is the block gradient f s k. Conventions:
Disclosed changes relative to the page:
Trivializing readings are excluded. A sorry-free companion file exhibits, for every , an instance (interval , linear objective, exact oracle) satisfying every hypothesis of the goal, together with an explicit infinite run whose initial suboptimality is positive. The run predicate forces the smallest accepted , and the norm is Euclidean.
Everything needed is in Mathlib: gradients in Hilbert spaces, convexity, PiLp. The descent lemma along a segment for a function with Lipschitz gradient on a convex set, used for (6.9), is reusable beyond this mission. Contributions welcome: proofs of the milestones, and a Lean proof that the printed constant fails on the disk instance.
The alternating direction method of multipliers (ADMM) solves problems of the form subject to . Themelis and Patrinos (arXiv:1709.05747v4, SIAM J. Optim. 30(1):149–181, 2020) show that, for nonconvex and , ADMM is the Douglas–Rachford splitting method applied to a reformulated problem whose second term is the image function , . Their convergence theory for DRS requires the nonsmooth term to be proper and lower semicontinuous (Assumption IIa4), so whether inherits lower semicontinuity from decides whether the theory applies to a given ADMM instance.
Image functions, also called epi-compositions or infimal post-compositions, are classical objects of variational analysis (Rockafellar and Wets, Variational Analysis; Bauschke and Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces; Auslender and Teboulle, Asymptotic Cones and Functions). For convex the question of when is closed has a long history through recession functions; Section 5.4.1 of the paper gives a characterization that needs no convexity.
Let . For the domain is ; is lower semicontinuous (lsc) if its epigraph is closed, and level bounded if every set , , is bounded.
Fix a matrix . The image function of under (Definition 5.1) is
with values in . Its domain is : outside that set the infimum is over values only.
Condition (5.5) at a point compares the best value of on the affine fibre with the values of far away along directions that nearly annihilates:
The right side equals .
For every lsc and every ,
Theorem 5.11 turns Assumption IIa4, a property of a derived function, into a checkable condition on and . Its level-bounded corollary covers every lsc with bounded sublevel sets, and the characterization explains why the pathological example (5.4) of the paper, in which is even , fails: a minimizing sequence on the fibre escapes to infinity while applied to it converges. Combined with the convergence theorem for ADMM in the same paper (Theorem 5.6), this identifies the ADMM instances to which the tight DRS stepsize theory applies.
The theorem is proved in the paper. As far as is known, no machine-checked proof of it, or of any closedness criterion for image functions, exists in Lean or in Mathlib. A formalization fixes the exact range of the equivalence, which the printed statement gets wrong (see Formalization scope), and supplies reusable infrastructure: the image function in EReal, and liminfs along the filter ", ".
Lower semicontinuity of at asks that values of on fibres , , not drop below . The natural argument picks near-minimizers on these fibres and passes to a limit; this works only when the stay bounded, and nothing in lsc of alone prevents them from escaping to infinity. The difficulty is to account exactly for the unbounded case, which must be compared with the fibre through by a translation , and that requires a point with . The converse requires turning a failure of (5.5), stated as a filter liminf, into a sequence witnessing the failure of lower semicontinuity.
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin p); is a continuous linear map between them. Every dimension, including , is allowed.EReal, and is assumed never to take the value . The image function is the EReal infimum , which may be and is off . Properness of is not assumed in the goal: if both sides hold.LowerSemicontinuousAt, the neighbourhood form of the page's sequential level-set criterion.Nesterov's accelerated gradient method for smooth convex functions, called NAG-C in the source paper, minimizes an -smooth convex function with function values decreasing at the rate . That rate is optimal among first-order methods (Nesterov, 1983). A line of work starting with Su, Boyd & Candès (2016) studies such methods through ordinary differential equations obtained in the limit of vanishing step size. Their low-resolution ODE reproduces the function-value rate. The same ODE also models the heavy-ball method, so it cannot explain why Nesterov's method behaves differently from heavy-ball.
Shi, Du, Jordan & Su (arXiv:1810.08907v3) keep the terms of the limit, where is the step size. The resulting high-resolution ODEs contain a gradient-correction term , which is absent from the heavy-ball ODE. This mission formalizes the paper's analysis of the high-resolution ODE of NAG-C (Section 4.1, pp. 21–24). Along this ODE the smallest squared gradient norm up to time decays like , while the low-resolution ODE gives only . Small gradients are the natural stopping criterion in practice and the natural target in nonconvex and dual problems, which is why the squared gradient norm is studied separately from function values (Nesterov, 2012).
Let have gradient and Hessian . For , the class consists of the differentiable with
The class is its subclass of twice continuously differentiable functions whose Hessian is Lipschitz continuous. A minimizer of is fixed.
Given a step size , put . The high-resolution ODE of NAG-C (1.12) is
with and . The analysis uses the Lyapunov function (4.1)
With it reduces to the Lyapunov function of Su, Boyd and Candès.
For every , every step size , and every solution of (1.12),
With this is . The infimum cannot be dropped, because the gradient norm need not decrease along the trajectory.
A companion item states Corollary 4.2 (p. 24): for .
Theorem 5 is the continuous-time model of the paper's Theorem 6, which shows that NAG-C itself, without modification, drives to zero at the rate . Combining the function-value rate with gives only . Previously known rates required modified methods (Ghadimi & Lan, 2016). The proof attributes the improvement to the gradient-correction term: the factor in Lemma 4.1 comes from the term in (4.1), which exists only because of the Hessian term in (1.12). The authors conjecture that the low-resolution ODE does not achieve the rate (p. 23).
The results of Section 4.1 are proved in the paper; no machine-checked version of them is known. Formalizing them produces a checked Lyapunov analysis of a second-order ODE with Hessian damping and explicit constants. It also gives a template that the discrete analysis of NAG-C (a separate mission in this series) mirrors step by step. Related Hessian-damped systems are analysed in Attouch, Chbani, Fadili & Riahi (2020), with qualitative integrability conclusions instead of an explicit bound on the infimum.
The obvious route goes through the function-value rate and the inequality . It loses a factor of and yields only . The cubic rate needs a Lyapunov function whose derivative contains a term proportional to . Proving the derivative identity requires differentiating through the chain rule with the Hessian, and then cancelling that derivative against the gradient-correction term of the ODE. The derivative bound also uses the co-coercivity inequality of -smooth convex functions. The remaining steps are measure-theoretic: integrate a one-sided derivative bound on , and compare an infimum with a weighted average.
EuclideanSpace ℝ (Fin n), is Mathlib's gradient, and is the Fréchet derivative of the gradient map applied to .Ruled out. A formalization would hold for junk reasons in any of these cases: the infimum is written as a bounded infimum over all reals (in Lean this is ); the velocity is not tied to ; the goal is stated at (where Lean divides by ); or derivatives are written with deriv, which is where a function is not differentiable. The statements here avoid all of these.
Infrastructure. A complete development needs:
The co-coercivity inequality and the interval-integral comparison are reusable beyond this mission. Proofs of the milestones in any order are welcome, as are independent proofs of the goal.
Douglas–Rachford splitting (DRS) minimizes a sum by alternating the proximal mappings of the two terms. It goes back to the alternating-direction schemes for heat conduction of Douglas and Rachford (1956), was cast as a splitting method for monotone operators by Lions and Mercier (1979), and through its dual form, the alternating direction method of multipliers (ADMM), it is a workhorse of signal processing, statistics and distributed optimization. For convex problems its convergence theory is complete. In applications, however, DRS and ADMM are routinely run on nonconvex problems (sparse regression with nonconvex penalties, phase retrieval, feasibility problems with nonconvex sets), and there the classical theory says nothing.
Timeline. Li and Pong (2016) proved subsequential convergence of DRS with for a smooth with Lipschitz gradient, for a sufficiently small stepsize, using the augmented Lagrangian as a merit function, and showed that cluster points are stationary. Li, Liu and Pong (Comput. Optim. Appl. 68(2), 2017) treated the Peaceman–Rachford case with a modified merit function and proved boundedness of the iterates for level-bounded . Themelis and Patrinos (arXiv:1709.05747, SIAM J. Optim. 2020) obtained convergence for every relaxation , and beyond for strongly convex , under stepsize bounds that they show to be tight. This mission formalizes that convergence result.
Let carry the Euclidean inner product and norm , and let . A function is proper if it is finite somewhere, and level bounded if every sublevel set , , is bounded. A differentiable is -smooth if , and -hypoconvex if is convex; may be negative.
Assumption I. is -smooth and -hypoconvex with ; is proper and lower semicontinuous; and has a minimizer.
The proximal mapping of with stepsize is the set
A DRS run with stepsize and relaxation is a sequence with
The Douglas–Rachford envelope (DRE) is
With , and , the admissible parameters are: with ; or, when , with .
Under Assumption I and admissible , every DRS run from any satisfies
In attack order: the lower bounds for smooth hypoconvex functions (Theorem 2.2); single-valuedness and Lipschitz properties of (Proposition 2.3(i), (ii)); real-valuedness and strict continuity of the DRE (Proposition 3.2); the sandwich (Proposition 3.3); and the equivalence of level boundedness (Theorem 3.4(i), (iii)); and the sufficient decrease
(Theorem 4.1). Two companion items: Remark 3.1 (, prox-bounded with threshold at least , and DRS runs exist from every when ) and the stationarity measure of Theorem 4.3(ii), .
The result gives convergence guarantees for DRS with any relaxation parameter on nonconvex problems where only is required to be smooth, with stepsizes up to when is convex. The companion mission on tightness (Theorem 4.7 of the paper) shows that DRS can fail to converge for , so these ranges cannot be enlarged under Assumption I. Through the equivalence of DRS and ADMM (§5 of the paper, a later mission of this series), the same conclusions transfer to nonconvex ADMM with a tight penalty bound.
The paper's proofs are complete, so the remaining work is formalization. As far as the platform's records show, no machine-checked proof of convergence of nonconvex DRS exists: the published DRS items cover the convex, monotone-operator setting only. The development also produces reusable pieces: the lower bounds for hypoconvex smooth functions, the proximal calculus of smooth functions, and the Douglas–Rachford envelope as a Lyapunov function.
In the convex case DRS is a fixed-point iteration of an averaged operator, and convergence follows from Fejér monotonicity. For nonconvex the reflected proximal maps are not nonexpansive, so this argument has no starting point. Convergence must instead come from a merit function that decreases along the iterates, and the difficulty is to find one whose decrease survives every relaxation with stepsizes all the way up to . Small-stepsize decrease estimates for do not extend to the full range. Cluster points must then be shown stationary for a lower semicontinuous, possibly nonconvex , which needs the outer semicontinuity of its proximal mapping rather than any continuity.
Points are EuclideanSpace ℝ (Fin p); every dimension , including , is allowed. is real-valued and , and are EReal-valued and never . The proximal mapping is a set, and runs are selections from it; no proximal function is chosen. The DRE is the EReal infimum of the expression above over , which is the page's value because that set is a singleton for . Stationarity is in the regular (Fréchet) subdifferential, the published platform definition NonconvexSplitting.Shared.IsRegularSubgrad; this is what the proof gives and is stronger than limiting stationarity. Cluster points are MapClusterPt points, and the rate is . All reciprocal bounds are multiplied out (, ), respecting the paper's convention .
Standing assumptions are Assumption I plus , which is added because the ranges use ; for , is affine. Three printed statements are corrected:
The goal does not mention these constants. Its hypotheses are exactly Assumption I with , , the admissible ranges, and a DRS run. The goal assumes no decrease of the envelope, no square-summability, no boundedness of the iterates, and no residual . The companion Remark 3.1 shows that runs exist, so the goal is not vacuous.
A complete development needs the regular subdifferential calculus for a smooth plus lower semicontinuous sum, the proximal optimality condition , existence of proximal points for prox-bounded lsc functions, and the outer semicontinuity of the proximal mapping. All of these are reusable beyond this mission. Contributions to any milestone, or to these general lemmas as separate theorems, are welcome.
The Conley–Zehnder index assigns an integer to a path of symplectic matrices that starts at the identity and ends at a matrix without eigenvalue . It is how periodic orbits of Hamiltonian and Reeb flows get graded. In Floer homology it gives the grading of the chain complex, generated by the -periodic orbits of a nondegenerate Hamiltonian (Salamon–Zehnder 1992; Salamon 1999). In contact homology and symplectic field theory it grades Reeb orbits. In the analysis of pseudoholomorphic curves it enters the Fredholm index formula for the linearized Cauchy–Riemann operator through the asymptotic orbits. In three-dimensional Reeb dynamics it defines dynamical convexity (every periodic orbit has index at least ), the hypothesis of the Hofer–Wysocki–Zehnder theorem on disk-like global surfaces of section (HWZ 1998).
Timeline. Conley and Zehnder introduced the index in their Morse-type index theory for periodic solutions of Hamiltonian equations (Conley–Zehnder 1984). Salamon and Zehnder gave the definition through a rotation function and related it to the Maslov index (SZ92). Robbin and Salamon extended it to arbitrary paths as a half-integer Maslov-type index (Robbin–Salamon 1993). Gutt attributes the properties naturality, homotopy, zero, product, loop, signature, determinant and inverse, and the characterization of the index by homotopy, loop and signature alone, to Salamon's lecture notes (Sal99) and to Audin–Damian (AD14); the statements used here are those of Gutt, Propositions 8–9. Gutt gives a self-contained account with several equivalent formulas, including the normalized complex determinant of the complex-linear part used below (Gutt 2014, §2).
Write with coordinates and let
The symplectic group is the set of real matrices with . Let be the set of with .
is the set of continuous paths with and . It carries the compact-open topology.
For , the complex-linear part is . It commutes with , so it has the block form , which is the complex matrix once is identified with by . Set
Let and . Each extends to a path with on , for , and . The map is then a loop in , and
For a loop with , the Maslov index is . For a symmetric matrix , is the number of positive eigenvalues minus the number of negative eigenvalues.
The map has the following three properties, and every map with these properties equals :
The result. The characterization makes the index a canonical invariant: any construction of an integer invariant of nondegenerate symplectic paths that is homotopy invariant and has the correct loop and signature behaviour is the Conley–Zehnder index. In practice this is how different definitions in the literature are identified with one another (rotation function, polar decomposition, complex-linear part, crossing forms, spectral flow of asymptotic operators). The listed properties are used directly to compute indices of concrete orbits, for instance the iterates of orbits of ellipsoids and the orbits of convex energy surfaces.
Formalizing it. All results here are classical and proved. No formalization of the Conley–Zehnder index exists in Mathlib. This mission produces a reusable library for symplectic linear algebra in Lean: the index and the Maslov index of loops as functions on path spaces, together with their computational properties. It is the first stage of a formalization of the Fredholm theory of linearized Cauchy–Riemann operators, whose index formula is stated in terms of Conley–Zehnder indices. It also gives a general-dimension definition against which the two-dimensional winding-interval definitions used in existing dynamical-convexity statements can be compared.
The index is defined through a choice: an extension of the path to inside and a continuous argument of a circle-valued map. Before any property can be stated as a property of a function, the result must be shown independent of these choices. That is not a local computation: it depends on the global topology of the symplectic group and on how the set of matrices with eigenvalue sits inside it.
The properties themselves are statements about the degree of maps into built from determinants, and is not a homomorphism. So none of the properties follows from a calculation on a single matrix, and loop and product require control of degrees under pointwise products and block sums. The uniqueness statement quantifies over all integer-valued functions on a path space. The argument for it has to use only the three listed properties and the topology of .
ConleyZehnder; all definitions are in ConleyZehnder_Setting.Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℝ. is Mathlib's Matrix.J, and is Matrix.symplecticGroup. Paths are C(unitInterval, Mat n) with the compact-open topology. is a Set of such paths, and "connected component" means connectedComponentIn (SP n).C(unitInterval, Mat n). Every property constrains only on , and the paths , , , and are passed as continuous maps with the stated pointwise values.IsArgLift f θ means . IsCZValue ψ k says that some extension and some lifts give , where is the part of the extension after . czIndex and maslovIndex are defined by choice from these predicates, with fallback value . Milestones 2 and 3 are what make the fallback unreachable. Without them, any property proved for czIndex would say nothing about the actual index.Matrix.IsHermitian.eigenvalues; for real matrices, Hermitian means symmetric. The norm bound is stated as for every eigenvalue . The signature property is stated as .Contributions welcome: general lemmas on degrees of maps (existence and uniqueness of lifts, additivity under products and concatenation, homotopy invariance), and the topology of and . These are reusable well beyond this mission.
S. David Promislow, Fundamentals of Actuarial Mathematics (third edition, 2015), Chapter 22, Section 22.5.3, Definition 22.5 and equation (22.9), PDF pages 439–442, defines tail value-at-risk using the value-at-risk quantile plus the stop-loss expected excess divided by one minus confidence. The textbook demonstrates the error in conditioning only on losses strictly greater than, or greater than or equal to, a discrete VaR when the quantile contains an atom. Its two-coin example has losses 0, 1, 1, 2 with equal joint probabilities: and . The present mission provides an exact finite integer-lattice formalisation of that convention.
Let aggregate loss be integer valued on with nonnegative masses , usually summing to one. Choose confidence and an integer quantile . The strict tail above the quantile is
The worst fraction of outcomes includes every loss strictly larger than q, then only enough outcomes at q to complete the required probability. Write that selected quantile-point mass as
For this selection to be feasible, q must be an appropriate upper quantile, captured by
The inequalities are explicit formal hypotheses. An arbitrary q need not be a valid VaR for the given confidence, even though the algebraic TVaR expression remains defined by the source.
The expected monetary loss across the worst probability mass is
Consequently, the correct tie-adjusted tail average is
The related net stop-loss transform is
A finite reorganisation yields the fundamental actuarial formula
The term at the VaR atom contributes q times just the required fraction, not q times every atom observation. For the two-coin loss distribution , q=1 and , the strict tail is 1/4 and the selected mass at the quantile is 1/4. The numerator is , so TVaR equals 3/2. The alternatives and are not the correct tie-adjusted TVaR at this confidence.
Under nonnegative probability coefficients and positive tail probability, the stop-loss premium is nonnegative and therefore . When , the stop-loss transform is zero and TVaR equals B, provided the quantile is selected consistently.
Five definitions represent strict tail probability, net stop-loss excess expectation, selected quantile atom, selected tail monetary numerator and its normalised TVaR. Twelve supporting theorem targets establish strict-tail and excess nonnegativity, terminal bounds, atom feasibility, exact tail coverage, tail numerator algebra, the stop-loss TVaR identity, the quantile lower bound and an explicit discrete two-coin counterexample to naive conditional-tail averaging. The thirteenth target combines feasible atom allocation, TVaR/stop-loss equality and .
An independent exact-rational suite checked 84 finite claim-grid/confidence combinations, including confidence zero and near one, integer quantile boundaries, strict loss tail and selected quantile-atom fractions.
This is a finite-support discrete loss theorem and does not silently assert continuous-tail integration, arbitrary infinite-support convergence or a general proof of coherent-risk-measure subadditivity. Its connection to the bounded stop-loss mission XXVIII is mathematical only; imports of that unpublished Draft are not permitted.
S. David Promislow, Fundamentals of Actuarial Mathematics (third edition, 2015), Chapter 24, Sections 24.5.2 and 24.5.3, PDF pages 489–491, derives Bühlmann least-squares credibility and extends it to unequal period exposure using the Bühlmann–Straub model. Relevant equations are (24.13)–(24.16), and the weighted generalisation on printed page 464. A complementary openly accessible reference is Loss Data Analytics, Chapter 12, Experience Rating Using Credibility Theory, https://openacttexts.github.io/LDAVer2/ChapCredibility.html.
The book's narrative contains an apparent transposition in one terminology sentence about v and w, but its mathematical definitions and formulas consistently identify as the expected process variance and as variance of hypothetical means. This mission uses those mathematical definitions, not the reversed labels.
Let denote the underlying class of a policyholder. The collective mean risk is . Let
EPV describes claim variability within a risk, whereas VHM describes the persistent difference in expected claims between risks. If observations across periods are conditionally independent given , and period has exposure volume , a Bühlmann–Straub period mean has conditional process variance proportional to .
For n periods of observed per-unit claims , define positive total exposure and the weighted experience mean by
The least-squares credibility factor is
This is equivalent to if and , but the displayed formula also covers with positive EPV. The denominator must be strictly positive; if both variance components vanish then every credibility weight produces the same prediction-error objective, so a unique ratio must not be asserted.
The resulting credibility premium per unit exposure is
The usual risk-type prediction objective is a mean-squared error of estimating the hypothetical risk mean. Under the conditional variance and independence assumptions its quadratic part is
For positive exposure, multiplication by P does not change its minimiser. To avoid introducing division by zero into the Lean source, define the algebraically equivalent scaled risk
With nonnegative P, EPV and VHM and strictly positive sum , completing the square gives
Thus , for any real z, and the optimiser is unique since D is strictly positive. When VHM=0 and EPV>0, Z=0 and the premium is fully collective. When EPV=0 with P·VHM>0, Z=1 and the premium uses individual experience.
Promislow's printed Example 24.8 uses group exposure volumes 40, 25 and 35 and aggregate period claim totals 4,000, 2,000 and 2,500. The weighted per-person experience is . With collective mean 100, EPV 125 and VHM 5, the experience credibility is
The original example then multiplies 88 by a forecast next-period exposure of 45 to obtain expected aggregate claims 3,960. The Lean mission targets the per-unit credibility estimator, not a blanket rule that every future exposure must equal 45.
Five source definitions represent finite total exposure, weighted observations, optimal weight, credibility premium and exposure-scaled MSE. Fourteen supporting theorem targets establish exposure summation, weighted constant observations, factor bounds and boundaries, premium identities, square completion, minimum and uniqueness. The fifteenth target combines admissibility and global least-squares optimality.
An independent exact-rational check verified 609 combinations of exposure, EPV, VHM and proposed credibility factors. It checked the completed-square equality, bounded optimal factor, global minimality and uniqueness for nonzero denominators, and reproduced Example 24.8.
A general Bayesian posterior mean is not always linear in observed experience. This mission proves optimality among affine credibility estimators under the stated covariance model, rather than asserting universal posterior-mean exactness. The formal risk quadratic encodes the variance decomposition and does not itself formalise an arbitrary latent stochastic probability space.
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.
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.
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.
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.