All missions

Motivation

A queue layout of a graph places its vertices on a line and splits its edges into classes, called queues, so that inside one queue no edge is nested inside another. The minimum number of queues is the queue-number. Queue layouts were introduced by Heath, Leighton and Rosenberg (1992) and Heath and Rosenberg (1992) as the dual of stack layouts (book embeddings): reading the vertex order from left to right, the edges of one queue are opened and closed in first-in first-out order. Queue layouts are closely tied to track layouts and, through them, to three-dimensional grid drawings of graphs (§9 of the paper).

Whether planar graphs have bounded queue-number was asked by Heath, Leighton and Rosenberg in 1992 and stayed open for 27 years. The best general bounds before 2019 grew with the number of vertices: $O(\sqrt n)$ by Heath, Leighton and Rosenberg (1992), $O(\log^2 n)$ by Di Battista, Frati and Pach (2013), and $O(\log n)$ by Dujmović (2015); for Euler genus $g$, Dujmović, Morin and Wood (2017) had $O(g + \log n)$. Dujmović, Joret, Micek, Morin, Ueckerdt and Wood (arXiv:1904.04791, J. ACM 2020) proved that every planar graph has queue-number at most $49$ (Theorem 1), and extended the result to every graph embeddable in a fixed surface (Theorem 2) and to every proper minor-closed class (Theorem 3).

This mission is Theorem 2: graphs of Euler genus $g$ have queue-number at most $4g + 49$. It is the second mission of a two-mission series; the first poses Theorem 1.

Setting

All graphs are finite and simple. A linear ordering $\preceq$ of the vertex set $V(G)$ is fixed. Two edges $vw$ and $xy$ with four distinct ends nest if $v \prec x \prec y \prec w$ (after renaming the ends). A queue is a set of edges no two of which nest. A $k$-queue layout of $G$ is a linear ordering together with a partition of $E(G)$ into $k$ queues, and $\operatorname{qn}(G) \le k$ means that a $k$-queue layout exists.

A layering of $G$ is an ordered partition $(V_0, V_1, \dots)$ of $V(G)$ such that every edge joins two vertices of the same or of consecutive layers. A BFS layering takes one root $r$ in each connected component and puts $v$ in layer $\operatorname{dist}(r, v)$. A BFS spanning tree of a connected graph $G$ rooted at $r$ is a spanning tree $T$ with $\operatorname{dist}_T(r, v) = \operatorname{dist}_G(r, v)$ for every $v$. A path in $T$ is vertical if the distance to $r$ grows by exactly one at every step.

The Euler genus of the orientable surface with $h$ handles is $2h$, and that of the non-orientable surface with $c$ cross-caps is $c$; the Euler genus of a graph is the least Euler genus of a surface it embeds in (footnote 2 of the paper). Planar graphs are exactly the graphs of Euler genus $0$. Combinatorially, an embedding of a graph is described by an embedding scheme: a cyclic order of the edges at each vertex (a rotation system) together with a sign on every edge (twisted or not). Tracing faces through the scheme gives a face count $f$, and with $n$ vertices, $m$ edges and $c$ components the scheme has Euler genus $2c - n + m - f$.

Formalization targets

Goal: Theorem 2 with the paper's bound

$$\text{Euler genus of } G \le g \ \Longrightarrow\ \operatorname{qn}(G) \le 4g + 49 .$$

The paper states Theorem 2 as $\operatorname{qn}(G) = O(g)$ and proves the explicit bound $4g + 49$ in §5. The goal poses that explicit bound, for every finite graph, connected or not.

Milestones

1. Lemma 18 (p. 18). Every BFS layering $(V_0, V_1, \dots)$ of a planar graph $G$ admits a $49$-queue layout whose vertex ordering lists $V_0$, then $V_1$, then $V_2$, and so on.
2. Lemma 21 (p. 19). If $G$ is connected with Euler genus at most $g$ and $T$ is a BFS spanning tree with layering $(V_i)$, there is a connected (or empty) subgraph $Z$ with at most $2g$ vertices in each layer such that $G - V(Z)$ is planar and sits inside a connected planar graph $G^+$ whose own BFS layering $(W_i)$ satisfies $W_i \cap (V(G)\setminus V(Z)) = V_i \setminus V(Z)$; vertical paths of the BFS tree of $G^+$ restrict to vertical paths of $T$.
3. The $4g$-queue step (p. 23). If $G$ has a layering with at most $2g$ vertices of $Z$ per layer and $G - Z$ has a $49$-queue layout ordered layer by layer, then $\operatorname{qn}(G) \le 4g + 49$.

Significance

The result. Theorem 2 settles boundedness of the queue-number for every class of graphs embeddable in a fixed surface, with a bound linear in the Euler genus. Through the connection between queue-number and track-number, the paper derives from it (§9, Theorems 54 and 58) that a graph of Euler genus $g$ with $n$ vertices has track-number $g^{O(g^{4/7})}$ and a three-dimensional grid drawing of volume $g^{O(g^{4/7})} n$, linear in $n$ for every fixed surface. It is also a step on the paper's route to Theorem 3 (proper minor-closed classes), since graphs on surfaces are the basic pieces of the Robertson–Seymour graph minor structure theorem. Lemma 21 is of independent use: it reduces a graph on a surface to a planar graph while controlling BFS layers.

Formalizing it. The result is proved; as far as is known it has no machine-checked proof. A formalization needs queue layouts, layerings, BFS layerings and vertical paths, and, independently of queues, a usable combinatorial theory of graphs on surfaces, which Lean's Mathlib does not have. The Euler genus definition of this mission (embedding schemes and face tracing) and Lemma 21 are reusable well beyond queue layouts.

Difficulty

The obvious reduction, deleting few vertices to make the graph planar, is not enough: a planar subgraph alone does not control how the deleted vertices interact with a queue layout. The deleted set must be thin in every BFS layer, and the planar remainder must carry a BFS layering compatible with the original one, which is what Lemma 21 provides. Its proof cuts the surface along a subgraph made of tree paths and must show that the cut graph is planar by an Euler-characteristic count over face-tracing data, and that distances from a new root agree with the old BFS distances. In Lean, the main obstacle is the surface side: Euler's formula for embedding schemes, the cutting operation on rotation systems, and the passage between the combinatorial notion of Euler genus and the drawing-based notion of planarity. The planar input, Lemma 18, is itself the whole of mission 1's argument (Theorem 15 with Lemmas 5 and 8).

Formalization scope

• Graphs are SimpleGraph V on a finite type V : Type with decidable equality and adjacency.
• "$\operatorname{qn}(G) \le k$" is HasQueueLayout G k: an injective map ord : V → ℕ (the linear ordering) and an assignment of the edges of $G$ (G.edgeSet, not all unordered pairs) to Fin k such that no two edges in one queue nest; nesting uses strict inequalities, so edges sharing an end never nest. Queues may be empty.
• A layering is a layer function L : V → ℕ; a BFS layering takes one root per component. Vertical paths are nonempty lists indexed from $0$ with distance $d + i$, $d \ge 0$.
• Euler genus is combinatorial: EulerGenusLE G g asks for an embedding scheme (rotation permutation of the darts, cyclic at every vertex, and a symmetric edge signature) whose Euler genus $2c - n + m - f$, computed in $\mathbb Z$, is at most $g$. The face count is half the number of face-tracing orbits plus the number of isolated vertices. Equivalence with footnote 2's topological definition is the Heffter–Edmonds–Ringel rotation principle and its non-orientable extension, with additivity over components; it is not part of the mission.
• Planarity is the published RobertsonSeymour1986.GM5.IsPlanar: a crossing-free drawing in $\mathbb R^2$ by simple arcs. "Euler genus $0$ iff planar" is a theorem connecting the two definitions, not built into either.
• "Euler genus $g$" is read as "at most $g$" throughout; every bound is monotone in $g$. In Lemma 21, "$Z$ is connected" reads "empty or connected" (the paper takes $Z = \emptyset$ when $g = 0$), and the restriction of a vertical path may be empty.
• Trivializing formalizations are ruled out: queues indexed on all pairs Sym2 V would deny edgeless graphs a $0$-queue layout; non-strict nesting would forbid adjacent edges in one queue; a drawing that tolerates crossings would make every graph planar; a face count without halving, or without isolated vertices, would make the Euler genus too small or too large (the sanity checks confirm $K_3$ has a scheme of Euler genus $0$, a twisted $K_3$ one of genus $1$, and two isolated vertices genus $0$).
• Welcome contributions: Euler's formula for embedding schemes, face-tracing lemmas, the planar case (Lemma 18, via mission 1's results), the cutting construction of Lemma 21, and the purely combinatorial $4g$-queue step.

