All missions

Motivation

Data-dependent risk bounds in statistical learning theory control the gap between the expected loss of a learned function and its empirical loss by a complexity penalty that is computed from the training data. The first such penalties were the maximum discrepancy of a function class (Bartlett, Boucheron and Lugosi, Model selection and error estimation, Machine Learning 48, 2002) and its Rademacher complexity (Koltchinskii, Rademacher penalties and structural risk minimization, IEEE Trans. Inf. Theory 47, 2001; Koltchinskii and Panchenko 2000). The maximum discrepancy compares the behaviour of the class on two fixed halves of the sample; the Rademacher complexity compares it on two random halves. Bartlett and Mendelson (JMLR 3, 2002), Lemma 3, show that these two quantities are equivalent up to a factor 2 and an additive $O(1/\sqrt n)$. This mission formalizes that lemma from the published JMLR article (pp. 463–482); the proof is its Appendix A.

Setting

Let $\mu$ be a probability measure on a measurable space $\mathcal X$ and let $X_1,\dots,X_n$ be independent samples from $\mu$. Let $F$ be a class of measurable functions $f:\mathcal X\to[-1,1]$. Let $\sigma_1,\dots,\sigma_n$ be independent uniform $\{\pm1\}$-valued random variables, independent of the sample.

The Rademacher complexity of $F$ is

$$R_n(F) = \mathbf E\sup_{f\in F}\left|\frac2n\sum_{i=1}^n\sigma_i f(X_i)\right|.$$

For even $n$, the maximum discrepancy of $F$ is the random variable

$$\hat D_n(F) = \sup_{f\in F}\left(\frac2n\sum_{i=1}^{n/2}f(X_i) - \frac2n\sum_{i=n/2+1}^n f(X_i)\right),$$

with no absolute value, and the expected maximum discrepancy is $D_n(F)=\mathbf E\hat D_n(F)$. The class is closed under negation if $f\in F$ implies $-f\in F$, and $-F=\{-f:f\in F\}$.

The proof works with the conditional supremum function

$$s(N) = \frac2n\,\mathbf E\left[\sup_{f\in F}\sum_{i=1}^n\sigma_i f(X_i)\;\middle|\;\sum_{i=1}^n\sigma_i=N\right],$$

defined for the values $N$ that $\sum_i\sigma_i$ can take.

Formalization targets

Goal: Lemma 3, first and second displays

For every even $n\ge2$,

$$\frac{R_n(F)}{2} - 2\sqrt{\frac2n} \le D_n(F) \le R_n(F) + 4\sqrt{\frac2n},$$

and if $F$ is closed under negation,

$$R_n(F) - 4\sqrt{\frac2n} \le D_n(F).$$

Milestones (Appendix A, pp. 479–480)

1. $R_n(F)\ge\mathbf E\,s(\sum_i\sigma_i)$, with equality when $F$ is closed under negation.
2. $D_n(F) = s(0)$.
3. $|s(N_1)-s(N_2)|\le 4|N_2-N_1|/n$.
4. $|\mathbf E s(N)-s(\mathbf EN)|\le\mathbf E|s(N)-s(\mathbf EN)|\le4\sqrt{2/n}$ for $N=\sum_i\sigma_i$.
5. $R_n(F)=R_n(F\cup-F)\le D_n(F\cup-F)+4\sqrt{2/n}$.
6. $D_n(F\cup-F)\le 2D_n(F)+D_n(\{f_0,-f_0\})$ for any $f_0\in F$ (a corrected form of the printed step, see below).

Significance

Lemma 3 makes the maximum discrepancy and the Rademacher complexity interchangeable in risk bounds: a bound in terms of one gives a bound in terms of the other with an explicit additive loss. The maximum discrepancy can be computed by a single empirical risk minimization on a relabelled sample, while the Rademacher complexity has the structural properties (monotonicity, convex-hull invariance, contraction) that make it easy to bound for concrete classes; the lemma transfers the second kind of estimate to the first quantity.

The lemma is proved in the paper; no machine-checked proof of it, or of the comparison between fixed and random half-sample splits, is known to exist. Formalizing it requires the exchangeability argument for i.i.d. samples, the conditioning of a uniform sign vector on its sum, and a moment bound for the Rademacher sum $\sum_i\sigma_i$, all with explicit constants.

Difficulty

The heart of the proof is that, conditioned on the number of positive signs, a uniform sign vector splits the i.i.d. sample into two random subsets of fixed sizes, and every split of the same sizes has the same law as the fixed split. Making this precise requires a permutation-invariance argument for product measures applied to a supremum over an arbitrary class, where measurability is not automatic. The step from classes closed under negation to general classes is where the printed argument is loose: since $\hat D_n$ has no absolute value, $\hat D_n(F\cup-F)$ is a maximum of two suprema that may be negative, and the naive bound $D_n(F\cup-F)\le2D_n(F)$ fails.

Formalization scope

The Lean development lives in the namespace RadGauss.Discrepancy. Sign vectors are Fin n → Bool (true ↦ 1, false ↦ -1) and expectations over signs are finite averages over all $2^n$ sign vectors; $s(N)$ is the average over the sign vectors with sum $N$. $R_n$ takes values in $[0,\infty]$ (a lower Lebesgue integral of an $[0,\infty]$-valued supremum), while $\hat D_n$, $D_n$ and $s$ are real, because the maximum discrepancy is signed. Inequalities of the form $a-c\le D$ are written $a\le D+c$ with real terms embedded by ENNReal.ofReal; this is equivalent to the printed form since $D_n(F)\ge0$ for nonempty $F$.

Hypotheses added to the page, all disclosed in each item:

• the sample size is even, $n=2m$ with $m\ge1$, since $\hat D_n$ needs half sums;
• $F$ is nonempty (the supremum over the empty class is $-\infty$ in the paper and $0$ in Lean);
• every $f\in F$ is measurable, and for every sign vector $\sigma$ the map $x\mapsto\sup_{f\in F}\sum_i\sigma_if(x_i)$ is measurable. This is the measurability guard: without it the Bochner integrals defining $D_n$ and $s$ would silently be $0$.

Corrections of printed statements:

• The Lipschitz bound on $s$ is printed for $0\le n_2<n_1\le n$ but used for negative values of $\sum_i\sigma_i$; it is stated for every pair of attainable values.
• The printed step $D_n(F\cup-F)\le2D_n(F)$ is false for the signed $\hat D_n$ of p. 464 ($F=\{f\}$, $f(X)$ uniform on $\{\pm1\}$, $n=2$ gives $1\le0$); the milestone states it with the additional term $D_n(\{f_0,-f_0\})\le2/\sqrt n$. The goal itself remains true.
• The third display of Lemma 3, $P\{|\hat D_n(F)-D_n(F)|\ge\epsilon\}\le2\exp(-\epsilon^2n/2)$, is false as printed ($F=\{f\}$ as above, $n=2$, $\epsilon=2$: the probability is $1/2>2e^{-4}$) and is not part of the mission.

