Optimization

Motivation

Chapter 2's convex-hull machinery gives an exact, finitely-generated linear description of a disjunctive set's convex hull, but for a mixed 0-1 program with $p$ binary variables that description lives in a space with roughly $pn$ auxiliary variables — one full lift per disjunction. This chapter surveys the alternative nonlinear higher-dimensional constructions that several authors proposed for the same target, $\mathrm{conv}(K_0)$: multiplying the constraint system by products of $x_j$ and $1-x_j$ and linearizing the resulting quadratic terms, rather than disjoining and projecting one variable at a time. Two such constructions — Lovász and Schrijver's "cones of matrices" lift $N(K)$, and Sherali and Adams's hierarchy $K_t$ — both converge to the integer hull, and the chapter's central point is that both convergence proofs reduce, after all the nonlinear machinery is stripped away, to results already established by disjunctive programming's own one-variable-at-a-time convexification (Theorem 2.1, specialized here to Theorem 7.1, and the sequential-convexifiability theorem of Chapter 3).

Setting

$K := \{x \in \mathbb R^n : Ax \ge b,\ x \ge 0,\ x_j \le 1,\ j=1,\dots,p\} = \{x : \tilde A x \ge \tilde b\}$ is the LP relaxation of a mixed 0-1 program with $p$ of its $n$ variables 0-1 constrained, and $K_0 := K \cap \{x_j \in \{0,1\},\ j=1,\dots,p\}$ its feasible set. $P_j(K)$ (Section 7.1) multiplies $\tilde A x \ge \tilde b$ by $(1-x_j)$ and $x_j$, linearizes $y_i := x_ix_j$ and $x_j := x_j^2$, and projects onto $x$; iterating over a coordinate sequence gives $P_{i_1,\dots,i_t}(K)$. $N(K)$ (Section 7.2, Lovász-Schrijver) instead linearizes with a single symmetric matrix $Y$ ($Y_{ij} = Y_{ji} = x_ix_j$ for every pair) before projecting, and iterates as $N^t(K) := N(N^{t-1}(K))$. $K_t$ (Section 7.3, Sherali-Adams) multiplies by every product of $t$ literals $\prod_{j\in J_1}x_j\prod_{j\in J_2}(1-x_j)$ ($|J_1\cup J_2|=t$), linearizes each resulting monomial with a fresh "moment" variable, and projects.

Formalization targets

Theorem 7.6 (goal) — the Sherali-Adams hierarchy reaches the integer hull

$$K_p = \mathrm{conv}(K_0).$$

The chain of results building toward it