Selected references

• V. Dujmović, G. Joret, P. Micek, P. Morin, T. Ueckerdt, D. R. Wood, Planar graphs have bounded queue-number, J. ACM 67(4), 2020; arXiv:1904.04791v5. https://arxiv.org/abs/1904.04791 , https://doi.org/10.1145/3385731
• L. S. Heath, F. T. Leighton, A. L. Rosenberg, Comparing queues and stacks as mechanisms for laying out graphs, SIAM J. Discrete Math. 5(3), 1992. https://doi.org/10.1137/0405031
• L. S. Heath, A. L. Rosenberg, Laying out graphs using queues, SIAM J. Comput. 21(5), 1992. https://doi.org/10.1137/0221055
• V. Dujmović, Graph layouts via layered separators, J. Combin. Theory Ser. B 110, 2015. https://doi.org/10.1016/j.jctb.2014.07.005
• V. Dujmović, P. Morin, D. R. Wood, Layered separators in minor-closed graph classes with applications, J. Combin. Theory Ser. B 127, 2017. https://doi.org/10.1016/j.jctb.2017.05.006
• B. Mohar, C. Thomassen, Graphs on Surfaces, Johns Hopkins University Press, 2001.

Motivation

A decision maker who must choose $x$ to minimize an expected cost $\mathbb E_F[c(x;\xi)]$ rarely knows the distribution $F$ of the uncertain parameter $\xi$; what is available is a sample $\xi^1,\dots,\xi^N$. Sample average approximation (SAA) replaces $F$ by the empirical distribution. Data-driven distributionally robust optimization (DRO) instead minimizes the worst case of the expected cost over a set $\mathcal F_N$ of distributions built from the data, which protects against the error of the empirical distribution at small $N$. Many such sets have been proposed: moment sets (Delage and Ye, 2010), $\phi$-divergence balls (Ben-Tal et al., 2013), Wasserstein balls (Mohajerin Esfahani and Kuhn, 2018).

Bertsimas, Gupta and Kallus (arXiv:1408.4445v3; Mathematical Programming, 2018, doi:10.1007/s10107-017-1174-z) observe that each such set can be read as the confidence region of a statistical goodness-of-fit (GoF) test, and call the resulting method Robust SAA. A basic question for any such method is whether, as $N\to\infty$, its objective, optimal value and optimal solutions converge to those of the full-information problem. The paper answers it for all data-driven DROs at once, with a single property of the test.

Setting

The support $\Xi\subseteq\mathbb R^d$ of $\xi$ is closed, and $\mathcal P(\Xi)$ is the set of Borel probability distributions on $\Xi$ with the topology of weak convergence. The data $\xi^1,\xi^2,\dots$ are i.i.d. from an unknown $F\in\mathcal P(\Xi)$. A data-driven uncertainty set (DUS) map assigns to each sample $(\xi^1,\dots,\xi^N)$ a set $\mathcal F_N\subseteq\mathcal P(\Xi)$; it is the confidence region of the test that rejects a hypothesis $F_0$ exactly when $F_0\notin\mathcal F_N$. Decisions lie in a closed set $X\subseteq\mathbb R^{d_x}$, the cost is $c(x;\xi)$, and the robust objective is the worst-case expectation

$$\mathcal C(x;\mathcal F_N)=\sup_{F_0\in\mathcal F_N}\mathbb E_{F_0}[c(x;\xi)] .$$

A test is uniformly consistent (Definition 3) if, for every data-generating $F$, almost surely every sequence $F_N$ that does not converge weakly to $F$ lies outside $\mathcal F_N$ for infinitely many $N$. The admissible instances are those satisfying three assumptions: (1) $c(\cdot;\xi)$ is equicontinuous in $x$ uniformly over $\xi$; (2) $X$ is bounded, or $c$ is coercive in $x$ uniformly over a set $D$ of positive $F$-probability and bounded below off $D$; (3) $\Xi$ is bounded, or there is a growth function $\phi\ge0$ with $c(x;\xi)=O(\phi(\xi))$ whose expectation the DUS tracks: $\sup_{F_0\in\mathcal F_N}|\mathbb E_{F_0}\phi-\frac1N\sum_i\phi(\xi^i)|\to0$ almost surely. The convergence conditions are (18) $\mathcal C(x;\mathcal F_N)\to\mathbb E_F[c(x;\xi)]$ uniformly on compact subsets of $X$; (19) convergence of optimal values; and (20) every sequence of robust minimizers has a limit point, and all its limit points are true minimizers.

Formalization targets

Goal: Theorem 2

For a DUS map with nonempty sets,

$$\mathcal F_N\ \text{is uniformly consistent}\iff\Big[\forall F,X,c\ \text{satisfying Assumptions 1–3}:\ (18),(19),(20)\ \text{hold a.s.}\Big].$$

The statement carries no rates and no constants; it is a characterization, so it does not depend on any particular test.

Milestones

1. Proposition 8: under uniform consistency and Assumptions 1 and 3, almost surely $\mathbb E_{F_N}[c(x;\xi)]\to\mathbb E_F[c(x;\xi)]$ for every $x\in X$ and every sequence $F_N\in\mathcal F_N$.
2. Proposition 9: deterministically, convergence of $\mathcal C(x_N;\mathcal F_N)$ along every convergent $x_N\to x$ implies (18).
3. Theorem 2, "only if" side: uniform consistency implies (18)–(20) a.s. for every admissible instance.
4. Theorem 2, "if" side: if the test is not uniformly consistent, some admissible instance fails (18)–(20) with positive probability.
5. Theorem 3: if $\mathcal F_N$ always contains the empirical distribution and the test is $c$-consistent (Definition 5, consistency with respect to the expected costs only), then (18)–(20) hold a.s.
6. Proposition 4 (first sentence): a uniformly consistent test is consistent in the classical sense, $\mathbb P(F_0\notin\mathcal F_N)\to1$ for each $F_0\neq F$.

Significance

The result. Theorem 2 reduces the asymptotic analysis of a data-driven DRO to a property of a statistical test, which can be checked once per test rather than once per optimization model. The paper uses it to classify DUSs: the $\chi^2$ and G-tests on a finite support and the Kolmogorov–Smirnov, Kuiper, Cramér–von Mises, Watson and Anderson–Darling tests on the line are uniformly consistent (Theorems 4–5, separate missions of this series), while the test of marginals is not even consistent and so cannot give convergence for every cost. The necessity direction makes the property sharp: a weaker test always admits a well-behaved cost on which the DRO fails to converge. Theorem 3 explains the remaining cases where a DRO converges for one given cost.

Formalizing it. The result is proved in the paper (§10.5), but its proof leans on several standard facts used without detail: the portmanteau theorem, uniform integrability arguments from Billingsley's Convergence of Probability Measures, the Lévy continuity theorem with the Cramér–Wold device, and coercivity arguments carried over from the paper's Theorem 1. A machine-checked version would fix exactly which regularity of the cost these steps need; three such conditions are stated explicitly here (see the scope section). No part of the result is formalized elsewhere to our knowledge; the platform has no notion of a data-driven uncertainty set or of uniform consistency.

Difficulty

Uniform consistency is a statement about weak convergence, while (18)–(20) are statements about expectations of an unbounded, $x$-dependent cost under the members of $\mathcal F_N$. Weak convergence controls expectations only of bounded continuous functions, so the "only if" side must recover convergence of $\mathbb E_{F_N}[c(x;\xi)]$ from Assumption 3, which requires uniform integrability, and then upgrade pointwise convergence to uniform convergence on compacts and to convergence of minimizers when $X$ is unbounded. The tempting route through a single limiting minimization problem fails: the sets $\mathcal F_N$ change with the sample, the worst case is a supremum over infinitely many distributions, and the minimizers of $\mathcal C(\cdot;\mathcal F_N)$ could escape to infinity unless coercivity on $D$ transfers to every member of $\mathcal F_N$. The "if" side needs, from the mere failure of uniform consistency, a single admissible cost whose worst-case objective detects every failure of weak convergence.

Formalization scope

Points are EuclideanSpace ℝ (Fin d), distributions are ProbabilityMeasure ↥Ξ (whose topology is weak convergence), and the data live on the canonical product space $\Xi^{\mathbb N}$ with the product law, 0-indexed. "Almost surely" is ∀ᵐ, and in Definition 3 one null set serves every sequence $F_N$. An expectation over a member of $\mathcal F_N$ is $+\infty$ when the integrand is not integrable, never Lean's default $0$. Minima in (19)–(20) are infima in the extended reals, so the empty and unattained cases need no special treatment; (20) applies to sequences that are minimizers for all large $N$.