A formalization in which $D_n$ or $s$ is a junk value (non-integrable or non-measurable suprema, an empty class, an odd sample size with truncated $n/2$) would make the goal trivial or meaningless; the hypotheses above rule that out, and the class $F=\{0\}$ satisfies all of them.

Welcome contributions include general lemmas on the invariance of $\mathbf E\sup_{f\in F}\Phi_f(X_{\pi(1)},\dots,X_{\pi(n)})$ under permutations $\pi$ of an i.i.d. sample, conditioning of uniform sign vectors on their sum, and the bound $\mathbf E|\sum_i\sigma_i|\le\sqrt n$. These are reusable well beyond this mission.

Selected references

• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002) 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
• P. L. Bartlett, S. Boucheron, G. Lugosi, Model selection and error estimation, Machine Learning 48 (2002) 85–113. https://doi.org/10.1023/A:1013999503812
• V. Koltchinskii, Rademacher penalties and structural risk minimization, IEEE Transactions on Information Theory 47 (2001) 1902–1914. https://doi.org/10.1109/18.930926
• L. Devroye, L. Györfi, G. Lugosi, A Probabilistic Theory of Pattern Recognition, Springer, 1996. https://doi.org/10.1007/978-1-4612-0711-5

Motivation

Kernel methods, such as support vector machines, predict with functions of the form $x \mapsto \sum_i \alpha_i k(x, x_i)$: finite expansions of a fixed similarity function $k$ centred at data points. Their statistical behaviour is governed by the size of the class of such expansions that the method searches. Bartlett and Mendelson, in Rademacher and Gaussian Complexities: Risk Bounds and Structural Results (JMLR 3, 2002), develop risk bounds in terms of the Rademacher and Gaussian complexities of a class, and in §4.3 (pp. 476–478) compute these complexities for the class of kernel expansions whose coefficient vector has quadratic form $\alpha' K \alpha \le B^2$. The resulting bound depends on the kernel only through its diagonal $k(x,x)$, which is what makes margin bounds for support vector machines dimension-free. This mission formalizes that computation. The source is the published JMLR article (pages cited by the journal's printed numbers).

Setting

Let $\mathcal X$ be a compact topological space. A kernel is a continuous function $k : \mathcal X \times \mathcal X \to \mathbb R$ such that for every $m$ and all $x_1, \dots, x_m \in \mathcal X$ the Gram matrix $K_{ij} = k(x_i, x_j)$ is symmetric and positive semidefinite. For $B \ge 0$ the class of kernel expansions is

$$F = \Big\{x \mapsto \sum_{i=1}^m \alpha_i k(x, x_i) : m \in \mathbb N,\ x_i \in \mathcal X,\ \alpha_i \in \mathbb R,\ \sum_{i,j}\alpha_i\alpha_j k(x_i, x_j) \le B^2\Big\},$$

with centres anywhere in $\mathcal X$ (Lean: kernelClass k B).

For a class $F$ of real functions on $\mathcal X$ and a sample $x_1, \dots, x_n$, let $\sigma_1, \dots, \sigma_n$ be independent uniform signs and $g_1, \dots, g_n$ independent standard Gaussians. The empirical Rademacher complexity and empirical Gaussian complexity (Definition 2, p. 464) are

$$\hat R_n(F) = \mathbb E_\sigma \sup_{f\in F}\Big|\frac2n\sum_{i=1}^n \sigma_i f(x_i)\Big|, \qquad \hat G_n(F) = \mathbb E_g \sup_{f\in F}\Big|\frac2n\sum_{i=1}^n g_i f(x_i)\Big|.$$

For a probability measure $\mu$ on $\mathcal X$ and an i.i.d. sample $X_1, \dots, X_n \sim \mu$, the Rademacher complexity is $R_n(F) = \mathbb E \hat R_n(F)$ and the Gaussian complexity is $G_n(F) = \mathbb E \hat G_n(F)$ (Lean: empiricalRademacher, empiricalGaussian, rademacherComplexity, gaussianComplexity).

A feature map of $k$ is a map $\Phi : \mathcal X \to \mathcal H$ into a real Hilbert space with $k(x_1, x_2) = \langle \Phi(x_1), \Phi(x_2) \rangle$.

Formalization targets

Goal: the expected complexity bound (§4.3, p. 478, display after the proof of Lemma 22)

With $X \sim \mu$,

$$R_n(F) \le 2B\sqrt{\frac{\mathbb E\, k(X,X)}{n}}, \qquad G_n(F) \le 2B\sqrt{\frac{\mathbb E\, k(X,X)}{n}}.$$

Milestone 1: feature-map inclusion (p. 477)

For any feature map $\Phi$ of $k$, $\|\sum_i \alpha_i \Phi(x_i)\|^2 = \sum_{i,j}\alpha_i\alpha_j k(x_i,x_j)$, and hence $F \subseteq \{x \mapsto \langle w, \Phi(x)\rangle : \|w\| \le B\}$.

Milestone 2: Lemma 22 (p. 477)

For every sample $X_1, \dots, X_n$,

$$\hat G_n(F) \le \frac{2B}{n}\sqrt{\sum_{i=1}^n k(X_i, X_i)}, \qquad \hat R_n(F) \le \frac{2B}{n}\sqrt{\sum_{i=1}^n k(X_i, X_i)}.$$

Significance

The goal shows that the kernel class has complexity of order $n^{-1/2}$, with a constant given by $B$ and the quantity $\mathbb E\, k(X,X)$, which is the trace of the integral operator $T_k f = \int k(\cdot, y) f(y)\, d\mu(y)$ on $L_2(\mu)$. No dimension of the feature space enters. Fed into the paper's margin-cost risk bound (Theorem 21, p. 476), the sample-wise Lemma 22 gives a data-dependent misclassification bound for support vector machines in terms of the trace of the Gram matrix of the training sample. Bounds of this form are the standard complexity estimate for kernel classes in learning theory textbooks.

The result is proved in the paper; nothing in this mission is open mathematics. What the mission adds is a machine-checked version with the paper's normalization (factor $2/n$, absolute value inside the supremum), covering both the Rademacher and the Gaussian complexity, for expansions with centres anywhere in $\mathcal X$. Related statements on the platform (Mohri et al.'s Theorem 5.10 and Proposition 9.3) use the $1/n$ normalization without absolute value, assume a uniform bound $\sup_x k(x,x) \le r^2$, and treat only the Rademacher case, so they do not imply the targets here.

Difficulty

The class $F$ is defined through the kernel, not through a feature map, and its expansions have arbitrarily many centres anywhere in $\mathcal X$. The supremum over $F$ is therefore a supremum over an infinite-dimensional family, and must be controlled without assuming a separate numerical upper bound on $k(x,x)$ or that the feature space is finite dimensional. For the Gaussian complexity the supremum sits inside an expectation over a continuous random vector, and the passage from the sample-wise bound to the expected bound must move an expectation inside a square root in the right direction. A bound with $\sup_x k(x,x)$ in place of $\mathbb E\, k(X,X)$ is weaker and is not the target.

Formalization scope

Conventions committed to in Lean:

