Operations Research

Motivation

The eigenvalues of the Laplacian of a graph carry metric information about the graph. The second-smallest one, $\lambda_1(G)$, was named the algebraic connectivity by Fiedler (Fiedler 1973), who showed it is positive exactly for connected graphs. N. Alon and V. D. Milman (J. Combin. Theory Ser. B 38 (1985) 73–88) showed that a large $\lambda_1$ also forces two further properties: small diameter and a concentration of measure phenomenon, in which almost every vertex is close to any set containing half the vertices. They used these facts to build explicit expanders and superconcentrators, which are sparse networks with strong connectivity guarantees used in the theory of computation and in communication network design.

This mission covers Section 2 of that paper, "The Main Tools": the edge-count inequality (Lemma 2.1), the isoperimetric inequalities (Theorems 2.5 and 2.6), and the resulting diameter bound (Theorem 2.7).

Timeline:

• 1973: Fiedler introduces $\lambda_1(G)$ as algebraic connectivity and proves $\lambda_1 \le \frac{n}{n-1}\min_v d(v)$.
• 1985: Alon and Milman prove the isoperimetric and diameter bounds of Section 2.
• 1986: Alon proves the converse direction, that edge expansion implies a spectral gap (Alon 1986).
• Later work sharpened the constant in the diameter bound, e.g. Chung 1989.

Setting

Let $G = (V, E)$ be a finite, connected, simple graph on $n = |V| \ge 2$ vertices. Write $d(v)$ for the degree of a vertex $v$, $d = \max_v d(v)$ for the maximum degree, and $A_G$ for the adjacency matrix. The Laplacian is the $V \times V$ matrix

$$Q = Q_G = \operatorname{diag}(d(v))_{v \in V} - A_G .$$

For real functions $f$ on $V$ with scalar product $(f, g) = \sum_v f(v)g(v)$, the quadratic form of $Q$ is $(Qf, f) = \sum_{\{u,v\} \in E} (f(u) - f(v))^2 \ge 0$. The eigenvalues of $Q$, counted with multiplicity, are real and are written $0 = \lambda_0 \le \lambda_1 \le \dots \le \lambda_{n-1}$. The algebraic connectivity $\lambda_1 = \lambda_1(G)$ is the second-smallest of them.

For vertices $u, v$, $\operatorname{dist}(u, v)$ is the number of edges of a shortest path from $u$ to $v$. For disjoint vertex sets $A, B$ the paper writes $\rho$ for the distance between them, $a = |A|/n$ and $b = |B|/n$ for their relative sizes, and $E_A$ ($E_B$) for the set of edges with both endpoints in $A$ (in $B$). $[x]$ denotes the integer part of $x \ge 0$.

Formalization targets

Goal: Theorem 2.7 (p. 79)

$$\operatorname{dist}(u, v) \;\le\; 2\left[\sqrt{2d/\lambda_1}\,\log_2 n\right] \qquad\text{for all } u, v \in V.$$

Milestones, in the order the proof uses them

1. Section 2, p. 76: $0 = \lambda_0 < \lambda_1$ for connected $G$.
2. Eq. (2.1), Rayleigh's principle: if $\sum_v f(v) = 0$ then $(Qf, f) \ge \lambda_1 \|f\|^2$.
3. Lemma 2.1: for nonempty $A, B$ at distance $\rho \ge 1$,

$$\lambda_1 n \le \frac{1}{\rho^2}\Big(\frac1a + \frac1b\Big)\big(|E| - |E_A| - |E_B|\big).$$

4. Remark 2.3: $\lambda_1 \le \frac{n}{n-1}\min_v d(v)$.
5. Theorem 2.5: if $\rho > 1$ then

$$b \le \frac{1-a}{1 + (\lambda_1/d)\,a\rho^2}.$$

6. Theorem 2.6: if every $A$–$B$ distance exceeds a real $\rho \ge 1$, then

$$b \le (1-a)\exp\!\Big(-\ln(1+2a)\Big[\sqrt{\lambda_1/(2d)}\,\rho\Big]\Big).$$

Each statement keeps the paper's explicit constants. The goal is the endpoint of this chain and the paper's headline graph-theoretic bound.

Significance

Theorem 2.7 gives, for any family of graphs of bounded maximum degree whose algebraic connectivity stays bounded away from zero, a diameter of order $\log n$. By the paper's Remark 2.8, the 4-regular graphs constructed in its Section 4 show that this order cannot be improved. Theorem 2.6 is a discrete concentration of measure inequality: the proportion of vertices at distance more than $\rho$ from a set of relative size $a$ decays exponentially in $\rho\sqrt{\lambda_1/(2d)}$. It is the graph analogue of the Gromov–Milman concentration for manifolds, and Section 3 of the paper applies it to cubes and other product graphs. Theorem 2.5 is the input for the construction of expanders from graphs with a spectral gap (Theorem 4.3 of the paper).

All results are proved in the paper, and the formal work here is a machine-checked version of known proofs. As far as could be determined, none of the four inequalities (Lemma 2.1, Theorems 2.5–2.7) has been formalized in Lean or elsewhere. Mathlib has the Laplacian matrix, its positive semidefiniteness, and the relation between its kernel and connected components, but no statement about its second eigenvalue. The spectral facts (milestones 1–2), stated for Mathlib's Matrix.IsHermitian.eigenvalues₀, are reusable for any future work on algebraic connectivity.

Difficulty

The combinatorial steps are short. The work is at the interface between the spectral definition and the quadratic form. Mathlib defines eigenvalues through the spectral theorem for a Hermitian matrix, sorted into a list. Obtaining Rayleigh's principle for the second eigenvalue from that list, with the constant functions as the eigenvector of $\lambda_0 = 0$, takes a Courant–Fischer-type argument over an orthonormal eigenbasis. It does not follow from positive semidefiniteness alone. Strict positivity of $\lambda_1$ additionally needs that the kernel of $Q$ is one-dimensional for a connected graph.

Theorem 2.6 iterates Theorem 2.5 over a sequence of neighbourhoods $\{v : \operatorname{dist}(v, A) \le j\mu\}$ with a real step length $\mu$, so it needs bookkeeping of integer parts and of real-valued distance thresholds. Theorem 2.7 then combines Theorem 2.6 with Remark 2.3 and needs the estimate $\tfrac12\, 2^{-[\log_2 n]} < 1/n$ with the integer part kept. Replacing $[\cdot]$ by the real number inside it changes the statement.

Formalization scope

• Graphs are Mathlib SimpleGraph V on a Fintype vertex type with decidable adjacency. Every item assumes G.Connected and $2 \le |V|$ (the goal writes $1 < |V|$, as the paper does).
• $Q$ is G.lapMatrix ℝ. $\lambda_1$ is the mission definition AlonMilman.Diameter.lambda1: the eigenvalue at index $n-2$ of eigenvalues₀, which lists the eigenvalues in decreasing order. It is $0$ by convention when $n < 2$, a case no theorem uses.
• $\lambda_1$ is defined spectrally. Defining it as the best constant in Eq. (2.1) would make Rayleigh's principle definitional and remove the spectral content of the mission, so that formalization is excluded. Likewise the goal quantifies over all pairs of vertices of a connected graph and does not use SimpleGraph.diam without connectivity, since that is $0$ for a disconnected graph.
• Distances are SimpleGraph.dist (a natural number). "The distance between $A$ and $B$ is $\rho$" is encoded as $\rho \le \operatorname{dist}(u, v)$ for all $u \in A$, $v \in B$. Because the bounds weaken as $\rho$ decreases, this is equivalent to the paper's exact distance. In Theorem 2.6 $\rho$ is real and the hypothesis is strict.
• $E_A$ is AlonMilman.Diameter.edgesWithin G A. All counts are cast to $\mathbb R$ before subtraction, $a = |A|/n$ is a real quotient, $[x]$ is Nat.floor, $\log_2$ is Real.logb 2, and $\ln$ is Real.log.
• Lemma 2.1 requires $A, B$ nonempty (so $a, b > 0$). Theorems 2.5 and 2.6 hold as stated for empty sets and carry no such hypothesis.

Contributions welcome: proofs of any milestone, and in particular general Mathlib-style lemmas for Rayleigh quotients and eigenvalues₀, which have uses beyond this mission.

Selected references

• N. Alon, V. D. Milman, λ1, isoperimetric inequalities for graphs, and superconcentrators, J. Combin. Theory Ser. B 38 (1985) 73–88. https://doi.org/10.1016/0095-8956(85)90092-9
• M. Fiedler, Algebraic connectivity of graphs, Czechoslovak Math. J. 23 (1973) 298–305. https://doi.org/10.21136/CMJ.1973.101168
• N. Alon, Eigenvalues and expanders, Combinatorica 6 (1986) 83–96. https://doi.org/10.1007/BF02579166
• F. R. K. Chung, Diameters and eigenvalues, J. Amer. Math. Soc. 2 (1989) 187–196. https://doi.org/10.1090/S0894-0347-1989-0965008-X

