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?
Many combinatorial optimization problems are linear programs over a polytope with exponentially many facets, and one way to solve them by a polynomial-size linear program is to write the polytope as the projection of a higher-dimensional polytope with few facets. The minimum number of facets needed is the extension complexity of the polytope. It is now understood for most textbook polytopes: flows, matchings (Rothvoß 2017), arborescences, travelling-salesman tours and stable sets (Fiorini et al. 2015). Matroids are a notable exception.
For a matroid , the independence polytope is the convex hull of the characteristic vectors of the independent sets. Rothvoß showed by a counting argument that many matroids have independence polytopes of exponential extension complexity (Math. Program. 2013), so a polynomial bound can only hold for special classes. Regular matroids, those representable over every field, are the natural class: they contain the graphic and cographic matroids, and Seymour's decomposition theorem describes all of them.
Timeline:
A matroid has a finite ground set and a family of independent sets; . For , is its characteristic vector, and
An extended formulation of a set of size is a system , with exactly inequalities such that if and only if some satisfies the system. The extension complexity is the least such . The paper defines as the minimum number of facets of a polytope projecting onto , and on p. 1 it gives the extended-formulation form as an equivalent definition.
A matroid is regular if it is represented over by a totally unimodular matrix : a set is independent exactly when the corresponding columns of are linearly independent. It is binary if it is represented over . It is graphic if it is the cycle matroid of a multigraph (independent sets are forests) and cographic if its dual is graphic. A cycle is a disjoint union of circuits. For binary , the sum has ground set , and its cycles are the sets , with a cycle of , that lie in that ground set. This sum is a 1-, 2- or 3-sum when the two ground sets share zero, one or three elements, under the side conditions of p. 3. In the 3-sum case the shared set is a triangle, a 3-element circuit of both parts. A matroid is 3-connected if it is neither a 1-sum nor a 2-sum.
The constant is not fixed; the exponent is the paper's. Section 8 of the paper sketches an improvement to without proof, so the goal keeps the proved exponent.
The result. Theorem 1 shows that linear optimization over the independent sets of any regular matroid is a linear program of size polynomial in , written down without any algorithm. Regular matroids are the largest classical matroid class for which such a bound was in question, and the bound separates them from general binary matroids. The proof also gives an extended formulation for the circuit dominant of a regular matroid, a separate result that this mission does not include.
Formalizing it. The theorem is proved on paper and has no machine-checked proof. Formalizing it needs a Lean theory of matroid sums (1-, 2- and 3-sums defined through cycle spaces), decompositions of regular matroids along trees, and extended formulations, with explicit bounds on how the size of an extended formulation behaves under products, intersections with hyperplanes and convex hulls of unions. Seymour's decomposition theorem enters only through Theorem 6, which can be taken as a black box while the polyhedral part is formalized.
The obvious induction fails at 3-sums. For 1- and 2-sums, the extension complexities of the parts add (Lemma 3), and an induction gives a polynomial bound. For a 3-sum, the best known symmetric formulation for has size with (p. 4). A constant larger than 1 compounded over a decomposition tree of logarithmic depth only gives a quasi-polynomial bound, and over an unbalanced tree an exponential one. So the parts of a 3-sum have to be treated differently, and the decomposition tree has to be rebalanced into a star whose leaves have at most about half the elements.
The cographic centre is a second obstacle: the formulation of the centre's part is known only when every triangle shared with a leaf is the set of edges at a degree-3 node of the underlying graph, and getting there requires the decomposition tree of Proposition 27.
Matroid α over one ambient type ; the parts of a sum share elements of (the triangle elements) that are not in . Statements that construct decompositions (Theorem 6, Proposition 27, Lemma 4) take infinite, so that fresh elements exist; otherwise "not a 2-sum" could hold for want of room.IsEFOfSize and extensionComplexity (size = number of inequalities, equations free). Every upper bound is the existence of an extended formulation of the stated size, and bounds in terms of the parts quantify over extended formulations of the parts. This rules out the trivializing reading with an infimum that is on sets with no extended formulation.Creditors can observe a firm's liabilities while learning its asset value only after a delay. In the model of Benzoni, Garlappi, and Goldstein, this gap matters when the firm has exhausted its ability to issue more debt: creditors know that the firm has stayed above its default boundary, but do not know how close it is to that boundary now. Even though asset value moves continuously, the creditors' next observation can reveal that default has already occurred. The resulting jump-to-default intensity is an instantaneous default rate based on the creditors' delayed information. It enters the paper's analysis of bond values and the term structure of credit spreads.
The held source is the Federal Reserve Bank of Chicago's 2019 working paper, Asymmetric Information, Dynamic Debt Issuance, and the Term Structure of Credit Spreads. The journal article appeared in 2023 under the title used in this mission's name. Page and equation numbers below refer to the working paper, whose numbering has not been reconciled with the journal version.
Let be the firm's log distance to default at time : default occurs when this value first reaches zero. Under the risk-neutral measure, the paper models its motion after the firm exhausts debt capacity as . Here is drift, is volatility, and is standard Brownian motion. The creditors observe the lagged value , where the information lag is positive. In Regime 4, , and the creditors also know that default has not occurred by . Thus on the conditioning event. The regime is described in §3.3.1 and equations (22)–(27) of the working paper.
Write for the standard normal cumulative distribution function. For an initial distance and a horizon , is the probability of staying above zero throughout that horizon. The paper gives
It sets for . The killed transition density is the difference of a Gaussian transition density from and an image term from , multiplied by the indicators of and . Its exact normalization and image coefficient are those of equations (D.2)–(D.3) in Lemma 1 of the Online Appendix. The conditional density of the unobserved current value , given and survival, is .
For a short future horizon , the conditional default probability from state is . The quotient
is the last line of the intensity definition (D.19). The Regime 4 intensity is its limit as decreases to zero. It depends on the lagged distance , rather than on calendar time separately.
The goal is Corollary 1, equation (32), on printed p. 16 of the working paper. For , it identifies the right limit of , the boundary derivative of , and a closed form:
The right derivative is used because the density vanishes for and can have a nonzero derivative from positive values. The paper writes an additional indicator in (32); the target states its meaningful branch , where the conditional density exists. The milestones follow the Appendix's sequence: Lemma 1 normalizes the killed density; (D.20) gives the small-horizon default limit close to the boundary; the boundary value used in (D.22) vanishes; (D.24) fixes a Gaussian tail integral; (D.25) identifies the intensity with the boundary derivative; and the final differentiation supplies the closed form. These are statements of the Online Appendix, pp. 11–19, not separate economic assumptions.
Equation (32) gives a default rate computable from a lagged observable and model parameters. It connects the paper's structural default boundary to an intensity seen by creditors who lack the current asset value. This provides a quantitative ingredient for the paper's Regime 4 debt valuation and credit spread comparisons. Its time independence in that regime follows from the fixed lag and stationary transition law; earlier regimes have a different information set and are outside this mission.
The paper proves the formula informally in the Online Appendix. The present mission asks for machine-checked proofs of the stated identities and limits. The published normal CDF definition is available on Prove2Me, while the killed-density normalization and the hazard limit remain theorem targets here. A complete development would also provide reusable analytic results about Gaussian tails, image densities, boundary derivatives, and integration on a half-line. No theorem in this proposal is claimed as already machine-checked.
For each fixed , the chance of crossing zero during a very short interval tends to zero. Taking that pointwise limit inside would miss the intensity: values of that shrink with still contribute after division by . The paper's passage from its conditional density and short-horizon survival formula to (D.25) is the substantive limit claim. A proof must also justify that is strictly positive, so the conditional density and the displayed denominator are meaningful, and must distinguish the right derivative at zero from a two-sided derivative.
Lean uses real parameters with , , and ; the drift has no sign restriction. The positivity conditions make every square root and division in the conditional density meaningful. The horizon approaches zero through positive reals. Integrals are Lebesgue integrals over with respect to the standard measure, matching the paper's . The standard normal CDF is imported from the published BlackScholesModel_Core definition.
The Brownian layer is represented by its explicit killed Gaussian density and survival law, which the paper takes from Harrison's first-passage result. A process-level Brownian motion, stopping time, and conditional probability construction are outside this mission. These laws are fixed formulas in the model definition; the paper's derived normalization, intensity limit, and closed form remain theorem statements. In particular, the intensity is the right limit of , and is computed from the explicit killed density and survival probability. Defining intensity as or taking as an arbitrary density would erase the goal. Contributions establishing the analytic limit, positivity, integral, and differentiation milestones are all in scope.
Classical sample-size calculations for a clinical trial fix a significance level and a power and solve for the number of patients. They do not ask what the trial is for. A value-based design asks instead: given what it costs to recruit patients and what a better adoption decision is worth to the patients treated after the trial, how long should the trial run and how fast should it recruit? Health technology assessment bodies such as NICE already decide adoption on cost-effectiveness grounds, and Bayesian decision-theoretic trial design goes back to the value-of-information literature of the 1990s and 2000s (Claxton & Posnett 1996; Chick, Forster & Pertile 2017).
Alban, Chick and Forster (Management Science 2023) make the two decisions explicit, recruitment duration and recruitment rate , and let the regulatory context decide the population that benefits after the trial. Their asymptotic result, Proposition 5, says that the optimal number of patient pairs grows as the square root of that population, and that the optimal expected net gain per post-trial patient converges to a value that does not depend on the switching costs.
A new technology N is compared with a standard S. A fraction of patients is on N before the trial. Patients are randomised in pairs; recruiting at rate for a time yields pairs. The incremental net monetary benefit of N over S has prior , each pair gives an observation , and . After pairs the posterior mean has predictive law with .
After the trial the decision maker adopts N, adopts S, or keeps the current mix, paying fixed switching costs . Without discounting, the expected net gain of a design with is
where is the cost per patient, the setup cost of recruitment capacity, and switches on rewards to trial patients. Without a trial, . The post-adoption population is either a fixed pool, , or set by a fixed horizon, , with incidence and observation delay . The paper also treats discounting at rate ; the asymptotic results take .
Problem (5) maximises over , where Table EC.1 takes and . With and , the paper distinguishes four cases: I (, fixed pool), II (, fixed horizon), III (, fixed pool), IV (, fixed horizon).
Write , for the standard normal density, for the standard normal linear loss, and
Assume and . For every selection of optimal designs, with :
with (Case I) or (Case IV). In Case II the denominator is , and in Case III (corrected, see below) it is . The goal also asserts that optimal designs exist once the population is large.
The closed form (8) of through ; existence of an optimal design (Proposition 1); the reductions to one decision variable (Propositions 2–4); and the four case lemmas EC.1–EC.4 of Appendix C.4, which together give Proposition 5. Lemma EC.4 adds the finer statement that in Case IV both and grow like .
The result turns an optimisation without a closed-form solution into a rule of thumb: for a large population, the optimal trial enrols about patients. The authors show in their ProFHER application that the approximation is accurate at realistic sizes. It also explains two qualitative facts, that fixed-pool and fixed-horizon contexts reach the same value per patient, and that switching costs become irrelevant at scale.
The paper proves these results with asymptotic arguments that are sketched in places ("by rearranging and some additional asymptotic approximations"). A formal proof makes every limit exchange explicit. The formalization also corrects a misprint: the Case III constant in Proposition 5 and the constant in (EC.4) are printed without the setup-cost term , and the proof's own optimality condition shows that it belongs there. None of these results has been machine-checked before; the platform has the normal linear loss and nothing on clinical-trial design.
The objective is not concave in , has a jump where the trial stops running, and its optimiser has no closed form. The square-root law concerns an arbitrary optimiser as the population grows. So it is not enough to differentiate an asymptotic approximation of and solve the first-order condition. One must show that every optimiser escapes every bounded set, that the exact first-order condition holds there, and that the error terms of and of the indifference points and vanish at the right rates. In Case IV two decision variables diverge at different rates, and the fixed horizon couples the trial length to the post-trial population.
All quantities are real. A design is a pair . The post-adoption term of is a Bochner integral against gaussianReal µ0 σZ², and is the published InventoryControl.normalLoss. is defined by the expectation (7) and (9), never by the closed form (8), which is a milestone. Optimality is IsOptOn f S x: and on .
Decision sets follow §3.6.1: in Cases I and II, with ; in Case III, with ; in Case IV, both are free. Under a fixed horizon, is added, because beyond it , outside the model (§2.4.1 requires ). The finite box statements use , , and a fixed pool has , as in Table EC.1. Other added hypotheses: the standing sign conditions of §2 and Table EC.1 (; ; ; ), (used in the proof of Proposition 1), and .
Limits are asserted for every selection of optimisers. A separate conjunct asserts that optimisers exist for large populations, so the statement cannot be satisfied vacuously by an empty set of optimisers. It is not about a stationary point of an approximation, and is never replaced by a formula.
Two printed slips are corrected and labelled. In Proposition 5, Case III has constant , and (EC.4) has the factor in its denominator. Both follow from the cost of pairs at fixed , which is ; at the corrected constant matches a numerical optimum to four digits, the printed one does not. The branch of Lemma EC.4, Proposition 6 (discounting) and the comparative statics of §3.5 are not formalized.
A complete development needs Gaussian expectations of piecewise-linear functions, semicontinuity arguments on a box with a jump, and asymptotic analysis of argmax sets. The Gaussian-loss identities are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the case lemmas.
The monotone complementarity problem (MCP) asks, for a continuous monotone map on the positive orthant, for a pair with , , and for every . It contains linear programming, convex quadratic programming, the monotone linear complementarity problem and the Karush–Kuhn–Tucker conditions of smooth convex programs. Interior-point methods solve it in polynomially many Newton-type steps when a strictly positive, well-centered starting point is known, but in general no such point is known, and the problem may be infeasible or feasible without any positive feasible point.
Andersen and Ye (Mathematical Programming 84, 1999) extended the homogeneous self-dual embedding of linear programming to the nonlinear MCP: one embeds the problem into a homogeneous problem that always has a trivial interior starting point, solves it by a path-following method, and reads off either a solution or a certificate of infeasibility. Section 8.4 of Ye, Interior Point Algorithms: Theory and Analysis (Wiley 1997, doi:10.1002/9781118032701) presents this construction, the convexity property of the residual set it rests on, and the analysis of one step of the algorithm. This mission formalizes that section.
Vectors are compared componentwise; is the all-ones vector, , , the Euclidean norm and the open orthant. A map is monotone if for all ; denotes its Jacobian.
The residual set is , and for the slice .
The homogeneous map on , with points written , is
The homogeneous model (HMCP) asks for with minimizing .
A map on is scaled Lipschitz with a monotone increasing if
The algorithm works in with and . At an iterate let and . The direction solves
and for a step size the new iterate is and .
Assume is scaled Lipschitz with , and let
If and , then and
The goal remains true when is only assumed differentiable on and scaled Lipschitz; this variant is posed beside the goal (see Formalization scope).
Theorem 8.29 is the one-step invariant behind the iteration bound of the homogeneous algorithm: combined with Lemma 8.28 it shows that the infeasibility residual and the complementarity gap shrink by the same factor per step while the iterates stay in a fixed neighborhood of the central path. Together with Theorem 8.25 (v)–(vi), which identifies solutions and infeasibility certificates of the MCP from maximal complementary solutions of the homogeneous model, this yields an algorithm that needs no feasible starting point and detects infeasibility. The convexity of (Theorem 8.23) is the structural fact that makes the homotopy path of the homogeneous model well defined.
These results are proved in the book (with Theorem 8.19, which Theorem 8.23 uses, left as an exercise). None of them is formalized on the platform: the existing Andersen–Ye material covers only the linear complementarity case, as a set-valued operator, and no statement about scaled Lipschitz maps or the nonlinear homogeneous map exists. A completed development gives a machine-checked analysis of an interior-point step for a nonlinear problem, with every constant explicit.
The algebra of Lemmas 8.27 and 8.28 depends on the identities and , which require differentiating a map defined through ; working with as a Fréchet derivative rather than a hand-written block matrix is part of the work. In Theorem 8.29 the nonlinearity enters only through the scaled Lipschitz bound, which applies only when , so the step must first be shown to stay well inside the orthant before the neighborhood estimate can be closed; the norms involved (, , and the scaled norms , ) must be chained in the right order. Theorem 8.23 is of a different kind: its proof passes through the homeomorphism of Theorem 8.19, whose proof the book leaves as an exercise, and a compactness argument along a homotopy.
Two points in the printed text need care. The block matrix (8.24) displayed for has a spurious transpose in its lower-left block; with the printed matrix Lemma 8.24 would fail for nonsymmetric , and the statements here use the true Jacobian. The printed proof of Theorem 8.25 (iii) (the scaled Lipschitz constant of from that of ) establishes the bound with , not the stated , and only for ; that part is not in this mission, and Theorem 8.29 assumes the scaled Lipschitz property of directly, as the book does.
Vectors are Fin N → ℝ, a point of is z : Fin (n+1) → ℝ with Fin.init z and z (Fin.last n) , and every Jacobian is Mathlib's fderiv. The standing assumptions of §8.4 are explicit hypotheses of every theorem: continuous and monotone on the open orthant , and differentiable there wherever or appears (the section assumes this silently). In the scaled Lipschitz condition, "monotone increasing" is read as nondecreasing on and ranges over . The direction is any solution of (8.42)–(8.43). The new dual iterate is defined by the first line of (8.47); its closed form is a conclusion. The book writes no in the statements of this mission: , , and are the book's explicit constants. is a total function in Lean (division by returns ), but every statement evaluates it and its derivative only at .
A trivializing formalization is excluded: the scaled Lipschitz hypothesis is not vacuous (it holds, for instance, for with any admissible ), the direction is not assumed to have any property beyond (8.42)–(8.43), and the monotonicity of and the identities (8.41) are proved milestones, not hypotheses of the goal.
Beyond the paper. One variant is posed: central_step_strong (strengthened) drops the continuity and monotonicity of from Theorem 8.29, because the scaled Lipschitz condition already forces , the only use the proof makes of monotonicity.
The development needs Fréchet derivatives of compositions with , finite-dimensional norm inequalities, and, for Theorem 8.23, invariance of domain or a direct proof of Theorem 8.19. The definitions (monotone maps on the orthant, the scaled Lipschitz condition, the homogeneous map) are reusable for the remaining parts of Theorems 8.25 and 8.26. Contributions of a proof of Theorem 8.19, and of the faithful Theorem 8.25 (iii), are welcome.
Primal-dual interior-point methods for linear programming come with two kinds of guarantee. The worst-case one is a bound of iterations to reduce the duality gap below . The asymptotic one says what happens to the duality gap near the end of the run, where practical codes spend their final iterations. For the predictor-corrector method of Mizuno, Todd and Ye (1993), Ye, Güler, Tapia and Zhang (1993) showed that the same algorithm that achieves the best known worst-case bound also drives the duality gap to zero quadratically. The proof needs neither nondegeneracy nor convergence of the iterates. Chapter 7 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley 1997, DOI 10.1002/9781118032701) gives a self-contained account. This mission formalizes its LP core.
Timeline, as attributed in the chapter's notes (§7.5): Zhang, Tapia and Dennis first obtained superlinear convergence of a primal-dual method assuming the iterates converge, and quadratic convergence assuming nondegeneracy. Quadratic convergence for general LP, with neither assumption, was first established by Ye, Güler, Tapia and Zhang, and independently by Mehrotra and by Tsuchiya. The monotone LCP version (§7.3) is due to Ye and Anstreicher, who also showed that the predictor step cannot converge superlinearly when no strictly complementary solution exists (Proposition 7.13). Monteiro and Wright extended that negative result to Newton-like methods in general.
Fix a real matrix of rank , and . Consider the standard-form pair
An interior point is a triple with , , , . Write , , for the all-ones vector and . The neighbourhood of the central path is
The strict complementarity partition collects the indices on which some optimal is positive () and those on which some optimal slack is positive (). The predictor direction at is the solution of
It is the case of the direction defined by , , . The scaling is , and denotes the Euclidean norm of the subvector of indexed by . Algorithm 4.5 (predictor-corrector, ) starts in . At each iteration it takes the largest step along that keeps the iterate in , then a full step along back towards the central path.
The order of convergence of a sequence (Definition 1.1) is the supremum of the with . Quadratic convergence (Definition 1.2) means .
For every there is a constant , depending only on and , such that at every with the predictor direction satisfies
The goal fixes no value of : it asserts only that one constant serves every point, which is the content the later results use.
Theorem 7.5, together with Lemma 7.3, says the whole predictor direction is . Through the step-size bound of Lemma 4.17 this gives and hence : quadratic convergence of the duality gap (Theorem 7.6). The same least-squares structure yields the LCP version (Theorem 7.12) and the variants of §7.4. Bounds of this kind on the directions near the optimal face also underlie finite termination and basis identification schemes.
On the formal side, no machine-checked development of interior-point asymptotics is known to the authors of this mission. Mathlib has the linear algebra (ranges, block matrices, least squares through orthogonal projection) but no linear-programming duality theory beyond what other missions supply. A formal proof would supply the Goldman–Tucker partition, the uniform bounds (7.6) and a Hoffman-type bound for least-squares solutions in reusable form.
Everything rests on a constant being uniform. For a single interior point, any bound holds with some depending on the point, so the content is entirely in choosing before the point. The natural first attempt bounds the direction through and on all indices, and this fails: on the entries grow like , and on they shrink like . Only the split along the optimal partition, with the least-squares characterization of the "large" components and the uniform bounds (7.6), balances the two. Relation (7.6) itself requires the partition to be strict (Goldman–Tucker) and an a priori bound on the iterates. For Theorem 7.6 the algorithm's step-size rule has to be carried as defined: a largest step over an interval of neighbourhood memberships.
Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ. All norms are Euclidean. and are defined as unions of supports of optimal solutions; that they partition the indices is a consequence solvers must prove, not an assumption. The standing assumption appears as a hypothesis.
Instantiations of the book's (p. 213: "may depend on and/or the original problem data, but … independent of the iteration "):
A constant chosen after the point would make the goal trivially true; the statements quantify first to rule this out. Algorithm 4.5 is run for every (no termination test), and its step is the greatest admissible , not a supremum. The order of convergence and all limits superior take values in EReal, so infinite values are not collapsed to junk reals. Lemma 7.4's second problem is stated as corrected (the printed objective is ill-typed and the sign of is inconsistent with (7.4)); see the findings.
Beyond the paper. One strengthened variant: Theorem 7.5 on for every and without the rank condition. The book's proof uses the neighbourhood only through , and the rank of enters nowhere.
Needed infrastructure: LP duality and strict complementarity (Goldman–Tucker), a Hoffman-type bound for minimum-norm solutions, and weighted least squares. The definitions of the neighbourhood, the direction and Algorithm 4.5 are shared with the chapter 4 analysis and are reusable for other interior-point results. Contributions proving any milestone independently are welcome.
Worst-case analysis of interior-point methods gives iteration bounds of order or , while practical codes finish in a number of iterations that barely grows with the problem size. Chapter 6 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley 1997, doi:10.1002/9781118032701) addresses the gap probabilistically. Its rigorous half (§6.2) takes the simplest nontrivial problem, the homogeneous linear feasibility problem with a random Gaussian matrix, and shows that it is solved in iterations with high probability, then extends this to random linear programs through the homogeneous self-dual model.
That analysis rests on a geometric fact about random cones: the probability that random vectors lie in a common open half-space through the origin. The answer is Wendel's formula (J. G. Wendel, A problem in geometric probability, Math. Scand. 11 (1962), 109–111); Ye restates it as Corollaries 6.11–6.12 and draws from it Theorem 6.13: with probability one a random homogeneous system is strictly feasible on exactly one side of its theorem of the alternative. Strict feasibility is what makes the condition number of the problem finite, which is what an interior-point termination procedure needs.
Let be a real matrix with columns ; vector inequalities are componentwise and is the all-ones vector. The homogeneous system (6.5) is
and its alternative (6.11) is the system , in . An interior feasible point of (6.5) is an with and ; of (6.11), a with .
In the standard Gaussian model (§6.2.2) the entries of are independent random variables. With the book defines
and is the same sum with replaced by .
A partition chooses columns for the matrix and leaves the other in . System (6.12) asks for with
For the one-step analysis of §6.1, is an orthogonal matrix with first column , and is uniformly distributed on the unit sphere of .
The Lean development lives in the namespace YeIPA.Random: the module YeIPA.Random.Setting defines IsFeasible65, IsInterior65, IsFeasible611, IsInterior611, IsFeasible612, gaussianMatrix, pnd and uniformSphere.
For , and standard Gaussian ,
Theorem 6.13 is the input to the chapter's main results: Theorem 6.15 (a feasible point of a random system satisfies the scaling condition (6.9) with high probability) and the iteration bounds of Theorems 6.16 and 6.23 for random feasibility and random LP problems. It turns a deterministic theorem of the alternative, which allows degenerate configurations, into a statement that such configurations have probability zero. Corollaries 6.11–6.12 are Wendel's formula in the form used for linear programming, and also give the exact probability that a random homogeneous system is feasible, a quantity that recurs in the analysis of random linear programs and of perceptron capacity. Lemma 6.5 is the concentration estimate behind the one-step analysis of predictor steps in §6.1.
None of these results is formalized on Prove2Me or, as far as a search shows, in Mathlib. Wendel's formula has no machine-checked proof that this mission could reference; the platform's PoissonDirichlet.Wendel.* items concern an unrelated identity. A complete development adds Gaussian random matrices, conic theorems of the alternative and an exact geometric probability to the platform.
The book cites Wendel's formula ("It is shown that …") and leaves its proof as Exercise 6.3, so Corollaries 6.11–6.12 must be proved from scratch. The natural first idea, conditioning on the column space or on a single column and integrating, does not close: the count of half-spaces is combinatorial, not an integral that evaluates in closed form. The probability-one statements need general position of Gaussian columns, which is the property that rules out the degenerate cases of the theorem of the alternative. Corollary 6.12 is not a consequence of Corollary 6.11 alone: the gap between "feasible" and "strictly feasible" is an event that must be shown to be null, and the book's own argument passes through the dual system and the identity for , which is itself part of what must be proved. Lemma 6.5 is a uniform statement over all orthogonal completions of , with an explicit threshold rather than an unspecified constant.
Vectors are functions on Fin n (indices ), matrices are Matrix (Fin m) (Fin n) ℝ, and the Gaussian model is the product measure Measure.pi of gaussianReal 0 1 over the entries, a sample being read as Matrix.of A. Probabilities are values of this measure in , compared with through ENNReal.ofReal. "With probability one" in Theorem 6.13 is an almost-everywhere statement for that explicit measure; the failure set is null. The section's standing assumption that has full row rank (p. 187) is carried as in the probabilistic statements, under which a Gaussian has rank almost surely, and as in Lemma 6.14. Every probabilistic statement assumes ; for both systems are empty and is undefined. In Lemma 6.14 a partition is an injection from into the columns; the variable is the last coordinate of a vector on Fin (m+1). In Lemma 6.5 the sequence is indexed by , the matrices are arbitrary with , deletes the first column, the uniform law is Lebesgue surface measure on the sphere normalized to mass one, is natural, and is written coordinatewise. No result of this chapter uses an bound in the stated items, so there are no constants to instantiate; Lemma 6.5's threshold is the book's own.
A trivializing formalization is ruled out: the probabilities are those of the explicit product Gaussian measure (not an arbitrary measure, nor "for almost every " against an unspecified measure), interior points are required to be strictly positive in every coordinate, and Theorem 6.13 asserts both the emptiness of one system and an interior point of the other.
Beyond the paper. One variant is posed. YeIPA.Random.lemma_6_14_corrected (corrected, finding F1) adds to Lemma 6.14: as printed the lemma fails for , where is empty and solves (6.12) for every , e.g. . The faithful Lemma 6.14 stays the milestone.
Infrastructure that a complete development needs and that is reusable beyond this mission: general position of Gaussian matrices (every minor nonzero almost surely), Gordan's theorem of the alternative for , Wendel's formula, and tail bounds for coordinates of a uniform point on the sphere. Proofs of any milestone, and of these supporting facts as separate lemmas, are welcome.
Interior-point methods for linear programming do not move along the boundary of the feasible region; they follow a curve of points that stay "central". The basic notion of centrality is the analytic center of a polytope, the interior point that maximizes the product of the slacks of its defining inequalities (Sonnevend, 1986, doi:10.1007/BFb0043914). Every path-following and potential-reduction algorithm repeatedly computes an approximate analytic center, so it matters how "approximately centered" is measured and what one Newton step does to that measure.
Chapter 3 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley, 1997, doi:10.1002/9781118032701) answers both questions for a polytope given by linear inequalities. It introduces three measures of proximity to the analytic center (dual, primal and primal-dual), proves that they are equivalent, and shows that the corresponding Newton steps square them. The same estimates reappear, with minor changes, in the complexity analysis of Karmarkar's algorithm and of the primal-dual potential-reduction methods of the later chapters. This mission formalizes those statements.
Let be a real matrix and . Vector inequalities are componentwise, is the all-ones vector, , , and is the Euclidean norm. The chapter works under standing assumptions: has rank , , and the polytope
is bounded with nonempty interior. An interior point of has . The homogeneous primal set is ; its interior points have , .
Three potential functions are used:
The analytic center is the interior point of maximizing , and the primal potential minimizer is the interior point of with minimizing .
The three proximity measures are
The dual Newton step is ; the primal Newton step is ; the primal-dual Newton directions solve , , , and are taken with step size for a constant .
For an interior point of , an interior point of , the analytic center and the primal minimizer :
Theorem 3.2 is what makes an "approximate analytic center" a well-defined notion: whichever of the three measures an algorithm controls, the other two and the potential gaps follow. Parts 3 and 4 convert a small residual into a bound on the logarithmic-volume gap and on the relative distance to the true center. These are the quantities used to start the Newton procedures of Theorem 3.3 and Corollary 3.8, and to bound the number of central-section and potential-reduction steps elsewhere in the book. Lemma 3.12 and Theorem 3.13 are the per-step estimate of the primal-dual potential-reduction method, the template for the linear-programming algorithms of Chapter 4.
None of these statements is formalized on Prove2Me. The platform has self-concordant Newton analysis (ConvexOptimization.newton_quadratic_phase_contraction) and proximity measures for self-scaled cones (SelfScaledIPM.FuncProx.*, open), but neither works with Ye's measures or steps. The results are classical and proved in the book. Formalizing them yields a reusable linear-algebraic layer (projections , scaled least squares, the primal-dual Newton system) for any later interior-point mission. It also checks hypotheses the book leaves implicit: Lemma 3.12 is false without the normalization that §3.4.2 states only once.
Most of the chapter's arguments are short on paper but depend on facts that are only described in words. In (i), and are the optimal values of weighted least-squares problems, and the domination needs that variational characterization, which goes through the invertibility of and (rank ). Part 4 is not a one-step estimate: it is obtained by running the Newton procedures of Theorem 3.3 and Corollary 3.8 indefinitely, summing a geometric series of quadratically shrinking corrections, and identifying the limit with the analytic center. That identification requires uniqueness of the center (strict concavity on a bounded polytope) and the correspondence between and through . Part 3 needs that correspondence as well. The positivity of the damped iterates in Lemma 3.12, which the book asserts "can be verified", has to be established before any logarithm is evaluated. Theorem 3.13 requires constants independent of , which rules out every argument that loses a dimension factor.
Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ; indices are -based. The Euclidean norm is written out as norm2, since Mathlib's norm on Fin n → ℝ is the sup norm. Matrix inverses are Mathlib's ⁻¹, which is on singular matrices. The rank hypothesis makes every inverted matrix positive definite at the points where the theorems use it, so the junk value is never reached. The standing assumptions (rank , , bounded with nonempty interior) are bundled as StandingAssumptions A c and are a hypothesis of every theorem. The normalization of §3.4.2 is a hypothesis of Lemma 3.12 and Theorem 3.13. The analytic center and the primal minimizer are defined by their extremal properties, not by the optimality system , so the goal cannot be obtained by unfolding a definition. The theorems are stated for the steps exactly as the book defines them, never for an arbitrary "good" step.
Explicit constants: no result in this mission uses . Theorem 3.13's constants are existential in the book ("we can choose … for a positive constant "). They are stated as quantified before , , and , which is what the proof establishes. A formalization in which or depends on the instance would be trivial and is ruled out by this quantifier order.
Beyond the paper. One variant is posed: a sharpness probe of Lemma 3.12 with the normalization removed (findings F1, F3). With , , , , the step only rescales , so the potential is unchanged while the claimed bound is about . A disproof is the expected outcome.
Not in scope: Theorem 3.11 (the primal-dual Newton step), whose positivity claim fails as printed (finding F2); the iteration-count theorems 3.4, 3.7, 3.9, stated with ; the central-section Lemmas 3.5–3.6; and Theorem 3.10 (affine scaling). Contributions welcome: the least-squares characterization of , as reusable lemmas, and the uniqueness of the analytic center.
Primal-dual interior-point methods for linear programming generate strictly positive iterates that approach the solution set but never reach it: the duality measure tends to zero, yet no iterate is ever an exact solution. Many applications need more than an approximate point — an exact optimal basis, a vertex, or the optimal partition of the variables into those that are positive and those that vanish at optimality. Chapter 7 of Stephen J. Wright's Primal-Dual Interior-Point Methods (SIAM 1997) studies the end game of these methods: how fast decreases once the iterates are close to the solution set, and how to jump from an interior iterate to an exact solution.
The finite termination procedure formalized here is due to Ye (Math. Programming 1992): guess the optimal partition from the current iterate and project onto the face of the feasible set it determines. The superlinear analysis of the affine-scaling step goes back to Ye, Güler, Tapia and Zhang (Math. Programming 1993); its key uniform bound on weighted least-squares solutions was proved independently by Stewart (Linear Algebra Appl. 1989) and Todd (Oper. Res. 1990). The bound on solutions of linear systems used throughout is Hoffman's (J. Res. Nat. Bur. Standards 1952).
Fix , , , with no assumption on the rank of . The primal problem is subject to , ; the dual is subject to , . Let and be their sets of optimal solutions and . The optimal partition is
A strictly complementary solution is with for and for . The quantity
measures how far the solution set reaches into each coordinate, and .
The strictly feasible set consists of triples with , , , . The duality measure is . The wide neighborhood is for , and the 2-norm neighborhood is , where is the vector of products and is Euclidean.
The affine-scaling direction at is any solution of
The partition estimate at is , , and the projection problem of Ye's procedure is
For there is a threshold such that every with
satisfies (i) and , and (ii) the projection problem has a solution, and every solution is a strictly complementary solution. The threshold is existential, as printed; the goal does not fix its value.
Theorem 7.12 turns any path-following method into a finite algorithm: once falls below , one linear least-squares problem, costing about one interior-point iteration, returns an exact strictly complementary solution, and with it the optimal partition. For integer data the threshold is bounded below by , which is how interior-point methods are made to terminate exactly within their polynomial iteration bounds (Chapter 3 of the book). Theorem 7.4 and Lemma 7.6 give the competing route — the affine-scaling step is , so predictor steps approach full length and the predictor-corrector method converges two-step quadratically.
None of these results is formalized on the platform. Hoffman's error bound exists there for a single consistent system with a constant chosen after the right-hand side; Lemma A.3 and its variant need one constant for all right-hand sides. The optimal partition, , the uniform weighted least-squares bound and the projection step are reusable for any formal treatment of interior-point methods, degenerate linear programs or error bounds.
Near a degenerate solution set the linear systems defining the affine-scaling step become arbitrarily ill-conditioned: the diagonal scaling has entries tending to and to , and the coefficient matrix has no nonsingular limit unless the solution is unique. Any bound that passes through the conditioning of that matrix degrades as ; the constants of Theorem 7.4 and Lemma 7.2 must be independent of the scaling. For Theorem 7.12 the difficulty is uniformity in the other direction: the threshold must be one number for the whole neighborhood, which needs a bound on the distance from an iterate to a face of the feasible set that does not depend on the iterate.
Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, points are triples (x, lam, s); the Euclidean norm is defined explicitly (Mathlib's default on Fin n → ℝ is the sup norm). Directions and the projection problem are defined by their equations and optimality, never by closed-form formulas. uses real suprema, which agree with the book's whenever ; every theorem is vacuous otherwise. No rank assumption on is made except in Lemma A.4, where the page states it. is not a hypothesis: membership in a neighborhood implies it.
Explicit constants: the book writes "there is a constant" in Lemmas 5.13 and 7.1; their proofs give (5.32) and (7.6), which are used. The constants , , , , have no closed form in the book (they come from Lemma 2.5, Hoffman's lemma and Lemma 7.2) and stay existential, but each is quantified before the point, the right-hand side or the scaling it must work for; a constant chosen after the point would make Theorem 7.4 trivial. A trivializing form of the goal — a threshold allowed to be , or a conclusion about some minimizer chosen by the solver — is ruled out by requiring , existence of a minimizer, and strict complementarity of every minimizer ( is not unique). In Lemma 7.6 the largest step is a hypothesis (IsGreatest), and the statement also asserts that the whole interval is admissible.
Beyond the paper: one variant is posed. lemma_A_3_strong (strengthened, finding F1) is Lemma A.3 for every consistent system , instead of ; this is Hoffman's 1952 theorem. Finding F2 records that the printed proof of Theorem 7.4 covers only full-row-rank ; the statement is kept as printed.
Needed infrastructure: LP optimal solution sets and the optimal partition, matrix inverses and ranks, finite sums. A uniform Hoffman bound and the Stewart–Todd bound are reusable well beyond this mission; contributions of either are welcome.
Primal-dual interior-point methods solve a linear program by following the central path from a point with strictly positive primal variables and dual slacks . The classical analysis assumes that the starting point is feasible: it already satisfies the equality constraints and . In practice such a point is rarely available, and the production codes of the early 1990s (OB1, and later the solvers built on Mehrotra's method) instead start from an arbitrary positive point and let the Newton steps reduce the constraint violation together with the duality gap. These infeasible-interior-point methods worked well long before they were understood. Global convergence was first proved by Kojima, Megiddo and Mizuno (Math. Programming 61, 1993), and polynomial complexity of a long-step variant by Zhang (SIAM J. Optim. 4, 1994).
Chapter 6 of Stephen J. Wright's Primal-Dual Interior-Point Methods (SIAM 1997) gives a self-contained account of this theory for one representative long-step method, Algorithm IPF. This mission formalizes the statements of that chapter.
Let (no rank assumption), , , and consider the primal s.t. , and the dual s.t. , . The solution set consists of the triples with , , and for all . For a triple the residuals are and , and the duality measure is . Norms are Euclidean unless marked.
Fix a starting point with , with residuals and duality measure . For and , the neighborhood is
Algorithm IPF has parameters and . At iterate it picks and solves the linear system
where , and . It takes the largest such that the point lies in and there is at most . That point is the next iterate. The analysis uses and the scaling .
A positive sequence converges Q-linearly if for some and all large . It converges R-linearly if it is dominated by a Q-linearly convergent sequence.
If and the start is infeasible, , then along Algorithm IPF
The statement fixes no rate. It asserts only the shape of the convergence, so it survives any improvement of the constants.
Theorem 6.1 is the reason infeasible starts are safe. A practitioner may start from any positive point. If the problem has a solution, the method then removes the infeasibility and the duality gap at a linear rate, without a Phase I. Lemma 6.7 is the core estimate: one uniform lower bound on the step length gives both rates, and its -explicit form (6.38) gives the complexity of Theorem 6.2. Theorems 6.8 and 6.9 show that the iterates identify the optimal partition . This is the basis of the finite-termination procedures of the next chapter.
These results are proved in the literature and in the book. They have not been machine-checked: the Prove2Me corpus contains a formalized convergence theorem for Vanderbei's path-following method under a boundedness hypothesis, but no infeasible-interior-point theory with the neighborhood . The mission would produce the first checked proof of global linear convergence for an infeasible primal-dual method. The definitions it introduces (the algorithm as a predicate on sequences, Q-/R-linear convergence) can be reused for the self-dual and termination chapters.
The obvious argument for a feasible method bounds the second-order term by a multiple of through the orthogonality . With infeasible iterates this orthogonality fails, and the cross terms involve the iterates themselves, which are not bounded a priori. The step from "the residuals shrink" to "the step length stays bounded below" therefore needs a bound on in terms of . That bound has to come from a solution of the linear program. The hypothesis is essential. The page prints Theorem 6.1 without it, but on the infeasible program , , the neighborhood condition keeps bounded away from zero. A solver should also note that the explicit displayed in the proof of Lemma 6.7 drops a factor against the bound (6.47) derived just before it, and can equal . Only the existential statement survives as printed. The bound (6.38) is left to the reader in the book (Exercise 4).
Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ. Euclidean norms and the 1-norm are defined explicitly, because Mathlib's default norm on Fin n → ℝ is the sup norm. "Generated by Algorithm IPF" is a predicate on the sequences , , and the directions. The direction is given by its linear equations, not by a closed form, and "the largest " is an IsGreatest hypothesis on the admissible set rather than a constructed maximum. The neighborhood is anchored at the run's own start. Every statement carries the hypotheses the chapter states once and then omits: ; (p. 111); where the proof starts from a solution (pp. 127, 185); and, for Lemma 6.7, a start inside (pp. 109, 120). Constants , , , are positive and quantified before the iteration index. in (6.38) is quantified after the algorithm's parameters and before the dimension and the instance. That is how "independent of " is rendered.
Explicit constants. Lemma 6.6's "a constant independent of " is stated with the value its proof sets, . The book gives no explicit for (6.38), and none is invented. Theorem 6.2 () is not posed, because an explicit iteration count would rest on that unproved exercise.
A trivializing formalization is ruled out. The Q-linear predicate requires and , not only a ratio bound, and R-linear convergence is domination by such a sequence. is explicit, since division by zero would make (6.49) vacuous. No hypothesis beyond the book's is added to make a run easier to exhibit, and the greatest step length is required to exist exactly as the algorithm prescribes.
Beyond the paper. One sharpness probe accompanies the goal: Theorem 6.1 with removed, expected to be false by the counterexample above; a disproof is the sought outcome.
Infrastructure that would help: the identity , orthogonality of and when and , the Goldman–Tucker theorem (strictly complementary solutions exist; Wright, Theorem 2.4), and Hoffman's bound for Theorem 6.9. Contributions of reusable lemmas on Q-/R-linear sequences are welcome.
Empirical risk minimization (ERM) chooses, from a fixed set of functions, the one with the smallest average loss on the training sample. Its risk is controlled by bounds whose confidence term grows with the VC dimension of the set and shrinks with the sample size . When the ratio is small, a fixed set is either too poor to approximate the target or too rich to be estimated reliably. The structural risk minimization (SRM) principle of Vapnik and Chervonenkis (1974) resolves this by nesting sets of growing capacity and choosing, as a function of the sample size, the element in which to minimize the empirical risk. It is the conceptual ancestor of model selection by complexity penalties, of support vector machines' margin control, and of the minimum description length principle.
Chapter 4 of Vapnik's The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) states the asymptotic rate of SRM (Theorem 4.1) together with the two finite-sample risk bounds it rests on, (4.1) and (4.2), and the finite-class bound (4.25) from which the book derives its minimum description length bound. The book prints no proofs; the standard ones are in Vapnik, Statistical Learning Theory (Wiley 1998), and Vapnik–Chervonenkis, Theory of Pattern Recognition (1974).
Let be a probability measure on a set and , , a set of nonnegative measurable functions indexed by an arbitrary set . The risk is and the empirical risk on an i.i.d. sample is .
The VC dimension of a set of real functions is the largest number of points shattered by the indicators , , , where for and otherwise (§3.6). In Lean: NatureSLT.SRM.vcDimReal Q A B : ℕ∞.
A structure is a sequence of nested nonempty subsets , (4.3). It is admissible if each has finite VC dimension and either (i) on , or (ii) for some (4.4). Write in case (i) and in case (ii). The union is assumed dense in for the metric .
A law (4.5) chooses an element, and minimizes over . The rate of approximation is (4.8).
Following footnote 3 (p. 97), random variables converge to with asymptotic rate if, for some constant , in probability. In Lean: NatureSLT.SRM.ConvergesWithRate.
If the law satisfies
then converges in probability to with asymptotic rate
This is NatureSLT.SRM.theorem_4_1, stated as printed. Finding F1 shows that as printed it is false: a law that keeps returning to a small element satisfies (4.7) while the risks oscillate. Finding F4 shows that the footnote-3 notion of rate can fail even when . A disproof of the goal is therefore a legitimate outcome.
Every constant is the book's: the and of , the and the under the root in (4.1), in (4.2), and the under the root in (4.25).
Theorem 4.1 is the book's asymptotic statement that SRM is consistent and adapts to the target. The rate is the sum of an approximation term and an estimation term, so a priori knowledge of the approximation rate yields the best law , as in the Example (4.9) on p. 98, where gives the rate . The bounds (4.1) and (4.2) are the finite-sample inequalities SRM minimizes in practice, for bounded and for heavy-but-not-too-heavy-tailed losses. (4.25) is the starting point of the book's comparison of SRM with the minimum description length principle (Theorem 4.3).
The platform holds related but different statements: UnderstandingML.srm_bound and UnderstandingML.srm_nonuniform_rate (SRM as nonuniform learning over a countable union with weights), UnderstandingML.mdl_bound (a prefix-free description-length bound with other constants), and FoundationsML.ModelSelection.srm_learning_guarantee_v2 (Open, Mohri et al.'s form). None states the asymptotic rate of Theorem 4.1 or the relative-deviation bounds (4.1), (4.2), (4.25) in the book's form. As far as is known, none of the four statements of this mission has a machine-checked proof.
The goal combines three things that each fail in a naive treatment. First, the uniform bound must be applied to a different class at every sample size, so its constants must be uniform in the element. Second, the approximation term tends to only if , which (4.7) does not imply; a proof that assumes it proves a different theorem. Third, the footnote-3 rate is a statement about the limit of a normalized error, not a bound on it, so an bound alone does not establish it.
For (4.1) and (4.2), the step from a VC dimension to a bound with these exact constants goes through the relative-deviation inequality with the annealed entropy at and the bound on the growth function in terms of . For (4.25) the obstacle is the relative (not additive) form: Hoeffding's inequality gives the wrong shape and does not suffice.
Samples are functions under the product measure (Measure.pi). is a type, the structure is Λs : ℕ → Set Λ (monotone, every element nonempty, indexed from ), and , are given sequences tied to the structure by the two admissibility cases. The empirical minimizer is a given map from samples to , and its existence is not claimed. Measurability is explicit throughout. Each is measurable and integrable, and the risk of the minimizer is a measurable function of the sample. In (4.1) and (4.2), the event "the bound holds for all " is assumed measurable. The ratio in (4.4) and (3.19) is multiplied out, with assumed integrable. Infima are over nonempty sets bounded below by , so no junk value of ⨅ enters. In (4.1) and (4.2) the range is assumed: the page leaves it implicit, and outside it the printed can be negative and the printed bound false (finding F5). The trivializing formalization the series warns about, a non-measurable event read as probability or an infimum over an empty element read as , is ruled out by those hypotheses.
Beyond the paper. One variant is posed: NatureSLT.SRM.theorem_4_1_corrected ([Corrected], finding F1). It adds and reads the rate as for some constant . It is not a milestone. The planner also notes (F3) that the printed derivation of (4.27) from (4.25)–(4.26) has a gap. Those statements are not part of this mission.
Reusable infrastructure: the VC dimension of a real class, the product-measure sample space, and the footnote-3 notion of rate. Contributions welcome: proofs or disproofs of each item, and a published definition of vcDimReal that the other missions of this series could reference.
Every guarantee that a learning machine trained by empirical risk minimization will perform well on unseen data rests on one kind of statement: a bound on the probability that, simultaneously over a whole set of functions, observed frequencies stray far from the probabilities they estimate. Vapnik and Chervonenkis proved the first such bounds for sets of events in 1968 and 1971 (Vapnik–Chervonenkis 1971), with the growth function as the capacity measure and the constant . Vapnik's later monographs (Estimation of Dependences Based on Empirical Data, 1979; Statistical Learning Theory, 1998) refined the constants, replaced the growth function by the distribution-dependent annealed entropy, introduced the relative-deviation bound that underlies fast rates for small risks, and extended everything to bounded real-valued loss functions. Chapter 3 of The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) collects the resulting "basic inequalities of the theory of bounds" in their final form, stated without proof, and derives from them the confidence bounds used throughout the book (structural risk minimization in Chapter 4, support vector machines in Chapter 5).
This mission formalizes those inequalities exactly as the book prints them.
Let be a probability space and let , , be a set of functions on indexed by an arbitrary parameter set (parameters need not be vectors). An i.i.d. sample is drawn from , i.e. from the product measure . For each the risk and the empirical risk are
When every is an indicator function (values in ), is the probability of the event and its frequency. The number of different binary vectors , , is , the number of separations of the sample by the set. Two capacity measures are built from it:
The annealed entropy depends on ; the growth function does not and dominates it.
For a set of real functions with , the book passes to the set of indicators , , , where for and otherwise; and are the annealed entropy and growth function of this indicator set.
For indicator functions and every ,
The constants are the book's: the factor , the exponent , and the entropy evaluated at . No sample-size restriction is imposed beyond .
The result itself. Theorem 3.1 and its relatives turn a capacity estimate into a confidence interval for the risk of every function in the set at once, including the one chosen by empirical risk minimization. They are the bridge between the combinatorics of Chapter 3 (the growth function is either or at most for VC dimension ) and every algorithmic guarantee in the rest of the book: structural risk minimization, the VC bound for margin hyperplanes, the support vector machine. The relative-deviation form (Theorem 3.2) is what makes bounds of order rather than possible when the empirical risk is near zero.
Formalizing it. The book prints no proofs. The classical argument is published (Vapnik–Chervonenkis 1971; Vapnik 1998, Chapter 4), but with other constants: the 1971 theorem has and needs , and the 1998 version has in place of . On Prove2Me the 1971 form is proved as VapnikChervonenkis.Inequality.theorem2_uniform_deviation_bound, together with its symmetrization and permutation lemmas, and finite-class uniform convergence with is proved as UnderstandingML.finite_class_uniform_convergence. Neither states the book's constants, the annealed entropy, the relative deviation or the real-function extension, so the statements here are new. Settling whether the book's constants hold as printed, for every , is part of the work.
The obvious route to Theorem 3.1 replaces the supremum over the possibly uncountable set by a finite one through a ghost sample of size and a count of separations on the doubled sample. Every step costs constants: the symmetrization inequality loses a factor and requires to be large, and the conditional deviation bound for sampling without replacement brings its own exponent. Reproducing the textbook argument therefore tends to yield the 1971 or 1998 constants, not the printed with no sample-size condition; reaching or refuting the printed form is the crux. The relative-deviation bound needs a separate normalization argument, and the real-function bounds require relating deviations of to deviations of its level-set indicators uniformly in the level .
The finite-class item (3.26) with (3.25) is expected to be false as printed: a single fair coin with and violates it (finding F1).
The sample is z : Fin ℓ → Z under Measure.pi (fun _ => F) with [IsProbabilityMeasure F]; is an arbitrary type and . Indicator functions carry the hypothesis that every value is or ; real functions carry with . and are written inline as the integral and the normalized sum. The event "the supremum exceeds " is written "some has deviation exceeding ", which is the same event for a strict inequality; a bare ⨆ α over an unbounded family would read Lean's junk value and make the bound trivially true, and is not used. Probabilities are compared in with ENNReal.ofReal of the real bound, and "with probability at least " is ENNReal.ofReal (1 - η) ≤ F^ℓ(event) with . In Theorem 3.2 and (3.4) the supremum runs over the with , which excludes the zero denominator.
The book assumes the events it measures to be measurable; this is made explicit: each is measurable, (or the counting function of the indicator set) is measurable on wherever an expectation of it appears, and the deviation events are measurable at every level. These hypotheses are needed so that a non-measurable count cannot turn into and make the bound vacuous or stronger than the book's. The finite-class items need no event-measurability hypothesis.
The definitions are numSeparations (, via Set.ncard of the set of vectors), annealedEntropy, growthFunction (a real supremum, bounded by for -valued families) and levelIndicators (indexed by , with ). They are reusable by any development of VC theory in this form.
Beyond the paper. One corrected variant is posed: eq_3_26_finite_corrected, the finite-class two-sided bound with in place of in (3.25). The evidence (finding F1) is that with and , , , the half-width is about while with probability . With the statement is the standard two-sided finite-class bound.
Welcome contributions: proofs or disproofs of the goal and milestones with the printed constants; proofs of the corrected variant; a disproof of the faithful (3.26) with (3.25).
A Jackson network of exponential single-server queues has a stationary distribution of product form: the numbers of customers at the nodes are independent in steady state, each geometric (Jackson, 1957; Jackson, 1963). The same property holds for a large family of networks (Kelly, Reversibility and Stochastic Networks, 1979), and it is what makes performance formulas for such networks explicit. A network can also be read as a quasi-birth-and-death process (QBD): take the number of customers at one node as the level and the vector of queue lengths at the other nodes as the phase. The phase set is then infinite, , and product form becomes the statement that level and phase are independent in steady state. Ramaswami and Taylor (Stochastic Models 12, 1996, pp. 121–142 and 143–164) characterized when a QBD has this independence property and used the characterization to find new product-form networks. Chapter 15 of Latouche and Ramaswami, Introduction to Matrix Analytic Methods in Stochastic Modeling (SIAM, 1999), gives a simplified version of these results, and this mission formalizes it.
Fix a countable set of phases, finite or infinite, and four real matrices indexed by . A continuous-time QBD is the Markov process on the states , with level and phase , whose infinitesimal generator is block-tridiagonal:
and are nonnegative, and have nonnegative off-diagonal and strictly negative diagonal entries, and the rows of sum to zero. The level is the set . The process stays in a state for an exponential time of rate and then jumps to with probability ; this jump chain together with the mean sojourns describes it. It is assumed irreducible and regular (finitely many transitions in every bounded time interval). It is positive recurrent if it returns to every state with probability one and the expected return time is finite. A stationary probability vector , partitioned by levels, satisfies , and .
Two matrices indexed by phases are defined by what they mean for the process:
The level is independent of the phase in steady state if for some probability vector on and some probability density on the levels. A vector is positive if for every phase.
The process is positive recurrent with level and phase independent in steady state if and only if there are a positive vector with and a scalar with
then for all . The criterion uses only the blocks of , not .
The goal says that independence of level and phase forces the level to be geometric, and it reduces the question to a linear system in for a fixed . That system involves only the generator's blocks, so it can be checked for models whose rate matrix has no closed form. Together with Theorem 15.2.1 it gives a QBD proof of the product form of open Jackson networks, and the same approach led Ramaswami and Taylor to product-form networks beyond Jackson's. The level-dependent version (§15.3) is described in the book but not proved there.
Formalizing the chapter adds the continuous-time layer of the matrix-analytic series: a generator on a countable state space, regularity, and positive recurrence defined by return times, with expected sojourn times as sums over trajectories of the jump chain. The product form of open migration processes, which contains the Jackson case, is on the platform as KellyStochasticNetworks.open_migration_equilibrium. It is a balance-equation statement about a network and does not concern QBDs. No QBD statement is on the platform.
The "if" direction of the goal looks like a computation: satisfies . But a solution of shows positive recurrence only through regularity, and on an infinite phase set that is a real hypothesis. Relating the generator condition to the eigenvector condition is the hard part. The book notes that the finite-dimensional argument (Perron–Frobenius theory for ) "fails in the case of an infinite number of phases": spectral arguments for are not available when is infinite, and every product of infinite matrices must be justified by nonnegativity. For Theorem 15.2.1, positivity of and is not visible in the hypotheses on the load. It comes from irreducibility of the network.
All declarations are in MatrixAnalytic.ProductForm. States are ℕ × ι with ι countable and arbitrary (levels from ; no finiteness of phases is assumed anywhere). The generator is qbdQ B A₀ A₁ A₂, and the hypothesis IsGeneratorC encodes the sign and zero-row-sum conditions. The continuous-time process is encoded through its jump chain and mean holding times, without measure theory. Irreducibility is that of the jump chain. Regularity (RegularCT) says that the sum of mean holding times along the jump chain diverges almost surely. Positive recurrence (PositiveRecurrentCT) says the return probability is one and the expected return time is finite. and are sums over taboo trajectories valued in , never solutions of . Defining by that equation, or positive recurrence by the existence of a stationary vector, would make the milestones circular and is ruled out. Positive recurrence and stationarity are separate objects. "Level independent of phase" is the factorization , not the geometric form, which is the conclusion. Vector equations over infinite phase sets are convergent sums; products of nonnegative matrices are computed in . The Jackson network indexes nodes by Option J with J finite, none being node 1. Its blocks are written out rate by rate, and the openness of the network ( invertible) is carried as the meaning of "the solution" of the traffic equations.
A complete development needs the theory of continuous-time chains on countable spaces through the jump chain (invariant measures, positive recurrence, the regular case), the continuous-time matrix-geometric property, and the series representation of . These are reusable well beyond this mission, and contributions of any of them are welcome.
A quasi-birth-and-death process moves on levels and, within a level, among finitely or infinitely many phases; its stationary distribution is matrix-geometric, , which is the central result of the matrix analytic method (Neuts, Matrix-Geometric Solutions in Stochastic Models, 1981; Latouche & Ramaswami 1999, Chapter 6). Several queueing models do not fit on a line of levels but on a tree. The standard example is a single-server queue with Poisson arrivals, phase-type service and last-come-first-served discipline: an arrival interrupts the customer in service, who keeps a record of the phase in which the service was interrupted. The state must then remember the whole stack of interrupted phases, not only its height, and the levels branch into an -ary tree. Multi-class LIFO queues, some random-access protocols and stack-based models in telecommunications have the same shape (Yeung & Sengupta 1994; Takine, Sengupta & Yeung 1995).
Chapter 14 of Latouche and Ramaswami shows that the matrix analytic picture survives this branching: the stationary distribution on the infinite tree is a product of matrices, determined by one expected-time matrix . This mission formalizes that chapter.
Fix a set of phases , with finite or countably infinite. A state is either the empty stack or a stack of phases with . The states , ranging over the phases, form the stack descriptor (or node) ; these nodes form an -ary tree whose root is (stacks of size one) and whose root's parent is .
The process is a continuous-time Markov process. Its data are two vectors and matrices indexed by the phases, and its only transitions are
Its generator (the book's (14.2)–(14.3)) is assumed to be irreducible, and the data are otherwise arbitrary.
When the process is positive recurrent, meaning that the expected time to return to any state is finite, it has a unique stationary probability vector with , and . We write for its value at and for its subvector on the node .
The key object is the matrix . Its entry is the expected total time spent in the state , starting from , before the first visit to . From it the chapter builds:
If the process is positive recurrent, then for all and all phases ,
The matrix-product form reduces the stationary distribution of a process on an infinite, exponentially branching state space to a single matrix. Equations (14.6) give a monotone fixed-point scheme for computing it, and Lemmas 14.3.4–14.3.6 turn the stability question into a spectral condition on , which is explicit in the rank-one case covering M/PH/1 queues under LIFO. Later work on tree-like quasi-birth-and-death processes and on multi-type branching structures in queueing (Bini, Latouche & Meini 2005) builds on exactly these statements.
These results are proved in the book, but none of them is machine-checked, and the platform has no continuous-time Markov processes on countable state spaces with expected-time quantities. The mission adds that substrate: generators, jump chains, expected sojourn times, return-time positive recurrence and stationary vectors. It also states the chapter's results over it.
The proof in the book is three lines: it applies a general censoring theorem to the subtree below a node. A formal proof needs that theorem for continuous-time processes on a countable state space. It also needs the homogeneity of the tree: is defined at the root node only, and the fact that every other node's expected-time matrix equals it is part of what must be shown, by an explicit isomorphism of subtrees. The stationary vector is characterized by , a system with infinitely many unknowns; its equality with occupation-time ratios requires recurrence and the absence of explosion. The stability lemma 14.3.4 has a one-line proof whose "if" direction leaves recurrence unaddressed, so a complete argument must supply more than the page does.
Phases are an arbitrary countable type, with finiteness assumed only in (14.6), in the second statement of Lemma 14.3.4 ("if is finite") and in Lemma 14.3.5. That lemma also carries the irreducibility of , which is the hypothesis of the quasi-birth-and-death drift criterion to which the book reduces it. A state is none (the empty stack) or a pair of a list of phases (bottom first) and the phase at the top.
The process is encoded by its embedded jump chain and holding rates. Probabilities are sums over finite trajectories of products of jump probabilities. Expected times are expected visit counts multiplied by mean holding times, valued in . , , and are defined by what they mean, never by (14.4) or (14.6) and never as "the minimal nonnegative solution" of an equation; this rules out the formalization in which the goal holds by definition. Positive recurrence is the return-time notion, never "a stationary vector exists", and the stationary vector is a probability vector, so the trivial solution is excluded. Matrix identities involving stationary probabilities are stated coordinatewise in , which also asserts the finiteness of the right-hand sides. The inverse in (14.6) is stated as a two-sided inverse together with the finiteness of .
Beyond the paper. No variant is posed. Corollary 14.3.2 writes , a symbol the chapter does not define otherwise; it is formalized as the level-1 vector , the only reading consistent with the corollary's own case .
Useful contributions beyond the listed statements: a general censoring theorem for continuous-time chains on countable state spaces, and the equivalence between return-time positive recurrence and the existence of a stationary probability vector for nonexplosive irreducible generators.
Many queueing and reliability models are Markov chains on a two-dimensional state space whose first coordinate, the level, moves by at most one unit per transition, while the second, the phase, records an auxiliary state such as the phase of a service time or the number of busy servers. When the transition probabilities do not depend on the level, such a chain is a homogeneous quasi-birth-and-death process (QBD), and its stationary distribution is matrix-geometric. In a large class of models they do depend on the level: queues with level-dependent arrival or service rates, retrial queues, systems with a finite but large number of sources, population models. These are nonhomogeneous (level-dependent) QBDs. Chapter 12 of Latouche and Ramaswami's textbook (SIAM 1999) shows that the structural theory of the homogeneous case carries over: the first-passage matrices still exist, still satisfy nonlinear matrix equations, and are still characterized as the minimal nonnegative solutions of those equations, now coupled across consecutive levels. The level-dependent theory with countably many phases is developed by Ramaswami and Taylor (Stochastic Models 12, 1996) and, on the computational side, by Bright and Taylor (Stochastic Models 11, 1995), the book's references [103] and [10].
For each level let be a nonempty countable set of phases; different levels may have different numbers of phases. The chain lives on the states with , and its transition matrix is block tridiagonal,
with (of size ) the transitions up from level , the transitions within level , and (of size ) the transitions down from level . The level is the set of states with first coordinate , and is the first time at which the chain is in . The chain is assumed stochastic and irreducible.
Three families of matrices are attached to the chain, for :
For a nonnegative matrix , denotes the series , as in the book.
For every ,
and each of the three sequences is the entrywise smallest sequence of nonnegative matrices that solves its system for all simultaneously.
The minimality theorem is what makes the level-dependent theory computable. The matrices , , are defined through events on infinite trajectories; the equations (12.7)–(12.9) are local, linking each level only to the next one; and minimality singles out the probabilistic solution among the many nonnegative solutions these equations have (for instance, for a transient chain with one phase per level the constant sequence solves (12.7), while ). Theorems 12.1.1 and 12.1.4 then express the stationary distribution as a matrix product and give a positive recurrence criterion; Theorem 12.1.5 is the recurrence criterion. Truncation and augmentation schemes for level-dependent chains, discussed in §12.2, rest on these facts.
The results are classical and proved; the book outlines the minimality proof ("long and arduous") and refers to the homogeneous arguments of its Chapter 8. None of them has a machine-checked proof. A formalization would provide a reusable development of first-passage decompositions on chains with a dependent, level-indexed state space, which the homogeneous missions of this series do not need.
The equations themselves follow from conditioning on the first transition, but making that rigorous requires splitting sums over infinite families of trajectories at first-passage epochs, on a state space where the phase set changes from level to level and may be infinite. The minimality claim is the hard part. A comparison level by level does not work: (12.7) at level involves , so a competing solution can only be compared with through the whole infinite sequence at once, and nothing anchors the comparison at a top level. Infinite matrix products and series must be handled with entries that may a priori be infinite.
The phase sets are a family ι : ℕ → Type* with [∀ n, Countable (ι n)], [∀ n, Nonempty (ι n)], and the state space is the dependent pair type Σ n, ι n, so the off-diagonal blocks are genuinely rectangular; Theorem 12.1.5 replaces countability by [∀ n, Fintype (ι n)]. The blocks are A₀ n , A₁ n and A₂ m , and ndqbdP A₀ A₁ A₂ assembles them into the transition matrix. In Lean is matG P m and is matR P m (indexed by the lower of the two levels), is matU P n. These matrices are defined as sums, over finite taboo trajectories, of products of one-step probabilities, with values in ℝ≥0∞; every matrix product, power and series is computed in ℝ≥0∞, and convergence and finiteness are stated as conclusions where the book proves them. Recurrence and positive recurrence are the return-time notions of the platform definition mm_countable, restated locally. Minimality is entrywise, among real nonnegative sequences solving the system for every level. Defining , or as the minimal solution of (12.7)–(12.9), or by the recursions of Theorem 12.1.2, would make the goal true by definition; that formalization is ruled out, and the definitions here are probabilistic.
In (12.6) the book prints , a product that is not defined when the levels have different numbers of phases; the statement uses , as in (12.8) and (12.9).
Beyond the paper. One variant is posed: recurrent_iff_G_stochastic_strong (strengthened) states Theorem 12.1.5 assuming only that level has finitely many phases. If is stochastic, level is visited infinitely often, and a finite level then contains a recurrent state. A recorded counterexample shows that the finiteness of level 0 cannot be dropped as well.
Contributions of path-decomposition lemmas for first-entrance sums on countable chains (first-step analysis, splitting at a first passage, monotone approximation under taboo of far levels) are reusable across the whole series and welcome.
Quasi-birth-and-death processes (QBDs) are Markov chains on pairs (level, phase) in which the level moves by at most one at each step. They model queues in random environments, priority queues, and many other systems treated by matrix-analytic methods (Latouche & Ramaswami 1999). Their stationary distribution, when it exists, is matrix-geometric, and computing it reduces to computing one matrix: the first-passage matrix , which records where the chain first lands when it moves down one level. Every algorithm for a QBD's stationary distribution is, at its core, an algorithm for (or for the related matrices and ).
The logarithmic reduction algorithm of Latouche & Ramaswami (1993) computes with a number of iterations proportional to the logarithm of the number needed by the basic linear schemes. It is still among the fastest general-purpose methods, alongside the closely related cyclic reduction (Bini, Latouche & Meini 2005). Its correctness rests on one identity: an infinite series built from a purely algebraic recursion equals the probabilistically defined matrix . This mission formalizes that identity, Theorem 8.4.1 of Latouche & Ramaswami's textbook, together with the intermediate equations of its proof and the convergence statement Theorem 8.4.2.
Let be a countable set of phases, finite or infinite, and let be nonnegative matrices indexed by . The homogeneous QBD is the Markov chain on the states , the level and the phase, whose transition matrix (8.1) is block tridiagonal:
The matrix is assumed stochastic and irreducible, which is the standing assumption of Chapter 8. Write for level , , and .
The first-passage matrix is
It is the probability, starting at level 1 in phase , of ever reaching level 0 and of doing so first in phase .
With the book's convention , the logarithmic reduction recursion is
with . It involves only the blocks .
where the empty product is the identity. The goal also asserts that every inverse and in the recursion has finite entries.
The series identity is what makes the logarithmic reduction algorithm (Figure 8.6 of the book) correct. Its partial sums are the algorithm's iterates, and the identification with the linear-progression iterates gives the quadratic convergence and the iteration count . Theorem 8.4.2 explains why the algorithm is numerically stable: the matrices it inverts approach the identity.
The results are classical and proved on paper; none is machine-checked. A formalization yields a verified link between a fast numerical recursion and the probabilistic object it computes. It also yields a reusable path-sum encoding of first passages for level-structured chains, on which the other algorithms of Chapter 8 (linear progression, cyclic reduction, the series for in Theorem 8.4.4) can be built.
The book's proof is short because it relies on the strong Markov property and spatial homogeneity. With an informal stopping-time calculus, each identity is "conditioning on the state at time ". In a path-sum formalization each such step becomes a bijection between sets of finite trajectories: concatenation at a first-passage epoch, together with the shift of levels by a multiple of . That shift moves the trajectories between levels where the transition matrix is homogeneous. The infinite sums over trajectories, the series inverse and the matrix products over infinitely many phases must be rearranged in . Proving that each series inverse is finite needs irreducibility; it is not automatic.
Theorem 8.4.2 needs more. Its proof uses , which fails when is periodic. As recorded under Beyond the paper, the printed limits for (ergodic case) and (transient case) are false in general, so a disproof of that milestone is a legitimate outcome.
Phases form a countable type ι ([Fintype ι] only for Theorem 8.4.2). States are ℕ × ι with levels counted from 0, and the transition matrix is the function qbdP B A₀ A₁ A₂. Matrices with nonnegative entries take values in ℝ≥0∞: products are tsums there, and every inverse in the recursion is the series (seriesInvE, the book's convention on p. 109). Finiteness of those series is asserted in the conclusions, never assumed. , and the passage probabilities of (8.37) and (8.45)–(8.48) are sums over finite trajectories of products of one-step transition probabilities. Positive recurrence ("ergodic" in the book) is the return-time notion; transient means not recurrent. "The stationary probability vector" is a stationary probability vector assumed to be the only one. Limits are entrywise.
is never defined as a solution of or of , nor as the value of the series; either would make the goal true by definition. Conversely, and are defined by the recursion, exactly as in the book, and their probabilistic meaning is a milestone.
The definitions restate the Markov-chain notions of the platform definition mm_countable locally. Reusable pieces include the path-sum first-entrance and first-entrance-after-a-visit matrices and the ℝ≥0∞ matrix algebra. Contributions are welcome on any milestone, on the series inverse's finiteness, and on the disproof of Theorem 8.4.2.
Beyond the paper. One corrected variant is posed. HLU_limits_corrected replaces the false clauses of Theorem 8.4.2 by (ergodic) and (transient). Evidence: a two-phase positive recurrent QBD with has , and its level reversal is a transient QBD with .
A quasi-birth-and-death process (QBD) is the matrix generalization of a birth-and-death chain: a Markov chain on pairs (level, phase) that moves at most one level per step. QBDs model queues in random environments, multi-server and priority systems, and communication links with correlated traffic, and their analysis rests on two matrices: the first-passage matrix and the rate matrix . Chapter 9 of Latouche and Ramaswami, Introduction to Matrix Analytic Methods in Stochastic Modeling (SIAM 1999, doi:10.1137/1.9780898719734), shows that the spectra of these probabilistic matrices are encoded in a polynomial written directly in the transition blocks. This links the matrix analytic method to the spectral approach to M/G/1- and GI/M/1-type chains (Gail, Hantler and Taylor, Adv. Appl. Probab. 28, 1996) and is the basis of spectral algorithms for and .
Timeline. The matrix-geometric form of the stationary distribution, with as its rate matrix, is due to Neuts (Matrix-Geometric Solutions in Stochastic Models, 1981). The construction of the Jordan structure from the matrix polynomial is due to Rama Murthy, Kim and Coyle (Stochastic Models 7, 1991), who treated ; Latouche and Ramaswami adapt it to (pp. 212–216).
Fix a finite set of phases. A homogeneous QBD is a Markov chain on the states , with level and phase , whose transition matrix is block tridiagonal: from level it moves within level with probabilities and up to level with probabilities ; from a level it moves up with probabilities , stays with probabilities and moves down with probabilities . The four blocks are nonnegative matrices, and . Chapter 9 assumes that the QBD is irreducible and positive recurrent (every state has a finite expected return time), and that is irreducible.
The first-passage matrix has entries = the probability, starting from , that the chain reaches level in finite time and does so first in . The rate matrix has entries = the expected number of visits to , starting from , before the first return to level . The matrix polynomial of the chapter and its determinant are
with , , and . Vectors are in a tower for relative to an eigenvalue if is an eigenvector and for (a Jordan chain).
For a positive recurrent QBD, is a nonzero polynomial and, counting multiplicities,
Milestones 1–3 are the algebraic identities the goal's proof rests on; milestones 4–5 are the rest of the chapter's numbered results, which extend the goal from eigenvalues to the full Jordan structure of .
The result. Theorem 9.3.1 separates the roots of one explicit polynomial into the spectrum of (inside the closed unit disk) and the reciprocal spectrum of (outside it). The eigenvalues of and , including the decay rate that governs the geometric tail of the stationary distribution (§9.1), can therefore be computed from the transition blocks without first computing or . Theorems 9.4.1 and 9.4.2 go further and recover eigenvectors and Jordan chains of from the null spaces of and its derivative, which is how §9.5 reconstructs itself.
Formalizing it. The results are proved in the book; none is formalized. The platform has countable Markov chains (MarkovMixing) and no matrix analytic objects. This mission produces Lean statements of the first-passage and rate matrices as trajectory sums and connects them to polynomial matrices over , a bridge between Markov chain probability and Mathlib's characteristic polynomials and root multisets that later spectral results (M/G/1-type chains, the caudal characteristic) can reuse.
Two steps resist. First, the matrices are probabilistic: before any algebra, the matrix equations satisfied by and , the finiteness of and the location of their spectra must be derived from first-passage probabilities and expected visit counts, that is, from series over trajectories of a chain with infinitely many states. Second, that every eigenvalue of is a root of is a determinant identity, but the theorem says more: the closed unit disk contains no other root, and the roots outside it are exactly accounted for by , with multiplicities, even when is singular and has degree below . Inclusion is easy; exhaustiveness is the content, and it is where the hypothesis of positive recurrence enters. The tempting shortcut, taking to be any nonnegative solution of , does not work: such equations have several nonnegative solutions, and for the non-minimal ones the root count is false.
Phases form a finite nonempty type ι with = Fintype.card ι; blocks are real functions ι → ι → ℝ, mapped to complex matrices for every spectral statement. The QBD is the transition function qbdP B A₀ A₁ A₂ on ℕ × ι. Stochasticity, irreducibility and positive recurrence (summable return-time tails) are restated from the platform definition mm_countable. is a sum, over first-passage trajectories, of products of one-step probabilities, and a sum of taboo-trajectory probabilities; both are computed in ℝ≥0∞ and read in ℂ (matGc, matRc), and the finiteness of is part of each conclusion that uses it. is the determinant of a matrix over ℂ[X]; roots are Polynomial.roots (with multiplicity), eigenvalues are roots of Matrix.charpoly, and is ‖z‖ ≤ 1. An eigenvector is nonzero, so Theorems 9.4.1–9.4.2 carry (resp. ).
The trivializing formalization is excluded: and are never defined as solutions or minimal solutions of a matrix equation, positive recurrence is never "a stationary distribution exists", and the goal asserts so that it cannot hold through the empty root multiset of the zero polynomial.
Beyond the paper. One strengthened variant restates Theorem 9.3.1 without the irreducibility of , a standing restriction of Chapter 9 that its proof never uses (finding F3). Findings also record that "eigenvector" must be read as nonzero in Theorems 9.4.1–9.4.2 (F1) and that the proof of 9.3.1 omits the argument that , which follows from being nonsingular (F2).
Contributions welcome: first-step analysis for trajectory-sum passage matrices (useful across the whole series), lemmas relating Matrix.det of a polynomial matrix to evaluation and to reversed polynomials, and root counting for products of determinants.
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.
A quasi-birth-and-death process (QBD) is the Markov chain behind queues with phase-type service or arrivals, priority queues, and many models of telecommunication and inventory systems: a level that moves up or down by at most one per step, and a phase that carries the rest of the state. Its stationary distribution is determined by three matrices indexed by phases, , and , which no closed formula gives in general. Every numerical method for QBDs therefore solves a nonlinear matrix equation that these matrices satisfy, such as or .
Such an equation typically has several nonnegative solutions. An algorithm is useful only if it converges to the solution that has the probabilistic meaning. Chapter 8 of Latouche and Ramaswami (SIAM 1999) settles this. Each of , and is the minimal nonnegative solution of its equation. The simplest iteration, started from , increases to it. The chapter's analysis of the rate of convergence goes through the level-reversed process. The quadratic equations and the iteration go back to Wallace and to Neuts (Neuts, Matrix-Geometric Solutions in Stochastic Models, 1981); the chapter proves convergence of its algorithms by taboo arguments on the sample paths of the chain.
Fix a set of phases, finite or countably infinite, and real matrices indexed by . The homogeneous QBD is the discrete-time Markov chain on states , , , with block-tridiagonal transition matrix
From a level the chain moves up with probabilities , stays with and moves down with . From level it stays with and moves up with . The chain is assumed irreducible. No recurrence assumption is made unless stated. The level is the set of states , and .
The central objects are defined by what they mean for the chain:
For a nonnegative matrix , denotes the series , also when the matrix has infinite order. A solution of a matrix equation is minimal in a set of nonnegative matrices if for all and every solution in the set.
For every irreducible QBD:
In the first two parts the competitors are the nonnegative matrices for which the series converges; in the last two, all nonnegative matrices. In each part the probabilistic matrix is itself an admissible solution.
Minimality is what makes every algorithm of the chapter, and the logarithmic and cyclic reduction methods built on them, correct. An iteration that is monotone from and stays below every nonnegative solution must converge to the probabilistic matrix and to no other root. Without the theorem, a numerically computed root of need not be the first-passage matrix, and the matrix-geometric formula built from it could be wrong. Theorem 8.2.3 identifies the convergence rate of the linear algorithm with the caudal characteristic , which also governs the tail of the stationary level distribution.
These results are proved in the book; none of them is formalized on the platform or, to our knowledge, elsewhere. Formalization produces a machine-checked link between taboo path probabilities over a possibly infinite phase set and the algebra of nonnegative matrix equations. Chunks on logarithmic reduction, level-dependent QBDs and M/G/1-type chains reuse that link directly.
The equations satisfied by , , (Theorems 6.2.9 and 6.2.10 of the book) are not enough: minimality needs the identification of the probabilistic matrices as limits of explicit monotone sequences. That is a first-passage decomposition of taboo trajectories under the strong Markov property, carried out with sums over paths rather than with a measure on path space. With infinitely many phases, every matrix product is an infinite series of nonnegative terms, and is a series whose convergence is part of what must be shown.
The printed proof that is minimal for proceeds by contradiction against a solution lying below . It does not cover solutions not comparable with , which the definition of minimality requires (finding F3 of this mission). Lemma 8.2.1's claim that is stochastic for a transient QBD fails when is reducible (finding F1). The faithful statement is posed as printed, beside a corrected variant.
States are ℕ × ι, ι a countable type with decidable equality; levels are counted from ; qbdP B A₀ A₁ A₂ is the transition matrix above, and the level-reversed QBD is qbdP B̂₁ A₂ A₁ A₀ with an arbitrary boundary block. Stochasticity, irreducibility, recurrence and positive recurrence are the return-time notions of the platform definition mm_countable, restated locally. , , , , , , are sums over finite taboo trajectories of products of transition probabilities, with values in ; products and the series are computed there, so "the series converges" means every entry is finite. Competing solutions range over real matrices with nonnegative entries.
Defining , or as the minimal solution of one of these equations would make the goal true by definition. It is ruled out here: they are probabilities and expected numbers of visits.
Lemma 8.2.1, Theorem 8.2.3 and Theorem 8.3.1 take [Fintype ι]: the latter two because the book does, the first because its spectral-radius clause concerns a finite matrix. Lemma 8.2.1 also takes [Nonempty ι]. Spectral radii are taken over ; "substochastic" in Lemma 8.2.1 means row sums at most one with one strictly less. In Theorem 8.3.1 the inverse is the matrix inverse, and its existence is a conclusion.
Beyond the paper. One variant is posed: [Corrected] Lemma 8.2.1 with irreducible (finding F1: a two-phase diagonal QBD is transient with not stochastic).
A complete development needs first-passage decompositions of path sums, monotone convergence for -valued series, recurrence criteria for QBDs (Chapter 7), and Perron–Frobenius theory for irreducible nonnegative matrices. The path-sum toolkit is reusable across the whole series; contributions of general lemmas on taboo decompositions are welcome.
Matrix analytic methods compute the stationary distribution of structured Markov chains (quasi-birth-and-death processes, M/G/1- and GI/M/1-type chains) by working on one block of states at a time. Every such computation rests on one device: watch the chain only while it is in a subset of the state space, and describe what happens in between through expected numbers of visits to the complement. Chapter 5 of Latouche and Ramaswami, Introduction to Matrix Analytic Methods in Stochastic Modeling (SIAM, 1999, doi:10.1137/1.9780898719734), develops this device for a countable chain. It gives the relation between stationary probabilities on disjoint subsets, the Markov renewal identities between first-passage and expected-visit matrices, and the restricted (or censored) chain on . Later chapters of the book use these results to derive the matrix-geometric form and the linear level reduction algorithms. Outside queueing theory, the same censored chain appears as Meyer's stochastic complement in numerical linear algebra and as the Schur complement of .
The censored chain goes back at least to Kemeny, Snell and Knapp, Denumerable Markov Chains (Springer, 1976, Chapter 6), whom the book cites for the proof. Freedman's Markov Chains (1971) calls it the restricted process. Grassmann, Taksar and Heyman (1985) turned the construction into the GTH algorithm, which is §5.4 of the book.
Let be a countable set and a stochastic matrix: and . It is the transition matrix of a Markov chain . The chapter's standing assumption is that the chain is irreducible (every state reaches every state with positive probability) and aperiodic. Its limiting probability vector is . When the chain is positive recurrent (every state has a finite expected return time), is the stationary probability vector: , , .
For , write for the submatrix of on and . Let and . The chapter's objects are expectations and probabilities of events of the chain:
Products of these matrices sum over the indicated subset. Following the book's convention, means the series for a nonnegative matrix , also when has infinite order.
The epochs of visits to are and . The restricted process is .
Let the chain be irreducible and positive recurrent with stationary vector , and let be nonempty. Then the restricted process is defined at all times and is a homogeneous Markov chain on with transition matrix
For every initial state and ,
is stochastic, irreducible and positive recurrent, and
so is its unique stationary probability vector.
Theorem 5.3.1 reduces the stationary distribution of a chain on to that of a smaller chain on , whose transition matrix is explicit in the blocks of . Applied with a set of levels, it gives the boundary equations of every matrix analytic model in the book. Applied one state at a time, it is the GTH elimination algorithm. Theorem 5.2.1 is the general form of for birth-and-death chains, and the mission's matrix-geometric and level-reduction results depend on it. The Markov renewal identities of Theorem 5.2.3 and Lemma 5.2.4 compute and from first-passage kernels, which is how the matrices , and of quasi-birth-and-death processes are characterized in later chapters.
The results are classical and proved in the book, partly by citation (Theorem 5.3.1 refers to Kemeny, Snell and Knapp for details, and the proof of Theorem 5.2.3 is left partly to the reader). No machine-checked version of any of them exists on this platform. The platform has countable chains and stationary distributions (mm_countable), and Sennott's first-passage identities for Markov decision processes, but no censored chain and no taboo-matrix calculus. What remains is the countable-state proof in full: the strong Markov decomposition of trajectories at the epochs , and the interchange of limits and infinite sums that the book handles with Fatou's lemma.
The algebraic identity is a short computation once Theorem 5.2.1 and (5.11) are available. The content is elsewhere.
The state space is a countable type S, and the transition matrix is a real function P : S → S → ℝ. Stochasticity, irreducibility, aperiodicity, positive recurrence (summable return-time tails) and stationarity have the bodies of the public definition mm_countable, restated in the namespace MatrixAnalytic.Taboo. Every probabilistic quantity (, , , , , and the law of the restricted process) is a sum over finite trajectories of products of transition probabilities, valued in , so every series exists and an infinite expectation is . Finiteness, where the book asserts it, is a stated conclusion. is always the series of powers, never a matrix inverse. is defined by its formula, and the theorem relates it to the restricted process's law. The restricted chain's irreducibility, positive recurrence and stationary vector are stated for read as a real matrix on the subtype of states of .
A trivializing formalization is ruled out: defining , or the restricted chain's transition matrix as the series or the formula the theorems assert would make Lemma 5.1.2, (5.23) and Theorem 5.3.1 true by definition, and that is why each is defined as an expectation over trajectories. Positive recurrence is the return-time notion, never "a stationary vector exists", which would make the restricted chain's positive recurrence follow from alone.
Committed conventions:
The continuous-time results of §5.5 are not part of this mission.
Contributions that would be reusable beyond it are welcome: a strong Markov decomposition of trajectory sums at hitting times, and a library of first-passage and taboo identities for countable chains in .
Scheduling independent jobs on machines that run at different speeds, so that the last job finishes as early as possible, is one of the basic problems of scheduling theory. In the classification of Graham, Lawler, Lenstra and Rinnooy Kan it is denoted , the minimum makespan problem on uniform parallel machines. It is strongly NP-hard, so the question is how close to the optimum a polynomial-time algorithm can get.
For identical machines, Graham's list scheduling (1966) is within a factor , and Hochbaum and Shmoys (J. ACM, 1987) gave a polynomial approximation scheme. For machines with speeds, the best guarantee published before 1988 was a relative error of 40 percent (Friesen and Langston). Hochbaum and Shmoys (SIAM J. Comput. 17(3), 1988) closed the gap with a polynomial approximation scheme: for every , a polynomial-time algorithm whose schedule has makespan at most times the optimum. Since the problem is strongly NP-hard, no fully polynomial scheme exists unless P = NP, so this is the best guarantee of its kind.
There are machines with speeds and jobs with processing times ; job takes time units on machine . A schedule is a map from jobs to machines (no preemption), its makespan is
and is the least makespan over all schedules.
A schedule has makespan at most exactly when it packs pieces of sizes into bins of sizes . A packing is truly feasible if every bin holds total size at most its own size, and -relaxed feasible if every bin holds at most times its size. An -relaxed decision procedure returns, on every instance with positive sizes, either an -relaxed feasible packing or the answer "none", and answers "none" only when no truly feasible packing exists.
The binary search of §2 starts from , and the schedule with all jobs on a fastest machine. At each iteration it runs a decision procedure on the deadline- instance, , and sets (keeping the packing returned as the current schedule) or . It runs for iterations and outputs the current schedule.
The decision procedure of §3 is all-pack, run with a parameter , an integer. It sorts the bins by non-increasing size and normalizes sizes so that the largest bin is . Sizes are grouped into geometric intervals , and a piece in interval is rounded down to . The procedure builds a multilayered graph whose nodes are state vectors: the counts of remaining pieces of the current bin interval and the next, by rounded size, and three slack counters in units , capped at . Configuration arcs pack one bin and update arcs pass from one bin interval to the next. all-pack answers with a packing traced from a path from "initial" to "success", or "none" if no packing can be traced. Its choices (ties, the path, which pieces fill a configuration, where small pieces go) are arbitrary.
For every there are and , depending only on , such that for every instance (, , ):
Here is the output of the binary search driven by . The goal fixes no exponent: it asserts the shape of the result (approximation ratio , polynomial size for fixed ), not the constants of Theorem 2.
The rounding bound ; Lemma 1 (node count ); Lemma 2 (out-degree ); Corollary 2 (arc count ); Lemma 3 (a truly feasible packing gives an initial–success path); the proof of Lemma 4 (every packing traced from a path is -relaxed feasible) and Lemma 4 as printed; the sentence of p. 549 that all-pack is a -relaxed decision procedure; and Theorem 1 (binary search with an -relaxed procedure is an -approximation).
The scheme settles the approximability of up to the exponent's dependence on . Its framework, the dual approximation approach, reduces approximate optimization to a relaxed decision problem: a procedure that may overfill bins slightly but never wrongly declares infeasibility. That framework reappears in Lenstra–Shmoys–Tardos for unrelated machines and in later schemes for bin packing and scheduling. The rounding-and-layered-graph technique of §3 is a template for dynamic programs over rounded item classes.
The result is proved on paper; no formalization of it is known. The platform has the Lenstra–Shmoys–Tardos scheme for a fixed number of unrelated machines, list scheduling, and Graham's LPT bound for identical machines. It has nothing for machines with speeds. A formalization would provide a checked binary-search/relaxed-decision framework over real deadlines, and a verified account of the state-vector bookkeeping of all-pack. Two printed claims need repair (below), so a formal proof also settles exactly which statements hold.
The definitions are elementary, but the bookkeeping is not. The slack counters of a state vector are kept in three different units, and the update arc re-expresses them for the next interval that contains bins. That interval may be one, two, or many intervals away, and each case consumes a different slack pool. Lemma 3 is an induction over stages: a truly feasible packing has to be read as a path whose capped counters still dominate the true slack. The proof writes "the reader can verify with little difficulty" and "the remaining cases … follow by similar calculations". Lemma 4 runs the other way, and the bound per bin depends on the granularity of rounded sizes and of usable slack.
Several printed details do not survive a literal reading. The rounding produces values per interval, while the state vectors of p. 544 have entries (finding F4). The packing rule of Lemma 4 places only the pieces of the current interval, although update also consumes pieces of later intervals (F5). Theorem 1 is false for (F1). The exponent of Theorem 2 is not what its derivation gives (F2).
Jobs and machines are indexed by Fin n and Fin m; schedules and packings are maps Fin n → Fin m, empty bins allowed. The makespan is a finite supremum over machines, and optimality is stated by comparison with every schedule . The deadline- instance has bins (not sizes rescaled by ). The paper's "log" is base 2, rounded up, and when negative. The binary search outputs the schedule kept with the final upper bound. A relaxed decision procedure is constrained on instances with positive sizes.
The paper's is split in two: is the target accuracy and the parameter of all-pack. This builds in the standing assumption that is a positive integer, and is . The §3 lemmas assume, as hypotheses, sorted bins normalized to and pieces in ; all-pack sorts and normalizes itself, so Theorem 1, the p. 549 statement and the goal carry no sortedness hypothesis. State vectors are indexed by the rounding classes. The slack counters take values , the top value standing for every multiple above (saturating addition). The first layer holds only the initial node, and success arcs leave the last stage when update with succeeds, which is the variant p. 546 calls simpler. The enormous bins are those of intervals (the printed "" on p. 548 is a typo). all-pack is a relation: it may output any packing traced from an initial–success path, and answers "none" exactly when no packing can be traced. Every is an explicit placed before the parameter and the instance, with in place of .
The goal is not "some schedule is -optimal", which an optimal schedule satisfies trivially. Its algorithm is the binary search driven by every resolution of all-pack, never an arbitrary relaxed decision procedure. Its constants are fixed before the instance, and the counter cap and the classes are part of the definitions, so the graph is finite and Lemma 3 is not false.
Beyond the paper. One variant item is posed: theorem_1_corrected (kind corrected, finding F1) adds to Theorem 1 and changes nothing else. For , eight identical machines and 128 jobs of size , a valid -relaxed procedure can drive the binary search to makespan , while for the bound holds. Theorem 1 itself stays as printed; a disproof of it is a legitimate result.
Contributions welcome: proofs of the milestones, in particular Lemma 3 (the stage induction) and the tracing argument of Lemma 4, and reusable lemmas about the binary search over real deadlines. The definitions of packings, relaxed decision procedures and the binary search can be reused by later missions on dual approximation.
Submodular function minimization asks for a subset of a finite set that minimizes a set function satisfying . Cut functions, matroid rank functions and entropy are submodular, and minimizing them is a subroutine in dynamic flows, facility location and source coding. Grötschel, Lovász and Schrijver showed in 1981–1988 that the problem is solvable in (strongly) polynomial time by the ellipsoid method, which is neither combinatorial nor practical. Whether a combinatorial strongly polynomial algorithm exists remained open until 1999, when two were found independently: one by Schrijver (J. Combin. Theory B 80, 2000) and one by Iwata, Fleischer and Fujishige (arXiv:math/0004089; J. ACM 48(4), 2001). This mission formalizes the second.
Let be a finite nonempty set with , and submodular with . For write and . The base polyhedron is . A linear ordering of generates the extreme base (the greedy algorithm). The exchange capacity is the largest with .
The scaling algorithm (§3) keeps , a convex combination of extreme bases generated by orderings , a skew-symmetric flow with , and with . A -scaling phase halves , clips , and then alternates pushes (exchange operations on a pair that is active: is not reachable from in the residual graph , but its successor in is) with augmentations of units along residual paths from to , each followed by a reduction of the convex combination to affinely independent .
The procedure Fix (§4) runs scaling phases from and an extreme base and returns an element with . The algorithm of Figure 3 keeps a digraph of compatible pairs ( for every minimizer ), lets be the set reachable from in and , computes , and in each iteration calls Fix on or from an extreme base generated by an ordering consistent with . It then adds an arc, contracts a cycle, or deletes and adds it to the output.
There is an absolute such that for every and every submodular with :
Lemma 2.1 (exchange capacity of an adjacent swap); Lemmas 3.1, 3.2, 3.3 (tightness of , relaxed weak and strong duality); the bound on augmentations per phase (§3.3); Lemma 4.1 (proximity); the Fix paragraph (§4, p. 12); the consistent-base bound and the case (p. 13); the two cases of an iteration (p. 13); and at most calls of Fix (proof of Theorem 4.2).
The result. The theorem gives a minimizer of any real submodular function using a number of operations bounded by a polynomial in alone, independent of the function's values, by combinatorial means (augmenting paths and exchanges, no ellipsoid). Its two ideas, scaling on a complete auxiliary graph and proximity-based fixing of elements, recur in later SFM algorithms such as Orlin 2009.
Formalizing it. The result is proved on paper and has no machine-checked proof. A formal proof would certify the correctness, termination and step bound of a concrete combinatorial algorithm over the reals, including the scaling-phase invariants, which the printed text gets slightly wrong in two places (see Beyond the paper). Schrijver's algorithm has a separate mission; the two share only the base-polyhedron layer.
The bound is a product of four counts (Fix calls, phases per call, augmentations per phase, pushes per augmentation), and each needs its own invariant. The phase count needs Lemma 4.1, whose proof relies on Edmonds' vector-reduction theorem (a base with ), which is not in Mathlib. The augmentation count chains Lemma 3.3 at , the rounding loss when clipping, and Lemma 3.2. The push count needs a potential that survives the growth of between augmentations; the printed argument does not hold as written. The bound on Fix calls needs a monotone potential across contractions and deletions, which change the ground set and the function. Correctness needs, as invariants of every reachable state, that arcs are compatible, the deleted sets lie in every minimizer, the cap is harmless, and the digraph stays acyclic so consistent orderings exist.
V : Finset α of an ambient type, with read on subsets of and vectors α → ℝ vanishing off in . The algorithm of Figure 3 runs on Fin n. Its current vertices are disjoint blocks of original elements, the current function is of the union, contraction merges blocks, and deletion replaces by .ec is the supremum form of (2.1).fix_finds_element_corrected replaces the Fix paragraph's phases by : the printed count gives only , and for , , , no element satisfies after one phase. [Sharpness probe] lemma_3_3_probe is Lemma 3.3 under the end condition printed in Figure 1 (, or ). It is false for the modular with values on two points with , where , and .Finset; Edmonds' vector reduction; Carathéodory's theorem (in Mathlib). The phase invariants and base-polyhedron lemmas are reusable for other SFM missions. Proofs of single milestones are welcome.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.
Ellipsoids are the simplest convex bodies that can approximate an arbitrary convex set to within a factor depending only on the dimension. They are used for exactly that in control (reachable sets of linear systems), robust optimization (uncertainty sets) and the ellipsoid method. A linear system with illustrates the need. Its reachable set grows by an arithmetic sum at every step, so an ellipsoidal description of it requires approximating a sum of ellipsoids by a single ellipsoid, recursively and cheaply.
Timeline. Fritz John (1948) proved that every convex body has a unique maximal-volume inscribed ellipsoid and a unique minimal-volume circumscribed one, each within a factor ( for symmetric bodies) of the body; the circumscribed case goes back to Löwner. Boyd, El Ghaoui, Feron and Balakrishnan (1994) gave semidefinite programs whose solutions are ellipsoids that provably contain a sum of ellipsoids. Nesterov (1998) and Ye (1999) proved a approximation bound for semidefinite relaxations of quadratic maximization with commuting constraint matrices. Ben-Tal and Nemirovski (2001), Lecture 4, §4.9, combine the last two: the semidefinite outer ellipsoid of a sum of ellipsoids has volume at most times that of the smallest one.
All objects live in , with .
produces, from each feasible solution with , an ellipsoid .
Let be any optimal solution of . Let be such that is the smallest-volume full-dimensional ellipsoid containing . Then
This is the book's ratio in product form.
The goal is a quantitative guarantee for a tractable surrogate. Computing the smallest ellipsoid containing a sum of ellipsoids is believed hard when is part of the input. A single semidefinite program gives an ellipsoid within a factor in average linear size, uniformly in and . The reachable-set recursion of the motivating example therefore loses at most a fixed factor per step. Proposition 4.10.5 is also the textbook instance of a constant-factor semidefinite relaxation bound for quadratic maximization, used well beyond this chapter.
All results are proved in the book, except Theorem 4.9.1 (Exercise 4.71) and Proposition 4.10.5 (Exercise 4.58 from Exercise 4.38). Some ellipsoid results already exist as Lean statements on Prove2Me, in the Boyd–Vandenberghe convex optimization series: existence, uniqueness and -rounding of the Löwner–John ellipsoid of a finite point set. None of the statements here is formalized there. In particular, nothing exists for general solids, the inscribed ellipsoid, the symmetric factor, sums of ellipsoids, or the Nesterov–Ye bound.
The goal's statement is short, but its proof crosses several fields. The obvious idea, comparing with directly, fails: is in general not of the form produced by , since only reaches ellipsoids certified by a semidefinite relaxation. Closing that gap requires the full Nesterov–Ye bound for a quadratic maximization over the product of the . That bound is itself a substantial theorem, which the book proves only through a chain of exercises. Mathlib has volumes, determinants and positive semidefinite matrices. It has no Löwner–John theory for convex bodies, no Schur-complement LMI calculus for block matrices over sum types, and no semidefinite duality.
The book's Proposition 4.9.6 is false as printed. Its constraint admits every . For , , , , the ellipsoid is while . A corrected variant adds .
Vectors are Fin n → ℝ, and matrices are Matrix (Fin n) (Fin q) ℝ. and are Mathlib's PosSemidef and PosDef, which include symmetry. The unit ball is written with the dot product, because Mathlib's metric ball on Fin n → ℝ is a cube. Volume is Mathlib's volume divided by the volume of the Euclidean unit ball, valued in , so flat ellipsoids have volume . is Real.rpow. The block matrices are indexed by Fin m × Fin n. Optimal values appear only as explicit predicates: optimal = feasible with maximal objective, least upper bound, attained minimum.
In the goal, enters through hypotheses: , , and no full-dimensional ellipsoid with any centre that contains has smaller volume. These hypotheses are satisfiable, by Theorem 4.9.1 and the central symmetry of , so the goal is not vacuous. Volume is the measure-theoretic volume, not a formula in assumed as a definition: a formalization that defines the volume of as for every would not be the book's statement.
Two variants accompany the faithful statements. The first, [Corrected] Proposition 4.9.6, adds , following finding F1. A Lean disproof of the printed statement on the instance above exists locally. The second, [Strengthened] Proposition 4.9.5, drops the minimality of (finding F2): the printed proof uses only and . Proofs of either variant, and disproofs of the printed Proposition 4.9.6, are welcome.
A complete development needs: Lebesgue volume of linear images ( scaling); Schur complements for symmetric block matrices; semidefinite weak and strong duality, at least for the strictly feasible case; simultaneous diagonalization of commuting symmetric matrices; and the relaxation bound itself. The last four are reusable across the series' Lecture 4 missions.
Many combinatorial and nonconvex problems can be written as the maximization or minimization of a quadratic form under quadratic constraints. Such problems are NP-hard in general, but each has a semidefinite relaxation: a convex problem over positive semidefinite matrices, solvable to any accuracy in polynomial time, whose optimal value bounds the original one. The relaxation is useful exactly to the extent that this bound is tight, and the quality of the bound is measured by an explicit approximation ratio.
Lecture 4 of Ben-Tal and Nemirovski, Lectures on Modern Convex Optimization (SIAM, 2001), develops this theory from first principles and proves the two classical ratios. The history it follows:
This mission formalizes the book's statements of these results.
Let be a real symmetric matrix and let be the set of vectors with every coordinate equal to or . The quadratic sign problem (4.3.17) is
and its semidefinite relaxation (4.3.18) is
where means that is symmetric positive semidefinite. Every gives the feasible matrix , which is why . For a matrix , denotes the matrix with entries .
The MAXCUT problem (4.3.14) with weights is , with relaxation (4.3.15) . The constant is the largest with for all .
The general quadratically constrained problem (4.3.5) minimizes subject to , . Its Lagrangian lower bound (4.3.9) and Shor's relaxation (4.3.11) are semidefinite programs built from the bordered matrices .
Finally, the setting (SL.??) of the exercises takes a system , , with , the value , the relaxation value , and the dual (SDD) .
For every positive semidefinite ,
The constant is the book's, stated exactly.
Nesterov's theorem was the first constant-factor guarantee for semidefinite relaxation of a quadratic program whose objective is not a cut function, and it holds for every positive semidefinite form, including those arising in graph partitioning and in robust optimization. Together with the Goemans–Williamson theorem it underlies the matrix cube theorem and the approximate S-lemma later in the book, and the general logarithmic bound of Proposition 4.10.6 is the template for many approximation results in robust and chance-constrained optimization.
All statements of this mission are proved in the literature. On Prove2Me, a Goemans–Williamson statement exists in another form (the expected value of Gaussian rounding against the integer optimum, with constant ), and a constant-factor bound for the same objects as the goal exists with a much weaker constant ( with , via Grothendieck's inequality). Neither the factor nor the exact constant nor the bounds of Propositions 4.10.5–4.10.6 has a machine-checked statement or proof. Formalizing them also yields reusable infrastructure: optimal values of semidefinite programs as explicit predicates, the elliptope , and entrywise matrix functions.
The upper bounds (, Propositions 4.3.1–4.3.2) are the routine part. The lower bounds compare a continuous relaxation with a discrete optimum, and the book's constants (, , , ) leave no slack: an argument that loses any constant factor proves a different theorem. No feasible matrix of the relaxation is in general close to a rank-one matrix with , so the obvious idea of reading a sign vector off an optimal directly gives no factor at all. The objects involved also go beyond what Mathlib packages: optimal values of semidefinite programs, entrywise transcendental functions of matrices, and, for Propositions 4.10.5–4.10.6, duality between (SDP) and (SDD).
Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and is Mathlib's Matrix.PosSemidef, which includes symmetry. The matrices of §4.3.1 are indexed by Unit ⊕ Fin n. Optimal values are never a bare sSup: a maximization's optimal value enters as the hypothesis that a real number is the least upper bound of the objective over the feasible set, and these sets are nonempty and bounded, so the hypotheses are satisfiable for every instance. The optimal values of §4.3.1, which can be , are infima and suprema in EReal. The constant is defined as the exact infimum , never a decimal. The ratio of (4.3.16) is stated in product form, and : with Lean's convention , a ratio would make the all-zero-weight instance meaningless, and the product form rules out that trivialization. The book's standing conditions (symmetric data; in (SL.??)) are explicit hypotheses.
Contributions welcome: compactness of the elliptope and attainment of SDP values, rotation-invariant measures on spheres in Fin n → ℝ, entrywise functions of positive semidefinite matrices (Mathlib has the Schur product theorem, Matrix.PosSemidef.hadamard), and conic duality for (SDP)/(SDD). These are reusable well beyond this chapter.
Beyond the paper. One sharpness probe accompanies the goal: Nesterov's theorem with "" weakened to " symmetric". It is false (finding F3: for , , and fails); its disproof is the sought outcome.
Many questions in robust control and robust optimization reduce to one test: does a whole family of symmetric matrices, generated by perturbing a nominal matrix along several directions at once, stay positive semidefinite? A linear system whose coefficients are only known to lie in intervals is a typical case. Showing that one quadratic Lyapunov function certifies stability of every member of such an interval matrix comes down to exactly this test. Ben-Tal and Nemirovski isolate it as the Matrix Cube problem. The problem is NP-hard (Ben-Tal & Nemirovski, On tractable approximations of uncertain linear matrix inequalities affected by interval uncertainty, SIAM J. Optim. 12 (2002)). They prove that a simple semidefinite sufficient condition is never far from exact. The gap is controlled by a universal factor that depends only on the ranks of the perturbation directions.
This mission formalizes that result as it appears in §4.4.3 of Lectures on Modern Convex Optimization (Ben-Tal & Nemirovski, SIAM 2001), pp. 189–197, together with the lemmas its proof uses and its application to interval Lyapunov stability.
Matrices are real. is the space of symmetric matrices, its positive semidefinite cone, and means . For , is its vector of eigenvalues, so is the sum of their absolute values.
Fix with . For a level the matrix cube is
the image of the cube under an affine map. The Matrix Cube problem asks for the largest with .
The system of LMIs in symmetric variables is
Its feasibility can be checked by semidefinite programming. The largest for which it is solvable is , the optimal value of the semidefinite problem (4.4.45).
The approximation factor is the function
where is the standard Gaussian density on . The relevant rank is ; is not included.
For the application, is a stable matrix (all eigenvalues in the open left half-plane). has nonnegative entries, and is the interval matrix. asks for with for all , and is the supremum of the for which it is solvable. is the analogue of for this cube. It uses matrix variables and for , and is its supremum.
For all , all , all and all :
and
The result. Proposition 4.4.5 and Theorem 4.4.1 together bound the cube radius. It lies between the efficiently computable and . The factor is in general, independent of and , and exactly when every perturbation has rank at most two. Rank two is the situation of interval matrices, of Lyapunov certificates for interval systems (Proposition 4.4.6), and of a re-derivation of Nesterov's theorem for quadratic maximization over the unit cube (pp. 200–201). The same estimate underlies tractable approximations of robust LMIs with box uncertainty in robust semidefinite optimization.
Formalizing it. The results are proved in the book. None of them, and nothing on the matrix cube, the function or interval Lyapunov stability, is machine-checked on the platform. The formalization adds three things: a checked definition of as a Gaussian integral; a checked proof of the constants and ; and a checked bridge from semidefinite duality to a probabilistic rounding argument. The proof of Proposition 4.4.5 already has a sorry-free local check, which also exposed a sign slip in the printed proof.
The sufficient direction is elementary. The converse is not. Unsolvability of is a statement about a semidefinite program, and turning it into an explicit point with and needs three ingredients:
Bounding coordinate by coordinate, or using a worst-case vertex of the cube, gives a factor that grows with . The rank-dependent constant is what makes the theorem useful.
The constants need real analysis on Gaussian integrals. requires an exact minimization of over . The bound requires a symmetrization and an independence argument. Lemma 4.4.4 needs rotational invariance of the Gaussian measure and diagonalization inside an integral.
Matrix (Fin n) (Fin n) ℝ, and is (X - Y).PosSemidef (which includes symmetry). The index is Fin m, and is for every .CFC.sqrt W under MatrixOrder. Eigenvalues are Mathlib's IsHermitian.eigenvalues, used only through order-independent quantities.EReal, so is represented. Ratios are stated in product form, for example . The "max" in (4.4.45) is stated as attained.A formalization that replaced by an arbitrary function satisfying (4.4.37), or set , or allowed , would state a different (false or ill-posed) theorem; the statements here rule these out.
Infrastructure needed and reusable beyond this mission:
Contributions of separate lemmas are welcome, for example monotonicity of or .