• Complexities take values in $[0, \infty]$ (ℝ≥0∞); expectations over the Gaussian vector and over the sample are lower Lebesgue integrals against product measures, and the Rademacher expectation is the exact average over the $2^n$ sign vectors $\sigma : \mathrm{Fin}\,n \to \mathbb Z^\times$. An unbounded class has complexity $+\infty$, so a junk value of $0$ for a real supremum or a non-integrable expectation cannot make the bounds trivial.
• A kernel (IsKernel k) carries compactness of $\mathcal X$, joint continuity, and positive semidefiniteness (with symmetry) of every Gram matrix, as in the paper's definition. The goal puts the Borel $\sigma$-algebra on $\mathcal X$ and assumes $\mu$ is a probability measure; $\mathbb E\, k(X,X)$ is the Bochner integral of the continuous function $x \mapsto k(x,x)$.
• $B \ge 0$ is assumed in every statement (the paper fixes $B > 0$). For $B < 0$ the right-hand sides are negative while the left-hand sides are not, and the inclusion of milestone 1 fails.
• No $n \ge 1$ hypothesis: at $n = 0$ both sides of every bound are $0$ in Lean.
• The feature map in milestone 1 is a hypothesis (any real Hilbert space and any $\Phi$ with $k = \langle \Phi(\cdot), \Phi(\cdot)\rangle$); its existence is the RKHS theorem, referenced as the supporting platform item FoundationsML.Kernels.RKHS_exists.
• No measurability or integrability hypotheses on $\hat R_n(F)$ or $\hat G_n(F)$ are assumed, and none is needed.

A trivializing formalization is ruled out: the goal is stated for the kernel class $F$ itself, not for the larger ball of linear functionals of a feature map, and not for the subclass with centres at the sample points.

Infrastructure a complete development needs: Gaussian integration over $\mathbb R^n$ (second moments of a standard Gaussian vector), Jensen's inequality for the square root under a lower Lebesgue integral, and Cauchy–Schwarz for positive semidefinite bilinear forms (or the RKHS feature map). The Definition 2 complexities are shared with the paper's other missions and reusable. Contributions of any of these milestones, and of proofs of the goal that avoid the feature map, are welcome.

Selected references

• P. L. Bartlett and S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002), 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
• N. Cristianini and J. Shawe-Taylor, An Introduction to Support Vector Machines, Cambridge University Press, 2000. https://doi.org/10.1017/CBO9780511801389
• N. Aronszajn, Theory of Reproducing Kernels, Transactions of the American Mathematical Society 68 (1950), 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
• M. Mohri, A. Rostamizadeh and A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018. https://mitpress.mit.edu/9780262039406/

Motivation

Vertex connectivity measures how robust a network is against the failure of nodes. It can be measured in two ways that look different. One way counts the fewest nodes whose removal disconnects the network. The other counts the routes between two nodes that share no intermediate node. Whitney's theorem (1932) says that the two measures agree for every pair of nodes. It is the vertex form of Menger's theorem, and it underlies reliability analysis of communication and transportation networks, the design of fault-tolerant routing, and much of structural graph theory.

M. L. Balinski's 1961 paper On the graph structure of convex polyhedra in n-space proves that the graph of a bounded full-dimensional polyhedron in $n$-space is $n$-tuply connected (the subject of Mission I of this series). It then invokes Whitney's theorem to conclude that any two vertices of such a polyhedron are joined by $n$ disjoint paths. Balinski gives a short new proof of Whitney's theorem through the max-flow min-cut theorem of Ford and Fulkerson and of Dantzig and Fulkerson. That makes the theorem a consequence of linear programming duality. This mission formalizes that part of the paper: the network vocabulary, the max-flow min-cut theorem with capacities on both points and lines, the integrality of maximum flows, and Whitney's theorem itself.

Timeline.

• 1927: Menger states the disjoint-paths theorem for separating sets.
• 1932: Whitney proves the characterization of $n$-connected graphs by $n$ disjoint paths between every pair of points.
• 1956: Ford and Fulkerson and Dantzig and Fulkerson prove the max-flow min-cut theorem.
• 1961: Balinski derives Whitney's theorem from it with a unit-capacity network.

Setting

A graph $G$ consists of a finite set $V$ of points and a set of lines, each line being a pair of distinct points. A path from $p_s$ to $p_k$ is a sequence of lines $(p_1,p_2),(p_2,p_3),\dots,(p_m,p_{m+1})$ with $p_1 = p_s$, $p_{m+1} = p_k$ and $m \ge 1$. Paths are disjoint if they have no point in common except possibly their first and last points.

$G$ is $n$-tuply connected if it has at least $n+1$ points and, for every set $X$ of fewer than $n$ points, the graph $G - X$ remaining after deleting $X$ is connected. $G$ has $n$ disjoint paths from $p_s$ to $p_k$ if there are $n$ pairwise distinct paths from $p_s$ to $p_k$, none of which repeats a point, and no two of which share a point other than $p_s$ and $p_k$.

A network is a connected graph with a capacity $c(x) \ge 0$ on every point and $c(e) \ge 0$ on every line, and with a distinguished source $p_s$ and sink $p_k$. A flow assigns a number $f(C) \ge 0$ to every path $C$ from $p_s$ to $p_k$, such that for every point $x$ and every line $e$

$$\sum_{C \ni x} f(C) \le c(x), \qquad \sum_{C \ni e} f(C) \le c(e).$$

Its value is $\operatorname{val}(f) = \sum_C f(C)$. A disconnecting set is a pair $(X,F)$ of points and lines that meets every walk from $p_s$ to $p_k$. Its value is $\sum_{x\in X} c(x) + \sum_{e \in F} c(e)$.

The unit network of the proof has capacity $1$ on every point except $p_s$ and $p_k$, and capacity $n+1$ on every line except the line $p_sp_k$ (if present), which has capacity $1$. In Lean these are IsNTuplyConnected, HasNDisjointPaths, IsFlow, flowValue, IsDisconnecting, cutValue, unitCapV and unitCapE, all in the namespace Balinski61.Whitney.

Formalization targets

Goal: Whitney's theorem (p. 434)

For a finite graph $G$ with at least two points and any $n \ge 0$:

$$G \text{ is } n\text{-tuply connected} \iff \text{for all } p_s \ne p_k,\ G \text{ has } n \text{ disjoint paths from } p_s \text{ to } p_k.$$

Both directions are part of the goal.

Milestones, in the order of the proof

1. Max-flow min-cut (p. 433). In every network there is a number $M$ that is the value of some flow and of some disconnecting set, with every flow of value at most $M$ and every disconnecting set of value at least $M$.
2. Integrality (p. 434). If all capacities are integers, some maximum flow has only integer path flows.
3. Min-cut in the unit network (p. 434). If $G$ is $n$-tuply connected and $p_s \ne p_k$, every disconnecting set of the unit network has value at least $n$.
4. Paths from unit flows (p. 434). An integral flow of value at least $n$ in the unit network yields $n$ disjoint paths from $p_s$ to $p_k$.
5. Sufficiency (p. 434). If every pair of distinct points is joined by $n$ disjoint paths, $G$ is $n$-tuply connected.

Significance