Four hypotheses are added to the page, each used by the paper's own proof: every $\mathcal F_N$ is nonempty (otherwise the worst case is $-\infty$ and uniform consistency is vacuous); $c(x;\cdot)$ is continuous on $\Xi$; the set $D$ of Assumption 2b is open; the growth function $\phi$ of Assumption 3b is continuous, with $\mathbb E_F\phi<\infty$ as fixed on p. 10 of the paper. Theorem 3 additionally assumes Assumption 2, which its proof uses. Proposition 4 assumes the rejection events are measurable. A formalization in which the worst case uses the raw Bochner integral, the supremum ranges over a possibly empty set, or (20) requires minimizers at $N=0$ would make the statements false or vacuous, and is ruled out.

A full development needs weak convergence and the portmanteau theorem (in Mathlib), uniform integrability and its relation to convergence of means under weak convergence, the strong law of large numbers for the growth function and the empirical measure, the Lévy continuity theorem in several dimensions (in Mathlib, via characteristic functions), and a countable convergence-determining class of bounded continuous functions. The uniform-integrability step and the path characterization of local uniform convergence (Proposition 9) are reusable beyond this mission. Contributions to any milestone are welcome; Proposition 9 is self-contained and deterministic.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Robust Sample Average Approximation, arXiv:1408.4445v3, 2016; Mathematical Programming 171 (2018). https://arxiv.org/abs/1408.4445v3, https://doi.org/10.1007/s10107-017-1174-z
• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3), 2010. https://doi.org/10.1287/opre.1090.0741
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
• P. Mohajerin Esfahani, D. Kuhn, Data-Driven Distributionally Robust Optimization Using the Wasserstein Metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1

Motivation

The newsvendor problem is the basic single-period inventory decision: a retailer orders $q\ge0$ units at unit cost $c$ before a random demand $\tilde d$ is observed, sells at unit price $p>c$, and loses unsold units. When the demand law is known, the optimal order is a quantile of that law. In practice the law is rarely known, and a distributionally robust newsvendor instead hedges against the worst law in an ambiguity set of laws consistent with partial information.

Scarf (1958; reference [42] of arXiv:1806.05379) solved the case where only the mean and the variance of demand are known, and observed that for a range of small profit margins the robust newsvendor orders nothing. Demand data in retail and spare-parts settings are often heavy tailed: Pareto fits with exponent close to $1$ have been reported, so a finite mean is plausible while a finite variance is not. Das, Dhara and Natarajan (arXiv:1806.05379) therefore replace the variance by an $\alpha$-th moment for an arbitrary real $\alpha>1$. This mission formalizes their result that the zero-order phenomenon survives for every such $\alpha$.

Setting

Write the critical ratio as $\eta=1-c/p\in[0,1)$. A demand law is a probability measure $F$ on $[0,\infty)$. Fix a real $\alpha>1$ and two moments $m_1,m_\alpha$ with

$$m_\alpha>m_1^\alpha>0 .$$

The ambiguity set is

$$\mathcal F_{1,\alpha}=\Big\{F:\ \int_0^\infty w\,dF(w)=m_1,\ \int_0^\infty w^\alpha\,dF(w)=m_\alpha\Big\},$$

the laws on $[0,\infty)$ with mean $m_1$ and $\alpha$-th moment $m_\alpha$. The worst-case expected shortage is

$$\Pi_{1,\alpha}(q)=\sup_{F\in\mathcal F_{1,\alpha}}\mathbb E_F[\tilde d-q]^+ ,$$

and the robust newsvendor problem (3.2) is

$$\min_{q\ge0}\ \big((1-\eta)q+\Pi_{1,\alpha}(q)\big).$$

An optimal order quantity is a minimizer $q^*\ge0$ of this objective. Two thresholds appear:

$$\eta_0=1-\Big(\frac{m_1^\alpha}{m_\alpha}\Big)^{1/(\alpha-1)},\qquad q_0=\frac{\alpha-1}{\alpha}\Big(\frac{m_\alpha}{m_1}\Big)^{1/(\alpha-1)} .$$

In Lean these are ambiguitySet, worstCase, robustCost, eta0, q0 and IsOptimalOrder in the namespace HeavyTailNV.ZeroOrder.

Formalization targets

Goal: Proposition 3.2 (p. 13)

$\eta_0\in(0,1)$, and

• for every $\eta\in[0,\eta_0)$ the set of optimal order quantities is exactly $\{0\}$;
• for every $\eta\in(\eta_0,1)$ an optimal order quantity exists, and every optimal order quantity $q^*$ satisfies $q^*>0$ and

$$q^*\ge q_0 ;$$

• for $\eta=\eta_0$ every $q\in[0,q_0]$ is optimal.

Milestones

1. Proposition 3.1 (p. 12): for $0\le q\le q_0$,

$$\Pi_{1,\alpha}(q)=m_1-q\Big(\frac{m_1^\alpha}{m_\alpha}\Big)^{1/(\alpha-1)},$$

and the two-point law with mass $(m_1^\alpha/m_\alpha)^{1/(\alpha-1)}$ at $(m_\alpha/m_1)^{1/(\alpha-1)}$ and the rest at $0$ lies in $\mathcal F_{1,\alpha}$ and attains the supremum. 2. Properties of $\Pi$ (§2.1, p. 6): $\Pi_{1,\alpha}$ is non-increasing and convex, $\Pi_{1,\alpha}(q)+q=m_1$ for $q\le0$, and $\Pi_{1,\alpha}(q)\to0$ as $q\to\infty$. 3. Display (3.10) (p. 14): for $\eta\in[0,1)$ and $0\le q\le q_0$,

$$(1-\eta)q+\Pi_{1,\alpha}(q)=m_1-q(\eta-\eta_0).$$

Significance

Proposition 3.2 shows that for every finite moment order $\alpha>1$, however high, there is a nonempty interval $[0,\eta_0)$ of critical ratios in which the robust newsvendor orders nothing, and it gives the threshold $\eta_0$ and the minimum positive order $q_0$ in closed form. For $\alpha=2$ it recovers Scarf's zero-order region. The worst-case law associated with $\Pi_{1,\alpha}$ therefore carries a positive mass at zero demand, which is the low-service-level counterpart of the paper's heavy-tail result for high critical ratios (the companion mission of this series).

The results are proved in the paper: the proof of Proposition 3.1 follows the statement on pp. 12–13 and the proof of Proposition 3.2 is on p. 14. None of them has a machine-checked proof. Formalizing them requires a usable treatment of moment-constrained suprema over probability measures on $[0,\infty)$, of the stop-loss transform $q\mapsto\mathbb E[\tilde d-q]^+$, and of minimizers of convex functions on a half-line. These pieces recur across robust inventory and pricing models.

Difficulty

The closed form of Proposition 3.1 is the central step. The lower bound is a computation with a two-point law. The matching upper bound has to hold against every law in $\mathcal F_{1,\alpha}$, including laws with unbounded support and non-integer $\alpha$. The paper obtains it from a dual certificate for the moment problem (3.3)–(3.4), and weak duality for this semi-infinite problem is not available off the shelf. The closed form also holds only on $[0,q_0]$. To conclude anything about minimizers on all of $[0,\infty)$, where no closed form is known for general $\alpha$ (the dual leads to equations $aw^\alpha+bw+c=0$, p. 11), one needs convexity of $\Pi_{1,\alpha}$ on the whole line. Inspecting the objective on $[0,q_0]$ alone does not determine the global minimizers.

Formalization scope

• Demand laws are Measure ℝ with IsProbabilityMeasure F and F (Set.Iio 0) = 0. Moments are Bochner integrals, and the set requires Integrable (fun w => w) F and Integrable (fun w => w ^ α) F (real rpow), so that the moment equalities are genuine.
• $\Pi_{1,\alpha}$ is a real sSup. Under the standing hypotheses $\alpha>1$, $m_1>0$, $m_\alpha>m_1^\alpha$ the set is nonempty (it contains the two-point law of Proposition 3.1) and the expectations are bounded above by $m_1+|q|$, so the value is not Lean's default for an empty or unbounded set. Every statement carries these standing hypotheses of (3.1); no other hypothesis is added except the range $\eta\in[0,1)$ in (3.10), which is the paper's standing range of the critical ratio.
• Optimality is minimization over $q\in[0,\infty)$, as in (3.2), not over $\mathbb R$. Over $\mathbb R$ the objective equals $m_1-\eta q$ for $q\le0$, and part (a) would fail at $\eta=0$.
• Trivializing readings are ruled out. Part (a) asserts that $\{0\}$ is the whole set of minimizers, not only that $0$ is a minimizer. Part (b) asserts that a minimizer exists, so its lower bound is not vacuous. Dropping the support constraint, the normalization, or the integrability clauses would change the problem or let junk integrals satisfy the moment constraints.
• The unit cost and price never appear; everything is stated in $\eta$.
• The ambiguity set, worst-case value and objective come from the shared HeavyTailNV.Tail.Model. This mission defines the thresholds, optimality predicate and two-point law in HeavyTailNV.ZeroOrder.Model. Contributions to the general moment-problem duality used by Proposition 3.1 are welcome and reusable well beyond this mission.

