All missions

Motivation

Global commodity trade separates supply from consumption by months of shipping. Australia and Brazil supply most of the world's iron ore, while China, Japan and South Korea consume over 80% of it. Importers therefore sign long-term contracts before they know the demand they will serve. Under the traditional fixed-price contract (FPC) the price is set at signing. Under the contingent-price contract (CPC) the price is pegged to an index and stays open until delivery, which exposes the importer to the index.

Conventional wisdom treats that exposure as a cost. Xing, Liu, Zhang and Zhao (Management Science, 2024) show a mechanism in the other direction. The unrealized CPC price is correlated with demand, so a firm's demand forecast also tells it something about its cost. They call this the price-learning effect. A larger price volatility strengthens it, and past a threshold a larger price volatility raises equilibrium profits. The model builds on the Gaussian duopoly literature on private information, which goes back to Vives (1984).

Setting

Two firms $A,B$ order a commodity and resell it in one market. With quantities $q_A,q_B$, firm $i$ with rival $j$ faces the market-clearing price

$$p_i=a+\varepsilon_a-q_i-\gamma q_j,\qquad\gamma\in[0,1].$$

Under the FPC the firm pays the known price $w$, and under the CPC it pays $s=\mu_s+\varepsilon_s$. Its realized profit is $\pi_i=(p_i-c_i)q_i$, with $c_i=w$ or $c_i=s$.

The noises are centered and jointly Gaussian. The pair $(\varepsilon_a,\varepsilon_s)$ has standard deviations $\sigma_a,\sigma_s$ and correlation $\rho\in[0,1)$. Firm $i$ observes the private signal $f_i=\varepsilon_a+\varepsilon_i$, where $\varepsilon_i\sim N[0,\sigma_i^2]$. The pair $(\varepsilon_A,\varepsilon_B)$ has correlation $\eta\in[0,1)$ and is independent of $(\varepsilon_a,\varepsilon_s)$.

The relative price volatility is $\theta=\sigma_s/\sigma_a$. The derived constants are

$$\lambda_i=\frac{\sigma_a^2}{\sigma_a^2+\sigma_i^2},\quad\beta=\frac{\eta\sigma_A\sigma_B}{\sigma_a^2},\quad\kappa=\frac{1}{4-\gamma^2\lambda_A\lambda_B(1+\beta)^2}.$$

Each assignment of contracts gives a Cournot subgame: CC, CF, FC or FF, with the first letter firm $A$'s. A strategy maps the firm's signal to a real quantity. A Bayesian Nash equilibrium is a profile from which no firm gains by deviating to any measurable, square-integrable strategy. The ex ante profit $\Pi^k_i$ is the expectation of $\pi_i$ at the equilibrium of subgame $k$.

Formalization targets

Goal: Proposition 1

Let $\rho>0$ and hold every parameter except $\theta$ fixed. Equilibria of CC and FC exist at every $\theta>0$. In the CC subgame, on either side of $1/\rho$,

$$\theta\mapsto\Pi^{CC}_i(\theta)\text{ is nonincreasing on }(0,1/\rho],\text{ nondecreasing on }[1/\rho,\infty),$$

strictly so when $\gamma\lambda_j(1+\beta)\neq2$. In the FC subgame with $\gamma\neq0$, $\Pi^{FC}_A$ and $\Pi^{FC}_B$ are strictly decreasing below, and strictly increasing above, the thresholds

$$\theta^T_A=\frac{-2+\gamma\lambda_B(1+\beta)}{\rho\gamma\lambda_B(1+\beta)},\qquad\theta^T_B=\frac{2-\gamma\lambda_A(1+\beta)}{2\rho}.$$

The strictness hypothesis in (a) is a correction: the printed proposition omits it, and at equality $\Pi^{CC}_i$ is constant in $\theta$. An instance is $\sigma_a=1$, $\sigma_A=6$, $\sigma_B=1$, $\eta=1/2$, $\gamma=1$.

Milestones

1. Lemma 1. $E[\varepsilon_a|f_i]=\lambda_if_i$, $E[\varepsilon_s|f_i]=\rho\theta\lambda_if_i$, $E[f_j|f_i]=(1+\beta)\lambda_if_i$.
2. §4.1. $\kappa>0$.
3. Lemma 2(a). FF has a unique equilibrium, with quantities (1).
4. Lemma 2(b). CC has a unique equilibrium, with quantities (2).
5. Lemma 2(c). FC has a unique equilibrium, with quantities (3)–(4), and CF has the exchanged one.
6. Eq. (6). $\Pi^{CC}_i$ in closed form at every equilibrium of CC.
7. Eqs. (7)–(8). $\Pi^{FC}_A,\Pi^{FC}_B$ in closed form at every equilibrium of FC.

Significance

The result reverses the usual reading of volatility in procurement. Volatility is a cost only while it is small. Beyond $1/\rho$ in CC, firms lean on cost-side updating and their quantities track the contract price more closely. This is why the paper's later results, on contract choice, predict that significant price volatility pushes firms towards the CPC. The closed forms (6)–(8) also separate each profit into an efficiency component and an information benefit, which the rest of the paper uses.

The result is proved in the published paper, and no machine-checked proof of it is known to exist. The proofs are in the paper's Appendix, which is not part of the source file used here, so every statement of this mission was checked independently of them. Formalizing the result adds the correction to (a), and a complete account of the conventions the paper leaves implicit: the joint law of the noises, the sign of the quantities, and uniqueness up to null sets.

Difficulty

The monotonicity itself is elementary once (6)–(8) are known. The work lies before it, in two places.

The first is Gaussian regression for a four-dimensional law with correlated forecast noises, which gives Lemma 1.

The second is that the equilibrium quantifies over every admissible strategy, while the closed forms are affine. Solving the coefficient equations of the affine ansatz, the obvious first step, proves neither that the affine profile beats non-affine deviations nor that no non-affine equilibrium exists. Lemma 2 claims both, among strategies unrestricted in sign, so the corner analysis of ordinary Cournot models plays no role.

Formalization scope

Everything is in the namespace CommodityCPC. BayesianGame is a general object: a prior, real signals, payoffs, admissible strategies, ex ante payoff and IsBNE. Params holds $a,\mu_s,w,\sigma_a,\sigma_A,\sigma_B,\rho,\eta,\gamma$ with their standing assumptions; $a,\mu_s,w$ are arbitrary reals. The volatility $\theta$ is a separate argument, and $\sigma_s=\theta\sigma_a$. The space is $\mathbb R^4$ with four independent standard normals, and the noises are explicit linear forms in them, realizing the joint law above. The Lean name for $\lambda_i$ is lam.

Quantities are real and unrestricted in sign. The paper's affine strategies are negative with positive probability, so a nonnegativity constraint would contradict Lemma 2, and its remark that standard deviations are "sufficiently smaller" than $a,\mu_s$ has no formal content. Equilibrium is ex ante, and uniqueness is $P$-almost sure on $\sigma_i(f_i)$.

A trivializing formalization is ruled out: the equilibrium and $\Pi$ are primitives, never defined through (1)–(8), deviations are not restricted to affine strategies, and the goal includes existence so that its comparisons of equilibria are not vacuous.

The development needs Mathlib's Gaussian measures, conditional expectation and $L^p$ spaces. Gaussian regression for jointly normal vectors and the uniqueness argument for quadratic Bayesian games are reusable beyond this mission. Proofs of the goal, of any milestone, or of intermediate lemmas are welcome.

Selected references

