All missions

Motivation

In a two-tier supply chain a retailer orders from a supplier, and the supplier must forecast those orders. If the retailer shares its demand data, the supplier forecasts with full information. If not, the supplier sees only the order stream. A large literature (Lee, So and Tang 2000; Gavirneni, Kapuscinski and Tayur 1999; Giloni, Hurvich and Seshadri 2014) asks when sharing has value and how large that value is. Caldentey, Giloni, Hurvich and Zhang (SSRN 4319721, version of January 20, 2024; published in Mathematics of Operations Research, 2024) answer this for an i.i.d. Gaussian demand and arbitrary linear ordering policies. They compute the entire efficient frontier between the retailer's inventory variance and the supplier's forecast error, both with and without sharing.

Timeline of the problem as the paper presents it:

• Gavirneni et al. (1999) and Lee et al. (2000) show that sharing can lower supply chain costs for specific ordering rules (order-up-to, AR(1) demand).
• Giloni et al. (2014) use what are, in effect, Blaschke products to construct the supplier's full-information shocks when the orders are not invertible.
• Caldentey et al. (2021) solve the full-sharing frontier under stronger conditions and propose only a finite-dimensional heuristic for the no-sharing case.
• The present paper solves the no-sharing frontier exactly, via the Smirnov–Beurling factorization in the Hardy space $H^2$.

Setting

Demand is $D_t=d+\epsilon_t$, where $(\epsilon_t)$ is Gaussian white noise with variance $\sigma_\epsilon^2>0$. The retailer orders $O_t=d+\sum_{n\ge0}\tilde\psi_n\epsilon_{t-n}$. The policy $\tilde\psi$ is a real sequence in the set

$$\tilde\Psi=\Bigl\{\tilde\psi:\ \sum_n\tilde\psi_n=1,\ \sum_n\tilde\psi_n^2<\infty,\ \sum_{n\ge1}\Bigl(\sum_{k<n}\tilde\psi_k-1\Bigr)^2<\infty\Bigr\}.$$

Its z-transform is $\tilde\psi(z)=\sum_n\tilde\psi_nz^n$ on the unit disk. The boundary value $\tilde\psi(e^{-i\lambda})$ is the radial limit $\lim_{r\uparrow1}\tilde\psi(re^{-i\lambda})$.

• The retailer's inventory variance is $\sigma_I^2(\tilde\psi)=\sigma_\epsilon^2\bigl(1+\sum_{n\ge1}(\sum_{k<n}\tilde\psi_k-1)^2\bigr)$.
• With sharing, the supplier's one-step forecast error is $\sigma^2_{S|FI}=\sigma_\epsilon^2\tilde\psi_0^2$.
• Without sharing, it is Kolmogorov's expression $\sigma^2_{S|NS}=\sigma_\epsilon^2\exp\bigl(\frac1{2\pi}\int_{-\pi}^{\pi}\log|\tilde\psi(e^{-i\lambda})|^2d\lambda\bigr)$.

Let $\Theta(z)=\frac1{2\pi}\int\frac{e^{i\lambda}+z}{e^{i\lambda}-z}\log|\tilde\psi(e^{-i\lambda})|\,d\lambda$, with Taylor coefficients $\theta_n$. Assumption 2 requires $(\theta_n)\in\ell^2$.

The two efficient frontiers are the infima

$$\Sigma^2_{FI}(\sigma)=\inf\{\sigma_I^2(\tilde\psi):\tilde\psi\in\tilde\Psi,\ \sigma^2_{S|FI}(\tilde\psi)\le\sigma^2\},$$ $$\Sigma^2_{NS}(\sigma)=\inf\{\sigma_I^2(\tilde\psi):\tilde\psi\in\tilde\Psi\ \text{with Assumption 2},\ \sigma^2_{S|NS}(\tilde\psi)\le\sigma^2\}.$$

Formalization targets

Goal: Theorem 2 (p.20)

$$\Sigma^2_{NS}(\sigma)=\begin{cases}\dfrac{\sigma_\epsilon^2}{4}\Bigl(5-\log\dfrac{4\sigma^2}{\sigma_\epsilon^2}\Bigr),&0<\sigma<\sigma_\epsilon/2,\\[1mm]\sigma_\epsilon^2+((\sigma_\epsilon-\sigma)^+)^2,&\sigma\ge\sigma_\epsilon/2,\end{cases}$$

for every $\sigma_\epsilon>0$ and $\sigma>0$. The goal is stated on the explicit problem (26). It is not stated through any factorization.

Milestones

1. Theorem 1: $\Sigma^2_{FI}(\sigma)=\sigma_\epsilon^2+((\sigma_\epsilon-\sigma)^+)^2$, with a unique MA(1) minimizer.
2. Lemma 2 (Smirnov–Beurling): $\tilde\psi=Q\cdot B\cdot G$, with $Q$ outer, $B$ a Blaschke product and $G$ singular inner.
3. Proposition 6: $\sigma^2_{S|FI}=(B(0)G(0))^2\sigma^2_{S|NS}\le\sigma^2_{S|NS}$, with equality iff $\tilde\psi$ is outer.
4. Lemma 3: dropping $B$ keeps $\sigma_{S|NS}$ and lowers $\sigma_I$.
5. Proposition 5: $\sigma_I^2=\frac{\sigma_\epsilon^2}{2\pi}\int|\frac{z\tilde\psi(z)-1}{1-z}|^2d\lambda$.
6. Lemma 6: conjugate symmetry of the factors, and $Q(1)=B(1)=G(1)=1$.
7. Lemma 8: the arc integral around a simple pole.
8. §9.7 Step 1: $\sigma_I^2(QG)=S_1(Q)+\int\frac{d\mu}{1-\cos\lambda}\ge S_1(Q)+\mu(\mathbb T)/2$.
9. Lemma 4: under Assumption 2, $\exp\Theta$ is outer.
10. Proposition 4: outer $\iff$ unimodular multiple of the Szegő function $\iff$ invertible orders.
11. Lemma 5: strict convexity of $\tilde C(Q)$ in $(\theta_1,\theta_2,\dots)$.
12. §9.7 Step 2: $\tilde C_Q\ge(5-2\log2\sigma)/4$, attained at $Q^\star=(1+z)/2$.
13. Proposition 3: an explicit family $\tilde\psi_\delta$ whose costs converge to $\Sigma^2_{NS}(\sigma)$.

Significance

Theorem 2 gives the exact price of withholding demand information. For $\sigma\ge\sigma_\epsilon/2$ the two frontiers coincide, so sharing has no value there. For $\sigma<\sigma_\epsilon/2$ the ratio $\Sigma^2_{NS}/\Sigma^2_{FI}$ tends to infinity as $\sigma\downarrow0$. Combined with linear cost weights, this yields the paper's thresholds for when a retailer should share (§7.3). Proposition 6 measures the value of sharing for any single policy: it is the squared modulus of the inner factor at the origin.

The results are proved in the paper. None of them, and none of the Hardy-space theory they use, has a machine-checked proof on the platform. Mathlib has Fourier series on the circle, Parseval's identity and Abel's limit theorem, but no Hardy spaces, outer functions, Blaschke products, singular inner functions or Smirnov–Beurling factorization. A formalization of the goal therefore checks an optimization result whose proof combines time-series modelling, complex analysis and convex optimization. It also leaves reusable Hardy-space infrastructure behind.

Difficulty

The obvious approach optimizes over the coefficients $\tilde\psi_n$ directly. It fails because $\sigma^2_{S|NS}$ is not continuous in $\tilde\psi$ (p.20): Kolmogorov's integral sees only $|\tilde\psi|$ on the circle and ignores the zeros inside the disk. The problem must instead be decomposed by the inner–outer factorization. The inventory variance then depends on the Blaschke and singular factors through a boundary integral with a pole at $z=1$, which the residue theorem does not handle directly (§9.7 Step 1). Finally, the infimum is not attained for $\sigma<\sigma_\epsilon/2$. The limiting policy $\frac{1+z}2\exp(\gamma\frac{z-1}{z+1})$ carries a singular inner factor and violates the forecast constraint. The upper bound therefore needs an approximating family (Proposition 3) and a continuity argument in $\sigma$.

