Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Twin-width is a graph and matrix invariant introduced by Bonnet, Kim, Thomassé and Watrigant (J. ACM 69(1), Article 3, 2021). Classes of bounded twin-width include bounded tree-width and clique-width graphs, proper minor-closed classes, posets of bounded width, and permutations avoiding a fixed pattern; on all of them, first-order model checking is fixed-parameter tractable once a contraction sequence is given. The difficulty in applying this framework is to bound twin-width for a concrete class, because a contraction sequence is an intricate object.
Section 5 of the paper supplies the tool that makes such bounds routine: the Grid Minor Theorem for twin-width (Theorem 5.4). It reduces bounding twin-width to finding an order of the rows and columns of a matrix (for a graph, an order of its vertices) in which no large mixed minor appears. The paper then uses it for pattern-avoiding permutations, posets of bounded width and -minor free graphs (Section 6, Table 1). The argument is modelled on the proof of the Stanley–Wilf conjecture by Marcus and Tardos (JCTA 107, 2004) and on its use by Guillemot and Marx for permutation pattern matching (SODA 2014).
Timeline. Füredi and Hajnal (1992) conjectured a linear bound on the number of s in a -matrix avoiding a permutation pattern. Marcus and Tardos (2004) proved it, with constant , via -grid minors. Fox (arXiv:1310.8378) improved the constant to , and Cibulka and Kynčl (arXiv:1607.07491) to . Guillemot and Marx (2014) built from the grid structure a decomposition of permutations; Bonnet et al. (2020 preprint, 2021 journal) generalized it to arbitrary matrices over a finite alphabet, which is Theorem 5.4.
Let be an matrix with entries in a finite alphabet of size . For sets of rows and of columns, the zone is the submatrix on those rows and columns; it is constant if all its entries are equal.
A partition of is a pair of a partition of the rows and a partition of the columns. Its error value is the largest number, over all parts (respectively ), of parts of the other side forming a non-constant zone with it. A contraction sequence is a sequence of partitions starting from the finest one (all singletons), ending at the coarsest one (one row part, one column part), each obtained from the previous by merging two row parts or two column parts. has twin-width at most , , if some contraction sequence has error value at most throughout.
A division is a partition whose parts consist of consecutive indices. is -twin-ordered if it has a contraction sequence of error value at most consisting of divisions.
A zone is vertical if its rows are all equal, horizontal if its columns are all equal, and mixed otherwise. A -mixed minor is a division into row intervals and column intervals all of whose zones are mixed; is -mixed free if it has none. For -matrices, a -grid minor is such a division in which every zone contains a . Finally .
For :
$$M\ \text{-twin-ordered}\ \Longrightarrow\ M\ \text{-mixed free},
t\ge1,\ M\ \text{-mixed free}\ \Longrightarrow\ \operatorname{tww}(M)\le 4c_t,\alpha^{4c_t+2}.$$
The constant is the one the paper's proof produces; the paper's summary is not formalized.
Theorem 5.4 characterizes bounded twin-width of matrices, up to the order of rows and columns, by the exclusion of a mixed minor. Its second item is used in Section 6 of the same paper to show that -minor free graphs, posets of bounded width and pattern-avoiding permutations have bounded twin-width, and in later papers of the twin-width series as the standard route to twin-width upper bounds. Without it, each such bound needs its own explicit contraction sequence.
The result is proved in the paper; no machine-checked proof of it exists in Mathlib or on the platform. The mission produces a machine-checked statement and, once solved, a proof of the grid theorem with its explicit constant, a formal treatment of contraction sequences of matrices, and a statement of the Marcus–Tardos theorem with the Cibulka–Kynčl constant, which is itself absent from Mathlib.
The first item is comparatively short. The second item is where the work lies. The natural first idea — contract greedily as long as the error value stays below a bound depending on — does not work: the error value is not monotone under fusions, and nothing in the absence of a mixed minor directly prevents a greedy sequence from getting stuck with large error. Any proof has to identify a quantity that is monotone under fusion and is bounded by a density argument, and then turn a sequence controlled by that quantity into a contraction sequence of bounded error value; the paper's choices (mixed value, Lemmas 5.6 and 5.7) are the milestones. The density argument rests on the Marcus–Tardos theorem with an explicit single-exponential constant, a substantial combinatorial result in its own right and not available in Mathlib.
Matrices are Matrix (Fin n) (Fin m) A with [Fintype A], and is Fintype.card A. Partitions are Mathlib Finpartitions of univ; the finest is ⊥, and "coarsest" means at most one part. Twin-width is the partition form of p. 3:18, as a predicate MatTwinWidthLE M t with exactly one merge, of rows or of columns, per step; it is never an infimum over a possibly empty set. Divisions in minors are given by strictly increasing cut points , so all parts are non-empty. Vertical and horizontal mean "all rows (columns) of the zone agree". Grid minors use Bool entries. Since is not an integer, is a real power, and the bound is ; the mixed-value bound of Lemma 5.7 is .
Hypotheses added relative to the page: in Theorems 5.3, 5.4 and Lemma 5.7; in the second item of Theorem 5.4, in Theorem 5.3 and in Lemma 5.7, since for every non-empty matrix is vacuously -mixed free and the bound would be false; in the row-type count. Theorem 5.3 is stated with the explicit constant that the paper quotes and uses, not as a bare existence statement.
The statements are not trivializable by the usual routes: twin-width is not a junk infimum, a contraction sequence cannot jump to one part in a single step, the error value counts non-constant zones per part on both sides, minors range over divisions with non-empty interval parts rather than arbitrary partitions, and all bounds depend only on and , never on .
A complete development needs: finite partitions and their merges, divisions as interval partitions, the Marcus–Tardos theorem, and bookkeeping for sequences of partitions. The partition machinery and Theorem 5.3 are reusable beyond this mission (graph twin-width in the other missions of this series, pattern avoidance). Proofs of individual milestones, and of the Marcus–Tardos theorem from its original argument, are welcome.
Training a neural network means running a first-order method on a loss that is built from compositions of elementary operations, many of them nonsmooth: ReLU, max-pooling, absolute values, sorting, norms. The gradient the optimizer uses is not computed by hand. It is computed by automatic differentiation (autodiff), most often in its reverse mode, backpropagation, which applies the chain rule of calculus operation by operation. When every operation is smooth, the output is the gradient. When some are not, each nonsmooth operation is assigned some "derivative" at its kinks (for ReLU at , typically ), and the chain rule is applied anyway. The result is in general neither a gradient, nor a Clarke subgradient, nor an element of any classical subdifferential: the classical subdifferentials do not satisfy the chain rule that autodiff applies.
Bolte and Pauwels (TSE Working Paper 1044, 2019; Mathematical Programming, 2021) introduced conservative set-valued fields to give these outputs a meaning. A conservative field is a set-valued map whose circulation along every closed path vanishes, exactly as for a gradient field. It obeys a chain rule along absolutely continuous curves. This mission formalizes the paper's Theorem 8: forward-mode and reverse-mode automatic differentiation, run with conservative fields for the elementary operations, return a conservative field for the composed function. The companion mission of this series formalizes the paper's Theorem 1, that a conservative field equals the gradient of its potential almost everywhere.
Write for Euclidean space and for a set-valued map, assigning a subset to every point. A path is absolutely continuous, with derivative for almost every .
A conservative field (Definition 1) is a set-valued map with closed graph and nonempty compact values such that for every absolutely continuous loop () the circulation is Lebesgue integrable with integral . A function is a potential for , or is a conservative field for (Definition 2), if is conservative and for every absolutely continuous path from to . A map is a conservative mapping for (Definition 4) if, along every absolutely continuous curve , for almost every , for all .
An evaluation program (§5.1) has inputs and intermediate nodes . Node has a tuple of distinct earlier nodes and an elementary function . Algorithm 1 sets for and returns . Each comes with a conservative field (property (d)). Given a choice for every :
The autodiff fields are and , the sets of outputs of Algorithm 2 and Algorithm 3 over all choices at .
If every is a locally bounded conservative field for , then
"Conservative field for " is meant in full: closed graph, nonempty compact values, zero circulation and the potential identity.
Theorem 8 says what backpropagation computes on a nonsmooth program: an element of a conservative field of the function, a set that behaves like a gradient along curves. This is what lets the paper's later results apply to deep learning: stochastic subgradient methods driven by such outputs converge, for definable losses, to points that are critical for the conservative field. It is also the reason why spurious outputs of autodiff (a nonzero "derivative" of a function that is identically zero) are harmless: by the companion Theorem 1 they occur only on a Lebesgue null set.
The result is proved in the paper, and nothing here is open. To our knowledge none of it has been machine-checked: there is no formal account of conservative fields, and the existing formalizations of backpropagation treat smooth layered networks only. This mission produces a formal model of evaluation programs and of both autodiff modes, a formal chain-rule calculus for conservative mappings (Lemmas 2–5), and the theorem itself. Formalizing it exposed three points the printed text leaves to the reader: the overwriting update of Algorithm 3, the nonempty-values hypothesis missing from Lemma 2, and the local boundedness that Theorem 8 needs (see Formalization scope).
The obvious argument is "autodiff applies the chain rule, and conservative fields satisfy the chain rule". The chain rule along curves (Lemmas 3–5) only gives the derivative identity of Definition 4 for each element of . It does not give the set-valued properties of Definition 1. Passing back to a conservative field (Lemma 2) needs to have closed graph, nonempty compact values and local boundedness. These depend on how the sets vary with through the forward pass, and they fail without local boundedness of the . Lemma 2 relates an integral identity along every path to a pointwise almost-everywhere identity, and both directions involve the measure theory of absolutely continuous curves that Mathlib supports only in part. The equality of reverse and forward modes is linear algebra, but the two algorithms traverse the graph in opposite orders, and the printed reverse update is not the one the equality needs.
is EuclideanSpace ℝ (Fin n), and the conservative-field layer is polymorphic in the dimension: each lives on . A path is a function ℝ → ℝ^n that is AbsolutelyContinuousOnInterval on , with = deriv γ. Definitions 1–2 require the circulation to be interval-integrable, because Lean integrates a non-integrable function to . Definition 4 and the chain rule (5) assert HasDerivAt, not an equation for deriv, so they cannot hold by default at points of non-differentiability. Nodes are Fin q, numbered from . Parent tuples are duplicate-free lists of smaller nodes, and input nodes have none.
and range over all admissible choices. A single fixed choice would give a map that is not a conservative field in general, and the formal statement does not use one.
Deviations from the printed text, each recorded with its item:
Theorem numbers and pages are those of the TSE Working Paper 1044 (October 2019), the version this mission cites. The journal version is typeset differently.
The conservative-field definitions duplicate those of the companion mission and are meant to be merged with them. Contributions are welcome at every level: Lemma 2 and Lemmas 3–5 form a reusable nonsmooth chain-rule calculus, and the reverse-equals-forward identity is a standalone statement about backpropagation that holds for arbitrary weights.
Many stochastic dynamic programs in operations research, such as inventory control with partially observed demand or the pricing of American options, are too large to solve exactly. A heuristic policy gives a lower bound on the optimal expected reward; to judge whether it is good enough one needs an upper bound. Brown, Smith and Sun (Oper. Res. 2010) build such bounds by information relaxation: let the decision maker see more than she would in reality, and charge a penalty for using the extra information. The construction generalizes the martingale duality for optimal stopping of Haugh and Kogan (Oper. Res. 2004), Rogers (Math. Finance 2002) and Andersen and Broadie (Manage. Sci. 2004).
In applications, the analyst chooses both the relaxation and the penalty, trading the quality of the bound against the cost of computing it. Proposition 2.3 of the paper collects four properties that govern this choice. The first is the subject of this mission.
Uncertainty is a probability space , and decisions are made in periods . The natural filtration records what is known in each period, with . An action sequence is , chosen from feasible sets . Period rewards are -measurable random variables and the total reward is .
A policy is a map from outcomes to feasible action sequences. It is adapted to a filtration if the period- action is -measurable; denotes these policies. A filtration with for all is a relaxation of , written . A penalty is a function ; it is dual feasible if for every . For any relaxation and dual feasible , the dual bound
is at least the optimal value (weak duality, Lemma 2.1).
The paper's main source of penalties is Proposition 2.2. Given generating functions depending only on , set
Such a penalty has zero mean along every nonanticipative policy, and its dual bound is computed by the backward recursion (10), the Bellman recursion with rewards and conditional expectations given .
For filtrations and one common sequence of generating functions , let be the Proposition 2.2 penalty of . Then
With a common generating function, a looser relaxation gives a weaker bound.
Milestone 1 is on the goal's path; milestones 2–4 are the remaining parts of the same proposition.
Proposition 2.3(i) tells the analyst how to read a weak bound. If a cheap generating function (for instance , the zero penalty) gives a satisfactory bound under some relaxation, it will give a bound at least as tight under any less informative relaxation that still contains ; conversely, moving to a looser relaxation without improving the generating function can only weaken the bound. Part (ii) is a continuity statement: penalties close to the ideal penalty give bounds close to the optimal value. Part (iii) permits the subtracted conditional expectation to be computed under an intermediate filtration, which the paper uses when volatility is unobserved in its option-pricing example. Part (iv) is the justification for estimating penalties by nested simulation, as in the methods of Haugh–Kogan and Andersen–Broadie: unbiased estimates yield valid, if weaker, upper bounds.
The results are proved in the paper's electronic companion. To our knowledge none of them, nor the information-relaxation duality framework itself, has a machine-checked proof. Formalizing them requires a usable theory of policies adapted to a filtration, penalties evaluated along random action sequences, and backward recursions with conditional expectations, all of which are reusable for other duality results in stochastic dynamic programming.
The obvious argument for (12) compares the two suprema policy by policy: . This fails, because the two bounds use different penalties: for a fixed -adapted policy, and need not agree, so the larger policy set alone does not order the bounds. The penalty changes with the relaxation exactly so as to remove part of the value of the extra information, and the statement asserts that it never removes more than that information is worth. Even the representation (10) of a dual bound by a backward recursion is nontrivial: it requires near-optimal actions to be selected measurably in every period.
In Lean, the further difficulty is the composition of an action-indexed family of conditional expectations with a random action: , where each is only defined almost surely. Countability of the action set is what makes this composite well defined up to null sets.
Periods are Fin (T + 1); an action sequence is a function Fin (T + 1) → X for one countable action type X with the discrete σ-algebra (the disjoint union of the per-period action sets). Filtrations are Mathlib Filtrations of the ambient σ-algebra; a relaxation is 𝔽 ≤ 𝔾. Policies are maps Ω → (Fin (T + 1) → X) with values in the feasible set, adapted when each action is measurable for the corresponding σ-algebra. Conditional expectations are Mathlib's μ[f | m], so identities between them hold almost surely. Dual bounds are suprema in EReal over the adapted policy sets, so an infinite bound is represented and no junk value arises from an unbounded supremum.
Pinned regularity, beyond the paper's text: period rewards and generating functions are uniformly bounded (almost surely for the latter) and measurable, so that every expectation exists; in part (iv), the estimates are measurable and uniformly bounded. In part (ii), the difference of two dual bounds is taken in EReal, and the case where both bounds are (where the page's difference is undefined) is excluded.
The penalties of the goal are computed from by the formula of Proposition 2.2; stating the goal for arbitrary penalties with Proposition 2.2's properties would be a different and false claim. Likewise in part (iv) is constructed from and the estimates.
The definitions duplicate those of mission 1 of this series (the framework, the recursive model, the penalty construction); they are expected to be merged. Contributions of reusable lemmas about adapted policies over countable action sets and about backward recursions with conditional expectations are welcome.
Bounded-confidence models describe a population of agents who repeatedly average their opinions with those of agents whose opinions are close to their own. They are used to study consensus and polarization in opinion formation, and in control as a primitive for decentralized rendezvous of mobile agents. Simulations of these models show a robust phenomenon: opinions converge to clusters, and the distances between clusters are typically close to twice the confidence radius rather than just above it. For finitely many agents this regularity has resisted proof.
V. D. Blondel, J. M. Hendrickx and J. N. Tsitsiklis (SIAM J. Control Optim. 48 (2010) 5214–5240) study a continuous-time version of the model in two forms: with discrete agents, and with a continuum of agents indexed by . For the continuum they prove that regular initial opinions converge to clusters whose separation obeys a lower bound depending on the cluster weights. To transfer such conclusions to finitely many agents one needs to know that the -agent model is close to the continuum model when is large. Section 4 of the paper proves this on every finite time horizon. This mission formalizes that result.
Discrete agents. There are agents with real opinions , . Agents and interact when . A solution of (2.1) is a continuous with
for all and all . The right-hand side is discontinuous when the interaction graph changes, so the integral form is used. A solution is proper if it is the unique solution from its initial value, its non-differentiability times have no accumulation point, and two agents that meet stay together.
Continuum agents. Agents are indexed by with Lebesgue measure. is the set of bounded measurable functions . For , is the set of nondecreasing with for ; such are regular. The interaction operator is
and a solution of (3.2) from is a measurable with every and for all and all .
The embedding. For , is the step function with on and . It distributes the agents over blocks of of length .
Let , the solution of (3.2) from , and for each let be a proper solution of (2.1) with nondecreasing and . Then for every and there is with
The statement fixes no rate in and no dependence of on ; it asserts only uniform convergence on bounded time intervals.
The theorem says that the continuum model is the large-population limit of the -agent model over any fixed time window. Combined with the paper's continuum convergence result (Theorem 6), it supports the paper's Conjecture 1 on intercluster distances for finitely many agents, and it is the first step of the paper's Proposition 5, which derives Conjecture 1 for random initial opinions from a stability conjecture for the continuum. It is a mean-field limit for a model whose interaction kernel is discontinuous, where standard Lipschitz mean-field arguments do not apply directly.
All four results and the goal are proved in the paper (with the time-scale correction described below). None of them has a machine-checked proof that this mission is aware of. The formalization contributes a checked continuous-dependence estimate for a discontinuous integral equation, a checked statement that the finite-agent dynamics embed in the continuum dynamics, and a precise record of the time normalization under which the two models agree.
The operator is not Lipschitz on : moving one opinion across the confidence threshold changes the interaction set discontinuously. The obvious Gronwall argument for continuous dependence therefore fails for two arbitrary solutions. It works only around a trajectory that stays in some , where few agents sit near the threshold, which is why the lower slope bound must hold at every time and not only at time . The perturbed trajectory, coming from agents, is a step function and is never regular, so the estimate must be one-sided in this sense.
A literal reading of the page also fails. The page writes , but for in block the continuum interaction equals times the discrete right-hand side of (2.1). With and , both models are linear; at the sup distance between and tends to . The discrete time must be rescaled by .
Namespace BHTOpinion.Approx. Agents of the discrete model are Fin n (0-based); the continuum index set is Set.Icc (0:ℝ) 1 with Lebesgue measure. Opinion functions are ℝ → ℝ, of which only the values on matter; trajectories are written x t α, time first, with time in ℝ and explicit guards. In 0-based form, on ; for the definition returns , and every statement assumes .
Explicit readings of the paper's phrases:
A trivializing formalization is ruled out: the hypotheses are satisfied by , the conclusion is not vacuous because is evaluated at only, and the perturbed initial values in Proposition 4 range over all of , not over regular functions.
Infrastructure needed: Gronwall's inequality for a sup-norm difference, measure-theoretic bookkeeping for on step functions, and a change of variables in interval integrals. The Lipschitz estimate on and the slope bound are reusable for any continuum bounded-confidence model. Contributions to any milestone are welcome; the embedding milestone is independent of the other three.
In many production and service settings a single resource is shared by several parties, each judging the outcome only by how its own work is treated. Multi-agent scheduling studies this situation. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) introduced the two-agent single-machine model in which two agents, A and B, each own a set of jobs and each minimize their own objective. Their paper treats two questions: the constrained problem, minimizing A's objective subject to a bound on B's, and the Pareto problem, describing every schedule that cannot be improved for one agent without hurting the other.
For the Pareto problem the first quantity of interest is the number of distinct trade-offs, because the natural way to compute the whole front is to solve the constrained problem repeatedly with a decreasing bound (the paper's scheme PP, Figure 4, p. 239). Enumeration of this kind is polynomial exactly when the number of nondominated pairs is polynomially bounded. This mission formalizes the paper's bound for the case where both agents minimize a maximum of regular cost functions (§11.1, pp. 239–240).
Agent A owns the jobs and agent B owns , with . Every job has a processing time . All jobs are available at time . A schedule is an ordering of all jobs; the machine processes them in that order from time without idle time, so the completion time of a job is the sum of the processing times of the jobs up to and including it.
Each A-job carries a cost function and each B-job a cost function , all nondecreasing (regular). The agents' objectives are the maximum costs
This covers the makespan and maximum lateness of each agent as special cases.
A schedule is nondominated if no schedule satisfies and with at least one inequality strict. The pair of a nondominated schedule is a nondominated pair, and the schedule corresponds to that pair. Write for the set of nondominated pairs. Different nondominated schedules can share a pair; the problem asks for , with one schedule per pair. Job precedes job in if comes before in the ordering.
The paper prints the bound . It is off by one: with , unit processing times and , the schedules AB and BA give the two nondominated pairs and . The goal states , the bound the printed argument supports once the first schedule is counted.
The bound places among the two-agent problems whose Pareto front has polynomially many points. Combined with the polynomial algorithm for the constrained problem (Theorem 4.1 of the same paper), it means the full front can be listed with polynomially many constrained solves. The structural content is an order statement: as the bound on agent B tightens along the front, B-jobs overtake A-jobs and never fall back, so each of the (A-job, B-job) pairs changes order at most once. The same question for other pairs of objectives is the subject of later work on multi-agent scheduling, collected in the monograph of Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal (Springer 2014).
The result is published but, to our knowledge, has no machine-checked proof. Formalizing it also fixes the printed off-by-one error in the statement. The overtaking lemmas are of independent use for other pairs of regular min-max objectives.
The obvious argument walks along the front and charges each step to one (A-job, B-job) pair that changes order. Two things must be secured. First, the charged pair must change order in a consistent direction; schedules corresponding to a pair are not unique, and nothing forces two arbitrary representatives of different pairs to agree on the order of the jobs they do not charge. Lemma 11.2 asserts that representatives can be chosen so that no B-job falls back behind an A-job, and establishing it requires control over every job pair simultaneously, not one at a time as in Lemma 11.1. Second, a step must change at least one order. The tempting proof looks at a B-job attaining and argues that the jobs it overtakes include an A-job; this fails for an arbitrary choice of that B-job, since another B-job with a flatter cost function can be the one that moves. Finally, the count of reversals bounds the number of steps, not the number of pairs; the first pair has to be added.
Jobs are Fin nA ⊕ Fin nB (Sum.inl h is , Sum.inr k is , 0-based). A schedule is a duplicate-free list containing every job, and completion times are prefix sums of processing times; this is the published sequence model MooreLateJobs.Shared.completionTime (Moore 1968), reused as a reference item. Processing times are real and nonnegative; costs are real-valued and Monotone; so that both maxima exist. Nondominance compares against all schedules of all jobs. Precedence compares first positions in the list.
The count is over pairs, , measured with Set.encard, so finiteness is part of the goal. Counting nondominated schedules instead would be a different and false statement: permuting jobs inside a block often leaves both maxima unchanged. The printed bound is replaced by and the reason is given in the goal's statement; stating a larger bound "to be safe" or the printed one would make the mission either weaker than the paper's argument or false. The scheme PP and the choice of in it are not formalized; they are the paper's computation device, not part of the theorem. In the exchange claim the paper's σ and σ̃ are schedules of consecutive pairs; the milestone states it for any two nondominated schedules with the two strict inequalities, which includes that case. Running times are not formalized.
A complete development needs elementary facts about completion times when one job is moved within a sequence, the simultaneous statement of Lemma 11.2, and a counting argument along the front. Contributions of reusable lemmas about job moves in the sequence model are welcome.
A probability distribution on the real line is self-decomposable (of class L) if its characteristic function satisfies for every , with again a characteristic function. Equivalently, a random variable can be written as with a copy of independent of . Class L consists exactly of the limit laws of normalized sums of independent summands, and its members are infinitely divisible, absolutely continuous (when nondegenerate) and unimodal.
None of this transfers to counting variables: apart from , no random variable on satisfies , because leaves the lattice. Steutel and van Harn (Memorandum COSOR 78-07, 1978; Ann. Probab. 7 (1979) 893–899) replaced scalar multiplication by binomial thinning, which keeps the variable integer valued. The resulting notion of discrete self-decomposability later became the basis of integer-valued autoregressive (INAR) time-series models (Al-Osh and Alzaid, 1987).
Timeline:
A distribution on is a sequence with ; its probability generating function (p.g.f.) is . The generating function of a sequence is written .
The -thinning of a variable with p.g.f. is with independent Bernoulli() variables ; its p.g.f. is . A distribution with p.g.f. is discrete self-decomposable (Definition 2.1) if for every
with a p.g.f.; in variables, .
A distribution is infinitely divisible if for every its p.g.f. is the -th power of a p.g.f. When , its canonical sequence is the unique solution of
Throughout §2 the paper assumes .
For a distribution with :
for some and some p.g.f. of a distribution with , the pair being unique; and
Theorem 2.2 reduces discrete self-decomposability, a condition quantified over all and over unknown factors , to a single monotonicity condition on the sequence computed recursively from . It is the entry point of the rest of the paper: combined with Theorem 2.3 it gives unimodality of every discrete self-decomposable distribution (Corollary 2.4), and §3 shows that discrete stable distributions are discrete self-decomposable. In time-series modelling it identifies the marginals that a stationary INAR(1) process can have for every .
The result has been proved since 1979; to our knowledge none of it is formalized in any proof assistant, and Mathlib has neither probability generating functions on nor infinite divisibility. The mission produces a machine-checked version of the canonical form together with the compound-Poisson characterization of infinite divisibility on (Lemma 1.2), which the paper only cites.
The forward direction is not a consequence of (2.1) for any single : one factorization constrains very little, and the information sits in the whole family of factors , , which are not given explicitly. Turning that family into a statement about needs a passage to a limit of p.g.f.'s, and the fact that such a limit is again a p.g.f. (the continuity theorem for p.g.f.'s, Feller vol. 1, p. 280) is not in Mathlib. The paper does not prove Lemma 1.2 either; it cites Feller and Steutel. For the converse, nonnegativity of the canonical sequence is not enough: the obvious attempt to show that has nonnegative coefficients fails for infinitely divisible in general, and the monotonicity of is exactly what is needed. Finally, every identity is stated between real functions on , and passing to identities between coefficients requires the uniqueness of power-series coefficients on a real interval.
p : ℕ → ℝ with ∀ n, 0 ≤ p n and HasSum p 1; the p.g.f. is the real function pgf p z = ∑' n, p n * z ^ n. All identities between p.g.f.'s are required for real (or for (1.4), (2.4), (2.6), (2.7)), not for complex ; p.g.f.'s agreeing on have equal coefficients, so this is equivalent. is Lean's deriv of pgf p.Reusable beyond this mission: the p.g.f. and infinite-divisibility vocabulary, Lemma 1.2 (compound Poisson characterization), and Lemma 1.1. A continuity theorem for p.g.f.'s on , and the uniqueness of power-series coefficients from values on , are welcome as independent contributions.
Multivariate multipoint evaluation asks for the values of one polynomial at points of . Kedlaya and Umans showed that this problem is equivalent to modular composition, the computation of for univariate polynomials, and that fast algorithms for it yield the fastest known algorithms for factoring univariate polynomials over finite fields (Kedlaya–Umans, Dagstuhl Seminar Proceedings 08381, 2008; journal version SIAM J. Comput. 40(6), 2011, doi:10.1137/08073408X). Modular composition is the bottleneck of the factoring algorithms of von zur Gathen and Shoup (1992) and Kaltofen and Shoup (1998), so a near-linear multipoint evaluation algorithm translates directly into a faster factoring algorithm.
The paper gives two such algorithms. Section 4 works over any ring and is not algebraic: it lifts the problem to the integers and reduces modulo many small primes. Section 6, the subject of this mission, gives an algebraic algorithm, using only ring operations, for fields of small characteristic. Its correctness rests on one identity, Lemma 6.1, which lets the evaluation of the -variate at a point be read off from the evaluation of a single univariate polynomial at a related point of an extension ring.
Let be a prime and a finite field of characteristic . Fix integers and . Let be a power of with (the paper takes the least such power), and let be a polynomial of degree that is irreducible over . Then:
Three maps connect the problem to :
In the Lean development these are K, R, h, ι (the inclusion ), sigma i (), E, S, sigmaInv i ( on ), gAlpha, phi, pi, gIter () and fStar, in the namespace KedlayaUmans.FrobeniusLift.
For every with degree at most in each variable and every ,
The result. Lemma 6.1 is the correctness half of Theorem 6.2: to evaluate at points one computes the lifts , evaluates the one univariate polynomial at all of them by fast univariate multipoint evaluation, and projects back with . Since univariate multipoint evaluation runs in nearly linear time, the identity turns a multivariate problem into a univariate one at the cost of the degree growth . Corollary 6.3 turns this into an operation count of for every , provided and the characteristic satisfies .
Formalizing it. The lemma is proved in the paper; no machine-checked version is known to exist. This mission states it for the objects exactly as constructed in Section 6 (an explicit interpolant for , the canonical-representative projection for ) and splits its proof into the five steps above. The definitions of the rings and , the Frobenius powers on a ring that is not a field, and the Kronecker substitution into a quotient ring are reusable for formalizing other uses of the Frobenius-lift technique, such as the Parvaresh–Vardy codes and their Guruswami–Rudra instantiation, which the paper names as the inspiration for this algorithm (§1.5, p. 6).
The obvious attempt is to treat as evaluation at and push it through . This fails: is a unit, not zero, so evaluation at does not factor through , and is not a ring homomorphism. The identity holds only because the polynomial is already reduced modulo , which requires both the degree bound and the fact that raising to the power does not raise the degree of modulo . The second fact depends on being fixed by and on . The equality further needs that does not kill the leading coefficient in , a ring with possible zero divisors. Finally, interpolation must happen in , not a field, which is possible only because the nodes lie in the subfield .
F with [Field F] [Fintype F] [CharP F p], a prime ([Fact p.Prime]). is a polynomial over ZMod p with [Fact (Irreducible P)]; is P.natDegree and is p ^ P.natDegree. is AdjoinRoot of mapped to F; is never assumed to be a field and is never assumed irreducible over F.m ^ 2 * d < h, which contains the paper's case. is a hypothesis.IsPrimitiveRoot η (h - 1), equivalent to generating since .∀ i, f.degreeOf i ≤ d - 1.Fin m, starting at ; substitutes for .Lagrange.basis over the field at the nodes , mapped into , with coefficients . is the remainder modulo (AdjoinRoot.modByMonicHom) evaluated at .A formalization that takes to be any element satisfying (6.2), or defines as a ring homomorphism, would make the goal trivial or false; both are ruled out because and are explicit definitions with no hypotheses attached, and (6.1) and (6.2) are milestones to be proved.
Infrastructure a full proof needs: the Frobenius on polynomial rings in characteristic (, cf. Mathlib's expand and map_frobenius_expand), Lagrange interpolation transported along a ring homomorphism from a field, degree bounds for MvPolynomial.eval₂, and reducedness of (from separability of over the perfect field ). Proofs of any milestone, and alternative arguments, are welcome.
Multivariate multipoint evaluation asks for the values of a polynomial over a ring , with individual degrees at most , at given points of . Kedlaya and Umans showed that, over finite fields and rings , this problem can be solved in time nearly linear in the input size , for (Kedlaya–Umans 2008, §4). Through their reduction of modular composition, the computation of , to multipoint evaluation (§3 of the same paper), this gives the first nearly-linear-time algorithm for modular composition over finite fields. That in turn gives the fastest known algorithms for factoring univariate polynomials over , with bit operations for a randomized algorithm on degree- polynomials (abstract and §8).
Timeline. Brent and Kung (1978) gave the baby-step/giant-step algorithm for modular composition (J. ACM 25). Huang and Pan (1997) improved the exponent using fast rectangular matrix multiplication. Kaltofen and Shoup (1998) introduced the factoring framework that the factoring application builds on (Math. Comp. 67). Kedlaya and Umans (2008, SIAM J. Comput. 2011) gave the multimodular algorithm formalized here, together with an algebraic algorithm for small characteristic.
Let and write for the integers modulo . Every element of has a lift, its representative in . For , replaces each coefficient by its lift; lifts a point coordinatewise.
Algorithm MULTIMODULAR with degree parameter and rounds takes (degree at most in each variable) and a point . It lists the primes at most , reduces and modulo each , and evaluates the reductions . It does this directly when , and by recursion with rounds otherwise. It then returns, reduced modulo , the unique integer in congruent to modulo every .
Let be monic of degree and . The lift of is its representative of degree at most , with coefficients lifted to , an element of . Put
Algorithm MULTIMODULAR-FOR-EXTENSION-RING runs in four steps.
For monic of degree , , , , every of degree at most in each variable, and every :
In the order the paper's proofs use them:
The result makes multivariate multipoint evaluation exact and fast over every finite ring of the form , which includes every finite field . Combined with the paper's reduction from modular composition (Theorem 3.1) it yields modular composition of degree- polynomials over in bit operations (§7). That is the step on which the paper's improvements to univariate polynomial factorization, irreducibility testing and minimal-polynomial computation rest (§§7–8). The same algorithm gives a data structure answering polynomial-evaluation queries in time polylogarithmic in the degree (§5).
The theorem is proved in the paper; nothing in it is open. As far as is known, no part of it has been machine-checked. This mission formalizes the correctness of both algorithms exactly as the paper defines them, step for step, including the Chinese-remainder recombination, the explicit prime threshold , and the base- digit recovery. Lemma 2.4 is an explicit Chebyshev-type lower bound on the primorial, valid for all , and is reusable independently of this mission.
The recursion itself is routine. Two points carry the content. The first is the explicit prime threshold: the algorithm uses only primes up to , so its correctness depends on the explicit inequality of Lemma 2.4 for every , not on an asymptotic prime-number estimate. The small cases are part of the claim. The second is the extension-ring step: the integer produced over must determine the polynomial exactly. That needs simultaneous control of its degree and of every coefficient, against the specific constants and . A bound on evaluated at a point does not by itself suffice.
Lean represents as ZMod r with (NeZero r, excluding ZMod 0 = ℤ), polynomials as MvPolynomial (Fin m) _ with variables indexed , and as AdjoinRoot E for a monic E with E.natDegree. "Degree at most in each variable" is ∀ i, f.degreeOf i ≤ d - 1. is the natural logarithm; the paper does not fix a base, and the natural log is the strongest reading of Lemma 2.4. The primes for real are the primes . Each algorithm is defined for a single evaluation point, since the paper processes the points independently. The leaf evaluates at directly; that value is what Theorem 4.1's FFT algorithm outputs. is as printed on p. 15; p. 16 prints .
The hypotheses and are not written in the paper but are needed. For , , the threshold is , no prime is used, and MULTIMODULAR returns . For the inequality and the degree bound both fail.
Only correctness is formalized. Every running-time bound in Theorems 4.1, 4.2, 4.4 and Corollaries 4.3, 4.5 is out of scope. The Chinese-remainder step and the digit step are defined from the residues and from alone: an algorithm that evaluates in and reduces it, or that computes in directly, would make the theorems trivial and is not the algorithm stated here.
Needed infrastructure: explicit primorial lower bounds (Mathlib has primorial and Chebyshev's ), the Chinese remainder theorem for several moduli (ZMod.prodEquivPi), bounds on evaluations of polynomials with nonnegative coefficients, and uniqueness of base- representations of polynomials. Lemma 2.4 and the base- uniqueness are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 2.4.
Large optimization problems often split into blocks owned by different agents (subsystems of a power grid, vehicles in a formation, scenarios of a stochastic program) that are coupled only through a few linear constraints. Distributed optimization methods solve such problems by letting each agent work on its own block and exchanging a small amount of information, typically a vector of prices for the coupling constraints. The classical method of this kind is dual decomposition (Everett 1963; Bertsekas and Tsitsiklis, Parallel and Distributed Computation, 1989): fix the prices, let every agent solve its own subproblem, then update the prices by a gradient or Newton step on the concave dual function. Dual decomposition is reliable for strictly convex problems but has no convergence guarantee for nonconvex ones.
Houska, Frasch and Diehl (SIAM J. Optim. 26 (2016)) proposed ALADIN (augmented Lagrangian based alternating direction inexact Newton), which adds a proximal term to the agents' subproblems and replaces the price update by a coupled equality-constrained quadratic program. ALADIN is used in distributed model predictive control and in power-system optimization. Remark 4.2 and Appendix A of the paper explain where it sits relative to the classical method: if the proximal term is switched off (), the price update of ALADIN is exactly a regularized Newton step of dual decomposition. Lemma 5 is the precise statement of that equivalence, and it is the goal of this mission.
The problem (1.1) has blocks :
with , twice continuously differentiable, and . One iteration of Algorithm 2 (ALADIN) starts from a primal point and prices and does the following.
and the new prices are .
On the dual-decomposition side, (A.3) is the gradient of the dual function at , and the (inexact) dual Newton step (A.4) with a symmetric negative semidefinite scaling matrix and step size is
where plays the role of a Levenberg–Marquardt regularization parameter.
Assume every strictly convex, every convex, of full row rank, positive definite, and . Then for every , with
the matrix is invertible and
The result. Lemma 5 places ALADIN on a known map. With it inherits the convergence theory of dual decomposition for strictly convex problems for small step sizes, independently of how crude the approximations , are, as long as . It also reinterprets the augmented-Lagrangian parameter as the inverse of a dual Levenberg–Marquardt parameter, and it isolates the proximal term as the only ingredient that distinguishes ALADIN from dual decomposition and makes the nonconvex analysis of the paper possible.
Formalizing it. The lemma is proved in the paper; to our knowledge no machine-checked proof exists. A formal proof certifies an identity whose printed form contains a typo (see below), and produces reusable linear-algebra facts: the closed-form solution of an equality-constrained strictly convex quadratic program via the reduced inverse , the semidefiniteness of , and the closed-form maximizer of a regularized concave quadratic.
The proof is a chain of exact eliminations, and the work is in carrying each one out without losing a sign or a hypothesis. The step most easily done wrong is the minimization over : the constraint couples the block coordinates, the minimizer is expressed through the inverse of (invertible only because has full row rank). A second trap is the sign convention for : it must agree with footnote 4 (), or the conclusion flips. The tempting shortcut of treating the max–min dual of (3.3) abstractly runs into the fact that strong duality and attainment are not free; working from the KKT system of (3.3) avoids that.
Vectors are Fin n → ℝ; blocks are indexed by Fin N; matrices are Mathlib Matrix over Fin index types; the gradient is the vector of partial derivatives computed with fderiv. The step-1 output is a local minimizer of the decoupled problem together with KKT multipliers (the paper assumes LICQ for the lower-level constraints). The QP (3.3) and enter through the KKT system of (3.3), not through a closed-form expression: defining or by the formula of the conclusion would make the goal true by definition and is ruled out. is the formula (A.3); that it is the gradient of the dual function is a cited fact the lemma does not use. The invertibility of is part of the conclusion, because Mathlib's matrix inverse returns on a singular matrix.
Correction of (A.6). As printed, (A.6) has the bracket . This is a typo for , as in (A.5) on the same page and as the explicit minimization over forces; with the printed bracket the identity fails already for , , , . The mission uses the corrected matrix and writes the pseudo-inverse as an inverse, which it is under the hypotheses.
The hypotheses of strict convexity of , convexity of and are kept as on the page although the identity does not use them. The related platform draft GoldfarbIdnani.DualQP.properties_2_6_to_2_9 (not proved) states properties of the same reduced inverse; it is not imported. Proofs of the four milestones and of the goal are welcome; the milestones are self-contained matrix and calculus facts and can be attacked independently.
Matrix completion asks for a low-rank matrix from a small random subset of its entries. It models collaborative filtering (recommendation systems), sensor-network localisation, and structure from motion. In practice the revealed entries are corrupted by noise, and the most widely used estimator is nuclear-norm regularized least squares: fit the observed entries in squared error while penalizing the sum of singular values. The estimator is a convex program, so it is solved reliably by proximal and singular-value-thresholding methods, and it needs no knowledge of the rank.
Its statistical accuracy was not understood. In the noiseless case, convex relaxation recovers the matrix exactly from nearly the information-theoretic minimum number of samples (Candès–Recht 2009, Candès–Tao 2010, Gross 2011). With noise, the available bounds for the plain convex program (Candès–Plan 2010) give under random noise. That can be a factor of order above the oracle lower bound, and the numerical performance of the program is far better. Sharper rates were known only for modified estimators: Negahban–Wainwright 2012 add a spikiness constraint, Koltchinskii–Lounici–Tsybakov 2011 use a different estimator. In 2019, Chen, Chi, Fan, Ma and Yan (arXiv:1902.07698; SIAM J. Optim. 30(4), 2020, doi:10.1137/19M1290000) showed that the unmodified convex program attains near-optimal error in the Frobenius, entrywise and spectral norms simultaneously. Their argument goes through nonconvex gradient descent. This mission formalizes that theorem.
The unknown matrix is of rank , with singular value decomposition . The columns of are orthonormal, and with , and condition number . Write for the largest Euclidean norm of a row of . is -incoherent if and (Definition 1). Incoherence says that the energy of is not concentrated on a few rows or columns.
Under Assumption 1, each index enters the observed set independently with probability . One observes for , where the are i.i.d., zero-mean, and have sub-Gaussian norm . Let keep the entries indexed by and zero the rest. The convex estimator is any minimizer of
where is the nuclear norm, is the spectral norm and is the largest absolute entry.
Suppose and . Then with probability , every minimizer of (3) satisfies
Every best rank- approximation is within of in Frobenius norm, and satisfies the same three bounds.
satisfies under Conditions 1–2. 2. Probabilistic layer: Lemma 3 (Condition 1(a)), Lemma 19, Lemmas 7 and 8, and Lemma 4. Lemma 4 gives Conditions 1(b) and 2 uniformly over an neighbourhood of the truth. 3. Algorithmic layer: Lemma 5, the error bounds and the small-gradient iterate of gradient descent started at the truth, and (31), its consequence for .
The bounds of Theorem 2 match the minimax lower bounds up to logarithmic factors when and are bounded. This holds in all three norms and for noise of any size below a threshold. The theorem also shows that the convex solution is nearly of rank . Neither statement requires modifying the estimator, so practitioners running standard solvers get the guarantee as is. The entrywise bound (11b) shows an implicit regularization: the convex program spreads its error over all entries without being told to.
The theorem has a complete published proof. What this mission adds is a machine-checked version, which has value of its own here. The proof chains about twenty lemmas, including a leave-one-out analysis of gradient descent with polynomially many iterations. Its constants are hidden behind "" at nearly every step. The formal development fixes the quantifier order of every such constant. It also records the hypotheses the proof uses without stating them, such as the independence of the sampling pattern from the noise. No part of this paper has been formalized before. The deterministic layer (Lemmas 20, 2, Claims 2–3) applies to any Burer–Monteiro factorization of a nuclear-norm problem, not only to this one.
The obvious approach is to analyse the convex program directly through a dual certificate, as in the noiseless theory. With noise there is no exact recovery, and the certificate approach loses a factor polynomial in . The difficulty is to transfer statistical bounds from a point one can control, the nonconvex iterate, to a point one cannot construct, the convex minimizer. The two are compared through an approximate first-order condition. That comparison is useful only if injectivity and concentration hold uniformly over all factor pairs near the truth, because the iterates depend on and on the noise. A fixed-tangent-space injectivity bound, the usual tool, does not suffice. The entrywise control of the iterates requires leave-one-out sequences, and those sequences make up most of the appendix.
Matrices are Matrix (Fin n) (Fin n) ℝ and factors Matrix (Fin n) (Fin r) ℝ, using the published matrix_completion_basic, _svd and _tangent definitions (nuclear norm, SVD data, , , spectral, Frobenius and entrywise norms). comes with an explicit SVD with positive singular values, so its rank is exactly . Definition 1 is MatrixCompletion.A0. The sub-Gaussian bound is the moment form of [Ver12, Definition 5.7] above, not Mathlib's MGF form. The randomness lives on an arbitrary probability space. The sampling indicators and the noise entries are each mutually independent, and the two families are independent of each other. This last independence is an added hypothesis, which the paper's proofs use. "With probability " is stated as an outer-measure bound on the failure event. Every unnamed constant ("", "sufficiently large ", "sufficiently small ") is an existential placed before and all data, together with an . Explicit constants of the paper are kept: the exponents and , , , , , , , the factors in (31), the in (12), and in Lemma 2.
The goal keeps the randomness in the statement. A version with fixed and that assumes Conditions 1–2 or the conclusions of Lemma 5 would be Lemma 2 plus (31), not Theorem 2, and is not acceptable as a proof of the goal. The goal quantifies over every minimizer of (3) and every best rank- approximation. Excluded: Theorem 1 (the corollary), the noise condition of Remark 4, approximate minimizers (Remark 6), Lemmas 1 and 6, and the internal lemmas of the leave-one-out analysis (App. D), which solvers may add as supporting theorems. The development needs nuclear-norm subgradients, Weyl's inequality, matrix Bernstein and spectral-norm bounds for sparse random matrices. These are reusable well beyond this mission, and contributions of them are welcome. Theorem and equation numbers are those of the authors' preprint (Sep. 2019, arXiv:1902.07698) and may differ in the SIAM typesetting.
Training a neural network with nonsmooth activations (ReLU, max-pooling, absolute values) means running a stochastic gradient method in which the "gradient" is whatever the automatic differentiation library returns. For nonsmooth programs that output is in general neither a gradient nor a Clarke subgradient: the chain rule fails for the Clarke subdifferential, and the same function written in two ways can receive two different derivatives at the same point. Bolte and Pauwels (TSE Working Paper 1044, 2019; published in Mathematical Programming, 2021) introduced conservative set-valued fields as a class of generalized derivatives that is closed under the operations automatic differentiation performs and still carries enough information to analyse descent methods.
The framework is used in the analysis of nonsmooth automatic differentiation and of stochastic subgradient methods in machine learning (for instance Bolte and Pauwels, NeurIPS 2020). The present mission formalizes the first structural theorem of the theory.
Write for Euclidean space with inner product . A set-valued map assigns to each a subset ; it has closed graph if is closed in . A path is absolutely continuous if it is differentiable almost everywhere and ; it is a loop if .
Definition 1. is a conservative field if it has closed graph, nonempty compact values, and for every absolutely continuous loop
The integrand is Lebesgue measurable (Lemma 1), so the condition is that circulations along loops vanish, as for gradient fields in classical vector calculus, but with a maximum over the set in place of a single vector.
Definition 2. A function is a potential for (and is a conservative field for ) if for every and every absolutely continuous path from to
Examples: the gradient of a function; the Clarke subdifferential of a semialgebraic locally Lipschitz function; the output of forward or reverse mode automatic differentiation on a program built from definable elementary functions (the subject of the companion mission in this series).
If is a conservative field and a (locally Lipschitz continuous) potential for , then for Lebesgue-almost every , is differentiable at and
The result. Theorem 1 says that a conservative field, although set-valued and possibly far from any subdifferential, differs from the gradient of its potential only on a Lebesgue-null set. Several consequences in the paper rest on it: the Clarke subdifferential of is contained in the convex hull of every conservative field for , so it is the minimal convex-valued conservative field (Corollary 1), and a Fermat rule at local extrema of (Proposition 1). Combined with the companion result that automatic differentiation produces conservative fields, it implies that the derivatives returned by automatic differentiation agree with the gradient outside a Lebesgue-null set.
Formalizing it. The theorem is proved in the paper; this mission formalizes the known proof. No conservative-field calculus exists in Mathlib or on the platform. The mission produces the definitions of conservative fields and potentials in Lean, a measurability result for marginal functions of closed-graph set-valued maps along absolutely continuous paths, and an almost-everywhere identification of measurable selections with gradients that can be reused for other "derivative equals selection almost everywhere" statements.
The obvious argument runs: is locally Lipschitz, hence differentiable almost everywhere by Rademacher's theorem, and at a point of differentiability must be . The second step fails. Conservativity is an integral condition along curves, and it says nothing about the value of at an individual point of differentiability; a pointwise argument cannot exclude extra elements of . The identification therefore holds only almost everywhere and has to be extracted from integral information, which brings in three ingredients absent from Mathlib: measurability of for closed-graph compact-valued maps with no local boundedness assumption; measurable selections of such maps, including a countable family dense in every value (a Castaing representation); and, for Remark 3(d), the local boundedness of conservative fields (Borwein, Moors and Wang). Passing from "almost every point of every line" to "almost every point of " also requires measurability of the exceptional set, which is not automatic.
is EuclideanSpace ℝ (Fin p), Lebesgue measure is volume, and a set-valued map is EuclideanSpace ℝ (Fin p) → Set (EuclideanSpace ℝ (Fin p)). A path is a function ℝ → ℝ^p satisfying AbsolutelyContinuousOnInterval γ 0 1 (Mathlib's – definition on , equivalent there to the paper's); its values outside are irrelevant and is deriv γ. The maximum and minimum over are sSup and sInf of the image of a nonempty compact set, hence attained.
Since Lean's integral of a non-integrable function is , Definitions 1 and 2 require the circulation to be integrable in addition to having the stated integral; without this conjunct every field with non-integrable circulations would count as conservative, which is a trivializing reading excluded here. Likewise "" is formalized as differentiability of at together with set equality , because Lean's gradient is where is not differentiable. Definition 2 is the paper's form (2) with base point ; the min-form and the forms (3)–(4) are consequences, not definitions. Measurable selections appear as hypotheses (Borel measurable with ); their existence is not claimed by any milestone. The local Lipschitz hypothesis of Theorem 1 is kept as printed, and local (not global) Lipschitz continuity is used throughout.
Theorem numbers and pages refer to the TSE Working Paper 1044 version (October 2019), not to the Mathematical Programming typesetting.
Welcome contributions: a Castaing representation / Kuratowski–Ryll-Nardzewski selection theorem for closed-graph compact-valued maps on ; Rademacher's theorem for locally Lipschitz functions; Fubini-type "null on every line implies null" lemmas on EuclideanSpace; the fundamental theorem of calculus for absolutely continuous vector-valued paths.
Online covering models decisions that must be made as requirements arrive. A planner knows the cost of each available resource, but learns the requirements one at a time and cannot undo an allocation already made. This occurs, for example, when requests for network service or elements needing coverage appear over time. The central question is how much more an online fractional allocation can cost than a best allocation chosen after all requirements are known. Buchbinder and Naor study this question through a paired covering and packing linear program and give an online scheme for arbitrary nonnegative constraint coefficients, not only incidence coefficients in (Buchbinder and Naor, 2009, §§2–4).
The result targeted here is Theorem 4.1 of that paper. It concerns the fractional covering scheme of §4, before the separate extension to box constraints in §4.1. The theorem is a statement about the particular phased scheme, so the scheme's state and update rule form part of the mathematical setting. The online requirement also matters: after each new constraint, earlier allocations remain in force (Buchbinder and Naor, 2009, pp. 4, 8).
Let be a finite nonempty set of primal variables and let index constraints in arrival order. The known cost of variable is . Constraint has coefficient for variable ; when it arrives, the online algorithm learns its coefficients. The normalized offline covering problem minimizes over subject to for every constraint considered. Its packing dual maximizes over subject to for each . The finite data and sign conventions are those of Figure 1 (Buchbinder and Naor, 2009, pp. 3–4).
The scheme accepts a parameter and asks for coverage only to . It maintains a sequence of phases. The first phase bound is times the least ratio among the positive coefficients of the first constraint. The bound doubles at a restart. Within a phase, the vector begins at zero, the initial primal allocation is , and the allocation subsequently follows the exponential expression on page 8. The current phase may need to process constraints already seen in earlier phases. Old phase vectors are retained: the actual online allocation is the coordinatewise maximum of the current and all finished phase vectors. Thus resetting a phase does not retract an earlier allocation (Buchbinder and Naor, 2009, p. 8).
For every nonempty arrival prefix of length , a run of the phased scheme exists. Every completed run has output satisfying
and, for every nonnegative offline comparison vector satisfying for each ,
The paper states the ratio as . Its closing display on page 9 yields the explicit factor used here. The benchmark uses the unscaled covering constraints of Figure 1; replacing them with constraints at would change the guarantee (Buchbinder and Naor, 2009, Theorem 4.1 and proof, pp. 8–9).
The milestone list follows the four claims printed under Theorem 4.1. A finished phase has dual objective at least ; every phase dual vector satisfies the packing constraints; the sum of phase primal costs through the current phase is less than ; and the actual allocation covers every arrived constraint to . These are statements about the phase records of the scheme, including a partly processed round that ends in a restart (Buchbinder and Naor, 2009, pp. 8–9).
The theorem gives a cost guarantee for a general online covering problem while allowing arbitrary nonnegative coefficients. It separates the cost paid by an allocation from the level of coverage requested through . Its four claims identify the quantities that make the guarantee meaningful: the dual vector certifies a lower bound for an offline comparison, the phase costs control the online expenditure, and the output remains feasible as constraints arrive. The same primal–dual setting is used elsewhere in the paper for online packing and for applications of covering and packing methods (Buchbinder and Naor, 2009, §§3–5).
The paper proves Theorem 4.1. This mission asks for a machine-checked account of the known result and of the scheme to which it applies. A published formal restatement, OnlinePrimalDual.GeneralPacking.theorem14_3, already gives a ratio conclusion under an assumed ratio bound and an assumed weak-duality inequality; those hypotheses contain the main work needed here. The present goal instead quantifies over runs generated by the update rule and asks both that a run exists and that all such runs satisfy the guarantees. The published general instance definition is reused, so the finite covering and packing data have a shared interface.
An online allocation cannot be evaluated solely from its final vector. A phase restart resets the working dual vector and restarts the constraint scan, while allocations from completed phases still affect the actual output. A statement about arbitrary vectors with a presumed cost bound would leave out this behavior. The continuous update also requires a precise stopping event when coverage or the phase cost reaches its threshold. The cost guarantee is sensitive to which condition wins if both occur together, and to whether a phase can restart indefinitely. Those details must be represented before any claim about completed phases has the paper's meaning (Buchbinder and Naor, 2009, pp. 8–9).
Lean uses OnlinePrimalDual.GeneralPacking.GeneralInstance I (Fin m) for the coefficient matrix and costs. A nonempty finite type represents the primal variables; Fin m supplies the ordered constraints. The theorem assumes , , and a positive coefficient in every constraint. The last condition makes each arriving constraint coverable and makes the first ratio minimum nonempty; zero coefficients are omitted from that minimum. The paper treats infeasible all-zero rows implicitly. The minimum is over a finite nonempty set, so the real infimum in the Lean definition equals the ordinary minimum. All sums are finite and all logarithms are natural.
The run is an event relation with three events: arrival of one new constraint after all known constraints have been processed, completion of a covered round at its first stopping time, and restart at the cost cap while coverage remains deficient. A restart doubles , records the old phase, resets the dual variables, and resumes at the first known constraint. The state records the current phase and all finished phases; the output takes their coordinatewise maximum. A simultaneous coverage and cost event counts as covered. Reaching the cost cap models the continuous stopping time behind the paper's wording that the cost “exceeds” the bound. The theorem asserts run existence, so a ratio claim cannot hold merely because the run relation has no witness.
The explicit instantiation in this mission is , from the page 9 closing display. The first-phase case is bounded there by times the optimum and is included in the same stated coefficient. The comparison vector must satisfy the original level-one constraints. Theorem 4.2, which adds upper bounds on variables and appears in §4.1, is outside this mission. The run definition, phase-cost and coverage functions, and the four claims are reusable infrastructure for later work on continuous online primal–dual schemes.
Classical scheduling theory optimizes one objective for one decision maker. Many shop floors are shared: two departments, two customers or two firms submit jobs to the same machine, and each cares only about how its own jobs are treated. Agnetis, Mirchandani, Pacciarelli and Pacifici, Scheduling Problems with Two Competing Agents (Operations Research 52(2), 2004), set up this two-agent scheduling model and classified the complexity of its single-machine cases for the standard objectives (maximum of regular cost functions, number of late jobs, total weighted completion time). The paper started a line of research on multi-agent scheduling; its notation is the standard one in that literature.
This mission covers the paper's first case, §4: both agents measure a schedule by the largest cost among their own jobs. It is the case with a polynomial greedy algorithm, and it serves as the template for the paper's other cases.
Agent A owns jobs and agent B owns jobs . Each job has a processing time ; all jobs are available at time . A schedule is an ordering of all jobs, processed on one machine one after another from time without idle time, so the completion time is the sum of the processing times of and the jobs before it. Each A-job has a nondecreasing cost function and each B-job a nondecreasing (the costs are regular). The two objectives are
The constrained optimization problem asks for a schedule minimizing among those with (the feasible schedules). A schedule is nondominated if no schedule has and with one inequality strict.
The backward rule of §4 builds a schedule from the end. With the set of unscheduled jobs and the time at which the next job placed will end, it places last any unscheduled B-job with ; if there is none, it places last an unscheduled A-job of least ; if neither exists, it stops and declares the instance infeasible.
The paper justifies the rule by a reduction to Lawler's single-agent problem (Lawler 1973): every job gets one cost with values in , equal to for A-jobs, to for a B-job meeting the bound at time and to for one violating it.
Both parts hold for every tie-breaking. The printed theorem states a running time ; only the correctness half is a target.
The theorem shows that the two-agent problem with maximum-cost objectives is no harder than its single-agent counterpart: a greedy rule that gives priority to any B-job still within budget and otherwise serves agent A's cheapest job is optimal. Theorem 4.2 turns this into a point of the Pareto frontier with one more optimization, without the binary search over that §3 of the paper describes for the general case. In §11 the paper enumerates nondominated pairs by repeatedly solving the constrained problem, and §11.1 bounds their number for this case.
None of these results has a machine-checked proof that we know of. The single-agent theorem of Lawler is the subject of the published Prove2Me statement LawlerPrec.MinMax.lawler_rule_optimal, which is open; its costs are real-valued, so it does not apply directly to the costs of the reduction. This mission's results are self-contained and can be proved either through such a generalization or directly.
The rule is nondeterministic: any eligible B-job may be chosen, and ties among A-jobs are broken arbitrarily, so the optimality claim is about every possible output, not one canonical sequence. Lawler's exchange argument has to be carried through the extended-real costs, where a B-job's cost jumps from to at its deadline, and the ordering by B-first priority has to be shown to be one of Lawler's least-cost choices. The completeness half needs that a stuck state (no A-job left and every remaining B-job over budget at ) rules out every schedule, not just the rule's.
Fin nA ⊕ Fin nB (Sum.inl h is , Sum.inr k is , 0-based). Schedules and completion times reuse the published definition MooreLateJobs.Shared.completionTime (Moore 1968): a duplicate-free list containing every job, processed from time without idle time.IsBackwardRuleSeq): at every position of the sequence, with the jobs at positions and the completion time at position , the job there is an eligible B-job if one exists in , and otherwise an A-job of least in . "Ties are broken arbitrarily" means the property admits every choice. "The rule stops" means no sequence through that state has the property, so "the rule completes" is the existence of a complete sequence with the property.EReal with only maximum and order; "1|prec|f_max" is taken with the empty precedence relation. "Finite objective value" means the minimum is a real number.The definitions (two-agent model, maximum costs, constrained problem, nondominance) are reusable by the rest of this series. Proofs of the milestones, and a generalization of Lawler's theorem to extended-real costs, are welcome.
Multi-agent scheduling studies a machine shared by parties with their own jobs and their own objectives. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) introduced the two-agent single-machine model: agents and each own a set of jobs, and the schedule must serve both. The paper frames this within multiagent systems, where agents negotiate the use of a common resource over time, and its schedules are meant to support that negotiation: either the best schedule for one agent given what the other accepts, or the whole set of nondominated (Pareto-optimal) schedules. The paper classifies the complexity of the constrained problems for the classical regular objectives.
One of its polynomial cases concerns the number of late jobs on both sides: agent accepts schedules in which at most of its jobs are late, and agent minimizes the number of its own late jobs. For a single agent, minimizing the number of late jobs is solved by Moore's algorithm (Moore 1968), and a dynamic program of the Lawler–Moore type over jobs in due-date order solves related weighted versions (Lawler & Moore 1969). §7 of the 2004 paper adapts that dynamic program to two agents by tracking the number of late jobs of each agent separately.
There are jobs , all available at time . Job has a processing time , a due date , and an owner, agent or agent . A schedule is a sequence of all jobs processed on one machine from time without idle time or preemption; the completion time of is the sum of the processing times of and the jobs before it. Job is late if and early otherwise. denotes the number of late jobs of agent .
Given an integer , the problem asks for a schedule with (a feasible schedule) minimizing . An instance may have no feasible schedule at all.
The jobs are numbered in earliest-due-date (EDD) order, . A partial schedule of is described by its set of early jobs: the jobs of run first, in EDD order, each completing by its due date, and the other jobs of count as late. The table is the minimum completion time of the last early job over partial schedules of with at most late -jobs and at most late -jobs, and if there is none. It is computed by , at a negative index, and
when belongs to (with in place of when belongs to ), where if and otherwise.
For a feasible instance with jobs in EDD order, for some , and
is the optimal value of : some feasible schedule has exactly late -jobs, and every feasible schedule has at least .
A feasible instance has an optimal schedule whose early jobs come first, in EDD order, and whose late jobs come last.
For : if is finite, it is the minimum, attained, of over partial schedules of with at most late -jobs and at most late -jobs; if , there is no such partial schedule.
The theorem places among the polynomially solvable two-agent problems (Table 1 of the paper lists it as ), in contrast with , which the same paper shows binary NP-hard. Through the binary-search argument of §3.1, solving the constrained problem for every also yields the nondominated pairs of the corresponding Pareto problem.
The result is proved in the paper; to the knowledge of this mission it has no machine-checked proof. The mission produces a checked correctness proof of the table, including the boundary convention, which the printed text leaves incomplete (see below). Further welcome work: the complexity bound in an explicit cost model, and the weighted variant.
The table is defined over partial schedules, in which the jobs outside the early set are only counted as late, while the problem is posed over complete sequences, in which lateness is measured: a job declared late may finish on time once it is appended. The correctness of must bridge the two objects in both directions, and the bridge is the structural Lemma 7.1, which the printed proofs use without detail. Lemma 7.2 is an optimal-substructure claim: it requires that the early set of minimizing total processing time is also the right one to extend by , which holds only because of the EDD numbering. Finally, the printed boundary gives only ; the natural reading for makes Theorem 7.3 false, so the boundary must be read from the definition of , not from the display.
Fin n, 0-based, numbered in EDD order, with an owner label ag : Fin n → Agent; this follows the paper's single numbered list in §7 rather than separate index sets per agent. EDD order is the hypothesis Monotone d, ties allowed. Data are natural numbers.MooreLateJobs.Shared.completionTime (sequences without idle time) and late jobs the published MooreLateJobs.NumLate.lateSet (late iff ), reused as references with the data cast to .WithTop ℕ, with ⊤ for ; no large sentinel number is used. The boundary is for all , the value forced by the "at most" definition of ; a negative index gives ; early means , as in the recursion (the proof of Lemma 7.2 prints a strict "").Nat.find of the existence clause, which the goal asserts.Balanced truncation reduces a large control system to a small one by discarding the states that are both hard to reach and hard to observe. For linear systems "hard to reach" is measured exactly by the controllability Gramian : the minimal input energy needed to steer the system from to is . For bilinear systems, in which the input also multiplies the state, no such exact formula is known, and several papers have tried to describe the nonlinear controllability energy functional through state-dependent Gramians.
Gray and Mesko ([25] in the paper, 1998) and Condon and Ivanov ([11], 2005) stated that, for with sufficiently small, the gradient of is given by a state-dependent Gramian of the linearization, , and derived from this comparison inequalities between and the algebraic Gramian. Benner and Damm (SIAM J. Control Optim. 49(2), 2011, doi:10.1137/09075041X) observed that this formula needs an integrability condition that is not automatic, and gave an explicit two-dimensional system for which it fails (Example 3.3, pp. 697–698). This mission formalizes that counterexample.
A bilinear control system with state and input is
with real matrices and ; write for the -th column of . The system is locally controllable if the pair is controllable, that is, the Kalman matrix has rank .
Linearizing the system at a state and the input gives a linear system whose input matrix has columns . Its controllability Gramian is the solution of the Lyapunov equation
When is stable, (3.9) has exactly one solution for every , and it is symmetric. The claim under test is
A vector field on an open set is integrable (a gradient field) if for some real function .
Example 3.3 is the single-input system (, ) with
and a real parameter . In Lean these are exA, exN ν and exb (with exB the matrix ), equation (3.9) is IsLinGramian, and controllability is IsControllable.
For every , with solving (3.9) for every : the pair is controllable, and for every there is no with
The goal refutes every potential , not only , so it does not depend on how is defined; it is exactly the statement that the field is not integrable on any punctured neighbourhood of the origin, which is how (3.8) is claimed.
The result. The example shows that the state-dependent Gramian of the linearization does not, in general, describe the controllability energy of a bilinear system through (3.8), even for a locally controllable system and arbitrarily close to the origin. As a consequence, the inequalities and derived in [25, 11] from (3.8) lose their justification, and the comparison of with the algebraic Gramian requires the different argument the paper develops in its later sections. The example is a minimal one: two states, one input, one coupling parameter.
Formalizing it. The counterexample is proved in the paper by a hand computation through Kronecker products, and that computation contains a sign slip (see below); a machine-checked version settles the claim independently of it. The result is proved in the paper and, to our knowledge, has not been formalized anywhere. The general derivative formula (milestone 2) is reusable for any parametric Lyapunov equation.
The obvious route is to compute the Jacobian of at one point and observe that it is not symmetric. Two steps of this route need care. First, is defined only implicitly, through (3.9) at every point, so its differentiability in , and that of its inverse, must be derived from the invertibility of the Lyapunov operator and of near the point. Second, passing from "the Jacobian of is not symmetric" to " is not a gradient" requires the symmetry of second derivatives of a function that is only assumed differentiable with gradient on a punctured ball; the regularity of is inherited from that of , not assumed. The goal is also not a statement about a single point: it must hold for every radius , so the asymmetry must be exhibited at points arbitrarily close to the origin, where it is of order .
Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the paper's indices are Fin m. In the goal the plane is EuclideanSpace ℝ (Fin 2) and the potential is required to satisfy HasGradientAt at each point of the punctured ball , with no further regularity.Matrix.inv, which returns at singular matrices; is invertible near the origin, and milestones 2–4 assume invertibility (or ) where they use it.Contributions welcome: proofs of the four milestones, in particular the smooth dependence of the solution of a Lyapunov equation on its right-hand side (milestone 2), which is general and reusable.
Progressive hedging separates a stochastic optimization problem by scenario, solves those smaller problems, and coordinates their first-stage decisions through weighted aggregation and price updates. It is useful when the full extensive formulation is too large to solve directly. For stochastic mixed-integer programs, its iterates can provide feasible decisions, but a feasible cost alone does not reveal how far that cost is from the global optimum. A lower bound gives the missing comparison: the difference between a feasible cost and a valid lower bound is an optimality gap. Branch-and-bound methods also use lower bounds to discard regions whose best possible cost cannot improve the current solution. These are the reasons the authors seek a bound available during a progressive-hedging run, rather than only after convergence. Gade et al., author manuscript, §§1–3.
The paper establishes lower bounds for two-stage stochastic mixed-integer programs, extends them to scenario bundles, and studies their behavior computationally. The mission concerns the mathematical statement that the price vector produced at each completed iteration is eligible for a decomposed lower bound. The paper was published in Mathematical Programming in 2016; the theorem and page labels here follow the authors' SAND2013-9195J manuscript. Gade et al., author manuscript.
Let be a finite set of scenarios and let be their probabilities, with . A first-stage decision is made before the scenario is known. Its first coordinates are nonnegative integers; the others are unrestricted reals. It incurs cost and must satisfy . After scenario is observed, a second-stage decision incurs cost . Its first coordinates are nonnegative integers, and it must satisfy . The recourse matrix is common to all scenarios. The scenario feasible set contains pairs satisfying these restrictions for one . Gade et al., §2, pp. 3–5.
In the extensive scenario formulation, each scenario has a copy of the first-stage vector, and a common vector enforces implementability through . Its optimum is . Algorithm 1 starts with zero prices , solves unpenalized scenario problems, and at iteration computes and . Later scenario solves add both and to their objectives. Here is the algorithm's scalar parameter. Gade et al., Algorithm 1, p. 6.
For any scenario prices , define the decomposed dual value by
Proposition 1 states that prices with satisfy . The price invariant in §3.1 states that the update maintains this weighted zero sum. The mission's goal combines these source claims at every completed iteration of Algorithm 1:
The formal goal is the lower-bound inequality; the zero-sum statement and Proposition 1 are its two milestones. Gade et al., Proposition 1, p. 6, and §3.1, p. 7.
For a partition of the scenarios, a bundle has probability . A bundle subproblem uses one first-stage vector for its scenarios and second-stage weights . Proposition 3 gives the corresponding inequality when . The proposal also records the bundle price invariant and the resulting inequality at each completed bundled iteration as companion statements. Gade et al., §3.3, pp. 9–10.
The scenario bound turns each price vector into an independent set of optimization problems whose weighted values certify a lower bound on the original mixed-integer optimum. The bound does not require the scenario first-stage decisions to agree at that iteration. The bundle result gives the same kind of certificate when several scenarios are solved together. These are the paper's known results, not new open mathematical conjectures. Gade et al., §§3.1 and 3.3.
Formalizing them requires a reusable interface for finite-support stochastic mixed-integer models, their scenario feasible sets, implementability equations, price systems, and finite prefixes of both algorithms. It also separates the general price-feasibility inequality from the algorithmic invariant. The mission currently proposes statements with open Lean proofs; it does not claim a machine-checked proof of these paper results.
An iteration of progressive hedging solves scenario problems with a quadratic proximal term, while the lower-bound calculation uses scenario problems without that term. Their objective values cannot simply be identified. The relevant connection is the price vector: to apply Proposition 1 at an arbitrary iteration, its weighted zero-sum condition must follow from the actual aggregation and price-update rules. The bundle version adds normalization by , so every bundle must have positive mass and the bundle weights must cover the full scenario distribution. Gade et al., §§3.1 and 3.3.
Lean represents vectors as Fin n → ℝ, linear constraints componentwise, and the extensive formulation with the weighted implementability equation printed in (15). The dimensions satisfy and , as required by the paper's spaces . The finite scenario weights are positive and sum to one. The first integer coordinates are nonnegative; every remaining real coordinate is free. The paper's assumptions that the SMIP has an attained finite optimum and each is nonempty are explicit in the goal and Propositions 1 and 3. The scenario and bundle subproblem values, and , live in the extended reals: an unbounded-below subproblem retains rather than acquiring an arbitrary real infimum. Gade et al., §§2–3.
An algorithm run is a finite prefix through its last aggregation and price update, with exact minimizers recorded as conditions on its sequences; a stopping test truncates the prefix. The proximal term is the Euclidean sum of squared coordinate differences. No positivity condition on is added to the lower-bound statements, since the page does not require one for these claims. Bundles form a partition, but equal bundle sizes are not required for the inequalities. Algorithm 2's printed w^ν(i) at initialization and Σ_i P_β x^ν(β) at aggregation are read with bundle indices. A bundle recourse vector is represented as a function on all scenarios, with only its coordinates inside the bundle constrained or used.
The exact equations of the scenario model and runs prevent a trivial encoding that assumes dual feasibility or the desired bound as part of a run. Contributions to the model, the price invariants, the extended-real weak-duality arguments, and the bundle extension are all within scope. The paper's convexified limit result (Proposition 2), its cited Theorem 1, and multi-stage Algorithm 3 are outside this mission.
Benders decomposition solves an optimization problem in two groups of variables by fixing one group, solving the remaining subproblem, and turning what the subproblem's solution proves into a constraint, the Benders cut, on the fixed variables. In the classical method of Benders (1962) the subproblem is a linear program and the cut comes from its LP dual. Many problems that decompose naturally have subproblems that are not linear programs: scheduling, satisfiability, 0-1 and constraint programs. Hooker and Ottosson (Math. Program. 96, 2003) replaced the LP dual by the inference dual, the problem of inferring the strongest bound on the objective from the constraints, and obtained a Benders scheme in which any sound inference method produces cuts. This logic-based Benders decomposition has since become a standard technique for planning and scheduling problems that combine an assignment master problem with combinatorial subproblems.
The correctness of the generic scheme rests on two short theorems of the paper. Theorem 1 says that if every cut is valid, then each of the algorithm's three ways of stopping reports the right answer. Theorem 2 says that the algorithm stops when the fixed variables range over a finite set. This mission formalizes both theorems, together with the facts used in the proof of Theorem 1.
An optimization problem (1) has a domain , a feasible set and a real-valued objective ; its value is . Optimal values lie in : an infeasible minimization has value , an unbounded one , and the reverse holds for maximization. For propositions about , implies with respect to , written , if holds at every where holds. The inference dual (2) of (1) is
In Benders decomposition the variables are pairs with , , and problem (6) is over . Fixing at a trial value gives the subproblem (7), over , with inference dual (8): s.t. . A bounding function defines the cut . The cut satisfies
(B1) if every feasible of (6) satisfies , and
(B2) if , the value obtained in the subproblem dual.
The cuts generated so far form the master problem (9): s.t. for every cut , .
The generic Benders algorithm (Figure 1 of the paper) starts with and some . While the subproblem dual at has a feasible , it formulates with and adds its cut. If the master is then infeasible, it stops and reports (6) infeasible. Otherwise it takes an optimal solution of the master and repeats. When the loop exits, the optimal value of (6) is reported as .
In Lean, LogicBenders.Generic.Setting defines all of these objects: optVal, subVal, IsDualFeasible, ValidCut, masterLHS, IsMasterOptimal and MasterInfeasible, and a Run with the predicates IsRun, StopsAtWhile and StopsAtMaster.
Assume (B1) for every cut the run has added. Then three statements hold.
If (B1) and (B2) hold, is finite, and the subproblem dual is solved to optimality, then no run of the algorithm continues forever.
Lemma 3 (p. 20) gives a criterion for a 0-1 inequality to imply the branching clause (29). The §4 statement (p. 7) characterizes when a feasible linear system implies .
Theorem 1 is what allows any sound inference method to supply Benders cuts. Correctness needs only (B1), so the method that derives the cuts (resolution, constraint propagation, a branch-and-bound proof, LP duality) never has to be re-verified at the level of the decomposition. The paper's specializations to satisfiability, 0-1 programming and machine scheduling, and much of the later literature on logic-based Benders, rely on this theorem when they check validity of their cuts and nothing more. Theorem 2 is the matching termination guarantee, and the example on p. 10 shows that the finiteness of cannot be dropped.
Both theorems are proved in the paper, and to the extent known no machine-checked version exists. A formalization makes the paper's implicit conventions precise: values in , what "the subproblem dual is infeasible" means when is always a feasible bound, and exactly which cuts the master contains at each iteration. It also exposes two gaps in the printed proofs. Theorem 1's first clause uses the attainment of the subproblem optimum without stating it. Theorem 2's printed proof claims the subproblem value increases at every iteration, which is false, although the theorem itself is true. The definitions form a small reusable layer for later formalizations of specific logic-based Benders schemes.
The mathematics is elementary, and the difficulty lies in stating it faithfully. Several readings of the statements are wrong. A "run" whose are not master optima for exactly the cuts generated so far makes Theorem 1 false. Optimal values taken as real infima turn the infeasible case into junk. Defining "dual infeasible" over the extended reals makes clause 3 vacuous. For Theorem 2, the obvious argument is the printed one, that (or ) increases strictly. It fails: with three values of and cuts equal to away from their own , the subproblem value can decrease between iterations while stays fixed. The printed argument therefore cannot be transcribed, and the theorem needs a proof the page does not give.
X stands for , Y for and D for . The feasible set is S : Set (X × Y) and the objective is f : X → Y → ℝ. Optimal values are EReal infima and suprema, with for infeasible and for unbounded problems.EReal, so is always feasible. "The subproblem dual is infeasible" is therefore stated as "no real is feasible". A master optimum means and is at most that maximum at every ; the value means the master is unbounded.ybar k, has bound zbar k, and adds cut k. The structure IsRun encodes Figure 1 exactly: zbar 0 = ⊥, every iteration finds a dual-feasible beta k > zbar k with cut k (ybar k) = beta k, and the next is a master optimum for exactly the cuts 0, …, k. An unconstrained "run", or a dual infeasibility that satisfies vacuously, would trivialize the goal, and both are ruled out by these definitions.Retailers decide which product variants to stock, and most assortment-planning tools model consumer choice with the multinomial logit (MNL) model: a consumer who does not find an acceptable variant simply leaves without buying. Cachon, Terwiesch and Xu (Retail Assortment Planning in the Presence of Consumer Search, working paper of December 2002; published in MSOM 7(4), 2005, doi:10.1287/msom.1050.0088) point out that consumers also search: a consumer who likes what the store offers may still walk out to look elsewhere, and that is more likely when the assortment is narrow.
In practice a retailer does not know consumer preferences; it estimates them from sales data and re-plans. This mission formalizes §5.1 of the paper, which asks what happens when a retailer runs this estimate-and-replan loop with the traditional no-search MNL model while consumers actually search. The loop can settle at a heuristic equilibrium in the sense of Cachon and Kok (2002), and the question is how that equilibrium compares with the truly optimal assortment.
There are product variants, labelled from most to least popular, with preferences , and a no-purchase option ("variant 0") with preference . An assortment of depth is the set . Variant has margin , with whenever (monotone margins, p. 6), and carrying it at demand incurs an operational cost , where is concave and increasing on (demand is normalised to one consumer).
True demand: the independent assortment model. With a constant (Theorem 1 of the paper: ) and , the probability that a consumer searches is , and variant has demand
The no-purchase demand is , and the true profit is .
Estimates. Observing for , the retailer fits the MNL model, normalised by : for , and for variants not carried it reuses the estimates from an initial depth test with the full assortment. The no-search model fed with preferences predicts the shares and the profit .
Heuristic equilibrium. A depth is a heuristic equilibrium when maximises over : the assortment is optimal for the estimated preferences, and the estimates are those observed under the assortment. An optimal depth maximises the true profit over .
If is a heuristic equilibrium and is an optimal depth such that every deeper depth is strictly worse ( for ), then
Theorem 8 says that a retailer who ignores consumer search and plans iteratively from its own sales data can only err on the side of a too-narrow assortment, never a too-deep one. The bias is structural: Theorem 7 shows that the estimates get every product variant's relative preference right but misjudge the no-purchase option in a direction fixed by the depth. The result thus separates the part of the MNL model that survives consumer search (IIA among products) from the part that does not (IIA with respect to the no-purchase option).
The results are proved in the paper, by short arguments, but some steps are only asserted: the non-negativity of variant profits at the equilibrium is attributed to "the previous section", and the overlapping assortment model is dismissed with "the similar process". No machine-checked proof of these results is known. A formalization makes explicit the hypotheses the paper leaves implicit (, and a strict-deeper condition on in place of the presumed uniqueness of the optimum), and delivers a reusable formal model of MNL estimation under search.
Each step is elementary, and the difficulty lies in keeping two profit functions apart and carrying the right inequalities between them. The tempting shortcut, "the estimates are correct, so the no-search optimum is the true optimum", fails: the estimates are correct only up to the no-purchase preference , which depends on , and that single number shifts every predicted share. The proof of Theorem 7 must reduce the comparison of and to the monotonicity of the function . The step from no-purchase demand to profit needs every predicted variant profit to be non-negative, which requires the monotone labelling of preferences and margins together with concavity of and ; the paper asserts it without proof.
Fin n, 0-based: the paper's variant is index . Depths are natural numbers, and depth is the published RetailVariety.Structure.popularSet n x; the MNL share is the published RetailVariety.Structure.share.Fin n; its preference and estimate are separate reals.Trivializing formalizations are ruled out: the estimates are not the true preferences (in particular , which would force ); is not an arbitrary maximiser but one with all deeper depths strictly worse; , where nothing is observed, is excluded rather than given junk estimates; and nothing is claimed for the overlapping model.
Contributions welcome: proofs of the milestones, in particular Theorem 7 and the positivity step, and a formal treatment of the overlapping model with its additional hypotheses.
A retailer choosing which variants of a product to stock (colours, sizes, models) faces a trade-off that operations management has studied since van Ryzin and Mahajan (1999): a deeper assortment attracts more purchases, but each added variant takes demand away from the variants already on the shelf. This loss is called cannibalization. In the standard model of consumer choice, the multinomial logit (MNL), cannibalization holds exactly: every variant's purchase probability falls when a variant is added.
The MNL assumes that a consumer who walks into a store buys either from that store or nothing. Real consumers can also leave to search elsewhere, and a deeper assortment makes them less likely to leave. Cachon, Terwiesch and Xu (working paper, 2002; published in Manufacturing & Service Operations Management, 2005, doi:10.1287/msom.1050.0088) add search to the MNL and ask whether cannibalization survives. Two forces now act on a variant's demand when the assortment expands: the share of buyers who choose it falls, and the share of consumers who stay in the store rises. This mission formalizes their answer for the first of their two search models, the independent assortment model, in which the outside option does not depend on what the retailer stocks.
There are possible variants ; the retailer stocks an assortment . A faux variant represents not buying.
Gumbel shocks. Fix a scale and let be Euler's constant. The zero-mean Gumbel law with scale has distribution function and density
Utilities. Variant has expected net utility (utility minus price), and the no-purchase option has (its price is ). A consumer's realised utilities are and , with independent and Gumbel. The preference of variant is , and .
No search. The consumer buys the variant of with the highest utility, or nothing if is higher. The probability that she buys is .
Search. A consumer may instead search at a cost and receive , where is another independent Gumbel shock that she has not yet observed. Having seen , the best utility in the store, she searches when the expected gain minus the expected loss is at least :
The independent-assortment demand is the probability that variant has the highest utility in , beats the no-purchase option, and the consumer does not search. Write (the search threshold), and .
For all and with ,
The goal leaves the utilities , , , the search cost , the scale and the number of variants arbitrary.
Theorem 1 says that under independent-assortment search the demand for every stocked variant is its MNL demand scaled by one common factor, the probability that the best option in the store clears the threshold . The threshold itself does not depend on the assortment. Theorem 2 then shows that the MNL's cannibalization effect dominates the retention effect of a deeper assortment, so each variant's demand still falls strictly when variants are added. The paper's later results on the shape of the profit function and on the structure of optimal assortments under search build on this closed form.
The paper's proofs are short but rely on steps it states without proof: the MNL formula is cited from Anderson, de Palma and Thisse (1992), the search rule is obtained "after rearranging terms", and the closed form follows from a change of variables. No machine-checked version of these steps is known. The mission produces a checked derivation of a logit-type closed form from an explicit random-utility model with an outside option and an endogenous stopping decision, at the paper's scale and with its centring constant .
Theorem 2 is not monotonicity of a single fraction. Adding a variant enlarges the denominator of and simultaneously raises the factor , so the sign of the change is a competition between the two, and a bound on either factor alone does not settle it. The comparison becomes one-dimensional only after Theorem 1 is available, and Theorem 1 itself requires computing a probability of an event defined by finitely many strict inequalities among independent Gumbel variables together with the consumer's search decision. That calculation is an iterated integral over the product law, with the decision rule, the mean of the Gumbel law and the change of variables each needing their own justification.
Fin n, 0-based (the paper's variant is index ). The no-purchase option is the extra index none of Option (Fin n). Assortments are Finset (Fin n), and is S ⊂ Splus.IsZeroMeanGumbel μ G says the probability measure G on ℝ has distribution function above; and is Real.eulerMascheroniConstant. Such a law exists for every (checked sorry-free locally).Option (Fin n) → ℝ with the product measure Measure.pi (fun _ => G). The search shock does not appear in it: the consumer decides before observing , so only its law enters, as integration against G in the search rule.noSearchProb) and (searchProb) are the real values of the probabilities of the choice events, with strict inequalities. The search event uses the paper's decision rule (the displayed integral), not the threshold ; the equivalence is a milestone. The closed form is the published RetailVariety.Structure.share.Ruled out. Demand defined by the closed form (3), which would make Theorem 1 true by definition and Theorem 2 a calculus fact; Theorem 2 with and ; a standard Gumbel law (scale , mean ) in place of the paper's zero-mean scale- law; and a model without the no-purchase option.
Infrastructure. A complete development needs the distribution theory of the Gumbel law (density, mean), choice probabilities of products of i.i.d. continuous variables as iterated integrals, and calculus for . The Gumbel and MNL lemmas are reusable for any logit-based choice model, including the other missions of this series. Contributions of proofs of any milestone, or of general MNL infrastructure that the milestones can import, are welcome.
A retailer deciding which variants of a product to stock trades off two effects. A deeper assortment captures consumers whose favourite variant would otherwise be missing, but it splits demand among more variants, each of which then carries its operational costs (shelf space, handling, inventory) at a smaller, less efficient scale. Van Ryzin and Mahajan (Management Science 1999) showed that under multinomial-logit (MNL) demand the optimal assortment consists of the most popular variants, which reduces the search over assortments to candidates.
Cachon, Terwiesch and Xu (working paper, 2002; published in MSOM 2005) add consumer search: a consumer who finds nothing good enough in the store may leave to look elsewhere, and a deeper assortment makes that less likely. In their independent-assortment model the search threshold does not depend on the store's assortment, but the fraction of consumers who stay does. This mission formalizes their Theorem 5: even with this extra dependence, the profit change from adding a variant is quasi-convex in that variant's preference.
There are variants. Variant has a preference and the no-purchase option has preference (in the paper , with the net utility and the Gumbel scale). For an assortment the MNL purchase probability without search is
A consumer searches when her best alternative in the store, including no purchase, falls below a threshold . With Euler's constant and , this happens with probability , and by the paper's Theorem 1 the independent-assortment demand is
Each variant sold earns a margin , and stocking a variant with demand costs , where the cost function is concave and increasing on (economies of scale). Variant 's profit is . Write .
Fix and a variant , and treat 's preference as a variable. Let be variant 's profit in ; its demand carries the factor , not . The cannibalization loss and the profit change are
Quasi-convexity of says that a variant is worth adding, if at all, at an extreme of its popularity. The paper uses it to conclude that, as without search, the optimal assortment under independent-assortment search lies among the popular assortments, the sets of the most preferred variants. This reduces assortment optimization to candidates. The paper also shows that the conclusion fails in its overlapping-assortment model, so the independent-assortment case marks where this structural result survives the addition of search.
The result is proved in the paper; none of it has a machine-checked proof. The paper's proof contains gaps that a formalization must close: several sign and monotonicity facts are asserted without proof ("It can be shown", "by a similar argument as in Theorem 4"), display (8) is printed without a factor , and the step from (10) to (11) rests on an inequality asserted without the full expression. A complete formal proof of Theorem 5 therefore also fixes the argument.
The no-search analogue (Theorem 4) is easy: the numerator of is increasing, so changes sign at most once. Here the search factor depends on , and the derivative splits as with , , nondecreasing and nonincreasing, but neither nor is monotone. So the argument used for Theorem 4 no longer applies, and when and the derivative cannot be written as a positive factor times a monotone one. The proof needs a separate second-order argument at critical points in that case. Showing only that has at most one zero is also not enough: it must change sign from negative to positive.
Fin n (0-based); the no-purchase option is a separate real v0 > 0, not an element of Fin n. All preferences are positive. The MNL probability is the published RetailVariety.Structure.share, referenced, not redefined.deriv c. The value is unconstrained; .Function.update v j x on insert j S, with . Quasi-convexity is Mathlib's QuasiconvexOn ℝ (Set.Ici 0).A retailer that sells a product in many variants (colours, sizes, flavours) has to decide which variants to stock. This is the assortment planning problem. Each variant added to the shelf brings new demand. It also cannibalizes demand from the variants already stocked, and it lowers their cost efficiency, because operational costs (shelf space, handling, holding) usually show economies of scale. Cachon, Terwiesch and Xu, in Retail Assortment Planning in the Presence of Consumer Search (Wharton working paper, December 2002), study this trade-off under the multinomial logit (MNL) model of consumer choice. They compare a model without consumer search with two models in which consumers may leave to search elsewhere.
There are nonempty assortments of variants, so full enumeration is impractical. The retailer wants to know whether attention can be restricted to the popular assortments , the assortments made of the most preferred variants.
Timeline. Van Ryzin and Mahajan (Management Science 45(11), 1999, doi:10.1287/mnsc.45.11.1496) showed that, without search and with a cost derived from the newsvendor model, the profit change from adding a variant is quasi-convex in that variant's preference. As a consequence, the optimal assortment is a popular one. Cachon, Terwiesch and Xu (working paper 2002; Manufacturing & Service Operations Management 7(4), 2005, doi:10.1287/msom.1050.0088) extended the quasi-convexity to any concave increasing cost (Theorem 4 of the working paper), and then to search with independent assortments (Theorem 5). This mission formalizes Theorem 4.
Let be the possible variants. Variant has a preference ; in the paper , where is the variant's expected net utility and is the Gumbel scale. The no-purchase option has preference . With assortment , the MNL demand of variant is
Variant has margin (price minus purchase cost). Stocking it incurs an operational cost , where the cost function is concave and increasing on (the consumer population is normalised to , so demands lie in ). The profit of variant is , and the retailer's profit is .
Fix and a variant , and let . Treat 's preference as a variable. Write for variant 's demand with assortment , and for its profit. The loss on the variants already stocked is
and the net profit change from adding is . Adding is profitable exactly when . Write .
that is, every sublevel set is an interval. The goal holds for every concave increasing and every choice of margins, and assumes no differentiability.
The result. A quasi-convex function on an interval attains its maximum at an endpoint. So if adding a less preferred variant to is profitable, adding a more preferred variant (with ) is at least as profitable. With monotone margins, this exchange argument shows that an optimal assortment with variants consists of the most popular variants. The search for the optimal assortment then reduces from candidates to . The paper uses this structure again for the search model with independent assortments (Theorem 5) and in its analysis of a heuristic equilibrium (Theorem 8).
Formalizing it. The theorem is proved in the paper, and is not known to have been formalized anywhere. The mission produces a machine-checked proof for an arbitrary concave increasing cost, with per-variant margins. The paper's proof differentiates and writes a single common margin. A formal proof settles that neither assumption is needed. Van Ryzin and Mahajan's newsvendor-specific Lemma 1 is posed separately on Prove2Me (RetailVariety.Structure.lemma_1). It concerns a different function, a ratio on , and is not a special case of the statement here.
Adding changes every demand at once: 's own demand rises while all of 's demands fall, each through the shared denominator . The obvious approach is to show that is convex, and it fails: is in general not convex in , for example, when is linear and every margin equals some , is a positive multiple of the concave demand plus a constant. The paper's own argument goes through the derivative (6). It needs a derivative of , and its last step ("at most one with ") is literally false when the numerator of (6) vanishes on an interval, for instance when is linear with slope equal to a common margin, so that is constant. A rigorous proof must handle a non-differentiable concave , the endpoint where 's demand is , and a numerator that may be constant on stretches.
Fin n, 0-based (the paper's variant is index ). The no-purchase option is not a variant: is a separate real, with and for all .RetailVariety.Structure.share (from RetailVariety.Structure.Model), with assortments as Finset (Fin n). is share applied to the preference vector with 's entry replaced by the variable, on insert j S, and is assumed.ConcaveOn ℝ (Set.Icc 0 1) c, MonotoneOn c (Set.Icc 0 1)). Nothing is assumed about , so .m : Fin n → ℝ are arbitrary reals. The monotone-margin assumption of §3 is not needed and not imposed.QuasiconvexOn ℝ (Set.Ici 0). The domain is the closed half-line, including .deriv c. The goal does not.The following formalizations would trivialize the problem and are ruled out: a specific cost (newsvendor, power, linear); convexity instead of quasi-convexity; only on ; or a common margin imposed without need.
Contributions welcome: proofs of the milestones, a proof of the goal that avoids derivatives, and general lemmas on quasi-convex functions of one variable and on the algebra of MNL shares, which the companion missions of this series (I and III–V) can reuse.
Treewidth measures how closely a graph resembles a tree. Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (SIAM J. Comput. 45(2), 2016) study an algorithm for producing tree decompositions. Its headline result is algorithmic; this mission formalizes one combinatorial lemma used in its analysis.
In §4.3.2, p. 349, the authors isolate a purely combinatorial fact, Lemma 4.3, which bounds the number of nodes of a rooted tree in terms of a measure placed on its nodes. They use it for the partial tree decomposition built by FindPartialTD, with a measure of the form . This mission formalizes Lemma 4.3 and the steps of its proof. The lemma is self-contained and does not mention graphs or treewidth.
A rooted tree consists of a finite vertex set , a root , and a parent map defined on such that every vertex reaches by iterating . If , then is a child of and is the parent of . A vertex without children is a leaf. The descendants of are the vertices with for some (including itself), and the subtree rooted at is the tree they span; is its number of vertices, and .
A measure is any function . Lemma 4.3 considers measures with three properties, for a constant :
Throughout, .
Under properties (i)–(iii),
Each step is stated for an arbitrary vertex of , with the subtree in the role of the paper's tree.
The result. Lemma 4.3 converts two local conditions, superadditivity of the measure over the children of each node and geometric decay by a factor along each parent–child edge, into a global linear bound on the size of the tree. Superadditivity alone does not bound the size: a long path with constant measure satisfies (i) and (ii). Decay alone does not either: a star with many leaves satisfies (iii). The counting principle can also be used when a recursive construction splits a resource among child nodes while reducing that resource along every edge.
Formalizing it. The lemma is proved in the paper. The mission produces formal statements of the lemma and the main bounds in its proof, over a published, reusable encoding of finite rooted trees by parent maps. A complete development would also establish structural facts about descendants and children that can be reused for other results about finite rooted trees.
The summed bound for the children's subtrees contains the term . When , superadditivity alone does not give the target's final : a path with constant measure is a counterexample if geometric decay is omitted. Formalization also has to account for the fact that the reusable tree representation is a parent map on a finite type, rather than an inductively constructed tree.
The rooted tree is the published definition HarelTarjan.Compressed.RootedTree: a finite vertex type V with a root and a total parent map in which every vertex reaches the root, with the convention . is Fintype.card V, and is the published subtree size size T v (the number of descendants of , including ). The local definition file adds IsChild T v c ( and ) and children T v; the condition removes the pseudo-edge , so the root is never its own child.
Conventions: is real valued, as on the page; property (ii) is a sum over a possibly empty set of children; the constant of property (iii) is a parameter with the two hypotheses and , because the conclusion is stated with that same . The fraction is real division, and the hypothesis keeps it away from Lean's convention . The bound keeps the page's "".
A trivializing formalization is ruled out explicitly: the parent–child relation is directed by the root, so property (iii) constrains each edge in one direction only. A symmetric reading (" for all adjacent ") would be unsatisfiable for and make every statement vacuous; the hypotheses here are satisfied, for example, by the two-vertex tree with and .
A complete development needs the decomposition of size T v as and an induction principle for parent-map trees. Both are reusable for statements about rooted trees given by parent maps, and contributions of them as separate lemmas are welcome. The paper's subsequent application is outside this mission's scope.
Classical mean field theory describes exchangeable diffusions, each interacting with the empirical average of all the others. As the particles become independent copies of a McKean–Vlasov process (propagation of chaos). Many systems of interest are not exchangeable. Particles sit at the vertices of a network and interact only with their neighbours, as in models of opinion dynamics, epidemics on contact networks, synchronisation of oscillators and systemic risk in financial networks. When the network is dense and its adjacency structure converges, the natural limit object is a graphon, a symmetric measurable function that encodes the limiting edge density between "positions" (Lovász, Large Networks and Graph Limits, 2012).
Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) develop a law of large numbers for such systems. This mission formalizes their second main result, Theorem 3.1. Under cut-metric convergence of the interaction kernels, the empirical measure of the -particle system converges in probability to the averaged law of a continuum graphon particle system. Related work includes Bhamidi, Budhiraja and Wu (Stochastic Process. Appl., 2019) on weakly interacting particles on inhomogeneous random graphs, Coppini, Dietert and Giacomin (Stoch. Dyn., 2020) on Erdős–Rényi graphs, and Bet, Coppini and Nardi (arXiv:2006.07670) on oscillators on dense random graphs.
Write with Lebesgue measure and fix a horizon . Let with the uniform norm . On one probability space take independent initial states with laws and independent -dimensional Brownian motions , for all . The graphon particle system (2.1) for a graphon and Lipschitz coefficients is the continuum of nonlinear diffusions
where is the law of . Write for the path law of and for the averaged law.
The -particle system (3.1) places particle at label , starts it at , drives it by , and weights its interaction with particle by :
The weights come from a step graphon , constant on the squares of the -grid. Either , or are independent Bernoulli variables for , independent of the noise (Condition 3.1). The kernels converge in the cut norm . Two further norms appear: the operator norm , and the Wasserstein-2 distance on .
Assume the initial laws are measurable in with a uniform -moment and are Lipschitz (Condition 2.1). Assume is -continuous on each interval of a finite cover of (Condition 2.2(a)), and that Condition 3.1 holds with in the cut metric. Then
If, in addition, is continuous at for a.e. at each interior point of the cover (Condition 2.2(b)), then
In order: Remark 2.1, where cut-norm convergence implies operator-norm convergence; Theorem 2.1(a), continuity of in ; the weak-LLN bound (6.4); the discretization bound (6.11); Lemma 6.1,
Lemma 6.2, a law of large numbers for the continuum particles ; the approximation of by continuous graphons; the continuity (6.12) of in the graphon, in a corrected qualitative form; the empirical coupling bound for ; and (6.14).
Theorem 3.1 shows that the averaged graphon law is the correct macroscopic description of a dense heterogeneous particle system. This holds for deterministic weights and for Erdős–Rényi-type random weights, and the graphon may be discontinuous. It is the foundation for graphon mean field games and for control of large networked systems, where replaces the intractable -particle law. Under the regularity Condition 2.2(b) the convergence holds in , particle by particle, along the natural coupling.
The result is proved in the paper (§6.1–§6.2). Nothing in it is formalized. A formal proof would produce reusable infrastructure: graphons, the cut and operator norms, Lusin approximation of graphons, Wasserstein distances between empirical measures, and laws of large numbers for random probability measures on path space. It also needs pathwise stability estimates for SDE systems built on Itô integrals, which goes well beyond what Mathlib has today.
The particles are neither exchangeable nor identically distributed. The classical propagation-of-chaos argument compares each particle with an i.i.d. copy of one McKean–Vlasov process, and it does not apply here. Each must be compared with its own limit , and the error has two sources: the random or discretized weights , and the replacement of by . Cut-metric convergence controls only through integrals against bounded test functions. The interaction term, however, integrates the unbounded function against varying laws . When is merely measurable, the map need not be continuous, and the error of replacing by the average over the labels need not vanish. The direct estimate therefore fails for (3.3) without Condition 2.2(b), and this is the case the goal must cover.
The setting file GraphonMF.DenseLLN.Setting fixes these conventions:
Fin d → ℝ with the sup norm. All statements are invariant under this choice: constants are existential and the other conclusions are limits.Peng1990.SMP.IsItoProcess. The filtrations are the uncompleted natural filtrations and .WassersteinDRO.Duality.wassersteinDistance with values in .Two encodings would trivialize the targets, and both are ruled out. A pointwise or almost-sure reading of (3.3), or convergence of for a single test function, is not the claim. Choosing the constants of Lemma 6.1 and (6.11) after the sequence would make them nearly empty, so they are chosen before it. A sorry-free check confirms that the solution predicates are satisfiable: with the constant paths solve both systems.
Solvers will need several pieces of library work: the inequality , BDG-type moment bounds for the Itô integrals of Peng's library, Gronwall estimates, Lusin's theorem on , and the metrization of weak convergence on (Lévy–Prokhorov). Contributions to any of these are welcome independently of the goal. The paper's proofs are in its §5 (Theorem 2.1) and §6.1–§6.2 (Lemmas 6.1, 6.2 and Theorem 3.1).
Policy gradient methods optimize a parameterized policy for a Markov decision process by local search on its expected cost. The objective is nonconvex, so local search can in principle stall at a poor stationary point. Bhandari and Russo, Global Optimality Guarantees for Policy Gradient Methods show that for a broad family of control problems this does not happen, and, in quantitative form, that the objective is gradient dominated: its suboptimality is bounded by a multiple of the size of its gradient. The multiple involves a single problem-dependent quantity, the effective concentrability coefficient , which measures how well the initial state distribution covers the states that matter for optimal behaviour. Theorem 2 and the convergence rates of Theorem 5 of the paper are only informative when is finite, so sufficient conditions for a finite are what make those results usable. This mission formalizes the paper's three such conditions (Theorem 4).
Distribution-mismatch coefficients of this kind go back to Kakade and Langford (2002), and appear in the analyses of approximate dynamic programming by Scherrer and Geist (2014) and of policy gradient methods in finite MDPs by Agarwal et al. (2021).
A discounted Markov decision process consists of a measurable state space , nonempty feasible action sets , a bounded measurable per-period cost , a transition kernel , a discount factor and an initial probability distribution on . A feasible measurable stationary policy () picks an action in every state. Its cost-to-go is the expected discounted cost from , its discounted state-occupancy measure is
and its average cost is . The Bellman operator acts on bounded measurable functions by
An optimal policy minimizes at every state; . A policy class is indexed by a convex set , and .
The effective concentrability coefficient (Definition 3) is the smallest scalar such that
with , and if no scalar works. It converts a -weighted Bellman error into a -weighted optimality gap.
If for every measurable set , then satisfies (13); equivalently
(a) If is finite and for all , then . (c) If is a contraction with modulus in a norm with , then .
The element-wise inequalities , (5); the performance difference identity (29); the sup-norm bound (26); the occupancy-weighted inequality from the proof of part (b); and the contraction step from the proof of part (c).
Theorem 4 is what turns the paper's gradient-dominance theorem into a usable statement: with part (b), the constant in Theorem 2 is bounded by the worst-case likelihood ratio between the optimal policy's state distribution and the initial distribution, a quantity that can be checked without knowing the policy class. Part (a) shows that in finite problems any fully supported initial distribution suffices, and part (c) gives a route through weighted norms, used in the paper for optimal stopping (Lemma 13).
The results are proved in the paper. None of them is machine-checked. The mission produces a general-state-space formalization of the discounted cost MDP (kernels, occupancy measures, Bellman operators, measurable selection) together with the performance difference identity on measurable state spaces; existing formal developments of policy gradient theory on the platform are for finite MDPs only. The occupancy-measure and Bellman-operator layer is shared with the other missions of this series.
The argument for part (b) is short on paper, but each step is a measure-theoretic statement about infinite-horizon objects. The performance difference identity (29) exchanges an infinite discounted sum with integration against the chain's laws and needs the occupancy measure to be built from the -step kernels of the controlled chain. The change of measure from to needs the Bellman error to be nonnegative and integrable; its measurability is not automatic, because is a pointwise minimum over uncountably many actions, and is supplied by the measurable selection assumption. Part (c) needs the fixed-point property of the optimal cost-to-go, which again rests on measurable selection.
All statements use one Lean layer: MDP S A with measurable spaces S, A (a generalization of the paper's Borel subsets of Euclidean spaces), the cost and kernel given on all of , measurable stationary policies MPolicy S A, and costToGo, occupancy, loss, bellmanPi, bellmanOpt. The paper prints the Bellman operators (3)–(4) without the discount factor; every later use includes it, and so does the formalization. The optimal policy is a binder πstar with IsOptimal M πstar. Assumptions 1 and 2 of the paper are standing hypotheses of every main statement.
The coefficient is never formed as a number: "" is the predicate IsConcBound M Θ πθ πstar X, which says that satisfies (13); because the right-hand side of (13) is nondecreasing in the scalar, the two are equivalent. Part (b) quantifies over every with setwise, which is equivalent to ; a real-valued essential supremum is avoided because it reads exactly when the paper's bound is infinite. Part (a) assumes for every state, since otherwise is on paper and in Lean. Part (c) requires the norm comparison (21) on all bounded measurable functions, as its proof uses it on and , and encodes "a norm" by subadditivity, the one property used.
A formalization in which (13) or the occupancy-weighted inequality is assumed, or in which is a junk value of an empty infimum, would make the goal trivial; neither is used.
Contributions are welcome on every milestone, in particular on the performance difference identity and the measurability of the cost-to-go and of , which are reusable for any discounted MDP on a measurable state space.
Policy gradient methods optimize a parameterized policy by gradient descent on its expected total cost. They are a staple of reinforcement learning and of simulation-based optimization in operations research, but the objective is nonconvex in the policy parameters, and the standard theory guarantees convergence only to a stationary point. J. Bhandari and D. Russo (arXiv:1906.01786v3, Operations Research, 2024, DOI 10.1287/opre.2021.0014) identify structural conditions under which every stationary point is globally optimal.
Their first result (Theorem 1) requires the policy class to be closed under policy improvement. That excludes many classes used in practice, where it is known only that some member of the class is optimal: base-stock policies in finite-horizon inventory control are the standard example (Bertsekas, Dynamic Programming and Optimal Control, 1995). For stationary policy classes, containing an optimal policy is not enough: the paper's Example 1 has a policy class that contains the optimal policy, and policy gradient still gets stuck in a bad local minimum. Theorem 3 shows that for finite-horizon problems with a non-stationary policy class (separate parameters for each period), containing an optimal policy suffices, together with a single-period regularity condition imposed only at the optimal cost-to-go. This mission formalizes Theorem 3.
A Markov decision process consists of a state space , nonempty feasible action sets , a bounded measurable cost , a transition kernel , a discount factor and an initial distribution . A policy is a measurable map with ; is the set of all of them. The cost-to-go is , the loss is , and the discounted state-occupancy measure is . An optimal policy has pointwise for all ; . With the Bellman operator , the weighted policy-iteration objective is
A parameterized policy class is for a convex , and . A point is stationary for if is differentiable at and for all .
The finite-horizon structure (Condition 3) embeds a time-inhomogeneous problem in this discounted formulation: the states split into stages ; from a state in , , every feasible action leads to ; and is a costless absorbing state. The parameter is a concatenation , the parameter set is a product , and on the action depends only on . The stage objectives are .
Condition 4 asks that for every , the problem has no suboptimal stationary points. Assumption 3 asks that for every . Condition 0 asks that the policy-iteration objective be continuously differentiable in the parameters.
Under Conditions 0, 3 and 4 and Assumption 3, if is an optimal policy for some , then every stationary point of on satisfies
Theorem 3 covers finite-horizon dynamic programs in which a structured class of time-varying policies is known to contain an optimal policy, but is not closed under policy improvement: the paper's Example 8, multi-period inventory control with base-stock policies, is the motivating case. Policy gradient on such a class has no suboptimal stationary points, so any method that finds a stationary point finds a globally optimal policy, optimal among all policies and not only within the class. Condition 4 involves only the Bellman objective of the optimal cost-to-go , which often has regularity (for instance convexity) that the cost-to-go of an arbitrary policy lacks.
The result is proved in the paper. To our knowledge no part of it, nor the policy gradient theorem for deterministic policies on general state spaces, has a machine-checked proof. Formalizing it requires a measure-theoretic treatment of occupancy measures, the stage-wise decomposition of the weighted policy-iteration objective, and the backward induction of App. D.2.
The obvious approach reasons stage by stage directly on , but couples the stages: changing changes the distribution of states visited after stage . The paper's argument instead passes through the policy gradient theorem, which turns stationarity of into stationarity of single-period problems weighted by the occupancy measure of the current policy. These single-period problems involve , while Condition 4 speaks about ; relating them requires a backward induction over stages in which almost-sure equality on stage is transported to stage through the balance equation. This step needs the occupancy measures of all policies in the class, including policies other than , to be equivalent to , which is where Assumption 3 enters. The naive variant with a stationary policy class fails (Example 1).
The state and action spaces are arbitrary measurable spaces (the paper takes Borel subsets of Euclidean spaces; no argument uses that structure). Cost and kernel are given on all state-action pairs; the cost is bounded. Policies are deterministic, stationary and measurable; parameters live in EuclideanSpace ℝ (Fin d), so gradients and norms are Euclidean. is never defined as an infimum: an optimal policy is a hypothesis, with . Stages and sub-vectors are numbered from by a measurable stage index and a block index on coordinates; the product structure of is encoded as closure under exchanging one block.
Hypotheses beyond the printed sentence of Theorem 3, all disclosed in the item statements: Assumption 3 (announced on p. 17 as required, used in the proof); Condition 0 (needed for Lemma 6, which the proof invokes), in a joint form that the proof of Lemma 6 uses and that implies the printed partial-map form; the standing Assumptions 1 and 2 of §2; and, inside Condition 4, differentiability of on , the premise of Definition 1. The Bellman operators carry the factor omitted in the printed (3)–(4). The stage-wise balance equation is stated for ; the printed range fails at the absorbing state.
A formalization in which the goal assumes the stage-wise characterization (31), the balance equation, or on any stage is not Theorem 3; neither is one where "contains an optimal policy" means optimal only within . Stationarity includes differentiability, so a junk zero gradient never makes a point stationary.
Needed infrastructure: occupancy measures as series of iterated kernels and their balance equation, the cost-to-go as a bounded measurable function, the performance difference identity, the policy gradient theorem, and the decomposition of integrals over the stage partition. The occupancy-measure and policy gradient results are reusable for every mission of this series; contributions of these general lemmas are welcome.