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?
Primal-dual interior-point methods are the standard polynomial-time algorithms for linear programming and the basis of most commercial LP solvers. Among them, path-following methods are the ones with the cleanest complexity theory: they keep every iterate inside a neighborhood of the central path and shrink the duality measure by a fixed factor per step. Chapter 5 of Stephen J. Wright's Primal-Dual Interior-Point Methods (SIAM 1997) presents three such methods — a short-step method, the Mizuno–Todd–Ye predictor-corrector method, and a long-step method — and analyzes each from a small set of one-step estimates.
The short-step method and its iteration bound go back to Kojima, Mizuno and Yoshise (1989) and Monteiro and Adler (1989); the predictor-corrector method with two nested 2-norm neighborhoods is due to Mizuno, Todd and Ye (Math. Oper. Res. 1993); the long-step method in the wide neighborhood with its bound is in the same line of work. Wright's chapter gives a single, uniform treatment of the three, with explicit constants.
Fix , , , with no assumption on the rank of . The primal problem is subject to , , and the dual is subject to , . A primal-dual point is a triple . The strictly feasible set consists of the triples with , , and (componentwise).
For vectors write , and , so is the vector of pairwise products . The duality measure is . The 2-norm neighborhood of the central path is
and the one-sided -norm neighborhood is , .
Given a centering parameter , a search direction is any solution of the step equations
Along it, and . The vector of products is the second-order term that the linearization ignores.
Let satisfy
If and solves the step equations with this , then
This is a one-step statement with no algorithm loop. It is the invariant of the short-step method (, ).
Theorem 5.6 is the step that turns the linear decrease of (Lemma 5.1) into a convergence proof: once the full step is known to stay in , the duality measure falls by the factor at every iteration, and the generic complexity theorem of Chapter 3 gives the iteration bound, the standard bound for primal-dual interior-point methods. Lemmas 5.7 and 5.8 give the same bound for the adaptive predictor-corrector method, and Lemma 5.10 with Theorem 5.11 the bound for the long-step method, which is the variant closest to practical codes.
On the platform, the Mizuno–Todd–Ye predictor-corrector analysis has been formalized in a different parametrization (pairs with an existential dual multiplier, and a different step bound); the results of this chapter in Wright's triple form, the general Lemma 5.3, the short-step invariant and the long-step reduction are not yet formalized. A machine-checked version yields reusable infrastructure: the step equations, the two neighborhoods and the pairwise-product bounds are used by every later chapter of the book (infeasible methods, superlinear convergence, finite termination).
The step equations are linear, but neighborhood membership is not: the products are quadratic in , and the quadratic coefficient is not controlled by the equations individually — only the sum vanishes. A bound on in terms of alone, uniformly over the neighborhood, is the crux; a naive bound through the norms of and separately involves the conditioning of and is not uniform. The second subtlety is strict positivity: the proximity inequality at every does not by itself rule out a coordinate of or changing sign, and the conclusion of Theorem 5.6 requires , for the whole segment.
Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, points are triples (x, lam, s). The norm is the explicit Euclidean norm (Mathlib's default norm on Fin n → ℝ is the sup norm). and are subsets of , so membership includes both equality constraints and strict positivity. The direction is defined by its linear equations, never by a closed-form solution, so no rank assumption and no nonsingularity are presupposed. Where the page leaves the ranges implicit, the standing ones are hypotheses: for , for , for the step equations. In Lemmas 5.1 and 5.5, ranges over all reals, as the page places no restriction on it.
Explicit constants: the book's "there is a constant independent of " in Theorem 5.11 is replaced by the its proof derives (p. 100); every other constant is printed in the statements. In (5.19), the case is read as ; real division by zero, which would make and Lemma 5.7 trivial on the interval , is excluded by an explicit case split. "The largest " in Algorithms PC and LPF is a hypothesis (IsGreatest) on the chosen step, never a construction. A trivializing formalization — one that states only the proximity inequality without strict feasibility — is ruled out by the definition of .
Beyond the paper: one variant is posed beside the faithful goal. theorem_5_6_strong (strengthened, finding F1) is Theorem 5.6 for every real : condition (5.15) already forces when , and the bound is not used by the argument.
Needed infrastructure: finite sums and the Euclidean norm on Fin n → ℝ, Matrix.mulVec and dot products, real powers. Proofs of Lemma 5.3 and of the positivity argument along the segment are reusable well beyond this mission; contributions of either are welcome.
Interior-point methods solve linear programs by moving through the interior of the feasible region instead of along its edges. Two families dominate the theory: path-following methods, which keep the iterates near a central path, and potential-reduction methods, which instead measure progress by a single merit function and only ask that it fall by a fixed amount at every iteration. The second family grew out of Karmarkar's projective algorithm (Karmarkar 1984). The primal-dual potential used here was introduced by Tanabe and by Todd and Ye (Todd–Ye 1990), and the primal-dual step analysed in this mission is that of Kojima, Mizuno and Yoshise (Kojima–Mizuno–Yoshise 1991). It attains the iteration bound, the best known for any interior-point method.
The mission follows Chapter 4 of S. J. Wright, Primal-Dual Interior-Point Methods (SIAM 1997), the standard graduate text on the subject. Its argument is self-contained and fully quantitative: a fixed decrease of per step, and an explicit iteration count.
Let , and , with no rank assumption on . The primal problem is subject to , , and the dual is subject to , . The strictly feasible set is
inequalities being componentwise. The duality measure is . Write , and .
For a parameter , the Tanabe–Todd–Ye potential is
evaluated where . Algorithm PR iterates as follows. At it computes the search direction , the solution of
It then sets and takes a step length that minimizes over .
The analysis compares along the direction with a quadratic. For define
and the quadratic estimate . Let , and with . Here is the Euclidean norm and the max-norm.
For , , , the direction above, and :
and every minimizer of the potential along the direction satisfies
The goal fixes and the constant because the book does. Its proof in fact gives .
Theorem 4.6 is the per-iteration guarantee of the method. Combined with Theorem 4.4 it yields Corollary 4.7. At this is an bound on the number of iterations needed to reduce the duality measure below . The same template underlies potential-reduction methods for linear complementarity and semidefinite programming: a fixed decrease of a potential, plus the inequality linking the potential to .
Formalizing the chapter yields a machine-checked complexity proof of a primal-dual interior-point method for linear programming, with every constant explicit. It also yields reusable pieces: the logarithmic estimates of Lemma 4.1, the bound of by the potential, and the generic counting argument of Theorem 4.4. The results are classical and proved on paper. No formal version of this chapter exists on the platform. The related published items cover a different potential-reduction method (Mizuno–Todd–Ye, in a wide neighbourhood) and a different counting bound (Bertsimas–Tsitsiklis).
The proof of Lemma 4.5 is the centre of the argument. It needs a lower bound on uniform over all strictly feasible points, including badly centred ones. A naive bound through loses the factor that cancels against .
The hypothesis is essential, and Theorem 4.6 does not print it. It is stated for Lemma 4.5 and Corollary 4.7. For the conclusion fails: at , the potential can fall by at most about .
The step from the quadratic estimate to the potential has its own subtleties. The open interval need not contain a minimizer, and can equal (at , ). The second conclusion of the goal is therefore stated for every minimizer, and a proof must not assume .
Vectors are Fin n → ℝ and matrices are Matrix (Fin m) (Fin n) ℝ. All definitions are in Definitions.Def_WrightPDIPM_Potential_Setting. These are Fo, mu, Phi, alphaMax, IsFeasibleDirection, IsPRDirection, g1, g2, q, vvec, vmin, rvec, alphaBar and IsPRStep. The search direction is defined by its linear equations, never by a closed-form inverse. The arg min of the line search is a hypothesis (IsMinOn on the open interval), never constructed.
is the formula itself, and every statement evaluates it only at positive vectors. Standing hypotheses of the chapter are explicit binders: , , for Lemma 4.3(i), and for Theorem 4.6. Indices are integer ceilings compared with in .
The book's O(·) in (4.32) is decoration: the explicit is what is stated. Theorem 4.6 has no O(·); its constants are and .
A trivializing formalization is ruled out. The direction is the solution of the PR system, not an arbitrary feasible direction (for which the claim is false). The coefficients are computed from it, not free reals (for which it would be empty). never takes Lean's junk value , since whenever .
Beyond the paper. Two variants are posed next to the faithful items.
lemma_4_5_strong (strengthened, finding F2) proves (4.28) for . Lemma 4.5 prints a strict inequality, but its proof covers the endpoint, which Theorem 4.6 and Corollary 4.7 use.theorem_4_6_probe (sharpness, finding F1) is Theorem 4.6 under only . It is expected to be false, since a centred point with , falls by at most , and a disproof is welcome.Contributions welcome: proofs of any milestone, a proof of the goal, and a disproof of the probe.
Estimating a probability density, a conditional probability or a conditional density from data can be written as solving a linear operator equation whose right-hand side is a distribution function. The true is unknown; only its empirical estimate is available, built from observations. The Glivenko–Cantelli theorem and the Kolmogorov–Smirnov law (Vapnik 2000, §7.3) guarantee that is close to in the uniform metric. However, the operator (for densities, integration) has an unbounded inverse. A small change in the right-hand side can produce an arbitrarily large change in the solution, so solving directly gives nonsense. Hadamard called such problems ill-posed.
Regularization handles this. Tikhonov (1963) proposed replacing the equation by the minimization of a penalized residual. Tikhonov and Arsenin (1977) proved that the regularized solutions converge to the true solution when the data error and the regularization parameter go to zero together in a controlled way. Vapnik and Stefanyuk (1978) extended this to random right-hand sides, the case of statistical estimation, and Stefanyuk (1986) to the case where the operator is estimated as well. Chapter 7 of The Nature of Statistical Learning Theory collects these results, without proofs, as the foundation of its SVM approach to density and conditional-probability estimation. This mission formalizes them.
Let and be metric spaces and a continuous one-to-one operator. The operator equation (7.12) is . Its solution exists and is unique, but need not be continuous.
A regularization functional is a map that is lower semicontinuous and whose sublevel sets are compact for every . Its domain is . In Lean this is NatureSLT.IllPosed.IsRegularizer.
Tikhonov's functional (Method T) for a parameter and a right-hand side is
which is NatureSLT.IllPosed.tikhonovFunctional. A regularized solution is any minimizer of over .
In the deterministic problem, for every an approximation with is given, and minimizes with and . In the stochastic problem, are random elements of converging to in probability, and minimizes with and . When the operator is also estimated by random continuous operators , their distance to is measured by (7.48),
which is NatureSLT.IllPosed.operatorDistance.
Let the exact solution lie in the domain of , and suppose satisfies (7.17):
Then every family of minimizers of satisfies in as . This is the weakest statement in the chapter: it fixes no rate and assumes only metric structure.
The constants are the book's: the of (7.17), the of (7.21), the factor and the threshold of Theorem 7.4, and the , of (7.49).
Theorem 7.1 is what makes regularization a method rather than a heuristic: it names the admissible parameter choices, no faster than , under which the regularized solution recovers the true one. Theorems 7.3 and 7.4 turn it into probability statements. Combined with any rate of convergence of the empirical distribution function, they give consistency of density estimation by Method T, which is the Corollary on p. 239. Theorem 7.5 does the same when the operator itself is estimated from data, as in conditional probability estimation (§7.9). Chapter 7's SVM estimators of densities and conditional probabilities rest on these statements.
The results are classical and proved in the literature cited. None of them is machine-checked. The platform has Tikhonov-regularized dynamics (TikhonovHDD) and finite-dimensional ridge identities (RobustLS.Tikhonov), but not the convergence theory of Tikhonov's method for operator equations. A formalization supplies a reusable notion of regularization functional on a metric space, the Tikhonov functional over , and the operator distance (7.48), for later work on inverse problems and nonparametric estimation.
The obvious approach, inverting and passing to the limit, fails because is not continuous: alone does not force . The deterministic theorems need control of the regularized solutions that the residual does not give, and in Theorem 7.2 that control must be obtained without compact sublevel sets, since the balls of an infinite-dimensional Hilbert space are not compact. In the stochastic theorems the difficulty is uniformity: a deterministic convergence statement for each outcome does not give the explicit comparison of probabilities that (7.21) and (7.49) assert. In (7.49) the bound must hold for every parameter below a threshold that depends only on , , .
Two warnings from reading the chapter apply. Theorem 7.4 as printed is false: with exact data () both probabilities vanish for all large , and the strict inequality fails (finding F1). Also, the three "uniqueness" properties of listed on p. 235 are mutually inconsistent at , which is why they are not assumed (finding F3).
All statements live in NatureSLT.IllPosed. takes values in ℝ≥0∞. The book's "positive" is nonnegativity and its domain is . "Semicontinuous" is lower semicontinuity. The exact solution is assumed to lie in the domain of (the book assumes this tacitly); otherwise every point could minimize . Every theorem is stated for every family of minimizers, given as a hypothesis, never for a chosen sequence, and does not assert that minimizers exist. Statements of the form "there exists a sequence that converges" are a trivializing formalization and are ruled out. The limit in (7.17) is read as a limsup in , and is taken along . Hilbert spaces are real. Linearity of (Theorems 7.2 and 7.4) makes a real normed space. In the stochastic theorems the probability space is arbitrary, and the random elements , (and in 7.5 the random distance ) are Borel measurable by hypothesis, so no event gets probability zero by convention. In (7.48) a point with contributes if and otherwise. In Theorem 7.5, is quantified before the random data, so it is uniform over all of them.
Beyond the paper. One variant item is posed: [Corrected] Theorem 7.4, the same statement with in place of . Its evidence is the exact-data counterexample above, which has been checked in Lean. The faithful Theorem 7.4 stays a milestone.
Not included: the Glivenko–Cantelli theorem in the book's in-probability form (the platform's GlivenkoCantelli.glivenko_cantelli is the almost-sure form), the Kolmogorov–Smirnov limit laws (7.10)–(7.11), and Theorem 7.6, whose notion of consistency is not pinned down on the page. Contributions welcome: compactness arguments in metric spaces, weak compactness and the Radon–Riesz property in Hilbert spaces, and measurability lemmas for minimizers.
A support vector machine never computes its feature map. It only evaluates a kernel , the inner product of the feature vectors of and . When the features are the first terms of an expansion, or infinitely many terms damped by regularizing weights, the learning algorithm is practical only if that inner product has a closed form. Chapter 6 of V. N. Vapnik, The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1), §6.3–6.5, gives such closed forms for the kernels generating orthogonal-polynomial, spline and Fourier expansions. It also states Theorem 6.1, which lifts any one-dimensional kernel to dimensions. The book prints these identities without proof and cites classical sources (Mikhlin 1964; Gradshtein and Ryzhik 1980). Several of them, as printed, are off by a constant factor, which a formal check settles.
Kernels in this mission are real functions of two real variables (or of two vectors of ) of the form , a finite or convergent sum over basis functions with weights .
For and real with , the series converges and
The only numbered theorem of the section, Theorem 6.1, is close to an unfolding of the definitions. The goal is therefore the deepest identity of the section that is correct as printed.
Milestones 2, 4 and 6 are stated exactly as printed and are believed false (see Formalization scope). A disproof of each is a complete answer.
The result itself. Each closed form replaces an infinite or high-dimensional inner product by a constant number of elementary operations. That is what makes the regularized Fourier, Hermite and spline kernels usable in an SVM. Theorem 6.1 is the mechanism by which every multidimensional kernel of Chapter 6 is obtained from a one-dimensional one. The constants matter in practice. A wrong prefactor rescales the kernel matrix, and so the effective regularization of the SVM solution.
Formalizing it. The identities themselves are classical (Christoffel 1858, Darboux 1878, Mehler 1866, and the Fourier series of on ). As far as a search of the platform shows, none is stated on Prove2Me in these forms. SpikedWishart.Separated.eq_299 (Open) is one Christoffel–Darboux instance for a specific Hermite family. AronszajnRK.Product.direct_product_kernel concerns reproducing-kernel Hilbert spaces, not finite or summable feature sums. The mission produces machine-checked versions of the book's catalogue, together with a formal verdict on the three displays that are off by a constant.
The goal and (6.32) are infinite-series identities with no ready-made counterpart in the library, and the goal holds only on . Outside that range the left side is -periodic and the right side is not, so no argument that ignores the range can succeed. The Christoffel–Darboux formula needs a theory of orthogonal polynomials for a general measure, which Mathlib does not yet provide. (6.24) involves the iterated derivatives of and a doubly infinite parameter family. The spline identity requires evaluating a piecewise-polynomial integral exactly. Theorem 6.1 for infinite bases requires summability over a product index set . The three false displays (2, 4, 6) hide their error in a constant factor. Two of them still reduce to an identity a solver may expect to hold.
Everything is over . Series are stated with HasSum, or as Summable together with an equation for tsum. A divergent series therefore never reads as . Sums over are written over with in place of . The Christoffel–Darboux polynomials are indexed as in the book ( is the constant), they are orthonormal up to , and the measure has all moments finite. The Hermite is the physicists' family, defined through iteratedDeriv. It is not Mathlib's probabilists' Polynomial.hermite. The normalization constants of (6.24) are existentially quantified, since the book does not give them. The range of in (6.24) and (6.26) is : the book's without the singular point . The Dirichlet display is stated where . The goal adds , which the page leaves unstated. Spline points lie in with . In Theorem 6.1, the multidimensional kernel is the sum over multi-indices of products of basis functions, a statement to be proved and not the product of kernels by definition. A formalization that defined the -dimensional kernel as would make the theorem trivial, and is ruled out.
Beyond the paper. Three corrected variants sit beside the faithful statements. Each changes one clause only. dirichlet_kernel_corrected (finding F1) uses the denominator , since at and the printed display reads . hermite_kernel_corrected (F2) takes without the Gaussian factor. At the printed (6.24) forces for all , and the corrected form is Mehler's formula. hermite_kernel_multidim_corrected (F3) uses the prefactor , since at , , the printed (6.26) reads . One further observation is recorded without a variant: (6.33) also holds for , because both sides are even in .
Reusable beyond this mission are the two definitions (the physicists' Hermite functions and the truncated power) and any proof of the summable form of Theorem 6.1. Proofs, disproofs of the three false milestones, and general lemmas on Fourier series of and are all welcome.
Primal-dual interior-point methods are the standard polynomial-time algorithms for linear programming and the basis of most commercial LP solvers. They do not move along the boundary of the feasible polyhedron, as the simplex method does. Instead they follow a curve through its interior, the central path, toward the solution set. Every convergence and complexity result about these methods assumes that this curve exists. Stephen J. Wright's monograph Primal-Dual Interior-Point Methods (SIAM, 1997, doi:10.1137/1.9781611971453) proves existence in its Chapter 2 from the standard LP background: existence of solutions, boundedness of solution sets, the Goldman–Tucker partition, and a primal-dual logarithmic barrier.
This mission is the first in a series that formalizes the book chapter by chapter. Later missions (potential reduction, path following, infeasible methods, finite termination, the homogeneous self-dual form) take the objects defined here as given.
Let , and . Nothing is assumed about the rank of . The primal and dual linear programs in standard form are
with all vector inequalities componentwise. The primal-dual feasible set consists of the triples with , and . The strictly feasible set is the same set with . The solution sets are , the minimizers of (2.1); , the maximizers of (2.2); and . The index sets and collect the coordinates for which some has , and some has , respectively.
For , the central path conditions (2.25) ask for with
The reduced strictly feasible set is the set of pairs such that for some . The primal-dual log barrier on it is
In Lean all of these objects live in the single definition module WrightPDIPM.CentralPath.LP, under the names F, Fo, OmegaP, OmegaD, Omega, indexB, indexN, Hcirc, ftau and CentralPathConditions.
If and , then two things hold. First, has exactly one local minimizer relative to :
Second, the central path conditions (2.25) have a solution .
The result itself. Theorem 2.8 shows that the central path exists as soon as the problem has a strictly feasible primal-dual point. Every path-following and potential-reduction method in the book either tracks this curve or measures its iterates against neighbourhoods of it, so the theorem is the foundation the book's convergence and complexity results stand on. Theorem 2.4 provides the strictly complementary partition , which the local and superlinear convergence analysis and the finite-termination results use. Theorems 2.1 and 2.3 are the duality and boundedness facts beneath both.
Formalizing it. These are classical results with complete textbook proofs. The work left is machine-checking them in the book's own form: standard-form LP, no rank assumption, the primal-dual barrier rather than the primal barrier, and minimality relative to . Related statements are already on the platform: Farkas's lemma and LP strong duality in Bertsimas–Tsitsiklis form, a central-path theorem in Matoušek–Gärtner form under the assumption with the primal barrier, and Goldman–Tucker for the inequality-form LP. None of them is any of the statements above, but their proofs may be reusable.
The natural first step is to minimize by compactness. This does not work directly, because is neither closed nor bounded and is not coercive on all of . The quadratic term is indefinite in general, and only its restriction to the affine set of feasible pairs is linear. To obtain a minimizer one must show that the level sets of inside are compact. This needs a boundedness statement (Lemma 2.5) that uses a strictly feasible point in an essential way, together with lower bounds that keep away from . A second difficulty is that has empty interior in whenever . Passing from the minimizer to the conditions (2.25) is therefore a constrained first-order argument with multipliers, and it must work without having full row rank, so the multiplier is not unique. For Goldman–Tucker, the obstacle is the step from "every index is positive at some optimum" to a single optimum that is positive on every index of and of at once.
Vectors are Fin n → ℝ and matrices are Matrix (Fin m) (Fin n) ℝ. Inequalities are componentwise. Indices are 0-based in Lean and is Set.univ. Primal-dual points are triples (x, λ, s). "Bounded" means Bornology.IsBounded. and are defined as sets of optimal points (feasible, and at least as good as every feasible point), so no infimum or supremum is taken and an unattained optimum gives the empty set. No rank assumption on is made anywhere. No result in this chapter has an or an unspecified constant, so no constants are instantiated.
"Local minimizer in " means IsLocalMinOn (ftau τ) (Hcirc A b c), that is, minimality among nearby points of . Local minimality in all of would make the claim false. Uniqueness is asserted for the minimizer only, never for . uses Real.log and is only ever evaluated on , where every .
The hypothesis is part of the goal and cannot be weakened. If , then and the first conclusion becomes false. A formalization that drops it, or one that replaces "unique local minimizer on " with "a global minimizer exists", is not this theorem.
The book prints Theorem 2.4 without a hypothesis. The faithful item carries the section's standing case , which by Theorem 2.1 gives .
Beyond the paper. One sharpness probe, theorem_2_4_probe, states Theorem 2.4 exactly as printed, with no hypothesis. It is expected to be false. For , , , the primal is infeasible and the dual objective is unbounded, so . A disproof is the sought outcome.
Infrastructure that is reusable beyond this mission includes the standard-form LP objects, the solution sets and the / partition, all of which later chapters use; KKT conditions for linearly constrained convex minimization; and strict convexity of . Contributions of general lemmas toward any of these are welcome.
A separating hyperplane in is a classifier of VC dimension , so a bound on its generalization error that goes through the VC dimension degrades with the dimension of the space. Support vector machines construct hyperplanes in feature spaces of enormous dimension and still generalize. Chapter 5 of V. N. Vapnik, The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) explains this by a different capacity measure. When a hyperplane is required to separate the data with a margin , and the data lie in a ball of radius , the VC dimension is bounded by roughly , independently of .
Timeline. The optimal (maximal margin) hyperplane goes back to Vapnik and Chervonenkis (1965, 1974). Its use with kernels, in place of an explicit feature space, is due to Boser, Guyon and Vapnik (COLT 1992), and the soft-margin support vector machine to Cortes and Vapnik (Machine Learning 20 (1995)). The margin bound appears as Theorem 5.1 of the book, which prints no proofs (Preface, p. xi). In Burges's tutorial (Data Min. Knowl. Disc. 2 (1998)) the bound for "gap tolerant classifiers" carries a ceiling, .
Vectors live in with the Euclidean inner product . A -margin separating hyperplane is a hyperplane with and . It classifies as if and as if ; vectors in the strip get no label (§5.4.2, p. 132). Vectors are shattered by these hyperplanes if each of the labelings is realized by one hyperplane that classifies every with label . The VC dimension on a set is the largest for which some are shattered, or . In Lean these are MarginClassifies, MarginShatters and marginVCDim in NatureSLT.Margin.
For training data with , a hyperplane is in canonical form if for all (5.8). The optimal hyperplane satisfies (5.8) and minimizes over and (5.9). Its support vectors are the with equality in (5.8). The dual functional is (5.17). In Lean: IsCanonicalSeparating, IsOptimalHyperplane, supportVectors and dualW.
If every lies in a sphere (closed ball) of radius and , then
with the integer part. As printed this is false (see Beyond the paper), and a disproof of the goal is a legitimate outcome of the mission.
Theorem 5.1 is the reason the book gives for the generalization of the optimal hyperplane in high-dimensional feature spaces (§5.6.1). With the bound (3.24) it drives the Corollary on p. 133 and the choice of in structural risk minimization. Milestones 1–4 are the convex-optimization facts on which the construction of the support vector machine rests: margin maximization as a quadratic program, its Kühn–Tucker characterization and the dual problem. Milestone 5 is the condition under which a kernel can replace the feature-space inner product.
On the platform, UnderstandingML.hard_svm_max_margin (the analogue of milestone 1 with the convention ) and UnderstandingML.support_vectors (the bias-free Hard-SVM) are proved. UnderstandingML.kernel_iff_posSemidef characterizes kernels by positive semidefinite Gram matrices, and HighDimStat.Rkhs.thm12_20_mercer_v2 (open) is the eigen-expansion of a continuous kernel on a compact space. There is no margin-dependent VC dimension bound; the BartlettNN.Margin.* results bound fat-shattering dimensions of real-valued classes. The mission adds the book's bias-carrying statements, the first formal Δ-margin VC bound, and machine-checked settlements of the misprinted statements.
The dimension part of the bound, , is the classical VC dimension of affine half-spaces; the content is the radius part. A solver has to control how far apart the two classes of an arbitrary dichotomy of points in a ball can be pushed by a unit-normal hyperplane with a free bias. The bias does not cancel for unbalanced dichotomies, and this is exactly where the printed integer part and the correct bound part ways. The Kühn–Tucker milestone requires optimality conditions for a convex quadratic program with linear inequality constraints. The Mercer milestone requires the spectral theory of Hilbert–Schmidt integral operators on of a set of positive Lebesgue measure. Neither is packaged in Mathlib in this form.
Vectors are EuclideanSpace ℝ (Fin n); training data are indexed by Fin ℓ; labels are real numbers with as a hypothesis, and both classes present, the setting of §5.5. In the shattering definition, labels are booleans. "Sphere of radius " is a closed ball about an arbitrary center; and are hypotheses. The VC dimension takes values in , so an unbounded family is , never a junk value. Shattering requires every point to be classified with its margin: a definition that let points fall into the strip would make the bound trivial, and is ruled out. Optimality is a predicate on a given pair ; no item asserts that an optimum exists. The typo "" of §5.4.2 is read as . The Mercer items take () measurable of positive Lebesgue measure, with orthonormal in and the expansion converging in .
Not drafted: the Corollary on p. 133 and Theorem 5.2 (p. 139). Both are probabilistic, and their hypotheses (what the VC dimension of a set of partial classifiers means inside (3.24), the training-set size in the leave-one-out argument) are not pinned down on the page.
Beyond the paper. Two [Corrected] variants are posed beside the faithful items. (1) Theorem 5.1 with the ceiling : the vertices of an equilateral triangle inscribed in the unit circle of are shattered with , while , a counterexample to the printed bound that has been checked in Lean. (2) Mercer's theorem with in the condition and the coefficients: a kernel over the incomplete system on has positive coefficients, yet for .
Contributions welcome: a convex-quadratic-programming KKT library for finitely many linear constraints; integral operators with kernels and their spectral expansion; disproofs of the faithful Theorem 5.1 and Theorem 5.3.
Statistical learning theory asks when minimizing the error on a finite sample also controls the error on unseen data. For a set of classifiers, the answer given by Vapnik and Chervonenkis is governed by a single combinatorial quantity: how many different ways the set can label points. Bounds on the generalization error of empirical risk minimization are stated in terms of the logarithm of this number, the growth function, and they are informative only if the growth function grows sublinearly in .
The theorem at the centre of this mission says that there is no middle ground: the growth function is either exactly for every , or, from some point on, it is bounded by a logarithmic function . The integer is the VC dimension. This dichotomy is what turns the abstract bounds of Chapter 3 of V. N. Vapnik, The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) into constructive ones (Eq. (3.24) of the book).
Timeline. Vapnik and Chervonenkis announced the connection between the growth function and the shattering number in 1968 and proved it in 1971 (Theory Probab. Appl. 16 (1971)), in the form for all or . Sauer (J. Combin. Theory A 13 (1972)) and Shelah (Pacific J. Math. 41 (1972)) independently proved the sharp polynomial bound . The logarithmic form used in the book follows from that sum together with the estimate . The book states its results without proofs (Preface, p. xi).
Let be a nonempty set and a nonempty set of parameters, and let , , be a set of indicator functions on : each takes only the values and . For a sample (repetitions allowed), let
be the number of different binary vectors obtained as ranges over (Section 2.3.2, p. 42). The growth function is
(Section 2.7, p. 55), with the natural logarithm. Since , always .
Points are shattered if for every some has for all . The VC dimension is the maximum number of shattered points, or if arbitrarily many points are shattered (Section 3.6, p. 80). For a set of real functions , the VC dimension is that of the indicators , (Eq. (3.22)), where the step function is for and for .
In the Lean development these are numSeparations, growthFunction, Shatters, vcDim, stepFunction and vcDimReal in the namespace NatureSLT.GrowthFunction.
Either
or there is an integer with and such that
The range is the one the book gives in both of its restatements of the theorem: the display after the Definition on p. 79 and Eq. (3.23) on p. 83.
The dichotomy is what makes the VC dimension a usable complexity measure. Combined with the bounds of Section 3.3, it gives distribution-free generalization bounds whose confidence term depends on and only (Eq. (3.24)). It also explains why finiteness of the VC dimension is a sufficient condition for consistency of empirical risk minimization for every probability measure (p. 80): the growth function, divided by , tends to zero exactly when it is not linear. Examples 1 and 2 show that the VC dimension is not the number of parameters: linear functions have as many as their parameters, while a one-parameter family of sines has infinitely many.
The theorem is classical and has been proved many times. Related statements are already machine-checked on the platform in other forms: Sauer's lemma for concept classes (ComputationalLearning.sauer_lemma, FoundationsML.RademacherVC.sauer_lemma, HighDimProb.Chaining.sauer_shelah), the bound (ComputationalLearning.phi_polynomial_bound), the 1971 dichotomy with the bound for sets of events (VapnikChervonenkis.GrowthFunction.theorem1_growth_dichotomy), and the VC dimension of open halfspaces with labels (UnderstandingML.vcDim_halfspaces). What is not on the platform is the book's statement: the logarithmic bound for the growth function of an indexed set of -valued functions, with characterized through the growth function itself, and the book's examples with the closed half-space convention . This mission produces that statement and connects it to the shattering definition.
The obvious argument proves only half. That and pin down the largest shattered set is elementary; the content lies in the bound for : a class that shatters no points must realize only polynomially many labelings of every points, with the explicit constant of the logarithmic form, and nothing in the definition of the growth function gives this directly. A tempting shortcut is to read the bound as valid for every , as the theorem's display does in isolation: this is false whenever , since exceeds . The range is essential. For the examples, the upper bound in Example 1 is a Radon-type statement about points in , and Example 2 requires controlling the sign of simultaneously for all with one parameter.
Indicator functions are boolean-valued, true standing for , and written Q α z for the book's ; samples are maps Fin ℓ → Z, so indices run from . is the cardinality of the finite set of realized vectors in Fin ℓ → Bool; the supremum over samples is a supremum of natural numbers bounded by , and is Real.log of its cast. The VC dimension is valued in ℕ∞. and are assumed nonempty in every theorem, so the supremum is over a nonempty set of samples and is at least ; the junk value never enters. At the book's expression is undefined; the formal statements evaluate it as , the limit as , and the correct bound in that case, where . The step function has . Points of are EuclideanSpace ℝ (Fin n); in Example 1(ii) the bounds of the real-function definition are , .
A trivializing formalization is ruled out: the goal is the disjunction of a linear growth function and the explicit bound with fixed by and , not an existence statement over an arbitrary and not a bound in which an empty parameter set makes the growth function vanish.
Beyond the paper. One variant is posed beside the faithful goal: a sharpness probe (growth_function_dichotomy_probe) claiming the logarithmic bound for every , i.e. without . Its evidence: for and all subsets, and . A disproof is the sought outcome.
A complete development needs: finite cardinality arguments for sets of binary vectors, the Sauer–Shelah lemma for an indexed family (Mathlib has Finset.card_shatterer_le_sum_vcDim for finite set families), the estimate , Radon's theorem or an affine-independence argument for Example 1, and elementary trigonometry for Example 2. The bridge between indexed families of indicator functions and set families is reusable by every later mission of this series. Contributions of any milestone, of bridge lemmas to the existing Sauer-type theorems, and of a disproof of the probe are welcome.
A retailer of a seasonal or perishable product must commit to a stock level before demand is known, and must also choose the price at which to sell. The two decisions interact: the price shifts the demand distribution, and the stock level determines how much of that demand can be served. The price-setting newsvendor is the single-period model of this interaction. It goes back to Whitin (1955) and Mills (1959), and it is the building block of the joint pricing and inventory literature in operations research and economics.
Petruzzi and Dada, Pricing and the Newsvendor Problem: A Review with Extensions, Operations Research 47(2), 1999 (doi:10.1287/opre.47.2.183), unify the additive and multiplicative versions of the model and give conditions under which the joint optimum is characterized analytically. Their Theorem 1 treats additive demand. Earlier results required the demand noise to be a Pólya frequency function of order 2 (Ernst 1970) or extended this to the log-normal (Young 1978). Theorem 1 replaces those assumptions by a condition on the hazard rate that every distribution with a nondecreasing hazard rate satisfies.
Demand at price is with , where , . The noise is a random variable on the range , , with probability density (nonnegative, zero off , integrating to ), distribution function and mean . The paper requires . Stocking costs per unit; each leftover unit is disposed of at cost with (a negative is a salvage value); each unit of unmet demand costs a penalty . No sign is imposed on or .
The firm stocks units, where is the stocking factor. Leftovers occur when , shortages when . The expected profit is
With expected leftovers and expected shortages , it splits as , a riskless profit less a loss function (eqs. (1)–(3)). The riskless price is . The firm solves
For each fixed the best price is (Lemma 1), so (4) reduces to maximizing over . The hazard rate is .
The Lean development lives in the namespace PetruzziDada.Additive. The definition Model carries the data with the standing assumptions above, and defines y, F, μ, Λ, Θ, expProfit (the integral above), Ψ, L, p0, price, reducedProfit (), R (its derivative), hazard and HazardCondition.
If for and , then there is with
The optimal policy is then , . The goal leaves the density arbitrary beyond the stated condition.
Theorem 1(b) is also stated, as printed, but it is not a milestone (see Difficulty).
Theorem 1 tells a practitioner when the joint stocking and pricing problem needs only its first-order condition: one root-finding problem in replaces a two-dimensional search. The hazard condition holds for every density with a nondecreasing hazard rate, such as the uniform density on , and it tolerates a hazard rate that decreases, as long as it does not decrease faster than . The result is the analytical core of much later work on joint pricing and inventory decisions.
The theorem is proved in the paper; it has not been machine-checked. Formalizing it puts the classical price-setting newsvendor on the platform: an objective defined by an integral whose limits move with the decision, a reduction by optimizing out the price, and a unimodality argument for a derivative. The definitions (the density model, , , the hazard rate) are reusable for the multiplicative case of the same paper and for other newsvendor results.
The objective is an integral with variable limits and a density that is assumed only integrable, so eq. (5) is a Leibniz rule in which pointwise continuity of cannot be used. The derivative of the reduced objective is itself differentiable only where is, and its second derivative involves . The hazard condition, however, controls the sign of only at critical points of , and turning that local information into a global shape of on a closed interval, with a density that may jump at , is a real-analysis lemma that Mathlib does not provide in this form.
Two published steps need care. The printed proof says "", but the model allows ; Theorem 1(c) still holds then, by a different argument (finding F3). Theorem 1(b) claims that is the largest root of under the hazard condition alone, and this is false as printed: when the maximum can sit at , which need not be a root (finding F1; for uniform on , , , , , no root exists). Theorem 1(c)'s extra hypothesis is exactly what excludes this.
The distribution of is given by its density , with , off , interval-integrable on and ; the bounded range is part of the model. All integrals are interval integrals. The expected profit is the integral of p. 184, not , and optimality ranges over and every real price . The hazard rate is , which Lean evaluates to where ; the hazard condition is therefore required on instead of the printed , since is undefined. At each the condition asks for a genuine derivative of relative to (one-sided at ) with , never a junk derivative. The derivative is Mathlib's deriv; the reduced objective is differentiable everywhere, which is part of a milestone. The milestones on and add continuity, respectively differentiability, of and , which the paper uses silently; the goal adds nothing. The milestone on the endpoint values states without the printed "".
These choices rule out the trivializing formalizations: an objective defined as (which would make eq. (1) definitional and Lemma 1 a quadratic identity), optimality over alone or over all real , a hazard condition read through a junk derivative (which would reduce it to ), and a goal restricted to uniform, exponential or IFR densities.
Beyond the paper. Two variants are posed beside the faithful statements. theorem_1b_corrected (corrected, finding F1) replaces the conclusion of Theorem 1(b) by " is or the largest root"; the uniform counterexample above shows the printed conclusion fails while the corrected one holds. theorem_1c_probe (sharpness probe, finding F2) is Theorem 1(c) with optimality over all real ; for the reduced objective is with , which is unbounded, so a disproof is expected and shows that the restriction to cannot be dropped.
Contributions welcome: proofs of the milestones, general lemmas on interval integrals with moving limits against an integrable density, and a reusable unimodality lemma ("a function whose critical points are all strict local maxima rises, then falls").
Many queueing, inventory and storage models are Markov chains on a two-dimensional state space : a level (a queue length, a stock level) and a phase (the state of an arrival or service environment). When customers arrive in batches, the level can jump up by several units in one step but comes down one unit at a time; when services are grouped, it is the other way round. These two families, the M/G/1-type and GI/M/1-type chains, were developed by Neuts along separate lines (Neuts 1981; Neuts 1989, references 2 and 3), and they are the embedded chains of the classical M/G/1 queue at departures and the GI/M/1 queue at arrivals.
Chapter 13 of Latouche and Ramaswami, Introduction to Matrix Analytic Methods in Stochastic Modeling (SIAM 1999, doi:10.1137/1.9780898719734), shows that both families are embedded in quasi-birth-and-death processes (QBDs), and derives from the QBD theory of the earlier chapters the two central results: the first-passage matrix of an M/G/1-type chain is the minimal nonnegative solution of , and the stationary distribution of a GI/M/1-type chain is matrix-geometric, . This mission formalizes those statements.
Fix a countable set of phases and two sequences of real matrices and . States are pairs , , ; the level is the set of states with first coordinate . Row vectors act on the left: is the row vector .
The M/G/1-type chain (skip-free to the left) has transition matrix (13.1): from it moves to with probability ; from , , it moves to with probability , . The GI/M/1-type chain (skip-free to the right) has transition matrix (13.2): from it moves to with probability and to with probability , . Both matrices are assumed stochastic: nonnegative entries, rows summing to one.
The M/G/1-type chain is embedded in a QBD (13.3) on the states : the level is and the phase is the pair , where counts the levels still to be climbed. A jump from to becomes the sequence , with probabilities (Table 13.1, blocks (13.4)–(13.7)). In this QBD,
with the first passage time from to , and is the QBD's matrix of first-passage probabilities from to .
A state is positive recurrent when its expected return time is finite, and a stationary probability vector is nonnegative, sums to one and satisfies .
For a stochastic M/G/1-type chain and every level , the matrix of (13.9) has finite entries and is the minimal nonnegative solution of
that is, it solves (13.10) and lies entrywise below every nonnegative real matrix with .
is the minimal nonnegative solution of (13.27), and, as printed, is for every the expected number of visits to before the first return to , starting from .
Theorem 13.1.4 turns a probabilistic object, the matrix of first-passage probabilities one level down, into the minimal solution of a matrix equation of the size of one level. Every numerical method for M/G/1-type chains, including the quadratically convergent algorithms of Bini and Meini, computes this solution. Theorem 13.1.5 (Ramaswami's formula) then gives the stationary distribution recursively from . Theorem 13.2.3 is the matrix-geometric property of GI/M/1-type chains, the origin of the matrix-analytic approach. Together these results cover the stationary analysis of batch-arrival and batch-service queues.
All four results are classical and proved in the book. None of them is formalized. Lean's Mathlib has no theory of first-passage matrices or of block-structured Markov chains. On Prove2Me the closest results are scalar ones: the geometric law of the G/M/1 arrival chain (QueueingFundamentals.GM1.arrival_point_geometric), the M/G/1 departure chain (QueueingFundamentals.MG1.*) and Foster-type classification of GI/M/1 chains (FosterQueues.GIM1.*). The matrix statements here contain those as the case of one phase.
The equation (13.10) follows formally from a first-step decomposition once is known to be well defined independent of the level. The hard part is the passage between the chain and its QBD embedding. A first passage of the QBD from down to splits into successive one-level passages, a strong-Markov decomposition that must here be carried out as an identity of sums over trajectories. Minimality cannot be read off the equation: it needs the comparison of with the iterates of the map started from , with every series over a possibly infinite phase set. For Theorem 13.1.5 the inverse has to be shown finite, which uses recurrence. Reading the interpretive clause of Theorem 13.2.3 literally is a trap (see below).
Everything lives in the namespace MatrixAnalytic.SkipFree. Chains are real matrices ℕ × ι → ℕ × ι → ℝ on a countable phase type ι, and nothing requires finitely many phases. The QBD embedding has phase type ℕ × ι. Levels are counted from . Stochasticity, irreducibility, positive recurrence (finite expected return time) and stationary probability vectors restate the platform definition mm_countable. Probabilities and expected numbers of visits (, , and the visits in (13.26)) are sums over finite trajectories of products of one-step transition probabilities, valued in . Products, powers and series of nonnegative matrices are also computed in . The book's is , and finiteness is a conclusion wherever the book asserts it. "Minimal" is entrywise, over nonnegative real matrices.
and are never defined as solutions of (13.10) or (13.27), nor as "the minimal nonnegative solution". That definition would make Theorems 13.1.4 and 13.2.3 true by construction. is the first-passage probability (13.9), and is existentially quantified with its probabilistic meaning stated.
Beyond the paper. Finding F1/F2: the interpretive clause of Theorem 13.2.3 names the wrong taboo set. With one phase, , , , the minimal solution of (13.27) is , but the expected number of visits to from before reaching is . The faithful item states the page and is expected to be disproved. The corrected variant gm1_matrix_geometric_corrected counts visits before the return to , which is what the proof's records.
Infrastructure needed: path-sum decompositions (first step, last exit, concatenation at a first-passage time) for countable chains, monotone iteration for matrix power series in , and censoring of a chain on a subset of states. All of these are reusable for the other chapters of this series. Proofs that go directly through the skip-free chain, without the QBD embedding, are welcome.
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.
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.
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.
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.