Formalization scope

• Policies are real sequences $\mathbb N\to\mathbb R$.
• "$\sum\tilde\psi_n=1$" is convergence of the partial sums, not absolute summability: $\tilde\psi$ is only square summable.
• Boundary values are radial limits (limUnder along $r\uparrow1$). The integrand of (26) is written $\log|\tilde\psi(e^{-i\lambda})|^2$, which equals $\log(\tilde\psi(e^{-i\lambda})\tilde\psi(e^{i\lambda}))$ for real coefficients.
• $\theta_n$ is the Taylor coefficient $\Theta^{(n)}(0)/n!$.
• Both frontiers are real sInfs of sets of attained values. These sets are nonempty and bounded below by $\sigma_\epsilon^2$. The goal is not a statement about a minimizer.
• $H^2$ is represented by square-summable complex coefficient sequences. "Outer" is Definition 3: the closed span of the shifts is all of $\ell^2$.
• Blaschke products carry the convergence factors $|z_k|/z_k$ and a unimodular constant. Singular inner functions in the factorization have constant 1. This is the normalization under which Lemmas 3 and 6 and Proposition 6 hold as printed.
• The outer factor uses the orientation of (29). The printed (32) is not the outer factor for complex coefficients.
• Proposition 5 restores the factor $\sigma_\epsilon^2$ that (36)–(37) omit.
• Lemma 6 states the limit of $Q$ at $1$ inside Stolz regions. The printed continuity of $Q(e^{i\lambda})$ at $\lambda=0$ fails on the circle, and the paper gives no proof of that clause.

A trivializing encoding would be an empty feasible set, for which sInf ∅ = 0. It is ruled out because the policy $(1,0,0,\dots)$ satisfies Assumption 2 and is feasible for every $\sigma\ge\sigma_\epsilon$.

The infrastructure is reusable well beyond this mission:

• the Hardy space $H^2$ with radial boundary values;
• inner–outer factorization;
• Kolmogorov–Szegő prediction theory;
• the $L^2$ linear past of a stationary process.

Contributions to any of these are welcome, as are self-contained proofs of the milestones (Theorem 1 and Lemma 8 need no Hardy-space theory).

Selected references

• R. Caldentey, A. Giloni, C. Hurvich, Y. Zhang, Information Design and Sharing in Supply Chains, SSRN 4319721 (version of January 20, 2024); Mathematics of Operations Research (2024). https://ssrn.com/abstract=4319721, https://doi.org/10.1287/moor.2023.008
• W. Rudin, Real and Complex Analysis, 3rd ed., McGraw-Hill, 1987 (Theorem 17.17).
• N. Nikolski, Hardy Spaces, Cambridge University Press, 2019 (Theorems 2.6.5, 2.6.7). https://doi.org/10.1017/9781316882108
• P. J. Brockwell, R. A. Davis, Time Series: Theory and Methods, 2nd ed., Springer, 2006. https://doi.org/10.1007/978-1-4419-0320-4
• A. Giloni, C. Hurvich, S. Seshadri, Forecasting and information sharing in supply chains under ARMA demand, IIE Transactions 46(1), 2014. https://doi.org/10.1080/0740817X.2012.689122
• H. L. Lee, K. C. So, C. S. Tang, The value of information sharing in a two-level supply chain, Management Science 46(5), 2000. https://doi.org/10.1287/mnsc.46.5.626.12047

Motivation

Contingent convertible bonds (CoCos) are bank debt that converts into equity when the issuing bank is in distress, so that the bank is recapitalised without a default (Avdjiev, Kartasheva & Bogdanova 2013). A trigger based on the bank's own stock price is transparent and fast, but circular: the stock price depends on whether the debt converts, and whether it converts depends on the stock price. Sundaresan & Wang (2015) observed that with such a trigger neither existence nor uniqueness of an equilibrium stock price is guaranteed, and this concern is cited as the main reason stock price triggers have not been used in practice. For a single bank, Glasserman & Nouri (2016) and Pennacchi & Tchistyi (2019) gave sufficient conditions for existence and uniqueness.

Balter, Schweizer and Vera (arXiv:2011.06474, later in Mathematics of Operations Research, 2023) ask the same question when banks hold each other's CoCos, so that one bank's conversion changes the assets of the others. This mission formalizes their existence theorem for the case where every bank sets a fair or super-fair threshold.

Setting

There are $n$ banks $[n]=\{1,\dots,n\}$. Bank $i$ has assets net of liabilities $a_i$ and convertible debt $c_i$. If its stock price $s_i$ is at most its conversion threshold $l_i$, the debt is not paid back but converted into $m_i>0$ new shares (the original number of shares is $1$). The fraction of bank $j$'s convertible debt held by bank $i$ is $w_{ij}\in[0,1]$, with $w_{ii}=0$ and $\sum_i w_{ij}\le 1$; such a pair $(m,W)$ is called admissible.

Each price vector $s$ determines a partition of the banks into bankrupt $B=\{i:s_i<0\}$, converting $C=\{i:0\le s_i\le l_i\}$ and healthy $H=\{i:s_i>l_i\}$. The pair $(a,s)$ is a $(B,C,H)$-equilibrium when the partition is the one read off $s$ and

$$(1+m_i)s_i=a_i+\sum_{j\in C}w_{ij}m_js_j+\sum_{j\in H}w_{ij}c_j\quad(i\in B\cup C),\qquad s_i=a_i-c_i+\sum_{j\in C}w_{ij}m_js_j+\sum_{j\in H}w_{ij}c_j\quad(i\in H).$$

Writing $v_F$ for $v$ with the entries outside $F$ set to zero, these equations say $a=\Phi(s)$ with

$$\Phi(s)=L_{B,C}\,s+(I-W)c_H,\qquad L_{B,C}=I+\mathrm{Diag}(m_B)+(I-W)\,\mathrm{Diag}(m_C),$$

where $(B,C,H)$ is the partition read off $s$. Thresholds are fair if $l_i=c_i/m_i$, super-fair if $l_i>c_i/m_i$, and sub-fair if $l_i<c_i/m_i$. Assumption 1 is that $I-W$ is invertible.

Formalization targets

Goal: Theorem 1 (p.21)

For every admissible $(m,W)$ with $I-W$ invertible, thresholds $l\ge0$ and credit amounts $c$ with $l_i\ge c_i/m_i$ for all $i$,

$$\Phi \text{ is surjective, and for every } a\in\mathbb R^n \text{ there is } s \text{ with } \Phi(s)=a \text{ and a partition making } (a,s) \text{ an equilibrium}.$$

No constant is fixed; the statement covers every $n$, every network and every fair or super-fair choice of thresholds.

Milestones

1. Lemma 1: each $s$ is an equilibrium for exactly one partition, with $a=\Phi(s)$.
2. §2, pp.11–12: every $L_{B,C}$ is strictly diagonally dominant and invertible.
3. Theorem 2 (Poincaré–Miranda) and Proposition 2, a multivariate intermediate value theorem.
4. Propositions 3 and 4: in the fair case $\Phi$ is continuous and bijective.
5. §3.3, p.19: $\hat\Phi(s)=\Phi(s)-(I-W)d_{H(\Phi(s))}$, the super-fair map as a shifted fair map, where $H(a)$ is the set of banks healthy at $a$ in the fair case and $d=c^{\mathrm{fair}}-\hat c\ge0$.
6. Lemma 5: sign patterns of $(I-W)^{-1}$ and $L_{B,C}^{-1}(I-W)$.
7. Lemmas 3, 4, Corollary 1, Lemma 2: properties of the set map $h(X)=H(\hat a+(I-W)d_X)$, ending in a fixed point $h(X)=X$.

Significance

The result. With interbank holdings, the map from prices to assets is piecewise affine with $3^n$ pieces, and the paper shows that existence of equilibrium is decided by the thresholds alone: with sub-fair thresholds there are asset vectors with no equilibrium at all (Proposition 1, not part of this mission), while with fair or super-fair thresholds an equilibrium always exists, although it may not be unique. For a regulator this is a design rule: a CoCo with a stock price trigger set below the fair level can leave the market without any consistent price. The fair case is also formally close to the Eisenberg–Noe clearing model, so tools transfer between the two.