Theorem 7.1 ($P_j(K)$ equals the one-variable convex hull, a special case of Theorem 2.1), Theorem 7.2 (iterating $P_j$ over a fixed sequence reaches the hull of imposing $0/1$ on all of them), Corollary 7.3 (iterating over every 0-1 index reaches $\mathrm{conv}(K_0)$), Theorem 7.4 ($N(K) \subseteq P_j(K)$ for every $j$), Theorem 7.5 (iterating $N$ over $p$ steps reaches $\mathrm{conv}(K_0)$, by the same containment), and Theorem 7.7 ($K_t \subseteq P_{1,\dots,t}(K)$, proved by a genuine induction re-deriving every valid inequality of $P_{1,\dots,t}(K)$ from $(NL_t)$'s own rows).

Significance

The results themselves. This chapter is disjunctive programming's account of why three independently-developed convexification hierarchies — its own lift-and-project, Lovász-Schrijver, and Sherali-Adams — all reach the same integer hull: not by coincidence, but because each one's convergence proof is, at bottom, a disguised instance of the book's own Theorem 2.1 and Chapter 3 machinery. This is part of what situates disjunctive programming as the unifying framework behind several major lift-and-project hierarchies used throughout integer programming.

Formalizing it. No object in this mission exists on the platform prior to it or in Mathlib. This mission restates 03-sequential-convex's and 02a-convex-hull's vocabulary locally (per the series convention that a draft mission cannot import another draft mission's definitions), specialized throughout to the split disjunction $x_j \in \{0,1\}$.

Difficulty

The chapter's own account of the Sherali-Adams construction (Section 7.3) is narrative rather than displaying an explicit linear system for $(NL_t)$, unlike every other construction in this chapter (contrast eq. (7.1) and eq. (7.4), both displayed explicitly) — Step 1 says only "multiply $\tilde Ax \ge \tilde b$ with every product of the form $\prod_{j\in J_1}x_j \cdot \prod_{j\in J_2}(1-x_j)$." Deriving the actual linear system this multiplication produces requires expanding every $(1-x_j)$ factor via inclusion-exclusion over $S \subseteq J_2$ before the monomials can be linearized — a real, if mechanical, derivation step this mission had to carry out itself (RowNLt, see MODERATION_NOTES.md) rather than transcribe from a displayed equation. Theorem 7.7's own proof is a genuine argument (an induction re-deriving a valid inequality of $P_{1,\dots,t}(K)$ from $(NL_t)$'s rows layer by layer), not a restatement, so it is included as a milestone with real mathematical content rather than assumed.

Correcting BRIEF.md. The brief's "Recommended goal theorem" section mislabels Theorem 7.6 as the Lovász-Schrijver result "$K^p = \mathrm{conv}(K_0)$" — cross-checked directly against the PDF, Theorem 7.6 (p. 95, PDF 101) is stated [112] Kp = conv(K0), cited to Sherali and Adams, appearing immediately after Section 7.3 introduces $K_t$. The actual Lovász-Schrijver iteration-reaches-the-hull result, cited [99], is Theorem 7.5 (Np(K) = conv(K0)), formalized in this mission as a milestone (lovasz_schrijver_reaches_hull) rather than the goal. See STATUS.md.

Formalization scope

Three distinct convexification operators are kept fully distinguishable throughout, as BRIEF.md warns: Pj/IteratedSplit (one-variable-at-a-time, Section 7.1, Def_..._Basic), NOp/MK (Lovász-Schrijver, Section 7.2, Def_..._Lifts), and KtSet/IsXt (Sherali-Adams, Section 7.3, Def_..._Lifts) — no shared abbreviation or lemma conflates their defining predicates, even though all three converge to the same hull.

$N^t(K)$'s iteration (Theorem 7.5) is formalized via a dependent family of representations A t, b t for t : Fin (p+1) with a hypothesis relating consecutive steps to NOp's image at the previous step — the same pattern 04-normal-forms's Theorem 4.10 uses — since each successive $N^t(K)$ genuinely has a different, larger ambient constraint system, not a fixed matrix's power.

Theorem 7.7 is stated for an arbitrary $t$-subset $S \subseteq N'$ rather than the literal prefix $\{1,\dots,t\}$ the book's own statement uses (its own proof, by induction, treats an arbitrary inequality of $P_{1,\dots,t}(K)$ with no dependence on the prefix's specific ordering), which is what the goal theorem's proof, applied at $S = N'$, actually needs.

The Bienstock-Zuckerberg results quoted narratively in Section 7.5 ("Theorem 1"/"Theorem 2", [43]/[44]) are out-of-cone: the book itself presents them only as a survey of a further lift operator, under their own source papers' numbering, not as Balas's own numbered results, and does not restate their proofs.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 7.
• L. Lovász, A. Schrijver, Cones of matrices and set-functions and 0-1 optimization, SIAM Journal on Optimization 1 (1991), 166-190 (cited in the text as [99], the origin of the $N(K)$ construction and Theorems 7.4-7.5).
• H.D. Sherali, W.P. Adams, A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems, SIAM Journal on Discrete Mathematics 3 (1990), 411-430 (cited in the text as [112], the origin of the $K_t$ construction and Theorem 7.6).

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).

Motivation

Chapter 2 gives a compact lifted description of the closed convex hull of a disjunctive set once it is written as a union of polyhedra (its disjunctive normal form, DNF). But most discrete optimization problems present their feasible region the opposite way: as a conjunction of many small disjunctions (the conjunctive normal form, CNF) — "linear constraints, and $x_1 \in \{0,1\}$, and $x_2 \in \{0,1\}$, and so on" — each easy to reason about on its own but expensive to convert to DNF directly, since converting a CNF with $t$ conjuncts of $q_1,\dots,q_t$ terms each can blow the DNF up to as many as $q_1 \times \cdots \times q_t$ polyhedra. Chapter 4 develops the machinery for moving between these two extremes without paying that combinatorial cost all at once: the basic step, which merges two conjuncts into one, and the hull-relaxation, an intermediate polyhedral relaxation that tightens monotonically with every basic step performed, converging exactly to the true convex hull once the disjunctive set reaches DNF.

Setting

A disjunctive set is in regular form (RF) if $F = \bigcap_{j \in T} S_j$ with each $S_j = \bigcup_{i \in Q_j} P_i$ a union of polyhedra. $S_j$ is elementary if every $P_i$ is a halfspace (the RF is then the CNF), and improper if $S_j$ literally equals a single polyhedron $P_i$. Writing $T^*$ for the improper indices, $P_0 := \bigcap_{j \in T^*} S_j$ is $F$'s polyhedral part. The hull-relaxation of a regular form is

$$h\text{-}\mathrm{rel}(F) := \bigcap_{j \in T} \mathrm{cl}\,\mathrm{conv}(S_j),$$

a relaxation of $F$ distinct from $\mathrm{cl}\,\mathrm{conv}(F)$ itself: it convexifies each conjunct before intersecting, which is generally weaker. A basic step replaces two conjuncts $S_k, S_l$ ($k \ne l$) of a regular form by their intersection $S_k \cap S_l$ (itself brought to DNF via distributivity), reducing the number of conjuncts by one; repeating this $|T|-1$ times brings any regular form to DNF. For a convex set $S$, its extreme direction vectors are the extreme rays of its recession cone.

Formalization targets

Theorem 4.7 (goal) — the hull-relaxation hierarchy

For a sequence of regular forms $F_0, \dots, F_t$ of the same disjunctive set, with $F_0$ in CNF, $F_t$ in DNF, and each $F_i$ obtained from $F_{i-1}$ by a basic step:

$$P_0 = h\text{-}\mathrm{rel}(F_0) \supseteq h\text{-}\mathrm{rel}(F_1) \supseteq \cdots \supseteq h\text{-}\mathrm{rel}(F_t) = \mathrm{cl}\,\mathrm{conv}(F_t).$$

The chain of lemmas the goal is built from

Theorem 4.1 ($S_k \cap S_l = \bigcup_{(i,j)}(P_i \cap P_j)$, the basic-step identity), Theorem 4.4 (the hull of a union of halfspaces is $\mathbb{R}^n$ or the halfspace itself), Lemma 4.5 ($h\text{-}\mathrm{rel}(F_0) = P_0$ for a CNF $F_0$), and Lemma 4.6 ($\mathrm{cl}\,\mathrm{conv}(S_1 \cap S_2) \subseteq \mathrm{cl}\,\mathrm{conv}(S_1) \cap \mathrm{cl}\,\mathrm{conv}(S_2)$, driving each inclusion of the chain).

The sharpening and payoff results

Theorem 4.8 (an exact extreme-point/extreme-direction criterion for when Lemma 4.6 is equality), Corollary 4.9 (a worked case where merging "0-1" disjunctions brings no gain), and Theorem 4.10 (any regular form is the projection of a mixed 0-1 program using no more binary variables than the original CNF).

Significance

The results themselves. Theorem 4.7 turns the exponential CNF-to-DNF blowup into a controllable, monotone process: rather than converting all at once, a solver can perform basic steps selectively — wherever Theorem 4.8's criterion promises a genuine tightening — and always have a valid, improving polyhedral relaxation available at every intermediate stage. Theorem 4.10 is what makes this practical for integer programming specifically: it shows the number of 0-1 variables needed never has to grow, no matter how many basic steps are performed, only the number of continuous lifted variables does.

Formalizing it. No object in this mission — regular form, the hull-relaxation operator, basic steps, or extreme direction vectors — 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).

Difficulty

The obvious first attempt collapses h-rel to cl conv throughout, reasoning that since the chain ends at $\mathrm{cl}\,\mathrm{conv}(F_t)$, the intermediate terms should behave the same way. This is exactly backwards: h-rel is always at least as large as the true convex hull at every intermediate stage (Lemma 4.6 gives containment, not equality, in general), and the chapter's own Example 1 exhibits a CNF whose hull-relaxation strictly exceeds $\mathrm{cl}\,\mathrm{conv}(F)$ until enough basic steps have been performed. The real difficulty Theorem 4.8 isolates is recognizing which basic steps actually tighten the relaxation: merging conjuncts whose extreme points and directions already coincide with those of the pairwise intersections gains nothing (Corollary 4.9's worked case), while merging conjuncts that interact more intricately can produce a strictly tighter bound — and no general rule beyond Theorem 4.8's own extreme-point criterion identifies which case holds.

Formalization scope

All results are stated over Fin n → ℝ with matrices Matrix (Fin m) (Fin n) ℝ. A regular form's conjuncts are represented as an arbitrary function T → Set (Fin n → ℝ) (rather than requiring every conjunct's internal polyhedral structure to be uniformly tracked through the whole chapter), with IsDisjunctiveUnion/IsElementaryDisjunction as existential well-formedness predicates asserting each conjunct genuinely is a union of polyhedra/halfspaces where that matters. IsBasicStepOf states a basic step abstractly via an index-type equivalence, since its mathematical content is which two conjuncts merge and into what, not any particular relabeling scheme; Theorem 4.7's own sequence of regular forms is a dependent family T : Fin (t+1) → Type* precisely because each basic step genuinely changes the index type (one fewer conjunct).

Theorem 4.7's three-part conclusion (initial equality, step-by-step containments, final equality) is stated as a conjunction rather than a single chained relation, since Lean has no native mixed equality/containment chain notation; this preserves the chapter's own warning that only the last hull-relaxation in the chain is asserted equal to the true convex hull. Theorem 4.10's index set $M_i$ (which term of each original disjunction a given conjunct's disjunct picked) is taken as given structural data satisfying the book's own defining relationship, matching the source's own treatment of $M_i$ as a named auxiliary index set rather than a from-scratch construction. Chapter 4's §4.5–4.6 (a machine-sequencing application with its own bespoke scheduling objects, Theorems 4.11–4.12) is out of scope for this mission — it introduces application-specific vocabulary not shared by the chapter's general hull-relaxation theory, not because it is difficult.

A trivializing formalization is ruled out explicitly: every theorem is stated for generic finite index types, never fixed at a small size that would collapse a union or intersection to a single term, and the chapter's own propositional-logic DNF/CNF conversion (informal narrative via truth tables in §1.3) is not itself a formalization target — this mission works entirely at the polyhedral-set level the chapter's own numbered results occupy.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 4, §4.1–4.4.
• V. Chvátal, Linear Programming, W. H. Freeman, 1983 (cited in the text as [12], the origin of Theorem 4.1's basic step).
• E. Balas, Disjunctive programming: Properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998), 3–44 (the origin of the hull-relaxation hierarchy).