Whitney's theorem turns a statement about all small deletion sets into the existence of explicit, verifiable path systems, and back again. In applications it certifies connectivity by exhibiting paths, and it certifies that connectivity is no larger by exhibiting a separating set. It is the base of the theory of $k$-connected graphs: ear decompositions, the fan lemma, and the structure of minimally $k$-connected graphs all use it. Inside this paper it supplies the COROLLARY that any two vertices of a bounded full-dimensional polyhedron in $n$-space are joined by $n$ disjoint edge paths.

None of these results is formalized for vertex connectivity at this Mathlib revision. Mathlib has edge connectivity and connected components but no vertex Menger theorem. The Prove2Me library has max-flow min-cut statements for arc capacities only and integrality results for basic solutions of network LPs, but no flow model with capacities on points. A completed development gives a reusable vertex-capacitated max-flow min-cut theorem for undirected graphs and the first machine-checked Whitney theorem in this library. The results are classical and proved; the remaining work is the formalization.

Difficulty

The sufficiency direction is elementary. The necessity direction needs a global object (a flow, or a family of paths) to exist from purely local hypotheses about deletions. The obvious induction on $n$, which deletes a point and applies the hypothesis to a smaller graph, does not keep the path systems disjoint. In Balinski's route the weight falls on max-flow min-cut and integrality for path flows with capacities on points, neither of which exists in the library. A second difficulty sits in a case the paper's proof skips: a disconnecting set of the unit network may use the line $p_sp_k$ (capacity $1$) together with up to $n-2$ points, and the deletion hypothesis of $n$-tuple connectedness speaks only about points.

Formalization scope

Graphs are Mathlib SimpleGraphs on a Fintype with decidable equality and adjacency. Paths are walks with IsPath. A flow is a real function on the finite type G.Path ps pk of simple paths; "through a point" and "through a line" mean membership in the walk's support and edge list. Capacities are functions V → ℝ and Sym2 V → ℝ. Nonnegativity, connectivity of $G$ and $p_s \ne p_k$ are hypotheses of the network theorems.

The following readings of loose phrases are explicit in the statements:

• "dropping out $n-1$ or fewer points" is $|X| < n$;
• "$n$ disjoint paths" means $n$ pairwise distinct simple paths. The printed path syntax permits repeated vertices; in a graph with lines $p_s a$, $p_s b$, and $p_s p_k$, the distinct walks $p_s,a,p_s,p_k$ and $p_s,b,p_s,p_k$ share only their endpoints even though the graph is not $2$-tuply connected. The theorem therefore uses its conventional simple-path reading;
• path flows live on simple paths (merging and shortcutting changes no maximum value);
• the paper leaves the capacities of $p_s$ and $p_k$ in the unit network unassigned, and here they are $n+1$;
• "the condition is sufficient is obvious" is the full statement that $n$-tuple connectedness follows;
• the hypothesis $|V| \ge 2$ is added to the goal and to sufficiency, because the paper's "any pair of points" presupposes it and the equivalence fails for a one-point graph.

The max-flow min-cut milestone states that the maximum and the minimum are attained. A statement that only bounds some flow by every cut is satisfied by the zero flow. A connectivity notion without the $n+1$ point count would make every complete graph $n$-connected for all $n$. Both trivializations are excluded.

Contributions welcome: a vertex-capacitated augmenting-path or LP-duality proof of max-flow min-cut for path flows, integrality by an augmenting-path argument, the unit-network lemmas, and direct combinatorial proofs of Whitney's theorem that bypass flows.

Selected references

• M. L. Balinski, On the graph structure of convex polyhedra in n-space, Pacific J. Math. 11 (1961), 431–434. https://doi.org/10.2140/pjm.1961.11.431
• H. Whitney, Congruent graphs and the connectivity of graphs, Amer. J. Math. 54 (1932), 150–168. https://doi.org/10.2307/2371086
• L. R. Ford, Jr. and D. R. Fulkerson, Maximal flow through a network, Canadian J. Math. 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
• G. B. Dantzig and D. R. Fulkerson, On the max-flow min-cut theorem of networks, in Linear Inequalities and Related Systems, Ann. of Math. Stud. 38, Princeton Univ. Press, 1956, 215–221. https://doi.org/10.1515/9781400881987
• K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927), 96–115. https://doi.org/10.4064/fm-10-1-96-115

Why price without knowing demand

A seller with a fixed stock of a single product and a finite selling season has to set prices without knowing how demand responds to them. This is the standard situation in revenue management: airline seats, hotel rooms, fashion goods and event tickets. The classical theory of dynamic pricing (Gallego and van Ryzin, 1994) assumes that the demand function $\lambda(p)$, the rate of purchase requests at price $p$, is known. In practice it has to be learned from sales, while the season runs and the stock is consumed.

Besbes and Zeevi (2009) asked how much revenue is lost for not knowing $\lambda$. They answered it with explicit policies and matching-order bounds. Their setting differs from the multi-armed bandit literature it borrows from in three ways:

• the problem is constrained by an initial inventory;
• the set of prices is a continuum;
• the set of possible demand functions is a nonparametric class.

This mission formalizes their first main result, Proposition 1: a simple learn-then-price policy has worst-case relative regret of order $(\log n)^{1/2}n^{-1/4}$ in a market of size $n$.

Setting

Prices. Fix $0<\underline p<\overline p<\infty$ and an off price $p_\infty>0$ outside $[\underline p,\overline p]$. The seller may charge any price in $[\underline p,\overline p]\cup\{p_\infty\}$; charging $p_\infty$ stops demand.

Demand. Requests arrive as a Poisson process whose intensity at time $t$ is $\lambda(p(t))$. Let $N$ be a unit-rate Poisson process. By the time change (1), the cumulative requests up to time $t$ under a price path $p(\cdot)$ are $N\big(\int_0^t\lambda(p(s))\,ds\big)$. The seller starts with inventory $x$ and sells until either the horizon $T$ ends or the stock runs out. The expected revenue of a policy $\pi$ is $J^\pi(x,T;\lambda)$.

Demand class. $\mathcal L=\mathcal L(M,\underline K,\overline K,m)$ is the set of regular demand functions satisfying Assumption 1. Regular means:

• $\lambda\ge0$ and $\lambda(p_\infty)=0$;
• $\lambda$ is non-increasing on $[\underline p,\overline p]$, with inverse $\gamma$;
• the revenue rate $r(l)=l\gamma(l)$ is concave.

Assumption 1 requires:

• (i) $\lambda\le M$ on $[\underline p,\overline p]$;
• (ii) $\lambda$ is $\overline K$-Lipschitz and $\gamma$ is $\underline K^{-1}$-Lipschitz;
• (iii) $\max_p p\lambda(p)\ge m$.

Benchmark. The deterministic relaxation (5) replaces the random demand by its mean:

$$J^D(x,T\mid\lambda)=\sup\Big\{\int_0^T p(s)\lambda(p(s))\,ds:\int_0^T\lambda(p(s))\,ds\le x\Big\}.$$

The regret of a policy is $\mathcal R^\pi=1-J^\pi/J^D$.