Motivation

A Markov decision process (MDP) is controlled with transition probabilities estimated from data, and optimal policies computed for the estimated model can perform badly when the estimates are off. Robust MDPs replace the single transition model by a set of models and optimize the worst case over that set. Two readings of "the set" are possible. In the stationary uncertainty model, the unknown transition matrices are fixed but unknown; this is the reading that confidence regions from statistics support, but the resulting min–max problem is hard to solve. In the time-varying uncertainty model, an adversary ("nature") may pick different matrices at every stage; this relaxation is solved exactly by robust dynamic programming. Nilim and El Ghaoui (Oper. Res. 2005) solve the second problem in place of the first, and Theorem 4 of their paper justifies the substitution for discounted costs: in the infinite horizon the two readings, and the restriction to stationary controllers, all give the same value, and in the finite horizon the two readings differ by an amount that decays geometrically in the horizon.

Timeline:

• 1973: Satia and Lave study MDPs with uncertain transition probabilities (Oper. Res. 21).
• 1994: Puterman's monograph collects the nominal theory, including the optimality of stationary deterministic policies for discounted finite MDPs (Wiley).
• 2001: Bagnell, Ng and Schneider state a robust Bellman recursion for stationary games without proof (CMU-RI-TR-01-25).
• 2005: Iyengar (Math. Oper. Res. 30) and Nilim and El Ghaoui independently prove the robust Bellman recursion under rectangular uncertainty; Nilim and El Ghaoui add Theorem 4.
• 2013: Wiesemann, Kuhn and Rustem extend robust MDPs beyond rectangular sets (Math. Oper. Res. 38).

Setting

States form a finite set $\mathcal X = \{0,\dots,n-1\}$ and actions a finite nonempty set $\mathcal A$. A stage cost $c(i,a)\ge 0$ is given for every state and action, together with a discount factor $0<\nu<1$ and an initial state $i_0$. For every action $a$ and state $i$ a nonempty set $\mathcal P_i^a$ of probability vectors in the simplex $\Delta_n$ is given: the possible rows of the transition matrix $P^a$. Rectangularity means that every row is chosen independently: one stage of nature is a family $(P^a)_{a\in\mathcal A}$ with $i$-th row of $P^a$ in $\mathcal P_i^a$, and the set of such families is $\mathcal Q$.

A controller policy $\pi=(\mathbf a_0,\mathbf a_1,\dots)$ assigns an action $\mathbf a_t(i)$ to each state at each stage; the set of all of them is $\Pi$, and the stationary ones (the same map at every stage) form $\Pi_s$. A nature policy $\tau=(P_t^a)$ picks one element of $\mathcal Q$ per stage; the set is $\mathcal T$, and the stationary ones form $\mathcal T_s$. Starting from $\mu_0 = e_{i_0}$, the state law evolves by $\mu_{t+1}(j)=\sum_i \mu_t(i)P_t^{\mathbf a_t(i)}(i,j)$. The discounted costs over horizon $N$ and over the infinite horizon are

$$C_N(\pi,\tau)=\sum_{t=0}^{N-1}\nu^t\sum_i\mu_t(i)\,c(i,\mathbf a_t(i)),\qquad C_\infty(\pi,\tau)=\lim_{N\to\infty}C_N(\pi,\tau).$$

For a controller class $\mathcal C\in\{\Pi,\Pi_s\}$ and a nature class $\mathcal S\in\{\mathcal T,\mathcal T_s\}$ the robust values are $\phi_\infty(\mathcal C,\mathcal S)=\inf_{\pi\in\mathcal C}\sup_{\tau\in\mathcal S}C_\infty(\pi,\tau)$ and $\phi_N(\Pi,\mathcal S)=\inf_{\pi\in\Pi}\sup_{\tau\in\mathcal S}C_N(\pi,\tau)$. Finally $c_{\max}=\max_{i,a}c(i,a)$ and $\varepsilon_N=\nu^Nc_{\max}/(1-\nu)$.

Formalization targets

Goal: Theorem 4 (p. 786)

$$\phi_\infty(\Pi,\mathcal T)=\phi_\infty(\Pi_s,\mathcal T_s)=\phi_\infty(\Pi_s,\mathcal T)=\phi_\infty(\Pi,\mathcal T_s),$$ $$0\le \phi_N(\Pi,\mathcal T)-\phi_N(\Pi,\mathcal T_s)\le \frac{\nu^N c_{\max}}{1-\nu}\quad\text{for every }N .$$

The second line is the paper's "the gap goes to zero at a geometric rate $\nu$", with the constant the paper's own argument produces.

Milestones (proof order of the paper)

1. Eq. (34): $C_N(\pi,\tau)\le C_\infty(\pi,\tau)\le C_N(\pi,\tau)+\varepsilon_N$ for all $\pi\in\Pi$, $\tau\in\mathcal T$, $N$.
2. Eq. (35): $\phi_N(\Pi,\mathcal T)\le\phi_\infty(\Pi,\mathcal T)\le\phi_N(\Pi,\mathcal T)+\varepsilon_N$.
3. Step (e): the same sandwich for $\phi_N(\Pi,\mathcal T_s)$ and $\phi_\infty(\Pi,\mathcal T_s)$.
4. Eq. (33): for every $\varepsilon>0$ and all large $N$, $\phi_\infty(\Pi_s,\mathcal T_s)-\varepsilon\le\phi_N(\Pi,\mathcal T)\le\phi_\infty(\Pi_s,\mathcal T_s)$.
5. Step (c): for every stationary $\pi$, $\sup_{\tau\in\mathcal T}C_\infty(\pi,\tau)=\sup_{\tau\in\mathcal T_s}C_\infty(\pi,\tau)$, hence $\phi_\infty(\Pi_s,\mathcal T)=\phi_\infty(\Pi_s,\mathcal T_s)$.
6. Step (d), nominal fact: for stationary $\tau$, $\inf_{\pi\in\Pi}C_N(\pi,\tau)\to\inf_{\pi\in\Pi_s}C_\infty(\pi,\tau)$.
7. Step (d): $\phi_\infty(\Pi,\mathcal T_s)=\phi_\infty(\Pi_s,\mathcal T_s)$.

Significance

The first half of Theorem 4 says that, for discounted robust MDPs with rectangular uncertainty, nothing is gained by either player from non-stationary behaviour: the controller may restrict itself to stationary deterministic policies and nature's time variation buys it nothing. This is what makes the stationary game (6), solved by the robust Bellman recursion of Theorem 3, the right infinite-horizon object. The second half is a quantitative guarantee for practitioners: solving the tractable time-varying problem (4) instead of the statistically motivated but hard stationary problem (3) costs at most $\nu^Nc_{\max}/(1-\nu)$ in value.

The result is proved on paper. As far as a search of the platform shows (September 2026), no robust MDP result has a machine-checked proof here; the nominal counterpart, optimality of stationary policies for discounted finite MDPs, is on the platform as BertsekasDP.discounted_main_theorem in a different model encoding (state-dependent control sets). A complete development contributes a reusable encoding of robust MDPs with time-varying and stationary adversaries, the truncation estimates for discounted costs, and a formal record of one step whose printed argument is incomplete (Step (d), see Difficulty).

Difficulty

The truncation estimates (34), (35) and Step (e) are elementary. The equalities in (31) are not: they compare values of games whose players have infinite-dimensional strategy sets, and the paper writes "min" and "max" where the infima and suprema need not be attained, since the row sets are neither closed nor convex. Two steps of the printed proof rely on results the mission does not import. Step (a) identifies $\phi_N(\Pi,\mathcal T)$ with iterates of the robust Bellman recursion, which is Theorems 1 and 3 of the paper (formalized in sibling missions of this series). Step (c) says only "following similar steps as in Step (a)". Step (d) is incomplete as printed: it shows that for each fixed stationary nature the controller's best time-varying and best stationary responses agree, which is a statement about a max–min value, whereas $\phi_\infty(\Pi,\mathcal T_s)$ is a min–max value. The obvious attempt to exchange the infimum over $\Pi$ with the supremum over $\mathcal T_s$ from that per-nature fact alone fails; the exchange requires a duality statement for the stationary game.

Formalization scope

States are Fin n; the action type is finite and nonempty. The row sets are an arbitrary family rows a i ⊆ stdSimplex ℝ (Fin n) with each set nonempty; nonemptiness is implicit in the paper and explicit here, and no convexity or closedness is assumed. A stage of nature is the subtype of families A → Fin n → (Fin n → ℝ) whose rows lie in the given sets, so rectangularity is built in. Controller policies are sequences ℕ → Fin n → A, nature policies sequences of stage choices; stationary policies of either player are the constant sequences. $C_N$ is defined from the forward state distribution (not from a Bellman recursion) and reads only stages $<N$, so the finite-horizon values over infinite sequences are exactly the paper's values (3) and (4) with stage costs $\nu^tc$ and zero terminal cost. $C_\infty$ is the sum of the series of nonnegative stage costs, which converges for $0\le\nu<1$ and equals $\lim_N C_N$. Every min and max of the paper is a real infimum ⨅ or supremum ⨆; all families are nonempty and lie in $[0,c_{\max}/(1-\nu)]$, and attainment is not assumed anywhere. The discount factor satisfies $0<\nu<1$, as in §4 of the paper.

