All missions

Motivation

Production in agriculture, semiconductors, pharmaceuticals and many other industries suffers from random yield: only a random fraction of a planned production run turns out usable. When a retailer buys from such a supplier, someone in the chain bears the risk that less arrives than was ordered. Geng, Guo, Xiao and Yang (SSRN 3546872; Manufacturing & Service Operations Management 25(3), 2023, doi:10.1287/msom.2022.0198) study two levers a retailer can pull to push that risk away from itself. Payment postponement means paying only for what is delivered rather than for what was ordered. Pricing postponement means fixing the retail price after the delivery is known rather than committing to it in advance. Both are common in practice, and their effect on the other members of the chain, the supplier and the end consumers, is not obvious: shifting risk changes the supplier's wholesale price and production, and so everyone's payoff.

This mission formalizes the paper's answer for pricing postponement (its Proposition 5): when does moving from ex ante to responsive pricing make the supplier, the retailer and the consumers all better off, and when does it hurt the supplier?

Setting

A supplier sells one product to a retailer, who sells it in a market with linear demand $d(p) = a - bp$, $a, b > 0$, and inverse demand $p(t) = (a-t)/b$. The supplier plans a production quantity $Q$ at unit cost $c$, but only $YQ$ is realized, where the yield factor $Y$ equals $1$ with probability $\theta$ and $\alpha$ with probability $1-\theta$, for $\alpha, \theta \in (0,1)$. Write $\mu = \alpha(1-\theta)+\theta$ for the mean yield. The retailer orders $q$ and receives $\hat q = \min\{YQ, q\}$.

There are four scenarios. Under pay-by-order (O) the retailer pays $wq$; the supplier then produces exactly $Q = q$. Under pay-by-delivery (D) it pays $w\min\{YQ,q\}$, and the supplier may inflate production above $q$. Under ex ante pricing (A) the retailer commits to a price $p$ when it orders; under responsive pricing (R) it sets $p$ after observing $\hat q$, maximizing $p\min\{d(p),\hat q\}$. In each of OA, OR, DA, DR the supplier first sets the wholesale price $w$, the retailer then orders (and, ex ante, prices), the supplier chooses $Q$, the yield is drawn, and under responsive pricing the price is set last. Both firms are risk-neutral. Admissible actions are $0 < p < a/b$, $q \ge 0$, $Q \ge 0$, and $c < w < a/b$ (pay-by-order) or $c/\mu < w < a/b$ (pay-by-delivery); costs range over $0 < c < a\mu/b$.

The solution concept is subgame-perfect equilibrium. Its outcome is the triple $(\pi^k_R, \pi^k_S, CS^k)$ of the retailer's and supplier's expected profits and the expected consumer surplus $CS^k = \mathbb E\,\mathcal S(p,\hat q)$, with

$$\mathcal S(p,X) = \int_0^{\min\{d(p),X\}} \big(p(t)-p\big)\,dt .$$

The paper derives each scenario's equilibrium in closed form, piecewise in $c$, with thresholds such as $c^{OA}_1, c^{OA}_2, c^{OR}, c^{DR}_1$ (its Lemmas 1–4 and Appendix B).

Formalization targets

Goal: Proposition 5

(O) Pay-by-order, any $\alpha\in(0,1)$. Comparing equilibria of OA and OR:

$$\max\{c^{OR}, c^{OA}_2, 0\} < c < \tfrac ab\mu \;\Longrightarrow\; \pi^{OA}_R < \pi^{OR}_R,\ \pi^{OA}_S < \pi^{OR}_S,\ CS^{OA} < CS^{OR};$$

an increasing function $\Theta(\alpha)$ such that $\theta < \Theta(\alpha)$ implies $c^{OA}_1 > \tilde C > 0$ and the same triple of increases on $\tilde C < c < c^{OA}_1$; and, if $c^{OR} > 0$,

$$0 < c < \min\{c^{OR}, c^{OA}_1\} \;\Longrightarrow\; \pi^{OA}_R < \pi^{OR}_R,\ \pi^{OR}_S < \pi^{OA}_S,\ CS^{OA} < CS^{OR}.$$

(D) Pay-by-delivery, $\alpha \ge 9/16$. Comparing equilibria of DA and DR: all three quantities strictly increase for $c^{DR}_1 < c < a\mu/b$, and all three are unchanged for $0 < c < c^{DR}_1$.

Milestones

The equilibrium of each scenario (Lemmas 1–4, with existence and uniqueness of the outcome on each open piece of $c$), the two last-stage responses (production (4) and the ex post price (5)), Lemma 2(i) (when $c^{OR} \ge 0$), the threshold claim behind (O)(ii) ($\theta < \Theta(\alpha) \Rightarrow c^{OA}_1 > \tilde C > 0$ and $c^{OR} < \tilde C$), and the ordering $c^{DR}_1 < c^{DR}_2 < c^{DA}$ for $\alpha \ge 9/16$.

Significance

The result. Proposition 5 shows that pricing postponement can be a Pareto improvement for the entire chain, consumers included, and identifies where: at high or intermediate production cost under pay-by-order, and above $c^{DR}_1$ under pay-by-delivery. It also identifies the one place where it is not: under pay-by-order, low cost, and severe and likely yield loss, the retailer gains at the supplier's expense, because it orders a large quantity at a low wholesale price. Under pay-by-delivery and low cost, pricing postponement changes nothing, since the supplier already absorbs the yield risk by inflating production. These statements feed the paper's managerial conclusions on when a retailer facing unreliable supply should adopt flexible pricing and how this affects its supplier.

Formalizing it. The paper proves its lemmas by "the results in Appendix B" and its propositions as "straightforward comparisons". A machine-checked development would make the backward induction itself explicit: four three-stage games, each with kinks in the production and order responses and boundary optima of the wholesale price. Drafting this mission already turned up four printed slips: a consumer-surplus denominator in Appendix B.1 ($8b\alpha^3$ for $8b\alpha^2$), a consumer-surplus value in Appendix B.4 that no single equilibrium produces, a production tie rule under which scenario DR has no equilibrium on an interval of costs, and swapped labels in display (2). None of them changes Proposition 5. To our knowledge, none of the paper's results has been formalized.

Difficulty

Once Lemmas 1–4 are known, each comparison in Proposition 5 is algebra between explicit pieces. The work is in Lemmas 1–4. The obvious approach, maximizing each stage's closed-form objective, does not suffice. The equilibrium must be optimal in every subgame, including order quantities and wholesale prices never played. The objectives are only piecewise smooth, so the maximizer often sits at a kink: at $w = \hat w$ in scenario OA, the retailer is indifferent between inflating its order and not; at $w = c/(\alpha(1-\theta))$ in scenario DR, the supplier is indifferent between inflating production and not, and the supplier's value is discontinuous there. Existence of an equilibrium in DR on $(c^{DR}_1, c^{DR}_2)$ depends on how that tie is resolved. On top of this come inequalities between thresholds involving nested square roots, e.g. $c^{OR} < \tilde C$ under $\theta < \Theta(\alpha)$, and the monotonicity of $\Theta$.

Formalization scope

Everything is finite-dimensional real arithmetic: $\mathbb E f(Y) = \theta f(1) + (1-\theta)f(\alpha)$, with no measure theory. The cost $c$ is a separate argument, and every threshold depends on $(a,b,\alpha,\theta)$ only. The standing assumptions are $a,b>0$, $\alpha,\theta\in(0,1)$ and $0<c<a\mu/b$, the paper's (1) and (3). Strategies are functions of everything observed before the move. Optimality is required at every node. Under pay-by-order $Q = q$, as the model prescribes. Conventions committed to, all disclosed in the items:

• when the supplier is indifferent between producing $q$ and inflating, it produces $q$;
• consumer surplus uses the ex post price under OR/DR and the committed price under OA/DA;
• $c^{OA}_2$ is the larger root of an explicit quadratic, identified with the paper's "second root" of a quartic;
• $\tilde C$ is the explicit (6), and $\Theta$ is the explicit formula of the proof, with its monotonicity part of the goal;
• lemmas are stated on open intervals of $c$, because at a threshold the outcome is not unique;
• the consumer-surplus values of Appendix B.1 (middle piece) and B.4 (middle piece) are corrected to the equilibrium values.

The profits are the outcomes of equilibria of the game, not the closed forms of Appendix B. The goal also asserts that equilibria exist for every admissible cost, so it cannot hold vacuously through an unsatisfiable equilibrium predicate.

Contributions welcome: the last-stage lemmas (4) and (5), the threshold inequalities, the scenario equilibria (Lemmas 1–4), and the goal. The equilibrium framework is shared with the three sibling missions on Propositions 2, 3 and 4 of the same paper.