Scaling. In a market of size $n$ the inventory is $nx$ and the demand function is $n\lambda$, as in (11). The corresponding quantities are $J^\pi_n$, $J^D_n=nJ^D$ and $\mathcal R^\pi_n$.

Algorithm 1, $\pi(\tau,\kappa)$. The policy has three phases.

1. Learning. On $[0,\tau]$ it tests $\kappa$ equally spaced prices $p_i=\underline p+(i-1)(\overline p-\underline p)/\kappa$, each for $\Delta=\tau/\kappa$ time units. It estimates $\lambda(p_i)$ by the normalized request counts $\hat\lambda(p_i)$.
2. Optimization. It chooses $\hat p^u=\arg\max_i p_i\hat\lambda(p_i)$ and $\hat p^c=\arg\min_i|\hat\lambda(p_i)-x/T|$, and sets $\hat p=\max\{\hat p^u,\hat p^c\}$.
3. Pricing. It charges $\hat p$ on $(\tau,T]$ until the stock runs out.

Formalization targets

Goal: Proposition 1

Let $\tau_n\asymp n^{-1/4}$ and $\kappa_n\asymp n^{1/4}$, and let $\pi_n=\pi(\tau_n,\kappa_n)$. Then there is a finite constant $C$, independent of $\lambda$ and $n$, such that

$$\sup_{\lambda\in\mathcal L}\mathcal R^{\pi}_n(x,T;\lambda)\le\frac{C(\log n)^{1/2}}{n^{1/4}}\qquad(n\ge2).$$

The constant is left unspecified, as in the paper. Its dependence on the class parameters, $x$ and $T$ is "somewhat complex" (p. 12), and the order $(\log n)^{1/2}n^{-1/4}$ is the content of the result.

Milestones

The milestones follow the proof in the appendix, in order:

• the scaling $J^D_n=nJ^D$ (p. 12);
• Fact 1, $J^D\ge m\min\{T,x/M\}$ on $\mathcal L$;
• Lemma 1, the solution of (5): charge $p^D=\max\{p^u,p^c\}$ until the stock runs out;
• Lemma 2, a Poisson deviation bound;
• the revenue lower bound (A-2);
• Lemma 3, the learned price is near $p^D$ with high probability;
• Lemma 4 and the Case 1 bound (A-11), for $\lambda(\overline p)\le x/T$;
• Lemma 5 and the Case 2 bound (A-15), for $\lambda(\overline p)>x/T$;
• the Step 4 bound $\mathcal R^\pi_n\le C_{12}(u_n+\tau_n)$, where $u_n=(\log n)^{1/2}\max\{1/\kappa_n,(n\Delta_n)^{-1/2}\}$.

Significance

Proposition 1 shows that a seller who knows only a nonparametric class of demand functions can approach the full-information revenue uniformly over the class. Learning costs a vanishing fraction of revenue, and the policy needs no parametric model. Together with the paper's lower bound of order $n^{-1/2}$ for every admissible policy (Proposition 2, not in this mission), it brackets the minimax regret of nonparametric pricing under an inventory constraint. The result is a reference point for the learning-and-earning literature in operations management that followed it.

The result is proved in the paper; to our knowledge, it has no machine-checked proof. Formalizing it requires:

• a working theory of policies driven by a time-changed Poisson process, with sales capped by an inventory;
• the deterministic relaxation of Gallego and van Ryzin for a continuum of prices with an off price;
• uniform (over the class) Poisson concentration bounds.

The mission produces Lean statements of all of these. A proof would also check every constant chain of the appendix, where the argument uses some displays in a form slightly different from their printed statement (see the scope section).

Difficulty

The obvious argument controls the estimation error at the tested prices and concludes that $\hat p$ is close to the optimal price. It breaks in two places.

First, $p^D$ is the larger of two prices, the revenue maximizer and the price that sells the inventory exactly. Near the boundary between these regimes, the revenue rate at $\hat p$ is not controlled by the error in $\hat p$ alone: it needs the concavity of the revenue rate and the inverse Lipschitz bound on $\gamma$.

Second, when demand at the highest price exceeds the inventory rate ($\lambda(\overline p)>x/T$), the revenue is limited by stock-outs rather than by the price. The bound must then show that nearly all of the inventory is sold during the pricing phase, uniformly over the class.

Throughout, every constant must be independent of the demand function, so the estimates have to hold uniformly over an infinite-dimensional class.

Formalization scope

• Poisson process. The demand is driven by IsPoissonProcess N 1 on a probability space $(\Omega,\mathbb P)$, a published platform definition: ℕ-valued, $N(0)=0$, monotone paths, independent Poisson increments. The time change (1) is rendered by evaluating $N$ at cumulative intensities.
• Inventory. The inventory of the market of size $n$ is $\lfloor nx\rfloor$ units, and sales are $\min\{N(\cdot),\lfloor nx\rfloor\}$. The cap is never dropped.
• Revenue. $J^\pi_n$ is the Bochner expectation of a bounded, finitely-valued revenue, so it is a genuine integral.
• Demand functions. A demand function is a map $\mathbb R\to\mathbb R$, nonnegative, with $\lambda(p_\infty)=0$. Regularity and Assumption 1 are imposed on $[\underline p,\overline p]$, and the inverse $\gamma$ is Function.invFunOn.
• Benchmark. $J^D$ is a supremum over measurable price paths with integrable demand rate. The supremum is genuine: the set of path revenues is nonempty and bounded.
• Algorithm. The grid excludes $\overline p$, as in the paper. Ties in the grid argmax and argmin go to the smallest index. The estimates compare $\hat\lambda(p_i)$ with $x/T$.
• Tuning. $\tau_n\asymp n^{-1/4}$ and $\kappa_n\asymp n^{1/4}$ are encoded with explicit constants $0<c\le c'$, with $\tau_n\in(0,T]$ and $\kappa_n\ge1$. Constants may depend on $c,c'$, the class parameters, the prices, $x$ and $T$, but never on $\lambda$ or $n$.
• Range of $n$. Bounds whose right side vanishes at $n=1$ because $\log1=0$ are stated for $n\ge2$: the goal and (A-15).
• Typo correction. Lemma 5's event uses $nx-C_9nu_n$, as in its proof, not the printed $nx-C_9u_n$.
• Ruled out. A specific demand curve, a fixed $n$, deterministic demand, a finite price set, a known $\lambda$, constants depending on $\lambda$, or dropping the inventory cap would each make the statement a different and easier theorem. None is used.
• Not included. The lower bound of Proposition 2 and the second assertion of Lemma 1 ($J^\pi\le J^D$ for all admissible policies) are not included.

Contributions are welcome at any level: proofs of the milestones (Fact 1, Lemma 1 and Lemma 2 are self-contained), measurability and integrability lemmas for the revenue functional, and a reusable Poisson concentration library built on Mathlib's poissonMeasure.

Selected references

• O. Besbes and A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6):1407–1420, 2009. https://doi.org/10.1287/opre.1080.0640
• G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• K. Talluri and G. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2005. https://doi.org/10.1007/b139000

Motivation