Selected references

• B. Das, A. Dhara and K. Natarajan, On the heavy-tail behavior of the distributionally robust newsvendor, Operations Research 69(4), 2021; preprint arXiv:1806.05379v2, 2019. https://arxiv.org/abs/1806.05379
• H. Scarf, A min–max solution of an inventory problem, in K. Arrow, S. Karlin and H. Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, pp. 201–209, Stanford University Press, 1958 (no DOI; reference [42] of https://arxiv.org/abs/1806.05379).

Motivation

A queue layout represents a graph by placing its vertices in a line and assigning edges to queues. The order and assignment must prevent nested edges from sharing a queue. This gives a graph parameter that measures how much queue capacity is needed for a particular graph. Heath, Leighton, and Rosenberg asked whether one fixed number of queues suffices for every planar graph. The question remained open while bounds depending on the graph's number of vertices, degree, or treewidth were known. Dujmović, Joret, Micek, Morin, Ueckerdt, and Wood resolved it by proving a uniform bound of 49. Their paper also develops layered partitions, a structural tool used beyond queue layouts. These claims and the historical account appear in the source paper, pp. 3–5 and 16.

Setting

A finite simple graph $G$ has vertices $V(G)$ and unordered edges $E(G)$. Choose a linear order of $V(G)$. Two disjoint edges nest when their endpoints appear as $a<b<c<d$, with one edge joining $a$ to $d$ and the other joining $b$ to $c$. A queue is a set of edges with no nested pair. A $k$-queue layout is a vertex order together with an assignment of every edge to one of $k$ queues; $\operatorname{qn}(G)\le k$ means such a layout exists. Edges sharing an endpoint cannot nest. Empty queues are allowed, so an edgeless graph can use zero queues. These are the paper's definitions in §1, pp. 3–4.

A layering assigns vertices to layers $V_0,V_1,\ldots$ such that endpoints of an edge lie in the same or adjacent layers. A BFS layering starts from one selected root in each connected component and places each vertex in the layer equal to its graph distance from that root. A vertex partition divides $V(G)$ into disjoint nonempty parts. Its quotient graph $G/\mathcal P$ has those parts as vertices; distinct parts are adjacent if an edge of $G$ joins them. An $H$-partition may index the parts by vertices of another graph $H$: the quotient's edges must be represented by edges of $H$, while an indexed part may be empty. A partition has layered width at most $\ell$ with respect to a fixed layering if every part contains at most $\ell$ vertices of every layer. The exact definitions are in §2, pp. 7–9.

A graph is planar when it can be drawn in the plane with vertices at distinct points and edges as simple arcs that meet only at shared endpoints. A tree decomposition covers every vertex and edge of a graph by bags indexed by a tree, with the bags containing each vertex forming a connected subtree. Treewidth at most three means that a tree decomposition exists with every bag of size at most four. The paper uses these standard notions in §2 and §4, pp. 7, 12, and 16.

Formalization targets

Queue bound for planar graphs

The goal is the explicit upper bound the paper derives for its Theorem 1:

$$\forall G\text{ finite and planar},\qquad \operatorname{qn}(G)\le49.$$

The printed theorem says that planar queue-number is bounded, and the authors state 49 immediately after it. A bound that depends on $|V(G)|$ would not express the result. The goal uses the paper's own constant, as given in Theorem 1 and the following sentence, p. 5.

Layered partition and transfer bounds

The structural target is Theorem 15, p. 16: for every BFS layering of a planar graph, there is a partition of layered width at most three whose quotient remains planar and has treewidth at most three. The queue transfer target is Lemma 8, p. 10:

$$\operatorname{qn}(G)\le 3\ell\operatorname{qn}(H)+ \left\lfloor\frac{3\ell}{2}\right\rfloor$$

when $G$ has an $H$-partition of layered width $\ell$. Its layout orders vertices layer by layer. The milestone list also includes the rainbow characterization, the blowup lemma, the complete-graph queue number, and the five-queue bound for planar graphs of treewidth at most three. These are the stated supporting results along the route to 49 in §2–§4.1, pp. 7 and 10–16.

Significance

The goal establishes a constant queue bound for all planar graphs, independent of their size, degree, and treewidth. Theorem 15 supplies a reusable structural statement: even if the original graph has large treewidth, its quotient by small layer intersections has treewidth at most three while remaining planar. The paper goes on to treat graphs of bounded Euler genus and proper minor-closed classes, and describes connections with graph products and other graph parameters in its abstract and introduction, pp. 1 and 5.

The result is proved in the cited paper. This mission records Lean statements of the goal and six supporting milestones; their proofs remain to be formalized. A completed development would connect finite graph orders, nested-edge combinatorics, layered partitions, planar drawings, and tree decompositions in one machine-checked chain. The queue and partition definitions can also support later work on graph classes beyond the planar case.

Difficulty

A vertex order chosen without regard to a graph's structure can contain large rainbows, forcing many queues in that order. Planarity alone does not specify an order or an edge assignment, and a direct bound from ordinary treewidth does not cover planar graphs with arbitrarily large treewidth. The central structural requirement is to find a partition whose parts remain small in each BFS layer while its quotient has low treewidth. The queue transfer lemma must retain a layer-by-layer vertex order and account for edges within parts and between parts. The paper, pp. 10–11 and 16, identifies these as distinct constraints in its stated results.

Formalization scope

Vertices form a finite type and edges are those of a Mathlib simple graph. A vertex order is an injective map into $\mathbb N$; strict inequalities on four endpoints encode nesting. Queue assignments are functions on the graph's edge set, so the empty graph's zero-queue case is present. The statements use an existence predicate for $\operatorname{qn}(G)\le k$, without taking a numerical infimum. Layerings are functions to $\mathbb N$, with BFS roots chosen separately for disconnected components. Theorem 15 uses a partition into nonempty parts, and the quotient has exactly those parts as vertices. Treewidth at most three uses a published tree-decomposition definition with bags of size at most four.

The locally checked drawing definition has the same fields as the published plane-drawing definition; the published module was unavailable from the local index in this run. Planarity means existence of a crossing-free drawing, not a drawing that permits crossings. The formulation does not use a universal edge carrier that would rule out zero queues, a non-strict nesting test, or a default numerical treewidth. The near-triangulation, Sperner, and tripod statements from the paper's deeper proof are outside this proposal's milestone scope; the partition theorem remains a full milestone. Solvers may contribute the omitted geometric and tree-decomposition infrastructure when proving it.

Selected references

• V. Dujmović, G. Joret, P. Micek, P. Morin, T. Ueckerdt, and D. R. Wood, Planar graphs have bounded queue-number, Journal of the ACM 67(4), 2020. arXiv:1904.04791v5; DOI:10.1145/3385731.

The Hlawka inequality for Schatten $p$-norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real $p\ge80$, also holds for every real $p\ge70$. This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. Because the cutoff-80 mission already covers every $p\ge80$, the new work is the range from 70 to 80.

The cutoff came down from 90 to 80 in under two days, through moona3k's proofs at 89, 88, 87, 85, 84 and 80. The step to 89 sharpened the estimates of the cutoff-90 argument, and the step to 85 added a new idea, a weighted pair-curvature and confinement estimate. How far these methods reach is not known; 70 asks for ten more units. The goal theorem below gives the exact statement.

This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 70 or lower also settles this mission.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

• K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
• Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library
• Ezzeri Esa and project contributors, The cyclic bound for every real p ≥ 90, research note with appendices and exact certificates, 2026. Research note

Established results on Prove2Me

• The accepted sharp diagonal bound for every real p ≥ 80.
• The accepted real coordinate bound for every real p ≥ 80.
• The accepted diagonal Schatten norm identity.

Why kernel well-posedness matters

Boundary control of a transport equation acts at the edge of a spatial interval, while the state evolves throughout the interval. A backstepping transformation connects the original state to a simpler target state by integrating against kernels on a triangular region. The transformation is useful only when those kernels exist with the regularity and uniqueness needed to define a single feedback law. Coron, Vazquez, Krstic and Bastin use this construction for a two-component quasilinear hyperbolic system. Their Appendix A isolates a four-component linear kernel system and proves its well-posedness independently of the later stability arguments (Coron et al., Appendix A).

This mission concerns that appendix result. The paper states a generic system broad enough to include the kernel equations arising from its controller design. Its goal is a unique continuous solution on the closed triangle, assuming continuous coefficients and strictly positive transport speeds. The result supplies the existence and uniqueness premise for the paper's later linear and quasilinear stabilization results. It is a proved result in the source preprint; the work here is to state its analytic content precisely in Lean and leave its proof as a formalization target.

Setting

Let $\mathcal T=\{(x,\xi):0\le\xi\le x\le1\}$. There are four unknown real functions $F^1,\ldots,F^4$ on $\mathcal T$. Two positive, continuous functions $\epsilon_1,\epsilon_2$ describe the characteristic speeds. Four functions $g_j$ supply forcing, and sixteen functions $C_{ji}$ couple the unknown components. The functions $g_j$ and $C_{ji}$ are continuous on $\mathcal T$. Boundary functions $h_j,q_j$ are continuous on $[0,1]$. The paper's equations (A.1)–(A.4) have first-order directional derivatives of $F^j$ on the left and $g_j+\sum_i C_{ji}F^i$ on the right (Coron et al., p. 18).

The boundary data have two forms. Components $F^2$ and $F^3$ are prescribed on the diagonal $\xi=x$: $F^2(x,x)=h_2(x)$ and $F^3(x,x)=h_3(x)$. Components $F^1$ and $F^4$ are prescribed on the lower edge $\xi=0$ with linear dependence on $F^2(x,0)$ and $F^3(x,0)$. For example, $F^1(x,0)=h_1(x)+q_1(x)F^2(x,0)+q_2(x)F^3(x,0)$. The fourth component uses $q_3,q_4$ in the same way. Those edge couplings are part of the problem, rather than optional side conditions.

For merely continuous $F^j$, a classical partial derivative need not exist. Accordingly, the mission uses the paper's characteristic integral equations (A.23) as the meaning of solution. The travel-time coordinates are $\phi_i(x)=\int_0^x\epsilon_i(z)^{-1}\,dz$ for $i=1,2$, with $\phi_3=\phi_1+\phi_2$. Each characteristic starts on the prescribed part of the boundary and ends at $(x,\xi)$. The value of $F^j(x,\xi)$ equals its starting boundary value plus the forcing and coupling integrals along that characteristic. A continuously differentiable solution of the differential equations and the boundary conditions satisfies this integral form (Coron et al., pp. 19–20).

Formalization targets

The goal is Theorem A.1: for every set of data with the continuity and positivity assumptions above, there is a continuous characteristic solution $F$ on $\mathcal T$, and any two such solutions agree at every point of $\mathcal T$:

$$\exists F\in C(\mathcal T)^4\;\operatorname{CharSolution}(F),\qquad \forall F,F'\in C(\mathcal T)^4,\quad \operatorname{CharSolution}(F)\land\operatorname{CharSolution}(F')\Longrightarrow F=F'\text{ on }\mathcal T.$$

