Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A quasi-birth-and-death process moves on levels and, within a level, among finitely or infinitely many phases; its stationary distribution is matrix-geometric, , which is the central result of the matrix analytic method (Neuts, Matrix-Geometric Solutions in Stochastic Models, 1981; Latouche & Ramaswami 1999, Chapter 6). Several queueing models do not fit on a line of levels but on a tree. The standard example is a single-server queue with Poisson arrivals, phase-type service and last-come-first-served discipline: an arrival interrupts the customer in service, who keeps a record of the phase in which the service was interrupted. The state must then remember the whole stack of interrupted phases, not only its height, and the levels branch into an -ary tree. Multi-class LIFO queues, some random-access protocols and stack-based models in telecommunications have the same shape (Yeung & Sengupta 1994; Takine, Sengupta & Yeung 1995).
Chapter 14 of Latouche and Ramaswami shows that the matrix analytic picture survives this branching: the stationary distribution on the infinite tree is a product of matrices, determined by one expected-time matrix . This mission formalizes that chapter.
Fix a set of phases , with finite or countably infinite. A state is either the empty stack or a stack of phases with . The states , ranging over the phases, form the stack descriptor (or node) ; these nodes form an -ary tree whose root is (stacks of size one) and whose root's parent is .
The process is a continuous-time Markov process. Its data are two vectors and matrices indexed by the phases, and its only transitions are
Its generator (the book's (14.2)–(14.3)) is assumed to be irreducible, and the data are otherwise arbitrary.
When the process is positive recurrent, meaning that the expected time to return to any state is finite, it has a unique stationary probability vector with , and . We write for its value at and for its subvector on the node .
The key object is the matrix . Its entry is the expected total time spent in the state , starting from , before the first visit to . From it the chapter builds:
If the process is positive recurrent, then for all and all phases ,
The matrix-product form reduces the stationary distribution of a process on an infinite, exponentially branching state space to a single matrix. Equations (14.6) give a monotone fixed-point scheme for computing it, and Lemmas 14.3.4–14.3.6 turn the stability question into a spectral condition on , which is explicit in the rank-one case covering M/PH/1 queues under LIFO. Later work on tree-like quasi-birth-and-death processes and on multi-type branching structures in queueing (Bini, Latouche & Meini 2005) builds on exactly these statements.
These results are proved in the book, but none of them is machine-checked, and the platform has no continuous-time Markov processes on countable state spaces with expected-time quantities. The mission adds that substrate: generators, jump chains, expected sojourn times, return-time positive recurrence and stationary vectors. It also states the chapter's results over it.
The proof in the book is three lines: it applies a general censoring theorem to the subtree below a node. A formal proof needs that theorem for continuous-time processes on a countable state space. It also needs the homogeneity of the tree: is defined at the root node only, and the fact that every other node's expected-time matrix equals it is part of what must be shown, by an explicit isomorphism of subtrees. The stationary vector is characterized by , a system with infinitely many unknowns; its equality with occupation-time ratios requires recurrence and the absence of explosion. The stability lemma 14.3.4 has a one-line proof whose "if" direction leaves recurrence unaddressed, so a complete argument must supply more than the page does.
Phases are an arbitrary countable type, with finiteness assumed only in (14.6), in the second statement of Lemma 14.3.4 ("if is finite") and in Lemma 14.3.5. That lemma also carries the irreducibility of , which is the hypothesis of the quasi-birth-and-death drift criterion to which the book reduces it. A state is none (the empty stack) or a pair of a list of phases (bottom first) and the phase at the top.
The process is encoded by its embedded jump chain and holding rates. Probabilities are sums over finite trajectories of products of jump probabilities. Expected times are expected visit counts multiplied by mean holding times, valued in . , , and are defined by what they mean, never by (14.4) or (14.6) and never as "the minimal nonnegative solution" of an equation; this rules out the formalization in which the goal holds by definition. Positive recurrence is the return-time notion, never "a stationary vector exists", and the stationary vector is a probability vector, so the trivial solution is excluded. Matrix identities involving stationary probabilities are stated coordinatewise in , which also asserts the finiteness of the right-hand sides. The inverse in (14.6) is stated as a two-sided inverse together with the finiteness of .
Beyond the paper. No variant is posed. Corollary 14.3.2 writes , a symbol the chapter does not define otherwise; it is formalized as the level-1 vector , the only reading consistent with the corollary's own case .
Useful contributions beyond the listed statements: a general censoring theorem for continuous-time chains on countable state spaces, and the equivalence between return-time positive recurrence and the existence of a stationary probability vector for nonexplosive irreducible generators.
In a quasi-birth-and-death process (QBD) a queue length or buffer content (the level) moves up or down by at most one per step while an auxiliary Markov environment (the phase) modulates the rates. When buffers are bounded the level lives in , and a basic performance question is how long it takes, on average, for an initially empty buffer to fill: the expected first passage time from the bottom level to the top level. Overflow and loss analyses of finite-buffer queues in telecommunication and manufacturing models ask exactly this quantity, and higher moments follow from the same linear systems.
Chapter 11 of Latouche and Ramaswami's Introduction to Matrix Analytic Methods in Stochastic Modeling (SIAM 1999) gives two exact algorithms for it: a linear level reduction, adding one level at a time (Gaver, Jacobs and Latouche, Advances in Applied Probability, 1984), and a reduction by bisection that doubles the number of levels at each step (Latouche and Ramaswami, Stochastic Models, 1995), reaching levels in about steps. This mission formalizes the probabilistic identities on which both algorithms rest.
Fix and a finite set of phases. The states are pairs with level and phase ; the level is . A finite QBD is the discrete-time Markov chain with block-tridiagonal transition matrix (10.2): from level it moves up one level with the probability matrix , down one level with , and stays in its level with at level , at level and in between. The matrix is stochastic and the chain is irreducible.
Let . For levels :
with and . For let be the first exit time from the block , and let
All of these are taboo quantities of the chain: probabilities of sets of trajectories and expected values of hitting times.
For , the matrix is nonsingular and
The goal is the identity the bisection algorithm ends with. Milestones 3 and 4 are its doubling step, and milestones 1 and 2 give the linear algorithm.
Lemmas 11.2.1–11.2.2 justify the Linear Level Reduction Algorithm (Figure 11.1 of the book), which is block LU factorization of for the transient part of the chain. Lemmas 11.3.1–11.3.3 justify the Reduction by Bisection algorithm (Figure 11.2): it computes with products of matrices instead of , using the fact that the levels form a homogeneous block. The same decompositions, applied to the matrices and , underlie the doubling and cyclic-reduction methods for infinite QBDs.
These results are proved in the book, partly in condensed form: Lemma 11.3.3 is left to the reader, and of the six relations of Lemma 11.3.2 only (11.13)–(11.15) and (11.17) are argued explicitly, the others "in a similar manner". No machine-checked version of any of them exists. The Prove2Me platform has finite and countable Markov chains (MarkovMixing) and scalar hitting-time results (MarkovMixing.gamblers_ruin), but no block-structured first passage theory. This mission supplies the strong-Markov decompositions at hitting times of level sets, in matrix form, together with the nonsingularity arguments that make the formulas well defined.
Every identity is a first-passage decomposition: condition on where the chain first enters a level, or first leaves a block of levels. Three points stop the obvious argument from being routine. First, the quantities are infinite sums over trajectories, and splitting a trajectory at a hitting time must be done as an exact bijection of taboo paths, with expected times given as tail sums. Second, the bisection lemmas compare exit probabilities of different blocks of levels. is defined for the levels , but the relations use it for the shifted levels . The shift is legitimate only because the transition matrix is homogeneous on the levels , and the identification has to be proved. Third, each inverse requires a spectral argument: the series converges because irreducibility forbids returning to forever without visiting . Turning this into nonsingularity of a real matrix needs a bound on the spectral radius of a substochastic matrix, not a mere appeal to probability. Finiteness of every expectation likewise rests on irreducibility of the finite chain.
States are pairs in with a finite type. The transition matrix is (10.2) for the levels and elsewhere. The standing assumptions (nonnegative blocks, stochastic rows, , irreducibility on the levels ) form one predicate. Probabilities and expectations are defined as sums over finite taboo trajectories of products of one-step probabilities, valued in . Expectations are tail sums . The quantities are defined, as in the book, for the chain itself, and the theorems use them only in the book's range . Identities without an inverse are stated in . Identities with an inverse are stated between real matrices: each matrix inverted is proved nonsingular, and each expectation that is read as a real number is proved finite, both as part of the conclusion.
None of , , , , may be defined as the solution of the chapter's equations. Doing so would make every target true by definition, so they are defined only as hitting quantities of the chain. Lemma 11.2.2 prints , and the two printed expressions differ. The faithful statement uses the second one, .
Beyond the paper. One variant is posed, level_by_level_corrected (kind: corrected). It states Lemma 11.2.2 with , the recursion (10.3) the proof cites. Evidence: with one phase, and , the printed first expression gives , whereas .
A complete development needs the following. Strong-Markov path splitting for path-sum hitting quantities is reusable for any countable chain. So are the convergence of and the nonsingularity of for substochastic matrices that cannot keep mass forever. Contributions of either as standalone lemmas are welcome.
Quasi-birth-and-death processes (QBDs) are Markov chains on pairs (level, phase) in which the level moves by at most one at each step. They model queues in random environments, priority queues, and many other systems treated by matrix-analytic methods (Latouche & Ramaswami 1999). Their stationary distribution, when it exists, is matrix-geometric, and computing it reduces to computing one matrix: the first-passage matrix , which records where the chain first lands when it moves down one level. Every algorithm for a QBD's stationary distribution is, at its core, an algorithm for (or for the related matrices and ).
The logarithmic reduction algorithm of Latouche & Ramaswami (1993) computes with a number of iterations proportional to the logarithm of the number needed by the basic linear schemes. It is still among the fastest general-purpose methods, alongside the closely related cyclic reduction (Bini, Latouche & Meini 2005). Its correctness rests on one identity: an infinite series built from a purely algebraic recursion equals the probabilistically defined matrix . This mission formalizes that identity, Theorem 8.4.1 of Latouche & Ramaswami's textbook, together with the intermediate equations of its proof and the convergence statement Theorem 8.4.2.
Let be a countable set of phases, finite or infinite, and let be nonnegative matrices indexed by . The homogeneous QBD is the Markov chain on the states , the level and the phase, whose transition matrix (8.1) is block tridiagonal:
The matrix is assumed stochastic and irreducible, which is the standing assumption of Chapter 8. Write for level , , and .
The first-passage matrix is
It is the probability, starting at level 1 in phase , of ever reaching level 0 and of doing so first in phase .
With the book's convention , the logarithmic reduction recursion is
with . It involves only the blocks .
where the empty product is the identity. The goal also asserts that every inverse and in the recursion has finite entries.
The series identity is what makes the logarithmic reduction algorithm (Figure 8.6 of the book) correct. Its partial sums are the algorithm's iterates, and the identification with the linear-progression iterates gives the quadratic convergence and the iteration count . Theorem 8.4.2 explains why the algorithm is numerically stable: the matrices it inverts approach the identity.
The results are classical and proved on paper; none is machine-checked. A formalization yields a verified link between a fast numerical recursion and the probabilistic object it computes. It also yields a reusable path-sum encoding of first passages for level-structured chains, on which the other algorithms of Chapter 8 (linear progression, cyclic reduction, the series for in Theorem 8.4.4) can be built.
The book's proof is short because it relies on the strong Markov property and spatial homogeneity. With an informal stopping-time calculus, each identity is "conditioning on the state at time ". In a path-sum formalization each such step becomes a bijection between sets of finite trajectories: concatenation at a first-passage epoch, together with the shift of levels by a multiple of . That shift moves the trajectories between levels where the transition matrix is homogeneous. The infinite sums over trajectories, the series inverse and the matrix products over infinitely many phases must be rearranged in . Proving that each series inverse is finite needs irreducibility; it is not automatic.
Theorem 8.4.2 needs more. Its proof uses , which fails when is periodic. As recorded under Beyond the paper, the printed limits for (ergodic case) and (transient case) are false in general, so a disproof of that milestone is a legitimate outcome.
Phases form a countable type ι ([Fintype ι] only for Theorem 8.4.2). States are ℕ × ι with levels counted from 0, and the transition matrix is the function qbdP B A₀ A₁ A₂. Matrices with nonnegative entries take values in ℝ≥0∞: products are tsums there, and every inverse in the recursion is the series (seriesInvE, the book's convention on p. 109). Finiteness of those series is asserted in the conclusions, never assumed. , and the passage probabilities of (8.37) and (8.45)–(8.48) are sums over finite trajectories of products of one-step transition probabilities. Positive recurrence ("ergodic" in the book) is the return-time notion; transient means not recurrent. "The stationary probability vector" is a stationary probability vector assumed to be the only one. Limits are entrywise.
is never defined as a solution of or of , nor as the value of the series; either would make the goal true by definition. Conversely, and are defined by the recursion, exactly as in the book, and their probabilistic meaning is a milestone.
The definitions restate the Markov-chain notions of the platform definition mm_countable locally. Reusable pieces include the path-sum first-entrance and first-entrance-after-a-visit matrices and the ℝ≥0∞ matrix algebra. Contributions are welcome on any milestone, on the series inverse's finiteness, and on the disproof of Theorem 8.4.2.
Beyond the paper. One corrected variant is posed. HLU_limits_corrected replaces the false clauses of Theorem 8.4.2 by (ergodic) and (transient). Evidence: a two-phase positive recurrent QBD with has , and its level reversal is a transient QBD with .
A quasi-birth-and-death process (QBD) is the matrix generalization of a birth-and-death chain: a Markov chain on pairs (level, phase) that moves at most one level per step. QBDs model queues in random environments, multi-server and priority systems, and communication links with correlated traffic, and their analysis rests on two matrices: the first-passage matrix and the rate matrix . Chapter 9 of Latouche and Ramaswami, Introduction to Matrix Analytic Methods in Stochastic Modeling (SIAM 1999, doi:10.1137/1.9780898719734), shows that the spectra of these probabilistic matrices are encoded in a polynomial written directly in the transition blocks. This links the matrix analytic method to the spectral approach to M/G/1- and GI/M/1-type chains (Gail, Hantler and Taylor, Adv. Appl. Probab. 28, 1996) and is the basis of spectral algorithms for and .
Timeline. The matrix-geometric form of the stationary distribution, with as its rate matrix, is due to Neuts (Matrix-Geometric Solutions in Stochastic Models, 1981). The construction of the Jordan structure from the matrix polynomial is due to Rama Murthy, Kim and Coyle (Stochastic Models 7, 1991), who treated ; Latouche and Ramaswami adapt it to (pp. 212–216).
Fix a finite set of phases. A homogeneous QBD is a Markov chain on the states , with level and phase , whose transition matrix is block tridiagonal: from level it moves within level with probabilities and up to level with probabilities ; from a level it moves up with probabilities , stays with probabilities and moves down with probabilities . The four blocks are nonnegative matrices, and . Chapter 9 assumes that the QBD is irreducible and positive recurrent (every state has a finite expected return time), and that is irreducible.
The first-passage matrix has entries = the probability, starting from , that the chain reaches level in finite time and does so first in . The rate matrix has entries = the expected number of visits to , starting from , before the first return to level . The matrix polynomial of the chapter and its determinant are
with , , and . Vectors are in a tower for relative to an eigenvalue if is an eigenvector and for (a Jordan chain).
For a positive recurrent QBD, is a nonzero polynomial and, counting multiplicities,
Milestones 1–3 are the algebraic identities the goal's proof rests on; milestones 4–5 are the rest of the chapter's numbered results, which extend the goal from eigenvalues to the full Jordan structure of .
The result. Theorem 9.3.1 separates the roots of one explicit polynomial into the spectrum of (inside the closed unit disk) and the reciprocal spectrum of (outside it). The eigenvalues of and , including the decay rate that governs the geometric tail of the stationary distribution (§9.1), can therefore be computed from the transition blocks without first computing or . Theorems 9.4.1 and 9.4.2 go further and recover eigenvectors and Jordan chains of from the null spaces of and its derivative, which is how §9.5 reconstructs itself.
Formalizing it. The results are proved in the book; none is formalized. The platform has countable Markov chains (MarkovMixing) and no matrix analytic objects. This mission produces Lean statements of the first-passage and rate matrices as trajectory sums and connects them to polynomial matrices over , a bridge between Markov chain probability and Mathlib's characteristic polynomials and root multisets that later spectral results (M/G/1-type chains, the caudal characteristic) can reuse.
Two steps resist. First, the matrices are probabilistic: before any algebra, the matrix equations satisfied by and , the finiteness of and the location of their spectra must be derived from first-passage probabilities and expected visit counts, that is, from series over trajectories of a chain with infinitely many states. Second, that every eigenvalue of is a root of is a determinant identity, but the theorem says more: the closed unit disk contains no other root, and the roots outside it are exactly accounted for by , with multiplicities, even when is singular and has degree below . Inclusion is easy; exhaustiveness is the content, and it is where the hypothesis of positive recurrence enters. The tempting shortcut, taking to be any nonnegative solution of , does not work: such equations have several nonnegative solutions, and for the non-minimal ones the root count is false.
Phases form a finite nonempty type ι with = Fintype.card ι; blocks are real functions ι → ι → ℝ, mapped to complex matrices for every spectral statement. The QBD is the transition function qbdP B A₀ A₁ A₂ on ℕ × ι. Stochasticity, irreducibility and positive recurrence (summable return-time tails) are restated from the platform definition mm_countable. is a sum, over first-passage trajectories, of products of one-step probabilities, and a sum of taboo-trajectory probabilities; both are computed in ℝ≥0∞ and read in ℂ (matGc, matRc), and the finiteness of is part of each conclusion that uses it. is the determinant of a matrix over ℂ[X]; roots are Polynomial.roots (with multiplicity), eigenvalues are roots of Matrix.charpoly, and is ‖z‖ ≤ 1. An eigenvector is nonzero, so Theorems 9.4.1–9.4.2 carry (resp. ).
The trivializing formalization is excluded: and are never defined as solutions or minimal solutions of a matrix equation, positive recurrence is never "a stationary distribution exists", and the goal asserts so that it cannot hold through the empty root multiset of the zero polynomial.
Beyond the paper. One strengthened variant restates Theorem 9.3.1 without the irreducibility of , a standing restriction of Chapter 9 that its proof never uses (finding F3). Findings also record that "eigenvector" must be read as nonzero in Theorems 9.4.1–9.4.2 (F1) and that the proof of 9.3.1 omits the argument that , which follows from being nonsingular (F2).
Contributions welcome: first-step analysis for trajectory-sum passage matrices (useful across the whole series), lemmas relating Matrix.det of a polynomial matrix to evaluation and to reversed polynomials, and root counting for products of determinants.
In a queue with a finite buffer, a multi-server system with a capacity limit, or a communication link with a bounded number of packets in transit, the number of customers is a level that takes only finitely many values, and the rest of the state (service phase, arrival phase, environment) is a phase. The resulting Markov chain is a finite quasi-birth-and-death process (finite QBD): it moves by at most one level per step, and its transition probabilities do not depend on the level except at the two boundaries. Finite QBDs model M/PH/1/K and PH/M/1/K queues, finite-buffer multiplexers and loss systems, and computing their stationary distribution is the routine numerical task behind blocking probabilities and buffer-dimensioning.
Chapter 10 of Latouche and Ramaswami, Introduction to Matrix Analytic Methods in Stochastic Modeling (SIAM 1999), gives the standard exact method, linear level reduction, adapted from Gaver, Jacobs and Latouche (Advances in Applied Probability, 1984): remove the levels one at a time, solve the chain watched on the last remaining level, and rebuild the stationary vector level by level. The chapter shows that every matrix the algorithm computes has a probabilistic meaning, which is what makes the algorithm a probabilistic form of block Gaussian elimination rather than an algebraic trick. This mission is the tenth of a series formalizing the book.
Fix and a finite nonempty set of phases. The state space is the set of pairs with level and phase ; the level is the set of states with first coordinate , and . Five real matrices define the block tridiagonal transition matrix
so moves up one level, down one level, and (or , at the boundaries) stays. is assumed stochastic (nonnegative, rows summing to one) and irreducible (every state reaches every state). Its stationary vector is the row vector with , , , partitioned into blocks .
For a set of states, the probability, starting from , that the first visit to after time is a visit to is the sum, over all finite trajectories from to whose intermediate states avoid , of the products of one-step transition probabilities. The process restricted on has these first-return probabilities as its transition matrix.
Two families of matrices are defined by recursion. Upwards:
Downwards:
and for .
For an irreducible finite QBD, is invertible for , and
these equations determine up to a multiplicative constant. Moreover, for , is the matrix of probabilities of returning from to before a visit to , and is the matrix of first passage probabilities from to .
The goal is the finite counterpart of the matrix-geometric property , of the infinite QBD (Theorem 6.2.1 of the book): with a finite upper boundary the matrices depend on the level, and the stationary vector is a product of level-dependent factors. Together with Lemma 10.1.1 and Theorem 10.1.2 it justifies the two block-elimination algorithms of the chapter (bottom-up and top-down), whose cost is linear in the number of levels, and Theorem 10.4.1 reduces the whole computation to one system for the M/PH/1/K and PH/M/1/K queues.
The results are classical and proved in the book, except that Theorem 10.1.3's proof is omitted as "a repetition of the argument" for Theorem 10.1.2. None of them is formalized. The mission produces a formal account of finite block tridiagonal chains, taboo first-entrance probabilities as trajectory sums, and the link between restricted (censored) chains and block Gaussian elimination, all reusable by the later chapters on first passage times and level-dependent QBDs.
The algebra of block elimination is routine once the inverses exist; the content is that they exist and that the recursively defined matrices are the probabilities claimed. The obvious approach, verifying by substituting the recursions, proves neither: it presupposes invertibility of and , which holds only because the corresponding taboo matrices are strictly substochastic in an irreducible chain, and it says nothing about first passage probabilities. Identifying the recursion with the probabilities requires decomposing trajectories at their visits to a level, inductively in the number of removed levels, and passing to the limit in infinite sums of trajectory weights. Uniqueness of the solution, and the rank-one reduction of Theorem 10.4.1, then rest on the first passage matrices being stochastic.
The state space is Fin (M + 1) × ι with ι a nonempty Fintype, levels counted from ; the transition matrix is the explicit block tridiagonal qbdMatrix, and every theorem assumes , stochasticity and irreducibility. Row vectors act on the left (vecMul). The first-visit probabilities are sums over of firstEntryStep, a finite sum of products of one-step probabilities over trajectories with intermediate states avoiding the taboo set, and every statement asserts the convergence of that series (HasSum) to the stated matrix entry. , and are defined by the book's recursions with Mathlib's matrix inverse, which is on a singular matrix; every theorem therefore concludes the invertibility of each matrix it inverts, and none assumes it. Defining or as the first-passage probabilities and the theorem as their recursion, or assuming the inverses exist, would trivialize the mission; both are excluded by this design. The probabilistic meanings in Lemma 10.1.1 and Theorem 10.1.3 are part of the conclusions. "Determined by" and "given by" are formalized as uniqueness of the solution (up to a constant for Theorem 10.1.3, which states no normalization).
The basic Markov chain notions restate the public platform definition mm_countable. Results stated in the chapter but not included: Lemma 10.3.1 and Theorem 10.3.2 (they need the rate matrices , of the infinite QBD and its level reversal) and the folding method of §10.2 (unnumbered). Contributions of general lemmas on censored finite chains and on substochastic taboo matrices are welcome.
Quasi-birth-and-death processes (QBDs) are the workhorse models of queueing theory, telecommunications and inventory systems whenever a counting variable (the number of customers, packets or items) moves up or down by one while a second, finite or countable, phase variable records the state of the environment: the phase of a service-time distribution, of an arrival process, of a server's availability. The single most used fact about them is that the stationary distribution is matrix-geometric: the probability vector of level is the vector of level multiplied by a fixed nonnegative matrix . The result goes back to Evans (1967) for scalar , was developed into a general theory by Neuts (Matrix-Geometric Solutions in Stochastic Models, 1981), and is proved in Chapter 6 of Latouche and Ramaswami (Introduction to Matrix Analytic Methods in Stochastic Modeling, SIAM 1999) by a direct probabilistic argument in which is a matrix of expected numbers of visits. This mission formalizes that chapter: the matrix-geometric property, the probabilistic matrices , , and the equations relating them, the spectral radius bound, and the boundary equations.
Fix a set of phases, finite or countably infinite, and four square matrices indexed by . A homogeneous QBD is the discrete-time Markov chain on the states , with level and phase , whose transition matrix is block-tridiagonal:
From level the chain moves up one level with probabilities , stays with , moves down with ; from level it stays with and moves up with . The level is the set . The chain is assumed irreducible and positive recurrent (finite expected return time to every state), and denotes its stationary probability vector, partitioned by levels.
Four families of matrices indexed by phases carry the theory, all defined by what they mean for the chain:
The book writes for the series .
For a positive recurrent QBD there is a nonnegative matrix with
where is the expected number of visits defined above at every level (in particular finite and independent of ) and is the expected number of visits defined above at every level . The goal includes these interpretations: they are what distinguishes the theorem from the bare existence of some matrix with .
The matrix-geometric form reduces the infinite stationary system to a single matrix and a finite boundary vector : every marginal distribution and moment of the level follows in closed form (for instance ), the level has a discrete phase-type distribution, and the nonlinear equations for , , are the starting point of every numerical method for QBDs (linear and logarithmic reduction, Chapter 8 of the book). Downstream chapters of this series (stability, minimal solutions, spectral analysis, level-dependent and tree-structured processes) all take these objects and relations as given.
Formalizing the chapter produces, on top of the textbook proof, a machine-checked bridge between path-level probability (expected numbers of visits as sums over taboo trajectories) and matrix algebra over a possibly infinite phase set. No part of the matrix analytic layer is formalized on the platform, which has countable Markov chains and scalar birth-and-death formulas only; the results here are classical and proved, not formalized.
The textbook proof is three lines long because it invokes two theorems on censored chains (Theorems 5.2.1 and 5.2.3 of the book) that express the stationary vector of one part of the state space through that of the complement and the expected-visits matrix . Neither is available: a solver must build the censoring argument, or an equivalent regenerative argument, from path sums. The second difficulty is homogeneity: , , , are defined level by level, and their independence of the level is a statement about a bijection between taboo trajectories at different levels, not a notational convenience. Third, the phase set may be infinite, so the matrix products are infinite series and the formal manipulations of the book (postmultiplying by , for instance) are not available as written. The obvious first idea, to define as a solution of , is ruled out: that equation has several nonnegative solutions and taking one as a definition makes Theorem 6.2.10 vacuous.
States are ℕ × ι with ι an arbitrary countable type with decidable equality; levels are counted from ; the transition matrix qbdP B A₀ A₁ A₂ is (6.1) exactly, so the block structure is built in. Irreducibility, positive recurrence (the return-time notion at every state) and stationarity (nonnegative, summing to one, ) restate the platform definition mm_countable. The matrices , , , , are sums over finite taboo trajectories of products of one-step transition probabilities, valued in (ℝ≥0∞); vector–matrix products, matrix powers and are computed there, so no summability hypothesis appears and no junk value can occur. The goal asserts that these probabilistic quantities equal the entries of real nonnegative matrices. None of , , , is defined as a solution of the chapter's equations; a formalization that did so would make the milestones true by definition and is excluded.
Corollary 6.2.4 and Lemma 6.3.1 assume finitely many phases ([Fintype ι]): the first because the book does, the second because is then a genuine matrix inverse and "the unique solution" ranges over all real vectors of ; invertibility of and finiteness of the entries of and are conclusions, never hypotheses. The spectral radius is taken over . The section's temporary aperiodicity assumption, used in the book only to read as a limit, is not imposed.
A complete development needs: the strong Markov property in path-sum form (first-passage decompositions of taboo sums), censored chains on a countable state space, uniqueness of the stationary vector of a positive recurrent irreducible chain, and the Perron–Frobenius-type fact that a convergent series forces . The path-sum decompositions and the matrix algebra are reusable across the whole series and in any countable-state Markov chain development; contributions of such general lemmas are welcome.
Quasi-birth-and-death processes (QBDs) are the standard Markov models of queues with structured arrivals and service: a queue fed by a Markovian arrival process, a server with phase-type service times, a buffer in a telecommunication link with a fluctuating source. Their stationary distribution has the matrix-geometric form (Neuts, Matrix-Geometric Solutions in Stochastic Models, 1981), but that form only describes a chain once it is known to be positive recurrent. Chapter 7 of Latouche and Ramaswami, Introduction to Matrix Analytic Methods in Stochastic Modeling (SIAM 1999, doi:10.1137/1.9780898719734), answers the prior question: when is a QBD stable? The authors stress that the two issues are distinct, "a fact which was somewhat blurred in early presentations of matrix analytic methods" (p. 147).
The answer for finitely many phases is the mean-drift criterion: average the one-step change of the level over the stationary law of the phase; the QBD is positive recurrent exactly when this average is negative. The criterion goes back to Neuts (1981); the book's proof follows the Markov-modulated random walk argument of Asmussen (Applied Probability and Queues, pp. 235–239).
A QBD is a Markov chain on the states , where is the level and ranges over a set of phases, finite or countably infinite. The level is the set of states . Given matrices indexed by phases, the transition matrix (6.1) is block tridiagonal. From level the chain moves within according to and up according to ; from level it moves up according to , stays according to and moves down according to . The chain is assumed irreducible throughout. The phase matrix is stochastic.
Let be the first passage time from to . The first-passage matrix has entries . is stochastic if and substochastic if with at least one strict inequality. The matrix , (7.2), has entries . The restricted chain on has transition matrix . is the expected number of visits to from before the first return to , and . The rate matrix has entries , the expected number of visits to from before the first return to .
A state is recurrent if the chain returns to it with probability one and positive recurrent if the expected return time is finite. The QBD is null recurrent if it is recurrent but not positive recurrent, and transient if it is not recurrent.
When the number of phases is finite and is irreducible, denotes the stationary probability vector of (, , ), and the mean drift is
For an irreducible QBD with finitely many phases and an irreducible ,
The result itself. Theorem 7.2.3 decides stability from , , alone, by solving one finite linear system for . Theorem 7.1.1 and Corollary 7.1.2 give the same classification through and , but deciding numerically whether is fragile when is close to (p. 151). The drift criterion is what licenses the matrix-geometric solution of Chapter 6 and the algorithms of Chapter 8 for a given model.
Formalizing it. All of these results are proved in the book, and none is machine-checked. The platform has countable Markov chains (recurrence and positive recurrence via return times) and scalar queueing classifications (, embedded chains), but no level–phase chain, no first-passage matrix and no drift criterion for Markov-modulated walks.
The obvious argument says: the level is a random walk whose increments have mean , so it drifts to when . But the increments are not independent; they are driven by the phase chain. The law of large numbers for the Markov-modulated walk gives . That settles only up to recurrence; positive recurrence needs a separate expectation bound. At it settles nothing. That case takes most of the book's proof: it shows the expected passage time is infinite, using the class structure of (Theorem 7.2.1) to compare passage times to a fixed phase. In the reducible case the phases outside the closed classes must leave in finite expected time. The printed hypothesis of Theorem 7.3.1 does not guarantee that (see below). For Corollary 7.1.2, the passage from to " is stochastic" is left implicit in the printed proof, and the identity it displays for carries a spurious "" (finding F2).
States are pairs in with a phase type . It is countable in Theorem 7.1.1 and finite (Fintype) exactly where the book says " is finite". The QBD is the function qbdP B A₀ A₁ A₂, and every theorem assumes it stochastic and irreducible. Recurrence, positive recurrence, null recurrence and transience are properties of this chain, defined through return-time tails (sums over trajectories of products of transition probabilities), for every state. , , , and are defined in the same probabilistic way, with values in , so "finite" means .
The trivializing formalization is ruled out: positive recurrence is never defined as "", " stochastic" or "a stationary distribution exists", and , are never defined as solutions of (7.1) or ; with either shortcut Theorem 7.1.1 and Corollary 7.1.2 would hold by definition.
Irreducibility of a nonnegative matrix (, and their blocks) asks that some power have a nonzero entry. "After a permutation" is a bijection of the phases with . The spectral radius is taken over , together with finiteness of the entries of . The stationary vectors and are hypotheses, not choices. The countable-chain definitions restate the platform definition mm_countable locally.
Not formalized: Theorem 7.2.4 (continuous-time QBDs), which needs a continuous-time chain on a countable state space.
Beyond the paper. Theorem 7.3.1 is stated as printed, with substochastic in the book's sense (row sums at most one, one strictly less), and as printed it is false (finding F3). If contains a closed class of along which the level performs a symmetric random walk, the class criterion holds strictly yet the QBD is null recurrent; with an upward drift there it is transient. A corrected variant replaces "substochastic" by the convergence of , which is what the proof uses. A disproof of the printed item and a proof of the variant are both welcome.
A complete development needs Markov-modulated random walks, a strong law for them, the strong Markov property in path-sum form, and Perron–Frobenius facts for nonnegative matrices. These are reusable well beyond this mission (Chapters 8–13 of the book). Contributions are welcome at every milestone, including partial results such as transience for .
A quasi-birth-and-death process (QBD) is the Markov chain behind queues with phase-type service or arrivals, priority queues, and many models of telecommunication and inventory systems: a level that moves up or down by at most one per step, and a phase that carries the rest of the state. Its stationary distribution is determined by three matrices indexed by phases, , and , which no closed formula gives in general. Every numerical method for QBDs therefore solves a nonlinear matrix equation that these matrices satisfy, such as or .
Such an equation typically has several nonnegative solutions. An algorithm is useful only if it converges to the solution that has the probabilistic meaning. Chapter 8 of Latouche and Ramaswami (SIAM 1999) settles this. Each of , and is the minimal nonnegative solution of its equation. The simplest iteration, started from , increases to it. The chapter's analysis of the rate of convergence goes through the level-reversed process. The quadratic equations and the iteration go back to Wallace and to Neuts (Neuts, Matrix-Geometric Solutions in Stochastic Models, 1981); the chapter proves convergence of its algorithms by taboo arguments on the sample paths of the chain.
Fix a set of phases, finite or countably infinite, and real matrices indexed by . The homogeneous QBD is the discrete-time Markov chain on states , , , with block-tridiagonal transition matrix
From a level the chain moves up with probabilities , stays with and moves down with . From level it stays with and moves up with . The chain is assumed irreducible. No recurrence assumption is made unless stated. The level is the set of states , and .
The central objects are defined by what they mean for the chain:
For a nonnegative matrix , denotes the series , also when the matrix has infinite order. A solution of a matrix equation is minimal in a set of nonnegative matrices if for all and every solution in the set.
For every irreducible QBD:
In the first two parts the competitors are the nonnegative matrices for which the series converges; in the last two, all nonnegative matrices. In each part the probabilistic matrix is itself an admissible solution.
Minimality is what makes every algorithm of the chapter, and the logarithmic and cyclic reduction methods built on them, correct. An iteration that is monotone from and stays below every nonnegative solution must converge to the probabilistic matrix and to no other root. Without the theorem, a numerically computed root of need not be the first-passage matrix, and the matrix-geometric formula built from it could be wrong. Theorem 8.2.3 identifies the convergence rate of the linear algorithm with the caudal characteristic , which also governs the tail of the stationary level distribution.
These results are proved in the book; none of them is formalized on the platform or, to our knowledge, elsewhere. Formalization produces a machine-checked link between taboo path probabilities over a possibly infinite phase set and the algebra of nonnegative matrix equations. Chunks on logarithmic reduction, level-dependent QBDs and M/G/1-type chains reuse that link directly.
The equations satisfied by , , (Theorems 6.2.9 and 6.2.10 of the book) are not enough: minimality needs the identification of the probabilistic matrices as limits of explicit monotone sequences. That is a first-passage decomposition of taboo trajectories under the strong Markov property, carried out with sums over paths rather than with a measure on path space. With infinitely many phases, every matrix product is an infinite series of nonnegative terms, and is a series whose convergence is part of what must be shown.
The printed proof that is minimal for proceeds by contradiction against a solution lying below . It does not cover solutions not comparable with , which the definition of minimality requires (finding F3 of this mission). Lemma 8.2.1's claim that is stochastic for a transient QBD fails when is reducible (finding F1). The faithful statement is posed as printed, beside a corrected variant.
States are ℕ × ι, ι a countable type with decidable equality; levels are counted from ; qbdP B A₀ A₁ A₂ is the transition matrix above, and the level-reversed QBD is qbdP B̂₁ A₂ A₁ A₀ with an arbitrary boundary block. Stochasticity, irreducibility, recurrence and positive recurrence are the return-time notions of the platform definition mm_countable, restated locally. , , , , , , are sums over finite taboo trajectories of products of transition probabilities, with values in ; products and the series are computed there, so "the series converges" means every entry is finite. Competing solutions range over real matrices with nonnegative entries.
Defining , or as the minimal solution of one of these equations would make the goal true by definition. It is ruled out here: they are probabilities and expected numbers of visits.
Lemma 8.2.1, Theorem 8.2.3 and Theorem 8.3.1 take [Fintype ι]: the latter two because the book does, the first because its spectral-radius clause concerns a finite matrix. Lemma 8.2.1 also takes [Nonempty ι]. Spectral radii are taken over ; "substochastic" in Lemma 8.2.1 means row sums at most one with one strictly less. In Theorem 8.3.1 the inverse is the matrix inverse, and its existence is a conclusion.
Beyond the paper. One variant is posed: [Corrected] Lemma 8.2.1 with irreducible (finding F1: a two-phase diagonal QBD is transient with not stochastic).
A complete development needs first-passage decompositions of path sums, monotone convergence for -valued series, recurrence criteria for QBDs (Chapter 7), and Perron–Frobenius theory for irreducible nonnegative matrices. The path-sum toolkit is reusable across the whole series; contributions of general lemmas on taboo decompositions are welcome.
Matrix analytic methods compute the stationary distribution of structured Markov chains (quasi-birth-and-death processes, M/G/1- and GI/M/1-type chains) by working on one block of states at a time. Every such computation rests on one device: watch the chain only while it is in a subset of the state space, and describe what happens in between through expected numbers of visits to the complement. Chapter 5 of Latouche and Ramaswami, Introduction to Matrix Analytic Methods in Stochastic Modeling (SIAM, 1999, doi:10.1137/1.9780898719734), develops this device for a countable chain. It gives the relation between stationary probabilities on disjoint subsets, the Markov renewal identities between first-passage and expected-visit matrices, and the restricted (or censored) chain on . Later chapters of the book use these results to derive the matrix-geometric form and the linear level reduction algorithms. Outside queueing theory, the same censored chain appears as Meyer's stochastic complement in numerical linear algebra and as the Schur complement of .
The censored chain goes back at least to Kemeny, Snell and Knapp, Denumerable Markov Chains (Springer, 1976, Chapter 6), whom the book cites for the proof. Freedman's Markov Chains (1971) calls it the restricted process. Grassmann, Taksar and Heyman (1985) turned the construction into the GTH algorithm, which is §5.4 of the book.
Let be a countable set and a stochastic matrix: and . It is the transition matrix of a Markov chain . The chapter's standing assumption is that the chain is irreducible (every state reaches every state with positive probability) and aperiodic. Its limiting probability vector is . When the chain is positive recurrent (every state has a finite expected return time), is the stationary probability vector: , , .
For , write for the submatrix of on and . Let and . The chapter's objects are expectations and probabilities of events of the chain:
Products of these matrices sum over the indicated subset. Following the book's convention, means the series for a nonnegative matrix , also when has infinite order.
The epochs of visits to are and . The restricted process is .
Let the chain be irreducible and positive recurrent with stationary vector , and let be nonempty. Then the restricted process is defined at all times and is a homogeneous Markov chain on with transition matrix
For every initial state and ,
is stochastic, irreducible and positive recurrent, and
so is its unique stationary probability vector.
Theorem 5.3.1 reduces the stationary distribution of a chain on to that of a smaller chain on , whose transition matrix is explicit in the blocks of . Applied with a set of levels, it gives the boundary equations of every matrix analytic model in the book. Applied one state at a time, it is the GTH elimination algorithm. Theorem 5.2.1 is the general form of for birth-and-death chains, and the mission's matrix-geometric and level-reduction results depend on it. The Markov renewal identities of Theorem 5.2.3 and Lemma 5.2.4 compute and from first-passage kernels, which is how the matrices , and of quasi-birth-and-death processes are characterized in later chapters.
The results are classical and proved in the book, partly by citation (Theorem 5.3.1 refers to Kemeny, Snell and Knapp for details, and the proof of Theorem 5.2.3 is left partly to the reader). No machine-checked version of any of them exists on this platform. The platform has countable chains and stationary distributions (mm_countable), and Sennott's first-passage identities for Markov decision processes, but no censored chain and no taboo-matrix calculus. What remains is the countable-state proof in full: the strong Markov decomposition of trajectories at the epochs , and the interchange of limits and infinite sums that the book handles with Fatou's lemma.
The algebraic identity is a short computation once Theorem 5.2.1 and (5.11) are available. The content is elsewhere.
The state space is a countable type S, and the transition matrix is a real function P : S → S → ℝ. Stochasticity, irreducibility, aperiodicity, positive recurrence (summable return-time tails) and stationarity have the bodies of the public definition mm_countable, restated in the namespace MatrixAnalytic.Taboo. Every probabilistic quantity (, , , , , and the law of the restricted process) is a sum over finite trajectories of products of transition probabilities, valued in , so every series exists and an infinite expectation is . Finiteness, where the book asserts it, is a stated conclusion. is always the series of powers, never a matrix inverse. is defined by its formula, and the theorem relates it to the restricted process's law. The restricted chain's irreducibility, positive recurrence and stationary vector are stated for read as a real matrix on the subtype of states of .
A trivializing formalization is ruled out: defining , or the restricted chain's transition matrix as the series or the formula the theorems assert would make Lemma 5.1.2, (5.23) and Theorem 5.3.1 true by definition, and that is why each is defined as an expectation over trajectories. Positive recurrence is the return-time notion, never "a stationary vector exists", which would make the restricted chain's positive recurrence follow from alone.
Committed conventions:
The continuous-time results of §5.5 are not part of this mission.
Contributions that would be reusable beyond it are welcome: a strong Markov decomposition of trajectory sums at hitting times, and a library of first-passage and taboo identities for countable chains in .
Birth-and-death chains are the simplest Markov chains with an unbounded state space. They model a queue that gains or loses one customer at a time, a population that grows or shrinks by one, and a random walk with a reflecting barrier. In matrix analytic methods they serve as the scalar model for quasi-birth-and-death processes (QBDs). A QBD is a chain on pairs (level, phase) that moves at most one level per step, and its theory is the subject of most of the book. Latouche and Ramaswami (SIAM 1999, Chapter 4) give birth-and-death chains a proof that, in their words, "may appear more involved than those usually given in the literature". They do this on purpose: they want to introduce, in the scalar case, the probabilistic objects and arguments that later carry over to block matrices.
There are three such objects:
In the QBD chapters these become the matrices , and . The facts that is the minimal nonnegative solution of a quadratic matrix equation and that the stationary distribution is matrix-geometric, , are the backbone of every algorithm in the field. This mission formalizes the scalar versions.
A discrete-time birth-and-death chain is a Markov chain on with transition matrix . Here whenever . Throughout, the chain is irreducible, i.e. and for every . The spatially homogeneous chain has the following transitions:
Here , , and .
The taboo probability is the probability that the chain started in is in at time without visiting at times . It is the sum, over all such trajectories, of the products of their one-step transition probabilities. For the book defines:
, and are the corresponding generating functions .
A state is recurrent if the chain returns to it with probability one. It is positive recurrent if, in addition, the expected return time is finite. A stationary distribution is a nonnegative vector with and . The limit probabilities of an aperiodic chain are .
For the spatially homogeneous chain:
and for every the first-passage probability is the minimal nonnegative solution of
Theorem 4.2.5 is the scalar prototype of the minimal-solution characterization of the matrix (Theorem 8.1.4 of the book). The quadratic always has the root . That root is the first-passage probability only when the chain is recurrent. In the transient case the probability is the other root . So "solves the equation" does not identify , and minimality is the selection rule that does. Theorems 4.2.1 and 4.2.3 give the complete classification of birth-and-death chains and the product form of their stationary distribution, and Theorem 4.2.4 gives the geometric law . These two are the scalar forms of the matrix-geometric theorem for QBDs.
The results are classical and proved in the book, except where the book says "the remainder of the theorem is easy to prove" or leaves a formal proof to the reader. None has a machine-checked proof on the platform. The mission produces formal proofs that work from the probabilistic definitions: the classification, the stationary distribution and the passage probabilities are all derived from sums over taboo trajectories. The platform has a related but different statement, QueueingFundamentals.BirthDeath.birth_death_steady_state. It is about solutions of the balance equations of a continuous-time birth–death process. It does not concern the recurrence or the stationary distribution of the chain itself.
The algebra is short once the probabilistic relations are available. The difficulty is in establishing those relations from path sums:
There is an obvious shortcut: solve the quadratic and pick a root. It is not available, because the statement to prove is exactly which root is the probability. Showing that solves the equation does not settle this: the root also solves it, and it is the wrong value whenever the chain is transient. Positive recurrence is defined by the expected return time, so its equivalence with needs an argument that links return times to the stationary vector.
ℕ → ℕ → ℝ.mm_countable with the same bodies, in the namespace MatrixAnalytic.BirthDeath.Beyond the paper. One variant is posed. It is a strengthening of Theorem 4.3.1 to the closed disc (finding F1). All coefficient sequences have finite sums, and there, so the identities extend by continuity. At they are exactly the relations of Section 4.2.
Reusable infrastructure includes the taboo path-sum calculus (first-step and last-exit decompositions, strong-Markov factorization of passage times) and the link between limit probabilities and expected visits. Both carry over to the QBD missions of the same series. Contributions of general lemmas about tabooProb are welcome.
Renewal processes model ordered sequences of events on : arrivals to a queue, service completions, equipment failures. Their defining feature is that successive intervals between events are independent and identically distributed. Two quantities answer most practical questions about such a process: the renewal function , the expected number of renewals in , and the renewal density . For a general interval distribution neither has a closed form; solves a renewal integral equation.
When the intervals have a phase-type (PH) distribution, the time to absorption of a finite Markov process, both quantities become explicit matrix expressions. This is the starting point of Chapter 3 of Latouche and Ramaswami's Introduction to Matrix Analytic Methods in Stochastic Modeling (SIAM 1999). PH renewal processes are the arrival streams of most matrix-analytic queueing models, and the closed form of is the template for the corresponding formula for Markovian arrival processes (Section 3.6 of the book; Neuts 1979, Lucantoni 1991).
A PH representation on phases consists of a nonnegative row vector and an matrix with , for , and nonnegative exit vector , where is the all-ones column vector. It describes a Markov process on that starts in phase with probability , moves among the phases at the rates , and is absorbed into state at rate . Throughout, is nonsingular and there is no atom at : .
The PH renewal process restarts the Markov process instantaneously after each absorption, in a phase drawn from ; the absorption epochs are the renewals. Ignoring the instantaneous visits to , the phase at time is a Markov process with generator
where is the outer product. The representation is irreducible if every phase has a path of positive rates to the absorbing state and can be reached from a phase with .
Let be the number of renewals in . The pair is a Markov process whose generator has in its diagonal blocks and just above them. Write
The renewal function of the process started with a renewal at time is . The remaining objects are the stationary vector of the phase process, the matrix , and the mean interrenewal time .
For an irreducible representation and every , the matrix is nonsingular, the series defining converges, and
The result itself. Theorem 3.1.4 gives the renewal function of a PH renewal process in closed form from the representation alone. It separates the linear term , the content of the elementary renewal theorem, from a correction that converges as to . The matrix is the deviation matrix of the phase process, and the same argument, with replaced by the vector of batch rates, gives the expected count of a Markovian arrival process (Theorem 3.6.1). Theorem 3.2.1 and Lemma 3.2.3 are the two standard ways to compute the distribution of the number of renewals: by solving a linear system of differential equations, and by uniformization.
Formalizing it. These results are proved in the book, and in the earlier literature it cites, by hand. The platform has no continuous-time Markov chain layer and no phase-type objects. The mission builds the PH renewal process from a generator and the matrix exponential, and states the counting probabilities as transition probabilities of the process . The definitions are reusable by every later mission on PH-driven queues.
The obvious route to the goal is to integrate the renewal density: . That route is unavailable here for two reasons. First, the density is itself a theorem (Theorem 3.1.2): it must be derived from the counting probabilities , which requires exchanging a derivative with an infinite sum over and controlling the tail of the number of renewals. Second, is singular (), so cannot be written as . The book's argument replaces by , which needs both the nonsingularity of (Lemma 3.1.3, which rests on the irreducibility of , Lemma 3.1.1) and the identity . A formal proof also has to relate the countable-state process to finite matrix exponentials, which the next section fixes by construction.
Phases form an arbitrary finite type; row vectors act on the left, column vectors on the right; all quantities are real. The matrix exponential is Mathlib's NormedSpace.exp. The standing assumptions of the chapter (, , , , , nonsingular, irreducibility) are hypotheses of every theorem. The counting probabilities are encoded through the generator of restricted to the levels . Since the number of renewals never decreases, the restriction is the generator of the process killed on leaving level , and is an entry block of its matrix exponential. Where the book inverts a matrix it proves nonsingular, nonsingularity is part of the conclusion. The renewal function is a series, and its convergence is asserted rather than assumed.
The renewal function is defined as an expected number of renewals, not as . That definition would make the renewal density true by construction and reduce the goal to matrix calculus.
Infrastructure that a complete development needs, and that is reusable: the matrix exponential of block upper-triangular matrices, termwise differentiation of matrix power series, uniformization of a finite generator, and the deviation matrix of an irreducible finite generator. Contributions of any of these as separate lemmas are welcome.
Scheduling independent jobs on machines that run at different speeds, so that the last job finishes as early as possible, is one of the basic problems of scheduling theory. In the classification of Graham, Lawler, Lenstra and Rinnooy Kan it is denoted , the minimum makespan problem on uniform parallel machines. It is strongly NP-hard, so the question is how close to the optimum a polynomial-time algorithm can get.
For identical machines, Graham's list scheduling (1966) is within a factor , and Hochbaum and Shmoys (J. ACM, 1987) gave a polynomial approximation scheme. For machines with speeds, the best guarantee published before 1988 was a relative error of 40 percent (Friesen and Langston). Hochbaum and Shmoys (SIAM J. Comput. 17(3), 1988) closed the gap with a polynomial approximation scheme: for every , a polynomial-time algorithm whose schedule has makespan at most times the optimum. Since the problem is strongly NP-hard, no fully polynomial scheme exists unless P = NP, so this is the best guarantee of its kind.
There are machines with speeds and jobs with processing times ; job takes time units on machine . A schedule is a map from jobs to machines (no preemption), its makespan is
and is the least makespan over all schedules.
A schedule has makespan at most exactly when it packs pieces of sizes into bins of sizes . A packing is truly feasible if every bin holds total size at most its own size, and -relaxed feasible if every bin holds at most times its size. An -relaxed decision procedure returns, on every instance with positive sizes, either an -relaxed feasible packing or the answer "none", and answers "none" only when no truly feasible packing exists.
The binary search of §2 starts from , and the schedule with all jobs on a fastest machine. At each iteration it runs a decision procedure on the deadline- instance, , and sets (keeping the packing returned as the current schedule) or . It runs for iterations and outputs the current schedule.
The decision procedure of §3 is all-pack, run with a parameter , an integer. It sorts the bins by non-increasing size and normalizes sizes so that the largest bin is . Sizes are grouped into geometric intervals , and a piece in interval is rounded down to . The procedure builds a multilayered graph whose nodes are state vectors: the counts of remaining pieces of the current bin interval and the next, by rounded size, and three slack counters in units , capped at . Configuration arcs pack one bin and update arcs pass from one bin interval to the next. all-pack answers with a packing traced from a path from "initial" to "success", or "none" if no packing can be traced. Its choices (ties, the path, which pieces fill a configuration, where small pieces go) are arbitrary.
For every there are and , depending only on , such that for every instance (, , ):
Here is the output of the binary search driven by . The goal fixes no exponent: it asserts the shape of the result (approximation ratio , polynomial size for fixed ), not the constants of Theorem 2.
The rounding bound ; Lemma 1 (node count ); Lemma 2 (out-degree ); Corollary 2 (arc count ); Lemma 3 (a truly feasible packing gives an initial–success path); the proof of Lemma 4 (every packing traced from a path is -relaxed feasible) and Lemma 4 as printed; the sentence of p. 549 that all-pack is a -relaxed decision procedure; and Theorem 1 (binary search with an -relaxed procedure is an -approximation).
The scheme settles the approximability of up to the exponent's dependence on . Its framework, the dual approximation approach, reduces approximate optimization to a relaxed decision problem: a procedure that may overfill bins slightly but never wrongly declares infeasibility. That framework reappears in Lenstra–Shmoys–Tardos for unrelated machines and in later schemes for bin packing and scheduling. The rounding-and-layered-graph technique of §3 is a template for dynamic programs over rounded item classes.
The result is proved on paper; no formalization of it is known. The platform has the Lenstra–Shmoys–Tardos scheme for a fixed number of unrelated machines, list scheduling, and Graham's LPT bound for identical machines. It has nothing for machines with speeds. A formalization would provide a checked binary-search/relaxed-decision framework over real deadlines, and a verified account of the state-vector bookkeeping of all-pack. Two printed claims need repair (below), so a formal proof also settles exactly which statements hold.
The definitions are elementary, but the bookkeeping is not. The slack counters of a state vector are kept in three different units, and the update arc re-expresses them for the next interval that contains bins. That interval may be one, two, or many intervals away, and each case consumes a different slack pool. Lemma 3 is an induction over stages: a truly feasible packing has to be read as a path whose capped counters still dominate the true slack. The proof writes "the reader can verify with little difficulty" and "the remaining cases … follow by similar calculations". Lemma 4 runs the other way, and the bound per bin depends on the granularity of rounded sizes and of usable slack.
Several printed details do not survive a literal reading. The rounding produces values per interval, while the state vectors of p. 544 have entries (finding F4). The packing rule of Lemma 4 places only the pieces of the current interval, although update also consumes pieces of later intervals (F5). Theorem 1 is false for (F1). The exponent of Theorem 2 is not what its derivation gives (F2).
Jobs and machines are indexed by Fin n and Fin m; schedules and packings are maps Fin n → Fin m, empty bins allowed. The makespan is a finite supremum over machines, and optimality is stated by comparison with every schedule . The deadline- instance has bins (not sizes rescaled by ). The paper's "log" is base 2, rounded up, and when negative. The binary search outputs the schedule kept with the final upper bound. A relaxed decision procedure is constrained on instances with positive sizes.
The paper's is split in two: is the target accuracy and the parameter of all-pack. This builds in the standing assumption that is a positive integer, and is . The §3 lemmas assume, as hypotheses, sorted bins normalized to and pieces in ; all-pack sorts and normalizes itself, so Theorem 1, the p. 549 statement and the goal carry no sortedness hypothesis. State vectors are indexed by the rounding classes. The slack counters take values , the top value standing for every multiple above (saturating addition). The first layer holds only the initial node, and success arcs leave the last stage when update with succeeds, which is the variant p. 546 calls simpler. The enormous bins are those of intervals (the printed "" on p. 548 is a typo). all-pack is a relation: it may output any packing traced from an initial–success path, and answers "none" exactly when no packing can be traced. Every is an explicit placed before the parameter and the instance, with in place of .
The goal is not "some schedule is -optimal", which an optimal schedule satisfies trivially. Its algorithm is the binary search driven by every resolution of all-pack, never an arbitrary relaxed decision procedure. Its constants are fixed before the instance, and the counter cap and the classes are part of the definitions, so the graph is finite and Lemma 3 is not false.
Beyond the paper. One variant item is posed: theorem_1_corrected (kind corrected, finding F1) adds to Theorem 1 and changes nothing else. For , eight identical machines and 128 jobs of size , a valid -relaxed procedure can drive the binary search to makespan , while for the bound holds. Theorem 1 itself stays as printed; a disproof of it is a legitimate result.
Contributions welcome: proofs of the milestones, in particular Lemma 3 (the stage induction) and the tracing argument of Lemma 4, and reusable lemmas about the binary search over real deadlines. The definitions of packings, relaxed decision procedures and the binary search can be reused by later missions on dual approximation.
Submodular function minimization asks for a subset of a finite set that minimizes a set function satisfying . Cut functions, matroid rank functions and entropy are submodular, and minimizing them is a subroutine in dynamic flows, facility location and source coding. Grötschel, Lovász and Schrijver showed in 1981–1988 that the problem is solvable in (strongly) polynomial time by the ellipsoid method, which is neither combinatorial nor practical. Whether a combinatorial strongly polynomial algorithm exists remained open until 1999, when two were found independently: one by Schrijver (J. Combin. Theory B 80, 2000) and one by Iwata, Fleischer and Fujishige (arXiv:math/0004089; J. ACM 48(4), 2001). This mission formalizes the second.
Let be a finite nonempty set with , and submodular with . For write and . The base polyhedron is . A linear ordering of generates the extreme base (the greedy algorithm). The exchange capacity is the largest with .
The scaling algorithm (§3) keeps , a convex combination of extreme bases generated by orderings , a skew-symmetric flow with , and with . A -scaling phase halves , clips , and then alternates pushes (exchange operations on a pair that is active: is not reachable from in the residual graph , but its successor in is) with augmentations of units along residual paths from to , each followed by a reduction of the convex combination to affinely independent .
The procedure Fix (§4) runs scaling phases from and an extreme base and returns an element with . The algorithm of Figure 3 keeps a digraph of compatible pairs ( for every minimizer ), lets be the set reachable from in and , computes , and in each iteration calls Fix on or from an extreme base generated by an ordering consistent with . It then adds an arc, contracts a cycle, or deletes and adds it to the output.
There is an absolute such that for every and every submodular with :
Lemma 2.1 (exchange capacity of an adjacent swap); Lemmas 3.1, 3.2, 3.3 (tightness of , relaxed weak and strong duality); the bound on augmentations per phase (§3.3); Lemma 4.1 (proximity); the Fix paragraph (§4, p. 12); the consistent-base bound and the case (p. 13); the two cases of an iteration (p. 13); and at most calls of Fix (proof of Theorem 4.2).
The result. The theorem gives a minimizer of any real submodular function using a number of operations bounded by a polynomial in alone, independent of the function's values, by combinatorial means (augmenting paths and exchanges, no ellipsoid). Its two ideas, scaling on a complete auxiliary graph and proximity-based fixing of elements, recur in later SFM algorithms such as Orlin 2009.
Formalizing it. The result is proved on paper and has no machine-checked proof. A formal proof would certify the correctness, termination and step bound of a concrete combinatorial algorithm over the reals, including the scaling-phase invariants, which the printed text gets slightly wrong in two places (see Beyond the paper). Schrijver's algorithm has a separate mission; the two share only the base-polyhedron layer.
The bound is a product of four counts (Fix calls, phases per call, augmentations per phase, pushes per augmentation), and each needs its own invariant. The phase count needs Lemma 4.1, whose proof relies on Edmonds' vector-reduction theorem (a base with ), which is not in Mathlib. The augmentation count chains Lemma 3.3 at , the rounding loss when clipping, and Lemma 3.2. The push count needs a potential that survives the growth of between augmentations; the printed argument does not hold as written. The bound on Fix calls needs a monotone potential across contractions and deletions, which change the ground set and the function. Correctness needs, as invariants of every reachable state, that arcs are compatible, the deleted sets lie in every minimizer, the cap is harmless, and the digraph stays acyclic so consistent orderings exist.
V : Finset α of an ambient type, with read on subsets of and vectors α → ℝ vanishing off in . The algorithm of Figure 3 runs on Fin n. Its current vertices are disjoint blocks of original elements, the current function is of the union, contraction merges blocks, and deletion replaces by .ec is the supremum form of (2.1).fix_finds_element_corrected replaces the Fix paragraph's phases by : the printed count gives only , and for , , , no element satisfies after one phase. [Sharpness probe] lemma_3_3_probe is Lemma 3.3 under the end condition printed in Figure 1 (, or ). It is false for the modular with values on two points with , where , and .Finset; Edmonds' vector reduction; Carathéodory's theorem (in Mathlib). The phase invariants and base-polyhedron lemmas are reusable for other SFM missions. Proofs of single milestones are welcome.Phase-type (PH) distributions are the distributions of absorption times of finite Markov chains. Introduced by Neuts in the 1970s (the book follows his framework, Latouche–Ramaswami, §2.3), they are the standard way to put non-exponential service times, interarrival times and lifetimes into a model while keeping it Markovian: a PH random variable is a walk through finitely many exponential (or geometric) "phases", so a queue or reliability model with PH ingredients is again a Markov chain, now on a state space of levels times phases. Every quasi-birth-and-death process in the matrix analytic literature has PH or Markovian-arrival inputs, and the matrices , and studied here reappear in every later chapter of Latouche and Ramaswami's book (SIAM 1999).
This mission formalizes Chapter 2 of that book: the definition of continuous and discrete PH distributions, the formulas for their distribution functions, the criterion for absorption in finite time, and the closure of the discrete family under sums, mixtures and minima.
Fix a finite set of phases and adjoin an absorbing state . A PH representation is a pair of a row vector and a square matrix indexed by the phases, with
where is the all-ones column vector. The Markov process on with initial distribution and generator
has transition function , . The time until absorption into has the PH distribution , with distribution function . Absorption with probability 1 from phase means as ; the distribution is nondefective if . The expected total time in phase starting from phase is .
The discrete analogue uses a substochastic with , the transition matrix , and the absorption time with .
For every PH representation ,
and if is nonsingular then every expected sojourn time is finite and
The result itself. Theorem 2.4.3 converts a probabilistic property of the absorbing process (absorption in finite time from every phase) into an algebraic one (nonsingularity of ), and gives the matrix its meaning as the matrix of expected sojourn times. Every formula after it in the book assumes it: the Laplace–Stieltjes transform , the moments , the mean drift of PH renewal processes in Chapter 3, and the rate and first-passage matrices of the QBD chapters, which are built from PH-structured blocks. The closure theorems are the reason PH distributions are a modelling class at all: sums, mixtures and minima of PH variables stay inside the class, and finitely supported distributions are in it, so it is dense in the distributions on .
Formalizing it. All results are classical and proved in the book; none is formalized. Mathlib has the matrix exponential, Kronecker and block matrices, but no phase-type distributions, no generator-to-transition-function interface for absorbing chains, and no expected sojourn times. This mission builds that layer and states the chapter's results on it. It is the substrate for the remaining fourteen missions of the series.
The equivalence in Theorem 2.4.3 connects an asymptotic property of with the determinant of its transient block. Neither direction is a finite computation: the forward direction must extract finiteness of all sojourn times from the hypothesis that absorption happens almost surely and then identify the sojourn-time matrix as an inverse of ; the reverse direction must show that a nonsingular with the sign pattern (2.4) forces and the integrability of on , a statement about all that no finite expansion of the exponential series settles. A purely algebraic shortcut through eigenvalues (" is stable") needs the spectral facts about semistable matrices that the book only sketches in Remark 2.4.5. Theorem 2.4.1 already requires the block form of for the lower block-triangular , and the closure theorems require tracking powers of block and Kronecker-structured transition matrices.
Phases form an arbitrary finite type ι; the absorbing state is none in Option ι. Vectors are functions ι → ℝ, row vectors act on the left. On a finite state space the law of the continuous-time process is its transition function, defined as Mathlib's NormedSpace.exp (x • Q); the discrete chain's -step probabilities are the matrix power . The distribution functions and are defined from these transition probabilities, not by the closed formulas of Theorems 2.4.1 and 2.5.3, so those theorems carry content. Absorption with probability 1 is the limit ; the expected sojourn time is a lower Lebesgue integral in , so an infinite expected time is never replaced by a junk real , and the goal asserts finiteness explicitly. Nonsingularity is IsUnit T.det; it is a hypothesis only where the book assumes it (the "moreover" part of Theorem 2.4.3 and Eq. (2.11)) and a conclusion in the equivalence. The closure theorems are stated through the laws: a convolution of probability mass functions for independent sums, a product of survival functions for independent minima, a convex combination of distribution functions for mixtures; each also asserts that the constructed pair is a valid discrete PH representation. The trivializing formalization, defining by or defining absorption by nonsingularity of , is ruled out by these definitions.
Beyond the paper. No variant items are posed. Theorem 2.6.3 (the PH representation of ) is not in this mission; a planning finding records that its printed representation fails when has an atom at .
Needed infrastructure: the block structure of and of ; nonnegativity and row sums of for a generator; limits and integrals of matrix exponentials; block-matrix and Kronecker power identities. Most of it is reusable for the PH renewal processes and QBDs of the later missions. Contributions of general lemmas about matrix exponentials of Metzler matrices are welcome.
Many transportation and evacuation questions ask how much can be shipped from a source to a sink within a time horizon, when every arc has both a capacity per period and a traversal time. Ford and Fulkerson posed this maximal dynamic flow problem in 1958 and solved it by a reduction that is now standard in network optimization: instead of solving a linear program on a network copied once per period, solve one minimal cost flow problem on the original network and repeat its chain flows over time. Their account in Chapter III, §9 of Flows in Networks (RAND Report R-375-PR, 1962; Princeton University Press, 1962) is the source of the notions of the time-expanded network and the temporally repeated flow, which underlie later work on earliest arrival flows, quickest flows and evacuation planning (see Skutella, 2009).
Timeline. Ford and Fulkerson, Constructing maximal dynamic flows from static flows (Operations Research 6, 1958), proved that a temporally repeated flow is optimal. Gale (1959) showed that a single dynamic flow can be maximal for every horizon simultaneously, a question the book raises right after the theorem formalized here. Hoppe and Tardos (2000) solved the quickest transshipment problem with several sources and sinks.
A network has a finite node set , two distinct nodes (source) and (sink), and a set of ordered pairs of distinct nodes (arcs); both and may be arcs. Each arc carries a positive integer capacity and a nonnegative integer cost ; in the dynamic problem is the traversal time, a positive integer.
A static flow from to of value is a real function on the arcs with , net outflow at , at , and at every other node. For an integer , the -th related program maximizes over static flows. Integer node numbers and a flow satisfy the optimality properties (3.18)–(3.20) for this program when , , whenever , and whenever . The arc numbers are .
A dynamic flow for periods assigns to each arc and departure time an amount with , arriving at at time , together with nonnegative hold-overs that wait at from to , with unbounded capacity. Conservation holds at every intermediate node at every time, and the value is the net amount leaving , equal to the net amount entering , over the horizon: these are the constraints (9.2)–(9.5). Equivalently, it is a static flow in the time-expanded network , whose nodes are the copies , , with arcs of capacity and hold-over arcs of infinite capacity. A dynamic cut is a node set of containing every and no ; its capacity is the total capacity of the arcs of leading from to its complement.
A chain decomposition of a static flow of value is a finite family of chains from to with amounts , using at most on each arc in total and of total value at least . The temporally repeated flow it generates sends along starting at every time with , where is the traversal time of .
Let the traversal times be positive integers, let be an integral static flow of value and integer node numbers satisfying the optimality properties for the -th related program. Then has a chain decomposition; every chain decomposition of generates a temporally repeated flow that is a maximal dynamic flow for periods, with value
and the cut of determined by is a minimal dynamic cut. In the book and are the outputs , of the minimal cost flow routine of §3, which satisfy these properties by Theorem 3.1.
A variant item states the goal for every real static flow maximizing , with no integrality and no node numbers assumed (finding F1).
The theorem turns a linear program whose size grows with the horizon into a minimal cost flow problem of fixed size, and it identifies the optimal value as an explicit function of a static flow. Equation (9.20) then shows that is a convex piecewise linear function of , with slopes the values of the successive static flows.
The result is proved, in 1958 and in the book. It has, as far as a search of the platform shows, no machine-checked proof: no item states a dynamic flow, a time-expanded network or a temporally repeated flow. A complete development would produce reusable formal notions of time-expanded networks and of chain decompositions of node-arc flows, and a formal proof of LP-duality-style optimality for the s–t minimal cost flow program.
Constructing the temporally repeated flow and checking that it is feasible is the easy half. The hard half is maximality over all dynamic flows, including those that use hold-overs and are generated by no static flow: an upper bound on every dynamic flow for periods has to be matched exactly to a quantity computed on the original, much smaller network. A newcomer who tries to compare dynamic flows with temporally repeated ones directly finds no such comparison: the maximal dynamic flow of the book's Fig. 9.7 is not temporally repeated.
Two pitfalls are on the page. The printed definition (9.17) of the minimal cut has an upper limit under which the set is empty (finding F2); the statement uses the node set (9.18) that the text describes. And the clause " for some arc" of Theorem 3.5 depends on how the routine produced its flow and fails for an arbitrary pair satisfying the optimality properties (finding F3); the statement carries what Theorem 3.1 says of the routine's , that it is also optimal for the -th program.
Nodes form a Fintype with decidable equality; arcs a Finset (N × N) without loops; capacities and costs are natural numbers, with capacities positive on arcs and, in the §9 statements, traversal times positive. Static flows are real functions on the arcs in Chapter I's net form, which agrees with the §3 form (3.7)–(3.10) when no arc enters or leaves . Node numbers are integer valued. The routine of §3 is not formalized: every statement quantifies over flows and node numbers satisfying the optimality properties, which is what Theorem 3.1 asserts of the routine's outputs. Dynamic flows are the linear program (9.2)–(9.5) itself, with times in , hold-overs as separate nonnegative variables (infinite capacity is never written as a number), and incoming terms present only when the departure time is nonnegative. A minimal dynamic cut is a dynamic cut that no hold-over arc crosses and whose capacity is at most that of every other such cut; cuts crossed by a hold-over arc have infinite capacity. Maxima are stated as attained.
The trivializing formalizations are ruled out: the maximal dynamic flow value is not defined through (9.6) but as the greatest value of the program (9.2)–(9.5), and "temporally repeated" is an explicit construction from a chain decomposition, so not every dynamic flow is one.
Needed: finite sums over arcs and times, list-based chains, and duality for both the static and the time-expanded network; Mathlib has no network flow theory, and these definitions are reusable beyond this mission. Proofs of the milestones, of the goal and of the strengthened variant are all welcome.
In a communication or transportation network, a planner often needs not one maximal flow value but all of them: the largest amount that can be sent between every pair of locations. For an undirected network with nodes there are such values. In 1961, R. E. Gomory and T. C. Hu (Multi-terminal network flows, J. SIAM 9 (1961)) answered two questions about them. Which tables of numbers can occur as the all-pairs maximal flow values of some network? And how many maximal flow computations are needed to find them all? Mayeda (1960) and Chien (1960) studied the same questions at about the same time.
Ford and Fulkerson's Flows in Networks (RAND Report R-375-PR, 1962; Princeton University Press, 1962) gives the theory in its fourth chapter, "Multi-Terminal Maximal Flows", following Gomory and Hu. This mission formalizes the first half of that chapter: the cycle criterion for maximal spanning subtrees (§1), the characterization of flow functions and their realization by trees (§2), and the condensation lemma behind the Gomory–Hu procedure (§3).
An undirected network has a finite set of nodes and a set of undirected arcs. An arc joins two distinct nodes, and at most one arc joins any two nodes. Each arc carries a nonnegative real capacity .
A flow of value from to assigns to each ordered pair a number , the flow from to . It vanishes unless is an arc. On each arc it satisfies , and , so flow moves in only one direction. The net flow out of a node, , is at , at , and at every other node. The maximal flow value from to is the largest value of a flow from to . The book calls the function giving this value for every pair of distinct nodes the flow function of . It is symmetric, and is left undefined.
A symmetric function on pairs of distinct nodes is realizable if some undirected network on has flow function . It is realizable by a tree if the arcs of such a network form a tree on , that is, a connected graph without cycles.
For a set of nodes with complement , the cut capacity is the total capacity of the arcs joining to . is a minimal cut separating and if , , and no other such node set has a smaller cut capacity. The condensed network shrinks all of to a single node. Arcs between nodes of (the ordinary nodes) are kept. The arcs from an ordinary node to become one arc whose capacity is their sum.
Given a connected graph with real arc lengths , a spanning subtree is a tree obtained from by deleting arcs. Arcs of are in-tree and the rest are out-of-tree. is maximal if no spanning subtree of has a larger total length.
For a nonempty finite node set and a symmetric on pairs of distinct nodes, is realizable if and only if, for all pairwise distinct ,
Moreover, if is realizable, it is realizable by a tree.
Theorem 2.1 says that the all-pairs maximal flow values of an undirected network take a very restricted form. Every network is flow-equivalent to a tree on the same nodes. At most distinct values occur. Every value is a minimum of values along a path. The Gomory–Hu tree, with its maximal flow computations instead of , rests on this structure, and Lemma 3.1 is what makes that procedure correct: each later flow problem can be solved on a smaller, condensed network without changing the answer. Gomory–Hu trees are used in network reliability, in the separation of odd-cut inequalities for matching polytopes (Padberg and Rao, 1982), and in graph clustering. Theorem 1.1 is the cycle-optimality criterion for maximum-weight spanning trees. It underlies the correctness of Kruskal's algorithm, which the book derives from it.
These are classical results, proved in the 1950s and 1960s. On Prove2Me, Padberg and Rao's odd-cut results take an odd cut-tree as a hypothesis and do not construct one. Minimum-spanning-tree exchange properties exist in other encodings (rooted parent functions, a list-scan Kruskal). No formal statement of the realizability theorem, of the triangle condition on flow functions, or of the condensation lemma is known on the platform. The work is to formalize the known proofs. They connect undirected maximal flows with the max-flow min-cut theorem, spanning-tree exchange arguments and cut submodularity, and every one of these is reusable on its own.
The obvious first step for Lemma 2.1 compares flows directly, and it does not work. The inequality is a statement about maxima, and a flow of value from to cannot be assembled by concatenating an – flow and a – flow, because the two flows compete for the same arc capacities. Every statement here is about attained maxima of flow values, and nothing in the mission's statements supplies the max-flow min-cut theorem for undirected networks with the one-direction constraint . A solver must bring that in. For Lemma 3.1, the two networks have different node types, so flows have to be transported between them in both directions, and the naive way of pushing a flow forward into the condensed network can lose value. For Theorem 1.1, necessity is a single exchange, but sufficiency is not: the book itself remarks that it is "not obvious".
Nodes are a Fintype with decidable equality. Arcs are a Mathlib SimpleGraph, so they are undirected and loop-free with at most one arc per pair. Capacities are a symmetric real function, nonnegative on arcs. Flows are real functions on ordered pairs that satisfy the book's constraints (10.1) of Chapter I. The maximal flow value is an attained maximum (IsGreatest), never a bare supremum. A flow function is constrained only off the diagonal, matching the book's " undefined", so (2.1) is quantified over pairwise distinct nodes. The book's alternative convention is not used. Extending by on the diagonal would break (2.1) at . The goal and Lemma 2.2 assume off the diagonal. The book leaves this implicit (flow values are nonnegative), and without it the "if" direction fails for . The goal assumes nonempty, because a tree is connected. "Realizable by a tree" means the network's graph is a tree on all of . Some tree arcs may have capacity . The condensed network has node type Option X, where none is the condensed node. Spanning subtrees are subgraphs with T.IsTree. Lengths are a function on unordered pairs, and "the chain of in-tree arcs" is any path in , which is unique.
A trivializing formalization is excluded. The flow function is defined by actual flows, never by path minima in a tree or by cut capacities. Realizability is the existence of a network whose flows have those maximal values, never a restatement of (2.1).
Not included: Lemma 3.2 and Theorem 4.1. Both concern objects that the book defines by a construction ("the final tree " of the Gomory–Hu procedure, and the network of §4), and stating them faithfully would require formalizing those constructions. Contributions welcome: an undirected max-flow min-cut theorem in this encoding, the tree-network flow computation, and a formal Gomory–Hu construction for a later mission.
An matrix of 's and 's is the incidence matrix of sets against elements, or the adjacency matrix of a bipartite graph, or, when , the adjacency matrix of a directed graph on nodes. The first question about such matrices is when one exists with prescribed row and column sums. Gale (1957) and Ryser (1957) answered it independently with a partial-sum criterion against the conjugate sequence. Ore (1956) solved the companion problem for directed graphs: when does a given directed graph have a subgraph with prescribed in- and out-degrees? Fulkerson (1960) treated the square case in which 's are forbidden on the main diagonal, which is the degree problem for directed graphs without loops.
Ford and Fulkerson's Flows in Networks derives all of these from the supply-demand theorem for network flows. Chapter II, §11 states a two-sided version of Ore's theorem (Theorem 11.1, Corollary 11.2). §12 states the Gale–Ryser theorem in inequality form (Theorem 12.1, Corollaries 12.2–12.3) and Fulkerson's zero-trace theorem (Theorem 12.4, Corollaries 12.5–12.6). This mission formalizes those statements, citing the RAND typescript (Report R-375-PR, 1962), Chapter II, pp. 70–92.
A directed graph has a finite node set and a set of ordered pairs with , at most one per ordered pair. A subgraph keeps the nodes and takes an arc set . Its local degree at is the pair , : the numbers of arcs of entering and leaving . For , is the set of heads of arcs leaving and the set of tails of arcs entering ; and count the arcs from to and from to ; .
A -matrix has every entry or . For nonnegative integers the conjugate sequence is . For nonnegative integers , the diagonally restricted conjugate sequence is defined as follows. In an array, row places dots in its leftmost columns other than column , and is the number of dots in column :
For this gives , which is not monotone.
In Lean these are Digraph, IsSubgraph, outDeg, inDeg, succSet, predSet, numArcsTo, numArcsFrom (file Def_FlowsNetworks_Matrices_Digraph) and IsZeroOne, conj, diagDot, diagConj (file Def_FlowsNetworks_Matrices_ZeroOne), all in the namespace FlowsNetworks.Matrices.
For nonnegative integers and , there is an -matrix with
if and only if
The result itself. Theorem 12.4 characterizes the out-degree upper bounds and in-degree lower bounds that a loopless directed graph on labelled nodes can meet. With equal totals, it characterizes the degree sequences of such graphs (directed graphs with no loops and no parallel arcs). Theorem 12.1 is the inequality form of the Gale–Ryser theorem, which underlies the theory of the class of -matrices with given margins: Ryser's structure matrix, interchanges, and term rank. Ore's theorem is its counterpart for an arbitrary host graph. Corollaries 12.2–12.3 and 12.5–12.6 are the closed forms used in scheduling and seating problems, such as families at tables with no two relatives at one table.
Formalizing it. All results are classical and proved. On the platform, the Gale–Ryser theorem exists only as AppliedComb.ManyFaces.gale_ryser (Keller–Trotter, Theorem 16.12). That statement requires equal sums and exact margins, sorts both sequences, and requires positive parts. The book's version has one-sided bounds, arbitrary totals, an unsorted and zero entries, so it is drafted here, not referenced. No zero-trace theorem, diagonally restricted conjugate, or directed-subgraph degree theorem was found on the platform.
Each criterion is a family of inequalities, and the content is that these few inequalities suffice. A direct argument has to show that a deficiency in some arbitrary set of columns, or of nodes, is already seen by an initial segment of the sorted sequence. The diagonal restriction breaks the usual monotonicity: need not be monotone (the example above has ), so the standard exchange argument for conjugate sequences does not apply unchanged. The ordering hypotheses are essential. Without both Theorem 12.1 and Theorem 12.4 are false (findings F1, F2: , for 12.1; , for 12.4). The existence side needs an integral object (a matrix or a subgraph), not a fractional one.
Matrices are Matrix (Fin m) (Fin n) ℕ with entries at most . Every integer datum is a natural number, so nonnegativity is built in. Indices are -based: the book's index is i + 1, and is the sum over i.val < k. Orderings are Antitone. Zero trace is written , as printed. Directed graphs have a finite node type with decidable equality, arcs form a Finset (N × N) with no loops, and a subgraph is an arc set . Corollaries 12.3, 12.5 and 12.6 carry the ordering hypotheses of the theorem they specialize. In Corollary 11.2 the page prints in (11.19), which is read as because the corollary prescribes exact degrees. Its summation range, printed , is read as , as in (11.14).
The trivializing formalization is ruled out: and are explicit counts computed from the integers , never defined through the existence of a matrix, and every partial-sum criterion is required for every , not only for .
Beyond the paper. Two sharpness probes accompany the faithful statements. Each is expected to be false, and a disproof is the sought outcome. zero_one_matrix_existence_probe is Theorem 12.1 without (F1: , , satisfies the criterion but admits no matrix). zero_trace_theorem_probe is Theorem 12.4 without (F2: , , likewise).
A complete development needs integral network-flow feasibility (the supply-demand theorem with integrality, or a direct combinatorial substitute), the bijection between integral flows on a bipartite network and -matrices or subgraphs, and conjugate-sequence identities such as . These pieces are reusable for the rest of Chapter II. Direct combinatorial proofs that avoid flows are equally welcome.
The value of a maximal flow is the basic output of network-flow models of transport, communication and supply systems. A planner who can enlarge the capacity of a link wants to know what the enlargement buys. For a single link the answer is simple. For two links it is a question about interaction: does enlarging one make enlarging the other more valuable (the links reinforce each other) or less valuable (they interfere)? L. S. Shapley answered it, and Ford and Fulkerson give his theorems and proofs in Section 13 of Chapter I of Flows in Networks. Any two arcs either always reinforce or always interfere, and in several positions the network's geometry alone decides which. These are early instances of supermodularity and submodularity of an optimal value in its parameters, a theme that later became central in parametric optimization and discrete convex analysis.
A network is a finite set of nodes together with a set of ordered pairs of distinct nodes, the arcs. The arc has initial node and terminal node . There is at most one arc from to , but and may both be arcs. The nodes are split into a set of sources, a disjoint set of sinks, and the remaining intermediate nodes . Each arc carries a capacity .
A flow from to is a function on the arcs with on every arc, and with conservation at every intermediate node . Here is the total flow on arcs leaving and the total on arcs entering it. Its value is the net amount leaving the sources, . The maximal flow value is the largest value of a flow. A node set containing every source and no sink determines the cut , the set of arcs from to its complement, with capacity , the sum of their capacities.
Fix two distinct arcs and and keep every other capacity fixed and finite. Write for the maximal flow value when is replaced by , and for the value when and are replaced by and . These two capacities may also be , and then may be . For a rectangle with corners , , , in the nonnegative quadrant, with , the difference quotient is
The interaction constant is
which may be , or indeterminate ().
The goal leaves the sign open. Which sign occurs depends on the whole network: in the book's Fig. 13.3, removing a third arc turns into .
Corollary 13.2 refines the goal by naming the sign. Theorem 13.3 and Corollary 13.4 fix the sign from positions alone.
Theorem 13.1 says that the cross effect of two capacities on the maximal flow value never changes sign. The marginal value of capacity on one arc is monotone in the capacity of the other, in a direction fixed once and for all by the network. Corollary 13.2 reduces that direction to a single number computed from four maximal-flow values at the corners and . Theorem 13.3 and Corollary 13.4 show that some directions are forced by position: arcs in series reinforce, and arcs that compete at a common node interfere. These facts underlie sensitivity analysis of maximal flows. They are also the two-parameter case of the lattice and submodularity structure of minimal cuts.
The theorems were proved by Shapley and printed with proofs by Ford and Fulkerson (RAND, 1962). Their proofs argue from a picture of how the regions of linearity of can sit in the quadrant (Fig. 13.2). No machine-checked proof of any statement of Section 13 exists on Prove2Me. Proved max-flow min-cut statements exist there for a single source and sink and in other conventions, and are related to milestone 1 rather than identical to it. Formalizing the section gives a checked account of the parametric behaviour of the maximal flow value. That includes the infinite capacities the section allows, and the indeterminate case of , which a picture handles only informally.
The first idea is to read the sign off formula (13.4): is the minimum of four affine functions, so its mixed second difference is determined by which pieces are active at the four corners of a rectangle. A minimum of four arbitrary affine functions, however, can have mixed differences of both signs. The claim depends on constraints that the four corner values satisfy because they come from one network, and on how the regions of linearity can meet. The book's proof uses a case analysis of these configurations: at most one diagonal boundary segment, and its slope fixed by . Making that analysis rigorous, including the degenerate configurations where regions are empty or corner values are infinite, is the core of the goal and of Corollary 13.2.
Milestone 1 also has to be established in the several-source form, with arcs allowed to enter sources and to leave sinks, where the reduction to a single source and sink must respect flows whose sources have net inflow.
Nodes form a finite type with decidable equality; arcs are a finite set of ordered pairs without loops; sources and sinks are disjoint finite sets, either of which may be empty (then and every statement holds trivially, as in the book). Capacities of the fixed arcs are finite nonnegative reals. The two varied capacities and every maximal flow value lie in (ℝ≥0∞). A flow is a real function vanishing off the arcs, and the maximal flow value is the supremum of flow values in . That supremum is taken over a nonempty set (the zero flow), so it is never a default value, and it is exactly when flow values are unbounded. The maximal flow value is not defined as a minimum cut capacity; equality with the minimum cut is milestone 1.
The difference quotient is taken at finite real arguments over every rectangle with and ; and may be negative. The book prints the third term of (13.12) as . The rectangle the theorem names needs , which is the formalized quotient; with the printed term the claim already fails for two arcs in series. The constant is a four-way value (indeterminate, , , real), so is never silently assigned a number.
"Of one sign" is formalized as one sign for all rectangles at once. The rectangle-by-rectangle reading, under which every real number is trivially or , is ruled out.
A complete development needs flows with several sources and sinks, cuts, and the max-flow min-cut theorem in that form; the definitions here are self-contained and reusable for any parametric max-flow statement. Contributions of the general piecewise-linear structure of in one or two capacities are welcome.
The maximal flow problem asks how much of a commodity can be sent from one node of a network to another when every arc has a capacity. It was posed in the 1950s in the study of rail networks, and its answer, the max flow min cut theorem of L. R. Ford, Jr. and D. R. Fulkerson, became the organizing result of combinatorial optimization: the bottleneck of a network, a cheapest set of arcs separating the two terminals, has exactly the capacity of the best flow. Chapter I of Ford and Fulkerson's Flows in Networks is the canonical exposition. This mission formalizes Chapter I, §§1–9, in the RAND typescript of the book (Report R-375-PR, 1962), whose numbering is used throughout.
Timeline. Ford and Fulkerson proved the theorem in 1956 for undirected networks in an arc–chain formulation ("Maximal flow through a network", Canadian J. Math.); Elias, Feinstein and Shannon gave an independent proof the same year (IRE Trans. Inf. Theory). The book restates the theory for directed networks with node–arc flows, which is the form used in all later applications and the form formalized here.
A network is a finite set of nodes together with a set of ordered pairs of distinct nodes, the arcs. At most one arc leads from to , but both and may be arcs. Each arc has a capacity , a real number. For node sets , is the set of arcs from to , and is the sum of a function over those arcs; .
Fix two distinct nodes, the source and the sink . A flow of value from to is a function on the arcs with such that the net flow out of every node, , is at , at , and elsewhere. A flow is maximal if no flow has larger value. A node set with , determines the cut separating and , of capacity ; a minimal cut has least capacity.
A flow augmenting path with respect to is a sequence of distinct nodes from to in which each consecutive pair is joined either by a forward arc with or by a reverse arc with . The source set of a flow is the smallest node set containing and closed under such steps; the sink set is the smallest node set containing and closed under such steps taken backwards. With lower bounds , , the bounds are replaced by .
with both extrema attained. The goal fixes nothing beyond the book's hypotheses: any finite network, any nonnegative real capacities.
The result itself. The theorem converts an optimization over a continuum of flows into a finite minimum over node sets, and the integrity theorem makes the conversion combinatorial. The later chapters of the book derive from these two results the supply–demand and circulation theorems, the König–Egerváry theorem, Menger's theorem, Dilworth's theorem and Hall's theorem on distinct representatives. Corollary 5.2 is the correctness criterion of every augmenting-path algorithm, and Corollaries 5.3–5.4 and Theorems 5.5–5.6 describe the lattice of minimal cuts that later work on parametric flows and cut enumeration uses.
Formalizing it. The theorem is proved, and several machine-checked versions exist on this platform in other conventions: FordFulkerson56.MinCut.minimal_cut_theorem (the 1956 undirected arc–chain form), AppliedComb.Flows.max_flow_min_cut and AppliedComb.Flows.integral_max_flow (networks without 2-cycles and without arcs into the source or out of the sink), LinearOptimization.max_flow_min_cut (positive extended-real capacities, parallel arcs), VanderbeiLP.Networks.max_flow_min_cut (value measured on a return arc), and the augmenting-path criteria GoldbergTarjan.Generic.max_flow_iff_no_augmenting_path and EdmondsKarp.ShortestPath.isMaxFlow_iff_no_augPath. None states the book's node–arc theorem for directed networks in which antiparallel arcs, arcs into the source and zero capacities are all allowed. This mission states it in exactly the book's conventions, together with the minimal-cut structure theory of §5 and the lower-bound form of §9, which have no platform counterpart.
The inequality "max flow min cut" holds for every pair of a flow and a cut and is routine. The difficulty is the reverse inequality together with attainment: the theorem asserts that a maximal flow exists, and this is not free over the reals. The labeling method of §8 need not terminate when capacities are irrational: the book gives a network in §8 where it converges to a flow of value one quarter of the maximum. So an argument that only runs the algorithm covers rational or integral data and leaves the general statement open. Theorems 5.5 and 5.6 add reasoning about inductively defined node sets and about arc sets rather than node sets: two different node sets can determine the same cut, which is why Theorem 5.6 compares arc sets and needs .
Nodes are a Fintype with decidable equality; arcs a Finset (N × N) with no loops; capacities and flows functions , flows required to vanish off and to be nonnegative on it. Capacities are finite reals throughout. The source and sink are distinct (), the book's "two distinguished nodes". A cut is given by its node set ; where the book compares cuts (Theorem 5.6) the Lean compares the arc sets . Every maximum and minimum is stated as attained (IsGreatest, IsLeast) or through explicit "maximal flow" and "minimal cut" predicates; no sSup or sInf appears. The source and sink sets are defined as intersections of all node sets closed under the book's rules (a), (b) and (a′), (b′), not through a reachability algorithm.
The statement admits a trivializing formalization that is ruled out here: defining the maximal flow value as the minimal cut capacity, or minimal cuts through flow values, or replacing by ; flows, cuts, maximality and minimality are each defined from the network alone.
Beyond the paper. Two variant items accompany the faithful statements. A strengthening of Corollary 5.3: one flow, not assumed maximal, that saturates and is zero on already makes the cut minimal and the flow maximal, since by Lemma 4.1 its value equals the cut capacity. A sharpness probe for Theorem 5.6: the statement with weakened to , which the book's Fig. 5.2 shows to be false (two arcs, capacities 1 and 0, give two minimal cuts while the source-set and sink-set cuts coincide); a disproof is the sought outcome.
A complete development needs finite sums over arc sets and their splitting along (the identities (3.3)–(3.4)), compactness of the flow polytope or an augmenting-path argument, and an inductive closure argument for the source set. The network, flow and cut definitions are reusable by the rest of this series (circulations, dynamic flows, flow functions) and by any formalization of matching or connectivity theorems through flows. Proofs by either route, compactness or the labeling method with integrality, are welcome.
Many questions in operations research and combinatorics ask whether a system of linear inequalities on a network has a solution: can the demands at a set of warehouses be met from the supplies at a set of factories through roads of limited capacity; is there a nonnegative matrix with bounded entries whose row and column sums lie between given limits; can a periodic schedule be met when every activity has a minimum and a maximum rate. Chapter II of L. R. Ford, Jr. and D. R. Fulkerson's Flows in Networks (RAND Report R-375-PR, 1962; Princeton University Press, 1962, doi:10.1515/9781400875184) answers these questions by feasibility theorems: a system of flow constraints has a solution exactly when a family of inequalities, one for each set of nodes, holds.
The history in the chapter's first three sections is short. D. Gale proved the supply-demand theorem in 1957 (A theorem on flows in networks, Pacific J. Math. 7 (1957) 1073–1082). A. J. Hoffman proved the circulation theorem, with lower and upper bounds on every arc, in 1960 (Some recent applications of the theory of linear inequalities to extremal combinatorial analysis, Proc. Sympos. Appl. Math. 10, AMS, 1960), originally through the separation theorem for convex sets. Ford and Fulkerson derive all of these, and the two-sided variants, from the max flow min cut theorem of their Chapter I.
A network is a finite set of nodes together with a set of ordered pairs of distinct nodes, the arcs; there is at most one arc from to , but both and may be arcs. Each arc carries a real capacity . For a real function on the arcs and node sets ,
so is the total of on arcs leaving and the total on arcs entering . For a node set , ; for a node function , .
In §§1–2 the nodes are partitioned into sources , intermediate nodes and sinks (any of them may be empty). Sources carry a supply , sinks a demand . A function on the arcs is a feasible flow for the supply-demand problem when the net outflow is at most at every source, zero at every intermediate node, the net inflow is at least at every sink, and on every arc.
In §3 there are no distinguished nodes. A lower bound function with is given on the arcs, and a feasible circulation is a function on the arcs with
For a network with capacities and lower bounds , a feasible circulation exists if and only if
With this is the goal.
The circulation theorem is the most general of the chapter's feasibility criteria for directed networks: the supply-demand theorem, the existence of – flows between lower and upper arc bounds (Chapter I, §9), and the transportation-matrix criterion of Corollary 2.3 all follow from it or from its extension, Theorem 3.2, by adjoining arcs, and the rest of Chapter II applies them to systems of distinct representatives and (0, 1)-matrices.
All results of the mission have been proved for more than sixty years. None of them, in this form, is formalized on Prove2Me: the platform has decomposition results for circulations and max flow min cut statements in other conventions, but no Gale or Hoffman feasibility criterion. The mission produces machine-checked versions of the six numbered results and the goal over one shared notion of network, in the book's notation.
Necessity is the routine half of every theorem. Sufficiency asks for a flow built from a family of inequalities, one per node set, and constructing a flow arc by arc or node by node with local repairs gives no argument that the repairs stop or that all constraints hold at once. The statements also differ in ways that are easy to get wrong: §§1–2 bound the net outflow at sources but the net inflow at sinks, §3 bounds the net inflow everywhere, the node bounds of Theorem 3.2 carry no sign condition and may be negative, and Theorem 2.1 needs two inequalities per node set rather than one. Real-valued data rule out any argument by induction on integer flow values without a separate limiting step.
Nodes form a Fintype with decidable equality; arcs are a Finset (N × N) with no loops; capacities and flows are real functions . A flow is required to vanish off , and every sum runs over arcs only, so the values of and off never matter. Supplies, demands and node bounds are real functions on all of whose values enter only through sums over the sets the book names (, , …). The partition is three pairwise disjoint Finsets covering . ranges over all subsets of , including and . Each section's sign convention is copied: §§1–2 bound the net outflow at sources and the net inflow at sinks, §3 bounds the net inflow. Corollary 2.3 is stated for real matrices indexed by Fin m × Fin n. All data are finite reals; no integrality is assumed.
Feasibility is always stated as the existence of a function on the arcs satisfying the book's displayed constraints. Defining feasibility through the cut condition itself, or through a linear-programming solver predicate, would make every theorem definitional and is ruled out.
Beyond the paper. One variant is posed beside the faithful goal: [Strengthened] Theorem 3.1, the circulation theorem for any real lower bound without (capacities stay nonnegative). The substitution reduces it to a supply-demand problem with nonnegative capacities , whose Gale condition is regardless of the sign of ; it implies the faithful statement.
A complete development needs Chapter I's max flow min cut theorem in some form (or the linear-programming duality theorem, or Farkas' lemma), the manipulation of arc sums over node sets, and the auxiliary-network constructions. The definitions of networks, arc sums and partitions are reusable by the later Chapter II missions. Proofs of any milestone, of the variant, and alternative proofs through LP duality are welcome.
A convex program whose objective and feasible set are known only through oracles, routines that answer queries about one point at a time, can still be solved to any prescribed accuracy with a number of queries bounded in advance. The ellipsoid method is the classical algorithm that achieves this. It was introduced for convex minimization by Yudin and Nemirovski (Ekonomika i Matematicheskie Metody, 1976) and by Shor (Cybernetics, 1977), and it became widely known when Khachiyan used it to prove that linear programming is solvable in polynomial time (Soviet Math. Dokl., 1979). Grötschel, Lovász and Schrijver turned the method into a general tool of combinatorial optimization, the equivalence of separation and optimization (Springer, 1988).
Ben-Tal and Nemirovski's Lectures on Modern Convex Optimization (SIAM 2001) present the method in §5.2 as the engine of their theorem that convex programs are polynomially solvable, and prove an explicit, fully quantified complexity bound for it, Theorem 5.2.1. This mission is the tenth of a series formalizing the book's main results and covers §5.2 (pp. 342–352).
Vectors are elements of , , with the Euclidean norm . The problem is
where is convex and is a closed, bounded, convex set with nonempty interior. Two radii are known in advance (assumption A): lies in the ball and contains some ball , whose centre is not known.
The data are accessed through two oracles. A separation oracle for answers a query by "" when that holds, and otherwise returns a vector with for all . A first order oracle for returns and a subgradient of at : for all .
An ellipsoid is with . For , put and
The ellipsoid method with accuracy starts from , , . At step it queries the separation oracle at . If a separator is returned, the step is nonproductive, and . Otherwise the step is productive: the first order oracle is queried at ; a zero subgradient stops the method with result ; a nonzero one becomes , and . Then , (computed from ), , and the method stops if
returning the productive search point , , with the smallest value of . Finally .
For every accuracy , every separation oracle for and every first order oracle for , the ellipsoid method terminates after no more than
steps, and its result satisfies
Theorem 5.2.1 bounds the number of oracle calls by a quantity that depends only on the dimension, on and on : the cost of each additional digit of accuracy is steps, whatever the instance. Each step costs one call of each oracle and arithmetic operations. This is the ingredient the book's Theorem 5.3.1 combines with polynomial computability to conclude that convex programs are polynomially solvable, and it is the reason semidefinite and conic quadratic programs, the subject of the earlier lectures, are tractable in theory. The bound is also explicit enough to be checked numerically, with no hidden constants.
On the formal side, the platform has machine-checked versions of related results in other forms: Bertsimas and Tsitsiklis's half-ellipsoid lemma with the weaker ratio and polyhedral feasibility version, Bubeck's version for objectives bounded on with a convergence-rate conclusion, and Shor's localization theorem. None of these is the book's method: its guesses , its stopping rule (5.2.17), the explicit step count (5.2.18), or the exact volume identity (5.2.14). A formal proof of Theorem 5.2.1 gives a machine-checked oracle complexity bound with a stopping rule computable from the run alone.
The book's description of the method runs to two pages; the central difficulty is the termination analysis, not the geometry. The volume of the ellipsoids decreases geometrically, but their diameters need not, so the search points need not converge, and the method cannot know how close it is to the optimum. A naive argument that the search points approach the optimum therefore fails, and the stopping test (5.2.17), which only sees , and the guesses , has to be related to the unknown optimality gap. The analysis must also cover runs in which no step was productive for a long time, and the possibility that the result is undefined. On the geometric side, (∗) requires the exact determinant of a rank-one update and the elementary but not immediate inequality . Reasoning about a recursively defined algorithm also means carrying invariants (the ellipsoid contains every point of not yet cut off, ) through the induction.
Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and the Euclidean norm eucNorm x = √(x ⬝ᵥ x) is defined explicitly (Mathlib's norm on Fin n → ℝ is the sup norm). Volumes are MeasureTheory.volume on Fin n → ℝ, valued in ℝ≥0∞. The setting (5.2.9) with assumption A is the predicate IsBlackBoxProgram f X r R. The oracles are arbitrary functions of the query point satisfying (5.2.10) and (5.2.11); every theorem is quantified over all of them, and none sees the centre . The method is a function run from the number of steps performed to an outcome, running with the current and best productive point, or stopped with an optional result; TerminatesAt t res says the run stops exactly at step . and are reals given by IsGreatest/IsLeast, and is expressed by comparison with every point of , so no supremum or infimum with a default value occurs. Ceil is Int.ceil and the step bound is compared in . A statement about an arbitrary sequence of ellipsoids or an arbitrary "state" carrying no link to the run would trivialize the goal; here the ellipsoids, guesses and result are those the method constructs from the oracles' answers.
Beyond the paper. The book's statement (∗) also has a case , whose printed centre moves by regardless of the segment's length; the containment fails for , , . The case is posed as printed (expected to be disproved) and as a corrected variant with centre . Theorem 5.2.1 assumes and is unaffected.
A complete development needs the determinant of a rank-one update (Matrix.det_add_replicateCol_mul_replicateRow), Lebesgue measure of linear images (MeasureTheory.Measure.addHaar_image_linearMap), the continuity of convex functions on , and an induction over run. The ellipsoid update lemma and the oracle and method definitions are reusable for other cutting-plane methods. Proofs of individual milestones, in particular (∗), are welcome as separate contributions.
Semidefinite programming (SDP), the optimization of a linear function over the intersection of an affine subspace with the cone of positive semidefinite matrices, is the workhorse behind relaxations in combinatorial optimization, robust optimization and control. Its practical and theoretical tractability rests on interior point methods: algorithms that follow the central path, a curve of strictly feasible primal-dual pairs parametrized by a penalty parameter , along which the duality gap equals . The polynomial-time analysis of these methods, due to Nesterov and Nemirovski (Interior-Point Polynomial Algorithms in Convex Programming, SIAM 1994) and, for the primal-dual SDP family considered here, to Monteiro and Zhang and others in the 1990s, reduces to one local statement: a single Newton-type update, started close to the path, lands close to the path again while the penalty parameter grows by a factor .
This mission formalizes that local statement in the form given by Ben-Tal and Nemirovski, Lectures on Modern Convex Optimization (SIAM 2001), Lecture 6, Theorem 6.5.2, for the whole family of primal-dual updates obtained from commutative scalings.
Let and let be the space of real symmetric matrices with the Frobenius inner product and norm . For , is its positive semidefinite square root. Fix a linear subspace , its orthogonal complement in , and . The primal-dual pair is
is strictly primal feasible if and ; is strictly dual feasible if and . For such a pair the duality gap is .
The distance of a pair to the point of the central path with parameter is
and the neighbourhood consists of the triples with , strictly feasible and distance at most .
The updating (U), with parameters , takes a strictly feasible pair and
The choices , and the Nesterov–Todd scaling are all admissible in step 2.
If and the strictly feasible pair satisfies , then for every admissible the system of step 3 has exactly one solution, and
The proof reduces to the case with , and , and the milestones are the numbered facts of that reduced situation, with and :
Theorem 6.5.2 is the step that turns the central path into an algorithm: once a pair in is known, iterating (U) keeps every iterate in and increases the penalty parameter by a constant factor every steps, so the duality gap (Proposition 6.4.2) falls below after steps. The statement covers a whole family of search directions at once, including the Nesterov–Todd direction used by SDP solvers, and by Remark 6.5.2 it specializes to LP when all matrices are diagonal.
The result is classical and proved in the book; it has not been machine-checked. The platform has formalizations of central-path facts for LP and for inequality-form barrier problems, and open items on self-scaled short-step methods, but no statement about primal-dual Newton steps for SDP. A formal proof would supply reusable matrix-analysis infrastructure: Frobenius estimates through eigenvalues, the Löwner order under congruence, and unique solvability of Sylvester-type systems with subspace constraints.
The obvious approach, perturbation analysis of the Newton system in the original variables, does not close: the bound has to hold uniformly in the condition of and , and only the scaled quantities , are controlled by and . The reduction to with diagonal commuting has to be justified, including invariance of the distance under scaling and the change of the subspaces , to , . Uniqueness uses the orthogonality in an essential way. The final estimate passes from the scaled distance to the distance measured at the new point , which needs the Löwner bound and monotonicity of the trace under congruence. The concluding numerical inequality holds for every , not only asymptotically.
All matrices are Matrix (Fin k) (Fin k) ℝ with . is a Submodule ℝ of matrices with every element symmetric, and is the set of symmetric with for all , so the unknowns of the linear systems are symmetric. is Mathlib's CFC.sqrt (with open scoped MatrixOrder), positive (semi)definiteness is Matrix.PosDef/Matrix.PosSemidef, and the Frobenius norm is defined explicitly. The book's (P) comes from a conic problem under Assumption A ( injective) with ; every subspace is such an image, so the formal statements quantify over subspaces. The distance to the central path is defined by its SDP closed form (6.4.11), so no existence result for the central path is needed. The goal is stated for every admissible scaling , and "the system has a unique solution" is a separate conjunct from the properties of that solution, so the goal cannot hold vacuously through an unsolvable system. The milestones of the proof are stated in the book's reduced situation (diagonal , , ) with all of its hypotheses.
Results of §§6.3–6.4 for general canonical cones (products of semidefinite and Lorentz cones with their barriers and ), namely Propositions 6.3.1–6.3.2 and Theorems 6.4.1–6.4.2, and Theorem 6.5.1 (primal path-following), are not part of this mission: they need a calculus of canonical barriers on block-structured spaces. Proofs of any milestone, reusable lemmas on the Löwner order and the matrix square root, and a sorry-free proof of the numerical inequality are welcome.
Many questions in robust control and robust optimization reduce to one test: does a whole family of symmetric matrices, generated by perturbing a nominal matrix along several directions at once, stay positive semidefinite? A linear system whose coefficients are only known to lie in intervals is a typical case. Showing that one quadratic Lyapunov function certifies stability of every member of such an interval matrix comes down to exactly this test. Ben-Tal and Nemirovski isolate it as the Matrix Cube problem. The problem is NP-hard (Ben-Tal & Nemirovski, On tractable approximations of uncertain linear matrix inequalities affected by interval uncertainty, SIAM J. Optim. 12 (2002)). They prove that a simple semidefinite sufficient condition is never far from exact. The gap is controlled by a universal factor that depends only on the ranks of the perturbation directions.
This mission formalizes that result as it appears in §4.4.3 of Lectures on Modern Convex Optimization (Ben-Tal & Nemirovski, SIAM 2001), pp. 189–197, together with the lemmas its proof uses and its application to interval Lyapunov stability.
Matrices are real. is the space of symmetric matrices, its positive semidefinite cone, and means . For , is its vector of eigenvalues, so is the sum of their absolute values.
Fix with . For a level the matrix cube is
the image of the cube under an affine map. The Matrix Cube problem asks for the largest with .
The system of LMIs in symmetric variables is
Its feasibility can be checked by semidefinite programming. The largest for which it is solvable is , the optimal value of the semidefinite problem (4.4.45).
The approximation factor is the function
where is the standard Gaussian density on . The relevant rank is ; is not included.
For the application, is a stable matrix (all eigenvalues in the open left half-plane). has nonnegative entries, and is the interval matrix. asks for with for all , and is the supremum of the for which it is solvable. is the analogue of for this cube. It uses matrix variables and for , and is its supremum.
For all , all , all and all :
and
The result. Proposition 4.4.5 and Theorem 4.4.1 together bound the cube radius. It lies between the efficiently computable and . The factor is in general, independent of and , and exactly when every perturbation has rank at most two. Rank two is the situation of interval matrices, of Lyapunov certificates for interval systems (Proposition 4.4.6), and of a re-derivation of Nesterov's theorem for quadratic maximization over the unit cube (pp. 200–201). The same estimate underlies tractable approximations of robust LMIs with box uncertainty in robust semidefinite optimization.
Formalizing it. The results are proved in the book. None of them, and nothing on the matrix cube, the function or interval Lyapunov stability, is machine-checked on the platform. The formalization adds three things: a checked definition of as a Gaussian integral; a checked proof of the constants and ; and a checked bridge from semidefinite duality to a probabilistic rounding argument. The proof of Proposition 4.4.5 already has a sorry-free local check, which also exposed a sign slip in the printed proof.
The sufficient direction is elementary. The converse is not. Unsolvability of is a statement about a semidefinite program, and turning it into an explicit point with and needs three ingredients:
Bounding coordinate by coordinate, or using a worst-case vertex of the cube, gives a factor that grows with . The rank-dependent constant is what makes the theorem useful.
The constants need real analysis on Gaussian integrals. requires an exact minimization of over . The bound requires a symmetrization and an independence argument. Lemma 4.4.4 needs rotational invariance of the Gaussian measure and diagonalization inside an integral.
Matrix (Fin n) (Fin n) ℝ, and is (X - Y).PosSemidef (which includes symmetry). The index is Fin m, and is for every .CFC.sqrt W under MatrixOrder. Eigenvalues are Mathlib's IsHermitian.eigenvalues, used only through order-independent quantities.EReal, so is represented. Ratios are stated in product form, for example . The "max" in (4.4.45) is stated as attained.A formalization that replaced by an arbitrary function satisfying (4.4.37), or set , or allowed , would state a different (false or ill-posed) theorem; the statements here rule these out.
Infrastructure needed and reusable beyond this mission:
Contributions of separate lemmas are welcome, for example monotonicity of or .
A homogeneous quadratic inequality may hold at every point where other quadratic inequalities hold. Deciding when this happens is the quadratic analogue of the question the Farkas lemma answers for linear inequalities. It is the core of robust optimization with ellipsoidal uncertainty, of absolute stability in control (where it is known as the S-procedure), and of trust-region and quadratically constrained programming. The answer one wants is a linear certificate: nonnegative multipliers with , a condition that can be checked by semidefinite programming.
Lecture 4 of Ben-Tal and Nemirovski, Lectures on Modern Convex Optimization (SIAM, 2001, doi:10.1137/1.9780898718829), states the classical case and, in its exercises (§4.10.5), traces how far it extends:
Vectors are and matrices are real . For a symmetric matrix , the quadratic form is . means that is positive semidefinite, and means is positive definite. A quadratic inequality is a consequence of a system , if it holds at every satisfying the system. The system is strictly feasible if some satisfies both inequalities strictly.
The inhomogeneous case uses and . For the topological steps, is the unit sphere of . The projective space is with each identified with , and is the canonical projection.
Let and let be symmetric matrices such that (i) some linear combination is positive definite and (ii) , for some . Then
The S-lemma converts a semi-infinite family of quadratic implications into one linear matrix inequality. This is what makes robust counterparts of conic quadratic constraints with ellipsoidal uncertainty semidefinite-representable (Proposition 4.5.1 of the book), and it gives trust-region subproblems and quadratic programs with one constraint their exact semidefinite duals. The two-constraint version extends this exactness to problems with two quadratic constraints in dimension at least three. Polyak's convexity theorem is the structural fact behind it, and it is of independent use in the study of joint numerical ranges.
All statements are proved in the literature. On Prove2Me, the inhomogeneous S-procedure in another sign convention is proved (ConvexOptimization.s_procedure), as is the finite Helly theorem (FamousTheorems.helly_theorem). The homogeneous S-lemma is a special case of the former but is not stated on the platform. The infinite Helly theorem with the boundedness condition, Polyak's theorem, the projective-space connectedness facts and the two-constraint S-lemma have no machine-checked statement or proof there. Two statements beyond the book are posed alongside it (see Formalization scope).
The "if" directions are one line each. Every "only if" direction must produce multipliers from a pointwise implication, and there is no Farkas lemma for quadratic inequalities to do it. With two constraints a direct separation argument needs the joint range of three quadratic forms to be convex. That range is not convex in general, and it can fail to be convex for , so any argument has to use the dimension. The book's milestones for this step are topological: paths on spheres, quotients by the antipodal map, and connectedness in projective space. None of this is packaged for this use in Mathlib. Two printed details mislead a solver who follows the page. The matrix in Proposition 4.10.1 omits in its northwestern entry. The hint for (SL.C) (Exercise 4.48) asks for a positive definite combination , where only semidefiniteness can be obtained. The proof of Theorem 4.3.3 also swaps the roles of and at one step.
Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ. The form is x ⬝ᵥ (A *ᵥ x) and symmetry is Matrix.IsHermitian. and are Mathlib's Matrix.PosSemidef and Matrix.PosDef, both of which include symmetry. The bordered matrix of Proposition 4.10.1 is indexed by Unit ⊕ Fin n with the scalar entry first, as printed. For Propositions 4.10.2 and 4.10.4, the sphere is Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1. is its quotient by with the quotient topology (one definition item), which has the same topology as the book's metric . The book's linear connectedness, which allows the empty set, is stated pairwise. Every hypothesis of the page is an explicit binder. In particular, strict feasibility appears in every S-lemma variant, appears in (SL.C), (SL.D) and Proposition 4.10.4, and the positive definite combination in (SL.C) involves all three of with coefficients of any sign. The implication is quantified over all of and the multipliers carry their sign constraints. Dropping (ii), or leaving unconstrained, turns the goal into a statement that is false or trivial, and neither is the book's.
Beyond the paper. Two variants are posed beside the faithful items. One is a corrected Proposition 4.10.1 with northwestern entry : as printed, the matrix criterion fails for , , . The other is a sharpness probe of (SL.C) without , for which , , is a counterexample; its disproof is the sought outcome.
Contributions welcome: the joint range of quadratic forms (Dines's theorem, Polyak's theorem), the projective space as a topological space, and infinite Helly-type intersection theorems. All are reusable beyond this chapter.
Truss topology design asks for the stiffest elastic bar construction that can be built from a given set of potential bars with a given amount of material. It is one of the oldest test cases of structural optimization (Bendsøe and Sigmund, Topology Optimization, Springer 2003) and one of the main applications in Ben-Tal and Nemirovski's Lectures on Modern Convex Optimization (SIAM 2001). The quantity being minimized, the compliance of the truss under a load, is defined through the solution of a linear system and takes the value when the structure cannot carry the load, so it is not obviously a convex function, let alone one a solver can handle. Lecture 1 of the book shows that the single-load problem happens to become a linear program. Section 3.4.3 explains why: the compliance, as a function of the bar volumes and of the load jointly, is conic quadratic representable, and its epigraph has an explicit description by second-order cone constraints. That description is what turns multiload designs, bounds on bar volumes and other variants into conic quadratic programs.
This mission is the fourth of a series formalizing the book's main results, and covers Lecture 3, §3.4.3 (pp. 120–128), together with Proposition 2.4.2 of Lecture 2, on which it relies.
A ground structure consists of real matrices , (for a classical truss and is the direction vector of bar ). A truss is a vector with (the bar volumes) and a load is . The bar-stiffness matrix is
and the compliance is
with when the equilibrium equation has no solution; the value does not depend on which solution is used. For that are not nonnegative the compliance is extended by . The potential energy of the loaded truss is .
The ice cream cone is . A set is conic quadratic representable (CQr) if there are finitely many inequalities , affine in and in additional variables , such that exactly when some satisfies all of them; a function with values in is CQr when its epigraph is. A linear vector inequality is almost solvable if for every some with makes solvable.
For all , and , (extended compliance) if and only if there are vectors with
where and for . In particular, is CQr.
The proposition gives an explicit second-order cone description of the epigraph of the compliance, jointly in the design and the load . Consequences: single-load, multiload and volume-constrained truss design problems become conic quadratic programs solvable by interior-point methods; the compliance is a convex function of ; and the proposition contains a second variational principle (the reaction forces minimize the stored energy subject to equilibrium, p. 128). It also explains the linear-programming formulation of Lecture 1.
The results are classical and proved in the book; none of them is machine-checked. A formalization adds checked statements of the variational principle for positive semidefinite quadratic forms, the conic theorem of the alternative for almost solvability, and a first instance of conic quadratic representability on the platform, with the convention made explicit.
The compliance is defined through solvability of a singular linear system, so neither convexity nor any representation is visible from the definition. The equivalence in the goal must handle trusses with missing bars (), where is singular and the convention matters, and loads outside the range of , where the compliance is infinite. The book's route goes through a conic theorem of the alternative, which in the conic case characterizes only almost solvability, not solvability; passing from the strict epigraph to the non-strict one in the goal requires a separate attainment argument. A step-by-step translation must keep track of the perturbations of the right-hand side.
Vectors are functions on finite index types (Fin m → ℝ, Fin n → ℝ, Fin (k i) → ℝ); the stacked inequality of (3.4.49) is indexed by the pairs , , followed by two extra coordinates, the last of which is the distinguished coordinate of . The compliance takes values in EReal: ⊤ exactly when is unsolvable, and otherwise the real number ; it only ever appears in comparisons with a real . The convention , is encoded by requiring whenever together with Lean's real division; Lean's alone would let a missing bar carry any force, and this trivializing reading is ruled out. The CQr conclusion is not "some representation exists" in an unconstrained sense: it is a finite system of Lorentz-cone constraints , , affine in the variables, exactly as on p. 86. Proposition 2.4.2 carries the book's standing assumptions: a pointed closed convex cone with nonempty interior, and Assumption A (full column rank of , p. 53, in force by Remark 2.4.1).
Beyond the paper. One variant is posed: a strengthened Proposition 2.4.2 without Assumption A and on arbitrary finite index sets. Evidence: the systems involved depend on only through its column space, so a basis of that space reduces the general case to the stated one. This is the form actually used on p. 126, where the matrix of (3.4.49) can fail Assumption A (for example , ), a gap in the printed argument recorded as a finding.
Needed infrastructure: positive semidefinite quadratic forms and their minimization (Mathlib's Matrix.PosSemidef), dual cones and separation in finite dimension, the ice cream cone and its self-duality, and continuity of minimum values of quadratic forms under perturbation. The definitions of the Lorentz cone, CQr sets and functions, and almost solvability are reusable across the series. Proofs of individual milestones are welcome independently; Lemma 3.4.1 and statement (O) are self-contained.