The OR Formalization Drive

Motivation

The Legendre-Fenchel transform is the single most structurally important operation in convex analysis: for a proper closed convex function $f$, its conjugate $f^\bullet(p) = \sup_x \{\langle p,x\rangle - f(x)\}$ is again proper closed convex, and the transform is an involution — $f^{\bullet\bullet} = f$. This one fact underlies duality theory across optimization: every strong-duality theorem is, at bottom, a statement about conjugate pairs. Chapters 6 and 7 of this book developed M-convex and L-convex functions as if they were two separate theories, each with its own exchange axiom, optimality criterion, and proximity theorem. Chapter 8 reveals they were never separate: the Legendre-Fenchel transform, suitably discretized, is a bijection between the two classes. This mission formalizes that discrete conjugacy theorem together with its classical real-valued precursor and a genuine function-level generalization of Edmonds's intersection theorem, completing the picture that chunks 06 through 09 built the two halves of.

Setting

Let $V$ be a finite ground set. For $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$, the Legendre-Fenchel transform is $f^\bullet(p) = \sup\{\langle p,x\rangle - f(x) : x \in \mathbb R^V\}$; $f$ is submodular if $f(x)+f(y) \ge f(x\vee y)+f(x\wedge y)$ and supermodular under the reverse inequality. For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$, the discrete Legendre-Fenchel transform restricts the same supremum formula to $p \in \mathbb Z^V$: $f^\bullet(p) = \sup\{\langle p,x\rangle - f(x) : x \in \mathbb Z^V\}$ for $p \in \mathbb Z^V$ — a genuinely different object from the real-valued transform, since the supremum is now over integer $x$ only, and the codomain is checked back against the discrete M-/L-convexity axioms of chunks 06–09. The integer biconjugate $f^{\bullet\bullet}$ is the transform applied twice. $f$ is integer valued if every finite value it takes is an integer (the classes $M[\mathbb Z\to\mathbb Z]$, $L[\mathbb Z\to\mathbb Z]$ of the goal theorem are exactly the M-/L-convex functions with this property).

Formalization targets

Goal: Theorem 8.12 (the discrete conjugacy theorem)

(1) The classes $M[\mathbb Z\to\mathbb Z]$ and $L[\mathbb Z\to\mathbb Z]$ are in one-to-one correspondence under the discrete Legendre-Fenchel transform: for $f \in M[\mathbb Z\to\mathbb Z]$ and $g \in L[\mathbb Z\to\mathbb Z]$, $f^\bullet \in L[\mathbb Z\to\mathbb Z]$, $g^\bullet \in M[\mathbb Z\to\mathbb Z]$, $f^{\bullet\bullet}=f$, and $g^{\bullet\bullet}=g$. (2) The same correspondence holds between $M^\natural[\mathbb Z\to\mathbb Z]$ and $L^\natural[\mathbb Z\to\mathbb Z]$.

Milestones: Theorem 8.1, Proposition 8.11, Theorem 8.17

Theorem 8.1: the conjugate of a real-valued submodular function is always supermodular — the classical warm-up, and evidence that submodularity/supermodularity is not symmetric under conjugation on its own (the converse fails). Proposition 8.11: the integer biconjugate recovers $f$ at any point with a nonempty integer subdifferential — the fact that makes discrete biconjugation meaningful at all. Theorem 8.17 (the M-convex intersection theorem): a point jointly minimizes a sum of two M$^\natural$-convex functions if and only if a single linear functional separately certifies it as a minimizer of each perturbed function — the function-level generalization of chunk 04's Edmonds's intersection theorem for M-convex sets.

Significance

The result itself. The discrete conjugacy theorem is, in the book's own words, "the unifying result of the entire book": every theorem proved separately for M-convex functions (chunks 06–07) has an exact mirror for L-convex functions (chunks 08–09) precisely because the Legendre-Fenchel transform carries one class to the other. Theorem 8.17's function-level Edmonds generalization shows the payoff directly — the classical matroid-intersection-style min-max duality of chunk 04 was never really about sets; it is a special case (indicator functions) of a duality that holds for the whole class of M-convex functions.

Formalizing it. No matching item exists on the platform for conjugate functions, discrete conjugacy, or this generality of intersection theorem. This mission gives the first formal statement of the discrete conjugacy theorem, distinguishing it carefully from its real-valued (polyhedral) precursor, Theorem 8.4 — a genuinely different, harder theorem this mission does not draft (see Formalization scope), since the integer bijection needs the M-/L-proximity theorems of chunks 06–09 to control integrality under convex extension, while the real-valued case does not.

Difficulty

The obvious approach — try to prove the discrete conjugacy theorem directly by mimicking the real-valued proof (Theorem 8.4) with ℤ in place of ℝ everywhere — fails, because the real-valued proof's key step (Proposition 8.3, an infimal-convolution argument comparing arg min sets of perturbed polyhedral functions) has no immediate discrete analogue: a discrete arg min need not vary continuously with the perturbation the way a polyhedral one does. The book's actual strategy instead routes through the convex extension of the discrete function (chunk 06/08's bridge to chapter 3's integral convexity), applies the already-proved real-valued conjugacy theorem to the extension, and then must separately argue that the resulting conjugate, restricted back to integer points, is again integer-valued and satisfies the discrete exchange axiom — an argument that needs different treatment depending on whether the original function's domain is bounded or unbounded (an exhaustion argument via restriction to a growing integer interval, invoking chunk 06's proximity theorem to control convergence). Skipping this discreteness argument and treating the real-valued theorem as if it settled the integer case would silently discard exactly the chapter's own point.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq. ConvexConjugate (the discrete transform) has domain and codomain both (V → ℤ) → WithTop ℝ, obtained by taking the defining supremum in EReal (a complete lattice, so it is always total) and projecting back via a new FromEReal map — this is what lets the biconjugate f•• typecheck as an equality of functions of the same type as f. ConvexConjugateR (the real-valued transform, used only by the milestone Theorem 8.1) is a separate object with no shared code, per the explicit warning against conflating the two transforms; the two never appear in the same item.

A trivializing formalization of the goal would draft only the real-valued case (Theorem 8.4) as if it were the discrete theorem, or would silently allow WithTop ℝ's subtraction-avoidance convention to change which values are compared; neither is done. Theorem 8.4 itself (the polyhedral conjugacy theorem) is not drafted in this mission at all — it would require a fresh, otherwise-unused polyhedral M-/L-convex-function layer on Rⱽ that no other item here needs (see MODERATION_NOTES.md). The M-/L-separation theorems (8.15, 8.16) and the Fenchel-type duality theorem (8.21) are likewise left for a follow-on mission; contributions building the polyhedral bridge or the separation theorems, which depend on machinery this mission establishes, are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.

Motivation

Chapter 8 is where discrete convex analysis explains why it needed two separate notions — M-convexity (exchangeability) and L-convexity (submodularity) — rather than one. The answer is conjugacy: under the classical Legendre-Fenchel transform, the two classes turn out to be exactly dual to each other, the discrete analogue of the fact that convex analysis's transform is self-dual within a single class of convex functions. Mission 10-conjugacy-i proved the integer-lattice version of this fact (Theorem 8.12) but explicitly deferred the polyhedral version — Theorem 8.4, the chapter's own headline "Conjugacy theorem" — noting it needed a real-variable M-/L-convex-function layer the series had not yet built. That layer now exists, built across missions 23-24-ch06*-mconvexfunctions and 26-27-ch07*-lconvexfunctions. This mission proves Theorem 8.4 and its companions: the polar-cone correspondence it induces, its nonpolyhedral generalization, the separation and Fenchel-duality theorems for M♮-/L♮-convex functions, and the basic theory of M2-convex functions (sums of M-convex functions), which the Edmonds intersection theorem's own combinatorics is built from.

Setting

Fix a finite ground set $V$. For $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$, the Legendre-Fenchel transform is $f^\bullet(p) = \sup_x [\langle p,x\rangle - f(x)]$. A polyhedral convex function $f$ is M-convex ($f \in M[\mathbb R \to \mathbb R]$) if it satisfies (M-EXC[R]); $g$ is L-convex ($g \in L[\mathbb R \to \mathbb R]$) if it satisfies (SBF[R]) and (TRF[R]). A concave function $h$ is always represented via $h_2 = -h$, an ordinary convex function, so every "$f \ge h$" hypothesis is restated as "$f + h_2 \ge 0$" — an equivalent formulation avoiding any need to represent $-\infty$ in the codomain. A polyhedral cone's polar is $C^\circ = \{y : \langle y,x\rangle \le 0\ \forall x \in C\}$. A function is M2-convex if it is the sum of two M-convex functions.

Formalization targets

Goal: the conjugacy theorem (Theorem 8.4)

The classes of polyhedral M-convex functions and polyhedral L-convex functions are in one-to-one correspondence under the Legendre-Fenchel transform: $f \in M \Rightarrow f^\bullet \in L$, $g \in L \Rightarrow g^\bullet \in M$, and the transform is an involution ($f^{\bullet\bullet}=f$, $g^{\bullet\bullet}=g$) on each class, with the identical statement for the M$^\natural$/L$^\natural$ variants. This is the theorem mission 10-conjugacy-i deferred, citing exactly the missing infrastructure this series has since built.

Supporting structural targets