Motivation

Computing the convex hull of a disjunctive set — a union of finitely many polyhedra — is generally hard in direct proportion to how many polyhedra are in the union: Chapter 2's Theorem 2.1 gives a compact lifted description, but working with it still means reasoning about all the disjunctions of the program simultaneously. A natural question, with obvious practical consequences for integer and combinatorial optimization, is whether the convex hull can instead be built up incrementally: impose one disjunction, take the convex hull of what results, then impose the next disjunction on that, and so on. If this "sequential convexification" procedure always reached the true convex hull, computing facets of a hard disjunctive set would reduce to a sequence of much easier single-disjunction computations. Balas shows the answer is negative in general — a two-variable integer program is a standard counterexample — but identifies an important class of disjunctive programs, the facial ones, for which sequential convexification always works. This class includes 0-1 programming (pure or mixed), nonconvex quadratic programming, separable programming, and the linear complementarity problem, though not general integer programming.

Setting

Let $F_0 := \{x \in \mathbb{R}^n : Ax \ge b,\ x \ge 0\}$. A disjunctive program in conjunctive normal form has constraint set

$$F := \Big\{x \in F_0 : \forall j \in S,\ \exists\, i \in Q_j,\ d_i x \ge d_{i0}\Big\},$$

for a finite set $S$ and, for each $j \in S$, a finite set $Q_j$ of halfspace data $(d_i, d_{i0})_{i \in Q_j}$ — one elementary disjunction per $j \in S$. The program is facial if every inequality $d_i x \ge d_{i0}$ appearing in some disjunction defines a face of $F_0$, i.e. $F_0 \cap \{x : d_i x \ge d_{i0}\}$ is an extreme subset of $F_0$ for every such $i$. Fixing an ordering $\sigma$ of $S$, the sequential-convexification recursion sets $F_0$ (step zero) to be the base polyhedron and, for each subsequent step, imposes the next disjunction and reconvexifies: $F_{k+1} := \mathrm{conv}\big[\bigcup_{i \in Q_{\sigma(k)}} (F_k \cap \{x : d_i x \ge d_{i0}\})\big]$.

For the necessity direction, write $D_j := \bigvee_{i \in Q_j}(d_i x \ge d_{i0})$ and, reversing every inequality, $\bar D_j := \bigvee_{i \in Q_j}(d_i x \le d_{i0})$.

Formalization targets

Theorem 3.1 (goal) — faciality is sufficient

$$F \text{ facial} \implies F_{|S|} = \mathrm{conv}(F), \quad \text{for every ordering } \sigma \text{ of } S.$$

This is the weakest correct statement of the recursion's endpoint: it asserts the sequential procedure reaches exactly $\mathrm{conv}(F)$ (not, say, some fixed superset), and — since $\sigma$ is universally quantified — that this holds regardless of the order in which disjunctions are imposed.

Lemma 3.2 — the halfspace-intersection lemma

$$P \subseteq H^+ \implies H^- \cap \mathrm{conv}(P) = \mathrm{conv}(H^- \cap P),$$

for a union $P$ of finitely many polyhedra and opposite halfspaces $H^+, H^-$.

Theorem 3.3 — the exact necessary-and-sufficient condition

$$\mathrm{conv}\big[(\mathrm{conv}\,F_{j-1}) \cap D_j\big] = \mathrm{conv}(F_{j-1} \cap D_j) \iff \text{the constraint boundary condition holds for } F_{j-1}, D_j.$$

Significance

The results themselves. Theorem 3.1 is what makes sequential convexification a practical tool rather than a theoretical curiosity: for a 0-1 program with $n$ binary variables, it lets the convex hull be built in $n$ stages, each requiring only the facets of a two-term disjunction — tractable, in contrast to generating facets of the full integer hull directly. Theorem 3.3 puts the boundary of applicability on rigorous footing: faciality is sufficient but not necessary, and Theorem 3.3 pins down the exact condition, showing precisely why sequential convexification is a genuinely restrictive property (holding for 0-1 programs but not general integer programs) rather than a universal fact about unions of polyhedra.