The rate in the goal is the explicit bound $\nu^Nc_{\max}/(1-\nu)$; a formalization stating only that the gap tends to zero, or stating (31) with the infinite-horizon cost replaced by a Bellman fixed point, proves a different theorem and is not accepted.

A complete development needs: the stochastic-matrix facts for the forward distribution, geometric-series bounds, robust value iteration for the time-varying and the stationary adversary, and nominal stationarity of discounted MDPs. The model and truncation estimates are reusable for any discounted robust MDP result. Contributions of any milestone, and of proofs of Step (c) and Step (d) by any route, are welcome.

Selected references

• A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
• J. K. Satia, R. E. Lave, Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• J. A. Bagnell, A. Y. Ng, J. Schneider, Solving Uncertain Markov Decision Processes, Technical Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001.
• W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov Decision Processes, Mathematics of Operations Research 38(1):153–183, 2013. https://doi.org/10.1287/moor.1120.0566

Motivation

Given a $k$-connected graph, many connectivity algorithms run in time that grows with the number of edges $|E|$. A sparse certificate is a spanning subgraph with only $O(k|V|)$ edges that is still $k$-connected; computing one first and running the expensive algorithm on it replaces $|E|$ by $k|V|$ in the bound. Finding a $k$-connected spanning subgraph with the minimum number of edges is NP-complete for every fixed $k \ge 2$ (Garey and Johnson, problem GT31), so the question is how cheaply a sparse, not necessarily minimum, certificate can be found.

Nagamochi and Ibaraki (Algorithmica 7 (1992) 583–596) answered this with a single linear-time scanning procedure, FOREST, which partitions the edges into classes $E_1, E_2, \dots, E_{|E|}$. They showed that the prefix unions $E_1 \cup \dots \cup E_k$ are certificates for edge-connectivity and, for simple graphs, for node-connectivity. The node-connectivity result is the subject of this mission; the edge-connectivity result is the preceding mission of this series.

Timeline:

• 1980: Galil gives an algorithm testing $\kappa(G) \ge k$ whose running time depends on $|E|$ (SIAM J. Comput. 9).
• Before 1992 (as cited on p. 583): Suzuki et al. give $O(|E|)$-time algorithms for sparse 2- and 3-node-connected spanning subgraphs; Nishizeki and Poljak find, for general $k$, a $k$-node-connected spanning subgraph with at most $k(|V|-1)$ edges in $O(|V|^{1/2}|E|^2)$ time.
• 1992: Nagamochi and Ibaraki prove that FOREST, which runs in $O(|V| + |E|)$ time, yields a $k$-node-connected spanning subgraph $G_k$ of every simple $k$-node-connected graph, with $|E(G_k)| \le k|V| - k(k+1)/2$. Their Theorem 3.1 states a stronger, local form.
• 1993: Cheriyan, Kao and Thurimella isolate "scan-first search" as the general principle behind such certificates (SIAM J. Comput. 22 (1993)).

Setting

A graph $G = (V, E)$ has a finite node set $V$ with $|V| \ge 2$ and a finite edge set $E$; each edge has an unordered pair of two distinct end nodes. In this mission the graph is simple: no two edges have the same end nodes. For $F \subseteq E$, $(V, F)$ is the spanning subgraph with edge set $F$.

The local node-connectivity $\kappa(x, y; H)$ of nodes $x, y$ in a graph $H$ on $V$ is $|V| - 1$ if $x$ and $y$ are adjacent in $H$, and otherwise the minimum size of a node set $W \subseteq V - \{x, y\}$ whose deletion leaves no $x$–$y$ path. The node connectivity is $\kappa(G) = \min_{x, y} \kappa(x, y; G)$.

Procedure FOREST keeps a label $r(v) \ge 0$ on each node, initially $0$. While some node is unscanned, it chooses an unscanned node $x$ of largest label; for each unscanned edge $e = (x, y)$ it puts $e$ into the class $E_{r(y)+1}$, increases $r(x)$ by one if $r(x) = r(y)$, and increases $r(y)$ by one; then it marks $x$ scanned. Ties are broken arbitrarily. The time instants are the states between these elementary operations; $E^*_i$ denotes the class $i$ at an instant, and $E_i$ its final value. Put

$$G_i = (V,\ E_1 \cup E_2 \cup \dots \cup E_i).$$

Formalization targets

Goal: Theorem 3.1

For a simple graph $G$ and the classes of any completed run of FOREST, for $1 \le i \le |E|$,

$$\kappa(x, y; G_i) \ \ge\ \min\{\kappa(x, y; G),\ i\} \qquad \text{for any } x, y \in V. \tag{3.1}$$

The statement is local: it holds pair by pair, not only for the global minimum, and for every tie-breaking of the procedure.

Milestones, in the order the proof uses them

1. Lemma 2.2: at every instant, a node $v$ meets $E_i$ exactly for $i = 1, \dots, r(v)$.
2. Lemma 2.4(b): at every instant, a $u$–$v$ path in $E^*_j$ yields $u$–$v$ paths in every $E^*_i$, $i < j$.
3. In-degree at most one (§2, p. 588): orienting each edge from the earlier-scanned to the later-scanned end, every node has at most one entering arc in each class.
4. Lemma 3.1: if an $x$–$y$ path of $E^*_j$ has the form $x, u_1, \dots, u_k = w, y$ with $k = 1$ or $u_1$ scanned before $w$, then any $w$–$x$ and $w$–$y$ paths in $E^*_i$ ($i < j$) share a node other than $w$.
5. Lemma 3.2: for a node cut set $W = \{w_1, \dots, w_i\}$ of $G_{i+1}$ (in scan order) separating a component $X$ from the rest $Y$, immediately after $w_t$ is scanned every $X$–$Y$ path of $E^*_t$ passes through $w_t$, and $E^*_j$ has no $X$–$Y$ path for $t + 1 \le j \le i + 1$.

A companion item states the paper's announcement in §3: $G_k$ is $k$-node-connected for every $1 \le k \le \kappa(G)$.

Significance

Theorem 3.1 at $i = k$ shows that the first $k$ classes of FOREST form a $k$-node-connected spanning subgraph whenever $G$ is, and the edge-count analysis of the companion mission bounds its size by $k|V| - k(k+1)/2$. Since FOREST runs in linear time, any algorithm testing $\kappa(G) \ge k$ can be run on $G_k$ instead of $G$; the paper uses this to improve the bound for testing $\kappa(G) \ge k$ from $O(\max\{k^2|V|^{1/2}, k|V|\}|E|)$ to $O(\max\{k^3|V|^{3/2}, k^2|V|^2\})$, and similar gains for computing the number of node-disjoint paths between two nodes. The local form (3.1) is what makes the $s$–$t$ applications possible.

The result is proved on paper. As far as a search of the platform shows, neither FOREST nor local node-connectivity has a machine-checked treatment there; Mathlib has no notion of vertex connectivity of a pair of nodes. This mission produces a formal model of FOREST as a nondeterministic transition system and the statements needed to verify the paper's proof step by step.

Difficulty

For edge-connectivity the analogous statement follows from a general principle: any sequence of maximal spanning forests, each taken in what remains of the graph, preserves local edge-connectivity up to its length. The obvious attempt is to prove (3.1) the same way, from the fact that each $E_i$ is a maximal spanning forest of what the earlier classes leave. The paper gives no such argument for node-connectivity: its proof uses the specific scan order of FOREST in an essential way, through the orientation of edges from earlier- to later-scanned nodes and the in-degree bound of that orientation (Lemmas 3.1 and 3.2). The argument tracks, for a hypothetical node cut $W$ of size $i$ in $G_{i+1}$, the classes at the moments the nodes of $W$ are scanned, which requires reasoning about intermediate states of the algorithm and about paths in several classes at once. None of this reduces to a static property of the output partition.

Formalization scope

