Theoretical Computer Science

Motivation: cut metrics, flows and the planar embedding conjecture

A finite metric space embeds into $L_1$ exactly when its metric is a nonnegative combination of cut metrics $\delta_S(x,y)=|\mathbf 1_S(x)-\mathbf 1_S(y)|$. For this reason the least distortion with which a graph metric embeds into $L_1$ governs the gap between multicommodity flow and sparsest cut: Linial, London and Rabinovich (1995) and Aumann and Rabani (1998) connected metric embeddings to the approximate max-flow/min-cut theorem, and Gupta, Newman, Rabinovich and Sinclair (2004) proved that the worst flow–cut gap on a fixed graph equals the worst $L_1$ distortion of its weighted shortest-path metrics. They conjectured (the GNRS conjecture) that every proper minor-closed graph family embeds into $L_1$ with uniformly bounded distortion. The planar case has been the central open instance.

Timeline

• 1981 — Okamura and Seymour: multicommodity flows in planar graphs with all terminals on one face (JCTB 1981), giving isometric $L_1$ representations of one-face metrics.
• 1993 — Klein, Plotkin and Rao: decompositions of graphs excluding a fixed minor (STOC 1993).
• 1999 — Rao: every $n$-vertex planar metric embeds into $L_1$ (via Euclidean space) with distortion $O(\sqrt{\log n})$ (SoCG 1999).
• 2003 — Newman and Rabinovich: series-parallel metrics may need $\Omega(\sqrt{\log n})$ distortion into Euclidean space, so the Euclidean route cannot give a constant (DCG 2003).
• 2004 — Gupta, Newman, Rabinovich and Sinclair: constant distortion for series-parallel graphs, and the GNRS conjecture (Combinatorica 2004).
• 2006 — Chekuri, Gupta, Newman, Rabinovich and Sinclair: $k$-outerplanar graphs, with a bound exponential in $k$ (SIDMA 2006).
• 2008–2010 — Chakrabarti, Jaffe, Lee and Vincent: sharp bound $2$ for series-parallel graphs (FOCS 2008); Lee and Raghavendra: matching lower bound (DCG 2010). Lee and Sidiropoulos relate the planar case to the full conjecture (STOC 2009).
• 2013 — Sidiropoulos: constant distortion for planar metrics realized in nonpositively curved simply connected surfaces (FOCS 2013).
• 2019–2025 — Face-cover bounds by Krauthgamer, Lee and Rika (SODA 2019) and Filtser (TALG 2025); Abraham, Filtser, Gupta and Neiman recover Rao's bound via shortest-path decompositions (SICOMP 2022).
• 2026 — An OpenAI preprint, Planar Graph Metrics Embed into $L_1$ with Constant Distortion (OpenAI Math Release, September 23, 2026), claims the planar case of the GNRS conjecture. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

Let $G$ be a finite connected simple graph on vertex set $V=\{0,\dots,n-1\}$ with symmetric edge lengths $\ell(u,v)=\ell(v,u)>0$ on edges. The graph metric $d_G(x,y)$ is the infimum of $\sum\ell(e)$ over walks from $x$ to $y$. $G$ is planar if it has a drawing in $\mathbb R^2$: distinct points for vertices and, for each edge, an injective arc between its endpoints whose interior avoids every vertex and meets the interior of no other edge.

A map $f:V\to L_1(\Omega,\mu)$ into the real $L_1$ space of some measure space has distortion at most $C$ if $d_G(x,y)\le\|f(x)-f(y)\|_1\le C\,d_G(x,y)$ for all $x,y$.

Formalization targets

Goal: Theorem 1.1 (planar graph metrics in $L_1$)

There is a constant $C\ge1$ such that for every $n$, every connected planar graph $G$ on $n$ vertices and every symmetric positive edge-length function $\ell$, there are a measure space $(\Omega,\mathcal F,\mu)$ and $f:V\to L_1(\Omega,\mathcal F,\mu;\mathbb R)$ with

$$d_G(x,y)\;\le\;\|f(x)-f(y)\|_1\;\le\;C\,d_G(x,y)\qquad(x,y\in V).$$

The constant is not fixed: the goal asserts only existence, so any improvement of the constant is compatible with it. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem settles the planar case of the GNRS conjecture. By the Gupta–Newman–Rabinovich–Sinclair equivalence it gives a universal constant bound on the fractional flow–cut gap for arbitrary demands in planar graphs. With the bounded-treewidth companion preprint it also yields constant distortion for the fixed-parameter almost-embeddable families of Lee and Sidiropoulos (Corollary 10.1 of the source). The general clique-sum closure needed for the full GNRS conjecture is not established.

Formalizing it. The statement is elementary (finite graphs, arcs in the plane, an $L^1$ space), yet the proof combines a geometric column model of planar graphs, random multiscale cut constructions and packing estimates. A formal proof would certify every scale-combination step, where errors in uniformity are easy to make.

Difficulty

Standard random-partition methods for planar graphs separate pairs at each distance scale with good probability, but naive summation over scales costs a factor proportional to the number of scales, which is unbounded when edge lengths vary. Embedding first into Euclidean space cannot work: Newman–Rabinovich show $\Omega(\sqrt{\log n})$ Euclidean distortion is necessary already for series-parallel graphs. The difficulty is to combine separations at different scales while keeping a single uniform upper bound on every edge.

Formalization scope

• Vertices are Fin n; the graph is a SimpleGraph (Fin n) with G.Connected (so $n\ge1$). Singletons are allowed.
• IsPlanar G asks for an injective vertex placement in ℝ × ℝ and, for each ordered adjacent pair, an injective continuous arc on the unit interval with the right endpoints, whose interior avoids all vertex points and meets the interior of another arc only if it is the same unoriented edge.
• Edge lengths are a function Fin n → Fin n → ℝ, symmetric, and positive on adjacent pairs; values on non-adjacent pairs are irrelevant. graphDistance is the sInf of walk lengths; for a connected graph with nonnegative edge lengths the set of walk lengths is nonempty and bounded below, so the infimum is the genuine shortest-path distance.
• The target space is MeasureTheory.Lp Ω ℝ 1 μ for an existentially chosen measure space, and the inequalities are stated without a rescaling factor (the rescaling is absorbed into $f$).
• Infrastructure needed: plane drawings and their combinatorial consequences (rotation systems, noncrossing column models), cut-metric representations of $L_1$ metrics, and the probabilistic multiscale construction. Plane-drawing and cut-metric infrastructure is reusable.

Selected references

• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15 (1995). https://doi.org/10.1007/BF01200757
• Y. Aumann, Y. Rabani, An $O(\log k)$ approximate min-cut max-flow theorem and approximation algorithm, SIAM J. Comput. (1998). https://doi.org/10.1137/S0097539794285983
• A. Gupta, I. Newman, Y. Rabinovich, A. Sinclair, Cuts, trees and $\ell_1$-embeddings of graphs, Combinatorica (2004). https://doi.org/10.1007/s00493-004-0015-x
• S. Rao, Small distortion and volume preserving embeddings for planar and Euclidean metrics, SoCG 1999. https://doi.org/10.1145/304893.304983
• I. Newman, Y. Rabinovich, A lower bound on the distortion of embedding planar metrics into Euclidean space, Discrete Comput. Geom. (2003). https://doi.org/10.1007/s00454-002-2813-5
• C. Chekuri, A. Gupta, I. Newman, Y. Rabinovich, A. Sinclair, Embedding $k$-outerplanar graphs into $\ell_1$, SIAM J. Discrete Math. (2006). https://doi.org/10.1137/S0895480102417379
• A. Chakrabarti, A. Jaffe, J. R. Lee, J. Vincent, Embeddings of topological graphs: lossy invariants, linearization, and 2-sums, FOCS 2008. https://doi.org/10.1109/FOCS.2008.79
• J. R. Lee, A. Sidiropoulos, On the geometry of graphs with a forbidden minor, STOC 2009. https://doi.org/10.1145/1536414.1536450
• A. Sidiropoulos, Non-positive curvature and the planar embedding conjecture, FOCS 2013. https://doi.org/10.1109/FOCS.2013.27
• I. Abraham, A. Filtser, A. Gupta, O. Neiman, Metric embedding via shortest path decompositions, SIAM J. Comput. (2022). https://doi.org/10.1137/19M1296021
• A. Filtser, A face cover perspective to $\ell_1$ embeddings of planar graphs, ACM Trans. Algorithms (2025). https://doi.org/10.1145/3686800
• OpenAI, Planar Graph Metrics Embed into $L_1$ with Constant Distortion, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Planar-Graph-Metrics-Embed-into-L1-with-Constant-Distortion-September-23-2026/paper.pdf

