Combinatorics

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

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

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

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$,

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$:

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

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

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

Motivation

A network designer may need a cheap connection that keeps the number of links at each site within a local capacity. The minimum bounded-degree spanning tree problem asks for the cheapest spanning tree of a weighted, undirected graph whose vertex degrees respect prescribed upper bounds. The capacity constraints matter in settings where a low-cost tree alone can overload a few hubs. They also make the optimization problem difficult: even with unit edge weights and a bound of two at every vertex, feasibility includes the Hamiltonian path problem. Singh and Lau study the useful relaxation in which the returned tree may exceed each degree bound by one while its cost stays no greater than the best tree satisfying every original bound Singh–Lau 2007.

The weighted result settled the bounded-degree form of a conjecture discussed in their paper. Goemans had obtained a cost-preserving degree guarantee of $B_v+2$; an earlier unweighted local-search result attained a $+1$ degree allowance but did not cover arbitrary real costs. Singh and Lau's Theorem 1.2 gives the $+1$ allowance in the weighted setting, without assuming nonnegative costs or triangle inequalities Singh–Lau 2007, pp. 661–662. The platform's open WilliamsonShmoys.minimum_degree_tree_local_search_approximation concerns the related unweighted minimum-degree local-search problem, with a different objective and guarantee.

Setting

Let $V$ be a finite vertex set and $E$ a finite set of unordered, non-loop edges. A spanning tree $T\subseteq E$ connects every vertex without a cycle. Every edge $e$ has a real cost $c_e$, so $c(T)=\sum_{e\in T}c_e$. Each vertex $v$ has an integer upper bound $B_v$ on its tree degree $d_T(v)$. A feasible original solution has $d_T(v)\le B_v$ for all $v$.

The paper studies a broader connecting-tree problem. A forest $F$ is already selected; its connected components, including isolated vertices, are supernodes. The remaining graph has edges $E$ disjoint from $F$. A set $H\subseteq E$ is an $F$-tree if $H\cup F$ is a spanning tree. Degree bounds are active only at vertices in $W\subseteq V$, and $d_H(v)$ counts edges of $H$, not edges of $F$. The initial spanning-tree problem is the case $F=\varnothing$ and $W=V$ Singh–Lau 2007, p. 665.

For an edge set $Q$ and vertex set $S$, write $Q(S)$ for edges of $Q$ with both endpoints in $S$, and $\delta_E(v)$ for edges of $E$ incident to $v$. The LP-MBDCT relaxation has a nonnegative variable $x_e$ for each $e\in E$. It requires $x(E)=|V|-|F|-1$, requires $x(E(S))\le |S|-|F(S)|-1$ for every nonempty union $S$ of supernodes, and requires $x(\delta_E(v))\le B_v$ for $v\in W$. Its objective is $\sum_{e\in E}c_ex_e$. At $F=\varnothing$, $W=V$, this is the spanning-tree LP in equations (1)–(5) Singh–Lau 2007, pp. 662, 665.

Formalization targets

Theorem 1.2: bounded-degree spanning trees

For every feasible initial LP, the paper's Figure 4 algorithm has a terminating run. Every possible run returns a spanning tree $T$ satisfying

In particular, $c(T)$ is at most the cost of every spanning tree satisfying the original bounds, and thus at most the original optimum. Every run has at most $2|V|-1$ iterations. The cost comparison against every LP-feasible vector states the stronger bound used by Theorem 4.2 Singh–Lau 2007, pp. 661, 666.

Theorem 4.2 and its milestones

The connecting-tree theorem makes the same cost and degree guarantee for an arbitrary feasible state $(E,B,W,F)$, with $d_H(v)\le B_v+1$ only for $v\in W$. The attack path follows the paper's numbered results: Lemma 4.3 describes tight constraints by a laminar family, Claim 4.5 classifies vertices with one excess token, Lemma 4.6 bounds tokens inside a laminar subtree, and Lemma 4.1 says each nonterminal basic solution has either a unit-valued edge or a removable degree constraint. Theorem 4.2 then supplies the general guarantee Singh–Lau 2007, pp. 666–667.

Significance

The result allows one unit of violation at each local degree bound while preserving the cost benchmark exactly. It applies even when negative edge costs make standard multiplicative cost ratios awkward. The connecting-tree statement is useful beyond the initial instance because it covers a forest already accumulated and a subset of degree constraints still active.