• W. Xing, L. Liu, F. Zhang, Q. Zhao, The Bright Side of Price Volatility in Global Commodity Procurement, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.00304 (the version used here: SSRN 4717149, https://ssrn.com/abstract=4717149)
• X. Vives, Duopoly information equilibrium: Cournot and Bertrand, Journal of Economic Theory 34(1), 1984, 71–94. https://doi.org/10.1016/0022-0531(84)90162-5

Motivation

In two-stage robust optimization a decision maker fixes a here-and-now decision $x$, an adversary then picks an uncertain parameter $\zeta$ from an uncertainty set $\mathcal U$, and finally a wait-and-see decision $y$ is chosen with knowledge of $\zeta$. When the objective and constraints are linear in $y$, a large toolbox is available: linear decision rules, Fourier–Motzkin elimination, Benders decomposition, column-and-constraint generation (Zeng and Zhao 2013). When $y$ enters through convex nonlinear functions $g_i(y)$, none of these applies directly, and even imposing a linear decision rule leads to maximizing a convex function over a polyhedron, which is NP-hard in general.

de Ruiter, Zhen and den Hertog (2023) show that for a polyhedral uncertainty set and fixed recourse the nonlinear problem is equivalent to a two-stage robust problem whose adjustable variable enters linearly. This extends the consecutive dualization of Bertsimas and de Ruiter (2016), which treats the linear case, to convex recourse.

Setting

Vectors are real column vectors. The data are a set $\mathcal X\subseteq\mathbb R^{n_x}$; functions $f_i:\mathbb R^{n_x}\to\mathbb R$ and $g_i:\mathbb R^{n_y}\to\mathbb R$, $i=0,\dots,m_1$, all convex; arbitrary real functions $F_{ij}$ on $\mathbb R^{n_x}$, $i=1,\dots,m_1$, $j=1,\dots,n_\zeta$, with rows $F_{i\cdot}(x)$; affine maps $A(x)=A^0+\sum_{l=1}^{n_x}A^lx_l\in\mathbb R^{m_2\times n_\zeta}$ and $b(x)=b^0+\sum_l b^lx_l\in\mathbb R^{m_2}$; a recourse matrix $B\in\mathbb R^{m_2\times n_y}$; and a nonempty polyhedral uncertainty set $\mathcal U=\{\zeta\ge0:\ D\zeta=d\}$ with $D\in\mathbb R^{p\times n_\zeta}$, $d\in\mathbb R^p$.

The primal problem (1) is

$$\inf_{x\in\mathcal X}\ \sup_{\zeta\in\mathcal U}\ \inf_y\bigl\{f_0(x)+g_0(y)\ \big|\ \zeta^\top F_{i\cdot}(x)+f_i(x)+g_i(y)\le0,\ i=1,\dots,m_1,\ A(x)\zeta+By=b(x)\bigr\}.$$

Write $\Phi(x)$ (primalValue) for the value of $x$, the $\sup_\zeta\inf_y$ part.

The convex conjugate of $g$ is $g^*(s)=\sup_y\{s^\top y-g(y)\}$, and $v\,g^*(u/v)$ denotes its perspective, closed at $v=0$. The dual uncertainty set is

$$\mathcal V=\Bigl\{(u,v,w,z):\ v\ge0,\ v_0=1,\ v_i(g_i)^*\Bigl(\frac{u_i}{v_i}\Bigr)\le z_i,\ i=0,\dots,m_1,\ \sum_{i=0}^{m_1}u_i=-B^\top w\Bigr\},$$

and the dualized model (6) is $\inf_{x\in\mathcal X}\Psi(x)$ with

$$\Psi(x)=\sup_{(u,v,w,z)\in\mathcal V}\ \inf_\lambda\Bigl\{\sum_{i=0}^{m_1}v_if_i(x)+d^\top\lambda-w^\top b(x)-\sum_{i=0}^{m_1}z_i\ \Big|\ \sum_{k=1}^pD_{kj}\lambda_k\ge w^\top A_{\cdot j}(x)+\sum_{i=1}^{m_1}v_iF_{ij}(x),\ j=1,\dots,n_\zeta\Bigr\}$$

(dualValue). Assumption 1 (relatively complete recourse) asks that for every $x\in\mathcal X$ and $\zeta\in\mathcal U$ some $y$ satisfies the constraints of (1), strictly for each $i\ge1$ whose $g_i$ is nonlinear.

Formalization targets

Goal: Theorem 1 (Dual Formulation), p.1796

Under (2), (3), convexity and Assumption 1,

$$\forall x\in\mathcal X:\ \bigl(\Phi(x)<+\infty\iff\Psi(x)<+\infty\bigr)\qquad\text{and}\qquad\inf_{x\in\mathcal X}\Phi(x)=\inf_{x\in\mathcal X}\Psi(x).$$

Both clauses are part of the goal: the feasible here-and-now decisions coincide, and so do the optimal values.

Milestones

1. Refined Slater duality. For a convex program with finite convex $\varphi,h_i$ on $\mathbb R^n$ and affine equalities, a point feasible for all constraints and strictly feasible for the non-affine $h_i$ gives a zero duality gap, in the extended reals.
2. Conjugate of a weighted sum. $\inf_y\{\sum_iv_ih_i(y)-s^\top y\}=-\inf\{\sum_iv_ih_i^*(u_i/v_i):\sum_iu_i=s\}$ for $v\ge0$.
3. First dualization. Under the recourse condition at $(x,\zeta)$, the inner value of (1) equals $\sup_{\mathcal V}\{\sum_iv_if_i(x)+\sum_{i\ge1}v_i\zeta^\top F_{i\cdot}(x)+w^\top(A(x)\zeta-b(x))-\sum_iz_i\}$.
4. Second dualization. $\sup_{\zeta\in\mathcal U}c^\top\zeta=\inf\{d^\top\lambda:\ D^\top\lambda\ge c\}$ for nonempty $\mathcal U$, both sides possibly $+\infty$.
5. Pointwise equality. $\Phi(x)=\Psi(x)$ at every $x$ satisfying Assumption 1.

Significance

Model (6) is a two-stage robust problem in which the adjustable variable $\lambda$ appears linearly and the convex structure of the recourse has moved into the new uncertainty set $\mathcal V$. Every technique for adjustable robust linear problems therefore applies to it. The paper uses (6) to derive a tractable linear-decision-rule approximation (8), to recover primal linear decision rules (Theorem 2) and to compute lower bounds from scenarios (Theorem 3). Each of these rests on the exact equivalence of Theorem 1. When all $f_i$, $F_{ij}$ and $g_i$ are affine, Theorem 1 coincides with Theorem 1 of Bertsimas and de Ruiter (2016).

The theorem is proved in the paper's e-companion; no machine-checked version exists. A formal proof checks the two-step duality chain in the extended reals, including cases the paper does not discuss: an unbounded $\mathcal U$ (both values $+\infty$), an empty $\mathcal V$ (both values $-\infty$), and constraints with affine $g_i$, which need no strict feasibility.

Difficulty

The obvious argument is "Lagrange duality in $y$, then LP duality in $\zeta$, then swap the two suprema", and each step needs care. Lagrange duality without a gap requires a constraint qualification. Assumption 1 gives only a refined Slater point, strict for the non-affine constraints and merely feasible for the affine ones, so the textbook Slater theorem, which demands strictness everywhere, does not apply. The conjugate of $\sum_iv_ih_i$ must be written as an infimal convolution of perspectives, including weights $v_i=0$, where the naive convention $0\cdot(+\infty)=0$ gives the wrong set. LP duality must be used in its extended form, since the dual can be infeasible while the primal is unbounded. Finally, the notion of "feasible" in Theorem 1 must be the finiteness of the worst-case value: the scenario-wise reading (a $y$ for every $\zeta$, a $\lambda$ for every $\mathcal V$-point) is false already for a one-dimensional instance with $\mathcal U=\mathbb R_+$.

Formalization scope

All vectors are Fin n → ℝ, the index $i=0,\dots,m_1$ is Fin (m1+1), and the rows $F_{i\cdot}$, $i=1,\dots,m_1$, are Fin m1, paired with f i.succ, g i.succ. The data are bundled in the structure DualTwoStageRO.Problem; convexity of the $f_i,g_i$ and nonemptiness of $\mathcal U$ are hypotheses of the theorems. Every optimal value is in EReal: an infimum over an empty set is $+\infty$ and a supremum over an empty set is $-\infty$, so no junk real value can make the goal vacuous. "Feasible for (1)" is $\Phi(x)<+\infty$ and "feasible for (6)" is $\Psi(x)<+\infty$. The perspective of $g_i^*$ at $v_i=0$ is $0$ at $u_i=0$ and $+\infty$ otherwise. "Nonlinear $g_i$" is read as "non-affine $g_i$". $\lambda$ is free. No dimension is assumed positive, $\mathcal U$ may be unbounded, and $\mathcal X$ is arbitrary. $\mathcal V$ is the printed set; restricting it to points where the $\lambda$-problem is feasible, or computing values in ℝ with sSup/sInf, would trivialize or falsify the goal.

A complete development needs Lagrangian duality with a refined Slater condition, the conjugate of a sum of finite convex functions, and LP duality in the extended reals. All three are reusable beyond this mission. Proofs of the milestones and alternative routes to the goal are welcome.

Selected references

• F. J. C. T. de Ruiter, J. Zhen, D. den Hertog, Technical Note—Dual Approach for Two-Stage Robust Nonlinear Optimization, Operations Research 71(5):1794–1799, 2023. https://doi.org/10.1287/opre.2022.2289
• D. Bertsimas, F. J. C. T. de Ruiter, Duality in Two-Stage Adaptive Linear Optimization: Faster Computation and Stronger Bounds, INFORMS Journal on Computing 28(3):500–511, 2016. https://doi.org/10.1287/ijoc.2016.0689
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• B. Zeng, L. Zhao, Solving two-stage robust optimization problems using a column-and-constraint generation method, Operations Research Letters 41(5):457–461, 2013. https://doi.org/10.1016/j.orl.2013.05.003

Motivation

Integer linear programs $\min\{c^\top x : Ax\le b,\ x\in\mathbb Z^n\}$ are NP-hard in general, and one of the best-known tractable classes is the one where $A$ is totally unimodular (TU): every square submatrix has determinant in $\{-1,0,1\}$. It is a long-standing open question whether integer programs with a $\Delta$-modular constraint matrix (full column rank, all $n\times n$ subdeterminants bounded by $\Delta$ in absolute value) are efficiently solvable for constant $\Delta$. Beyond the TU case, progress exists only for $\Delta=2$ (Artmann, Weismantel and Zenklusen, STOC 2017), whose proof reduces bimodular programs to TU programs with a parity constraint.

A natural intermediate class is that of congruency-constrained TU problems: a TU system together with one constraint $\gamma^\top x\equiv r\pmod m$. For prime $m$ these are equivalent to integer programs whose $n\times n$ subdeterminants lie in $\{0,\pm m\}$ (p.1 of the paper). Nägele, Santiago and Zenklusen (arXiv:2109.03148) give the first algorithm beyond parity constraints.

Timeline:

• 2017: Artmann–Weismantel–Zenklusen, strongly polynomial algorithm for bimodular integer programs and for TU problems with parity constraints ($m=2$).
• 2019: Nägele–Sudakov–Zenklusen, submodular minimization under congruency constraints for prime power moduli (Combinatorica 2019).
• 2022–2024: Nägele–Santiago–Zenklusen, feasibility for $m=3$ (SODA 2022; this preprint, v3 2023; Mathematics of Operations Research 2024).

Setting

Let $T\in\{-1,0,1\}^{k\times n}$ be totally unimodular, $b\in\mathbb Z^k$, $m\in\mathbb Z_{>0}$, $\gamma\in\mathbb Z^n$. The CCTUF problem (congruency-constrained TU feasibility) with $r\in\mathbb Z$ asks to show infeasibility of, or find a solution of,

$$Tx\le b,\qquad\gamma^\top x\equiv r\pmod m,\qquad x\in\mathbb Z^n.$$

The R-CCTUF problem replaces the single residue by a set $R\subseteq\{0,\dots,m-1\}$ of target residues: $\gamma^\top x\equiv r\pmod m$ for some $r\in R$. The larger $R$, the easier the problem; $|R|=m$ is an ordinary TU problem. The optimization version CCTU minimizes $c^\top x$ over the same set and must report infeasibility, unboundedness (arbitrarily small objective values) or a minimizer.

An algorithm is randomized in the paper's sense (footnote 4) if it always correctly reports infeasibility and finds a solution of a feasible problem with probability at least $1-1/n$, $n$ the number of variables.

Formalization targets

Goal: Theorem 1

$$\exists\ \text{a strongly polynomial randomized algorithm for CCTUF with } m=3.$$

The goal fixes the modulus and nothing else: $k$, $n$ and the integers $b,\gamma,r$ are arbitrary, rows may repeat, and one program serves all instances.

Milestones

• the general form, Theorem 2: for every prime $m$, a strongly polynomial randomized algorithm for R-CCTUF with $|R|\ge m-2$ (for $m=3$ this contains Theorem 1);
• the recursion along Seymour's decomposition (Theorem 14) of TU matrices into network matrices, their transposes, two $5\times5$ matrices, and 1-, 2-, 3-sums;
• the base blocks: Theorem 15 (feasibility for base blocks), from Theorems 35, 40 and 52 (CCTU for network matrices, transposed network matrices, and matrices with a constant-size core);
• the decomposition step, Theorem 22, built from the narrowed pattern of a 3-sum: Lemmas 21, 54, 57 and Theorems 18, 19;
• the proximity tools: Lemma 7 (decomposition into elementary vectors), Lemma 8 and Lemma 25 (one TU-appendable scalar product can be confined to a range of width $m-|R|$).

Significance

Theorem 1 is the first polynomial algorithm for congruency-constrained TU problems beyond parity, and so the first result for the $\{0,\pm3\}$-subdeterminant integer programs mentioned above. Its general form, Theorem 2, climbs two steps of the hierarchy of R-CCTUF problems for every prime modulus; the recursion it introduces (patterns over pairs of scalar products, controlled with the Cauchy–Davenport inequality) is the paper's main methodological contribution. Theorem 1 is proved in the paper; nothing in it has a machine-checked proof. The formalization would add a cost model for integer algorithms with coins and oracles, Seymour's decomposition as an algorithmic statement, network matrices, and integer decomposition in TU cones, none of which exist on the platform in this form.

Difficulty

The natural algorithm guesses the two scalar products $(\alpha,\beta)$ that couple the blocks of a 1-, 2- or 3-sum and recurses on both blocks. This is polynomial only when the decomposition is balanced; Seymour's theorem guarantees only two columns on the smaller side, so the recursion depth can be linear and the enumeration exponential. The paper avoids this by solving the small side completely, analysing the resulting pattern of feasible residues, and either progressing in the number of target residues (which needs $m$ prime) or replacing the small side by two variables. The base blocks rest on results from other papers: randomized exact-length circulations (Camerini–Galbiati–Maffioli) for network matrices, and congruency-constrained submodular minimization for their transposes. These are part of the proof, not assumptions, and have no Lean substrate.

Formalization scope

All algorithmic statements use one machine, CongruencyTU.Machine: a RAM over integer registers with unit-cost $+,-,\times$, integer division and remainder (Lean's Euclidean conventions), comparison, indirect addressing, coin flips, an oracle instruction, and halting. Strongly polynomial means one program, fixed before the input, whose cost is at most $p(\text{number of input integers})$ and whose registers have bit length at most $q(\text{input bit size})$; the bit-length clause is essential, since unit-cost multiplication would otherwise compute with exponentially long numbers. Integer remainder is unit-cost on purpose: with only $+,-,\times,/$ and comparisons, Theorem 1 is false already for a fixed-dimension instance whose feasibility is $\gamma_1\equiv1\pmod 3$. Randomness is a uniform coin string of length equal to the cost bound; probabilities are fractions of coin strings, compared in $\mathbb Q$. "Constant modulus" means the program may depend on $m$ but not on the instance. Instances are lists of integers (dimensions, the matrix row by row, $b$, $\gamma$, $r$ or $R$), and outputs are $[0]$ for "infeasible" or $1::x$ for a solution $x$.

No cited algorithm (Tardos' strongly polynomial LP algorithm, Camerini–Galbiati–Maffioli, Nägele–Sudakov–Zenklusen, Seymour's decomposition algorithm) appears as a hypothesis: a statement assuming them would be conditional. Theorem 22 is an oracle reduction, quantified over every oracle that solves the smaller problems. Lemma 8 is stated with singleton intervals allowed, since the printed version (strict $i_1<i_2$) is false for $m=2$, $R=\{1\}$, $r=(1,0)$.

Problems of form (1) are given with totally unimodular 3-sum summands; network matrices use a spanning tree on $\{0,\dots,k\}$; the core of Definition 51 is any submatrix reached by deletions to which no deletion applies. Contributions are welcome on every layer: the cost model's basic programs (arithmetic on lists, Gaussian elimination with bounded bit sizes), Tardos' algorithm, Seymour's decomposition, network-matrix recognition, the combinatorial lemmas (Lemmas 8, 57, Theorem 19), and the pattern analysis.

Selected references

• M. Nägele, R. Santiago, R. Zenklusen, Congruency-Constrained TU Problems Beyond the Bimodular Case, arXiv:2109.03148v3, 2023; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2109.03148v3
• S. Artmann, R. Weismantel, R. Zenklusen, A strongly polynomial algorithm for bimodular integer linear programming, STOC 2017. https://doi.org/10.1145/3055399.3055473
• M. Nägele, B. Sudakov, R. Zenklusen, Submodular minimization under congruency constraints, Combinatorica 39, 2019. https://doi.org/10.1007/s00493-019-3900-1
• P. M. Camerini, G. Galbiati, F. Maffioli, Random pseudo-polynomial algorithms for exact matroid problems, Journal of Algorithms 13, 1992. https://doi.org/10.1016/0196-6774(92)90012-2
• É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Operations Research 34, 1986. https://doi.org/10.1287/opre.34.2.250
• P. D. Seymour, Decomposition of regular matroids, Journal of Combinatorial Theory, Series B 28, 1980. https://doi.org/10.1016/0095-8956(80)90075-1

Why the variance of service capacity matters

Systems that serve jobs with deadlines and can adjust their capacity on the fly, such as electric-vehicle charging stations and cloud data centers, pay for both the level and the volatility of the resource they draw. A charging station that buys energy on the day-ahead market needs a predictable power draw, and peaks strain the grid. Nakahira, Ferragut and Wierman (arXiv:2004.12280v2, 2020; Operations Research, 2023) ask which distributed scheduling rule, one that sets each job's service rate from that job's own remaining demand and remaining time, minimizes the stationary variance of the total service capacity. They also allow demands and deadlines to be violated at a price.

Before this paper, optimality results for such schedulers were known only in special settings: a static single server, or deterministic worst-case models. The paper's results are exact and in closed form for stationary Poisson arrivals: Exact Scheduling (Theorem 1), a rate cap at $\delta/2$ for soft demands (Theorem 2), a rate cap at $\sqrt\varepsilon$ with deadline extension for soft deadlines (Theorem 3), and their combination, Generalized Exact Scheduling (Theorem 4).

Setting

A job $k$ has an arrival time $a_k$, a service demand $\sigma_k$ and a sojourn time $\tau_k$, so its deadline is $a_k+\tau_k$. The job types $(\sigma,\tau)$ lie in a bounded set $S\subseteq\{0\le\sigma\le\tau\}$ and have a probability law $\mu$ on $S$. Jobs arrive as a Poisson random measure $N$ on $\mathbb R\times\mathbb R^2$ with intensity $\Lambda\,da\otimes\mu$: arrivals at rate $\Lambda>0$ on $[0,\infty)$, with independent types.

A rate profile $v(\sigma,\tau,y)\in[0,1]$ is the service rate of a job of type $(\sigma,\tau)$ when its remaining time is $y$ (form (14)); $y$ starts at $\tau$ and becomes negative after the deadline. A job served by $v$ receives $\hat\sigma_v(\sigma,\tau)=\int_{-\infty}^{\tau}v\,dy\le\sigma$ units of service, and its deadline extension is $\mathrm{ext}_v(\sigma,\tau)=\sup\{-y:v(\sigma,\tau,y)>0\}\in[0,\infty]$. The service capacity $P(t)$ is the sum of the rates of all jobs present at time $t$. With a unit cost $\delta\ge0$ per unit of unmet demand and $\varepsilon>0$ per unit of extension, the objective is

$$\mathrm{cost}(v)=\mathrm{Var}(P)+E[\delta U]+E[\varepsilon W],$$

the stationary variance of $P$ plus the long-run rates of the two penalties. A policy of form (4) is a function $u(x,y)$ of remaining demand $x$ and remaining time $y$; it produces a rate profile through the trajectory $x(s)=\sigma-\int_0^s u(x(s'),\tau-s')\,ds'$ of each job.

Formalization targets

Goal: Theorem 4

With $J^*(\sigma,\tau)$ equal to $\sigma^2/\tau$ if $\sigma/\tau\le\min\{\delta/2,\sqrt\varepsilon\}$, to $\delta(\sigma-\delta\tau/4)$ if $\sigma/\tau>\delta/2$ and $\delta/2\le\sqrt\varepsilon$, and to $2\sqrt\varepsilon\,\sigma-\varepsilon\tau$ if $\sigma/\tau>\sqrt\varepsilon$ and $\sqrt\varepsilon<\delta/2$:

$$\min_{v\ \text{feasible}}\ \mathrm{cost}(v)=\Lambda\,\mathbb E_\mu\big[J^*(\sigma,\tau)\big],$$

attained by the profile (96), which Generalized Exact Scheduling (25) produces along every trajectory. If $\varepsilon\ne\delta^2/4$, the minimizer is unique almost everywhere.

Milestones

1. Campbell's formula (Theorem 7): $\mathbb E[\int g\,dN]=\int g\,d\nu$ and $\mathrm{Var}(\int g\,dN)=\int g^2\,d\nu$ for $g\in L^1\cap L^2$.
2. Lemma 2: $\mathrm{Var}(P)=\Lambda\int\!\int_{-\infty}^{\tau}v^2\,dy\,d\mu$.
3. Eq. (81) and the $E[W]$ display: a per-job penalty $c$ has long-run rate $\Lambda\int c\,d\mu$.
4. Lemmas 1, 7 and 8: the optimal profiles and values (16), (22), (24) under strict, soft-demand and soft-deadline constraints.
5. The per-job minimization of $s^2/T+\delta(\sigma-s)+\varepsilon(T-\tau)$ in the proof of Lemma 9.
6. Lemma 9: the profile (96) is optimal over all feasible profiles, with value (26).
7. Appendix E: policy (25) produces the rates (96).

What the result gives

Theorem 4 says that the optimal trade-off between capacity volatility, unmet demand and late completion is decided job by job, from local information only. A job is served at its flat rate $\sigma/\tau$ when that rate is below both thresholds. Otherwise the rate is capped at $\delta/2$ and part of the demand is dropped, when demand is the cheaper constraint to violate, or it is capped at $\sqrt\varepsilon$ and the deadline is extended. The closed form of the optimal cost gives the exact value of relaxing each constraint, and it contains Theorems 1 to 3 as special cases.

The result is proved in the paper; nothing here is open. Nothing in it is machine-checked. A formalization would add to the library a Poisson random measure with Campbell's first- and second-moment formulas, the variance formula for an infinite-server system with time-varying rates (a form of Brumelle's formula), and a complete optimality proof for a stochastic scheduler. Three printed statements are corrected along the way (next section), so the formal version is also the first correct statement of the theorem.

Difficulty

The obvious argument is to minimize $\int v^2$ job by job with Cauchy–Schwarz, and that is the core of the proof. It is not the whole proof. First, the variance of $P(t)$ must be computed from the point process: Campbell's formula for a random measure needs simple-function approximation together with independence on disjoint sets, and Mathlib has neither the formula nor the random measure. Second, the penalties cannot be read at a fixed time. $U(t)$ sums over jobs whose deadline is exactly $t$, which is almost surely empty, so a literal reading makes serving nothing free; the objective must use long-run rates. Third, the uniqueness clause requires an equality analysis of the per-job minimization, which is not unique at $\varepsilon=\delta^2/4$. Fourth, realizing the optimal profile by a policy of form (4) is an ODE statement with a singular right-hand side $x/y$ as $y\to0$ and a discontinuous one at $x=0$ after the deadline.

Formalization scope

Arrival times range over $[0,\infty)$ and stationary quantities are limits as $t\to\infty$: $\mathrm{Var}(P)$ is the $\limsup$ of the $[0,\infty]$-valued variance of $P(t)$, and each penalty is the $\limsup$ of $T^{-1}\,\mathbb E[\sum_{a_k+\tau_k\le T}c(\sigma_k,\tau_k)]$. Lemma 2 and (81) prove that these are limits. The continuity equation (5) is not formalized. Sums over jobs are integrals against $N(\omega)$. Costs live in $[0,\infty]$, and the extension is an $[0,\infty]$-valued supremum, so a job served forever costs $\infty$. Feasibility contains $\hat\sigma_v\le\sigma$ (constraint (80)). The mark law is any probability measure on $S$, not necessarily a density. The lower bound ranges over all measurable rate profiles of form (14), which contain the realized rates of every policy of form (4).

Three printed statements are false and are corrected. The third line of (25) reads "$\sqrt\varepsilon\,\mathbf 1\{x>0\}$ otherwise", which keeps serving a job after its deadline when $\delta/2<\sqrt\varepsilon$ and costs $5/4$ instead of $3/4$ at $\sigma=\tau=\delta=\varepsilon=1$; the corrected policy stops at the deadline in that regime. The indicators of (26) are reversed, and they are replaced by those matching (25) and (96). Theorem 7 assumes only $\int g^2<\infty$, which does not give absolute convergence, so the formula carries the added hypothesis $\int|g|\,d\nu<\infty$. Uniqueness is claimed only for $\varepsilon\ne\delta^2/4$, where it holds.

$\mathrm{Var}(P)$ and the penalty rates are computed from the point process and never defined by their closed forms, which are milestone conclusions. A definition of $\mathrm{Var}(P)$ as $\Lambda\int\int v^2$ would make Lemma 2 trivial and is excluded. Existence of a Poisson random measure is classical but not in Mathlib; contributions constructing one, or proving Campbell's formula, are reusable well beyond this mission.

Selected references

• Y. Nakahira, A. Ferragut, A. Wierman, Generalized Exact Scheduling: A Minimal-Variance Distributed Deadline Scheduler, arXiv:2004.12280v2, 2020; Operations Research, 2023. https://arxiv.org/abs/2004.12280v2
• F. Baccelli, P. Brémaud, Elements of Queueing Theory: Palm Martingale Calculus and Stochastic Recurrences, Springer, 2003 (Campbell's formula; Brumelle's formula). https://doi.org/10.1007/978-3-662-11657-9
• J. F. C. Kingman, Poisson Processes, Oxford University Press, 1993 (existence and Campbell's theorem), ISBN 978-0-19-853693-2.
• S. L. Brumelle, On the relation between customer and time averages in queues, Journal of Applied Probability 8(3):508–520, 1971. https://doi.org/10.2307/3212187

Motivation

Active disturbance rejection control (ADRC) is a feedback design in which an observer estimates, in real time, not only the state of an uncertain plant but also its total disturbance: the combined effect of unmodelled dynamics, external disturbances and the mismatch between the true and the nominal control gains. The controller cancels this estimate and then applies a nominal stabilizing law. The method is used in motion control, power electronics, chemical process control and MEMS gyroscopes, and its practice ran well ahead of its theory. Before this paper, global convergence of a closed loop with a nonlinear ADRC had been proved only for a class of SISO systems without zero dynamics (Guo–Zhao, CCDC 2012, reference [9] of the paper), the nonlinear observer alone had been analysed without feedback (Guo–Zhao 2011), and semiglobal results existed for linear observers. Guo and Zhao (SIAM J. Control Optim. 51 (2013)) treat MIMO systems with zero dynamics and nonlinear observers, and prove a global convergence theorem, Theorem 3.1, which is the goal of this mission.

Setting

The plant has $m\ge1$ subsystems. Subsystem $i$ has states $x^i=(x^i_1,\dots,x^i_{n_i})$ in a chain of integrators driven by an unknown function and by the controls $u\in\mathbb R^m$:

$$\dot x^i_j=x^i_{j+1}\ (j<n_i),\qquad \dot x^i_{n_i}=f_i(x,\xi,w_i)+\sum_{k}a_{ik}u_k,\qquad \dot\xi=F_0(x,\xi,w),$$

where $\xi\in\mathbb R^s$ is the zero dynamics and $w(t)$ a bounded disturbance with bounded derivative. The gains $a_{ik}$ are unknown; the designer knows an invertible nominal matrix $(b_{ik})$ with inverse $(b^*_{kl})$. The reference is a signal $z^i=(z^i_1,\dots,z^i_{n_i+1})$ with $\dot z^i_j=z^i_{j+1}$, typically produced by a tracking differentiator.

The extended state observer (ESO) has states $\hat x^i=(\hat x^i_1,\dots,\hat x^i_{n_i+1})$ and gain $1/\varepsilon$:

$$\dot{\hat x}^i_j=\hat x^i_{j+1}+\varepsilon^{n_i-j}g^i_j(e^i_1),\quad \dot{\hat x}^i_{n_i}=\hat x^i_{n_i+1}+g^i_{n_i}(e^i_1)+u^*_i,\quad \dot{\hat x}^i_{n_i+1}=\tfrac1\varepsilon g^i_{n_i+1}(e^i_1),$$

with $e^i_1=(x^i_1-\hat x^i_1)/\varepsilon^{n_i}$. The feedback ADRC(G) is $u^*_i=\varphi_i(\tilde x^i-z^i)+z^i_{n_i+1}-\hat x^i_{n_i+1}$, $u=b^*u^*$, where $\tilde x^i=(\hat x^i_1,\dots,\hat x^i_{n_i})$ and $\varphi_i$ defines a stable reference model. The last observer state estimates the extended state $x^i_{n_i+1}=f_i(x,\xi,w_i)+\sum_k(a_{ik}-b_{ik})u_k$.

Assumption A2 gives Lyapunov functions $V_1^i$ for the observer error dynamics, A3 gives Lyapunov functions $V_2^i$ for the reference model, GA1 bounds the derivatives of $f_i$, GA3 bounds the growth of $F_0$, and condition (3.1) says the gain mismatch is small:

$$\min_i\lambda^i_{13}-\sqrt m\sum_{i,k,l}\beta^i_1|a_{ik}-b_{ik}|\,|b^*_{kl}|\,\Lambda^l_{n_l+1}>0.$$

Formalization targets

Goal: Theorem 3.1

There are $\Gamma_1,\Gamma_2$, depending on the signals $w,z$ only through a bound on them, such that for some $\varepsilon_0>0$, every $\varepsilon\in(0,\varepsilon_0)$ and every solution, eventually

$$|x^i_j-\hat x^i_j|\le\Gamma_1\varepsilon^{n_i+2-j}\ (1\le j\le n_i+1),\qquad |x^i_j-z^i_j|\le\Gamma_2\varepsilon\ (1\le j\le n_i).$$

The goal fixes no constant: it asserts the $O(\varepsilon)$ shape, uniform in the initial value.

Milestones

The milestones follow the proof: the error equations (3.6); the bound (3.9) on the derivative $\bar\Delta_i$ of the extended state; the Lyapunov estimates (3.15), (3.17) and the two-case sign lemma (3.18)–(3.20); then, given an a priori bound on $\bar\Delta_i$, the estimates (3.21), (3.23), (3.25) for the observer error; and, given $\|e^i\|\le\Gamma_1\varepsilon$, the estimates (3.27), (3.29) for the tracking error.

Significance

Theorem 3.1 is a global separation principle for nonlinear ADRC: a high-gain observer and an observer-based feedback can be designed separately, and from any initial value the closed loop tracks the reference with error $O(\varepsilon)$ while the observer recovers the total disturbance. The paper's examples (Example 5.1, Proposition 5.3 on linear output regulation) use it to design observers.

No ADRC or extended-state-observer result is formalized on the platform or, to our knowledge, elsewhere. A complete development would be the platform's first convergence proof for a closed-loop observer and controller.

As printed, the theorem needs three corrections, each forced by a counterexample that satisfies every printed assumption. (i) GA2 lets the gains $a_{ik}(w_i(t))$ vary in time while $\xi$ may grow. With $m=n_1=s=1$, $\dot\xi=1$, $f_1=\xi$, $a_{11}=1+\sin t/10$, $b=1$, $\varphi(y)=-y$, $z\equiv0$, simulation of the closed loop at $\varepsilon=0.02$ shows $|x_1-z_1|$ growing linearly in $t$. The formalization takes $a_{ik}$ constant. (ii) In (3.1), $b^*_{kl}$ appears with its sign. Replacing $(a,b)$ by $(-a,-b)$ leaves the loop unchanged and flips the sign of the sum, so with $a=1$, $b=-1$ the printed condition holds while the closed-loop matrix has an eigenvalue $42.8$ at $\varepsilon=0.01$. The formalization uses $|b^*_{kl}|$. (iii) A1 bounds $z^i_1,\dots,z^i_{n_i}$ only, but the feedback uses $z^i_{n_i+1}$ and the proof uses $\dot z^i_{n_i+1}$. A reference with $z_2=\dot z_1$ spiking at late times breaks the observer bound, so the formalization bounds all components and $\dot z^i_{n_i+1}$. Two readings complete the setting: $|g^i_j(r)|\le\Lambda^i_j|r|$, since the printed $\Lambda^i_jr$ makes A2 unsatisfiable, and positivity of $\lambda^i_{11},\lambda^i_{21},\lambda^i_{23}$. Several displays of the proof also carry slips ((3.13) drops a term from $\Pi_4$, (3.16)–(3.20) write $\Pi_2$ for $\Pi_4$, (3.23) lacks the initial-value factor); the milestones state the corrected versions.

Difficulty

The proof is a chain of ODE estimates with explicit constants, but three steps are hard. First, the bound (3.9) requires differentiating the extended state along the closed loop across $m$ coupled subsystems; as printed, the computation (3.8) has sign and term slips. Second, the paper passes from "$\dot V\le0$ outside the ball of radius $R$" to "$\|(e,\eta)\|\le R$ eventually", which does not follow: a decreasing $V$ confines the solution to a sublevel set of $V$, not to the ball. The proof needs an $\varepsilon$-independent ultimate bound obtained by a sublevel-set argument, and this step is not posed as a milestone. Third, $\varphi_i$ is only Lipschitz, so the extended state is only locally Lipschitz in time. The comparison arguments for $\sqrt{V_1}$ and $\sqrt{V_2}$ must work almost everywhere, and $\sqrt V$ is not differentiable where $V=0$.

Formalization scope

Indices are 0-based (Fin (n i), Fin (n i + 1), with the page's $n_i+1$ at Fin.last). All vectors live in EuclideanSpace, so every norm is Euclidean, as in the factor $\sqrt m$ of (3.1). Solutions are trajectories with one-sided derivatives within $[0,\infty)$ (HasDerivWithinAt … (Set.Ici 0)), and the theorem quantifies over every solution with a free initial value. The time derivative $\bar\Delta_i$ is never a Lean deriv: milestones about it hold "for every derivative, wherever one exists". Minima and maxima over subsystems are Finset.inf'/sup' over the nonempty Fin m.

The goal is not trivial. $\Gamma_1,\Gamma_2$ are chosen before $\varepsilon$, the solution and the signals, and no boundedness of the solution is assumed. A proved sanity check exhibits data satisfying every hypothesis together with a solution of the closed loop.

The definitions layer holds the data structure, Assumptions A2 and A3, the hypothesis bundle, the closed loop, the error coordinates and the constants $\Xi^i,\Pi_1,\dots,\Pi_4,\lambda$. Reusable beyond this mission: comparison lemmas for $\sqrt V$ under $\dot V\le-aV+b\sqrt V$ almost everywhere, and a Lipschitz chain rule bound for derivatives of $\varphi\circ y$. Proofs of any milestone, of the missing ultimate-boundedness step and of the goal are welcome.

Selected references

• B.-Z. Guo, Z.-L. Zhao, On convergence of the nonlinear active disturbance rejection control for MIMO systems, SIAM J. Control Optim. 51(2) (2013) 1727–1757. https://doi.org/10.1137/110856824
• B.-Z. Guo, Z.-L. Zhao, On the convergence of an extended state observer for nonlinear systems with uncertainty, Systems Control Lett. 60 (2011) 420–430. https://doi.org/10.1016/j.sysconle.2011.03.008
• B.-Z. Guo, Z.-L. Zhao, On convergence of nonlinear active disturbance rejection for SISO systems, Proceedings of the 24th Chinese Control and Decision Conference, IEEE, 2012, pp. 3507–3512 (no stable link known; reference [9] of the main paper).
• J. Han, From PID to active disturbance rejection control, IEEE Trans. Ind. Electron. 56(3) (2009) 900–906. https://doi.org/10.1109/TIE.2008.2011621

Why quick response can raise waste

Overproduction is a central environmental problem of the fashion industry: garments and fabric that do not sell, called deadstock, are commonly incinerated or sent to landfill, and most of a garment's footprint comes from making the fabric. Quick response, in which finished goods are produced after demand is observed, is widely promoted as a remedy because it reduces excess production of finished goods. Long and Gui ask what quick response does upstream, to the amount of fabric a firm buys. Their first main finding is that a firm with quick response holds fewer leftover finished goods but more leftover fabric, and that total deadstock goes up. The operational value of quick response is studied by Fisher and Raman (1996) and Cachon and Swinney (2011), among others; the question here is its environmental side.

Setting

A firm sells one product at a fixed price $p_f$. The market size $Y$ is random with cdf $F$ on support $[a,b]$, and a realization $y$ gives demand $D_f(y)=(1-p_f)y$. Fabric costs $c_m$ per unit, regular production costs $c$ per unit, and $c+c_m<p_f<1$. One unit of product uses one unit of fabric.

In the benchmark model the firm chooses fabric $x$ and production $q$ with $0\le q\le x$ before $Y$ is known, and earns

$$\mathbb E\Pi^B(x,q)=p_f\,\mathbb E\min\{D_f(Y),q\}-c_mx-cq.$$

In the quick response model the firm may also produce from leftover fabric after seeing $y$, at the higher unit cost $c+\delta$ with $\delta>0$. Its stage-2 rule is $q^Q_\delta(x,q,y)=\min\{(D_f(y)-q)^+,x-q\}$ if $p_f-(c+\delta)>0$, and $0$ otherwise, and it earns

$$\mathbb E\Pi^Q(x,q)=p_f\,\mathbb E\min\{D_f(Y),q+q^Q_\delta(x,q,Y)\}-c_mx-cq-(c+\delta)\,\mathbb E\,q^Q_\delta(x,q,Y).$$

Optimal decisions $(x^B,q^B)$ and $(x^Q,q^Q)$ are the maximizers of these profits. Deadstock finished goods are $\Theta^j_l=\mathbb E[(q^j-D_f(Y))^+]$ in model $j$. Deadstock fabric is $\Theta^Q_m=\mathbb E[(x^Q-q^Q-q^Q_\delta)^+]$ with quick response, and $\Theta^B_m=0$ in the benchmark model, where all fabric is used.

Formalization targets

Goal: Proposition 2

For every $\delta>0$,

$$\Theta^Q_l\le\Theta^B_l,\qquad\Theta^Q_m\ge\Theta^B_m,\qquad\Theta^Q_m+\Theta^Q_l\ge\Theta^B_m+\Theta^B_l,$$

and as $\delta$ decreases, $\Theta^Q_l$ decreases while $\Theta^Q_m$ and $\Theta^Q_m+\Theta^Q_l$ increase. The goal is stated for every admissible law of $Y$ and asserts that optimal decisions exist.

Milestones

1. The stage-2 rule $q^Q_\delta$ is an optimal stage-2 production decision (§3.1, p.10).
2. The benchmark optimum: $F\bigl(q^B/(1-p_f)\bigr)=1-(c_m+c)/p_f$ and $x^B=q^B$ (§3.1, p.10).
3. Lemma 1: with the threshold $\bar\delta^Q=\bigl(\tfrac{p_f}{c_m+c}-1\bigr)c$, below it the optimal decisions are given by two critical fractiles, with $q^Q<x^Q$ and positive expected stage-2 production; at or above it they coincide with the benchmark solution and stage-2 production is zero.
4. Proposition 1: $x^Q\ge x^B$ and $q^Q\le q^B$, and as $\delta$ decreases, $x^Q$ increases and $q^Q$ decreases.

Significance

The result separates two effects that public discussion merges: quick response reduces waste at the finished-goods stage and increases it at the fabric stage, and the second effect dominates. The paper builds on this in its life cycle analysis and in its study of upcycling and of waste-reduction policy. A policy maker who counts only leftover garments would reach the opposite conclusion.

The result is proved in the paper; no machine-checked proof is known, and a search of this platform found neither this statement nor its model. Formalizing it adds a two-stage newsvendor with a raw-material stage and recourse production, over a general continuous demand law, with exact comparative statics in the recourse cost. The platform's existing newsvendor results concern other models.

Difficulty

The natural first argument is that quick response matches supply to demand, so every kind of leftover should fall. It fails because the firm's fabric order is itself a decision, and the option to produce later raises the value of holding fabric. A comparison of the two models therefore has to compare optimizers of two different problems, across a regime change at $\bar\delta^Q$.

Three obstacles are specific to formalization. The problem is a constrained two-variable maximization whose constraint $q\le x$ binds in one regime and is slack in the other, and the case $p_f\le c+\delta$ changes the objective itself. The law of $Y$ is assumed to have no atoms but need not have a density, whereas the paper's proofs differentiate integrals against $dF$. Strictness and uniqueness rest on the support condition and do not hold for a general cdf.

Formalization scope

The law of $Y$ is a probability measure $\mu$ on $\mathbb R$, with $F$ the Mathlib cdf μ. The paper's phrase "on support $[a,b]$" is read as: $0\le a<b$, $\mu$ is carried by $[a,b]$, $\mu$ charges every open subinterval of $[a,b]$, and $\mu$ has no atoms. Continuity of $F$ is needed for the fractile equations to have solutions. The parameter structure also records $p_f<1$, $c_m>0$ and $c\ge0$, which the model implies.

Decisions range over $\{0\le q\le x\}$. Optimal decisions are maximizers of the expected profits and are never defined by critical-fractile formulas, which would make most targets arithmetic. The benchmark fabric deadstock is defined as the unused fabric $(x-q)^+$ at a decision, so $\Theta^B_m=0$ at the optimum is a consequence. Statements hold for every optimal pair; existence is asserted separately, so they are not vacuous.

"Decreases" and "increases" in $\delta$ are weak over all $\delta>0$, because the quantities are constant on $[\bar\delta^Q,\infty)$. The targets add strictness for $\delta_1<\delta_2$ with $\delta_1<\bar\delta^Q$, which is what the paper's proof shows.

A complete development needs a newsvendor library for a general law on a bounded interval: properties of $t\mapsto\mathbb E\min\{D,t\}$ and $t\mapsto\mathbb E(t-D)^+$, and quantiles of a continuous cdf. That library is reusable beyond this mission. Contributions of such general lemmas are welcome, as are proofs of the milestones in any order.

Selected references

• X. Long, L. Gui, Waste Not Want Not? The Environmental Implications of Quick Response and Upcycling, Manufacturing & Service Operations Management, 2023. Statements are cited from the SSRN copy of 2023-08-10. https://doi.org/10.1287/msom.2022.0040, https://ssrn.com/abstract=4013877
• G. P. Cachon, R. Swinney, The value of fast fashion: Quick response, enhanced design, and strategic consumer behavior, Management Science 57(4):778–795, 2011. https://doi.org/10.1287/mnsc.1100.1303
• M. Fisher, A. Raman, Reducing the cost of demand uncertainty through accurate response to early sales, Operations Research 44(1):87–99, 1996. https://doi.org/10.1287/opre.44.1.87

Motivation

Fresh produce is perishable, and its demand depends on how fresh it is. A grocery retailer that orders strawberries before demand is realized does not, in a traditional supply chain, know how long ago the batch was harvested or how it was stored, so the freshness of what she sells is itself a source of demand uncertainty. Blockchain-based traceability systems, such as the food traceability platform that Walmart and IBM launched on Hyperledger Fabric, record that upstream information and make it visible to the retailer before she orders. Keskin, Li and Song (Management Science, 2024) ask how much such freshness transparency is worth to the retailer, and answer it in closed form in a newsvendor model with normally distributed freshness and demand shocks. Their Theorem 1 is the paper's headline profit result; the later sections (food waste, smart contracts, pricing, dual sourcing) build on the same model.

Setting

A retailer sells a perishable product over one period. She orders $q$ units at the unit wholesale price $w > 0$, sells at the unit retail price $p > w$, loses unmet demand, and salvages each leftover unit at the unit salvage value $s < w$ (possibly zero or negative). With demand $d$ her profit is

$$\pi(q,d) = p\min\{q,d\} + s\,(q-d)^+ - w\,q .$$

Demand depends on the freshness state $X$ of the batch:

$$D = \lambda + \beta X + \varepsilon, \qquad X \sim N(\mu_X, \sigma_X^2),\quad \varepsilon \sim N(0, \sigma^2),$$

with $X$ and the demand shock $\varepsilon$ independent, baseline demand $\lambda > 0$ and freshness sensitivity $\beta > 0$. Write $\varphi$ and $\Phi$ for the standard normal density and distribution function, $r = (p-w)/(p-s) \in (0,1)$ for the critical ratio, $z^* = \Phi^{-1}(r)$ for the safety factor, and $\sigma_D = \sqrt{\beta^2\sigma_X^2 + \sigma^2}$ for the standard deviation of $D$.

The blockchain retailer observes $X = x$ before ordering. She maximizes $G_x(q) = \mathbb E[\pi(q, \lambda + \beta x + \varepsilon)]$ and earns $\Pi^*(x) = \sup_q G_x(q)$; her expected profit is $\mathbb E_X[\Pi^*(X)]$. The traditional retailer knows only the distribution of $X$; she maximizes $G(q) = \mathbb E[\pi(q, D)]$ and earns $\Pi^*_o = \sup_q G(q)$.

Formalization targets

Goal: Theorem 1

$$\mathbb E_X[\Pi^*(X)] = (p-w)(\lambda+\beta\mu_X) - (p-s)\,\sigma\,\varphi(z^*), \qquad \Pi^*_o = (p-w)(\lambda+\beta\mu_X) - (p-s)\,\sigma_D\,\varphi(z^*),$$ $$V := \mathbb E_X[\Pi^*(X)] - \Pi^*_o = (p-s)(\sigma_D - \sigma)\,\varphi(z^*) > 0 .$$

All four clauses are part of the goal, for every admissible parameter tuple.

Milestones

1. Lemma EC.1: the three partial expectations $\mathbb E[\min\{Y,t\}]$, $\mathbb E[Y\mathbb 1_{\{Y\le t\}}]$, $\mathbb E[Y\mathbb 1_{\{Y>t\}}]$ of $Y \sim N(\mu,\sigma^2)$ in terms of $\varphi$ and $\Phi$.
2. Eq. (2): $q^*(x) = F^{-1}_{D_x}(r) = \lambda + \beta x + \sigma z^*$ is the unique maximizer of $G_x$.
3. Expected sales, Case 1: $\mathbb E[\min\{D_x, q^*(x)\}] = \lambda + \beta x + \sigma[(1-r)z^* - \varphi(z^*)]$.
4. Eq. (3): $\Pi^*(x) = (p-w)(\lambda+\beta x) - (p-s)\sigma\varphi(z^*)$, attained.
5. Case 1 closed: $\mathbb E_X[\Pi^*(X)] = (p-w)(\lambda+\beta\mu_X) - (p-s)\sigma\varphi(z^*)$.
6. Compound demand: $D \sim N(\lambda + \beta\mu_X, \beta^2\sigma_X^2 + \sigma^2)$.
7. Eq. (4): $q^*_o = F^{-1}_D(r) = \lambda + \beta\mu_X + \sigma_D z^*$ is the unique maximizer of $G$.
8. Expected sales, Case 2: $\mathbb E[\min\{D, q^*_o\}] = \lambda + \beta\mu_X + \sigma_D[(1-r)z^* - \varphi(z^*)]$.
9. Case 2 closed: $\Pi^*_o = (p-w)(\lambda+\beta\mu_X) - (p-s)\sigma_D\varphi(z^*)$, attained.

Significance

Theorem 1 turns the value of information into a single formula. The profit gain from transparency is proportional to the reduction $\sigma_D - \sigma$ in the standard deviation of the demand the retailer plans against, scaled by the overage–underage cost $(p - s)$ and by $\varphi(z^*)$. It is strictly positive for every parameter tuple, and its comparative statics (Proposition 1: increasing in $\sigma_X$ and $\beta$, decreasing in $\sigma$) follow by differentiation. The expected-sales computations of its proof are reused verbatim in the proof of the paper's food-waste result (Theorem 2, p.ec12), so a formal version of Theorem 1 and its milestones is the base for the rest of §2.

The result is proved in the paper; nothing here is open. To the best of current knowledge none of these statements has a machine-checked proof. The mission produces: a formal newsvendor profit with salvage and real-valued orders; the normal partial-expectation identities of Lemma EC.1, which recur throughout inventory theory; a formal proof that the critical-fractile order is the unique optimum for normal demand; and the closed-form value of freshness transparency.

Difficulty

The computation in the paper is short, but it rests on facts that are routine on paper and not available as such in Lean. The newsvendor optimality step is a first-order condition for an expected profit whose integrand is not differentiable in $q$, and uniqueness of the optimum depends on the normal distribution function being strictly increasing. Lemma EC.1 is an improper integral of $y$ against the Gaussian density, which Mathlib provides only as a measure and a density, not as these partial expectations. Case 2 needs the law of $\lambda + \beta X + \varepsilon$, which combines affine images of Gaussians with the convolution of independent Gaussians. Case 1 then needs $\Pi^*(X)$ to be integrable, which holds only because $\Pi^*(x)$ is affine in $x$; the supremum in the definition must first be shown to be attained, or the integral is of an unknown function. A first idea, applying a generic "newsvendor critical fractile" lemma, does not apply verbatim: the order quantity ranges over all of $\mathbb R$ and the salvage value may be negative.

Formalization scope

Lean namespace BlockchainNV. The parameters and their standing inequalities form a structure Params ($w>0$, $p>w$, $s<w$, $\lambda>0$, $\beta>0$, $\sigma_X>0$, $\sigma>0$). The random model IsModel places $X$ and $\varepsilon$ on an arbitrary measurable space $(\Omega, P)$ with HasLaw X (gaussianReal μX (σX^2).toNNReal) P, HasLaw ε (gaussianReal 0 (σ^2).toNNReal) P and IndepFun X ε P; Mathlib's Gaussian takes the variance. $\varphi$ is gaussianPDFReal 0 1 and $\Phi$ is cdf (gaussianReal 0 1). The safety factor $z^*$ is a real z with the hypothesis $\Phi(z) = (p-w)/(p-s)$, which determines it. $\Pi^*(x)$ and $\Pi^*_o$ are sSup of the expected profit over all $q \in \mathbb R$; milestones 4 and 9 assert that the suprema are attained maxima, so the sSup is not Lean's junk value. $\mathbb E_X[\Pi^*(X)]$ is the Bochner integral $\int \Pi^*(X\,\omega)\,dP$. The order quantity and the demand are unrestricted reals, as in the paper's base model: restricting $q \ge 0$ would change $\Pi^*(x)$ for small $x$ and falsify the first clause.

The positivity of $\sigma_X$ and $\sigma$ is not optional: with $\sigma_X = 0$ the Gaussian becomes a Dirac mass and $V = 0$. Clause 3 follows from clauses 1–2 by algebra and clause 4 from $\sigma_D > \sigma$; the content of the goal is in clauses 1 and 2.

Infrastructure that a complete development needs and that is reusable beyond this mission: the normal partial expectations, the first-order optimality of the newsvendor with general salvage value, and the law of an affine combination of independent Gaussians. Contributions of any of these as standalone lemmas are welcome.

Selected references

• N. Bora Keskin, Chenghuai Li, Jing-Sheng Song, The Blockchain Newsvendor: Value of Freshness Transparency and Smart Contracts, Management Science, 2024. https://doi.org/10.1287/mnsc.2021.02949
• Nicholas C. Petruzzi, Maqbool Dada, Pricing and the Newsvendor Problem: A Review with Extensions, Operations Research 47(2), 1999. https://doi.org/10.1287/opre.47.2.183
• Yan Qin, Ruoxuan Wang, Asoo J. Vakharia, Yuwen Chen, Michelle M. H. Seref, The Newsvendor Problem: Review and Directions for Future Research, European Journal of Operational Research 213(2), 2011. https://doi.org/10.1016/j.ejor.2010.11.024