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.
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?
At a busy airport the runway is the bottleneck, and the order in which aircraft land or take off determines how much of its capacity is used. Wake turbulence forces a minimum time between consecutive operations that depends on the weight classes of the leading and trailing aircraft, so reordering a first-come-first-served (FCFS) queue can increase throughput or reduce delay. Controllers cannot reorder freely: constrained position shifting (CPS), introduced by Dear (1976, MIT Flight Transportation Laboratory Report R76-9), allows each aircraft to move at most positions from its FCFS position, which keeps the sequence fair and predictable.
Balakrishnan and Chandran (Oper. Res. 58(6), 2010) cast CPS scheduling as dynamic programming on a layered network whose paths are the admissible sequences. For makespan and total delay the separations are assumed to satisfy the triangle inequality, which holds for arrivals only or departures only. When arrivals and departures share a runway it fails: in the separation table of the paper, a heavy arrival followed by a departure and then a small arrival needs only seconds through the departure, while the direct requirement is seconds. Section 6.2 of the paper handles this case for arbitrary per-aircraft cost functions, by expanding the network state. This mission formalizes that construction and its correctness.
Time is discrete: all data are integer multiples of one period. There are aircraft labelled in FCFS order, a maximum shift , a minimum separation between a leading aircraft and a trailing aircraft , a time window for each aircraft, a finite set of precedence pairs ( lands before ), and a cost of landing aircraft at period .
A -CPS sequence is a bijection from positions to aircraft with . A feasible schedule is a -CPS sequence with integer landing times such that precedence pairs are respected, , and
Its cost is .
The CPS network has stages . A node of stage is a list of distinct aircraft that may occupy positions ; its last aircraft is the final aircraft . An arc joins consecutive stages when the lists overlap. Removing the nodes that violate a precedence pair gives the network . For a node , is the set of integer times in the window of .
The modified network of §6.2 has nodes : a node of , a time , and a lower bound on the separation between and its predecessor, with at stage and otherwise , where, for the penultimate and final aircraft of ,
An arc requires an arc of , , , and at least the separation between the penultimate aircraft of and . Arcs entering cost .
Under , positive costs, and the polygon inequalities of three or more hops (below):
each minimum existing exactly when the other does; 3. every minimum-cost path represents a feasible, optimal schedule.
The result turns a scheduling problem with arbitrary separable costs, time windows, precedence and non-metric separations into a shortest-path problem whose size is polynomial in for fixed and in the number of periods. It covers mixed arrival–departure operations, where the triangle inequality genuinely fails, and it is the basis of the paper's §7.1 algorithm for coupled arrivals and departures.
The paper proves Lemmas 5 and 6 in a few paragraphs and omits the proof of Lemma 4. No machine-checked version of the CPS network or of these lemmas exists. A formal development pins down the boundary cases the prose passes over (the first two stages, the last stage where has no successors), and it makes explicit an assumption the prose leaves unstated: Lemma 5 needs the polygon inequalities, not only the two-step check in its proof.
The obvious argument checks separations only between consecutive aircraft, which is what the network of §6.1.2 does. Without the triangle inequality this misses aircraft two positions apart. The state repairs that but is capped at , so one must show that the cap loses nothing: a capped value still certifies the separation to the next aircraft. That uses the definition of over the successors of a node in , so the proof depends on how the network is pruned. Separations three or more positions apart are not tracked at all and rely on the polygon inequalities. Relating network paths to sequences (Theorem 1) requires reasoning about overlapping windows of the sequence and about the precedence pruning rule.
Aircraft and positions are -based (Fin n), stages -based, and (NeZero n). Times, windows and separations are natural numbers (periods); , , and time differences are integers, since involves differences of separations that can be negative. Separation is required for all pairs of aircraft, not only consecutive ones. Minima are stated with IsLeast on sets of costs, never with a real infimum.
The following readings of the paper are committed:
A trivializing formalization is ruled out: the networks are concrete definitions computed from the instance, not arbitrary graphs pinned by hypotheses, and the goal compares two independently defined minima, so it cannot hold by an empty feasible set or an unconstrained optimum.
A complete development needs basic list combinatorics (windows of a sequence, overlap of consecutive windows), the correspondence between bijections and paths, and finite minimization. The CPS network layer is shared with the other missions of this series and is reusable for any CPS scheduling result. Contributions on Theorem 1 alone are welcome, as it is independent of the time-expanded networks.
In a linearly parameterized bandit, a decision maker repeatedly chooses an arm from a set and observes a noisy reward whose mean is the inner product with an unknown parameter vector . The model covers pricing, assortment and recommendation problems in which arms are described by feature vectors and the number of arms is large or infinite, so that learning arm by arm is hopeless and information must be shared through the common parameter.
Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, published in Mathematics of Operations Research, 2010) give matching lower and upper bounds of order for this problem when the arm set is the unit sphere. This mission is the lower bound, Theorem 2.1. It says that the dimension enters the regret linearly and that no policy can do better than , which makes the phased exploration policy of the paper's Section 3 optimal up to a constant.
Timeline. For , Mersereau, Rusmevichientong and Tsitsiklis (2009) showed regret and Bayes risk . Dani, Hayes and Kakade (2008) proved an minimax lower bound for a compact arm set built from products of circles. Rusmevichientong and Tsitsiklis (2010) proved the lower bound for the sphere itself, both for the regret and for the Bayes risk under a Gaussian prior, with the explicit constant .
Fix a dimension . The arms are the unit sphere , with the Euclidean norm . The unknown parameter is drawn from the prior : each coordinate is an independent normal with mean and variance , so . Playing arm in period yields the reward
where the noise variables are independent standard normals, independent of .
A history lists the arms played and rewards observed up to period . A policy chooses the arm of period from the history. Since , the regret of given and the Bayes risk of over periods are
The milestones use the least mean squares estimator and orthonormal vectors that are orthogonal to and are functions of .
For every policy and every ,
The constant is absolute; the parameter may depend on .
The result. Theorem 2.1 shows that the regret and Bayes risk of linearly parameterized bandits grow at least linearly in the dimension, even when the arm set is as regular as a sphere and the noise is Gaussian. Together with the paper's Theorem 3.1 it pins the optimal order at on the sphere, and it shows that the Bayes risk achievable in dimension one does not survive in dimension two or more. Since the sphere is one compact arm set, the theorem also shows that the paper's upper bounds of order for general compact arm sets (Section 4) cannot be improved beyond logarithmic factors in that generality (Table 1, p. 8).
Formalizing it. The theorem is proved in the paper; to our knowledge it has not been machine-checked. The platform has a minimax lower bound for the unit ball with a fixed-norm parameter (Lattimore and Szepesvári, Theorem 24.2), which is a different statement: a frequentist bound over a finite family of parameters, not a Bayes risk under a continuous Gaussian prior. Formalizing Theorem 2.1 requires Gaussian posterior computations with an adaptively chosen design, a piece of Bayesian linear regression that is reusable well beyond bandits.
The obvious argument fixes the parameter's norm and treats the problem as a Gaussian estimation problem in each direction orthogonal to the current estimate. That fails because is random under the prior: the risk per direction trades off exploration, weighted by , against estimation error, weighted by , and neither weight is bounded. The proof has to localise to an interval with positive probability uniformly in , which is the content of Lemma 2.4 and the reason the lemma needs .
The second obstacle is that the design is adaptive: the arms depend on past rewards, so the posterior of given must be identified as Gaussian with covariance even though the regressors are random and history-dependent. Lemma 2.3 rests on this identification and on a matrix inequality for diagonal entries of an inverse.
The source is arXiv:0812.3465v2; its printed page numbers equal the PDF's. All declarations live in the namespace LinParamBandits.LowerBound.
EuclideanSpace ℝ (Fin r), so norms are Euclidean and inner is . Every theorem carries , the paper's standing assumption.stdGaussian); the noise is an i.i.d. standard normal sequence (Measure.infinitePi), independent of .arm ψ z η t is the paper's .A complete development needs: measurability of the trajectory map, the Gaussian posterior for a sequentially chosen design, the inequality for positive definite , a chi-square lower-tail bound, and Gaussian tail values. The posterior computation and the chi-square bound are reusable; contributions of either, or of a proof of any single milestone, are welcome.
Two-stage stochastic linear programming chooses a first-stage decision before a random parameter is revealed and pays an optimal second-stage (recourse) cost afterwards. The classical model fixes the distribution of the random parameter. In practice it is rarely known beyond a few moments, and a decision maker who is averse to risk does not evaluate the recourse cost by its plain expectation. Bertsimas, Doan, Natarajan and Teo (Math. Oper. Res. 35(3), 2010) take both points seriously: the distribution is only known to belong to the class of all distributions with given mean and second-moment matrix, the cost is passed through a convex piecewise-linear disutility, and the decision is evaluated against the worst distribution in the class.
Moment-based worst-case bounds go back to Scarf's newsvendor and to the Chebyshev-type bounds of the moment problem (Isii 1962; Bertsimas and Popescu 2005). Delage and Ye (Oper. Res. 58(3), 2010) showed that a broad class of such minimax problems is solvable in polynomial time by the ellipsoid method. For the case in which the uncertainty sits in the objective of the second-stage linear program, this paper gives a single semidefinite program (its Theorem 2.1, the subject of a companion mission) and, in §2.2, identifies the distributions that come arbitrarily close to the worst case. This mission is about the second result.
The first-stage region is . For the recourse set is and the second-stage cost of an objective vector is
The disutility is with . The moment class consists of the distributions of a random vector with and . The worst-case value at is
Its dual (6) is
with symmetric and . Its semidefinite reformulation (8) has the dual (9):
Its variables are scaled conditional moments: is the probability that the th piece of is active, and , are the first and second moments of on that event, multiplied by .
The standing assumptions are Assumption 3, for every , so that is finite, and Assumption 4, . Recourse sets are assumed nonempty.
For every there is a sequence with , and
where all three are finite optimal values: a supremum over a nonempty bounded-above set, an infimum over a nonempty bounded-below set, and a supremum over a nonempty bounded-above set.
Theorem 2.2 says that the semidefinite bound is tight and that the worst case is approached by explicit mixtures. With probability the cost vector sits at the conditional mean , and with a small probability it is perturbed by a large Gaussian. The construction tells which scenarios a minimax solution guards against. The paper's numerical section uses it to stress-test solutions computed under other distributional assumptions. For the risk-neutral case () the bound collapses to Jensen's bound . For it is a combination of Jensen bounds, one per piece of the disutility.
Theorem 2.2 is proved in the paper; no part of it, nor the strong duality of the moment problem that it relies on, is formalized on the platform or, to our knowledge, elsewhere. The mission asks for machine-checked proofs of the identity and of the steps of the extremal construction. Several of these are reusable beyond this paper: weak and strong duality of moment problems, the existence of optimal solutions of moment-type semidefinite programs, and Jensen's inequality for the value function of a linear program.
Most of the argument is linear programming and bookkeeping. The step is a strong-duality theorem for an infinite-dimensional linear program over measures. The paper cites it from Isii's theory of the moment problem, and none of that theory exists in Mathlib. The construction of near-extremal distributions also needs care. A single distribution in generally cannot attain , so the bound is reached only along a family whose second moments are matched by rare, large perturbations. Lemma 2.1 needs measurable selections of an active piece of and of a dual optimal solution of the second-stage program as functions of . When the optimal solution of (9) has zero-weight blocks, the mixture is undefined until the solution is first rearranged.
Vectors are Fin d → ℝ, matrices Matrix (Fin r) (Fin d) ℝ, and distributions are probability measures on Fin d → ℝ with square-integrable coordinates. They are not densities as in the paper's (5). The moment class uses the published MomentDRO.Conf definitions, and is the uncentred second moment. The paper writes both for the dimension of and for dual vectors. Here the dimension is and dual vectors are named π. Indices are zero-based. Bordered matrices are Matrix.fromBlocks on Fin d ⊕ Fin 1 and is Matrix.PosSemidef. is a real infimum and the optimal values are real sSup/sInf of value sets. Every statement that uses an optimal value also asserts IsLUB/IsGLB, so junk values cannot make a statement true.
As printed, Assumption 2 (complete recourse) and Assumption 3 for all contradict each other whenever has a row. The formalization keeps Assumption 3 for all and replaces complete recourse by nonemptiness of , which is what §2's proofs use. Assumption 1 is not used and is omitted. The hypotheses are jointly satisfiable, for example by , , , and .
The sequence clause of Theorem 2.2 alone holds for every finite supremum, so it does not capture the theorem. The goal therefore also asserts the equalities , with all three values genuine, and these carry the content. A formalization that drops them, or states them only through junk values, is ruled out.
A complete development needs the duality theory of the moment problem, Jensen's inequality for concave functions on , compactness arguments for semidefinite feasible sets, and multivariate Gaussian mixtures (ProbabilityTheory.multivariateGaussian in Mathlib). Proofs of individual milestones are welcome. So is a general moment-problem duality theorem from which strong_duality follows.
Zara ships inventory from a central warehouse to each of its stores every week, and for a short-lived fashion item the warehouse holds a limited amount of each size. Deciding how many units of each size to ship to each store is therefore a constrained allocation problem whose objective is the expected sales a store will realize from a given inventory. Caro and Gallien (working paper, 2007; published in Operations Research, 2010) built such a model, embedded it in a weekly shipment optimization, and tested it in a field experiment in Zara's store network. The store-level sales model has one unusual feature, taken from Zara's practice: as soon as one of the major sizes of an item runs out, the whole item is removed from display, so stock-outs of different sizes interact.
The expected sales under that policy have no closed form usable inside a mixed integer program. The paper replaces them by an explicit piecewise-linear function and asserts that this replacement is an upper bound. This mission formalizes that claim, the chain of identities and inequalities that lead to it, and the paper's statement that its shipment program represents the approximation exactly.
A reference is offered in a finite set of sizes , with major sizes and minor sizes . Sale opportunities for size follow a Poisson process with rate , independent across sizes, where is the time since the last replenishment and is the time between replenishments.
Given an inventory vector , the virtual stockout time of size is , and for a set of sizes . Writing , the number of sales in one period is
since every size stops selling when the first major size runs out, and a minor size also stops when it runs out itself. The expected sales function is .
For the approximation, let be the lower incomplete Gamma function, and define the tangent coefficients
with the tangent at equal to the constant . For each size choose a nonempty finite set of tangent indices. The approximate expected sales function is
with . In Lean the objects are expectedSales, hA (), a, b, tangent and gTilde in the namespace FastFashion.Approx.
For every independent Poisson family with positive rates, every , every nonempty , every choice of nonempty finite tangent sets, and every ,
The statement fixes no tangent set, so it covers the paper's numerical choice (7) and every refinement of it.
In the shipment program (MIP) (13)–(19) of §3.2, with positive prices, every optimal solution has at every store .
The upper bound is what makes the paper's optimization coherent: the MIP maximizes , and the bound guarantees that this objective never underestimates the expected revenue of a shipment plan, with an error controlled by the number of tangents. Identity (6) exhibits as a concave function of with explicit Erlang-type slopes; (2) is a standard optional-sampling identity for compensated Poisson processes stopped at a bounded stopping time; and the MIP statement is the step that turns a minimum of affine functions into linear constraints.
The paper proves none of these in detail: (2), (4) and (5) are justified by a reference to the optional sampling theorem, (6) by a sentence on discrete concavity, and the upper bound and the MIP claim by one sentence each. None of the statements has a machine-checked proof. A formalization produces a checked chain from the Poisson model to the deterministic program, fixes the indexing error in the printed coefficients of (6), and isolates the exact hypotheses (nonempty major sizes, nonempty tangent sets, positive prices) under which the claims hold.
The deterministic parts — (3) given pathwise monotonicity, the envelope inequality given concavity, and the MIP argument — are short. The probabilistic identities are not. Equation (2) needs the optional sampling theorem for the compensated process in continuous time, applied at (the paper cites Karatzas and Shreve 1991), which requires showing that is a stopping time for the joint filtration of the family and that is still a martingale with respect to that larger filtration; this is where independence across sizes enters. Equation (4) needs the distribution of , the -th arrival time, which is Erlang; the statement in the model is about first hitting times of a counting process, not about sums of exponential inter-arrival times, so the link between the two descriptions has to be built. Equation (5) needs the identity between Poisson tails and the incomplete Gamma function.
A tempting shortcut is to define directly by formula (2), or by formula (4); both make the corresponding milestones definitional and the goal a statement about formulas rather than about sales. The formalization defines from and from the stopping times.
Finset and the minor sizes its complement. The demand is a structure IsPoissonFamily λ N P: each is a counting process with , non-decreasing right-continuous paths with unit jumps, Poisson increments of mean , independent increments, and the processes are independent across sizes. is a probability measure.WithTop ℝ), so the infimum of an empty set is , never ; is a real number in .The paper's further remark that inherits the qualitative properties of Proposition 1, and the multicolor extension of Appendix §5.2, are not included. Contributions of general infrastructure are welcome: optional sampling for continuous-time counting processes, Erlang hitting-time laws for Poisson processes, and the Poisson-tail/incomplete-Gamma identity are all reusable well beyond this mission.
Facilities fail: plants close, warehouses flood, suppliers strike. Reliable facility location models choose facility sites knowing that each opened site may be unavailable, and they assign every customer a primary facility and an ordered list of backups. Snyder and Daskin (Transportation Science, 2005) introduced the level-assignment formulation with a common failure probability. Cui, Ouyang and Shen (Operations Research 58(4), 2010; working paper UCTC-FR-2010-02, February 2010) let every site have its own failure probability , with failures independent. With site-dependent probabilities, even for fixed open sites, the best backup list for one customer is no longer simply the nearest sites in order of distance (their Example 1, p. 11).
The paper solves the model by Lagrangian relaxation. Relaxing the constraints that link assignments to open sites splits the problem into one relaxed subproblem (RSP) per customer , solved at every subgradient iteration. The authors show that (RSP) is the minimization of a set function over sets of at most sites, and their Proposition 3 asserts that is supermodular, which makes the branch-and-bound algorithm of Goldengorin et al. for supermodular minimization applicable. This mission formalizes Proposition 3 and the steps of its proof (Appendix A.3).
Fix a customer with demand rate and unserved-demand penalty . There are regular sites with unit costs , failure probabilities and Lagrange multipliers . An emergency facility with index never fails () and costs per unit: being served by it means not being served. The customer is assigned at levels with . A level- facility serves the customer exactly when the facilities at levels have all failed.
The variables are (site is the level- facility), (the probability that serves at level , given the earlier levels) and , which the linearization constraints force to equal . The constraints of (RSP) say that every level is filled by one regular site or comes after the emergency facility, that each regular site is used at most once, that the emergency facility appears exactly once, and that
For a set , is the minimum of
over the feasible points that use no regular site outside . The customer's subproblem is .
For every customer , every and all regular sites outside with ,
The paper states " is supermodular" without restriction. That statement is false: for sets larger than the inequality can fail (an instance with , is recorded in the goal's statement). The cardinality bound covers all the sets the subproblem ranges over, and the paper's proof uses it implicitly.
Supermodularity of is what the paper's exact algorithm for (RSP) rests on: the branch-and-bound method of Goldengorin et al. prunes by comparing marginal costs, and its correctness requires them to be monotone. Each Lagrangian iteration solves such subproblems, so this property sits inside the paper's whole solution method. The closed form (milestone 1) is also a self-contained statement about the optimal backup order with site-dependent failure probabilities: once the set of sites is fixed, nearest-first is optimal, and sites beyond the penalty distance are never used.
Formally, nothing in this mission is machine-checked yet. The paper's argument has gaps that a formalization has to repair: the missing cardinality hypothesis; a "strict" sign claim (milestone 3) that is only weak when some or ; counts printed as infima; and an intermediate inequality in Case 2 that does not hold as printed, although the case's conclusion does. A checked proof settles which version of Proposition 3 is true.
The algebra of the cases is routine once the closed form is available. The hard step is the closed form itself: is defined as the minimum of a mixed-integer program, and the paper justifies the closed form only by "a similar argument as in the proof of Proposition 2", an exchange argument. One has to show that every feasible point is a nearest-first chain truncated at the emergency facility, that and are then determined by , that reordering a chain by distance never increases the cost, and that adding a site within the penalty distance never hurts. With at most regular levels, the exchange must respect the level budget. This is exactly where the cardinality hypothesis enters.
A tempting shortcut is to define by its closed form. That makes milestone 1 true by definition and detaches the goal from the optimization problem; the definition here is the program (5).
Lean conventions: one customer at a time, with the index dropped in the definition. Regular sites are Fin J; all sites are Fin (J+1), with Fin.last J the emergency facility, whose cost and probability are built into the extended data. Levels are Fin (R+1). Variables are real-valued, with as a constraint. is the infimum of the set of feasible objective values. This set is nonempty and bounded below, and in fact finite, so the infimum is the minimum. Data hypotheses: , , ; costs, penalties and multipliers carry no sign assumption. The list is any duplicate-free list of sorted by distance. Ties are allowed.
Printed typos corrected in the definitions: the level constraint (4b) counts the emergency facility in its first sum; (5b) includes the linearization constraints (4h); (5c) covers regular site ; (5a) has for the undefined .
Excluding the configurations with from the goal is deliberate. Weakening the goal further, for example to or to sets on which is modular, would trivialize it.
Contributions welcome: a proof of the closed form (an exchange argument on level chains, reusable for the other propositions of the paper), then the marginal-cost algebra and the two cases.
A large control system is often built from many subsystems , each of which is input-to-state stable (ISS) with respect to the states of the others. Whether the interconnection is again ISS is decided by a small gain condition on the matrix of interconnection gains. For two subsystems this goes back to Jiang, Teel and Praly (1994) and to the Lyapunov version of Jiang, Mareels and Wang (1996). For subsystems, Dashkovskiy, Rüffer and Wirth formulated the condition as a property of a monotone operator on (2007). Rüffer's thesis (2007) and the paper on which this mission is based (arXiv:0901.1842, SIAM J. Control Optim. 2010) turned it into a Lyapunov construction.
The construction needs a geometric object: a path in the positive orthant, unbounded in every coordinate, along which the gain operator strictly decreases every component. For a linear gain matrix this is a Perron vector. For nonlinear gains, its existence is the first of the paper's two main results (Theorem 5.2). This mission formalizes that theorem and the lemmas of §8 that prove it. The companion mission formalizes the second main result, the Lyapunov function built from such a path.
Write . Vectors in are compared componentwise: means for all , and means for all . A function is of class if it is continuous, strictly increasing and , and of class if it is moreover unbounded.
A gain matrix is with and . A monotone aggregation function (MAF) is a continuous with for , whenever , and as . Typical examples are sums and maxima. Given MAFs , the gain operator is
The paper assumes from p. 8 on that , restricted to the coordinates of the nonzero entries of row , still has the strict monotonicity (Remark 2.6). The small gain condition (SGC) is : for every , at least one component of is strictly smaller than the corresponding component of . The set
collects the points that every component of strictly decreases.
An -path (Definition 5.1) is a continuous with every component such that (i) each is locally Lipschitz on ; (ii) on every compact the derivatives of all , where they exist, lie in for constants depending on only; and (iii) for all .
Let be a gain matrix and a compatible vector of MAFs. Assume one of: (i) is linear with spectral radius less than one; (ii) is irreducible and ; (iii) and ; (iv) the entries of are bounded and . Then
In cases (i)–(iii) the entries are in , and in case (iv) they are in .
The milestones follow §8 in the order the proof uses them.
An -path turns a small gain condition into a Lyapunov function. If each is an ISS Lyapunov function of , then is one for the network (Theorem 5.3). So Theorem 5.2 is the step that makes the small gain condition a certificate of network stability, and the corollaries of §5–§7 (sums, maxima, neural networks) all pass through it.
The results are published and proved on paper. None is machine-checked: no proof assistant library contains MAFs, gain operators, the sets and , or -paths. The paper cites three ingredients without proof: Lemma 8.6, Proposition 8.9 and the scaling step of Theorem 8.11. It also gives Theorem 8.14 only as a sketch. Formalizing them closes those gaps in one place.
For bounded gains the problem is easy: far out, every point of a large ray lies in , and the only work is the descent to the origin. With entries, is unbounded and no ray need stay in . Following the image of a single point fails, because forward iterates go to , not to infinity. The paper instead uses backward orbits inside . That this set is nonempty and unbounded is a fixed-point argument of Knaster–Kuratowski–Mazurkiewicz type (Propositions 8.9 and 8.10), not a monotonicity argument. A second obstacle is strictness. A backward orbit is only -increasing, while Definition 5.1 needs strictly increasing components with derivative bounds. This is where the diagonal scalings of Lemmas 8.6–8.7 enter.
is ℝ≥0 and is Fin n → ℝ≥0, with subsystems indexed from . The strict order is a named predicate (SLt), never Lean's < on functions, which means " and ". The small gain condition is ∀ s ≠ 0, ¬ s ≤ T s. The inverses are carried as explicit two-sided inverses, and derivatives are ordinary real derivatives at points where they exist. Compatibility (Remark 2.6) and are hypotheses of every statement about . Irreducibility is the matrix-power form of p. 12, which Mathlib's Matrix.isIrreducible_iff_exists_pow_pos connects to Matrix.IsIrreducible. The spectral-radius hypothesis says that every complex eigenvalue has modulus . The 1-norm defines .
Hypotheses made explicit or corrected:
A path with , or with Lean's < on functions, is not an -path. Such a reading would make the goal follow from the origin alone, and it is ruled out.
Needed infrastructure: comparison-function calculus (inverses and compositions of functions), piecewise linear interpolation in with Lipschitz inverse bounds, and a KKM-type argument on the simplex. The first two are reusable well beyond this mission. Contributions of any milestone, proofs of the cited ingredients (Lemma 8.6, Proposition 8.9, Proposition 8.10, the scaling step of Theorem 8.11) and a full proof of Theorem 8.14 are welcome.
A manufacturer that sells through a retailer can accept returns: it pays a return credit for every unit the retailer has not sold at the end of the season. Returns policies are common in publishing, software and computer hardware, and since Pasternack (Marketing Science, 1985) they have been studied as a way to make the retailer order more. Retailers also raise demand through sales effort: merchandising, shelf space, point-of-sale advertising. A recurring view in the marketing and operations literature is that returns weaken this incentive. Padmanabhan and Png (1995, p. 70) write that "by reducing the risk of losses due to excess inventory, a returns policy lessens some of the retailer's incentive to invest in such efforts", and Kandel (1996, p. 348) makes the same argument for consignment.
T. A. Taylor, Supply Chain Coordination Under Channel Rebates with Sales Effort Effects (Management Science 48(8), 2002), studies a newsvendor retailer who chooses an order quantity and a sales effort level before demand is observed. Its Proposition 4 shows that in this model the conventional view is reversed: a larger return credit makes the retailer exert strictly more effort. This mission formalizes that proposition and the solution of the retailer's problem it rests on.
Prices satisfy and (Assumption A1): is the retail price, the wholesale price, the manufacturing cost and the salvage value, which may be negative. A demand factor has a density with for every (Assumption A4), distribution function and partial mean .
The retailer chooses an effort level , and demand is . Effort costs , where is strictly convex and strictly increasing with (Assumption A5; the paper declares every convexity and monotonicity statement strict). Write .
Under a returns-only contract with , the retailer orders , exerts effort , and earns the expected profit
This is the integrated channel's profit with in place of and in place of . An optimal pair is a maximizer of over , . The paper's is the effort of such a pair, and is the critical fractile .
If , is an optimal pair under the credit , is an optimal pair under , and , then
The paper writes this as . Its proof shows strict monotonicity, and that is the statement here.
For a fixed , the unique maximizer of over is , and
An optimal pair with satisfies
and conversely every solving this first-order condition gives the optimal pair .
The result. Proposition 4 separates two effects of a return credit. For a fixed order quantity, a larger credit lowers the marginal value of effort: it pays the retailer for unsold units, and effort only matters through sold units. This is the fixed-quantity comparison on which the conventional view rests; Cachon's survey states it for buy-backs as Eq. (19) (on Prove2Me as CachonCoord.EffortNewsvendor.sec_6_4_1_effort_coordination, clause 1). Once the order quantity is chosen together with the effort, the larger credit raises the order, and the effort follows. For the multiplicative demand model the net effect is unambiguous for every demand density and every convex effort cost. A manufacturer that wants more retailer effort can therefore use the return credit as a lever, and a model that ignores the quantity response gets the sign wrong.
Formalizing it. The result is proved in the paper, in a four-line appendix argument that relies on the §4.2 solution of the retailer's problem; neither is machine-checked anywhere. The mission produces a checked newsvendor-with-effort solution (the scaling and the profit ), which the other missions of this series and any multiplicative-effort supply-chain model can reuse, and a checked statement of the comparative statics in the return credit.
The obvious argument differentiates the retailer's first-order condition in with the order held fixed, and it gives the wrong sign; the order quantity must be re-optimized. The correct comparison runs through the reduced problem in the effort alone, and it needs the §4.2 solution in full: the scaling of the optimal order with the effort, which turns and into newsvendor expectations of at ; the value of the optimal order as a function of ; and the first-order characterization of the optimal effort. The comparison across credits then involves two objects: the function , and the retailer's reduced profits under the two credits at a common effort level. The statement compares maximizers of two different optimization problems, not roots of an equation, so a formal proof must connect optimality of the pair to the first-order condition, which uses the strict convexity of and the positivity of the density.
Everything lives in the namespace ChannelRebate.ReturnsEffort. The definitions file holds:
Demand: a measurable density , zero on , positive on , integrating to , with finite mean;EffortCost: A5 with strict convexity and strict monotonicity on and ;returnsProfit;The expectations are the published CachonCoord.Newsvendor.expSales and expLeftover applied to the law of (the image of the law of under ).
The formalization makes the following commitments, each recorded on its item:
The goal is about optimal pairs of the joint problem. Defining as the root of the first-order condition, or fixing the order quantity and varying , would give a different and, in the second case, false statement; neither is the target.
Contributions are welcome:
The two facts the paper's proof uses — that is strictly increasing on , and that the retailer's reduced profit at a fixed effort increases with the credit — may be posted as supporting theorems.
Manufacturers of computer hardware, software and automobiles routinely pay their retailers channel rebates: a payment per unit the retailer sells to end customers. A target rebate pays only for units sold beyond a target level. These industries also commonly offer returns: a credit for each unsold unit. Both instruments are used to change the retailer's behaviour, and the retailer controls two things that matter to the manufacturer: how much stock she orders, and how much sales effort she exerts to raise demand. Effort cannot be observed or written into a contract, but sales can.
T. A. Taylor's paper (Management Science 48(8), 2002) asks whether a contract built on sales and returns can make an independent retailer choose the effort level and the order quantity that maximize the profit of the whole supply chain, while splitting that profit in any desired proportion. Its Proposition 2 shows that returns alone, linear rebates alone, or target rebates alone cannot do this. Its Theorem 2, the goal of this mission, shows that a target rebate combined with returns can, when demand is uniform and effort cost is quadratic.
A manufacturer with unit production cost sells to a retailer at wholesale price ; the retailer sells at the fixed retail price , and unsold units have salvage value . The standing assumption is and ( may be negative). Before demand is seen, the retailer chooses an order quantity and an effort level . Demand is , where is uniform on , with distribution function and . Effort costs , .
The integrated channel, which owns both firms, earns
Its optimum uses the critical fractile , defined by , the effort and the order . Its optimal profit is , where .
A target rebate and returns contract pays the retailer for every unit sold beyond the target , and credits her for every unsold unit. Her profit is
The manufacturer earns . The other quantities the statements use are:
Contract terms of Theorem 2. Put and
and are the fixed points on of and , with and evaluated at , . and are the retailer's profits at effort and at effort .
For every there is such that for every the following holds. Pairs with
exist. Every such pair gives , and . The pair is the retailer's unique optimum under , and
The result. Theorem 2 shows that two contractible instruments can align two decisions, one of them not contractible. The rebate pushes effort and quantity up when sales are high, and the return credit raises both when demand is low. Together they reproduce the integrated channel's optimum , and the free parameter allocates the profit between the firms in any proportion. Proposition 2 of the same paper rules out each instrument alone. This makes Theorem 2 the basis for the paper's recommendation that rebates and returns be used together. The uniform instance is the only one in which the paper proves this; for normal demand it gives only numerical evidence.
Formalizing it. The theorem is proved in the paper; it has not been formalized. The printed proof treats the wholesale price as fixed while it varies: and contain , so , and move with . A machine-checked proof therefore has to repair the argument, not only transcribe it. A numerical check (p = 10, c = 4, s = 1, a = 1; for example κ = 1.2, ε = 0.012 gives w* ≈ 4.889, T* ≈ 1.095) found the statement itself consistent.
The retailer's problem is not concave. For fixed effort, has a kink at , and the optimal order jumps from to at . After the order is optimized out, the profit in effort, , has an upward kink at and can be convex and then concave beyond it. Checking the first-order condition at is therefore not enough. Coordination is a statement about the global maximum of a kinked, non-concave function, and comparing the two local candidates is what the threshold and the profits , do. The contract is then pinned down by two equations in whose coefficients themselves depend on through and .
Everything is stated for , taken as Lebesgue measure on , and for , as in all of Lemmas 3–6 and Theorem 2. Lemma 2 and the §4.1–4.2 solutions, which the paper states for general demand, are specialised to this instance. The uniform law has bounded support, so the paper's Assumption A4 (positive density on ) is not imposed; the paper allows that relaxation on p. 995.
The expectations use the published expSales and expLeftover (Cachon's newsvendor definitions) of the image law of under . and are integrals of the uniform density, not hard-coded closed forms. Every inverse (, , ), the threshold , the function and its root , the fixed points , and the profits , are stated by their defining equations, never by a choice function. "Optimal" means a maximizer over , . Channel coordination means that the retailer's set of maximizers is exactly . The manufacturer's profit , which the paper does not display, is written from the contract's cash flows: units bought back at are salvaged at .
A trivializing formalization is ruled out: coordination is global optimality of , not a first-order condition at . may depend on but not on . and are tied to their fixed-point equations and are not free variables.
A complete development needs:
The uniform newsvendor identities and the kinked-maximization lemmas are reusable beyond this mission. Contributions to any milestone, and alternative proofs of the existence part of Theorem 2, are welcome.
An insurance company that collects premiums and pays random claims is ruined when its surplus becomes negative. The probability of ultimate ruin is the classical solvency criterion of risk theory, going back to Lundberg and Cramér. Real insurers have two levers on this probability: they can invest part of the surplus in a risky asset, and they can cede part of every claim to a reinsurer, at a price. The question of how to use both levers dynamically, as a function of the current surplus, so as to make the probability of ruin as small as possible, is a stochastic control problem for a jump-diffusion.
H. Schmidli, On minimizing the ruin probability by investment and reinsurance, Ann. Appl. Probab. 12 (2002), solves this problem for the Cramér–Lundberg model with proportional reinsurance and investment in a Black–Scholes asset. The main results are a verification theorem (Theorem 1, the subject of this mission) and an existence theorem for the associated integral equation (Theorem 2, the companion mission).
Timeline. Hipp and Plum (2000) treated investment in the Cramér–Lundberg model through the Hamilton–Jacobi–Bellman equation, assuming a bounded solution. Schmidli (2001) treated optimal proportional reinsurance alone. The 2002 paper combines investment and reinsurance, and proves the verification theorem without assuming the solution to be bounded.
Claims arrive at the jumps of a Poisson process with rate ; the claim sizes are i.i.d. with continuous distribution function , , independent of . The insurer receives premiums at rate . A risky asset , with and a standard Brownian motion independent of the claims, is available.
A strategy is a pair of processes , predictable for the smallest right-continuous filtration generated by the claims and : is the amount invested in the risky asset (locally bounded), and is the retention level, meaning the insurer pays of a claim occurring at time , at a reinsurance premium rate . The surplus starting from solves
where is the aggregate claims process. The ruin time is , the survival probability is , and the value function is .
The premium function is decreasing and continuous on , , , and there is with for and for (full reinsurance is too expensive).
The Hamilton–Jacobi–Bellman equation for is, with the convention for ,
For strictly concave the maximum over is attained at (equation (2)); denotes a measurable maximiser in .
Let be strictly increasing and nonnegative on , continuous there, twice continuously differentiable on , zero on , and a solution of (1) at every . Then is bounded, ,
and every surplus process from following , has survival probability .
The proof of Theorem 1 runs through: Lemma 3 (for small surplus the optimal retention is ); the identity along the feedback strategy; the inequality for every strategy; Lemma 1 (almost surely, either ruin occurs or ); the existence of a strategy with ; the comparison with equality for the feedback strategy; and the absence of ruin by creeping, .
The second sentence of Theorem 1 (that satisfies the hypotheses whenever is a decreasing solution of the integral equation (5)) and its last sentence (at most one such solution of (1) with ) are separate items.
Theorem 1 reduces a control problem over all predictable strategies to an analytic question: find one increasing smooth solution of (1). Combined with Theorem 2 (existence of a solution of (5)), it shows that the optimal survival probability is and that the optimal strategy is a Markov feedback rule in the current surplus. It also yields that this solution is bounded, which Hipp and Plum (2000) had to assume, and closes the gap they left open on ruin by creeping (Remark (iii), p. 897). Numerical procedures for the optimal strategy (§5 of the paper) rest on this identification.
The theorem is proved in the paper; nothing in it is formalized. The mission produces a machine-checked verification theorem for a controlled jump-diffusion with an Itô integral against Brownian motion, a Poisson claim stream and a predictable control, together with a formal model of the Cramér–Lundberg process with investment and reinsurance that later results in risk theory can reuse.
The standard verification argument applies Itô's formula to and uses (1) to show that is a supermartingale, and a martingale under the feedback strategy. Here is not at (), is discontinuous at after the extension by , and is not assumed bounded, so the stochastic integral is only a local martingale and the passage needs both Lemma 1 and a separate argument that the feedback process does not creep through . Lemma 1 itself is only sketched in the paper ("We will just describe the argument"). The optimality part needs a surplus process following the feedback rule; its existence is not proved in the paper.
The model is formalized on a measurable space with a probability measure: i.i.d. exponential interarrival times (realising the Poisson process), i.i.d. claim sizes with law , and a real Brownian motion (IsBrownianReal), the three families mutually independent. Independence of from the claims is not printed in the paper but is used by (1) and its proof; it is a disclosed standing assumption. The filtration is , not completed. The Itô integral is the published relation EthierKurtz.HasBrownianItoIntegral, and its paths are required to be continuous, so that the pathwise ruin event is well defined. The surplus equation holds for every and every sample point.
Conventions: the premium is real valued (so , which the paper allows to fail when ); the supremum in (1) is stated as a least upper bound equal to , so an unbounded family never counts as a solution; is on and (1) is required for ; is a supremum over all admissible triples (strategy and surplus process); the controls of the feedback rule at non-positive pre-jump surplus are left free, and optimality is stated for . Expectations of are lower Lebesgue integrals of nonnegative functions, so no default value of a non-integrable expectation satisfies an inequality. The optimality clause is stated for every process following the feedback rule; it would be vacuous if no such process existed, and its existence is not part of the target.
Infrastructure needed: Itô's formula for a semimartingale with Brownian and compound-Poisson parts, the compensator of the compound Poisson random measure, localisation, and optional stopping. The model definitions, the HJB predicate and the comparison lemmas are reusable for other ruin-minimisation and dividend problems. Contributions to any milestone, and to general stochastic-calculus lemmas they need, are welcome.
Manufacturers in computer hardware, software and automobiles routinely pay channel rebates to their retailers: a payment per unit the retailer sells to end consumers, as opposed to per unit the retailer buys. A target rebate pays only for units sold beyond a target level, a linear rebate pays for every unit sold. T. A. Taylor, Supply Chain Coordination Under Channel Rebates with Sales Effort Effects, Management Science 48(8) (2002), doi:10.1287/mnsc.48.8.992.168, asks whether such payments can make an independent retailer act in the interest of the whole supply chain.
The question belongs to the supply-chain contracting literature built on the newsvendor model. A wholesale price above cost makes the retailer under-order relative to the integrated channel (double marginalization, Spengler 1950). Returns contracts (Pasternack 1985) and revenue sharing (Pasternack 1999; Cachon and Lariviere 2000, as cited by Taylor) are known remedies. Cachon's survey, Supply Chain Coordination with Contracts (Handbooks in OR & MS 11, 2003), discusses sales-rebate contracts through a first-order condition. Taylor's Theorem 1 is the global statement for the target rebate, with an explicit contract and an arbitrary profit split, and without any lump-sum side payment.
This mission covers §3 of the paper, the model without sales effort. Missions II–IV of the series cover §4, where the retailer's effort also affects demand.
A manufacturer sells to a retailer who places one order of size before observing demand . Demand has a density with for and for every (Assumption A4), and a finite mean. Write
The retail price , the production cost and the salvage value are fixed with and ; may be negative. A contract specifies a wholesale price , a rebate and a target (Assumption A1: , , , ). No other transfer is allowed (Assumption A3).
and the manufacturer earns .
The contract coordinates the channel when is the retailer's unique optimal order. Finally .
Fix . For every sufficiently small there is exactly one triple with , , and
and this triple has , , , coordinates the channel, and gives the retailer and the manufacturer .
Theorem 1 shows that a single sales-based instrument, a target rebate, achieves what a wholesale price alone cannot: the retailer orders the channel-optimal quantity, and the channel profit is split in any proportion . The parameter can be set to the retailer's opportunity cost, so a manufacturer with all the bargaining power extracts the rest of the channel profit without a side payment. Proposition 1 explains why the target is needed: a linear rebate that coordinates the channel leaves the manufacturer with a loss. The quantity-only analysis is also the base case of §4, where the paper shows that a target rebate combined with returns coordinates effort and quantity as well.
The results are proved in the paper (Appendix, p. 1005). No machine-checked proof of any of them is known to exist. The mission produces a Lean statement of the model and of each result, and invites formal proofs of the newsvendor solution, the shape of the kinked profit, the threshold lemma and the coordination theorem.
The retailer's profit is not concave: its derivative jumps up at the target. The usual newsvendor argument, a stationary point of a concave function is a global maximum, therefore fails. A first-order condition at shows only that is a local candidate on . The retailer may still prefer the smaller candidate on , and coordination fails exactly when she does. Theorem 1(b) requires comparing the two branches globally, through the threshold of Lemma 1, and then showing that the contract's target lies strictly below .
The contract itself is defined implicitly. solves an equation involving the critical fractile , and solves (1). Existence and uniqueness of both, and the placement of relative to , are part of the claim.
All definitions are in ChannelRebate.Quantity.Setting. Demand is a structure Demand carrying the density with the properties listed under Setting; its law is Lebesgue measure with density . and are expSales and expLeftover of the published definition CachonCoord_Newsvendor_Contracts, applied to this law. is the local rebateUnits. and are interval integrals from .
Conventions:
Demand; no continuity of is assumed.A formalization that reads coordination as the first-order condition at , or that defines or by a choice function, would make Theorem 1 vacuous or weaker, and is ruled out by the statements above.
A complete development needs the newsvendor calculus for a density (derivatives of and in , strict monotonicity of on ), the intermediate value theorem for the two implicit equations, and the global comparison of the two concave branches. The newsvendor calculus is reusable for missions II–IV of this series and for other newsvendor contracts. Proofs of the milestones in any order are welcome.
Two-stage stochastic programs are solved with an approximation of the true distribution of the random data: an empirical measure, a scenario tree, or a discretization. Whether the computed decisions mean anything depends on how the optimal value and the solution set react when the underlying probability measure is replaced by a nearby one, and on which distance between measures "nearby" refers to. Rachev and Römisch (preprint, edoc.hu-berlin.de; published in Math. Oper. Res. 27 (2002) 792–818, doi:10.1287/moor.27.4.792.304) organize this question in two steps. First, a minimal information distance , built from the integrands of the problem itself, controls optimal values and solution sets (their Theorems 2.2 and 2.3). Second, for a given class of models, is bounded by a canonical probability metric that depends only on the analytical properties of the integrands.
For linear two-stage programs the integrands are locally Lipschitz in the random parameter and the canonical metric is a Fortet–Mourier metric. When the second stage has integer variables, the recourse function is discontinuous, and metrics of Fortet–Mourier type no longer control the problem. This mission formalizes the paper's answer for that case (§3.2): mixed-integer two-stage programs are Hölder stable with respect to a polyhedral discrepancy built from Lipschitz functions restricted to polyhedra. The structure of mixed-integer value functions that makes this possible goes back to Blair and Jeroslow (1977), Bank et al. (1982) and Schultz (1996), all cited in the paper.
Let , let be closed and a polyhedron, i.e. an intersection of finitely many closed half-spaces. The second stage has costs , and - and -matrices , . Its value function is
and is the set of right-hand sides for which the constraint set is nonempty. The right-hand side and the technology matrix depend affinely on . For a Borel probability measure on the program is
Three conditions make (9) well defined: (B1) and have rational entries; (B2) for all (relatively complete recourse); (B3) there is with and (dual feasibility).
and denote the optimal value and solution set of (9) under ; for an open bounded , and are the same objects with replaced by . is a complete local minimizing (CLM) set if it is nonempty and contained in . The minimal information distance is . The moment classes are , and the polyhedral metric is
Finally, is the growth function at , , and .
Under (B1)–(B3), with for some , , and an open bounded neighbourhood of , there are , and such that for all with
and is a CLM set. The constants and the number of faces are existential; only the exponent is fixed.
For bounded and every the same conclusions hold with the Lipschitz rate , where over polyhedra with at most faces.
Theorem 3.6 says that, for mixed-integer recourse, closeness of the distributions in is enough for closeness of optimal values and of localized solution sets, with an explicit Hölder exponent that degrades with the second-stage dimension and improves with the number of moments. Two consequences follow. Scenario reduction and discretization methods for mixed-integer models can be judged by a polyhedral discrepancy; and, through the entropy estimates of §4 of the paper, empirical approximations converge at rates governed by uniform laws for polyhedra. Corollary 3.7 shows that for bounded supports the rate becomes Lipschitz in the polyhedral discrepancy.
The results are proved in the paper, partly by reference: Lemma 3.5 is quoted from Bank et al., Schultz, and Blair–Jeroslow, and the partition argument behind (12) refers to Schultz (1996). None of it has a machine-checked proof. Formalizing the mission produces the first formal treatment of mixed-integer value functions with rational data, a formal version of the minimal-information-distance stability theorems in the objective-only case, and the polyhedral metric itself.
The obvious route to a stability estimate, a Lipschitz bound on followed by a Fortet–Mourier or Wasserstein bound, fails at the first step: jumps across the boundaries of the pieces , so is only piecewise Lipschitz, with pieces that move with . Any metric that controls must therefore see the indicator functions of these pieces, which is why polyhedra enter. The second obstacle is that there are countably many unbounded pieces: a single polyhedral bound covers only a bounded region of , and the tail outside it must be paid for with moments, which is the origin of the exponent. Lemma 3.5 itself, in particular the uniform Lipschitz constant and the local finiteness of the partition, rests on rationality of and ; without (B1) the value function need not be lower semicontinuous.
, , are Euclidean spaces (the paper never fixes its norm, and every constant in the statements is existential). Measures are Borel probability measures on with . The integral of the extended-real integrand is the published DupacovaWets.Consistency.expect ( when ). , optimal values and are extended-real infima, on empty sets; the paper's "min" is read as an infimum. Distances and take values in , and every estimate between optimal values states explicitly that both are finite, so that no convention for can make a bound vacuous. is a linear map and its operator norm. Integer vectors are tuples of natural numbers; , are real matrices with rational entries.
Disclosed reading: a "polyhedron with at most faces" is an intersection of closed half-spaces. Because is existential in Theorem 3.6 and Corollary 3.7, the theorems are equivalent under this reading and under a facet count. The clause "piecewise polyhedral" of Lemma 3.5 is not defined in the paper and is not formalized. The page states ""; the argument proves and uses , and that direction is the one formalized. Theorems 2.2 and 2.3 are stated in their objective-only () form for a general normal integrand.
The integrals in are Bochner integrals over , which are meaningful because measures in with integrate . A formalization that took the supremum over all of instead of , quantified over all of , or let a non-integrable function contribute would not state the paper's theorem, and these readings are excluded.
Needed infrastructure: the structure theory of mixed-integer value functions with rational data (the partition of Lemma 3.5 and the attainment of the minimum in (10)), lower semicontinuity of integral functionals of normal integrands via Fatou's lemma, Berge's upper semicontinuity of parametric argmin maps, and approximation of polyhedral pieces by polyhedra. The value-function results and the general stability theorems are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 3.5, are welcome.
Scheduling jobs on unrelated parallel machines to minimize the total weighted completion time is a basic model of machine scheduling: each job may take a different time on each machine, and a job becomes available on a machine only at a machine-dependent release date. In the three-field notation the problem is . Already the sequencing problem on a single machine with release dates is strongly NP-hard, so the question is how well it can be approximated in polynomial time.
Timeline (as surveyed in §1 of the paper):
This mission formalizes that last result.
There are jobs and machines. Job has a weight ; on machine it has a processing time and a release date . A nonpreemptive schedule runs every job without interruption on one machine, starting no earlier than its release date there, and each machine processes at most one job at a time. With completion times , the objective is .
Smith's order on machine : if , or the ratios are equal and .
Time slots. Sort the release dates on machine as and set . The -th time slot holds the jobs started on machine within . An assignment of jobs to slots is feasible if job goes to a slot with . For assignment variables , the slot starts are
and for a 0/1 assignment the completion time of is (17).
(CQP). Minimize with
subject to (14), if (18), (20), and (21). In matrix form the objective is , which is convex.
Randomized rounding. Each job is put into exactly one slot , with probability , the choices being pairwise independent across jobs. The resulting slot assignment is turned into a schedule by (15)–(17).
For every instance with , , :
The bound is stated for every feasible , so it needs no optimum of (CQP), and with (3) it gives the positive half of Corollary 3.6.
The result gives a -approximation for from a program of polynomial size, with a short analysis that holds job by job. The relaxation (CQP) is also the basis of §4, where the same rounding compares nonpreemptive with preemptive schedules, and its relaxation property bounds the optimum of (CQP) against the optimal schedule within a factor .
The result is proved in the paper; none of it is formalized. A formal development adds a checked model of release-date schedules and time slots on unrelated machines, the exchange argument behind Smith's rule in the presence of release dates, and a measure-free treatment of pairwise independent rounding. These pieces are reusable for other slot-based relaxations.
The analysis of Lemma 3.5 is short; the work lies in the reduction to slot assignments. Lemma 3.1 is an exchange argument, but swapping two jobs can push a job into a different time slot, so the naive bubble sort within a slot does not obviously terminate in a slot-sequenced schedule. Lemma 3.2 needs an induction across slots that accounts for empty slots and ties . Lemma 3.3 is a shifting argument on fractional solutions whose objective change is a quadratic computation, and the step size printed on p. 18 must be divided by to land exactly on . The relaxation conjunct of the goal chains Lemmas 3.1, 3.2, 3.3 and the p. 17 identity.
Jobs are Fin n, machines Fin m, and slots Fin m × Fin n, all 0-based. is cross-multiplied, which equals the page's ratio order because . is the sorted tuple of release dates; is never represented by a real number. Constraint (21) is imposed only for slots before the last, and a job's slot is the largest with . Schedules are a machine and a real start time per job; two jobs on one machine must satisfy or . Randomized rounding is a probability weight on slot assignments with marginals and product joint probabilities for distinct jobs; full independence is not required, and the product weight is one instance. The standing assumptions , , of p. 2 are hypotheses of every theorem; Lemmas 3.1 and 3.3, which assert existence, also assume .
A statement of the bound alone, , would say nothing about schedules: conjuncts 1 and 3 of the goal are what tie it to the scheduling problem, and neither may be dropped.
Not formalized: polynomial-time solvability of (CQP), the running time of the algorithm, the tightness half of Corollary 3.6, and the first sentence of Lemma 3.1 as a statement about every optimal schedule (false when some ).
Contributions welcome: proofs of any milestone; a general library of time-slot schedules; and the convexity of (22) (positive semidefiniteness of ), which is not a milestone here.
Time-indexed formulations are a standard way to model scheduling problems as integer programs: a binary variable records whether job starts at time . They were introduced by Pritsker, Watters and Wolfe (1969) and give strong linear relaxations, at the price of many variables. In project scheduling, jobs are linked by time lags: a lag of length requires , and since may be negative, lags express both minimal and maximal distances between start times, i.e. time windows. Many project scheduling objectives (weighted completion times, net present value, earliness–tardiness, and the Lagrangian subproblems of resource-constrained scheduling) reduce to minimizing a sum of start-time dependent costs subject to such lags.
Möhring, Schulz, Stork and Uetz showed that this problem, despite being an integer program, is solved by one minimum cut computation in a directed graph built from the time-indexed variables. This makes the Lagrangian relaxation of resource-constrained project scheduling computationally practical, which is the use the paper puts it to.
Timeline.
Jobs form the set ; job has an integral processing time . A set of time lags is given, with integral lengths . A schedule is an integral vector of start times; it is feasible if for all and it lies within the horizon : and . Starting job at time costs . The earliest and latest feasible start times and are the minimum and the maximum of over feasible schedules. Throughout, a feasible schedule is assumed to exist.
The integer program (1)–(5) has variables :
for all , , , and all variables with outside are zero.
The minimum cut digraph has a source , a sink , and nodes for . Its arcs are the assignment arcs for , of capacity ; the temporal arcs for and , ; and the auxiliary arcs and . Temporal and auxiliary arcs have infinite capacity. An --cut splits with , ; its capacity is the total capacity of the arcs from to . An -cut is an --cut containing exactly one assignment arc of every job. The mapping (7) sends a cut to with iff is in the cut.
A companion statement (p. 8) covers strictly positive weights: then every minimum --cut is an -cut, and (7) is a bijection between minimum --cuts and optimal solutions.
The result. Theorem 1 shows that the time-indexed integer program with arbitrary (also negative) time lags has an integral linear relaxation in disguise: it is a minimum cut problem, solvable in strongly polynomial time, with push-relabel (Corollary 1). This is what allows the paper to compute Lagrangian lower bounds for resource-constrained project scheduling with time windows by repeated minimum cut computations, and to use the resulting dual information for list scheduling heuristics (§§3–4). The construction is a direct reduction, sparser than the closure-based route of Chang and Edmonds.
Formalizing it. The result is proved on paper; no machine-checked proof is known. The mission produces a formal model of the time-indexed project scheduling IP with time lags and of its cut digraph, together with checked versions of the correspondence and of each lemma of its proof. The model of cuts with infinite capacities and tagged parallel arcs is reusable for other cut-based reductions (selection, closure, and image segmentation problems).
The bijection itself is bookkeeping. The substance is in two places. First, Lemma 1: a minimum cut need not be an -cut (a zero-weight assignment arc can be cut twice), and repairing it to the canonical prefix cut must not introduce a temporal arc into the cut. The repair argument shifts a hypothetical violating temporal arc back along the lag, and needs that the lags are consistent with the earliest and latest start times, and , facts about the feasible schedules rather than about the graph. Second, Lemma 3: temporal arcs exist only for in a restricted window, so a finite-capacity -cut satisfies the temporal constraint (3) only after a boundary case analysis at and . The naive reading "every temporal constraint is an infinite arc" is false at the boundary.
An instance is a Lean structure with fields ; jobs are Fin (n + 1), start times are integers, and is a function (integrality by type). The standing assumptions of §2 are hypotheses of every theorem: (p. 5) and the existence of a feasible schedule (p. 4). The horizon condition , is read from "", "" and "" (p. 5), which the paper never writes as a formula. The paper's artificial jobs and with zero processing time are not assumed: §2.2 never uses them, so the statements are stronger. and are defined as the minimum and maximum feasible start times, never taken as parameters. Capacities live in with on temporal and auxiliary arcs; arcs are a tagged type, so parallel arcs and self-lags remain distinct. A cut is its source side . Running-time claims (the clause of Lemma 1, Corollary 1, the Goldberg–Rao bound) are not formalized.
Trivializing formalizations are ruled out: the integer program is not replaced by schedules, infinite capacities are not big-M constants, the minimum is taken over all --cuts and not only over -cuts, and are computed from the instance rather than quantified over.
Needed infrastructure: finite sums in , minimum and maximum of finite sets of integers, and elementary reasoning on integer intervals. Proofs of any milestone, and of the auxiliary fact used in Lemma 3, are welcome.
Measurements of Ethernet and Internet traffic in the 1990s showed that the amount of data offered to a link is bursty on every time scale and that the lengths of transmissions (file sizes, connection durations) have heavy, regularly varying tails. Two families of approximations for the cumulative input were proposed: fractional Brownian motion, which has dependent Gaussian increments, and α-stable Lévy motion, which has independent, heavy-tailed increments. The two lead to very different predictions for buffer overflow and link dimensioning.
T. Mikosch, S. Resnick, H. Rootzén and A. Stegeman (Ann. Appl. Probab. 12 (2002) 23–68) showed that both answers are correct in different regimes, and that the regime is decided by how fast the connection rate grows relative to the time scale. This mission formalizes their result for the infinite source Poisson model under slow growth, where the limit is a totally skewed α-stable Lévy motion. Companion missions treat the ON/OFF model and the fast-growth regime with its fractional Brownian limit.
A transmission length has law on with tail . Condition (2.8) asks
with slowly varying ( for every ). The mean is finite and the variance infinite. The quantile function (2.9) is .
In the -th model, connections start at the points of a homogeneous Poisson process on with rate , labelled so that . Connection transmits at unit rate for a time ; the are iid with law and independent of the . The number of active connections and the cumulative input are
The rate is a positive non-decreasing function of . Slow Growth Condition 1 is
where is evaluated at .
The stable law is the law with characteristic function for . α-stable Lévy motion has independent stationary increments with . Write
Under (2.8) and Condition 1,
convergence of the finite-dimensional distributions to a totally skewed () α-stable Lévy motion.
On the scale. The paper prints the limit . Its own proof establishes (pp. 37–38), which makes the Lévy measure of the limit. The totally skewed stable law with that Lévy measure has (Samorodnitsky–Taqqu, Property 1.2.15; also the paper's own criterion on p. 47 with , and the the paper prints in Theorem 2). Since decreases from to on (), the printed limit has the wrong scale and the theorem as printed is false. The goal states the corrected scale ; milestones quote the page as printed.
(2.14), the covariance of ; Lemma 1 part 1 (Condition 1 ); Lemma 2, slow part (); (4.15), negligibility of the boundary pieces ; the tail limit of ; (4.17), ; (4.20)–(4.21), ; (4.19), corrected, the stable limit of ; the corrected one-dimensional limit of ; and of §4.5, which reduces the fidi convergence to the one-dimensional one.
The theorem shows that under slow connection growth the cumulative input is asymptotically a process with independent, infinite-variance increments. Long-range dependence present in each model (the covariance (2.14) decays like ) disappears on the time scale , and the heavy tail of the transmission lengths dominates. Together with the fast-growth result (fractional Brownian motion) it explains why both approximations are found in measured traffic, and it identifies the critical quantity .
The result is proved in the paper, modulo the scale. No part of it is machine-checked. The mission produces a formal statement of the infinite source Poisson model with its marked point process structure, a formal statement of stable laws and stable Lévy motion through their characteristic functions, and machine-checked versions of the paper's estimates. Correcting the printed scale is part of the output.
The pieces are controlled by first moments, regular variation and Lemma 2. The central step is the stable limit of : a sum of a Poisson number of iid, heavy-tailed summands whose law changes with . A classical central limit theorem does not apply because the variance is infinite, and the summands form a triangular array. The paper cites a point-process limit (Resnick's Exercise 4.4.2.8) for this step; a formal proof needs a convergence theorem for row-wise iid triangular arrays to stable laws, with the constant computed exactly.
Each has its own probability space carrying the -th model, and every statement quantifies over all such families. The Poisson points are given by their iid exponential spacings , indexed by . (2.8) is stated as " is slowly varying", with lengths non-negative. is , which equals the page's generalized inverse for . is a cardinality and the region sums are sums of non-negative terms; their junk values (an infinite set, a non-summable family) occur only on null events. is an interval integral. The growth hypothesis is: , non-decreasing, Condition 1. No other hypothesis is added.
The fidi limit is pinned by its characteristic function on for sorted times : the product of the characteristic functions of evaluated at . The existence of the limit law is part of the claim. One-dimensional limits are stated the same way on . Convergence in probability to is for every .
Trivializing formalizations are excluded:
A complete development needs regular variation (Karamata's theorem, Potter bounds, generalized inverses), the Poisson random measure of the marked points, and stable limits for triangular arrays. All three are reusable beyond this mission. Proofs of the milestones are welcome separately, as are general Mathlib-style lemmas on regular variation.
A Markov decision process (MDP) is evaluated by solving a linear fixed-point equation built from its transition probabilities. In practice those probabilities are rarely known exactly: they are estimated from data, elicited from experts, or obtained by aggregating the states of a larger model, and each estimate comes with an error band. Givan, Leach and Dean (Bounded-parameter Markov decision processes, Artificial Intelligence, 2000) replace each transition probability by a closed interval and ask what can still be said about the value of a policy. Their answer for a fixed policy is an interval value: at each state, the smallest and the largest expected discounted reward the policy can obtain over all exact MDPs consistent with the intervals.
The same model reappears under other names. Robust MDPs with rectangular uncertainty sets (Nilim and El Ghaoui, Operations Research, 2005; Iyengar, Mathematics of Operations Research, 2005) take the pessimistic end of the interval, and optimistic model-based reinforcement learning (for example UCRL-type algorithms) takes the optimistic end over a confidence set. Interval transition models are also used to bound the error of state aggregation. In all of these, the basic computational question is how to evaluate a fixed policy against a whole family of MDPs at once.
Fix a finite set of states and a finite nonempty set of actions. An exact MDP has transition probabilities , each row a probability distribution, a reward per state, and a discount rate . A policy is a map . Its value function is the expected discounted cumulative reward of the Markov chain with transition matrix :
On the space of value functions , with the sup norm , the value-iteration operator is , and is the same with the action in place of . An operator on is a contraction mapping if for all and some .
A bounded-parameter MDP (BMDP) gives intervals with , a reward and a discount rate . An exact MDP belongs to if it has the same and and every transition probability lies in its interval. The interval value of a policy (Definition 3) is
Interval policy evaluation acts on an interval value function by
with lower and upper bound maps .
For the optional part, interval value iteration adds a maximization over actions: and take, at each state, the largest of the candidate intervals for the lexicographic orders (upper end first) and (lower end first). For a value function , and are the actions maximizing and , and , .
For every BMDP, every policy , and every interval value function with ,
The limit is the interval value of Definition 3, an extremum over infinitely many MDPs; nothing about the starting point is assumed beyond its being an interval value function.
The result. The interval value is defined as a minimum and a maximum over a continuum of MDPs, and there is no a priori reason it should be computable by a dynamic program. The goal says it is: one operator, whose per-state step is a small linear program over a box intersected with a simplex, iterated from any start, converges to both ends of the interval simultaneously. The pessimistic end is the robust value of the policy under rectangular uncertainty, so the goal is also a policy-evaluation theorem for interval-rectangular robust MDPs; the optimistic end is the value used by optimism-based exploration. Theorem 11 is the bridge between the "game" definition (nature picks the MDP) and the fixed-point characterization; Theorem 13 is the corresponding first step for the optimal interval values of the companion mission.
Formalizing it. The results are proved in the paper (2000), with Theorem 11 relying on the existence of a single member MDP that is -minimizing at every state simultaneously (the paper's Theorem 7). No machine-checked version of the BMDP model or of these results is known. Nearby statements formalized elsewhere concern other models: robust MDPs with costs and general row sets, and optimistic Bellman equations over compact confidence sets. This mission produces the BMDP model and its interval operators, the contraction and fixed-point theorems, and the convergence theorem, all stated against the member-MDP definition of .
The contraction estimates (Theorems 10 and 13) follow the familiar pattern for Bellman operators, with the extra point that the minimum or maximum over the infinite family must be attained. The real difficulty is Theorem 11. The obvious argument compares with state by state; but is a minimum taken separately at each state, possibly by a different MDP at each state, and need not a priori be the value function of any single member MDP. Without a member MDP that is minimizing at all states at once, the inequality does not follow. Establishing that simultaneous minimizer is the central step.
All statements live in the namespace BoundedParamMDP.IntervalEval. The exact MDP, the BMDP, its member MDPs, , , and Definition 3's , are the shared definitions BoundedParamMDP.Optimal.MDP and BoundedParamMDP.Optimal.BMDP used by the companion mission, so its theorems apply to the same objects. Conventions:
Q → A.F p α q , rows nonnegative and summing to , a state reward R, and the discount rate as a field. Rewards are tight (the paper's footnote 3): members share the BMDP's R and γ.Member B; all quantities are bounded, so these are the genuine values (and attained, by the paper's Lemma 1).(V↓, V↑) of functions Q → ℝ. The operators are defined on all pairs; the goal assumes as the paper's interval notion, though the conclusion does not need it.Q → ℝ (the sup norm (4)); convergence of pairs is in the product topology. A contraction mapping is "there exists ", as on p. 6; the modulus is not fixed to .A trivializing formalization is excluded: the limit in the goal is Definition 3's infimum and supremum over member MDPs, not the fixed point of , so the goal is not Banach's theorem alone; and the member type is nonempty for every BMDP, so the infima and suprema are not the junk value .
The proof of Theorem 11 uses the paper's Lemma 1 (attainment in the order-maximizing family), Theorem 3 ( is the unique fixed point of ), Theorem 6 (comparison principle) and Theorem 7 (existence of -minimizing and -maximizing MDPs). These are milestones of the companion mission Bounded-parameter Markov Decision Processes 1 and are not restated here. The Banach fixed-point theorem is Mathlib's ContractingWith. Contributions welcome: proofs of the milestones, a reusable lemma on the attained minimum of a linear function over a box intersected with the simplex, and the order-maximizing construction itself.
Many problems in optimization and in the discretization of partial differential equations reduce to a linear complementarity problem with an obstacle: find with
for a matrix and vectors . When is symmetric positive definite this is the optimality system of the quadratic program subject to . Finite-difference and finite-element discretizations of obstacle problems and of control-constrained optimal control problems lead to systems of exactly this form, with in the thousands or millions.
The primal-dual active set strategy solves such systems by guessing, at every iteration, which constraints are active and solving one linear system for that guess. It was introduced as a special case of generalized Moreau–Yosida approximations by Ito and Kunisch, and was observed to converge in a few iterations, typically without a line search. M. Hintermüller, K. Ito and K. Kunisch, The primal-dual active set strategy as a semismooth Newton method, SIAM J. Optim. 13(3):865–888, 2002 (DOI 10.1137/S1052623401383558; authors' version HAL hal-01660511) explained that behaviour: the strategy is a semismooth Newton method for a nonsmooth reformulation of the problem, and therefore inherits local superlinear convergence. This mission formalizes that local theory, the first of a five-part series on the paper.
Fix , , and . Vectors are ordered componentwise. The complementarity conditions are equivalent to one nonsmooth equation, so the problem becomes
with the maximum taken componentwise. The paper writes for the matrix and calligraphic , for index sets; the two are unrelated.
Primal-dual active set algorithm. Given an iterate , the active set is and the inactive set is . The next iterate solves
A run is a sequence of iterates, from arbitrary initial data , in which every pair follows its predecessor in this way.
A P-matrix is a square matrix all of whose principal minors are positive. For a P-matrix every principal block is invertible, so every step is uniquely solvable, and (3.1) has exactly one solution .
Slant differentiability. Let be Banach spaces and . A map from to the bounded linear operators is a slanting function for in an open set if for every
The derivative is evaluated at the perturbed point , not at ; this is what lets a nonsmooth map such as qualify. A sequence converges superlinearly to if and for every , eventually .
For (3.1) put . For let be the diagonal matrix with entries where , where and where . The paper's is the block matrix (2.4) obtained by using with for the max-term of .
For a P-matrix , and the solution of (3.1), there is such that every run with satisfies
The radius depends on the data and the solution, not on the run. The goal speaks about the active set algorithm itself; its identification with a semismooth Newton method is a milestone.
Three companion statements accompany the goal: a run exists from every initial pair; a run that converges to reaches it after finitely many steps (§3, p. 7); and if and , the run equals from the first iterate on (Remark 3.4 (iii)).
The result. Theorem 3.1 explains why the primal-dual active set strategy converges fast in practice, and it does so through a notion, slant differentiability, that carries over to function spaces, where Clarke's generalized Jacobian is not available. The paper's later sections (missions II–V of this series) use the same framework for global convergence under M-matrix, diagonal-dominance and perturbation hypotheses, and for superlinear convergence in . Theorem 1.1 itself is an abstract local convergence result for nonsmooth Newton methods that applies far beyond complementarity problems.
Formalizing it. The results are proved on paper; none of them is machine-checked. Mathlib has the Fréchet derivative and Newton-type fixed-point arguments, but no slant differentiability, no semismooth Newton method and no theory of the primal-dual active set strategy. A completed mission gives a reusable Lean statement and proof of the Chen–Nashed–Qi theorem in Banach spaces, slant differentiability of the componentwise maximum, and a verified bridge between a combinatorial active set iteration and a Newton iteration.
The map is not differentiable at , so the classical Newton convergence theorem does not apply to . The obvious substitute is a condition with the derivative at the base point, ; the paper notes (p. 3) that with it Theorem 1.1 would need an additional uniformity assumption in when is infinite dimensional. Statements and proofs therefore have to work with the derivative at the perturbed point, which is the point at which the Newton iteration evaluates it. A second difficulty is bookkeeping: the identification of the Newton step with the active set step is a block computation over index sets that change with , and the bound on must hold uniformly over all active sets, using only that principal blocks of a P-matrix are invertible.
Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and the order is componentwise. Pairs live in (Fin n → ℝ) × (Fin n → ℝ) with the max of the two sup norms; in finite dimension every norm gives the same notion of superlinear convergence. Property (A) is stated as a little-o relation, so nothing is divided by ; boundedness of , required in the original Chen–Nashed–Qi definition, is deliberately not part of it, as in the paper. and are total maps; the paper's domain plays no role.
Standing assumptions: in every statement; is a P-matrix wherever the paper uses it (the goal, the inverse bound, the existence of runs, finite termination, Remark 3.4 (iii)), via the published definition RobinsonSR.Schur.IsPMatrix. The solution of (3.1) is a hypothesis; for a P-matrix it exists and is unique, which is a separate classical theorem not restated here. A step of the algorithm is a relation and a run is an infinite sequence of steps; the "Stop" option of the algorithm is not modelled. Nonsingularity in Theorem 1.1 means a two-sided bounded linear inverse, and the Newton iteration is written as the linear equation .
The radius in Theorem 1.1 and Theorem 3.1 is quantified before the sequence; a formalization in which may depend on the run, or in which superlinear convergence drops either the convergence or the rate condition, does not state the theorem. A companion item shows runs exist, so the goal is not vacuous.
Contributions welcome: proofs of Theorem 1.1 in Banach spaces (reusable for missions II–V), of Lemma 3.1, of the block identities, and of the uniform inverse bound over all active sets.
The ferromagnetic Ising model is the basic model of statistical mechanics for interacting binary variables. On a finite graph it is a probability distribution over spin configurations, and its normalizing constant, the partition function, encodes the thermodynamics: the free entropy per vertex determines the magnetization, the correlations, and the location of phase transitions. On lattices this quantity is understood only in special cases. On sparse random graphs, such as random regular graphs and Erdős–Rényi graphs with bounded average degree, physicists predicted it with the cavity method (Mézard and Parisi, The Bethe lattice spin glass revisited, 2001): locally these graphs look like trees, and on trees the model can be solved by a recursion. The same recursion underlies belief propagation, the message-passing algorithm used in coding theory and machine learning.
Timeline:
Let be a sequence of finite graphs. The Ising measure at inverse temperature and magnetic field is
each edge counted once, and the free entropy density is .
A degree distribution is a law on with ; its size-biased version is , and . The Galton–Watson tree has a root with children with probability , and every other vertex independently has children with probability ; is its first generations.
The ball is the subgraph induced by the vertices within distance of , rooted at . The sequence converges locally to if, for every and every rooted tree , the fraction of vertices with (root-preserving isomorphism) tends to . It is uniformly sparse if .
The cavity recursion acts on laws of a real random variable :
with and i.i.d. copies of independent of . For it has a unique fixed point supported on . The Bethe functional of a law of is
with independent of the .
Assume is uniformly sparse, converges locally to , and . Then for every :
and has a limit as , with . This is the paper's statement that the limit exists for every , equals (2.9) for , is even in , and is continuous at .
The result. Theorem 2.4 establishes the replica-symmetric (Bethe) formula for the ferromagnetic Ising model on the standard sparse random graph ensembles at all temperatures, including below the critical temperature where the Gibbs measure on the limiting tree is not unique. It identifies the free energy of random regular graphs, Erdős–Rényi graphs and configuration models with arbitrary degree distributions of finite variance, and the derivative identities that follow give the limiting magnetization and energy per edge. The tree estimates of Section 4 also yield the convergence of belief propagation (the companion mission of this series).
Formalizing it. The theorem is proved; nothing in this mission has been machine-checked before. A formal proof requires infrastructure that Lean's Mathlib does not have: Ising measures with boundary conditions, correlation inequalities, Galton–Watson trees as laws of offspring functions, local weak convergence of graph sequences, distributional fixed-point equations, and the Monge–Kantorovich distance on the real line. While stating the milestones, Corollary 6.3 turned out to be false as printed (the constant should be ; a counterexample is ); the mission states the corrected version, which is what the paper's proof gives.
The obvious route through uniqueness of the Gibbs measure on the tree fails below the critical temperature: different boundary conditions give different limits, so local quantities are not determined by the local graph structure alone. The paper replaces uniqueness by insensitivity to positive boundary conditions when (Lemma 4.3), which rests on Griffiths and GHS monotonicity and on averaging over the random tree; the deterministic statement is false. Passing from derivatives to the free entropy itself requires that the Bethe functional be stationary in the cavity law (Corollary 6.3), so that the -dependence of can be ignored. Finally, the case at low temperature is reached only as a limit: there is no fixed-point characterization at .
true); edges are unordered and counted once. Graphs live on Fin n.List ℕ → ℕ in Ulam–Harris form; random trees are laws of offspring functions under the product σ-algebra. Galton–Watson trees are infinite product measures. Fields on trees are nonrandom functions of the vertex.ProbabilityMeasure ℝ, and convergence in distribution is weak convergence. Expectations over are series with product laws.A complete development needs: Griffiths and GHS inequalities for finite Ising models (reusable for any ferromagnetic model); Ulam–Harris random trees with conditional independence; local weak convergence of graph sequences (reusable for random graph theory); distributional recursions with stochastic ordering; and the coupling characterization of the Wasserstein-1 distance on . Contributions of any milestone are welcome, as are proofs of the classical inequalities of Section 3 independent of this paper.
The learning with errors (LWE) problem underlies much of post-quantum public-key cryptography, and its hardness rests on Regev's reduction from worst-case lattice problems to LWE (Regev, J. ACM 2009). Every step of that reduction is calibrated by the smoothing parameter of Micciancio and Regev (SIAM J. Comput. 2007): the Gaussian width above which a discrete Gaussian on a lattice behaves like a continuous one. The approximation factors of the reduction are stated in terms of , and they are converted into factors for the standard lattice problems (GapSVP, SIVP) by comparing with the successive minima of and of its dual.
Upper bounds on (Lemmas 2.11 and 2.12 of the paper, from Micciancio–Regev) say the smoothing parameter is not too large. Claim 2.13 is the matching lower bound: the smoothing parameter cannot be much smaller than , and hence than . The second comparison goes through Banaszczyk's transference theorem (Banaszczyk, Math. Ann. 296 (1993)), , which relates the geometry of a lattice to that of its dual.
This mission formalizes Claim 2.13 from the published J. ACM article (Article 34, 2009), together with the steps of its proof and the transference theorem it cites. The paper's main theorem, Theorem 3.1, is a quantum reduction about efficient algorithms; it is outside this series of missions.
Work in , , with the Euclidean norm and inner product . A lattice is the set of integer combinations of linearly independent vectors. Its dual is
again a lattice, with .
The successive minima used here are , the length of a shortest nonzero vector of , and , the least such that contains linearly independent vectors of length at most .
For the Gaussian function is (Eq. (4)), and for a countable set , . In particular .
For the smoothing parameter is the smallest such that (Definition 2.10).
For any lattice and any ,
Both inequalities of the chain are part of the goal. The asymptotic "In particular" sentence of the claim (, large enough ) is not.
The result. Claim 2.13 shows that the smoothing parameter for a negligible exceeds every constant multiple of and of . Together with the upper bound of Lemma 2.12, it locates within a polynomial factor of . This is what lets the reduction's guarantees, phrased in , be read as approximation factors for SIVP and GapSVP. The transference theorem is used throughout the geometry of numbers and in lattice-based cryptography to pass between a lattice and its dual.
Formalizing it. The claim and its proof are classical and short, but neither is machine-checked. The mission produces formal definitions of the dual lattice, the successive minima , and the smoothing parameter on EuclideanSpace ℝ (Fin n), a proof that Definition 2.10 is well posed, and a statement of Banaszczyk's transference theorem. The upper bound of the transference theorem is a substantial result in its own right (the paper cites it without proof), and a formal proof of it would be reusable well beyond this mission.
The first inequality of the goal is elementary once the smoothing parameter is known to be attained, with exactly. That step is not a formality: it needs the continuity and strict monotonicity of an infinite lattice sum in the scale parameter, and the fact that a shortest nonzero dual vector exists, both of which rest on the discreteness of .
The second inequality is a single line in the paper, "by Lemma 2.3", but it uses the upper bound of Banaszczyk's theorem, applied to the dual lattice. The easy lower bound does not suffice, and a Minkowski-type argument gives a bound worse than linear in . Applying the lemma to also needs to be a lattice with dual .
EuclideanSpace ℝ (Fin n). A lattice is L : Submodule ℤ _ with [DiscreteTopology L] [IsZLattice ℝ L]. The dual is LinearMap.BilinForm.dualSubmodule (innerₗ _) L.tsums. They are summable over discrete subgroups, so no summability hypotheses are added.sInf). The paper's "smallest" is the attainment proved in milestones 1 and 2, not built into the definition. and are defined for every -submodule, so they apply to without extra instances.Real.sqrt gives there and the goal reduces to true statements. No hypothesis is added, since the page says "any ".Contributions welcome: the attainment of and for IsZLattice (and for the dual), the identity in this setting, continuity and monotonicity of Gaussian lattice sums, and above all Banaszczyk's transference theorem.
Many problems in signal processing, statistics and decision theory have two blocks of variables coupled by a smooth term: matrix factorization, blind deconvolution, feasibility problems for two sets, and models of two agents adjusting their decisions in turn. Minimizing over one block at a time (alternating minimization, or Gauss–Seidel) is the natural method. Without convexity it can oscillate, and its iterates need not converge. Attouch, Bolte, Redont and Soubeyran (Math. Oper. Res. 35(2), 2010; arXiv:0801.1780) regularize each block step by a proximal term. They prove that, when the objective satisfies the Kurdyka–Łojasiewicz (KL) inequality, every sequence of the method that does not run off to infinity has finite length and converges to a critical point.
Timeline:
Let and be proper (never , finite somewhere) and lower semicontinuous. Let be continuously differentiable, with Lipschitz on bounded sets. This is assumption (H) for
The product carries the Euclidean norm . Write .
Given and step sizes , the proximal alternating scheme is
Assumption (H1) asks that , that be proper, and that for all , for some .
The Fréchet subdifferential is the set of with . The limiting subdifferential collects the limits of along with . A point is critical if . has the KL property at if there are , a neighbourhood of and a continuous concave with , , , such that
If satisfies (H), (H1) and has the KL property at every point of , then every sequence of (5–6) satisfies
Theorem 9 makes the KL inequality the single hypothesis behind global convergence of a nonconvex block method. Semi-algebraic, subanalytic and definable data satisfy it, so the theorem covers sparse and low-rank regularizers, indicator functions of semi-algebraic sets, and polynomial couplings. With , and it yields convergence of an averaged alternating projection method between two closed sets (§3.4 of the paper). The proof pattern of sufficient decrease, a relative-error subgradient bound and the KL inequality was later abstracted for PALM and many other algorithms. A formal proof of this paper's argument therefore covers the template those analyses reuse.
The result has been proved since 2010. To our knowledge it has not been formalized in any proof assistant. Mathlib has the Fréchet derivative and the gradient, but no limiting subdifferential and no KL theory. The published Prove2Me definitions of the limiting subdifferential and of the KL property (from the Li–Pong ADMM series) are reused here, so this mission also tests that infrastructure on a second algorithm.
The decrease estimate (7) gives only . That makes steps vanish and limit points critical (Proposition 6), but it does not give convergence, because square-summable steps can have infinite total length. Turning square summability into summability needs the KL inequality. That inequality holds only near a critical point and only on a sublevel band, so the iterates must first be shown never to leave a ball , by an induction that uses the very finite-length estimate it is trying to establish. The constants in (16) are arranged so that this induction closes. A second difficulty is nonsmooth calculus: the subdifferential sum rule for and the closedness of the graph of along sequences with converging function values. Lower semicontinuity alone does not give convergence of the function values; the proximal inequalities do.
Everything lives in the namespace ProxAltMin.Conv, in Lean 4 with Mathlib. Conventions:
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and the product is the product WithLp 2 (… × …), not the sup-norm product.EReal with "never " as part of properness.Theorem and page numbers are those of arXiv:0801.1780v3 (22 Jan 2013), which is the version read; the published article has the same content.
A trivializing formalization is ruled out: the run predicate is satisfiable (Lemma 5's existence milestone; for any constant sequence is a run), the constants and are tied to the data rather than chosen by the prover, and no conclusion is a sum or a distance whose library value is on bad input.
Needed infrastructure: the subdifferential calculus behind Proposition 3 (a smooth perturbation and a separable sum), the closedness of the limiting subdifferential, existence of proximal minimizers for coercive lower semicontinuous functions on , and the elementary but delicate bookkeeping of Theorem 8. The first two are reusable well beyond this mission. Contributions welcome: proofs of any milestone, and general lemmas on limiting subdifferentials stated as separate theorems.
A well-quasi-order is a reflexive, transitive relation in which every infinite sequence contains a pair with . Showing that a class of finite combinatorial objects is well-quasi-ordered by a containment relation is a standard way to prove that every property closed under that containment is characterised by finitely many forbidden objects. The best-known instance is the Graph Minor Theorem (Wagner's conjecture), completed by Robertson and Seymour in Graph Minors XX (JCTB 92, 2004).
Nash-Williams proposed the analogous conjecture for a different containment, immersion, in which edges of the smaller graph are mapped to edge-disjoint paths of the larger graph. Graph Minors XXIII (JCTB 100, 2010) proves it by deriving a general well-quasi-ordering theorem for labelled hypergraphs from the machinery of Graph Minors XX.
Timeline.
All graphs and hypergraphs are finite. A graph has a vertex set , an edge set , and for each edge an unordered pair of ends; an edge with equal ends is a loop, and several edges may have the same ends (parallel edges). A graph is loopless if no edge is a loop. A path has at least one vertex and no repeated vertices; a circuit has at least one edge and no repeated vertices, so a loop and a pair of parallel edges are circuits.
An immersion of in is a map on such that is injective on vertices; every non-loop edge with ends goes to a path of with ends ; every loop at goes to a circuit of through ; and , share no edge when .
A hypergraph has finite sets , and an incidence relation; is the set of ends of the edge , of any size. Write for the complete graph on . A collapse of to maps each vertex of to a non-null connected subgraph of , pairwise vertex-disjoint, and each edge of injectively to an edge of , so that meets whenever is incident with , and every edge of every is covered by some edge of incident with both and . The transpose of a graph is the hypergraph with vertex set , edge set and the same incidence.
A quasi-order is an ideal of if it is a sub-quasi-order closed downwards in ; a shadow is a tuple of well-quasi-orders and finite sets, ordered lexicographically (Section 3 of the paper).
The immersion theorem implies that every class of finite graphs closed under taking immersions is characterised by finitely many excluded immersions. Theorem 1.6 is stronger than both 1.1 and Wagner's conjecture: it handles hypergraphs, labels from an arbitrary well-quasi-order and ordered edges, which is the form in which the Graph Minors machinery is reused by later work.
All results here are proved in the paper. None of them has a machine-checked proof: Mathlib has well-quasi-orders and Higman's lemma, but not the Graph Minor Theorem or any notion of graph immersion. The value of this mission is a faithful formal statement of the immersion theorem and of the reductions the paper performs in Section 1 (1.3 and the passage from 1.6 to 1.4, 1.5 and 1.1), each of which can be formalized independently of Graph Minors XX, plus the order-theoretic lemmas 3.1 and 3.2.
The reductions in Section 1 (1.3, and the passages from 1.6 to 1.4, 1.5 and 1.1) are short on paper but require a working library of multigraph walks, paths and circuits, which Mathlib does not have for graphs with loops and parallel edges. The real difficulty is 1.6, which the paper derives from a theorem on patchworks of Graph Minors XX (its 2.2) together with tangle results of Graph Minors X, and therefore rests on the structure theory of the whole Graph Minors series. No route around that theory is known: when the hypergraphs are loopless graphs, a collapse of to makes a minor of , so already 1.2 contains Wagner's conjecture. Nor does 1.2 alone give 1.1: loops cannot be routed through the transpose construction of 1.3, and the paper handles them by counting loops at each vertex as a label from the well-quasi-order , which is why the labelled forms 1.4–1.6 are needed.
A graph is Graph V E with ends : E → Sym2 V; a hypergraph is Hypergraph V E with inc : E → V → Prop; each lives on its own finite types, and a sequence is a family indexed by ℕ (from ; the paper's becomes ). Paths and circuits are walks with vertex and edge lists; the ends of a path are unordered. An immersion is the structure GraphImmersion H G; a collapse of to is Collapse G H, whose branch sets are Subgraphs of ⊤ : SimpleGraph V(G) (Mathlib's Subgraph.Connected includes non-emptiness). Well-quasi-orders are Mathlib's WellQuasiOrdered on a type with a preorder for 1.4–1.7, and QO.IsWQO on subsets of an ambient type for 3.1–3.2, where quasi-orders are compared by inclusion. Directed graphs for 1.7 are DirGraph V E with heads and tails.
Three trivializing formalizations are excluded: the collapse keeps condition (iv), so branch sets cannot use arbitrary pairs of vertices; immersion paths are edge-disjoint, not vertex-disjoint (which would give topological minors, not a well-quasi-order); and each graph lives on its own type, never all on one fixed finite type, which would make the goal a pigeonhole statement. Strong immersion is not stated.
Contributions welcome: proofs of 3.1, 3.2 and 1.3, the reductions 1.6 ⇒ 1.4 ⇒ 1.2 and 1.4 + 1.3 ⇒ 1.5 ⇒ 1.1, and library material on multigraph walks, paths and circuits, which is reusable beyond this mission. A proof of 1.6 would require formalizing the Graph Minors series.
A busy runway is the bottleneck of an airport, and the order in which arriving or departing aircraft use it determines how many operations fit into an hour. Consecutive aircraft must be spaced by minimum separations that depend on both aircraft (a light aircraft behind a heavy one needs a long gap because of wake turbulence), so reordering the first-come-first-served (FCFS) queue can raise throughput considerably. Unrestricted reordering is unacceptable in practice: it makes the controllers' job harder and can push one aircraft to the back of the queue indefinitely. Following Dear (1976), constrained position shifting (CPS) allows each aircraft to move at most positions away from its FCFS position, with between 1 and 3 in practice.
Earlier algorithms for CPS either exploited a small number of aircraft types and ignored time windows and precedence constraints (Psaraftis 1980), or needed exponentially many parallel processors (Trivizas 1998), and Carr (2004) conjectured that runway scheduling under CPS has exponential complexity in general. Balakrishnan and Chandran (Oper. Res. 58(6), 2010) showed that, for fixed , the problem with time windows and precedence constraints is solved by dynamic programming on a network whose size is linear in the number of aircraft. This mission formalizes the core of that result: the network, its precedence pruning, and the dynamic program for the minimum makespan.
There are aircraft, labelled in FCFS order, and the landing positions are also . An instance consists of
A -CPS sequence is a bijection from positions to aircraft with for all . A feasible schedule is such a with landing times such that , for all positions , and every precedence pair is respected. The makespan is , the landing time of the last aircraft.
The CPS network has stages . A node of stage is a list of distinct aircraft occupying the positions that end at , each within of its FCFS position; its last entry is its final aircraft. An arc joins a stage- node to a stage- node when the first entries of are the last entries of . A source-sink path picks one node per stage, joined by arcs, and its sequence puts the final aircraft of the stage- node at position . The pruned network deletes the nodes that violate a precedence pair : those containing before , or at a position less than , or at a position greater than .
On , with the window of the final aircraft of , the separation between the final aircraft of and , and the predecessors of , the dynamic program is at stage 1 and
with .
where is stage of ; the second identity is stated as " is the least makespan iff is the least admissible " for every real .
The network turns a search over permutations into a shortest-path-like computation over nodes, so for the small values of used in practice the minimum makespan with time windows and precedence constraints is computed in time linear in . The same network underlies the paper's algorithms for total delay (§5.2) and, in a time-expanded form, for arbitrary separable costs without the triangle inequality (§6).
The paper's proofs are short and informal. A formalization pins down exactly what means (the paper describes it only as "arrival time of the final aircraft of node in an optimal solution"), makes precise which nodes the precedence pruning removes, and checks the correctness of the stage- rule. The result has not been machine-checked before.
Two features of the model make the correctness of the network nontrivial. First, a node records only a window of at most consecutive positions, so nothing local prevents a path from using the same aircraft twice or omitting one; Theorem 1 asserts that the global sequence is nevertheless a permutation, and Lemmas 1 and 2 assert that precedence, a global property of the sequence, is detected inside single nodes. Second, the recursion (1) adds the separation only between consecutive aircraft, while feasibility constrains every pair of aircraft; the triangle inequality is what reconciles the two, and without it Lemma 3 fails.
The obvious reading of §4.1 also fails: taking the least over all stage- nodes, as the paper prints, can select a node whose final aircraft lands after its latest time. The goal filters stage by .
All data are real numbers; aircraft and positions are Fin n, 0-based; stages are 1-based natural numbers; [NeZero n] encodes . Separations are pairwise in the definition of feasibility, never only consecutive. The recursion takes values in WithTop ℝ, with ; optima are stated with IsLeast over sets of makespans, never with a real infimum. Precedence pairs are a Finset of ordered pairs of distinct aircraft, covering both of the paper's cases.
Explicit readings of loose phrases:
Not formalized: running times (Proposition 1 and the preprocessing remark), the predecessor pointers and tie-breaking that reconstruct an optimal sequence, the removal of nodes unreachable from the source or the sink (it does not change the set of source-sink paths), asymmetric shifts (§3.2) and disjoint time windows.
A formalization that defines feasibility with consecutive separations only, defines by the recursion and states Lemma 3 as an unfolding, or states Theorem 1 as "some CPS sequence exists iff some path exists" would be trivial; the statements here avoid all three.
The definitions (instance, -CPS sequences, the CPS network and its pruning) are shared with the two other missions of this series (total delay, discrete time) and may be consolidated later. Proofs of the milestones, and lemmas about the window structure of the network, are welcome.
Fast-fashion retailers such as Zara replenish their stores several times a week from a central warehouse, and the warehouse holds a limited stock of each garment that must be split across hundreds of stores. Caro and Gallien built the store-level sales model behind the shipment-allocation system they developed with Zara and tested in a live pilot (Caro and Gallien, Inventory Management of a Fast-Fashion Retail Network, working paper, August 2, 2007; published in Operations Research 58(2), 2010). One display policy shapes the model. A garment (a reference) comes in several sizes, a few of which are designated major sizes. As soon as one major size runs out in a store, the whole reference is removed from the shop floor, so the remaining stock of the other sizes stops selling.
The allocation optimization only works if expected store sales have the right shape. They must grow with inventory, show decreasing marginal returns, and show complementarity across sizes. Proposition 1 of the paper establishes these properties for the model. The paper also cites the analogous result of Lu and Song (2003) for assemble-to-order systems as the template for its proof.
Fix a finite set of sizes , split into the major sizes and the minor sizes . Time is measured from the last replenishment, and the next replenishment comes at time .
Demand is random. On a probability space, each size has a counting process , the number of sale opportunities for in . It is a Poisson process with rate :
The processes of different sizes are mutually independent. In Lean this family is IsPoissonFamily lam N P.
An inventory vector gives the stock of each size right after replenishment. The virtual stockout time of size is
the time at which size would run out if it stayed on display. For a set of sizes , write and . Under the major-size policy, the random sales over one period are
The expected sales function is (expectedSales). The proof also uses (hA) and the marginal difference (delta), where is the -th unit vector.
For every and all sizes :
and is supermodular on the lattice :
The statement is uniform in the rates, the horizon and the choice of major sizes, so it covers every instance of the model.
The result. Proposition 1 justifies treating each store's expected sales as a concave, complementary function of the size profile. The paper's allocation MIP is built on that structure. It approximates by a lower envelope of tangents and embeds the approximation in a mixed integer program that allocates warehouse stock across stores. The proposition explains why sending a unit of a major size can raise the value of the minor sizes already in a store. It also explains why the marginal value of a size falls as more of it is shipped. Without these properties a greedy or envelope-based allocation would have no structural footing.
Formalizing it. The result is proved on paper, with one error in the printed proof. The last line of the Appendix display gives as a probability, but the quantity is a time. The correct value carries a factor and has in place of . This mission states the corrected identity. As far as is known, no machine-checked proof of any part of the result exists. A complete development would give a verified link from a continuous-time stochastic model to the discrete convexity properties that inventory optimization relies on. It would also produce reusable facts about Poisson processes and their hitting times along the way.
The monotonicity of is pathwise and elementary. The other properties are not pathwise properties of . Under the major-size policy, a realisation of need not have decreasing increments in . The concavity and the complementarity appear only after taking expectations and rewriting through the stopping times, using identity (2). That identity is an optional-sampling statement for the compensated Poisson processes at the bounded random times . These times depend on several independent processes at once, so the relevant filtration is the joint one. Mathlib has optional sampling only in discrete time.
The marginal-difference formula needs three ingredients:
The first idea, proving concavity of directly from (1) path by path, fails for the reason above.
All objects live in the namespace FastFashion.Structure:
Fintype with decidable equality. The major sizes are a Finset Sp and the minor sizes are its complement. No nonemptiness assumption is placed on the sizes or on ; is allowed, as in the paper.Pi.single s 1.WithTop ℝ. It is on paths that never reach , so it is never Lean's junk value , and . The truncation (stopMin) is a real number in .Supermodularity.Monotonicity.SupermodularOn, applied on the whole lattice.Two formalizations would trivialize the mission, and neither is used. is defined as the expectation of from (1), never by formula (2), and is never defined by a product-of-probabilities integral. Proposition 1 states both readings of "supermodular": the per-coordinate marginal-difference inequalities and the lattice inequality.
Deviations from the printed text:
Infrastructure a complete development needs:
The Poisson-process and hitting-time lemmas are reusable well beyond this mission and are welcome as separate contributions. The companion mission on the paper's tangent-envelope approximation uses the same model layer.
Runway capacity is the binding constraint at many busy airports. An aircraft landing or taking off behind another must wait a minimum separation time that depends on the two aircraft's weight classes, because of wake vortices; the US Federal Aviation Administration publishes these spacing requirements. Reordering aircraft changes the sum of the separations incurred and hence the delays, but unrestricted reordering is unacceptable to airlines and controllers: an aircraft that arrived early could be pushed to the end of the queue. Constrained position shifting (CPS), introduced by Psaraftis (1980) and used in the United States and Europe since, allows each aircraft to move at most positions from its first-come-first-served (FCFS) position.
Balakrishnan and Chandran (Operations Research 58(6), 2010) recast CPS scheduling as dynamic programming on a layered network, the CPS network, whose size is polynomial in the number of aircraft for fixed . Their §4 minimizes the makespan (the landing time of the last aircraft). §5.2 minimizes the total delay, equivalently the average delay, which measures passenger and airline cost more directly. This mission formalizes §5.2.
There are aircraft labelled in FCFS order, a maximum position shift , separations (the minimum time between leading aircraft and trailing aircraft ), and a finite set of precedence pairs with , meaning that must land before . The separations satisfy the triangle inequality , as wake-vortex separations do for arrivals-only or departures-only operations.
A -CPS sequence is a permutation of the aircraft (position receives aircraft ) with for every . A feasible schedule is a -CPS sequence that places before for each precedence pair, together with landing times (by position) such that
There are no time windows. Its total delay is , measured from time , at which all aircraft are available.
The CPS network has stages . A node of stage is a sequence of distinct aircraft that can occupy positions (each within of its position). Its last aircraft is its final aircraft. An arc joins a stage- node to a stage- node when the sequences overlap: the first aircraft of are the last aircraft of . A source-sink path picks one node per stage, and its sequence assigns position to the final aircraft of the stage- node. Precedence is incorporated by deleting every node that places before for some pair , or that places an aircraft outside the positions a pair allows it (§3.1). The result is the pruned network . For nodes , is the separation between their final aircraft.
For a node in stage and times along a path to , the paper uses the partial objective
Give the arc from stage to stage the distance , and source and sink arcs distance . Then a feasible schedule exists if and only if has a source-sink path, and
where each minimum exists exactly when the other does.
where is the set of predecessors of in .
The result turns a sequencing problem over up to orders into a shortest-path computation on a directed acyclic graph with nodes, and it does so while respecting precedence constraints, which earlier CPS algorithms (Psaraftis 1980; Trivizas 1998) could not handle. It is the average-delay counterpart of the makespan algorithm of §4 and shares its network. The same network carries the discrete-time models of §6.
The paper's proof of the equivalence is one sentence ("follows from properties of shortest paths and is omitted here"). Propositions 2 and 3 are proved in a few lines, and Theorem 1 by an argument about windows of consecutive positions. None of these results has a machine-checked proof. A formal development makes explicit the conventions the prose leaves implicit (the time origin, pairwise separations, which nodes Proposition 3 refers to) and checks that the recursion and the shortest-path value really compute the minimum total delay.
The arc distances weight the separation into stage by , the number of aircraft whose landing it delays. The equivalence needs two directions. A path's length must be the total delay of the schedule that lands each aircraft at its predecessor's time plus the separation, and that schedule must satisfy every pairwise separation, not only the consecutive ones; this is where the triangle inequality enters. Conversely, every feasible schedule must have total delay at least the length of its sequence's path, and every feasible sequence must be a path of . The last point is Theorem 1 with precedence pruning: a node sees only consecutive positions, so detecting a violated precedence pair inside one node requires the position filter of §3.1 for pairs that reverse FCFS order. Proposition 3 is false for nodes that lie on no source-sink path, which the printed statement does not exclude.
Aircraft and positions are Fin n, 0-based, and stages are 0-based natural numbers, so the arc into stage has distance . Separations are real, nonnegative and satisfy the triangle inequality; feasibility requires them between every pair of positions. Landing times are real and nonnegative. The paper fixes no time origin, but its path length equals the total delay exactly when delays are measured from , and without a lower bound on the times the objective has no minimum. Minima are stated with IsLeast on sets of values, never with a real infimum. Feasibility and the existence of a path are stated separately, because the equality of least elements alone does not force them to exist.
The following loose phrases are given explicit readings. "In an optimal solution" (Proposition 2) means a feasible schedule whose total delay is at most that of every feasible schedule. "The CPS network" in Proposition 3 means nodes lying on a source-sink path, stated for the network without precedence pruning, which also covers the pruned one. "" means the least element of the set of values of over partial schedules ending at , and the printed is read as . The boundary value is not printed and is stated explicitly. Precedence pruning uses the printed Case II rule. Running times (the bound) are not formalized.
A trivializing formalization would require separations only between consecutive aircraft, define the minimum by the recursion itself, or use a network whose nodes need not be distinct or admissible. Here the minimum is defined directly over feasible schedules, separations are pairwise, and the nodes are checked against the paper's Figure 1 (stage sizes 2, 4, 7, 14, 14, 7 and 13 paths for , ).
The development needs finite sums, permutations of Fin n and lists. The network layer (stages, arcs, precedence pruning, Theorem 1) is shared with the makespan and discrete-time missions of this series and reusable for any CPS objective. Proofs of any milestone, alternative proofs of the goal, and generalizations (asymmetric shifts, §3.2) are welcome.
Large engineered systems — power grids, chemical plants, logistics and communication networks — are usually modelled as many interacting subsystems. A stability certificate for the whole network is rarely available directly, but each subsystem can often be analysed on its own, treating the states of its neighbours as disturbances. Input-to-state stability (ISS), introduced by Sontag (Sontag 1989), is the robustness notion that makes this decomposition work: it bounds the state by a decaying function of the initial condition plus a gain of the input. A small-gain theorem states that if the gains by which the subsystems influence each other are "small" in a suitable sense, the interconnection is again ISS.
Timeline. Jiang, Teel and Praly proved a nonlinear small-gain theorem for two ISS systems in trajectory form (1994), and Jiang, Mareels and Wang gave its Lyapunov version for two subsystems (1996). Dashkovskiy, Rüffer and Wirth extended the trajectory version to subsystems with the condition on a nonlinear gain operator (2007). The paper of this mission (arXiv:0901.1842, SIAM J. Control Optim. 48(6), 2010) gives the Lyapunov version for subsystems with general monotone aggregation of the gains, and constructs the network's ISS Lyapunov function explicitly.
The network consists of subsystems
with overall state and dynamics , . is the Euclidean norm.
A function is of class if it is continuous, strictly increasing and , and of class if moreover unbounded. A positive definite function is continuous with only at . A Lyapunov function candidate is continuous, satisfies for some , and is locally Lipschitz away from the origin.
A candidate is an ISS Lyapunov function for if there are and a positive definite with
at every point of differentiability of .
On , means for every . A monotone aggregation function (MAF) is continuous, positive off the origin, strictly increasing for this strict order, and unbounded as . Subsystem has an ISS Lyapunov function with gains , and MAF on if, wherever is differentiable,
The diagonal gains vanish, . The gain operators are
An Ω-path with respect to is a continuous with every , such that each is locally Lipschitz on , its derivative lies in , , at its points of differentiability in any compact (constants depending on only), and for all .
Assume each is an ISS Lyapunov function for with gains , and MAFs ; is an Ω-path with respect to ; satisfies
and each is continuous. Then
is an ISS Lyapunov function for the network, with gain :
for a positive definite . The rate is existential and is not fixed by the statement.
The milestones follow the proof on pp. 14–15:
The result. Theorem 5.3 converts a small-gain condition into an explicit Lyapunov function for the network. Combined with the converse ISS Lyapunov theorem, it gives ISS of the interconnection, and with zero input it gives global asymptotic stability. It covers additive, maximum-type and multiplicative aggregation of gains, and it handles subsystems without iterating a two-system result. A second main result of the paper (Theorem 5.2, a separate mission) supplies the Ω-path from the condition . Together they reduce the stability of a network to a property of its gain operator.
Formalizing it. The result is proved on paper. As far as we know, no ISS notion, small-gain theorem or monotone aggregation framework has been machine-checked in Lean. This mission produces a Lean statement of the construction, and of its nonsmooth-analysis steps, against which a complete proof can be checked. It also corrects a misprint in the theorem's implication (see Formalization scope).
The function is a maximum of rescaled functions and is not differentiable on the set where two indices are active, even when every is smooth. The subsystem hypotheses only control derivatives at points where the corresponding is differentiable. At a point where is differentiable, the active may not be. So the obvious argument — differentiate the active branch and apply (2.7) — fails, and the decrease must be transported through generalized gradients. A second obstacle is uniformity: the rate must depend on alone. This requires the lower derivative bound in the Ω-path definition and a compactness argument on spheres. Dropping the lower bound breaks the theorem, because could flatten and remove the decrease.
Blocks are EuclideanSpace ℝ (Fin (N i)). The network state is the product PiLp 2 (the Euclidean norm, not the sup norm), and the input is EuclideanSpace ℝ (Fin M). Subsystems are indexed by Fin n (0-based) with . Gains, MAFs, Ω-paths and rates live on ℝ≥0. Lyapunov functions are real-valued with an explicit nonnegativity clause. The strict order on is a named predicate, not Lean's Pi <. The inverses and are explicit arguments with both compositions the identity. Every derivative is guarded by a differentiability hypothesis. Clarke's generalized gradient (2.5) is the published ClarkeGradients.Shared.generalizedGradient on the blocks, and the same definition restated on a general Hilbert space for and .
Implicit hypotheses made explicit:
Corrected statement. The printed implication (5.5) has the trigger . With as defined in (2.9), and as the paper's corollaries use it, that implication is false. A counterexample is one subsystem with , , and , at , . The proof's chain of inequalities writes where (2.9) gives . The goal keeps (2.9) and uses the trigger , under which the proof closes.
The hypotheses are jointly satisfiable. An example is with , , , , , and dynamics . The conclusion is a decrease inequality at the points of differentiability of for an existential positive definite rate, so it cannot be met by a vacuous choice: must be positive away from zero. Trajectory-level ISS (Theorem 2.3, cited by the paper) and the corollaries that conclude ISS are out of scope.
Reusable infrastructure: comparison classes, monotone aggregation functions, gain operators and Ω-paths (shared with the Ω-path mission), and the maximum and chain rules for Clarke gradients. Proofs of the nonsmooth calculus milestones are welcome independently of the goal.
Facility location models decide where to open depots, warehouses or service centres and which customers each one serves. Classical models assume that an open facility always works. In practice facilities are disrupted by weather, strikes, power loss or supplier failure, and a network designed for normal operation can become very expensive when its nearest facilities go down. Reliable facility location models place facilities so that the sum of the fixed cost and the expected transportation cost, taken over random facility failures, is minimal.
Cui, Ouyang and Shen (UCTC-FR-2010-02, 2010; published as Oper. Res. 58(4):998–1011) study the case in which each site fails independently with its own probability. The most direct model of this situation is a scenario-based stochastic program: list every pattern of failures, give it its probability, and let each customer be served optimally in each pattern. That program has scenarios for candidate sites and cannot be written down for realistic . The paper proposes instead a compact formulation in which each customer receives an ordered list of backup facilities ("levels") and the probability that each level is the one that serves her is carried by a small set of recursive variables. This mission is about the claim that the compact model loses nothing.
The level-assignment technique comes from Snyder and Daskin (Transp. Sci. 39(3):400–416, 2005), who treated the case of one common failure probability for all sites. The uniform-probability model of Snyder and Shen's textbook is on the platform as SupplyChainTheory_disruptions; it is a different model (one , no cap on the number of levels) and is not reused here.
There are customers with demand rates and candidate sites with fixed costs and failure probabilities . Failures are independent. Shipping one unit from site to customer costs , and each unit of missed demand of customer costs a penalty . An emergency facility with index never fails (), costs nothing to open (), and "serves" at the penalty cost .
The compact model (RUFL). Each customer is assigned to facilities at levels , with ; a level- facility serves her exactly when all her facilities at levels have failed. The variables are (site open), (facility is customer 's level- facility) and , the probability that serves at level . Constraints (1b)–(1d) say that each level holds one facility until the emergency facility appears, which happens exactly once, and that only open sites are used, each at most once. Constraints (1e)–(1f) fix : and . The objective is
The scenario model (SSP). A scenario is , with if site operates in (and always). Its probability is . With (customer served by in ), (SSP) minimizes
subject to and for regular .
If , both programs have optimal solutions, and for every optimal of (RUFL) and every optimal of (SSP),
The paper states this as "formulation (1a)–(1g) is equivalent to the stochastic programming formulation that covers all failure scenarios"; its proof shows equality of optimal values, and that is the reading formalized.
The proposition says that, with enough levels, the compact model is exact: its optimal value is the true minimum expected cost over all failure patterns. The compact model has variables and constraints against for (SSP), and after the standard linearization of the products it is an ordinary mixed-integer program to which the paper's Lagrangian relaxation applies. For the paper notes the compact model is in general not equivalent; Proposition 1 is the anchor that says what the parameter trades away.
The result is proved in the paper; as far as we know it has not been formalized. The work here is to formalize that proof: the product-measure computation behind milestone 1, the two explicit solution maps, and the exchange argument behind the normalization. The probability identity for "first success in an ordered list of independent trials" and the scenario-to-level bookkeeping are reusable for other reliability models built on Snyder–Daskin levels.
The cost identities are routine once the right bookkeeping is in place; the obstacle is that bookkeeping. In direction (RUFL) → (SSP) one must show that the recursion (1e)–(1f), which multiplies by and sums over all regular , collapses to the closed product along a customer's assigned list, using that (1b)–(1d) put exactly one facility on each level until the emergency facility and that (1c) forbids repeats. Then the sum over the scenarios must be regrouped by the first operating facility on that list, which needs milestone 1 on a product space.
The converse direction is where enters, and the naive attempt fails: an arbitrary optimal (SSP) solution may serve a customer by different, equally good facilities in different scenarios in ways that no single ordered list reproduces. The normalization step removes this freedom; only after it can one read off a single list per customer, and guarantees that this list (all open sites no farther than the penalty, then ) fits on the available levels.
Indices are 0-based; facilities are Fin (J+1) with Fin.last J the emergency facility, and levels are Fin (R+1). The extended data , , and the conventions , are definitions, not hypotheses. Scenarios are Fin J → Bool and is the explicit finite product; no measure theory is involved, and (17a) is a finite sum. Binary variables are real numbers constrained to . is expressed by taking the instance type Instance I J J; with the standing this means . Demand rates are nonnegative; no sign is assumed on , or .
Two printed constraints are corrected, and the formalization commits to the corrections. The first sum in (1b) is printed over the regular sites ; it runs here over all facilities, as the paper's own reading of (1b) requires. Constraint (17c) is printed as , which gives each site a capacity of one customer per scenario and makes Proposition 1 false; it is stated here per customer, .
The goal asserts existence of optimal solutions of both programs before comparing their values, so it cannot hold vacuously. Contributions welcome: proofs of the milestones, a general lemma on the probability that the first success among independent Bernoulli trials occurs at a given position, and an existence-of-optimum lemma for finite binary programs.