The OR Formalization Drive

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

Motivation

Caching (online paging) is one of the oldest problems in online algorithms: a fast memory of $k$ slots serves a sequence of requests, and every request for an element not in the fast memory is a cache miss that forces the element to be loaded, possibly evicting another one. With the whole request sequence known in advance, evicting the element whose next request is furthest in the future is optimal (Bélády, 1966). Without that knowledge, no deterministic algorithm is better than $k$-competitive, and the best randomized algorithms are $\Theta(\log k)$-competitive (Fiat, Karp, Luby, McGeoch, Sleator and Young, 1991).

Lykouris and Vassilvitskii asked what happens in between: an online algorithm receives, with every request, a machine-learned prediction of the element's next arrival time. A good predictor should make the algorithm nearly as good as Bélády's rule (consistency), and a bad predictor should never make it worse than a classical algorithm (robustness). Their paper (arXiv:1802.05399v4; J. ACM 2021) is one of the founding papers of learning-augmented algorithms, and its algorithm, Predictive Marker, is the reference point for the later literature on caching with predictions.

Timeline.

• 1966: Bélády's furthest-in-future rule is optimal offline.
• 1985: Sleator and Tarjan show that deterministic online paging is at best $k$-competitive.
• 1991: Fiat et al. introduce the Marker algorithm, $2H_k$-competitive, and the clean-element lower bound on the optimum.
• 2018: Lykouris and Vassilvitskii (arXiv:1802.05399) introduce Predictive Marker, with ratio $2\min(1+2S_\ell(\epsilon), 2H_k)$ for an $\epsilon$-accurate predictor.
• 2020: Rohatgi (arXiv:1910.12172, SODA 2020) and Wei (arXiv:2005.13716, APPROX/RANDOM 2020) improve the dependence on the error.

Setting

A request sequence $\sigma = (z_1, \dots, z_n)$ lists elements of a set $Z$. A cache of size $k \ge 1$ starts empty. A request for a cached element is a hit; otherwise it is a miss, the element is loaded, and if the cache is full some element is evicted first. The offline optimum $\mathrm{Opt}(\sigma)$ is the least number of misses over all eviction schedules chosen with knowledge of $\sigma$.

With each request $z_i$ the algorithm receives a real prediction $h_i$. The true label $y_i$ is the position of the next request of $z_i$, or $n+1$ if there is none. For a loss function $\ell \ge 0$, the error of the predictions is $\eta_\ell(h,\sigma) = \sum_i \ell(y_i, h_i)$, and the predictions are $\epsilon$-accurate when $\eta_\ell(h,\sigma) \le \epsilon \cdot \mathrm{Opt}(\sigma)$.

The spread of $\ell$ measures how cheaply a predictor can get the order of arrivals completely wrong: $S_\ell(m)$ is the least length $T \ge 1$ such that every strictly increasing integer sequence $a_1 < \dots < a_T$ and every non-increasing real sequence $b_1 \ge \dots \ge b_T$ have total loss $\sum_i \ell(a_i, b_i) \ge m$.

Predictive Marker (Algorithm 1) works in the phases of the Marker algorithm. Requested elements are marked. A phase ends when the cache is full, every cached element is marked, and a miss occurs; then all marks are removed. An element requested in a phase but not in the previous one is clean, and $Q(\sigma)$ is the total number of clean elements. Each clean miss starts a chain. An element evicted in the current phase that is requested again (a stale miss) extends the chain in which it was evicted. Evictions are among unmarked elements. As long as the chain's length $n(r,c)$ is at most $H_k = 1 + \tfrac12 + \dots + \tfrac1k$, the evicted element is one with the largest prediction. After that it is chosen uniformly at random. The expected number of misses of Predictive Marker is $\mathrm{cost}_{PM}(\sigma)$.

Formalization targets

Goal: Theorem 3.3

If $S$ is concave on $[0,\infty)$ and majorizes the spread, then for every $\epsilon \ge 0$, every tie-breaking rule, and every sequence with $\epsilon$-accurate predictions,

$$\mathbb E\bigl[\mathrm{cost}_{PM}(\sigma)\bigr] \le 2\cdot\min\bigl(1 + 2S(\epsilon),\ 2H_k\bigr)\cdot \mathrm{Opt}(\sigma).$$

Milestones

• Claim 1 (Fiat et al.): $Q(\sigma) \le 2\,\mathrm{Opt}(\sigma)$.
• Proof of Theorem 3.3, last sentence: $\mathrm{Opt}(\sigma) \le Q(\sigma)$.
• Lemma 3.3: a chain that evicts by the predictions only has length $n(r,c) \le 1 + S(\eta_{r,c})$, where $\eta_{r,c}$ is the error of the predictions on the elements evicted into it.
• Lemma 3.4: $\mathbb E[n(r,c)] \le \mathbb E[\min(1 + 2S(\eta_{r,c}), 2H_k)]$.