Four source results mark the path to that goal. Lemma A.3 keeps every characteristic in $\mathcal T$ and records its continuity and coordinate inequalities. Lemma A.4 bounds the integral of the $n$th power of its first coordinate by $K_\epsilon x^{n+1}/(n+1)$. Lemma A.5 bounds one application of the linear integral operator to an increment satisfying a factorial estimate. Proposition A.6 bounds the resulting infinite series by $\bar\phi\exp(\bar C K_\epsilon x)$ (Coron et al., pp. 19, 21–23). These are the mission's four milestones.

Significance

Theorem A.1 fixes a genuine mathematical issue behind the feedback construction: a kernel cannot be treated as an arbitrary coefficient of a controller when its defining boundary problem has not been solved. Existence gives a kernel for the transformation; uniqueness makes that kernel determined by the coefficient data. The theorem is stated for a generic coupled system, so the same result can support several kernels rather than just one equation in the control design (Coron et al., Appendix A).

Formalizing this known proof would add a reusable interface for characteristic coordinates, bounded coefficient functions on a triangle, and coupled Volterra-type integral operators. The present proposal contains statements, not completed proofs. The local prior-art search found no published Goursat kernel item with the same four-component system and boundary conventions. The broader paper's linear and quasilinear stability results are separate missions; this one records their analytic kernel prerequisite without importing their controller definitions.

Difficulty

The mixed boundaries make the usual one-direction transport picture insufficient. Two characteristic families enter from $\xi=0$, while two enter from the diagonal. Moreover, the lower-edge values of $F^1$ and $F^4$ depend on the other components at that edge. Thus a bound for one component cannot ignore the other three or assume all boundary values are given independently. A candidate continuous solution must also be shown to agree with the same integral equations at the corner and along both boundary segments. The explicit characteristics involve the inverse of $\phi_3$, whose argument and range must be checked throughout $\mathcal T$ (Coron et al., pp. 19–23).

Formalization scope

The Lean data bundle contains globally defined real functions, with continuity and positivity imposed only on $[0,1]$ or $\mathcal T$. Such functions represent continuous data on those closed domains by extension; values outside the domains do not enter the statements. The four components use Fin 4, indexed $0,1,2,3$ in Lean for the paper's $1,2,3,4$. The two lower-edge couplings and the two diagonal values are all included in IsCharSolution. Equality in the uniqueness clause is restricted to $\mathcal T$, because the extensions outside it are unconstrained.

The coordinate inverses are Function.invFunOn on $[0,1]$; only arguments in their ranges have mathematical meaning here. Lemma A.3 includes the domain facts that keep the characteristics in range. Integrals are over finite characteristic intervals with continuous integrands, and the maxima in (A.35) are suprema of continuous images of compact sets, not suprema over all real inputs. Proposition A.6 asserts summability before using an infinite sum. Lemmas A.4 and A.5 include $n=0$, a valid base case needed by the source's induction. Lemma A.5 makes the continuity of the increment explicit so its integrals retain their intended values. Existence and uniqueness both remain in the goal; retaining only one would change Theorem A.1. Two formalizations would trivialize or falsify the goal and are ruled out: dropping the boundary conditions (A.5)–(A.7) from the solution notion makes uniqueness false, and reading the PDEs (A.1)–(A.4) classically for a merely continuous $F$ would make existence false; the solution notion is the paper's characteristic integral form with all boundary conditions. Contributions to the characteristic and operator estimates, continuity of the constructed limit, and the uniqueness argument are within scope.

Selected references

• J.-M. Coron, R. Vazquez, M. Krstic and G. Bastin, Local Exponential H² Stabilization of a 2 × 2 Quasilinear Hyperbolic System Using Backstepping, arXiv preprint arXiv:1208.6475v1, 2012, Appendix A, pp. 18–23. Preprint.

Motivation

Ride-hailing, freelancing and delivery platforms are intermediaries that post a price to buyers and a price to sellers and then match the two sides. Both sides are forward-looking: an agent who arrives can wait before requesting, and an agent who requests waits until she is matched, at a cost per unit of time. Chen and Hu, Pricing and Matching with Forward-Looking Buyers and Sellers (SSRN 2859864; Manufacturing & Service Operations Management 22(4), 2020, doi:10.1287/msom.2018.0769), measure simple pricing and matching policies against an upper bound that holds for every policy. This mission formalizes that upper bound in its mechanism-design form: no incentive-compatible two-sided dynamic mechanism earns more than the expected value of a clairvoyant assignment problem in virtual values.

The bound extends the virtual-value approach of Myerson (1981) and its bilateral-trade version by Myerson and Satterthwaite (1983) from a single static trade to a market with random arrivals on both sides, waiting costs and a timing constraint that matched units change hands at the same instant.

Setting

Over a horizon $[0,T]$, buyers arrive as a Poisson process of rate $\lambda^d>0$. A buyer has type $\phi=(t_\phi,v_\phi)$: arrival time $t_\phi$ and valuation $v_\phi\in[\underline v,\bar v]$, drawn with continuous positive density $f^d$ and c.d.f. $F^d$, independently of the arrival time. Sellers arrive as an independent Poisson process of rate $\lambda^s>0$, with types $\psi=(t_\psi,c_\psi)$ and costs $c_\psi\in[\underline c,\bar c]$ of continuous positive density $f^s$ and c.d.f. $F^s$. The paper assumes $\underline c\le\bar v$ and that the virtual value $V^d(v)=v-(1-F^d(v))/f^d(v)$ and the virtual cost $V^s(c)=c+F^s(c)/f^s(c)$ are increasing (Assumptions 1–2). Write $H^T$ for the realized arrivals.

