Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Networks of coupled oscillators model generators in an electric power grid, pacemaker cells, Josephson junction arrays and many other systems in which units with their own rhythm interact through their phase differences. Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012, doi:10.1137/110851584) show that, after a singular-perturbation reduction, the transient-stability question for a lossy power network with non-uniform generators becomes a synchronization question for a non-uniform Kuramoto model: oscillators with different damping coefficients, different natural frequencies, an arbitrary coupling graph and phase shifts induced by line losses.
This mission concerns the cleanest regime of that model: lossless coupling and natural frequencies proportional to the damping. There the oscillators do more than agree on a frequency; they agree on a phase. For the classic Kuramoto model (Kuramoto, 1975) with identical frequencies, phase synchronization from inside an open half-circle was obtained by consensus methods for nonlinear coupled systems (Lin, Francis and Maggiore, 2007) and by Jadbabaie, Motee and Barahona (2004). Theorem V.10 of Dörfler–Bullo extends this to non-uniform damping, directed coupling with a globally reachable node, and gives an explicit worst-case rate for symmetric coupling. The proof rests on the contraction theory of time-varying consensus protocols (Moreau, 2004).
There are oscillators. Oscillator has a phase on the circle, a damping coefficient and a natural frequency . Oscillators interact through coupling weights (, with ) and phase shifts . The non-uniform Kuramoto model (8) is
The weights define a directed graph with an edge from to whenever ; a globally reachable node is a node to which every node has a directed path. For the closed arc set is the set of configurations whose angles all lie in a closed arc of length .
This mission assumes zero phase shifts, , and proportional frequencies, for all . The phases synchronize exponentially to a trajectory when there are and with for all and .
For the rate, is the Laplacian of a weight array, is its second-smallest eigenvalue (the algebraic connectivity) when , , , , and .
For every solution with , :
Theorem V.10 gives phase synchronization of non-uniform oscillators from every initial configuration inside an open half-circle, for directed coupling graphs that need only a globally reachable node, and identifies the limit phase: anywhere in the initial range in general, the damping-weighted mean under symmetric coupling. The rate separates three effects: graph connectivity (), initial phase cohesiveness () and non-uniformity of the damping (, ). For the classic Kuramoto model the statements reduce to known results ([19] and [33] of the paper).
The result is proved in the paper; no machine-checked proof is known. A formal proof needs a Dini-derivative argument for the maximum of finitely many smooth functions along an ODE, a contraction theorem for linear time-varying consensus with positive, bounded weights on a graph with a globally reachable node, and a Courant–Fischer bound on the weighted disagreement. Each is a reusable piece of infrastructure for networked control and synchronization.
The obvious argument linearizes: , so the model looks like linear consensus. That only holds near the diagonal; from an arc of length close to the effective weights come close to zero and depend on the state, so neither a fixed Laplacian nor a local linearization covers the claimed region. One needs first that the arc never grows, which is a statement about a non-smooth function (the arc length) along trajectories, and then exponential convergence of a consensus protocol whose weights are time-varying and, for directed graphs, non-symmetric, so there is no quadratic Lyapunov function in general. For the explicit rate the disagreement vector is orthogonal to , not to , and the angle between the two hyperplanes has to be controlled.
Angles are represented by real lifts ; the vector field is -periodic in each coordinate, so solutions on the torus are projections of solutions on . is encoded as for all on the initial lift, and every conclusion (invariance, , , the weighted mean, the convergence bounds) refers to that lift and the same continuous lifted trajectory, which is at least as strong as the statement on the torus. A solution is a curve on whose derivative within equals the vector field at every ; statements quantify over every such curve. The model is stated with the paper's general field and hypotheses , ( arbitrary, not set to zero).
Conventions and corrections, each disclosed in the item's Formalization Note:
AlonMilman.PropertyT.lambda1 applied to the symmetric Laplacian.Exponential convergence requires a rate ; a statement with or with a solution predicate that no curve satisfies would be trivial. The synchronous trajectory satisfies the solution predicate, so the hypotheses are satisfiable.
Infrastructure welcome beyond this mission: upper Dini derivatives and comparison lemmas for maxima of differentiable functions, exponential stability of linear time-varying consensus (Moreau's theorem), and Laplacian ordering for entrywise-dominated weights.
A real number is normal in base when every block of base- digits occurs in its expansion with limiting frequency , exactly as it would in a sequence of independent uniformly random digits. It is normal (absolutely normal) when it is normal in every base . Whether the classical constants of analysis, above all , are normal is one of the oldest open questions linking number theory and probability: it asks whether a number defined by geometry has digits that are statistically indistinguishable from random ones.
Timeline.
Large-scale digit computations of are statistically consistent with normality. No base is known in which is normal, and it is not even known that any particular digit occurs infinitely often in its decimal expansion.
A digit sequence is a function ; is the first digit after the point. A word is a finite list of naturals. For , the occurrence count is the number of positions with for every . Overlapping occurrences each count.
The sequence is normal in base (IsNormalSeq b s) if, for every word with all entries ,
The -th base- digit of a real after the point is
The real is normal in base (IsNormalReal b x) if is normal in base . Two remarks:
This is the conjecture in its standard form, normality in every base. The base-ten case is the special case .
None are listed. No decomposition of this problem into intermediate statements is known that would be a faithful attack path, and the mission does not invent one. Proposals for intermediate targets are welcome in the discussion; see the contributions listed under Formalization scope.
The known theorems of the subject (Champernowne's constructions, the Copeland–Erdős theorem, Borel's theorem) concern numbers built to be normal or almost every number; they are not steps toward and are kept in the separate mission Explicit normal numbers: Champernowne and Copeland–Erdős.
A proof that is normal in base would give every finite digit pattern a definite limiting frequency in its expansion. It would be the first normality result for a classical constant not built to be normal. Every known normal number is constructed digit by digit (Champernowne, Copeland–Erdős, Sierpiński, Becher–Figueira) or shown to exist by a measure argument (Borel). Even the base-2 case would settle the Bailey–Crandall programme for .
Formalization status. The goal is open mathematics. The definitions it is stated with are published and are shared with the mission Explicit normal numbers: Champernowne and Copeland–Erdős, where Champernowne's theorems and the Copeland–Erdős theorem have machine-checked proofs.
The constructive results all prove normality from the digit-by-digit description of the number. In particular, the Copeland–Erdős block criterion needs the expansion to be an explicit concatenation of blocks. has no such description. Its known series (Machin-type formulas, BBP) give digits as values of exponential sums, and no known method controls the joint distribution of long digit blocks of such values.
Borel's theorem does not help: it only says that the exceptional set is null, and gives no criterion for deciding whether a given number lies in it. Neither high-precision digit statistics nor irrationality measures for imply normality.
All declarations live in the namespace Normal and use the definition bundle Normal_Core:
count, IsNormalSeq, digit, IsNormalReal;ofDigits b s ;flatten, digitsBE, concatDigits;Committed conventions:
The definitions agree with Borel's, and the mission does not admit a trivialising reading. A real number is not normal merely because it is irrational, and the empty word imposes only the trivial condition.
The bundle also contains a verbatim copy of the integer-arithmetic definition IsNormal from xiangyazi24/agafonov; its equivalence with IsNormalSeq is proved on the platform (Normal.isNormalSeq_iff_isNormal), so results stated in either form transfer.
Welcome contributions:
Random time changes occur when a process is observed on an operational clock rather than calendar time. In queueing models, for example, an arrival-count path may be evaluated at an evolving service clock. A functional limit theorem for the outer path and another for the clock are useful together only when evaluating one path at the times supplied by the other preserves convergence. Ward Whitt's 1980 paper studies several path operations with this question in mind; composition is its first main operation. The issue is specific to paths with jumps, because a small shift of the clock can move an evaluation across a jump.
Let be nonempty intervals of real time, with , and let be a complete separable metric space. The càdlàg path space consists of paths that are right continuous and have left limits on . Its subspace contains the continuous paths. The nondecreasing clock space consists of càdlàg real-valued paths on that are nondecreasing and take their values in . Its subspace contains the continuous, strictly increasing clocks. For and , composition is the path on .
Convergence uses the Skorohod topology. On a compact interval , let be the increasing homeomorphisms of and let . With denoting uniform distance, Whitt's metric is
Thus close paths may have nearby jumps at different times, provided an increasing time change aligns them. On a general interval, convergence is checked on compact subintervals whose endpoints are continuity points of the limit or endpoints of the full interval. Whitt gives this definition in §2, then gives , , and in §3. All subsets carry relative topologies and products carry product topologies.
For in and in , the first milestone states
The path-space definition and the two preparatory milestones are a small-oscillation partition for a càdlàg path, cited by Whitt from Billingsley, and Whitt's Lemma 2.2, which relates convergence on a compact interval to convergence on the two pieces made by splitting it at a continuity point.
The second case, and the combined goal, also allow the outer limit path to jump. Let mean the endpoints of that belong to . The corrected target is
The goal includes both cases for simultaneously varying and . The endpoint condition is vacuous for an endpoint excluded from . It is part of the strictly increasing clock case only; it imposes no extra restriction when the outer limit path is continuous.
This theorem supplies a precise condition for carrying two path limits through a random time transformation. In particular, the assertion includes convergence of the composed paths as elements of a càdlàg space, not merely convergence of their values at individual times. The distinction matters at jumps: pointwise convergence does not control the placement or ordering of nearby jumps. The result is a deterministic continuity statement that can be paired with probabilistic mapping theorems when the corresponding random paths are available.
Whitt proved the composition theorem in 1980, subject to the endpoint issue described below. The formalization work here is to construct its path-space interface in Lean, state the corrected continuity theorem with every domain condition visible, and eventually replace the open sorry proofs with checked proofs. The interface can also support the paper's later results on reflection, first passage, and time reversal; those results are separate missions. No proof of this mission's goal is claimed yet.
The tempting argument is to use separate continuity of and and then substitute into the first convergence. That argument loses control of evaluations near a jump of . A time change may align a jump of with the corresponding jump of , while the clock may cross those times differently. Continuity of the outer limit path removes that difficulty in one case; in the other, the clock must be continuous and strictly increasing. The source explicitly shows that composition is not continuous on all of (§3, p. 75).
The endpoints impose a further obstruction because increasing homeomorphisms of a closed time interval fix its endpoints. Bauer's Remark on p. 75 observes a failure at the right endpoint. There is a symmetric failure at the left endpoint, so the statement here includes both. This is a correction to the printed theorem, not a new claim that the uncorrected theorem is true.
Paths are represented as total functions , with only values on the named interval used. The domain assumptions OrdConnected and Nonempty express nonempty real intervals. The outer interval is also required to have nonempty interior: the formal convergence predicate checks only compact intervals with , so on a one-point it imposes nothing, and the case would fail for constant outer paths with different values. A clock's range condition is explicit, as is nondecreasingness for every prelimit clock. Membership of all paths in the relevant càdlàg spaces is part of the convergence predicates. The output predicate likewise requires every composition and its limit to be càdlàg. This rules out the trivialization in which one merely proves convergence of selected point evaluations or assumes the compositions already have the conclusion's path-space properties.
The compact uniform distance and the infimum over time changes take values in . They use the actual metric on , not a real supremum with a default value on an unbounded set. A time change is a total function whose restriction to the compact interval is continuous, strictly increasing, and onto. Continuity at a time means continuity relative to the path's interval. The general-interval convergence predicate checks the compact intervals specified by Whitt and requires each sequence member to belong to . The theorem is written as sequential continuity; Whitt's spaces are metrizable, making that equivalent to topological continuity. The real-valued clock space uses the relative topology inherited from real-valued càdlàg paths.
The endpoint correction is exact in the Lean statement. At the right endpoint, take , , for , and . Then is zero while . At the left endpoint, take , , , , and . The outer paths converge in on , but the compositions disagree at . Both examples show why continuity of at the image of every included endpoint is required in the case.
The development needs the càdlàg definition, metric and convergence predicates, compact restriction lemma, and the finite oscillation partition. Their definitions and lemmas are reusable for other functionals on path spaces. Contributions that prove the milestones and goal under the stated hypotheses are welcome. This mission does not formalize the Borel measurability or probability-measure machinery discussed elsewhere in Whitt's paper; Theorem 3.1 itself is a deterministic continuity claim.
Random coordinate descent minimizes a smooth convex function by updating one coordinate at a time, chosen at random. Each iteration needs a single partial derivative instead of the full gradient, which is what makes the method usable on problems whose dimension is in the millions or billions ("huge-scale" problems). Nesterov's paper Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362, doi:10.1137/100802001) gave the first global efficiency estimates for such methods and started a large literature on randomized block and coordinate methods.
The basic method RCDM of the paper takes, along coordinate , a step of length , where is a Lipschitz constant of the -th partial derivative along the -th coordinate. For simple functions these constants are known; for more complicated ones they are not, and a practical method has to estimate them on the fly. Section 6.1 of the paper analyses a backtracking strategy with restore for this purpose and proves that it keeps the efficiency of RCDM up to a constant factor. This mission formalizes that analysis, Theorem 7 of the paper.
Write and for the -th standard basis vector of , . The function is convex and differentiable, attains its minimum , and its partial derivatives are coordinate-wise Lipschitz with constants ((2.2) with one-dimensional blocks):
The weighted norm and its dual are and ((2.7) with ), and
measures the size of the initial level set, being the set of minimizers.
The random adaptive coordinate descent method RACDM (6.1) keeps estimates , initialised with given lower bounds . At iteration it
The loop test uses only the sign of one partial derivative and never a function value. With (the expectation over ) and the number of partial derivatives computed in iterations , Theorem 7 states three facts about this method.
This is the rate of RCDM, ((2.14)), with a larger constant.
The result shows that the constants in RCDM need not be known: a method that starts from any lower bounds and adjusts them by doubling and halving converges at the same rate, and pays on average about two partial derivatives per iteration plus a logarithmic one-time overhead. This is what makes random coordinate descent applicable to functions whose coordinate smoothness is not available in closed form, and the doubling-with-restore pattern recurs in later adaptive and accelerated coordinate methods (the paper itself indicates the same technique for its accelerated method, (6.5)).
The theorem is proved in the paper; to our knowledge no machine-checked proof exists. The known-constant analogues for scalar coordinates are on Prove2Me in Bubeck's §6.4 development (the one-step and expected decreases are proved there; the rate is open). This mission adds a formal model of the adaptive method itself, including its doubling loop as a first-failure search, and the three statements of Theorem 7 on top of the published coordinate-descent definitions.
The analysis of RCDM rests on the one-step bound , which follows from the smoothness of along the coordinate line. For RACDM the step uses an estimate that may be smaller than , and then the same argument gives no decrease at all: a step that is too long can increase . The method never checks function values, so the decrease has to be extracted from the sign test alone, and it holds only because is convex along the line, not merely smooth. A second point is that the estimates are random and depend on the whole history, so the expected decrease must hold for every state the method can reach; this is what item 1 secures. The counting statement needs the exact number of loop iterations, so the loop has to be modelled as the least number of doublings after which the test fails, not as some number of doublings.
The formalization works with scalar coordinates (, as the paper does in §6.1) on EuclideanSpace ℝ (Fin n), coordinates indexed . It reuses the published definition ConvexOptAlg_CoordDescent_Defs: IsCoordSmooth f g L is (2.2) with an explicit gradient map , wnorm L 1 and wnormDual L 1 are and , and rcdExpect L 0 k is the expectation over uniform draws as a finite weighted sum. The mission's own definition NesterovRCD.Adaptive.RACDM encodes the trial point, the number of doublings (a minimum over ), one iteration, the run along an explicit sequence of draws, and the count .
The following choices are made explicitly.
A trivializing encoding is ruled out: the loop count is the least at which the sign test fails (an arbitrary admissible would change the method and make the count meaningless), the draws are uniform, and the rate is stated in the norm of the true constants , not of the estimates. Contributions welcome: proofs of the milestones, a one-dimensional co-coercivity lemma for convex smooth functions of one variable (reusable well beyond this mission), and the recursion argument from the expected decrease to the rate.
Dynamic programming rests on time consistency: a control that is optimal when viewed from time stays optimal when viewed from any later time. Many problems of mathematical finance lack this property. The continuous-time mean–variance portfolio problem (Zhou–Li 2000) contains a variance, that is, a nonlinear function of an expectation, and state-dependent risk aversion (Björk–Murgoci–Zhou) lets the criterion itself depend on the current state. For such problems an optimal control computed today is abandoned tomorrow, and the HJB equation is not available.
One response, going back to the game-theoretic view of non-commitment (Ekeland–Lazrak, arXiv:math/0604264; Björk–Murgoci, SSRN 1694759), is to replace optimality by equilibrium: a control that no "future self" can improve by deviating on an infinitesimally short interval. Those works consider feedback (Markov) controls. Hu, Jin and Zhou (arXiv:1111.0818v1) define equilibrium within open-loop controls for a general stochastic linear–quadratic (LQ) problem with random coefficients, and characterize it by a flow of forward–backward SDEs, in the spirit of the stochastic maximum principle (Peng 1990). This mission formalizes that characterization: §2 and §3 of the paper, up to Theorem 3.2. The other two missions of the series build on it. Mission II treats a scalar state with deterministic coefficients (Theorem 4.4), and Mission III treats mean–variance portfolio selection (Theorem 5.4).
Let be a standard -dimensional Brownian motion on with its filtration , and let . A control is a process , that is, progressively measurable with . Its state solves the linear SDE
Here is a bounded deterministic matrix function. (), () and () are essentially bounded progressive processes, and . At time , with state and , the cost is
are bounded symmetric processes with , and are symmetric with . The last two terms make the problem time-inconsistent. Given with state , the spike variation at is for . The control is an equilibrium (Definition 2.1) if for every and every such , almost surely
For each , the first adjoint process solves on the BSDE (3.1) with driver and terminal value . The second adjoint process solves the matrix BSDE (3.2) with terminal value . With these, define
Suppose , its state , and for every a solution of (3.1) are given, and suppose satisfies condition (3.4):
Then is an equilibrium control.
Theorem 3.2 is the paper's general tool. Its two explicit results are applications of it. With a scalar state and deterministic coefficients, a pair of coupled Riccati-type equations gives a linear feedback equilibrium (Theorem 4.4). In mean–variance portfolio selection with state-dependent risk aversion and a possibly random risk premium, the equilibrium strategy is found through a quadratic BSDE (Theorem 5.4). Each is proved by exhibiting a solution of the flow (3.6) and checking (3.4). The theorem therefore separates the existence question (solving a flow of FBSDEs) from the equilibrium question. The paper notes that the general existence question remains open.
The results are proved in the paper and have no machine-checked proof. The mission produces a precise statement of open-loop equilibrium for a stochastic LQ problem with random coefficients, together with Lean statements of the spike expansion and of the adjoint flows. Mission II and Mission III restate the same model, and their final steps apply this theorem. Formal proofs of the milestones exercise Itô calculus for linear SDEs and BSDEs with bounded coefficients: product rules, conditional estimates, and uniqueness and sign properties of linear BSDEs. This is infrastructure that Mathlib does not yet have.
The obvious argument is a first-order expansion of in . It fails because the spike changes the control by , which is not small, on a set of small measure. The state's deviation is then of order in , its square contributes at order , and a second-order term appears that a first-order adjoint cannot capture. Two features are absent from the classical maximum principle. The adjoint equations form a whole flow indexed by , because the terminal value of (3.1) contains and . And every statement is conditional on , so the expansion has to hold almost surely at the level of conditional expectations. That rules out arguments based on unconditional expectations.
Brownian motion, , Itô integrals and SDE solutions come from the published definition Peng1990_SMP_Stochastic. The formalization commits to the following conventions.
The conclusion of the goal is Definition 2.1 itself. It mentions neither nor the adjoint processes, so the goal cannot be closed by unfolding. A definition of equilibrium in terms of (3.4) or (3.5) would make Theorem 3.2 trivially true and is ruled out. Condition (3.5) of p. 6 is not a hypothesis of any statement. A degenerate, noise-free example checks that the hypotheses of the goal can hold together.
Contributions are welcome as follows. Proofs of the three milestones are reusable for Missions II and III and for any spike-variation argument. So are general lemmas on linear SDEs and BSDEs over Peng's Itô integral: uniqueness, conditional moment bounds, the Itô product rule, and positivity of linear matrix BSDEs.
A differential variational inequality (DVI) couples an ordinary differential equation with a finite-dimensional variational inequality whose solution acts as an algebraic input to the dynamics. The class contains linear complementarity systems, mechanical systems with unilateral contact and friction, dynamic Nash games and many hybrid engineering models. Pang and Stewart's paper (Math. Program. 113 (2008); author's version hal-01366027v1) set up a unified theory of such systems: existence of solutions, uniqueness, and convergence of numerical time-stepping schemes.
The numerical question is the practical one. A DVI is solved by discretizing time and solving one finite-dimensional variational inequality per step. Whether the discrete trajectories approximate a true solution as the step size shrinks is not automatic: the algebraic variable can switch discontinuously, so the discrete 's need not converge pointwise. Section 7 of the paper answers this for a semi-implicit Euler scheme applied to the initial-value problem, and the answer is also an existence proof for the DVI.
Fix and write . Let be a nonempty closed convex set, let , , and . For , is the set of with for all . The initial-value DVI (6.2) is
The standing assumptions are (A): , and are Lipschitz continuous on (for the metric ), and (B): .
A weak solution is a pair with , integrable on with for almost every , the integral equation for , and the integral form of the VI,
The time-stepping scheme (7.2) uses a step , grid points , a parameter , and :
for . The iterates are turned into functions of time: is the continuous piecewise linear interpolant of the , and is the piecewise constant interpolant equal to on .
Suppose the iterates satisfy the uniform bounds (7.5),
for all small . Then along some ,
If moreover (a) with Lipschitz and (7.6), or (b) with positive semidefinite, then every such limit pair is a weak solution of (6.2).
The proof decomposes into the paper's own steps: Lemma 7.1 (the implicit Euler step is uniquely solvable, with the bounds (7.4)); the uniform step bound , which makes equicontinuous; the fact that a weak limit of -valued functions is -valued almost everywhere; the integral VI (7.7) under (a); the integral equation (7.8); and the weak lower semicontinuity (7.9) of for positive semidefinite , which handles (b).
Lemma 7.2 (a discrete Gronwall bound giving (7.5) from one-step growth conditions), Lemma 7.3 ((7.5) from linear growth of the VI solutions) and Proposition 7.1 (existence of the iterates for small ) are included as further targets: together with Theorem 7.1 they reduce the hypotheses on the iterates to conditions on .
Theorem 7.1 is simultaneously a convergence theorem for a practical numerical method and an existence theorem: any scheme with bounded iterates produces, in the limit, a weak solution of the DVI. Combined with Proposition 7.1 and Lemma 7.3 it yields existence for DVIs whose VI part has linearly growing solution sets, including linear complementarity systems with positive semidefinite , without the upper-semicontinuity machinery of differential inclusions. Case (b) covers monotone linear complementarity systems, the class arising in passive electrical networks and frictionless contact.
The results are proved in the paper. None of them is machine-checked. A formalization would produce a reusable Lean account of Euler polygons, equicontinuity estimates for discrete schemes, and weak limits of constrained sequences, all of which recur in the numerical analysis of nonsmooth dynamical systems.
The obvious argument would pass to the limit in each step of the scheme pointwise. This fails because has no pointwise or strong limit in general: only weak compactness is available. The nonlinear term does not commute with weak limits, so the variational inequality cannot be passed to the limit directly. Each of the two cases supplies the missing compactness or convexity: in (a) the bound (7.6) makes converge uniformly, and in (b) positive semidefiniteness makes the quadratic term weakly lower semicontinuous. Membership also does not follow from pointwise reasoning and needs convexity of .
Vectors are EuclideanSpace ℝ (Fin k), inner products are ⟪u, v⟫_ℝ, and matrices are continuous linear maps with the operator norm. is the published definition SolodovSvaiterVI.Alg21.viSol Φ K. Positive semidefinite matrices are not assumed symmetric.
Step sizes are with an integer , so that the grid ends exactly at . "For all " becomes "for all ", and "" becomes a strictly increasing sequence of 's. The iterates are a family indexed by and are hypotheses of the goal; their existence is the separate Proposition 7.1. Weak convergence in is tested against every function, and the uniform convergence of is on all of . Condition (7.6) is imposed for , because the paper's convention makes vacuous.
A weak solution carries integrability of both integrands as explicit conditions. Without them a non-integrable pair would satisfy the integral conditions vacuously, since a Lean integral of a non-integrable function is zero. The following readings are also excluded: convergence of the scheme only at grid points; a scheme in which solves the VI at instead of ; and a conclusion about one particular subsequence instead of every subsequence along which both limits exist.
A complete development needs: compactness in (Arzelà–Ascoli), weak sequential compactness of bounded sets in , Mazur's lemma on convex combinations, and estimates for piecewise linear and piecewise constant interpolants. The last two items are reusable for other time-stepping schemes. Proofs of any milestone, and of auxiliary interpolation lemmas, are welcome.
Out of scope: the weaker Carathéodory assumption (A′), the implicit scheme (7.3), the cited fixed-point theorems 7.2–7.3, and Theorem 7.4 (which combines Theorem 7.1 with the existence results of §6).
A differential variational inequality (DVI) couples an ordinary differential equation for a state with a finite-dimensional variational inequality that the algebraic variable must solve at every instant. The class contains complementarity systems from contact mechanics and electrical circuits with diodes, linear complementarity systems from control theory, differential Nash games, and the first-order optimality conditions of optimal control problems with inequality constraints. J.-S. Pang and D. E. Stewart introduced the unified framework in Differential variational inequalities, Math. Program. 113 (2008) (author's version, hal-01366027), and Section 6 of that paper settles the first question any such model raises: when does the initial-value problem have a solution on a whole prescribed time interval?
Before this work, existence results for these systems were tied to special structure: linear complementarity systems with "minimal" and "passive" data, or a given initial condition compatible with the complementarity kernel. Theorem 6.1 gives existence for every initial state under five separate conditions on the variational inequality, each describing a different class of DVIs.
Fix and write . For a set and a map , the variational inequality asks for with for all ; its solution set is . The initial-value DVI studied here is
with nonempty, closed and convex, , , and . Two standing assumptions hold throughout: (A) , , are Lipschitz continuous on ; (B) is bounded on in operator norm.
A pair is a weak solution (in the sense of Carathéodory) on if ; is integrable on with almost everywhere; for , with an integrable integrand; and for every continuous ,
with an integrable integrand. The existence proof passes through the differential inclusion with the set-valued right-hand side
Further objects: the recession cone ; the dual cone ; the VI kernel , the solution set of ; an R₀ pair , one with ; a psd-plus matrix , one with for all and ; and the linear growth property
Under (A) and (B), if any one of the following holds, then (6.2) has a weak solution on for every :
Theorem 6.1 is the existence result behind the rest of the paper: Sections 7 and 8 prove that time-stepping schemes converge to weak solutions of (6.2), and those results are informative only for problems that have solutions. Condition (d) gives existence for every initial state of linear complementarity systems , with , where earlier results required passivity or a compatible initial state. Propositions 6.2–6.5 are results on static variational inequalities in their own right: the linear growth of solution sets in the data had not been a focus of VI theory.
The result is proved in the paper, modulo two cited theorems (Deimling's existence theorem for convex-valued differential inclusions and Filippov's measurable selection lemma). None of it is formalized. A Lean development would supply set-valued upper semicontinuity, Carathéodory solutions of differential inclusions, and existence and linear growth theory for VIs on closed convex and polyhedral sets: material with uses well beyond this paper.
The obvious route, solving the VI for as a function of and substituting into the ODE, fails: the solution map is in general set-valued and discontinuous, so the resulting right-hand side is neither single-valued nor continuous, and classical ODE existence does not apply. The detour through the differential inclusion (6.4) requires convex values, which hold when is monotone but must be proved separately in case (e), where is not monotone. It also requires linear growth (6.5), which for unbounded is a genuine statement about the asymptotics of VI solutions and needs a different argument under each of the five conditions: coercivity, a recession-cone condition, the VI kernel, or a fixed-point argument on polyhedra. Finally, Deimling's theorem and Filippov's lemma are substantial results of set-valued analysis that are not in Mathlib.
Points of are EuclideanSpace ℝ (Fin k); matrices are continuous linear maps, is the operator norm and the adjoint. Data on are curried functions on of which only the values on matter, and Lipschitz continuity on uses the metric . is the published definition SolodovSvaiterVI.Alg21.viSol Φ K. Positive semidefinite matrices are not assumed symmetric. "Monotone" in (a) and Proposition 6.2 means monotone on . The coercivity (6.6) is written in the equivalent form " for with ". Upper semicontinuity is the open-neighbourhood form relative to . In Proposition 6.4 (b) the Lipschitz property is stated on the dual cone , where the paper's proof establishes it (the statement prints ). Nonemptiness of , the paper's standing assumption on variational inequalities, is a hypothesis throughout.
The weak-solution definitions carry explicit integrability conditions on the integrands of the integral equation and of (2.4), and (2.4) is required for every continuous with values in . A definition without those integrability conditions (a Lean integral of a non-integrable function is zero), a variational condition tested only on constant , or (A)–(B) replaced by global boundedness of and would make the goal a different and weaker statement; none of these is used.
Contributions welcome at every level: proofs of the milestones, a general theory of upper semicontinuous set-valued maps and Carathéodory solutions of differential inclusions, and existence results for variational inequalities via recession cones and degree theory.
A spectral sparsifier of a weighted graph is a graph on the same vertices, with few edges, whose Laplacian quadratic form is within a factor of that of on every vector. Spielman and Teng introduced the notion in their work on nearly-linear-time solvers for symmetric diagonally dominant linear systems (Spielman–Teng 2004; arXiv:0808.4134): a sparsifier can replace a dense graph as a preconditioner, and it preserves every cut value up to the same factor, strengthening the cut sparsifiers of Benczúr and Karger (BK96).
Their construction first handles graphs whose edge weights lie in a bounded range. Arbitrary weights need an extra idea, which §10.2 of Spectral Sparsification of Graphs formalizes as Lemma 10.2 (Pullback): when a graph's vertex classes are held together by edges far heavier than those between them, one may contract each class to a single vertex, sparsify the much smaller contracted graph, and pull the result back to the original vertices. The approximation factor degrades only by , where measures the gap between heavy and light weights. The same contraction idea goes back to Benczúr and Karger's treatment of weighted cut sparsifiers.
A weighted graph on a finite set , , is a symmetric function with ; its edges are the pairs with . Its Laplacian quadratic form is
A graph is a -approximation of if for all . We write when for all , for the graph whose weights are the sums, and for the single edge of weight .
Let be a partition of with map . Write for the edges between different parts, , and , . The contraction of under is the graph on with weight for and no self-loops. Given a graph on , a graph on is a pullback of under if every edge of joins different parts, is the contraction of , and for every edge of exactly one edge of has , . A pullback thus has as many edges as .
Let , , let be a -approximation of the contraction of under , and let be a pullback of . Assume (1) each is connected by edges in , (2) every edge in has weight at least , (3) every edge in has weight . Then
Choose representatives ; let , be the copies of , on , and , .
The constants are the paper's; the goal is the lemma as printed.
Lemma 10.2 is the reduction from arbitrary weights to bounded weights in Spielman and Teng's sparsification algorithm (Sparsify, §10.2): the edges of each weight scale are sparsified on a graph in which all much heavier edges have been contracted, so the number of vertices handled at each scale stays small, and the total size of the sparsifier is only a logarithmic factor larger than in the bounded-weight case. The statement itself is purely about quadratic forms and holds for any approximation of the contraction, however it was obtained; it applies equally to later sparsification methods such as sampling by effective resistances.
The lemma is proved in the paper. As far as is known, none of these statements has a machine-checked proof: Mathlib has the Laplacian of a simple graph (SimpleGraph.lapMatrix) but no weighted Laplacian order, no contraction of weighted graphs and no notion of spectral approximation. The mission produces those objects and a complete formal proof of the lemma and its intermediate claims.
The individual steps are elementary, but the proof combines three kinds of bookkeeping. Lemma 10.3 is a Cauchy–Schwarz inequality along a path, which must be applied to a path assembled from two walks inside parts and one edge between representatives; obtaining a simple path of length at most from the connectivity hypothesis requires shortening walks. The summed bounds require recognising that the copies of the unit edges between representatives add up exactly to , which uses hypothesis 3 and the fact that contraction counts each edge between two parts once. Claim (c) needs, in addition, that the total weight of is at most times that of and that each pullback edge has the weight of its image edge. The constants are tight in one place: requires both and .
A natural shortcut, comparing with directly, fails: and have different edges, and their Laplacians are only comparable through the heavy intra-part edges.
A weighted graph is a function w : V → V → ℝ on a Fintype V with IsWGraph w (symmetric, nonnegative, zero diagonal); sums and scalar multiples are pointwise. lapForm w x is , IsApprox σ w̃ w keeps both inequalities of the definition, and GraphLE is . The partition is a surjective map π : V → Fin k (nonempty parts). , are crossPart w π, intraPart w π; hypothesis 1 is reachability, between any two vertices of the same part, in the simple graph of -edges. Representatives are any r : Fin k → V with π (r i) = i, and liftAlong r z places a graph on Fin k on them; the goal does not mention representatives. is Fintype.card V.
Two hypotheses implicit in the paper are explicit: (with the lemma is false), and that every edge of a pullback joins two different parts (contraction cannot see an edge inside a part, so without this a pullback could carry an arbitrary heavy edge and the lemma would be false). In Lemma 10.3 the edge weights are positive and the path has at least one edge.
A trivializing formalization is ruled out: dropping hypothesis 2 or 3, allowing or intra-part pullback edges, or letting the pullback forget the uniqueness of the edge over each makes the statement false or weaker, and stating only one of the two inequalities of -approximation is a different theorem. Every statement here keeps both.
The algorithm Sparsify and its analysis (Lemma 10.4, Theorem 10.5, Proposition 10.6, Theorem 10.7, Lemmas 10.8–10.9) and all running-time claims are out of scope. The weighted Laplacian form, its additivity and nonnegativity, and the transport of a quadratic form along an injective vertex map are reusable beyond this mission; contributions of such general lemmas, and a proof of Lemma 10.3 by Cauchy–Schwarz, are welcome.
A manufacturer must commit to production before a retailer knows how much it will buy. In practice the retailer sends a forecast first, and the manufacturer plans against it. When the forecast binds neither party, the retailer has no reason to report it honestly, and the manufacturer has no reason to plan for the market rather than for its own margin. Purchasing managers have described this to Tsay directly, and Lee, Padmanabhan and Whang (1997) document such "phantom ordering" in several case studies.
A. A. Tsay, The Quantity Flexibility Contract and Supplier-Customer Incentives (Management Science, 1999), models the situation as a two-stage newsvendor game with a demand-information update between production and purchase. Its first result, Proposition 1, is the benchmark the rest of the paper builds on. Even when both parties share the same beliefs about demand, a linear transfer price alone leaves the manufacturer underproducing relative to a central planner, and the supply chain loses expected profit, for every transfer price. That inefficiency motivates the quantity flexibility (QF) contract studied in the remainder of the paper and in the companion mission of this series.
Costs. The retail price is and the unit transfer price paid by the retailer to the manufacturer (the EM) is . The unit production cost is , the unit salvage value is (the same for either party), and the unit goodwill loss on unmet demand is . The paper's standing assumptions (§3.1, p. 1344) are
Three critical fractiles recur:
Demand (§3.3). Market demand is . The signal has distribution function , which is differentiable and strictly increasing, and finite variance. The error is independent of . is the distribution function of , is the standard normal distribution function, and .
Timing (§3.2). The EM produces knowing only the prior. Then is observed and the retailer buys . Then is realized, and both parties salvage their surplus. Given , the retailer's expected profit from purchase is
Without commitment the retailer buys . The EM's expected profit is
and the retailer's is . A central planner producing before the signal earns
Let maximize and maximize . Then, for every transfer price admitted by the standing assumptions,
and the retailer's optimal purchase under is . 3. §5.2, p. 1347. The EM's optimal production exists and is unique:
Proposition 1 shows that sharing demand information does not remove inefficiency. Under common beliefs and with no commitment, no linear transfer price makes the decentralized chain efficient. Adjusting moves profit between the parties but cannot recover the planner's expected profit. This is the reason the paper studies richer contracts, and the efficiency result for the QF contract (the paper's Proposition 6) is measured against the benchmark defined here.
The paper prints no proofs ("All proofs are omitted due to space limitations", p. 1341). A machine-checked development therefore supplies arguments the published record does not contain. It also exhibits the exact hypotheses the result needs. In particular it covers the degenerate case , where the signal is perfect. No part of this mission has a prior formal proof. Newsvendor critical-fractile results exist on Prove2Me for single-decision models, but without the production stage and information update used here.
The EM and the planner solve newsvendor problems against different demand laws. The EM faces the retailer's purchase , while the planner faces . Their fractiles are and . The obvious comparison, , settles the case only. For the two quantities are inverse distribution functions of different random variables. may be negative, and the planner's distribution is a convolution. A comparison of fractiles alone therefore does not order and . The strict profit gap also needs more than optimality of : it requires comparing the decentralized system profit at with the planner's profit at the same production, and then using uniqueness of the planner's optimum.
The analytic infrastructure is also substantial. It includes differentiating expectations of piecewise-linear functions under a Gaussian law and under a general prior, continuity and strict monotonicity of a convolution's distribution function, and existence of a root of .
All objects live in the namespace TsayQF.NoCommit, in one definitions file Model.
Data with fields and the standing assumptions (i)–(iii) as fields. "For any " is quantification over all Data. No sign is imposed on .ν on ℝ; is cdf ν. "Differentiable and invertible" is Differentiable ℝ (cdf ν) together with StrictMono (cdf ν), and "mean and variance" is MemLp id 2 ν.v : ℝ≥0, so and v = 0 is allowed. The law of is the pushforward of ν.prod (gaussianReal 0 v) under addition, and given demand has law gaussianReal μ v.z with hypothesis cdf (gaussianReal 0 1) z = kR D. The milestones state existence of a solution of each fractile equation and characterize the maximizers by it.IsMaxOn over Set.univ for productions and over Set.Iic Q for the purchase. Productions range over ; the paper's presumption that and are almost certainly nonnegative is not imposed, because no result here needs it.The goal must not be weakened to non-strict inequalities, and the EM's demand must remain the retailer's purchase , not market demand. Either change trivializes the result or changes it. Reusable pieces are the newsvendor critical-fractile characterization for a general continuous strictly increasing distribution, and monotonicity and continuity of the distribution function of a sum of independent variables with one Gaussian summand. Proofs of the milestones as standalone lemmas are welcome.
Minimizing the sum of the largest eigenvalues of a symmetric matrix that depends affinely on parameters is a basic problem of eigenvalue optimization (survey: A. S. Lewis and M. L. Overton, Eigenvalue optimization, Acta Numerica 5, 1996, doi:10.1017/S0962492900002646). Its objective is convex, and is differentiable at exactly when ; at optimal solutions the eigenvalues tend to coalesce, which makes the problem a model problem of nonsmooth optimization. G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues (Math. Oper. Res. 23(2), 1998, doi:10.1287/moor.23.2.339), gives a quantitative explanation in terms of the number of free parameters.
The paper also proves a bound on the rank of extreme points of semidefinite programs, now often called the Pataki bound (also obtained by Barvinok, 1995): an extreme point of satisfies . This bound is used throughout low-rank semidefinite optimization, for instance in the Burer–Monteiro approach.
is the space of real symmetric matrices, means is symmetric positive semidefinite, and . For , are its eigenvalues and, for ,
The multiplicity is the largest with for some .
A face of a convex set is a convex such that , , imply ; an extreme point is a one-point face; is the maximal number of affinely independent points of , minus one. Write and
Let be linearly independent, , and assume and (the standing assumptions of §4). The affine eigenvalue problem is
and denotes its set of optimal solutions, a closed convex set. For the semidefinite program
has optimal value ; is its set of optimal solutions .
If is an extreme point of and , then
The theorem says that once the number of free parameters exceeds , the -th and -st eigenvalues necessarily coincide at extreme optimal solutions, so is typically nonsmooth at its minimizers, and it bounds from below the dimension of the subdifferential , which is . The intermediate rank bounds of §2 are reusable on their own for any semidefinite program.
The results are proved in the paper. As far as is known, none of them (neither the Pataki rank bound, nor the semidefinite characterization of , nor Theorem 4.3) has a machine-checked proof. Formalizing them produces a library of faces and dimensions of spectrahedra, the SDP representation of the Ky Fan sum , and the multiplicity bound itself.
Extremality of in is a statement in the parameter space and gives no direct information on the spectrum of : perturbation arguments on the eigenvalues alone break down precisely at the coalesced eigenvalues the theorem is about, where is not differentiable. The quantitative bound (4.30) also needs more than the optimal value : it depends on the whole optimal set , on the dimension of faces of spectrahedra, and on an exact count relating the ranks of the optimal to the multiplicity of . None of these (faces and dimension of spectrahedra, the semidefinite representation of , eigenvalue run lengths) is in Mathlib.
Matrices are Matrix (Fin n) (Fin n) ℝ; is the published BurerMonteiro.RankIncrease.frob, the primal and dual feasible sets are the published IsPrimalFeasible/IsDualFeasible, and is the published ProjLikeRetr.Spectral.eig B ⟨i-1,_⟩ (Mathlib's nonincreasing eigenvalues, 0-based). Every matrix whose eigenvalues are taken is assumed symmetric. Faces, extreme points and dimension are defined as on p. 341; dimension is integer valued with . All rank bounds are compared in . is the argmin set and is the set of feasible points no worse than every feasible point; no infimum is used. Optimal values are stated as least elements of the set of feasible objective values.
Hypotheses added relative to the page, each disclosed in its item: in the statements of §3, which mention ; (p. 340) in every §4 statement; one common matrix order in Theorem 2.2; and in the rank identity of p. 348, which is false as printed when (, , gives ) and is used in the paper only in the equal case. The linear independence of is kept with included, as on p. 348.
Trivializing formalizations are ruled out: is not defined through a possibly junk infimum, a face must be convex and contained in the set, the dimension is not a junk , is the run length of equal eigenvalues and not a constant or an index, and the eigenvalues are only ever taken of symmetric matrices.
A complete development needs: the rank–dimension bound for faces of spectrahedra (reusable for any SDP), the semidefinite characterization of with its optimal set, and convexity facts on . Proofs of any milestone, alternative proofs of the rank bounds, and the general smooth case of §5 are welcome.
In the job shop problem, jobs are sequences of operations, each to be processed on a given machine for a given time, and the goal is a schedule of minimum makespan (the time at which the last job finishes). Two numbers bound the optimum from below: the longest job and the most loaded machine. Their maximum is written . The best approximation algorithms for job shops have a performance guarantee polylogarithmic in (Shmoys, Stein and Wein 1994; Goldberg, Paterson, Srinivasan and Sweedyk 2001). Whether flow shops and job shops admit a constant-factor approximation was Open Problem 7 of Schuurman and Woeginger (1999).
Mastrolilli and Svensson (J. ACM 58(5), 2011) answered it negatively for the generalized flow shop. Their Theorem 1.2 states that for all sufficiently large constants it is NP-hard to distinguish generalized flow shop instances with a schedule of makespan from instances in which no schedule finishes more than half of the jobs within . The proof is a gap-preserving reduction from graph colouring. This mission formalizes the combinatorial heart of that reduction.
Timeline. Shmoys, Stein and Wein (1994) gave an -approximation for job shops, improved by a factor by Goldberg et al. (2001). Williamson et al. (1997) proved that approximating flow shops with unit operations within a ratio better than is NP-hard. Feige and Scheideler (2002) gave acyclic job shop instances with optimum and asked whether flow shops admit a much better upper bound than . Khot (2001) proved the colouring hardness this reduction starts from. Mastrolilli and Svensson (FOCS 2008; J. ACM 2011) proved Theorem 1.2 and its job shop variants.
A generalized flow shop (flow shop with jumps) is a job shop with a fixed linear order on the machines in which every job visits its machines in increasing order but may skip machines. Operations may have length . A zero-length operation still occupies its machine for an instant, so it cannot be processed strictly inside another operation on the same machine.
Let be a simple graph with vertices whose vertices are partitioned into independent sets . Vertex has frequency . For an integer write . The instance has groups of machines, each with one machine per vertex. The machines are ordered by group first and, within a group, by decreasing frequency. A vertex of frequency owns groups of identical jobs. The job has a long-operation of length on each of the machines , where . It also has a short-operation of length on every machine of every neighbour of , in every group. A long-operation is good if the next long-operation of the same job starts at most time units after it ends. is the set of first halves of the good long-operations on , and is the time they cover.
is the chromatic number of and the size of its largest independent set.
For every graph with a proper colouring into classes and every integer , with :
Remark 3.6 (lengths, loads, operation count), Claim 3.8 (an independent set's jobs fit in ), Lemma 3.7 (completeness), Lemma 3.10 (most long-operations are good), Lemma 3.11 (adjacent vertices have disjoint -intervals), Lemma 3.12 (one group carries of first-half time), and Lemma 3.9 (soundness: an independent set of size ).
The result. Together with Khot's colouring hardness, the gap shows that no polynomial-time algorithm approximates the generalized flow shop within any constant factor unless P = NP, and rules out an -approximation under a stronger complexity assumption (Theorem 1.3). It also shows that on the no-instances of the reduction every schedule has makespan greater than , far above the trivial lower bound . Because soundness bounds the number of jobs finished early, the same reduction also gives hardness for the sum of completion times (footnote 2).
Formalizing it. The paper proves every statement of this mission; none is open. As far as the catalog shows, none has a machine-checked proof. The soundness argument rests on a timing property of zero-length operations: a job of higher frequency must wait for a long-operation of an adjacent lower-frequency job. Such properties are easy to state loosely and easy to get wrong, so a verified proof would be useful. A formal proof would also make explicit the thresholds the paper leaves as "sufficiently large ".
Completeness is constructive and routine once the job and machine indexing is under control. The difficulty is soundness. One might argue directly that jobs of adjacent vertices never overlap in time, but that is false: a schedule may run them in parallel at the cost of delays. The argument controls it only on average. It throws away the jobs that finish late and the long-operations followed by a long delay. It shows that the first halves of the remaining long-operations of adjacent vertices are disjoint in each machine group. Then it finds a moment covered by many such first halves. Each step needs a precise count: of good operations per job, of covered time per group, and of overlap multiplicity at a point. The degenerate conventions (empty colour classes, , the last long-operation of a job) have to be handled throughout.
The instance is the published JobShopLTAS.Core.Instance (machines and jobs Fin (r^{2d} n), real nonnegative processing times, disjunctive machine constraint under which a zero-length operation cannot sit strictly inside another operation on its machine), with its IsFeasibleSchedule and makespan. The graph has vertex set Fin n and the partition into independent sets is a Mathlib proper colouring G.Coloring (Fin d). Frequencies are 1-based, as are group indices. Within a group the paper leaves machines of equal frequency unordered; they are ordered by vertex index. Every job's operation list is its machine set sorted by the global order. is the Lebesgue measure of the union of the intervals.
Explicit readings of the paper's wording:
Not formalized: "NP-hard", "for all sufficiently large ", "in time polynomial in and ", Khot's Theorem 1.7, the choice , , and the randomized Lemma 3.1 behind Theorem 1.3.
A model in which zero-length operations occupy no machine time would make soundness false, and stating soundness only for schedules of an independent set's jobs would make it vacuous. The goal is about every feasible schedule of , built from , in the published model, where zero-length operations do conflict.
A complete development needs counting lemmas for the indexing of jobs and machines, sorting facts for the operation lists, and a measure-theoretic averaging argument (a point covered by many intervals). The averaging argument and the good-operation counting are shared with the flow shop gap of Theorem 1.1 and reusable there. Proofs of any milestone, and sorry-free sanity checks on small instances, are welcome.
Large service systems (call centers, hospital wards, cloud server pools) run with many servers, and for many of them no exact formula describes how the number of busy servers moves over time. Heavy-traffic limits replace such a system by a diffusion process that is easier to analyze. The many-server regime, in which the number of servers and the arrival rate grow together, goes back to Halfin and Whitt (1981) and is the basis of square-root staffing rules in call-center practice.
The simplest many-server model is the queue. Its stationary number in system is Poisson with mean , so the centered and -scaled stationary count is asymptotically normal when . The question here is about the whole process: does the scaled number in system converge, as a random path, to a diffusion? The classical answer, the Ornstein–Uhlenbeck limit, was first established by Iglehart (1965) with Stone's theorem for birth-and-death processes, and was revisited by strong approximation (Mandelbaum, Massey and Reiman 1998) and, for general service times, by Krichagina and Puhalskii (1997).
Pang, Talreja and Whitt (2007) is a tutorial survey that proves this limit, and its finite-waiting-room extension, with martingale methods. The authors present the argument as a template for non-Markovian and network models (Reed 2009; Dai and Tezcan; Gurvich and Whitt). This mission formalizes the result and the steps of the paper's proof.
Fix a service rate . For each , the -th system has arrival rate . Let and be independent Poisson processes of rate , and let be a random initial number of customers, independent of and . The number in system is the -valued process with right-continuous paths having left limits that satisfies, almost surely,
The departure term is a random time change: each of the customers in service completes service at rate . The diffusion-scaled process is , the paper's (3). The space consists of paths on that are right-continuous with left limits, and denotes convergence in distribution.
The limit is the Ornstein–Uhlenbeck (OU) process , driven by a standard Brownian motion , with independent of :
The proof also uses the scaled martingales and , the fluid processes and , and stochastic boundedness. A sequence of real random variables is stochastically bounded if it is tight, and a sequence of processes is stochastically bounded in if is, for every .
If in , with an arbitrary limit law , then
where is the OU process (5) with . The goal fixes no initial distribution and assumes no moment condition on .
Theorem 1.1 describes the transient behavior of a large infinite-server system, not only its stationary law: fluctuations of order around the offered load form a Gaussian Markov process that relaxes at rate . It is the reference case for the Halfin–Whitt regime, whose finite-server version, Theorem 1.2 of the same paper (the queue), is the subject of the companion mission. The milestones are general tools reused well beyond queueing: Gronwall's inequality, the Lipschitz integral map, the Poisson FCLT, stochastic boundedness via Lenglart's inequality, and the fluid limit from stochastic boundedness.
The theorem is proved and classical; no machine-checked proof of it, or of the milestones below, is known. No formal library currently has the Poisson functional central limit theorem in , compensators of counting processes, or random time changes of martingales. Formalizing the paper's proof would produce these, plus a template for the martingale method of heavy-traffic analysis. Alternative proofs, such as the paper's §4.3 route without martingales, are equally welcome as solutions.
Equation (12) is a fixed-point equation: appears inside the argument of . The integral map of Theorem 4.1 is continuous, so the obvious argument is to apply the continuous-mapping theorem to the martingale representation. That reduces the goal to the joint convergence of . But is a Poisson martingale evaluated at the random time , and its limit is identified only after the fluid limit is known. The fluid limit is itself a statement about the whole sequence , and it needs a separate argument, either Gronwall at fluid scale or stochastic boundedness. Lemma 3.2 requires optional stopping at the continuum of stopping times , and the moment conditions (22) must be checked through the crude bound. Removing needs a truncation of the initial conditions (§6.3).
CouplingConverges): a Skorokhod representation with almost-sure uniform convergence on compact intervals. Convergence to a deterministic path is uniform convergence on compacts in probability (UocInProb). is stated with bounded continuous test functions.Type.A formalization that fixes , assumes converges almost surely, adds to the goal, or replaces convergence in by convergence of finite-dimensional distributions proves a weaker theorem and does not close the goal.
Contributions are welcome at every level. The Poisson FCLT, Lenglart's inequality and the composition map are reusable library results, independent of queueing.
Large service systems such as call centers, hospital wards and cloud server pools have many parallel servers, finite buffers and customers who leave when they wait too long. Their performance is usually analysed through heavy-traffic diffusion limits: the number of customers in the system, centred and rescaled, converges as the system grows to a diffusion process whose law is computable. The quality-and-efficiency-driven (QED) regime of Halfin and Whitt (Oper. Res. 29, 1981) is the scaling in which the number of servers and the arrival rate grow together so that the probability of delay stays strictly between and . Garnett, Mandelbaum and Reiman (M&SOM 4, 2002) proved the QED limit for the Erlang-A model with unlimited waiting room. Whitt (Math. Oper. Res. 30, 2005) added finite waiting rooms of size of order , which produce a reflecting upper barrier in the limit.
Pang, Talreja and Whitt (Probab. Surveys 4, 2007) give a self-contained martingale proof of these limits. Theorem 1.2 of that paper, the target of this mission, covers the model with finite waiting room and abandonment. It contains the Erlang-B (loss) model () and finite-buffer Erlang-C models () as special cases.
Fix a service rate , an abandonment rate , a constant and a barrier . For , model is an queue: servers, a waiting room of places, Poisson arrivals of rate , exponential services of rate , first-come first-served service, and an exponential patience of rate for each waiting customer. An arrival that finds all places occupied is blocked and lost.
The number in system is constructed from independent rate-1 Poisson processes , , and an independent initial value by
where counts blocked arrivals. The QED scaling is
and the scaled process is .
The limit is a reflected diffusion: a pair of processes with right-continuous paths with left limits, , nondecreasing and nonnegative, a standard Brownian motion independent of , and
The regulator increases only when sits at .
If in , then in , where solves the reflected equation above with , and every solution with initial law has the same law:
The goal fixes no rate of convergence and no stationary quantity; it asserts the process limit and its characterization by (9)–(10).
The theorem supplies the diffusion approximation behind square-root staffing rules for systems with finite buffers: it says that buffers of order are visible in the limit as a barrier at , and that the limit for (Erlang-B with or without abandonment) is a reflected Ornstein–Uhlenbeck-type process. Stationary blocking and delay probabilities of the limit then approximate those of the large finite system.
The result is proved in the literature (Whitt 2005; Pang, Talreja and Whitt 2007, whose proof of Theorem 1.2 is a sketch built on §7.1). It is not formalized anywhere. A formal proof would supply a checked martingale representation for a birth–death queue with blocking, a checked reflection map with state-dependent drift, and the continuous-mapping step through it. The unlimited-waiting-room case is posed separately on the platform as the Erlang-A limit of Garnett, Mandelbaum and Reiman and is not part of this mission.
The obvious route is the one used for the Erlang-A model: write as a continuous function of the scaled Poisson noise and apply the continuous-mapping theorem. With a finite waiting room this fails as stated, because the blocking process is not a function of the noise alone. It depends on the path of through the times the system is full. The proof must instead identify as the image of the noise under a reflection map with a drift inside it, prove that this map is well defined and continuous, and control the martingale terms through random time changes whose limits are deterministic. The barrier in model is , not , so the continuous-mapping step has to handle a moving barrier as well.
BellWilliams2001.ThresholdPolicy.IsCadlag. Brownian motion is ErlangA.Diffusion.IsStandardBM, indexed by ; martingales are Mathlib Martingales indexed by .ManyServerQED.Scheduling.IsPoissonProcess. is independent of the primitives and for all . Blocked arrivals are counted with the left limit , correcting (114) as printed. and are allowed.BellWilliams2001.ThresholdPolicy.CouplingConverges (Skorohod coupling with almost sure uniform convergence on compacts), equivalent to weak convergence for a continuous limit. Uniform distances use supDist on .ErlangA.Diffusion.drift; is independent of ; and are adapted to the filtration of and ; condition (10) is "the Lebesgue–Stieltjes measure of , extended by to negative times, gives zero mass to ". Uniqueness is uniqueness in law of . The limit space lives in Type.Contributions welcome: Stieltjes-integral and counting-process lemmas for , a reflection map with Lipschitz drift on , the Poisson functional central limit theorem, and martingale facts for randomly time-changed Poisson processes. The last three are reusable well beyond this mission.
The Kurdyka–Łojasiewicz (KL) inequality is the analytic engine behind most global convergence proofs for descent methods on nonconvex problems: proximal point and proximal gradient schemes, alternating minimization, ADMM variants and subgradient flows all reach a critical point with finite trajectory length once the objective satisfies a KL inequality. Its origin is Łojasiewicz's gradient inequality for real-analytic functions ([Łojasiewicz, 1963]); Kurdyka extended it to differentiable functions definable in an o-minimal structure, with a reparametrization ψ of the values, on bounded sets (Kurdyka, Ann. Inst. Fourier 48 (1998)).
Optimization objectives are rarely smooth or finite everywhere: indicator functions of constraint sets, ℓ₁ penalties, rank functions and maxima take the value +∞ or have kinks. Bolte, Daniilidis, Lewis and Shiota (SIAM J. Optim. 18(2) (2007), 556–572) proved that every lower semicontinuous function definable in an o-minimal structure satisfies a KL inequality for Clarke subgradients, globally in space. This mission formalizes that result (Theorem 14) and the chain of statements in §4 of the paper on which its proof rests.
Timeline. Łojasiewicz (1963): gradient inequality for real-analytic functions near a critical point. Kurdyka (1998): the inequality ‖∇(ψ∘f)‖ ≥ 1 for C¹ definable functions on bounded sets. Bolte, Daniilidis and Lewis (SIAM J. Optim. 17(4) (2007)): nonsmooth Łojasiewicz inequality for lower semicontinuous subanalytic functions with the limiting subdifferential. Bolte, Daniilidis, Lewis and Shiota (2007): this paper, for definable functions, Clarke subgradients, and unbounded sets.
Write ℝⁿ for Euclidean space with norm ‖·‖ and inner product ⟨·,·⟩, and let f : ℝⁿ → ℝ ∪ {+∞} be lower semicontinuous, with domain dom f = {x : f(x) < +∞} and graph Graph f = {(x, f(x)) : x ∈ dom f} ⊆ ℝⁿ⁺¹. Π : ℝⁿ⁺¹ → ℝⁿ forgets the last coordinate.
Subdifferentials. A vector x* is a Fréchet subgradient of f at x ∈ dom f if liminf_{y→x, y≠x} [f(y) − f(x) − ⟨x*, y − x⟩]/‖y − x‖ ≥ 0. The limiting subdifferential ∂f(x) collects the limits of Fréchet subgradients x_k at points x_k → x with f(x_k) → f(x); the singular subdifferential ∂^∞f(x) collects the limits of t_k x_k with t_k ↘ 0⁺. The Clarke subdifferential is
with the closed convex hull. It may be empty even on dom f, for example for −‖x‖^{1/2} at 0.
O-minimal structures. An o-minimal structure 𝒪 on (ℝ, +, ·) is a sequence of Boolean algebras 𝒪ₙ of subsets of ℝⁿ (the definable sets) that is stable under A ↦ A × ℝ, A ↦ ℝ × A and the projection Π, contains every algebraic set {p = 0}, and whose one-dimensional sets are exactly the finite unions of intervals and points. Semialgebraic sets, the globally subanalytic sets and the sets definable with the exponential each form such a structure. A function is definable if its graph is.
Stratifications. A C^p stratification of a set X is a locally finite partition of X into C^p submanifolds (strata) such that a stratum meeting the closure of another lies in its frontier. It is Whitney-(a) if tangent spaces T_{x_k}X_i converging to 𝒯 along x_k → x ∈ X_j satisfy T_xX_j ⊆ 𝒯, and a stratification of a set in ℝⁿ⁺¹ is nonvertical if e_{n+1} is tangent to no stratum. For x in a stratum X_i, ∇_R f(x) is the Riemannian gradient of f restricted to X_i.
For every lower semicontinuous definable f there are ρ > 0, a strictly increasing continuous definable ψ : [0, ρ) → ℝ, C¹ on (0, ρ) with ψ(0) = 0, and a continuous definable χ : ℝ₊ → (0, ρ) such that
Neither ρ, ψ nor χ is fixed: the goal asserts only their existence, so it is independent of any choice of exponent.
Corollary 9 (ii)–(iii) (finitely many Clarke critical and asymptotic critical values) and Corollary 12 (the KL inequality around the zero set) are included as further statements.
The result. Theorem 14 makes the KL property available, with no further verification, for every lower semicontinuous objective built from semialgebraic, globally subanalytic or exp-definable pieces. Global convergence theorems for proximal alternating minimization, proximal gradient methods, PALM and nonconvex ADMM take a KL inequality as hypothesis; definability is how that hypothesis is checked in applications. The inequality is relative to the value 0, holds globally through χ(‖x‖), and controls every Clarke subgradient rather than only the one of least norm. Corollary 9 is a definable, nonsmooth Morse–Sard theorem.
Formalizing it. The theorem has been proved since 2007; it has not been formalized. Lean's Mathlib has no o-minimal geometry: no cell decomposition, monotonicity theorem, definable choice or Whitney stratification. A complete development of this mission would supply the first machine-checked KL inequality for a general class of nonsmooth functions, and the o-minimal infrastructure it needs is reusable for every result in optimization and real algebraic geometry that cites "tame" functions.
The statements are short; the proofs rest on geometry absent from Lean. Lemma 8 is proved in the paper by citation of a stratification theorem for definable maps ([Shiota, Geometry of Subanalytic and Semialgebraic Sets, 1997, II.1.17]). Proposition 10 and Theorem 11 use the monotonicity lemma for definable functions of one variable and definable selection. The natural first idea — apply Kurdyka's inequality on each stratum and take a minimum — fails twice: Kurdyka's inequality is local on bounded sets, and the reparametrizations ψ_i of different strata must be compared near 0, which needs the monotonicity lemma once more. Passing from the strata to Clarke subgradients needs the projection formula of Corollary 9, which in turn depends on nonverticality and the Whitney-(a) condition.
ℝⁿ is EuclideanSpace ℝ (Fin n); ℝ ∪ {+∞} is EReal, with f never equal to ⊥ as a standing hypothesis; ℝⁿ⁺¹ carries the value in the last coordinate. The Fréchet and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff. The Clarke subdifferential uses closedConvexHull. An o-minimal structure is a structure with a family O n of sets of subsets of ℝⁿ satisfying Definition 6 (Boolean algebra as: ∅, complements, binary unions; one-dimensional sets as finite unions of order-connected sets). Definability of ψ, χ and of the strata is part of every conclusion that asserts it. Tangent spaces are spans of Mathlib's tangentConeAt; C^p submanifolds are local graphs; the Riemannian gradient on a set U is a vector g in the tangent space with HasFDerivWithinAt h ⟪g, ·⟫ U x.
Inequality (22) is stated as ψ′(|f(x)|)·‖x*‖ ≥ 1, never as 1/ψ′ ≤ ‖x*‖, so that ψ′ = 0 cannot make it hold through 1/0 = 0. The goal mentions no strata, no auxiliary functions of the proof and no Clarke critical points; a formalization that adds such hypotheses, drops definability of ψ and χ, or restricts to bounded sets is a different theorem.
Welcome contributions: the elementary closure properties of o-minimal structures (definability of sums, compositions, images), the monotonicity theorem for definable functions of one variable, definable choice, cell decomposition and Whitney stratification — all reusable well beyond this mission.
Network revenue management decides, over a finite selling horizon, which products to offer to arriving customers when the products share limited resources: seats on flight legs, hotel room-nights, rental capacity. The exact dynamic program is intractable for realistic networks, so practice relies on heuristics built from a deterministic linear program (DLP), the fluid relaxation that replaces random demand by its mean. Its value is an upper bound on the revenue of every policy, and the quality of a heuristic is measured by its revenue loss against it.
For the fluid-based heuristics, the loss grows with the size of the system: a static policy derived from one DLP solution loses order when capacities and demand rates are both scaled by (Gallego and van Ryzin, 1997; Talluri and van Ryzin, 1998). Re-solving the DLP during the horizon is common practice, but for a long time it was unclear whether re-solving helps asymptotically; Cooper (2002) showed that naive re-solving can even hurt. Jasin and Kumar (Math. Oper. Res. 37(2), 2012, doi:10.1287/moor.1120.0537) proved that a re-solving heuristic with probabilistic allocation control (PAC) has a loss bounded by a constant independent of , in a model that also covers customer choice through random resource consumption. Later work (Bumpensanti and Wang, 2020, arXiv:1802.06192) removed the nondegeneracy assumption with a different re-solving rule.
The horizon is . Customer types arrive as independent Poisson processes of rates . Each of the offers belongs to one type ; iff , and . Presenting offer consumes a random vector of the resources, i.i.d. across presentations, and earns revenue , with ; models a customer who buys nothing. Resource starts with capacity , and bounds every . Write and . The DLP is
Assumption 2.1 requires to be nondegenerate with a unique optimal solution ; Assumption 2.2 requires that every optimum of the LP without capacity constraints violates .
PAC re-solves at times . At it solves with the remaining capacity, obtaining ; until it picks offer for an arriving type- customer with probability and presents it only if the remaining capacity is at least on every resource. In the -th system capacities are and rates ; is the DLP value and the revenue of PAC. Mid-point PAC re-solves at , , with the smallest integer such that : about re-solves.
There is , independent of , such that mid-point PAC satisfies
The goal fixes no constant: it asserts only that the loss is bounded uniformly in .
The result shows that re-solves suffice for a loss that does not grow with the size of the system, against an upper bound that is valid for every policy; so PAC is within a constant of the optimal policy, and the DLP bound, the optimal value and PAC are asymptotically equivalent to order . Theorem 5.3 makes the trade-off between re-solving frequency and loss explicit for any schedule, and Corollary 5.1 guarantees that re-solving in this form never worsens the static bound.
The result is proved on paper. No part of it is formalized: the mission produces a machine-checked model of a Poisson network with random consumption and a re-solving policy, a statement of LP perturbation theory for nondegenerate programs, and compound-Poisson moment bounds, each reusable for other re-solving and fluid-approximation results in revenue management.
The obvious argument compares PAC with its fluid path and bounds the deviation of the remaining capacity by a martingale estimate over the whole horizon. That gives only : deviations late in the horizon cannot be corrected. A constant bound needs re-solving to correct earlier deviations, which in turn needs the re-solved DLP solution to depend linearly and stably on the capacity deviation (the perturbation analysis of App. B) and a hitting-time estimate for when that linear regime fails. The capacity check and the coupling between the re-solved solutions and the random consumption make the process non-Markovian in the obvious state variables.
Types are Fin NT, offers Fin n, resources Fin m. The model is a structure holding , , , the consumption laws (measures on ), and the revenue functions. Standing readings (IsValid): and ; each is a probability measure with almost surely (the page has on p. 317 and on p. 327; the weaker one is used); revenue functions are measurable, vanish at , and are nonnegative and bounded by a common constant (implicit on the page). is a reading fixed by App. A.1.
is a backward recursion over the windows between re-solves. Each window holds a Poisson number of arrivals with i.i.d. types (superposition and marking), and the expected value is computed arrival by arrival with the capacity check on every resource. PAC is quantified over every DLP selector that returns an optimal solution and is measurable in the capacity, since the page leaves ties open after time 0. All constants are chosen after the instance and before , the selector, the schedule, and . Nondegeneracy follows Bertsimas–Tsitsiklis: every basic feasible solution has exactly active constraints.
Disclosed deviations from the page:
A formalization in which PAC does not check capacity, or stops checking after a hitting time, earns exactly and would make the goal trivial; the model here applies the check at every arrival. A constant chosen after would also be trivial, since the loss is at most times the revenue bound.
The source is the published Math. Oper. Res. version; printed page = PDF page + 311. Sample-path lemmas (B.2–B.4, C.1–C.3) are not stated. Contributions are welcome on the LP perturbation lemma, the compound-Poisson moment bound and the measurability of the PAC recursion, each of which stands alone.
First-order methods for nonsmooth, nonconvex optimization (proximal algorithms, alternating minimization, subgradient-type descent) are analysed through generalized derivatives. Convergence and complexity arguments need a lower bound on the size of those derivatives away from critical points. For the Clarke subdifferential of a general lower semicontinuous function no such bound is available: Clarke subgradients can be small, or even zero, at points where the function decreases steeply along a smooth piece of its domain.
Bolte, Daniilidis, Lewis and Shiota (SIAM J. Optim. 18(2), 2007) showed that the obstruction disappears for functions whose graph admits a Whitney stratification, a partition into smooth manifolds that fit together regularly. Semialgebraic functions, and more generally functions definable in an o-minimal structure, have such stratifications. For these functions every Clarke subgradient is at least as long as the gradient of the function along the stratum through the point. This projection formula is the step from the geometry of the graph to the nonsmooth Kurdyka–Łojasiewicz inequality of the same paper, which underlies the convergence theory of many splitting methods (Attouch–Bolte–Svaiter 2013; Bolte–Sabach–Teboulle 2014).
This mission covers §2–§3 of the paper: the definitions, the projection formula (Proposition 4) and its Corollary 5 (i). The Kurdyka–Łojasiewicz part (§4) is a separate mission of the same series.
Let be lower semicontinuous, with domain and graph .
A stratification of a nonempty set is a locally finite partition of into submanifolds (the strata) such that implies for . It has the Whitney-(a) property if, whenever converge to () and the tangent spaces converge to a subspace , then ; subspaces converge in the gap . A Whitney stratification is a stratification with this property.
A stratification of is nonvertical if for every and (condition (H)). Let drop the last coordinate. For let be the stratum containing and . Nonverticality makes the tangent space of the graph of a linear form over ; the vector representing it is the stratum gradient , characterized by .
For lower semicontinuous whose graph admits a nonvertical Whitney stratification, and every ,
Further items state that the stratum gradient exists and is unique under (H), the equality when (Remark 4), the chain of (7), nonverticality for locally Lipschitz functions (Remark 3), and the nonsmooth Morse–Sard theorem of Corollary 5 (ii).
The inequality (14) says that Clarke critical points of a stratifiable function are critical points of its restriction to a stratum, and that the Clarke subdifferential is never shorter than the smooth gradient along the stratum. Two consequences are drawn in the paper. With countably many strata and the classical Morse–Sard theorem it gives a nonsmooth Morse–Sard theorem: the set of Clarke critical values has measure zero (Corollary 5 (ii)). Combined with the o-minimal Łojasiewicz inequality for the restrictions it gives the nonsmooth Kurdyka–Łojasiewicz inequality for definable lower semicontinuous functions (§4), the hypothesis behind global convergence results for proximal and splitting algorithms on semialgebraic problems.
All results of this mission are proved in the paper. None has a machine-checked proof that we know of: Mathlib has the tangent cone, Fréchet differentiability and orthogonal projections, but no stratifications, no singular or Clarke subdifferential of an extended-valued function, and no projection formula. The work is to formalize the paper's proof, which reduces the projection formula to the behaviour of Fréchet normals under limits of tangent spaces.
The first step, (11), is local and smooth: along a curve in the stratum the function is differentiable, and a Fréchet subgradient must agree with the derivative in tangent directions. The difficulty is the passage to limits in (12). A limiting subgradient at is a limit of Fréchet subgradients at points which may lie in a different, higher-dimensional stratum ; nothing in the smooth argument relates to . The relation is supplied exactly by the Whitney-(a) property, together with the compactness of the Grassmannian and the local finiteness of the stratification. Without Whitney-(a) the inclusions fail, so a proof that never uses it is wrong. The singular part requires the same argument for rescaled subgradients , whose normals become horizontal in the limit.
is EuclideanSpace ℝ (Fin n), is EuclideanSpace ℝ (Fin (n+1)) with the function value as the last coordinate, and is EReal with never . The Fréchet and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff; the tangent space (span of the tangent cone) and submanifolds (coordinate slices of some dimension) are the published ProjLikeRetr.Retractor definitions. The closed convex hull in (6) is closedConvexHull, not convexHull. Strata may be empty; local finiteness is required at points of the stratified set; a gap supremum over an empty unit sphere is . The stratification hypothesis is taken of class , the weakest case of the paper's "-Whitney".
The stratum gradient is defined intrinsically: with . It is not defined as a derivative of along the whole projected set . That set can fail to be a submanifold for a discontinuous lower semicontinuous , and every statement would then hold vacuously at such points. A companion item proves existence and uniqueness of the stratum gradient under (H), so the goal is not vacuous. The goal quantifies over all elements of ; this set may be empty (Remark 4), which is the page's restriction to , and no real-valued distance to is used.
A complete development needs the tangent space of a submanifold as the image of the chart derivative, convergence of subspaces and compactness of the Grassmannian of , Fréchet normals to epigraphs, and the density of in for lower semicontinuous . These pieces are reusable beyond this mission; the subspace gap and Whitney stratifications are prerequisites of the §4 mission. Contributions of any of the listed lemmas are welcome, as are proofs of the companion items.
Packing arc-disjoint arborescences is one of the basic tractable problems of combinatorial optimization. Edmonds' branching theorem (1973) says that a digraph contains arc-disjoint spanning arborescences rooted at a vertex if and only if every non-empty vertex set is entered by at least arcs. Its undirected counterpart is the Tutte–Nash-Williams theorem on edge-disjoint spanning trees, and Frank showed how the undirected theorem follows from the directed one through an orientation argument. Both results underlie network-design and connectivity-augmentation algorithms, and the cut condition in Edmonds' theorem is the model for many min–max theorems on packings.
Katoh and Tanigawa (2013), motivated by the rigidity of frameworks with boundaries, introduced matroid-based packings of rooted trees in undirected graphs: the roots of the trees are elements of a matroid, and every vertex must be covered by trees whose roots form a base. Durand de Gevigney, Nguyen and Szigeti (arXiv:1207.1985, 2012) gave the directed counterpart. Their Theorem 1.6 characterizes digraphs with roots that admit a matroid-based packing of arborescences, contains Edmonds' theorem as the special case of the free matroid with all roots at one vertex, and implies Katoh and Tanigawa's undirected theorem through Frank's orientation theorem. Its proof is short and purely combinatorial.
Timeline:
A digraph has a finite vertex set and a finite set of arcs, each with a tail and a head; parallel arcs are allowed. For , is the set of arcs entering (tail outside, head inside) and . An arborescence rooted at is a sub-digraph that is a directed tree in which has in-degree and every other vertex has in-degree ; the single vertex is an arborescence.
Let be a finite set and a placement of its elements at vertices (several elements may sit at one vertex). The triple is a digraph with roots. Write and . Let be a matroid on with rank function .
In Lean these are Digraph, Arborescence, MIndependent, MConnected and IsBasicPacking in the namespace BasicPackArb.Main; the proof-side notions (tight sets, domination, good and bad arcs, the parallel extension) are in a second definitions module.
The statement is universally quantified over the vertex, arc and root types, the digraph, the placement and the matroid. It has no constants.
The result. Theorem 1.6 is a good characterization: both sides can be certified, and the condition (3) is a cut condition with a submodular right-hand side. It unifies Edmonds' branching theorem (free matroid, all roots at one vertex) with matroid-constrained packings, and through Frank's orientation theorem it yields Katoh and Tanigawa's theorem on rooted-tree decompositions, which is used in combinatorial rigidity. The same paper derives from it a description of the convex hull of basic packings and a polynomial algorithm for the minimum-cost version.
Formalizing it. The result is proved on paper; no machine-checked proof of Theorem 1.6, of Edmonds' branching theorem, or of any of the claims is known on this platform. A formal proof needs a multi-digraph library with arc deletion, arborescences as sub-digraphs, in-degree functions of vertex sets and their submodularity, and matroid rank and span arguments on top of Mathlib's Matroid. The milestones follow the paper's induction on the number of arcs.
The necessity direction is a counting argument. Sufficiency is the substance. The natural first attempt, building the arborescences greedily or splitting into Edmonds instances, fails because the arborescences are not spanning and the covering condition is a base condition at every vertex, coupled through the matroid. The hard step is Claim 2.4: deleting an arc can destroy condition (3), and it must be shown that some bad arc, together with a suitable new parallel root, can be removed without doing so. Condition (3) has to be controlled for every vertex set at once, with a right-hand side that changes with the matroid. Formally, the lifting step requires gluing two arborescences with an arc and checking that the base condition survives the identification of the parallel pair.
Fintype V with decidable equality. Arcs: an ambient type with tail, head and a finite arc set arcs, so parallel arcs and loops are allowed and deletes one arc.Matroid S with ground set all of (a finite type); rank is Matroid.eRk with values in ; base is IsBase, independence is Indep.Option S with the new element none; is the comap of along , which makes none parallel to and restricts to on .A formalization in which arborescences need not lie in , or need not be reachable from their root, or in which the packing is a set of arborescences, or the per-vertex condition is "spanning" or "independent" rather than "base", states a different theorem and is ruled out by the definitions above.
Contributions welcome: proofs of the claims in any order, general lemmas on submodularity of and on tight-set uncrossing (reusable for other arborescence-packing results), and a proof of Edmonds' branching theorem as a corollary of the goal.
Nonlinear semidefinite programming asks to minimize a smooth function subject to smooth equality constraints and a constraint that a smooth matrix-valued function be positive semidefinite. It covers robust control design, structural optimization, and nonconvex matrix problems such as low-rank approximation and nearest-correlation-matrix problems. Algorithms for it (sequential quadratic programming, augmented Lagrangian and semismooth Newton methods) converge fast locally only when the Karush–Kuhn–Tucker (KKT) point they approach is stable under perturbation, and the question is which checkable conditions guarantee that stability.
For classical nonlinear programming the answer has been known since the 1980s: at a local minimizer, Robinson's strong second order sufficient condition together with linear independence of the active gradients is equivalent to strong regularity of the KKT point (Robinson 1980; Jongen et al. 1987; Kojima 1980). D. Sun extended this equivalence to nonlinear semidefinite programs, where the constraint cone is not polyhedral and second-order analysis carries an extra curvature term.
Timeline.
is a finite-dimensional real inner-product space, is Euclidean space, and is the space of real symmetric matrices with the Frobenius inner product . is the cone of positive semidefinite matrices. The problem is
with , , twice continuously differentiable. Write and . The Lagrangian is , and the multiplier set consists of the with , and in the normal cone (so and ). A triple with is a KKT point.
For a closed set , is the tangent cone and its lineality space. Robinson's constraint qualification at is ; constraint nondegeneracy replaces by . The critical cone is .
For with Moore–Penrose pseudo-inverse , set . Let be the metric projector, , and with . Then and . The strong second order sufficient condition (SSOSC) at is
The KKT map is on ; its zeros are the KKT points. The KKT system is also the generalized equation with and . A solution is strongly regular if, for all small , the linearized equation has a unique solution near that depends Lipschitz-continuously on . Clarke's generalized Jacobian is the convex hull of the B-subdifferential , the set of limits of Jacobians at nearby differentiability points. is the directional derivative. The uniform second order growth condition and strong stability quantify over all -smooth parameterizations of the problem.
At a local minimizer satisfying Robinson's CQ, with , the following are equivalent:
The matrix analysis of : Lemma 1 (a B-subdifferential chain rule), Lemma 2, Propositions 3 and 4 (the block structure of and ), and Proposition 7 (the inequality ). Second-order theory: Proposition 8 (the strict CQ gives a unique multiplier and ), Theorem 10 (the classical second-order conditions with the sigma term) and Lemma 11 ( equals the sigma term on ). The equivalences: Remark 15 (strong regularity iff a natural map is a Lipschitz homeomorphism), Proposition 16 ((a) ⇒ (b) ⇒ (c) at any KKT point), Lemma 18 (uniform growth ⇒ SSOSC) and Lemma 20 ().
The theorem identifies the SSOSC, a condition that can be checked from the problem data, with the stability notions that local algorithms need. Strong regularity is the hypothesis under which Newton-type methods for the KKT system converge locally and solutions vary Lipschitz-continuously with the data. Nonsingularity of gives quadratic convergence of semismooth Newton methods. Uniform growth and strong stability are what sensitivity analysis uses. Without the theorem, each of these properties has to be verified separately for semidefinite programs. The theorem also shows that the classical nonlinear programming equivalence survives on a non-polyhedral cone if the curvature term is added.
The result is proved in the literature but has no machine-checked proof. Formalizing it requires the B-subdifferential and Clarke Jacobian of the PSD projector, second order tangent sets of , and the Robinson–Kummer characterization of strong regularity. None of these exists in Mathlib. Items (g) and (i), which use the topological degree, are not formalized.
The obvious route is to copy the nonlinear programming proof: write strong regularity as nonsingularity of a reduced Jacobian on the active constraints. This fails because is not polyhedral. The KKT map is only semismooth, and its generalized Jacobian at a non-strictly complementary point is a whole family of operators, parametrized by . Nonsingularity has to be shown for every member of that family. The curvature of the cone appears only through , which links the second-order condition to the Jacobian family. The converse directions combine several external theorems (Bonnans–Shapiro's stability theory, Clarke's inverse function theorem, Kummer's characterization), each needing nonsmooth infrastructure.
All objects are defined in SunNLSDP.Equiv.Setting. is the subspace of symmetric vectors in EuclideanSpace ℝ (n × n) for a finite index type n, so its inner product is exactly the Frobenius product. and are WithLp 2 products, carrying the sum of the inner products. is computed by the continuous functional calculus. The metric projector returns its argument when no minimiser exists; it is applied only to nonempty closed convex sets. Clarke's Jacobian, , the one-sided directional derivative, the normal cone and the lineality space are the published definitions NonsmoothNewton.Shared.clarkeJac, NonsmoothNewton.Local.dirDeriv and RobinsonSR.Reduction.Setting.
Conventions committed to:
Items (g) and (i) of Theorem 21 are omitted, because Brouwer degree is unavailable; no surrogate for the index is substituted. A formalization that reads the CQs or nondegeneracy as two decoupled equations, or states SSOSC only on instead of , proves a different theorem and is ruled out.
Reusable infrastructure: the PSD projector and its generalized Jacobians, second order tangent sets, the Moore–Penrose pseudo-inverse of symmetric matrices, and the characterization of strong regularity by Lipschitz homeomorphisms. Proofs of individual milestones are welcome, as are lemmas on and on strong regularity of generalized equations.
Augmented Lagrangian methods are among the standard ways to solve smooth nonlinear programs. They replace a constrained problem by a sequence of subproblems in which some constraints are moved into the objective through a penalty term and multiplier estimates. The method of Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18(4), 2007) is the theory behind the ALGENCAN solver. It moves only the "upper-level" constraints into the objective, keeps arbitrary "lower-level" constraints in the subproblems, and requires the subproblems to be solved only approximately.
A convergence theory for such a method has to say what the limit points of the iterates are. This mission is about the second half of that theory (Theorem 4.2): a limit point that is feasible is a KKT point of the original problem, provided it satisfies a weak constraint qualification, the constant positive linear dependence condition (CPLD) of Qi and Wei (SIAM J. Optim. 10(4), 2000). Earlier global convergence results for augmented Lagrangian methods, such as Conn, Gould and Toint's, assumed linear independence of the active gradients (LICQ) at all limit points. CPLD is implied by MFCQ and by LICQ, holds automatically for linear constraints, and is required only at feasible points.
Timeline of the relevant notions:
The problem (2.1) is
with and constraint maps into , all continuously differentiable. and .
The augmented Lagrangian with respect to (2.2) is
Algorithm 3.1 works in outer iterations with a penalty parameter and safeguarded multipliers , that stay in fixed boxes. At iteration it finds and lower-level multipliers , that satisfy the KKT conditions of "minimize on " up to a tolerance . It then computes the first-order estimates and . Finally it increases by a factor unless a feasibility-complementarity measure has decreased by the factor .
A point satisfies CPLD if, whenever some gradients of constraints active at have a nontrivial vanishing linear combination with nonnegative coefficients on the inequalities, those gradients remain linearly dependent at every point of a neighbourhood of .
If is a limit point of and satisfies CPLD with respect to all constraints of (2.1), then is a KKT point of (2.1). If moreover satisfies MFCQ and , then
The theorem says that the algorithm has the right limit points: a feasible limit point is stationary under a constraint qualification weaker than MFCQ and LICQ, with no assumption on the penalty parameters. Milestone 3 is a result of independent interest: an "approximate KKT" sequence converges to a KKT point under CPLD. This sequential argument was later developed into the theory of approximate KKT conditions (Andreani, Haeser & Martínez 2011), and it applies to any algorithm that produces approximate KKT points, not only to this one. Milestone 4 gives the classical fact that MFCQ bounds the multipliers of such sequences.
All results are proved in the paper. As far as is known, none has a machine-checked proof. Neither CPLD nor the augmented Lagrangian method of this paper is formalized in Mathlib or on the platform. The companion missions of this series formalize Theorem 4.1 (feasibility of limit points) and Theorem 5.4 (boundedness of the penalty parameters).
The obvious argument divides the approximate KKT relation by the size of the multipliers, passes to the limit and obtains a contradiction with the constraint qualification. Under CPLD this argument fails, because CPLD does not bound the multipliers: they may diverge along the sequence even though the limit is a KKT point, and the limit of the normalized relation need not contradict anything at itself. CPLD speaks about linear dependence on a whole neighbourhood of , while the relation holds only at the iterates, so the information has to be transferred from to nearby points. A pointwise version of CPLD (dependence at only) is plain positive linear dependence, and with it the statement is false.
A second difficulty is complementarity (milestone 2). The safeguarded multipliers do not vanish on inactive constraints. Whether does depends on whether the penalty parameters are bounded, which needs the update rule of Step 4.
is EuclideanSpace ℝ (Fin n) and is Mathlib's gradient. The problem is a structure of component functions indexed by Fin m. The standing assumption "continuous first derivatives on a sufficiently large and open domain" is read as ContDiff ℝ 1 on all of .
A run of Algorithm 3.1 is a predicate on sequences (IsRun), not a computed object:
KKT, CPLD and MFCQ are defined once for an abstract program with finite index types. The constraints of (2.1) enter as the families and :
"Limit point" is MapClusterPt. (4.8) is required for every strictly increasing reindexing converging to , and it bounds the unsafeguarded estimates , ; the safeguarded ones are bounded by construction and would make (4.8) trivial.
Trivializing formalizations are ruled out:
Contributions welcome: proofs of the four milestones and of the goal, and in particular a reusable conic Carathéodory lemma and a library-level "approximate KKT + CPLD ⇒ KKT" theorem (milestone 3), which is useful well beyond this paper.
Augmented Lagrangian methods solve a constrained problem by minimizing a sequence of penalized subproblems while updating estimates of the Lagrange multipliers. Each subproblem carries a penalty parameter . When grows without bound the subproblems become ill-conditioned and hard to solve, and the method behaves like a plain external penalty method. Avoiding that growth is one of the main reasons for using multiplier updates at all, so conditions under which stays bounded matter both in theory and in practice (Bertsekas 1982; Conn, Gould, Toint 1991).
Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18 (2007); HAL hal-01295437) propose an augmented Lagrangian method, Algorithm 3.1, in which only some of the constraints are penalized. Their §5 shows that, under classical local hypotheses at the limit point and a subproblem tolerance tied to the current infeasibility, the penalty parameters remain bounded. This mission formalizes that result for equality-constrained problems (Theorem 5.4), together with the general case (Theorem 5.5) as a companion statement.
Let , , , , be continuously differentiable. Problem (2.1) is
The upper-level constraints are penalized by the PHR augmented Lagrangian
while the lower-level constraints stay in the subproblems.
Algorithm 3.1 fixes , , , a box , a bound and tolerances . At outer iteration it finds and lower-level multipliers such that is an -approximate KKT point of minimizing over the lower-level set, in the sense of (3.1)–(3.4). It then forms the first-order multiplier estimates
and safeguarded estimates , which in §5 are the projections of on their boxes. Finally it updates the penalty parameter: with ,
In §5.1 there are no inequality constraints (): problem (5.1), with Lagrangian . Assumptions 1–6 at the limit of are: convergence, feasibility, linear independence of all constraint gradients, near , the second-order sufficient condition with multipliers , and in the interior of the safeguard box.
Under Assumptions 1–6, , and for a sequence ,
with and . 4. (5.10): if , then for large. 5. Contraction: if , then for large.
Theorem 5.5, the general problem (2.1) under Assumptions 7–13 (LICQ, , a second-order condition on the tangent subspace of all active constraints, multipliers inside the safeguard boxes, strict complementarity for the active upper-level inequalities), with ; and two steps of its proof, (5.13) and (5.14).
Theorem 5.4 tells a user of the method when it does not degenerate: if the safeguard box contains the true multipliers and the subproblems are solved to a precision proportional to the current infeasibility, then the penalty parameter is eventually constant. The Remark after Theorem 5.5 draws the practical conclusion that the box should be large enough to contain the true multipliers. The result underlies the analysis of the ALGENCAN solver built on Algorithm 3.1.
The results are proved on paper. To our knowledge none of them, nor the PHR augmented Lagrangian method itself, has a machine-checked formalization. A formal proof would also pin down two gaps in the printed statements, recorded under Formalization scope: the case and the early iterations in Lemma 5.3. The local analysis (a uniformly nonsingular KKT matrix and implicit-function error bounds for multiplier estimates) is reusable for other augmented Lagrangian and SQP methods.
Without the second-order structure there is no reason for to stay bounded: the update test compares consecutive infeasibilities, and nothing in the global theory forces them to decrease geometrically. The local argument has to show that contracts by a factor of order , which requires error bounds for both and that hold uniformly as varies in an interval containing . The uniformity in the perturbation parameter , around the singular-looking limit , is the central difficulty. Applying the implicit function theorem at each fixed does not give it.
is EuclideanSpace ℝ (Fin n). Constraint maps are families of real functions indexed by Fin m, and problem (5.1) is (2.1) with . The norm in (3.1), on and on is Euclidean. Every , and the norms in (3.4), on and on , are the sup norm. The paper's norm is arbitrary and the constants absorb the change. A run of Algorithm 3.1 is a predicate on sequences: x 0 is , the outer iterations are , and the three tolerances of Step 2 are kept separate. The gradient in (3.1) is the true gradient of the defined augmented Lagrangian. "Continuous first derivatives" is on ; "continuous second derivatives near " is ContDiffAt ℝ 2. Hessians are derivatives of gradients. Every statement that uses a Hessian assumes at , so it cannot be a junk value. Assumption 5 is pinned to Fletcher's equality-constrained second-order sufficient condition. Linear independence is that of a family indexed by a sum type, so equal gradients count as dependent.
Added hypotheses, each stated in the item's Formalization Note:
Statements that would trivialize the goal are excluded. These include a run predicate that no sequence satisfies, merging the three tolerances into , collapsing gradient families into sets, a junk Hessian, and assuming or in the goal. The last two appear only as milestone hypotheses.
A complete development needs the PHR gradient formula, uniform invertibility of a continuous family of matrices on a compact interval, a quantitative inverse function estimate for maps, and the convergence of multiplier estimates under LICQ. Proofs of any milestone, and reusable lemmas for these pieces, are welcome.
The proximal algorithm is the basic implicit scheme for minimizing a function : from the current point it moves to a minimizer of plus a quadratic penalty on the distance travelled. For convex its convergence theory is classical (Martinet 1970, Rockafellar 1976). For nonconvex, nonsmooth the situation is different: descent and boundedness give only that limit points are critical, and the whole sequence may fail to converge even for smooth (Palis–de Melo; Absil, Mahony and Andrews, SIAM J. Optim. 2005).
Attouch and Bolte (Math. Program. 116, 2009, online 2007; author's version hal-00803898) showed that the Łojasiewicz inequality, which holds for real-analytic functions and for continuous subanalytic functions, restores convergence of the whole sequence for the nonsmooth proximal algorithm, together with explicit rates. The argument is Łojasiewicz's original gradient-flow idea transferred to a discrete, nonsmooth setting. It became the template for the later convergence analyses of proximal alternating minimization, forward–backward splitting and PALM under the Kurdyka–Łojasiewicz property, which are used throughout nonconvex optimization, signal processing and machine learning.
Timeline:
Points live in with the Euclidean norm . Let be proper (never , finite somewhere) and lower semicontinuous, with domain .
The limiting subdifferential is the set of limits of Fréchet subgradients along sequences with . A point with is critical, and the set of critical points is .
Fix and step sizes . From an arbitrary the proximal algorithm produces
Any minimizer may be selected. The standing hypotheses are
with the convention (Remark 4). The number in (5) at a point is a Łojasiewicz exponent of that point.
denotes the set of limit points of .
Under (H1), (H2), (H3), if is bounded then
It fixes no constants and holds for every admissible step sequence and every selection in (2).
Theorem 5 (rates): with a Łojasiewicz exponent of , gives finite termination, gives with , and gives . Also: well-posedness of (2) under (H1), Proposition 2 (v), and Remark 2.
The theorem turns subsequential convergence into convergence of the whole sequence, with finite length, for a class that includes semi-algebraic, real-analytic and continuous subanalytic functions. Finite length is the property later used to analyse splitting and alternating schemes under the Kurdyka–Łojasiewicz property, and Theorem 5 is the first rate classification by the Łojasiewicz exponent for a nonsmooth algorithm.
The results are proved on paper. No machine-checked proof of Theorem 4 or Theorem 5 is known to exist. A formalization adds a checked convergence theorem for the nonsmooth proximal algorithm with extended-real-valued , and a reusable set of descent, limit-set and uniformization lemmas that apply to other Łojasiewicz-type analyses.
Descent and give only , which does not imply convergence: the iterates can circle a continuum of critical points with square-summable but non-summable steps, as in the counterexamples for smooth functions. The step that must be supplied is summability of itself. The local inequality (5) holds only near one critical point with its own constants, while the iterates approach a whole compact set , so the local constants first have to be made uniform near that set. The nonsmooth setting adds two difficulties: takes the value , and subgradients are limits of Fréchet subgradients, so their closure properties have to be established for this subdifferential.
is EuclideanSpace ℝ (Fin n); is allowed. is EReal-valued and proper means never and somewhere not . Lower semicontinuity is Mathlib's LowerSemicontinuous. (H2) is ContinuousOn f {x | f x ≠ ⊤}. The limiting subdifferential and are the published platform definitions NonconvexSplitting.Shared.LimitingSubdiff and NonsmoothLojasiewicz.Continuous.crit. Algorithm (2) is a predicate on a sequence (every step is some minimizer), not a proximal map. Limit points are cluster points of the sequence. The power in (5) is lojPow θ s = if s = 0 then 0 else s ^ θ, which implements ; real values of are used only where is finite.
Standing assumptions carried by the goal and Theorem 5: proper and lower semicontinuous, (H1), (H2), (H3), with , a sequence complying with (2), and boundedness of its range. Milestones drop the assumptions their claims do not use. The milestones (8) and (9) also assume for all and use . Both come from the proof's normalization. This reduction is not a hypothesis of Theorem 4: a goal that assumed it, mentioned the constants , or assumed (8) would not be the paper's theorem.
The development needs the closure properties of the limiting subdifferential, the Fermat rule for proximal steps, and compactness and connectedness of limit sets of sequences with vanishing steps. These are reusable for every Łojasiewicz-type convergence proof. Proofs of individual milestones, of the rate lemmas in the proof of Theorem 5, and of the example are welcome.
Multistage stochastic linear programs model sequential decisions under uncertainty: capacity and reservoir planning, hydro-thermal scheduling, inventory and asset–liability management. When the data process is stagewise independent, the problem decomposes by dynamic programming into one linear program per stage, coupled through expected cost-to-go functions. These functions are convex and piecewise linear, and the stochastic dual dynamic programming (SDDP) method of Pereira and Pinto (1991) approximates them from below by cutting planes. SDDP is the standard solution method in the long-term planning of hydro-dominated power systems, and its convergence theory determines what the bounds it reports actually mean.
Shapiro's paper (Optimization Online 2009/12/2509; European J. Oper. Res. 209(1), 2011, doi:10.1016/j.ejor.2010.08.007) analyses SDDP applied to a sample average approximation (SAA) of the true problem, with all of the data random. Its convergence result, Proposition 3.1, asserts finite convergence with probability one when the forward scenarios are subsampled independently. A related almost-sure finite convergence theorem for a different algorithm (DOASA, with randomness only in the right-hand sides and cut sharing across outcomes) is due to Philpott and Guan (2008); it is posed as a separate mission on this platform and is not restated here.
There are stages. The decision satisfies and, at the first stage, with deterministic data . For the data are replaced by a sample , , each with probability , independently across stages, and the stage- constraint is . The SAA cost-to-go functions are defined backwards from :
A scenario is a choice ; there are of them, each of probability . A policy depends only on the outcomes up to stage ; it is optimal for the SAA problem if it is feasible on every scenario and its expected cost is minimal.
SDDP keeps, for each stage, a finite set of cuts whose maximum lies below . An iteration has a forward step: scenarios are sampled, and along each of them the decisions solve the stage problems with in place of , (3.13)–(3.14). It also has a backward step: from down to , at each trial point the stage- problems with the current cuts are solved for all outcomes, and the cut (3.17) is added, where averages over basic optimal (extreme-point) dual solutions .
Suppose the forward scenarios are drawn independently and uniformly from the SAA scenarios, (A1) holds ((3.13) and (3.14) have finite optimal values for every scenario at every iteration), and the backward steps use basic optimal dual solutions. Then
The goal fixes no iteration count, no rate and no number of forward scenarios .
The result separates SDDP's sampling from its convergence: on a finite scenario tree, independent subsampling of forward paths suffices for the method to stop at an optimal policy, without ever enumerating the tree. It explains why the lower bound eventually equals the SAA optimal value, which is what makes the gap-based stopping rules of the paper (§3, Remarks 4–6) meaningful. The paper's closing remark stresses that without independence of the forward scenarios there is no guarantee of convergence.
The proposition is proved in the paper. No machine-checked proof of it, or of any SDDP convergence theorem, exists to our knowledge. Formalizing it requires a precise account of what the method is: which dual solutions, which forward solutions, which order of updates. Several of these points are left implicit on the page.
Finiteness of the cut universe (milestones 4–5) is a statement about extreme points of dual polyhedra whose dimension grows with the cut sets of the next stage, so it must be organized stage by stage from down. The central difficulty is the last step of the argument. Once the approximations have stopped changing, one must show that the stable cuts are exact where the forward policy goes, so that the forward policy satisfies (3.18). The obvious argument, "if (3.18) fails at the last stage where it fails, the next cut there increases ", does not work as printed: (3.18) holding at later stages does not by itself make the next-stage approximation exact at the trial point. Closing this step is where the conventions on forward solutions and on sampling listed below become essential.
The Lean development is in the namespace ShapiroSDDP.Convergence. Stages are numbered
; the data of stage are stored under index (the coupling matrix is indexed by the
decision it multiplies); V t is , with V t ≡ 0 for . Cost-to-go
values are real infima, used only on reachable decisions. The explicit readings are:
iIndepFun);Optimality of a policy is defined by expected cost, never by (3.18), so that milestone 6 is not definitional. Sampling is stated as i.i.d. uniform draws, not as "every scenario recurs", which is milestone 7. All of depend on the outcome. If some lacks full row rank, no basic dual solution exists and no run exists; a sorry-free witness instance shows that all hypotheses of the goal can hold together.
Useful infrastructure: LP weak and strong duality (LinearOptimization.lp_weak_duality,
LinearOptimization.lp_strong_duality exist on the platform in their own encoding), finiteness of
extreme points of polyhedra, attainment for polyhedral objectives, and the second Borel–Cantelli
lemma (ProbabilityTheory.measure_limsup_eq_one). Proofs of any milestone, and reusable lemmas on
LPs with cut epigraphs, are welcome.
In shop scheduling, jobs consist of chains of operations, each to be processed on a prescribed machine, and the goal is to minimize the makespan, the time at which the last operation finishes. Almost every approximation algorithm for job shops, acyclic job shops and flow shops is analysed against one quantity: the trivial lower bound , where the congestion is the largest total processing time requested on one machine and the dilation is the largest total processing time of one job. Any schedule has makespan at least .
How weak can this bound be? Leighton, Maggs and Rao (1994) showed that for acyclic job shops with unit-length operations the optimum is . For operations of arbitrary length, Feige and Scheideler (2002) proved an upper bound of for acyclic job shops, and gave acyclic job shop instances whose optimum is . Flow shops, in which every job visits every machine in one common order, are much more structured, and no flow shop instance with optimum was known. Feige and Scheideler asked whether flow shops admit a significantly better upper bound. Mastrolilli and Svensson (J. ACM 2011, Theorem 1.1) answered this negatively by constructing flow shops whose optimal makespan is a factor above .
Timeline:
A job shop instance has machines and jobs; job is a sequence of operations , operation needs time units without interruption on machine . A feasible schedule assigns a start time to every operation so that each operation starts after the previous operation of its job has completed, and no two operations on one machine overlap. A zero-length operation therefore still occupies an instant on its machine: it cannot be performed strictly inside another operation there. The makespan is the largest completion time.
The instance , for natural numbers :
Operations of positive length are long-operations, the others short-operations. For a schedule, the -th long-operation of a job of frequency is good if the delay from its end to the start of the next long-operation of is at most ; the last long-operation of a job is never good. is the set of first halves of the good long-operations on machine , and the total time they cover.
For all natural numbers and : every job of has length , every machine has load (so ), and every feasible schedule satisfies
With this gives the paper's statement, an optimal makespan of .
The theorem shows that the lower bound , against which all known flow shop algorithms are analysed, can be off by a factor growing with . Any flow shop algorithm with guarantee relative to the optimum must therefore use a stronger lower bound than . The same frequency construction is the gap gadget behind the paper's inapproximability results for generalized flow shops and job shops (Theorems 1.2 and 1.3).
The result has been proved since 2011; as far as is known it has no machine-checked proof. The mission produces a formal model of the instance , a formal proof of the explicit bound for every , , and reusable statements about delays and first-half intervals in the published job shop model JobShopLTAS.Core.Instance.
The bound must hold for every feasible schedule, with no structural restriction such as a permutation or non-delay schedule. The obvious approach, comparing each machine's load with the makespan, only gives , since every machine carries exactly . The gain comes from interaction between machines of different frequencies in one group: a high-frequency job running in parallel with a low-frequency long-operation is held back by its zero-length operation on the low-frequency machine. Turning this into a quantitative bound requires controlling, for every job at once, how long it waits between consecutive long-operations, and that waiting is only bounded when the makespan is already small. Encoding the index arithmetic of (groups, frequencies, copies, positions of the long-operations) and the zero-length operations faithfully is a substantial part of the work.
JobShopLTAS.Core.Instance: machines Fin m, jobs Fin n, real processing times and start times, IsFeasibleSchedule Finset.univ s (nonnegative starts, chain precedence, disjunctive machine constraint s o + p o ≤ s o' ∨ s o' + p o' ≤ s o) and makespan Finset.univ s. Under that constraint a zero-length operation cannot sit strictly inside another operation on its machine, which the paper's argument needs.Welcome contributions: proofs of the counting facts about the encoding, of the milestones, and general lemmas about feasible schedules in JobShopLTAS.Core.Instance (completion time of a job bounds its delays; disjoint intervals in have total length at most ).
An investor who trades continuously in a market driven by Brownian motion, and who may only hold portfolios in a prescribed set, wants to maximize the expected utility of terminal wealth. With power utility , , this is the constant-relative-risk-aversion problem that goes back to Merton (Merton 1971). When there are fewer stocks than sources of noise the market is incomplete, and when portfolio proportions are restricted (no short sales, bounded positions, a fixed allocation) the problem is constrained.
For convex constraints, duality methods settle the problem (Cvitanić–Karatzas 1992; Kramkov–Schachermayer 1999). They do not apply when the constraint set is closed but not convex, as for integer-lot or "all-or-nothing" restrictions. Hu, Imkeller and Müller (2005, arXiv:math/0508448) treat that case by a martingale optimality principle: they build a process that is a supermartingale for every admissible strategy and a martingale for one, and obtain it from a backward stochastic differential equation (BSDE) with a driver that grows quadratically in . The existence theory for such equations is due to Kobylanski (2000).
This mission formalizes the power-utility result, Theorem 14 of the paper. A companion mission treats the exponential-utility result, Theorem 7.
Fix a horizon and a probability space carrying an -dimensional Brownian motion ; is the augmentation of its natural filtration. is the Euclidean norm, and is Lebesgue measure on .
Market. There is a bond with zero interest and stocks with prices . The rates and the volatility are predictable and uniformly bounded, and for constants . The market price of risk is .
Constraints. A closed set of row vectors constrains the proportions of wealth held in the stocks. In the variable the constraint reads . For a closed , , and is the (possibly multi-valued) projection.
Wealth and admissible strategies. From initial capital the wealth (11) is
The admissible class (Definition 13) consists of predictable with for -a.e. and a.s. The value is (12), .
The BSDE. is the class of predictable, -a.e. bounded processes and that of predictable with . The BSDE (15) is
A BMO martingale is one with over stopping times (equation (2)).
(15) has a unique solution , and for
attained by some with
The page prints ; its proof measures utility by , so the value of (12) with carries the factor (see Formalization scope).
The theorem gives the value of a constrained power-utility problem in closed form through one scalar, , of a BSDE, and identifies an optimal strategy as a measurable selection of a projection onto the constraint set. Convexity of the constraint is not needed; when is a convex cone the result recovers the strategy obtained by other methods (Remark 16 of the paper). The same scheme handles exponential and logarithmic utility in the paper's other sections, and the dynamic programming principle of Proposition 15 follows from it.
The result is proved in the paper. As far as the platform's records show, none of it is formalized: there is no quadratic BSDE, no BMO martingale and no continuous-time utility-maximization statement on the platform. A complete formalization would add an existence and uniqueness theory for BSDEs with quadratic growth, the BMO criterion for stochastic exponentials, and a verification theorem for constrained portfolio problems, each reusable well beyond this paper.
The verification argument is short on paper; its inputs are not. Existence for (15) rests on Kobylanski's existence theorem for drivers of quadratic growth, which is not in Mathlib; the Lipschitz theory does not cover a driver growing like . Uniqueness needs a comparison principle for such drivers. Lemma 17 and the martingale property of need the theory of BMO martingales and of their stochastic exponentials, also absent. The comparison milestone concerns processes that are only local supermartingales. A naive attempt that treats as a martingale for every admissible fails: for a general , which is only locally square integrable, it is merely a local supermartingale.
All declarations live in HuImkellerMuller.Power. Time is ℝ≥0; vectors of are EuclideanSpace ℝ (Fin m), with products as inner products; is a Set (Fin d → ℝ). The Brownian motion, the augmented filtration, the measure and the Itô-integral operator I are reused from published definitions (EthierKurtz_IsStandardBrownian, CvitanicKaratzas92_Optimality_Market). The wealth is constructed from I, and ; is computed from and .
Conventions and disclosed readings:
The value is a supremum of lower integrals, never of Bochner integrals: a Bochner expectation of a non-integrable is and would make the supremum meaningless. The goal asserts existence of a solution of (15) and does not take one as a hypothesis, so it cannot hold vacuously.
Contributions welcome: a theory of BSDEs with quadratic growth (Kobylanski), BMO martingales and Kazamaki's criterion, measurable selection of metric projections, and proofs of the deterministic milestone (14) and the growth bound (H1).
A linear multistage stochastic program chooses decisions over stages while a random vector is revealed one piece at a time; each decision may depend only on what has been observed so far. Such programs model production planning, capacity expansion, hydro scheduling and portfolio problems. Computing their optimal value exactly is intractable in general: Shapiro and Nemirovski argue that even medium-accuracy solutions are out of reach when the number of stages grows (Shapiro–Nemirovski 2005), and already the one-stage problem is #P-hard (Dyer–Stougie 2006, Theorem 3.2, as cited by the paper).
Linear decision rules restrict every decision to be an affine function of the observations. Introduced for robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004) and carried into stochastic programming by Shapiro and Nemirovski and by Chen, Sim, Sun and Zhang (2008), they turn the problem into a finite one whose optimal value is an upper bound. Kuhn, Wiesemann and Georghiou (Optimization Online 2009/02/2218; Math. Program. 130, 2011) apply the same restriction to the dual problem, which yields a lower bound. They show that, for polyhedral supports, both bounds are values of explicit linear programs. This mission formalizes the multistage version of that statement, Theorem 3 of the preprint.
Stages are . The uncertainty is with and ; by convention and . The history at stage is , , and the truncation operator maps to . The law of has support , a nonempty bounded polyhedron spanning , whose first two constraints encode . denotes conditional expectation given , and is the second-order moment matrix.
A stage- decision is a square-integrable Borel function of (written ). The program minimizes
with deterministic matrices , and . The linear conditional mean assumption requires almost surely for some ; it holds, for example, for stagewise independent data.
The primal approximation sets and slacks . The dual approximation keeps general rules but imposes the slack equations only in the weak form . The linear programs (4.2) and (4.6) are written in the matrices , multipliers and slack matrices , with .
Under the standing assumptions, the linear conditional mean assumption, and strict feasibility of ,
as extended-real optimal values. Both equalities are part of the goal.
The theorem makes both linear-decision-rule bounds on a multistage stochastic program computable by linear programming, with size polynomial in , , and and hence typically linear in the number of stages. The gap between the two values measures the suboptimality of the primal linear rule. These results underlie later work on piecewise-linear and lifted decision rules and on multistage robust and distributionally robust optimization.
The preprint omits the proof of Theorem 3 ("it widely parallels the argumentation in Section 2"), so a formal proof has to supply the multistage details: the conditional-expectation bookkeeping, the truncation operators and the transfer of the one-stage cone description to non-anticipative slacks. No part of this paper has been machine-checked before; the companion mission of this series formalizes the one-stage Theorem 1.
The obvious route repeats the one-stage argument stage by stage, and it breaks at the slack constraints of . A slack must be a function of alone, while the one-stage cone characterization of moment vectors concerns functions of the full ; Lemma 3 bridges them only through the linear conditional mean assumption and conditional expectations. A second difficulty is the closure gap between that cone and its polyhedral outer description: the equality of and relies on strict feasibility, and a proof that ignores it is wrong. On the primal side, the passage from almost sure constraints to identities of matrices needs both that every point of is charged by and that spans .
Vectors are functions Fin d → ℝ; stage is the Fin T index and coordinate is index 0. The history dimension is kbar kk t, the truncation is the restriction to the first coordinates, and is also given as a matrix. is Mathlib's condExp with respect to the σ-algebra generated by . " is the support of " means: closed, , and every ball around a point of has positive mass. Decision rules are Borel functions of the history whose composition with is in . Optimal values are infima in EReal ( if infeasible, if unbounded), and "equivalent" means equal optimal values. The matrices are data, with the conditional-mean identity as a hypothesis.
Three conventions are fixed where the page is silent or misprinted. Strict feasibility of , not defined in §4, is the analogue of (2.9) for the standard form (4.1): slacks at least almost surely. The equality constraint of is printed with inside ; the formalization follows (4.7), where the sum covers only . The sign condition in (4.5c) is printed as for a function of , and is read as . The theorem's last sentence (polynomial size, efficient solvability) is informal and not formalized. One hypothesis is added: the goal's second equality assumes or that some row of (the rows of below (2.1b)) is nonzero (the first equality is stated without it). For the support is the single point , and if has no nonzero row beyond (2.1b) the cone of Proposition 3 is all of ; the printed second equality then fails (a strictly feasible one-stage instance has while (4.6) is unbounded below). The added hypothesis excludes exactly this case.
Expectations are Bochner integrals, which vanish on non-integrable functions; under the standing assumptions is bounded almost surely, so all integrands involving square-integrable rules are integrable and no constraint is satisfied vacuously. Matrix.inv returns on singular matrices, but is positive definite under the standing assumptions. The linear conditional mean hypothesis cannot be dropped from Lemmas 2 and 3: without it need not exist.
A complete development needs the support and moment facts of §2 (, almost sure constraints extend to ), Farkas-type duality for the polyhedron , the tower property of conditional expectation, and the cone results of Propositions 3 and 4 of the preprint. These are reusable across the series. Proofs of the milestones, or of these supporting facts as separate lemmas, are welcome.