• Graphs. A node type V and an edge type E, both finite, with ends : E → Sym2 V; loop-freeness is ∀ e, ¬ (ends e).IsDiag and simplicity is Function.Injective ends. The standing assumptions of p. 583 and p. 589 ($|V| \ge 2$, no self-loop, a simple graph when node-connectivity is discussed) appear as hypotheses; §2 items are stated for loopless graphs, as on the page.
• Connectivity. $\kappa(x, y; (V, F))$ is valued in $\mathbb N_\infty$: $|V| - 1$ on adjacent pairs, the minimum node cut otherwise, and $\top$ when $x = y$, where (3.1) holds trivially.
• FOREST. A nondeterministic step relation with three steps (select, scan, finish), a run of length $K$ from the initial state, and completion when every node is scanned. Every tie-breaking is allowed, so the theorems quantify over all completed runs. A time instant is a state of a run; "scanned before" compares positions in the run's selection order; "immediately after $w_t$ has been scanned" is the state right after the finish step of $w_t$.
• Excluded. The running time "$O(|V| + |E|)$" and everything in §4 (the connectivity-testing algorithms and their bounds) are not stated: the paper fixes no machine model. The edge bounds on $|E_i|$ belong to the edge-connectivity mission.
• Ruled out. Stating (3.1) for an arbitrary partition into maximal spanning forests, or reading the classes $E^*_j$ of Lemmas 3.1–3.2 off the final state, would state a different theorem from the one the paper proves; the classes are those of a run of FOREST at the instant the page specifies.
• Infrastructure. Reachability avoiding a node set, walks and paths in SimpleGraph, and invariants of the FOREST transition system. The definitions duplicate those of the edge-connectivity mission by design and are candidates for a shared layer. Contributions of general lemmas about the run (label invariants, monotonicity of classes along a run) are welcome.

Selected references

• H. Nagamochi, T. Ibaraki, A linear-time algorithm for finding a sparse $k$-connected spanning subgraph of a $k$-connected graph, Algorithmica 7 (1992), 583–596. https://doi.org/10.1007/BF01758778
• Z. Galil, Finding the vertex connectivity of graphs, SIAM J. Comput. 9 (1980), 197–199. https://doi.org/10.1137/0209016
• J. Cheriyan, M.-Y. Kao, R. Thurimella, Scan-first search and sparse certificates: an improved parallel algorithm for $k$-vertex connectivity, SIAM J. Comput. 22 (1993), 157–174. https://doi.org/10.1137/0222013
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979.

Motivation

Many real-world disjunctive models are not unions of polyhedra in a single shared space, but unions of polyhedra in different spaces linked by a logical implication: some action affecting one set of entities has consequences for another. Balas's treatment of such models (§17 of the book, following [17]) reduces to understanding a single auxiliary object attached to each polytope in isolation: its dominant, the set of points that dominate (coordinatewise) some feasible point. Dominants and their duals, blockers, have a long history in combinatorial optimization — blocking-pair theory for covering and packing polyhedra traces to Fulkerson (D. R. Fulkerson, Blocking and anti-blocking pairs of polyhedra, Mathematical Programming 1 (1971), 168–194, https://doi.org/10.1007/BF01584085) — but this chapter develops a self-contained, constructive theory tailored to polytopes inside the unit cube, culminating in an exact, facet-complete description of the dominant for an arbitrary such polytope.

Setting

For a polyhedron $P \subseteq \mathbb{R}^n_+$, the dominant is $P^+ := P + \mathbb{R}^n_+ = \{y \ge 0 : y \ge x \text{ for some } x \in P\}$, and the blocker is $P^* := \{\pi \in \mathbb{R}^n_+ : \pi x \ge 1 \text{ for all } x \in P\}$ — the covering inequalities valid for $P$. (The blocker is not the reverse polar of 02b-polarity: restricting to the nonnegative orthant is essential and changes the object.) For $x^* \in \mathbb{R}^n_+$, the upper-separation value is $\alpha_P(x^*) := \min\{\pi x^* : \pi \in P^*\}$; a violated covering inequality for $x^*$ exists exactly when $\alpha_P(x^*) < 1$. A polytope $P \subseteq [0,1]^n$ is upper monotone (with respect to $[0,1]^n$) if $P = P^+ \cap [0,1]^n$ — the natural "closure" condition under which the theory of this chapter applies cleanly.

For $S \subseteq N := \{1,\dots,n\}$, write $a(S) := \sum_{j\in S} a_j$. Given $P \subseteq \mathbb{R}^n$ and a coordinate subset $S$, the projection $P^S$ keeps only the $S$-coordinates, letting the rest range freely. $I^S$ is the set of valid inequalities $\pi x \ge 1$ of $P^S$ with $\pi_j > 0$ exactly on $S$, tight at $|S|$ linearly independent points of $P^S$.

Formalization targets

Proposition 13.1. For an upper monotone $P = \bigcap_i P_i$ (each $P_i$ a single inequality in $[0,1]^n$), $P^+ = \bigcap_i P_i^+$.

Theorem 13.3. For $P = \{x \in [0,1]^n : ax \ge 1\}$ ($a \ge 0$) upper monotone,

$$P^+ = \Big\{x \ge 0 : \sum_{j\in S} \frac{a_j x_j}{1-a(N\setminus S)} \ge 1 \text{ for every } S\subseteq N \text{ with } 1-a(N\setminus S)>0\Big\}.$$

Theorem 13.5. For the same $P$ and any $x^* \ge 0$, with $x^*_q$ the greatest coordinate value $x^*_j$ satisfying $a(N\setminus S(x^*_j))<1$ and $x^*_j \le g(x^*_j)$: $S(\alpha_P) = S(x^*_q)$ and $\alpha_P = g(x^*_q)$, an explicit, computable value.

Theorem 13.7 (goal). For an arbitrary polytope $P \subseteq [0,1]^n$ (not necessarily upper monotone):

$$P^+ = \{x \ge 0 : \pi x \ge 1 \text{ for every } S \subseteq N \text{ and } \pi \in I^S\},$$

and every one of these inequalities is facet-defining for $P^+$.

Corollary 13.8. Every facet-defining inequality of $P^+$ has at most $\dim(P)+1$ nonzero coefficients.

The targets move from the intersection-distributivity fact (13.1) through an explicit, exponentially-large but fully closed-form facet system for the single-inequality case (13.3) and its constructive, polynomial evaluation recipe (13.5) to the fully general facet characterization (13.7, requiring no monotonicity assumption at all) and its immediate corollary on facet sparsity (13.8).

Significance

Theorem 13.7 is a rare case in polyhedral combinatorics of a complete and exact facet description obtained for the dominant of an arbitrary polytope, not merely a valid relaxation or an algorithmic separation oracle — every facet is accounted for, and every listed inequality is genuinely a facet, not merely valid. Corollary 13.8's support bound is the mechanism that makes Theorem 13.10 (not part of this mission) tractable: it lets the facets of a dominant built from a disjunction of polytopes in different spaces be characterized purely in terms of each factor's own low-dimensional facets, avoiding an exponential blowup in the combined space.