Formalizing it. No object in this mission — faciality, the sequential-convexification recursion, or the relative-boundary constraint condition — exists on the platform prior to this mission or in Mathlib. This mission restates the disjunctive-set vocabulary of the earlier missions in this series locally (per the series convention that a draft mission cannot import another draft mission's definitions) and is otherwise self-contained.

Difficulty

The natural first guess is that sequential convexification should always work, since at each step the procedure only discards points excluded by a valid disjunction. The book's own two-variable integer-programming example (imposing integrality on $x_1$, then on $x_2$) refutes this directly: the resulting set strictly contains the true integer hull. The reason faciality repairs this is subtle and is exactly what Lemma 3.2 isolates: the recursion's correctness at each step needs the previous partial hull, intersected with the new disjunction's halfspace, to already equal the convex hull of the intersection taken before convexifying — and this commutation of convex hull and halfspace intersection is exactly what fails when the halfspace does not respect a face of the underlying polyhedron. Theorem 3.3 shows this is not merely Lemma 3.2's specific route to a sufficient condition, but the precise dividing line: the "if" direction says checking the boundary condition only for segments between two points already suffices, which is what makes facial sufficiency provable by induction in the first place.

Formalization scope

All results are stated over Fin n → ℝ with matrices Matrix (Fin m) (Fin n) ℝ. The disjunction structure uses a finite index type S with a dependent family of finite index types Qidx : S → Type*, matching the book's S, Q_j. Faciality (Facial) uses Mathlib's IsExtreme directly, matching the book's own primary definition of "defines a face" rather than its immediate "clearly equivalent" restatement (F₀ ⊆ {d_i x ≤ d_{i0}}). The relative boundary in Theorem 3.3 ("the boundary of $\bar D_j$ in the affine space spanned by $\bar D_j$") is Mathlib's intrinsicFrontier, the standard formalization of a set's boundary relative to its own affine hull. The book's own "$\in$" in the constraint boundary condition's conclusion (rather than "$\subseteq$", which set-membership syntax would require for a set on the left) is read as set inclusion, the only mathematically sound reading, and is transcribed as ⊆ in the Lean statement while the milestone's verbatim text preserves the book's own "$\in$" unchanged, per the verbatim-quotation convention.

A trivializing formalization is ruled out explicitly: Theorem 3.1 is stated for an arbitrary finite S and Qidx, not fixed at a small size (e.g. |S| = 1, which would make the recursion's endpoint trivially equal to a single step and prove nothing about sequencing), and the recursion's ordering σ is universally quantified rather than fixed to a canonical choice, matching the theorem's own order-independence claim.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 3.
• E. Balas, Disjunctive programming: Properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998), 3–44 (cited in the text as [6], the origin of Theorem 3.1).
• R. Stubbs, S. Mehrotra, A branch-and-cut method for 0-1 mixed convex programming, Mathematical Programming 86 (1999), 515–532 (cited in the text as [116], extending sequential convexifiability to convex mixed 0-1 programs).

Motivation

Theorem 2.1 (the previous mission in this series) shows that the closed convex hull of a union of polyhedra has a compact description after lifting to a higher-dimensional space. That description comes in two dual flavors: a primal one, as the projection of an explicit lifted polyhedron, and a polar one, characterizing the hull's facets directly via a cone built from the disjuncts' own data. Both flavors matter in practice: a cutting-plane algorithm needs to know exactly which inequalities are facet-defining (so as not to waste effort generating redundant cuts), and the two routes — projection and polarity — offer complementary tools for deciding this. This mission formalizes both routes and the machinery connecting them, closing out Chapter 2 of Balas, Disjunctive Programming (Springer, 2018).

The projection route (§2.2–2.3) develops general facts about projecting an arbitrary polyhedron that predate and underlie the disjunctive-programming application: the classical projection formula via extreme rays of a projection cone, how dimension and facet structure behave under projection, and a refinement (via a coordinate transformation) that eliminates the redundant inequalities the plain projection formula can produce. The polarity route (§2.4) develops the reverse polar, an object introduced by Balas specifically for this purpose, whose iterated application recovers the closed convex hull of a disjunctive set directly, culminating in an exact characterization of when an inequality is facet-defining purely in terms of extreme rays of an explicit cone $W_0$.

Setting

For a matrix system $(A,B,b)$ with $m$ rows, let $Q := \{(u,x) \in \mathbb{R}^p \times \mathbb{R}^q : Au+Bx \le b\}$, and let $\mathrm{Proj}_x(Q) := \{x : \exists\, u,\ (u,x) \in Q\}$ be its projection onto the $x$-space. The projection cone is $W := \{v : vA=0,\ v \ge 0\}$. A vector $v$ is an extreme ray of a cone $W$ if $v \ne 0$, $v \in W$, and the ray it generates is an extreme subset of $W$. The dimension $\dim(P)$ of a polyhedron is the dimension of its affine hull, and a set $F$ is a facet of $P$ if it is a proper face of $P$ of dimension $\dim(P)-1$. Partitioning $(A,B,b)$'s rows into those tight throughout $Q$ (the equality subsystem) and the rest, $r$ and $r^*$ denote the rank of the tight rows' combined and $A$-only submatrices, respectively.

For $S \subseteq \mathbb{R}^n$, the polar is $S^0 := \{x : xy \le 1\ \forall y \in S\}$ and the reverse polar is $S^\# := \{x : xy \ge 1\ \forall y \in S\}$; more generally the scaled polar at level $\alpha_0$ is $F_{(\alpha_0)} := \{y : xy \ge \alpha_0\ \forall x \in F\}$. For a disjunctive set $F = \bigcup_{h \in Q} P_h$ with $P_h := \{x : A_h x \ge b_h\}$ and $Q^* := \{h : P_h \ne \emptyset\}$, the cone $W_0 := \{(\alpha,\alpha_0) : \exists\, (u_h)_{h \in Q^*},\ \forall h,\ u_h A_h = \alpha,\ \alpha_0 \le u_h b_h,\ u_h \ge 0\}$.

Formalization targets

Theorem 2.18 (goal) — facet characterization via polarity

For a full-dimensional disjunctive set $F$ ($\dim(F)=n$) and $\alpha_0 \ne 0$:

$$\alpha x \ge \alpha_0 \text{ defines a facet of } \mathrm{cl\,conv}(F) \iff (\alpha,\alpha_0) \text{ is an extreme ray of } W_0.$$

The polarity chain feeding the goal

Proposition 2.13 ($0 \in \mathrm{cl\,conv}(S) \iff S^\# = \emptyset \iff S^\#$ bounded), Theorem 2.14 ($S^{\#\#} = \mathrm{cl\,conv}(S) + \mathrm{cl\,cone}(S)$ when $0 \notin \mathrm{cl\,conv}(S)$), Corollary 2.15 ($\mathrm{cl\,conv}(S) = S^{00} \cap S^{\#\#}$), Theorem 2.16 (the scaled polar stabilizes: $F_{(\alpha_0)}^{\#\#\#} = F_{(\alpha_0)}^{\#}$), and Corollary 2.17 ($F_{(\alpha_0)} = \{\alpha : (\alpha,\alpha_0) \in W_0\}$) — each the weakest statement needed for the next.

The projection track (independent of the goal's direct proof, sharing its definitions)

Theorem 2.5 ($\mathrm{Proj}_x(Q) = \{x : (vB)x \le vb,\ v \in \mathrm{extr}(W)\}$), Proposition 2.6 (projection preserves integrality), Theorem 2.7 ($\dim(\mathrm{Proj}_x(Q)) = \dim(Q)-p+r^*$), Corollaries 2.8–2.10 (facet/face behavior under projection), and Proposition 2.11 / Corollary 2.12 (sharper facet characterizations via a coordinate-transformed projection cone).

Significance

The results themselves. Theorem 2.18 is the practical payoff of the entire polarity apparatus: it turns "is this inequality facet-defining for the convex hull of a union of polyhedra" from a geometric question into an algebraic one about extreme rays of an explicit, finitely-generated cone built directly from the disjuncts' own constraint data — exactly the kind of question a cutting-plane algorithm needs answered to avoid generating redundant cuts. The projection track is foundational general polyhedral theory in its own right (Theorem 2.5's formula underlies Benders decomposition and classical Fourier-Motzkin elimination as special cases, per the book's own remarks), independently useful beyond the disjunctive setting.

Formalizing it. No object in this mission — polars, reverse polars, projection cones, extreme rays of a cone, or the dimension/facet apparatus of a polyhedron — exists on the platform prior to this mission or in Mathlib (a q=polar search returns only an unrelated cyclic-polytope construction from the Hirsch-conjecture series, with different conventions and object). This mission restates the disjunctive-set vocabulary of the companion ConvexHull mission locally (per the series convention that a draft mission cannot import another draft mission's definitions) and builds the polarity apparatus from scratch on top of it.

Difficulty

The natural first attempt at Theorem 2.18 tries to characterize facets of $\mathrm{cl\,conv}(F)$ directly from the lifted-polyhedron representation of Theorem 2.1, projecting facet by facet. This misses the point of the polarity route entirely: Theorem 2.18's proof instead goes through $F_{(\alpha_0)}$, showing a vertex of $F_{(\alpha_0)}$ corresponds to a nonhomogeneous subset of rank $n$ of $F_{(\alpha_0)}$'s own defining system being tight — algebra entirely in the dual space of multipliers, never touching the lifted polyhedron's facets directly. The two obstacles Theorem 2.14 and Proposition 2.13 exist to clear are, respectively: reverse polars do not satisfy the ordinary polar's clean involution property (an extra $\mathrm{cl\,cone}(S)$ summand appears, capturing recession directions the reverse-polar construction alone cannot see), and reverse polars are either empty or automatically unbounded (never merely "small"), which is why the apparatus needs the normalization $0 \notin \mathrm{cl\,conv}(F)$ throughout.

Formalization scope

All results are stated over finite index sets and matrices Matrix (Fin (m h)) (Fin n) ℝ (disjunctive-set data, m : Q → ℕ dependent) or Matrix (Fin m) (Fin p) ℝ / Matrix (Fin m) (Fin q) ℝ (projection-track data). PolyDim and IsFacet are stated generically over any real vector space (via Module.finrank of vectorSpan and Mathlib's IsExtreme), so the same definitions serve both Poly2-shaped pairs and cl conv F ⊆ Fin n → ℝ directly in Theorem 2.18. IsExtremeRay is likewise stated generically, reused for cones in plain vector space, (v,v0)-space, and the triple (v,w,v0)-space Proposition 2.11 needs.

Two results (Proposition 2.11, Corollary 2.12) build on a coordinate-transformed polyhedron Q̃/cone W̃ that the book itself only cites from [14] rather than constructing; consistent with the book's own treatment, this mission takes W̃ (or its (v,v0)-projection) as given data together with its defining relationship to Proj_x(Q), rather than re-deriving the transformation — a choice recorded in MODERATION_NOTES.md, not a weakening of either statement's content. Proposition 2.11's complexity remark ("O(max{m,q}³)") is a proof aside about the transformation's cost, not part of either result's mathematical claim, and is out of scope per the book-wide disposition (triage.json).

A trivializing formalization is ruled out explicitly: the projection-track results are stated for generic m, p, q, never fixed at small values, and Theorem 2.18 is stated for a generic finite disjunctive index set Q, not specialized to |Q| = 1 (which would collapse W_0 to ordinary LP polarity and prove nothing about unions).

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 2, §2.2–2.4.
• E. Balas, Disjunctive programming: Properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998), 3–44 (cited in the text as [6], the origin of the reverse-polar apparatus alongside [10]).
• Balas, Pordli (cited as [14] in the text) — the coordinate-transformation construction behind Proposition 2.11 and Corollary 2.12.
• Balas, Portugal (cited as [30] in the text) — the source of the dimensional results of §2.2.2.

Motivation

The generalized assignment problem (GAP) asks for the cheapest way to give each of $n$ tasks to exactly one of $m$ agents when every agent has a limited amount of a resource and different agents consume different amounts of it for the same task. It models assigning jobs to machines or computers, software tasks to programmers, commercials to time slots, and customers to single-source plants in capacitated facility location. The problem is NP-hard, so exact methods rely on lower bounds that are cheap to compute and strong enough to prune a branch and bound tree.

G. Terry Ross and Richard M. Soland (Mathematical Programming 8, 1975) gave such a bound. The relaxation that ignores the resource limits is solved by giving every task to its cheapest agent; the overloaded agents are then repaired by one small binary knapsack problem each, whose optimal values are added as penalties. Their paper then shows that this repaired bound is not an ad hoc heuristic: it is exactly the value of a Lagrangean relaxation of the GAP at an explicit choice of multipliers. This identity made the Ross–Soland bound the reference point for the later Lagrangean and column-generation methods for the GAP (for example Fisher, Jaikumar and Van Wassenhove, Management Science 1986 and Savelsbergh, Operations Research 1997).

Setting

Agents are $I=\{1,\dots,m\}$ and tasks $J=\{1,\dots,n\}$. Giving task $j$ to agent $i$ costs $c_{ij}$ and uses $r_{ij}\ge 0$ units of agent $i$'s resource; agent $i$ has $b_i>0$ units. The problem is

$$\text{(P)}\qquad \min\ \sum_{i\in I}\sum_{j\in J}c_{ij}x_{ij}\quad\text{s.t.}\quad\sum_{j\in J}r_{ij}x_{ij}\le b_i\ (i\in I),\quad\sum_{i\in I}x_{ij}=1\ (j\in J),\quad x_{ij}\in\{0,1\}.$$

Dropping the resource constraints gives the relaxation (PR). It is solved by choosing, for each task $j$, a cheapest agent $i_j$ with $c_{i_jj}=\min_{i}c_{ij}$ and setting $x_{i_jj}=1$; its value is $Z=\sum_jc_{i_jj}$. Let $J_i=\{j: i_j=i\}$ be the tasks this solution gives to agent $i$, $I'=\{i:\sum_{j\in J_i}r_{ij}>b_i\}$ the overloaded agents, and $d_i=\sum_{j\in J_i}r_{ij}-b_i$ the excess of agent $i$. The penalty of moving task $j$ away from $i_j$ is $p_j=\min_{k\ne i_j}(c_{kj}-c_{i_jj})$. For $i\in I'$ the binary knapsack problem

$$\text{(PK}_i)\qquad\min\ z_i=\sum_{j\in J_i}p_jy_{ij}\quad\text{s.t.}\quad\sum_{j\in J_i}r_{ij}y_{ij}\ge d_i,\quad y_{ij}\in\{0,1\}$$

chooses the cheapest set of tasks to move off agent $i$; call its optimal value $z^*_i$. The knapsack bound is

$$\mathrm{LB}=Z+\sum_{i\in I'}z^*_i .$$

Dualizing the assignment constraints with multipliers $\lambda_j$ gives the Lagrangean relaxation

$$\text{(PR}_\lambda)\qquad\min\ \sum_{i\in I}\sum_{j\in J}c_{ij}x_{ij}+\sum_{j\in J}\lambda_j\Bigl(1-\sum_{i\in I}x_{ij}\Bigr)\quad\text{s.t.}\quad\sum_{j\in J}r_{ij}x_{ij}\le b_i\ (i\in I),\quad x_{ij}\in\{0,1\}.$$

Finally $c_{1j}$ and $c_{2j}$ are the smallest and second smallest of $c_{1j},\dots,c_{mj}$, counted with multiplicity.

Formalization targets

Goal: the knapsack bound is the Lagrangean bound at $\lambda=c_2$

For every cheapest-agent choice $j\mapsto i_j$ and every choice of optimal knapsack solutions,

$$\mathrm{LB}=\min\Bigl\{\sum_{i}\sum_{j}c_{ij}x_{ij}+\sum_{j}c_{2j}\Bigl(1-\sum_{i}x_{ij}\Bigr)\ :\ x\ \text{feasible for (PR}_\lambda)\Bigr\},$$

the minimum being attained, and consequently $\mathrm{LB}\le\sum_i\sum_jc_{ij}x_{ij}$ for every $x$ feasible for (P). This is the paper's "principal result of this Lagrangean analysis" (§2, p. 96). It has no constants to improve; it is an identity between two optimization problems.

Milestones

In the paper's order of use: (PR) is solved by the cheapest agents (pp. 93–94); every lower bound on (PR$_\lambda$) is a lower bound on (P) (p. 95); (PR$_\lambda$) separates into one binary knapsack per agent (p. 95); at $\lambda=c_2$ the variables that are zero in the (PR) solution can be fixed at zero, the substitution $y_{ij}=1-x_{ij}$ turns agent $i$'s part into (PK$_i$), $p_j=c_{2j}-c_{1j}$, and agent $i$'s part has value $-\sum_{j\in J_i}p_j+z^*_i$ (p. 96). Two side results close the section: the solution obtained by moving the tasks the knapsacks select has cost exactly LB, so it is optimal whenever it is feasible (pp. 94–95); and the optimal dual multipliers of the bounded-variable linear program (PR$_L$) are exactly the vectors with $c_{1j}\le\lambda_j\le c_{2j}$ (pp. 95–96).

Significance

The identity says that a bound computed from one sorting pass and a handful of small knapsacks equals a Lagrangean dual bound at a closed-form multiplier. Validity of LB for (P) then follows from weak Lagrangean duality alone, and the multiplier $c_2$ is the upper end of the range of optimal dual multipliers of the linear program (PR$_L$), which the paper singles out as a suitable choice of multipliers. The rebuilt solution gives the algorithm a feasible incumbent at no extra cost whenever the knapsack repairs happen to respect all budgets.

The result is proved in the paper, in one sentence. The mission turns that sentence into checked statements: the separation of (PR$_\lambda$), the reduction of each agent's subproblem to (PK$_i$), the handling of ties among cheapest agents, and the role of nonnegative resources. As far as a search of the platform shows, nothing about the generalized assignment problem or its Lagrangean bounds has been formalized; the definitions here (assignment relaxations, per-agent knapsacks, bounded-variable duals) are reusable for other GAP and facility-location missions.

Difficulty

The Lagrangean relaxation at $\lambda=c_2$ is a larger problem than the knapsack bound suggests: a feasible $x$ may give a task to several agents or to none, and may use any agent, not only the cheapest one. The knapsack bound, by contrast, only looks at the tasks each agent receives in the (PR) solution. The paper bridges the two in one sentence of three observations, and each observation depends on a condition the sentence does not state: the sign of the resource coefficients, the treatment of agents that are not overloaded (for which no knapsack is solved), and ties among cheapest agents, which make some penalties zero and require the statement to hold for every tie-break. An inequality in one direction only (LB is a valid bound) is not the claim; the equality needs a feasible point of (PR$_\lambda$) whose value is exactly LB.

Formalization scope

Agents are Fin m and tasks Fin n, indexed from 0. Costs, resources, budgets, multipliers and variables are real numbers; a 0-1 variable is a real equal to 0 or 1, so the paper's sums are literal. The cheapest-agent selection is an arbitrary function a : Fin n → Fin m with IsCheapest c a, so every statement holds for every tie-break. $p_j$ and $c_{2j}$ are minima over the other agents, which requires $m\ge2$ (hm : 1 < m); $c_{2j}$ is proved to be the second smallest cost with multiplicity. Optimal values are never encoded as sInf: $z^*_i$ is the objective of a given optimal knapsack solution, and "the bound provided by (PR$_\lambda$)" is stated as a lower bound over all feasible points that is attained.

Standing hypotheses: $b_i>0$ (printed on p. 92), $r_{ij}\ge0$ (implicit in "the resource required", and necessary: with a negative $r_{ij}$ both (PR$_\lambda$) and (P) can fall below LB), and $m\ge2$. All costs are finite; the "not permissible" pairs of the paper's numerical example are outside the model.

A formalization that states only $\mathrm{LB}\le$ every (PR$_\lambda$) value, or that restricts the (PR$_\lambda$) competitors to the (PR) support or to at most one agent per task, would be a weaker theorem and does not meet the goal. The (PR$_L$) dual is written out explicitly with multipliers $u_{ij}\ge0$ for the bounds $x_{ij}\le1$; "each optimal dual multiplier lies anywhere in the range $c_{1j}\le\lambda_j\le c_{2j}$" is read as "the optimal multipliers are exactly this box".

Needed infrastructure is only finite sums over Fin and Finset.inf'. Proofs of the milestones, and lemmas on separable binary programs that could serve other Lagrangean-relaxation missions, are welcome.

Selected references

• G. T. Ross and R. M. Soland, A branch and bound algorithm for the generalized assignment problem, Mathematical Programming 8 (1975) 91–103. https://doi.org/10.1007/BF01580430
• A. M. Geoffrion, Lagrangean relaxation for integer programming, Mathematical Programming Study 2 (1974) 82–114. https://doi.org/10.1007/BFb0120690
• M. L. Fisher, R. Jaikumar and L. N. Van Wassenhove, A multiplier adjustment method for the generalized assignment problem, Management Science 32 (1986) 1095–1103. https://doi.org/10.1287/mnsc.32.9.1095
• M. Savelsbergh, A branch-and-price algorithm for the generalized assignment problem, Operations Research 45 (1997) 831–841. https://doi.org/10.1287/opre.45.6.831

Motivation

Retailers of seasonal goods sell at a full price first and mark down later. Customers who know this can wait for the markdown, and a firm that always has stock left for the markdown teaches them to wait. One remedy is to stock less than the low-price market would absorb, so that a customer who waits risks not getting the good at all. Liu and van Ryzin (Management Science 54(6), 2008) model this capacity rationing as a two-period game between a monopolist who chooses a stocking quantity and risk-averse customers who choose when to buy, and they characterize exactly when rationing is worth its cost in lost sales. The paper belongs to the revenue-management literature on strategic customers, where the firm's decision must anticipate the customers' best response to it.

Setting

A firm announces a price $p_1$ for period 1 and a lower price $p_2<p_1$ for period 2 and buys $C$ units at unit cost $\alpha<p_2$ before sales start; there is no replenishment. A market of $N>0$ customers, each wanting one unit, has valuations $v$ drawn independently from a distribution $F$; from §3 on, $F$ is uniform on $[0,\bar U]$.

Period-2 requests are filled at random with probability $q$, the fill rate, which customers anticipate correctly. Every customer has the same utility $u$: strictly increasing, concave, twice differentiable, with $u(0)=0$; from §3 on, $u(x)=x^\gamma$ with $0<\gamma<1$ (smaller $\gamma$ means more risk aversion). A customer with valuation $v$ buys in period 1 exactly when

$$v\ge p_1\quad\text{and}\quad u(v-p_1)\ge q\,u(v-p_2).$$

The threshold $v(q)$ separates early buyers from waiters.

Under the §3 assumptions, a cutoff $v\in[p_1,\bar U]$ is induced by the fill rate $q(v)=((v-p_1)/(v-p_2))^\gamma$ and the stocking quantity $C(v)=\frac{N}{\bar U}(\bar U-v+(v-p_2)q(v))$. The firm's profit from a segmented market is

$$\Pi(v)=\frac{N}{\bar U}\left((p_1-\alpha)(\bar U-v)+(p_2-\alpha)(v-p_2)\left(\frac{v-p_1}{v-p_2}\right)^\gamma\right),\tag{6}$$

and the profit from serving everybody at the low price is $\Pi^{NS}=(p_2-\alpha)\frac{N}{\bar U}(\bar U-p_2)$. The firm's optimal profit is the larger of $\Pi^0=\max_{p_1\le v\le\bar U}\Pi(v)$ and $\Pi^{NS}$. The first-order condition of (6) is

$$\left(\frac{v-p_1}{v-p_2}\right)^\gamma\left(1+\frac{\gamma(p_1-p_2)}{v-p_1}\right)-\frac{p_1-\alpha}{p_2-\alpha}=0,\tag{7}$$

with root $v^0>p_1$, and the critical valuation bound is

$$U_c=\frac{(p_2+\gamma(p_1-\alpha))v^0-p_2(p_1+\gamma(p_2-\alpha))}{v^0-p_1+\gamma(p_1-p_2)}.\tag{8}$$

In Lean these objects are IsCustomerUtility, buysEarly, cutoff (module LiuVanRyzin.Model) and fillRate, capacity, segProfit, lowPriceProfit, focLHS, criticalU (module LiuVanRyzin.PowerModel).

Formalization targets

Goal: Proposition 3 (p. 1122)

If $\bar U\ge U_c$, rationing is optimal: $v^0\in[p_1,\bar U]$, $v^0$ maximizes $\Pi$ on $[p_1,\bar U]$, and $\Pi(v^0)\ge\Pi^{NS}$. If $\bar U<U_c$, serving the whole market at the low price is optimal:

$$\Pi(v)\le\Pi^{NS}\qquad\text{for all }v\in[p_1,\bar U].$$

The goal fixes no constants; it is the paper's dichotomy, stated with its own (7) and (8).

Milestones, in attack order

1. Proposition 1 (p. 1120): for every $q\in[0,1)$ the threshold $v(q)\ge p_1$ exists and is unique, for a general utility.
2. Proposition 2 (p. 1120): $v(q)$ is strictly increasing in $q$, and convex if $u'''\ge 0$.
3. Proposition 5 (p. 1123): $C(v)$ and $q(v)$ are strictly increasing on $[p_1,\bar U]$, so choosing $C$ is the same as choosing $v$ or $q$.
4. §3.1, root of (7) (p. 1122): the left side of (7) strictly decreases on $v>p_1$ and changes sign, so $v^0$ exists and is unique.
5. Lemma 1 (p. 1122): $\Pi$ is strictly concave on $v\ge p_1$; its maximizer on $[p_1,\bar U]$ is $v^0$ if $v^0\le\bar U$, and $\bar U$ otherwise.
6. §3.1, bounds (p. 1122): $U_c$ decreases in $v^0$, $p_1<v^0<p_1+\gamma(p_2-\alpha)$, and $p_1+\gamma(p_2-\alpha)<U_c<p_1+p_2-\alpha$.

Significance

Proposition 3 answers the paper's central question: whether a firm facing strategic, risk-averse customers should deliberately under-stock. The answer depends on a single number, $U_c$, which depends on prices, cost and risk aversion but not on the market size, and it is compared with the top of the valuation range. Corollary 1, the $\gamma\to1$ limits of Proposition 4, and the comparative statics of Propositions 6–8 on how the optimal fill rate moves with $p_1$, $p_2$ and $\gamma$ are all read off from it. The bounds of milestone 6 turn it into sufficient conditions stated in the primitives alone.

The results are proved in the paper's e-companion (Online Appendix C). No machine-checked proof of any of them is known. Formalizing them gives a verified instance of a pattern that recurs throughout revenue management: a customer best response (a threshold), a reduction of the firm's problem to one scalar decision, a concavity argument, and a comparison of two regimes.

Difficulty

Most of the work is analysis of real powers with a moving base. $\Pi$ contains $(v-p_2)\bigl((v-p_1)/(v-p_2)\bigr)^\gamma$, whose derivative blows up at $v=p_1$, so its concavity on the closed half-line $[p_1,\infty)$ is not a routine second-derivative computation at the endpoint. The regime comparison in Proposition 3 is not implied by Lemma 1: Lemma 1 locates the segmented optimum, but whether it beats $\Pi^{NS}$ depends on $\bar U$, which enters $\Pi$ both through the prefactor $N/\bar U$ and through $\bar U-v$. The equivalence of that comparison with $\bar U\ge U_c$ requires eliminating $(v^0-p_1)/(v^0-p_2)$ with (7).

For Propositions 1–2 the utility is general: the threshold is defined by an inequality between $u(v-p_1)$ and $q\,u(v-p_2)$, and neither its monotonicity in $q$ nor its convexity under $u'''\ge0$ follows from a closed form. Only for $x^\gamma$ is there one.

Formalization scope

All quantities are real numbers. The utility of Propositions 1–2 is a function $u:\mathbb R\to\mathbb R$ that is strictly increasing, concave and continuous on $[0,\infty)$, twice differentiable on $(0,\infty)$, with $u(0)=0$. The threshold $v(q)$ is defined as the infimum of the set of early buyers, not assumed. Powers are Real.rpow; every power-model statement stays on $v\ge p_1$, or on $v>p_1$ where $(v-p_1)^{-1}$ appears. $\Pi$ is written in the closed form (6). The root $v^0$ is a binder constrained by $v^0>p_1$ and (7), and milestone 4 shows such a root exists. "Increases" in Propositions 2 and 5 is read as strictly increasing.

Hypotheses the paper uses without stating them, added here:

• $0\le p_2<\bar U$ in the goal. The uniform law gives $N\bar F(p_2)=\frac N{\bar U}(\bar U-p_2)$ only for $p_2\in[0,\bar U]$, and it makes $\bar U>0$.
• $p_1\le\bar U$ in the second part of Lemma 1, because (6) maximizes over the interval $[p_1,\bar U]$.
• Continuity of $u$ at $0$ in Propositions 1–2. The paper's "twice differentiable" implies it for any utility differentiable at $0$, and $x^\gamma$ satisfies it.
• In Proposition 2, "nonnegative third derivative" is read as $u\in C^3(0,\infty)$ with $u'''\ge0$ there.

The goal cannot be trivialized: $v^0$ is pinned to the root of (7), part 2 quantifies over every $v\in[p_1,\bar U]$, and the optimum is compared with $\Pi^{NS}$ exactly as the paper defines optimality.

Contributions are welcome at every level. Useful ones include the real-power calculus lemmas behind milestones 3–6, a proof of Propositions 1–2 for general concave utilities, and reusable facts about thresholds defined by single-crossing inequalities.

Selected references

• Q. Liu, G. van Ryzin, Strategic Capacity Rationing to Induce Early Purchases, Management Science 54(6):1115–1131, 2008. https://doi.org/10.1287/mnsc.1070.0832
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer, 2004. https://doi.org/10.1007/b139000

Motivation

Firms that sell new products (consoles, books, films) often take preorders before release. A preorder serves two purposes at once. It lets the firm charge early adopters a different price from later buyers, a form of price discrimination, and the number of preorders is advance demand information: an early signal of how large regular-season demand will be. Li and Zhang (MSOM 15(1), 2013) ask whether better advance information always helps a seller who runs a preorder, when consumers are strategic and anticipate the seller's stocking decision. Their answer is no. The second-period stocking decision improves, but the preorder price can fall. Whether the net effect is positive depends on the low-type margin and the size of the early-adopter segment.

This mission formalizes that answer, §4 of the paper: the preorder profit as a function of the demand correlation $\rho$.

Setting

A seller sells a perishable product over two periods. High-type consumers, with valuation $v_H$, arrive in the first period and may preorder at price $p_1$. Low-type consumers, with valuation $v_L < v_H$, arrive in the second period, when the price is $p_2$. A high type who waits values the product at $\delta v_H$, where $\delta \le 1$ and $\delta v_H > v_L$. The unit cost is $c$, with $0 < c < v_L$. Unsold units have no salvage value and unmet demand carries no penalty. Write $\Delta = \delta v_H - v_L$.

The demands are jointly normal with correlation $\rho \in [0,1)$. The high-type demand has mean $\mu_H$, and $X$ denotes its standardization, a standard normal variable. The low-type demand has mean $\mu_L$, standard deviation $\sigma_L$ and $\lambda_L = \mu_L/\sigma_L$. Given $X = x$, the updated low-type demand $\tilde X_L(x)$ is normal with mean $\tilde\mu_L(x) = \mu_L + \rho\sigma_L x$ and standard deviation $\tilde\sigma_L = \sigma_L\sqrt{1-\rho^2}$. $\Phi$ and $\phi$ are the standard normal distribution function and density, and $z_L$ solves $\Phi(z_L) = (v_L - c)/v_L$.

In the second period the seller charges $p_2 = v_L$ and solves a newsvendor problem. It orders

$$Q(x) = \tilde\mu_L(x) + z_L\tilde\sigma_L \qquad (1)$$

and earns $\Pi_L(x) = (v_L - c)(\mu_L + \rho\sigma_L x) - v_L\phi(z_L)\sigma_L\sqrt{1-\rho^2}$ (2). A waiting high type believes half of the remaining consumers will be served before her, so her belief of product availability is

$$\xi(\rho) = \mathbb E\Big[\Pr\Big(\tfrac{\tilde X_L(X)}{2} < Q(X)\Big)\Big]. \qquad (3)$$

In the rational-expectations equilibrium every high type preorders at $p_1 = v_H - \Delta\xi$. The preorder profit is

$$\Pi^p(\rho) = (v_H - \Delta\xi(\rho) - c)\mu_H + \Pi_L(0). \qquad (4)$$

The threshold is

$$\tilde\mu(\rho) = -\frac{v_L\phi(z_L)\sigma_L}{2\Delta z_L\,\phi\big(2z_L\sqrt{1-\rho^2} + \lambda_L\big)}. \qquad (6)$$

Formalization targets

Goal: PROPOSITION 2

$$\begin{aligned} &\text{(i) } c < v_L < 2c:\ \Pi^p \text{ strictly increases on every interval where } \mu_H < \tilde\mu(\rho),\\ &\qquad\text{and strictly decreases on every interval where } \mu_H \ge \tilde\mu(\rho);\\ &\text{(ii) } v_L \ge 2c:\ \Pi^p \text{ strictly increases on } [0,1). \end{aligned}$$

Milestones

1. (1)–(2): $Q(x)$ is the unique maximizer of $\mathbb E[v_L\min(Q,\tilde X_L(x)) - cQ]$, and its value is $\Pi_L(x)$.
2. (3): $\xi(\rho) = \mathbb E\big[\Phi\big((\lambda_L + \rho X)/\sqrt{1-\rho^2} + 2z_L\big)\big]$.
3. LEMMA 1(i): if $c < v_L < 2c$, then $z_L < 0$ and $\xi$ is strictly increasing in $\rho$.
4. LEMMA 1(ii): if $v_L \ge 2c$, then $z_L \ge 0$ and $\xi$ is non-increasing in $\rho$, strictly so when $v_L > 2c$.
5. After (5): $\dfrac{d}{d\rho}\Pi_L(0) = v_L\phi(z_L)\sigma_L\,\rho/\sqrt{1-\rho^2} > 0$ for $\rho \in (0,1)$.
6. PROPOSITION 2(i), pointwise: for $\rho \in (0,1)$, $d\Pi^p/d\rho > 0 \iff \mu_H < \tilde\mu(\rho)$ and $d\Pi^p/d\rho < 0 \iff \mu_H > \tilde\mu(\rho)$.
7. LEMMA 2(i): if $-\lambda_L/2 < z_L < 0$, then $\tilde\mu$ is strictly increasing in $\rho$.
8. LEMMA 2(ii): if $z_L \le -\lambda_L/2$, then $\tilde\mu$ is quasi-convex in $\rho$.

Significance

The proposition splits the value of advance demand information into two effects with opposite signs. Better information always raises the second-period profit (milestone 5). Its effect on the preorder price depends on the margin. When $v_L < 2c$, the seller stocks below the conditional mean. A more precise forecast then raises the stock and the availability $\xi$, and waiting becomes more attractive, which lowers the preorder price. The threshold $\tilde\mu(\rho)$ says which effect wins, and LEMMA 2 describes its shape. This is the basis for the paper's later comparisons of preorder, price-guarantee and no-preorder strategies.

The paper states these results and leaves the proofs to an online appendix. None of them has a machine-checked proof. A complete development would also give reusable facts about normal laws: the expectation $\mathbb E[\Phi(a + bX)]$ for standard normal $X$, the normal newsvendor solution with its closed-form optimal profit, and derivatives of Gaussian integrals with respect to a correlation parameter.

Difficulty

The model is explicit, so the difficulty is not in modelling. It is in turning the two expectations into closed forms and differentiating them. The availability $\xi$ is an integral over $X$ of a normal probability whose mean and variance both move with $\rho$. The expected newsvendor profit involves $\mathbb E[\min(Q, Y)]$ for a normal $Y$. Neither closed form is in Mathlib, and neither is a derivative in $\rho$ of a Gaussian integral. The obvious route, differentiating under the integral sign in (3), needs domination estimates that are uniform in $\rho$ near each point, and these degenerate as $\rho \to 1$.

Signs are the second difficulty. $z_L$ changes sign at $v_L = 2c$, $\tilde\mu$ carries a leading minus and divides by $z_L$, and the derivative of $\Pi^p$ vanishes at $\rho = 0$ and wherever $\tilde\mu(\rho) = \mu_H$. Strict monotonicity on an interval has to be recovered from a derivative that is positive except at finitely many points.

Formalization scope

Everything lives in the namespace PreorderADI.Correlation. A structure Params holds $v_H, v_L, c, \delta, \mu_H, \mu_L, \sigma_L, z_L$. The predicate Params.Standing records the model's assumptions: $v_H > v_L$, $c < v_L$, $\delta \le 1$ and $\delta v_H > v_L$, together with $\Phi(z_L) = (v_L-c)/v_L$. $\sigma_H$ is omitted because nothing in §4 uses it after standardization. $\Phi$ is ProbabilityTheory.cdf (gaussianReal 0 1) and $\phi$ is gaussianPDFReal 0 1. The normal law with mean $m$ and standard deviation $s$ is gaussianReal m (s^2).

The formalization commits to the following conventions and additions:

• Added hypotheses. Four hypotheses are added to the page's assumptions:
  • $c > 0$, so that $z_L$ exists;
  • $\sigma_L > 0$, so that the conditional law is a genuine normal law;
  • $\mu_L > 0$, so that $\lambda_L > 0$, as LEMMA 2 presupposes;
  • $\mu_H > 0$, which PROPOSITION 2(ii) needs.
• $z_L$. $z_L$ is a parameter pinned down by $\Phi(z_L) = (v_L-c)/v_L$, not an inverse function with junk values.
• Range of $\rho$. $\rho$ ranges over $[0,1)$, the paper's "we will focus on $\rho \ge 0$" together with $\rho < 1$. Derivative statements use $(0,1)$.
• $\xi$ and $\Pi^p$. $\xi$ is defined as the first expression of (3), the expected probability, so that no closed form is assumed. $\Pi^p$ is defined by (4). PROPOSITION 1, which derives (4) as the unique equilibrium profit, is not formalized: the paper defines the equilibrium only through conditions that already assume every high type preorders.
• Monotonicity. "Increases in $\rho$ when $\mu_H < \tilde\mu(\rho)$" is formalized as strict monotonicity on every order-connected $I \subseteq [0,1)$ on which the condition holds. "Decreasing" in LEMMA 1(ii) is non-strict, since $\xi$ is constant when $v_L = 2c$. Quasi-convexity is Mathlib's QuasiconvexOn.
• The ε_v sentence is omitted. PROPOSITION 2(i) also claims that some $\varepsilon_v > 0$ makes $\Pi^p$ always decrease when $v_L < c + \varepsilon_v$. That claim is false in the paper's own model. As $v_L \downarrow c$, $\tilde\mu(\rho) \to \infty$ for $\rho$ below roughly $\sqrt 3/2$, so $\Pi^p$ increases there for every fixed $\mu_H$. The paper's Figure 1 shows the same behaviour.
• Out of scope. §5 rests on an approximation that treats normal demands as nonnegative, so it is excluded. §§6–7 depend on models given only in the online appendix and are excluded too.

A statement about the closed form $\Phi(\lambda_L + 2z_L\sqrt{1-\rho^2})$ in place of $\xi$ would make LEMMA 1 a one-line monotonicity fact. So would a definition of $\Pi^p$ that bypasses (3). The definitions rule both out.

Welcome contributions include proofs of the milestones, general Mathlib-style lemmas on Gaussian expectations of $\Phi$ and of $\min(Q, Y)$, and a formalization of PROPOSITION 1 from conditions (i)–(v).

Selected references

• C. Li and F. Zhang, Advance Demand Information, Price Discrimination, and Preorder Strategies, Manufacturing & Service Operations Management 15(1):57–71, 2013. https://doi.org/10.1287/msom.1120.0398
• G. P. Cachon and R. Swinney, Purchasing, Pricing, and Quick Response in the Presence of Strategic Consumers, Management Science 55(3):497–511, 2009. https://doi.org/10.1287/mnsc.1080.0948
• X. Su and F. Zhang, On the Value of Commitment and Availability Guarantees When Selling to Strategic Consumers, Management Science 55(5):713–726, 2009. https://doi.org/10.1287/mnsc.1080.0967