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?
Large engineered systems — power grids, chemical plants, logistics and communication networks — are usually modelled as many interacting subsystems. A stability certificate for the whole network is rarely available directly, but each subsystem can often be analysed on its own, treating the states of its neighbours as disturbances. Input-to-state stability (ISS), introduced by Sontag (Sontag 1989), is the robustness notion that makes this decomposition work: it bounds the state by a decaying function of the initial condition plus a gain of the input. A small-gain theorem states that if the gains by which the subsystems influence each other are "small" in a suitable sense, the interconnection is again ISS.
Timeline. Jiang, Teel and Praly proved a nonlinear small-gain theorem for two ISS systems in trajectory form (1994), and Jiang, Mareels and Wang gave its Lyapunov version for two subsystems (1996). Dashkovskiy, Rüffer and Wirth extended the trajectory version to subsystems with the condition on a nonlinear gain operator (2007). The paper of this mission (arXiv:0901.1842, SIAM J. Control Optim. 48(6), 2010) gives the Lyapunov version for subsystems with general monotone aggregation of the gains, and constructs the network's ISS Lyapunov function explicitly.
The network consists of subsystems
with overall state and dynamics , . is the Euclidean norm.
A function is of class if it is continuous, strictly increasing and , and of class if moreover unbounded. A positive definite function is continuous with only at . A Lyapunov function candidate is continuous, satisfies for some , and is locally Lipschitz away from the origin.
A candidate is an ISS Lyapunov function for if there are and a positive definite with
at every point of differentiability of .
On , means for every . A monotone aggregation function (MAF) is continuous, positive off the origin, strictly increasing for this strict order, and unbounded as . Subsystem has an ISS Lyapunov function with gains , and MAF on if, wherever is differentiable,
The diagonal gains vanish, . The gain operators are
An Ω-path with respect to is a continuous with every , such that each is locally Lipschitz on , its derivative lies in , , at its points of differentiability in any compact (constants depending on only), and for all .
Assume each is an ISS Lyapunov function for with gains , and MAFs ; is an Ω-path with respect to ; satisfies
and each is continuous. Then
is an ISS Lyapunov function for the network, with gain :
for a positive definite . The rate is existential and is not fixed by the statement.
The milestones follow the proof on pp. 14–15:
The result. Theorem 5.3 converts a small-gain condition into an explicit Lyapunov function for the network. Combined with the converse ISS Lyapunov theorem, it gives ISS of the interconnection, and with zero input it gives global asymptotic stability. It covers additive, maximum-type and multiplicative aggregation of gains, and it handles subsystems without iterating a two-system result. A second main result of the paper (Theorem 5.2, a separate mission) supplies the Ω-path from the condition . Together they reduce the stability of a network to a property of its gain operator.
Formalizing it. The result is proved on paper. As far as we know, no ISS notion, small-gain theorem or monotone aggregation framework has been machine-checked in Lean. This mission produces a Lean statement of the construction, and of its nonsmooth-analysis steps, against which a complete proof can be checked. It also corrects a misprint in the theorem's implication (see Formalization scope).
The function is a maximum of rescaled functions and is not differentiable on the set where two indices are active, even when every is smooth. The subsystem hypotheses only control derivatives at points where the corresponding is differentiable. At a point where is differentiable, the active may not be. So the obvious argument — differentiate the active branch and apply (2.7) — fails, and the decrease must be transported through generalized gradients. A second obstacle is uniformity: the rate must depend on alone. This requires the lower derivative bound in the Ω-path definition and a compactness argument on spheres. Dropping the lower bound breaks the theorem, because could flatten and remove the decrease.
Blocks are EuclideanSpace ℝ (Fin (N i)). The network state is the product PiLp 2 (the Euclidean norm, not the sup norm), and the input is EuclideanSpace ℝ (Fin M). Subsystems are indexed by Fin n (0-based) with . Gains, MAFs, Ω-paths and rates live on ℝ≥0. Lyapunov functions are real-valued with an explicit nonnegativity clause. The strict order on is a named predicate, not Lean's Pi <. The inverses and are explicit arguments with both compositions the identity. Every derivative is guarded by a differentiability hypothesis. Clarke's generalized gradient (2.5) is the published ClarkeGradients.Shared.generalizedGradient on the blocks, and the same definition restated on a general Hilbert space for and .
Implicit hypotheses made explicit:
Corrected statement. The printed implication (5.5) has the trigger . With as defined in (2.9), and as the paper's corollaries use it, that implication is false. A counterexample is one subsystem with , , and , at , . The proof's chain of inequalities writes where (2.9) gives . The goal keeps (2.9) and uses the trigger , under which the proof closes.
The hypotheses are jointly satisfiable. An example is with , , , , , and dynamics . The conclusion is a decrease inequality at the points of differentiability of for an existential positive definite rate, so it cannot be met by a vacuous choice: must be positive away from zero. Trajectory-level ISS (Theorem 2.3, cited by the paper) and the corollaries that conclude ISS are out of scope.
Reusable infrastructure: comparison classes, monotone aggregation functions, gain operators and Ω-paths (shared with the Ω-path mission), and the maximum and chain rules for Clarke gradients. Proofs of the nonsmooth calculus milestones are welcome independently of the goal.
A linear two-stage stochastic program with fixed recourse chooses a here-and-now decision before a random vector is observed, and pays a recourse cost afterwards. It is the basic model of stochastic programming, used in capacity planning, energy and supply-chain models. In practice the distribution of is never known exactly: it is estimated from data, replaced by a discrete scenario approximation, or perturbed for robustness. The question is how much the optimal value and the optimal decisions can move when is replaced by a nearby , and in which distance between probability measures "nearby" should be measured.
Rachev and Römisch (Math. Oper. Res. 27(4), 2002, doi:10.1287/moor.27.4.792.304; the mission cites the authors' preprint from edoc.hu-berlin.de) answer this with the method of probability metrics: they derive from the structure of the integrand a canonical distance on measures for each class of models. For linear two-stage programs the canonical distance is the Fortet–Mourier metric of order 2.
Timeline. Robinson and Wets (1987) studied qualitative stability of two-stage programs with respect to weak convergence of measures. Walkup and Wets (1969) had earlier established the piecewise-bilinear structure of the second-stage value function used here. Römisch and Schultz (1991) proved a quantitative stability result for two-stage programs with complete recourse in the Wasserstein metric . The present paper (published 2002) replaces complete recourse by relatively complete recourse plus dual feasibility, and by the metric , which it bounds by a multiple of (p. 13).
Let be a nonempty polyhedron and a polyhedron. Fix , an -matrix , and data , and an -matrix depending affine linearly on . The second-stage value is
with and . The integrand is when and , and otherwise. For a Borel probability measure on the problem is
with optimal value and solution set . Two assumptions are made: (A1) and for all ; (A2) has a finite second moment.
The Fortet–Mourier metric on , the probability measures on with finite second moment, is
For an open bounded , the growth function is , and with .
Under (A1), (A2), and an open bounded neighbourhood of , there are and such that for every with :
The constants are existential, so the goal does not depend on any particular estimate of them.
The theorem says that, under the two natural well-posedness conditions of linear recourse models, optimal values are Lipschitz continuous and solution sets move by at most , where only sees test functions with the local Lipschitz growth of the integrand. Since , the result contains the earlier stability theorem.
The results are proved in the paper, except Lemma 3.1, which it cites from Walkup and Wets (1969). None of them is formalized in Mathlib or on Prove2Me. A formalization would provide a checked model of the two-stage recourse function, the Fortet–Mourier metrics, and an end-to-end quantitative stability theorem for stochastic programs, none of which exist in Mathlib.
The obvious argument bounds by and then by . Two steps fail. First, the supremum ranges over all of , which may be unbounded, while lies in only for in a bounded set; the argument must localize to and then show, using convexity, that for close to the localized and global problems coincide. Second, the Lipschitz estimate in for requires the piecewise-bilinear structure of (Lemma 3.1) and a chaining argument across the polyhedral pieces of ; the integrand is not differentiable.
EuclideanSpace ℝ (Fin n). The paper never fixes its norm and all its constants are existential, so the Euclidean norm is a faithful instance. Second-stage vectors are coordinate vectors Fin k → ℝ; index sets are 0-based.DupacovaWets.Consistency.expect over restricted to .Measurements of Ethernet and Internet traffic in the 1990s showed that cumulative traffic is self-similar and long-range dependent: correlations of the input rate decay so slowly that they are not summable, and fluctuations at large time scales do not average out the way Poisson-type models predict (Leland et al. 1994). A widely accepted explanation is that the lengths of individual transmissions (file sizes, session durations) are heavy tailed, with infinite variance. Queueing and capacity-planning calculations then depend on which stochastic process approximates the cumulative input over long horizons.
Two approximations had been proposed: fractional Brownian motion, a Gaussian self-similar process with dependent increments, and α-stable Lévy motion, a heavy-tailed process with independent increments. Mikosch, Resnick, Rootzén and Stegeman (Ann. Appl. Probab. 12 (2002) 23–68) showed that both arise from the same models and that the answer depends on how fast the number of sources grows relative to the time scale. This mission formalizes their Gaussian answer for the superposition of ON/OFF sources: Theorem 4.
A single ON/OFF source alternates between ON-periods, during which it sends work at rate , and silent OFF-periods. The ON-periods are iid with law and the OFF-periods iid with law , both on , all independent, with means , and . The tails are regularly varying: for ,
with slowly varying ( for every ). So both periods have finite mean and infinite variance, and the ON-periods have the heavier tail.
To make the source stationary, a delay is used, where is Bernoulli with and have the integrated-tail laws . With the source's activity is
a stationary process with .
The -th model superposes independent copies , where is integer valued, non-decreasing and . The cumulative input is . With the quantile , the fast growth condition is
equivalently . The normalisation and limit constants are
A standard fractional Brownian motion is a mean-zero Gaussian process on with continuous paths and .
If Condition 2 holds, then
In the order of the paper's argument: the mean (p. 27); the covariance decay (2.5) ; Condition 2 (p. 61); the variance asymptotic (7.1) for ; Lemma 13, the one-dimensional limit ; the covariance limit (7.4); and the second-moment bound behind tightness (p. 63). (2.5) and (7.1) are cited by the paper from Heath–Resnick–Samorodnitsky and Willinger–Taqqu–Sherman–Wilson; they are stated here as the paper states them.
Theorem 4 justifies fractional Brownian motion as the model of aggregate traffic from many heavy-tailed sources in a single, simultaneous limit, replacing the iterated limit of earlier work, and it upgrades finite-dimensional convergence to weak convergence of paths. Functionals of the path, such as the supremum of that governs the buffer content of a fluid queue, therefore inherit Gaussian approximations. Together with Theorem 2 it shows that a single growth condition on decides between Gaussian and stable approximations.
The result is proved in the paper; it is not formalized anywhere. A formalization adds a machine-checked statement of the theorem and reusable developments of regularly varying functions, the stationary alternating renewal process, fractional Brownian motion, and convergence in .
The obvious route is a central limit theorem for , a sum of iid bounded terms; but the number of terms and their distribution change with , so one needs a triangular-array limit theorem whose variance condition rests on the exact asymptotic (7.1). That asymptotic in turn needs the covariance decay (2.5) of a single stationary source, which requires renewal theory for the alternating process with infinite-variance periods. Convergence of finite-dimensional distributions alone does not give the theorem: tightness in needs a moment bound on increments that is uniform in for small time lags, which requires Potter-type bounds for the regularly varying function .
atTop on . Each model has its own probability space carrying independent sources; the theorems hold for every such family. Lean's X n, Y n are the paper's , and Lean's sources are the paper's . Time in the normalised process runs over .Telephone call centers are large service systems: hundreds of agents answer callers who wait in a queue and hang up when their patience runs out. Staffing them is a trade-off between the cost of agents and the quality of service, and in large centers both the efficiency (agents busy almost all the time) and the service level (most callers answered almost immediately) can be high at once. Garnett, Mandelbaum and Reiman (M&SOM 4(3), 2002) study the simplest model that captures customer abandonment, the Erlang-A or queue, and derive approximations for it in the regime where the number of agents is large.
Their Theorem 2 is the process-level justification of these approximations: the queue-length process, centred at the number of agents and scaled by its square root, converges to a one-dimensional diffusion. The steady-state performance formulas of the paper (delay probability, abandonment probability, waiting times) are computed from this diffusion and its stationary law.
Timeline.
Fix a service rate . For each the -th system has statistically identical agents, Poisson arrivals of rate , exponential service times of rate , an unlimited waiting room served first come, first served, and exponential patience of rate for every caller. A caller whose wait in queue reaches their patience abandons and does not return. The number of callers in the system, , is a birth–death process on with birth rate and death rate in state . Its initial value is an arbitrary random variable.
The traffic intensity is . The centred and scaled process is
When it counts waiting callers and when it counts idle agents, both in units of .
For and , the drift is the piecewise-linear function
and the limit diffusion solves , where is a standard Brownian motion independent of . The noise is additive, so this means: has continuous paths and for all . Below it behaves like an Ornstein–Uhlenbeck process with restraining force , above like one with restraining force .
Assume
and for a probability law on . Then
where is the solution of with , and this solution is unique in law.
On every probability space with a standard Brownian motion and an independent initial value , the equation has a solution adapted to , and any two solutions with the same and initial value are indistinguishable.
The infinitesimal expectation and variance of at the point , as displayed on p. 224, satisfy
The result. Theorem 2 is the basis for the paper's QED (quality- and efficiency-driven) approximations , which give explicit formulas for the probability of delay, the probability of abandonment and the waiting-time distribution in terms of , and . Unlike the case, may be of either sign: abandonment keeps the system stable even when the offered load exceeds the number of agents. The resulting square-root staffing rule , with , is used in call-center practice.
Formalizing it. The result is proved in the paper by Stone's criteria for birth–death processes, with uniqueness of the limit equation delegated to the literature. No many-server process limit exists on Prove2Me or in Mathlib. A formal proof would give the first machine-checked heavy-traffic process limit for a many-server queue, and the infrastructure (Poisson time-change representation of a birth–death process, path-space weak convergence to a continuous diffusion, well-posedness of a Lipschitz additive-noise SDE) would serve every other diffusion limit in queueing theory.
The infinitesimal-moment computation is elementary; it identifies the limit but does not prove convergence. The hard step is the passage from generator convergence to weak convergence of processes on : tightness of in the Skorokhod space, which needs control of the jumps (of size ) and of the unbounded state space, and identification of every limit point as a solution of the equation, which needs uniqueness of the limit. A pointwise limit of the drifts at each fixed is not enough: the convergence has to be controlled locally uniformly along the paths. A finite-dimensional limit at fixed times is weaker than the theorem.
IsBrownianReal with every path continuous and every coordinate measurable. is independent of , which is implicit in the paper. The goal asserts existence of a solution with and uniqueness of its law; dropping the uniqueness clause, fixing to a point mass, restricting to , , , or the stationary case is a different theorem.Contributions welcome: a Poisson time-change existence theorem, tightness criteria in , well-posedness of Lipschitz SDEs with additive noise, and the martingale-problem approach to identifying limits.
A simulation metamodel is a cheap surrogate for an expensive stochastic simulation: after running the simulation at a few design settings, one predicts the mean response at settings never simulated. Kriging, the interpolation method of geostatistics and of the design and analysis of computer experiments (DACE; Sacks, Welch, Mitchell and Wynn 1989; Santner, Williams and Notz 2003), treats the unknown response surface as a realization of a random field and predicts by the best linear predictor. Kriging was developed for deterministic computer codes, where an observation is the exact response. A stochastic simulation returns the response plus sampling noise, and the noise may be correlated across settings when the experimenter uses common random numbers (CRN).
Ankenman, Nelson and Staum, Stochastic Kriging for Simulation Metamodeling (Proc. 2008 Winter Simulation Conference, pp. 362–370), extend kriging to this setting. The mission formalizes §2 of that paper: the form of the optimal linear predictor, called stochastic kriging, and the formula for its mean squared error, which shows how much the simulation noise costs. The source used throughout is the WSC 2008 proceedings paper, not the later Operations Research 58(2) 2010 article, whose numbering differs.
Fix a probability space and a set of design settings . On replication at setting the simulation outputs (display (3), with constant trend)
The constant is the overall mean. is a mean-zero random field, the extrinsic uncertainty imposed by the modeller. is mean-zero sampling noise, the intrinsic uncertainty of the simulation; its variance may depend on , and noises at different settings may be correlated (CRN). All of these have finite second moments, and the field is uncorrelated with the noise.
An experiment design runs replications at each of design points . The data are the sample means (4)
and the target at a point is the noise-free response .
Write . Then is the matrix of these covariances at the design points, is the vector , and is the covariance matrix of the averaged noises . A linear predictor (5) is with arbitrary weights ; its mean squared error is . The optimal MSE is the infimum of this quantity over all weights.
There is a rule , assigning a positive definite matrix to every pair of positive definite matrices, such that in every model as above with and , and at every ,
The bracket is the usual kriging MSE. The goal also states that strictly exceeds it whenever . The matrix is existential and depends only on the two covariance matrices, not on .
If , the stochastic kriging predictor
is of the form (5), attains the smallest MSE among all predictors of that form, and is the only one that does.
Display (7) quantifies the price of simulation noise. With exact observations the best achievable error is the kriging MSE; with noisy observations it is larger by a positive definite form in the cross-covariance vector. Every point that is correlated with the design therefore loses accuracy. The two examples make this concrete. In (10) the MSE increases with the intrinsic correlation , which is why the paper concludes that common random numbers, a standard variance-reduction device for comparing systems, do not help prediction. Display (14) is the baseline against which the paper measures the cost of estimating the noise variance. The conditional-expectation statement shows that under Gaussian assumptions stochastic kriging is optimal among all predictors, not only linear ones.
The results are classical in substance: they are the best-linear-prediction formulas of second-order random-field theory, applied to data whose covariance is . The paper states them without proof ("we can show"). No machine-checked version exists. Formalizing them yields a reusable, measure-theoretic best-linear-predictor theorem for random vectors defined from a model rather than postulated, together with the Loewner-order fact behind the positive definiteness of .
The algebra is short; the difficulty is in deriving the second-moment structure from the model, not assuming it. The covariance of must be computed from the sample-mean definition, using bilinearity of covariance over finite sums of square-integrable variables, and shown to equal . The cross-covariance with must be shown to equal . The MSE of an arbitrary affine predictor then has to be written as a quadratic in , and its infimum identified.
A first idea is to take "a random vector with mean and covariance " as the hypothesis. That proves a different, more abstract statement and leaves the model's content unproved.
For the second line of (7), the positive definiteness of does not follow from a scalar argument. It is a matrix inequality, for , and it fails without : when the two lines coincide.
X; design points are x : Fin k → X, so the paper's index is i.val + 1. Replication is index j - 1 of a sequence ε : ℕ → X → Ω → ℝ.covariance. The optimal MSE is an infimum over all of , with no unbiasedness constraint and no sign constraint.Infrastructure needed and reusable beyond this mission:
Contributions to any of these are welcome.
Stochastic simulation models of queues, supply chains and manufacturing systems are often too slow to run at every input setting of interest. A metamodel fitted to a moderate number of simulation runs then stands in for the simulation, for instance inside an optimization or a sensitivity analysis. Kriging, developed in geostatistics and in the design and analysis of deterministic computer experiments (DACE), predicts an unknown response surface by treating it as a realization of a Gaussian random field. Deterministic kriging interpolates its data exactly, which is wrong for stochastic simulation, where each run returns the response plus sampling noise.
Ankenman, Nelson and Staum's stochastic kriging separates the two sources of uncertainty: the extrinsic uncertainty of the unknown surface and the intrinsic uncertainty of the simulation output. Its optimal predictor requires the intrinsic noise variances, which are never known in practice and are replaced by sample variances computed from the same replications. This mission formalizes the paper's first key result: this plug-in step introduces no prediction bias.
The source is the Winter Simulation Conference 2008 proceedings version of the paper (pp. 362–370). The later Operations Research 58(2) (2010) article numbers its results differently and is not the reference here.
Fix a probability space and design variables . On replication at setting the simulation returns
where is a constant trend, is a mean-zero random field on (the unknown surface) and is the noise of replication . The quantity to predict at any point , simulated or not, is the noise-free response .
An experiment design is a list of pairs , , with distinct design points and replications at . The data are summarized by the sample means , collected in the vector , and the sample variances
The extrinsic covariances are the matrix and the vector .
Assumption 1. is a stationary Gaussian random field: all its finite-dimensional laws are multivariate normal with mean , the covariance is with and , and the covariance matrix at finitely many distinct points is positive definite. At each design point the noises are i.i.d. with ; noises at different design points are independent (no common random numbers); and the whole noise family is independent of .
The intrinsic variance at a design point is estimated by , giving and the plug-in stochastic kriging predictor
Under Assumption 1, with replications at every design point, the prediction error is integrable and
Theorem 1 says that the practitioner's shortcut, estimating the noise variances from the replications and plugging them into the optimal predictor, keeps the predictor unbiased; the cost of not knowing the intrinsic variance is paid entirely in mean squared error. This is what makes the paper's subsequent comparison of the plug-in MSE with the known-variance MSE the right measure of the penalty for estimation.
None of these statements has a machine-checked proof, and Mathlib has neither the chi-squared law of the normal sample variance nor the independence of the normal sample mean and sample variance. A complete development produces these classical facts of normal sampling theory for the first time in Lean, together with a reusable model of noisy observations of a Gaussian random field.
The predictor is a nonlinear function of the data: its weight vector is random and depends on the same replications as . Linearity of expectation therefore does not apply directly: the obvious argument, which treats the weights as constants, fails, and the dependence between the estimated variances, the sample means and the field has to be controlled exactly. The joint independence structure of Assumption 1 — across replications, across design points, and between noise and field — is load-bearing; a weaker pairwise or pointwise independence does not suffice. Integrability of the error must also be established, since the weights depend on random variances.
Design points are indexed by Fin k (the paper's is i.val + 1) and lie in EuclideanSpace ℝ (Fin d); replication of the paper is index j - 1 of a sequence, so sums run over Finset.range. The field is M : EuclideanSpace ℝ (Fin d) → Ω → ℝ with Mathlib's IsGaussianProcess; covariances are ProbabilityTheory.covariance; stationarity is with . The noise law is HasLaw … (gaussianReal 0 (V (x i))); independence is one iIndepFun over the family indexed by Fin k × ℕ plus one IndepFun between that whole family and the whole field. The variance function is ℝ≥0-valued with assumed; replication counts satisfy wherever appears and where only means appear. The chi-squared law is gammaMeasure (ν/2) (1/2).
The covariance quantities and in (13) are the true ones; only is estimated, and is built from the same replications as . A formalization in which is deterministic or independent of the data, in which the matrix may be singular (Lean's Matrix.inv returns there, reducing the claim to ), or in which the expectation is asserted without integrability, would trivialize the goal and is ruled out: positive definiteness of at distinct design points is part of Assumption 1, and integrability is part of the conclusion. may coincide with a design point.
A complete development needs: the law of linear images of independent Gaussian vectors; independence of the sample mean and the residual vector for i.i.d. normal samples (Cochran's theorem); the chi-squared law of the normal sample variance; the strong law of large numbers for the sample variance; and a measurability and boundedness argument for the random weight vector. The normal-sampling results are reusable well beyond this mission and are welcome as separate contributions.
A correlated equilibrium (Aumann 1974) is a probability distribution over strategy profiles of a game such that no player gains by deviating from a recommended strategy, given the recommendation. It is the solution concept of choice when players can condition on common signals, and its set is a convex polytope defined by linear inequalities, which makes it computationally tractable in a way that Nash equilibrium is not. A natural question in learning in games is whether simple adaptive behaviour by individual players, each using only their own payoffs and the observed history, leads to it.
Hart and Mas-Colell (2000) answer this with regret matching: each player switches away from their last action with probabilities proportional to the regret for not having played other actions in the past. They show that if every player uses this rule, the empirical distribution of play converges almost surely to the set of correlated equilibria. The procedure and its analysis became standard references for no-regret learning, internal (swap) regret, and the counterfactual-regret-minimization algorithms used in large imperfect-information games.
Timeline. Foster and Vohra (1997) obtained convergence to correlated equilibria by calibrated forecasting. Fudenberg and Levine (1999) gave conditionally consistent procedures with the same consequence. Hart and Mas-Colell (2000) gave the regret-matching procedure (2.2), in which a player's probabilities depend on regrets only, together with a Blackwell-approachability variant (their Theorem A, the subject of the companion mission 2 of this series).
A finite game has a finite set of players , a finite strategy set for each player, and payoffs on . A probability distribution on is a correlated -equilibrium if for every player and all
a correlated equilibrium is the case .
The game is played at , producing a history . For the regret of player is
the average gain player would have had by playing every time they played . Fix with for every , where and . Under regret matching (2.2), if player last played , then at they play each with probability and repeat with the remaining probability; the first-period mixed actions are arbitrary, and given the history the players randomize independently. The empirical distribution of play is .
Almost surely, converges to the set of correlated equilibria:
This is convergence to a set, not to a point; the paper notes that need not converge.
They follow the Appendix proof:
The squared distance satisfies a block recursion (M1). The cross term is rewritten through the transition probabilities (M2) and compared with a stationary auxiliary process (M3–M5). It then factors into a difference of consecutive matrix powers (M6), which is small (M7). This gives
Along this gives a.s. (M9–M10), and then a.s. (M11). A companion item states the strong law for dependent variables that M10 cites.
The result. The Main Theorem shows that correlated equilibrium is reached by uncoupled play: each player needs only their own payoff function and the history of play, and nothing about the others' payoffs. Steps M10–M11 give more than the goal, namely that every player's internal regrets vanish almost surely. The procedure underlies later work on swap regret, calibrated learning and regret-minimization algorithms for extensive-form games.
Formalizing it. The result is proved in the paper. As far as a search of the platform and the local index shows, it has no machine-checked proof. The mission asks for one, following the paper's eleven steps. Several pieces are general and reusable: a bound on consecutive powers of a stochastic matrix with positive diagonal (LEMMA, proof of M7); a perturbation bound for multi-step transition probabilities (LEMMA, proof of M4); and a strong law of large numbers for martingale differences with general normalizing sequences, which Mathlib does not have in this form.
The natural approach is Blackwell approachability: show that the expected regret vector moves toward the nonpositive orthant in one step. It fails here. The one-step condition holds when a player uses an invariant distribution of , which is the procedure of Theorem A, but regret matching uses a row of instead. The cross term of the one-step recursion therefore does not vanish.
The proof has to work over blocks of periods. Within a block the players' choices are not independent given , because the transition probabilities change with time. The paper therefore compares the play with a process whose transitions are frozen at time . The matrix-power estimate cannot use convergence of , since only the diagonal of is known to be positive and may be reducible or periodic in its off-diagonal structure. The block length must also balance the errors and , which is why the subsequence appears.
Players form a Fintype ι, strategies form Fintypes S i, each nonempty, and a profile is a function ∀ i, S i. is Mathlib's stdSimplex. Time is 0-based: play τ is , and a history is a tuple Fin t → ∀ i, S i. Regrets, , and are deterministic functions of a finite history. Every statement has , because the Lean value at is a default. A play of a behaviour profile on a probability space (IsPlay) is a sequence of profile-valued random variables with measurable level sets whose conditional law given any history of positive probability is the product of the players' mixed actions. Statements quantify over every probability space carrying a play, and conditional quantities given assume . The auxiliary -process is encoded by its explicit law, a power of the product transition matrix. The paper's (footnote 34) is a constant chosen after the game, and and before the initial play, the probability space and the play. Distances on are sup distances.
The hypotheses are exactly footnote 5's: and , with one for all players. The goal requires every player to follow (2.2). If other players may play arbitrarily the statement is false (§4(d)), so IsPlay constrains all of them. The goal is stated with an existential correlated equilibrium at distance less than , not with a distance to a possibly empty set, so no encoding makes it vacuous.
Disclosed choices:
Contributions are welcome at every milestone. The two LEMMAs and the strong law are self-contained and independent of the game.
A dynamic programming problem in Blackwell's sense describes a controller who observes the state of a system, picks an action, collects a return, and watches the system move at random to a new state, forever. Blackwell treated the discounted case, with a bounded return and a discount factor below one (Blackwell 1965), and the positive bounded case. Strauch's paper (Strauch 1966) studies the third case, the negative case: the return is non-positive and there is no discounting. Equivalently, a non-negative cost is minimized over an infinite horizon. This is the setting of stochastic shortest-path, optimal stopping with costs, and many inventory and search problems in which the total cost may be infinite.
In the negative case two standard tools of the discounted theory break down. An optimal policy need not exist, and the natural algorithm, value iteration from the zero function, need not converge to the optimal return. Strauch's §9 gives a condition on the action sets, essential finiteness, under which both are restored. The introduction (p. 872) summarizes the finite case: "In the negative case, … if A is finite, there is an optimal policy (Section 9)." In the later terminology of Bertsekas and Shreve (1978), Strauch's negative case is their positive-cost model, for which value iteration from zero is known to require such finiteness or compactness conditions.
The state space and the action space are non-empty Borel sets. The law of motion is a probability measure on depending measurably on . The return , collected when action is taken in state and the next state is , is a Borel function with and for every .
A policy chooses the th action at random, with a law depending measurably on the whole history . A Markov policy is a sequence of measurable maps ; the stationary policy uses one map at every stage. The expected return from the initial state is
the sum of the expected stage returns. The optimal return is , over all policies, and is optimal if at every state.
For a measurable and a non-positive Borel , the operator of is
and the operator of a Markov policy is , with the operator of . Value iteration is the sequence .
Actions and are equivalent at if and . is essentially finite by if there is a partition of into Borel sets such that for every action is equivalent at to one of . A finite is essentially finite by any Markov policy whose first rules are the constant rules.
If is essentially finite by and is the operator of , then
Both parts are kept together, as printed. The goal fixes no constants and no rate.
where is the set of -generated policies (each rule equal to on the th piece of a Borel partition). 2. Proof of Theorem 8.4, p. 887. pointwise. 3. Proof of Theorem 9.1, p. 887, first step. Under essential finiteness, is non-increasing and for every policy . 4. Proof of Theorem 9.1, p. 887, second step. Under essential finiteness, .
Inside the proof of Theorem 9.1 the paper writes for ; the mission writes for it and reserves for .
An optional extra item states the introduction's special case: if is finite, an optimal policy exists (§1, p. 872).
Theorem 9.1 gives, in the negative case, both a computational and an existential conclusion. Value iteration from zero computes the optimal return, so the optimal total cost of an essentially finite problem is the limit of the optimal finite-horizon costs. An optimal policy exists and can be taken stationary, so the controller needs only a single measurable decision rule. Without a hypothesis of this kind neither conclusion holds in the negative case; Example 6.1 of the paper exhibits a problem where the limit of value iteration, the best return among generated policies, and the best stationary return all differ.
The result is proved in the paper. What the mission adds is a machine-checked statement and, eventually, proof of it on general Borel spaces, with the return allowed to equal . Blackwell's discounted analogue already has a published statement on Prove2Me (DiscountedDP.Stationary.theorem7b_optimal_stationary), in a bounded-return model; the negative case is a separate statement in a separate model. No formalization of the negative case is known to exist.
The discounted proof rests on the contraction property of in the supremum norm, and in the negative case that property is missing: returns are unbounded below and there is no discount. The obvious argument, " decreases to some , and is the optimal return because finite-horizon play approximates infinite play", fails at the second step. The finite-horizon optimum can stay strictly above the infinite-horizon optimum, because a policy can postpone a cost beyond every fixed horizon; this is exactly the gap Example 6.1 exhibits. Closing it needs the essential finiteness of the actions together with the reduction of arbitrary policies to Markov ones (milestone 2), whose proof in the paper passes through the measurable-selection results of §7–§8.
EReal and are computed as minus the lintegral of the loss , which keeps the value . is the sum over stages of the expected stage loss, which equals the paper's integral over futures by monotone convergence.EReal.Policies, Markov policies, stationary policies and -generated rules come from the published definitions DiscountedDP.Stationary.Model, .Return and .Operators; the negative model is defined locally because the published Problem has a bounded return and a discount factor below one. A complete development needs the Ionescu-Tulcea construction of the history laws (already encoded as iterated composition products), monotone convergence for kernels, the measurable-selection step behind milestone 2, and a pigeonhole argument over the essentially finite action classes. The model and the Markov-reduction milestone are reusable by the other missions of this series. Proofs of any milestone, and alternative routes to milestone 2, are welcome.
Queueing models often represent work arriving to and leaving a server by a real-valued input path. The resulting workload cannot fall below a barrier. Functional limit theorems describe what happens to such paths under scaling, but a limit for the input path is useful only when it can be carried through the workload transformation. Ward Whitt’s 1980 paper studies several path transformations that occur in stochastic-process limits and states conditions under which their limits can be computed in Skorohod topologies. Section 6 treats the running supremum and a reflecting barrier, including paths with a linear drift that changes with the scaling index. This mission formalizes the three-regime reflection result, Theorem 6.4, and the source results on its dependency path. Whitt (1980)
The result is already proved in the paper. Its formal Lean statement remains an open proof target here. The mission is therefore concerned with formalizing the known theorem, including its exact jump conditions and convergence modes, rather than proposing a new queueing claim. Whitt (1980), pp. 80–81
A càdlàg path on a real interval is right-continuous and has a limit from the left wherever approaches a time from the left. The collection of such real-valued paths is . For a compact interval , the distance between and allows an increasing homeomorphism of time and measures the larger of its distance from the identity and the uniform distance between and . On a general interval, convergence is specified by restrictions to compact subintervals whose endpoints are continuity points of the limit or endpoints of . The paper uses complete separable metric spaces for general path-space results; Section 6 specializes to real-valued paths and intervals with as a closed left endpoint. Whitt (1980), pp. 70, 80
For and , define the running supremum and running infimum . The reflecting-barrier map is . This is the paper’s definition: it subtracts the full running infimum. The identity path is , and denotes the zero path. A path has no positive jumps if for each in ; no negative jumps reverses that inequality. Whitt (1980), pp. 80–81
The goal is Theorem 6.4. Suppose in and . Its three conclusions are
Here means uniform convergence on every compact subinterval. The goal keeps all three drift regimes together, as the printed theorem does. Its milestones are the finite-partition fact cited from Billingsley, the interval-splitting Lemma 2.2, continuity of addition at limits without shared discontinuities in Theorem 4.1, the running-supremum inequality in Theorem 6.1, the three-regime supremum theorem 6.2, and the paper’s explicit claim that is -continuous. Whitt (1980), pp. 71, 79–81
The theorem specifies which output path appears after reflection as the linear centering changes. Finite drift leaves a reflected limit with drift included; large positive drift leaves the centered input limit; large negative drift drives the reflected path uniformly to zero when upward jumps of the limit are excluded. The distinction between and the stronger compact-uniform mode in the last case is part of the result. These statements make the paper’s barrier transformation usable when an input-process limit is already known. Whitt (1980), Theorem 6.4
A completed formal development would establish reusable path-space components: a precise convergence interface for real intervals, a theorem about addition with disjoint discontinuities, and continuity properties of running extrema and reflection. The present Lean items state these results and compile with proof placeholders. No machine-checked proof of these mission theorems is claimed here. The milestone list follows the claims Whitt states or cites, so later proofs can be attached to the same mathematical targets. Whitt (1980), §§2, 4, 6
A uniform estimate alone does not establish a limit: separate paths may converge using different changes of time, and addition can fail when the limiting paths jump together. Whitt’s Theorem 4.1 gives continuity precisely at pairs with disjoint discontinuity sets. In the reflection theorem, a linearly growing drift also changes which extrema matter, and the sign of a jump decides whether the large-drift conclusion can hold. The negative-drift conclusion asks for compact-uniform convergence, which is stronger than merely retaining convergence. These are real constraints on the statement; dropping a jump condition or replacing by changes the theorem. Whitt (1980), pp. 78–81
Paths are total functions , but only their values on the stated interval count. The Lean definitions require càdlàg membership of both prelimit and limit paths in each convergence claim. A time change on is strictly increasing, continuous, and onto; this represents the paper’s increasing homeomorphism. Uniform and distances take values in the extended nonnegative reals, so an unbounded supremum cannot silently become zero. Continuity points use continuity within , and the discontinuity set likewise contains only points of . Sequential convergence is used because the paper’s spaces are metrizable. These choices encode the paper’s path-space conventions rather than imposing conditions on values outside . Whitt (1980), §§2, 4, 6
The compact form of Theorem 6.1 uses metric (2.1); the noncompact metric (2.2) is outside this mission’s definition layer. Theorem 4.1 retains the paper’s complete separable metric-space setting and metric compatibility of addition. Its measurability clause is omitted: this mission does not construct the Borel measurable space of , and a product measurable structure on all total functions would express a different claim. The source’s is used on both prelimit and limit paths; it is not replaced by a clipped running infimum. Whitt (1980), pp. 70, 78–81
The definition layer, the addition theorem, the running-extremum results, and the barrier continuity statement are welcome proof targets. The theorem’s centered-path hypothesis remains a genuine convergence assertion, and the jump conditions apply to the limit path only. A vacuous convergence predicate or an independently assumed conclusion would not represent this mission’s goal.
A processor can save energy by running slowly when work is light, but a deadline may force it to run faster. Yao, Demers, and Shenker formulated this tradeoff as an offline and online scheduling problem for a variable-speed processor in their 1995 FOCS paper. Their Average Rate Heuristic (AVR) uses only each job's arrival, deadline, and required work to set speed. This mission formalizes their quadratic-power analysis: AVR's worst-case energy is at least four and at most eight times the minimum possible energy. The authors prove these bounds in Theorem 2, rather than an exact value.
The question matters when an online scheduler must choose speed before seeing later jobs. Deadline feasibility alone does not measure energy: processing the same number of cycles at twice the speed for half as long can cost more when power grows superlinearly. The paper's model isolates that dependence in a power function , so the competitive guarantee measures the energy price of AVR's speed choices. The initial motivation, model, and heuristic are in §§1–4 of the paper.
Fix a nondegenerate time window . A finite job instance assigns each job an arrival time , deadline , and nonnegative required work in CPU cycles. Every job window lies inside . A schedule has nonnegative processor speed and selects at most one job at each time. Speed and job selection are constant between finitely many breakpoints. The schedule is feasible if each job receives its full work inside its own window:
For a power function , its energy is . An optimal schedule minimizes this quantity among feasible schedules. These definitions follow §2, p. 375. The intensity of an interval is the total work of jobs whose full windows it contains, divided by . An interval with maximum intensity is critical; Theorem 1 identifies the processor speed on that interval in an optimal schedule §3, p. 375.
Each job's density is , extended as a step function equal to on and zero elsewhere. AVR runs at speed and chooses the earliest-deadline available job. For quadratic power, its energy is
The competitive ratio is the least upper bound of over instances, where is the least feasible energy §4, p. 376, Eq. (2).
The goal is the paper's Theorem 2, p. 381:
The upper bound compares AVR with every feasible schedule. The lower bound says that every constant strictly below four is exceeded by the AVR-to-feasible-energy ratio on some instance. This formulation does not claim that one finite instance attains four.
The milestone path follows the paper: Theorem 1 characterizes optimal speed; Lemma 5.1 reduces to jobs of type A or B; Eq. (5) splits their costs; Lemma 5.2 and Eq. (7) control the A contribution; Lemmas 5.3–5.6 reduce the analysis to canonical instances; Lemma 5.8 supplies a matrix bound; Lemma 5.7 gives and ; Example 2 approaches the lower constant. These statements and their order come from §5, pp. 378–381. The paper also states a higher-power result, Theorem 3, for real :
That result is a companion item. The extended abstract leaves its full proof to a longer paper §6, pp. 381–382.
The upper bound guarantees that AVR's energy is controlled by a fixed multiple of the offline optimum for every finite job set, even though AVR sets speed from individual job densities. The lower family rules out a guarantee below four for this heuristic. Together they delimit the performance of AVR under quadratic power; they do not give its exact worst-case ratio. The A/B reductions and the tree-induced matrix estimate are useful mathematical interfaces for later analyses of interval-structured schedules.
The paper proves Theorem 2 in the mathematical sense. This mission supplies machine-checkable statements and definitions, with proofs left open for solvers. Closing it requires formal proofs of the reduction steps, the matrix estimate, and the limiting example, plus an explicit connection from the optimal-schedule analysis to comparison with every feasible schedule. No completed Lean proof is claimed here.
The simple calculation exposes overlap between job windows but does not say how that overlap compares with an optimal schedule. An optimal schedule may run jobs in a different order and may preempt them. The paper therefore changes the instance while preserving the optimal speed profile: it first separates cumulative execution into two types, then reduces to single execution intervals and specially aligned, nested windows. The matrix inequality controls the resulting expression. A pointwise comparison of AVR speed with optimal speed cannot replace these reductions, because an optimal schedule can concentrate work on critical intervals while AVR spreads each job's density across its entire window §5, pp. 377–381.
Jobs use Fin n, allowing the empty instance. The instance requires , , containment in the window, and . A schedule uses real-valued speed and an optional job label; none denotes no assigned job. Its piecewise-constant requirement is witnessed by finitely many increasing breakpoints. Values at breakpoints are unrestricted by the piecewise-constant clauses, and speed comparisons in the theorems are almost-everywhere statements. Job windows are closed, as printed; endpoints do not affect the integrals. A schedule may have positive speed while no job is assigned, since the source does not equate idleness with zero speed.
Every energy expression is a real interval integral. The schedule conditions ensure the integrands in theorem hypotheses are piecewise constant away from finitely many points. Density denominators are positive. An execution-speed quotient for a zero-work job can have zero denominator, in which case Lean returns zero; such a job contributes no executed work. The goal uses quantified comparisons with feasible schedules rather than a real infimum, and Lemma 5.6 uses all upper bounds on a nonempty canonical family rather than a real supremum. The lower bounds quantify over every smaller constant, avoiding a false attainment claim. These choices guard against default values for empty or unbounded extrema.
Theorem 1's printed convexity hypothesis is strengthened to strict convexity and nondecreasing power on nonnegative speeds: its stated speed uniqueness fails for a linear power function, and a decreasing power function rewards idle speed. This repair is explicit in that item's description. Existence of a quadratic optimum is included as a milestone from the algorithm of §3, although it is not a separately numbered theorem. Example 2 includes the variable exponent , the limiting ratios at and , and an eventual upper bound of four across the family. The A-job order resolves exact ties by index. For canonical and tree-induced nesting, intervals that meet only at an endpoint count as disjoint; this admits the paper's displayed four-interval matrix.
The development needs Mathlib's real interval integrals, finite sums, measures of intervals, matrix eigenvalues, and real-power limits. The finite schedule model, canonical-instance data, and tree-induced matrix interface can be reused beyond this particular ratio bound. Contributions may establish these interfaces' elementary properties, the paper's milestone theorems, or independent proofs of the goal, provided they preserve the stated job and schedule classes.
Functional limit theorems describe the behavior of entire time-indexed paths under scaling. In queueing and other stochastic models, a path of departures, workload, or accumulated input may be related to another path by reversing a finite observation window. To carry a limit theorem through that change of viewpoint, one needs to know how reversal acts on the topology of the path space. Ward Whitt's 1980 paper studies composition, reflection, first passage, and time reversal as maps that transfer functional limit theorems to derived processes (Whitt 1980).
The time-reversal result is a precise metric statement. Ordinary reversal preserves the Skorohod distance exactly. A version shifted to begin at the group identity satisfies a bound with constant two. These facts give continuity and, when the random paths satisfy the hypotheses, make reversal available to the continuous mapping theorem. Whitt's introduction explains how deterministic path continuity connects to stochastic-process limits (Whitt 1980, pp. 67–69).
Let be a complete separable metric group, written additively, with identity and metric . The metric is translation invariant: moving both points by the same group element leaves their distance unchanged. Let contain the càdlàg paths , meaning paths that are right continuous and possess left limits. Section 8 additionally requires , so the terminal value agrees with the value approached from earlier times. Let . These are the spaces Whitt fixes for time reversal (Whitt 1980, p. 83).
The uniform distance is . A time change is an increasing homeomorphism of onto itself; is the identity time change. The distance used in the paper is
Two paths may be close when their values can be matched after a small distortion of time. This is the paper's equation (2.1), rather than an unspecified equivalent metric (Whitt 1980, p. 70).
The reverse-time map reads the left limit at the reflected time:
The left limit is essential: the direct value places jumps on the wrong side and generally does not give a right-continuous reverse path. The terminal convention gives , so . Whitt also uses the reflected time change in the proof (Whitt 1980, pp. 83–84).
The goal is Whitt's Theorem 8.1. For every ,
The second inequality also applies when both paths lie in , since . The constant is the paper's printed constant, not a parameter to optimize in this mission (Whitt 1980, Theorem 8.1, p. 83).
The milestones record four claims from the theorem's proof: reversal preserves its path spaces and has inverse behavior on its natural domains; reflected time changes stay in ; reversal obeys exact and bounded uniform-distance relations; and reversal interacts with time changes through . Their descriptions reproduce the printed proof sentences. The proof calls the time-change cost a “minimum” once, although equation (2.1) and the displayed calculation use a maximum. The formal target follows equation (2.1) (Whitt 1980, pp. 70, 84).
An isometry preserves every distance, so ordinary reversal preserves convergent and Cauchy sequences in this metric. The bound for makes shifted reversal Lipschitz and therefore continuous. A functional limit theorem for input paths can then be translated into one for the corresponding reversed paths whenever the path-space hypotheses hold. The result is already proved in Whitt's paper; the open work here is a machine-checked development of its definitions, supporting claims, and metric theorem.
Formalizing the result also creates reusable interfaces for endpoint-constrained càdlàg paths, left-limit reversal, uniform path distance, and reflected time changes. Those interfaces may support later statements about reversed stochastic models. This mission does not assert weak convergence of probability laws or Borel measurability; those would require a separate measurable-space development for .
The immediate idea does not preserve càdlàg paths at jumps: a right-continuous jump becomes left-continuous. The correction uses left limits, but endpoint behavior then matters. Without , the shifted reverse path need not start at the identity. The assertion also concerns an infimum over all allowed time changes, so a uniform-distance statement alone does not establish the theorem. These are the points at which reflection of the time axis becomes a claim about the precise path-space topology (Whitt 1980, pp. 83–84).
Lean represents paths as total functions ; all path conditions, metrics, and equality claims read only . Càdlàg membership requires right continuity and left limits within the interval, with included in . Completeness and separability are explicit because the paper calls a complete separable metric space. The additive metric group is represented by an additive commutative group with an explicit translation-invariance hypothesis. This chooses the commutative reading exemplified by ; the paper uses additive notation but does not separately state commutativity.
The paper's is encoded by strict increase, continuity, and surjectivity on , which characterize increasing homeomorphisms there. The paper's is equation (2.1) on both sides of the goal. Lean uses extended nonnegative distances for and , avoiding the default value a real supremum can assign to an empty or unbounded set. The claims do not become trivial by dropping membership: it is an explicit hypothesis, and the zero path over satisfies it. A local, sorry-free check confirms that instance. Two easier statements are excluded on purpose: the goal is stated for the distance , not the uniform distance , and reads the left limit , not the value .
The proof's first sentence says the maps are one-to-one and onto. The map forgets an additive offset and is not injective on all of ; the formal milestone expresses involution for on and for the restriction of to . One identity printed for with also holds for every ; the formal milestone uses that broader domain and says so in its item description. Contributions are welcome for the left-limit and time-change infrastructure as well as the four listed statements and the goal.
A finite Markov decision process is usually solved under one of two criteria: the expected total discounted reward, for a fixed interest rate, or the long-run average reward. Neither is satisfactory when the interest rate is small and not known precisely. Blackwell (Blackwell 1962) showed that some stationary policy is optimal for every discount factor close enough to one, and that the average-reward criterion cannot tell apart policies with the same gain but very different transient rewards. Veinott's 1969 paper interpolates between these two: it introduces a hierarchy of -discount optimality criteria, indexed by , each more selective than the previous, and characterizes the stationary policies that meet each level through the Laurent expansion of the discounted return in the interest rate.
Timeline. Blackwell (1962) introduced the expansion of the discounted return near to first order and the criteria now called and discount optimality. Veinott (1966) gave a policy improvement method for the bias () criterion. Miller and Veinott (1969) gave the full Laurent expansion and a policy improvement algorithm for Blackwell optimality in the stochastic case. The present paper (1969) extends this to substochastic transition matrices and to negative interest rates in the transient case, defines the criteria, and proves Theorem 4, the subject of this mission.
There are finitely many states (the paper's ); in each state a finite nonempty action set . Action in state earns and leads to state with weight , where (the remaining mass is the probability of stopping). A decision rule picks one action per state; and are its reward vector and substochastic transition matrix, . A policy is a sequence of decision rules, is a stationary policy, and .
For an interest rate and , the discounted return is
For a substochastic , is the Cesàro limit of its powers and its deviation matrix.
A policy is discount optimal if, componentwise,
is the set of with discount optimal, and . The sign (interest rate approaching zero from below) is considered only in the transient case, where converges for every .
The Laurent coefficients of are and , ; with and , otherwise, the test quantities are
is the matrix with columns , and , where means that the first nonzero entry of every row of is positive and .
For and :
The two halves bracket between two finitely checkable conditions.
In the order the proof uses them: the Cesàro limit and (15); Lemma 5 (the reduced resolvent); Theorem 2 (the Laurent expansion ); Lemma 7 ( nonnegative, positive diagonal, nonsingular for small ); Theorem 3 (the expansion of ); (30)–(31) (the comparison identity); Lemma 8 (the expansion of the test quantity); Lemma 9 (the coefficient identity); the nonemptiness of ; the characterization ; Theorem 5 (lexicographic improvement).
Theorem 4 turns a criterion stated through limits over all, possibly non-stationary, policies into a finite test on one-step switches. It is what lets the policy improvement method of Miller and Veinott stop early when only an discount optimal policy is sought, rather than an (Blackwell) optimal one, and it recovers Blackwell's algorithm for and Veinott's 1966 algorithm for as the cases . The -discount hierarchy is the standard framework for sensitive optimality in Markov decision processes and underlies the average-overtaking and bias criteria used in later work.
The results are proved in the paper (Theorem 3 and Lemma 8 by reference to Miller–Veinott). None of them is formalized: the platform has the Cesàro limit matrix and the deviation matrix as definitions (from Blackwell 1962), and an open statement of their basic properties for stochastic matrices only. This mission adds the substochastic matrix theory of §3, the Laurent expansion of discounted returns with Veinott's normalization, and the lexicographic characterization of discount optimality.
The definition of compares with every policy, and the comparison is a liminf of a scaled difference of infinite series. The obvious route, comparing Laurent coefficients, applies only to stationary policies, whose returns have Laurent expansions; reducing the comparison with arbitrary policies to stationary ones requires the existence of an discount optimal stationary policy, which is a separate existence theorem. The second difficulty is that may be singular or zero and the chain may have several recurrent classes: Lemma 7 is what replaces an analysis of the chain structure in the inductive step of the proof.
Lean 4 with Mathlib, namespace VeinottSensitiveDP.Sensitive. States form a nonempty Fintype; each state has its own finite nonempty action type A s; policies are sequences ℕ → F with π 0 the paper's . All quantities are real. and are the published limitMatrix and deviationMatrix; their properties for substochastic matrices are milestones, not assumptions. is a tsum with Veinott's extra factor ; every theorem about it carries the hypotheses under which the series converges. The spectral radius is that of the complexified matrix. The sign is a real parameter , and statements for assume the transient case. The liminf in (27) is encoded as "for every , eventually ", which is the extended-real liminf. Matrices with columns are functions of an integer column index read on .
A trivializing formalization would define by comparison with stationary policies only, or directly as the lexicographic maximizers of ; here is defined by (27) against all policies, and the lexicographic characterization is a milestone.
Contributions welcome: proofs of the matrix results of §3 (reusable for any work on deviation matrices and Laurent expansions of Markov chains), of the Laurent expansions, and of the existence of discount optimal stationary policies.
Demand for many products is not stationary: it rises and falls with the economy, the season, a product's life cycle or a customer's state. Song and Zipkin (1993) (DOI 10.1287/opre.41.2.351) model this by a world-driven demand process: an exogenous Markov chain (the "state of the world") whose current state sets the rate of a Poisson demand stream. The model contains the classical stationary inventory model as the case of one world state, and it is a standard example of a Markov-modulated decision problem in operations research.
For stationary demand with a fixed order cost, optimal policies go back to Scarf (1960) for finite horizons and Iglehart (1963) for the infinite horizon; Veinott (1966) bounded the optimal parameters by quantities computed from the one-period cost alone. This mission formalizes the extension of both results to the fluctuating-demand model (§3.2 of the paper). A companion mission treats the linear order-cost case, in which a world-dependent basestock policy is optimal.
The world is a continuous-time Markov chain on a countable set with generator , , and bounded rates. While , unit demands arrive at Poisson rate ; shortages are backlogged. An order arrives after a random lead time , independent of the world and the demand. The inventory position is on-hand stock minus backorders plus stock on order.
Costs: a fixed cost per order and a unit cost , both paid on arrival; a holding cost rate and a penalty cost rate ; a discount rate . With , the discounted costs are and . If is the demand during a lead time from world state and ,
Uniformization at a rate turns the problem into a discrete-time dynamic program with , and the myopic cost . For a terminal cost the -stage costs satisfy the recursion (10):
where if and . Throughout, Assumption 1, , holds and . The terminal cost is the optimal cost of the linear model (); its is written , and is the smallest minimizer of .
A function is -convex (Definition 2) if for all and all integers . The policy with parameters orders up to when and the world is in state , and does not order otherwise. With the smallest minimizer of and , the paper defines
Let be the smallest minimizer of and the largest with . For every the sequence has limit points; for any choice of limit points , the world-dependent policy with these parameters is optimal for the infinite-horizon discounted problem, and
Lemma 4 (uniform bounds on the iterates); Theorem 3 (-convexity of , and optimality of an rule for each -stage problem); Lemmas 5 and 6 (difference comparisons); Theorem 4 (the bounds above for every ); Theorem 5(a)–(d) (convergence of , , the property of limit points, and the optimality equation (2)).
The result shows that the classical structure survives Markov modulation of demand with an infinite world space and stochastic lead times: a stationary policy whose two parameters depend only on the current world state is optimal over the infinite horizon. The bounds of Theorem 6 locate those parameters in an interval computed from the myopic cost and the linear model alone, uniformly in the horizon.
The results are proved in the paper, except that Theorem 5 refers to Iglehart (1963) and Lemma 4 to Song's thesis. To our knowledge none of them has a machine-checked proof. A formalization would also produce reusable machinery: -convexity on the integers, the Scarf-type inductive argument with a countable world state, and the passage from finite-horizon to infinite-horizon optimality for a nonnegative-cost Markov decision process with unbounded costs.
The one-period cost is unbounded in and the world space may be infinite, so the usual contraction argument for discounted dynamic programs does not apply. Convergence of needs the uniform bound of Lemma 4. Optimality of the limit policy needs a separate argument, because a pointwise limit of rules need not exist: the parameter sequences are only known to have limit points. The lower bounds and hold only because the terminal cost is the linear model's optimal cost, which makes the difference comparisons of Lemma 6 possible; the paper notes that Lemma 6 depends on this choice of .
All definitions live in the namespace SongZipkinFluct.FixedCost. Inventory positions and order-up-to levels are integers. The demand law is defined through uniformization at rate , as an exact series representation of the Markov-modulated Poisson count, and the lead time is a probability law on independent of the rest. The standing conventions , , and are hypotheses of the model. Assumption 1 and are hypotheses of each theorem.
The iterates are defined by the recursion (10), with the minimum written as an infimum over integers . and are the suprema over , which are finite and equal the limits by Lemma 4 and Theorem 3. Every minimizer and every extremal integer (, , , , , , , , ) is passed through its defining property, never through sInf/sSup on . The goal also asserts that all of them exist, so its hypotheses can be met. A limit point of an integer sequence is a value taken infinitely often.
Optimality is over all deterministic history-dependent feasible policies and from every initial state. Costs are valued in , and a policy's cost is the supremum of its finite-horizon discounted costs in the uniformized problem (1). Restricting the comparison to or stationary policies would trivialize the goal and is ruled out. -convexity is the integer version of Definition 2, not convexity over -scalars.
Welcome contributions: -convexity calculus on , convergence of the uniformized demand series, Lemma 4, and an Iglehart-type limit argument for countable-state Markov decision processes with nonnegative costs.
A single stock of one product often serves customers of different importance: emergency and routine orders for spare parts, contract and spot customers, high- and low-priority patients for a blood bank. When stock runs low, the question is not only how much to order but how much of the remaining stock to hand to the less important customers now, and how much to hold back for more important demand that may still arrive. Stock rationing policies answer this question with critical rationing levels: demand of a class is served only while the stock stays above that class's level.
Topkis (1968) studied this problem as a finite-horizon dynamic program with demand classes, nonstationary costs and demands, and an arbitrary degree of backlogging. His Theorem 1 shows that, when each interval has either complete backlogging or none, a policy given by critical levels is optimal. This mission concerns his Theorem 3, which treats the case of complete backlogging: the critical levels of a class do not depend on what happens in the classes below it.
Timeline. Veinott (1965) considered demand classes but imposed the policy with all critical levels equal to . Topkis's 1966 report treated , partially duplicated independently by Evans (1968) and by Kaplan's 1966 report "Stock Rationing", in which, according to Topkis, the result of Theorem 3 was used implicitly. Topkis (1968) extended the analysis to classes and stated Theorem 3 explicitly.
A period is divided into intervals, indexed backwards: interval is followed by further intervals, and interval is the first. There are demand classes; class is the most important. In interval a random demand vector with law and finite means arrives; demands in different intervals are independent. Given the stock and the outstanding demand (backlog plus new demand), the decision is the vector , , of demand left unsatisfied; the stock drops to . A penalty and a holding cost are charged, and the backlog carried into the next interval is , with for complete backlogging. At the end of the period a salvage cost is charged.
The standing assumptions are: convex and continuous on ; convex and continuous on ; convex and continuous on with ; and . The minimal expected cost satisfies the recursion (1):
With the -th unit vector, the critical rationing level is if is strictly decreasing on , and is the smallest minimizer of that function on otherwise. denotes a right derivative.
Assume and that the demands of different classes are independent in each interval. Fix a class . Then for two instances of the model that differ only in the penalties of the classes and in the demand distributions of the classes ,
(a) the marginal quantities
coincide, and
(b) the critical rationing levels coincide.
The result. Theorem 3 reduces the size of the problem. Under complete backlogging, class 1 demand does not influence any critical rationing level, and the class- critical levels can be found from a problem with only the classes , with a degenerate demand distribution for class . Since computing the levels requires tabulating functions of several variables, which Topkis calls prohibitive for large , this is the observation that makes the levels of the most important classes computable.
Formalizing it. The theorem is proved in the paper by a short sketch that points to two case formulas, (16) and (17), to Theorem 1 (c), and to an interchange of expectation and right derivative. A machine-checked proof would supply the induction, the case analysis and the interchange in full. No formalization of any part of Topkis's paper is known: the result is proved on paper, not formalized.
The obvious argument is an induction on showing that itself does not depend on the lower classes. It fails: does depend on the penalties and demands of every class, since lower-class demand is still served and penalized. Only certain directional derivatives are invariant, and these derivatives depend on the critical levels of every class and on the optimal rationing decision, which themselves change from one instance to the other unless the invariance is already known for the previous interval. The derivatives are one-sided, may be at the boundary, and must be passed through an expectation.
The Lean development, in namespace TopkisRation.Backlog, fixes these conventions:
Fin n (class of the paper is index ); intervals are natural numbers counted backwards; vectors are ordered pointwise;sInf for the infimum and the Bochner integral for , and every statement restricts to , ;sInf;"Does not depend on" is stated with two instances , that agree on every datum the conclusion uses except the freed ones: the same , , , the same and the same for in intervals , and the same class- marginal law for in every interval. The penalty of class itself is not freed. Data of intervals beyond and the ordering cost are unconstrained. Part (b) is stated for arbitrary critical levels of the two instances; existence of critical levels is part of the paper's §1 and is not assumed away, so (b) is not vacuous. The goal does not assume the p. 173 claim, the case formulas (16)–(17), or Theorem 1. Encoding "does not depend" as "is a function of the remaining data" is ruled out.
Needed infrastructure: one-sided derivatives of convex functions and their monotone limits, interchange of right derivative and expectation for convex integrands, and the convexity and rationing-policy results of §1 (Theorem 1, Lemma 2). These are reusable for the other missions of this series. Contributions welcome: proofs of the milestones, a formal version of (16)–(17), and the existence of critical levels.
A single server shared by several classes of jobs must decide, at every moment, which class to work on. When each class incurs a linear delay cost per unit of waiting time and needs mean service time , the classical rule (serve the waiting class with the largest ) minimizes expected cost in many settings, from the M/G/1 queue to discrete-time models (Buyukkoc, Varaiya and Walrand, Adv. Appl. Probab. 1985). Linear costs are a strong restriction: in telecommunications, manufacturing and service systems the penalty for delay often grows faster than linearly, and with convex costs the static priority order of the rule is no longer optimal.
Van Mieghem (Ann. Appl. Probab. 1995) proposed the generalized rule: with nondecreasing convex delay costs and marginal costs , serve the class with the largest index evaluated at its current delay or workload. The paper proves that, in heavy traffic, this dynamic index policy is asymptotically optimal among all scheduling policies, including policies whose scaled workloads do not converge. This mission formalizes that result and the chain of propositions it rests on.
There are job classes. In the th system, the th class- job arrives after an interarrival time and needs service . counts class- arrivals in and counts class- completions within units of server time. A policy is an allocation , where is the time in spent on class . From it come the headcount , the workload (work present in class ), the class-FIFO delay of a job arriving at , and the cumulative cost . Feasible policies are continuous, nondecreasing and work conserving.
The th system runs on and is studied at the diffusion scale: , , likewise, and . Arrival and service processes expand as and . Assumption 1 asks that these terms converge, with rates , , and that the system is in heavy traffic: , where and is the traffic intensity. Assumption 2 asks that the costs scale, , and Assumption 3 that be strictly convex and .
The scaled total workload has a policy-independent limit , with the one-dimensional reflection map. The key static problem splits a total among classes:
Under Assumptions 1–3, for feasible policies with
the costs and delays converge,
Lemma 1 and Proposition 2 (jumps (33)–(34), first-order allocation (27), total workload (32), boundedness, equivalences (35)); Proposition 3 (); Proposition 4 (Little's law); Proposition 5 (converging policies); uniqueness and continuity of (§4.1); the Kuhn–Tucker characterization (46)–(50); and Proposition 6, the lower bound
Proposition 6 is what makes Proposition 7 an optimality statement; it is a separate milestone and not part of the goal.
The result. Proposition 7 identifies a simple, myopic index rule that is optimal at the diffusion scale for every time simultaneously, for arbitrary convex delay costs and nonstationary rates. It extends the rule beyond linear costs, links it to the "hug the optimal workload curve" policies of heavy-traffic control, and shows that the instantaneous allocation problem (43) is all that matters asymptotically. Later work on Brownian control of multiclass queues and on convex-cost scheduling (Mandelbaum and Stolyar 2004) builds on this.
Formalizing it. The paper's proofs are short and informal at several points, and the formalization makes these points explicit: the domain of every uniform limit, the policy class, and the reading of . No part of this paper has a machine-checked proof. A completed mission would give a verified heavy-traffic analysis of a multiclass single-server queue at the sample-path level, the first on the platform with a deterministic diffusion scaling and an explicit reflection map.
The obvious route is to show that converges and then pass to the limit in the cost. That fails for the lower bound: Proposition 6 must cover policies whose class workloads never converge (polling-type policies), so it cannot use compactness of and must instead compare the cost of an arbitrary split of with the optimal split, locally in time. For the goal, (51) controls only the indices, so the convergence of must be extracted from (51) through the inverse marginal costs, the convergence of the total workload, and the Kuhn–Tucker conditions of (43). Delay convergence then needs a uniform control of over windows of length , and cost convergence needs the convergence of the costs applied to delays of order .
Lean namespace GenCMu.HeavyTraffic. The development is deterministic and works one sample path at a time; the stochastic version (Proposition 8) is not part of this mission. Conventions committed to:
Fin d; job indices start at ; every "→" between functions is uniform convergence ((11)), on unless stated; is written as "eventually bound ".A trivializing formalization is ruled out: no theorem assumes the convergence of or , the uniqueness of minimizers, or the lower bound, and the joint satisfiability of all hypotheses has been checked in Lean for .
Needed infrastructure: sample-path reflection-map estimates, counting/partial-sum inversion with uniform errors, parametric convex optimization (Berge's theorem for (43)), and Riemann-sum arguments for the lower bound. The reflection-map and inversion lemmas are reusable beyond this mission. Contributions to any milestone are welcome. The definitions are frozen, so a proof that needs a different definition should be raised in the discussion.
A random walk in a random environment is a walk whose step probabilities are sampled once at each site and then reused whenever the walk returns there. Repeated visits therefore reveal the same local bias instead of drawing a fresh probability. This makes the walk different from an ordinary random walk with a single averaged step probability. Solomon's 1975 paper asks how the random environment changes the long-run direction and speed of a one-dimensional nearest-neighbor walk. Its Section 1 gives the speed law and the associated limits for first passage times. These results distinguish escape at a nonzero linear rate from escape or recurrence at zero linear rate. Solomon (1975)
The question matters whenever a particle repeatedly crosses the same heterogeneous medium. Averaging the local right-step probabilities predicts the drift of a homogeneous comparison walk, but it does not generally predict the speed in the sampled medium. Sites with a small right-step probability can hold up the walk through repeated excursions. The formula in Theorem (1.16) quantifies this effect using a moment of the ratio of left-step to right-step probability. Solomon (1975), pp. 7–8
An environment is a sequence of numbers in . In a fixed environment, a walk at site moves to with probability and to with probability . It starts at . For the random environment, the variables are independent and identically distributed. First the environment is sampled; then the walk moves according to the fixed probabilities at its sites. The probability law that averages over both choices is the annealed law . The mission's model records this law through every finite path cylinder, jointly with every measurable event concerning the environment. Solomon (1975), pp. 1–2
Write for the ratio of leftward to rightward probability. At the endpoints, when and when . Let and ; either may be infinite. For an integer site , the passage time is the first positive time at which visits , with if the site is never reached; put . The positive ladder times are where the passage times are finite. Their joint sequence, rather than individual identically distributed variables alone, is relevant to the speed law. Solomon (1975), pp. 5–7
The goal is the complete three-case statement of Theorem (1.16). All limits below hold almost surely. If , then
If , the symmetric limits are
In the remaining case, , both normalized passage times tend to infinity and tends to zero. The reciprocal inequality is understood in the extended nonnegative reals, including . The milestone list follows the paper's supporting statements: a transience observation, a fixed-environment mean passage-time identity, a separated-block independence lemma, stationarity and ergodicity of ladder times, and the annealed mean ladder-time formula. Solomon (1975), pp. 3, 5–7
The theorem gives a numerical asymptotic speed in either direction when the corresponding ratio has mean below one. It also identifies a zero-speed regime through explicit conditions on the two reciprocal moments. The passage-time clauses say more than the final speed alone: they describe the time required to reach distant positive and negative sites and distinguish a finite linear time scale from an infinite one. The same section compares the speed with that of a homogeneous walk obtained by replacing every local probability with ; the random environment can slow the walk. Solomon (1975), pp. 7–8
Solomon proved these results in 1975. This mission asks for machine-checked proofs of the known statements and a reusable Lean description of the annealed nearest-neighbor model. The fixed-environment chain, first passage times, and the shift law of a sequence of ladder times are useful interfaces for further formal work on random media. No proof of these draft statements is claimed by the mission proposal. Solomon (1975)
The direct attempt to apply an ordinary law of large numbers to the step increments does not fit the model: those increments are not strictly stationary in a nonconstant environment. The walk revisits previously sampled site probabilities, so a later increment depends on the path's history through the sites it has encountered. The paper points out this obstruction before introducing ladder times. An additional issue is that a passage time need not be finite, and the means and may also be infinite. Any argument that converts these quantities to ordinary real numbers too early loses the zero-speed cases. Solomon (1975), pp. 5, 7
Lean represents sites by and time indices by . A probability space carries the jointly sampled environment and path. The environment lies in pointwise and is independent and identically distributed across all integer sites. The path law is fixed by its joint finite-dimensional cylinder probabilities, which express the annealed construction from the paper. In particular, the path cannot be chosen independently of the environment merely because its one-step marginal probabilities look right. This rules out a trivializing model that forgets the dependence between the sampled medium and the walk.
The ratios , their reciprocal and their expectations take values in . Passage times take values in , and normalized passage-time limits are expressed in extended nonnegative reals. The position ratio has a real limit. The theorem permits both endpoint probabilities, and , and imposes no nondegeneracy assumption. Each convergence statement is almost sure. The ergodicity milestone concerns the full joint law of the sequence under the left shift; shift preservation supplies strict stationarity. Solomon (1975), pp. 1–2, 5–7
A complete development needs measure-theoretic probability, the fixed-environment chain and annealed cylinder law, extended-valued integration and first passage times, and ergodic theory for the ladder-time shift. The model and passage-time interfaces can be reused in later one-dimensional random-environment results. Contributions proving the listed milestones, sharpening their interfaces without changing their meaning, or supplying general probability lemmas used by the known proof are within scope.
Robertson and Seymour introduced tangles in Graph Minors. X (J. Combin. Theory Ser. B 52 (1991) 153–190) as the precise obstruction to tree-decompositions of small width: a graph has a tangle of large order exactly when it has no tree-decomposition of small width. A tangle points to a highly connected region of a graph without naming its vertices, by designating for every low-order separation which side is the "small" one. Large grids, large clique minors and surface embeddings with high representativity all induce tangles.
A graph usually contains several such regions. The structure theory of the Graph Minors series needs to look at all of them at once: to decompose a graph along a tree so that each highly connected region sits at its own node, and any two regions are separated as cheaply as possible. Section 10 of the paper provides that decomposition, and its later versions ("tree of tangles" theorems) have become a standard tool in structural graph theory, in matroid theory and in abstract separation systems (see Diestel, Hundertmark and Lemanczyk, Profiles of separations: in graphs, matroids and beyond, Combinatorica 39 (2019), and Carmesin, Diestel, Hundertmark and Stein, Connectivity and tree structure in finite graphs, Combinatorica 34 (2014)). This mission formalizes the original 1991 statement for hypergraphs.
A hypergraph has a finite vertex set , a finite edge set and an incidence relation; an edge may have any number of ends. A subhypergraph is given by a vertex set and an edge set, closed under taking ends of its edges; , , act on both sets. A separation is a pair of subhypergraphs with and ; its order is .
A tangle of order is a set of separations of order such that (i) of every separation of order , one of , is in ; (ii) no three members of satisfy ; (iii) for . Two tangles are indistinguishable if one contains the other, and a separation distinguishes from if and .
A tree-decomposition assigns a subhypergraph to each node of a tree , so that the cover , are pairwise edge-disjoint, and whenever lies on the path from to . An edge of , with components of , makes the separations and , where . Two separations cross unless one of four nestings holds ( and , or the analogous three); a set of separations is laminar if no two members cross.
A tie-breaker maps separations into a linearly ordered set so that (i) exactly when or ; (ii) or ; (iii) separations of smaller order get smaller -order. Given , the -distinction is the separation of minimum -order distinguishing from . A separation is -robust if for every separation of the hypergraph , one of , has -order at least , and doubly -robust if is -robust too.
Let , , be mutually distinguishable tangles in (each with its own order) and a tie-breaker. Then there is a tree-decomposition with such that
and (ii) for , each edge of the – path in whose separations have the smallest -order on that path makes the - and -distinctions, the first with 's side first.
The theorem gives a single decomposition for all tangles at once: any family of pairwise distinguishable tangles is displayed by a single tree-decomposition, with each tangle "living" at its own node (property (i)) and every pair separated by its cheapest distinction (property (ii)). The paper derives from it that a hypergraph has at most maximal tangles ((10.4), p. 184), and Section 11 uses the same machinery to build tree-decompositions whose pieces "almost" carry a local structure, a step used in the later Graph Minors papers.
None of these statements is formalized in any proof assistant as far as a search of the Prove2Me library shows; the platform has simple-graph tree-decompositions with vertex bags (from Graph Minors V), which are a different object from the hypergraph tree-decompositions here. The mission produces machine-checked statements of the tangle-tree theorem in its original hypergraph form, together with the lemma chain the authors use. The remaining work is a formal proof of each item; (9.1) is "left to the reader" in the paper and therefore needs an argument written from scratch.
The naive approach takes, for every pair of tangles, a separation of minimum order distinguishing them, and tries to arrange these separations in a tree. That fails: minimum-order distinguishing separations for different pairs may cross, and no tree-decomposition makes two crossing separations. Ties among minimum-order separations must be broken consistently across all pairs at once, and even a laminar family of distinctions does not obviously yield a tree whose nodes correspond one-to-one to the tangles, as property (i) and demand.
V, E; every theorem assumes [Finite V] [Finite E] (the paper's "all hypergraphs in this paper are finite", p. 154). Subhypergraphs are pairs of a vertex set and an edge set closed under ends.IsTangle G θ 𝒯 includes . In (10.3) the tangles have independent orders .SimpleGraph on Fin n that is a tree. In the goal, node is , which encodes with the distinct; the hypothesis is the paper's.Multistage decision problems under uncertainty are often modelled by a finite set of scenarios: each scenario fixes one possible future, and for it a deterministic problem can be solved. What makes the problem stochastic is the requirement that decisions may depend only on information available at the time they are taken. Rockafellar and Wets (WP-87-119, 1987; journal version Math. Oper. Res. 16 (1991) 119–147) proposed the progressive hedging algorithm, which solves the scenario problems separately with a penalty and a price term and blends their solutions step by step into a single policy that respects the information constraints. The method is a standard decomposition scheme of stochastic programming and is implemented in solver libraries such as PySP and mpi-sppy.
For convex problems the paper proves convergence through the theory of the proximal point algorithm. Many practical scenario models are not convex (integer-like penalties, nonconvex costs). For that case the paper proves one result, Theorem 6.1: the algorithm cannot be expected to find a global minimum, but whenever it converges, its limit is a stationary point. This mission formalizes that result.
Let be a finite set of scenarios with probabilities , . A decision is a vector , split into blocks taken at times . For each scenario there is a scenario subproblem
Throughout, every is nonempty and closed, every is locally Lipschitz, and the sets are bounded.
A policy is a map . Policies form a space with inner product and norm . For each time the scenarios are partitioned into bundles of scenarios indistinguishable at time . A policy is implementable, , when each is constant on every bundle of ; it is admissible, , when for all . The aggregation operator replaces by its conditional expectation over the bundle of ; , and . With the problem is
Progressive hedging with parameter keeps and . It sets , computes for every from
and updates . In the nonconvex case, is only required to be -locally optimal: optimal among the points of within Euclidean distance of it, for a fixed .
denotes Clarke's generalized gradient of a locally Lipschitz and Clarke's normal cone to a closed set .
If and , then , and
moreover is a local minimizer of , which is (P) with replaced by , and .
Theorem 6.1 is the paper's only guarantee outside convexity. It says that progressive hedging, run with local solvers on nonconvex scenario subproblems, cannot converge to a point that fails the first-order conditions, and that the limiting price system is a Lagrange multiplier for the nonanticipativity constraint . It needs no constraint qualification, unlike the general necessary condition of Theorem 4.1: the multiplier is produced by the algorithm. This is the basis for using progressive hedging as a heuristic for nonconvex and mixed-integer stochastic programs.
The result is proved in the paper; to our knowledge it has not been machine-checked. A complete formalization would give checked statements of the scenario model (, , , with the weighted inner product), of the algorithm with inexact local subproblem solutions, and of Clarke's optimality conditions for problems with separable structure. The convex convergence theory of the same paper is the subject of the companion mission Scenarios and Policy Aggregation in Optimization Under Uncertainty 1.
The local optimality of is relative to a ball centred at the iterate, which moves. Passing to the limit requires a radius that is uniform in and in the norm of ; this is what provides, and it only covers points strictly inside the limiting ball: a point of at distance exactly from may lie outside every ball around the iterates. The step from local optimality to the multiplier condition uses Clarke's necessary condition for minimization over a closed set and the sum rule for a Lipschitz function plus a smooth one; neither is in Mathlib. Theorem 4.1 needs, in addition, a calculus rule for normal cones of an intersection under a qualification condition, and the transfer of Clarke's objects between with the weighted inner product and the individual scenario spaces.
is EuclideanSpace ℝ (Fin n). A policy is a function S → EuclideanSpace ℝ (Fin n). The weighted inner product and norm of are explicit definitions (ip, pnorm); Lean's built-in norm on policies (the sup norm) is used only for topological notions: convergence of the iterates and "locally optimal" without a radius, which do not depend on the norm. The radii are in the weighted norm, the radius in the Euclidean norm of . Time blocks are a monotone map from coordinates to periods; bundles are the classes of a setoid on for each period. The standing assumptions are fields of the model structure, so every theorem carries them. Indices are 0-based and sequences are indexed by ; the run starts from and . Theorem 4.1 is stated in its decomposed form (4.4), scenario by scenario.
Clarke's generalized gradient and normal cone are the published platform definitions ClarkeGradients.Shared.generalizedGradient (convex hull of limits of gradients) and ClarkeGradients.FlowInvariance.normalCone (closure of the cone generated by the generalized gradient of the distance function); for locally Lipschitz functions and closed nonempty sets these are the objects the paper uses.
Formalizations that trivialize the statement are excluded: Theorem 6.1 carries no convexity hypothesis and no constraint qualification, the -balls are not measured in the sup norm, and the run predicate is satisfiable (the model files come with a sanity check exhibiting a run).
Useful infrastructure, reusable beyond this mission: Clarke's necessary condition for local minimization of a Lipschitz function over a closed set, the sum rule with a function, products of normal cones, and basic facts about (an orthogonal projection onto for the weighted inner product). Contributions of any of these are welcome.
Two stationary random sequences can have identical distributions at each individual time while differing in their dependence across time. Comparing only their one-time marginals therefore misses a feature relevant to stochastic-process comparison. Ornstein's measures the cost of matching two whole stationary processes: it minimizes the expected discrepancy at one time over joint laws that are themselves stationary. Kamae, Krengel, and O'Brien use stochastic order to replace that optimization over pairs of processes with an optimization over a single common lower process in Theorem 8 of their 1977 paper. This mission formalizes that identity and the stationary coupling results supporting it.
A two-sided path with values in a space is a sequence . The shift sends to the path whose coordinate is . A probability law on paths is stationary, written , when . A law on pairs of paths is jointly stationary, written , when it is invariant under . Its first and second marginals are denoted and . These are the objects defined at the start of Section 8.
When has a partial order, paths are ordered coordinatewise: means for every integer . For probability laws on any such space, write if for every bounded, measurable, increasing real function . Thus stochastic order compares laws through all bounded increasing observations, including observations that depend on several time coordinates. The paper introduces this order on a partially ordered Polish space whose order graph is closed and whose measurable sets are Borel sets in Section 1.
For real-valued paths, is the value at time zero. If the time-zero values under stationary laws and are integrable, define Ornstein's distance by
The stationary constraint on is part of the definition. It asks for a matching of the full processes, even though the cost is evaluated at one coordinate. The paper notes that this formula is equivalent to Ornstein's original definition for the processes considered here on p. 910.
The ordered special case is Lemma 3: if , then
The main target is Theorem 8, equation (18). For stationary real process laws with finite first moments at time zero,
The supremum ranges over stationary laws of whole paths, ordered on the full coordinatewise path space. The milestone list includes Theorem 7's stationary monotone coupling, Lemmas 2 and 3, and three claims made inside the proof of Theorem 8: the triangle inequality , which the paper asserts without proof ("since is a distance"), the attainment of the infimum defining , and the fact that the law of the coordinatewise minimum of an optimal stationary coupling lies below both and . These are the statements from the paper that delimit the target.
The identity expresses a distance defined through stationary joint distributions using only stationary laws below both inputs in stochastic order. It therefore links a coupling cost to an order-theoretic optimization. In the ordered case, Lemma 3 evaluates the distance directly from the difference of means. The authors point out that the general formula replaces an infimum over laws on a product path space by a supremum over laws on one path space on p. 911.
The 1977 results are proved on paper; these mission statements are open Lean proof targets. A completed formalization would supply reusable definitions for stationary path laws, stationary couplings, stochastic order on path spaces, and , together with checked statements about their interaction. It would also make the closed-order and first-moment conditions explicit at every point where a subsequent result uses them. The separate mission for Theorem 1 contains the general coupling characterization that the paper invokes in Theorem 7.
The cost in inspects only time zero, but admissibility of a coupling involves every time coordinate at once. An arbitrary coupling of the time-zero marginals need not extend to a stationary coupling of the two processes. The stationary-coupling existence statement must preserve both full path marginals and the coordinatewise order. On the optimization side, taking an infimum in the real numbers is justified only after the coupling class is shown nonempty and its costs are finite; attaining the infimum requires more than those two facts. These are the obstacles made explicit by Theorem 7 and the proof of Theorem 8.
The Lean path space is , with Mathlib's product topology, Borel measurable structure, and coordinatewise order. The shift sends coordinate to the old coordinate . For Theorem 7, carries the paper's standing assumptions: it is Polish, its order is a closed partial order, and its measurable structure is Borel. Measurability of quantified functions is explicit, following the paper's convention that sets and functions under discussion are measurable. Theorem 8 and its Section 8 milestones specialize to .
The real-valued definition of takes the infimum over jointly stationary probability couplings with the specified full path marginals. Under the target's finite-first-moment hypotheses, the product coupling makes this class nonempty, every displayed cost is integrable, and costs are bounded below by zero. The goal states the supremum with an explicit finite least upper bound. It considers common lower laws with an integrable time-zero coordinate: such laws give the finite values intended by the paper, and this restriction does not remove the optimal value. These choices exclude totalized integrals and default real infima or suprema from supplying a spurious identity. Theorem 7's support condition is concentration on the closed set of ordered path pairs.
Reusable contributions include general facts about stationary measures on countable products, measurable coordinatewise order and meet maps, and stationary coupling compactness. The target specifically requires the order to test bounded increasing functions on the full path space; replacing it with a comparison of time-zero marginals would give a different claim. Likewise, dropping the joint stationarity constraint from the definition of would turn it into the Kantorovich (Wasserstein-1) distance of the time-zero marginals, a different and in general smaller quantity; the formalization keeps that constraint. The source is the published Annals of Probability version; throughout this mission printed page PDF page .
In a population divided into many species, a ranked frequency is the fraction belonging to the th most common species. The Poisson–Dirichlet distribution is a model for such random ranked frequencies. It also arises from ranked jumps of a stable subordinator, which gives the model its connection to random interval partitions. Pitman and Yor's 1997 paper develops both descriptions and studies quantities derived from the ranked sequence. Its §7.3 asks how much of the remaining total mass belongs to the th ranked component when is large. This is the chain factor , the quantity studied here. These interpretations and the result are in Pitman and Yor (1997).
For , the paper first analyzes the tail ratio under through Proposition 11 and its Laplace transform. Proposition 14 relates to that base law by a local-time density. The limiting behavior in Proposition 44 combines those two themes. The paper states both an almost-sure limit and a Gaussian fluctuation limit, but the variance printed for the latter conflicts with the variance of displayed immediately before it. The mission retains the paper's almost-sure assertion as its goal and records the corrected fluctuation assertion separately. Pitman and Yor (1997), pp. 863–865, 890–891.
Choose and . Let be independent random variables, where has the beta distribution with parameters . Its density on is for parameters . Form the stick-breaking lengths
Sort these lengths in decreasing order, retaining multiplicities. The law of the resulting sequence is , exactly Definition 1 of the paper. Pitman and Yor (1997), p. 857.
For that ranked sequence, define the tail ratio and chain factor
The distinction between and the original independent factors matters: the former is computed after ranking and is generally dependent across indices. The paper also uses the function for . It appears in the Laplace transform of . Pitman and Yor (1997), pp. 863–865, 890.
The central target is Proposition 44, display (150): for and ,
The milestones state the distribution and Laplace transform of from Proposition 11(ii), its mean , the almost-sure limit of under , and Proposition 14's change-of-measure formula. The Gaussian companion records the central limit theorem for and the corrected version of Proposition 44's display (151):
The printed variance in (151) is . It differs from the variance forced by the preceding central limit theorem: and the derivative of at give . At , the corrected and printed values are and . The verbatim milestone text preserves the paper's wording; the companion theorem discloses the correction. Pitman and Yor (1997), pp. 890–891.
Display (150) identifies the almost-sure scale of the ranked chain factor: behaves like a deterministic constant divided by . This makes the order of magnitude precise for every permitted , despite the dependence among ranked components. The companion fluctuation statement gives a distributional scale around that limit and exposes a numerical inconsistency in the printed version. Neither conclusion is simply a statement about the independent beta factors ; the paper compares the two sequences precisely because they have different limiting distributions. Pitman and Yor (1997), p. 891.
The result is proved in the paper, while its statements and their supporting definitions still need a machine-checked development. A completed formalization would make the ranked-frequency law, the tail-ratio limit, and the local-time change of measure available as separately reusable results. It would also settle the corrected variance at the level of a precise probability-law statement rather than silently adopting the paper's printed constant.
The tempting shortcut is to use Proposition 11(ii), which says that each has the law of a sum of independent copies of , and invoke a strong law. That information concerns each one-dimensional law separately; it does not exhibit the whole sequence as partial sums of a single independent sequence. Almost-sure convergence is a statement about their joint coupling, so the shortcut leaves a gap. The Gaussian conclusion raises a different issue: its limit must survive the change from to , and its variance must be consistent with the displayed variance of . These are the two substantive tasks beyond the calculation of the Laplace transform. Pitman and Yor (1997), pp. 864, 890–891.
Lean represents a random ranked sequence as on a probability space. Its index means the paper's . Thus the goal uses , and the tail-ratio milestones use . The paper's Definition 1 is represented by independent beta coordinate laws followed by a decreasing ranking. The ranking counts multiplicity using extended cardinality, so an infinite set of terms above a threshold cannot acquire a finite fallback count. The law of the ranked sequence is expressed through measurable preimages. This avoids treating a nonmeasurable ranking map as a zero measure through Measure.map.
All targets retain ; the targets also retain . The beta law and integrals use these parameter ranges. Real expectations state integrability or square integrability where needed, preventing a nonintegrable Bochner integral or variance from supplying a fallback zero. The nonnegative change-of-measure identity uses extended nonnegative integrals, and its local time is identified by the almost-sure limit rather than by an arbitrary extra weight or a limit operator with a default value. The Gaussian variances are positive on this parameter range, despite being represented by nonnegative real parameters in Mathlib. The formalization must use the actual tail ratio of the sequence, not an independently assigned factor process.
The reusable infrastructure includes the ranked-value operation, the stick-breaking law, convolution powers, the tail-ratio and chain-factor definitions, and the bridge between and . Contributions that establish these interfaces or prove the displayed mean, strong law, and central limit assertions directly against them are within scope. Pitman and Yor (1997), Definition 1, Propositions 11, 14, 44.
Semiconductor wafer fabrication lines are reentrant: a wafer returns to the same photolithography or etching station many times along its route, so the parts competing for a machine are at different stages of completion. In such a line, a local dispatching rule decides at every machine which waiting part goes next, and the question is whether a given rule keeps the line stable whenever there is enough capacity. Lu and Kumar (IEEE TAC 36(12), 1991) showed that the answer depends on the rule. Some natural buffer priority rules make the line unstable even when every machine has spare capacity (their Example 1; see also Kumar and Seidman 1990). Two rules are proved stable for every route: first buffer first serve (FBFS) and last buffer first serve (LBFS).
LBFS serves at each machine the waiting part that is closest to completion. It is the "pull" rule of the two, and the one closer to practice: it minimizes work in progress in many settings and coincides with earliest due date when parts arrive in due-date order. This mission formalizes the paper's LBFS results, §V. The sibling mission (FBFS, §IV) treats the other policy on the same model.
Timeline:
A nonacyclic flow line has service centers; center has identical machines, each processing one part at a time. Every part follows the same route through buffers : in buffer it waits at center , then needs units of uninterrupted processing on one machine of that center. A center may serve several buffers.
Parts are released into ; part is released at time and exits at time , when its service at ends. Finitely many parts may be present at time , in any buffer, some already in service. With the number of releases in , the arrivals are bursty with rate and burst if
The work per machine that one part brings to center is , and the load is with . The capacity condition is (3). Also , and is the maximum per-machine work brought to a center by a part in , counting only buffers (6).
Scheduling is nonidling (a machine idles only if every buffer of its center is empty) and nonpreemptive, and a machine takes the part at the head of a buffer. Under LBFS, a machine takes a part from only if every buffer of its center with is empty. The number of parts in the system at time is .
Under (1) and (3), for every with ,
Here is the explicit constant of the delay estimate. The paper prints the second bound as ; its proof establishes the form above, which is the one posed.
The delay estimate behind the goal, in the order of its proof:
for a part that finds parts in the system on release.
Then the Pipeline Property , order preservation (parts exit in the order they enter), and the recursion (14) for the number in system along successive exit times. A further item states that LBFS is stable in the sense of §II: every delay is bounded.
Theorem 2 says the delay of a part under LBFS grows with the number of parts ahead at rate : the line behaves like a pipeline whose speed is set by its bottleneck center, although parts revisit centers. Theorem 3 converts this into a bound on work in progress that holds for all time, with an asymptotic bound that does not depend on the initial state. Together they give stability of LBFS for every route and every burst size, with explicit constants. This is a deterministic, sample-path result: no distributional assumption on arrivals is needed. Its constants are explicit, so they can be evaluated for a given line.
The results are proved in the paper; none is formalized. The mission produces a machine-checked model of a multi-server reentrant line with nonidling, nonpreemptive, head-of-buffer buffer-priority dispatch, together with Theorems 2 and 3 on it. The model carries over to the other policies of the paper (FBFS, least slack, earliest due date).
The obvious argument fails because under LBFS parts released later do interfere with a part : they occupy machines nonpreemptively at the low-priority buffers must still pass. So the delay of cannot be bounded by the work ahead of it alone. The paper's estimate is an induction from the end of the line backwards over the truncated systems , nested with an induction on the position of in its buffer. The constant is recomputed at every level from , so is halved at each level. A formal proof must also handle what the paper treats informally:
All declarations are in the namespace ReentrantScheduling.LBFS.
WithTop ℝ, with ⊤ meaning never, so a run need not serve every part, and the theorems assert that parts are served. A formalization with real-valued start times would assume every part is served, which is half of what stability asserts.Set.encard, never Set.ncard, which would count an infinite set as and make the capacity rule vacuous.The model is reusable for other dispatch rules on reentrant lines. Proofs of any milestone are welcome, as are lemmas on admissible runs (FIFO within buffers, finiteness of ).
Not posed here:
QueueingStability.LuKumar.theorem31;Semiconductor wafer fabs are the standard example of a reentrant manufacturing line: a wafer visits the same lithography or etching station many times along a route of hundreds of steps, so each station holds parts at many different stages of completion and must decide, every time a machine frees up, which of them to serve next. Kumar (Re-entrant lines, Queueing Systems 13, 1993) singled these lines out as a third class of manufacturing systems besides flow shops and job shops, and stability of their scheduling policies became a central question in the analysis of queueing networks.
The question is sharp because the obvious conjecture is false. Kumar and Seidman (IEEE TAC 35(3), 1990) gave a deterministic network in which a distributed policy is unstable although every machine has spare capacity, and Lu and Kumar (IEEE TAC 36(12), 1991, Example 1, p. 1409) gave a two-station reentrant line in which a buffer priority policy is unstable at load below one. Their paper then identifies policies that are always stable: first buffer first serve (FBFS, Theorem 1), last buffer first serve (Theorem 3) and the due-date policies least slack and earliest due date (Theorem 4). This mission formalizes Theorem 1.
Timeline:
A nonacyclic flow line has service centers; center has identical machines in parallel, each working on one part at a time. Every part follows the same route: it visits buffers in order, buffer sits at center , and a part in needs time units of uninterrupted processing on one machine of . The same center may appear many times along the route.
Parts enter at ; part is released at time . The releases are deterministic but may be bursty: with the number of parts released in ,
for constants . Each part brings units of work per machine to center , and the load is . The arrival rate is within capacity when (3). At time the line may hold finitely many initial parts in arbitrary buffers, some of them already in service.
A schedule is nonidling (a machine idles only if every buffer of its center is empty), nonpreemptive (a started service runs to completion) and serves the part at the head of the chosen buffer. Under FBFS a free machine at center takes a part from only if every buffer of with is empty. With the time part exits after its service at , the schedule is stable if there is with
may depend on the initial state as well as on .
For every line, every with , and every admissible FBFS run whose releases satisfy (1),
The statement fixes no constant: is chosen after the run.
An interval is an -busy period if at every instant some part waits in a buffer , , at center . With , and
Milestone 4 has an explicit bound independent of the initial state; the goal additionally covers the finitely many parts present or released during the transient.
Theorem 1 says that the simplest "push" discipline, always serving the earliest stage first, keeps every part's delay bounded on every reentrant line whose stations have spare capacity, for every initial state and every bursty but rate-limited release pattern. By Little's law it also bounds the work in process. Together with Example 1 it shows that stability is a property of the policy, not of the load condition alone, and it gave one of the first two positive results for a whole class of reentrant lines. The explicit constants make the delay guarantee quantitative after the transient.
The result is proved in the paper. As far as the platform record shows it has not been formalized: the related platform items concern the fluid models of Dai and Weiss, which have no parts, no burstiness and no nonpreemption, and a fixed instance of Example 1. This mission produces a machine-checked sample-path model of reentrant lines under buffer priority policies and a checked proof of Theorem 1 with its explicit busy-period constants. The same model serves the sibling mission on LBFS (Theorem 3 of the paper).
A first idea is a work-conservation argument per center: total work arriving at grows at rate per machine, so the center cannot fall behind. This fails because the work arriving at a center from a later buffer depends on how fast the upstream centers have pushed parts to , and an upstream center can release a burst that the downstream center absorbs only after other buffers have starved; Example 1 is exactly such a cascade under a different priority order. Any argument must therefore bound the delay of a part at a buffer in terms of delays it suffered upstream at other centers, uniformly in the initial state, while nonpreemption lets a part wait up to for a machine busy with a lower-priority buffer and the release constraint (1) controls only arrivals to , not to later buffers. On sample paths one must also show that the initial parts clear in finite time and that only finitely many parts are served in any bounded interval.
Lean represents a line by a structure with , , , the route center : Fin l → Fin S and processing times τ with . The positivity is a pinned hypothesis: the paper leaves it implicit, its proof divides by , and its only zero processing times are those of Example 1. Buffers are 0-based: the paper's is Lean index . The load is written , equal to for .
A run is a type of parts with an injective line order, a finite set of initial parts, entry buffers, release times, and for each part and buffer the start of service in WithTop ℝ, meaning never served. Admissibility imposes, at every : precedence (service begins after arrival, except that initial parts may be in service at time ), capacity , nonidling, head of buffer with ties broken by the line order, and the priority rule. All counts use Set.encard. The theorems hold for every admissible run, not for one particular tie-breaking schedule. The constants are definitions computed from the line and ; the times are existential after the run.
Two trivializing formalizations are ruled out: start times in ℝ would make every part served by construction and stability half empty, and a capacity constraint stated with Set.ncard would be vacuous for infinitely many parts. never depends on the part. A sanity file exhibits a nontrivial admissible run satisfying (1) and checks that the empty run is admissible and stable.
The page prints (p. 1410) as a product of the two brackets; the inequality it is solved from gives the quotient, which is also the printed form of , and the formalization uses the quotient.
The sample-path model (Line, Run, Admissible, Arrivals, Stable) is reusable for any buffer priority policy and for the LBFS mission. Contributions welcome: proofs of the milestones in the listed order, lemmas on finiteness of the parts served in bounded time, and interval-counting lemmas for busy periods. Not posed here: Example 1, which is already on the platform as an open problem (QueueingStability.LuKumar.theorem31), Theorems 2–3 (LBFS, sibling mission), Theorems 4–5 and Corollary 1 (due-date policies, several flow lines).
Flexible manufacturing systems are often scheduled by simple distributed rules: each machine looks only at its own buffers and decides, in real time, which part type to work on next. Switching from one part type to another costs a set-up time during which the machine produces nothing, so a natural rule is to work on a buffer until it is empty and only then switch. Perkins and Kumar (IEEE Trans. Automat. Control 34, 1989; reference [18] of the paper) showed that such clearing policies, and in particular clear-a-fraction policies, keep every buffer bounded on acyclic systems whenever each machine has spare capacity. Whether the same holds when material flows around a cycle of machines was left open.
Kumar and Seidman (IEEE TAC 35(3), 1990) answered it negatively by two examples. Example 1 is a single re-entrant part type. Example 2, the subject of this mission, has two part types, neither of which ever revisits a machine, and shows two further phenomena: instability without re-entrance, and the coexistence, for one and the same system, of a bounded periodic regime and an unbounded one, selected only by the initial state.
A manufacturing system has part types arriving at rates and machines . Parts of type follow a fixed route; at stage they wait in buffer at machine , and processing one of them takes . Switching a machine from buffer to buffer takes the set-up time . Flows are continuous: is the level of buffer , and are its cumulative input and output, and
A machine works in runs: a set-up for a buffer, then processing it at rate while it is nonempty, and at the rate of its inflow while it is empty. A clearing policy (Definition 1) keeps a machine on a buffer until the first time that is empty and another of its buffers is nonempty, and then sets it up for one of those. The system is stable if for every buffer .
Example 2 (Fig. 3) has two part types with and two machines. Part type 1 visits buffer 1 at machine 1 and then buffer 2 at machine 2; part type 2 visits buffer 3 at machine 2 and then buffer 4 at machine 1. Processing times are and setting up to buffer takes . The parameters satisfy the capacity condition (1), and , and
conditions (7)–(10). The paper's feasible instance is , with . For this system there is exactly one clearing policy.
For every parameter set satisfying (1) and (7)–(10):
The result shows that stability of a scheduling policy is a property of the initial state as well as of the system: the same parameters admit a bounded periodic orbit and an orbit along which the backlog of buffer 1 is multiplied by in every cycle. The capacity condition (1) holds throughout, so the instability does not come from overload: spare capacity is lost because one machine starves the other. The example also shows that a cycle in the machine graph suffices, without any part type revisiting a machine. Sections IV and V of the paper respond to this by giving a stronger capacity condition under which clear-a-fraction policies are stable, and a supervisory mechanism that stabilizes any policy.
The paper's argument is a stage-by-stage computation of a piecewise-linear trajectory. It has not been machine-checked. A formalization fixes what a clearing trajectory is (including the switching instants at which a buffer is empty but just starting to fill), proves that the trajectories exist and are determined by the initial state, and checks the paper's closed forms. One printed constant is wrong: the offset of the full cycle lacks a final , and the milestone states the corrected value.
The computations within each stage are linear algebra. The difficulty is the event structure. Every stage depends on the order in which the two machines' events occur: whether machine 1 clears buffer 1 before machine 2 has finished its set-ups, whether buffer 2 is still nonempty when buffer 1 empties, and so on. These orderings hold only for large, or only because (8) holds with equality and (9)–(10) hold strictly. The periodic regime depends on exact synchronization. In Case 2, a machine processing an empty buffer at the reduced rate must not be forced off it while its other buffer is empty and not yet fed. A proof must also establish existence of each trajectory, not only compute it.
Fin P, machines Fin M, buffers as pairs with Lean index for paper stage , real time, and no transport delay or assembly (as in the paper). Example 2 is an instance of this general model, with machines 1, 2 as Lean 0, 1.Contributions welcome: existence and uniqueness of clearing trajectories for the two-machine instance, the event-ordering lemmas for large , the restart (time-shift) property of trajectories, and the three milestones.
Portfolio decisions in continuous time must respect both market uncertainty and investment restrictions. A ban on short sales, for example, restricts the vector of wealth fractions a trader may hold at every instant. The corresponding optimal consumption and investment problem is harder than its unrestricted counterpart because a candidate portfolio obtained from the usual pricing equations may violate the constraint. Cvitanić and Karatzas introduced auxiliary markets indexed by a process and used a dual optimization problem to establish existence of an optimal constrained policy in their 1992 paper. This mission formalizes the paper's existence theorem, Theorem 13.1, together with the results in Sections 12–13 that specify its dual target.
Fix a finite horizon and a complete probability space carrying a standard -dimensional Brownian motion . Information at time is the probability augmentation of the filtration generated by up to . A bond earns short rate ; stocks have appreciation vector and volatility matrix . The market assumptions require progressively measurable coefficients, a uniform lower bound on , uniform nondegeneracy of , finite expected interest-rate integral, and finite energy of the market price of risk §2.
A portfolio specifies fractions of wealth held in the stocks, while is consumption and is wealth. The feasible portfolios lie in a fixed nonempty closed convex set . Its support function is , which may equal . The process indexing an auxiliary market belongs to when it has finite expected quadratic energy and finite expected integrated support value. Its deflator combines an interest-rate discount with a Brownian exponential. The class consists of those for which the budget map is finite for every §§4, 8.
The running utility and terminal utility are strictly increasing and strictly concave for positive arguments. An admissible constrained policy has nonnegative wealth, finite expected negative utility, and for Lebesgue-time times probability almost every . The primal value is the supremum of its expected utility over all such policies with initial capital . The dual value is the infimum, over , of expected conjugate utility evaluated at §§5–6, 12.
The first conclusion of Theorem 13.1 is the paper's condition (12.9):
Thus the infimum is attained by a drift with a finite budget map. It is a conclusion of this mission, even though earlier Section 12 results assume it. The milestones include weak duality (12.8), the dual representation of Proposition 12.1, the capital-matching result of Proposition 12.2, and the analytic properties of the extended dual functional in Proposition 13.2 pp. 792–795.
The theorem's second conclusion is
Here is the constrained admissible class. Theorem 12.4 establishes this conclusion when dual attainment is assumed; Theorem 13.1 provides that assumption under the paper's stated utility and dual-finiteness conditions p. 794.
The result supplies an optimizer, rather than only a bound on the best attainable utility. It also identifies a minimizing auxiliary market for every positive dual parameter, making the dual description usable at a specified initial capital. The dual representation links the primal value to a convex function that can be studied without choosing a constrained policy first §§12–13.
The theorem is proved in the paper; the remaining work here is a machine-checked development of its definitions, hypotheses, and existence argument. The mission also produces reusable definitions of an almost-surely square-integrable Brownian integral relation, extended-real utility expectations, an extended support function, and constrained wealth classes. The Brownian state space and predictable step-sum substrate credit the published Ethier–Kurtz formalizations. The paper refers some analytic steps to earlier works instead of reproducing full proofs, including Lemma 12.3 and a final finiteness argument pp. 793–796.
Weak duality alone only bounds the constrained value from above. It does not supply a minimizer of , and an arbitrary minimizing auxiliary process need not belong to . The dual functional must retain meaningful infinite values on the full finite-energy process space ; replacing them with total-operation defaults can turn the needed coercivity and lower-semicontinuity statements into different claims. Even after dual attainment, the minimizing parameter for a prescribed capital must match the budget map §§12–13. These are the precise gaps between a numerical bound and the asserted optimal policy.
Lean uses with its Euclidean norm, a finite positive horizon, a complete probability measure, and the augmented Brownian filtration. Processes are functions of time and sample point; almost-everywhere restrictions on portfolios and auxiliary drifts are distinct from pathwise -almost-sure statements. A policy is represented by a triple whose wealth process satisfies the integral equation, matching the paper's pair together with its unique wealth solution. The integral operator is bound to the local Itô construction by predictable step approximations; it is not a free function. Integrands must be in its almost-sure square-integrable domain.
Support values, utility at zero, expected utility, and value functions use extended reals. The extension is the right limit ; an extended-real supremum defines conjugate utility where zero arguments arise. The inverse marginal is a positive-argument inverse of . The minimization in ranges over , while (12.9) asks for a minimizer in . Its witnesses remain explicit choices in statements involving ; no default-valued inverse is introduced. The functional of (13.3) is defined on , uses the paper's formula on , and is off . On it agrees almost everywhere with the original dual objective, an equality requiring a formal lemma. Assumption 6.2 and conditions (5.8), (8.25), (12.2), (12.3), and (12.11) are explicit. Their quantifiers cover both utilities and every time in where stated. The mission rules out a vacuous dual-attainment hypothesis, a zero default for an unbounded support supremum, and an unconstrained stochastic-integral operator. Contributions proving the source milestones and the analytic lemmas they need are in scope.
Many nonlinear control systems behave like a chain of integrators, , with additional terms that are small either near the origin or far from it. Designs based on weighted homogeneity handle such systems by making the closed loop invariant under a dilation, which gives robustness to perturbations that are dominated by the homogeneous part (Rosier, Homogeneous Lyapunov function for homogeneous continuous vector field, Systems & Control Letters, 1992, doi:10.1016/0167-6911(92)90078-7). A single homogeneous approximation, however, describes the system only at one scale. A perturbation that is negligible near the origin may dominate at infinity, and a design tuned to the origin can then fail globally.
Andrieu, Praly and Astolfi (arXiv:0903.0298v1; SIAM J. Control Optim., 2008, doi:10.1137/060675861) introduce homogeneity in the bi-limit: a function or vector field has one homogeneous approximation near the origin and another, possibly with different weights and degree, at infinity. They develop the basic calculus of this notion, a converse Lyapunov theorem for it, a recursive observer and a recursive state feedback for the chain of integrators, and combine them into a global output feedback. This mission formalizes that output-feedback result and the chain of results it rests on.
For a weight with all and , the dilation is . A continuous function is homogeneous in the 0-limit with triple , degree , if is continuous and not identically zero and, for every compact and every , there is such that
Homogeneity in the ∞-limit with triple is the same statement for all . A vector field is homogeneous with triple , , when each is homogeneous with triple and . Bi-limit means both at once.
For the chain of integrators, and . Given degrees , the weights are
The output feedback studied is
with a gain , a state feedback and an output-injection vector field , where means . Its homogeneous approximations are the same closed loop with and with in place of .
For and there exist , homogeneous in the bi-limit with triples and , and , homogeneous in the bi-limit with triples and , such that
The pair is fixed before . No constant appears in the goal.
The theorem gives a single dynamic output feedback for the chain of integrators that is homogeneous with prescribed degrees near the origin and at infinity, and that stabilizes globally for every gain . Because the degrees at the two ends are independent, the same design can be matched to perturbations of different orders at small and large amplitudes; the paper derives from it output-feedback stabilizers for systems in feedback and feedforward form (Corollaries 5.2 and 5.3), which are outside this mission. The converse Lyapunov theorem (Theorem 2.20) and the key lemma (Lemma 2.13) are general tools for any vector field homogeneous in the bi-limit.
The results are proved in the paper; none of them, nor the notion of homogeneity in the bi-limit, has a machine-checked proof. The platform has a definition of global asymptotic stability for continuous vector fields (from the series on Chitour, Ushirobira, Efimov and Perruquetti's prescribed-time stabilization) and Mathlib has the needed analysis, but there is no converse Lyapunov theorem and no theory of weighted homogeneous vector fields. A complete formalization would supply both.
Lyapunov arguments for homogeneous systems usually compare a function with its homogeneous approximation on the unit sphere and then scale. With homogeneity in the bi-limit the comparison holds only for small or for large dilation parameters, with no control at intermediate scales, and the two approximations have different weights, so no single dilation brings the whole space to a compact set. Each statement has to hold for the system and for both approximations at once. Theorem 2.20 additionally requires a converse Lyapunov theorem for continuous, non-Lipschitz vector fields whose solutions need not be unique, so a flow map is not available. Finally, the gain in the goal is arbitrary: an argument that only works for large enough proves a weaker statement.
Points of are functions Fin n → ℝ, with the paper's coordinate at index ; the closed loop lives on Fin (n + n) → ℝ with first and second. Real powers are Real.rpow; the signed power is . Every clause of Definitions 2.1, 2.3 and 2.5 is kept: positive weights, nonnegative function degrees, continuity, approximating functions not identically zero, uniformity on compact subsets of . Dropping any of them makes the goal weaker than the paper's.
Global asymptotic stability reuses the published ChitourPrescribedTime.FixedTime.GloballyAsymptoticallyStable on the Euclidean space, applied to the time-invariant field: the origin is an equilibrium, every initial state has a solution on , and stability and uniform attractivity hold for every solution. The mission adds that no solution escapes to infinity in finite time, so that every solution is covered; for continuous autonomous fields this is the textbook notion. Positive and negative definiteness, properness ( along the cocompact filter), and partial derivatives (Fréchet derivative on a basis vector) are defined in the mission's definition files.
Corrections and readings, each disclosed in the item concerned:
A formalization in which the closed loop is replaced by its linearization, the homogeneity predicate is weakened to pointwise convergence, or the quantifier on is moved before and , proves a different statement and does not close the goal. Contributions welcome: a library of weighted dilations and homogeneous functions, the converse Lyapunov theorem, and proofs of the milestones in any order.