Twelve further results build the surrounding theory. Proposition 8.2 gives the easy two-variable case of the general submodularity-preservation fact (Theorem 8.1, already a milestone of mission 10-conjugacy-i); Proposition 8.3 is the technical minimizer-difference lemma the goal's harder direction is built from. Theorem 8.5 derives the M-convex/L-convex cone polarity from the goal, and Theorem 8.6 extends the correspondence beyond the polyhedral case to general closed proper convex functions. Proposition 8.14 and Theorems 8.15-8.16 build the separation theory for M♮-/L♮-convex and concave function pairs, with integral witnesses when the functions are integer valued; Theorem 8.21 (parts 1-2) derives the Fenchel-type strong-duality equality these separation theorems make possible. Propositions 8.29-8.30 and Theorem 8.31 (plus Theorem 8.32, found by direct reading immediately after 8.31) build the basic theory of M2-convex functions: their domains and minimizer sets are M2-convex, they are integrally convex, and their global optimality reduces to a finite local check.

Significance

The goal is the theorem that retroactively explains this entire series' two-track structure: missions 20-25 (M-convex sets and functions) and 08/21/26-28 (L-convex sets and functions) are not two independent theories that happen to share techniques — they are conjugate images of each other, so every theorem proved on one side has a dual counterpart automatically available on the other via Theorem 8.4. This is made concrete immediately: Theorem 8.5's cone polarity and the diagram the book draws connecting $M_0[\mathbb R]$, $0L[\mathbb R\to\mathbb R]$, and submodular set functions $S[\mathbb R]$ (already correspondences this series proved independently, in missions 24-ch06d-mconvexfunctions and 28-ch07d-lconvexfunctions) are shown to be facets of one single conjugacy fact rather than three separate coincidences. The separation and Fenchel duality theorems (8.15, 8.16, 8.21) are the discrete analogues of the two theorems every convex optimization course opens with, and the book is explicit that they are not corollaries of the classical versions plus convex extensibility — they carry genuinely combinatorial content, specializing to Frank's discrete separation theorem and Edmonds's intersection theorem as examples the book itself gives.

None of these results are open — they are Murota's account of the duality at the heart of discrete convex analysis, the reason the theory needed two dual notions rather than one. What this mission contributes is a faithful, machine-checked formal statement of each, completing a theorem mission 10-conjugacy-i explicitly left for a future session once the necessary polyhedral apparatus existed, and including one result (Theorem 8.32) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal's harder direction (L⇒M) would try to verify the exchange inequality for $g^\bullet$ directly from the definition of the transform; the book's actual proof instead identifies the exchange inequality with a statement about weighted minimizers of $g$ itself via Proposition 8.3 (the minimizer-difference bound), converting a claim about the conjugate function into a claim about $g$'s own combinatorial structure — a genuine change of perspective, not a direct calculation. Proposition 8.3's own proof is the hardest single argument in this block: it derives the minimizer-difference bound by a contradiction argument that constructs an explicit pair of "worse" minimizers via a join/meet perturbation and derives a strict inequality from Theorem 7.29's translation inequality — a multi-step combinatorial argument with no direct shortcut.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; convex functions are WithTop ℝ valued throughout (never EReal, except for the Legendre-Fenchel transform itself, whose defining supremum/infimum can genuinely be infinite). All thirteen numbered results found in this chunk's page range — the twelve in BRIEF.md's own table plus Theorem 8.32 — are placed, with one documented scope reduction: Theorem 8.21 states only its real-attainment parts (1)-(2), not the integer-attainment refinement of parts (3)-(4), which needs a separate argument no other result in this chunk requires — see HARD.md. Concave functions $h$ are always represented via $h_2 = -h$ and every inequality $f \ge h$ restated as $f + h_2 \ge 0$, avoiding WithTop ℝ negation entirely. This chunk's own BRIEF.md inherited the chapters-4-7 page-offset boilerplate (printed = PDF $-$ 19); chapter 8 uses offset 18, confirmed against the PDF's own footers — every citation here uses the corrected offset. This mission's base vocabulary is redeclared from missions 10-conjugacy-i, 20-ch04b-mconvexsets, 21-ch05b-lconvexsets, 23-24-ch06*-mconvexfunctions, and 26-27-ch07*-lconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the thirteen sorrys are welcome; the goal and Proposition 8.3 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota and A. Shioura, "M-convex function on generalized polymatroid," Mathematics of Operations Research, 24 (1999), pp. 95-105 [152] (the polyhedral M-/L-convex conjugacy theory this mission's real-variable results are drawn from).

Motivation

Mission 29-ch08b-conjugacyduality opened chapter 8's account of M2-convex functions — sums of M-convex functions — proving their domains and minimizers are M2-convex and that they are integrally convex. This mission completes that program and builds its exact mirror for L2-convex functions (integer infimal convolutions of L-convex functions), the class that appears on the opposite side of Edmonds's intersection theorem's min-max relation from M2-convexity. It proves optimality and proximity theorems for both classes, shows their subdifferentials add (a discrete analogue of the classical subdifferential sum rule), derives how the Legendre-Fenchel transform interacts with the sum/infimal-convolution operation, and — the technically hardest result in the whole cluster — establishes that L♮₂-convex functions are integrally convex, by a genuinely different and more intricate argument than the M2-side analogue required.

Setting

Fix a finite ground set $V$. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is L2-convex if $g = g_1 \square g_2$, the integer infimal convolution $g_1\square g_2(p) = \inf\{g_1(p_1)+g_2(p_2) : p_1+p_2=p\}$, of two L-convex functions $g_1, g_2$; L$^\natural_2$-convex if the summands are L$^\natural$-convex. An M2-convex function is a sum $f_1+f_2$ of two M-convex functions (mission 29-ch08b-conjugacyduality). The integer subdifferential $\partial_{\mathbb Z} f(x)$ and real subdifferential $\partial_{\mathbb R} f(x)$ generalize the subgradient set to integer- and real-valued perturbation directions respectively.

Formalization targets

Goal: L$^\natural_2$-convex functions are integrally convex (Theorem 8.42)

Every L$^\natural_2$-convex function is integrally convex, and in particular every L$^\natural_2$-convex set is integrally convex. The book's own proof is the most intricate argument in this cluster: given $p$ in the Minkowski sum $D_1+D_2$ of two L-convex sets, it constructs an explicit representation of $p$ as a convex combination of finitely many integer points of $D_1+D_2$, all lying in $p$'s own integral neighborhood, via the sorted fractional-part values of a chosen decomposition $p=p_1+p_2$ — a genuinely different technique from the M2-side analogue (Theorem 8.31), whose proof is a two-line consequence of convex extensibility.

Supporting structural targets

Eleven further results build the M2-/L2-convex theory in parallel. Theorems 8.33-8.34 give the M2-optimality criterion (a nonnegative-sum condition over cyclic exchange families) and its scaling-based proximity theorem; Theorem 8.35 shows subdifferentials of a sum of M$^\natural$- convex functions add, and that subdifferentials of M2-/M$^\natural_2$-convex functions are L2-/L$^\natural_2$-convex; Theorem 8.36 computes the conjugate of a sum as the infimal convolution of conjugates, with biconjugacy recovering the original sum. Propositions 8.39-8.41 transfer L-(natural-)convexity from summands to the domain and minimizer set of an L2-convex function, and give the precise attainment condition under which a linearly-perturbed infimal convolution's minimizer set splits additively. Theorems 8.43-8.44 give the L2-optimality and L2-proximity theorems, the exact L-side mirrors of Theorems 8.33-8.34; Theorem 8.45 mirrors Theorem 8.35 for subdifferentials of an infimal convolution; and Theorem 8.46 (found by direct reading, immediately following 8.45 and explicitly named by the book as 8.36's counterpart) shows biconjugacy for L$^\natural$-convex infimal convolutions.

Significance

The M2-/L2-convex function classes are where discrete convex analysis's abstract machinery meets concrete combinatorial optimization: Edmonds's matroid intersection theorem and its generalizations are literally statements about M2-convex minimization, with the L2-convex side supplying the dual bound. Theorem 8.35's subdifferential additivity is the discrete analogue of the classical Moreau-Rockafellar sum rule, and its proof (via the M-convex intersection theorem, already a milestone of mission 10-conjugacy-i) shows the sum rule holding without the constraint-qualification technicalities the continuous theory needs — a case where the discrete theory is cleaner than its continuous ancestor. Theorem 8.42's harder, dedicated proof technique is itself informative: it demonstrates that L2-convexity's combinatorial structure is not a routine transcription of the M2-convex case, foreshadowing the book's broader theme that M- and L-convexity, while conjugate, are not interchangeable in how their proofs actually work.