Selected references

• X. Geng, X. Guo, G. Xiao, N. Yang, Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement?, SSRN 3546872 (author version, 2022); Manufacturing & Service Operations Management 25(3), 2023. https://ssrn.com/abstract=3546872, https://doi.org/10.1287/msom.2022.0198

Establish the separation exponent $\alpha\ge2.007$ for total Boolean functions, improving on the depth-20 specialization of OpenAI's construction.

Precisely, for every $\varepsilon>0$ and every integer $S\ge2$, construct a function $f$ with $s(f)\ge S$ and $bs(f)\ge s(f)^{2.007-\varepsilon}$.

A finite certificate is sufficient: supply a function and an input $x$ with $s(f)\le A$, $bs(f,x)\ge B$, $A,B>1$, and $A^{2.007}\le B$, then apply the shared certificate theorem. Sharper estimates, improved parameters, and different constructions are all eligible; direct family proofs are also welcome.

This is an open research target. The preceding benchmarks are $2$ classically and approximately $2.006470828$ from the depth-20 seed. Numerical searches guide discovery but do not replace certified bounds. Intermediate improvements are welcome as separate campaign entries.

Motivation

The price of anarchy (PoA) of a nonatomic congestion game measures how much total cost is lost when a continuum of selfish users routes traffic instead of a central planner. Worst-case bounds on the PoA over classes of cost functions are classical: $4/3$ for affine costs and $\Theta(\beta/\ln\beta)$ for polynomial costs of degree at most $\beta$ (Roughgarden and Tardos 2002; Roughgarden 2003). Worst-case bounds say nothing about how the PoA of one particular instance reacts when its demands and cost functions are perturbed, which is what matters when traffic data are measured with error or change over time.

Z. Wu and R. H. Möhring (arXiv:2007.13979v3, published in Mathematics of Operations Research, 2023) study this sensitivity through Hölder continuity of the PoA map $\Gamma \mapsto \rho(\Gamma)$ on a metric space of games. Earlier work considered changes of the demand alone: Englert et al. (2010), Takalloo and Kwon (2020) and Cominetti et al. (2020), as cited in the paper, fix the cost functions and vary the demand. Wu and Möhring vary both. Their main positive results are local: Hölder continuity with exponent $1/2$ near every game with Lipschitz costs. This mission formalizes their negative result, Theorem 8, which says that no global version of this regularity is possible.

Setting

Fix a network with arcs $A$, a non-empty finite set $K$ of origin–destination (O/D) pairs, and for each pair $k$ a set $S_k$ of paths, each a non-empty set of arcs, with $|S_k| \ge 2$ and every arc on some path (Condition 1). A game $\Gamma = (\tau, d)$ consists of cost functions $\tau_a$, continuous, non-decreasing and non-negative on $[0,\infty)$, and demands $d_k \ge 0$ with total demand $T(d) = \sum_k d_k$. The game space $\mathcal G(G,K,S)$ consists of the games with $T(d) > 0$ and $\tau_a(x) > 0$ for $x \in (0, T(d)]$ (Condition 2).

A flow splits each $d_k$ non-negatively over $S_k$; its arc flows are $f_a = \sum_{s \ni a} f_s$ and its total cost is $C(\Gamma, f) = \sum_a f_a \tau_a(f_a)$. A Wardrop equilibrium (WE) is a flow in which every used path of a pair has minimal cost among the paths of that pair. With $C^*(\Gamma)$ the minimum total cost and $\tilde C(\Gamma)$ the total cost of a WE flow,

$$\rho(\Gamma) = \frac{\tilde C(\Gamma)}{C^*(\Gamma)}.$$

The distance of two games $\Gamma = (\tau, d)$, $\Gamma' = (\sigma, d')$ is

$$\|\Gamma - \Gamma'\| = \max\Big\{\|d - d'\|_\infty,\ \max_{a,\ x \in [0, \min\{T(d),T(d')\}]} |\tau_a(x) - \sigma_a(x)|,\ \|\tau(T(d)) - \sigma(T(d'))\|_\infty\Big\}.$$

The cost normalization $\Psi_\upsilon(\tau, d) = (\tau/\upsilon, d)$, $\upsilon > 0$, divides all costs by $\upsilon$. A $\gamma$-neighborhood of $\Gamma$ is an open set $U \ni \Gamma$ of games on which $|\rho(\Gamma) - \rho(\Gamma')| \le \varkappa_\Gamma \|\Gamma - \Gamma'\|^\gamma$ for some constant $\varkappa_\Gamma > 0$.

Formalization targets

Goal: Theorem 8b)

For every game $\Gamma \in \mathcal G(G,K,S)$ and every $\gamma > 0$,

$$\neg\,\exists\, \varkappa > 0\ \ \forall \Gamma' \in \mathcal G(G,K,S):\ |\rho(\Gamma) - \rho(\Gamma')| \le \varkappa\, \|\Gamma - \Gamma'\|^\gamma,$$

that is, the whole game space is never a $\gamma$-neighborhood: Hölder continuity of $\rho$ holds at best locally, even with a constant depending on the game.

Milestones

1. $\rho(\Psi_\upsilon(\Gamma)) = \rho(\Gamma)$ for $\upsilon > 0$ (§3.5).
2. $\|\Psi_\upsilon(\Gamma) - \Psi_\upsilon(\Gamma')\| = \|\Gamma - \Gamma'\|/\upsilon$ when $d = d'$ (3.11).
3. Some demand vector carries two games with different PoA (p. 24).
4. Theorem 8a): no $\gamma > 0$, $\varkappa > 0$ make $\rho$ uniformly Hölder continuous on $\mathcal G(G,K,S)$.
5. $\rho$ is unbounded on the demand slice $\{\Gamma' : d' = d\}$ whenever $d$ is supported on a single O/D pair (p. 25, corrected; see below).

Significance

Theorem 8 separates what can be proved about the sensitivity of the PoA from what cannot. Part a) rules out uniform Hölder (in particular Lipschitz) bounds; part b) rules out global bounds even with a game-dependent constant. Together they explain the shape of the paper's positive results (Theorems 9 and 12), which hold on balls around a game with constants that depend on that game.

The result is proved in the paper; no machine-checked version exists. Formalizing it fixes the exact hypotheses under which it holds. Two are not visible on the page: paths must form an antichain (otherwise $\rho \equiv 1$ is possible), and the unboundedness step of part b) does not hold on every demand slice. The milestones on cost normalizations are reusable for any scale-invariance argument about the PoA.

Difficulty

The invariance and scaling milestones are bookkeeping about suprema and infima. The substance is in the constructions. For 8a), two games with equal demands and different PoA are needed, which requires an explicit game whose Wardrop equilibrium is strictly inefficient on an arbitrary network satisfying Condition 1 and the antichain condition, so the WE cost and the SO cost must be computed or bounded, not just estimated asymptotically.

For 8b), the paper argues that a global Hölder bound makes $\rho$ bounded on the demand slice of $\Gamma$, and that $\rho$ is unbounded there because the slice contains Pigou-like games. The second step fails in general: with several O/D pairs, other pairs can be forced through the arcs that distinguish the paths of every pair, and on such a slice $\rho$ can be bounded (an explicit three-pair network with $\rho \le 5/2$ on the slice $d = (1,1,1)$ is recorded in the milestone). The natural repair compares $\Gamma$ with games on a different slice, whose demand sits on one pair, and requires bounding the distance between games with different demands as the costs are normalized away.

Formalization scope