Both directions are proved in the source (Balas's own treatment, following the joint framework of [17]) but have no counterpart on this platform: nothing existing treats dominants, blockers, or upper monotonicity. This mission produces the first Lean statements of all five targets.

Difficulty

The obvious shortcut for Theorem 13.7 is to state only the validity half of the claim (every inequality from $I^S$ is valid for $P^+$) and treat "facet-defining" as a decoration — after all, Proposition 13.1's polar-style validity argument generalizes easily. But the theorem's actual force is the converse: not merely that these inequalities suffice to describe $P^+$, but that none of them is redundant, and no other facet exists. The book's own converse proof needs a genuine perturbation argument (splitting a facet candidate with fewer than $|S|$ independent tight points into two distinct valid inequalities averaging back to it, contradicting facetness) — this is where the real content lives, and a formalization that only captures the forward direction would understate the theorem substantially.

For Theorem 13.5, the difficulty is that $S(\alpha)$ and $g(\alpha)$ are themselves defined in terms of $\alpha$, so "the largest $x^*_j$ satisfying [a condition stated in terms of $S(x^*_j)$ and $g(x^*_j)$]" is a genuinely self-referential extremal characterization, not a closed-form formula one could simply plug into — hence its faithful statement (via IsGreatest over an explicit, self-referential candidate set) rather than an unwound algebraic expression.

Formalization scope

The ambient space is Fin n → ℝ throughout, matching the series default. Dominant/Blocker are given their own names (not reusing, even informally, 02b-polarity's polar/reverse-polar vocabulary), per BRIEF.md's explicit warning that the nonnegativity restriction makes these different objects. PolyDim/IsFacet are restated from 02b-polarity/11a-intersection-cuts (affine dimension via Module.finrank of vectorSpan, faces via IsExtreme), since Chapter 2 already pins these down precisely for this series and Chapter 13's own facet claims use the same notion. IsUpperMonotone is stated exactly as Definition 4 (P = P⁺ ∩ [0,1]ⁿ), not paraphrased as coordinatewise monotonicity, per BRIEF.md's explicit warning that these are different conditions.

IsInIS (membership in $I^S$) uses LinearIndependent ℝ directly for the "|S| linearly independent points" hypothesis, matching the book's own wording; since every such point satisfies $\pi x=1$, a linear dependence among them is automatically an affine dependence (the coefficients of any nontrivial linear relation among them must sum to zero), so this is not a weakening of the more familiar "affinely independent" reading a reader might otherwise expect. A trivializing formalization to rule out explicitly: describing Theorem 13.7's $P^+$ using only the validity half of the claim (dropping "each of these inequalities is facet-defining for $P^+$") — this mission states both conjuncts, since the facet-exactness is the theorem's genuine content beyond a Farkas-style validity certificate.

This mission depends on no other chunk's Lean definitions; it restates the affine-dimension/facet vocabulary of 02b-polarity/11a-intersection-cuts only informally, per the series convention. Corollary 13.6 (an $O(n)$-time algorithmic claim for computing $\alpha_P$) is out-of-cone per BRIEF.md: it is fully quantified, not a veto-V3 case, but is a computational-complexity statement outside this mission's polyhedral-characterization scope.

Selected references

• D. R. Fulkerson, Blocking and anti-blocking pairs of polyhedra, Mathematical Programming 1 (1971), 168–194. https://doi.org/10.1007/BF01584085
• E. Balas and R. G. Jeroslow, Strengthening cuts for mixed integer programs (for the broader monotonization-of-polyhedra context cited by this chapter's introduction), European Journal of Operational Research 4 (1980), 224–234. https://doi.org/10.1016/0377-2217(80)90106-X
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 13, §13.1–13.2. https://doi.org/10.1007/978-3-030-00148-3

Motivation

Many graph algorithms for connectivity questions run in time proportional to the number of edges. When the question is only whether a graph is $k$-edge-connected, or what its local edge-connectivities are up to a threshold $k$, most edges are irrelevant: a spanning subgraph with $O(k|V|)$ edges already carries the answer. Such a subgraph is called a sparse certificate. Computing one first and running the expensive algorithm on it replaces $|E|$ by $k|V|$ in the running time of connectivity testing, of Matula-type edge-connectivity algorithms, and of $s$–$t$ flow computations used as connectivity oracles.

Nagamochi and Ibaraki (Algorithmica 7, 1992) gave a procedure, FOREST, that computes such a certificate for edge-connectivity and, on simple graphs, for node-connectivity, with a single graph search. The same partition of the edges into forests is the engine of their deterministic minimum-cut algorithm for multigraphs (SIAM J. Discrete Math. 5, 1992), which later became the maximum-adjacency ordering of the Stoer–Wagner minimum-cut algorithm (J. ACM 44, 1997).

Timeline:

• 1927: Menger identifies the minimum number of edges separating two nodes with the maximum number of edge-disjoint paths between them.
• 1992: Nagamochi and Ibaraki publish Procedure FOREST and prove that its $i$-th prefix preserves local edge-connectivity up to $i$ in multigraphs, and local node-connectivity up to $i$ in simple graphs.
• 1993: Cheriyan, Kao and Thurimella (SIAM J. Comput. 22) obtain sparse certificates by scan-first search; Frank, Ibaraki and Nagamochi (J. Graph Theory 17) give a shorter proof for the node-connectivity case.
• 1994: Nishizeki and Poljak (Discrete Appl. Math. 55) publish the forest-decomposition lemma (Lemma 2.1 below), found independently.

Setting

A graph $G = (V, E)$ is finite and undirected, has $|V| \ge 2$ nodes, may have multiple edges (several edges with the same pair of end nodes), and has no self-loop. It is simple if no two edges have the same end nodes. For $F \subseteq E$, $(V, F)$ is the spanning subgraph with edge set $F$. It is a forest if it has no cycle; two parallel edges form a cycle. It is a maximal spanning forest in $(V, H)$, for $F \subseteq H$, if adding any edge of $H \setminus F$ to $F$ creates a cycle.

The local edge-connectivity $\lambda(x, y; H)$ is the minimum number of edges of $H$ whose removal leaves no path from $x$ to $y$; parallel edges count separately. It is $\infty$ when $x = y$.

Procedure FOREST keeps a label $r(v) \in \mathbb{N}$ on every node, initially $0$, and classes $E_1, E_2, \dots, E_{|E|}$, initially empty. While an unscanned node exists, it picks an unscanned node $x$ of largest label; for every unscanned edge $e$ from $x$ to a node $y$, it puts $e$ into $E_{r(y)+1}$, increases $r(x)$ by one if $r(x) = r(y)$, increases $r(y)$ by one, and marks $e$ scanned; then it marks $x$ scanned. Ties among nodes and the order of edges are free. On termination, $G_i = (V, E_1 \cup \cdots \cup E_i)$.

Formalization targets

Goal: Theorem 2.1 (pp. 588–589), without the running time

For every graph $G$ and every completed execution of FOREST on $G$:

1. every edge lies in exactly one class $E_i$, $1 \le i \le |E|$;
2. for $i = 1, \dots, |E|$,

$$\lambda(x, y; G_i) \ge \min\{\lambda(x, y; G),\ i\} \qquad \text{for all } x, y \in V; \tag{2.1}$$

3. $|E_i| \le |V| - 1$ for all $i$;
4. if $G$ is simple, $|E_i| \le |V| - i$ for $i \le |V| - 1$ and $E_i = \emptyset$ for $i \ge |V|$.

Milestones

• Lemma 2.2 (p. 587): during the execution, a node $v$ has incident edges in exactly the classes $E_1, \dots, E_{r(v)}$.
• Lemma 2.3 (p. 587): each $(V, E_i)$ is a forest at every instant.
• Lemma 2.4 (p. 588): (a) an edge $(u, v)$ added to $E_i$ has its end nodes joined by a path in $E_{i-1}$; (b) a path in $E_j$ between $u$ and $v$ yields a path in every $E_i$, $i < j$.
• Lemma 2.5 (p. 588): each output $(V, E_i)$ is a maximal spanning forest in $G - E_1 \cup \cdots \cup E_{i-1}$.
• Lemma 2.1 (p. 584): any sequence of successive maximal spanning forests satisfies (2.1).

Companions

• the sparse certificate (p. 589): if $\lambda(x, y; G) \ge k$ for all $x, y$, then $G_k$ is $k$-edge-connected with $|E(G_k)| \le k(|V| - 1)$, and $|E(G_k)| \le k|V| - k(k+1)/2$ for simple $G$;
• Lemma 2.6 (p. 589): for $k \le \delta(G)$, $G_k$ has a node of degree exactly $k$.

Significance

(2.1) says that one search produces, for every threshold $k$ at once, a subgraph with at most $k(|V|-1)$ edges that keeps every local edge-connectivity up to $k$. Any algorithm whose running time grows with $|E|$ can then be run on $G_k$ in place of $G$; §4 of the paper uses this to speed up $k$-connectivity tests and the computation of local connectivities. The same forest partition is the structural fact behind the Nagamochi–Ibaraki and Stoer–Wagner minimum-cut algorithms. Lemma 2.6 shows that the certificate is tight: its edge-connectivity is exactly $k$ when $\lambda(G) \ge k$.

The results are proved in the paper. No machine-checked proof of them is known. Formalizing them means formalizing a graph search with free tie-breaking as a transition system, reasoning about invariants of all its executions, and proving a cut-counting statement for multigraphs. Mathlib's connectivity notions, such as SimpleGraph.IsEdgeReachable, do not see parallel edges, so the multigraph cut theory here is new.

Difficulty

Lemma 2.1 is a short cut argument once maximality is available. The difficulty is showing that FOREST, which assigns each edge to a class by looking only at the label of one end node, produces maximal forests in the successive residual graphs (Lemma 2.5). The obvious invariant, that the class of an edge is the first forest it does not close a cycle in, is not what line 7 computes. The label $r(y)$ records only which classes touch $y$, not which component of each class contains $y$. The paper's argument needs Lemma 2.4(a): at the moment an edge is added to $E_i$ its ends already lie in one tree of $E_{i-1}$. That relies on the choice of the unscanned node of largest label, on the order of lines 8 and 9, and on an argument about the scan order of tree roots.

Formalization scope

• Graphs. A graph is a finite node type V with $|V| \ge 2$, a finite edge type E, and ends : E → Sym2 V with no diagonal value (no self-loops). Parallel edges are distinct elements of E. Simplicity is injectivity of ends, and edge subsets are Finset E. A forest is an edge set in which every edge is a bridge, a condition that sees parallel edges.
• Connectivity. $\lambda$ is an infimum in ℕ∞ over separating edge sets, $\infty$ at $x = y$. (2.1) is kept "for all $x, y$", as printed.
• FOREST. FOREST is a nondeterministic step relation (select, scan, finish) on explicit states: labels, class index per edge ($0$ = unscanned), scanned nodes, current node and selection order. The theorems quantify over every run from the initial state, so no tie-breaking rule is fixed. "At some time instant" is a state of the run; "upon completion" is a run whose last state has every node scanned. Lemma 2.2 is stated at every state, not only after a scan block (the other steps change neither labels nor classes). Lemma 2.4(a) assumes $i \ge 2$, since $E_0$ does not exist.
• Exclusions. Theorem 2.1's clause "is found in $O(|V| + |E|)$ time", the bucket implementation, and the time bound of the certificate are not formalized: the paper fixes no machine model. The goal consists of the structural conclusions only. The bound printed "if $G$ is multiple" is stated for every loopless graph.
• Non-triviality. The goal is about the classes of a run of FOREST. An arbitrary partition of $E$ into maximal spanning forests is Lemma 2.1's hypothesis, not a formalization of Theorem 2.1. A statement in which the classes are unconstrained variables, or in which the run hypotheses cannot be met, would be trivial. A separate sanity file checks that a complete run on the triangle $K_3$ exists and attains $|E_1| = |V| - 1$, $|E_2| = |V| - 2$.
• Welcome contributions. Useful reusable infrastructure includes:
  • a cut and Menger layer for finite multigraphs;
  • forest and bridge lemmas for edge-indexed graphs;
  • invariant-style reasoning over runs.

Selected references

• H. Nagamochi, T. Ibaraki, A linear-time algorithm for finding a sparse $k$-connected spanning subgraph of a $k$-connected graph, Algorithmica 7 (1992) 583–596. https://doi.org/10.1007/BF01758778
• H. Nagamochi, T. Ibaraki, Computing edge-connectivity in multigraphs and capacitated graphs, SIAM J. Discrete Math. 5 (1992) 54–66. https://doi.org/10.1137/0405004
• T. Nishizeki, S. Poljak, $k$-connectivity and decomposition of graphs into forests, Discrete Appl. Math. 55 (1994) 295–301. https://doi.org/10.1016/0166-218X(94)90014-0
• J. Cheriyan, M.-Y. Kao, R. Thurimella, Scan-first search and sparse certificates: an improved parallel algorithm for $k$-vertex connectivity, SIAM J. Comput. 22 (1993) 157–174. https://doi.org/10.1137/0222013
• A. Frank, T. Ibaraki, H. Nagamochi, On sparse subgraphs preserving connectivity properties, J. Graph Theory 17 (1993) 275–281. https://doi.org/10.1002/jgt.3190170302
• M. Stoer, F. Wagner, A simple min-cut algorithm, J. ACM 44 (1997) 585–591. https://doi.org/10.1145/263867.263872

Motivation

The Gomory mixed-integer (GMI) cut is the single most widely deployed cutting plane in practical mixed-integer programming: every commercial solver generates it, from a simplex tableau row, essentially for free. Yet the GMI cut is not the strongest cut derivable from the same row: once a subset of the variables is known to be integer-constrained, that integrality can be used to tighten the cut's coefficients further, a technique due to Balas and Jeroslow that predates and motivates most of the general disjunctive-cut machinery of this book (E. Balas and R. G. Jeroslow, Strengthening cuts for mixed integer programs, European Journal of Operational Research 4 (1980), 224–234, https://doi.org/10.1016/0377-2217(80)90106-X). This mission formalizes the culmination of that line of work: two refinements of the GMI cut, each strictly stronger than the plain GMI coefficient on part of the variable set, obtained by applying monoidal cut strengthening — optimizing a cut's coefficients over an algebraic monoid of admissible integer shifts — to the two-term split disjunction that produces the GMI cut in the first place (E. Balas and R. Jeroslow, as above; the monoidal strengthening framework itself due to R. E. Gomory and E. L. Johnson, and formalized in the generality used here by G. Nemhauser and L. Wolsey and by J. -P. P. Richard, Y. Li and A. Miller).

Setting

Fix a row of a simplex tableau: $y = a_0 - \sum_{j\in J} a_j x_j$, with $x_j \ge 0$ for $j \in J$, $x_j$ integer for $j$ in a subset $J_1 \subseteq J$, and $0 < a_0 < 1$. If $y$ is itself integer-constrained, every feasible solution satisfies the split disjunction $y \le 0 \lor y \ge 1$, from which the ordinary GMI cut $\alpha x \ge 1$ follows, with $\alpha_j := \max\{a_j/a_0,\ -a_j/(1-a_0)\}$ uniformly over all of $J$.

For a general $q$-term disjunction $\bigvee_{h\in Q}(\sum_j a^h_j x_j \ge a^h_0)$ with a known background lower bound $b^h_0 \le a^h_0$ on each term's left side, the cut monoid is

$$M := \{\mu \in \mathbb{Z}^q : \textstyle\sum_{h\in Q} \mu_h \ge 0\}.$$

Given the disjunction and the lower bounds, replacing each term's coefficient $a^h_j$ (for $j$ in the integer-constrained set $J_1$) with $a^h_j + \mu^j_h(a^h_0 - b^h_0)$ for any fixed $\mu^j \in M$ leaves the disjunction — and hence the disjunctive cut it implies — valid; optimizing this replacement over the whole monoid strengthens the resulting cut. For the normalized $q$-term disjunction $\bigvee_{i\in Q}(\sum_j a_{ij}x_j \ge a_{i0})$ (each right-hand side scaled to a common reference), the unstrengthened cut coefficient is $\beta_j := \max_{i\in Q} a_{ij}/a_{i0}$.

Formalization targets

Theorem 11.19. For the general $q$-term disjunctive-cut situation, every $x \ge 0$ satisfying the background lower bound and the disjunction also satisfies the monoidally-strengthened cut $\sum_j \alpha_j x_j \ge \alpha_0$, with

$$\alpha_j = \begin{cases} \inf_{\mu^j\in M}\max_{h\in Q}\theta_h[a^h_j+\mu^j_h(a^h_0-b^h_0)], & j\in J_1, \\ \max_{h\in Q}\theta_h a^h_j, & j\in J\setminus J_1,\end{cases} \qquad \alpha_0 = \min_{h\in Q}\theta_h a^h_0.$$

Proposition 11.22. For the normalized disjunction, and any fixed monoid elements $m^j \in M$ ($j\in J_1$), every $x\ge0$ integer on $J_1$ satisfying the disjunction and the background lower bound also satisfies the strengthened disjunction with each term's coefficients shifted by $m^j$ — the fact that licenses optimizing over the whole monoid afterward.

Corollary 11.25. For each disjunct index $k$, the cut $\delta^k x \ge 1$ is valid, with $\delta^k_j := \min\{(a_{kj}+a_{k0}-b_k)/a_{k0},\ \beta_j\}$ on $J_1$ and $\delta^k_j :=\beta_j$ elsewhere — a version of monoidal strengthening needing no optimization over $M$ at all.

Theorem 11.26 (goal). Specializing the same monoidal strengthening machinery to the two-term split disjunction $y \le 0 \lor y \ge 1$ itself: both $\alpha^+ x \ge 1$ and $\alpha^- x \ge 1$ are valid cuts, with $\alpha^+$ given by a three-case piecewise formula (eq. (11.55)) refining the GMI coefficient on part of $J_1$, and $\alpha^-$ symmetric (eq. (11.56)).

The targets move from the general monoidal-strengthening theorem (11.19) through its validity engine in normalized form (Proposition 11.22, directly cited by the intermediate Theorem 11.23 that the goal specializes) and its optimization-free cousin (Corollary 11.25, immediately preceding the goal in the same subsection) to the concrete payoff for the single most-used cut in practice.

Significance

Theorem 11.26's cuts are not a theoretical curiosity: Corollary 11.27 (not drafted this pass) gives an explicit, checkable condition under which each cut is strictly stronger than the plain GMI cut, and Example 4 (p. 187–188) gives a fully worked six-variable instance where the improvement is concrete and numerically verifiable. Since the GMI cut is generated by essentially every mixed-integer solver at essentially every node of a branch-and-cut search, a cheap, always-valid strengthening of it — derivable from the same tableau row with no extra data beyond knowing which variables are integer-constrained — has direct practical reach far beyond this one book.

Both directions are proved in the source (Balas and Jeroslow 1980 for the underlying strengthening idea; this book's own Theorem 11.19/Proposition 11.22/Theorem 11.23 chain for the general monoidal framework applied here) but have no counterpart on this platform: nothing existing treats monoidal cut strengthening, the cut monoid itself, or a refinement of the GMI cut. This mission produces the first Lean statements of all four targets.

Difficulty

The obvious shortcut for Theorem 11.26 is to collapse $\alpha^+$'s three-case definition into the plain GMI formula $\max\{a_j/a_0,\ -a_j/(1-a_0)\}$ applied uniformly — after all, that formula already gives a valid cut, and the strengthened cases can only make individual coefficients smaller (better). But a uniform formula reproduces exactly the plain GMI cut and can never be strictly stronger than it, which is the entire content the goal theorem (via Corollary 11.27) is building toward; the piecewise case split over $J^+_1$ (where $a_j>1$), $J^{>}_1$ (where $a_0-1\le a_j\le1$), and the rest is not incidental bookkeeping but the mechanism by which integrality actually buys something.

For Proposition 11.22 and Theorem 11.19, the difficulty is that the strengthening must remain valid simultaneously for every choice of the monoid element $\mu^j$ (or $m^j$) — not merely for some cleverly chosen one — since Theorem 11.19's conclusion then takes an infimum over the entire monoid $M$, which is generally infinite. Fixing a single "obviously good" $\mu^j$ and stopping there would prove a weaker, non-optimized statement.

Formalization scope

The ambient space is Fin n → ℝ throughout, matching the series default, with the disjunction index set Q represented as Fin q and the cut monoid CutMonoid q : Set (Fin q → ℤ). Theorem 11.19 is formalized with scalar per-term coefficients $a^h_j$ (one real number per disjunct $h$ and variable $j$), rather than the fully general "each term a multi-row system $A^h x \ge a^h_0$" framing the book's surrounding prose (§11.8's opening) sketches before specializing: every downstream result this mission needs (Proposition 11.22 onward, via (11.38)) is already stated at the single-inequality-per-term level, so this is not a weakening relative to what is actually used, only relative to a more general preamble that is never itself given a numbered, formalizable statement. AlphaJStrengthened uses sInf over the (possibly infinite) monoid literally, not a fixed near-optimal representative. AlphaPlus/AlphaMinus use the exact three-case structure of (11.55)/(11.56) — collapsing them into the uniform GMI formula is the trivializing formalization this mission rules out, since a uniform formula could never realize the theorem's actual (strictly stronger, on part of the domain) claim.

This mission depends on no other chunk's Lean definitions; it restates 11a-intersection-cuts's disjunctive-cut vocabulary only informally (the underlying disjunctive-cut idea, not any specific Lean declaration), per the series convention. A complete development needs: properties of sInf over an unbounded-below-safe subset of ℤ-indexed reals, and case analysis on Int.floor/ Int.ceil for the piecewise formulas. The cut-monoid and unstrengthened/strengthened-coefficient definitions are reusable by any later mission touching monoidal strengthening (e.g. a future mission on Theorem 11.23's full Lopsided-cut construction or the multiple-term-disjunction material of §11.9.2–11.9.3, not drafted this pass).

Selected references

• E. Balas and R. G. Jeroslow, Strengthening cuts for mixed integer programs, European Journal of Operational Research 4 (1980), 224–234. https://doi.org/10.1016/0377-2217(80)90106-X
• R. E. Gomory and E. L. Johnson, T-space and cutting planes, Mathematical Programming 96 (2003), 341–375. https://doi.org/10.1007/s10107-003-0389-3
• J.-P. P. Richard, Y. Li, and L. A. Miller, Valid inequalities for MIPs and group polyhedra from approximate liftings, Mathematical Programming A 118 (2009), 253–277. https://doi.org/10.1007/s10107-007-0190-9
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 11, §11.8–11.9. https://doi.org/10.1007/978-3-030-00148-3

Motivation

Chapter 6 built lift-and-project (L&P) cuts from a cut-generating LP, and Chapter 7 surveyed alternative nonlinear constructions reaching the same integer hull. This chapter asks a sharper question: how do L&P cuts relate, coefficient for coefficient, to older, more classical cutting planes — simple disjunctive cuts and mixed integer Gomory cuts, derived directly from a simplex tableau rather than from an auxiliary LP? The answer is an exact correspondence: every L&P cut from a basic solution of the cut-generating LP is equivalent to a specific simple disjunctive cut from a specific tableau basis, and conversely. This correspondence is not merely of theoretical interest — it converts a question about an infinite family of cuts into a finite, countable one (bases of a linear system), and it is what lets the chapter's capstone result, Theorem 8.7, establish a uniform rank bound of $p$ (the number of 0-1 variables) across four cut families at once, by proving it for one and transporting the proof to the other three.

Setting

$(CGLP)_k$ (eq. (8.1)) is the cut-generating LP for the disjunction $-x_k \ge 0 \lor x_k \ge 1$, with an added normalization constraint $ue+u_0+ve+v_0=1$ that makes its feasible polytope bounded — so a "basic solution" can be identified with an extreme point of that polytope. Given a basic solution with $u_0,v_0>0$ and basic $u/v$-components indexed by $M_1,M_2$ (Lemma 8.1-8.2), the $n\times n$ submatrix $\hat A$ of $\tilde A$ indexed by $J:=M_1\cup M_2$ is nonsingular, giving a simplex tableau in which $x_k$ is expressed as $x_k = \bar a_{k0} - \sum_{j\in J}\bar a_{kj}x_j$ (eq. (8.5)). The simple disjunctive cut from $x_k\le 0 \lor x_k\ge 1$ applied to this row has coefficients $\pi_j := \max\{\pi^1_j,\pi^2_j\}$, $\pi_0 := \bar a_{k0}(1-\bar a_{k0})$ (eq. (8.7)-(8.8)).

Formalization targets

Theorem 8.7 (goal) — a uniform rank bound across four cut families

The rank of the LP relaxation $P$ with respect to (a) unstrengthened L&P cuts, (b) simple disjunctive cuts, (c) strengthened L&P cuts, (d) mixed integer Gomory cuts (equivalently, strengthened simple disjunctive cuts) is at most $p$, the number of 0-1 variables.

The chain of results building toward it

Lemma 8.1 (basicness forces $u_0,v_0>0$), Lemma 8.2 (a basic solution's index sets give a nonsingular submatrix), Lemma 8.3 ($0<\bar a_{k0}<1$), Theorem 8.4A (a basic L&P cut equals a simple disjunctive cut), Theorem 8.4B (the converse: every simple disjunctive cut from a valid basis equals some basic L&P cut), and Theorem 8.5 (the same correspondence, strengthened).

Significance

The results themselves. Theorems 8.4A/8.4B are, in the book's own words, an "exact correspondence between lift-and-project cuts for a mixed 0-1 program and earlier cuts from the literature" — placing L&P cuts, simple disjunctive cuts, and (via Theorem 8.5) mixed integer Gomory cuts on the same logical footing, all generated by choosing a basis of one underlying linear system. Theorem 8.7 is the payoff: a single uniform bound covering four cut families that the literature had previously bounded (if at all) by separate arguments, and by contrast to the unbounded rank of pure-integer fractional Gomory cuts, exhibiting a case where the mixed 0-1 structure yields much stronger guarantees.

Formalizing it. No object in this mission exists on the platform prior to it or in Mathlib. This mission restates 06-lift-project-cuts's $(CGLP)$ apparatus and Theorem 6.4's strengthened cut formula locally, per the series convention that a draft mission cannot import another draft mission's definitions, adapted throughout to this chapter's normalized $(CGLP)_k$ and its disjunction on a single fixed coordinate $k$.

Difficulty

Formalizing "basic solution" required a genuine choice: unlike Chapter 6, $(CGLP)_k$'s normalization constraint makes its feasible set a bounded polytope, so this mission identifies "basic solution" with an extreme point of that polytope (Set.extremePoints) for Lemma 8.1 (whose own statement has no reference to specific index sets), while Lemmas 8.2 onward take the basic index sets $M_1,M_2$ directly as hypothesis data, matching how those theorems are themselves phrased ("let the basic components... be indexed by $M_1$ and $M_2$"). Theorem 8.7's rank bound required designing one generic HasRankAtMost predicate, parametrized by an abstract cut-closure operator, applicable uniformly to all four families — mirroring the book's own proof structure, which establishes the bound for one family and transports it to the other three via Theorems 8.4A/8.4B and 8.5, rather than arguing each part from scratch.

Formalization scope

The row/variable identification gap (see MODERATION_NOTES.md). The book's own eq. (8.4)- (8.5) identifies certain rows of the augmented, $m+p+n$-row matrix $\tilde A$ (those that are bound constraints $x_j\ge 0$) with the variables they bound, so that a chosen nonbasic row set $J$ doubles as a set of "nonbasic variables." This mission's abstract row type does not track that identification (matching the abstraction already used throughout 06-lift-project-cuts and 07-higher-dim): Surplus instead defines the tableau row's nonbasic quantities directly as the slack expression $s_j := (\tilde Ax)_j - \tilde b_j$, a genuine affine function of $x$ for every row, which reduces to $x_j$ itself exactly when row $j$ is that bound constraint — mathematically equivalent to the book's own substitution, stated without needing the row-to-variable lookup. Eq. (8.10)'s "$j\in J\cap N'$" strengthening-eligibility test has the same gap; this mission takes the row-positions eligible for strengthening as an explicit Finset parameter rather than deriving membership from row identity.

Corollary 8.6 is out of scope for this mission — see HARD.md. Its facet-counting bound depends on the same row/variable identification (the printed bound is $\binom{m+p+n-1}{n}$, excluding row $k$ specifically because it is $x_k$'s own bound row) and would additionally require a general notion of "number of facets of a polyhedron" that this mission's abstraction, and Mathlib, do not provide; it does not feed Theorem 8.7's own proof, which cites only Theorems 8.4A/8.4B and 8.5.

Theorem 8.7 is stated via one generic HasRankAtMost predicate applied to SplitConvexify (part a) and three closure operators (SimpleDisjClosureOfSet, StrengthenedLPClosureOfSet, MIGClosureOfSet, parts b-d) defined by intersecting a represented polyhedron with every cut of the corresponding family, then lifted to bare sets by quantifying over every linear representation — since, unlike the split-convexification closure, these three cut families are defined via an explicit basis or CGLP solution and so genuinely need some concrete representation of the current polyhedron at each step of the recursion (the same representation-dependence Theorem 7.5's Lovász-Schrijver iteration required in 07-higher-dim).

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 8.
• E. Balas, M. Perregaard, A precise correspondence between lift-and-project cuts, simple disjunctive cuts, and mixed integer Gomory cuts for 0-1 programming, Mathematical Programming B 94 (2003), 221–245 (cited in the text as [33], the origin of Lemma 8.2 and Theorems 8.4A/8.4B).
• E. Balas, M. Perregaard, Lift-and-project for mixed 0-1 programming: recent progress, Discrete Applied Mathematics 123 (2002), 129–154 (cited in the text as [32], the origin of Theorem 8.5's strengthened-cut coefficient identification).
• F. Eisenbrand, A. Schulz, Bounds on the Chvátal rank of polytopes in the 0-1 cube, in Integer Programming and Combinatorial Optimization (IPCO 7), LNCS 1610 (1999), 137–150 (cited in the text as [73], the source of the unbounded pure-integer Gomory rank result this chapter's Theorem 8.7 contrasts with).

Motivation

A mixed 0-1 program's feasible region is a disjunctive set built from the split disjunctions $x_j \le 0 \lor x_j \ge 1$, one per binary variable — a special case general enough that Chapter 2's convex-hull machinery applies directly, yet structured enough to produce closed-form cutting planes efficiently. The resulting lift-and-project (L&P) cuts, generated by solving a small auxiliary linear program (the cut-generating LP, CGLP) rather than by hand-derived combinatorial argument, were part of a cluster of ideas that drove a dramatic improvement in commercial mixed-integer solvers' practical performance from the mid-1990s onward. This chapter develops the theory that makes L&P cuts computationally practical: how to bound how many rounds of cutting are needed (disjunctive rank), what can and cannot be guaranteed about intermediate fractional solutions during sequential convexification, how to generate a cut cheaply by solving the CGLP only over the LP relaxation's active variables and lift the result back to the full variable space in closed form, and how to strengthen a single-disjunction cut into one valid for the whole integer program using the integrality of the other 0-1 variables.

Setting

For the mixed 0-1 program $\min\{cx : Ax \ge b,\ x \ge 0,\ x_j \in \{0,1\},\ j=1,\dots,p\}$, let $P$ be its LP relaxation (written $\{x : \tilde A x \ge \tilde b\}$ after folding in the bound constraints) and $D := \{x \in P : x_j \le 0 \lor x_j \ge 1,\ j=1,\dots,p\}$ its disjunctive feasible set. Sequential convexification produces $P_1 := \mathrm{conv}(P \cap \{x_1 \in \{0,1\}\})$, then $P_{1j} := \mathrm{conv}(P_1 \cap \{x_j \in \{0,1\}\})$, and so on. The cut-generating LP (CGLP) for the disjunction on coordinate $j$ asks for $(\alpha,\beta)$ and multipliers $u,v \ge 0$, scalars $u_0,v_0$, satisfying $\alpha - u\tilde A + u_0 e_j = 0$, $\alpha

• v\tilde A - v_0 e_j = 0$,$\beta - u\tilde b = 0$,$\beta - v\tilde b - v_0 = 0$. Solving `(CGLP)` only over a **restricted** set of active rows/columns$M_R, R$ gives (CGLP)^R, whose solution can be lifted back to a solution of the full (CGLP) in closed form.

Formalization targets

Theorem 6.4 (goal) — the general mixed-integer cut-lifting formula

$$\gamma_k = \min\{\alpha^1_k + u_0\lceil \bar m_k\rceil,\ \alpha^2_k - v_0\lfloor \bar m_k\rfloor\} \ (k \in N'), \qquad \gamma_k = \alpha_k\ (k \notin N'), \qquad \bar m_k = \frac{\alpha^2_k - \alpha^1_k}{u_0+v_0},$$

with $\gamma x \ge \beta$ valid for the whole mixed 0-1 program, strengthening a cut $\alpha x \ge \beta$ valid only for the single disjunction on $j$.

The chain of results building toward it

Theorem 6.1 (an extreme point of $P_1$ cut off at a facet of $P_{1j}$ cannot be fractional in $x_1$ without being fractional in $x_j$ too), Theorem 6.2 (an explicit closed-form extension of a restricted CGLP solution to the full CGLP), and Corollary 6.3 (the same fact, stated transparently via a $\max\{\alpha^1,\alpha^2\}$ formula and asserted feasible for the full CGLP).

Significance

The results themselves. Theorem 6.4 is what turns lift-and-project cuts from "valid for one binary variable's split" into genuine cuts for the whole mixed-integer program, using no information beyond the integrality of the other 0-1 variables — this strengthening step is part of why L&P cuts became practically competitive with other cutting-plane families. Theorem 6.2 and Corollary 6.3's cut-lifting property is, independently, what makes generating L&P cuts affordable at industrial scale: solving the CGLP only over a problem's few hundred active variables rather than its hundreds of thousands of total variables, then reading off the remaining coefficients in closed form.

Formalizing it. No object in this mission — the cut-generating LP, its restricted version, or the mixed-integer cut-lifting formula — exists on the platform prior to this mission or in Mathlib. This mission restates the disjunctive-set and convex-hull vocabulary of the earlier missions in this series locally (per the series convention that a draft mission cannot import another draft mission's definitions), applied specifically to the split disjunction on a single 0-1 variable.

Difficulty

The natural first attempt at Theorem 6.1 assumes that once $x_1$ has been "locked in" by sequential convexification, every subsequent cut generated while processing later variables respects that integrality — the book's own Figures 6.1-6.2 refute this directly, exhibiting facet- defining cuts that cut through the interior of an edge at a point fractional in every coordinate. Theorem 6.1's genuine content is the narrower but still useful fact that extreme points of the right intersection cannot exhibit this failure. The difficulty in Theorem 6.4 is recognizing that naively substituting $x_j - mx \le 0 \lor x_j - mx \ge 1$ for varying integer vectors $m$ gives a family of valid cuts, not a single one — the theorem's content is the closed-form choice of $m$ (via rounding $\bar m_k$ up or down, whichever yields the smaller coefficient) that is provably optimal within this family, not merely one valid choice among many.

Formalization scope

All results are stated over Fin n → ℝ with the CGLP's row space left as an abstract finite type M (rather than fixing the exact m+p+n-row block structure the book's own augmented matrix Ã has), since the substantive content of every theorem in this chapter depends only on dot products against columns of Ã, never on which literal row a given bound constraint occupies. Alpha1/Alpha2 (Corollary 6.3's row-restricted dot products) and Alpha1_64/Alpha2_64 (Theorem 6.4's eq.-(6.4) values, which add or subtract $u_0$/$v_0$ at the disjunction coordinate) are kept as separate definitions throughout, per BRIEF.md's explicit warning that the two chapters' "$\alpha^1,\alpha^2$" notation refers to different formulas despite the shared symbol.

Theorem 6.2's closed-form extension is formalized via the values it assigns (matching every printed formula for ū_{m+i}, v̄_{m+i}, ᾱ_i), without committing to the book's own literal row-block indexing (m+i vs. m+n+i) for the fresh rows a full reading of the source does not fully disambiguate for variables outside the 0-1 index set — Corollary 6.3, the chapter's own "more transparent" restatement of the same fact, is instead formalized with an explicit fresh-row construction (AtilExt, BtilExt) verifying genuine feasibility for the extended (CGLP). In Theorem 6.4, $u_0, v_0 > 0$ is stated as an explicit hypothesis, matching BRIEF.md's flag that this positivity (needed for $\bar m_k$'s division) is implicit in the CGLP feasibility setup rather than a free-standing assumption of the printed theorem.

A trivializing formalization is ruled out explicitly: Theorem 6.4's conclusion is stated as genuine validity for the full MIPDisjunctiveSet (imposing $0/1$ simultaneously on every $k \in N'$), not merely as the closed-form formula for $\gamma$ with no accompanying validity claim, which would omit the theorem's actual mathematical content.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 6.
• E. Balas, S. Ceria, G. Cornuéjols, A lift-and-project cutting plane algorithm for mixed 0-1 programs, Mathematical Programming 58 (1993), 295–324 (cited in the text as [19], the origin of Theorems 6.2 and the CGLP construction).
• E. Balas, M. Perregaard, A precise correspondence between lift-and-project cuts, simple disjunctive cuts, and mixed integer Gomory cuts for 0-1 programming, Mathematical Programming 94 (2003) (cited in the text as [20], the origin of Corollary 6.3).