None of these results are open — they are Murota's account of the sum/infimal-convolution closure properties of M-convex and L-convex functions, continuing chapter 8's duality program into its most combinatorially concrete corner. What this mission contributes is a faithful, machine-checked formal statement of each, including one result (Theorem 8.46) the platform's own automated extractor missed, extending the shared Lean vocabulary (InfConv, L2Convex, M2ConvexSet) mission 29-ch08b-conjugacyduality began; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to adapt the M2-side integral-convexity proof (a direct appeal to convex extensibility) verbatim; the book's own proof shows this does not work, requiring instead a from-scratch construction: decompose $p=p_1+p_2$, take fractional parts $a_1 = p_1-\lfloor p_1\rfloor$ and $a_2=\lceil p_2\rceil-p_2$, sort their combined distinct values, build threshold sets exactly as in the Lovász-extension construction, and verify each resulting integer point $q_i = \lfloor p_1\rfloor+\chi_{U_{1i}}+\lceil p_2\rceil-\chi_{U_{2i}}$ both lies in $D_1+D_2$ (via L-convex-set closure properties, Theorem 5.10) and in $p$'s integral neighborhood (a case split on whether $p(v)$ is itself an integer) — a genuinely multi-stage combinatorial argument with no single-inequality shortcut, unlike almost every other result in this mission.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; M2-/L2-convex functions are (V→ℤ)→WithTop ℝ. All twelve numbered results found in this chunk's page range are placed, with no partial-coverage scope reduction needed — every clause of every result, including all three parts of Theorems 8.35 and 8.45 and the full cyclic-exchange condition of Theorems 8.33-8.34, is stated in full. One numbered result nominally in this chunk's page range, Theorem 8.32, is not re-placed here: it was already found and placed as a milestone in mission 29-ch08b-conjugacyduality, whose own page range overlaps this chunk's by one page (PDF245) — see HARD.md. "g1□g2 > −∞" hypotheses are omitted rather than translated, since WithTop ℝ has no −∞ element to violate. This mission's base vocabulary is redeclared verbatim from mission 29-ch08b-conjugacyduality rather than imported, since sibling drafts in this series cannot yet reference one another; ConvexConjugate is redeclared from mission 10-conjugacy-i. Contributions completing any of the twelve sorrys are welcome; the goal and Theorem 8.35 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota and A. Shioura, "Extreme points of a generalized polymatroid," Discrete Applied Mathematics, 152 (2005), pp. 268-278 [153] (the L2-convex integral-convexity proof this mission's goal is drawn from).
• K. Murota and A. Tamura, "Application of M-convex submodular flow problem to mathematical economics," Japan Journal of Industrial and Applied Mathematics, 20 (2003), pp. 257-277 [162] (the M2-proximity theorem, Theorem 8.34).

Motivation

Missions 29-ch08b-conjugacyduality and 30-ch08c-conjugacyduality built the M2-/L2-convex function classes and proved their conjugacy correspondence is nearly complete. This mission finishes that correspondence (Theorems 8.48-8.49) and then turns to chapter 8's capstone application: a Lagrangian duality theory for integer programs, built entirely from the M-/L-convexity machinery developed across the whole book. It develops the general perturbation-based duality framework (mirroring Rockafellar's conjugate duality for nonlinear programming), specializes it to M-convex programs via the perturbation $F_r$, and proves the strong duality theorem this specialization exists to deliver — together with its mirror construction recovering the primal problem from the dual.

Setting

An M-convex program consists of a set $B\subseteq\mathbb Z^V$ satisfying (REG) — $B$ is an M-convex set — and an objective $c:\mathbb Z^V\to\mathbb Z\cup\{+\infty\}$ satisfying (OBJ) — $c$ is an M-convex function. The general duality framework embeds any $f(x)=c(x)+\delta_B(x)$ in a family of perturbed problems via $F:\mathbb Z^V\times\mathbb Z^V\to\mathbb Z\cup\{+\infty\}$ with $F(x,0)=f(x)$, yielding an optimal-value function $\varphi$, a Lagrangian $K$, and a dual objective $g$. For M-convex programs the perturbation $F_r(x,u)=c(x)+\delta_B(x+u)+r(u)$, for an M-convex regularizer $r$ with $r(0)=0$, makes this framework concrete; the case $r\equiv 0$ is written with subscript $0$.

Formalization targets

Goal: Strong duality for M-convex programs (Theorem 8.59)

For a feasible, bounded-below M-convex program, $\min(P)=\varphi_r(0)=\varphi_r^{\bullet\bullet}(0) =\max(D_r)$, and $\operatorname{opt}(D_r)=-\partial_{\mathbb Z}\varphi_r(0)$. This is the theorem mission 11-conjugacy-ii-lagrange's own STATUS.md explicitly deferred, noting it needs the specific M-convex perturbation $F_r$ (Eq. (8.61)) and Propositions 8.55-8.56/Theorems 8.57-8.58 as prerequisites — all built as milestones of this mission.

Supporting structural targets

Theorem 8.48 completes the M2-/L2-convex conjugacy correspondence; Theorem 8.49 characterizes separable convex functions as exactly the M$^\natural_2$-and-L$^\natural_2$-convex functions. Theorem 8.53 (reduced to parts (1),(2),(4)) gives the general perturbation-independent duality identities: the dual objective is $g=-\varphi^{\bullet}(-\cdot)$, weak duality's biconjugate form $\sup(D)=\varphi^{\bullet\bullet}(0)$, and the equivalence of strong duality with biconjugate exactness. Proposition 8.55 shows the M-convex perturbation $F_r$ legitimately instantiates the general framework; Proposition 8.56 (reduced to part (1)) gives the closed form for the unregularized Lagrangian kernel $K_0$ via the conjugate of $B$'s indicator function; Theorems 8.57 and 8.58 establish the resulting convexity/concavity of the kernel, the dual objective, and the optimal-value function in each of their arguments. Propositions 8.62-8.63 and Theorems 8.64-8.65 build and analyze the mirror construction — the dual perturbation $G_r$, its optimal-value function $\gamma_r$, and the dual-of-dual reconstruction — showing that for bounded $B$ the process exactly recovers the primal problem and its own strong duality theorem.

Significance

This is chapter 8's payoff: a full nonlinear-integer-programming duality theory, built without any convexity assumption beyond M-/L-convexity, mirroring Rockafellar's classical conjugate duality approach line for line while replacing every continuous convexity argument with a discrete M-/L-convexity one. Theorem 8.59's proof is a two-line consequence of the machinery this mission assembles (Theorems 8.35, 8.53, 8.58), which is itself the point: the discrete theory's hard combinatorial work (Theorems 8.35, 8.36, 8.42 from prior missions) is what makes the strong duality theorem here nearly free, exactly as convex analysis makes classical Lagrangian duality nearly free once Fenchel duality is established. The bidirectional construction of Theorems 8.62-8.65 is the discrete analogue of the classical fact that Lagrangian duality is symmetric between primal and dual convex programs.

None of these results are open — they are Murota's own account of M2-/L2-conjugacy and Lagrangian duality (section 8.3.3 and section 8.4), continuing chapter 8's duality program to its conclusion. What this mission contributes is a faithful, machine-checked formal statement of each, completing the platform's coverage of chapter 8's duality theorems begun in missions 10-conjugacy-i and 11-conjugacy-ii-lagrange; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The EReal-valued ($\mathbb Z\cup\{\pm\infty\}$) typing is essential and new to this mission: unlike every prior mission in this series, the general framework's derived quantities ($\varphi$, $K$, $g$, and their mirror-construction analogues $G_r$, $\gamma_r$, $\tilde K_r$, $\tilde f$) are defined as infima/suprema over families that are not a priori bounded, so they can genuinely equal $-\infty$ or $+\infty$ — a value WithTop ℝ cannot represent and whose sInf instance would silently substitute a junk value (0) rather than correctly returning $-\infty$. The book's own repeated "$X$ is convex (resp. concave), or $X\equiv+\infty$, or $X\equiv-\infty$" disjunctive escape clauses (Theorems 8.57, 8.58, Propositions 8.63) are captured with two small generic combinators, IsEmbedOf/IsNegOf, rather than restating the embedding by hand at each of the roughly dozen occurrences.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; the base M-/L-/M2-/L2-convexity vocabulary is redeclared verbatim from missions 29-ch08b-conjugacyduality and 30-ch08c-conjugacyduality, since sibling drafts in this series cannot yet reference one another. Two results carry a documented partial-coverage scope reduction (see HARD.md): Theorem 8.53 is placed with only parts (1),(2),(4), the purely algebraic identities holding unconditionally for any perturbation $F$, omitting parts (3),(5),(6), which characterize $\operatorname{opt}(D)$ under the book's own biconjugacy hypothesis (8.55) — a hypothesis this mission's M-convex-specific Theorem 8.59 later establishes directly rather than invoking Theorem 8.53's general form; and Proposition 8.56 is placed with only part (1), the $K_0$ closed form, omitting part (2), the $K_r$ closed form via the infimal convolution $\delta_{-B}\square r[y]$, not independently needed elsewhere in this chunk. One numbered result nominally in this chunk's page range, Theorem 8.46, is not re-placed here: it was already found and placed as a milestone in mission 30-ch08c-conjugacyduality, whose own page range overlaps this chunk's by one page (PDF251/printed 233) — see HARD.md. Contributions completing any of the twelve sorrys are welcome; the goal and Theorem 8.57 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• R. T. Rockafellar, "Conjugate duality and optimization," CBMS-NSF Regional Conference Series in Applied Mathematics, SIAM, 1974 [177] (the classical conjugate-duality framework this mission's section 8.4 adapts to the discrete M-/L-convex setting).
• K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 [140] (the original source of M2-/L2-convexity, Theorems 8.35, 8.36, 8.45, 8.46, 8.48, and the Lagrange duality theory of section 8.4).

Motivation

Chapters 6 through 8 built M-convex and L-convex functions and their conjugacy theory as abstract combinatorial objects on the integer lattice. Chapter 9 grounds that theory in a setting every reader already knows: network flows. The chapter's throughline is that the classical minimum cost flow problem — flows bounded by simple arc capacities, with a single linear cost — is a shadow of a much richer submodular flow problem, in which the constraint on a flow's boundary is not "equal a fixed supply vector" but "lie in the base polyhedron of an arbitrary submodular set function." This mission formalizes the feasibility theory for both problems and its capstone: a max-flow min-cut theorem for submodular flows that specializes to the classical max-flow min-cut theorem exactly when the submodular function degenerates to a plain capacity function.

Setting