Lean represents paths as $0/1$ columns of an arc–path incidence matrix and pairs as a map from paths to pairs, on top of the published KellyStochasticNetworks_Wardrop definitions (arc flows, feasible flows, Wardrop's first principle). The commitments are:

• the standing assumptions are G1–G2 (non-empty $K$, non-empty paths), $0/1$ incidences and Condition 1;
• the antichain condition (no path of a pair inside another path of the same pair) is an added hypothesis of every theorem. It holds for loop-free paths of a digraph, which the paper assumes;
• costs are real functions whose properties are required on $[0,\infty)$ only;
• $C^*$ is an infimum over all flows and $\tilde C$ a supremum over WE flows. All WE flows have the same cost;
• the distance uses the sup norm and a supremum over the compact set $A \times [0, \min\{T(d),T(d')\}]$;
• powers are real powers with $\gamma > 0$.

Every game in every statement ranges over the game space. A formalization quantifying over arbitrary pairs $(\tau, d)$ would be trivial: Lean's $0/0 = 0$ gives such pairs $\rho = 0$, and a junk game next to a real one breaks any Hölder bound for free.

The unboundedness milestone is posed for single-pair demand slices instead of the page's arbitrary slice, because the page's version is false for some multi-pair networks. Its asymptotic rate $\Theta(\beta/\ln\beta)$ is cited by the paper and not posed. Contributions of the two constructions (a strictly inefficient game for 8a, Pigou-type games on one pair for 8b) and of the distance estimates are welcome; related Pigou statements exist as SelfishRouting.Linear.figure_3_pigou (Roughgarden–Tardos).

The source is the arXiv preprint v3; the published MOR version is not the cited artifact.

Selected references

• Z. Wu, R. H. Möhring, A sensitivity analysis of the price of anarchy in nonatomic congestion games, Mathematics of Operations Research 48(3), 2023; cited as arXiv:2007.13979v3 (2021). https://arxiv.org/abs/2007.13979v3
• T. Roughgarden, É. Tardos, How bad is selfish routing?, Journal of the ACM 49(2), 2002. https://doi.org/10.1145/506147.506153
• T. Roughgarden, The price of anarchy is independent of the network topology, Journal of Computer and System Sciences 67(2), 2003. https://doi.org/10.1016/S0022-0000(03)00044-8

Motivation

The price of anarchy (PoA) of a nonatomic congestion game is the ratio between the total travel cost at a Wardrop equilibrium, where every traveller uses a cheapest route, and the minimum total cost a central planner could achieve. Worst-case bounds on the PoA are classical (Roughgarden and Tardos, 2002), but traffic studies observe that the empirical PoA is close to $1$ both in light and in heavy traffic (Youn, Gastner and Jeong, 2008; O'Hare, Connors and Watling, 2016). This raises the question of how the PoA of a fixed network with fixed cost functions behaves as the demand varies.

For decreasing demand the literature had one convergence result: for polynomial costs, Colini-Baldeschi, Cominetti, Mertikopoulos and Scarsini (2020) show $\rho \to 1$ when the total demand tends to $0$ with fixed demand proportions, at rate $O(T(d))$. Wu and Möhring (2021) obtain a rate for arbitrary cost functions that are strictly positive and Lipschitz near $0$, with no condition on the demand proportions, as a corollary of their sensitivity analysis of the PoA. This mission formalizes that corollary, Corollary 5.1 of arXiv:2007.13979v3.

Setting

A structure consists of a finite set $A$ of arcs, a finite nonempty set $\mathcal K$ of origin–destination (O/D) pairs, and for every pair $k$ a set $\mathcal S_k$ of at least two paths, each a nonempty set of arcs; every arc lies on some path. A game $\Gamma = (\tau, d)$ is a vector of arc cost functions $\tau_a : [0,\infty) \to [0,\infty)$, continuous and non-decreasing, together with demands $d_k \ge 0$ of total $T(d) = \sum_k d_k$. The game space $\mathcal G(G, \mathcal K, \mathcal S)$ consists of the games with $T(d) > 0$ and $\tau_a(x) > 0$ on $(0, T(d)]$.

A flow $f = (f_s)$ routes $d_k$ over $\mathcal S_k$ with $f_s \ge 0$. Arc flows are $f_a = \sum_{s \ni a} f_s$ and the total cost is $C(\Gamma, f) = \sum_a f_a \tau_a(f_a)$. A flow is a Wardrop equilibrium if every used path is a cheapest path of its pair. With $\mathcal C^*(\Gamma)$ the minimum total cost and $\tilde{\mathcal C}(\Gamma)$ the cost of a Wardrop equilibrium (all equilibria have the same cost),

$$\rho(\Gamma) = \frac{\tilde{\mathcal C}(\Gamma)}{\mathcal C^*(\Gamma)} \ge 1.$$

Games are compared by the distance (3.3),

$$\|\Gamma - \Gamma'\| = \max\Big\{\|d - d'\|_\infty,\ \max_{a,\ x \in [0, \min\{T(d), T(d')\}]} |\tau_a(x) - \sigma_a(x)|,\ \|\tau(T(d)) - \sigma(T(d'))\|_\infty\Big\},$$

and the demand normalization $\Lambda_\upsilon(\tau, d) = (\tau \circ \upsilon, d/\upsilon)$, with $(\tau_a \circ \upsilon)(x) = \tau_a(x\upsilon)$, rescales a game to a different total demand. The cost slice of $\tau$ is the set of games whose costs agree with $\tau$ on $[0, T(d)]$.

Formalization targets

Goal: Corollary 5.1 (p. 43)

Let the costs $\tau_a$ be strictly positive on $[0,\infty)$ and Lipschitz on $[0, b]$ with constant $M_\tau > 0$, and let $\tau_{\min}(0) = \min_a \tau_a(0)$. There is $\delta > 0$ such that for every demand vector $d \ge 0$ with $0 < T(d) < \delta$,

$$\rho(\tau, d) \le 1 + \frac{8 \cdot |A| \cdot (|\mathcal K| + 1)}{\tau_{\min}(0)} \cdot M_\tau \cdot T(d).$$

Milestones

1. §3.5, p. 22. $\Lambda_\upsilon$ preserves the game space, maps WE and SO flows to WE and SO flows (divided by $\upsilon$), scales the total cost by $1/\upsilon$, and leaves $\rho$ unchanged.
2. p. 43, first display. With $\sigma_a \equiv \tau_a(0)$ and $\Gamma' = (\sigma, d/T(d))$: $\|\Gamma' - \Lambda_{T(d)}(\tau, d)\| = \max_a |\tau_a(T(d)) - \tau_a(0)| \le M_\tau T(d)$ when $T(d) \le b$.
3. p. 43. $\mathcal C^*(\Gamma') \ge \tau_{\min}(0)$ for every $d$.
4. p. 43, second display. For $T(d)$ below a threshold independent of $d$: $\rho(\Gamma') = 1$ and $|\rho(\Lambda_{T(d)}(\tau,d)) - \rho(\Gamma')| \le 8|A|(|\mathcal K|+1) M_\tau T(d)/\tau_{\min}(0)$.

Significance

The corollary gives a rate of convergence of the PoA to $1$ in light traffic for every cost vector that is strictly positive at $0$ and Lipschitz near $0$, with an explicit constant depending only on the number of arcs, the number of O/D pairs, the Lipschitz constant and the free-flow costs $\tau_a(0)$. It removes the fixed-proportion condition on the demands needed in the earlier polynomial result, and it combines with the heavy-traffic results for regularly varying costs to show that the PoA is bounded on whole cost slices (p. 43).

The result is proved in the paper, in a few lines on top of the local Lipschitz estimate (4.33) of Theorem 12a). To our knowledge it has no machine-checked proof. Formalizing it requires a Lean model of nonatomic congestion games with demand normalizations and the metric (3.3), together with the comparison between a game of total demand $1$ and the constant-cost game at the same demand, which is reusable for other light-traffic statements.

Difficulty

A direct bound $\rho(\tau, d) \le 1 + c\,T(d)$ cannot simply be read off as $T(d) \to 0$: the costs $\mathcal C^*$ and $\tilde{\mathcal C}$ both tend to $0$ with the demand, so their ratio is a quotient of two vanishing quantities, and an additive estimate on each cost says nothing about the ratio. The difficulty is to obtain a bound in which neither the threshold on $T(d)$ nor the constant depends on the demand vector $d$, including the proportions $d_k/T(d)$, which may vary arbitrarily, and some of which may vanish. Any argument whose constants depend on the particular game near which it works (as a pointwise Hölder constant does) gives only a pointwise statement, not the uniform one asserted here.

Formalization scope

The Lean development lives in the namespace SensitivityPoA.SmallDemand and builds on the published definition KellyStochasticNetworks_Wardrop (flows, arc flows, Wardrop's first principle). Conventions:

• The structure is a 0/1 arc–route incidence matrix with a map from routes to O/D pairs. Standing assumptions (disclosed): every route contains an arc, $\mathcal K$ is nonempty, and Condition 1 (every arc on some route, $|\mathcal S_k| \ge 2$). Routes are arbitrary 0/1 columns, a generalization of loop-free paths.
• Cost functions are functions $\mathbb R \to \mathbb R$ that are continuous, non-decreasing and non-negative on $[0,\infty)$. "Strictly positive" means $\tau_a(x) > 0$ for all $x \ge 0$. "Lipschitz on $[0,b]$ with constant $M_\tau$" means $|\tau_a(x) - \tau_a(y)| \le M_\tau |x-y|$ for $x, y \in [0,b]$; nothing is assumed beyond $b$.
• $\mathcal C^*$ is the real infimum of the total cost over flows, $\tilde{\mathcal C}$ the real supremum over WE flows, $\rho$ their quotient. The maxima in (3.3) are real suprema of images of compact sets and Mathlib's sup norm.
• The corollary is stated for the game $(\tau, d)$ itself; games of the cost slice agree with it on $[0, T(d)]$.
• Corrected slip. The corollary prints the constant $8 \cdot M_\tau \cdot |A| \cdot (|\mathcal K|+1)/\tau_{\min}(0) \cdot M_\tau$, with $M_\tau$ twice. The display it summarizes has $M_\tau$ once, which is what is posed; it implies the printed form whenever $M_\tau \ge 1$.

A trivializing formalization is ruled out: the threshold $\delta$ is chosen before $d$ (choosing it after $d$ makes the statement vacuous), $T(d) > 0$ is required (at $T(d) = 0$ Lean's $0/0 = 0$ would make $\rho = 0$), every game considered lies in the game space, and the bounds use $\le$, which holds at equality cases.

Contributions welcome: proofs of the milestones, the comparison of WE costs under pointwise cost perturbation (the variational inequality of Wardrop equilibria), and existence of Wardrop equilibria for costs that are continuous and monotone only on $[0,\infty)$. The source is the arXiv preprint v3; the published version in Mathematics of Operations Research is not the cited artifact.

Selected references

• Z. Wu, R. H. Möhring, A sensitivity analysis of the PoA in non-atomic congestion games, arXiv:2007.13979v3, 2021; published as A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games, Mathematics of Operations Research 48(3), 2023. https://arxiv.org/abs/2007.13979 , https://doi.org/10.1287/moor.2022.1292
• R. Colini-Baldeschi, R. Cominetti, P. Mertikopoulos, M. Scarsini, When is selfish routing bad? The price of anarchy in light and heavy traffic, Operations Research 68(2), 2020. https://doi.org/10.1287/opre.2019.1894
• T. Roughgarden, É. Tardos, How bad is selfish routing?, Journal of the ACM 49(2), 2002. https://doi.org/10.1145/506147.506153
• H. Youn, M. T. Gastner, H. Jeong, Price of anarchy in transportation networks: efficiency and optimality control, Physical Review Letters 101, 2008. https://doi.org/10.1103/PhysRevLett.101.128701
• S. J. O'Hare, R. D. Connors, D. P. Watling, Mechanisms that govern how the price of anarchy varies with travel demand, Transportation Research Part B: Methodological 84:55–80, 2016 (cited in arXiv:2007.13979v3, p. 50).

Motivation

The RangeDivisor problem asks whether an integer has a divisor in a specified short interval. It is the decision problem connecting number theory to the two item periodic joint replenishment model studied by Schulz and Telha. Their Appendix starts with Partition, the problem of splitting a list of positive integers into two groups of equal sum, and constructs a RangeDivisor instance from primes chosen near carefully scaled powers of two. The equivalence between the two yes instances is the mathematical target here. Schulz and Telha, Appendix, pp. 16–17

The route has a history. Karp included Partition among classical combinatorial decision problems in 1972. Shor discussed an NP complete variant of factoring in 2011, and Schulz and Telha adapted that connection to their joint replenishment setting. The paper cites a 2016 conditional short interval result of Dudek, Grenié, and Molteni to obtain primes that can be sampled near the requested powers. That prime existence claim motivates the reduction, while this mission starts with primes satisfying the specified windows. Karp, 1972 Shor, 2011 Schulz and Telha, p. 16

Setting

A Partition input is an indexed list $a_1,\ldots,a_n$ of natural numbers. It is a yes instance if some index set $S$ has $2\sum_{i\in S}a_i=\sum_i a_i$. Indices matter: equal entries may occur more than once and can be assigned separately. For this reduction, $n\ge1$, $B\ge1$, and each entry lies in $[2^B,2^{B+1})$. The total is assumed even. Write $A=\frac12\sum_i a_i$, so $A$ is then an integer even though its Lean definition is real valued. Schulz and Telha, Appendix, p. 16

Set $\lambda=3B/2^B$ and $b_i=\lambda a_i$. The input also includes a real constant $c$ and a prime $p_i$ for each index. Every prime lies in the open interval

$$2^{b_i}-cb_i2^{b_i/2}<p_i<2^{b_i}+cb_i2^{b_i/2},$$

and the paper's quantitative small window condition $cb_i<\lambda2^{b_i/2}/(4n)$ holds for every $i$. Define $M=\prod_i p_i$, $L=2^{\lambda(A-1/2)}$, and $U=2^{\lambda(A+1/2)}$. The RangeDivisor instance uses the integer endpoints $\lceil L\rceil$ and $\lfloor U\rfloor$. A valid instance $(M,L',U')$ has $0<L'\le U'\le M$ and $L'+U'<2\sqrt{2L'U'}$; it is a yes instance if some divisor of $M$ belongs to $[L',U']$. These conditions are part of the target, not conventions left to the reader. Schulz and Telha, pp. 12, 15–17

Formalization targets

Appendix reduction

The goal states the full correctness of the rounded numerical construction. Under the prime windows above and the paper's condition $2^{\lambda/2}+2^{-\lambda/2}<2\sqrt2$, the triple $(M,\lceil L\rceil,\lfloor U\rfloor)$ is a valid RangeDivisor instance and

$$M\text{ has a divisor in }[\lceil L\rceil,\lfloor U\rfloor] \quad\Longleftrightarrow\quad (a_i)_{i=1}^n\text{ admits an equal sum partition}.$$

The milestones follow the Appendix's stated intermediate claims: the elementary power estimate, the chain of prime windows, the equivalence for a subset sum and its subproduct, the unrounded divisor equivalence, the numerical interval condition, and the paper's rounding assertion. The unrounded equivalence is a separate milestone because it isolates the number theoretic claim from the integer endpoint convention. Schulz and Telha, pp. 15–17

Significance

The result turns equal sum partitions into divisors in a controlled interval of a product of primes. This is the first mathematical half of the paper's route from Partition to the periodic joint replenishment decision problem; Lemma 3 supplies the second half. The present theorem identifies exactly which numerical statements that route needs, including validity of the rounded interval. Without the equivalence, the constructed integer might have a divisor in the interval for reasons unrelated to the original Partition input. Schulz and Telha, §3 and Appendix

The paper proves its reduction on paper. This mission asks for machine checked proofs of the reduction's arithmetic assertions, not a new complexity result. The reusable pieces are finite product bounds for real powers, the description of divisors of a finite prime product as subproducts, and a rounding result for the RangeDivisor side condition. Such pieces can support other reductions that encode additive choices by products of nearby primes.

Difficulty

The prime bounds are stated one index at a time, while a divisor of $M$ may combine any number of factors. Controlling the product through a strict interval must account for every subset size, including the empty subset and repeated primes. The converse has an additional discrete issue: a product close to the target power should correspond to the exact integer half sum, not merely to a nearby real value. After that, changing real endpoints to integer endpoints must preserve both the divisor question and the numerical promise required by RangeDivisor. A statement only about divisors in the unrounded interval leaves the eventual decision instance incomplete.

Formalization scope

Lean represents inputs as functions Fin n → ℕ, index subsets as finite sets, primes with Nat.Prime, and exponents and interval endpoints in the real numbers. The real powers use real exponentiation; $A$ uses real division, not truncated natural division. The general Partition and RangeDivisor predicates are separate definitions. The Appendix's $\lambda$, $b_i$, $L$, and $U$ are derived definitions of the particular input, so a theorem cannot choose convenient values for them. Strict window inequalities remain strict, and the goal retains the printed sampling window rather than assuming only the later multiplicative bound. It explicitly asserts the rounded instance condition as well as the yes instance equivalence.

The printed converse needs an even total: if the total is odd, $A$ is half integral and a subset one half unit away can produce a product inside $(L,U)$ without being a Partition solution. A computational reduction can send an odd total to a fixed no instance; this theorem covers the nontrivial even branch. The prose condition that $B$ is sufficiently large is replaced by the paper's displayed inequality $cb_i<\lambda2^{b_i/2}/(4n)$, and the printed endpoint condition is stated directly. The proof must not gain a vacuous equivalence by allowing zero indices, by selecting the primes existentially to fit the answer, or by dropping the sampled prime windows.

This mission formalizes the correctness of the reduction behind Theorem 2; polynomial running time, randomized prime sampling, the conditional prime count, the padding of arbitrary Partition inputs to a fixed bit range, and the NP hardness assertion are outside its Lean statement. The Riemann hypothesis is needed by the paper to justify finding suitable primes efficiently, not as an assumption of the arithmetic equivalence once those primes are given. Contributions that establish the product, divisor, or rounding milestones are welcome. Schulz and Telha, pp. 15–17

Selected references

• A. S. Schulz and C. Telha, Integer Factorization: Why Two-Item Joint Replenishment Is Hard, Operations Research, 2024; the formalization uses arXiv:2007.09045v1 (2020), Appendix, pp. 16–17.
• R. M. Karp, Reducibility Among Combinatorial Problems, in Complexity of Computer Computations, 1972. DOI.
• P. W. Shor, An NP-complete variant of factoring, 2011. Original post cited by the paper.
• A. W. Dudek, L. Grenié, and G. Molteni, Primes in explicit short intervals on RH, International Journal of Number Theory 12(5), 2016, 1391–1407; cited in Schulz and Telha, p. 16.

Motivation

Fair division of indivisible goods asks how to split a set of items among agents with different tastes so that nobody has a strong reason to complain. Fairness notions such as envy-freeness up to any good (EFX) and the maximin share (MMS) have been studied extensively as algorithmic targets: given the agents' valuations, compute an allocation satisfying the notion. In practice the valuations are private, and an agent may misreport them to obtain a better bundle. Truthful mechanisms are too weak for this setting: for two agents, no truthful mechanism without payments produces EFX (or even EF1) allocations when there are more than four goods (Amanatidis, Birmpas, Christodoulou, Markakis, EC 2017).

Amanatidis, Birmpas, Fusco, Lazos, Leonardi and Reiffenhäuser (arXiv:2109.08644, Mathematics of Operations Research 2024) take a different route. They let agents bid strategically and ask how fair the pure Nash equilibria of a non-truthful mechanism are with respect to the agents' true valuations. For two agents they study a modified version of the classical cut-and-choose protocol, due in this form to Plaut and Roughgarden (SIAM J. Discrete Math. 2020). They show that it always has equilibria and that all of them are MMS, and hence EFX. As an algorithm run on truthful values, the same mechanism guarantees no more than a $5/6$ fraction of the maximin share.

Setting

There are two agents $N=\{1,2\}$ and a set $M=\{g_1,\dots,g_m\}$ of $m$ indivisible goods. Agent $i$ has a non-negative value $v_i(g)$ for each good and values a bundle $S\subseteq M$ additively, $v_i(S)=\sum_{g\in S}v_i(g)$. There is no free disposal, so an allocation $(A_1,A_2)$ is a partition of $M$.

• EFX (Definition 2.1): for all $i,j$ and every good $g\in A_j$ with $v_i(g)>0$, $v_i(A_i)\ge v_i(A_j\setminus\{g\})$.
• Maximin share (Definition 2.3): $\mu_i=\max_{(X_1,X_2)}\min\{v_i(X_1),v_i(X_2)\}$, the maximum over partitions of $M$ into two bundles. An allocation is MMS if $v_i(A_i)\ge\mu_i$ for both agents.
• Bids: each agent reports a bid vector $\mathbf b_i\in\mathbb R^m_{\ge0}$, and $\mathbf b_i(S)=\sum_{h\in S}\mathbf b_i(h)$.
• Pure Nash equilibrium (Definition 2.7): a bid profile $\mathbf b$ is a PNE of a mechanism $\mathcal M$ if no agent $i$ has a bid $\mathbf b'_i\in\mathbb R^m_{\ge0}$ with $v_i(\mathcal M(\mathbf b'_i,\mathbf b_{-i}))>v_i(\mathcal M(\mathbf b))$.

Mod-Cut&Choose (Mechanism 2) works as follows:

1. It sorts the goods in non-increasing order of agent 1's bid, breaking ties by index.
2. It builds two bundles $E_1,E_2$ greedily: each good goes to the bundle with the smaller $\mathbf b_1$-value, ties to $E_1$.
3. Agent 2 receives the bundle with the larger $\mathbf b_2$-value (ties to $E_1$), and agent 1 receives the other.

In the Lean development these objects are val, IsBestResponse, IsPNE and rank (namespace StrategicAlloc.RRFair, shared with the sibling missions) and IsEFX, mu, IsApproxMMS, cut and modCutChoose (namespace StrategicAlloc.CutChoose).

Formalization targets

Goal: Theorem 4.3 (p. 18)

For every instance with two agents and non-negative additive valuations,

$$\exists\,\mathbf b:\ \mathbf b\text{ is a PNE of Mod-Cut\&Choose},\qquad\text{and}\qquad \forall\,\text{PNE }\mathbf b:\ \mathcal M(\mathbf b)\text{ is MMS and EFX w.r.t. } v_1,v_2 .$$

Both halves are part of the goal. Existence alone, or fairness of equilibria alone, is a weaker statement.

Milestones

1. Theorem 2.5 (p. 5): for two agents every MMS allocation is EFX.
2. §2.1, p. 5: $n\cdot\mu_i(n,S)\le v_i(S)$. This is the published open statement LittleCharity.MMS.mms_le_average, used here as a reference.
3. Lemma 4.1 (p. 17): for every partition $(X_1,X_2)$ of $M$, agent 1 has a non-negative bid under which the cut is $\{E_1,E_2\}=\{X_1,X_2\}$.
4. Corollary 4.2 (p. 18): agent 1 can force a $\mu_1$-partition, i.e. a cut with $\min\{v_1(E_1),v_1(E_2)\}=\mu_1$.
5. Proof of Theorem 4.3, p. 18: agent 2's truthful bid is a best response to every bid of agent 1.
6. Proof of Theorem 4.3, p. 18: with her truthful bid, agent 2 receives at least $v_2(M)/2$.

Significance

The theorem identifies a simple mechanism whose strategic outcomes are as fair as the best allocations that exist for two agents: every MMS allocation is EFX, and an MMS allocation always exists for two agents. The mechanism achieves this without any truthfulness requirement. It is the positive counterpart to the impossibility results for truthful mechanisms. It is also the starting point of §4.2 of the same paper, which asks how much of this guarantee survives for every mechanism whose equilibria are always EFX (Theorems 4.5 and 4.7).

The result is proved in the paper. As far as the platform's catalogue shows, none of it is formalized. This mission produces:

• a machine-checked model of strategic fair division with bids, in which deviations range over all non-negative real bid vectors;
• an executable definition of Mod-Cut&Choose with its exact tie-breaking;
• formal proofs of the "agent 1 can force any cut" lemma and of MMS ⇒ EFX for two agents.

Difficulty

The fairness half is short once its ingredients are available. The weight lies in Lemma 4.1: the cut phase is a greedy procedure over a bid-sorted order, and showing that every partition of $M$ can be produced requires explicit bids and an invariant along the greedy loop. The case where both sets have at least two goods needs carefully calibrated values. The tie-breaking rules (lexicographic sorting, ties to $E_1$ in both phases) enter the argument, and the formalization fixes them exactly.

A natural shortcut is to restrict agent 1's strategies to orderings of the goods, or to assume that any cut is reachable. Either one turns Lemma 4.1 into an assumption. The existence half needs no compactness argument: the set of possible cuts is finite, so a best cut for agent 1 exists, but this has to be connected with deviations over the continuum of real bid vectors.

Formalization scope

• Agents are Fin 2 (agent 1 is 0) and goods are Fin m, indexed in the order $g_1,\dots,g_m$ that lexicographic tie-breaking refers to.
• Valuations and bids are functions Fin 2 → Fin m → ℝ. Non-negativity of $v$ is a hypothesis of every theorem, and every bid in a profile or deviation is required to be non-negative.
• mu v i reuses the published LittleCharity.MMS.mms with two bundles and $S=M$.
• EFX is the paper's Definition 2.1, which removes only goods of positive value. The every-good variant LittleCharity.MMS.IsEFX is not used.
• Disclosed correction: line 2 of Mechanism 2 on the page sorts "w.r.t. $v_1$". A mechanism reads only bids, and the proof of Lemma 4.1 sorts by the declared bids, so the formal mechanism sorts by agent 1's bid $\mathbf b_1$.

The statements rule out the trivializing formalizations. Deviations are not restricted to a subset of bids (rankings, truthful bids, a finite menu). MMS and EFX are measured with the true valuations, never with the bids. The mechanism's tie-breaking is fixed rather than arbitrary.

A complete development needs basic finite-sum and finite-supremum facts and a proof that the greedy cut covers $M$ with disjoint bundles. The model layer (val, IsEFX, IsPNE over all non-negative bids) is shared with the four sibling missions on Round-Robin and on mechanisms with EFX equilibria. Proofs of any milestone, and of mms_le_average, are welcome.

Selected references

• G. Amanatidis, G. Birmpas, F. Fusco, P. Lazos, S. Leonardi, R. Reiffenhäuser, Allocating Indivisible Goods to Strategic Agents: Pure Nash Equilibria and Fairness, Mathematics of Operations Research, 2024; arXiv:2109.08644v2. https://arxiv.org/abs/2109.08644
• B. Plaut, T. Roughgarden, Almost Envy-Freeness with General Valuations, SIAM Journal on Discrete Mathematics 34(2), 2020. https://doi.org/10.1137/19M124397X
• I. Caragiannis, D. Kurokawa, H. Moulin, A. D. Procaccia, N. Shah, J. Wang, The Unreasonable Fairness of Maximum Nash Welfare, ACM Transactions on Economics and Computation 7(3), 2019. https://doi.org/10.1145/3355902
• G. Amanatidis, G. Birmpas, G. Christodoulou, E. Markakis, Truthful Allocation Mechanisms Without Payments: Characterization and Implications on Fairness, EC 2017. https://doi.org/10.1145/3033274.3085147

Why the two-item periodic JRP is hard

The joint replenishment problem (JRP) is the multi-item extension of the economic order quantity (EOQ) model. Each item is reordered periodically and pays its own ordering and holding costs, and a joint ordering cost is shared by items ordered at the same time. Before this work no hardness result was known for the periodic JRP (p. 10), even though no exact polynomial-time algorithm was known either (Schulz and Telha, arXiv:2007.09045; Operations Research, 2024, as Integer Factorization: Why Two-Item Joint Replenishment Is Hard).

The paper explains this through number theory. In the periodic JRP the joint cost is incurred every $\gcd(q_1, q_2)$ periods, so the objective contains a greatest common divisor of the decision variables. The paper's Theorem 2 states that, assuming the Riemann hypothesis, the two-item periodic JRP is NP-hard under randomized reductions. The proof composes two reductions:

• Shor's reduction from Partition to RangeDivisor ("does $M$ have a divisor in $[L, U]$?"), given in the paper's appendix and based on Shor (2011); this is where the Riemann hypothesis enters;
• a reduction from RangeDivisor to the two-item periodic JRP, whose correctness is Lemma 3 (pp. 13–14).

This mission formalizes Lemma 3. Mission 4 of this series formalizes the Partition half; missions 1 and 2 formalize the integer-factorization reductions behind Theorem 1.

Setting

A period is a positive integer $q$. An item with ordering cost $K$ and holding cost $H$ costs

$$\mathrm{EOQ}_{K,H}(q) = \frac{K}{q} + Hq$$

per unit time. The two-item periodic JRP (objective (3), p. 10) minimizes, over $q_1, q_2 \in \mathbb{Z}_+$,

$$\mathrm{JRP}(q_1, q_2) = \mathrm{EOQ}_{K_1,H_1}(q_1) + \mathrm{EOQ}_{K_2,H_2}(q_2) + \frac{K_0}{\gcd(q_1, q_2)}.$$

As a decision problem (p. 13), it asks whether some $(q_1, q_2)$ has cost at most a threshold $z$.

An instance of RangeDivisor (p. 12) is a triple of integers $M \ge U \ge L > 0$ satisfying

$$L + U < 2\sqrt{2LU};$$

it is a yes-instance when $M$ has a divisor $q$ with $L \le q \le U$.

Given such a triple, the instance $\mathrm{JRP}_{M,U,L}$ sets

$$K_0 = LU,\quad K_1 = 0,\quad H_1 = 1,\quad K_2 = M^3(M+1),\quad H_2 = M(M+1),$$

and the threshold is $z_{M,L,U} = L + U + 2M^2(M+1)$, where $2M^2(M+1) = \mathrm{EOQ}_{K_2,H_2}(M)$. Once item 2 is fixed at $q_2 = M$, item 1 solves problem (5):

$$\min_{q_1 \in \mathbb{Z}_+} \ \frac{LU}{\gcd(q_1, M)} + q_1 .$$

In Lean these objects are JRPHard.Aperiodic.eoq, JRPHard.Periodic.periodicCost, JRPHard.Periodic.coefK2, JRPHard.Periodic.coefH2 (shared with missions 1 and 2), and IsRangeDivisorInstance, HasDivisorIn, coefK0, rangeCost, threshold, obj5 and fConv in the namespace JRPHard.RangeDiv.

Formalization targets

Goal: Lemma 3

For every RangeDivisor instance $(M, L, U)$,

$$K_0,\ K_2,\ H_2 \le 2M^4 \quad\text{and}\quad \Big(\exists\, q \mid M,\ L \le q \le U\Big) \iff \Big(\exists\, q_1, q_2 \in \mathbb{Z}_+:\ \mathrm{JRP}_{M,U,L}(q_1, q_2) \le L + U + 2M^2(M+1)\Big).$$

Milestones (the steps of the proof, pp. 14–15)

1. Item 2 is pinned: every plan with $q_2 \ne M$ costs more than $z_{M,L,U}$.
2. $f(q) = LU/q + q$ is a lower bound on problem (5)'s objective, $f(L) = f(U) = L + U$, and $f$ is minimized at $\sqrt{LU}$.
3. $\gcd(q, M) \ne q \Rightarrow \gcd(q, M) \le q/2$.
4. If $\gcd(q, M) \ne q$, the objective of (5) at $q$ is at least $2\sqrt{2LU} > L + U$.
5. A divisor $q \in [L, U]$ of $M$ has objective at most $L + U$.
6. A period with objective at most $L + U$ divides $M$ and lies in $[L, U]$.

Significance

Lemma 3 is the step that carries hardness from number theory to inventory theory. With Shor's result it shows that, under the Riemann hypothesis, no polynomial-time exact algorithm for the two-item periodic JRP exists unless NP problems can be solved in randomized polynomial time. The paper concludes (p. 15) that no algorithm for the two-item problem may be simultaneously exact and polynomial on all inputs, so some concession, such as heuristics, must be made.

The result is proved in the paper; it has not been machine-checked. The mission produces a checked statement of the reduction's correctness with every coefficient explicit, and it corrects two imprecisions in the printed lemma (the threshold and the unspecified "sufficiently large" coefficients of item 2; see below). The objects (eoq, periodicCost) are the same ones used in mission 2 of this series.

Difficulty

Each step is elementary, but the statement mixes integer and real reasoning. The objective of (5) is not monotone or convex in $q$: its value jumps between $LU/q + q$ at divisors of $M$ and at least $2LU/q + q$ elsewhere. The argument must show that the gap between these two curves exceeds the window around $L + U$, and this is exactly what RangeDivisor's condition $L + U < 2\sqrt{2LU}$ provides. Without that condition a non-divisor can be cheaper than $L + U$ (for $L = 1$, $U = 100$, $M = 7$, the period $q = 14$ has objective $100/7 + 14 < 101$). The pinning of $q_2 = M$ also has to beat the slack $M + 2\sqrt{LU}$ against $L + U$, which is where $M \ge U$ is used.

Formalization scope

This mission formalizes the correctness of the reduction behind Theorem 2 (its JRP half, Lemma 3); polynomial running time is not formalized. Theorem 2 itself, Shor's NP-completeness of RangeDivisor under randomized reductions, and "one can construct in polynomial time" are not stated. What remains of the polynomial-time claim is the explicit coefficients and the bound $K_0, K_2, H_2 \le 2M^4$ (bit length at most $4\log_2 M + 2$).

Conventions:

• periods are natural numbers, and every quantified period is assumed positive (Lean's $K/0 = 0$ and $\gcd(0, M) = M$ would otherwise create spurious cheap plans);
• costs are real numbers; $L$, $U$, $M$ and the coefficients are natural numbers cast to $\mathbb{R}$;
• RangeDivisor's condition is stated with Real.sqrt exactly as printed;
• "the optimal value is at most $z$" is the decision form "some plan has cost at most $z$" (p. 13); the minimum is attained, so the two agree.

Two disclosed departures from the printed lemma:

• The threshold. The page writes "the optimal value of $\mathrm{JRP}_{M,U,L} \le L + U$". The two-item cost also contains item 2's term $2M^2(M+1)$, so the literal comparison never holds and would make the lemma false. The threshold is $z_{M,L,U} = L + U + 2M^2(M+1)$, the $z_{M,L,U}$ announced in §3.1.
• The item-2 coefficients. The page chooses "sufficiently large values of $K_2$ and $H_2$, as in … Lemma 2". The statement fixes Lemma 2's values $K_2 = M^3(M+1)$, $H_2 = M(M+1)$ rather than quantifying existentially, which would let any instance satisfy the lemma.

A formalization that drops the positivity of periods, states the threshold as $L + U$ on the full two-item cost, or leaves $K_2, H_2$ existential does not capture Lemma 3 and is ruled out.

No library beyond Mathlib (Nat.gcd, Real.sqrt) is needed. Proofs of the milestones, and alternative proofs of the goal, are welcome.

Selected references

• A. S. Schulz and C. Telha, Integer factorization and Riemann's hypothesis: Why two-item joint replenishment is hard, arXiv:2007.09045v1, 2020; published as Integer Factorization: Why Two-Item Joint Replenishment Is Hard, Operations Research, 2024. https://arxiv.org/abs/2007.09045
• P. W. Shor, An NP-complete variant of factoring, Theoretical Computer Science Stack Exchange, 2011 (version 2011-03-01, as cited by the paper). https://cstheory.stackexchange.com/q/4785
• S. Arora and B. Barak, Computational Complexity: A Modern Approach, Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511804090

Motivation

A max-XORSAT instance asks for a binary assignment that satisfies as many parity constraints as possible. A matrix specifies the parity check in each constraint, while a second binary vector specifies the desired parity. The objective can be written as the number of satisfied constraints minus the number violated, so an assignment with a high objective value is also a good approximate solution. Jordan and coauthors study decoded quantum interferometry (DQI), a way to sample candidate assignments by encoding a weighted superposition of error patterns and then decoding their syndromes. Their ideal-state analysis assumes that low-weight errors have distinct syndromes. Real decoders can succeed on many errors even when this uniqueness condition fails, which makes the theorem in this mission relevant to the algorithmic regime beyond the guaranteed decoding radius. Jordan et al., §§8.1 and 10.

The paper's 2024 preprint introduced DQI for linear constraint satisfaction and related optimization problems. Its revised 2025 version studies the effect of decoder failures on the measured objective in Theorem 10.1. This mission uses that revision, arXiv:2408.08292v5, and isolates the first inequality of equation (172). The same section supplies explicit identities for the norm of the postselected state and for its objective matrix, making the theorem a bounded campaign of finite combinatorics and linear algebra. Jordan et al., §10, pp. 35–43.

Setting

Fix integers $m,n\ge0$ and a binary matrix $B\in\mathbb F_2^{m\times n}$. Its $i$th row defines a parity $b_i\cdot x$ of an assignment $x\in\mathbb F_2^n$. For a binary vector $v\in\mathbb F_2^m$, the objective is

$$f_v(x)=\sum_{i=1}^{m}(-1)^{b_i\cdot x+v_i}.$$

An error pattern $y\in\mathbb F_2^m$ has syndrome $B^\top y$ and Hamming weight $|y|$. The weight-$k$ shell $E_k$ contains all errors with $|y|=k$. Choose $0\le\ell\le m$ and real weights $w_0,\ldots,w_\ell$. The ideal syndrome-space state in equation (140) sums $(-1)^{v\cdot y}|B^\top y\rangle$ over each $E_k$, multiplied by $w_k/\sqrt{\binom m k}$. Jordan et al., equations (140) and (171).

A deterministic decoder $\mathrm{dec}:\mathbb F_2^n\to\mathbb F_2^m$ guesses an error from its syndrome. It correctly identifies $y$ when $\mathrm{dec}(B^\top y)=y$. Write $D_k\subseteq E_k$ for the correctly identified errors and $F_k=E_k\setminus D_k$ for the failures. The shell failure rate is $\varepsilon_k=|F_k|/\binom m k$, and $\varepsilon=\max_{0\le k\le\ell}\varepsilon_k$. Postselecting successful decoding leaves the unnormalized state $\widetilde P_D(f)$ formed by replacing each $E_k$ in the ideal state with $D_k$. Apply the binary Hadamard transform, divide by the resulting norm, measure $x$, and evaluate $f_v(x)$. Denote this measured expectation by $\langle f_v\rangle$. Jordan et al., §10.3, pp. 39–40.

Formalization targets

Theorem 10.1: the averaged objective

Let $N=\sum_{k=0}^{\ell}w_k^2(1-\varepsilon_k)$ be the squared norm of the postselected state. The goal, for $N>0$ and uniform $v\in\mathbb F_2^m$, is

$$\mathbb E_v\langle f_v\rangle\ge \frac{w^\top A^{(m,\ell,0)}w-2\varepsilon(m+1)w^\top w}{N}.$$

The matrix $A^{(m,\ell,0)}$ is the symmetric tridiagonal matrix in equation (70): its diagonal is zero and its entries adjacent to the diagonal are $a_k=\sqrt{k(m-k+1)}$. This is the first inequality of (172), with the decoder's actual failure fractions in $N$ and the worst shell failure rate in the correction. It has no minimum-distance hypothesis. Jordan et al., Theorem 10.1, pp. 39–40.

Supporting targets

The milestone list includes the norm identity of Lemma 10.4, the ideal and postselected objective matrices of Lemmas 10.2 and 10.5, the normalized expectation identity in (179), the averaged matrix identities of Lemmas 10.3 and 10.6, and the error-matrix bound of Lemma 10.7. A separate companion item records the second comparison printed in (172) under an explicit sign condition; without that condition, the printed comparison can fail. Jordan et al., §10, pp. 36–43.

Significance

The result assigns a quantitative cost to decoding errors. It says how the measured max-XORSAT objective changes when some error patterns are lost during postselection, while permitting a code whose low-weight errors share syndromes. Consequently the theorem addresses the setting in which practical decoding succeeds often but exact distance-based uniqueness is unavailable. The denominator also records the survival probability of the weighted state, so the bound keeps the actual normalization visible. Jordan et al., §10, pp. 35 and 39–43.

A complete formalization would provide reusable definitions for binary syndrome decoding, shellwise failure rates, real-amplitude states, normalized measurement expectations, and finite objective matrices. The paper proves the result on paper; this mission asks for machine-checked proofs of the stated goal and its milestones. The formal development would also document exactly which part of equation (172) requires an additional sign assumption. No proof is claimed by the draft statements themselves.

Difficulty

When two errors have the same syndrome, the ideal syndrome state can combine their amplitudes, so its norm need not equal $w^\top w$. Postselection changes which errors remain, and the measured objective depends on the normalized state for each $v$. Replacing that normalized expectation with the objective of an average state would change the claim. The proof must keep the decoder fixed while $v$ varies and must control the error matrix uniformly over every real weight vector. The printed second inequality of (172) adds a separate sign issue: a smaller positive denominator reverses the expected comparison when the numerator is negative. Jordan et al., equations (161), (171)–(172), (179)–(182).

Formalization scope

Lean uses ZMod 2 for bits, Fin m and Fin n for zero-based coordinates, functions for binary vectors, and Matrix for $B$. The decoder is one function of the syndrome, independent of $v$. Hamming shells, correct and failed decoding sets, and $\varepsilon_k$ are computed from that function. Weights and amplitudes are real. The postselected state uses the factor $1/\sqrt{\binom m k}$; the Hadamard transform uses $1/\sqrt{2^n}$. The average over $v$ is the sum over all $2^m$ vectors divided by $2^m$. The tridiagonal entries compute $m-k$ in the reals, preserving the square-root formula at the boundary.

Two domain conditions are made explicit. The bound $\ell\le m$ rules out absent weight shells, for which Lean would otherwise assign zero to division by $\binom m k=0$. The condition $N>0$ rules out a zero postselected state, whose normalized expectation would likewise be assigned a meaningless zero by total real division. The goal ranges over every binary matrix, every fixed deterministic decoder, and every real weight vector satisfying those conditions. It states the expectation of the explicit postselected state after a Hadamard transform, rather than an unconstrained expectation variable.

The supporting development needs finite character sums, Hamming-shell cardinalities, matrix quadratic forms, and an operator bound for a symmetric real matrix. These components can serve other finite decoding and quantum-state calculations. Contributions proving the seven cited milestones or the goal are within scope. The circuit's resource accounting, asymptotic equation (173), and numerical decoder studies are outside this mission.

Selected references

• S. P. Jordan, N. Shutty, M. Wootters, A. Zalcman, A. Schmidhuber, R. King, S. V. Isakov, T. Khattar, and R. Babbush, Optimization by Decoded Quantum Interferometry, arXiv:2408.08292v5, 2025 revision of the 2024 preprint. arXiv

Motivation

In the classical secretary problem, candidates arrive one at a time in uniformly random order, and a decision maker must accept or reject each one irrevocably. The decision maker sees exact scores, or at least a total ranking of the candidates seen so far. In hiring, admissions and procurement the observed scores are often biased: evaluations of candidates from different groups, or produced by different evaluators, cannot be compared reliably, even when comparisons inside a group can. Salem and Gupta (SSRN 3444283; Management Science, 2023, doi:10.1287/mnsc.2023.4926) model this by giving the algorithm only the comparisons it can trust. These form a partial order on the candidates, and the true scores remain hidden.

The question is how much is lost when only partial ordinal information is available. The paper's answer is governed by the width of the partial order, the largest number of mutually incomparable candidates. Width 1 is the classical totally ordered problem. Width $N$ means that no comparison is available at all. This mission formalizes the paper's first positive result with explicit constants: an algorithm, ProxyLabel, whose competitive ratio grows linearly in a known estimate of the width.

Setting

A finite set $C$ of $N$ elements carries a partial order $\preceq$. Each element $a$ has a hidden true score $w(a) \ge 0$. The scores are pairwise distinct and consistent with the order: $a \prec b$ implies $w(a) < w(b)$. The width $\omega$ of $(C, \preceq)$ is the largest size of an antichain, a set of pairwise incomparable elements.

The elements arrive in a uniformly random order. The algorithm knows $N$ and a selection capacity $k \ge 1$. At each time it sees the comparisons of $\preceq$ among the elements that have arrived. It may select at most $k$ elements, and every decision is irrevocable. The offline optimum $\mathrm{OPT}$ is the largest total score of at most $k$ elements. An algorithm is $\rho$-competitive if, on every instance,

$$\mathbb E\Big[\frac{w(\mathrm{Alg})}{\mathrm{OPT}}\Big] \ge \frac1\rho,$$

where $w(\mathrm{Alg})$ is the total score of the selected elements and the expectation is over the arrival order and the algorithm's randomness.

ProxyLabel (Algorithm 1 of the paper) takes a width estimate $\omega' \in \mathbb N$. It works as follows.

1. Each element receives a label $\ell(a) \in \{1, \dots, k\}$, uniformly and independently.
2. It draws $m \sim \mathrm{Bin}(N, \omega'/(\omega'+1))$ and lets the sample $S$ be the first $m$ arrivals. Sampled elements are never selected.
3. A later element $a$ is selected if it is maximal among all previously seen elements with its label, sampled or not, and no element with its label has been selected yet.

Each label class therefore contributes at most one element: the first non-sampled one that beats everything of its label seen before.

Formalization targets

Goal: Proposition 5.2

If $\omega' \ge \omega / c$ for some $c \ge 1$, then ProxyLabel has competitive ratio at most

$$\rho = \frac{e^{c}(\omega'+1)}{\big(1 - \frac1k\big)^{k-1}} \ \le\ e^{c+1}(\omega'+1),$$

with the convention $0^0 = 1$. That is, $\mathbb E[w(\mathrm{Alg})] \ge \mathrm{OPT}/\rho$.

Milestones, from the proof (pp. 16–17)

1. Under uniform labels, the $j$-th best element is the maximum of its label class with probability $(1 - 1/k)^{j-1} \ge (1 - 1/k)^{k-1} \ge 1/e$.
2. Display (3): conditional on that event, it is selected with probability at least $\frac{1}{\omega'+1}\big(1 - \frac{1}{\omega'+1}\big)^{\omega}$.
3. If $\omega/c \le \omega'$ with $c \ge 1$, this quantity is at least $1/(e^{c}(\omega'+1))$.
4. Hence each of the top $k$ elements is selected with probability at least $(1 - 1/k)^{k-1}/(e^{c}(\omega'+1))$.
5. $\mathbb E[w(\mathrm{Alg})] \ge \sum_{i=1}^k \mathbb P(a_i \in \mathrm{Alg})\, w(a_i)$ over the top $k$ elements $a_1, \dots, a_k$.

Companion: Corollary 5.1

With the exact width $\omega' = \omega$, the ratio is at most $e(\omega+1)/(1 - 1/k)^{k-1} \le e^2(\omega+1)$, and it is $e(\omega+1)$ for $k = 1$.

Significance

Proposition 5.2 shows that partial ordinal information costs at most a factor linear in the width, provided a width estimate within a constant factor is available. Proposition 5.1 of the same paper shows that no algorithm beats ratio $\omega$, so the bound is order-optimal. ProxyLabel is also the building block of the paper's width-free algorithm PosetLabel (§5.4), which estimates the width from a first sample and then runs ProxyLabel's selection phase.

The result is proved in the paper and has not been machine-checked. A complete development would give a formal model of online selection on a poset under random arrival, with an explicit selection rule and exact finite averages for probabilities. It would also contain a formal use of Dilworth's theorem inside a probabilistic argument, and the elementary inequalities $(1 - 1/k)^{k-1} \ge 1/e$ and $(1 - 1/(\omega'+1))^{\omega} \ge e^{-c}$ in the form the proof needs.

Difficulty

The events of the algorithm are tangled. The sample is a prefix of a random order with a random length. Whether an element is selected depends on everything that arrived before it, on the labels, and on whether an earlier element of the same label was already selected. The bound must be proved for every finite poset and every consistent scoring, with exact constants, on the finite probability space of arrival orders, labellings and sample sizes. The width enters only through the structure of a single label class, a subposet whose width is at most $\omega$, so the argument has to pass from the global width to an arbitrary random subposet.

A tempting simplification lets every passing unsampled element be selected. That algorithm can select several elements of one label, so its expected score is larger and the bound becomes easier. It is not ProxyLabel.

Formalization scope

• Elements are a finite type α with a PartialOrder, so $N$ is Fintype.card α. The width $\omega$ is the published definition AppliedComb.Posets.width α, the maximum size of an antichain. Dilworth's theorem is the published, proved theorem AppliedComb.Posets.dilworth.
• A consistent scoring is $w : \alpha \to \mathbb R$ with $w \ge 0$, $w$ injective, and $a < b \Rightarrow w(a) < w(b)$. These three conditions are the paper's standing assumptions (§3.1, §3.3), not additions.
• Arrival orders are bijections α ≃ Fin N, and labellings are functions α → Fin k. Labels are independent of the order, which is the same distribution as assigning labels on arrival.
• Probabilities and expectations are explicit finite averages with weights $1/N!$, $1/k^N$ and the binomial weights $\binom{N}{m}p^m(1-p)^{N-m}$ with $p = \omega'/(\omega'+1)$.
• The selection rule is encoded exactly. An element is selected iff it is unsampled, no earlier element of its label (sampled or not) is above it, and no earlier unsampled element of its label passed the same test.
• OPT is the maximum of $\sum_{a \in s} w(a)$ over sets with $|s| \le k$, so it is the total score when $k \ge N$.
• The competitive ratio is stated as $\mathrm{OPT}/\rho \le \mathbb E[w(\mathrm{Alg})]$. This agrees with Definition 3.4 when $\mathrm{OPT} > 0$; the page's ratio is undefined when $\mathrm{OPT} = 0$.
• $(1 - 1/k)^{k-1}$ has a natural exponent, so $k = 1$ gives $0^0 = 1$. The width estimate $\omega'$ is a natural number.
• The proposition's "interval order" is a slip of the page: the algorithm and the proof concern arbitrary posets, and the goal is stated for every finite poset.
• The order-optimality clause of Corollary 5.1 refers to Proposition 5.1, the subject of mission II of this series, and is not stated here.
• The goal is a statement about the full expectation of the selected score over arrival order, labels and sample size. It is not the conditional bound (3). A formalization in which several elements per label can be selected, or in which "previously seen" excludes the sample, proves a statement about a different algorithm.

Contributions are welcome on every milestone. The prefix-of-a-random-order lemma (a binomially sized prefix is an i.i.d. Bernoulli sample) is reusable well beyond this mission.

Selected references

• J. Salem and S. Gupta, Secretary Problems with Biased Evaluations Using Partial Ordinal Information, SSRN 3444283 (version of 2022-04-17); Management Science, 2023. https://ssrn.com/abstract=3444283, https://doi.org/10.1287/mnsc.2023.4926
• R. P. Dilworth, A Decomposition Theorem for Partially Ordered Sets, Annals of Mathematics 51(1), 1950, 161–166. https://doi.org/10.2307/1969503
• R. Kleinberg, A Multiple-Choice Secretary Algorithm with Applications to Online Auctions, SODA 2005. https://dl.acm.org/doi/10.5555/1070432.1070519