Single-machine scheduling with precedence constraints, written $1|\mathrm{prec}|\sum w_jC_j$ in the notation of Graham et al., asks for an order of $n$ weighted jobs on one machine that respects a given partial order and minimizes the weighted sum of completion times. The problem is strongly NP-hard (Lawler 1978; Lenstra and Rinnooy Kan 1978), and closing its approximability gap is listed by Schuurman and Woeginger among ten outstanding open problems in scheduling theory. Several 2-approximation algorithms are known (Schulz 1996; Hall et al. 1997; Chudak and Hochbaum 1999; Chekuri and Motwani 1999; Margot et al. 2003).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph built from the precedence order. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) observed that this graph is the graph of incomparable pairs of dimension theory, and used that identification to obtain $(2-2/f)$-approximations for orders of fractional dimension at most $f$. This mission formalizes that framework: the identification of the two graphs and the rounding guarantee of the paper's Theorem 5.1.

Setting

An instance $S$ consists of a finite set $N$ of jobs, a partial order $P$ on $N$ (reflexive, antisymmetric, transitive; $(i,j)\in P$ with $i\ne j$ means job $i$ finishes before job $j$ starts), processing times $p_j\ge 0$ and weights $w_j\ge 0$.

Two jobs $x,y$ are incomparable, $x\parallel y$, when neither $(x,y)$ nor $(y,x)$ lies in $P$. The set $\operatorname{inc}(P)$ of incomparable pairs consists of ordered pairs and is closed under swapping. A linear extension of $P$ is a linear order $L\supseteq P$ on $N$; it reverses $(x,y)\in\operatorname{inc}(P)$ when $y<x$ in $L$. A nonempty multiset $L_1,\dots,L_t$ of linear extensions is a $k:t$-realizer if every incomparable pair is reversed by at least $k$ of them. The fractional dimension $\operatorname{fdim}(P)$ is the least ratio $t/k$ over all $k:t$-realizers.

The vertex cover graph $G^S_P$ has the incomparable pairs as nodes; nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$, or $j=k$ and $(i,\ell)\in P$, or $(i,\ell),(k,j)\in P$ (symmetrically closed). Node $(i,j)$ has weight $w_{(i,j)}=p_iw_j$, and $w(C)=\sum_{u\in C}w_u$. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$. The LP relaxation [CS-LP] asks for $x\in[0,1]^{\operatorname{inc}(P)}$ with $x_u+x_v\ge1$ on every edge, minimizing $\sum_u w_ux_u$. For a solution $x$ write $V_a=\{u: x_u=a\}$, and for a linear extension $L$ let $I_{1/2}(L)$ be the pairs of $V_{1/2}$ reversed in $L$.

The graph of incomparable pairs $G_P$ (Felsner and Trotter 2000) also has the incomparable pairs as vertices; two of them are adjacent when the pair of them is a minimal set of incomparable pairs that no linear extension reverses entirely.

Formalization targets

Goal: Theorem 5.1 (p. 658)

For an instance $S$, a $k:t$-realizer $L_1,\dots,L_t$ of $P$, and a half-integral optimal solution $x$ of [CS-LP], put $C_i=V_1\cup\bigl(V_{1/2}\setminus I_{1/2}(L_i)\bigr)$. Then every $C_i$ is a vertex cover of $G^S_P$, and

$$\frac1t\sum_{i=1}^t w(C_i)\;\le\;\Bigl(2-\frac{2}{t/k}\Bigr)\mathrm{OPT}.$$

Milestones

• Proposition 3.2 (p. 657): $G^S_P=G_P$.
• Footnote 4 (p. 659): the pairs reversed by a linear extension are independent in $G^S_P$.
• Eq. (4): $\frac1t|\{i: L_i\text{ reverses }u\}|\ge k/t$ for every incomparable pair $u$.
• Eq. (5): $\frac1t\sum_i w(I_{1/2}(L_i))\ge \frac kt\,w(V_{1/2})$.
• Hochbaum's observation (§5, p. 659): for half-integral feasible $x$, $V_1\cup C$ covers $G^S_P$ whenever $C$ covers $G^S_P[V_{1/2}]$.
• Eqs. (6)–(8): $\frac1t\sum_iw(C_i)\le w(V_1)+(1-\frac kt)w(V_{1/2})\le 2(1-\frac kt)(w(V_1)+\frac12w(V_{1/2}))\le(2-\frac2{t/k})\mathrm{OPT}$ when $P$ is not a linear order.

Significance

The result. Combined with the cited Theorem 2.1 (Ambühl–Mastrolilli 2009; Correa–Schulz 2005), which turns an $\alpha$-approximate vertex cover of $G^S_P$ into an $\alpha$-approximate schedule, Theorem 5.1 gives a $(2-2/f)$-approximation for $1|\mathrm{prec}|\sum w_jC_j$ whenever the precedence order has an efficiently samplable realizer with $t/k\le f$. The paper applies it to interval orders ($3/2$), convex bipartite orders and semiorders ($4/3$), orders of bounded degree and orders of interval dimension two; for the earlier special classes it matched or improved the best known ratios, and for the last two it gave the first results. Proposition 3.2 makes the dimension theory of posets (realizers, critical pairs, fractional dimension) directly available to the vertex cover approach.

Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. The mission produces a Lean development of incomparable pairs, linear extensions, $k$-fold realizers and the hypergraph of incomparable pairs, which other dimension-theory missions can reuse, and a verified LP-rounding argument for half-integral vertex cover solutions under a distribution of independent sets.

Difficulty

Most of the rounding argument is arithmetic over finite sums. The central nontrivial step is the inclusion $G_P\subseteq G^S_P$ in Proposition 3.2: for two incomparable pairs that are not adjacent under the three-case rule, one must construct a single linear extension reversing both. This needs an extension of $P$ by two new comparabilities whose transitive closure is still antisymmetric, followed by Szpilrajn's theorem; checking that every potential cycle is excluded by the three cases is the actual content. The opposite inclusion, and footnote 4, follow from transitivity and antisymmetry of linear orders. A second point of care is the inequality $t\ge 2k$ used in step (7): it is not part of the definition of a realizer, and follows from each linear extension reversing exactly one of $(x,y)$ and $(y,x)$.

Formalization scope