This mission formalizes the known 2007 result as an open Lean proof target; the paper proves the mathematics, while the declarations here currently have no machine-checked proofs. A completed development would provide a reusable account of a spanning-tree LP with forest contraction, basic solutions defined by tight rows, and a finite relational algorithm with all choices exposed. These objects could support the paper's lower-and-upper-bound extension and other iterative-rounding results.

Difficulty

Rounding an arbitrary fractional edge upward can increase cost beyond the LP benchmark. Restricting the algorithm to edges with value exactly one protects that benchmark, but a nonterminal basic solution need not present a unit-valued edge. The central structural question is then whether some active degree constraint can be removed with only a one-unit effect on the final degree. The tight subtour rows and degree rows overlap, so counting edges from the support alone is insufficient; Lemmas 4.3–4.6 resolve the dependency and token-counting issues that make the direct argument fail Singh–Lau 2007, pp. 666–667.

Formalization scope

Lean represents edges as Sym2 V in finite sets, excluding diagonal edges. It represents LP vectors on all unordered pairs but requires zero values outside the current edge set. A forest is acyclic on the full vertex set. A compatible subtour set is a union of its connected components. Subtour right-hand sides are real numbers, so subtraction does not truncate at zero; the empty set is excluded because the literal row would make the LP infeasible. Degree bounds are integers so the algorithm's decrements are total. A basic feasible solution is determined uniquely by its tight equality rows among vectors supported on the current edge set. Linear independence in Lemma 4.3 is checked on the positive support.

Figure 4 is a relation because the LP optimum, a unit-valued edge, and a qualifying vertex may each be chosen in several ways. Its edge and vertex tests are mandatory when their conditions hold. The vertex test uses the support before deleting the selected edge and bounds after decrementing its endpoints, following the printed order. “The algorithm returns” is represented by existence of a run, an iteration bound on every step chain, and guarantees for every returned set. “Cost at most the LP optimum” means cost no greater than the objective at every feasible LP vector. “Polynomial time” is represented by the iteration count; the ellipsoid LP solver and separation-oracle complexity are outside this mission. Lemma 4.6's token distribution is expressed as its explicit counting inequality.

The goal asserts the Figure 4 output and its LP cost guarantee. Bare existence of a tree with cost at most the optimum and degrees at most $B_v+1$ would be witnessed by an original optimal tree and would lose the algorithmic theorem. A return guarantee without run existence would hold vacuously for a stuck relation. Contributions that prove the stated structural lemmas, establish the LP oracle's basic-optimum availability, or close the algorithm invariant are within scope. No existing platform item treats this bounded-degree LP and iterative-rounding algorithm under these conventions; the plain minimum-spanning-tree LP definition uses a different edge representation and no forest or degree constraints.

Selected references

• Mohit Singh and Lap Chi Lau, Approximating Minimum Bounded Degree Spanning Trees to within One of Optimal, Proceedings of the 39th ACM Symposium on Theory of Computing (STOC), 2007, pp. 661–670. DOI: 10.1145/1250790.1250887.

Why tangles need to be organised into a tree

Robertson and Seymour introduced tangles in Graph Minors. X (J. Combin. Theory Ser. B 52 (1991) 153–190) as the precise obstruction to tree-decompositions of small width: a graph has a tangle of large order exactly when it has no tree-decomposition of small width. A tangle points to a highly connected region of a graph without naming its vertices, by designating for every low-order separation which side is the "small" one. Large grids, large clique minors and surface embeddings with high representativity all induce tangles.

A graph usually contains several such regions. The structure theory of the Graph Minors series needs to look at all of them at once: to decompose a graph along a tree so that each highly connected region sits at its own node, and any two regions are separated as cheaply as possible. Section 10 of the paper provides that decomposition, and its later versions ("tree of tangles" theorems) have become a standard tool in structural graph theory, in matroid theory and in abstract separation systems (see Diestel, Hundertmark and Lemanczyk, Profiles of separations: in graphs, matroids and beyond, Combinatorica 39 (2019), and Carmesin, Diestel, Hundertmark and Stein, Connectivity and tree structure in finite graphs, Combinatorica 34 (2014)). This mission formalizes the original 1991 statement for hypergraphs.

Setting