Let $G = (V, A)$ be a finite directed graph, with $\mathrm{tail}, \mathrm{head} : A \to V$ giving each arc's start and end vertex. The boundary of a flow $\xi : A \to \mathbb R$ is $\partial\xi(v) = \sum_{a : \mathrm{tail}(a) = v} \xi(a) - \sum_{a : \mathrm{head}(a) = v} \xi(a)$. For $X \subseteq V$, $\Delta^+X$ and $\Delta^-X$ are the arcs leaving and entering $X$. Given an upper capacity $\bar c : A \to \mathbb R \cup \{+\infty\}$ and lower capacity $\underline c : A \to \mathbb R \cup \{-\infty\}$, the cut capacity function is $\kappa(X) = \bar c(\Delta^+X) - \underline c(\Delta^-X)$. A submodular set function $\rho : 2^V \to \mathbb R \cup \{+\infty\}$ with $\rho(\emptyset) = \rho(V) = 0$ plays the same structural role as $\kappa$ but is arbitrary problem data rather than a derived quantity.

Formalization targets

Goal: Theorem 9.13 (max-flow min-cut for submodular flows)

For a feasible maximum submodular flow problem on a specified arc $a_0$: $\sup\{\xi(a_0) : \xi \text{ feasible}\} = \min\big(\bar c(a_0), \min_X\{\bar c(\Delta^-X) - \underline c(\Delta^+X \setminus \{a_0\}) + \rho(X) : a_0 \in \Delta^+X\}\big)$, a common value in $\mathbb R \cup \{+\infty\}$; if the data is integer valued and the value is finite, an integer-valued maximum flow exists.

Milestones: Proposition 9.2, Theorem 9.3, Theorem 9.10

Proposition 9.2: the cut capacity function $\kappa$ is always submodular — the fact that lets the classical minimum cost flow problem's feasibility be phrased in exactly the same base- polyhedron language as the general submodular flow problem. Theorem 9.3: a flow meeting the capacity constraint with boundary $x$ exists if and only if $x(X) \le \kappa(X)$ for all $X$ and $x(V) = 0$ — the classical case, and the direct predecessor of the goal's feasibility side. Theorem 9.10: the submodular flow problem is feasible if and only if $\bar c(\Delta^-X) - \underline c(\Delta^+X) + \rho(X) \ge 0$ for all $X$ — obtained from Theorem 9.3 via Edmonds's intersection theorem in the book's own proof, and the feasibility half of the goal's own maximum-flow variant.

Significance

The result itself. Theorem 9.13 is a genuine generalization of the max-flow min-cut theorem — one of the most-cited results in combinatorial optimization — to a submodularly constrained setting where the classical single-source-single-sink cut structure is replaced by an arbitrary vertex subset $X$ scored by a submodular function $\rho$ rather than merely counted. It specializes to the classical theorem when $\rho$ is the indicator of a fixed boundary value and the graph carries a single source/sink; the book's own derivation (dividing the target arc $a_0$ and reducing to Theorem 9.10's feasibility criterion) is exactly the kind of "one shared mechanism explains two theorems" result this whole book is organized around.

Formalizing it. A prior-art search (GET /theorems?q=max-flow min-cut) found two existing platform items for the classical theorem — LinearOptimization.max_flow_min_cut (Bertsimas & Tsitsiklis, single source/sink, plain capacities) and menger_directed_max_flow (Ford-Fulkerson, integer capacities) — both at a genuinely different, simpler generality (no lower capacity bounds, no submodular vertex-cut function, a fixed source/sink rather than an arbitrary marked arc). A further search (q=network flow) found a distinct mission formalizing Bertsimas & Tsitsiklis's uncapacitated network flow LP theory (basic feasible solutions, tree solutions, basis-matrix integrality) — a different technique (linear-algebraic, not cut-based) for a different problem (no capacities at all). Neither family is reused; this mission gives the first formal statement of submodular-flow feasibility and its max-flow min-cut theorem at the book's own generality.

Difficulty

The obvious shortcut — state only the value equality of Theorem 9.13 and drop the integrality clause — would misrepresent the theorem's own content: the equality of the extremal values follows from ordinary LP duality on the polyhedron $B(\kappa) \cap B(\rho)$ (arguably already within reach of chunk 04's Edmonds's intersection theorem machinery, as the book's own proof of the feasibility predecessor Theorem 9.10 uses exactly that), whereas the integer-flow existence half is the theorem's genuine combinatorial content, unique to the integer lattice. This chunk keeps both halves in every drafted theorem (Theorem 9.3, 9.10, and the goal) rather than only the polyhedral half.

A second, more structural difficulty governed this chunk's scope: BRIEF.md recommended Theorem 9.4 (the potential-optimality criterion) and its M-convex-cost specialization Theorem 9.14 as milestones, but both need a polyhedral convexity hypothesis on real-valued (or M-convex) functions over $\mathbb R^V$ that this series has never built — the identical scope boundary chunk 10 hit with Theorem 8.4. Rather than silently drop the polyhedral-convexity hypothesis (which would make the drafted statement unsound, since the theorem's hard direction genuinely needs it), this chunk selects only results — Proposition 9.2, Theorem 9.3, Theorem 9.10, Theorem 9.13 — that need no convexity apparatus of any kind, only the submodularity of $\kappa$/$\rho$ and elementary capacity-constraint feasibility.

Formalization scope

$V$ and $A$ are Fintypes with DecidableEq V (and DecidableEq A where a Finset.erase is needed); tail, head : A → V are plain functions, not a bundled graph structure. Every capacity- and cut-related quantity is WithTop ℝ-valued (ℝ ∪ {+∞}) throughout, with no EReal: a per-term check (documented in MODERATION_NOTES.md) confirms every subtraction this chunk needs is really an addition of two terms each individually in $\mathbb R \cup \{+\infty\}$, via a small new cast NegLowerToUpper : WithBot ℝ → WithTop ℝ. The base polyhedron $B(\rho)$ is stated by its defining inequalities rather than via a named polyhedral object (chunk 04's BasePolyhedron is ℤ^V-domain and does not fit chapter 9's real-vector- space setting). Not drafted: Theorem 9.4/9.14 (needs the real-domain polyhedral-convexity layer above), Theorem 9.6 (needs a real-domain polyhedral L-convexity notion for its dual-integrality half), Theorem 9.5/9.18/9.20/9.22 (negative-cycle criteria, an alternative non-potential certificate family, checked against platform prior art and found adjacent only), Propositions 9.23–9.25 (supporting technical facts), and Theorems 9.26–9.28 (the separate network- transformation technique of §9.6). A trivializing formalization would state Theorem 9.13's value equality with the integrality clause dropped, or would silently allow $\bar c$/$\underline c$ to range over all of EReal (permitting a nonsensical $\underline c(a) = +\infty$ upper- capacity-like lower bound); neither is done — both the integrality clause and the WithTop ℝ/WithBot ℝ type-level domain restriction are kept exactly as the book states them.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.

Motivation

Two strategic levers shape the balance of power between a manufacturer and the retailer that resells its product. The first is strategic inventory: a buyer that orders more than it sells today, and carries the surplus into the next period, weakens the supplier's leverage over tomorrow's wholesale price. Anand, Anupindi and Bassok (Management Science 2008) showed that in a two-period channel the buyer withholds inventory exactly when its unit holding cost is below $\alpha/4$. The second is supplier encroachment: a supplier that can sell directly to consumers competes with its own buyer. Arya, Mittendorf and Sappington (Marketing Science 2007) showed that the threat of encroachment can lower wholesale prices and benefit both parties.

Guan, Gurnani, Geng and Luo, Strategic Inventory and Supplier Encroachment (MSOM 2019), combine the two levers in one game. Their headline qualitative finding is Proposition 4.2. When the supplier's direct channel is costly, but not quite too costly to use, the buyer keeps withholding inventory at every finite holding cost. This contrasts with the $\alpha/4$ cutoff of Anand et al. This mission formalizes that proposition, together with the equilibrium characterizations of Appendix A on which it rests.

Setting

There is one supplier and one buyer, two periods, deterministic demand and complete information. In each period the market price is $p = \alpha - q$, where $q$ is the total quantity sold in that period and $\alpha > 0$ is the demand intercept. The buyer pays a per-unit holding cost $h \ge 0$ on inventory carried into period 2. The supplier pays a per-unit direct selling cost $s \ge 0$. All other costs and the salvage value are zero. The moves are:

1. The supplier quotes a wholesale price $w_1 \ge 0$.
2. The buyer orders $Q_1$ and sells $q_1$, with $0 \le q_1 \le Q_1$. It carries the inventory $I = Q_1 - q_1$ into period 2.
3. The supplier quotes $w_2 \ge 0$.
4. The buyer orders $Q_2 \ge 0$ and sells $q_2$, with $0 \le q_2 \le I + Q_2$.
5. Having observed everything, the supplier sells $q_s \ge 0$ directly. The period-2 price is $\alpha - q_2 - q_s$.

The total profits are

$$\Pi_b = (\alpha - q_1)q_1 - w_1 Q_1 - hI + (\alpha - q_2 - q_s)q_2 - w_2 Q_2, \qquad \Pi_s = w_1 Q_1 + w_2 Q_2 + (\alpha - q_2 - q_s - s)q_s .$$

A strategy profile assigns an action to every history at which a player moves. It is a subgame perfect equilibrium (SPE) if, at every feasible history, the mover's prescribed action is feasible and no feasible alternative, followed by the profile afterwards, raises the mover's total profit. The equilibrium path is the outcome the profile generates; the equilibrium inventory is $I$ on that path. Following the paper (§4), the goal theorem sets $\alpha = 1$.