A direct mechanism $y^T$ assigns to every buyer an outcome $(s_\phi,m_\phi,p_\phi)$: the time $s_\phi\in[t_\phi,T]$ at which she leaves, the indicator $m_\phi\in\{0,1\}$ that she receives a unit, and her payment $p_\phi$. Every seller receives $(s_\psi,m_\psi,p_\psi)$ likewise, $p_\psi$ now paid to her. The balancing condition requires that at every $t\in[0,T]$ the number of buyers who receive a unit at $t$ equals the number of sellers who deliver one at $t$. The buyer's utility is $U^d=v_\phi m_\phi-p_\phi-b(s_\phi-t_\phi)$ and the seller's is $U^s=p_\psi-c_\psi m_\psi-h(s_\psi-t_\psi)$, with waiting costs $b,h\ge0$. The intermediary's profit is

$$\Pi(y^T)=\sum_{\phi\in H^T}p_\phi-\sum_{\psi\in H^T}p_\psi .$$

Incentive compatibility (ICd) asks that no buyer gain, in the interim expectation $E_{-\phi}$ over all other agents, by reporting another valuation or a later arrival time $t_{\hat\phi}\in[t_\phi,T]$; individual rationality (IRd) asks that her interim utility be nonnegative. (ICs) and (IRs) are the seller counterparts. Problem (B′) maximizes $E[\Pi(y^T)]$ over feasible mechanisms subject to these constraints; its value is $J^*$.

The comparison object is the clairvoyant assignment problem (B): knowing $H^T$ in advance, choose a partial matching $x$ of buyers to sellers maximizing

$$\sum_{\phi,\psi}\Big(V^d(v_\phi)-V^s(c_\psi)-b\,(t_\psi-t_\phi)^+-h\,(t_\phi-t_\psi)^+\Big)x_{\phi\psi};$$

its optimal value is $\bar J(H^T)\ge0$.

Formalization targets

Goal: the mechanism-design bound

For every feasible, well-defined mechanism satisfying (ICd), (IRd), (ICs) and (IRs),

$$E\big[\Pi(y^T)\big]\le E\big[\bar J(H^T)\big],$$

with $\bar J(H^T)$ integrable. This is the last display of the proof of Lemma 1 (Online Appendix p. 4), $J^*\le\bar J^1\le\bar J^2\le E[\bar J(H^T)]$.

Milestones