Motivation

In the local model of differential privacy, each individual randomizes their own data before handing it to an untrusted learner. Local protocols are the deployed form of private data collection, and in practice every round of interaction with the population is expensive: the learner must broadcast new instructions and wait for new reports. Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith, What Can We Learn Privately? (arXiv:0803.0924v3, published in SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090; theorem numbers below are those of arXiv v3) show that local learning is equivalent to learning with statistical queries (SQ) in the sense of Kearns (1998), and that the equivalence maps noninteractive local learners to nonadaptive SQ learners. The question whether interaction is ever necessary in the local model therefore becomes the question whether adaptivity is ever necessary for SQ learning.

This mission formalizes the paper's answer (§5.3, Theorem 5.16): a concept class, MASKED-PARITY, that an adaptive SQ learner learns exactly with $d+1$ queries in two rounds, while every nonadaptive SQ learner with fewer than exponentially many queries fails against a specific valid oracle, under the uniform distribution on examples.

Setting

Fix $d$, a power of two. The domain is $D=\{0,1\}^d\times\{0,1\}^{\log d}\times\{0,1\}$, with points $u=(x,i,b)$, and examples are drawn from the uniform distribution $\mathcal D$ on $D$. For $r\in\{0,1\}^d$ and $a\in\{0,1\}$, the concept $c_{r,a}:D\to\{+1,-1\}$ is

$$c_{r,a}(x,i,b)=\begin{cases}(-1)^{r\odot x+a}&b=0,\\(-1)^{r_i}&b=1,\end{cases}$$

where $r\odot x$ is the inner product modulo 2. MASKED-PARITY is the class $\{c_{r,a}\}$: on the half $b=0$ it is the parity $r$ or its negation, according to the mask $a$; on the half $b=1$ it reveals the bit $r_i$.

A statistical query is a function $g(u,y)$ of an example and a label together with a tolerance $\tau$. The SQ oracle for the target $c$ answers with any real $v$ such that $|v-\mathbb E_{u\sim\mathcal D}[g(u,c(u))]|\le\tau$; the learner must succeed for every such answer. An SQ learner is nonadaptive if it fixes all its queries before receiving any answer, and adaptive otherwise. Write $\langle f,h\rangle=\mathbb E_{u\sim\mathcal D}[f(u)h(u)]$ and $\mathrm{err}(f,h)=\Pr_{u\sim\mathcal D}[f(u)\ne h(u)]$.

The lower bound uses the decomposition of a query into $f_g(u)=\frac{g(u,1)-g(u,-1)}2$ and $C_g=\frac12\mathbb E[g(u,1)+g(u,-1)]$, the restrictions $c^s_{r,a}$, $f^s_g$ of $c_{r,a}$ and $f_g$ to the half $b=s$ (equation (6)), and the oracle

$$\mathcal O_{c_{r,a},\mathcal D}(g,\tau)=\begin{cases}C_g+\langle f^1_g,c^1_{r,a}\rangle&\text{if }|\langle f^0_g,c^0_{r,a}\rangle|<\tau,\\ \mathbb E[g(u,c_{r,a}(u))]&\text{otherwise.}\end{cases}$$

Formalization targets

Goal: Theorem 5.16 (p. 27)

1. There is a two-round SQ learner ($d$ queries, then one), with $\{0,1\}$-valued queries of tolerance at least $\frac1{4d+1}$, that outputs $c_{r,a}$ for every target and every valid answers.
2. $\mathcal O$ is a valid SQ oracle, and every nonadaptive learner making $t$ queries with values $\pm1$ and tolerance at least $2^{-d/3}$, run against $\mathcal O$ on a uniformly random target, satisfies

$$\Pr_{c_{\bar r,\bar a}}\Bigl[\mathrm{err}(c_{\bar r,\bar a},h)\ge\tfrac14\Bigr]\ge\frac12-\frac t{2^{d/3+2}}.$$

Milestones