Formalization targets

Goal: Proposition 4.2

With $\alpha = 1$,

$$\forall h > 0\ \ \exists \epsilon > 0\ \ \forall s \in \big(\tfrac56 - \epsilon, \tfrac56\big):\quad \text{an SPE exists, and every SPE has } I > 0 \text{ and } hI < \tfrac{11}{72}.$$

Here $\epsilon$ may depend on $h$, and the bound $11/72$ applies at the same $(h, s)$.

Milestones, in attack order

1. Stage-3 best response (§3.1.1): in every SPE, the supplier sells $q_s = (\alpha - q_2 - s)^+/2$ at every history.
2. Eq. (1) (§3.1.1): with no inventory, the buyer's period-2 quantity is the four-branch function $q_b(w)$ of the period-2 wholesale price $w$.
3. Proposition 4.1, existence half: an SPE exists for every $h \ge 0$ and $s \ge 0$.
4. Region 8 (Tables A.1 and A.4): for $h < h_{11}$ with $s_3 \le s < 5\alpha/6$, or for $h < \alpha/4$ with $5\alpha/6 \le s < \alpha$, every SPE has $I = 5(\alpha - 4h)/34$ and the path of Table A.4.
5. Region 7, second part (Tables A.1 and A.3): for $h_{11} < h < h_{10}$ and $s_3 \le s < 5\alpha/6$, every SPE has $I = I^* = (2\alpha - 3s + x)/2$ and the path of Table A.3.
6. Region 10, second part (Tables A.1 and A.4): for $h > h_7$ and $2\alpha/3 < s < 5\alpha/6$, every SPE has $I = 0$.

The thresholds $x$, $s_3$, $h_7$, $h_{10}$, $h_{11}$ are explicit algebraic functions of $s$, given in Appendix A.

Significance

Proposition 4.2 separates the combined model from the two models it merges. Without a direct channel, inventory disappears once $h \ge \alpha/4$. With a direct channel, a threat of encroachment that is only barely credible keeps inventory alive at every holding cost. The total holding cost nevertheless stays below a constant, because the inventory shrinks as $h$ grows. Milestone 6 shows the flip side: for a fixed $s < 5\alpha/6$, a large enough $h$ removes the inventory. This is why the window $\epsilon$ must depend on $h$.

The paper's proofs are in an online appendix that is not reproduced in the article. The article itself gives the equilibrium only as tables. A formal development would supply a checked backward-induction proof of those tables in the regions near $s = 5\alpha/6$. It would also give a machine-checked SPE framework for multi-stage pricing-and-quantity games in supply chains, which none of the following exists for: Stackelberg pricing, sequential quantity competition, or dual-channel encroachment. No part of this paper has been formalized before.

Difficulty

The equilibrium is found by backward induction through five stages. Each stage's value function is only piecewise smooth, because the supplier's direct-channel response $(\cdot)^+$ switches on and off. As a result the buyer's period-2 profit has kinks, the supplier's period-2 profit as a function of $I$ has several local maxima, and the period-1 problems must compare branches whose boundaries are the irrational thresholds of Appendix A. The obvious approach, solving the first-order conditions stage by stage, fails at the kinks. At some region boundaries it also misses that the supplier is indifferent between two first-period prices, which makes the equilibrium path change discontinuously. Proposition 4.2 then needs uniform control of $h_7$, $h_{10}$ and $h_{11}$ as $s \uparrow 5/6$, where the denominator $3s - 2 - x$ of $h_7$ tends to $0$.

Formalization scope

• Representation. Strategies are functions of the full history, not Markov rules in $I$. IsSPE imposes optimality at every feasible history, including off-path ones. All actions are real numbers; wholesale prices and quantities are nonnegative, with $q_1 \le Q_1$ and $q_2 \le I + Q_2$.
• Normalization. The goal instantiates $\alpha = 1$ as the paper does from §4 on. The milestones keep a general $\alpha > 0$.
• Uniqueness is not stated. Proposition 4.1's uniqueness claim is false for strategy profiles: after the off-path price $w_2 = 0$, every order $Q_2 \ge q_2 - I$ is optimal. The goal and the region milestones therefore quantify over every SPE and carry existence as a separate conjunct.
• Corrected hypotheses.
  • The printed $s_3 = (\sqrt{(37 - 3\sqrt{65})/34} + 4/6)\alpha \approx 1.28\alpha$ is replaced by $(\sqrt{37 - 3\sqrt{65}}/34 + 4/6)\alpha \approx 0.772\alpha$, which matches the paper's "≈0.77".
  • Eq. (1) excludes the corner $w = 0$, $s < \alpha/3$, where its second branch is wrong.
  • Region 8 drops its boundary $h = h_{11}$ and Region 7 drops $h = h_{10}$, because the equilibrium path switches there and need not be unique.
• Ruled-out trivialization. The inventory in the goal is the inventory on the path of an SPE of the game above. It is not the closed form $5(1 - 4h)/34$ or $I^*$ from the tables, and the regional characterization is not a hypothesis. Otherwise the goal would reduce to algebra about the thresholds.
• Infrastructure and contributions. The definitions Game, IsSPE and Thresholds are shared by every statement. Welcome contributions include:
  • lemmas on maximizing concave piecewise-quadratic functions on half-lines;
  • a reusable backward-induction lemma for finite-stage games with real action sets;
  • interval-arithmetic facts about $x$, $h_7$, $h_{10}$ and $h_{11}$ near $s = 5/6$;
  • proofs of the paper's other regions.

Selected references

• T. Guan, H. Gurnani, X. Geng, Y. Luo, Strategic Inventory and Supplier Encroachment, Manufacturing & Service Operations Management 21(3):536–555, 2019. https://doi.org/10.1287/msom.2018.0705
• K. Anand, R. Anupindi, Y. Bassok, Strategic Inventories in Vertical Contracts, Management Science 54(10):1792–1804, 2008. https://doi.org/10.1287/mnsc.1080.0894
• A. Arya, B. Mittendorf, D. Sappington, The Bright Side of Supplier Encroachment, Marketing Science 26(5):651–659, 2007. https://doi.org/10.1287/mksc.1070.0280

Motivation

