The OR Formalization Drive

Motivation

Chapter 8 established an exact correspondence between lift-and-project cuts and simple disjunctive cuts, but its practical payoff is what this chapter develops: the cut-generating LP (CGLP)_k never needs to be formulated or solved on its own. Every pivot of (CGLP)_k can instead be mimicked directly on the much smaller simplex tableau of the original LP relaxation — replacing a large auxiliary linear program with bookkeeping on a tableau the solver already has. This chapter works out that correspondence at the level of individual pivots: which tableau pivot improves the resulting cut, and by how much, answered entirely in terms of ordinary tableau coefficients and two closed-form evaluation functions.

Setting

S:={1,…,m+p} and N:={m+p+1,…,m+p+n} index the surplus and structural variables of (LP) respectively — giving a direct correspondence between (LP)'s own variables and the surplus variables of Ãx≥b̃. For a basic solution with nonbasic set J (row set M1∪M2 from Chapter 8), Â:=Ã_J is the resulting nonsingular submatrix, and row k of the tableau reads x_k+ Σ_{j∈J}ā_{kj}s_j=ā_{k0}. Adding γ times row i to row k gives the composite row (9.10), x_k+γx_i+Σ_{j∈J}(ā_{kj}+γā_{ij})s_j=ā_{k0}+γā_{i0}, from which a new simple disjunctive cut can be read off whenever 0<ā_{k0}+γā_{i0}<1.

Formalization targets

Theorem 9.3 (goal) — the most-improving pivot column

The pivot column in row i most improving the cut from row k is indexed by l*∈J minimizing f⁺(γ_l) (if ā_{kl}ā_{il}<0) or f⁻(γ_l) (if ā_{kl}ā_{il}>0), over all l∈J with -ā_{k0}/ā_{i0}<γ_l<(1-ā_{k0})/ā_{i0}, γ_l:=-ā_{kl}/ā_{il}.

The chain of results building toward it

Lemma 9.1 (the tableau coefficients' closed form, eq. (9.4)-(9.5)) and Theorem 9.2 (the reduced costs of the CGLP columns u_i,v_i in terms of tableau coefficients, eq. (9.6)) are the two milestones the goal's own machinery is built from. Proposition 9.4, a bridge to Chapters 10-11's general split disjunctions, is included as a genuine milestone despite its payoff lying mostly outside this chapter.

Significance

The results themselves. This chapter is what makes lift-and-project cuts practical: instead of solving an (m+p+n)-row auxiliary LP from scratch for every candidate cut, a single pivot on the (LP)'s own tableau — guided by reduced costs that are themselves closed-form functions of tableau entries — identifies whether an improving cut exists and which one it is. Theorem 9.3's evaluation functions f⁺,f⁻ are exactly the tool a cutting-plane implementation would compute at every candidate pivot.

Formalizing it. No object in this mission exists on the platform prior to it or in Mathlib. This mission restates 08-cut-correspondence's (CGLP)_k apparatus locally, per the series convention and BRIEF.md's explicit instruction, and extends it with this chapter's own generalization to an arbitrary tableau row (needed since Lemma 9.1/Theorem 9.2 concern every basic variable's row, not only the disjunction row k).

Difficulty

Lemma 9.1's book proof is a four-case block-matrix verification (structural/surplus, basic/nonbasic); this mission instead states its content as the identity it is actually for — that the closed-form coefficients express every row's slack as an affine function of the nonbasic rows' slacks, for every point x — which follows tautologically from x=Â⁻¹b̂+Â⁻¹s_J's own definition once stated this way, without needing to reconstruct the block-matrix case analysis. Theorem 9.2's difficulty is that "reduced cost" is not already available as a formalized LP concept in this mission's apparatus; rather than build a generic LP reduced-cost theory, this mission follows the book's own derivation directly — explicitly constructing the pivoted-out extension of a basic solution (eq. (9.7)-(9.9)) and asserting that its objective value decomposes with r_{u_i},r_{v_i} as coefficients, which is genuine, non-circular content matching the proof's own final step ("we can then read the reduced costs... as the coefficients").

Formalization scope

This chapter makes the row/variable identification of Chapters 6-8 fully explicit (N directly indexes the structural variables), but no theorem's own displayed formula in this chunk needs that correspondence beyond what SurplusM's row-general treatment (this chunk's own generalization of 08-cut-correspondence's Surplus) already provides — see MODERATION_NOTES.md for why the S/N/B/R/P/Q block structure is proof machinery, not part of the stated content, throughout.