Formalizing it. The result is proved in the paper; none of it is machine-checked. A formal proof gives a verified existence theorem for a nonsmooth, discontinuous equilibrium map, a Lean statement of the Poincaré–Miranda theorem on $[-1,1]^n$, and sign results for inverse M-matrices of the kind that recur in network and Leontief models.

Difficulty

In the fair case $\Phi$ is continuous, monotone in the right directions and tends to $\pm\infty$ along the diagonal, so a Poincaré–Miranda argument gives surjectivity. In the super-fair case ($l_i>c_i/m_i$ for some $i$) this route fails: the map jumps by $-(m_il_i-c_i)(I-W)e_i$ when bank $i$'s price crosses its threshold upwards, so it is neither continuous nor injective, and degree or fixed-point arguments do not apply directly. The paper instead views the super-fair map $\hat\Phi$ as the fair map shifted by vectors depending on which banks are healthy, and reduces existence to a fixed point of a set map $h$ on subsets of banks. That $h$ is not monotone, so Tarski's theorem does not apply. Its iterates only oscillate between bounds that tighten, and the proof that the oscillation stops rests on Lemmas 3 and 4. These in turn need the inverse of the fair map along a segment, its piecewise-linear structure, and the sign pattern of $L_{B,C}^{-1}(I-W)$.

Formalization scope

Banks are Fin n; vectors are Fin n → ℝ; W : Matrix (Fin n) (Fin n) ℝ with W i j $=w_{ij}$ (holder $i$, issuer $j$), so the admissibility condition bounds column sums. $v_F$ is restrictTo F v. The partition is read off $s$ with strict inequalities for bankrupt and healthy and closed bounds for converting. Phi m W l c is $\Phi$ for credit amounts c: the fair map is Phi m W l (m * l), the super-fair map is Phi m W l c with c i / m i ≤ l i. $H(a)$ is Hfair, built from Function.invFun of the fair map. It is meaningful because that map is bijective (Proposition 4), and every statement using it assumes an admissible network and 0 ≤ l. Assumption 1 is IsUnit (1 - W).

All statements assume $l\ge0$. The paper uses this tacitly when it states that the price regions partition $\mathbb R^n$; without it the regions overlap and the fair map is discontinuous. Credit amounts in the goal and in Lemma 1 may have any sign. Lemma 5(b) and the diagonal-dominance milestone are stated for arbitrary, possibly overlapping $B$, $C$. Assumption 1 is carried by Lemmas 2, 4, 5(a), Corollary 1 and Theorem 1. The paper imposes it throughout its §3.3, but Lemma 3, the p.19 identity and Lemma 5(b) are stated here without it, which is more general; their proofs do not use it. The goal cannot be satisfied trivially: the admissibility hypotheses are satisfied by concrete networks, and both conclusions are nontrivial for $n=1$ with super-fair thresholds, where $\hat\Phi$ is discontinuous.

