Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Measurements of Ethernet and Internet traffic in the 1990s showed that the amount of data offered to a link is bursty on every time scale and that the lengths of transmissions (file sizes, connection durations) have heavy, regularly varying tails. Two families of approximations for the cumulative input were proposed: fractional Brownian motion, which has dependent Gaussian increments, and α-stable Lévy motion, which has independent, heavy-tailed increments. The two lead to very different predictions for buffer overflow and link dimensioning.
T. Mikosch, S. Resnick, H. Rootzén and A. Stegeman (Ann. Appl. Probab. 12 (2002) 23–68) showed that both answers are correct in different regimes, and that the regime is decided by how fast the connection rate grows relative to the time scale. This mission formalizes their result for the infinite source Poisson model under slow growth, where the limit is a totally skewed α-stable Lévy motion. Companion missions treat the ON/OFF model and the fast-growth regime with its fractional Brownian limit.
A transmission length has law on with tail . Condition (2.8) asks
with slowly varying ( for every ). The mean is finite and the variance infinite. The quantile function (2.9) is .
In the -th model, connections start at the points of a homogeneous Poisson process on with rate , labelled so that . Connection transmits at unit rate for a time ; the are iid with law and independent of the . The number of active connections and the cumulative input are
The rate is a positive non-decreasing function of . Slow Growth Condition 1 is
where is evaluated at .
The stable law is the law with characteristic function for . α-stable Lévy motion has independent stationary increments with . Write
Under (2.8) and Condition 1,
convergence of the finite-dimensional distributions to a totally skewed () α-stable Lévy motion.
On the scale. The paper prints the limit . Its own proof establishes (pp. 37–38), which makes the Lévy measure of the limit. The totally skewed stable law with that Lévy measure has (Samorodnitsky–Taqqu, Property 1.2.15; also the paper's own criterion on p. 47 with , and the the paper prints in Theorem 2). Since decreases from to on (), the printed limit has the wrong scale and the theorem as printed is false. The goal states the corrected scale ; milestones quote the page as printed.
(2.14), the covariance of ; Lemma 1 part 1 (Condition 1 ); Lemma 2, slow part (); (4.15), negligibility of the boundary pieces ; the tail limit of ; (4.17), ; (4.20)–(4.21), ; (4.19), corrected, the stable limit of ; the corrected one-dimensional limit of ; and of §4.5, which reduces the fidi convergence to the one-dimensional one.
The theorem shows that under slow connection growth the cumulative input is asymptotically a process with independent, infinite-variance increments. Long-range dependence present in each model (the covariance (2.14) decays like ) disappears on the time scale , and the heavy tail of the transmission lengths dominates. Together with the fast-growth result (fractional Brownian motion) it explains why both approximations are found in measured traffic, and it identifies the critical quantity .
The result is proved in the paper, modulo the scale. No part of it is machine-checked. The mission produces a formal statement of the infinite source Poisson model with its marked point process structure, a formal statement of stable laws and stable Lévy motion through their characteristic functions, and machine-checked versions of the paper's estimates. Correcting the printed scale is part of the output.
The pieces are controlled by first moments, regular variation and Lemma 2. The central step is the stable limit of : a sum of a Poisson number of iid, heavy-tailed summands whose law changes with . A classical central limit theorem does not apply because the variance is infinite, and the summands form a triangular array. The paper cites a point-process limit (Resnick's Exercise 4.4.2.8) for this step; a formal proof needs a convergence theorem for row-wise iid triangular arrays to stable laws, with the constant computed exactly.
Each has its own probability space carrying the -th model, and every statement quantifies over all such families. The Poisson points are given by their iid exponential spacings , indexed by . (2.8) is stated as " is slowly varying", with lengths non-negative. is , which equals the page's generalized inverse for . is a cardinality and the region sums are sums of non-negative terms; their junk values (an infinite set, a non-summable family) occur only on null events. is an interval integral. The growth hypothesis is: , non-decreasing, Condition 1. No other hypothesis is added.
The fidi limit is pinned by its characteristic function on for sorted times : the product of the characteristic functions of evaluated at . The existence of the limit law is part of the claim. One-dimensional limits are stated the same way on . Convergence in probability to is for every .
Trivializing formalizations are excluded:
A complete development needs regular variation (Karamata's theorem, Potter bounds, generalized inverses), the Poisson random measure of the marked points, and stable limits for triangular arrays. All three are reusable beyond this mission. Proofs of the milestones are welcome separately, as are general Mathlib-style lemmas on regular variation.
The ferromagnetic Ising model is the basic model of statistical mechanics for interacting binary variables. On a finite graph it is a probability distribution over spin configurations, and its normalizing constant, the partition function, encodes the thermodynamics: the free entropy per vertex determines the magnetization, the correlations, and the location of phase transitions. On lattices this quantity is understood only in special cases. On sparse random graphs, such as random regular graphs and Erdős–Rényi graphs with bounded average degree, physicists predicted it with the cavity method (Mézard and Parisi, The Bethe lattice spin glass revisited, 2001): locally these graphs look like trees, and on trees the model can be solved by a recursion. The same recursion underlies belief propagation, the message-passing algorithm used in coding theory and machine learning.
Timeline:
Let be a sequence of finite graphs. The Ising measure at inverse temperature and magnetic field is
each edge counted once, and the free entropy density is .
A degree distribution is a law on with ; its size-biased version is , and . The Galton–Watson tree has a root with children with probability , and every other vertex independently has children with probability ; is its first generations.
The ball is the subgraph induced by the vertices within distance of , rooted at . The sequence converges locally to if, for every and every rooted tree , the fraction of vertices with (root-preserving isomorphism) tends to . It is uniformly sparse if .
The cavity recursion acts on laws of a real random variable :
with and i.i.d. copies of independent of . For it has a unique fixed point supported on . The Bethe functional of a law of is
with independent of the .
Assume is uniformly sparse, converges locally to , and . Then for every :
and has a limit as , with . This is the paper's statement that the limit exists for every , equals (2.9) for , is even in , and is continuous at .
The result. Theorem 2.4 establishes the replica-symmetric (Bethe) formula for the ferromagnetic Ising model on the standard sparse random graph ensembles at all temperatures, including below the critical temperature where the Gibbs measure on the limiting tree is not unique. It identifies the free energy of random regular graphs, Erdős–Rényi graphs and configuration models with arbitrary degree distributions of finite variance, and the derivative identities that follow give the limiting magnetization and energy per edge. The tree estimates of Section 4 also yield the convergence of belief propagation (the companion mission of this series).
Formalizing it. The theorem is proved; nothing in this mission has been machine-checked before. A formal proof requires infrastructure that Lean's Mathlib does not have: Ising measures with boundary conditions, correlation inequalities, Galton–Watson trees as laws of offspring functions, local weak convergence of graph sequences, distributional fixed-point equations, and the Monge–Kantorovich distance on the real line. While stating the milestones, Corollary 6.3 turned out to be false as printed (the constant should be ; a counterexample is ); the mission states the corrected version, which is what the paper's proof gives.
The obvious route through uniqueness of the Gibbs measure on the tree fails below the critical temperature: different boundary conditions give different limits, so local quantities are not determined by the local graph structure alone. The paper replaces uniqueness by insensitivity to positive boundary conditions when (Lemma 4.3), which rests on Griffiths and GHS monotonicity and on averaging over the random tree; the deterministic statement is false. Passing from derivatives to the free entropy itself requires that the Bethe functional be stationary in the cavity law (Corollary 6.3), so that the -dependence of can be ignored. Finally, the case at low temperature is reached only as a limit: there is no fixed-point characterization at .
true); edges are unordered and counted once. Graphs live on Fin n.List ℕ → ℕ in Ulam–Harris form; random trees are laws of offspring functions under the product σ-algebra. Galton–Watson trees are infinite product measures. Fields on trees are nonrandom functions of the vertex.ProbabilityMeasure ℝ, and convergence in distribution is weak convergence. Expectations over are series with product laws.A complete development needs: Griffiths and GHS inequalities for finite Ising models (reusable for any ferromagnetic model); Ulam–Harris random trees with conditional independence; local weak convergence of graph sequences (reusable for random graph theory); distributional recursions with stochastic ordering; and the coupling characterization of the Wasserstein-1 distance on . Contributions of any milestone are welcome, as are proofs of the classical inequalities of Section 3 independent of this paper.
A well-quasi-order is a reflexive, transitive relation in which every infinite sequence contains a pair with . Showing that a class of finite combinatorial objects is well-quasi-ordered by a containment relation is a standard way to prove that every property closed under that containment is characterised by finitely many forbidden objects. The best-known instance is the Graph Minor Theorem (Wagner's conjecture), completed by Robertson and Seymour in Graph Minors XX (JCTB 92, 2004).
Nash-Williams proposed the analogous conjecture for a different containment, immersion, in which edges of the smaller graph are mapped to edge-disjoint paths of the larger graph. Graph Minors XXIII (JCTB 100, 2010) proves it by deriving a general well-quasi-ordering theorem for labelled hypergraphs from the machinery of Graph Minors XX.
Timeline.
All graphs and hypergraphs are finite. A graph has a vertex set , an edge set , and for each edge an unordered pair of ends; an edge with equal ends is a loop, and several edges may have the same ends (parallel edges). A graph is loopless if no edge is a loop. A path has at least one vertex and no repeated vertices; a circuit has at least one edge and no repeated vertices, so a loop and a pair of parallel edges are circuits.
An immersion of in is a map on such that is injective on vertices; every non-loop edge with ends goes to a path of with ends ; every loop at goes to a circuit of through ; and , share no edge when .
A hypergraph has finite sets , and an incidence relation; is the set of ends of the edge , of any size. Write for the complete graph on . A collapse of to maps each vertex of to a non-null connected subgraph of , pairwise vertex-disjoint, and each edge of injectively to an edge of , so that meets whenever is incident with , and every edge of every is covered by some edge of incident with both and . The transpose of a graph is the hypergraph with vertex set , edge set and the same incidence.
A quasi-order is an ideal of if it is a sub-quasi-order closed downwards in ; a shadow is a tuple of well-quasi-orders and finite sets, ordered lexicographically (Section 3 of the paper).
The immersion theorem implies that every class of finite graphs closed under taking immersions is characterised by finitely many excluded immersions. Theorem 1.6 is stronger than both 1.1 and Wagner's conjecture: it handles hypergraphs, labels from an arbitrary well-quasi-order and ordered edges, which is the form in which the Graph Minors machinery is reused by later work.
All results here are proved in the paper. None of them has a machine-checked proof: Mathlib has well-quasi-orders and Higman's lemma, but not the Graph Minor Theorem or any notion of graph immersion. The value of this mission is a faithful formal statement of the immersion theorem and of the reductions the paper performs in Section 1 (1.3 and the passage from 1.6 to 1.4, 1.5 and 1.1), each of which can be formalized independently of Graph Minors XX, plus the order-theoretic lemmas 3.1 and 3.2.
The reductions in Section 1 (1.3, and the passages from 1.6 to 1.4, 1.5 and 1.1) are short on paper but require a working library of multigraph walks, paths and circuits, which Mathlib does not have for graphs with loops and parallel edges. The real difficulty is 1.6, which the paper derives from a theorem on patchworks of Graph Minors XX (its 2.2) together with tangle results of Graph Minors X, and therefore rests on the structure theory of the whole Graph Minors series. No route around that theory is known: when the hypergraphs are loopless graphs, a collapse of to makes a minor of , so already 1.2 contains Wagner's conjecture. Nor does 1.2 alone give 1.1: loops cannot be routed through the transpose construction of 1.3, and the paper handles them by counting loops at each vertex as a label from the well-quasi-order , which is why the labelled forms 1.4–1.6 are needed.
A graph is Graph V E with ends : E → Sym2 V; a hypergraph is Hypergraph V E with inc : E → V → Prop; each lives on its own finite types, and a sequence is a family indexed by ℕ (from ; the paper's becomes ). Paths and circuits are walks with vertex and edge lists; the ends of a path are unordered. An immersion is the structure GraphImmersion H G; a collapse of to is Collapse G H, whose branch sets are Subgraphs of ⊤ : SimpleGraph V(G) (Mathlib's Subgraph.Connected includes non-emptiness). Well-quasi-orders are Mathlib's WellQuasiOrdered on a type with a preorder for 1.4–1.7, and QO.IsWQO on subsets of an ambient type for 3.1–3.2, where quasi-orders are compared by inclusion. Directed graphs for 1.7 are DirGraph V E with heads and tails.
Three trivializing formalizations are excluded: the collapse keeps condition (iv), so branch sets cannot use arbitrary pairs of vertices; immersion paths are edge-disjoint, not vertex-disjoint (which would give topological minors, not a well-quasi-order); and each graph lives on its own type, never all on one fixed finite type, which would make the goal a pigeonhole statement. Strong immersion is not stated.
Contributions welcome: proofs of 3.1, 3.2 and 1.3, the reductions 1.6 ⇒ 1.4 ⇒ 1.2 and 1.4 + 1.3 ⇒ 1.5 ⇒ 1.1, and library material on multigraph walks, paths and circuits, which is reusable beyond this mission. A proof of 1.6 would require formalizing the Graph Minors series.
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.
This entry records a completed elementary result in the campaign on odd numbers as sums of primes: every odd natural number greater than 1 is a sum of at most 4401 primes. It illustrates how an additive density estimate can reduce the number of prime summands in a Schnirelmann argument.
For every natural number , if is odd and , there is a multiset of primes with and . Repeated primes are allowed. The bound applies to every such , not only sufficiently large integers.
The goal references the existing proved 4401 theorem. Its statement is the campaign template instantiated with 4401.
The two supporting references are the density bound and Mann's theorem, both already proved.
Let and . The density estimate gives . Mann's theorem gives , so yields density at least . The sumset cover argument then produces 4400 odd prime summands, with one additional 3 to obtain the required parity. Explicit sums of 2s and 3s handle the remaining small and medium ranges. These steps are included in the accepted goal proof; they are not unfinished milestones.
All three referenced theorems have ACCEPTED proof submissions under the account moona3k, are marked Proved, and use Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. No new Lean statement or duplicate theorem is introduced by this proposal.
The density theorem's published source credits an extraction from the accepted 6101 proof. Mann's theorem is the classical additive density theorem of H. B. Mann; the accepted formalization follows the Dyson transform presentation cited in its theorem record. This entry assembles those existing results into the 4401 bound.
The 4401 bound was an intermediate improvement on 6101. It is not the current campaign frontier: the campaign now includes a proved bound of 27. This proposal preserves the earlier result and its proof route without claiming a new literature result or a new record.
Status: complete. This mission records a finished formalization rather than an open call for work. Every statement below, including the goal, was uploaded together with a proof that the platform has verified, so there is nothing left to prove.
The Lovász Local Lemma (LLL) is a basic tool of the probabilistic method. It shows that a collection of rare "bad" events can all be avoided simultaneously, even when the events are not independent, provided each event depends on only a few others. Its best-known application is to satisfiability: a -CNF formula in which every variable appears in few clauses has a satisfying assignment.
Quantum satisfiability (-QSAT) is the quantum analogue of -SAT. Clauses are replaced by projectors acting on qubits, and the question is whether some nonzero state is annihilated by all of them, equivalently whether the corresponding local Hamiltonian is frustration-free. Bravyi showed that -QSAT is -complete for , so sufficient conditions for satisfiability are of interest in quantum complexity theory and in many-body physics. Ambainis, Kempe and Sattath (arXiv:0911.1696, J. ACM 2012) proved a quantum version of the LLL in which probability is replaced by relative dimension, and derived a sufficient condition for -QSAT instances to be satisfiable.
Let be a nonzero finite-dimensional vector space. For a subspace , the relative dimension is
It plays the role of probability: subspaces replace events, intersection replaces conjunction, and replaces conditional probability.
Subspaces have dependency sets when, for every and every set of indices with and ,
In words, is independent, for relative dimension, of every intersection of subspaces outside its dependency set.
A -QSAT instance on qubits is a family of projectors , each acting on a set of qubits and extended by the identity on the others. It is satisfiable if a nonzero state lies in the kernel of every .
The formalization proves the local lemma once, for an abstract valuation: a real function on a bounded lattice that is nonnegative, monotone and modular, , with and . Relative dimension on subspaces and the uniform probability on subsets of a finite set are the two instances used.
Let be subspaces with dependency sets , and let satisfy for every . Then
All of these are proved on Prove2Me and can be found by name (tag quantum-lll):
QLLL.Valuation.lll.QLLL.quantum_lll_symmetric.QLLL.SAT.classical_lll, QLLL.SAT.classical_lll_symmetric.QLLL.SAT.sat_of_degree_le.QLLL.PiQSAT.inf_ker_extendOp_ne_bot on Mathlib's tensor product, and QLLL.QSAT.satisfiable_of_degree_le for orthogonal projectors.QLLL.SAT.exists_assignment_forall), and the local lemma for infinite index sets under a continuity hypothesis (QLLL.lll_iInf).The quantum local lemma gives a sufficient condition for -QSAT satisfiability that depends only on the local structure of the instance: the rank of the projectors and the number of projectors per qubit. It shows that the classical criterion survives the passage from events to subspaces, even though subspaces do not form a distributive lattice. Later work on constructive and tight versions, listed in the timeline, builds on this statement.
All results of this mission are proved and machine-checked. The Lean development was written as a complete formalization of the paper, and every statement here was uploaded together with a proof verified by the platform. What the mission adds is a reusable, Mathlib-based library: the local lemma for abstract valuations, its classical and quantum instances, -QSAT stated on Mathlib's tensor product of qubits, and linear algebra on intersections of tensor products of subspaces that Mathlib does not yet contain. Mathlib currently has no form of the Lovász Local Lemma.
The classical proof uses complements of events and the identity , together with the distributive law for events. Subspaces satisfy neither in general: the lattice of subspaces is modular but not distributive, and the orthogonal complement does not distribute over intersections. The argument has to be rebuilt from the properties of relative dimension that do hold. For -QSAT, the further difficulty is to show that constraints acting on disjoint sets of qubits are independent for relative dimension, which requires computing intersections and dimensions of tensor products of subspaces.
Conventions committed to in the Lean statements:
An infinite version of -QSAT is deliberately not included. Nonzero subspaces can have all finite intersections nonzero and zero total intersection, so the infinite statement has to be phrased with compatible families of density matrices, and the current Lean formulation does not yet restrict the constraints to positive operators.
The blueprint of the formalization, linking every paper statement to its Lean declaration, is at sattath.github.io/Quantum-Lovasz-Local-Lemma/blueprint. Natural extensions, outside the scope of this mission: the orthogonal-projector form of Corollary 16 on Mathlib's tensor product once inner products on -fold tensor products are available, Shearer-type conditions, and a measure-theoretic classical local lemma on general probability spaces.
This is my first contribution to Prove2Me, so the definitions, statements, proofs and descriptions may fall short of what an experienced contributor would produce. Some choices may be unidiomatic, some lemmas may duplicate Mathlib, and the split into entries could be better. Every proof is checked by Lean, so the theorems are correct as stated; the question is whether they are stated in the most useful way.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's earlier values ( down to ) came from Schnirelmann's method with every constant written out. The entry used the sharp singular-series weight in a pointwise sieve bound, and its large range stopped near because the pointwise bound loses the spread of the singular series. This entry replaces that large range by Riesel and Vaughan's weighted argument, which divides out the singular series exactly, using Dirichlet characters and the large sieve. Rosser–Schoenfeld's zero-based bound is replaced throughout by Chebyshev's elementary . No zeta- or -function zero input is used, and the result matches Vaughan's .
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in.
Let and . We show , then conclude with Mann's theorem. Let be the number of ordered pairs of odd primes with . Since , it suffices to show for large . Write and for the twin-prime constant.
TaoFivePrimes.siebert_prime_pair_bound), Cauchy–Schwarz gives . The kernel sum is a finite computation.MVSieve.primitive_character_large_sieve, MVSieve.large_sieve_weight_lower), with Chebyshev's bound in place of Rosser–Schoenfeld. This gives with room to spare.The argument reaches Vaughan's with no zeros of or -functions and no prime number theorem. New reusable components:
The Lean statement is the campaign template verbatim with in place of the value. The proof imports two platform theorems: RV27.middle_range (the small-shift range, ) and RV27.large_range (), and Schnir.basis_of_density (Mann's theorem). Those rest on TaoFivePrimes.siebert_prime_pair_bound, the PrimePairSieve nodes and the MVSieve large-sieve nodes.
PrimeNumberTheoremAnd (PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean).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 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 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 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.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 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.
In the edge-disjoint paths problem (EDP) one is given an undirected graph and a list of source–sink pairs, and asks how many pairs can be connected simultaneously by paths that share no edge. Its relaxation EDP with congestion (EDPwC) allows every edge to carry up to a fixed number of paths. Both are central problems of network routing and of approximation algorithms, and the standard algorithmic tool for them is the multicommodity flow relaxation: a linear program that may split each pair's unit of demand fractionally over many paths. Rounding this LP is how most approximation algorithms for routing work, so the ratio between its optimum and the best integral routing, the integrality gap, bounds what any LP-based algorithm can achieve.
Without congestion the gap of this relaxation can be as large as (Chekuri–Khanna–Shepherd 2006), and the question is how much a small congestion helps. Andrews, Chuzhoy, Guruswami, Khanna, Talwar and Zhang (Combinatorica 2010) proved hardness of approximation for EDPwC (their Theorems 1 and 2) and, independently and unconditionally, that the gap of the relaxation remains even when the integral solution may use congestion (their Theorem 5). In particular, for every fixed integer the gap between -integral and fractional multicommodity flow in undirected graphs is superconstant. This mission formalizes Theorem 5 for EDPwC.
Fix integers and . Write for and for the natural logarithm, and set
A random -uniform hypergraph on the vertex set has hyperedges , chosen independently, each uniformly among the -element subsets of the vertices.
From one builds a graph . For every hyperedge it has two vertices joined by a special edge; for every vertex of it has a source and a sink . If lies in the hyperedges with , the regular edges , for , and are added. The canonical path of is ; it crosses the special edge of every hyperedge containing . The EDP instance has one pair for each .
A feasible fractional solution puts flow on – paths , with routed amount for each pair and at most one unit of flow through each edge; its value is . An integral routing with congestion at most connects a set of pairs, each by one path, so that every edge lies on at most of these paths; its value is the number of connected pairs.
The analysis uses three events of : , that some set of vertices contains no hyperedge; , that more than vertices lie in more than hyperedges; and , that the graph obtained from by contracting every special edge has more than cycles of length at most .
There are absolute constants and such that for all and all integers with some hypergraph as above satisfies
so the integrality gap is at least . The paper's Theorem 5 states this as for congestion and vertices; the goal keeps the paper's own Section 2 parameters, which fix the instance and leave the constants open.
Lemma 6, Lemma 7 and Lemma 8 (); the joint good event of Section 2.4; the fractional solution of value ; and the three bounds of the gap analysis, (canonical paths), (long non-canonical paths), (short non-canonical paths), combined into .
The result shows that the multicommodity flow relaxation cannot certify a constant-factor approximation for undirected EDPwC with any constant congestion: against integral solutions of congestion its gap is at least . Any algorithm that compares its output with this LP inherits the bound. It complements the paper's hardness results, which hold only under a complexity assumption. The instance is a short explicit construction from a random hypergraph, so the theorem is also a statement in probabilistic combinatorics: random sparse uniform hypergraphs are, with constant probability, simultaneously "covering" (no large hyperedge-free set), of bounded degree, and nearly free of short cycles.
The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces one: a formal model of the path LP and of congestion-bounded integral routings on simple graphs, reusable for other routing gaps; a formal random-hypergraph model with first-moment and Chernoff-type estimates; and the deterministic gap analysis. Variants with better constants, or the stronger statement that at least a quarter of all hypergraphs work, are welcome as additional results.
The fractional side and the bound on canonical routings are short. The difficulty lies in two places. First, Lemma 8 bounds the expected number of short cycles of ; the adjacency of depends on all hyperedges at once (consecutiveness along each vertex's sequence), and the obvious estimate through the intersection graph of fails, because many hyperedges through a common vertex form a clique there. What keeps the count small is the order structure of each vertex's hyperedge sequence, which the intersection graph forgets. Second, the bound on short non-canonical paths requires turning two distinct routing paths of a pair into a short cycle of the contracted graph and charging it with the congestion constraint. Finally, the closing estimate holds only for large in the stated range of , and the printed chain for it is not literally correct, so the asymptotics have to be done afresh.
Vertices of are Fin n, hyperedges are indexed by Fin m with , and is an element of Fin m → {s : Finset (Fin n) // s.card = c}; probabilities are normalized counts over this finite set (uniform measure, which is independence of the hyperedges). The conventions are:
The goal cannot be met by an unrelated graph: the instance must be for a hypergraph with exactly hyperedges of size on vertices, the fractional solution must respect and capacity , and the integral bound is over all routings of congestion .
Not in scope: the ANFwC half of Theorem 5, the remark on a superconstant gap at , and the hardness results of Sections 3–5 (Theorems 1 and 2, Corollaries 3 and 4).
A complete development needs Chernoff and Markov bounds for counting measures, binomial-coefficient estimates, cycle extraction from two distinct paths in a simple graph, and the asymptotic estimates for . The routing and LP definitions and the cycle-extraction lemma are reusable beyond this mission.
A simulation run often estimates a steady-state mean without producing independent observations. A confidence interval must account for dependence in the output, and the relevant variance constant may be unknown. Standardized time series (STS) methods use the shape of an integrated output path to cancel that constant rather than estimating it separately. The resulting interval can be computed from one run, but its length can vary substantially with the chosen standardizing functional. Glynn and Iglehart introduced a common functional framework for these methods and asked how short their expected intervals can be as the run grows. Their 1990 paper identifies a universal lower bound.
The comparison is operational. A shorter confidence interval conveys a more precise estimate at the same nominal coverage. The authors also compare STS with procedures that consistently estimate the variance constant. They state that the lower bound is attained by the latter procedures and approached, but not attained, by STS intervals. The present mission isolates the bound for STS itself, Corollary 4.16. It does not make the claim that a particular STS rule attains it. This distinction follows the paper's introduction and §4.
Let be a real simulation output process for . Its integrated average path at run length is for . The unknown steady-state mean is . The paper assumes a functional central limit theorem in the space of continuous real paths:
where is standard Brownian motion. Convergence is weak convergence of random continuous paths in the uniform topology. This is Assumption (2.1), rather than a claim that every output process satisfies it. The paper lists several classes of processes for which such a theorem is available under further conditions (§2, pp. 2–3).
An STS scale functional belongs to when it is measurable, positively homogeneous, unchanged by subtracting any multiple of the identity path , positive at almost surely, and continuous at almost surely. The last two conditions ensure that the Brownian ratio is a meaningful distributional limit. The paper also describes these functionals through the bridge map : a member of can be written as for a suitable . Thus the scale is determined by a Brownian bridge while the endpoint is independent of it (Propositions 2.7–2.8).
Define . For a confidence level , choose endpoints with . The STS confidence interval from equation (2.10) has endpoints and . Its length is . Here lies strictly between zero and one; the endpoint equation is part of the construction, not an arbitrary choice.
The goal is Corollary 4.16 for every nonnegative under Assumption (2.1). Write for the standard normal distribution function and . Then
The expectation and liminf admit . The statement does not impose an integrability assumption that would remove that case. It quantifies over every admissible STS functional and every interval whose endpoints have the specified Brownian confidence mass (Corollary 4.16, p. 12).
Three substantial targets precede the corollary. Proposition 4.1(a) relates scaled expected length to . Proposition 4.3 says a symmetric choice of minimizes . Theorem 4.8 gives , where denotes the quantile of . The milestone list also includes the cited Brownian independence, mixture distribution, scale invariance, and continuous mapping statements that put these targets in context.
The corollary supplies a benchmark for the asymptotic expected length of any interval in this STS class. A proposed standardizing functional cannot beat the normal-quantile constant while retaining the stated functional limit and confidence construction. It also identifies the quantity against which the paper's other interval procedures can be compared. The bound applies uniformly to the class , not to a chosen batch size or a particular form of (Glynn–Iglehart 1990, §4).
The mathematical result has been proved in the source paper. This mission supplies formal statements and their shared definitions as proof targets; it does not claim that their Lean proofs already exist. A complete development would formalize the known arguments for the milestones and corollary, including the Brownian path representation, weak convergence, quantile properties, and expectation inequalities. Those components could be reused in other work on simulation output analysis and ratios of weakly convergent processes.
Weak convergence alone does not imply convergence of expectations. In particular, a continuous mapping limit for cannot simply be integrated as an ordinary finite real expectation when the family is not uniformly integrable. Proposition 4.1(a) asks only for a lower bound, and its statement must still account for . This is why the goal is expressed with a liminf and extended nonnegative expectations rather than a real-valued limit. A separate difficulty is that the interval width depends jointly on a distributional scale and a choice of two quantiles. Bounding either one in isolation does not state the corollary.
Paths are Mathlib's with its uniform metric and Borel sigma algebra. A standard Brownian motion is a measurable random continuous path agreeing with an -indexed real Brownian motion on . The paper's discontinuity set is the set where is not continuous. Assumption (2.1) includes joint measurability of and finite-interval pathwise integrability so that each integrated average is defined. The path is supplied together with its defining integral equation, which determines it pointwise. Its values are not free parameters.
Indices are natural numbers. At , the average uses Lean's total division and is zero; this initial value does not affect an asymptotic statement. The positive Brownian scale is finite. The parameters satisfy , and . The normal and STS quantiles appear as real parameters pinned by their distribution-function equations, avoiding an unbounded or empty real infimum. Expected nonnegative lengths and scales are integrals valued in . The class explicitly requires measurability of , the standing convention needed for its equality with .
The corollary retains the entire class and Assumption (2.1), with on all continuous paths. It cannot be replaced by a statement about a single easy functional or by assuming the bound on an auxiliary criterion. Useful contributions include the Brownian bridge independence theorem, the normal scale-mixture identity, distribution-function regularity, and the asymptotic expectation result.
Queueing analysis constantly moves between two kinds of long-run averages: the fraction of time a system spends in some set of states, and the fraction of arriving customers who find it there. Waiting-time formulas for the M/G/1 queue, blocking probabilities in loss systems and many decomposition arguments rest on the claim that, when arrivals form a Poisson process, the two coincide. This property is known as PASTA, Poisson Arrivals See Time Averages. It is used throughout queueing theory, inventory theory and the analysis of communication networks, usually without proof.
Before 1982 the property had been proved under strong extra structure:
Let be a probability space. On it live a process , the state of a system, with values in an arbitrary measurable space, and a Poisson process at rate , counting customer arrivals in . The interaction between and is unspecified: arrivals may change the state.
Fix a set of states with for every , and define
is the fraction of time in that is in . is the number of arrivals up to who find in , and is the fraction of arrivals who do.
The paths of are assumed left continuous with right-hand limits w.p. 1, so that an arrival is not counted as already present at its own arrival epoch. is assumed jointly measurable in . The single structural assumption is the Lack of Anticipation Assumption (LAA):
for each , and are independent.
The paper's proof of (6) uses this independence for every event of , the σ-field generated by . The mission therefore states Theorems 1–2, (6), Lemma 1, (10) and Lemma 2 under lack of anticipation with respect to : for each , is independent of . This implies the printed LAA. The printed LAA together with independent increments does not give (6) or Lemma 1, because pairwise independence of the future from the past of and from the past of is not independence from their joint past.
Under lack of anticipation (with respect to , see above), for every random variable ,
The limit may be random, and the theorem asserts nothing about whether either average converges. It asserts only that the two converge together, to the same limit.
The proof in §2 passes through the following statements, which form the milestone list:
For a Poisson process with bounded, integrable rate and , where , the same equivalence holds with replaced by the rate-weighted average . Display (12), , is its analogue of (3).
Theorem 1 justifies replacing customer averages by time averages, and conversely, in any model where arrivals are Poisson and the system does not anticipate them. Examples are queue-length distributions seen by arrivals in M/G/c systems, blocking probabilities in Erlang loss models, and state probabilities at arrival epochs in networks with Poisson external input. It needs no ergodic theory of the observed process: convergence of one average has to be established separately, by whatever means suit the model, and the theorem transfers it to the other. Lemma 2 also implies versions of PASTA under weaker modes of convergence (Remark 6).
The result has been proved for four decades and is textbook material. What this mission adds is a machine-checked proof. No formalization of Theorem 1 in a proof assistant is known. A complete development would also contain machine-checked versions of several standard facts not yet available in Mathlib:
The naive argument conditions on the arrival epochs and claims that each arrival "samples" the state at a uniformly random time. This fails because arrivals influence the state: after an arrival, a queue-length process is no longer independent of the arrival stream. LAA only says that the future increments of are independent of the past of . The difficulty is to turn this one-sided independence into an almost-sure statement about long-run averages, along every path and at all times rather than only at fixed ones.
On the technical side, the expected-value identity (3) needs a limit of grid sums. That limit relies on left continuity: without it, satisfies LAA with but . The passage from expectations to a strong law needs a martingale structure and a second-moment bound, and the interpolation between grid times needs a pathwise argument.
Welcome contributions:
All of these are useful well beyond this mission.
An assembly system must coordinate the production of components that meet at a common downstream item. A shortage of any required component can delay the finished product, while producing a component too early incurs holding cost. In Rosling's 1989 study, the central question is whether optimal decisions for such a tree can be understood using the simpler theory of a pure series inventory system. The paper proves an equivalence when the initial inventory positions are in a condition it calls long-run balance. That equivalence gives a precise route from an assembly network to serial inventory control without discarding its lead times or its discounted costs.
There are items in a tree rooted at end item . Every item has one immediate successor ; one unit of each component is needed for an end unit. Let be the production or delivery lead time of item . The total lead time is the sum of lead times on the path from to the end item, with , and the equivalent lead time is . Items are indexed so that is nondecreasing. These definitions and indexing conditions are in §§1–2 of the paper.
At the beginning of each period , outstanding orders arrive, the controller chooses the post-order echelon position , and then demand for the end item occurs. The pre-order position is , while is the position of predecessor from orders old enough to arrive after its lead time. A decision is feasible when for every immediate predecessor of . Decisions depend only on demands already observed. The demands are independent and identically distributed, nonnegative, and have a density and a finite positive mean.
The discounted Problem P charges echelon holding cost for item and a shortage coefficient for the end item. Its discount factor is . The objective is the expectation of the sum over periods of the holding charges and the expected end-item shortfall over demands, with a constant independent of the policy. The paper's Assumption requires every and . The system is in long-run balance in period when positions of adjacent items, compared at the same age relative to total lead time, satisfy equation (5):
The equivalent series system has successor , lead time , the same demand law and shortage coefficient, and holding coefficient . Theorem 2 states that its optimal policies and those of the assembly system agree when the assembly system is initially in long-run balance. In the formal statement, the first inclusion is unconditional; the reverse inclusion is conditional on Problem P attaining an optimum:
The target includes Lemmas 1 and 2, Theorem 1, Corollary 1, and the cost identity displayed in the proof of Theorem 2. Lemma 1 limits excess production, Lemma 2 gives a production lower bound, Theorem 1 describes when long-run balance is reached and preserved, and Corollary 1 uses the adjacent series position in that result. Each is stated at the strength given on pp. 568–569 of the paper.
Theorem 2 identifies the same policy choices in a tree assembly problem and a series problem whose stages have modified lead times and holding coefficients. It makes the serial interpretation exact for initially balanced systems and supports the paper's later discussion of series-system calculations. The statement is an equivalence of optimal policies, rather than just an equality of numerical values, so both the feasible-policy comparison and the cost comparison matter.
The theorem and its supporting results are proved in the 1989 paper; they have not been machine-checked in this development. A complete formalization would supply a reusable account of finite-history inventory policies, random demand histories, echelon positions, and extended-real discounted objectives. The published serial model SupplyChainTheory_multiechelon represents a different stage-indexed system; the assembly tree, its initial pipeline, and Problem P still need their own definitions. The paper's order-up-to Corollary 2 relies on an extension of earlier serial results and is outside this target.
The first natural comparison is to replace the tree's predecessor constraints with adjacent-item constraints. Those feasible sets are not equal for arbitrary states: positions at different total lead times can cross, and initial orders placed before period 1 affect the earliest periods. Long-run balance controls the necessary position comparisons, but equation (5) is empty for an item with . The printed proof also uses a middle inequality outside the range covered by equation (5) when an equivalent lead time vanishes. A faithful statement must account for these boundary cases without defining the series problem through the assembly problem's optimal policies.
Items use the paper's indices , with and . Lean period is paper period ; the policy sees exactly earlier demands. The common demand law is a probability measure on the reals, concentrated on nonnegative values, absolutely continuous with respect to Lebesgue measure, integrable, and of positive mean. The law of demand over periods is the pushforward of a finite product law under summation. Feasibility and the optimal-policy bounds are almost-sure statements, so changes on null histories do not alter them. Pathwise balance results quantify over one nonnegative demand path.
Initial positions include the orders placed before period 1. Their ages are monotone and obey the predecessor constraints inherited from that past. In addition to the paper's initial long-run balance, a separate boundary condition carries the missing comparison when . Discounting is restricted to : at the paper specifies average cost through a separate limiting prescription. The formal cost lies in the extended reals and is computed from its positive and negative parts; under the Assumption, feasible policies have a finite negative part. The policy-independent constant of equation (2) is omitted from both systems. “Optimal” means feasible and no more costly than every feasible policy, never a default value of an empty infimum.
The series system is built as a second instance of the same model, using the paper's successor, lead-time, and holding-coefficient transformations. Its cost and constraint (3) are then computed by the shared definitions. Contributions toward the lead-time identities, almost-sure policy comparisons, finite-time balance theorem, and extended-real cost identity are all part of the scope.
Axiomatic bargaining theory asks which rule should divide a set of feasible utility vectors among a group of agents, and answers by listing properties a reasonable rule must have and determining the rules that have them. Nash's solution (Nash 1950) and the Kalai–Smorodinsky solution (Kalai and Smorodinsky 1975) are the two classical answers for a fixed set of two agents. Both characterizations take the number of agents as given.
In many division problems the group is not fixed: a supply of goods that was to be shared among some agents must later be shared among more. Thomson (1983) (Math. Oper. Res. 8:319–326) introduced a framework in which the population varies and a solution is a family of rules, one for each finite group. He proposed an axiom tying the rules for different groups together: when new agents arrive and the resources stay fixed, none of the original agents should gain (population monotonicity). The paper shows that this axiom, combined with four standard ones, singles out the Kalai–Smorodinsky solution.
Timeline.
The agents are the natural numbers, and a group is a nonempty finite set of agents. For a group , is the space of real vectors indexed by , and its nonnegative orthant. For vectors, means for every , means for every , and means with .
A division problem for is a set that is compact, convex, contains a strictly positive vector, and is comprehensive: if and , then . The class of these problems is . The subclass also requires that whenever and , some satisfies .
A solution chooses a point for every group and every . The ideal point of is , with . The Kalai–Smorodinsky solution selects the largest point of on the segment from the origin to :
The axioms on a solution are:
For every solution ,
Two further statements accompany the goal. Corollary 2 says that no solution satisfies PO, An, S. Inv and Mon. Lemma 1 says that some solution other than satisfies WPO, An, S. Inv and Mon.
The theorem identifies the Kalai–Smorodinsky solution as the only rule, among those treating agents symmetrically and ignoring utility units, under which an arrival of new claimants never benefits existing ones. Corollary 2 shows that weak Pareto-optimality cannot be strengthened to Pareto-optimality. Lemma 1 shows that continuity cannot be dropped. Together they fix the logical boundary of the result. The replica construction of the appendix is a reusable device: a problem in which every agent of a larger group faces an exact copy of one agent's situation.
The result has been proved since 1983. It has not been machine-checked, and to our knowledge no proof assistant library contains bargaining problems, solutions or the Kalai–Smorodinsky solution. The mission produces these definitions and checks the full argument, including two steps the paper asserts without proof. One is that the replica problem has the required slices. The other is that problems satisfying condition (c) are dense in the Hausdorff metric. Formalizing the paper also exposes a printed slip: Theorem 2 is stated as an equivalence, but only one direction is true and proved, and only that direction is stated here.
Theorem 1 asks for routine but real convex analysis. Continuity of requires the ideal point and the maximal scalar to move continuously with in the Hausdorff metric. Comprehensiveness and the strictly positive vector are what make this work.
The substance is in Theorem 2. The first thought is to compare with inside alone, using only WPO, An and S. Inv. That cannot work: Lemma 1 exhibits a solution satisfying all four axioms that differs from , so the argument must leave the group . The proof builds a larger problem in which every member of an enlarged group faces a copy of the worst-treated agent's position. Mon then caps each agent's payoff in , and WPO fails at the diagonal point . Choosing the groups and bijections, and verifying that each slice of the convex comprehensive hull is exactly the intended copy, is the delicate part. The paper dismisses it as "clear".
Theorem 3 needs the density of in . An approximating problem must lose every flat face on its weak Pareto boundary while staying compact, convex and comprehensive.
Agents are ℕ, where the paper uses ; this relabelling is harmless. Groups are nonempty: for the empty group, is a point and WPO would hold for no solution, so the page's "finite subsets" is read as nonempty finite subsets. A group is a Finset ℕ, and is the function type P → ℝ, whose metric is the sup metric. Hausdorff convergence uses Mathlib's extended Hausdorff distance Metric.hausdorffEDist. Convergence in it is equivalent to Euclidean Hausdorff convergence, because the norms are equivalent.
A solution is a total function on all sets, together with the hypothesis IsSolution F that for . Every axiom quantifies over problems in only, and " is the Kalai–Smorodinsky solution" means agreement on every . Two formalizations of the goal would be trivial or false, and the statements here rule out both: one that equates and as functions, and one that drops IsSolution.
The remaining conventions are these.
sSup. Both suprema are attained on .P ≃ P'.Deviation from the page. Theorem 2's printed "if" direction is false, so only "only if" is stated. For example, choosing on and elsewhere gives a solution with that violates S. Inv. The replica milestone states the appendix construction existentially, for a generic agent instead of agent 1.
Out of scope: Theorem 4 (solutions defined on only, whose necessity proof is a sketch), and the remarks of §4.2–§4.4.
A complete development needs Hausdorff-metric continuity of maxima over compact sets and the convex comprehensive hull. It also needs elementary facts about slices and relabellings of comprehensive sets. All of these are reusable for other bargaining and fair-division formalizations. Contributions are welcome on any milestone, and on lemmas about that several milestones share.