Significance

The result. Theorem 3.3 gives both guarantees at once. For an exact predictor ($\epsilon = 0$) the ratio is a constant, $2(1 + 2S(0))$, independent of $k$; for an arbitrary predictor it is $4H_k$, within a constant factor of the optimal randomized ratio. In between, the ratio degrades with the error at the rate of the spread: for the absolute loss the spread grows like $\sqrt m$, so the ratio grows like $\sqrt\epsilon$. The spread and the chain decomposition are the tools later papers build on to trade consistency against robustness.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it, of the Marker analysis, or of the clean-element bound of Fiat et al. is known. A formalization supplies a precise model of a randomized online algorithm with predictions. It also settles the details the paper leaves implicit: the eviction missing from the clean branch of Algorithm 1 as printed, the cap $2H_k$ printed as $2\log k$ in Lemma 3.4, and the behaviour of the spread at $0$.

Difficulty

The obvious argument charges every miss to a chain and bounds each chain separately. That works for chains that follow the predictions, but a chain that switches to random evictions interacts with every other chain of the phase, because all of them evict from the same pool of unmarked elements. A bound on its expected length must hold whatever the other chains evict, including evictions that depend on earlier coin flips. A second difficulty is summing. The chain errors $\eta_{r,c}$ and the chain lengths are both random, while the hypothesis controls only the total error $\eta_\ell(h,\sigma)$ against $\mathrm{Opt}(\sigma)$, not the number of chains $Q(\sigma)$ in which the error is spread.

Formalization scope

Elements form a type with decidable equality. A request sequence is a list; predictions are one real per request, and every real sequence is allowed. Labels are 1-based next-arrival positions, with $n+1$ for elements never requested again. The paper prints the label with equal features; the element is meant. $\mathrm{Opt}$ is computed as the minimum over all demand-paging schedules from the empty cache, which loses no generality. $H_k$ is harmonic k as a real number, never $\log k$.

Predictive Marker is a PMF over final states. The random eviction of line 21 is uniform over the unmarked cached elements, and ties in the arg max are a parameter quantified universally. The eviction of lines 23–24 is also performed after a clean miss; as printed, it sits only in the stale branch. The expected cost lies in $[0,\infty]$.

The spread takes real arguments and lengths $T \ge 1$. $S$ must be concave on $[0,\infty)$, finite, and at least the spread. It must also be continuous at $0$, which the paper does not say: without it the chain lemma fails for losses whose minimal reversed-order loss stays $0$ over several lengths. $\epsilon$-accuracy is the pointwise condition on the given pair $(\sigma, h)$. The competitive ratio is written as a product, so $\mathrm{Opt}(\sigma) = 0$ needs no special case. Lemma 3.3 is stated pointwise for chains without random evictions, as its proof shows. Lemma 3.4 has $2H_k$ in place of the printed $2\log k$, with the minimum inside the expectation because $\eta_{r,c}$ is random.

The statement must not be trivialized. $\mathrm{Opt}$ is the true offline optimum, not Bélády's rule applied to the predictions. The expectation is taken over Predictive Marker's own run, never compared with itself. The spread hypothesis is satisfiable; for example, the constant loss $1$ has spread $\max(1,\lceil m\rceil) \le m + 1$.

Out of scope: Lemma 3.2 (the special-marking algorithm SM, which enters only through Lemma 3.4's proof); Lemma 3.1 and Corollaries 1–2, whose printed constants are false for small $m$ or disagree with Theorem 3.3; the lower bounds of §3.1 and §3.4; the extensions of §4; the experiments of §5; running time and learnability.

Welcome contributions: the Marker phase structure and its equivalence with the combinatorial phases, the clean-element bounds $Q/2 \le \mathrm{Opt} \le Q$ (reusable for any marking algorithm), and a bound on the expected number of misses caused by elements evicted uniformly at random within a phase.

Selected references

• T. Lykouris, S. Vassilvitskii, Competitive Caching with Machine Learned Advice, arXiv:1802.05399v4, 2020; J. ACM 68(4), 2021. https://arxiv.org/abs/1802.05399v4
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive paging algorithms, J. Algorithms 12(4), 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• L. A. Bélády, A study of replacement algorithms for a virtual-storage computer, IBM Systems Journal 5(2), 1966. https://doi.org/10.1147/sj.52.0078
• D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Comm. ACM 28(2), 1985. https://doi.org/10.1145/2786.2793
• D. Rohatgi, Near-optimal bounds for online caching with machine learned advice, SODA 2020. https://arxiv.org/abs/1910.12172
• A. Wei, Better and simpler learning-augmented online caching, APPROX/RANDOM 2020. https://arxiv.org/abs/2005.13716