Theorem 9.3's range condition on γ_l, truncated in BRIEF.md's own excerpt, was completed by reading the PDF directly (confirmed identical to the range derived earlier in the same section): -ā_{k0}/ā_{i0}<γ_l<(1-ā_{k0})/ā_{i0}.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 9.
• 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 the tableau-pivoting procedure this chapter derives Lemma 9.1 and Theorem 9.2 from).

Motivation

Lift-and-project (L&P) cuts strengthen the linear relaxation of a mixed 0-1 program by separating a fractional point from the convex hull of a disjunction such as $x_k \le 0 \lor x_k \ge 1$. Generating an optimal L&P cut means solving the cut-generating linear program (CGLP), a linear program lifted to a space with one new pair of variables per constraint of the original tableau — considerably larger than the tableau itself. Balas and Bonami showed that this higher-dimensional LP need not be solved explicitly at all: an optimal (or near-optimal) L&P cut can instead be produced by ordinary simplex pivots in the original LP tableau, each such pivot implicitly performing an entire block of pivots in the CGLP (E. Balas and P. Bonami, Generating lift-and-project cuts from the LP simplex tableau: open source implementation and testing of new variants, Mathematical Programming Computation 1 (2009), 165–199, https://doi.org/10.1007/s12532-009-0006-4). This correspondence is what made L&P cuts practical in commercial solvers: Perregaard's implementation in XPRESS needed only 5% of the iterations and 1.5% of the time of solving the CGLP explicitly, and Bonami's public implementation in COIN-OR put the method within reach of any solver.

A second, independent line of work asks how the CGLP's feasible region should be normalized. The textbook normalization (fixing the sum of the CGLP multipliers to $1$) is scale-dependent — rescaling one constraint of the original system changes which cut the CGLP returns — so Balas and Perregaard proposed the ray normalization $\alpha y = 1$ instead (E. Balas and M. Perregaard, Lift-and-project for mixed 0-1 programming: recent progress, Discrete Applied Mathematics 123 (2002), 129–154, https://doi.org/10.1016/S0166-218X(01)00340-7). Under this normalization the CGLP's optimal value has a clean geometric meaning: it is exactly the distance, measured along a fixed ray from the point being separated, to the convex hull of the disjunctive set. This mission formalizes both results: the pivot correspondence (Theorem 10.1) and the optimal-value characterization under the ray normalization (Theorem 10.2, Theorem 10.3, and Corollary 10.4).

Setting

Fix a finite index set $M$ for the rows of a simplex tableau over $n$ variables, a matrix $A \in \mathbb R^{M \times n}$, and a right-hand side $b : M \to \mathbb R$, so that the tableau reads $A x \ge b$ (a "tilde" is dropped from the informal $\tilde A, \tilde b$ notation for the optimal-basis tableau of the linear relaxation). A basis is an injection $\iota : \mathrm{Fin}\, n \to M$ picking out $n$ of the rows; write $\hat A$ for the $n \times n$ submatrix $\hat A_{ij} = A_{\iota(i), j}$ and $\hat b$ for the corresponding subvector. From these, the standard tableau quantities are read off: $\bar a_{k0} := e_k \hat A^{-1} \hat b$, $\bar a_{kj} := -(\hat A^{-1})_{kj}$, and the surplus of row $i \in M$ at a point $x$, $\mathrm{Surplus}_i(x) := (Ax - b)_i$.

Fix a distinguished row $k$ with a fractional basic variable, and a candidate pivot row $i \ne k$. For $\ell$ ranging over the nonbasic columns $J$, set $\gamma_\ell := -\bar a_{k\ell}/\bar a_{i\ell}$; this is the value of a parameter $\gamma$ at which the combined source row

$$x_k + \gamma x_i + \sum_{j \in J} (\bar a_{kj} + \gamma \bar a_{ij}) x_j = \bar a_{k0} + \gamma \bar a_{i0} \tag{10.1$_\gamma$}$$

has its $j$-th coefficient pass through $0$. The simple disjunctive cut obtained by applying the split disjunction $z \le 0 \lor z \ge 1$ (where $z$ is the left side of (10.1$_\gamma$)) to this row is the object CombinedCutSet.

On the CGLP side, $(\mathrm{CGLP})_k$ is the cut-generating LP associated with the disjunction $-x_k \ge 0 \lor x_k \ge 1$ from Chapter 8: it has one pair of nonnegative multiplier variables $(u_\rho, v_\rho)$ per row $\rho \in M$, plus $u_0, v_0 \ge 0$, tied together by the normalization $\sum_\rho u_\rho + u_0 + \sum_\rho v_\rho + v_0 = 1$, and its feasible solutions $(\alpha, u, u_0, v, v_0, \beta)$ correspond exactly to valid cuts $\alpha x \ge \beta$ for the disjunction. A basic feasible solution to $(\mathrm{CGLP})_k$ is described by a valid partition $(M_1, M_2)$ of the nonbasic rows, with $u_\rho = 0$ off $M_1$ and $v_\rho = 0$ off $M_2$.

Separately, fix a disjunctive set and write $P_D \subseteq \mathbb R^n$ for its convex hull — the object every cut ultimately wants to separate a point from. For a fixed direction $y \in \mathbb R^n$ and point $\bar x \in \mathbb R^n$, $(\mathrm{CGLP})_y$ is the cut-generating LP under the ray normalization: pairs $(\alpha, \beta)$ with $\alpha x \ge \beta$ valid for every $x \in P_D$ and $\alpha y = 1$, minimizing the objective $\alpha \bar x - \beta$.

Formalization targets

Theorem 10.1. For a genuine ordered pivot chain $j_1, \dots, j_t$ inside $J$ (no repeats, each consecutive pair flipping the sign of $\bar a_{k,\cdot}$ as $\gamma$ increases — rule (b) of the theorem), the simple disjunctive cut from the combined row at $\gamma = \gamma_{j_t}$ equals the lift-and-project cut $\{x : \beta \le \alpha x\}$ associated with a basic feasible solution to $(\mathrm{CGLP})_k$ for the resulting basis $J' := (J \cup \{i\}) \setminus \{j_t\}$:

$$\mathrm{CombinedCutSet}(k, i, J, \gamma_{j_t}) = \{x : \beta \le \alpha x\}.$$

Theorem 10.2. If $(\mathrm{CGLP})_y$ is feasible, it has a finite minimum if and only if the ray meets the disjunctive hull:

$$\text{finite min} \iff \exists\, \lambda \in \mathbb R,\ \bar x + \lambda y \in P_D.$$

Theorem 10.3 (goal). If $(\mathrm{CGLP})_y$ has an optimal solution $(\tilde\alpha, \tilde\beta)$, its optimal value is exactly the signed distance to $P_D$ along the ray, and the corresponding boundary point lies exactly on the optimal hyperplane:

$$\bar x^{\mathsf T} \tilde\alpha - \tilde\beta = \lambda^* := \min\{\lambda : \bar x + \lambda y \in P_D\}, \qquad (\bar x + \lambda^* y)^{\mathsf T} \tilde\alpha = \tilde\beta.$$

Corollary 10.4. Taking $y := x^* - \bar x$ for a point $x^*$ in the lifted polyhedron $P_Q$ gives an optimal solution whose hyperplane separates $\bar x$ and meets the segment $(\bar x, x^*]$ at the point closest to $x^*$.

The targets are ordered from the purely combinatorial pivot correspondence (10.1, independent of the ray normalization) through the abstract feasibility/boundedness dichotomy (10.2) to the concrete value formula that is this mission's goal (10.3), with the geometric illustration (10.4) as a companion result using the same machinery with a specific choice of ray.

Significance

Theorem 10.1 is the theoretical justification for every commercial L&P-cut implementation cited above: it says the pivot correspondence is not an approximation or a heuristic shortcut but an exact identity between a single LP pivot and a specific, describable sequence of CGLP pivots, which is what lets a solver generate an (quasi-)optimal L&P cut at the cost of ordinary simplex pivots instead of solving a much larger LP. Theorem 10.3 gives the ray-normalized CGLP an exact geometric meaning — its value is a distance, not merely a linear-programming optimum — which is what makes the ray normalization the more robust alternative to the scale-dependent constant-sum normalization used elsewhere in the book (§9), and is the basis for the geometric picture (Corollary 10.4, Fig. 10.3) of how a lift-and-project cut relates to the lifted polyhedron $P_Q$.

Both directions are proved in the source text (Balas and Bonami 2009 for Theorem 10.1; Balas and Perregaard 2002 for Theorems 10.2/10.3 and Corollary 10.4) but have no formalized counterpart on this platform: no existing item treats cut-generating LPs, ray normalizations of a projection cone, or the correspondence between two different pivoting processes. This mission produces the first Lean statements of both.

Difficulty

The obvious temptation for Theorem 10.1 is to existentially weaken "the sequence of $t$ pivots defined as follows" to "there exists some sequence of pivots realizing the same cut" — which would be true but not what the theorem says, and would erase the entire content that makes the result useful (an algorithm, not just an existence claim). The formalization instead carries the explicit ordered chain j1 :: middle ++ [jt] as data, with the three-part construction (rules (a), (b), (c)) encoded as hypotheses on that specific list via List.IsChain, so the theorem proved is the constructive one the book states, not a weaker existential shadow of it.

For Theorem 10.3, the proof pattern in the book resists a shortcut: showing $\lambda_0 = \lambda^*$ requires deriving a contradiction from each strict inequality ($\lambda_0 > \lambda^*$ violates optimality of the point on $P_D$'s boundary; $\lambda_0 < \lambda^*$ contradicts optimality of $(\tilde\alpha, \tilde\beta)$ for $(\mathrm{CGLP})_y$ via a competing separating hyperplane), so there is no way to avoid formalizing both directions of the boundedness dichotomy already needed for Theorem 10.2 first.

Formalization scope

The ambient space is $\mathrm{Fin}\ n \to \mathbb R$ throughout, matching the rest of the series. $(\mathrm{CGLP})_y$'s feasibility (IsCGLPYFeasible) is stated directly as validity of $(\alpha, \beta)$ for $P_D$ under $\alpha y = 1$, not through an explicit representation of the projection cone's extreme rays — this matches how the book's own Theorems 10.2/10.3 and Corollary 10.4 are phrased purely in terms of $(\alpha,\beta)$-validity for $P_D$, never in terms of a specific disjunction's multipliers, so this is not a weakening relative to the source. $P_D$ (the disjunctive hull that $(\mathrm{CGLP})_y$ is defined against) and $P_Q$ (the lifted polyhedron whose supporting hyperplane Corollary 10.4 describes) are kept as two independent Set (Fin n → ℝ) parameters with no assumed relationship between them, matching the book's own text, which never states one; conflating them would be a trivializing formalization that this mission explicitly avoids. "The point closest to $x^*$" on the segment $(\bar x, x^*]$ is formalized via IsGreatest on the parameter $t \in (0, 1]$ at which the optimal hyperplane meets the segment, rather than via an unformalized Euclidean-distance minimization, since that is what "closest" means for points colinear with $\bar x$ and $x^*$ on a single ray.

Corollary 10.4 corrects a typo in the printed text: the corollary as printed reads "let $y := \bar x$ for some $x^* \in P_Q$", omitting "$x^* -$" before $\bar x$; the very next line's figure caption gives the intended formula unambiguously as $y = x^* - \bar x$, and the formalization uses the corrected formula (see MODERATION_NOTES.md).

This mission depends on no other chunk's Lean definitions — the CGLP and tableau apparatus needed here (originally introduced in Chapters 8 and 9) is restated locally, per the series' convention against importing another draft mission's definitions across chunks that are being drafted concurrently. A complete development needs: Farkas-type separation for the boundedness dichotomy in Theorem 10.2, and careful bookkeeping of finite index sets and their images under the basis maps $\iota, \iota'$ for Theorem 10.1. The tableau infrastructure (Ahat, Bhat, Abar0, Abar, GammaOf) is reusable by any later mission touching the simplex-tableau side of lift-and-project cuts.

Selected references

• E. Balas and P. Bonami, Generating lift-and-project cuts from the LP simplex tableau: open source implementation and testing of new variants, Mathematical Programming Computation 1 (2009), 165–199. https://doi.org/10.1007/s12532-009-0006-4
• E. Balas and M. Perregaard, Lift-and-project for mixed 0-1 programming: recent progress, Discrete Applied Mathematics 123 (2002), 129–154. https://doi.org/10.1016/S0166-218X(01)00340-7
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 10, §10.1 and §10.6. https://doi.org/10.1007/978-3-030-00148-3

Motivation

Several classical min-max theorems of combinatorial optimization say that a discrete maximization problem and a continuous minimization problem have the same optimal value, and that both have integral optimal solutions when the data are integral. Edmonds' polymatroid intersection theorem (1970), Fujishige's Fenchel-type duality for submodular functions (1984), Frank's discrete separation theorem for a submodular/supermodular pair (1982), and the potential characterizations of weighted matroid intersection (Frank's weight splitting theorem, 1981; Iri and Tomizawa's criterion for the assignment problem, 1976) are instances. Murota's paper Convexity and Steinitz's exchange property, 1996 places all of them under one theorem: a Fenchel-type min-max formula for a pair of an M-concave and an M-convex function, with integrality on both sides.

Timeline:

• 1970: Edmonds proves the polymatroid intersection theorem.
• 1982: Frank proves the discrete separation theorem for submodular/supermodular set functions, with integrality.
• 1984: Fujishige proves a Fenchel-type min-max theorem for submodular functions.
• 1976–1981: Iri and Tomizawa characterize optimality for independent assignment by potentials; Frank proves the weight splitting theorem for weighted matroid intersection (1981).
• Early 1990s: Dress and Wenzel introduce valuated matroids.
• 1995–1996: Murota proves the valuated matroid intersection theorem (SIAM J. Discrete Math. 9, 1996) and the M-concave intersection theorem (Bonn report, 1995), and in the present paper the Fenchel-type duality (Theorem 6.4).
• Later: the result becomes the central duality theorem of discrete convex analysis (Murota, Discrete Convex Analysis, SIAM, 2003).

Setting

Let $V$ be a finite nonempty set. For $u\in V$, $\chi_u\in\mathbb Z^V$ is its characteristic vector; for $x\in\mathbb R^V$, $\operatorname{supp}^{\pm}(x)$ are the sets of coordinates where $x$ is positive or negative, $x(X)=\sum_{v\in X}x(v)$, and $\langle p,x\rangle=\sum_v p(v)x(v)$.

A finite integral base set is a finite nonempty $B\subseteq\mathbb Z^V$ such that for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ some $v\in\operatorname{supp}^-(x-y)$ has $x-\chi_u+\chi_v\in B$. These are exactly the integer points of integral base polytopes of submodular systems. $\overline B$ is the convex hull of $B$.

A function $\omega:B\to\mathbb R$ has the exchange property (EXC), and is called M-concave, if for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ some $v\in\operatorname{supp}^-(x-y)$ has $x-\chi_u+\chi_v,\ y+\chi_u-\chi_v\in B$ and

$$\omega(x)+\omega(y)\le\omega(x-\chi_u+\chi_v)+\omega(y+\chi_u-\chi_v).$$

A function $\zeta$ is M-convex when $-\zeta$ is M-concave.

For $\omega:B_1\to\mathbb R$ and $\zeta:B_2\to\mathbb R$ the concave conjugate and convex conjugate are

$$\omega^\circ(p)=\min_{x\in B_1}\big(\langle p,x\rangle-\omega(x)\big),\qquad \zeta^\bullet(p)=\max_{x\in B_2}\big(\langle p,x\rangle-\zeta(x)\big),$$

and the concave closure and convex closure are $\hat\omega(b)=\inf_p(\langle p,b\rangle-\omega^\circ(p))$ and $\check\zeta(b)=\sup_p(\langle p,b\rangle-\zeta^\bullet(p))$; they are finite exactly on $\overline{B_1}$ and $\overline{B_2}$.

The primal problem maximizes $\omega(x)-\zeta(x)$ over $x\in B_1\cap B_2$; the relaxed primal problem maximizes $\hat\omega(b)-\check\zeta(b)$ over $b\in\overline{B_1}\cap\overline{B_2}$; the dual problem minimizes $\zeta^\bullet(p)-\omega^\circ(p)$ over $p\in\mathbb R^V$. A maximum over an empty family is $-\infty$.

Formalization targets

Goal: Theorem 6.4

If $\omega$ and $-\zeta$ satisfy (EXC), then

$$\max_{x\in B_1\cap B_2}\big(\omega(x)-\zeta(x)\big)=\max_{b\in\overline{B_1}\cap\overline{B_2}}\big(\hat\omega(b)-\check\zeta(b)\big)=\inf_{p\in\mathbb R^V}\big(\zeta^\bullet(p)-\omega^\circ(p)\big),$$

with (P1) a finite dual infimum forces $B_1\cap B_2\neq\emptyset$, and (P2) if $B_1\cap B_2\neq\emptyset$ all values are finite and equal and the infimum is attained. If $\omega,\zeta$ are integer-valued, the infimum may be taken over $p\in\mathbb Z^V$ and is attained there when finite.

Milestones

1. Lemma 6.3 (weak duality): for arbitrary $\omega,\zeta$ on finite nonempty sets, primal $\le$ relaxed $=$ dual (the Fenchel identity (6.5)).
2. Lemma 6.1: $(-f)^\circ(p)=-f^\bullet(-p)$ and $(-f)^\wedge=-\check f$ on $\overline B$.
3. Lemma 4.5: an M-concave $\omega$ satisfies $\hat\omega=\omega$ on $B$.
4. Theorem 2.1: (B1) is equivalent to being the integer points of an integral submodular (or supermodular) base polytope, with the describing functions $\max_{x\in B}x(X)$ and $\min_{x\in B}x(X)$.
5. Theorem 6.5 (Frank's discrete separation theorem, cited in the paper).
6. Lemma 6.7: four equivalent forms of boundedness of the dual problem.
7. Theorem 6.6 (the M-concave intersection theorem, cited in the paper): optimality of $x^*$ for $\omega_1+\omega_2$ is equivalent to a potential $p^*$ with $x^*$ maximizing both $\omega_1[-p^*]$ and $\omega_2[p^*]$, integral when the data are.

Significance

The formula gives, in one statement, the integrality of an optimal solution of the relaxed primal problem (the essential content of the first half, as the paper observes on p. 296) and of the dual problem. The paper presents it as a unification of two groups of theorems: Edmonds' polymatroid intersection theorem, Fujishige's Fenchel-type duality and Frank's discrete separation theorem on one side, and Iri and Tomizawa's potential characterization for independent assignment with its extensions by Fujishige and Frank (weight splitting) on the other. In the paper it yields the primal and dual separation theorems (Theorems 6.8, 6.9) and the convolution results (Theorems 6.10, 6.11), and it is the prototype of the Fenchel-type duality of discrete convex analysis.

All results here are proved in the literature; none is known to be formalized. Mathlib has no submodular base polytopes, no matroid intersection theorem and no discrete convex analysis. A formal proof of Theorem 6.4 would also require formal proofs of the two cited results, Frank's discrete separation theorem and the M-concave intersection theorem, which the paper uses without proof.

Difficulty

Lemma 6.3 is polyhedral convex duality and holds for any functions. The content is equality with the integral problem: the relaxed maximum over the polytope $\overline{B_1}\cap\overline{B_2}$ must be attained at an integer point. For general finite sets it is not, and the intersection of two integral polytopes generally has fractional vertices. Both the integrality of $\overline{B_1}\cap\overline{B_2}$ (Edmonds) and the existence of an integral optimal potential depend on the exchange structure; a direct argument from the definitions of conjugates does not see it. The dual integrality claim, that $p$ can be taken integral, is again specific to (EXC) and fails for general concave extensions.

Formalization scope

Lean conventions, all in namespace SteinitzExchange.Duality:

• $V$ is a type with [Fintype V] [DecidableEq V] [Nonempty V]; integer vectors are V → ℤ, real vectors V → ℝ; finite sets of integer vectors are Finset (V → ℤ).
• A function on $B$ is a total (V → ℤ) → ℝ used only at points of $B$. M-convexity of $\zeta$ is (EXC) for fun x => -ζ x; $\omega$ lives on $B_1$ and $\zeta$ on $B_2$, which are distinct sets in general.
• Conjugates are real-valued min/max over the finite set. The closures are real ⨅/⨆ over $p\in\mathbb R^V$ and are evaluated only on the convex hulls, where they equal the paper's values; off the hulls they carry a junk value instead of $\mp\infty$, which no statement uses.
• The three optimal values are in EReal, as suprema and infima of coerced reals, so no $\infty-\infty$ occurs. EReal's supremum of the empty family is $-\infty$, the paper's convention. The dual infimum is never a real ⨅ (which would return $0$ when unbounded and make (P1) meaningless).
• Every "max" of the page includes attainment: (P2) asserts points $x$, $b$, $p$ at which the three values are achieved; the integral dual infimum is attained when it is not $-\infty$.
• "Integer-valued" means $\omega(x)\in\mathbb Z$ on $B_1$ and $\zeta(x)\in\mathbb Z$ on $B_2$; integral potentials and separating vectors are V → ℤ.
• Theorem 2.1's "$\forall X\subset V$" is read as all $X\subseteq V$.

Formalizations that would trivialize the goal are excluded: an unrestricted real infimum for the dual, a convex closure built from $\zeta^\circ$ instead of $\zeta^\bullet$, a single base set for both functions, and a relaxed maximum taken over all of $\mathbb R^V$ instead of $\overline{B_1}\cap\overline{B_2}$.

Needed infrastructure: finite convex hulls and polyhedral Fenchel duality, submodular base polytopes and their integrality, Frank's separation theorem, and the valuated intersection theorem. The submodular-system layer (Theorem 2.1, Theorem 6.5) is reusable beyond this mission. Contributions to any milestone, including proofs of the two cited theorems, are welcome.

Selected references

• K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124 (1996) 272–311. https://doi.org/10.1006/aima.1996.0084
• K. Murota, Valuated matroid intersection I: optimality criteria, SIAM J. Discrete Math. 9 (1996) 545–561.
• K. Murota, Submodular flow problem with a nonseparable cost function, Report 95843-OR, Forschungsinstitut für Diskrete Mathematik, Universität Bonn, 1995 (source of Theorem 6.6).
• A. Frank, An algorithm for submodular functions on graphs, Annals of Discrete Mathematics 16 (1982) 97–120 (source of Theorem 6.5).
• A. Frank, A weighted matroid intersection algorithm, J. Algorithms 2 (1981) 328–336.
• J. Edmonds, Submodular functions, matroids and certain polyhedra, in: Combinatorial Structures and Their Applications, Gordon and Breach, New York, 1970, 69–87.
• S. Fujishige, Theory of submodular programs: a Fenchel-type min-max theorem and subgradients of submodular functions, Mathematical Programming 29 (1984) 142–155.
• M. Iri and N. Tomizawa, An algorithm for finding an optimal "independent assignment", J. Oper. Res. Soc. Japan 19 (1976) 32–57.
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508

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

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 lift-and-project cut-generating LP (CGLP) is the workhorse of the book's cutting-plane machinery, but its number of variables grows with $q$, the number of terms in the disjunction — a real computational cost for disjunctions with many terms. An alternative representation of the same disjunctive hull, built from vertices and extreme rays rather than from a dual LP, trades this away: its number of variables is fixed at $n$ regardless of $q$, at the price of a constraint set that is generally exponential in size (T. H. Kim, V-polyhedral disjunctive cuts, PhD thesis and papers with E. Balas; the underlying representation traces to the classical Minkowski–Weyl theorem for polyhedra). This mission formalizes the chapter's capstone: the V-polyhedral, lift-and-project, and generalized-intersection-cut families — three representations that look structurally different — coincide exactly.

Setting

A disjunctive set in V-polyhedral (vertex-ray) form is $F := \bigcup_{h\in Q} P^h$, $P^h := \mathrm{conv}\,V^h + \mathrm{cone}\,R^h$, where $V^h$/$R^h$ are the (finite) sets of vertices and extreme rays of the $h$-th disjunct. The conic hull of a set $S$ is the set of all finite nonnegative combinations of its elements. For a reference point $x_F \in F$, the disjunctive cone $C_{x_F}$ is the homogenization, at $x_F$, of the translated disjunctive system: $(x',x_0') \in \mathbb{R}^n \times \mathbb{R}_+$ with $Ax' + (Ax_F-b)x_0' \ge 0$ and $\bigvee_h(D^hx' + (D^hx_F-d^h_0)x_0' \ge 0)$.

For a relaxation $\tilde P^h$ of each disjunct with $P^h \subseteq \tilde P^h \subseteq C(x^h)$ (the LP cone at the disjunct's own optimum $x^h$), write $\tilde V^h$, $\tilde R^h$ for its vertices and rays, and $C := \mathrm{conv}(\bigcup_h \tilde V^h) + \mathrm{cone}(\bigcup_h \tilde R^h)$ for the single combined polyhedron they generate. The associated L&P cut-generating LP is

$$\alpha = u^h \tilde D^h, \qquad \beta \le u^h \tilde d^h_0 \quad (h\in Q), \qquad \textstyle\sum_{h\in Q} u^h e = 1, \qquad u^h \ge 0.$$

Formalization targets

Proposition 12.1. $\alpha x \ge \beta$ is valid for $F$ if and only if $\alpha p \ge \beta$ for every $p \in V^h$ and $\alpha r \ge 0$ for every $r \in R^h$, over every $h \in Q$.

Proposition 12.3. For a cut $\alpha x \ge \beta$ tight at $x_F$ ($\alpha x_F = \beta$) and $x \in F$: $\alpha x < \beta$ if and only if $\alpha(x - x_F) < 0$ for the corresponding point $(x - x_F, 1)$ of $C_{x_F}$.

Theorem 12.4. If $(\alpha,\beta)$ satisfies $\alpha p \ge \beta$ for every $p \in \tilde V^h$ and $\alpha r \ge 0$ for every $r \in \tilde R^h$ (over every $h$), and the mixed-integer feasible set $P_I$ lies in the combined polyhedron $C$, then $\alpha x \ge \beta$ is valid for $P_I$.

Theorem 12.5 (goal). $(\alpha,\beta)$ is valid for the combined vertex-ray system if and only if there exists a multiplier $u = \{u^h\}_{h\in Q}$ making it simultaneously a feasible solution of the CGLP above and a generalized intersection cut from

$$S := \{x \in \mathbb{R}^n : u^h \tilde D^h x \le u^h \tilde d^h_0,\ h \in Q\}.$$

The targets move from the elementary generator-validity fact (12.1) and its algorithmic companion (12.3, which the iterative cut-generation procedure of §12.1 uses to search only adjacent extreme points) through the same validity criterion generalized to a relaxed system (12.4) to the three-way unification (12.5) that is the entire point of introducing the V-polyhedral representation in the first place.

Significance

Theorem 12.5 explains why the V-polyhedral approach is worth having at all: it produces exactly the same cuts as the lift-and-project CGLP, so nothing is lost by switching representations, while the computational cost profile is reversed (the book's own estimate, not part of this mission's targets, shows the V-polyhedral approach at least $q^3$ times cheaper for a $q$-term disjunction using $\tilde P^h = C(x^h)$). This matters directly for disjunctions with many terms — split disjunctions used one or two at a time throughout most of the earlier chapters — which the CGLP approach makes increasingly expensive as $q$ grows, but which the V-polyhedral approach handles without a growing variable count.

Both directions are proved in the source (this book's own §12, citing the underlying V-polyhedral cut idea to Balas's joint work with T. H. Kim, and the GIC-to-L&P equivalence to §11.4's own Theorem 11.5) but have no formalized counterpart on this platform: nothing existing treats V-polyhedral representations, disjunctive cones, or a three-way cut-family equivalence. This mission produces the first Lean statements of all four targets.

Difficulty

The obvious shortcut for Theorem 12.5 is to state only "the V-polyhedral cuts and the L&P cuts coincide" and treat the GIC leg as a footnote, since the book's own two-line proof dispatches the GIC equivalence by citing an earlier theorem rather than re-deriving it. But the theorem's actual claim is a three-way equivalence with a specific, described $S$ built from the very multipliers that solve the CGLP — dropping the GIC leg, or defining $S$ independently of those multipliers, would understate what is being asserted (the book's own remark following the theorem stresses that the GIC-defining points and the V-polyhedral vertices are typically different points that nonetheless yield equivalent cuts, which is exactly the content a two-way statement would erase).

For Theorem 12.4, the subtlety is that $C$ (the combined polyhedron) is not the union $\bigcup_h \tilde P^h$ but its convex hull — a strictly larger set in general — so validity for $C$'s generators is a priori a stronger requirement than validity for each $\tilde P^h$ separately; the theorem's force is that this stronger validity is still exactly what is needed (and obtained) to conclude validity for $P_I$.

Formalization scope

The ambient space is Fin n → ℝ throughout, matching the series default, with the disjunction index Q left as a general type for Propositions 12.1/12.3 (so the same Ph/DisjSet definitions serve any finite disjunction) and specialized to [Fintype Q] where a finite sum over disjuncts is needed (Theorem 12.4's combined polyhedron, the CGLP of Theorem 12.5). V^h/R^h (Proposition 12.1) and Ṽ^h/R̃^h (Theorem 12.4) are formalized with the same underlying definitions (Ph, IsVPolyhedralValid) applied to different vertex/ray data, per BRIEF.md's explicit warning that these are distinct objects — not by duplicating the definitions under two names. "Is a generalized intersection cut from $S$" (IsGICFromS) is formalized via the exact characterization Theorem 11.4's own remark in 11a-intersection-cuts gives for the GIC family (valid outside $S$'s interior, and a genuine cut), rather than by re-deriving the underlying extreme-ray construction — a trivializing formalization this mission rules out would instead drop this leg's dependence on the same multiplier u that witnesses the CGLP leg, decoupling S from the solution it is supposed to come from.

This mission depends on no other chunk's Lean definitions; it restates 02a-convex-hull's vertex/extreme-point vocabulary, 11a-intersection-cuts's cut apparatus, and 11b-monoidal-strengthening's disjunctive-cut conventions only informally, per the series convention. Theorem 12.2 (the extreme-ray/edge correspondence underlying the "adjacent vertices only" search strategy) was not drafted this pass — see HARD.md — since a faithful, non-circular formalization of "edge of a polytope incident with a point" needs face-lattice machinery beyond what any earlier chunk in this series has built. The ConicHull/DisjunctiveCone/CombinedC definitions are reusable by any later mission touching V-polyhedral cut generation.

Selected references

• E. Balas and T. H. Kim, Cutting planes from extended LP formulations, Mathematical Programming 156 (2016), 587–606. https://doi.org/10.1007/s10107-015-0885-2
• E. Balas and M. Perregaard, Generalized intersection cuts and a new cut generating paradigm, Mathematical Programming A 137 (2013), 19–35. https://doi.org/10.1007/s10107-011-0483-x
• A. Kazachkov, Non-Recursive Cut Generation, PhD dissertation, Carnegie Mellon University, 2018 (cited by Balas for the relaxation-based V-polyhedral cut generator of §12.2).
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 12. https://doi.org/10.1007/978-3-030-00148-3

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