• Jobs form a finite type N; the precedence order is a relation P : N → N → Prop with IsPartialOrder, carried by the structure Instance. Processing times and weights are nonnegative reals.
• $\operatorname{inc}(P)$ is the subtype IncPair P of N × N; a linear extension is a relation with IsLinearOrder containing P; a $k:t$-realizer is a family Fin t → LinearExtension P with $t>0$. Reversal of $(x,y)$ means $y<x$ in $L$ throughout; the page's "$y>x$" in Eq. (4) and "$\mathrm{Prob}[j>i]$" in Eq. (5) are the same family of inequalities because $\operatorname{inc}(P)$ is symmetric.
• $G^S_P$ is the symmetric closure of the printed three-case rule on distinct nodes. $G_P$ is defined through linear extensions and hyperedge minimality, never through the three-case rule, so Proposition 3.2 is a genuine statement and not a definitional equality.
• [CS-LP] drops the constant term $\sum_jp_jw_j+\sum_{(i,j)\in P}p_iw_j$ of [CS-IP], which does not affect optimality. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$, taken over a finite nonempty family.
• Not formalized: "efficiently samplable", "polynomial time" and "randomized algorithm". The expectation over a uniformly sampled $L_i$ is stated as the average $\frac1t\sum_{i=1}^t$, which is equivalent to it and stronger than the existence of one good index. The existence of a half-integral optimal [CS-LP] solution (Nemhauser–Trotter, cited) is a hypothesis on $x$. The conversion of a vertex cover into a schedule (Theorem 2.1, cited) is not formalized; the goal is stated for vertex covers of $G^S_P$.
• Constants: $2-2/(t/k)$ in real arithmetic; it equals $2-2k/t$, and equals $2$ when $k=0$.
• The paper assumes $\operatorname{fdim}(P)\ge2$, i.e. $P$ is not a linear order. Eqs. (6)–(8) carry that hypothesis as the paper does; the goal omits it because for a linear order both sides are $0$.
• Conclusion (a), that each $C_i$ is a vertex cover, is part of the goal and is not assumed.

Contributions welcome: proofs of the milestones in any order, and a reusable Szpilrajn-style lemma producing a linear extension that reverses a prescribed set of compatible incomparable pairs.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the approximability of single-machine scheduling with precedence constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4), 2009 (reference [2] of the paper).
• J. R. Correa, A. S. Schulz, Single-machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
• G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992 (reference [7]).
• S. Felsner, W. T. Trotter, Dimension, graph and hypergraph coloring, Order 17(2):167–177, 2000 (reference [13]).
• D. S. Hochbaum, Efficient bounds for the stable set, vertex cover and set packing problems, Discrete Appl. Math. 6(3):243–254, 1983 (reference [20]).
• G. L. Nemhauser, L. E. Trotter, Vertex packings: structural properties and algorithms, Math. Programming 8(1):232–248, 1975 (reference [29]).

Motivation

Interior point methods solve linear programs in a number of arithmetic operations polynomial in the bit length of the input (Karmarkar 1984). Whether linear programming admits a strongly polynomial algorithm, one whose number of arithmetic operations is bounded by a polynomial in the number of variables and constraints alone, is open; it is the ninth of Smale's problems for the next century (Smale 1998/2000, see the references). A natural question is whether some interior point method is strongly polynomial. Primal-dual path-following methods follow the central path of a log-barrier problem and are the methods used in practice.

Allamigeon, Benchimol, Gaubert and Joswig (arXiv:1708.01544, SIAM J. Appl. Algebra Geom. 2018) gave such a family. For linear programs $\mathbf{LW}_r(t)$ with $2r$ variables and $3r+1$ constraints, every path-following method that stays in the wide neighborhood of the central path needs at least $2^{r-1}$ iterations once $t$ is large enough. The same family disproves the "continuous Hirsch conjecture" of Deza, Terlaky and Zinchenko (DTZ09, see the references) on the total curvature of the central path. That curvature result is the subject of a separate mission. This mission formalizes the iteration bound.

Setting

For a real $m\times n$ matrix $A$, $b\in\mathbb R^m$, $c\in\mathbb R^n$ and $N:=n+m$, the paper considers the linear program in slack form and its dual,

$$\mathrm{LP}(A,b,c):\ \min\ \langle c,x\rangle\ \text{ s.t. }\ Ax+w=b,\ (x,w)\ge0,\qquad \mathrm{DualLP}(A,b,c):\ s-A^\top y=c,\ (s,y)\ge0 .$$

A primal-dual point is $z=(x,w,s,y)\in\mathbb R^{2N}$. The set $\mathcal F^\circ$ of strictly feasible points consists of the $z$ with all $2N$ coordinates positive that satisfy both equality systems. The duality measure is

$$\bar\mu(z)=\frac1N\big(\langle x,s\rangle+\langle w,y\rangle\big),$$

and for $0<\theta<1$ the wide neighborhood of the central path is

$$\mathcal N^{-\infty}_\theta=\Big\{z\in\mathcal F^\circ:\ x_js_j\ge(1-\theta)\bar\mu(z)\ \forall j,\ \ w_iy_i\ge(1-\theta)\bar\mu(z)\ \forall i\Big\}.$$

The central path itself is the set of points where all products $x_js_j$, $w_iy_i$ are equal. The neighborhood bounds the products only from below. It contains the $\ell_2$ and $\ell_\infty$ neighborhoods used by short-step, long-step and predictor-corrector methods.

The instance is $\mathbf{LW}_r(t)$, for $r\ge1$ and $t>0$:

$$\min\ x_1\ \text{ s.t. }\ x_1\le t^2,\ x_2\le t,\ x_{2j+1}\le t\,x_{2j-1},\ x_{2j+1}\le t\,x_{2j},\ x_{2j+2}\le t^{1-1/2^j}(x_{2j-1}+x_{2j})\ (1\le j<r),\ x_{2r-1},x_{2r}\ge0 .$$

With slacks $w_1,\dots,w_{3r-1}$ it becomes $\mathbf{LW}^=_r(t)=\mathrm{LP}(A,b,c)$ with $n=2r$, $m=3r-1$, $N=5r-1$. Its wide neighborhood is written $\mathcal N^{-\infty}_{\theta,t}$. A polygonal curve is a union $[z^0,z^1]\cup\dots\cup[z^{p-1},z^p]$ of $p$ segments, and it is contained in the neighborhood when every point of every segment is.

The milestones use the tropical semifield $\mathbb T=\mathbb R\cup\{-\infty\}$ with $a\oplus b=\max(a,b)$ and $a\odot b=a+b$. The tropical segment $\mathsf{tsegm}(u,v)$ is the set of points $\lambda\odot u\oplus\mu\odot v$ with $\lambda\oplus\mu=0$. The Funk metric is $\delta_F(x,y)=\max(0,\max_k(y_k-x_k))$, with $d_\infty(x,y)=\max(\delta_F(x,y),\delta_F(y,x))$ and the directed Hausdorff distance $d_\infty(X,Y)=\sup_{x\in X}\inf_{y\in Y}d_\infty(x,y)$. Finally, $\log_t$ is applied coordinatewise, with $\log_t0=-\infty$.

Formalization targets

Goal: Theorem 30 (p. 27)

Let $r\ge1$ and $0<\theta<1$, and suppose that

$$t>\Big(\max\Big((10r-2)!,\ \frac{((10r-1)!)^{24}}{(1-\theta)^3}\Big)\Big)^{2^{r-1}} .\tag{36}$$

If a polygonal curve $[z^0,z^1]\cup\dots\cup[z^{p-1},z^p]$ is contained in $\mathcal N^{-\infty}_{\theta,t}$ with $\bar\mu(z^0)\le1$ and $\bar\mu(z^p)\ge t^2$, then

$$p\ge2^{r-1}.$$

The threshold (36) is the paper's own explicit constant. Corollary 31 (Theorem B of the introduction) restates the result for algorithms. Any method whose iterates and the segments joining them stay in the wide neighborhood performs at least $2^{r-1}$ iterations to reduce the duality measure from $t^2$ to $1$.