• Proposition 5.18 (p. 28): the learner $\mathcal A_{\mathrm{MP}}$ recovers $\hat r=r$ and $\hat a=a$ from every valid answers.
• Equation (7) (p. 29): $\mathbb E[g(u,c_{r,a}(u))]=C_g+\langle f^0_g,c^0_{r,a}\rangle+\langle f^1_g,c^1_{r,a}\rangle$.
• The oracle (p. 30): $\mathcal O$ is valid and answers identically on $c_{r,0}$ and $c_{r,1}$ when $|\langle f^0_g,c^0_{r,0}\rangle|<\tau$.
• Orthogonality (p. 30): $\langle c^0_{r,a},c^0_{r',a}\rangle$ is $1/2$ if $r=r'$ and $0$ otherwise.
• Bessel bound (p. 30): $\sum_{(r,a)}2\langle f^0_g,c^0_{r,a}\rangle^2\le1$ for $\pm1$-valued $g$.
• Counting (p. 30): at most $2^{2d/3-1}$ pairs $(r,a)$ have $|\langle f^0_g,c^0_{r,a}\rangle|\ge2^{-d/3}$.
• $\Pr[\mathit{Good}]\ge1-t/2^{d/3+2}$ (p. 30).

Significance

The result. Combined with the paper's equivalence between local and SQ learning (Theorem 5.14), Theorem 5.16 shows that interaction is sometimes necessary in local differential privacy: there is a class learnable by an interactive local protocol with polynomially many examples, but not by any noninteractive one with fewer than exponentially many (Corollary 5.17). The separation concerns strong learning under a fixed distribution; the paper notes that adaptive and nonadaptive SQ learning coincide for weak learning, and that a distribution-free separation was left open.

Formalizing it. The result is proved in the paper and has, to our knowledge, no machine-checked proof. The mission produces a self-contained Lean model of statistical query learning with labelled queries and adversarial oracles, a finite Fourier calculus for parities on $\{0,1\}^d$ (orthogonality and a Bessel inequality for $\pm1$-valued functions), and the counting and union-bound argument of SQ lower bounds. The proof of part (2) contains several printed slips (listed below); a formal proof settles the corrected argument.

Difficulty

The upper bound is a direct computation. The difficulty is in part (2): the learner's hypothesis may be any function, not a concept of the class, and the lower bound must hold for every nonadaptive strategy at once. A naive argument that each query "reveals little about $a$" fails, because the true answer to a query does depend on $a$; the argument needs an oracle that is valid (within tolerance of the truth) and yet independent of $a$ on most targets, and a quantitative bound on how many targets any single $\pm1$-valued query can correlate with on the half $b=0$. That bound is an $L^2$ statement over all $2^{d+1}$ concepts, not a pointwise one.

Formalization scope

• Domain and distribution. The index $i\in\{0,1\}^{\log d}$ is encoded as Fin d, and every theorem assumes $d=2^m$ (implicit in the paper). Vectors are Fin d → ZMod 2, with 0-based bits. Expectations are averages over the finite domain; probabilities over the target are counts of pairs $(r,a)$ divided by $2^{d+1}$.
• Values. Concepts, hypotheses and queries are real-valued; labels $\pm1$ are reals. Queries in part (1) take values in $\{0,1\}$, as $\mathcal A_{\mathrm{MP}}$'s do; queries in part (2) take values $\pm1$ on labels $\pm1$, as in the paper's proof. The paper allows non-Boolean queries (p. 19); a version of part (2) for real queries with values in $[-1,1]$ is a true strengthening that the same argument supports, and is not stated.
• Oracles. An SQ oracle is adversarial within the tolerance: the upper bound holds for every valid answer. Part (2) exhibits the paper's oracle $\mathcal O$ and asserts its validity for every $\tau>0$. Without that conjunct an "oracle" that ignores the tolerance would make part (2) trivial; the statement rules this out.
• Learners. Learners are deterministic structures (a nonadaptive learner is a list of queries and tolerances plus an output map; a two-round learner's second-round queries are functions of the first-round answers). A randomized learner is a mixture over its coins and the bounds hold coin by coin. "Efficient" is not modelled. The informal "with a polynomial number of queries" is formalized through its quantitative "Specifically" sentence.
• Real powers. $2^{d/3}$, $2^{2d/3-1}$ and $2^{d/3+2}$ are real powers; no natural-number division is used.
• Corrections of the proof (not of the theorem). The event $\mathit{Good}$ on p. 30 is printed with $c_{\bar r,\bar a}$ and $\le$; the milestone uses $c^0_{\bar r,\bar a}$ and the strict $<$, which is what the counting display and the oracle's test require. The quotient $2^{2d/3-1}/2^{d+1}$ is printed as $2^{-d/3}$ and equals $2^{-d/3-2}$; "$c^0_{r,0}=-c^0_{r,0}$" should read $c^0_{r,1}=-c^0_{r,0}$. The final display of the proof gives $\frac12(1-t/2^{d/3+2})$, which is at least the theorem's bound.

Contributions welcome: the Fourier facts for $\{0,1\}^d$ (reusable for any parity-based SQ lower bound), the general decomposition (7), and the probability bound of part (2) from the milestones.

Selected references

• S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, A. Smith, What Can We Learn Privately?, SIAM J. Comput. 40(3) (2011) 793–826. arXiv:0803.0924v3, DOI 10.1137/090756090.
• M. Kearns, Efficient noise-tolerant learning from statistical queries, J. ACM 45(6) (1998) 983–1006. DOI 10.1145/293347.293351.
• A. Blum, M. Furst, J. Jackson, M. Kearns, Y. Mansour, S. Rudich, Weakly learning DNF and characterizing statistical query learning using Fourier analysis, STOC 1994. DOI 10.1145/195058.195147.
• N. Bshouty, V. Feldman, On using extended statistical queries to avoid membership queries, J. Mach. Learn. Res. 2 (2002) 359–395. JMLR.

Motivation

In the local model of differential privacy, no trusted curator holds the data: each individual randomizes their own record before handing it to the analyst. This is the model of randomized response in survey statistics and of the privacy-preserving telemetry deployed by large software vendors. Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith, What Can We Learn Privately? (arXiv:0803.0924v3, published in SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090), asked which learning tasks remain possible in this model. Their answer (§5) is that local algorithms are exactly as powerful as statistical query (SQ) algorithms in the sense of Kearns (J. ACM 1998), up to polynomial factors. This mission formalizes one direction of that equivalence: every local algorithm run on i.i.d. data can be simulated by an SQ algorithm.

This is the fourth of five missions on the paper. Mission III formalizes the converse direction (Theorem 5.7). All theorem numbers refer to arXiv:0803.0924v3.

Setting

A database is $z=(z_1,\dots,z_n)\in D^n$. Here its entries are drawn i.i.d. from a probability distribution $P$ on $D$.

• An $\varepsilon$-local randomizer (Definition 5.1) is a randomized map $R:D\to W$ to a discrete set $W$ such that $\Pr[R(u)=w]\le e^{\varepsilon}\Pr[R(u')=w]$ for all $u,u'\in D$ and $w\in W$.
• An $\varepsilon$-local algorithm $A$ making $t$ queries (Definitions 5.2, 5.3) sees the database only through an LR oracle. At its $k$-th call it names an index $i_k$ and an $\varepsilon_k$-local randomizer $R_k$, both possibly depending on its earlier answers, and receives a fresh sample of $R_k(z_{i_k})$. For each index $i$ the budgets of the calls on $i$ sum to at most $\varepsilon$. $A$ is noninteractive if its calls do not depend on earlier answers. Its output is a function of the $t$ answers. Its output distribution is taken over $z\sim P^n$ and the randomizers' coins.
• An SQ oracle for $P$ (Definition 5.4) answers a query $(g,\tau)$, with $g:D\to[-1,1]$ and tolerance $\tau$, with any number $v$ such that $|v-\mathbb E_{u\sim P}[g(u)]|\le\tau$. It may choose its answers adversarially and adaptively.
• An SQ algorithm $B$ (Definition 5.5) accesses $P$ only through such an oracle. It may use its own coins, and the number of queries it makes may be random and unbounded.
• The statistical difference of two distributions on a discrete space (p. 8) is $\max_S|\mu(S)-\nu(S)|$.

Formalization targets

Goal: Lemma 5.8 (p. 21)

There is an absolute constant $C$ such that for every $\varepsilon$-local algorithm $A$ making $t$ queries there is an SQ algorithm $B$ with the following properties against every distribution $P$ and every valid oracle:

$$\tau=\frac{\beta}{3e^{2\varepsilon}t},\qquad \mathbb E[\#\text{queries of }B]\le C\,t\,e^{\varepsilon},\qquad \mathrm{SD}\bigl(B,\ A(z),\ z\sim P^n\bigr)\le\beta .$$

The constant $C$ is the paper's $O(\cdot)$. The tolerance is the proof's own choice.

Milestones

1. Display (5) (p. 22): a single query estimates $p(w)=\Pr_{z_i\sim P}[R(z_i)=w]$ within a factor $1\pm\beta/(3t)$, whatever valid answer the oracle gives.
2. One rejection-sampling iteration (p. 23): every iteration terminates with probability at least $\frac{1-\varphi}{1+\varphi}e^{-\varepsilon}$. Conditioned on terminating, it outputs $w$ with probability in $(1\pm3\varphi)p(w)$.
3. The interactive estimate (p. 24): two queries estimate the conditional probability of the next answer given earlier answers on the same entry, within a factor $1\pm3e^{2\varepsilon}\tau$.
4. Claim 5.9 (p. 22): the noninteractive case, with the explicit bound $2t\,e^{\varepsilon}$ on the expected number of queries.

Significance

The result. Lemma 5.8, combined with Theorem 5.7, shows that a concept class is learnable by a locally private algorithm if and only if it is learnable with statistical queries (Theorem 5.14). Every SQ lower bound therefore becomes a lower bound for local privacy. For instance, parity functions are privately learnable by a centralized algorithm (Theorem 4.4) but not by a local one, because parities need exponentially many statistical queries (Corollary 5.15, which also uses the SQ lower bound of Blum et al., STOC 1994).

Formalizing it. The result is proved on paper. As far as we know it has no machine-checked proof. The paper's proof is a few paragraphs and leaves the model implicit: what an SQ algorithm with a random number of queries is, how an adversarial oracle interacts with it, and in what sense the per-randomizer errors add up over $t$ adaptively chosen randomizers. The formal statement makes each of these explicit. The milestones isolate the estimates the proof uses, so they can be proved independently of the composition argument.

Difficulty

The estimates in the milestones are elementary inequalities. The difficulty is in the goal. First, the oracle's answers, and therefore the estimates $\tilde p(w)$, change from iteration to iteration, so the simulated distribution is not a fixed rejection sampler: the output law must be controlled iteration by iteration against an adversary. Second, the SQ algorithm has no bound on its number of steps. Its output law is a limit over an unbounded run, and its query count is an expectation that is finite only because every iteration terminates with probability bounded away from zero. Third, in the interactive case the randomizers applied to one entry are correlated through the entry. The simulation must sample from the conditional law given earlier answers on that entry, while the errors of all $t$ steps combine along adaptively chosen histories.

Formalization scope

• Local randomizers have discrete output: R u : PMF W. The simulation uses the point probabilities $\Pr[R(z_i)=w]$. Every map $u\mapsto\Pr[R(u)=w]$ is required to be measurable.
• A local algorithm makes exactly $t$ calls. Its index, randomizer and budget at call $k$ are functions of the earlier answers. The budget is required along every answer sequence. Its own coins are calls to $0$-local randomizers.
• An SQ algorithm is a state machine with a random start, random transitions depending on the answer, and an output on stopping. Its output law is a sub-probability mass function. Its expected query count lies in $[0,\infty]$ and counts every query, including those in rejected iterations.
• The oracle is an arbitrary deterministic function of the whole state trajectory, constrained only by Definition 5.4. The conclusions must hold for every valid oracle, not for the exact-mean oracle alone.
• $B$ is quantified before $P$ and sees $P$ only through answers, and every query of $B$ is a measurable $[-1,1]$-valued function with tolerance exactly $\beta/(3e^{2\varepsilon}t)$. Without these two constraints the statement would be trivial: $B$ could hard-code $P$, or rescale a query to shrink its effective tolerance.
• The constant $C$ is quantified outside every other object.
• The implicit hypotheses $\varepsilon>0$ (the queries divide by $e^{\varepsilon}-e^{-\varepsilon}$), $0<\beta\le1$ and $t\ge1$ (so that $\varphi=\beta/(3t)\le1/3$ and $\tau$ is defined) are stated. The paper's reference input $\mathbf 0$ is an arbitrary point $u_0\in D$.
• Claim 5.9 states "$t\cdot e^{\varepsilon}$ queries". Its proof gives at most $2t\,e^{\varepsilon}$, which is the bound stated.
• The paper's refinement "noninteractive $A$ yields nonadaptive $B$" is not formalized. The simulation decides from each answer whether to stop, and so which randomizer the next query belongs to. It therefore does not prepare its queries before receiving answers in the sense of Definition 5.5. The goal is the adaptive statement for all local algorithms, which contains the noninteractive case. Claim 5.10, whose statement coincides with this goal, is represented by its estimate (milestone 3) rather than restated.
• The statistical difference is valued in $[0,\infty]$, which avoids junk values of a real supremum.

Reusable beyond this mission: the SQ-algorithm state machine with expected query count, the statistical difference of sub-probability mass functions, and the model of interactive local algorithms. Welcome contributions include proofs of the estimate milestones, a general lemma bounding the statistical difference of sequentially composed approximate samplers, and the termination and expected-runtime analysis of rejection sampling with varying acceptance probabilities.

Selected references

• S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, A. Smith, What Can We Learn Privately?, SIAM J. Comput. 40(3) (2011) 793–826; cited from arXiv:0803.0924v3. https://arxiv.org/abs/0803.0924 · https://doi.org/10.1137/090756090
• M. Kearns, Efficient noise-tolerant learning from statistical queries, J. ACM 45(6) (1998) 983–1006. https://doi.org/10.1145/293347.293351
• A. Blum, M. Furst, J. Jackson, M. Kearns, Y. Mansour, S. Rudich, Weakly learning DNF and characterizing statistical query learning using Fourier analysis, STOC 1994, 253–262. https://doi.org/10.1145/195058.195147
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating noise to sensitivity in private data analysis, TCC 2006. https://doi.org/10.1007/11681878_14
• S. L. Warner, Randomized response: a survey technique for eliminating evasive answer bias, J. Amer. Statist. Assoc. 60 (1965) 63–69. https://doi.org/10.1080/01621459.1965.10480775

Motivation

The learning with errors (LWE) problem underlies much of post-quantum public-key cryptography, and its hardness rests on Regev's reduction from worst-case lattice problems to LWE (Regev, J. ACM 2009). Every step of that reduction is calibrated by the smoothing parameter $\eta_\epsilon(L)$ of Micciancio and Regev (SIAM J. Comput. 2007): the Gaussian width above which a discrete Gaussian on a lattice behaves like a continuous one. The approximation factors of the reduction are stated in terms of $\eta_\epsilon(L)$, and they are converted into factors for the standard lattice problems (GapSVP, SIVP) by comparing $\eta_\epsilon(L)$ with the successive minima of $L$ and of its dual.

Upper bounds on $\eta_\epsilon(L)$ (Lemmas 2.11 and 2.12 of the paper, from Micciancio–Regev) say the smoothing parameter is not too large. Claim 2.13 is the matching lower bound: the smoothing parameter cannot be much smaller than $1/\lambda_1(L^*)$, and hence than $\lambda_n(L)/n$. The second comparison goes through Banaszczyk's transference theorem (Banaszczyk, Math. Ann. 296 (1993)), $1 \le \lambda_1(L)\lambda_n(L^*) \le n$, which relates the geometry of a lattice to that of its dual.

This mission formalizes Claim 2.13 from the published J. ACM article (Article 34, 2009), together with the steps of its proof and the transference theorem it cites. The paper's main theorem, Theorem 3.1, is a quantum reduction about efficient algorithms; it is outside this series of missions.

Setting

Work in $\mathbb{R}^n$, $n \ge 1$, with the Euclidean norm $\|\cdot\|$ and inner product $\langle\cdot,\cdot\rangle$. A lattice $L \subset \mathbb{R}^n$ is the set of integer combinations of $n$ linearly independent vectors. Its dual is

$$L^* = \{y \in \mathbb{R}^n : \langle x, y\rangle \in \mathbb{Z} \text{ for all } x \in L\},$$

again a lattice, with $(L^*)^* = L$.

The successive minima used here are $\lambda_1(L)$, the length of a shortest nonzero vector of $L$, and $\lambda_n(L)$, the least $r$ such that $L$ contains $n$ linearly independent vectors of length at most $r$.

For $s > 0$ the Gaussian function is $\rho_s(x) = \exp(-\pi\|x/s\|^2)$ (Eq. (4)), and for a countable set $A$, $\rho_s(A) = \sum_{x\in A}\rho_s(x)$. In particular $\rho_{1/s}(y) = \exp(-\pi s^2\|y\|^2)$.

For $\epsilon > 0$ the smoothing parameter $\eta_\epsilon(L)$ is the smallest $s$ such that $\rho_{1/s}(L^*\setminus\{0\}) \le \epsilon$ (Definition 2.10).

Formalization targets

Goal: Claim 2.13 (p. 34:20)

For any lattice $L$ and any $\epsilon > 0$,

$$\eta_\epsilon(L) \;\ge\; \sqrt{\frac{\ln 1/\epsilon}{\pi}}\cdot\frac{1}{\lambda_1(L^*)} \;\ge\; \sqrt{\frac{\ln 1/\epsilon}{\pi}}\cdot\frac{\lambda_n(L)}{n}.$$

Both inequalities of the chain are part of the goal. The asymptotic "In particular" sentence of the claim ($\epsilon(n) = o(1)$, large enough $n$) is not.

Milestones, in attack order

1. The remark after Definition 2.10 (p. 34:19). The map $s \mapsto \rho_{1/s}(L^*\setminus\{0\})$ is continuous and strictly decreasing on $(0,\infty)$, tends to $\infty$ as $s \to 0$ and to $0$ as $s \to \infty$, and $\epsilon \mapsto \eta_\epsilon(L)$ is its inverse; in particular $\rho_{1/\eta_\epsilon(L)}(L^*\setminus\{0\}) = \epsilon$.
2. The display of the proof of Claim 2.13 (p. 34:20). For $s = \eta_\epsilon(L)$ and $v \in L^*$ of length $\lambda_1(L^*)$,

$$\epsilon = \rho_{1/s}(L^*\setminus\{0\}) \ge \rho_{1/s}(v) = \exp\bigl(-\pi(s\lambda_1(L^*))^2\bigr).$$

3. Lemma 2.3, Banaszczyk's transference theorem (p. 34:18). For any $n$-dimensional lattice $L$,

$$1 \le \lambda_1(L)\cdot\lambda_n(L^*) \le n .$$

Significance

The result. Claim 2.13 shows that the smoothing parameter for a negligible $\epsilon$ exceeds every constant multiple of $1/\lambda_1(L^*)$ and of $\lambda_n(L)/n$. Together with the upper bound $\eta_\epsilon(L) \le \sqrt{\ln(2n(1+1/\epsilon))/\pi}\,\lambda_n(L)$ of Lemma 2.12, it locates $\eta_\epsilon(L)$ within a polynomial factor of $\lambda_n(L)$. This is what lets the reduction's guarantees, phrased in $\eta_\epsilon(L)$, be read as approximation factors for SIVP and GapSVP. The transference theorem is used throughout the geometry of numbers and in lattice-based cryptography to pass between a lattice and its dual.

Formalizing it. The claim and its proof are classical and short, but neither is machine-checked. The mission produces formal definitions of the dual lattice, the successive minima $\lambda_1$, $\lambda_n$ and the smoothing parameter on EuclideanSpace ℝ (Fin n), a proof that Definition 2.10 is well posed, and a statement of Banaszczyk's transference theorem. The upper bound of the transference theorem is a substantial result in its own right (the paper cites it without proof), and a formal proof of it would be reusable well beyond this mission.

Difficulty

The first inequality of the goal is elementary once the smoothing parameter is known to be attained, with $\rho_{1/\eta}(L^*\setminus\{0\}) = \epsilon$ exactly. That step is not a formality: it needs the continuity and strict monotonicity of an infinite lattice sum in the scale parameter, and the fact that a shortest nonzero dual vector exists, both of which rest on the discreteness of $L^*$.

The second inequality is a single line in the paper, "by Lemma 2.3", but it uses the upper bound of Banaszczyk's theorem, applied to the dual lattice. The easy lower bound $1 \le \lambda_1(L)\lambda_n(L^*)$ does not suffice, and a Minkowski-type argument gives a bound worse than linear in $n$. Applying the lemma to $L^*$ also needs $L^*$ to be a lattice with dual $L$.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n). A lattice is L : Submodule ℤ _ with [DiscreteTopology L] [IsZLattice ℝ L]. The dual is LinearMap.BilinForm.dualSubmodule (innerₗ _) L.
• Every theorem assumes $0 < n$: the paper's lattices are $n$-dimensional with $n \ge 1$. This is the only added hypothesis.
• Gaussian sums are real tsums. They are summable over discrete subgroups, so no summability hypotheses are added.
• $\eta_\epsilon(L)$, $\lambda_1$ and $\lambda_n$ are infima (sInf). The paper's "smallest" is the attainment proved in milestones 1 and 2, not built into the definition. $\lambda_1$ and $\lambda_n$ are defined for every $\mathbb{Z}$-submodule, so they apply to $L^*$ without extra instances.
• For $\epsilon \ge 1$ the paper's $\sqrt{\ln(1/\epsilon)/\pi}$ is the square root of a non-positive number; Lean's Real.sqrt gives $0$ there and the goal reduces to true statements. No hypothesis $\epsilon < 1$ is added, since the page says "any $\epsilon > 0$".
• The goal is a conjunction of both inequalities of the chain, not only the outer comparison $\eta_\epsilon(L) \ge \sqrt{\ln(1/\epsilon)/\pi}\,\lambda_n(L)/n$, which would be weaker. Lemma 2.3 states both bounds; stating only the easy lower bound would leave the goal's second inequality without its milestone.
• No printed statement needed correction.

Contributions welcome: the attainment of $\lambda_1$ and $\lambda_n$ for IsZLattice (and for the dual), the identity $(L^*)^* = L$ in this setting, continuity and monotonicity of Gaussian lattice sums, and above all Banaszczyk's transference theorem.

Selected references

• O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, J. ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
• W. Banaszczyk, New bounds in some transference theorems in the geometry of numbers, Math. Ann. 296, 625–635, 1993. https://doi.org/10.1007/BF01445125
• D. Micciancio, O. Regev, Worst-case to average-case reductions based on Gaussian measures, SIAM J. Comput. 37(1), 267–302, 2007. https://doi.org/10.1137/S0097539705447360

Motivation

Randomized load balancing asks how much a dispatcher gains from a little information. In the supermarket model, jobs arrive at $n$ servers and each job inspects a few servers chosen at random before joining one. With one random choice every server is an independent M/M/1 queue, and the expected time a job spends in the system is $1/(1-\lambda)$ at load $\lambda$. With two choices it is exponentially smaller as $\lambda \to 1^-$. This "power of two choices" underlies the design of distributed schedulers, hashing schemes and server farms, where querying every server is too expensive but querying two is cheap.

Timeline:

• 1994/1999. Azar, Broder, Karlin and Upfal proved the static version, balanced allocations: throwing $n$ balls into $n$ bins with $d \ge 2$ choices per ball gives a maximum load of $\log\log n/\log d + O(1)$ w.h.p., against $\Theta(\log n/\log\log n)$ for one choice (SIAM J. Comput. 1999).
• 1996. Vvedenskaya, Dobrushin and Karpelevich derived the dynamic limiting equations for $d = 2$ and showed convergence of their trajectories to the fixed point, without a rate (Problems of Information Transmission 32(1), 1996).
• 1996/2001. Mitzenmacher, independently, introduced the limiting system for general $d$, proved doubly exponential tails along every trajectory and exponential convergence to the fixed point in a weighted $L_1$ potential, and derived the limiting expected time $T_d(\lambda)$ (IEEE TPDS 2001). This mission formalizes Section 2 of that paper.

Setting

Customers arrive as a Poisson stream of rate $\lambda n$, $0<\lambda<1$, at $n$ FIFO servers. Each customer chooses $d$ servers independently and uniformly at random with replacement and joins the one holding the fewest customers; service times are exponential with mean $1$. Let $s_i(t)$ be the fraction of servers holding at least $i$ customers at time $t$.

A state is a sequence $s = (s_0, s_1, s_2, \dots)$ of reals with $s_0 = 1$, $s_i \ge 0$ and $s_0 \ge s_1 \ge s_2 \ge \cdots$. The empty state has $s_0 = 1$ and $s_i = 0$ for $i \ge 1$. As $n \to \infty$ the tails follow the limiting system

$$\frac{ds_i}{dt} = \lambda\,(s_{i-1}^d - s_i^d) - (s_i - s_{i+1}) \quad (i \ge 1), \qquad s_0 = 1. \tag{1}$$

A trajectory is a map $t \mapsto s(t)$, $t \ge 0$, whose values are states and whose coordinates satisfy (1) (from the right at $t = 0$). Throughout, $d \ge 2$ is an integer.

The fixed point is $\pi_i = \lambda^{(d^i - 1)/(d - 1)}$, so $\pi_0 = 1$, $\pi_1 = \lambda$, $\pi_2 = \lambda^{1+d}$. A customer arriving in state $s$ becomes the $i$-th customer of its queue with probability $s_{i-1}^d - s_i^d$ and then waits for $i$ services, so the expected time it spends in the system is

$$E(s) = \sum_{i=1}^{\infty} i\,(s_{i-1}^d - s_i^d).$$

The target constant is

$$T_d(\lambda) = \sum_{i=1}^{\infty} \lambda^{\frac{d^i - d}{d-1}}.$$

Formalization targets

Goal: Corollary 2

For $d \ge 2$ and $0 < \lambda < 1$, $T_d(\lambda) < \infty$, and:

$$\text{if } s_j(0) = 0 \text{ for some } j, \text{ then } E(s(t)) \xrightarrow[t\to\infty]{} T_d(\lambda);\qquad \text{if } s(0) \text{ is empty, then } E(s(t)) \le T_d(\lambda) \ \ \forall t \ge 0.$$

The hypothesis $s_j(0) = 0$ holds for every initial state that comes from a finite system.

Milestones, in the order the proof uses them

• Lemma 2. $\pi$ is the unique fixed point of (1) with $\sum_{i\ge1} s_i < \infty$.
• Theorem 2. If $s_j(0) = 0$ for some $j$, there are constants $N \ge 1$, $0<\alpha<1$, $\beta>1$, $\gamma>0$, independent of $t$, with $s_i(t) \le \gamma\,\alpha^{\beta^i}$ for all $i \ge N$, $t \ge 0$. From the empty state, $s_i(t) \le \pi_i$ for all $i$ and $t \ge 0$.
• Theorem 3. There are weights $w_i \ge 1$ such that $\Phi(t) = \sum_{i\ge1} w_i |s_i(t) - \pi_i|$ satisfies $\Phi(t) \le c_0 e^{-\delta t}$ ($\delta > 0$) whenever $\Phi(0) < \infty$, and in particular whenever $s_j(0) = 0$ for some $j$.
• Corollary 1. Under the conditions of Theorem 3 (weights $w_i \ge 1$ fixed before the trajectory, with $\Phi(0) < \infty$, or $s_j(0) = 0$ for some $j$), $\sum_{i\ge1} |s_i(t) - \pi_i| \le c_0 e^{-\delta t}$.
• Proof of Corollary 2, display. $\sum_{i\ge1} i(s_{i-1}^d - s_i^d) = \sum_{i\ge0} s_i^d$ for a state with $s_i \to 0$.
• Lemma 4. The drift of (1) is Lipschitz in $\ell^1$ on states, with constant $2 + 2d\lambda$.

Significance

The comparison $T_1(\lambda) = 1/(1-\lambda)$ against $T_d(\lambda)$ is the quantitative content of the power of two choices: the companion mission shows $T_d(\lambda)/\log T_1(\lambda) \to 1/\log d$ as $\lambda \to 1^-$, an exponential improvement. Corollary 2 is what connects that number to the dynamics: it says the fixed point's expected time is actually reached from realistic initial states, and is an upper bound from an empty start. Theorem 2's comparison argument and Theorem 3's weighted potential are reused across the mean-field analysis of load-balancing variants (threshold policies, heterogeneous servers, work stealing), so the formal statements here are templates for that literature.

All results are proved in the paper (Theorem 3's proof is written out for $d = 2$ with a remark that it extends). None has a machine-checked proof that we know of. The work is formalizing the known arguments for all $d \ge 2$, including the parts the paper delegates to a citation: quasimonotone comparison for countable ODE systems in Theorem 2, and the upper right Dini derivative handling of $|\epsilon_i|$ in Theorem 3.

Difficulty

The system is infinite-dimensional, so standard finite-dimensional ODE comparison and Lyapunov theorems do not apply as stated. Theorem 2 rests on a monotonicity property (raising the initial tails raises them for all time) that the paper justifies by a coupling intuition and a citation to a comparison theorem for quasimonotone systems; that theorem must be supplied for $\ell^\infty$-bounded countable systems. The plain $L_1$ distance is nonincreasing along trajectories but does not decay exponentially by a direct estimate; the weights $w_i$ must be built so that every coordinate's contribution to $d\Phi/dt$ is dominated by $-\delta w_i |\epsilon_i|$, while staying geometrically bounded so that $\Phi(0) < \infty$ under the doubly exponential tails of Theorem 2. Exchanging $t \to \infty$ with the infinite sum defining $E$ needs uniform tail control, which is again Theorem 2.

Formalization scope

• Namespace PowerTwoChoices.Limit; λ is lam : ℝ, $d : ℕ$ with $2 \le d$, $0 < \lambda < 1$ in every theorem.
• A state is x : ℕ → ℝ with x 0 = 1, nonnegative and antitone. A trajectory is s : ℝ → ℕ → ℝ, a state for every $t \ge 0$, with HasDerivWithinAt on Set.Ici 0 for each coordinate $i \ge 1$: right derivative at $t = 0$, two-sided for $t > 0$.
• Exponents are natural numbers: $\pi_i = \lambda^{\sum_{k<i} d^k}$, and $T_d$'s $i$-th term is $\lambda^{\sum_{1\le k<i} d^k}$.
• $\Phi$, the $L_1$ distance, $E$ and $T_d$ are sums in $[0,\infty]$, so a divergent series is $\infty$, never a default $0$. "Converges exponentially" (Definition 2) means $\Phi(t) \le c_0 e^{-\delta t}$ for all $t \ge 0$ with real $c_0$ and $\delta > 0$; $\delta$ may depend on the trajectory. The paper's $d(t)$ is renamed l1Dist.
• Time is real and $t \to \infty$ is Filter.atTop.
• Every theorem quantifies over trajectories; existence of a trajectory from a given state (Picard iteration, cited by the paper) is not part of the mission. The class is nonempty: the constant trajectory at $\pi$ is one.
• Ruled out: summing $E$ or $T_d$ as a real tsum (a divergent series would make the upper bound free and the limit attainable by a junk $0$), dropping the summability condition in Lemma 2 ($(1,1,\dots)$ is also a fixed point), choosing Theorem 3's weights after the trajectory, and stating anything for $d = 2$ only.
• Needed infrastructure: comparison principles for quasimonotone countable ODE systems, Dini-derivative Grönwall estimates, and interchange of limits and $\ell^1$ sums. All of these are reusable beyond this mission, and contributions of such lemmas as separate theorems are welcome.

Selected references

• M. Mitzenmacher, The Power of Two Choices in Randomized Load Balancing, IEEE Transactions on Parallel and Distributed Systems 12(10), 2001, pp. 1094–1104. https://doi.org/10.1109/71.963420
• Y. Azar, A. Z. Broder, A. R. Karlin, E. Upfal, Balanced Allocations, SIAM Journal on Computing 29(1), 1999, pp. 180–200. https://doi.org/10.1137/S0097539795288490
• N. D. Vvedenskaya, R. L. Dobrushin, F. I. Karpelevich, Queueing System with Selection of the Shortest of Two Queues: An Asymptotic Approach, Problems of Information Transmission 32(1), 1996, pp. 15–27.
• T. G. Kurtz, Approximation of Population Processes, SIAM, 1981. https://doi.org/10.1137/1.9781611970333

Motivation

Regev's On Lattices, Learning with Errors, Random Linear Codes, and Cryptography (J. ACM 56(6), 2009, Article 34; doi:10.1145/1568318.1568324) introduced the Learning with Errors (LWE) problem and built a public-key cryptosystem on it. The source for this mission is that published J. ACM article. The paper's main theorem, a quantum reduction from worst-case lattice problems to LWE, is outside this series; this mission formalizes a self-contained piece of finite combinatorics from §5.

In the cryptosystem the public key is a list of $m$ LWE samples, and a bit is encrypted by adding up a uniformly random subset of them. Semantic security rests on one fact: if the public key were truly uniform, the sum of a random subset of it would be close to uniform, so the ciphertext would carry no information about the bit. Claim 5.3 (p. 34:36) makes this precise for an arbitrary finite abelian group $G$. It is a special case of the leftover hash lemma of Impagliazzo and Zuckerman (1989), in which the family of functions $b \mapsto \sum_i b_i g_i$ indexed by $g \in G^l$ is a universal hash family. Variants of the same statement appear in the security proofs of most lattice-based encryption schemes that use random subset sums, including the dual-Regev and GPV-style constructions.

Setting

Let $G$ be a finite abelian group, written additively, with $|G|$ elements, and let $l \ge 0$ be an integer. For $g = (g_1, \dots, g_l) \in G^l$ and $b = (b_1, \dots, b_l) \in \{0,1\}^l$ the subset sum $\sum_i b_i g_i$ is the sum of the $g_i$ with $b_i = 1$ (the empty subset gives $0$). The distribution of the sum of a uniformly random subset of $g_1, \dots, g_l$ is

$$P_g(h) = \frac{1}{2^l}\,\bigl|\{\, b \in \{0,1\}^l \mid \textstyle\sum_i b_i g_i = h \,\}\bigr|, \qquad h \in G.$$

The paper defines the statistical distance of two densities as $\int |\varphi_1 - \varphi_2|$, with range $[0,2]$, and notes that the same definition applies to discrete random variables (p. 34:14). The distance of $P_g$ from the uniform distribution on $G$ is therefore

$$\Delta(g) = \sum_{h \in G} \Bigl| P_g(h) - \frac{1}{|G|} \Bigr|,$$

with no factor $\tfrac12$. Expectations and probabilities over $g$ refer to a uniform choice of $g_1, \dots, g_l \in G$, that is, the uniform distribution on all $|G|^l$ tuples, repetitions allowed: $\mathrm{Exp}_g[F(g)] = |G|^{-l}\sum_{g \in G^l} F(g)$.

In Lean these objects are RegevLWE.SubsetSum.subsetSum, P, statDistUniform and expectG.

Formalization targets

Goal: Claim 5.3

$$\mathop{\mathrm{Exp}}_g\bigl[\Delta(g)\bigr] \le \sqrt{\frac{|G|}{2^l}} \qquad\text{and}\qquad \Pr_g\Bigl[\Delta(g) > \sqrt[4]{|G|/2^l}\Bigr] \le \sqrt[4]{\frac{|G|}{2^l}}.$$

Both sentences of the claim are in the goal. The second is what the security proof (Lemma 5.4, p. 34:37) uses: for all but a $\sqrt[4]{|G|/2^l}$ fraction of public keys, the random subset sum is within $\sqrt[4]{|G|/2^l}$ of uniform. The constants are exactly as printed.

Milestones

1. The $\ell_2$ norm as a collision probability (p. 34:36). For every $g$, with $b, b'$ independent and uniform in $\{0,1\}^l$,

$$\sum_{h} P_g(h)^2 = \Pr_{b,b'}\Bigl[\textstyle\sum_i b_i g_i = \sum_i b'_i g_i\Bigr] \le \frac{1}{2^l} + \Pr_{b,b'}\Bigl[\textstyle\sum_i b_i g_i = \sum_i b'_i g_i \Bigm| b \neq b'\Bigr].$$

2. Collisions of distinct subsets (p. 34:37). For any $b \neq b'$, $\Pr_g[\sum_i b_i g_i = \sum_i b'_i g_i] = 1/|G|$.
3. Expected $\ell_2$ norm (p. 34:37). $\mathrm{Exp}_g[\sum_h P_g(h)^2] \le 1/2^l + 1/|G|$.
4. Cauchy–Schwarz and the $\ell_2$ identity (p. 34:37), pointwise in $g$:

$$\sum_h \Bigl|P_g(h) - \frac{1}{|G|}\Bigr| \le |G|^{1/2}\Bigl(\sum_h \Bigl(P_g(h) - \frac{1}{|G|}\Bigr)^2\Bigr)^{1/2}, \qquad \sum_h \Bigl(P_g(h) - \frac{1}{|G|}\Bigr)^2 = \sum_h P_g(h)^2 - \frac{1}{|G|}.$$

Significance

The result. Claim 5.3 is the step in the security proof of Regev's cryptosystem that removes the public key from the picture: once the key is replaced by uniform samples (by the LWE assumption), the claim shows that an encryption is statistically close to uniform, independently of the encrypted bit. The parameter choice $m \ge (1+\epsilon)(n+1)\log p$ of Lemma 5.4 is exactly what makes $|G|/2^m$ negligible for $G = \mathbb{Z}_p^n \times \mathbb{Z}_p$. Without the claim the cryptosystem would have a hardness assumption but no reduction from it.

Formalizing it. The claim is proved, with a complete argument in the paper; nothing here is open. To our knowledge no machine-checked proof of this statement, or of the leftover hash lemma for subset-sum hash families over a general finite abelian group, exists in Mathlib or on the platform. A formal proof gives a reusable, constant-exact statement of the subset-sum leftover hash lemma with the paper's normalization of statistical distance. The four milestones are standard facts about finite averages and collision probabilities that recur in many cryptographic security proofs.

Difficulty

There is no deep step; the work is in organizing finite counting arguments without loss. Two points need care. The collision fact $\Pr_g[\sum_i b_i g_i = \sum_i b'_i g_i] = 1/|G|$ holds for every pair $b \neq b'$ only because the coefficients $b_i - b'_i$ lie in $\{-1, 0, 1\}$: for a general linear form over a group with torsion, a nonzero coefficient vector need not give a uniformly distributed sum, so an argument that treats the coefficients as arbitrary integers fails. And passing from the $\ell_2$ bound to the expected $\ell_1$ distance requires the exchange of expectation and square root in the right direction (concavity), which is easy to misapply. The bound must hold for every finite abelian group and every $l$, including $l = 0$ and $|G| = 1$, with no asymptotic slack.

Formalization scope

• $G$ is any type with [AddCommGroup G] [Fintype G] [DecidableEq G]; $l : ℕ$, and $l = 0$ is allowed (then $P_g$ is the point mass at $0$ and the claim holds). No hypothesis is added to the paper's statement: $|G| \ge 1$ holds for every group.
• $\{0,1\}^l$ is encoded as Fin l → Bool; $g$ ranges over all functions Fin l → G, so the uniform choice of $g$ is over all $|G|^l$ tuples with repetition, not over $l$-element subsets of $G$.
• Every expectation and probability is an exact finite average with real values: $\mathrm{Exp}_g[F] = |G|^{-l}\sum_g F(g)$, and $\Pr_g[E]$ is the number of tuples satisfying $E$ divided by $|G|^l$. Probabilities over $(b, b')$ are counts over the $(2^l)^2$ pairs; the conditional probability given $b \neq b'$ divides by $(2^l)^2 - 2^l$. At $l = 0$ the paper's conditional probability is undefined; Lean's convention $0/0 = 0$ makes milestone 1 read $1 \le 1$ there, which is consistent with the paper.
• The statistical distance is $\sum_h |P_g(h) - 1/|G||$, without $\tfrac12$. A formalization with the $\tfrac12$-normalized total variation distance would state a weaker result (half the bound) and is excluded. "More than" in the second sentence is strict, "at most" is $\le$. The fourth root is Real.sqrt (Real.sqrt x).
• Milestone 4 states only the first two steps of the paper's final chain (the Cauchy–Schwarz inequality and the identity), pointwise in $g$; the remaining two steps (Jensen for the square root and the substitution of milestone 3) are part of the goal. Its milestone text quotes the whole chain for context.
• No definitions beyond the four above are needed, and no measure theory. Proofs of the milestones, and alternative proofs of the goal (for instance via Fourier analysis on $G$), are welcome.

Selected references

• O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. doi:10.1145/1568318.1568324
• R. Impagliazzo and D. Zuckerman, How to Recycle Random Bits, Proc. 30th IEEE FOCS, 248–253, 1989. doi:10.1109/SFCS.1989.63486
• J. Håstad, R. Impagliazzo, L. A. Levin and M. Luby, A Pseudorandom Generator from any One-way Function, SIAM Journal on Computing 28(4), 1364–1396, 1999. doi:10.1137/S0097539793244708

Motivation

Network design problems often ask for a cheap spanning tree in which no vertex is overloaded: in multicast and overlay networks the degree of a node bounds the number of copies it must forward, and in physical networks it bounds the number of ports. The minimum bounded degree spanning tree problem asks for a minimum-cost spanning tree whose degrees respect given bounds. Deciding whether a graph has a spanning tree of maximum degree 2 is already the Hamiltonian path problem, so exact solutions are out of reach, and the question becomes how little the bounds and the cost must be relaxed.

Some problems also impose lower bounds: a vertex that must serve as a hub, or a leaf-avoidance requirement, asks for degree at least $A_v$. Singh and Lau (STOC 2007) showed that the iterative rounding method they used for upper bounds extends to both kinds at once: a spanning tree of cost at most the LP optimum whose degree at every vertex lies in $[A_v-1,\,B_v+1]$.

Timeline. Fürer and Raghavachari (1994) found a spanning tree of maximum degree at most $\Delta^*+1$ in the unweighted case. For costs, Goemans (FOCS 2006) obtained cost at most OPT with degrees at most $B_v+2$. Singh and Lau (STOC 2007) improved this to $B_v+1$, which is the best possible additive violation unless P = NP, and gave the extension to lower and upper bounds formalized here. The journal version appeared in J. ACM 62(1), 2015.

Setting

Let $G=(V,E)$ be a finite simple graph with edge costs $c_e\in\mathbb R$; no sign or triangle inequality is assumed. Let $F$ be a forest on $V$ with no edge in common with $E$. A set $H\subseteq E$ is an $F$-tree if $H\cup F$ is a spanning tree of $V$, and $d_H(v)$ is the number of edges of $H$ at $v$. Integer lower bounds $A_v$ are given on $U\subseteq V$ and integer upper bounds $B_v$ on $W\subseteq V$. The minimum bounded degree connecting tree problem asks for a cheapest $F$-tree with $A_v\le d_H(v)$ on $U$ and $d_H(v)\le B_v$ on $W$; with $F=\varnothing$ it is the spanning-tree problem.

The supernodes are the vertex sets of the components of $(V,F)$, isolated vertices included, and $\mathcal I(F)$ is the family of unions of supernodes. For $S\subseteq V$, $E(S)$ and $F(S)$ are the edges with both endpoints in $S$, $\delta(S)$ the edges with exactly one endpoint in $S$, and $x(D)=\sum_{e\in D}x_e$. The linear relaxation LP-MBDCT$(G,\mathcal A,\mathcal B,U,W,F)$ minimizes $\sum_e c_ex_e$ subject to

$$x(E(V))=|V|-|F(V)|-1,\quad x(E(S))\le|S|-|F(S)|-1\ (S\in\mathcal I(F)),\quad A_v\le x(\delta(v))\ (v\in U),\quad x(\delta(v))\le B_v\ (v\in W),\quad x\ge0.$$

MBDCT Algorithm2 (Figure 5 of the paper) repeats: if $F$ is a spanning tree, stop; otherwise take a basic optimal solution $x^*$, delete the edges with $x^*_e=0$, move one edge with $x^*_e=1$ (if any) into $F$ and lower $A$ and $B$ by one at its endpoints, and otherwise remove from $U$ and $W$ one vertex whose support degree is at most two.

Formalization targets

Goal: Theorem 5.2

For every well-formed instance whose LP is feasible, MBDCT Algorithm2

1. has a terminating run;
2. makes at most $|V|-|F|-1+|U\cup W|$ iterations on every run;
3. returns only $F$-trees $H\subseteq E$ with

$$c(H)\le\sum_{e\in E}c_ex_e\ \text{for every feasible }x,\qquad A_v-1\le d_H(v)\ (v\in U),\qquad d_H(v)\le B_v+1\ (v\in W).$$

The statement fixes no constants beyond the paper's $\pm1$, and it is uniform over every choice of basic optimal solution, 1-edge and removed vertex.

Milestones

In the order the proof uses them: Lemma 5.3 (a basic solution is determined by a laminar family of tight sets and tight lower and upper degree rows, with $|E^*|=|\mathcal L|+|T_U|+|T_W|$); Claims 5.4, 5.7, 5.8 and 5.9 (special supernodes, cut sizes, the value $x^*(D(S))=r-1$ on the edges between the $r$ members of $S$, and when a set is special); Lemma 5.6 (every set of $\mathcal L$ keeps at least three tokens, exactly three only if it is special or $V$); and Lemma 5.1 (a basic solution has an edge with $x^*_e=1$ or a vertex of $U\cup W$ with support degree two).

Significance

The theorem gives, in one algorithm, a tree that is no more expensive than the LP lower bound and whose degrees miss both bounds by at most one. For the pure upper-bound problem it implies the $(1,B_v+1)$ guarantee, which cannot be improved to $B_v$ unless P = NP, since a Hamiltonian path is the case $B_v\equiv 2$. With lower bounds it also covers prescribed minimum degrees.

The result is proved in the paper; no machine-checked proof of it, or of any iterative rounding analysis, is known to exist. No platform item treats bounded-degree spanning trees or iterative rounding; the nearest related item is the open Williamson–Shmoys minimum-degree spanning tree local-search goal, which concerns a different, unweighted problem. Formalizing this mission requires the extreme-point structure of the spanning tree polytope with degree constraints (uncrossing to a laminar family), the token counting argument, and the induction over the algorithm's recursion, all of which are reusable for other iterative rounding results.

Difficulty

The obvious argument rounds an optimal LP solution once. It fails: an optimal vertex may be entirely fractional, and no single rounding keeps both the cost and the degrees. The algorithm instead re-solves the LP after each change, and its correctness rests on Lemma 5.1, that every extreme point of the current LP has an integral edge or a vertex with support degree two. That lemma is a counting statement about extreme points: the rank bound $|E^*|=|\mathcal L|+|T_U|+|T_W|$ from a laminar basis must be contradicted by a token distribution. With upper bounds only, every set of the laminar family can collect four tokens. With lower bounds a set may collect only three, and the proof must characterize those sets (special sets, Definition 5.5) and show by linear independence that the remaining cases cannot occur. A second difficulty is that the guarantee concerns the final tree after many iterations, so the degree accounting must survive the changes of $A$, $B$, $U$, $W$ and $F$ along the run.

Formalization scope

Vertices form a Fintype; edges are elements of Sym2 V with no loops, and $E$, $F$ are finite sets of edges with $F$ acyclic and disjoint from $E$. LP vectors are functions on Sym2 V that vanish off $E$. Right-hand sides are computed in $\mathbb R$, degree bounds are integers, and the subtour rows range over nonempty $S\in\mathcal I(F)$ (at $S=\varnothing$ the literal row $0\le-1$ would make the LP empty). A basic solution is a feasible $x$ that is the only vector on $E$ satisfying with equality every constraint tight at $x$, including the tight rows $x_e=0$. Supernodes are never contracted: the paper's contraction of a supernode with one active vertex is a proof device, and all of §5.1's notions are stated on the original instance.

The paper's loose phrases are made explicit as follows.

• "Polynomial time" becomes the iteration bound; the LP is solved by an oracle that returns any basic optimal solution. The ellipsoid method and the separation oracle are out of scope.
• "The algorithm returns" becomes three claims: a run exists, every run is bounded, and every returned set satisfies the guarantee. The guarantee alone would hold vacuously for a relation that can get stuck.
• "Cost at most the cost of the optimal LP solution" becomes $c(H)\le c\cdot x$ for every feasible $x$.
• "Distribute the tokens" (Lemma 5.6) becomes a counting inequality on the surplus of tokens.
• Claim 5.9's "contains exactly three special members" means that $S$ has exactly three members, all of them special.
• Figure 5's Step 4 is guarded by "no edge was picked in Step 3", as the paper's text under Lemma 5.1 states.
• "$F$ is not a spanning tree" and LP feasibility are explicit hypotheses where the paper leaves them implicit.

Two trivializations are ruled out. Existence of a cheap tree with degrees in $[A_v-1,B_v+1]$ is not the target: the statement is about the algorithm's outputs and quantifies over all of them. And a run that never terminates does not satisfy the goal, which requires a run to exist and every run to be bounded.

Contributions are welcome at every level: the laminar uncrossing argument (Lemma 5.3), which is reusable for any spanning-tree LP with degree rows; the counting claims; and the invariants of the recursion.

Selected references

• M. Singh, L. C. Lau, Approximating minimum bounded degree spanning trees to within one of optimal, STOC 2007, pp. 661–670. https://doi.org/10.1145/1250790.1250887
• M. Singh, L. C. Lau, Approximating minimum bounded degree spanning trees to within one of optimal, J. ACM 62(1), 2015. https://doi.org/10.1145/2629366
• M. X. Goemans, Minimum bounded degree spanning trees, FOCS 2006, pp. 273–282. https://doi.org/10.1109/FOCS.2006.48
• M. Fürer, B. Raghavachari, Approximating the minimum-degree Steiner tree to within one of optimal, J. Algorithms 17(3), 1994, pp. 409–423. https://doi.org/10.1006/jagm.1994.1042