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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
The stochastic linear quadratic (LQ) optimal control problem asks to steer a linear stochastic differential equation by a control so as to minimize a quadratic cost. It is the basic model of stochastic control: Wonham studied it in 1968 (Wonham 1968), and it is the model on which feedback design, mean-field control and LQ differential games are built (Yong–Zhou 1999).
Classically the cost weights are assumed nonnegative and the control weight uniformly positive definite, the standard conditions (1.4). Under them the Riccati equation has a unique solution and the optimal control is a linear state feedback. A stochastic problem can however be well posed when is indefinite, because the diffusion term also penalizes the control.
Timeline:
A probability space carries a standard one-dimensional Brownian motion . Its natural filtration, augmented by the -null sets, is . Fix a horizon and deterministic coefficients , , weights , , (functions of time) and . The admissible controls are the -progressively measurable processes with . The state from the initial pair solves
and the cost is
Standing assumptions (H1)–(H2): , , , , , on , and square-integrability of the random terms . No sign condition is imposed on , or . The homogeneous problem (SLQ) sets ; its cost is .
The map is uniformly convex if, for some ,
With and , the Riccati equation is
with the Moore–Penrose pseudoinverse. A solution is strongly regular if a.e. for some (4.10).
The goal fixes no constant: the on each side is existential.
Companion items: Remark 4.6 (the same bounds ), the well-posedness of the state equation and the cost (Sun–Yong 2014, Proposition 2.1), and Proposition 3.5 (the standard conditions (1.4) imply uniform convexity).
Theorem 4.5 gives a checkable sufficient condition for the classical structure of LQ control: under (4.2) the Riccati equation has a solution whose gain matrix is uniformly positive definite, so the optimal control is a state feedback with an invertible gain. It covers indefinite weights, and Proposition 3.5 shows that it contains the classical case (1.4). Combined with Sun–Yong's equivalence it yields Corollary 4.7, the feedback representation of the open-loop optimal control, which later missions of this series use.
The results are proved in the paper. As far as is known they have no machine-checked proof. Formalizing them requires stochastic calculus for controlled SDEs (Itô's formula for quadratic forms of a state process) linked to matrix ODE theory. The definitions this mission fixes (the LQ problem, the Riccati and Lyapunov equations with a pseudoinverse) can be reused by the other missions of the series and by any stochastic LQ formalization.
The direction (ii) ⇒ (i) is a completion of squares followed by Lemma 2.3. Lemma 2.3 is not obvious: it asserts a bounded inverse for an operator defined through an SDE.
The direction (i) ⇒ (ii) is the hard one. The obvious approach would solve (4.6) directly, but (4.6) is nonlinear and its coefficient may be singular. No sign condition gives a priori bounds. The paper instead builds a policy-iteration sequence of linear Lyapunov equations. The difficulty is to show that every iterate keeps , so that the next gain is defined, and stays bounded below. These bounds come from the cost functional (Proposition 4.4), not from the matrix equation. Uniform convergence of the iterates then needs integrable estimates under the weak integrability of (H1).
IsStdBrownian (Mathlib's IsBrownianReal per coordinate, published module Peng1990.SMP.Stochastic). is augmentedFiltration (published ReflectedBSDE.Existence.Setting).state_wellposed poses existence, uniqueness and integrability of the cost. Expectations are Bochner integrals, and is the Euclidean .EReal infimum over admissible controls.HarmonicGames.Decomposition.pinv. Where the paper prints ((4.19), p. 2290) Lean's matrix inverse is used; it is invertible there by .Ruling out trivial forms. Uniform convexity is not defined through the operator of (3.8), and strong regularity includes the integral Riccati equation. A formalization that drops the Riccati equation, or reads uniform convexity off a matrix condition, is a different theorem. No positivity of , or is assumed anywhere except in Proposition 3.5, whose hypothesis (1.4) is exactly that.
Contributions welcome: Itô's formula for with a (or absolutely continuous) matrix ; existence and uniqueness for linear SDEs with coefficients; existence and uniqueness for linear matrix ODEs; the Penrose identities for pinv.
Online reviews let consumers learn about a new product from the experience of earlier buyers. For a firm selling to strategic consumers, who time their purchases, this social learning (SL) cuts two ways. Reviews reveal quality, which can raise second-period demand; but a consumer who expects reviews also has a new reason to wait, and every consumer who waits writes no review. Papanastasiou and Savva (Management Science 63(4), 2017) build a two-period model in which both forces are endogenous and ask whether a monopolist that commits to its prices in advance is better or worse off when consumers learn from one another.
The benchmark without learning is the classical intertemporal pricing problem with strategic consumers (Landsberger and Meilijson, 1985), whose optimal pre-announced plan is a decreasing price path. This mission formalizes the paper's answer for pre-announced pricing: its Proposition 3.
A unit mass of consumers has preference types uniform on . A product of unknown mean quality is sold over two periods. Buying in period gives type the utility , where is the consumers' discount factor and the perceived quality. The firm has unit cost and does not discount.
Everyone shares the prior . Individual quality perceptions are , and is the SL influence parameter. If a mass buys in period 1 and posts reviews, the posterior mean is , where is the average rating. Seen from period 1, is random, with the pre-posterior law
Under pre-announced pricing the firm commits to a plan . Consumers then play a purchasing game. A set of early buyers is an equilibrium if every type in weakly prefers buying now, and , and every other type weakly prefers to wait. Here has the pre-posterior law for . In period 2 the remaining types buy iff . The firm's expected profit is
and the optimal pre-announced profit is its supremum over all plans and all their equilibria. Absence of SL is the same model at , where .
For there are thresholds and such that
Proposition 3 says that social learning helps the firm at both ends of the patience range. For myopic consumers this is the informational effect alone. For patient consumers it holds even though learning makes them strictly more inclined to wait (Lemma 2) and the committed price cannot react to the reviews. The paper's numerical experiments found no intermediate at which learning hurts, but the theorem asserts only the two ends. The result underlies the managerial conclusions of the paper: firms gain from encouraging reviews even when consumers are strategic.
The result is proved in the paper; nothing in the model has been machine-checked before. A formal proof would check the equilibrium analysis of a continuum purchasing game with an endogenous information externality. Its intermediate results also serve the paper's two other missions: responsive pricing, and the comparison of responsive with pre-announced pricing. These are the Normal convex-order monotonicity (Lemma 5), the implicit threshold equation (Lemma 2), the no-SL benchmark (Proposition 1) and a Maximum-Theorem continuity statement.
The equilibrium threshold solves an equation whose Normal kernel has a variance that depends on itself. Existence, uniqueness and monotonicity are not closed-form computations.
The endpoint is the delicate one. There learning makes waiting most attractive, and the strict gain over the no-SL optimum must come from a plan that still induces a positive mass of early buyers.
Continuity of in is a Maximum-Theorem argument for a supremum over an unbounded set of prices whose objective passes through an implicit equilibrium. Compactness of the relevant price set has to be established, not assumed.
Every statement is taken over the standing assumptions , , , , with firm discount factor and pure strategies. Further conventions:
The witness used in the printed proof of Proposition 2(i) does not settle the case .
A complete development needs Gaussian expectations of hinge functions and their monotonicity in the variance (strict convex order), an implicit-equation argument for the threshold, and a version of Berge's Maximum Theorem. The Gaussian lemmas and the no-SL benchmark are reusable across the series. Contributions to any milestone are welcome.
Liouville quantum gravity describes random surfaces whose area measure is formally , where is a Gaussian free field (GFF). Schramm–Loewner evolution (SLE) describes random fractal curves that arise as scaling limits of interfaces in critical lattice models. Sheffield's paper Conformal weldings of random surfaces: SLE and the quantum gravity zipper (arXiv:1012.4797, Ann. Probab. 44 (2016), DOI 10.1214/15-AOP1055) shows that the two theories fit together: SLE curves are the interfaces obtained by conformally welding independent quantum surfaces along their boundaries.
The starting point of that program is a coupling between the reverse Loewner flow and the free boundary GFF (Theorem 1.2 of the paper): zipping up the upper half-plane by a reverse SLE map, and changing coordinates by the rule of Liouville quantum gravity, does not change the law of the field. This mission formalizes that theorem and the calculations of §4.1 that prove it.
Timeline. Couplings of forward SLE with the GFF go back to Schramm–Sheffield for (arXiv:1008.2447) and to Dubédat for general (arXiv:0712.3018). The reverse coupling with the free boundary GFF and the factor is Sheffield's (2010 preprint, published 2016); it underlies the later mating-of-trees theory of Duplantier–Miller–Sheffield (arXiv:1409.7055).
Let . A test function is a smooth, compactly supported real function with support in ; it has mean zero if . For a function write .
The free boundary Green's function is , and the energy of two test functions is
A free boundary GFF is a random modulo-additive-constant distribution: for every family of mean-zero test functions , the vector is a centred Gaussian vector with covariance . Pairings with test functions of nonzero mean are not defined.
Fix and a standard Brownian motion , and put . The reverse Loewner flow is , where for each
the pathwise form of . Write and
The fraktur are deterministic functionals of the flow. Finally , , and .
For every , with independent of ,
that is, the pairing vectors with every finite family of mean-zero test functions have the same law. Here .
The result. Theorem 1.2 says that the free boundary quantum surface is invariant in law under zipping up by an independent reverse SLE for a fixed time. It is the stationarity statement behind the quantum gravity zipper: Theorems 1.3–1.4 and 1.8 of the paper (the welding of boundary arcs of equal quantum length, treated in the companion mission) start from it, and the subsequent theory of quantum wedges, quantum cones and mating of trees uses it as a basic tool. It also gives an alternate way to sample the field: first sample (hence the curve), then sample an independent GFF, and form .
Formalizing it. The theorem is proved in the literature, and the paper itself regards several steps as standard (Proposition 3.1 is cited to [She07]). No part of it has a machine-checked proof. A complete development would give Lean its first Gaussian free field, its first reverse Loewner flow, and martingale statements for SLE functionals; the deterministic Loewner calculus of milestones 1–4 is useful independently of the probabilistic part.
The time derivatives in milestones 1–3 are routine once the flow is known to be holomorphic in , and milestone 4 follows from them. The obstacle is upgrading local martingales to martingales and exchanging the stochastic dynamics with integration in . Itô's formula gives that is a continuous local martingale; that it is a true martingale needs the bound of milestone 4, which shows that it is a Brownian motion run for a time at most a constant times . Passing from points to and to (4.2) needs integrability of uniformly on the support of and a Fubini argument. Mathlib has neither Itô calculus nor quadratic variation, so these steps need either a stochastic-calculus library or a direct argument. The final step (milestones 9–10) needs the Cramér–Wold device for an infinite-dimensional Gaussian field and the change of variables .
𝓓(ℍ, ℝ); integrals are Bochner integrals for Lebesgue measure on and .multivariateGaussian 0 (E(ρ_i,ρ_j)) laws for every mean-zero family. Every statement pairs only with mean-zero test functions.IsBrownianReal, taken with every path continuous and every coordinate measurable; martingales are with respect to its natural filtration and hold for all .In Wasserstein distributionally robust optimization (DRO) a decision is evaluated against the worst distribution within an optimal-transport ball around a nominal distribution . For a Wasserstein distance of finite order , the ball constrains an average transport cost. The case is different. The -Wasserstein distance constrains the largest distance any unit of mass travels, so it describes perturbations in which every sample may move, but only within a fixed radius. This is the perturbation model of adversarial training (Sinha, Namkoong and Duchi 2018) and of distributionally robust chance constraints (Xie 2021).
Zhang, Yang and Gao (arXiv:2205.00362v4, §5.1) generalize to an arbitrary cost , the maximum transport cost . They show (Theorem 2) that on a Polish space with a continuous cost the worst-case loss is a nominal expectation of a local supremum. Their Theorem 1 covers finite-order costs. Its proof does not reach this case, because is not an integral of the cost, and a separate argument is needed.
Timeline. Strong duality for finite-order Wasserstein DRO was proved for empirical on convex subsets of by Mohajerin Esfahani and Kuhn (2018). On Polish spaces it was proved for a lower semicontinuous cost and an upper semicontinuous loss by Blanchet and Murthy (2019), and for a power of a metric by Gao and Kleywegt (2023). For distributionally robust chance constraints, Xie (2021) treated the 1-Wasserstein distance on a totally bounded Polish space. Yang and Gao (2022, Optimization Online) obtained the -Wasserstein chance-constraint reformulation on normed spaces. Zhang, Yang and Gao (arXiv 2022, v4 2024) state the -Wasserstein and maximum-transport-cost duality for a continuous cost on a Polish space (Theorem 2 and Example 7).
Let be a Polish space (complete, separable, metrizable) with its Borel -algebra , and let be a probability measure on , the nominal distribution. A cost is a continuous function with , written with the nominal point first. A loss is a measurable with . Expectations take values in .
For probability measures let be their couplings: the probability measures on with marginals and . The maximum transport cost and its robust loss are
For a metric , . The Legendre transform of is , and is the soft-penalty counterpart .
The proof uses the interchangeability principle (IP). A measurable satisfies (IP) if is -measurable and
where is the set of probability measures on with first marginal . It also uses the measurable projection (Proj) and measurable selection (Sel) conditions of §3 of the paper.
For every and every ,
The result. Theorem 2 turns an optimization over probability measures into one expectation under of a deterministic local problem. Each nominal point is replaced by the worst point of its -ball. For an empirical this is a finite sum of local maximizations. This is the reformulation used for -Wasserstein adversarial training and for distributionally robust chance constraints. Example 7 of the paper derives from it, for , the robust chance constraint on a Polish space. The theorem needs no convexity, no semicontinuity of and no finiteness of the support of .
Formalizing it. The result is proved on paper; no machine-checked proof exists. A formal proof requires measurable projection and selection on Polish spaces, which Mathlib has only in part (analytic sets, Lusin separation). It also needs Prokhorov compactness for couplings and essential suprema under weak convergence. The milestones isolate these, so each can be attacked separately and reused.
The obvious argument restricts to deterministic transport plans with . This argument has two gaps. First, the maximizing map must be measurable, and the local supremum is in general only universally measurable, not Borel. Measurable projection and selection theorems for analytic sets are therefore needed, and the expectation must be read against the completion of . Second, the constraint is an infimum over couplings, and an infimum need not be attained. Without attainment one only obtains an inequality. Attainment is where Polishness of and continuity of enter, and continuity cannot be dropped. Remark 5 of the paper gives a discontinuous metric cost on for which the identity fails.
[TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X].ModelRiskOT.Duality.extIntegral, with lower Lebesgue integrals in EReal. It agrees with the paper whenever one part is finite and gives for . For the universally measurable integrand of the goal it is the completed integral. The Bochner integral is not used.essSup of , so .EReal, so for . The Legendre transform ranges over all real .EReal.NullMeasurable.The goal is stated only through , , the Legendre transform and the local supremum. (IP), (Proj) and (Sel) appear only in milestones, so no hypothesis of the goal assumes the duality it asserts. The robust loss is not defined through an ENNReal comparison either, which would make the ball at negative radii coincide with the ball at radius .
A complete development needs the following:
Contributions to any of these layers are welcome independently.
A forward–backward stochastic differential equation (FBSDE) couples a forward SDE, solved from an initial state, with a backward SDE, solved from a terminal condition that depends on the forward state. Such systems arise from the stochastic maximum principle, from quasilinear parabolic PDEs through Feynman–Kac formulas, and in mathematical finance. Whenever a control problem or a market model is solved through its first-order conditions, a fully coupled FBSDE appears, and the question is whether it has a unique solution.
The history has a recurring gap: each method covers a different regime, and none handles coefficients that are random, fully coupled, and have a forward diffusion depending on the martingale integrand , over an arbitrary horizon.
Fix a horizon and a probability space carrying a one-dimensional Brownian motion , with its natural filtration augmented by the null sets. All processes are real valued. The FBSDE (1.1) is
for , with . The coefficients depend on and on . Assumption 2.1 asks that they be progressively measurable for fixed , that be finite, and that they be Lipschitz in with a common constant , uniformly in . Solutions are sought in the space of progressively measurable with .
A decoupling field (Definition 2.2) is a random field with such that, on every short interval and from every square-integrable initial state, the FBSDE with terminal map is uniquely solvable and its solution satisfies .
The difference quotients (3.1) of the coefficients — in the variables () and for — enter the scalar function
and its essential supremum and infimum over all quotients give the dominating ODEs (3.13): and , with the bounds of .
Fix with , , (5.13). There are and , depending only on , and , such that whenever Assumption 2.1 holds and the quotients satisfy one of the nine conditions of Cases I–III ((5.14); (5.15)–(5.18); (5.19)–(5.22)), uniformly in the quotient arguments, then (i) the FBSDE has a decoupling field whose quotient obeys the bound assumed of with replaced by , and (ii) for every there is a unique solution in , with
A companion statement, Corollary 7.5, gives well-posedness over under the sign conditions (7.5) or (7.6), with no smallness constant.
The theorem replaces structural assumptions (small horizon, monotonicity, deterministic coefficients, independent of ) by conditions that can be read off the coefficients through a scalar ODE. It covers random coefficients and a forward diffusion that depends on , the case in which the classical Riccati-type obstruction appears, and it recovers the earlier sufficient conditions as special cases (§7.4 of the paper). The decoupling field produced in (i) is uniformly Lipschitz, which is the input to the comparison and stability results of §8 and to numerical schemes based on .
The result is proved in the paper; nothing here is open mathematically. None of it is formalized: there is no machine-checked existence theory for coupled FBSDEs in any proof assistant this mission is aware of. A complete development would be the first formal well-posedness theorem for a fully coupled FBSDE, and the milestones — the ODE comparison lemma, the small-time theory, and the patching argument of Theorem 2.3 — are each self-contained.
The obvious approach is a contraction argument on . It works only when is small, because the Lipschitz constant of the solution map grows with the coupling; iterating it over a partition requires a terminal condition whose Lipschitz constant does not deteriorate from one subinterval to the next. Controlling that constant is the whole problem. Its spatial derivative satisfies a backward stochastic Riccati equation with quadratic growth in both and and a singularity where ; such equations need not have bounded solutions, and the standard comparison theory for quadratic BSDEs does not apply off the region where the generator is Lipschitz. A second difficulty is the small-time theory itself: when depends on , even a linear FBSDE with constant coefficients is well posed on short intervals only if (Theorem 7.1 of the paper), so in Cases II and III, where and are large, the contraction argument does not apply even for small .
The development reuses the platform's Peng1990.SMP.Stochastic (standard Brownian motion, , the Itô integral IsItoIntegral) and the augmented Brownian filtration of ReflectedBSDE.Existence.Setting. Time is , time integrals are over real intervals, and the stochastic integral is for an Itô integral process of .
Committed conventions:
The constants , and are chosen before the probability space and the coefficients. A formalization that places them after the coefficients, integrates without integrability, divides at the pole , uses a real-valued essential supremum of an unbounded family, or states uniqueness without a solution class would make the statements vacuous or false; none of these is used.
Contributions are welcome on every milestone. The ODE layer (Lemma 5.1 and the a priori bounds of Theorems 5.9–5.11) needs only real analysis and is a natural first target. The stochastic layer needs Itô-integral facts (linearity, restriction to subintervals, the Burkholder–Davis–Gundy and Doob inequalities in ) and the Lipschitz BSDE theory; these are reusable well beyond this mission.
Deciding whether a real polynomial is non-negative on is NP-hard already for quartics, and the standard computational substitute is to ask whether it is a sum of squares (SOS) of polynomials, which is a semidefinite feasibility problem. The two notions agree only in three cases, determined by Hilbert in 1888: univariate polynomials, quadratic forms, and ternary quartic forms (equivalently, polynomials of degree at most 4 in two variables). Outside those cases there are non-negative polynomials that are not SOS, among them symmetric ones: Choi and Lam exhibited a symmetric quartic form in four variables that is non-negative but not SOS.
Many polynomial optimization problems are symmetric, invariant under permutations of the variables. Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486, Math. Oper. Res. 2013) study how symmetry reduces the size of SDP relaxations. Their §5 uses the degree principle, introduced by Timofte (2003) and refined by Riener (2012), to replace one symmetric problem in variables by finitely many problems in few variables. For symmetric quartics this yields an exact SOS certificate of non-negativity in every dimension: Theorem 5.5, the goal of this mission.
Timeline:
Let . A polynomial is symmetric if for every permutation ; its degree is the total degree. A polynomial is a sum of squares if for some polynomials in the same variables.
For symmetric put
and let be the set of points with at most distinct components.
An -partition of is a vector of positive, non-increasing integers with ; denotes the set of all of them. For ,
and . For the partitions are with , ; there are of them.
For and a symmetric of degree ,
with the set of 2-partitions of .
Theorem 5.5 turns non-negativity of a symmetric quartic in any number of variables into semidefinite feasibility problems of fixed size, one per 2-partition, each in two variables. This is a certificate scheme that is exact, in contrast with the SOS relaxation in variables, which fails for the Choi–Lam quartic. Proposition 5.1 and (5.1) are the general mechanism behind it, and they apply to any symmetric problem whose degrees are small relative to : they underlie the reduced relaxation hierarchy of Theorem 5.2 of the same paper.
All four milestones and the goal are proved results in the literature; the work is formalization. As far as a search of the platform shows, neither the degree principle nor Hilbert's ternary quartic theorem has a machine-checked statement on Prove2Me, and Mathlib has the vocabulary (MvPolynomial.IsSymmetric, IsSumSq) but neither theorem. Hilbert's theorem is a classical result of real algebraic geometry that is reusable far beyond this mission, for example in any SOS-exactness argument in low dimension.
The obvious route to the goal is to apply Hilbert's theorem to each , and that is the whole printed proof; it gives only the direction "non-negative implies every is SOS". The converse, "every SOS implies non-negative", is not a consequence of Hilbert's theorem: it says that a symmetric quartic attains its infimum, if anywhere, on points with at most two distinct coordinate values, which is the degree principle with . The paper quotes the degree principle from Riener's earlier work without proof, and it is not available in Mathlib.
Hilbert's theorem itself is the hardest item. It is a statement about all non-negative quartic forms in three variables, with no symmetry to exploit, and every known proof needs substantial real algebraic geometry beyond what Mathlib provides; it is not a computation on a Gram matrix.
Polynomials are MvPolynomial (Fin n) ℝ; evaluation is MvPolynomial.eval; degree is totalDegree; symmetric is MvPolynomial.IsSymmetric; sum of squares is Mathlib's IsSumSq in the relevant polynomial ring (the empty sum is allowed, as on the page). An -partition is encoded by its block map , required to be monotone, surjective and with non-increasing fibre sizes; this is in bijection with the page's , and is the substitution . Infima in Proposition 5.1 and (5.1) are taken in EReal, so empty feasible sets give and unbounded problems give ; no extended-real arithmetic is used.
Disclosed additions and readings, each forced by the page:
Ruled out: replacing "sum of squares" by non-negativity of (which would make the goal Proposition 5.1 alone), real-valued infima (which are on empty or unbounded sets), or arbitrary maps in place of 2-partitions.
Welcome contributions: Hilbert's theorem on ternary quartics in any standard form; homogenization and dehomogenization lemmas for MvPolynomial and IsSumSq; the degree principle, first for (the case the goal needs) and then with constraints.
In many operational problems the decision is taken after observing covariates (weather, calendar, prices) that carry information about an uncertain quantity (demand, yield, return). The target is the conditional stochastic program: minimize over a feasible set . Kannan, Bayraksan and Luedtke (Math. Program. 2023) approach it in two steps: fit a regression model of on , then use the regression residuals as scenarios of the uncertainty at the new covariate . Their earlier work (Kannan, Bayraksan, Luedtke, arXiv:2207.13554) analysed the sample average approximation built in this way (ER-SAA). The 2023 paper wraps the same scenarios in a distributionally robust problem, to protect against the small-sample error of the regression and of the residuals.
This mission formalizes the paper's rate of convergence for a family of ambiguity sets that contains sample robust optimization and reweighting (φ-divergence, CVaR) sets as special cases.
Responses follow , with regression function and error of law . A known nonempty closed convex set contains the range of , with orthogonal projection . From data , with , one computes a regression estimate and residuals . At a covariate realization the scenarios are .
The true problem (3) is with , and the full-information SAA objective (4) is .
The unified ambiguity family of §5 has two radii. is the radius of balls around each scenario. is a set of probability vectors that shrinks to the uniform weights. The worst-case expected cost over the distributions with and is the ER-DRO objective
and the ER-DRO problem (8) is , with optimal solution . Taking gives sample robust optimization; taking gives ambiguity sets with the same support as the empirical residual distribution. The intermediate objective reweights the true scenarios.
Assume the following:
Then
Theorem 17 shows that robustifying the residuals-based SAA costs nothing in rate. With the ER-DRO estimators converge at the rate of the ER-SAA estimators, which is set by the regression step: for OLS or Lasso, and for kernel regression or random forests. It covers in one statement sample-robust sets, φ-divergence sets and CVaR sets around the residual scenarios. It is the template for the paper's mean-rate analogue (Theorem 18) and for the consistency results (Proposition 15, Theorem 16), which reuse Lemma 14.
The result is proved in the paper; nothing in it is machine-checked. The mission produces checked versions of the decomposition (12) and of each step. It also produces a reusable predicate, a statement of a functional CLT in through Mathlib's convergence in distribution, and the passage from a uniform objective rate to rates for the optimal value and the out-of-sample cost.
The paper's proof is short, but each line hides a step. The obvious bound on the regression term uses the plain average . Under a reweighting that average is no longer what appears, and controlling needs the factor , which stays bounded only because of the rate in Assumption 12.
The full-information term needs tightness of from convergence in distribution in . That is a continuous-mapping and Portmanteau argument on a function space, not on .
All suprema over may be infinite for individual data realizations, and the probabilities of the events involved need not be measurable. Arithmetic with (sums, products with , comparing rates ) must be carried out with these in mind.
Carriers are the Euclidean spaces , , . The data are random variables on a probability space , and sample is i : Fin n. The covariate is fixed, and the paper's "for a.e. " assumptions are hypotheses at that . No i.i.d. assumption is made. is a nonempty subset of the probability simplex. The limit clause of (9) concerns the family in the radius at fixed ; Theorem 17 does not use it, so it is omitted. Assumption 12 is printed as an equality for every , which cannot hold at (there ), so it is required for all large . is defined by the explicit formula of p. 20, which the paper states equals the worst-case expectation over . and a true minimizer are taken as given selections of minimizers; the paper's standing assumptions guarantee they exist.
means: for every there are and with for all , for -valued . Every supremum over is computed in , so an unbounded family is never read as . Convergence in distribution is Mathlib's TendstoInDistribution for the Borel -algebra on .
The sample-robust balls are centred at the projected residual scenarios, not at the true scenarios . Centring them at the true scenarios would make the regression term vanish and the goal close to the full-information result.
A complete development needs the Cauchy–Schwarz steps of Appendix A.6 and the nonexpansiveness of the projection onto a closed convex set (inequality (6)). It also needs a calculus of , tightness of norms under convergence in distribution in , and the passage from uniform objective rates to optimal-value rates. The calculus and the tightness lemma are reusable beyond this paper. Contributions proving any milestone, or general lemmas as separate theorems, are welcome.
Designing a network that survives the failure of any single link is a basic problem of network design: given a graph whose links can be bought, choose as few links as possible so that the chosen subgraph still connects all vertices after any one of its links is removed. This is the minimum 2-edge-connected spanning subgraph problem (2ECSS). It is NP-hard, since the 2-edge-connected spanning subgraphs with edges are exactly the Hamiltonian circuits, and it is a relaxation of the graphic travelling salesman problem: every tour of a 2-edge-connected graph yields a 2ECSS with at most as many edges.
Timeline of approximation ratios for unweighted 2ECSS:
A graph has finite vertex and edge sets; every edge has two distinct ends, and parallel edges are allowed. For , is the set of edges with exactly one end in , and for we write . An edge set is 2-edge-connected spanning (a 2ECSS of ) if is connected and stays connected after the deletion of any single edge of ; is 2-edge-connected if is.
The cut relaxation of 2ECSS is
Every 2ECSS crosses every cut at least twice, so , the minimum size of a 2-edge-connected spanning multi-subgraph.
An ear-decomposition of starts from a single vertex and adds ears : paths whose two ends, or circuits whose one vertex, lie on the earlier ears, and whose other (internal) vertices are new. The ears partition . An ear of length is even if is even, nontrivial if , and short if . A nontrivial ear is pendant if no nontrivial ear has an end among its internal vertices; denotes the number of pendant ears. is the minimum number of even ears over all ear-decompositions, and .
An ear-decomposition is nice if it has even ears, all its short ears are pendant, and internal vertices of different short ears are non-adjacent. The internal vertex sets of its short ears avoiding a set form an eardrum . An earmuff chooses, for some , a path with for each so that the union of their edges is a forest. is the largest such , and .
For every 2-edge-connected graph there is a 2ECSS with
The theorem gives a polynomial-time -approximation for unweighted 2ECSS. Because it compares with rather than with the optimum, it also bounds the integrality ratio of the cut relaxation on unweighted instances by (the paper's Corollary 31). The two lower bounds and and the construction of Theorem 24 are shared with the paper's result for graphic TSP and its result for connected--joins, so the milestones of this mission are also steps toward those results.
The theorem is proved in the paper, and to the best of current knowledge none of it is machine-checked: there is no formal development of ear-decompositions, of Frank's even-ear parameter , or of 2ECSS approximation in Mathlib or on Prove2Me. The work here is formalizing the known proofs. Theorems 7 and 19 rest on classical results that are absent from Mathlib: Frank's theorem on ear-decompositions and the Edmonds–Johnson/Lovász packing of -cuts.
The arithmetic of the final step is short: and . The difficulty lies in the lower bounds and in the decomposition. A natural first idea is to bound every nontrivial ear by its internal vertices. This fails for 3-ears, whose three edges cover only two new vertices, and the paper handles them by making all short ears pendant and pairwise non-adjacent and then re-choosing them as a maximum earmuff. That step needs a matroid-intersection or forest-representative min-max theorem (Theorem 18), which in turn yields . The bound needs Frank's characterization of through minimum -joins together with the half-integral packing of -cuts. None of this machinery exists formally yet.
Every definition is local to the namespace NicerEars.TwoEC. Reusable beyond this mission:
Contributions are welcome on any milestone. Especially valuable are Frank's Theorem 7, the -cut packing behind Theorem 19, and the basic fact that a graph with an ear-decomposition is 2-edge-connected.
Wasserstein distributionally robust optimization (DRO) replaces the expected loss under a nominal distribution (typically an empirical distribution) by the worst expected loss over all distributions within a given optimal-transport distance of . Its tractability rests on a strong duality theorem that turns a supremum over distributions into a one-dimensional minimization over a multiplier of an expectation under alone. Such duality results were proved under successively weaker hypotheses: for finitely supported on by Mohajerin Esfahani and Kuhn (2018), on Polish spaces with lower semicontinuous costs and upper semicontinuous losses by Blanchet and Murthy (2019), and on Polish spaces with general nominal distributions by Gao and Kleywegt (2023). Zhang, Yang and Gao (arXiv:2205.00362v4, 2024) show that, on an arbitrary probability space, strong duality holds exactly when the integrand satisfies an interchangeability principle (IP) between expectation and supremum. That reduces every duality question to verifying (IP).
This mission formalizes the paper's Proposition 2, which verifies (IP) for the most common choice of cost, the -th power of a metric, under minimal hypotheses on and on the loss. The paper uses it for distributionally robust Markov decision processes on Borel spaces, where value functions are only measurable for a completed -algebra.
Let be a metric space and its Borel -algebra. Let be a probability measure on that is tight: for every there is a compact with . Write for the completion of under ; a function is -measurable if it is -measurable.
Expectations take values in the extended reals : .
Let be -measurable with , let and , and define
Let be the set of probability measures on whose first marginal is . The function satisfies (IP) if is -measurable and
No constant is fixed; the statement holds for every and every , including , where may be .
Combined with Theorem 1 of the same paper, Proposition 2 yields strong duality for -Wasserstein DRO on any metric space with a tight nominal distribution, in particular on every Polish space and every Borel subset of one, without semicontinuity of the loss. Allowing to be merely -measurable is what makes the duality applicable recursively in dynamic programming, where each stage's value function is lower semianalytic rather than Borel.
The result is proved in the paper, with the case left to the reader. No machine-checked proof of it, or of any Wasserstein DRO duality theorem at this generality, is known to exist. A formalization would supply the omitted case and pin down the measure-theoretic conventions (extended-valued expectations, completed -algebras) that the paper treats briefly.
The inequality "" is pointwise. The reverse inequality requires a near-optimal coupling, i.e. a measurable near-maximizer of . A general measurable selection theorem is not available: is not assumed Polish and is not assumed Borel, so the projection and selection theorems behind Polish-space duality do not apply. The approximation must also control the expectation of a possibly unbounded , where integrals take extended values and must be avoided.
[MetricSpace X] [MeasurableSpace X] [BorelSpace X]; is a probability measure with IsTightMeasureSet {Phat} (Mathlib's tightness).NullMeasurable f Phat. A Borel-measurable would be a strictly weaker theorem and is ruled out.ModelRiskOT.Duality.extIntegral: in EReal with lower Lebesgue integrals and . The Bochner integral, which returns on non-integrable functions, is not used. Because need not be -measurable, the page leaves undefined for a general coupling; the lower-integral reading is adopted, and stays on as printed.X × NullMeasurableSpace X Phat, with the completion on the second factor.Contributions welcome: lemmas on lower Lebesgue integrals of null-measurable functions under push-forward measures, and tightness-based approximation arguments, both reusable beyond this mission.
The graphic TSP is the travelling salesman problem in the shortest-path metric of an unweighted connected graph: visit every vertex of a graph by a closed walk using as few edge traversals as possible. It is the unweighted special case of the metric TSP, and it is the setting in which the 3/2 barrier of Christofides' algorithm (1976) was first broken for general graphs. It is also a natural test bed for the subtour LP: for graphic instances the LP relaxation is the 2-edge-connected subgraph relaxation below, and the conjectured integrality ratio of 4/3 for metric TSP is open even here.
Timeline of approximation ratios for graphic TSP on general graphs:
A graph is finite and undirected, with vertex set and edge set ; it may have parallel edges but no loops. is the graph obtained by doubling every edge. For , is the set of edges with exactly one endpoint in .
For , a -join is an edge set in which exactly the vertices of have odd degree. A tour of (Definition 1) is a -join in such that is connected: a connected multi-subgraph using each edge at most twice in which every degree is even. By Euler's theorem its edges form a closed walk through every vertex, and conversely. is the minimum size of a tour.
The relaxation is
with . Every tour gives a feasible point, so (Proposition 2).
The analysis uses ear-decompositions: is built from one vertex by adding ears, each a path joining two existing vertices through new ones, or a circuit through one existing vertex. is the minimum number of ears of even length; counts pendant ears (nontrivial ears to which no nontrivial ear is attached). Short (2- and 3-) ears in a nice ear-decomposition (Definition 9) form an eardrum ; an earmuff (Definition 12) re-routes some of them so that their edges form a forest, and is its maximum size. The two lower bounds are
The result. Theorem 29 gives a polynomial-time 7/5-approximation for graphic TSP and shows that the integrality ratio of on graphic instances is at most 7/5. The same paper uses the shared machinery (nice ear-decompositions, earmuffs, the bound ) for a 3/2 bound for connected -joins, including graphic --path TSP, and a 4/3 bound for 2-edge-connected spanning subgraphs; those are separate missions of this series.
Formalizing it. The theorem is proved in the paper; none of it is machine-checked. The platform has metric-TSP results over Hamiltonian permutations (Christofides-type and Wolsey-type bounds), but no graphic TSP, no multigraph tours, no ear-decompositions and no -join polyhedra. The formalization would add a reusable multigraph layer (doubled graphs, -joins, ear-decompositions, Frank's ), two classical cited theorems (Frank's Theorem 7 and the Mömke–Svensson Lemma) and the paper's own earmuff analysis.
The two tour constructions are each worse than 7/5 on their own: Theorem 24 alone gives , and Lemma 28 alone gives . The bound comes only from taking the better of the two, balanced at , and only after the short ears have been re-chosen as a maximum earmuff, which the lower bound requires.
The cited inputs are deep. Theorem 19 relies on Frank's ear theorem and the Edmonds–Johnson–Lovász packing of -cuts; Theorem 27 relies on the odd-join polytope of an auxiliary 2-edge-connected graph; Lemma 23 relies on Lemma 10 (nice ear-decompositions exist) and a min-max theorem for earmuffs (Theorem 18, via matroid intersection or forest representatives). Mathlib has none of these. A Christofides-style argument (spanning tree plus matching) cannot get below 3/2 and is not a route to the goal.
Graph V E with ends : E → Sym2 V and no loops, over finite types, so parallel edges are allowed as in the paper. Restricting to simple graphs would be a weaker theorem and is ruled out. has edge type E × Fin 2, so every multiplicity is at most 2. Connectivity of an edge set is connectivity of the simple graph of pairs joined by one of its edges.Welcome contributions: proofs of any milestone; the multigraph and ear-decomposition layer (Whitney's theorem that 2-edge-connected graphs have ear-decompositions); -join existence and parity lemmas; the block decomposition at a cut vertex.
In graphic TSP the cities are the vertices of a connected graph and the distance between two of them is the number of edges on a shortest path. A closed walk visiting every vertex is the same thing as a connected multi-subgraph of in which every degree is even. Dropping "closed" and asking for a walk from to gives graphic --path TSP, where exactly and must have odd degree. Both are special cases of the connected--join problem: given and a vertex set of even size, find a smallest edge multiset in which exactly the vertices of have odd degree and which connects all vertices.
Graphic TSP is MAXSNP-hard (Papadimitriou and Yannakakis 1993), and until 2011 no algorithm beat the ratio of Christofides (1976) on it.
Timeline.
All graphs are finite and undirected, with parallel edges allowed and no loops. For a graph , is the graph with every edge doubled. A -join is an edge set such that is exactly the set of vertices of odd degree in . A connected--join of is a -join in such that is connected. Each edge of is used at most twice. A tour is a connected--join. is the minimum size of a connected--join.
For , is the set of edges with exactly one end in . For a partition of , is the set of edges joining different classes. The LP relaxation is
The proof works with ear-decompositions: a vertex followed by ears, each a path attached at its two ends or a circuit attached at one vertex. is Frank's minimum number of even-length ears. A nice ear-decomposition has even ears, all of its short (2- and 3-) ears are pendant, and the internal vertices of different short ears are non-adjacent. An eardrum is a family of single vertices and adjacent pairs that are pairwise non-adjacent. An earmuff chooses, for some of its members , a path whose internal vertex set is , so that the chosen paths together form a forest. is the maximum number of paths in an earmuff, and
For every connected graph and every with even there is a connected--join with
The result. Theorem 25 gives a -approximation for connected--joins, and therefore for graphic --path TSP. It also bounds the integrality ratio of by , and the paper shows this is tight (Figure 3). Lemma 23, Theorem 20 and Theorem 24 are shared with the 7/5 bound for graphic TSP and the 4/3 bound for 2-edge-connected spanning subgraphs: the three results differ only in the second construction used when there are few pendant ears. The earmuff lower bound is a combinatorial dual certificate for in its own right.
Formalizing it. The theorem is proved on paper; none of it is machine-checked. A formal development would contribute:
None of these is in Mathlib.
The natural first attempt is Christofides' construction: a spanning tree plus a parity-correcting join. The tree costs at most and the join at most , which gives only (paper, p. 3). It gives nothing better against .
Ear-decompositions with few even ears control the parity part (Proposition 6). Then short pendant ears become the bottleneck. Proposition 8 is good only when there are few 2-ears. When there are many pendant ears, the matching lower bound must account for them, and it is not visible from . It comes from the earmuff min-max theorem (Theorem 18), which rests on Lovász's matroidal generalization of Kőnig's theorem (Corollary 14). The ear-decomposition must also be re-chosen so that its clean short ears form a maximum earmuff while it stays nice (Lemma 23).
Graph V E with ends : E → Sym2 V over finite types. has edge type E × Fin 2, so a connected--join is a Finset (E × Fin 2) and uses each edge at most twice.All definitions are local to the namespace NicerEars.TJoin. Mathlib has neither an ear-decomposition theory nor a multigraph connectivity API. A reusable library of multigraph ears, -joins and forest representative systems would serve the two sibling missions (graphic TSP, 2ECSS) as well. Contributions to any milestone, and to general lemmas such as the existence of -joins in connected graphs, are welcome.
Wasserstein distributionally robust optimization (DRO) hedges a decision against every probability distribution within a given transport distance of a nominal one, typically the empirical distribution of data. The inner problem, the worst-case loss, is an optimization over an infinite-dimensional set of measures, and every practical use of Wasserstein DRO — tractable reformulations, statistical guarantees, regularization interpretations — rests on a strong duality theorem that replaces it with a one-dimensional minimization over a Lagrange multiplier.
Such duality theorems have been proved under progressively weaker hypotheses:
This mission formalizes the last of these, Theorem 1 of Zhang–Yang–Gao.
Let be a probability space, a measurable loss with , and a measurable transport cost with (Assumption 1). Expectations take values in , and the convention is used for products .
The Kantorovich transport cost between and a probability measure is
where is the set of couplings with marginals and . The worst-case loss is
with for . For let and
is the set of probability measures on with first marginal . A measurable satisfies the interchangeability principle (IP) if is -measurable (measurable for the completion of ) and
The Legendre transform of is .
satisfies (IP) for every if and only if the supremum functions are -measurable and
The minimum is attained. Both sides may be .
The result. Theorem 1 separates Wasserstein DRO duality into two parts. The first, the second display, holds with no regularity at all: the worst-case loss always equals a one-dimensional minimum over of a supremum over couplings with fixed first marginal. The second identifies exactly when that supremum can be moved inside the expectation, which is the form (D) used in applications: (D) holds for all radii if and only if (IP) holds. The question of when Wasserstein DRO has its standard dual becomes a question about measurable selection and measurable projection, which is studied in a companion mission of this series. The duality results of the timeline above become special cases in which (IP) can be verified.
Formalizing it. The results are proved in the paper; none of them has a machine-checked proof. A formalization produces a verified duality theorem at the level of generality of measurable spaces with extended-valued costs, together with a reusable layer: Kantorovich costs with values in , extended-real expectations, and one-dimensional Legendre transforms of extended-real functions.
The proof is short on paper because it delegates to one-dimensional convex analysis: the involution of the Legendre transform on (Rockafellar, Theorem 12.2), applied to . The work is in the extended reals. can be on all of , can be identically , and the costs and products involve . Concavity of on requires mixing near-optimal distributions and couplings, and lower semi-continuity of requires Fatou's lemma for functions bounded below by , not by . The "only if" direction of the goal has to recover (IP) for every from (D), which goes through biconjugation of and the right continuity at of both transforms. A proof that treats every value as finite does not cover the theorem.
The Lean development lives in the namespace ShortWDRODual.Legendre.
ENNReal-valued and curried, c x̂ x, with the nominal point first. The loss is real-valued and measurable.RWPI.SqrtLasso.transportCost (infimum over probability couplings of the lower Lebesgue integral of , in ).ModelRiskOT.Duality.extIntegral, in EReal. This agrees with the paper whenever one part is finite. It assigns to the undefined case , so a law or coupling with an undefined expectation never raises a supremum.EReal, so that for . Reading it as would make every Legendre transform .IsLeast). Concavity, convexity and monotonicity of extended-real functions are stated as explicit inequalities with real weights. Lower semi-continuity "on " is relative to .NullMeasurable. Disclosed reading: in the goal and in the fixed- milestone, the measurability of the supremum functions is stated explicitly next to the duality formula, because the paper's expectation in (D) presupposes it and (IP) contains it. Lemma 2's statement on assumes this measurability for , for the same reason.A complete development needs the one-dimensional Fenchel–Moreau theorem for extended-real functions on , gluing and mixing of couplings with a fixed first marginal, and Fatou's lemma for extIntegral. Each is reusable well beyond this mission. Contributions of any of these as separate lemmas are welcome.
A constraint on a decision requires the distribution of the random vector . In practice that distribution is known only partially: its support, a few moments, or the probability mass of some regions estimated from data. Distributionally robust optimization asks that the constraint hold for every distribution consistent with this information. Wiesemann, Kuhn and Sim (Optimization Online 3757, 2013; Oper. Res. 62(6), 2014) proposed one standardized format for this information. Their format contains, as special cases, many ambiguity sets used earlier: support and moment information (Delage and Ye, 2010), and mean–covariance and directional-deviation information (Goh and Sim, 2010). They then characterized exactly when a worst-case expectation constraint over such a set has a finite conic reformulation. This mission formalizes that characterization: the paper's Theorem 1 and the steps of its proof.
The uncertain parameters are , and an auxiliary random vector may be added to describe structure of . A proper cone is a closed convex cone with and nonempty interior. Write for , and for the dual cone. For indices the confidence sets are
with matrices , vectors and proper cones . The ambiguity set is
where . The paper imposes three conditions:
The distributionally robust constraint (3) is for all .
A set is strictly included in , written , if lies in the interior of . The nesting condition (N) requires that any two distinct confidence sets be strictly nested or disjoint. For each , indexes the confidence sets containing .
Under (C1)–(C3), (N) and the two regularity conditions (S1)–(S2) described below, the constraint (3) holds if and only if there are , and such that, for all and ,
When the are orthants, second-order cones or semidefinite cones, Theorem 1 turns the semi-infinite, measure-valued constraint (3) into a linear, conic-quadratic or semidefinite system of size polynomial in the data. The paper's Theorem 2 shows that when nesting fails, even checking is strongly NP-hard. Theorem 1 is therefore the tractable side of a sharp dividing line. The paper builds its conservative approximation for non-nested sets (Theorem 3) and its lifting results (Section 3) on it.
The result is proved in the paper; nothing here is open. The formalization contributes two things. First, the duality theory for finite moment problems over measures on a compact set, and conic strong duality for strictly feasible sets: neither exists in Mathlib as stated. Second, a corrected statement. As printed, the "only if" direction of Theorem 1 is false, because (C2) does not give the strong duality the proof attributes to it. No machine-checked version of Theorem 1 is known.
The sufficiency half is weak duality: a pointwise inequality on integrated against any . The necessity half needs three facts.
Vectors are Fin n → ℝ, products are Matrix.mulVec and dotProduct, and the outcome space is (Fin nP → ℝ) × (Fin nQ → ℝ) with its Borel -algebra. The index set is Fin (nI + 1), 0-based, with = Fin.last nI. Probabilities are μ.real. Constraint (3) is stated in its "for all " form, so no supremum of reals appears. The scalar and the vector are separate fields.
Every member of is a probability measure with finite first moment, so is a genuine integral and not Lean's default value . The expectation is genuine as well, since grows at most linearly. Hypothesis (C2) keeps nonempty, so (3) cannot hold vacuously. A sorry-free sanity file exhibits two nested intervals for which all hypotheses of the goal hold at once.
Hypotheses added to the paper's, each needed for a true statement:
(S1) also excludes some instances the page allows: or for , and expectation rows that cannot be shifted in every direction by measures on .
The sufficiency milestone drops (C2) and the standing bounds , which only strengthens it.
Needed infrastructure, all reusable: conic duality for closed convex cones, Lagrangian duality for linear programs over finite measures on a compact set, and the extension of a convex inequality from the boundary of a compact set. Contributions of any of these as separate lemmas are welcome.
Lasserre's hierarchy is a sequence of semidefinite relaxations for minimizing a polynomial over a set defined by polynomial equations and inequalities (Lasserre 2001). Under the archimedean condition its optimal values converge to the true minimum, but only asymptotically in general; in practice the hierarchy is often exact at a small relaxation order. J. Nie's paper (arXiv:1206.0319v2, Math. Program. 146 (2014)) explains this gap in two steps. Its Theorem 1.1 shows that finite convergence follows when the classical optimality conditions of nonlinear programming hold at every global minimizer. Its Theorem 1.2, the subject of this mission, shows that those optimality conditions hold at every local minimizer for all input data outside the zero set of finitely many polynomials in the coefficients. Together the two results give finite convergence of Lasserre's hierarchy for generic archimedean problems.
The genericity statement is also of independent interest in nonlinear programming: it says that degenerate local minimizers (failing constraint qualification, strict complementarity or second order sufficiency) are an algebraically exceptional phenomenon for polynomial data of fixed degrees.
Fix variables and write for the real polynomials of degree at most . Problem (1.1) is
with feasible set . For the active set is . At :
The input data are the coefficient vectors of ; a polynomial in the coefficients is a real polynomial evaluated at that vector. The paper's Condition 4.3 lists four families of such polynomials: resultants and discriminants (§2.4) of subsets of the constraints, and the polynomials of (4.6) and of (4.11), which detect a complex projective solution of the homogenised critical-point systems (4.5) and (4.10). Homogenisation is at the nominal degree , with .
For positive degrees there are polynomials in the coefficients such that
The theorem gives the second half of the paper's explanation of finite convergence: combined with Theorem 1.1, Lasserre's hierarchy converges in finitely many steps for all archimedean problems with input outside a proper algebraic subset. Section 5 of the paper derives further consequences, for instance that Marshall's boundary Hessian condition holds on a Zariski open set of data, and that Putinar-type certificates exist generically on the boundary of the cone of nonnegative polynomials. Beyond polynomial optimization, the statement is a precise algebraic form of the folklore that "generic nonlinear programs are nondegenerate".
The result is proved in the paper; no machine-checked version is known. A formalization fixes the exact quantifier structure (the printed statement is vacuous without a nonvanishing clause, and two items of Proposition 4.4 need an extra hypothesis), and builds reusable infrastructure: projective elimination over , homogenisation at a nominal degree, and the bordered-Hessian characterization of second order sufficiency.
The local part (Proposition 4.4, Lemma 4.6, Proposition 4.5) is linear algebra plus first and second order necessary conditions. The global part is not. Proposition 4.1 and 4.2 need the main theorem of elimination theory: the set of coefficient vectors for which a homogeneous (or bihomogeneous) system has a nonzero complex solution is Zariski closed, defined by polynomials in the coefficients. Mathlib has the univariate resultant only. Appendix A, which shows these polynomials do not vanish identically, has to control the homogenised systems both at finite points and at points at infinity (), where only the leading forms of the data are seen. Reasoning over alone does not suffice: the set of data whose real system is solvable is not the zero set of a polynomial.
Polynomials are MvPolynomial (Fin n) ℝ, points are Fin n → ℝ, and gradients and Hessians are formal partial derivatives. Homogenised polynomials have complex coefficients in n + 1 variables, variable 0 being , and homogenisation uses the nominal degree , not the actual degree. CQC is linear independence of an indexed family (repeated gradients count twice). The optimality conditions are bundled: CQC together with one multiplier pair satisfying (1.3), (1.4), (1.5) and (1.7); under CQC the multipliers are unique.
Condition 4.3 is encoded through the defining properties of Res, Δ, and (unsolvability of the corresponding complex projective systems) rather than through the polynomials themselves; since the goal is existential in the polynomials, this is not a weakening. Coefficient variables exist for monomials of every degree, so the goal's nonvanishing clause is asserted at an admissible input: a formal polynomial that is nonzero but vanishes on all admissible data (such as the variable of a monomial of degree ) does not satisfy it. Without that clause the printed theorem would be satisfied by .
Hypotheses added to the page, each disclosed in the statements: in Propositions 4.4 and 4.5 (Condition 4.3's standing assumption; Theorem 1.2 is stated for all , as printed), the nonvanishing clause in Theorem 1.2, and item (a) of Condition 4.3 in Proposition 4.4 ii)–iv) (with item (b) alone, , , , violates CQC). Proposition 4.2's nonsingularity is asserted at all complex critical pairs.
A complete development needs projective elimination theory over (reusable well beyond this mission), multivariate resultants and discriminants as polynomial functions of coefficients, Euler's identity for forms, and genericity facts about critical points of polynomial programs. Contributions to any of these, and direct proofs of the local milestones, are welcome.
An isotropic Gaussian random field is a spatial random quantity whose probability law is unchanged when the sphere is rotated. Such fields model spatially distributed uncertainty when no direction is preferred. The question in this mission is concrete: if a field is simulated by retaining only finitely many spherical harmonic frequencies, how rapidly does the simulation approach the full field? Lang and Schwab study this question while developing regularity, simulation, and stochastic partial differential equation results for isotropic fields on spheres (Lang and Schwab, 2015). Their §5 separates the error in expected spatial energy from the error seen along an individual sample. The latter is the target here.
Let be the unit sphere in and let be surface area measure, with . A point has angular coordinates , where . Spherical harmonics are the normalized complex functions indexed by a degree and an order . They form an orthonormal basis of complex with this unnormalized surface measure. The real factor is the normalized associated Legendre function appearing in for (§2, pp. 4–5).
The angular power spectrum is a nonnegative sequence recording the variance at each harmonic degree. Let and be independent standard normal random variables for the indices that occur below. The centered real field used in §5 is the ordered series
Its Karhunen–Loève truncation retains the outer sum through degree . These are the approximations analyzed and simulated in the paper (§5, p. 25). The norm measures the spatial size of a sample , while takes the th moment of that spatial norm over randomness. Lemma 5.1 relates this explicit series, in law, to an arbitrary centered isotropic Gaussian field with the same angular power spectrum (pp. 23–24).
The goal, Corollary 5.4, assumes , , an integer , and the tail condition for . It asserts almost-sure convergence in spatial and, for each , an eventual samplewise bound (p. 28):
The attack path retains three intermediate statements from §5. The squared mean-square error equals the exact spectral tail (the proof of Proposition 5.2, p. 26). Proposition 5.2 establishes convergence in and the bound
for (p. 25). Theorem 5.3 gives the same exponent for every finite , with a constant depending only on (p. 27). The goal's exponent may approach, but does not include, .
The mean-square estimate controls average approximation error, but it does not itself say whether one sequence of simulated fields converges along almost every outcome. Corollary 5.4 supplies that pathwise assertion and a quantitative rate for each exponent below the spectral threshold. It identifies the resolution needed to make the spatial error small for almost every sample, rather than only on average. The threshold directly links harmonic spectral decay to numerical truncation quality.
The cited results are already proved in the paper; the remaining task is to formalize their statements and proofs for the explicit KL model. The definition layer provides a reusable real representation of normalized spherical harmonics and mixed norms on . A completed proof would also make the transition from Gaussian moment estimates to samplewise convergence available as a machine-checked argument in this setting. No claim is made that these results already have machine-checked proofs.
The spherical harmonics are orthonormal, but an error bound for the full field needs more than termwise estimates. It must control the infinite tail while keeping the harmonic normalization, Gaussian variances, and the surface measure consistent. The passage from an expected error to one bound that eventually holds along almost every sample also requires estimates for arbitrarily high finite moments. A fixed second-moment bound does not yield the full range of exponents in Corollary 5.4. The paper's constant in Proposition 5.2 and the parameter dependence of the constant in Theorem 5.3 therefore matter to the final statement.
Lean uses EuclideanSpace ℝ (Fin 3) for the sphere. Coordinates represent the paper's . volume.toSphere supplies surface measure of mass . Legendre polynomials use Rodrigues' formula; the associated harmonics use Cartesian coordinates through , so they are defined at the poles without choosing an angle there. The field is the limit of the ordered partial sums . A nonconvergent sequence receives Lean's arbitrary limit value, but the theorems concern almost-everywhere convergence and norms, where such exceptional values must be shown irrelevant.
Spatial squared norms and mixed norms are extended nonnegative integrals. This keeps nonintegrable functions from taking a false zero norm. Lean's natural numbers include zero; in the paper is recorded as . Decay is required only above , exactly where the paper requires it. Coefficients that enter the series are measurable, jointly independent, and standard normal. The unused coordinates are zero, as specified in Lemma 5.1; coefficients at invalid indices are unconstrained. The field is the explicit series of p. 25, with Lemma 5.1 supplying the paper's identification in law with any centered isotropic field. In Theorem 5.3 the constant is chosen before the field and probability space, preventing it from depending on a particular spectrum or cutoff. The almost-sure conclusion is a spatial claim, never a pointwise assertion at each sphere point.
The displayed identity on p. 26 omits a square on its left-hand norm, although the neighboring formulas use squared norms. The formal error identity restores the square and the milestone preserves the printed wording. Contributions to the harmonic normalization, exact spectral identity, uniform finite-moment estimates, and the final almost-sure result all fit this mission. The normalizations, the positive cutoff, and the explicit independent Gaussian coefficients rule out vacuous or zero-field encodings.
The hard-core model on a finite graph at fugacity weights each independent set of by . Its normalizing constant, the independence polynomial , is a basic object of statistical physics (a lattice gas with hard-core exclusion) and of combinatorics ( counts independent sets).
The complexity of approximating on graphs of maximum degree is settled for general graphs: below the uniqueness threshold there is a deterministic approximation scheme (Weitz, STOC 2006, doi:10.1145/1132516.1132538), and above it the problem is NP-hard to approximate. On bipartite graphs the picture is different. Approximately counting independent sets of a bipartite graph defines the class #BIS, whose complexity is a major open problem of approximate counting, and Cai, Galanis, Goldberg, Guo, Jerrum, Štefankovič and Vigoda showed that for and the hard-core model on bipartite graphs of maximum degree is #BIS-hard (arXiv:1311.4839).
One route to partial progress is to find natural classes of bipartite graphs on which these #BIS-hard problems become tractable. Helmuth, Perkins and Regts did this for the hard-core model at high fugacity on the torus , using Pirogov–Sinai contour models and the cluster expansion (arXiv:1806.11548). Jenssen, Keevash and Perkins extended the method to abstract polymer models and to all bounded-degree bipartite expanders (arXiv:1807.04804; SIAM J. Comput. 49(4), 2020). This mission formalizes the mathematical core of their Theorem 1.
Let be a finite bipartite graph with vertex classes (odd vertices) and (even vertices), , and maximum degree at most . For a vertex set , the vertex boundary is the set of vertices outside with a neighbour in . For , is a bipartite -expander if
A subset of one class is small if it has at most half as many vertices as that class. The hard-core partition function is
with the independent sets of . A number is an -relative approximation to if .
is the graph on the same vertices in which two distinct vertices are adjacent when their distance in is at most ; a set is -connected when it induces a connected subgraph of . An even polymer is a nonempty, small, -connected set ; odd polymers are defined in . Two polymers are compatible if their distance in exceeds . Each polymer has the weight
and the polymer partition functions are , summed over the families of pairwise compatible even polymers (the empty family included), and likewise. Even polymers describe deviations from the ground state "all odd vertices occupied", and odd polymers from the other ground state.
For , , every bipartite -expander of maximum degree at most on vertices, and every
In the order of the paper's proof: Lemma 18 (every independent set has a small side); the identity ; the size bound for sparse independent sets; Lemma 20 (part 1 of the goal); the weight bound ; the count of at most -connected -sets through a vertex; and inequality (8), .
The two parts of the goal are exactly what Theorem 8 of the paper (adapted from Helmuth, Perkins and Regts) consumes: given a polymer model satisfying the Kotecký–Preiss condition, the truncated cluster expansion of yields an FPTAS and, through self-reducibility, a polynomial-time sampler. Together they give a deterministic approximate counting algorithm for a #BIS-hard problem on a natural graph class, at fugacities far above , the regime in which the problem is hard on general bipartite graphs. The same template (reduction to polymer models around ground states, then Kotecký–Preiss) underlies the paper's results for the Potts model, for random regular bipartite graphs and for proper colourings, and a large later literature on algorithms at low temperature.
The result is proved in the paper; to our knowledge none of it has been machine-checked. A formalization adds a precise treatment of the degenerate cases (see below), a reusable formal definition of abstract polymer models over vertex sets, and the elementary but intricate bijection between compatible polymer families and sparse sets.
Each step is elementary, and the difficulty lies in the bookkeeping. The reduction needs an exact correspondence between families of pairwise compatible polymers and sparse subsets of a class, and an exact double count over independent sets. The quantitative step of Lemma 20 compares the total weight of sparse independent sets, which have at most vertices, with ; the printed last inequality, , follows from only for up to about , and larger forces both classes to have at most nine vertices, a finite range that needs its own argument. The Kotecký–Preiss half needs the count of connected sets in a bounded-degree graph (Lemma 14 of the paper, from Galvin and Kahn), applied to , and a geometric series.
The algorithmic conclusion of Theorem 1 (an FPTAS and a polynomial-time sampling algorithm, with running time ) is not formalized: Mathlib has no machine model and the running times carry unspecified constants. The goal is the mathematics the algorithm rests on: the reduction to two polymer models and the Kotecký–Preiss condition for both. The cluster expansion and Theorem 8 are not part of the mission.
Conventions. The graph is a SimpleGraph V on a finite type, with a Finset V and its complement; bipartiteness is a hypothesis. The fugacity is lam. "" is 2 * #S ≤ #O in . Distances use the extended distance SimpleGraph.edist, so vertices in different components are never close. The Kotecký–Preiss sum ranges over the polymers of the same class incompatible with , including itself. Polymers are capped at half of their own class, not at ; the condition without this cap, or with compatibility in place of incompatibility, would be a different statement.
Two hypotheses differ from the page. Theorem 1 states the threshold as for an absolute constant ; the goal uses the threshold its proof uses (§4.3). The hypothesis is added: on the edgeless graph with one vertex in each class the expansion condition is vacuous, no side of the independent set is small, and Lemma 18 and Lemma 20 fail.
A complete development needs: the bijection between compatible families and sparse sets, Lemma 14 for , and real-power estimates. The polymer-model and graph-power definitions are reusable for the sibling missions of this series. Proofs of individual milestones are welcome independently.
A lookback option pays a function of the running maximum of the underlying asset over the life of the contract. When the prices of European call options of all strikes at the maturity are quoted, the risk-neutral law of the terminal price is known, but the law of the whole path is not. The robust (model-free) superhedging cost of the lookback payoff is the cheapest initial capital that, combined with a static position in the quoted calls and dynamic trading in the underlying, dominates the payoff in every model consistent with .
Hobson (Finance Stoch. 1998) computed this cost for by a pathwise inequality, and identified the extremal model through the Azéma–Yor solution of the Skorokhod embedding problem (Azéma–Yor 1979). Galichon, Henry-Labordère and Touzi (Ann. Appl. Probab. 2014, arXiv:1401.3921) recast model-free bounds as a dual stochastic control problem in which the marginal constraint is penalised by a Lagrange multiplier . Their Theorem 3.1 recovers Hobson's bound for every nondecreasing from that dual, with an explicit optimal multiplier and stopping time. The result is one of the founding examples of martingale optimal transport.
Let be a real Brownian motion with continuous paths and , adapted to a filtration with increments independent of the past, and let for a spot . Write . Let be the set of stopping times for which the stopped process is a uniformly integrable martingale.
The marginal is a probability measure on with finite first moment and mean . Its call prices are . The payoff is with of class and nondecreasing.
For a multiplier and set and . The admissible multipliers are
and the reduced superhedging problem (3.7) is
The barycenter function is for and otherwise. The Hardy–Littlewood transform is the probability measure with
The Azéma–Yor stopping time is , and the candidate multiplier is
that is, the convex function vanishing below that solves the weak ODE (3.21) with .
If and , then
The goal is the paper's theorem for the reduced problem (3.7), in its full two-equality form: the value, its attainment by , and its closed form.
The theorem identifies the model-free price of a lookback payoff as an explicit functional of the call prices, , and exhibits the extremal model (Brownian motion stopped at ) and the optimal static hedge (). It shows that the dual stochastic control formulation is sharp on a nontrivial path-dependent payoff, which is the template for later work on martingale optimal transport with path-dependent costs.
The result has been proved since 2014 (and Hobson's bound since 1998). It has not been formalized. A complete development would provide machine-checked versions of the Azéma–Yor embedding, the law of the maximum at the embedding, a verification theorem for a reflected optimal stopping problem with a nonsmooth obstacle, and the convex-analytic identities linking call prices to second-derivative measures. Each of these is reusable well beyond this paper.
The upper bound requires a verification argument for an optimal stopping problem of the pair with a reflection at the diagonal, where the candidate is only as regular as the convex multiplier : second derivatives are measures and the free boundary solves its ODE only in a relaxed sense. An Itô formula for functions does not apply; an Itô–Tanaka (local time) argument for concave functions of , with the reflection term killed by the Neumann condition, is needed, followed by a localisation that uses uniform integrability and the integrability condition in . The lower bound needs the Azéma–Yor embedding and the law of , neither of which is in Mathlib; the naive appeal to "the embedding exists" does not give the joint law of the stopped value and the maximum.
The Lean development lives in the namespace LookbackMOT.HL and uses Mathlib's IsBrownianReal, IsStoppingTime, stoppedProcess, stoppedValue, Martingale, UniformIntegrable and HasLaw. Committed conventions:
No trivializing reading is available. Payoff expectations are never Bochner integrals (which would be for non-integrable payoffs). lies in and in , so neither the supremum nor the infimum is over an empty set. The predicates for and are satisfiable (witnessed for in a sorry-free check). is only evaluated where a.s. Every division has a positive denominator on the sets that carry mass.
Contributions welcome: the Azéma–Yor embedding and the law of the maximum; an Itô–Tanaka or local-time calculus sufficient for concave functions of Brownian motion and its maximum; the call-price identities of convex analysis; and the analysis of .
Many operational decisions are linear programs whose cost vector is uncertain but partly predictable: shortest-path routing with uncertain travel times, portfolio choice with uncertain returns, shipment planning with uncertain costs. Before deciding, one observes features (traffic, market signals) correlated with the costs . Contextual linear optimization asks for a policy mapping features to decisions that minimizes the conditional expected cost, learned from past data .
Two families of methods compete. Estimate-then-optimize fits a regression of on and plugs it into the optimizer. Empirical risk minimization (ERM) and its "integrated" variants choose a policy directly to minimize the empirical decision cost. A widespread view holds that the integrated approach should win because it targets the decision cost. Hu, Kallus and Mao (arXiv:2011.03030, Management Science 2022) compare the two through their regret rates. Slow, noise-independent rates of order do not separate them. The separation appears under a margin (noise) condition controlling how often the problem is nearly dual-degenerate. This mission formalizes the paper's fast rate for ERM, Theorem 6.
Timeline. Margin conditions for classification go back to Mammen–Tsybakov (1999) and Tsybakov (2004); Massart–Nédélec (2006) obtained the corresponding fast rates for ERM over VC classes. El Balghiti, Elmachtoub, Grigas and Tewari (2019) gave slow generalization bounds for decision-focused losses in terms of the Natarajan dimension. Hu, Kallus and Mao (2020, revised 2021) proved the fast rate for ERM over policy classes of finite Natarajan dimension, a matching lower bound, and a faster rate for estimate-then-optimize.
The decision set is a polytope , nonempty, with on for some ; is its finite set of extreme points. The pair has , and . The optimal set at is .
A policy is a map . A data-driven policy maps a sample of i.i.d. draws to a policy, and its regret is
Given a class of policies, returns a member of minimizing .
The gap is the difference between the best value over suboptimal extreme points and the optimal value, set to when every point of is optimal. Assumption 2 (noise condition) with parameters requires
The Natarajan dimension of is the largest for which there are points and labels such that every pattern of choices between and is realized by some .
If Assumption 2 holds, , has Natarajan dimension at most , and contains an optimal policy , then for a constant depending only on ,
The constant is existential and uniform over all dimensions, polytopes, distributions, classes, and ; the goal fixes no numerical value.
With and :
Theorem 6 shows that the regret of ERM improves from to when the instance is rarely near dual degeneracy. With , the generic case when has a bounded density and is linear, the rate is . Theorem 7 of the same paper (mission 2 of this series) shows that the exponent is optimal for any method that uses only the policy class. Theorem 8 (mission 3) shows that estimate-then-optimize can reach , which is the paper's case against the conventional preference for integrated methods.
The result is proved in the paper; no machine-checked proof is known. Formalizing it adds a checked fast-rate theorem for a decision-focused learning method, a Lean statement of Bousquet's inequality in the form used throughout statistical learning theory, and a localized empirical-process bound for classes of finite Natarajan dimension.
The slow rate follows from uniform convergence of the empirical cost over . This argument cannot give more than : it bounds the deviation of every policy by the same worst-case amount, ignoring that near-optimal policies have small variance. The fast rate needs a variance–mean relation (Lemma 1, which is where the noise condition and the uniqueness assumption enter), a concentration inequality that exploits small variance (Lemma 2), and a localized complexity bound (Lemma 3), combined over shells of the class. Lemma 2 is itself a deep result whose known proofs go through the entropy method. Lemma 3 rests on chaining and on bounding the pseudo-dimension of the excess-loss class by the Natarajan dimension, neither of which is in Mathlib.
All declarations live in the namespace FastCLO.ERM. Conventions:
EuclideanSpace ℝ (Fin k). The polytope is a structure carrying , , , nonemptiness and the bound ; is the cardinality of Set.extremePoints, whose finiteness is a proof obligation, not a hypothesis.Measure.pi of .A statement in which the regret integrated the empirical cost instead of , or in which ERM minimized over a subset of the class, or in which the constant could depend on the instance, would be a different theorem; the Lean statements rule these out by construction.
Needed infrastructure: Bousquet's (or Talagrand's) inequality, symmetrization and Dudley chaining for empirical processes, packing bounds for classes of finite pseudo-dimension, and the Natarajan-to-pseudo-dimension reduction. These are reusable far beyond this mission; contributions of any of them are welcome.
The ferromagnetic Potts model assigns a larger weight to a coloring when more adjacent vertices have the same color. Computing its partition function is an approximate counting problem with connections to statistical physics and counting complexity. For three or more colors, Goldberg and Jerrum established #BIS-hardness of approximation on general graphs, and Galanis, Štefankovič, Vigoda, and Yang refined the hardness result for bounded-degree bipartite graphs Goldberg–Jerrum, Galanis et al.. These results make it useful to identify graph classes where the partition sum can still be approximated efficiently.
Jenssen, Keevash, and Perkins proved that edge expansion supplies such a class at sufficiently large inverse temperature. Their Theorem 3 gives an FPTAS and a polynomial-time sampling algorithm for the -color ferromagnetic Potts model on finite -expanders of maximum degree , when , , , and Jenssen–Keevash–Perkins. This mission records the mathematical reduction and the polymer convergence condition on which their algorithmic conclusion rests.
Let be a finite simple graph, let , and let . A coloring gives each vertex one of colors. Write for the number of edges whose endpoints receive the same color. The Potts partition function at inverse temperature is
For , its edge boundary consists of the edges with exactly one endpoint in . The graph is an -expander if whenever . The maximum-degree assumption means that each vertex has at most neighbors. All logarithms here are natural logarithms.
A color is a strict majority in when . Let be the Potts sum over colorings with that majority, and let . Because two colors cannot each occupy more than half the vertices, these sectors do not overlap. The monochromatic colorings are the model's ground states at positive .
A polymer is a nonempty vertex set for which the induced graph is connected and . Let be all edges with at least one endpoint in . Two polymers are compatible when the distance between every vertex of one and every vertex of the other exceeds one. In particular, overlapping or adjacent polymers are incompatible. With the Potts sum on the induced graph using the other colors, define
The sum includes the empty family. An -relative approximation to means Jenssen–Keevash–Perkins, Definitions 10–11.
The goal is the deterministic core of Theorem 3. For a nonempty -expander with the degree, color, and temperature bounds above, the explicit polymer expression approximates the Potts partition sum:
The error is the composition of the two -relative approximations in Lemmas 12 and 13; the paper does not print it as a separate constant. The same goal also asserts the Kotecký–Preiss condition, with the paper's decay function , for every polymer :
The milestone list follows the source's stated claims: Lemma 12 bounds the contribution outside the strict-majority sectors; Lemma 13 compares one sector with ; the weight bound controls individual polymers; Lemma 14 counts connected induced subgraphs containing a specified vertex; and displayed inequality (5) bounds the resulting per-vertex sum Jenssen–Keevash–Perkins, pp. 13–16.
The reduction makes a Potts partition sum on an expanding graph accessible through a finite polymer model whose weights have controlled decay. The Kotecký–Preiss condition is a quantitative convergence criterion for abstract polymer expansions Kotecký–Preiss. In this setting the two statements provide the mathematical hypotheses used with the algorithmic framework cited by the paper Helmuth–Perkins–Regts. Without the approximation, computing the polymer sum would not give a controlled Potts estimate; without the convergence condition, the cited framework would not apply at the stated temperature threshold.
The paper proves the mathematical and algorithmic results. This mission supplies Lean definitions and compile-checked statements, with proofs still to be formalized. A completed development would give reusable formal accounts of finite Potts sums, strict-majority sectors, graph edge expansion, polymer compatibility and weights, and the connected-set counting bound that the paper cites from Galvin and Kahn Galvin–Kahn.
The tempting approximation is to count only monochromatic colorings. That discards all nearby colorings, whose total weight matters even at low temperature. The polymer model retains connected deviations from a monochromatic coloring, but it also admits collections whose union is larger than half the graph. Controlling the weight of these extra configurations is part of the approximation statement. Separately, the convergence criterion sums over every polymer within distance one of a given polymer. A bound on one weight does not control that sum unless the number of connected vertex sets of each size is also bounded. These are the distinct estimates captured by Lemmas 12–14 and inequality (5) Jenssen–Keevash–Perkins, §3.
The Lean representation uses SimpleGraph V on a finite vertex type. Vertex sets are finite sets, the edge boundary counts each crossing edge once through its orientation from inside to outside, and polymer distance is extended graph distance, so disconnected components are infinitely far apart. Strict-majority colorings use ; expansion and polymers use the non-strict bound . The polymer weight uses the full incident-edge set and the induced Potts sum on colors. The empty compatible family contributes one to .
The vertex set is required to be nonempty in the goal and approximation lemmas: for , the strict-majority sum is zero while the Potts partition sum is one. Lemma 14 states because its printed bound is false for an isolated vertex with . The weight bound states , which is implied by the goal's threshold. These are the only additional domain pins. The stated goal uses the paper's exact , , and ; no free approximation value or freely chosen polymer family can trivialize it.
The algorithm and its running time are out of scope because this Mathlib environment has no machine model for the FPTAS and the paper uses unquantified big-O running times. The goal is the mathematical reduction and Kotecký–Preiss hypothesis consumed by Theorem 8. Contributions that establish the five milestone statements, the color-symmetry identity, or the combination of their bounds are useful; the finite graph and partition-sum definitions are reusable beyond this mission.
A random field on a sphere assigns a random value to every direction. Such fields appear when the underlying data are directional, including spherical models in spatial statistics and geophysics. The covariance of an isotropic field can be recorded by an angular power spectrum: one nonnegative number for each spherical harmonic degree. This changes the sample regularity question into a concrete spectral question. How fast must these numbers decay so that a realization is continuous, and how regular can that realization be? Lang and Schwab, 2015 give a sufficient summability condition and an exact range of Hölder exponents in their Theorem 4.5.
The question matters when a field is evaluated on a mesh or represented by finitely many spherical harmonics. A covariance function can be regular even when the original version of a random field has badly chosen values on null sets. The useful result is therefore the existence of one regular modification: at each fixed sphere point it agrees with the given field almost surely, while its sample paths are regular across the entire sphere. The paper treats this sample path result in §4, separately from its spectral characterization of covariance regularity in §3 and its later simulation and stochastic heat equation results.
Write for the unit sphere. Its geodesic distance is , the length of the shorter great circle arc between and . A random field is a jointly measurable map from a probability space times to the real numbers. A field is Gaussian when every finite collection of its values has a joint Gaussian distribution. Isotropy says that rotating all observation points together does not change that joint distribution. These are the conventions of Definition 2.1 in the paper.
For each degree , let be the Legendre polynomial normalized by , and let be its angular power. The field has a constant mean and covariance determined by :
Because , the same covariance is expressed by the distance kernel for . A modification of means almost surely for each fixed ; it need not agree on one common full measure set at every . The paper's Assumption 4.1, specialized to , asks for finiteness of .
For , the target is Theorem 4.5 of Lang and Schwab:
The same modification serves every eligible exponent. The result leaves the Hölder constant free to depend on the sample and the exponent, as it must.
The four milestones follow the source's statements and its proof order. The Legendre polynomial bounds on p. 16 lead to Lemma 4.2, for and . Lemma 4.3 transfers this to for every positive integer . Theorem 4.4 is a Kolmogorov–Chentsov theorem for any random field on : a moment exponent produces a continuous modification with every Hölder exponent below . The Gaussian and isotropic hypotheses belong to Lemma 4.3 and the goal; they are absent from Theorem 4.4.
The theorem provides a checkable bridge from a harmonic description of a field to sample path behavior. A practitioner can estimate or impose decay of the angular power spectrum, then know that a version of the field admits interpolation on the sphere with any exponent below . The endpoint is not asserted. The moment estimate and the spherical modification theorem can also be reused when studying fields produced by other models; in particular, Theorem 4.4 needs no Gaussian assumption.
The result was proved in the 2015 paper; this mission concerns its machine checked formalization. Mathlib supplies Gaussian process and measure theory interfaces, but the paper's sphere distance, Legendre normalization, angular kernel and spherical version of Kolmogorov–Chentsov must be connected. A platform goal for a Kolmogorov–Chentsov theorem on uses a different index space and hypotheses, so it does not cover the present milestone. The finished development will provide a reusable sphere indexed modification theorem as well as the paper's specific spectral criterion.
A bound on the covariance kernel controls the second moment of field increments, but it does not by itself supply one continuous version with a common pathwise regularity statement. The desired exponent concerns values at uncountably many points, whereas the definition of modification gives an almost sure equality separately at each point. The gap is visible even for simple processes: changing a field at one random location can preserve each fixed point's law while destroying continuity of individual paths. The sphere also carries a two dimensional geodesic metric, so a one dimensional modification theorem indexed by time cannot be substituted without a new argument.
Lean represents as the unit metric sphere in three dimensional Euclidean space. Coordinates have indices for the paper's . All regularity statements use , not the subtype's chord distance. Rodrigues' formula defines , and the kernel is a real infinite sum with its factor . The spectrum is nonnegative and has as part of the field model, matching the finite variance convention used in §2. The covariance formulation allows a nonzero constant mean: Theorem 4.5 does not require centering.
The moment inequalities use extended nonnegative integrals, avoiding a default zero for nonintegrable real integrals. The paper's positive integers are expressed with an explicit because Lean's naturals include zero. Real powers follow the usual convention: the degree zero term of is zero when . On compact , local Hölder continuity gives a global constant for each path and exponent. Exceptional sample paths may be redefined, so the formal conclusion states continuity and Hölder regularity for every sample of the chosen modification. The modification retains pointwise almost sure agreement and measurable evaluations; omitting agreement would make the goal trivial.
Contributions can address Legendre inequalities, covariance and Gaussian moment calculations, and a general Kolmogorov–Chentsov theorem for compact manifolds. The latter is reusable beyond this paper. The auxiliary Legendre and kernel definitions are also available to later spherical field missions.
Stochastic partial differential equations on the sphere model quantities that live on the surface of the Earth or of the sky and are perturbed by spatially correlated noise: temperature anomalies, geophysical fields, fluctuations of the cosmic microwave background. The simplest such model is the stochastic heat equation on the unit sphere with additive isotropic noise. Because the noise is isotropic and the Laplace–Beltrami operator is diagonal in the spherical harmonics, the equation decouples into one scalar Ornstein–Uhlenbeck equation per harmonic, and the solution can be simulated exactly in law by truncating its spherical-harmonic expansion at a degree . The practical question is how fast this spectral truncation converges, in mean square and along a single simulated path.
A. Lang and Ch. Schwab answer this in §7 of Isotropic Gaussian random fields on the sphere: regularity, fast simulation and stochastic partial differential equations (arXiv:1305.1170v3, Ann. Appl. Probab. 25(6), 2015). Their rates are expressed through the decay of the angular power spectrum of the noise, the same quantity that governs the sample regularity and the Karhunen–Loève truncation of isotropic Gaussian random fields in the earlier sections of the paper.
Let be the unit sphere with surface measure (total mass ) and the real square-integrable functions with norm . The spherical harmonics , , , are built from the Legendre polynomials ; the functions , , () form a real orthonormal basis of the degree- harmonics, on which the Laplace–Beltrami operator acts as multiplication by , .
On a probability space let (, , ) be independent real Brownian motions, and let , , be an angular power spectrum. The isotropic -Wiener process is
The stochastic heat equation is
Its solution is with
and the spectral approximation is . The norm measures random fields. The standing assumption of §7 is the decay condition
For every and every , almost surely
The goal fixes no constant; only the exponent enters, so it survives any improvement of the constants below.
Corollary 7.3 is the pathwise convergence rate of the spectral method for the stochastic heat equation on the sphere: a single simulated path of the truncated series is within of the true path in for all large , for any . Combined with the exact-in-law recursion on a time grid (pp. 36–38), it says that the only source of error in simulating this SPDE is the spectral truncation, and that the rate is governed by the decay exponent of the noise spectrum alone, with sufficing (no trace-class condition is needed, thanks to the smoothing of the heat semigroup). The mean-square and estimates of Lemmas 7.1 and 7.2 are the quantitative inputs; the bound for all is what makes a Borel–Cantelli argument possible.
The results are proved in the paper; none of them, nor the stochastic heat equation on the sphere, nor spherical harmonics, has a machine-checked formalization on the platform or in Mathlib. The work here is to formalize the known proof. Two printed statements need correction (see Formalization scope); the milestones state the bounds that the paper's proofs establish.
The obvious argument writes as the tail of the series, splits it into the damped initial condition and the noise, and bounds each. The noise part is a Gaussian random field whose angular power spectrum decays like , so its truncation error is controlled by the corresponding estimates for isotropic Gaussian random fields (Proposition 5.2 and Theorem 5.3 of the paper), which must be re-derived here. Several steps have no current library support: the Wiener integral of a deterministic integrand and its Gaussian law, orthonormality and completeness of the spherical harmonics in , moment equivalence for Gaussian vectors in a Hilbert space (to pass from to all ), and the passage between the pointwise series and its limit. The initial-condition tail decays like but not uniformly as , which is exactly why the printed "uniformly in time" bounds fail and why every statement takes fixed.
Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1 with coordinates indexed (the paper's ); is the measure toSphere of Lebesgue measure, of mass . Spherical harmonics are written in Cartesian form, , which is the paper's function also at the poles. For real the projection is written in the real orthonormal basis.IsBrownianReal processes on , independent as a family of path-valued random variables. The stochastic convolution is defined pathwise as , which equals the Wiener integral almost surely (integration by parts; a.s.). This is the one place where a stochastic integral is replaced by a pathwise expression.Many insurance benefits depend on a policyholder's health or membership state rather than simply on being alive or dead. A disability annuity pays while a life occupies a disabled state; a critical illness or death benefit may be triggered by moving from one state to another. A rigorous multiple-state valuation therefore distinguishes payments for occupying a state from payments for a transition between states, and must also specify the timing of the payments.
The discrete-time models in Promislow, Fundamentals of Actuarial Mathematics, third edition, Chapter 19 §§19.2.1–19.2.3 [1], provide these two actuarial payment categories. Dickson, Hardy and Waters, Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 8 [2], develop related multiple-state assumptions, transition probabilities, premium values and policy values. Norris, Markov Chains, §1.1 [3], supplies the finite-state stochastic-matrix foundation.
This mission develops the corresponding finite-horizon present-value formulas. It is the cashflow extension of the finite-state transition algebra in Mission X, but is designed as a self-contained draft while Mission X's definitions remain unpublished. The key mathematical obligations are correctly weighted transition benefits, state occupation annuities, finite-state distribution propagation, homogeneity and a capstone valuation decomposition.
Let be a finite set of insurance states. At the start of policy year , let represent the probability of state , and let be the conditional probability of occupying state at the end of the year, conditional on state at its start.
A state distribution must satisfy
A valid one-year transition kernel has nonnegative entries and rows summing to one:
The next year's marginal state distribution is obtained by propagating the current distribution through that kernel:
The supporting theorems show that nonnegativity and total probability are preserved by this operation. The transition kernels are allowed to change from one year to the next. A separate path-space process need not be constructed to establish these finite-sum valuation identities, but and must obey the propagation relationship to represent one coherent Markov insurance model.
Let be the payment made at the beginning of policy year to a contract then occupying state . For example, it could represent a disability annuity paid only while the person is disabled. The expected amount at that payment time is
The expected present value of the state-occupation cashflows over policy years is
A payment due at time zero is not discounted. A constant amount paid irrespective of state has its own expected value unchanged because the marginal state probabilities add to one. This is consistent with the state-occupation cashflow structure in [1, §19.2.3, equation (19.6)].
Let be the benefit payable at the end of policy year when the contract transitions from state to state over that year. The expected one-year amount is
The contract's expected present value of those transitions is
Unlike a reward depending only on the destination state, a transition-specific benefit may distinguish, for example, from . Keeping the pair explicit is necessary to represent such insurance benefits. This is the payment timing and transition structure considered in [1, §19.2.2, equations (19.2)–(19.4)].
The mission defines the complete finite-horizon value by adding the two types of cashflow:
Because finite sums are linear, scaling both monetary benefit schedules by a constant scales the entire expected present value by :
The capstone combines decomposition of the occupation and transition components with this scaling principle. Related milestones establish the zero-year, zero-benefit and one-year limits. For a one-year contract the exact timing reduces to
The displayed formula is deterministic expected-value algebra for finite state probabilities, rather than a claim about a pathwise cashflow random variable. The later development of a stochastic path-space model, conditional benefits and second moments remains a separate task.
The proposed Lean draft contains five definitions: a finite-state probability distribution, one-step distribution propagation, expected transition-stage reward, expected occupation-stage reward and the combined finite-term PV. Thirteen supporting theorems prove probability propagation, zero and constant payments, scaling, valuation decomposition and the one-year boundary. The final capstone packages the overall value decomposition and benefit scaling.
The formal theorem statements do not require the cashflow amounts to be nonnegative because their linearity is algebraic. Probability interpretation additionally requires legitimate state probabilities and transition kernels. The source explicitly avoids interpreting arbitrary arrays and as the marginals of one Markov chain unless they satisfy the propagation identity.
These declarations are proposed mathematical obligations, not accepted proofs. Individual Lean modules import only the definitions their statements actually use, with all imports before Lean commands. Because the local definitions are not yet published as importable Prove2Me modules, downstream theorem previews must be revisited after their definitions are confirmed and published.
[1] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, Chapter 19, Multi-state Models, §§19.2.1–19.2.3. Equations (19.2)–(19.4) address transition-based insurance benefits and equation (19.6) addresses occupation-based annuity benefits.
[2] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 8, Multiple State Models, especially §§8.3–8.7 on states, transition probabilities, premiums and policy values.
[3] Norris, J. R. (1997), Markov Chains, Cambridge University Press, Chapter 1, §1.1 on stochastic matrices and discrete-time transition probabilities. The matrix-multiplication setting here permits different kernels at successive durations, in line with Promislow's non-stationary treatment.
Prospective policy reserves measure the expected present value of an insurer's remaining benefits less remaining premiums, per policy still in force at a valuation date. When premiums and benefits occur at annual dates, consecutive reserve values satisfy a one-year cashflow balance. That recursion is central to valuation systems, reserve roll-forwards and the decomposition of a life insurance premium into risk and savings components.
This mission develops the annual net premium reserve recursion for a finite-term life assurance. It builds on the conceptual framework of prospective policy values without importing unconfirmed declarations from earlier Prove2Me missions. The principal actuarial sources are Gerber, Life Insurance Mathematics, third edition, Chapter 6 §6.3, notably equation (6.3.4) [1], and Dickson, Hardy and Waters, Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 7 §7.3.3 [2]. Both develop the balance between an opening reserve, the premium due and the expected benefit plus closing reserve.
A key objective is correct treatment of impossible conditional events: the aggregate expected-loss recursion does not require next-year survival to have positive probability, while the familiar conditional-reserve formula needs the next year's reserve to be defined for an in-force life.
Let be measurable curtate lifetime under a probability measure . Fix the contract term , integer valuation date , deterministic annual discount factor , death benefit and level premium . The insurer receives a premium at the start of each policy year for which . If , it pays the death benefit at the end of policy year , at calendar time .
The realised present value of the remaining net insurer loss, evaluated immediately before the time- premium, is
The date- premium appears in this expression and is worth one unit before multiplying by . Premiums earned before are excluded. The cashflow has finite calendar horizon even if the lifetime distribution is unbounded.
Define the probabilities of being in force, dying during the following year and surviving one further year by
The event partitions into two disjoint events, and , so
When , conditional annual death and survival probabilities are
No annual death-event independence assumption is made. The result follows directly from the disjoint partition of a natural-valued lifetime.
For , the future loss satisfies the pointwise identity
If the person dies in year , the current premium is collected and the discounted death benefit becomes due. If the person survives, the one-step-discounted continuation accounts for all remaining premiums and the eventual death benefit. Before the start of the contract's surviving period, all relevant terms vanish.
Taking expectations and using integrability of the finite-term cashflow gives the unnormalised recurrence
This identity remains meaningful when , because the future loss at is zero almost surely in that case. It is the safest formulation to prove before dividing by survival probabilities.
For , define the prospective reserve per policy in force at time as
The Lean definition uses ordinary real division, which is totalised at zero, but the actuarial interpretation above is asserted only under a positive survival-probability assumption. If both and , substitute and into the aggregate identity. Division by yields
The equation is the classical annual reserve balance: opening reserve plus premium equals the expected discounted claim and next-year reserve. Gerber [1, §6.3] also develops its decomposition into risk and savings premiums. This mission targets the core recursion and its probability and integrability prerequisites, rather than treating that later decomposition as already formalised.
The death-certain boundary is not hidden under a fictitious conditional reserve at . The aggregate identity above applies directly. A later extension can derive the explicit terminal conditional formula from it while preserving the zero-probability interpretation.
The draft introduces four definitions: the realised remaining loss, the in-force survival mass, death-year mass and prospective reserve quotient. Its twelve supporting theorems establish maturity and inception boundaries, the survival-event partition, conditional death/survival probabilities, loss integrability, the pointwise and integrated one-year recursions, reserve normalisation and the conditional reserve identity. A capstone combines the probability identity with the annual reserve recursion.
For , no covered future cashflow remains. At , , so the reserve is the unconditional expected loss at issue. The principal recursions allow any fixed real ; the usual insurance interpretation adopts a nonnegative discount factor. The proof obligations are finite-horizon and do not require a maximum possible lifetime.
The items are proposed Lean statements rather than accepted proofs. Their modules are dependency-ordered, with imports only at the beginning of each file. Until the supporting definitions have been individually published, downstream proof targets which import their modules must not be represented as ready for successful standalone compilation.
[1] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, §6.3, Recursions, especially equations (6.3.4)–(6.3.10) and the premium risk/savings interpretation. Springer book DOI.
[2] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 7, Policy Values, §7.3.3, Recursive formulae for policy values. This chapter explicitly develops one-year annual policy-value recursions and related annual profit calculations.
[3] Open Actuarial Textbooks Project, Life Contingencies: Basic Life Contingent Benefits, Chapter 3, for the curtate-lifetime timing conventions used in the finite death-benefit and premium cashflows.
Life-contingent benefits may depend on more than whether an insured life is alive or dead. Disability, recovery, critical illness and multiple causes of exit can all be represented by finite sets of states with possible transitions between them. Multiple-state models make it possible to value benefits on a transition, annuities paid while occupying a state, and different amounts payable according to the insured's health or other status. Dickson, Hardy and Waters develop the actuarial multiple-state setting in Actuarial Mathematics for Life Contingent Risks (2009), Chapter 8 [1]. Promislow presents a discrete-time, potentially non-stationary Markov model and its insurance and annuity applications in Fundamentals of Actuarial Mathematics (2015), §§19.2.1–19.2.3 [2].
This mission establishes the finite-state, discrete-time algebra needed before tackling more difficult continuous-time transition intensities, differential equations or multistate reserves. The capstone connects composition of transition matrices with discounted state-dependent cashflows. The mathematical emphasis is on correct probabilities, annual timing and finite sums.
Let be a nonempty finite set of possible policyholder states. For one policy year, define as the probability of ending the year in state , conditional on starting in state . To represent a genuine transition kernel it must satisfy
The model allows a different transition matrix in each year. It does not assume a constant transition law or that every state can reach every other state. For two successive policy years, with transition kernels and , the two-step transition probability is
The intermediate state is summed out. This is the finite Chapman–Kolmogorov composition used in the non-stationary discrete Markov chain of [2, §19.2.1]. The proof must show that composing two nonnegative row-stochastic kernels produces another nonnegative row-stochastic kernel. Associativity,
then permits an arbitrary finite sequence of yearly transition matrices to be grouped without changing the resulting transition probabilities.
The matrix calculations alone are not a theorem asserting that an arbitrary stochastic process has the Markov property. They formalise the transition-probability algebra assuming the yearly probabilities are the kernels of a Markov model. Proving a full path-space conditional-probability construction is outside this mission.
Suppose an annual payment depends on the state occupied after the next transition. Write for the amount paid at the next year end when the new state is , and for the continuation value at that date. Let be the deterministic one-period discount factor. The one-step prospective value in current state is
Both and are measured at the next year end, so this formula applies precisely one period of discounting to both. A constant amount paid at the next year end has value , by the row-sum property. The valuation operator is linear in reward and continuation cashflows, and it is nonnegative when the discount factor, transition probabilities and cashflows are nonnegative.
For a payment arising only at the end of the second year, the two-stage recursion simplifies to
This identity reconciles backward valuation with forward transition-probability composition. It is the discrete precursor to larger actuarial valuation and reserve recursions. Promislow's §§19.2.2–19.2.3 discuss state- and transition-dependent insurance and annuity cashflows [2].
When the discount factor is zero, a payment made only at the next year end has zero present value. When all future rewards and continuation values are zero, the valuation is zero. Neither algebraic identity requires a particular health-state interpretation.
The theorem graph uses a finite state type and sums over all states. A true actuarial example must supply valid transition probabilities, distinguish payments made on entering a state from those made for occupying the state, and preserve the timing of an insurance payment at the end of the year. No independence between annual state indicators is assumed. Multistate variance calculations need joint transition probabilities rather than naively treating indicators as independent [2, §19.2.2].
The mission creates three definitions, twelve supporting theorems and one capstone. The proof path begins with row normalisation and nonnegativity, proves composition and associativity, and then develops constant, zero, linear and two-step discounted reward identities. The capstone combines the preservation of a stochastic kernel, associative composition and the two-step reward valuation.
These are proposed Lean theorem statements, not claims of completed proofs. This draft uses Mathlib's finite-sum and elementary order algebra, with no reliance on unpublished actuarial mission definitions.
[1] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Cambridge University Press, Chapter 8, Multiple State Models, especially §§8.2–8.4. This provides the actuarial interpretation of state transitions and the Markov modelling assumptions.
[2] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, ISBN 9781118782460, Chapter 19, Multi-state Models, §§19.2.1–19.2.3. The discrete non-stationary transition model and subsequent state-dependent life insurance and annuity examples are the direct cashflow motivation.
[3] Norris, J. R. (1997), Markov Chains, Cambridge University Press, §1.1, Definition and Basic Properties. The book defines a stochastic matrix by its probability-distribution rows and states Theorems 1.1.1–1.1.3 on the Markov property and powers of the transition matrix. Its basic homogeneous-chain construction is a supporting special case, not an assertion that the time-varying matrices in this mission are all equal.
A net premium is usually set at policy inception. As an insured life survives and the remaining insurance term shortens, the expected future claim outgo and future premium income change. A prospective policy value measures the expected present value of the insurer's future loss on a policy that is still in force at the valuation date. This is the natural next stage after the equivalence principle of Actuarial Mathematics VIII. Dickson, Hardy and Waters provide the insurer's future-loss definition and the annual-cashflow policy-value framework in Actuarial Mathematics for Life Contingent Risks (2009), Chapter 7, §§7.3.1–7.3.3 [1]. Promislow covers both deterministic reserve recursions and the stochastic approach to reserves [2].
This mission formalises a finite-term life-assurance reserve at an integer valuation duration. Its central feature is survival conditioning: the reserve is a liability per surviving in-force policy, rather than the unconditional present value of the original contract. Separating these quantities avoids a common modelling error in stochastic policy values.
Let be measurable curtate future lifetime under a probability measure . Let denote the term, the valuation duration, a fixed per-period discount factor, the death benefit and the annual level premium.
Premiums are payable in advance at integer times while the life is alive. The benefit, if payable, occurs at the end of the year of death, at date . Only cashflows on or after duration enter the reserve, with discount exponents measured from .
The in-force survival event is
When , conditioning on this event gives the valuation basis for policies in force at . A statement about reserves conditional on survival must not silently assume that .
The remaining unit term-assurance benefit present value is
The remaining premium-annuity present value is
The realised future net loss is therefore
These finite expressions make it explicit whether a premium due at the valuation instant is included. Here is immediately before the premium at time , consistent with an annual premium payable in advance. The choice is essential when comparing reserve formulas across valuation conventions.
At the in-force event is certain. At or after , both remaining cashflow components vanish because the contract's coverage and premium period have ended.
For positive survival probability, the prospective term-policy reserve per in-force policy is
The second equality holds because the model defines the realised future loss as zero outside . It is a conditional-event expectation, rather than an unrestricted claim about conditional expectation with respect to an arbitrary sigma-algebra. The formal quotient definition makes the denominator explicit, and the principal reserve interpretation and capstone theorem retain as a hypothesis.
Linearity separates the reserve into benefit and premium components:
In particular, multiplying both cashflow amounts by gives
The finite payment period ensures integrability for any fixed real discount factor. When studying economic reserve properties, a nonnegative or positive discount factor can be imposed separately. No assumption of independence between survival indicators, benefits and premiums is made.
The principal boundary checks are survival at inception, ; exhaustion of cover at ; finite sums with ; and zero in-force probability. The total real-valued quotient happens to evaluate to zero when both its numerator and denominator are zero in Lean, but this does not create an actuarially meaningful conditional reserve for an impossible in-force event. The descriptive and main conditional theorems are explicitly scoped to positive probability.
Five definitions provide the in-force event, future benefit PV, future premium PV, future loss PV and the prospective reserve. Supporting theorems develop survival-event measurability, cashflow boundaries, nonnegativity where applicable, integrability, inception valuation, benefit–premium decomposition and scaling. The capstone combines the survival-normalised expected-loss identity, valuation decomposition and scaling.
The formalisation is deliberately self-contained at the level of future cashflow definitions so the owner Draft does not depend on the unconfirmed publication of any Mission VIII declarations. The intended later bridge is an exact identity between the duration-zero future loss and the loss-at-issue formula from Mission VIII, once those definitions are published. All theorems are proposed proof targets, not assertions of accepted proofs.
Gerber [4, §§6.3 and 6.5] provides an independent treatment of net premium reserves and annual reserve recursions. Its equation (6.5.6) expresses a whole-life net reserve through the premium difference, illustrating the same prospective viewpoint but not asserting the more general term-reserve theorem of this mission.
[1] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 7, Policy Values, Cambridge University Press. Relevant sections: §7.3.1 (future loss), §7.3.2 (policy values for annual cashflows) and §7.3.3 (recursive policy values), printed pages 176–195.
[2] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, ISBN 9781118782460. In particular §6.3 (reserve recursion) and §15.5 (stochastic reserves).
[3] Dickson, Hardy and Waters (2009), Chapter 6, §6.5.1, equation (6.1), on the equivalence principle at policy inception, publisher book record.
[4] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, Net Premium Reserves, §6.3 and §6.5, including the premium-difference reserve formula (6.5.6).