1. Lemma S.1 (Supplemental Note p. 1): $E_{-\phi}[p_\phi]\le v_\phi E_{-\phi}[m_\phi]-\int_{\underline v}^{v_\phi}E_{-\phi}[m_{\phi_{v'}}]\,dv'-bE_{-\phi}[s_\phi-t_\phi]$ under (ICd′) and (IRd).
2. Lemma S.2: $E[\sum_\phi p_\phi]\le E[\sum_\phi V^d(v_\phi)m_\phi-b(s_\phi-t_\phi)]$.
3. Lemma S.4: $E[\sum_\psi p_\psi]\ge E[\sum_\psi V^s(c_\psi)m_\psi+h(s_\psi-t_\psi)]$.
4. The pathwise step $\bar J^2\le E[\bar J(H^T)]$: for every profile and every balanced assignment of outcomes, buyer virtual surplus net of waiting, less seller virtual cost plus waiting, is at most the value of (B).

Lemma S.3 (Supplemental Note p. 3), the seller envelope bound with information rent $\int_{c_\psi}^{\bar c}E_{-\psi}[m_{\psi_{c'}}]\,dc'$, is posed as a further theorem of the mission, the mirror image of Lemma S.1; it is not listed as a milestone.

Here (ICd′) and (ICs′) are the one-dimensional constraints in which the reported arrival time is the true one; Lemmas S.1–S.4 are stated under these weaker hypotheses, as in the paper.

Significance

Lemma 1 of the paper, $J^{\pi,M}\le E[\bar J(H^T)]$ for every pricing policy $\pi$ and matching policy $M$, is the benchmark against which the paper's main theorem measures its waiting-adjusted fixed-price policy, and $E[\bar J(H^T)]$ is in turn bounded by a deterministic fluid value (Lemma 2). Lemma 1 is the composition of two facts: the revelation principle $J^{\pi,M}\le J^*$ (Lemma 3) and the mechanism-design bound $J^*\le E[\bar J(H^T)]$ posed here. The second carries the analytic content: it is where the envelope theorem, the exchange of integrals that turns payments into virtual values, and the timing argument appear.

The result is proved in the paper; its proofs are in the Online Appendix (Section A.2) and the Supplemental Note (Section A). No machine-checked proof of it, or of a dynamic two-sided Myerson bound of this kind, is known. A formal proof would also yield a reusable two-sided, Poisson-arrival version of the interim envelope and revenue-equivalence identities.

Difficulty

Each agent's type is two-dimensional, an arrival time and a valuation or cost, and arrival can only be misreported later. The relaxation to (ICd′)/(ICs′) makes the screening problem one-dimensional, but the interim expectation $E_{-\phi}$ ranges over a random population whose size is itself random. Turning $E[\sum_{\phi\in H^T}p_\phi]$ into an integral of interim payments requires the Mecke formula for the Poisson process, and the envelope argument must be carried out for interim utilities that are only known to be suprema of affine functions, using no differentiability of the mechanism. The pathwise step is combinatorial: the balancing condition at each instant pairs buyers with sellers discharged together, and those pairs must be compared with an optimal matching of (B), with duplicate types and unmatched agents handled.

A frequent first idea, bounding payments by valuations directly, gives only the first-best surplus $E[\sum (v_\phi-c_\psi)]$, which is not the target; the information rents must be extracted.

Formalization scope

The primitives are the published bilateral-trade environment MechanismDesign.BilateralTrade.Environment (densities on intervals, cdfB, cdfS, psiB $=V^d$, psiS $=V^s$, Regular $=$ Assumptions 1–2), and (B) is AssignmentGame.CoreLP.worth of the published assignment game, with sellers as rows and buyers as columns. The conventions committed to are:

1. Arrivals. Each side is a Poisson($\lambda T$) number of agents with i.i.d. types, arrival time uniform on $[0,T]$ and independent of the mark; this is equal in law to the Poisson process restricted to $[0,T]$. Profiles are multisets of types: agents are named by their types, as in the paper, and coincide only with probability zero.
2. Mechanisms map the reported buyer and seller profiles to an outcome for each type, $(s,m,p)$ with $t\le s\le T$ and $m\in\{0,1\}$ for listed agents and the balancing condition at every $t\in[0,T]$. The causality conditions of the paper (stopping times with respect to the filtration $\mathcal H_t$) and the timing variables $\tau,a$ are dropped. This enlarges the class of mechanisms; it is the clairvoyant class through which the paper's own proof passes ($\bar J^1\le\bar J^2$), and the bound for the larger class implies the paper's.
3. Interim expectations. $E_{-\phi}[g(y_{\hat\phi})]$ is the expectation, over an independent copy of $H^T$, of $g$ at the outcome of the report $\hat\phi$ inserted among the buyers (the Slivnyak–Mecke reading of "expectation taken with respect to $H^T\setminus\{\phi\}$").
4. Incentive constraints are quantified over every type and every report in the type spaces, not almost everywhere, with reported arrivals $t_{\hat\phi}\in[t_\phi,T]$.
5. Added hypotheses. Continuity of $f^d$, $f^s$ on their supports, without which $V^d,V^s$ are defined only almost everywhere; and WellDefined: outcomes are Borel in the listed types, interim payments are integrable, and total absolute payments are integrable. Integrability of $\bar J(H^T)$ and of the virtual-surplus sums is part of each conclusion.

A trivializing formalization is ruled out: the mechanism class is not restricted beyond the paper's feasibility, the constraints are not vacuous (the null mechanism satisfies them, so $J^*\ge0$), and expectations are of integrable functions. The goal quantifies over mechanisms rather than taking a supremum, which is equivalent because the class is nonempty.

A complete development needs the Mecke formula for the Poisson-count representation, an envelope theorem for suprema of affine functions on an interval, Fubini on the type space, and an exchange argument for matchings. All of these are reusable beyond this mission. Contributions of any of them, of the milestones in any order, or of alternative proofs are welcome.

Selected references

• Y. Chen and M. Hu, Pricing and Matching with Forward-Looking Buyers and Sellers, Manufacturing & Service Operations Management 22(4):717–734, 2020; submitted manuscript SSRN 2859864. https://ssrn.com/abstract=2859864, https://doi.org/10.1287/msom.2018.0769
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1):58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• R. B. Myerson and M. A. Satterthwaite, Efficient Mechanisms for Bilateral Trading, Journal of Economic Theory 29(2):265–281, 1983. https://doi.org/10.1016/0022-0531(83)90048-0
• P. Milgrom and I. Segal, Envelope Theorems for Arbitrary Choice Sets, Econometrica 70(2):583–601, 2002. https://doi.org/10.1111/1468-0262.00296
• G. Last and M. Penrose, Lectures on the Poisson Process, Cambridge University Press, 2017 (Mecke equation, Theorem 4.1). https://doi.org/10.1017/9781316104477

Motivation

Least-squares regression, $\min_X\|AX-B\|_F$ for a tall matrix $A\in\mathbb R^{n\times d}$ with $n\gg d$, is among the most frequently solved problems in numerical computation. Direct methods (QR or SVD) cost $O(nd^2)$ time, which is prohibitive when $n$ is in the millions. Sketching replaces the problem by a much smaller one: choose a matrix $S\in\mathbb R^{t\times n}$ with $t\ll n$, form $SA$ and $SB$, and solve $\min_X\|S(AX-B)\|_F$ instead. The question is when the solution of the small problem is nearly optimal for the original one.

Clarkson and Woodruff, Low Rank Approximation and Regression in Input Sparsity Time (STOC 2013; JACM 2017), showed that a very sparse random sketch (one non-zero per column, the CountSketch matrix) can be applied in time proportional to the number of non-zero entries of $A$ and still yields $(1+\varepsilon)$-approximate regression and low-rank approximation. §7 of that paper isolates the deterministic part of the argument: two conditions on a fixed sketch $S$ that guarantee a near-optimal solution, whatever distribution produced $S$.

Timeline. Sarlós (FOCS 2006) introduced sketch-and-solve regression with fast Johnson–Lindenstrauss transforms. Drineas, Mahoney, Muthukrishnan and Sarlós (Numer. Math. 2011) stated the structural conditions for single-response regression (their Lemma 1); Theorem 36 of Clarkson–Woodruff generalizes it to multiple responses. Clarkson and Woodruff then supplied the sparse sketches meeting the conditions in input-sparsity time.

Setting

All matrices are real. For a vector $v$ let $\|v\|_2^2=\sum_iv_i^2$; for a matrix $M$ let $\|M\|_F^2=\sum_{i,j}M_{ij}^2$. Fix $A\in\mathbb R^{n\times d}$ of rank at most $r$, a right-hand side $B\in\mathbb R^{n\times d'}$ and a sketch $S\in\mathbb R^{t\times n}$. Let $C(A)=\{Ax\}$ be the column space and $U\in\mathbb R^{n\times k}$ a matrix with orthonormal columns ($U^\top U=I$) spanning $C(A)$.

• $Y^*$ is a least-squares minimizer: it minimizes $\|AY-B\|_F^2$ (problem (8)).
• $\tilde Y$ is a sketched minimizer: it minimizes $\|S(AY-B)\|_F^2$ (problem (7)).
• $S$ is a subspace embedding for $A$ with parameter $\eta$ if $\bigl|\|SAx\|_2^2-\|Ax\|_2^2\bigr|\le\eta\|Ax\|_2^2$ for every $x$.
• $S$ satisfies the approximate matrix multiplication event (Lemma 32) for a pair $(U,W)$ with error parameter $e$ if $\|U^\top S^\top SW-U^\top W\|_F^2\le e^2\|U\|_F^2\|W\|_F^2$.

Formalization targets

Goal: Theorem 36 (p. 24)

If $S$ is a subspace embedding for $A$ with $0\le\eta\le1/2$ and satisfies the event of Lemma 32 for $(U,B-AY^*)$ with error parameter $\sqrt{\varepsilon/r}$, then every sketched minimizer satisfies

$$\|A\tilde Y-B\|_F^2\le(1+4\varepsilon)\|AY^*-B\|_F^2 .$$

This is the explicit form the paper's proof establishes; the printed $(1+\epsilon)$ bound on norms follows after rescaling $\varepsilon$.

Milestones

• Fact 34 (Pythagorean theorem): $C^\top D=0\Rightarrow\|C+D\|_F^2=\|C\|_F^2+\|D\|_F^2$.
• Fact 35 (normal equations): $C^-D$ is a minimizer; every minimizer $X^*$ satisfies $C^\top(CX^*-D)=0$ and $\|CX-D\|_F^2=\|C(X-X^*)\|_F^2+\|CX^*-D\|_F^2$.
• Lemma 37: for $A$ with orthonormal columns, $\|A(\tilde Y-Y^*)\|_F\le2\sqrt\varepsilon\|B-AY^*\|_F$.
• Theorem 39 (affine embeddings, an independent companion result of §7.5): under an embedding with parameter $\varepsilon\le1/2$ and the event of Lemma 32 with parameter $\varepsilon/\sqrt r$, $\|S(AX-B)\|_F^2-\|S\tilde B\|_F^2$ equals $\|AX-B\|_F^2-\|\tilde B\|_F^2$ up to $\pm2\varepsilon\|AX-B\|_F^2$ for all $X$, and $\|S(AX-B)\|_F^2=(1\pm3\varepsilon)\|AX-B\|_F^2$ if $S$ also preserves $\|\tilde B\|_F^2$ to $1\pm\varepsilon$.

Significance

Theorem 36 separates the algorithm design for sketched regression from its correctness proof: any random construction (CountSketch, subsampled randomized Hadamard transforms, leverage-score sampling, Gaussian matrices) yields a $(1+O(\varepsilon))$-approximate regression solver once it is shown to satisfy the two conditions with constant probability. Clarkson and Woodruff use it for their input-sparsity-time regression algorithm (Theorem 38) and, through Theorem 39 and affine embeddings, for low-rank approximation. The same conditions recur throughout the randomized numerical linear algebra literature (see Woodruff's survey Sketching as a Tool for Numerical Linear Algebra, 2014).

The results are proved in the paper (§7.3, §7.5 and Appendix A, p. 37). To our knowledge none has a machine-checked proof. Formalizing them produces a reusable, distribution-free layer of sketching theory: the probabilistic statements about specific sketches can then be proved separately and composed with it.

Difficulty

The obvious argument applies the subspace embedding to the residual $A\tilde Y-B$, but that vector does not lie in $C(A)$, so an embedding of $C(A)$ alone says nothing about it; embedding $C(A)$ augmented with the columns of $B$ instead costs a sketch dimension that grows with $d'$. The hypotheses of Theorem 36 control the optimal residual $B-AY^*$ only through the approximate-product condition, which is far weaker than norm preservation, and the difficulty is to transfer that control to the sketched solution (Lemma 37) with the constants $2\sqrt\varepsilon$ and $1+4\varepsilon$. A second obstacle is the passage from a general $A$ of rank at most $r$ to an orthonormal basis $U$ of $C(A)$: it changes $\|A\|_F$, which is why the approximate-product condition is stated for $U$.

Formalization scope

Matrices are Matrix (Fin m) (Fin n) ℝ; squared norms are explicit sums sqNorm and frobSq; the column space is the range of Matrix.mulVecLin; rank is Matrix.rank. Everything is deterministic: $S$ is an arbitrary fixed matrix and no probability space appears. The committed conventions are:

1. The subspace embedding is in squared form. In Theorem 36 and Lemma 37 its parameter $\eta$ plays the paper's $\epsilon_0^2$ (so $\epsilon_0\le1/\sqrt2$ becomes $\eta\le1/2$), which is how the proof of Lemma 37 (p. 37) uses it; in Theorem 39 the parameter is $\varepsilon$ itself, as that proof uses it.
2. "$S$ satisfies Lemma 32" is the event inside the probability, for the pair $(U,B-AY^*)$ (resp. $(U,\tilde B)$) that the proofs use, with $\le$ in place of the printed $<$ (a weaker hypothesis).
3. $\tilde Y$, $Y^*$, $X^*$ are arbitrary minimizers; "the solution" need not be unique. The Moore–Penrose inverse is specified by the four Penrose equations.
4. $r\ge1$ guards $\varepsilon/r$ and $\varepsilon/\sqrt r$; "$n>d$" (§7) concerns running times and is not assumed.

A trivializing formalization is ruled out: $\tilde Y$ is never defined as $Y^*$, the approximate-product hypothesis is an inequality and not the exact identity $U^\top S^\top S(B-AY^*)=0$, $\eta$ is non-negative, and the goal is stated for general $A$ of rank at most $r$, not only for orthonormal $A$. The hypotheses are jointly satisfiable (for instance $S=I$).

A complete development needs the Frobenius inner product and its Pythagorean identity, the normal equations for matrix least squares, the existence of the Moore–Penrose inverse, and the spectral-norm bound for a symmetric matrix from its quadratic form; all are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Theorem 36, are welcome.

Selected references

• K. L. Clarkson and D. P. Woodruff, Low Rank Approximation and Regression in Input Sparsity Time, arXiv:1207.6365v4, 2013; J. ACM 64(6), 2017. https://arxiv.org/abs/1207.6365
• P. Drineas, M. W. Mahoney, S. Muthukrishnan and T. Sarlós, Faster Least Squares Approximation, Numerische Mathematik 117(2), 2011. https://arxiv.org/abs/0710.1435
• T. Sarlós, Improved Approximation Algorithms for Large Matrices via Random Projections, FOCS 2006. https://doi.org/10.1109/FOCS.2006.37
• D. P. Woodruff, Sketching as a Tool for Numerical Linear Algebra, Foundations and Trends in Theoretical Computer Science 10(1–2), 2014. https://arxiv.org/abs/1411.4357

Why this market matters

An intermediary such as a ride platform must attract buyers and sellers who arrive at different times. A buyer may wait for a seller; a seller may wait for a buyer. Both sides can choose when to request a match, so an ask price and a bid price affect participation as well as the intermediary's margin. Chen and Hu study whether a simple posted-price policy remains profitable despite this waiting and the uncertainty of arrivals. Their submitted manuscript proves a finite-market guarantee and an asymptotic rate for the policy used here. The proof appears in its Supplemental Note, while the model and theorem are in the main text.

Market and benchmarks

Buyers arrive during a horizon $[0,T]$ as a Poisson process of rate $\lambda^d>0$, and sellers arrive independently at rate $\lambda^s>0$. A buyer's valuation $v$ has density $f^d$ on $[\underline v,\overline v]$ and a seller's cost $c$ has density $f^s$ on $[\underline c,\overline c]$. Marks are independent of arrival times. A buyer and a seller each trade at most one unit. If they wait after arrival, they incur costs $b$ and $h$ per unit time, respectively. The paper assumes regularity: the buyer's virtual value $V^d(v)=v-\bar F^d(v)/f^d(v)$ and the seller's virtual cost $V^s(c)=c+F^s(c)/f^s(c)$ are weakly increasing on their supports. Here $\bar F^d=1-F^d$.

A clairvoyant assignment knows all arrivals through $T$. For each possible buyer–seller pair it assigns virtual surplus $V^d(v)-V^s(c)$ less the waiting cost determined by their arrival order. It chooses a partial matching with greatest total value, denoted $\bar J(H^T)$. A separate fluid program chooses a measurable, nonnegative pair of price trajectories that clears demand and supply at every time. Its optimal value is $\bar J^*$. These are different objects: $\bar J(H^T)$ is random and uses indivisible agents, whereas $\bar J^*$ is a deterministic continuous-flow optimum. Lemma 2 of the manuscript compares their values in expectation.

Let $\mu^*$ be the greatest volume in $[0,\min\{\lambda^dT,\lambda^sT\}]$ with nonnegative marginal virtual surplus. The buyer and seller prices $p^*,w^*$ are inverse-distribution prices at that volume. Proposition 1 states that these constant prices attain the fluid optimum and $\bar J^*=(p^*-w^*)\mu^*$.

Formalization targets

The greedy matching policy pairs requests first come, first served. Under the waiting-adjusted fixed-price policy, a buyer's posted ask is $p^*$ minus $b$ times a conditional expected wait per match probability; the seller's posted bid is $w^*$ plus the corresponding $h$ term. The buyer adjustment is conditioned on the observed pre-arrival inventory signal. Agents request immediately exactly when their valuation or cost crosses the base-price threshold. The policy's expected profit $J$ is computed from posted prices paid by successfully matched agents.

The first target is the paper's finite-market bound:

$$\frac{J}{\bar J^*}\ge 1-\left(1+\frac{2(b+h)T}{3(p^*-w^*)}\right)\frac{1}{\sqrt{\mu^*}}.$$

When $J\ge0$, the benchmark comparison also gives $J/\mathbb E[\bar J(H^T)]\ge J/\bar J^*$. For scaled systems with arrival rates $n^{\alpha_d}\lambda^d$ and $n^{\alpha_s}\lambda^s$, where both exponents are positive, the second target is a constant $C$ independent of $n$ such that

$$\frac{J^{(n)}}{\bar J^{*,(n)}}\ge 1-\frac{C}{\sqrt{n^{\min\{\alpha_d,\alpha_s\}}}}\qquad(n\ge1).$$

The milestone list follows the source's Proposition 1, Lagrangian relaxation, Lemma 2, Poisson request counts, policy profit identity, Gallego–van Ryzin moment bound, and Lemma S.5 on arrival-rate monotonicity. The last three supply the finite bound and its scaling statement in the Supplemental Note.

What the result gives

The finite bound quantifies the cost of using fixed base prices and greedy matching instead of the fluid ideal. Its two terms separate the loss from random mismatch and the extra waiting adjustment. The scaled bound says that, as both sides' arrival rates grow, the fraction of the fluid value lost by this policy vanishes at a rate governed by the slower-growing side. This offers a concrete reason to use a simple policy when the market is large, while keeping the smaller-market correction visible.

The paper already proves these claims. This mission asks for machine-checked proofs of their precise statements. The fluid optimizer, the clairvoyant matching problem, the marked Poisson arrival model, and the policy-profit identity are reusable mathematical objects beyond this theorem. The positive-part moment bound is an already published theorem and is referenced rather than posed again.

Where the argument is difficult

The obvious comparison between posted-price profit and fluid revenue misses the cost of requests that wait or never match. The price corrections themselves are conditional expectations divided by conditional match probabilities; their effect cannot be captured by simply subtracting a constant waiting charge. The proof must connect those corrections to the time integral of the queue imbalance, then control the imbalance of two Poisson request streams. A second difficulty is that the fluid optimum and the expected clairvoyant optimum are defined through different feasible sets, so their comparison needs a separate relaxation argument. These obstacles are visible in the source's proof of Lemma 2 and Theorem 2.

Formalization scope

The density and virtual-value environment is the published bilateral-trade definition, imported through a local name alias required by the frozen shared market module. Lean represents arrivals by independent Poisson counts and independent identically distributed time-and-value marks. This is equal in law to the paper's homogeneous marked Poisson processes on $[0,T]$. Arrival time marks are uniform probability laws, and valuation and cost marks use the source densities. Simultaneous requests are ordered by index; such ties have probability zero. The deterministic program ranges over measurable, nonnegative, market-clearing paths with interval-integrable objective terms. Its value is the supremum of their objectives, not a formula involving $p^*$ and $w^*$; Proposition 1 must establish that formula. The clairvoyant value uses the published partial-assignment-game worth, so negative-weight pairs may remain unmatched.

The density functions are continuous on their supports, an explicit addition needed for the inverse prices and maximum volume used by Proposition 1. The lower support endpoints are nonnegative so the constant prices belong to the nonnegative fluid price domain; this fills an implicit domain convention in the manuscript. For Theorem 2 the overlap condition is strict, $\underline c<\overline v$, ensuring positive $\mu^*$ and $p^*-w^*$. The printed chain comparing $J/\mathbb E[\bar J]$ and $J/\bar J^*$ is stated under $J\ge0$: when the numerator is negative, the claimed direction fails. Both expectations used as finite numbers are accompanied by integrability conclusions. Division by a zero match probability at the terminal time uses a zero convention on a set of arrival times with probability zero.

The policy model builds in the myopic request behavior that Theorem 1 identifies as an equilibrium; its strategic proof is outside this mission. The policy profit is the expectation of actual posted-price payments, and the waiting compensations are literal tagged-arrival conditional ratios. Contributions that prove the inverse-distribution properties, Poisson thinning, queue profit identity, fluid optimization, or final moment estimate all address parts of the stated target.

Selected references

• Y. Chen and M. Hu, Pricing and Matching with Forward-Looking Buyers and Sellers, Manufacturing & Service Operations Management 22(4), 2020; submitted manuscript, SSRN 2859864.