A hypergraph $G$ has a finite vertex set $V(G)$, a finite edge set $E(G)$ and an incidence relation; an edge may have any number of ends. A subhypergraph is given by a vertex set and an edge set, closed under taking ends of its edges; $\cup$, $\cap$, $\subseteq$ act on both sets. A separation is a pair $(A,B)$ of subhypergraphs with $A\cup B=G$ and $E(A\cap B)=\emptyset$; its order is $|V(A\cap B)|$.

A tangle of order $\theta\ge1$ is a set $\mathcal T$ of separations of order $<\theta$ such that (i) of every separation $(A,B)$ of order $<\theta$, one of $(A,B)$, $(B,A)$ is in $\mathcal T$; (ii) no three members $(A_i,B_i)$ of $\mathcal T$ satisfy $A_1\cup A_2\cup A_3=G$; (iii) $V(A)\neq V(G)$ for $(A,B)\in\mathcal T$. Two tangles are indistinguishable if one contains the other, and a separation $(A,B)$ distinguishes $\mathcal T_1$ from $\mathcal T_2$ if $(A,B)\in\mathcal T_1$ and $(B,A)\in\mathcal T_2$.

A tree-decomposition $(T,\tau)$ assigns a subhypergraph $\tau(t)$ to each node of a tree $T$, so that the $\tau(t)$ cover $G$, are pairwise edge-disjoint, and $\tau(t)\cap\tau(t'')\subseteq\tau(t')$ whenever $t'$ lies on the path from $t$ to $t''$. An edge $e$ of $T$, with components $T_1,T_2$ of $T\setminus e$, makes the separations $(G^e_1,G^e_2)$ and $(G^e_2,G^e_1)$, where $G^e_i=\bigcup_{t\in V(T_i)}\tau(t)$. Two separations cross unless one of four nestings holds ($A_1\subseteq A_2$ and $B_2\subseteq B_1$, or the analogous three); a set of separations is laminar if no two members cross.

A tie-breaker $\lambda$ maps separations into a linearly ordered set so that (i) $\lambda(A,B)=\lambda(C,D)$ exactly when $(A,B)=(C,D)$ or $(A,B)=(D,C)$; (ii) $\lambda(A\cup C,B\cap D)\le\lambda(A,B)$ or $\lambda(A\cap C,B\cup D)<\lambda(C,D)$; (iii) separations of smaller order get smaller $\lambda$-order. Given $\lambda$, the $(\mathcal T_1,\mathcal T_2)$-distinction is the separation of minimum $\lambda$-order distinguishing $\mathcal T_1$ from $\mathcal T_2$. A separation $(A,B)$ is $\lambda$-robust if for every separation $(C,D)$ of the hypergraph $A$, one of $(C,B\cup D)$, $(D,B\cup C)$ has $\lambda$-order at least $\lambda(A,B)$, and doubly $\lambda$-robust if $(B,A)$ is $\lambda$-robust too.

Formalization targets

Goal: (10.3), p. 181

Let $\mathcal T_1,\dots,\mathcal T_n$, $n\ge1$, be mutually distinguishable tangles in $G$ (each with its own order) and $\lambda$ a tie-breaker. Then there is a tree-decomposition $(T,\tau)$ with $V(T)=\{t_1,\dots,t_n\}$ such that

and (ii) for $i\neq j$, each edge of the $t_i$–$t_j$ path in $T$ whose separations have the smallest $\lambda$-order on that path makes the $(\mathcal T_i,\mathcal T_j)$- and $(\mathcal T_j,\mathcal T_i)$-distinctions, the first with $t_j$'s side first.

Milestones

• (9.1), p. 177: the separations made by the edges of a tree-decomposition form a laminar set, and every laminar set is the set made by the edges of some tree-decomposition, each member by a unique edge.
• (9.2), p. 178: every hypergraph has a tie-breaker.
• (9.3), p. 179: a strict form of the second tie-breaker axiom, with two degenerate exceptions.
• (9.4), p. 180: doubly $\lambda$-robust separations do not cross.
• (10.1), p. 180: two tangles are distinguished by some separation if and only if neither contains the other.
• (10.2), p. 181: the $(\mathcal T_1,\mathcal T_2)$-distinction is doubly $\lambda$-robust.

Significance

The theorem gives a single decomposition for all tangles at once: any family of pairwise distinguishable tangles is displayed by a single tree-decomposition, with each tangle "living" at its own node (property (i)) and every pair separated by its cheapest distinction (property (ii)). The paper derives from it that a hypergraph has at most $|V(G)|$ maximal tangles ((10.4), p. 184), and Section 11 uses the same machinery to build tree-decompositions whose pieces "almost" carry a local structure, a step used in the later Graph Minors papers.

None of these statements is formalized in any proof assistant as far as a search of the Prove2Me library shows; the platform has simple-graph tree-decompositions with vertex bags (from Graph Minors V), which are a different object from the hypergraph tree-decompositions here. The mission produces machine-checked statements of the tangle-tree theorem in its original hypergraph form, together with the lemma chain the authors use. The remaining work is a formal proof of each item; (9.1) is "left to the reader" in the paper and therefore needs an argument written from scratch.

Difficulty

The naive approach takes, for every pair of tangles, a separation of minimum order distinguishing them, and tries to arrange these separations in a tree. That fails: minimum-order distinguishing separations for different pairs may cross, and no tree-decomposition makes two crossing separations. Ties among minimum-order separations must be broken consistently across all pairs at once, and even a laminar family of distinctions does not obviously yield a tree whose nodes correspond one-to-one to the tangles, as property (i) and $V(T)=\{t_1,\dots,t_n\}$ demand.

Formalization scope

• Hypergraphs are a structure with an incidence relation on types V, E; every theorem assumes [Finite V] [Finite E] (the paper's "all hypergraphs in this paper are finite", p. 154). Subhypergraphs are pairs of a vertex set and an edge set closed under ends.
• A tangle carries its order as a parameter: IsTangle G θ 𝒯 includes $\theta\ge1$. In (10.3) the tangles have independent orders $\theta_i$.
• The tree of a tree-decomposition is a SimpleGraph on Fin n that is a tree. In the goal, node $i$ is $t_i$, which encodes $V(T)=\{t_1,\dots,t_n\}$ with the $t_i$ distinct; the hypothesis $n\ge1$ is the paper's.
• A tie-breaker is a function on all pairs of subhypergraphs into an arbitrary type $\Lambda$ with a linear order; its axioms constrain only its values on separations. The goal quantifies over every such $\Lambda$, not just the paper's $\mathbb R^3$.
• (10.3)(ii) is stated with an explicit orientation (the one forced by (i)) and for every edge minimising the $\lambda$-order on the path.
• (10.1) and (10.2) are stated for hypergraphs; §10 opens with "tangles in a graph $G$", but (10.3) applies them to hypergraphs and their proofs do not use edge sizes.
• A trivializing formalization would make the tie-breaker axioms unsatisfiable, so that (9.3)–(10.3) hold vacuously; (9.2) is part of the mission precisely to rule this out.
• The definitions of hypergraph, tangle and tree-decomposition are shared with the other missions of the series, Graph Minors. X. Obstructions to Tree-Decomposition I (tangle number equals $\max(\beta,\gamma)$), II (branch-width and tree-width), III (the grid tangle) and V (pervasive classes of designs). The laminar/tie-breaker layer is reusable for any tree-of-tangles statement. Contributions welcome: proofs of the milestones in any order, and a formal proof of (9.1).

Selected references

• N. Robertson, P. D. Seymour, Graph Minors. X. Obstructions to Tree-Decomposition, J. Combin. Theory Ser. B 52 (1991) 153–190. https://doi.org/10.1016/0095-8956(91)90061-n
• J. Carmesin, R. Diestel, F. Hundertmark, M. Stein, Connectivity and tree structure in finite graphs, Combinatorica 34 (2014) 11–46. https://arxiv.org/abs/1105.1611
• R. Diestel, F. Hundertmark, S. Lemanczyk, Profiles of separations: in graphs, matroids and beyond, Combinatorica 39 (2019) 37–75. https://arxiv.org/abs/1608.07144

Motivation

Programs often reveal information through the memory locations they touch, even when the contents of those locations are hidden. An oblivious RAM simulation aims to conceal this access pattern. Goldreich and Ostrovsky studied the cost of doing so for arbitrary RAM programs and showed that the access sequence itself imposes a lower bound on simulation overhead. Their 1996 paper gives an upper-bound construction as well as the lower-bound theorem targeted here. The issue matters when a storage observer can see which addresses are accessed but must learn nothing about the program's private requests.

Theorem 6.1 of the paper states that simulating $t$ steps requires at least the initial memory size and, asymptotically, a multiple of $t\log t$ accesses. Its proof introduces a simpler ball-and-cell game that grants the player more information and freedom than the RAM simulation. The mission formalizes that game and its lower bound. This makes the combinatorial content of the published argument a precise theorem about randomized behavior and visible observations. The paper's earlier Theorem 1.2.2 on p. 437 is labeled informal and has a different explicit bound; the target here is Theorem 6.1 on pp. 469–470.

Setting

There are $m$ numbered balls and $m$ numbered cells. Cell $i$ initially contains ball $i$, and a player's hand is empty. Each cell can hold at most one ball and the hand can hold at most $b$ balls. In one access, the player names a cell and secretly takes its ball into a nonfull hand, places one held ball into an empty cell, or leaves the cell unchanged. Taking from an empty cell and placing into an occupied cell are illegal. The observer sees the named cell at each access but not the hidden operation. A run of $q$ accesses is written $a=((v_1,h_1),\ldots,(v_q,h_q))$, and its visible sequence is $V(a)=(v_1,\ldots,v_q)$.

A request sequence $r=(r_1,\ldots,r_t)$ names a ball for each of $t$ rounds. A run satisfies $r$ if it is legal and there are indices $1\le j_1\le\cdots\le j_t=q$ such that ball $r_i$ is in the player's hand after the first $j_i$ accesses. Equal indices are permitted: several rounds may finish after the same access. The player may know the entire request sequence in advance. That assumption is part of the paper's game, and the paper notes that its lower bound does not require an online player.

A randomized player assigns each request sequence a probability distribution over finite runs. It is correct if every run with positive probability satisfies its requests. It is oblivious if the distribution of $V(a)$ is identical for every pair of request sequences of length $t$. Thus the observer cannot infer the requested balls from the accessed cells, even statistically. These conditions quantify over all request sequences, not a selected input or a single deterministic access pattern.

Formalization targets

Theorem 6.1: access lower bound

For every correct oblivious player and every run in the support of its response, the mission targets

where $c_b>0$ and $T_b$ depend only on the fixed hand size $b$. This is the paper's $\max\{m,\Omega(t\log t)\}$ form, with $m$ representing the number $|y|$ of initially occupied memory words. It asserts a bound on every possible run, rather than only on average access count. No numerical constant is prescribed by the paper.

Intermediate counting targets

The milestones record the first-round $m$ bound, the at-most-$(b+2)^q$ count of legal hidden action sequences compatible with a visible sequence, and the implication from obliviousness that one visible sequence can serve every request sequence. They then state the corrected finite counting bounds

These preserve the paper's non-strict round ends. The milestone source text records the published formulas, while the formal statements and descriptions identify the corrections.

Significance

The result limits how cheaply a simulator can hide a program's memory access pattern when the observer sees addresses. In the game, a player is even allowed to remember the entire ball placement without cost, know the future requests, and randomize its actions. A lower bound under these permissive conditions applies to the more constrained access-pattern problem that motivated the game, subject to the paper's reduction from simulation to the game. The $m$ term also accounts for the initially occupied memory, independently of the asymptotic term.

The theorem is a published mathematical result, but the mission's Lean declarations are statements with proof holes until solvers supply machine-checked proofs. Formalizing the game creates reusable definitions for legal hidden operations, request satisfaction, randomized players, and visible distributions. Formalizing the corrected counting targets also makes explicit a discrepancy in the printed proof rather than silently relying on an invalid intermediate inequality.

Difficulty

The main difficulty is accounting for requests when several rounds end at the same access. The paper's observation that a fixed $q$-access run serves at most $b^q$ request sequences is false under its own non-strict indices. A run that fetches every ball it can hold may answer many later rounds without making another access. Likewise, the alternative binomial count in footnote 29 assumes distinct completion points and fails when $t>q$. The final asymptotic result still has a valid corrected counting target, but a proof cannot quote the published intermediate formulas literally. Randomized behavior adds another precise requirement: equality of visible distributions must support conclusions about runs with positive probability for each request sequence.

Formalization scope

The Lean carrier is the paper's ball-and-cell game from §6, rather than the interactive RAM machine model of §2. The game relaxes the simulation by giving the player free memory of ball locations and advance knowledge of requests. Balls, cells, and rounds use finite types Fin m and Fin t; these are zero-based encodings of the paper's $[m]$ and round labels. Action steps are counted from one, with the initial state at step zero. PMF represents the player's discrete probability distributions, and equality of PMF.map visible represents observer independence. Every positive-probability run must be legal and satisfy its requests. The visible and hidden sequences have the same finite length $q$.

The two printed estimates $b^q$ and $b^q(b+2)^q>m^t$ are false: with $m=b=q=2$ and $t=7$, taking both balls in two accesses satisfies all $2^7=128$ request sequences, while the printed product is $64$. Footnote 29's $\binom qt b^t$ also vanishes in this example. The formal milestones use Nat.multichoose q t to accommodate repeated round ends; at $q=t=0$ its value is defined directly, so no negative binomial upper index is used. The logarithm in the goal is the natural logarithm, and a threshold $T_b$ handles small $t$.

Correctness and legality are part of the player type, so an unrestricted sequence of cell names cannot satisfy the mission by bypassing the hand and cell rules. Obliviousness uses equality of full distributions, and the goal quantifies over every supported run. The required development includes finite-state transition reasoning, finite combinatorial counts, PMF support and mapping, and real logarithm estimates. These components, especially the game interface and support lemmas, can be reused by later access-pattern formalizations.

Selected references

• Oded Goldreich and Rafail Ostrovsky, Software protection and simulation on oblivious RAMs, Journal of the ACM 43(3):431–473, 1996. DOI: 10.1145/233551.233553. Theorem 6.1 and its proof are on pp. 469–470; the informal Theorem 1.2.2 is on p. 437.

Motivation

In the edge-disjoint paths problem (EDP) one is given an undirected graph and a list of source–sink pairs, and asks how many pairs can be connected simultaneously by paths that share no edge. Its relaxation EDP with congestion (EDPwC) allows every edge to carry up to a fixed number of paths. Both are central problems of network routing and of approximation algorithms, and the standard algorithmic tool for them is the multicommodity flow relaxation: a linear program that may split each pair's unit of demand fractionally over many paths. Rounding this LP is how most approximation algorithms for routing work, so the ratio between its optimum and the best integral routing, the integrality gap, bounds what any LP-based algorithm can achieve.

Without congestion the gap of this relaxation can be as large as $\Omega(\sqrt V)$ (Chekuri–Khanna–Shepherd 2006), and the question is how much a small congestion helps. Andrews, Chuzhoy, Guruswami, Khanna, Talwar and Zhang (Combinatorica 2010) proved hardness of approximation for EDPwC (their Theorems 1 and 2) and, independently and unconditionally, that the gap of the relaxation remains $(\log V)^{\Omega(1/c)}$ even when the integral solution may use congestion $c-1$ (their Theorem 5). In particular, for every fixed integer $i$ the gap between $(1/i)$-integral and fractional multicommodity flow in undirected graphs is superconstant. This mission formalizes Theorem 5 for EDPwC.

Setting

Fix integers $n\ge1$ and $c\ge2$. Write $\log$ for $\log_2$ and $\ln$ for the natural logarithm, and set

A random $c$-uniform hypergraph $H$ on the vertex set $\{0,\dots,n-1\}$ has $m=\lfloor\beta_2 n\rfloor$ hyperedges $h_0,\dots,h_{m-1}$, chosen independently, each uniformly among the $c$-element subsets of the vertices.

From $H$ one builds a graph $G=G(H)$. For every hyperedge $h_i$ it has two vertices $\ell_i,r_i$ joined by a special edge; for every vertex $v$ of $H$ it has a source $s(v)$ and a sink $t(v)$. If $v$ lies in the hyperedges $h_{i_1},\dots,h_{i_k}$ with $i_1<\dots<i_k$, the regular edges $(s(v),\ell_{i_1})$, $(r_{i_j},\ell_{i_{j+1}})$ for $1\le j<k$, and $(r_{i_k},t(v))$ are added. The canonical path of $v$ is $P(v)=(s(v),\ell_{i_1},r_{i_1},\dots,\ell_{i_k},r_{i_k},t(v))$; it crosses the special edge of every hyperedge containing $v$. The EDP instance has one pair $(s(v),t(v))$ for each $v$.

A feasible fractional solution puts flow $f(P)\in[0,1]$ on $s(v)$–$t(v)$ paths $P$, with routed amount $x_v=\sum_P f(P)\le1$ for each pair and at most one unit of flow through each edge; its value is $\sum_v x_v$. An integral routing with congestion at most $c-1$ connects a set of pairs, each by one path, so that every edge lies on at most $c-1$ of these paths; its value is the number of connected pairs.

The analysis uses three events of $H$: $\mathcal E_1$, that some set of $n/\beta_1$ vertices contains no hyperedge; $\mathcal E_2$, that more than $n/\beta_1$ vertices lie in more than $10\beta_2c$ hyperedges; and $\mathcal E_3(g)$, that the graph $G'$ obtained from $G$ by contracting every special edge has more than $(6\beta_2c^2)^{g+1}$ cycles of length at most $g$.

Formalization targets

Goal: Theorem 5 for EDPwC, in the explicit form of Section 2

There are absolute constants $\alpha>0$ and $N_0$ such that for all $n\ge N_0$ and all integers $c$ with $2\le c\le\alpha\log\log n/\log\log\log n$ some hypergraph $H$ as above satisfies

so the integrality gap is at least $\beta_1/(4c)$. The paper's Theorem 5 states this as $\Omega\big(\frac1{c}(\log V/(\log\log V)^2)^{1/(c+1)}\big)$ for congestion $c$ and $V$ vertices; the goal keeps the paper's own Section 2 parameters, which fix the instance and leave the constants $\alpha,N_0$ open.

Milestones

Lemma 6, Lemma 7 and Lemma 8 ($\Pr[\mathcal E_1],\Pr[\mathcal E_2],\Pr[\mathcal E_3(g)]\le\frac14$); the joint good event of Section 2.4; the fractional solution of value $n/c$; and the three bounds of the gap analysis, $|\mathcal P_1|\le n/\beta_1$ (canonical paths), $|\mathcal P_2|\le n/\beta_1$ (long non-canonical paths), $|\mathcal P_3|\le n/\beta_1+2gc(6\beta_2c^2)^{2g+2}$ (short non-canonical paths), combined into $|\mathcal P'|\le4n/\beta_1$.

Significance

The result shows that the multicommodity flow relaxation cannot certify a constant-factor approximation for undirected EDPwC with any constant congestion: against integral solutions of congestion $c-1$ its gap is at least $(\log V)^{\Omega(1/c)}$. Any algorithm that compares its output with this LP inherits the bound. It complements the paper's hardness results, which hold only under a complexity assumption. The instance is a short explicit construction from a random hypergraph, so the theorem is also a statement in probabilistic combinatorics: random sparse uniform hypergraphs are, with constant probability, simultaneously "covering" (no large hyperedge-free set), of bounded degree, and nearly free of short cycles.

The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces one: a formal model of the path LP and of congestion-bounded integral routings on simple graphs, reusable for other routing gaps; a formal random-hypergraph model with first-moment and Chernoff-type estimates; and the deterministic gap analysis. Variants with better constants, or the stronger statement that at least a quarter of all hypergraphs work, are welcome as additional results.

Difficulty

The fractional side and the bound on canonical routings are short. The difficulty lies in two places. First, Lemma 8 bounds the expected number of short cycles of $G'$; the adjacency of $G'$ depends on all hyperedges at once (consecutiveness along each vertex's sequence), and the obvious estimate through the intersection graph of $H$ fails, because many hyperedges through a common vertex form a clique there. What keeps the count small is the order structure of each vertex's hyperedge sequence, which the intersection graph forgets. Second, the bound on short non-canonical paths requires turning two distinct routing paths of a pair into a short cycle of the contracted graph and charging it with the congestion constraint. Finally, the closing estimate $2gc(6\beta_2c^2)^{2g+2}\le n/\beta_1$ holds only for large $n$ in the stated range of $c$, and the printed chain for it is not literally correct, so the asymptotics have to be done afresh.

Formalization scope

Vertices of $H$ are Fin n, hyperedges are indexed by Fin m with $m=\lfloor\beta_2n\rfloor$, and $H$ is an element of Fin m → {s : Finset (Fin n) // s.card = c}; probabilities are normalized counts over this finite set (uniform measure, which is independence of the hyperedges). The conventions are:

• $\log=\log_2$ and $\ln$ is natural; $\beta_1$ uses a real $1/c$-th power.
• The paper's integers $\beta_2n$, $n/\beta_1$ (bad-set size) and $g=3\beta_1\beta_2c^2$ are $\lfloor\beta_2n\rfloor$, $\lceil n/\beta_1\rceil$ and $\lceil3\beta_1\beta_2c^2\rceil$; the thresholds $n/\beta_1$, $4n/\beta_1$, $10\beta_2c$, $(6\beta_2c^2)^{g+1}$ stay real.
• "For sufficiently large $n$" and $c\le O(\log\log n/\log\log\log n)$ become absolute constants $N_0$ and $\alpha$, quantified before $n$ and $c$. Lemma 8 and the deterministic bounds carry instead the explicit inequalities on $\beta_1,\beta_2$ their arguments use.
• $G(H)$ is a simple graph (coinciding regular edges are one edge). A vertex in no hyperedge gets the edge $(s(v),t(v))$, the $k=0$ case of its canonical path; the page leaves this case out.
• $K_g$ counts cycles of $G'$, each once as an edge set; the paper's definition says "in $G$", its proof and use say $G'$.
• Routing paths are paths (no repeated vertex); lengths count edges of $G(H)$; canonicity is equality of vertex sequences.

The goal cannot be met by an unrelated graph: the instance must be $G(H)$ for a hypergraph with exactly $\lfloor\beta_2n\rfloor$ hyperedges of size $c$ on $n$ vertices, the fractional solution must respect $x_v\le1$ and capacity $1$, and the integral bound is over all routings of congestion $c-1$.

Not in scope: the ANFwC half of Theorem 5, the remark on a superconstant gap at $c=\Theta(\log\log V/(\log\log\log V)^2)$, and the hardness results of Sections 3–5 (Theorems 1 and 2, Corollaries 3 and 4).

A complete development needs Chernoff and Markov bounds for counting measures, binomial-coefficient estimates, cycle extraction from two distinct paths in a simple graph, and the asymptotic estimates for $\beta_1,\beta_2$. The routing and LP definitions and the cycle-extraction lemma are reusable beyond this mission.

Selected references

• M. Andrews, J. Chuzhoy, V. Guruswami, S. Khanna, K. Talwar, L. Zhang, Inapproximability of Edge-Disjoint Paths and Low Congestion Routing on Undirected Graphs, Combinatorica 30(5), 485–520, 2010. https://doi.org/10.1007/s00493-010-2455-9
• C. Chekuri, S. Khanna, F. B. Shepherd, An $O(\sqrt n)$ approximation and integrality gap for disjoint paths and unsplittable flow, Theory of Computing 2, 137–146, 2006. https://doi.org/10.4086/toc.2006.v002a007

Motivation

Szemerédi's regularity lemma partitions the vertex set of any graph into a bounded number of parts between which edges are distributed almost randomly. It is a central tool of extremal graph theory, but the number of parts it needs is a tower of exponentials in $1/\epsilon$, which makes it unusable in algorithms. In 1996 and 1999 Frieze and Kannan introduced a weaker notion, now called weak regularity: a partition is good if, for every pair of disjoint vertex sets $S,T$, the number of edges between them is predicted, up to an additive error $\epsilon n^2$, by the densities between the parts. This weaker requirement is enough to approximate dense instances of Max-Cut and other problems, and it can be met with only $2^{O(1/\epsilon^2)}$ parts.

The paper Frieze and Kannan, Quick approximation to matrices and applications, Combinatorica 19 (1999) derives such partitions from a matrix decomposition. Section 5.1 shows that if the adjacency matrix of a graph is approximated by a sum of a few cut matrices with small error in the cut norm, then the atoms of the sets defining those cut matrices form a pseudo-regular partition. The weak regularity of this paper later became the basis of the cut-distance theory of graph limits (Lovász, Large networks and graph limits, AMS, 2012).

Setting

Let $G=(V,E)$ be a simple graph with $n=|V|$ vertices and adjacency matrix $\mathbf A$. For a real $V\times V$ matrix $\mathbf M$ and $S,T\subseteq V$ write $\mathbf M(S,T)=\sum_{i\in S}\sum_{j\in T}\mathbf M(i,j)$. A cut matrix $\mathrm{CUT}(R,C,d)$ has entry $d$ on $R\times C$ and $0$ elsewhere. A cut decomposition of width $s$ is a sum $\mathbf D=\mathbf D^{(1)}+\dots+\mathbf D^{(s)}$ of cut matrices $\mathbf D^{(t)}=\mathrm{CUT}(R_t,C_t,d_t)$; its error is $\mathbf W=\mathbf A-\mathbf D$.