Milestones

1. Proposition 1 (p. 5). On the primal-dual feasible set, $\bar\mu((1-\alpha)z+\alpha z')=(1-\alpha)\bar\mu(z)+\alpha\bar\mu(z')$ for all $\alpha\in\mathbb R$.
2. Lemma 5 (p. 10). For $u\le v$ in $\mathbb T^d$, $\mathsf{tsegm}(u,v)$ is a polygonal curve whose segments, oriented from $u$ to $v$, have directions $e^{K_1},\dots,e^{K_\ell}$ with $K_1\subsetneq\dots\subsetneq K_\ell$ and $\ell\le d$.
3. Lemma 8 (p. 11). For a segment $S=[u,v]$ in $\mathbb R^d_+$ and $t>1$,

$$d_\infty\big(\mathsf{tsegm}(\log_tu,\log_tv),\ \log_tS\big)\le\log_t2 .$$

4. Lemma 11 (p. 13). For a $d\times d$ matrix $\mathbf M$ with monomial entries $\pm t^{\alpha_{ij}}$ and $t>1$, $\log_t|\det\mathbf M(t)|$ and $\operatorname{val}(\det\mathbf M)$ differ by at most $\log_td!$; the lower bound holds once $t\ge(d!)^{1/\eta(\mathbf M)}$.
5. Proposition 20 (p. 19). The explicit recursion for $x^\lambda$ gives the greatest point of the tropical polyhedron $\{x\in\mathcal P':x_1\le\lambda\}$, where $\mathcal P'\subseteq\mathbb T^{2r}$ is cut out by the tropicalized constraints (26) of $\mathbf{LW}_r$.

Significance

The theorem shows that the iteration count of a large class of primal-dual log-barrier interior point methods cannot be bounded by any function of $r$ that grows more slowly than $2^{r-1}$, uniformly in the data. The class includes the methods of Kojima–Mizuno–Yoshise, Monteiro–Adler and Mizuno–Todd–Ye. No such method is strongly polynomial. The constraint matrix of $\mathbf{LW}_r(t)$ is fixed by $r$ and $t$ alone, so the bound concerns the combinatorial dimension, not the bit length. The only property of the method used is that its trajectory stays in $\mathcal N^{-\infty}_{\theta,t}$. The lower bound therefore applies to every method with that property, whatever rule chooses its steps.

The result is proved in the paper; no machine-checked proof of it or of its tropical ingredients is known. A formalization would check the explicit threshold (36), which the paper derives in a few lines from bounds on Puiseux polyhedra. It would also produce reusable statements about tropical segments, the Funk and Hilbert metrics on $\mathbb T^d$, and determinants of monomial matrices.

Difficulty

Following the central path is not hard in principle: the obvious argument tracks the duality measure, which decreases by a constant factor per iteration in a neighborhood of the path. That argument gives only upper bounds. The lower bound requires showing that the neighborhood itself, for large $t$, is too thin to be crossed in a few straight steps, uniformly over every possible trajectory. The paper does this by passing to the limit $t\to\infty$ on logarithmic scale. The image of $\mathcal N^{-\infty}_{\theta,t}$ under $\log_t$ collapses onto a piecewise-linear tropical central path, and a segment of $\mathbb R^{2N}$ becomes, up to $\log_t2$, a tropical segment. The tropical central path of $\mathbf{LW}_r$ then has to be shown to need $2^{r-1}$ tropical segments. The limit argument has to be made quantitative at a finite, explicit $t$. That is where the Puiseux-series machinery (Theorems 12, 15 and 19 of the paper) and the explicit constant enter.

Formalization scope

Everything is stated over $\mathbb R$ and $\mathbb T$; the goal typechecks without the field of Puiseux series. A primal-dual point is an element of $\mathbb R^n\times\mathbb R^m\times\mathbb R^n\times\mathbb R^m$. The dual equation is $s-A^\top y=c$ with Mathlib's transpose, $\bar\mu$ divides by $N=n+m$ (equal to $5r-1$ for $\mathbf{LW}^=_r$), and the wide neighborhood is one-sided. The instance matrix is generated from the paper's 1-based row and column numbers; Lean indices are 0-based. A polygonal curve is a map $z:\{0,\dots,p\}\to\mathbb R^{2N}$ with segment ℝ (z i) (z (i+1)) ⊆ N. The power $2^{r-1}$ in (36) is a natural-number power and the factorials are natural-number factorials. $\mathbb T$ is WithBot ℝ, and distances that can be infinite take values in EReal, with the convention $-\infty+(+\infty)=-\infty$ encoded explicitly.

Two statements are repaired or restated. Lemma 11 is printed for all $t>0$, but its first inequality fails for $0<t<1$ (for $\mathbf M=\begin{pmatrix}t&1\\1&1\end{pmatrix}$ at $t=1/2$), so it is stated for $t>1$. Lemma 8 makes explicit its implicit hypotheses $t>1$ and $u,v\ge0$. Proposition 20 is stated in the form its proof establishes, as the greatest point of a tropical polyhedron. Its identification with the valuation of the Puiseux central path is not part of the item. Monomial matrices are given by sign and exponent matrices, and the valuation of the determinant is computed from the permutation expansion.

A trivializing formalization is ruled out: $\mathcal N^{-\infty}_{\theta,t}$ is not empty, since the build includes a sorry-free proof that it contains an explicit point for $r=1$, $t=2$, $\theta=1/2$. A curve with $p=0$ cannot satisfy both duality-measure conditions, since $t^2>1$.

The paper's Puiseux-series results are not posed: Theorems 12, 15, 19 and 29, Propositions 14, 16, 21 and 28, Corollary 17, and the count $\gamma([0,2])\ge2^{r-1}$ of §6.2. They need a faithful model of the field of absolutely convergent generalized Puiseux series and of the tropical central path. Contributions of that infrastructure, and of these statements as further milestones, are welcome. So are proofs of the five milestones, which need no Puiseux series. Proposition 1, Lemma 5 and Proposition 20 are elementary, and Lemma 8 and Lemma 11 are estimates with explicit constants.

Selected references

• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1), 2018; arXiv:1708.01544v2. https://arxiv.org/abs/1708.01544
• A. Deza, T. Terlaky, Y. Zinchenko, Central path curvature and iteration-complexity for redundant Klee–Minty cubes, in Advances in Applied Mathematics and Global Optimization, Adv. Mech. Math. 17, Springer, 2009, pp. 223–256. https://doi.org/10.1007/978-0-387-75714-8
• S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2), 1998, 7–15; reprinted in Mathematics: Frontiers and Perspectives, AMS, 2000. https://doi.org/10.1007/BF03025291
• M. Develin, B. Sturmfels, Tropical convexity, Doc. Math. 9, 2004. https://arxiv.org/abs/math/0308254
• S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453
• X. Allamigeon, S. Gaubert, M. Skomra, Tropical spectrahedra, Discrete Comput. Geom. 63, 2020; arXiv:1610.06746. https://arxiv.org/abs/1610.06746