The Russian option of Shepp and Shiryaev pays its holder, at an exercise time of their choosing, the running maximum of the stock price, discounted, with no fixed maturity. It is the standard example of a perpetual lookback option, and its value is a model problem of optimal stopping for a two-dimensional Markov process (the price and its running maximum). Perpetual contracts are simple to analyse but economically unrealistic: every real contract ends. Canadization (Carr, Randomization and the American put, Rev. Financial Stud. 11, 1998, https://doi.org/10.1093/rfs/11.3.597) replaces a fixed maturity by an independent exponential time $\eta(\lambda)$. The holder must exercise before $\eta(\lambda)$; if they have not, they are paid the claim evaluated at $\eta(\lambda)$. Because the exponential law is memoryless, the problem stays time-homogeneous and its value can be computed in closed form, while it approximates a contract of finite expected life $1/\lambda$.

Avram, Kyprianou and Pistorius (AKP04) solved both the perpetual and the Canadized Russian problem when the log-price is a spectrally negative Lévy process: a process with stationary independent increments whose only jumps are downward. This covers Brownian motion with drift, the Black–Scholes model, and jump-diffusions with downward jumps (crashes). Their answer is written with the scale functions $W^{(q)}$, $Z^{(q)}$ of the process. This mission is the third of three drawn from that paper, and formalizes the Canadized problem (§7, Theorem 3).

Timeline. Shepp and Shiryaev (1993) solved the Russian option for geometric Brownian motion. Carr (1998) introduced Canadization for the American put. Kyprianou and Pistorius (Ann. Appl. Probab. 13, 2003) studied perpetual options through fluctuation theory; §7 of [AKP04] builds on their calculations. Avram, Kyprianou and Pistorius (2004) solved the perpetual and Canadized problems for general spectrally negative Lévy processes.

Setting

Let $(\Omega,\mathcal F,\mathbf F=\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a filtered probability space with $\mathbf F$ right-continuous, and let $X=\{X_t\}_{t\ge0}$ be a spectrally negative Lévy process adapted to $\mathbf F$: $X_0=0$, paths càdlàg with no upward jumps and not monotone, increments $X_{s+t}-X_s$ stationary and independent of $\mathcal F_s$. The standing assumption is that $X$ has unbounded variation, or bounded variation and a Lévy measure $\Lambda(dx)\ll dx$.

The Laplace exponent is $\psi(\theta)=\log\mathbb E[e^{\theta X_1}]$. Fix $r\ge0$ with $\psi(1)=r$, and let $\mathbb P^1$ be the Esscher measure, $d\mathbb P^1/d\mathbb P|_{\mathcal F_t}=e^{X_t-rt}$.

For $q\ge0$ the $q$-scale function $W^{(q)}:\mathbb R\to[0,\infty)$ vanishes on $(-\infty,0]$, is continuous on $(0,\infty)$, and satisfies $\int_0^\infty e^{-\theta x}W^{(q)}(x)\,dx=(\psi(\theta)-q)^{-1}$ for $\theta>\Phi(q)$, where $\Phi(q)$ is the largest root of $\psi(\theta)=q$. Further, $Z^{(q)}(x)=1+q\int_{-\infty}^xW^{(q)}(y)\,dy$. All scale functions in this mission are those of $(X,\mathbb P)$.

Starting from $Y_0=z\ge0$ (the paper's $\mathbb P^1_{-z}$), the reflected process is $Y_t=\overline X_t-X_t$, where $\overline X_t=\max\{0,\sup_{u\le t}(-z+X_u)\}$ and the position is $-z+X_t$. Its passage time above $k$ is $\tau_k=\inf\{t\ge0:Y_t\notin[0,k)\}$.

Let $\alpha>0$, and let $\eta(\lambda)$ be an exponential random variable of rate $\lambda>0$ which under $\mathbb P^1$ is independent of $\mathcal F_\infty$. The Canadized Russian problem (32) is

$$w^{CR}(z)=\sup_\tau\ \mathbb E^1_{-z}\Big[e^{-\alpha(\tau\wedge\eta(\lambda))+Y_{\tau\wedge\eta(\lambda)}}\Big],$$

over all $\mathbb P^1$-a.s. finite $\mathbf F$-stopping times $\tau$. Write $p=\alpha+\lambda+r$.

Formalization targets

Goal: Theorem 3

With

$$\kappa_*=\inf\{x\ge0:\ Z^{(p)}(x)-pW^{(p)}(x)\le-\lambda/(p-\lambda)\},\qquad h(z)=\frac{(p-\lambda)e^zZ^{(p)}(\kappa_*-z)}{p}+\frac{\lambda e^z}{p},$$

for every $z\ge0$:

$$w^{CR}(z)=h(z),$$

and $\tau_{\kappa_*}$ is a $\mathbb P^1$-a.s. finite $\mathbf F$-stopping time attaining the supremum. The statement covers every variation regime at once.

Milestones

In attack order:

1. Lemma 2 (i), which gives the monotonicity behind $\kappa_*$.
2. Corollary 1 (29), the value of stopping at $\tau_k$ at discount rate $\alpha+\lambda$.
3. The elimination of $\eta(\lambda)$ (display after (32)):

$$\mathbb E^1_{-z}\big[e^{-\alpha(\tau\wedge\eta)+Y_{\tau\wedge\eta}}\big]=\mathbb E^1_{-z}\Big[e^{-(\alpha+\lambda)\tau+Y_\tau}+\lambda\int_0^\tau e^{-(\alpha+\lambda)t+Y_t}dt\Big].$$

4. The Itô identity (34).
5. The expected $d\overline X$-integral up to $\tau_k$.
6. Lemma 3 (33), the value of $\tau_k\wedge\eta(\lambda)$.
7. Lemma 4, with two misprints corrected.
8. The supermartingale property of $U_t=e^{-(\alpha+\lambda)t}h(Y_t)+\lambda\int_0^te^{-(\alpha+\lambda)u+Y_u}du$.
9. The identity $h(z)=e^z+(p-\lambda)e^z\int_0^{\kappa_*-z}W^{(p)}\ge e^z$.

Significance

The result. Theorem 3 gives the price and the optimal exercise rule of a Russian option with random (exponential) maturity, for every spectrally negative Lévy model at once. It makes three things explicit. The optimal rule is a threshold rule for the reflected process $Y$. The threshold $\kappa_*$ is the crossing point of one explicit function of the scale functions. Whenever $W^{(p)}(0+)\ge(p-\lambda)^{-1}$ (possible only with bounded variation), immediate exercise is optimal. Because scale functions are known in closed form for many models, including Brownian motion with drift and hyper-exponential jump-diffusions (§8 of the paper), the theorem produces explicit prices.

Formalizing it. The result is proved on paper. It is not formalized in any proof assistant, and none of its infrastructure is available in Lean. This mission produces:

• a path-level definition of spectrally negative Lévy processes;
• scale functions defined as definite descriptions;
• the reflected process and its passage times;
• the Esscher change of measure as data;
• a continuous-time optimal stopping problem with an independent random horizon, valued in $[0,\infty]$.

A machine-checked proof would also check the verification argument, which the paper states in detail only for the unbounded-variation case.

Difficulty

The obvious route is to compute the value of every threshold rule (Lemma 3) and optimize over $k$. That identifies the right candidate, but it does not show that no other stopping time does better. The verification step needs two things for all regimes of $W^{(p)}(0+)$: that $U$ is a supermartingale, and that $U$ stopped at $\tau_{\kappa_*}$ is a martingale. For processes of bounded variation, $h$ is only continuous, not $C^1$, at $\kappa_*$, so a smooth Itô formula does not apply directly. Computing the expected $d\overline X$-integral up to $\tau_k$ uses excursion theory of $Y$ away from $0$, which Mathlib does not have. Eliminating $\eta(\lambda)$ is easy only if $\eta$ is independent of the whole filtration. If it is independent of $X$ alone, a stopping time could depend on $\eta$.

Formalization scope

• Conventions. Time is $[0,\infty)$ (ℝ≥0) and values are real. Random times take values in WithTop ℝ≥0, and the payoff is $0$ on $\{\tau=\infty\}$. Expectations of nonnegative payoffs are lower Lebesgue integrals in $[0,\infty]$, and $w^{CR}$ is an extended-real supremum, so no expectation defaults to $0$. Equalities with a real right-hand side also assert finiteness.
• Readings of informal words.
  • "The usual conditions" means right-continuity of $\mathbf F$, without completeness. Completing $\mathcal F_0$ with $\mathbb P$-null sets would contradict the Esscher relation, since $\mathbb P^1$ and $\mathbb P$ are typically singular on $\mathcal F_\infty$.
  • "Unbounded variation" means "not almost surely of bounded variation on compacts". (AC) is stated through jumps.
  • "ψ(v) < ∞" means integrability of $e^{vX_1}$.
  • "Decreases monotonically" means strictly decreasing, and "the unique root" means unique on $[0,\infty)$.
  • $W^{(p)}(0+)$ is the right limit.
  • "Almost surely finite" and the law and independence of $\eta(\lambda)$ are all under $\mathbb P^1$, where independence is from $\mathcal F_\infty$. "Parameter $\lambda$" is the rate.
  • $\mathbb P^1_{s,x}$ is encoded pathwise through the reflected process with $Y_0=s-x$.
  • The elimination of $\eta$ is stated τ by τ, which implies the page's equality of suprema.
  • The supermartingale claim, derived on the page in the unbounded-variation case, is stated for all cases.
  • Corollary 1's discount rate is renamed $a$.
  • (34) is stated as $pA+B=e^{s-x}+C$ with $A$, $B$, $C$ finite.
• Definition choices. Scale functions are defined by choice from their defining property, never as hypotheses on an arbitrary function. $W^{(q)}$ for $q<0$ is the series (5), not the tilting formula of Remark 4. $\mathbb P^1$ is a measure given with the Esscher relation. $d\overline X_t$ is the Lebesgue–Stieltjes measure of the running-maximum path.
• Corrected misprints. Lemma 4 is printed with $p^{-1}$ and $-\lambda/p$. The definition of $\kappa_*$ (p. 233) and the proof of Theorem 3 (p. 235) require $(p-\lambda)^{-1}$ and $-\lambda/(p-\lambda)$, and the printed version is false when $p^{-1}\le W^{(p)}(0+)<(p-\lambda)^{-1}$. The corrected statement is formalized.
• Ruled out. A supremum over stopping times of a filtration containing $\sigma(\eta)$, or a real-valued supremum or Bochner expectation that could be $0$ by default, would trivialize the goal or change it. The admissible class is every $\mathbb P^1$-a.s. finite stopping time of the given filtration, of which $\eta$ is independent. Replacing the goal by the $\eta$-free rewriting would state milestone 3 as if it were Theorem 3.
• Needed and reusable. A complete development needs Lévy process theory, scale functions, fluctuation identities for the reflected process, optional stopping in continuous time, and Itô or change-of-variable formulas for semimartingales with jumps. The Lévy-process, scale-function and reflected-process definitions are shared with the other two missions of the series and are reusable in ruin theory and queueing. Proofs of any milestone, and sorry-free facts about the definitions, are welcome.

Selected references

• F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14(1), 215–238, 2004. https://doi.org/10.1214/aoap/1075828052
• P. Carr, Randomization and the American put, Rev. Financial Stud. 11(3), 597–626, 1998. https://doi.org/10.1093/rfs/11.3.597
• L. A. Shepp, A. N. Shiryaev, The Russian option: reduced regret, Ann. Appl. Probab. 3, 603–631, 1993. https://doi.org/10.1214/aoap/1177005715
• A. E. Kyprianou, M. R. Pistorius, Perpetual options through fluctuation theory, Ann. Appl. Probab. 13, 1077–1098, 2003. https://doi.org/10.1214/aoap/1060202835
• J. Bertoin, Lévy Processes, Cambridge University Press, 1996.

Motivation

Models of learning in games, and discrete choice models in econometrics, describe an agent who does not always pick the best alternative. Two descriptions of such an agent are standard. In the additive random utility model (McFadden 1981; Anderson, de Palma and Thisse 1992) the agent maximizes payoffs perturbed by random shocks. In the deterministic perturbation model (Fudenberg and Levine 1998) the agent chooses a probability vector and pays a deterministic, strictly convex cost for it. The logit choice rule arises from both: from i.i.d. extreme-value shocks, and from the entropy cost $V(y) = \eta \sum_j y_j \ln y_j$.

Hofbauer and Sandholm (Econometrica 70 (2002)) show that the second description is general enough to cover the first for every shock distribution with a strictly positive density, not only for logit. Their analysis of stochastic fictitious play rests on this: the deterministic representation provides the perturbed payoff functions from which Lyapunov functions for the learning dynamics are built, for arbitrary noise. This mission formalizes that discrete choice theorem, Theorem 2.1 of the paper, together with the steps of its proof.

Setting

Fix $n \ge 1$ alternatives $A = \{1, \dots, n\}$ with base payoffs $\pi = (\pi_1, \dots, \pi_n) \in \mathbb{R}^n$. A random vector $\varepsilon = (\varepsilon_1, \dots, \varepsilon_n)$ has a strictly positive density $f : \mathbb{R}^n \to \mathbb{R}$, whose law does not depend on $\pi$. The agent chooses the alternative whose total payoff $\pi_j + \varepsilon_j$ is largest, which gives the choice probability function $C : \mathbb{R}^n \to \mathbb{R}^n$,

$$C_i(\pi) = P\big(\operatorname{argmax}_j\, \pi_j + \varepsilon_j = i\big).$$

The probability simplex is $\Delta A = \{x \in \mathbb{R}^n_+ : \sum_j x_j = 1\}$, with relative interior $\operatorname{int}(\Delta A)$ (all coordinates positive) and tangent space $\mathbb{R}^n_0 = \{z \in \mathbb{R}^n : \sum_j z_j = 0\}$.

A deterministic perturbation is a function $V : \operatorname{int}(\Delta A) \to \mathbb{R}$. Because $V$ lives on the relative interior, its gradient $\nabla V(y)$ is the vector of $\mathbb{R}^n_0$ with $V(y + hz) = V(y) + (\nabla V(y) \cdot z) h + o(h)$ for all $z \in \mathbb{R}^n_0$, and its second derivative $D^2 V(y)$ is a quadratic form on $\mathbb{R}^n_0$. The perturbation is admissible if $V$ is twice continuously differentiable along the simplex, $D^2V(y)$ is positive definite on $\mathbb{R}^n_0$ for every $y$, and $\|\nabla V(y)\| \to \infty$ as $y$ approaches the boundary of $\Delta A$.

Formalization targets

Goal: Theorem 2.1

If $\varepsilon$ has a strictly positive density and $C$ is continuously differentiable, then there is an admissible $V$ such that, for every $\pi \in \mathbb{R}^n$,

$$C(\pi) = \operatorname*{argmax}_{y \in \operatorname{int}(\Delta A)} \big( y \cdot \pi - V(y) \big),$$

with a unique maximizer. The perturbation $V$ is one function serving all payoff vectors at once.

Milestones

The milestones are the steps of the paper's proof (pp. 5–7), in order:

1. Eq. (4). $DC(\pi)$ is symmetric, $\partial C_i/\partial \pi_j = \partial C_j / \partial \pi_i$, and its off-diagonal terms are strictly negative.
2. Eq. (5). $\partial C_i/\partial \pi_i = -\sum_{j \ne i} \partial C_j/\partial \pi_i$, and $DC(\pi)\mathbf{1} = 0$.
3. Eq. (6). $z \cdot DC(\pi) z > 0$ whenever $z$ is not proportional to $\mathbf{1}$.
4. Shift invariance and injectivity. $C(\pi + c\mathbf{1}) = C(\pi)$, and $C$ is one-to-one on $\mathbb{R}^n_0$.
5. Range observation. If the payoffs $\pi_j$, $j \in J$, stay bounded while the others tend to $+\infty$, then $C_j(\pi) \to 0$ for $j \in J$.
6. Convex potential. There is $W : \mathbb{R}^n \to \mathbb{R}$ with $\nabla W \equiv C$, strictly convex on $\mathbb{R}^n_0$.
7. Range. $C$ takes values in $\operatorname{int}(\Delta A)$, and $C(\mathbb{R}^n_0) = \operatorname{int}(\Delta A)$.

Significance

The result. Theorem 2.1 lets any smooth additive random utility model be replaced by an optimizing agent with a strictly convex, boundary-repelling cost. In the paper this is the bridge from the perturbed best response dynamic to a deterministic perturbed-payoff formulation, which yields Lyapunov functions for zero-sum games, games with an interior evolutionarily stable strategy, and potential games (§4 of the paper), and so the almost sure convergence of stochastic fictitious play under general noise (Theorem 6.1). Without it those convergence results would be restricted to noise distributions whose choice rule has a known deterministic representation, essentially logit. The paper also shows (Proposition 2.2) that the converse fails when $n \ge 4$: deterministic perturbations generate strictly more choice rules than random utility.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it is known. The mission asks for a formal proof of Theorem 2.1 and the seven steps above. Along the way it requires symmetric Jacobians of probability integrals, a gradient-field potential on $\mathbb{R}^n$, and the Legendre transform of a strictly convex function restricted to a hyperplane. None of these is currently packaged in Mathlib in the needed form.

Difficulty

The obvious argument is to take $V$ to be the Legendre transform of the potential $W(\pi) = \mathbb{E}\max_j(\pi_j + \varepsilon_j)$ and read off the first-order conditions. Three steps of that argument are not routine. First, the derivative identity (4) is a change of variables inside an $(n-1)$-fold integral over a moving region, and its strict sign needs the density to be positive on the relevant hyperplane sections. Second, the Legendre transform is well defined on all of $\operatorname{int}(\Delta A)$ only if $C$ maps $\mathbb{R}^n_0$ onto the whole open simplex. The paper takes this from Theorem 26.5 of Rockafellar (1970), whose hypotheses (essential smoothness, strict convexity, identification of the conjugate's domain) must be checked here. Third, positive definiteness of $D^2V$ and the gradient blow-up at the boundary are statements about the inverse of $C$ on $\mathbb{R}^n_0$. They need an inverse function argument on a subspace and a properness argument, not only pointwise convexity.

Verifying that $C(\pi)$ satisfies the first-order condition for one fixed $\pi$ does not suffice: the goal requires a single $V$ for all $\pi$, and a unique maximizer.

Formalization scope

Alternatives are indexed by Fin n with $n \ge 1$; vectors are Fin n → ℝ with its sup norm. The density is a real function $f$ that is continuous, strictly positive at every point, and has $\int f = 1$; the law of $\varepsilon$ is Lebesgue measure weighted by $f$. The paper's formula (4) evaluates $f$ on hyperplanes, which is meaningful for a continuous $f$. Without continuity the theorem can fail: a density that is positive everywhere but tends to zero near a hyperplane can make $C$ continuously differentiable with a vanishing off-diagonal derivative, and then no twice differentiable $V$ represents $C$. Continuous differentiability of $C$ is a hypothesis, as in the paper, stated as ContDiff ℝ 1 of the map $\pi \mapsto C(\pi)$. The event "$i$ is the argmax" uses strict inequalities; ties have probability zero.

$V$ is a function on $\mathbb{R}^n$ of which only the values on $\operatorname{int}(\Delta A)$ enter. Its smoothness and second derivative are taken in the chart $z \mapsto V(y + z)$ on the subspace $\mathbb{R}^n_0$. $\nabla V(y)$ is the tangent gradient of the paper's footnote 3, not an ambient gradient of an extension. The boundary blow-up is stated uniformly: for every $M$ there is $\delta > 0$ such that every tangent gradient at an interior point with some coordinate below $\delta$ has norm above $M$.

The goal cannot be satisfied trivially. $V$ must be chosen before $\pi$, all three admissibility conditions are part of the definition, and the maximizer must be unique. Weakening any of these (a $V$ depending on $\pi$, a $V$ without second derivatives, a non-strict maximum) changes the theorem.

Reusable infrastructure: differentiation of choice probabilities under a density, potentials of symmetric $C^1$ vector fields on $\mathbb{R}^n$, and Legendre duality for strictly convex functions on a subspace. Contributions of any of these as separate lemmas are welcome, as are alternative proofs of the milestones, for instance obtaining the potential directly as $\mathbb{E}\max_j(\pi_j + \varepsilon_j)$.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2265–2294, 2002. https://doi.org/10.1111/1468-0262.00376 (theorem numbers and pages here follow the authors' manuscript of February 21, 2002).
• D. Fudenberg and D. K. Levine, The Theory of Learning in Games, MIT Press, 1998.
• S. P. Anderson, A. de Palma and J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992.
• D. McFadden, Econometric Models of Probabilistic Choice, in C. F. Manski and D. McFadden (eds.), Structural Analysis of Discrete Data with Econometric Applications, MIT Press, 1981.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

One-dimensional bin packing asks for the fewest unit-capacity bins that hold a given list of items with sizes in $(0,1)$. It is the model behind cutting stock (cutting rolls of paper or steel to ordered widths), memory and file allocation, and batch scheduling on identical machines, and it is NP-hard. Its algorithmic study is therefore about approximation: how close to the optimum a polynomial-time algorithm can guarantee to come.

• 1961–1963: Gilmore and Gomory introduce the configuration linear program for cutting stock and solve it by column generation (Gilmore–Gomory 1961).
• 1974: Johnson, Demers, Ullman, Garey and Graham analyse First Fit and related heuristics, with asymptotic ratio $17/10$ and $11/9$ (Johnson et al. 1974).
• 1981: Fernandez de la Vega and Lueker give the first asymptotic approximation scheme, packing within $(1+\varepsilon)\,OPT(I) + 1$ bins in time linear in $n$ for fixed $\varepsilon$, using elimination of small pieces and linear grouping (Fernandez de la Vega–Lueker 1981).
• 1982: Karmarkar and Karp replace the enumeration of configurations by an approximate solution of the configuration LP and a rounding step, obtaining an additive term polynomial in $1/\varepsilon$ (this mission), and, with geometric grouping, $OPT(I) + O(\log^2 OPT(I))$ (Karmarkar–Karp 1982).
• 2013–2017: Rothvoß and then Hoberg–Rothvoß improve the additive term to $O(\log OPT \cdot \log\log OPT)$ and $O(\log OPT)$ (Hoberg–Rothvoß 2017).

Setting

An instance $I$ is a finite multiset of piece sizes, each in the open interval $(0,1)$. Write $n(I)$ for the number of pieces, $m(I)$ for the number of distinct sizes, and $SIZE(I)$ for the sum of all sizes. A packing of $I$ is a finite multiset of bins, each a multiset of sizes, whose union is exactly $I$ and in which every bin has total size at most $1$. Its cost is the number of bins, and $OPT(I)$ is the minimum cost.

A configuration of $I$ is a nonempty multiset of sizes occurring in $I$ with total at most $1$. With $b_t$ the number of pieces of size $t$ and $a_{tc}$ the number of occurrences of $t$ in configuration $c$, the fractional bin-packing problem is the linear program

$$\min\ \mathbf 1\cdot x\quad\text{s.t.}\quad x\ge 0,\qquad \sum_c a_{tc}x_c \ge b_t\ \ \text{for every size } t,$$

whose optimal value is $LIN(I)$. A basic feasible solution is an extreme point of its feasible region.

For instances $I,J$, write $I\le J$ if there is a one-to-one map $f$ from the pieces of $I$ into the pieces of $J$ with $x\le f(x)$. Linear grouping with parameter $k$ sorts $I$ non-increasingly, cuts it into groups $G_1,\dots,G_q$ of $k$ consecutive pieces (the last possibly shorter), rounds every piece of $G_i$ up to the largest size of $G_i$ to get $G_i'$, and outputs $J = \bigcup_{i\ge 2} G_i'$ and $J' = G_1$.

ALGORITHM 1 takes $I$ and $\varepsilon>0$: (1) discard the pieces of size $\le \max(1/n(I), \varepsilon/2)$, leaving $J$; (2) apply linear grouping to $J$ with $k = \lceil n(J)\varepsilon^2\rceil$, giving $K$ and $K'$; (3) put each piece of $K'$ in its own bin; (4) obtain from a Fractional Bin-Packing subroutine a basic feasible solution $x$ of the LP of $K$ with $\mathbf 1\cdot x\le LIN(K)+1$; (5) round $x$ to a packing of $K$ with at most $\mathbf 1\cdot x + (m(K)+1)/2$ bins; (6) shrink the pieces back to obtain a packing of $J$; (7) insert the discarded pieces, opening a new bin only when a piece fits nowhere. $A(I)$ is the cost of the resulting packing.

Formalization targets

Goal: Theorem 3, as its proof establishes it

$$A(I) \le (1+2\varepsilon)\,OPT(I) + \frac{1}{2\varepsilon^2} + 3 \qquad\text{for every } \varepsilon>0,\ \text{every instance } I,\ \text{every run of ALGORITHM 1.}$$

The additive term depends on $\varepsilon$ only, so ALGORITHM 1 is an asymptotic approximation scheme. The paper prints the factor $1+\varepsilon$, which fails for ALGORITHM 1 as printed (see Formalization scope); running the algorithm with $\varepsilon/2$ gives the paper's main result (4), $A(I)\le(1+\varepsilon)OPT(I)+O(\varepsilon^{-2})$, stated as a separate corollary with the explicit term $2/\varepsilon^2+3$.

Milestones

1. Lemma 1: $OPT(I)\le 2\,SIZE(I)+1$.
2. Lemma 2: $SIZE(I)\le LIN(I)\le OPT(I)\le LIN(I)+\frac{m(I)+1}{2}$.
3. Corollary 1: every basic feasible solution $x$ can be rounded to a packing of cost $\le \mathbf 1\cdot x + \frac{m(I)+1}{2}$.
4. Lemma 3: inserting pieces of size $\le g/2$ last, with new bins only when necessary, costs at most $\max(A, (1+g)\,OPT(I)+1)$.
5. Monotonicity: $I\le J$ implies $OPT$, $LIN$ and $SIZE$ do not decrease.
6. Lemma 4: linear grouping loses at most $k$ in $OPT$, $LIN$ and $SIZE$.
7. Proof steps (ii)–(iii) (corrected): $k\le 2\varepsilon\,OPT(I)+1$.
8. Proof step (iv): $m(K)\le 1/\varepsilon^2$.
9. Proof step (vii): $\mathbf 1\cdot x\le OPT(I)+1$.
10. Proof step (viii) (corrected): the packing of Step 6 has at most $(1+2\varepsilon)OPT(I)+\frac{1}{2\varepsilon^2}+\frac52$ bins.

Significance

The result showed that the configuration LP, of exponential size in general, can be used for a guaranteed approximation: its value is within $(m+1)/2$ of the integer optimum, and grouping reduces $m$ at small cost. The same template (eliminate small items, group, solve the configuration LP, round a basic solution, reinsert) underlies later schemes for bin packing, cutting stock, bin packing with cardinality constraints and scheduling, and the LP-based analysis is the starting point of the Rothvoß and Hoberg–Rothvoß improvements.

The theorems are proved in the literature; none of them has a machine-checked proof on the platform or, to our knowledge, in Mathlib. This mission produces a checked analysis of the algorithm, including a correction: the printed approximation factor is not valid for the algorithm as printed, and the checked statement records the factor its proof yields. The definitions (instances, packings, the configuration LP, basic solutions, the order $I\le J$, any-fit insertion) are reusable for the second mission of the series and for other bin-packing results.

Difficulty

The Lean statements are short, but several proofs need linear-programming structure that is not in Mathlib in this form. Lemma 2 and Corollary 1 use that an extreme point of $\{x\ge0,\ Ax\ge b\}$ has at most as many nonzero coordinates as there are rows of $A$; the configuration LP is indexed by a finite but implicitly described set of multisets. Monotonicity of $LIN$ under $I\le J$ ("clearly" in the paper) requires transporting a fractional solution across a piece-to-piece matching whose images are types, not pieces. The existence of a run requires an optimal basic feasible solution of the configuration LP. Lemma 3 concerns an insertion process with unrestricted order and bin choice, so its bound has to hold for every execution, not for one greedy rule.

Formalization scope

• Sizes are real numbers in the open interval $(0,1)$; the paper says "a rational number between 0 and 1". Real sizes generalize rational ones; the open interval is what the paper's arguments use.
• Instances are Multiset ℝ; packings are Multiset (Multiset ℝ) with join equal to the instance, bin loads at most $1$, empty bins allowed and counted. $OPT$ is a natural-number infimum over a set that is always nonempty.
• LP solutions are Multiset ℝ →₀ ℝ supported on configurations. $LIN$ is a real infimum over a set that is nonempty (singleton configurations) and bounded below by $0$. "Basic" is the extreme-point property; the bound on the number of nonzero coordinates is a consequence, not the definition.
• The Fractional Bin-Packing subroutine is modelled by its contract only (§5, p. 315): any basic feasible solution of cost at most $LIN(K)+1$. The ellipsoid method of §6 is not modelled.
• ALGORITHM 1 is a relation Alg1Run ε I P: $P$ is a possible output. Every open choice is quantified: the subroutine's output, the packing of Step 5 (any packing within the stated bound), the size reduction of Step 6 (bin by bin), and the insertion of Step 7 (any order, any fitting bin). The goal holds for every run, and a separate item states that a run exists, so the goal is not vacuous.
• The paper's $O(\cdot)$ in result (4) is replaced by the explicit $2/\varepsilon^2+3$.
• Corrected statements. The printed Theorem 3 bound $(1+\varepsilon)OPT(I)+\frac{1}{2\varepsilon^2}+3$ fails: for $\varepsilon=1/10$ and $19\,000$ pieces of size $0.051$, some run uses $1180$ bins while the bound is $1153$. The failing step is (ii), $SIZE(J)\ge\varepsilon\,n(J)$, since Step 1 discards only pieces $\le\varepsilon/2$. Steps (ii)–(iii) and (viii) are stated with $2\varepsilon$; step (iv) is stated as $m(K)\le 1/\varepsilon^2$ because its first link $m(K)\le n(K)/k$ fails when the last group is short.
• Running time (Theorem 3's first half, Corollary 1's time bound, the function $T$) is out of scope.
• Trivializations are ruled out: "some packing has at most the bound" is not the goal; the goal constrains every output of the algorithm, and the packing property of that output is part of its conclusion.

Proofs of any item are welcome; Lemma 2, Corollary 1 and the monotonicity display are the most reusable.

Selected references

• N. Karmarkar, R. M. Karp, An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem, Proc. 23rd FOCS (SFCS 1982), IEEE, pp. 312–320. https://doi.org/10.1109/sfcs.1982.61
• W. Fernandez de la Vega, G. S. Lueker, Bin packing can be solved within 1+ε in linear time, Combinatorica 1 (1981) 349–355. https://doi.org/10.1007/BF02579456
• P. C. Gilmore, R. E. Gomory, A Linear Programming Approach to the Cutting-Stock Problem, Operations Research 9 (1961) 849–859. https://doi.org/10.1287/opre.9.6.849
• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM J. Comput. 3 (1974) 299–325. https://doi.org/10.1137/0203025
• R. Hoberg, T. Rothvoß, A Logarithmic Additive Integrality Gap for Bin Packing, Proc. SODA 2017, 2616–2625. https://doi.org/10.1137/1.9781611974782.172