A complete development needs Poincaré–Miranda (from Brouwer's theorem on the cube, which is proved on the platform as Plasticity.Ext.Brouwer), continuity and invertibility of piecewise-affine maps, and M-matrix sign results. The Poincaré–Miranda theorem and Proposition 2 are reusable beyond this mission. Proofs of any milestone, and alternative routes to Lemma 2 such as a direct combinatorial argument on $h$, are welcome.

Selected references

• A. G. Balter, N. Schweizer, J. C. Vera, Contingent Capital with Stock Price Triggers in Interbank Networks, arXiv:2011.06474v1, 2020; Mathematics of Operations Research, 2023. https://arxiv.org/abs/2011.06474
• S. Sundaresan, Z. Wang, On the Design of Contingent Capital with a Market Trigger, Journal of Finance 70(2), 2015. https://doi.org/10.1111/jofi.12134
• P. Glasserman, B. Nouri, Market-Triggered Changes in Capital Structure: Equilibrium Price Dynamics, Econometrica 84(6), 2016. https://doi.org/10.3982/ECTA11113
• F. E. Browder, Fixed point theory and nonlinear problems, Bulletin of the AMS 9(1), 1983. https://doi.org/10.1090/S0273-0979-1983-15153-4
• L. Eisenberg, T. H. Noe, Systemic Risk in Financial Systems, Management Science 47(2), 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
• S. Avdjiev, A. Kartasheva, B. Bogdanova, CoCos: a primer, BIS Quarterly Review, September 2013. https://www.bis.org/publ/qtrpdf/r_qt1309f.htm

Motivation

A clutter is a family of subsets of a finite ground set none of which contains another. A clutter is ideal if its set covering polyhedron $\{x\ge 0 : \sum_{i\in C}x_i\ge 1 \text{ for every member } C\}$ has only integral vertices. It packs if the largest number of pairwise disjoint members equals the smallest number of elements meeting every member. Ideal clutters and clutters with the packing property are central objects in combinatorial optimization. The Replication Conjecture of Conforti and Cornuéjols (1993) and the question of which ideal clutters are minimally non-packing are both long open in general.

Abdi, Cornuéjols, Guričanová and Lee (Cuboids, a class of clutters) attached to every set $S\subseteq\{0,1\}^n$ a clutter, its cuboid, and translated idealness and packing of cuboids into geometric properties of $S$. The paper formalized in this mission, Resistant sets in the unit hypercube (LSE Research Online 102397, accepted manuscript of October 28, 2019; published in Math. Oper. Res. 46(1), 2021), studies one large class of such sets, the resistant sets. Their cuboids are ideal. The paper proves the Replication Conjecture for these cuboids and classifies the resistant sets whose cuboids are ideal minimally non-packing and have the largest possible number of members.

In the cuboids paper, 745 strictly non-polar sets of dimension at most 7 were enumerated, 74 of them half-dense. The infinite family $R_{k,1}$ and the sporadic set $R_5$ stood out among them. Theorem 1.17 of the paper shows that, among resistant sets, these are the only half-dense examples.

Setting

A point of the cube $\{0,1\}^n$ is a string $x=x_1\cdots x_n$, and $x\triangle y$ is coordinate-wise addition modulo 2. Fix $S\subseteq\{0,1\}^n$. Its points are feasible and the other points infeasible. Twisting $S$ by a point $x$ gives $S\triangle x=\{y\triangle x : y\in S\}$. A minimal point of a set is a point of inclusion-minimal support.

• Resistant. $S$ is resistant if, for every point $x$, the minimal points of $S\triangle x$ have pairwise disjoint supports. Equivalently, every induced clutter $\operatorname{ind}(S\triangle x)$ has pairwise disjoint members.
• Restriction. A restriction of $S$ fixes some coordinates to values and keeps the points of $S$ that agree with them, dropping the fixed coordinates. A restriction is proper if it fixes at least one coordinate and leaves at least one free.
• Isomorphism. Two sets are isomorphic if one is obtained from the other by twisting and relabeling coordinates. "$S$ has a $T$ restriction" means that some restriction of $S$ is isomorphic to $T$.
• Polar. Two points are antipodal if they differ in every coordinate. $S$ is polar if it contains two antipodal points or all its points agree on some coordinate. It is strictly non-polar if it is not polar but every proper restriction is polar.
• Half-dense. A non-polar set has at most $2^{n-1}$ points. It is half-dense if it has exactly $2^{n-1}$.

The sets of the classification use the reflective product $S_1\ast S_2=(S_1\times S_2)\cup(\overline{S_1}\times\overline{S_2})$:

$$R_{k,1}=\{\mathbf 0^{k+1},\mathbf 1^{k+1}\}\ast\{0\}\subseteq\{0,1\}^{k+2}\ (k\ge 1),\qquad R_5=R\ast\{0\}\subseteq\{0,1\}^5,$$

where $R=\{1000,1100,1110,1111,0111,0011,0001,0000\}$. For example $R_{1,1}=\{000,110,101,011\}$.

In the Lean development a point is Fin n → Bool, a set is a Finset (Fin n → Bool), and the predicates are IsResistant, IsPolar, IsStrictlyNonPolar, IsHalfDense, IsIso and HasRestriction; the sets are Rk1 k and R5.

Formalization targets

Goal: Theorem 1.17

For every $n\ge 1$ and every $S\subseteq\{0,1\}^n$,

$$S \text{ half-dense, strictly non-polar and resistant}\iff S\cong R_{k,1}\text{ for some }k\ge1\ \text{ or }\ S\cong R_5 .$$

The paper states this as "$\{R_{k,1}:k\ge1\}\cup\{R_5\}$ are, up to isomorphism, the only half-dense strictly non-polar sets that are resistant". Both directions are part of the goal.

Milestones

1. Remark 3.2: minors of resistant sets are resistant.
2. Theorem 1.8: $S$ is resistant iff it has no fragile restriction and no $\{\mathbf 0^k,\mathbf 1^k-e_1\}$ ($k\ge4$) restriction, iff it has no fragile minor.
3. The three propagation lemmas: Plane Propagation (Lemma 4.6), Sight Propagation (Lemma 4.8) and Path Propagation (Lemma 4.10).
4. The straight-circuit analysis of §5:
   • Lemma 5.1;
   • Lemma 5.2;
   • Proposition 5.3;
   • Lemma 5.4;
   • Theorem 5.5, which says that a straight infeasible circuit of length $2(n-1)$ in $\{x_n=0\}$ whose lift by $e_n$ is feasible forces an $R_{k,1}$ ($k\le n-2$) or $R_5$ restriction.
5. Proposition 6.1 and Theorem 6.2: a resistant non-polar set all of whose straight infeasible paths have length at most $n-1$ has an $R_{k,1}$ or $R_5$ restriction.
6. Remark 2.8, and the facts quoted from the cuboids paper: $R_{k,1}$ and $R_5$ are resistant, half-dense and strictly non-polar.

Significance

Theorem 1.17 answers Question 7.4 of the cuboids paper for cuboids of resistant sets. By Theorem 1.15 of the paper, a resistant set is strictly non-polar exactly when its cuboid is an ideal minimally non-packing clutter. So the theorem lists every ideal minimally non-packing cuboid of a resistant set that has the maximum number of members. The paper also uses it to decide when a reflective product $S_1\ast S_2$ of resistant sets is strictly polar (Theorem 1.18).

The intermediate results are reusable on their own:

• Theorem 1.8 is an excluded-restriction characterization of resistance.
• The propagation lemmas describe how feasibility spreads in any resistant set.
• Theorem 6.2 is a general structure theorem for resistant non-polar sets.

The paper's proofs are complete and refereed. No part of them has a machine-checked proof that this mission knows of. The mission asks for proofs of the published statements, not for new results.

Difficulty

The "if" direction is a finite statement for each $k$. It is uniform in $k$, however, and strict non-polarity of $R_{k,1}$ quantifies over every proper restriction of a cube of dimension $k+2$. So it cannot be settled by enumeration.

In the "only if" direction, half-density and non-polarity bound the straight infeasible paths. The difficulty is to turn that local information into a global description of $S$. The obvious approach, induction on $n$ through restrictions, does not work directly: strict non-polarity is not inherited by restrictions, and resistance alone allows many configurations. The paper instead fixes a longest straight infeasible path, closes it into a circuit of length $2(n-1)$ by Path Propagation, and analyses the feasible points next to the circuit coordinate by coordinate. The rerouting argument of Lemma 5.2 and the five-case induction of Lemma 5.4 are long case analyses on 3- and 4-dimensional subcubes, and they are the bulk of the work.

Formalization scope

Conventions:

• A point is Fin n → Bool with false for $0$. The paper's coordinate $i$ is the index $i-1$, and coordinate $n$ is lastCoord n _.
• A set is a Finset. Half-density is written $2|S|=2^n$.
• Resistance is defined through inclusion-minimal points of every twist, not through cardinality.
• A restriction is given in one step by an injection ι : Fin m ↪ Fin n of kept coordinates and the values of the others. The kept dimension satisfies $m\ge1$, and a proper restriction has $m<n$. The restriction that fixes nothing (the set itself) counts, as in the paper.
• Isomorphism is relabeling (a bijection of coordinates) followed by twisting, never complementation, and it forces equal dimension.
• A hypercube may be empty.
• Straight paths and straight circuits are given by a start point and a sequence of distinct coordinates (Remark 4.2 and the definition on p.22).

Allowing $0$-dimensional restrictions would trivialize the goal: the empty set in dimension $0$ is non-polar, so no set with an infeasible point would be strictly non-polar. The dimension bound $m\ge1$ rules this out.

Everything is built on Mathlib's Finset and finite function types; no external library is needed. The definitions (twisting, restrictions, minors, isomorphism, polarity) are reusable for other results of the cuboids paper and of this paper, such as Theorems 1.13–1.15 and 1.18. Contributions are welcome at every level: proofs of the milestones, decidability instances and lemmas that reduce small-dimensional cases to computation, and lemmas on twisting and restriction that the proofs use repeatedly.

Selected references

• A. Abdi, G. Cornuéjols, D. Lee, Resistant sets in the unit hypercube, accepted manuscript (Oct. 28, 2019), LSE Research Online 102397. https://eprints.lse.ac.uk/102397/ — published in Mathematics of Operations Research 46(1), 2021. https://doi.org/10.1287/moor.2019.1048
• A. Abdi, G. Cornuéjols, N. Guričanová, D. Lee, Cuboids, a class of clutters, Journal of Combinatorial Theory, Series B (2019). https://doi.org/10.1016/j.jctb.2019.10.002
• M. Conforti, G. Cornuéjols, Clutters that pack and the max-flow min-cut property: a conjecture, The Fourth Bellairs Workshop on Combinatorial Optimization, 1993 (cited as [9] in the paper; no online copy).
• G. Cornuéjols, Combinatorial Optimization: Packing and Covering, CBMS-NSF Regional Conference Series in Applied Mathematics 74, SIAM, 2001. https://doi.org/10.1137/1.9780898717105

Motivation

Ride-sharing platforms match passengers who request rides at different times and places. Three features of that problem are hard to separate: two passengers far apart yield a poor match, two requests far apart in time cannot be matched at all, and the platform does not know future demand. Ashlagi, Burq, Dutta, Jaillet, Saberi and Sholley (arXiv:1808.03526v1, published in Mathematics of Operations Research, 2023, as Edge-Weighted Online Windowed Matching) reduce these features to a graph matching problem on an arbitrary, not necessarily bipartite, graph.

The classical online bipartite matching literature takes $d = 0$: a vertex must be matched on arrival. Emek, Kutten and Wattenhofer (STOC 2016) and Huang et al. (STOC 2018) study delayed decisions in other models. The present model fixes a uniform deadline, and the weights are arbitrary.

Setting

A weighted graph has vertices $1, \dots, n$ and weights $v_{ij} \ge 0$ on undirected pairs. Vertices arrive one per period, vertex $i$ in period $\sigma(i)$, and the Adversarial Order setting assumes $\sigma(i) = i$. The weight of a pair is observed only when its later vertex arrives.

For a deadline $d \ge 1$, the online graph $G_{d,\sigma}$ keeps the edge $(i, j)$ exactly when $|\sigma(i) - \sigma(j)| \le d$. Vertex $i$ becomes critical at period $\sigma(i) + d$: the algorithm must match it then or let it depart. The benchmark $\mathrm{OFF}$ is the maximum weight of a matching of $G_{d,\sigma}$. A randomized online algorithm is $c$-competitive if its expected total weight is at least $c \cdot \mathrm{OFF}$.

Postponed Greedy (PG, Algorithm 3) gives each vertex $k$ a virtual seller $s_k$ with price $p(s_k)$ and a virtual buyer $b_k$. On arrival, $b_k$ bids once on the seller $s$ of largest margin $v_{s,b_k} - p(s)$. If the margin is positive, $b_k$ becomes the tentative match $m(s)$, displacing any earlier buyer, and $p(s)$ rises to $v_{s,b_k}$. The maximal margin is $q(b_k)$. When $k$ becomes critical with $m(s_k) = b_l$, a fair coin decides $k$'s status if it is still undetermined. A seller finalizes $(k, l)$ and collects $v_{k,l}$, and in either case $l$ receives the opposite status.

Formalization targets

Goal: Theorem 3.3

The theorem is stated for every $n$, every $d \ge 1$, all $v \ge 0$ and every tie-breaking rule for the $\operatorname{argmax}$, as four clauses. Every finalized pair is an edge of $G_{d,\sigma}$, for every outcome $\omega$ of the coins. The finalized pairs are vertex-disjoint, for every $\omega$. The expected reward satisfies

$$\mathrm{PG} = \frac{1}{2^n} \sum_{\omega} \mathrm{reward}(\omega) \ \ge\ \frac14\, \mathrm{OFF}.$$

And the state after $t$ periods depends only on the weights among vertices arrived by then and on the coins of vertices already critical.

Milestones

The proof of Theorem 3.3 uses no numbered result, so the milestones are its unnumbered claims, in proof order.

1. The virtual run $S, B, p, m, q$ reads no coin.
2. The matches $m^f$ form a collection of disjoint paths in $G_{d,\sigma}$.
3. Statuses alternate along a path, and $(k, l)$ is finalized exactly if $k$ is a seller.
4. A vertex with a final match is a seller with probability exactly $1/2$.
5. $\mathrm{PG} = \tfrac12 \sum_k p^f(s_k)$.
6. $\sum_s p^f(s) = \sum_b q(b)$.
7. $q(b_j) \ge v_{ij} - p(s_i)$ when $j$ arrives, for $i < j$ with $j - i \le d$.
8. $p(s)$ increases over time.
9. $\{p^f(s_k) + q(b_k)\}_k$ is feasible for the dual of the offline matching program.
10. $\mathrm{OFF}$ is at most the value of any feasible dual solution.

Significance

The result. Theorem 3.3 gives a constant competitive ratio for matching on arbitrary graphs with arbitrary non-negative weights and an adversarial arrival order. The paper's Figure 1 shows that no deterministic algorithm achieves a constant ratio, and the paper shows that no algorithm exceeds $1/2$. The same algorithm underlies the paper's extension to stochastic departures.

The formalization. The theorem is proved in the paper, and at the time of writing no machine-checked proof exists on this platform. The mission produces an executable-style specification of a randomized online algorithm, with the word "online" as a theorem clause, not a comment. It also produces a primal-dual argument for general-graph matching in the shape used by auction-style online algorithms. Weak duality for vertex potentials (milestone 10) is stated for every finite simple graph.

Difficulty

The obvious approach, assigning each vertex a seller or buyer role by an independent coin, loses a factor $4$ on each edge and gives only $1/8$ (Corollary 3.2). Postponed Greedy gains the factor $2$ by correlating the roles along paths of the virtual $2$-matching.

That correlation is the central difficulty. Whether $k$ is a seller is not one coin: it is the coin at the head of $k$'s path, flipped once per step along the path, and which vertices form that path depends on prices set after $k$ arrived. The claim "with probability exactly $1/2$" (milestone 4) needs the path structure to be independent of the coins (milestone 1), and it fails for a vertex with no final match. A vertex with no match is never a seller, which the proof's sentence leaves implicit, so milestone 4 is stated only for matched vertices.

Two further points are easy to get wrong. A buyer displaced from a seller never bids again, so the tentative matching need not be a maximum-weight matching of the virtual graph. The price of a seller rises while the seller is present, and the dual constraint for $(i, j)$ reads the price at the moment $j$ arrives, so the constraint at the final prices needs monotonicity (milestone 8).

Formalization scope

Vertices are Fin n, 0-based: vertex $k$ arrives in period $k$ and becomes critical in period $k + d$. Weights are v : Sym2 (Fin n) → ℝ. The run is a fold over the periods $0, \dots, n + d - 1$, with the arrival processed before the criticality within a period. Both choices are forced: processing criticality first makes the theorem false on $n = 2$, $d = 1$, and stopping at period $n$ collects nothing on $n = 2$, $d = 2$. Margins read onlineWeight, which is $0$ off the edges of the online graph, so the seller $s_k$ has margin $0$ for $b_k$. Coins are ω : Fin n → Bool, uniform, and the expectation is $2^{-n} \sum_\omega$. The benchmark reuses the published ProphetMatchingEFGT.optWeight, a finite maximum over matchings of a SimpleGraph.

The tie-breaking rule is a free parameter of the theorem, restricted to choose a maximizer and to see the arriving vertex, the seller set and the margins, but no coin. The reward is a sum over the finalized pairs, not the quantity $\tfrac12 \sum_k p^f(s_k)$, and the benchmark is on $G_{d,\sigma}$ and on no other graph. Each of these excludes a trivializing reading.

A complete development needs invariants of the state machine and no theory beyond Mathlib: finite sums, Finset and Sym2 manipulation, and counting on Fin n → Bool. Milestone 10 is reusable beyond this mission. Contributions to any milestone are welcome, in any order.

Selected references

• I. Ashlagi, M. Burq, C. Dutta, P. Jaillet, A. Saberi, C. Sholley, Maximum Weight Online Matching with Deadlines, arXiv:1808.03526v1, 2018. https://arxiv.org/abs/1808.03526
• J. Feldman, N. Korula, V. Mirrokni, S. Muthukrishnan, M. Pál, Online ad assignment with free disposal, WINE 2009, pp. 374–385. https://doi.org/10.1007/978-3-642-10841-9_34
• Y. Emek, S. Kutten, R. Wattenhofer, Online matching: haste makes waste!, STOC 2016, pp. 333–344. https://doi.org/10.1145/2897518.2897557
• Z. Huang, N. Kang, Z. G. Tang, X. Wu, Y. Zhang, X. Zhu, How to match when all vertices arrive online, STOC 2018, pp. 17–29. https://doi.org/10.1145/3188745.3188858

Motivation

In a coordination game on a graph, every player is a node and chooses a colour, and a node is rewarded for agreeing with its neighbours. These games model the adoption of a common standard, clustering, and the stabilisation of distributed protocols. When the graph is directed, the dynamics change sharply. A node is paid only by its in-neighbours and pays nothing back. Nash equilibria may fail to exist, and even on a single directed cycle, improvement dynamics can cycle forever. Apt, Simon and Wojtczak (arXiv:1910.02693v2, published in Mathematics of Operations Research, 2022) study when, from every starting configuration, some short sequence of profitable unilateral moves reaches a Nash equilibrium. Their two main graph classes come from networking. Simple cycles model token rings. Open chains of cycles model Ethernet ring protection (ITU-T G.8032), in which rings are joined in a sequence and consecutive rings share a single node.

Timeline:

• 2014–2017: Apt, de Keijzer, Rahn, Schäfer and Simon study coordination games on undirected graphs (WINE 2014; International Journal of Game Theory 46(3), 2017).
• 2016: Apt, Simon and Wojtczak, Coordination games on directed graphs (TARK 2015, EPTCS 215, arXiv:1606.07517), and Simon and Wojtczak, Efficient local search in coordination games on graphs (IJCAI 2016), report the first results for the directed case.
• 2019–2022: the journal version (arXiv:1910.02693v2) improves the bounds. It gives polynomial bounds on improvement paths for simple cycles (Theorems 3, 5, 7, 9) and open chains (Theorem 15), and proves NP-completeness of Nash-equilibrium existence in general (Theorem 36). Weighted open chains are not treated here; the paper points to the IJCAI paper for them (p.34).

Setting

Fix a finite set $M$ of colours. A coordination game is given by a directed graph on a finite vertex set $V$ without self-loops, a positive weight $w_{j\to i}$ on each edge, a colour assignment giving every node $i$ a non-empty set $C(i)\subseteq M$, and bonuses $\beta(i,c)\in\mathbb N$. A joint strategy $s$ picks $s_i\in C(i)$ for every node, and the payoff of node $i$ is

$$p_i(s)=\sum_{j\in N_i,\ s_j=s_i} w_{j\to i}+\beta(i,s_i),$$

where $N_i$ is the set of in-neighbours of $i$. Unless stated otherwise, graphs are unweighted ($w=1$) and there are no bonuses ($\beta=0$).

A node plays a best response if no colour in $C(i)$ gives it a higher payoff. A Nash equilibrium is a joint strategy in which every node plays a best response. An improvement step $s\to s'$ changes the colour of a single node to one that strictly increases that node's payoff. A game ensures improvement paths of length at most $X$ if from every joint strategy $s_0$ there are $s_0\to s_1\to\dots\to s_L$, $L\le X$, all improvement steps, with $s_L$ a Nash equilibrium.

A simple cycle is $1\to2\to\dots\to n\to1$. An open chain of $m\ge2$ cycles $\mathcal C_1,\dots,\mathcal C_m$, each with $v\ge3$ nodes, has cycles $\mathcal C_j=[j,1]\to[j,2]\to\dots\to[j,v]\to[j,1]$. For $j\le m-1$ the node $[j,1]$ coincides with the node $[j+1,k_j]$ of the next cycle, for some $k_j\in\{2,\dots,v\}$. No other nodes coincide, so the chain has $vm-(m-1)$ nodes.

Formalization targets

Goal: Theorem 15 (p.20)

For every open chain of $m\ge2$ cycles with $v\ge3$ nodes each, every choice of the attachment positions $k_j$, every colour set $M$ and every colour assignment $C$ with non-empty colour sets, the unweighted coordination game without bonuses on the chain satisfies

$$\text{ensures improvement paths of length}\le 3vm^3 .$$

Milestones

1. Theorem 3 (p.11): a weighted simple cycle with at most one bonus node ensures improvement paths of length $\le 2n-1$.
2. Theorem 7 (p.13): a weighted simple cycle with two bonus nodes ensures improvement paths of length $\le 3n$.
3. Cycle reduction (p.16). Given $s$, the cycle $\mathcal C_j$ behaves like a simple cycle whose link nodes carry a unit bonus $\beta^s_j$ for the colour of their predecessor in the adjacent cycle. Improvement paths of that cycle game lift to the chain.
4. Lemma 10 (p.16): on an open chain, and on a simple cycle with unit bonuses, a node with payoff $\ge1$ plays a best response.
5. Lemma 11 (p.17): once a cycle below the cycle being repaired by Algorithm 1 has grade $\mathrm U{+}$, it keeps that grade and the algorithm never returns to it.
6. Claim 1 (p.37): a sufficient condition for the progress measure $\mu$ to increase.
7. Range of $\mu$ (p.20): $\mathrm{guard}(s)+1\le\mathrm{NBR}(s)\le|\mathrm{prefix}(s)|\le m$ when $s$ is not a Nash equilibrium.
8. Counting (p.20): $\mu$ takes at most $1+m(m+1)(m+5)/6\le m^3$ values.

Significance

The result shows that on open chains of directed cycles, which lack the finite improvement property, short improvement paths always exist. Their length is polynomial in both the ring size and the number of rings. In particular a Nash equilibrium always exists and can be reached by local, one-node-at-a-time improvements, which is the kind of guarantee a distributed protocol needs. The same construction underlies the paper's polynomial-time algorithm for finding a Nash equilibrium on open chains and its bound for coalitional improvement paths (Theorem 23).

Formalizing it adds to the platform coordination games on directed graphs, improvement paths with a length bound, and the open-chain graph class. None of these are on the platform today. The results are proved in the paper. None of them has a machine-checked proof.

Status of the printed proof. A check of Lemmas 12 and 14 (pp.17–20, Appendix pp.35–39) found that both fail for some attachment positions. Lemma 12 claims that one round of Algorithm 1 on $\mathcal C_j$ changes only the grades of $\mathcal C_{j-1},\mathcal C_j,\mathcal C_{j+1}$, and Lemma 14 claims that $\mu$ increases in every round. When $k_{j-2}=2$, the node $[j-1,2]$ is the link node $[j-2,1]$, so recolouring $[j-1,1]$ can change the grade of $\mathcal C_{j-2}$. A concrete chain with $m=3$, $v=4$, $k_1=2$, $k_2=3$ has a round of Algorithm 1 in which $\mu$ drops from $(0,1,0,-3)$ to $(0,0,1,-1)$. These two lemmas are therefore not milestones. Theorem 15 itself is not contradicted: exhaustive search on small chains found improvement paths well within $3vm^3$. A complete proof needs a repaired progress argument or a different one.

Difficulty

The obvious argument fails at the start. Scheduling the nodes round-robin does not terminate on a directed cycle, since a colour can chase itself around the ring forever (Example 2, p.10). Even the cycle bounds need a specific schedule and a specific choice among best responses. On an open chain, repairing one cycle recolours its link nodes and can destroy the equilibrium of the neighbouring cycles. The index of the lowest broken cycle can therefore move down by an arbitrary amount (Figure 9, p.19). Termination needs a progress measure that increases at every round despite this back-and-forth, and the attachment positions $k_j=2$ and $k_j=v$ let a single repair reach two cycles away.

Formalization scope

A joint strategy is a function $s:V\to M$ with $s_i\in C(i)$. Payoffs are real. An improvement path of length at most $X$ is a list $s_0,\dots,s_L$, $L\le X$, of joint strategies in which each step changes exactly one node's colour to a colour in its set and strictly raises that node's payoff, and whose last element is a Nash equilibrium. Length counts steps. Simple cycles live on Fin n with edges $a\to a+1\pmod n$ and $n\ge2$. An open chain is a structure with $m\ge2$, $v\ge3$, a surjective naming map $(j,i)\mapsto[j+1,i+1]$ from Fin m × Fin v onto $V$, attachment positions with $k_j\ge2$, the link identifications, and nothing else identified. Its edges are exactly the cycle edges. The game on an open chain is unweighted and has no bonuses, as in the paper. Weighted open chains are outside this paper (p.34).

Non-empty colour sets are hypotheses everywhere. Without them there is no joint strategy and every statement would be vacuous. Improvement steps require a strict gain, so constant paths do not count.

The development needs the general strategic-game notions (best response, Nash equilibrium, improvement steps and paths, schedules), coordination games, simple cycles and open chains, and, for the milestones about Algorithm 1, the link bonuses $\beta^s_j$, grades, $\mathrm{NBR}$, $\mathrm{guard}$, $\mathrm{prefix}$, the measure $\mu$ and one round of the algorithm. The strategic-game layer is reusable for any finite game. Contributions are welcome on the cycle theorems, on a repaired progress measure for open chains, or on any other proof of Theorem 15.

Selected references

• K. R. Apt, S. Simon, D. Wojtczak, Coordination Games on Weighted Directed Graphs, arXiv:1910.02693v2, 2021; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1910.02693v2
• K. R. Apt, S. Simon, D. Wojtczak, Coordination games on directed graphs, Proc. TARK 2015, EPTCS 215, pp. 67–80, 2016. https://arxiv.org/abs/1606.07517
• S. Simon, D. Wojtczak, Efficient local search in coordination games on graphs, Proc. IJCAI 2016, pp. 482–488, 2016. https://arxiv.org/abs/1604.04809
• K. R. Apt, B. de Keijzer, M. Rahn, G. Schäfer, S. Simon, Coordination games on graphs, International Journal of Game Theory 46(3):851–877, 2017. https://arxiv.org/abs/1501.07388

Motivation

Spare parts, slow-moving retail items and humanitarian relief stock share a demand pattern: most periods see no demand, and a demand arrives only now and then. Planners of such long-tail or intermittent-demand items estimate the inter-arrival distribution from a finite observed history and feed it into an inventory policy. Bi, He and Teo (MSOM 2023) observe that this estimate is biased in a precise, computable way, for the same reason as the "hot hand" selection bias of Miller and Sanjurjo (Econometrica 2018): in a finite sequence of independent trials, the expected proportion of successes that immediately follow a success is strictly smaller than the success probability.

Timeline:

• Rinott and Bar-Hillel (2015), commenting on the working-paper version of Miller and Sanjurjo, give a combinatorial argument for the expected proportion of successes following a success in a finite i.i.d. sequence (SSRN 2642450); Bi, He and Teo adapt it, with an initial arrival at time $0$.
• Miller and Sanjurjo (2018) show that this selection bias is present in the standard measure of conditional dependence for i.i.d. Bernoulli trials, so the "gambler's fallacy" belief is partly a correct reading of finite data.
• Bi, He and Teo (2023) prove the bias for a general Markov chain of demand arrivals (Proposition 1), give a closed form for the expected empirical inter-arrival proportions under i.i.d. arrivals (Theorem 2), and prove that the relative bias is monotone in the arrival probability and in the horizon (Proposition 2).

Setting

Time positions are $0,1,\dots,n$. A demand arrival occurs at position $0$ by assumption, and at each of the positions $1,\dots,n$ independently with probability $p\in(0,1)$; write $q=1-p$ and $B(t)\in\{0,1\}$ for the arrival indicator, so $B(0)=1$.

For a gap length $j\ge1$, the empirical proportion $\hat p_j(n)$ is the number of positions $t\in\{0,\dots,n-1\}$ with $B(t)=1$, $B(t+1)=\dots=B(t+j-1)=0$, $B(t+j)=1$ and $t+j\le n$, divided by the number of arrivals $B(t)=1$ at positions $t\in\{0,\dots,n-1\}$. The denominator is at least $1$ because of the arrival at $0$. The biased estimate is

$$p_j(n)=\mathbb E\big[\hat p_j(n)\big],$$

and the relative bias of the estimate of $p=p_1$ is

$$\frac{p-p_1(n)}{p}.$$

In Lean, a sample path is ω : Fin n → Bool, the arrival indicator is arrival ω t, $\hat p_j(n)$ is empiricalGap n j ω, and $p_j(n)$ is biasedEstimate n j p, the weighted sum of $\hat p_j(n)$ over the $2^n$ paths with weights $\prod_k(p\text{ or }1-p)$.

Formalization targets

Goal: Proposition 2

For every $n\ge2$, the map $p\mapsto(p-p_1(n))/p$ is strictly decreasing on $(0,1)$; and for every $p\in(0,1)$, the map $n\mapsto(p-p_1(n))/p$ is strictly decreasing on $\{n\in\mathbb N:n\ge2\}$:

$$\frac{p-p_1(n)}{p}\ \text{is strictly decreasing in } p\in(0,1)\ \text{and in } n\ge2.$$

The printed proposition says "for all $n$". At $n=1$ the estimate is unbiased ($\hat p_1(1)=B(1)$, so $p_1(1)=p$) and the relative bias is $0$ for every $p$, which is not strictly decreasing in $p$ and is smaller than its value $(1-p)/2$ at $n=2$ (so part (ii) fails at $n=1$ under any reading). The goal is therefore stated for $n\ge2$, the range in which the proof (which divides by $m=n-1$) works. "Decreasing" is read as strict, which is what the proof gives.

Milestones

1. Theorem 2 (closed form). For $n\ge1$, $j\ge1$, $p\in[0,1]$,

$$p_j(n)=\sum_{i=1}^{n-j}\binom{n-1-j}{i-1}p^iq^{n-1-i}\frac{p+i}{i+1}+\mathbf 1[j=n]\,p\,q^{n-1}.$$

The printed theorem lacks the last term; without it the formula fails at $j=n$ (for $n=2$, $j=2$, $p=1/3$: $p_2(2)=2/9$, while the printed sum is empty). 2. EC.2.2 (i), derivative. With $m=n-1\ge1$ and $f(p)=p_1(n)/p$,

$$f'(p)=p^{-1}\Big(\sum_{i=1}^m\binom{m-1}{i-1}p^{i-1}(1-p)^{m-i}\frac{mp+2}{i+1}-1\Big).$$

3. (EC.1). For $m\ge1$, $(mp+2)\sum_{i=1}^m\rho_i/(i+1)>1$ with $\rho_i=\binom{m-1}{i-1}p^{i-1}(1-p)^{m-i}$.
4. (EC.2)–(EC.3), increment. For $m\ge1$,

$$p_1(n+1)-p_1(n)=\frac{pq}{mq}\Big[\sum_{i=0}^m\binom mi p^iq^{m-i}\frac{mp+2}{i+2}-1\Big].$$

The printed chain asserts a strict "$>$" in (EC.2); the two sides are in fact equal (both are $1/81$ at $n=2$, $p=1/3$), and the milestone states the equality. 5. Last inequality of EC.2.2 (ii). $\sum_{i=0}^m\binom mi p^iq^{m-i}\frac{mp+2}{i+2}\ge1$, strictly when $m\ge1$.

Significance

Proposition 2 explains why the finite-horizon effect matters most for long-tail items: the relative under-estimation of the arrival probability is largest when $p$ is small and the observation window is short. In the paper this drives the inventory results of §4: the delay of the delay-ordering policy chosen with the biased estimates, and the staggered base stock policy. Theorem 2 makes the bias computable exactly rather than by simulation.

On the formalization side, nothing in this mission has a machine-checked proof yet. The work is to formalize the paper's argument: the path-counting identity behind Theorem 2 (summing over $2^n$ Bernoulli paths), a derivative computation, and two strict Cauchy–Schwarz type bounds for binomial weights. The definitions of the empirical proportion and the expected estimate are reusable for other results on streaks and the hot-hand selection bias.

Difficulty

The main step is Theorem 2: converting an expectation of a ratio of two random counts into a binomial sum. The obvious route, linearity of expectation, fails because the denominator (the number of arrivals) is random and correlated with the numerator. The paper conditions on the number $i$ of arrivals among periods $1,\dots,n-1$ and counts the positions where a gap of length $j$ can sit, including the gap that closes exactly at the horizon. That case split is where the printed formula loses the $j=n$ term.

The monotonicity steps are elementary but require strictness throughout: both (EC.1) and the last inequality are of the form $\mathbb E[Y]\,\mathbb E[1/Y]>1$, and they are strict only because the binomial variable is non-degenerate for $m\ge1$ and $p\in(0,1)$.

Formalization scope

• Paths are Fin n → Bool for the periods $1,\dots,n$; the arrival at position $0$ is built into arrival, so the denominator of $\hat p_j(n)$ is at least $1$ for $n\ge1$ by construction, not by hypothesis.
• The expectation is a finite weighted sum over all $2^n$ paths; it equals the expectation under the i.i.d. Bernoulli($p$) product law.
• The estimate $p_j(n)$ is defined from the paths, not by the closed form of Theorem 2; defining it by the closed form would make Theorem 2 trivial and turn the goal into a statement about a polynomial chosen by hand.
• Milestones 2–5 use $m=n-1$ as a natural number with the horizon written $m+1$, so there is no truncated subtraction in the horizon.
• Monotonicity is StrictAntiOn, on Set.Ioo 0 1 in $p$ and on {n | 2 ≤ n} in $n$.

Welcome contributions: a proof of Theorem 2 by induction on $n$ or by conditioning on the number of arrivals; general lemmas on sums over Fin n → Bool against product Bernoulli weights; and the strict inequality $\mathbb E[X+c]\,\mathbb E[1/(X+c)]>1$ for non-degenerate binomial $X$.

Selected references

• S. Bi, L. He, C.-P. Teo, Taming the Long Tail: The Gambler's Fallacy in Intermittent Demand Management, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2023.1217
• J. B. Miller, A. Sanjurjo, Surprised by the Hot Hand Fallacy? A Truth in the Law of Small Numbers, Econometrica 86(6), 2019–2047, 2018. https://doi.org/10.3982/ECTA14943
• Y. Rinott, M. Bar-Hillel, Comments on a "Hot Hand" Paper by Miller and Sanjurjo (2015), SSRN working paper 2642450, 2015. https://ssrn.com/abstract=2642450

Motivation

Electric utilities run demand-response programs to cut peak load during supply shortages: when an event is called, a participating customer is paid a rebate for every unit by which its consumption falls below a baseline. The utility sees consumption, not demand, so the baseline is its estimate of what the customer would have consumed without the event. In practice the baseline is the customer's average historical consumption in non-event periods (the "normal-use" baseline used by PEPCO and BG&E). This creates a measurement problem. A customer whose demand happens to be low is paid for reductions it never made, and a customer whose demand is high has to cut a lot before it is paid anything.

Agrawal and Yücel (Management Science, 2022, doi:10.1287/mnsc.2021.4278) model this as a game between a utility and its customers. They ask how the utility should set the baseline and the rebate, and whether moving the baseline away from normal use helps or hurts the environment. Their headline finding is that the cost-optimal baseline can reduce the actual demand reduction and raise emissions, against the intuition that paying more effectively must buy more reduction. This mission formalizes that finding, Proposition 4 of the authors' manuscript of May 26, 2021, together with the chain of results it rests on.

Setting

Peak demand in an event (probability $\rho\in(0,1]$) is $\omega$, uniform on $[0,2\Omega]$. Without an event it is $\lambda$, uniform on $[0,2\Lambda]$ with $\Lambda<\Omega$. Off-peak demand $\varphi$ is uniform on $[0,2\Phi]$. The utility buys power at marginal cost $c^h_p$ in an event and $c^l_p<c^h_p$ otherwise, and $\Delta c=c^h_p-c^l_p$.

Given a baseline $b\ge0$ and a rebate $r\ge0$, a customer with demand $\omega$ shifts $s\le\omega$ units to the off-peak period. Its consumption is $\omega-s$, the estimated reduction is $S(s)=(b-(\omega-s))^+$, and the customer maximizes

$$C_c(s)=r\,S(s)-\frac{c_s}{2}s^2,\qquad s\le\omega .$$

A best-response selection $s^*(b,r\mid\omega)$ picks a maximizer for every $(b,r,\omega)$. The utility's expected net cost savings are

$$C(b,r)=\rho\,\mathbb E_\omega\bigl[\Delta c\,s^*-r\,S(s^*)\bigr],$$

and its total cost is $C_u=\bar C-C$ with $\bar C$ independent of $(b,r)$. The expected actual demand reduction is $X(b,r)=\rho\,\mathbb E_\omega[s^*]$. Total expected emissions are $E_u=\bar E-\Delta e\,X$, with emission intensities $e^h_g>e^l_g$ and $\Delta e=e^h_g-e^l_g$. Two regimes are compared:

• normal-use baseline: $b=\Lambda$, and the rebate $r_0$ maximizes $C(\Lambda,\cdot)$;
• optimized baseline: $(b^*,r^*)$ maximizes $C$ over $b,r\ge0$. When this maximizer is not unique, $(b^*,r^*)$ is the one with the least rebate.

The firm inflates the baseline if $b^*>\Lambda$ and deflates it if $b^*<\Lambda$.

Formalization targets

Goal: Proposition 4 (p.19)

For $0<\Lambda<\Omega$ and $c_s>0$ there are thresholds $c_D<c_I$, depending only on $(\Omega,\Lambda,c_s)$, such that

$$b^*>\Lambda:\quad X(b^*,r^*)\le X(\Lambda,r_0)\iff\Delta c\ge c_I,\qquad b^*<\Lambda:\quad X(b^*,r^*)\ge X(\Lambda,r_0)\iff\Delta c\le c_D,$$

and the same with total emissions $E_u$ in place of $X$, with the inequalities reversed. The goal pins the thresholds down: $c_D=\kappa\Lambda c_s$ with $\kappa\approx0.7941$ the root of $9\kappa^3+15\kappa^2-175\kappa+125$ in $(1/2,1)$, and $c_I=\tfrac12(4+\sqrt2)\Omega c_s$ when $\Lambda\le\frac{4+\sqrt2}{6}\Omega$, or the root of an explicit equation in $[\tfrac52\Omega c_s,3\Lambda c_s]$ otherwise.

Milestones, in proof order

1. Proposition 1: the customer's response has three regimes (no, partial, full shift).
2. Lemma 1: the reduction is overestimated iff $\omega<b$.
3. Closed form of $X(b,r)$ (p.OA1).
4. Lemma 2: monotonicity of $X$, of the overestimation $X_o$ and of the underestimation $X_u$.
5. $C_u=\bar C-C$ and $C=(\Delta c-r)X-rX_o+rX_u$.
6. Closed form of $r_0$, which is unique (p.OA2).
7. Lemma 3: at $b=\Lambda$ the program is offered iff $\Delta c>\Lambda c_s/2$, and $r_0$ increases in $\Delta c$.
8. Closed form of $(b^*,r^*)$ and of the whole maximizer set (pp.OA2–OA3).
9. Lemma 4: with both instruments the program is always offered, and $r^*$ increases in $\Delta c$.
10. Proposition 2: $b^*$ increases in $\Delta c$ up to $\tfrac52\Omega c_s$ and decreases after.
11. Proposition 3: inflate and lower the rebate iff $\Delta c>\tfrac53\Lambda c_s$.
12. Cases 1–4 of the proof of Proposition 4: $X(b^*,r^*)$ against $X(\Lambda,r_0)$.
13. $E_u=\bar E-\Delta e\,X$.

Significance

The result separates two things a regulator might expect to move together. Optimizing the baseline always raises the utility's savings. Proposition 4 says exactly when it also lowers the actual reduction of peak demand, and with it the environmental benefit that motivates these programs. For a large cost gap the inflated baseline comes with a lower rebate, and the lower rebate dominates. For a small cost gap the deflated baseline comes with a higher rebate, and the reduction rises. The thresholds are explicit functions of the model's primitives, so the regions can be located for any calibration, such as the Maryland one of the paper's Figure 3.

The paper proves the result by hand through a case analysis over the $(b,r)$ quadrant. Machine-checking it fixes several printed details that the formal statements had to correct. The emissions clause compares the emissions reduction $E$ where total emissions $E_u$ are meant. The proof's $c_I$ switches form at $\Lambda\approx0.9553\,\Omega$ instead of $\Lambda=\frac{4+\sqrt2}{6}\Omega\approx0.9024\,\Omega$. One display of Case 3 has the wrong sign. Three clauses of Proposition 1 fail at boundary cases. Each correction is recorded on its item with a counterexample. None of these results has a machine-checked proof yet.

Difficulty

The customer's objective is the maximum of two parabolas. It is not concave, so the best response jumps with $\omega$, and ties occur at isolated demand levels. The firm's objective $C(b,r)$ therefore has different closed forms on several regions of the quadrant, separated by curves such as $b=r/(2c_s)$, $b=2\Omega-r/(2c_s)$ and $rb=2\Omega^2c_s$. The maximum has to be global over all of them. The natural approach, setting the gradient to zero on the region that contains the paper's optimum, does not certify a global maximum. For $\Delta c\ge4\Omega c_s$ the savings are constant along the ridge $rb=2\Omega^2c_s$, so the maximizer is a curve rather than a point. The comparison of $X(b^*,r^*)$ with $X(\Lambda,r_0)$ then needs single-crossing arguments between a polynomial and a square-root expression, and the threshold changes form with $\Lambda/\Omega$.

Formalization scope

All quantities are real numbers. Expectations are interval integrals with the uniform densities written out, and the two-period expectations are iterated integrals. The customer's best response is an arbitrary selection s : ℝ → ℝ → ℝ → ℝ with IsBestResponse, never a closed formula. Selections differ only on null sets, so every expectation is the paper's. The firm's domain is $b\ge0$, $r\ge0$, and the customer's feasible set is $s\le\omega$. Optimality of $(b^*,r^*)$ and of $r_0$ is defined by maximizing $C$. The closed forms are milestones, not definitions. $X_o$ integrates the density only up to $2\Omega$, and $X_u$ is a set integral over $\{b\le\omega\le\omega_1\}$, so both make sense for $b>2\Omega$.

Defining $s^*$, $r_0$ or $(b^*,r^*)$ by their closed forms would make the goal a statement about formulas rather than about optimization, and placing the threshold quantifiers after $\Delta c$ would make the equivalences empty. The statements do neither.

Mathlib's interval integrals, Real.sqrt and max are the only infrastructure needed. Proofs of any milestone are welcome, as are alternative proofs of the firm's global optimum that avoid the full case analysis.

Selected references

• V. V. Agrawal, Ş. Yücel, Design of Electricity Demand-Response Programs, Management Science, 2022 (manuscript of May 26, 2021, with Online Appendix). https://doi.org/10.1287/mnsc.2021.4278
• FERC, Measurement and Verification for Demand Response, Federal Energy Regulatory Commission, 2013. https://perma.cc/C248-DJ72