Graph Theory

Motivation

In the single-machine scheduling problem $1|\mathrm{prec}|\sum w_jC_j$, a set $N$ of $n$ jobs, each with a processing time $p_j\ge 0$ and a weight $w_j\ge 0$, is processed on one machine without interruption, subject to precedence constraints given by a partial order $P$ on $N$. The aim is to minimize the weighted sum of completion times $\sum_j w_jC_j$. The problem is strongly NP-hard for general precedence constraints (Lawler 1978; Lenstra and Rinnooy Kan 1978), and its approximability was a recurring open question in scheduling theory (Schuurman and Woeginger 1999).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph $G^S_P$ built from the instance. Many problems on partial orders become polynomial when the order is an interval order, so it is natural to ask whether this one does too. Section 7 of Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 2011) answers no: the problem stays NP-hard on interval orders. The proof is a reduction from vertex cover in connected graphs of maximum degree 3. This mission formalizes the correctness of that reduction.

Setting

A poset $P=(N,P)$ is read as a reflexive relation: $(x,y)\in P$ means $x\le y$. Jobs $x,y$ are incomparable if neither $(x,y)$ nor $(y,x)$ is in $P$, and $\operatorname{inc}(P)$ is the set of ordered incomparable pairs. The vertex cover graph $G^S_P$ has one node $(i,j)$ for each incomparable pair, weighted $p_iw_j$. Two nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$, or $j=k$ and $(i,\ell)\in P$, or $(i,\ell)\in P$ and $(k,j)\in P$. Write $w(C_I)$ for the minimum weight of a vertex cover of $G^S_I$.

A poset is an interval order if each element $x$ can be assigned a closed real interval $[a_x,b_x]$ such that $x<y$ if and only if $b_x<a_y$.

The reduction starts from a graph $G=(V,E)$ with vertices $v_1,\dots,v_N$ and a spanning tree $T=(V,E_T)$ rooted at $v_1$, numbered so that each parent comes before its children. The paper uses a breadth-first search tree.

• Stage 1. The graph $G'$ is built from $T$. Each $v_i$ gets a pendant path $v_i - u^i_1 - u^i_2$. Each non-tree edge $\{v_i,v_j\}\in E\setminus E_T$ with $i<j$ gets the path $v_i - e^{ij}_1 - e^{ij}_2 - u^j_2$. The non-tree edges themselves are not edges of $G'$.
• Stage 2. The scheduling instance $S$ has jobs $s_0$, $s_1,\dots,s_N$, $m_1,\dots,m_N$, $e_1,\dots,e_N$, and $b_{ij}$ for each non-tree edge. Their intervals, processing times and weights are given in a table on p. 662. For example, $s_j$ has interval $[i,j]$, processing time $1/k^j$ and weight $k^i$, where $v_i$ is the parent of $v_j$. The precedence constraints $I$ are the interval order of these intervals. With $n$ the number of jobs, the parameter is $k=n^2+1$.
• The set $D$. It is $\{(s_0,s_1)\}\cup\{(s_i,s_j): v_i \text{ parent of } v_j\}\cup\{(s_i,m_i),(m_i,e_i)\}\cup\{(s_i,b_{ij}),(b_{ij},m_j)\}$. The graph $G'_I$ is the subgraph of $G^S_I$ induced by $D$.

Formalization targets

Goal: Theorem 7.1 (p. 661)

For every connected graph $G$ of maximum degree at most $3$, every parent-first spanning tree $T$ and every $m\in\mathbb N$, the precedence constraints $I$ of $S$ form an interval order, and

$$G \text{ has a vertex cover of size} \le m \iff \lfloor w(C_I)\rfloor \le m + |V| + |E\setminus E_T|.$$

Milestones, in the order the proof uses them

• Claim 1 (p. 662): $\tau(G') = \tau(G)+|V|+|E\setminus E_T|$, where $\tau$ is the vertex cover number.
• Remark 7.1 (p. 662): for jobs with intervals $[a,b]$ and $[c,d]$ and $a\le d$, $p_i\le 1/k^{\lceil b\rceil}$ and $w_j\le k^{\lceil c\rceil}$. On incomparable pairs $p_iw_j\in\{1\}\cup[0,1/k]$. Moreover, $p_iw_j\ge k$ forces $b<c$, and $p_iw_j=1$ forces $\lceil b\rceil=\lceil c\rceil$.
• Claim 2 (p. 663): an incomparable pair $(i,j)$ has $p_iw_j=1$ if it is in $D$, and $p_iw_j\le 1/k$ otherwise.
• Claim 3 (p. 663): $G'_I\cong G'$.
• §7, p. 664: with $k=n^2+1$, $\sum_{(i,j)\in\operatorname{inc}(I)\setminus D}p_iw_j<1$, and hence $w(C'_I)=\lfloor w(C_I)\rfloor$.

Significance

The result. Interval orders are a standard tractable class: several scheduling and order-theoretic problems that are hard in general become polynomial on them (Papadimitriou and Yannakakis 1979). Theorem 7.1 puts $1|\mathrm{prec}|\sum w_jC_j$ outside this pattern. Section 6 of the same paper shows that the problem nonetheless has a $3/2$-approximation on interval orders, so hardness and approximability are separated on this class. The paper also remarks that the proof makes weighted vertex cover NP-hard to approximate within some factor $r>1$ on the graphs $G^S_I$ arising from interval orders.

Formalizing it. The theorem is proved in the paper. Nothing in this mission is open, and none of it has been machine-checked before. The work splits into the following parts:

• a gadget argument on unweighted vertex covers (Claim 1, after Alimonti and Kann);
• an exact case analysis of incomparable pairs in a concrete interval order (Remark 7.1, Claim 2);
• a graph isomorphism (Claim 3);
• a rounding argument that links weighted and unweighted optima.

The definitions of $G^S_P$ and of minimum-weight vertex covers are shared with the other missions of this series.

Difficulty

The construction is explicit, and each step is elementary. The work is in the bookkeeping. Claim 2 requires classifying every incomparable pair of jobs, including pairs of different kinds such as $(b_{ij}, s_\ell)$, by comparing ceilings of interval endpoints. Half-integer endpoints ($m_i$, $b_{ij}$) are exactly what separates weight-one pairs from comparable ones. Claim 3 requires checking adjacency in $G^S_I$ for all pairs of nodes of $D$ in both directions. The paper writes out two cases in each direction and calls the rest similar.

Claim 1 has a direction that is not simply local. A vertex cover of $G'$ that misses both endpoints of a non-tree edge has to be repaired by swapping gadget vertices, and the repair must be repeated without increasing the size.

A natural first idea is to treat the light nodes (weight at most $1/k$) as negligible one at a time. This does not suffice: the argument needs their total weight to stay below $1$, which is what forces $k$ to grow with $n^2$.

Formalization scope

• Graph and tree. $G$ is a SimpleGraph (Fin N); vertex $v_{i+1}$ is i, and the root is index 0. The tree is a TreeLayout: a parent function returning none exactly at the root, with each parent of smaller index and adjacent in $G$. The statements hold for every such layout. This is stronger than the paper's breadth-first tree, and the proof uses only "parent before child".
• Hypotheses of the goal. Connectivity and the degree bound ((G.neighborSet v).ncard ≤ 3) are kept as in the paper. They matter only for the NP-completeness of the source problem.
• Jobs. The jobs form an inductive type with one constructor per row of the table. Their order is a PartialOrder instance: $x\le y$ iff $x=y$ or $b_x<a_y$. Processing times and weights are real numbers. Section 1 of the paper asks for nonnegative integers, but the instance uses $1/k^j$ and the formalization follows the instance as printed.
• Constants. The constants are explicit: $k=n^2+1$ with $n$ the cardinality of the job type, and $c=|V|+|E\setminus E_T|$. Remark 7.1 and Claim 2 are stated for every real $k>1$.
• Optimum values. $w(C_I)$ is a minimum over the finite family of vertex covers. Unweighted cover numbers are Mathlib's SimpleGraph.vertexCoverNum. The floor is Nat.floor, which agrees with the integer floor because $w(C_I)\ge 0$.
• Not formalized. The goal's wording ("NP-hard") is not formalized. Neither are the NP-completeness of degree-3 vertex cover (Garey, Johnson and Stockmeyer), the polynomial size of the construction, or Theorem 2.1 (cited), which turns a vertex cover of $G^S_I$ into a schedule. What is stated is the correctness of the reduction: the instance has interval-order constraints, and its optimum decides the vertex cover question.
• No trivialization. The instance $S$ is built from $G$ and $T$ exactly as in the table. The goal quantifies over all graphs and layouts, never over an instance $S$ assumed to have the properties.
• Contributions. Contributions are welcome on any milestone. Claims 1 and 3 are independent of the weights, and Claim 2 is independent of the graph theory.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4):488–503, 2009. https://doi.org/10.1007/s00453-008-9251-1
• J. R. Correa, A. S. Schulz, Single machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
• P. Alimonti, V. Kann, Some APX-completeness results for cubic graphs, Theoret. Comput. Sci. 237(1–2):123–134, 2000. https://doi.org/10.1016/S0304-3975(98)00158-3
• M. R. Garey, D. S. Johnson, L. Stockmeyer, Some simplified NP-complete graph problems, Theoret. Comput. Sci. 1(3):237–267, 1976. https://doi.org/10.1016/0304-3975(76)90059-1
• C. H. Papadimitriou, M. Yannakakis, Scheduling interval-ordered tasks, SIAM J. Comput. 8(3):405–409, 1979. https://doi.org/10.1137/0208031

Why the variable cost matters

The problem $1|\mathrm{prec}|\sum w_jC_j$ asks for an order in which to process jobs on one machine, respecting precedence constraints, so as to minimize the weighted sum of completion times. It is strongly NP-hard, and for decades the best approximation ratio known has been $2$, achieved by several unrelated algorithms (LP relaxations, Sidney decompositions, primal–dual methods).

Correa and Schulz (2005) and Ambühl and Mastrolilli (2009) showed that the problem is a special case of weighted vertex cover: its objective splits into a fixed cost, the same for every feasible solution, and a variable cost, which equals the weight of a vertex cover in an auxiliary graph $G^S_{\mathbf P}$. Approximating vertex cover in $G^S_{\mathbf P}$ within a factor $\alpha$ therefore approximates the scheduling problem within $\alpha$. Uhan observed that the classical 2-approximations owe their guarantee to the fixed cost and can be arbitrarily bad on the variable cost alone.

Section 8 of Ambühl, Mastrolilli, Mutsanas and Svensson, Math. Oper. Res. 36(4) (2011) (DOI), proves the converse: approximating the variable cost is as hard as approximating vertex cover itself. A better-than-2 algorithm for $1|\mathrm{prec}|\sum w_jC_j$ must therefore either exploit the fixed cost or improve on the best known approximation for vertex cover, a long-standing open question.

Setting

Scheduling instance. A finite set $N$ of jobs, a partial order $\mathbf P = (N,P)$ (reflexive; $(i,j) \in P$, $i \ne j$, means $i$ precedes $j$), processing times $p_j \ge 0$ and weights $w_j \ge 0$.

Incomparable pairs. Jobs $x,y$ are incomparable, $x \parallel y$, if neither $(x,y)$ nor $(y,x)$ lies in $P$. The set $\operatorname{inc}(\mathbf P)$ consists of the ordered pairs $(x,y)$ with $x \parallel y$.

The vertex cover graph $G^S_{\mathbf P}$. One node per incomparable pair $(i,j)$, of weight $w_{(i,j)} = p_i w_j$. Distinct nodes $(i,j)$ and $(k,\ell)$ are adjacent when, in one of the two orders, $j=k$ and $i=\ell$, or $j=k$ and $(i,\ell)\in P$, or $(i,\ell),(k,j) \in P$. For a set $C$ of nodes, $w(C) = \sum_{u\in C} w_u$; for a vertex cover $C$ this is the variable cost, and $\tau_w(G^S_{\mathbf P})$ is its minimum over all vertex covers.

The instance $S(G,k)$. Given a graph $G=(V,E)$ with $V = \{v_1,\dots,v_n\}$ and $k > 0$, the instance has jobs $v'_i$ (processing time $k^{-i}$, weight $0$) and $v''_i$ (processing time $0$, weight $k^{i}$), and precedence constraints $v'_i < v''_j$ and $v'_j < v''_i$ for each edge $\{v_i,v_j\} \in E$, plus $v'_i < v''_j$ for all $i<j$. The nodes $(v'_i, v''_i)$ of $G^S_{\mathbf P}$ have weight $1$ and are called heavy; all others are light. For a set $C$ of nodes, $C_G = \{v_i : (v'_i,v''_i)\in C\}$. The vertex cover number of $G$ is $\tau(G)$.

Formalization targets

Goal: Theorem 8.1

For every graph $G$ on $n$ vertices, every $r \ge 1$, $\varepsilon>0$ and every $k \ge 1$ with $k > n^2r/\varepsilon$: if $C$ is a vertex cover of $G^S_{\mathbf P}$ for $S = S(G,k)$ with $w(C) \le r\,\tau_w(G^S_{\mathbf P})$, then $C_G$ is a vertex cover of $G$,

$$|C_G| \le r\Bigl(\tau(G) + \frac{n^2}{k}\Bigr),$$

and, when $E \ne \emptyset$,

$$|C_G| \le r\Bigl(1+\frac{n^2}{k}\Bigr)\tau(G) < (r+\varepsilon)\,\tau(G).$$

The paper words the theorem as "approximating the variable cost of $1|\mathrm{prec}|\sum w_jC_j$ is as hard as approximating vertex cover"; the statement above is the mathematical content its proof establishes.

Milestones (§8, p. 664)

1. In $G^S_{\mathbf P}$, every heavy node has weight $1$, every light node has weight at most $1/k$, and the light nodes have total weight at most $n^2/k$ (for $k \ge 1$).
2. Heavy nodes $(v'_i,v''_i)$ and $(v'_j,v''_j)$ are adjacent if and only if $\{v_i,v_j\}\in E$; for $k>1$ the subgraph induced by the weight-1 nodes is isomorphic to $G$ via $(v'_i,v''_i) \mapsto v_i$.

Significance

The result. Theorem 8.1 is one half of an equivalence: by Theorem 2.1 (Correa–Schulz, Ambühl–Mastrolilli), minimizing the variable cost is a special case of weighted vertex cover; by Theorem 8.1, it is also as hard to approximate. Any hardness of approximation for vertex cover (NP-hardness of factor $1.36$ by Dinur and Safra; factor $2-\delta$ under the unique games conjecture by Khot and Regev) transfers to the variable cost. It also explains why the known 2-approximations must rely on the fixed cost, and it frames the later result of Bansal and Khot that the full objective is hard to approximate within $2-\delta$ under a variant of the unique games conjecture.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. The mission produces a checked account of the reduction: the vertex cover graph of an arbitrary precedence-constrained instance, the adjacency-poset instance built from a graph, and the quantitative transfer of approximation ratios. The definition of $G^S_{\mathbf P}$ is shared with the other missions of this series.

Difficulty

The construction is short; the care is in the bookkeeping. One must check that the precedence relation is a partial order, determine exactly which ordered pairs are incomparable, verify that two heavy nodes are adjacent only through the third clause of the adjacency rule and only when the corresponding vertices are adjacent in $G$, and bound the weights of all remaining nodes, including the many nodes of weight $0$. The transfer then compares an approximate cover of $G^S_{\mathbf P}$ with an optimal one whose heavy part comes from an optimal cover of $G$; the additive error $n^2/k$ must be converted into a multiplicative one, which requires $\tau(G)\ge 1$.

A first reading of the page suggests that $G^S_{\mathbf P}$ has at most $n^2$ nodes; it does not. The pairs $(v'_i,v'_j)$ and $(v''_i,v''_j)$ with $i\ne j$ are incomparable nodes of weight $0$, so there can be up to $4n^2-2n$ nodes. Only nodes of positive weight are few.

Formalization scope

• Model. Jobs form a finite type; precedence constraints are an explicit reflexive partial-order relation P : N → N → Prop. Processing times and weights are nonnegative reals. The vertex cover graph is a SimpleGraph on the subtype of incomparable ordered pairs, using the symmetric closure of the printed adjacency rule without loops. Vertex covers are Mathlib's SimpleGraph.IsVertexCover; $\tau(G)$ is Mathlib's vertexCoverNum, finite for a finite graph and converted with toNat; $\tau_w(G^S_{\mathbf P})$ is a minimum over finite vertex covers.
• The instance. The graph is a SimpleGraph (Fin n); i : Fin n stands for $v_{i+1}$, so exponents are $i+1$ and the order $i<j$ is that of Fin n. Jobs are Fin n ⊕ Fin n ($v'$ left, $v''$ right). The parameter $k$ is in $\mathbb R_{\ge 0}$.
• Added hypotheses. $k \ge 1$, implicit in the page ("$k > n^2r/\varepsilon$" does not imply it when $\varepsilon$ is large, and for $k<1$ the light nodes outweigh the heavy ones). The isomorphism with $G$ is stated for $k > 1$, since at $k=1$ some light nodes also have weight $1$. The multiplicative bound requires $E \ne \emptyset$; the additive bound holds for every graph.
• Not formalized. The phrases "approximation algorithm", "polynomial time" and "as hard as"; the passage from vertex covers of $G^S_{\mathbf P}$ to schedules (Theorem 2.1, cited from Correa–Schulz and Ambühl–Mastrolilli); the fixed cost. What is stated instead is the explicit map $C \mapsto C_G$ and the ratio it achieves, $r(1+n^2/k) < r+\varepsilon$. The false count "at most $n^2$ vertices" is not stated.
• Ruled out. The goal is not a statement about an arbitrary graph or an assumed cover of $G$: it concerns the specific instance $S(G,k)$ and every $C$ that is an $r$-approximate vertex cover of its graph, and the fact that $C_G$ covers $G$ is a conclusion, not a hypothesis.
• Welcome contributions. Proofs of the two milestones and of the goal; general lemmas on $G^S_{\mathbf P}$ (weights of vertex covers, behaviour under induced subgraphs) are reusable across the series.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• J. R. Correa, A. S. Schulz, Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
• C. Ambühl, M. Mastrolilli, Single Machine Precedence Constrained Scheduling Is a Vertex Cover Problem, Algorithmica 53(4):488–503, 2009. https://doi.org/10.1007/s00453-008-9251-6
• I. Dinur, S. Safra, On the Hardness of Approximating Minimum Vertex Cover, Annals of Mathematics 162(1):439–485, 2005. https://doi.org/10.4007/annals.2005.162.439
• S. Khot, O. Regev, Vertex Cover Might Be Hard to Approximate to within 2 − ε, Journal of Computer and System Sciences 74(3):335–349, 2008. https://doi.org/10.1016/j.jcss.2007.06.019
• N. Bansal, S. Khot, Optimal Long Code Test with One Free Bit, FOCS 2009, 453–462. https://doi.org/10.1109/FOCS.2009.23

Motivation

Sparse graphs with small nontrivial eigenvalues, expanders, are basic objects in combinatorics and theoretical computer science. They are used in error-correcting codes, derandomization, sorting networks, and the analysis of random walks. The Alon–Boppana bound says that a $d$-regular graph on $n$ vertices has a nontrivial eigenvalue of absolute value at least $2\sqrt{d-1}-o(1)$ (Alon 1986; Nilli 1991). Graphs that reach $2\sqrt{d-1}$ are Ramanujan graphs.

The classical explicit Ramanujan graphs of Lubotzky, Phillips and Sarnak (1988) and Margulis exist only for degrees $d = p+1$ with $p$ prime, and only for very sparse sequences of vertex counts. Constructions with $\lambda\le 2\sqrt{d-1}+\varepsilon$ for every degree came from Mohanty, O'Donnell and Paredes (STOC 2020, arXiv:1909.06988), but their graphs also do not have every number of vertices. Alon (arXiv:2003.11673, Combinatorica 41, 2021) asked for near-Ramanujan graphs of every degree and every large size. Theorem 1.3 of that paper answers this up to $\varepsilon$: for every $d$, every $\varepsilon>0$ and every large $n$ with $nd$ even there is an explicit $(n,d,\lambda)$-graph with $\lambda\le 2\sqrt{d-1}+\varepsilon$.

Setting

A $(n,d,\lambda)$-graph is a $d$-regular simple graph on $n$ vertices in which every nontrivial eigenvalue of the adjacency matrix $A$ has absolute value at most $\lambda$. The trivial eigenvalue is $d$, with the constant eigenvector $\mathbf 1$. Equivalently, every eigenvalue $\mu$ of $A$ with an eigenvector $f\ne0$, $\sum_v f(v)=0$, satisfies $|\mu|\le\lambda$.

Distances $\operatorname{dist}(v,w)$ are graph distances, and they are $\infty$ between components. The $k$-neighbourhood of a vertex $v$ is $B(v,k)=\{w:\operatorname{dist}(v,w)\le k\}$. The $k$-neighbourhood of an edge $uv$ is $B(u,k)\cup B(v,k)$, and $N_i$ is the set of vertices at distance exactly $i$ from $\{u,v\}$. A set contains no cycle if the subgraph induced on it is a forest. A ball contains at most one cycle if its induced subgraph has at most as many edges as vertices.

The construction starts from a $d$-regular graph $H$ on a vertex set $V$ and a set $U\subseteq V$. Write $N(U)$ for the set of neighbours of $U$, and let $m$ be a perfect matching on $N(U)$. Then $H'$ is the subgraph induced on $V\setminus U$, $M$ is the graph of matching edges $\{x,m(x)\}$, and $G=H'\cup M$.

Formalization targets

Goal: Theorem 1.3, relative to the input graph

Let $d\ge3$, $\varepsilon>0$, $r=\lceil 2/\varepsilon\rceil$. Suppose $H$ is an $(N,d,2\sqrt{d-1}+\varepsilon/2)$-graph in which the $(2r+4)$-neighbourhood of every vertex contains at most one cycle, and $r\le\log_{d-1}N$. Then for every $u$ with $ud$ even and $u\le N/(2d^{2r+3})$,

$$\exists\, G \text{ on } N-u \text{ vertices}:\quad G \text{ is an } \bigl(N-u,\ d,\ 2\sqrt{d-1}+\varepsilon\bigr)\text{-graph}.$$

The hypotheses on $H$ are what Theorem 3.3 (Mohanty–O'Donnell–Paredes) supplies, and that theorem is not formalized.

Milestones

• Lemma 3.1 (p. 10). A $d$-regular graph whose $(2r+4)$-balls contain at most one cycle has a set $U$ with $|U|\ge n/(2d^{2r+3})$, cycle-free $(r+1)$-balls, and pairwise distances $\ge 2r+3$.
• Lemma 3.2 (p. 11). If the $r$-neighbourhood of an edge $uv$ contains no cycle and $A f=\mu f$ with $\mu\ge2\sqrt{d-1}$, then

$$\sum_{w\in N_i}f^2(w)\ \ge\ \sum_{w\in N_{i-1}}f^2(w),\qquad 1\le i\le r .$$

• The variational characterization of nontrivial eigenvalues (§2.4, p. 8).
• In $G=H'\cup M$: $G$ is $d$-regular on $|V|-|U|$ vertices and $A_G=A_{H'}+A_M$. Matching edges have cycle-free $(r-1)$-neighbourhoods and pairwise disjoint $r$-neighbourhoods.
• Inequalities (9), (10), (11) (p. 13), and the spectral step: for every admissible $U$ and $m$, $G$ is an $(N-|U|,d,2\sqrt{d-1}+\varepsilon)$-graph.

Significance

Theorem 1.3 shows that the size restrictions of algebraic Ramanujan constructions cost nothing spectrally: up to an arbitrarily small $\varepsilon$, the Alon–Boppana bound is attained by explicit graphs on every admissible vertex count. The deletion method is local. It turns any near-Ramanujan graph whose short cycles are sparse into graphs of all nearby sizes, so it applies to future constructions as well. Lemma 3.2 is a self-contained delocalization statement in the tradition of Kahale 1995: eigenvectors of eigenvalues at least $2\sqrt{d-1}$ in absolute value cannot concentrate near tree-like edges.

The result is proved on paper. To our knowledge none of it is formalized; Mathlib has adjacency matrices, extended graph distance and acyclicity, but no theory of expanders. A complete development would give machine-checked versions of a delocalization lemma, of the greedy selection of far-apart vertices away from short cycles, and of the variational eigenvalue bound for induced subgraphs. It would also check two points the paper passes over. The proof of Theorem 1.3 treats only positive eigenvalues $\lambda\ge2\sqrt{d-1}$. And its claim that the $r$-neighbourhood of a matching edge is cycle-free fails when two deleted vertices are at distance exactly $2r+3$. This mission states the corrected forms (see Formalization scope).

Difficulty

The spectral bound for $G$ does not follow from interlacing alone. Deleting vertices is harmless, since by (9) the quadratic form of $H'$ is controlled by $H$. But the added matching contributes up to $\sum_{x\in N(U)}f(x)^2$ to $f^tA_Gf$, which can be as large as $\|f\|^2$ for an eigenvector concentrated on $N(U)$. The obvious estimate therefore gives only $\lambda\le 2\sqrt{d-1}+1+\varepsilon/2$. Closing the gap requires showing that an eigenvector of a large eigenvalue spreads its mass over the $r$ layers around each matching edge (Lemma 3.2). That in turn needs those neighbourhoods to be trees in $G$ and pairwise disjoint, which is where Lemma 3.1's choice of $U$ is used. The combinatorial part, tracking distances and cycles in $G$ when $G$ mixes edges of $H$ with matching edges, is the main formalization burden.

Formalization scope

• Representation. Vertex sets are finite types. Graphs are Mathlib SimpleGraphs with real adjacency matrices adjMatrix ℝ. The (n, d, λ) predicate requires IsRegularOfDegree d, symmetry, row sums $d$, and $|\mu|\le\lambda$ for every eigenpair $(\mu,f)$ with $f\ne0$, $\sum f=0$. Distances use the extended SimpleGraph.edist, never dist (which is $0$ across components). Cycle conditions are on induced subgraphs, and "at most one cycle" on a ball is $|E|\le|V|$. Deleted vertices are a Finset U; the new graph lives on the subtype {v // v ∉ U}. The matching is a fixed-point-free involution of $N(U)$.
• Explicit quantities replacing the paper's asymptotics. The paper writes "sufficiently large $n$" and $u=o(n)$. The goal instead takes any $u\le N/(2d^{2r+3})$ (the size Lemma 3.1 guarantees) with $ud$ even, plus Lemma 3.1's side condition $r\le\log_{d-1}N$. The equality $r=\lceil2/\varepsilon\rceil$ is used as $\lceil2/\varepsilon\rceil_+\in\mathbb N$. The paper's "every degree $d$" becomes $d\ge3$, the range of its proof.
• Corrections. (11) and Lemma 3.2's companion are stated for $|\mu|\ge2\sqrt{d-1}$, both signs. The matching-edge note is stated for the $(r-1)$-neighbourhood, which still yields the factor $1/r$ in (11). Lemma 3.2 itself is stated as printed.
• Out of scope. Theorem 3.3 ([18]) is a cited input: its graph is the hypothesis $H$. All claims of explicitness and polynomial running time are out of scope, as is §4's remark on applying the method to LPS graphs directly.
• No trivialization. The input hypotheses are exactly Theorem 3.3's conclusions plus Lemma 3.1's side condition, and they are met by high-girth Ramanujan graphs. No hypothesis mentions the spectrum or Rayleigh quotients of the constructed graph, and the goal's graph must be $d$-regular on exactly $N-u$ vertices.
• Reusable infrastructure. Welcome contributions include the variational characterization for symmetric matrices with constant row sums, a forest edge-count lemma for balls, BFS-layer structure of cycle-free balls in regular graphs, and the edge-disjoint decomposition $A_{G}=A_{H'}+A_M$. Each is useful beyond this mission.

Selected references

• N. Alon, Explicit expanders of every degree and size, arXiv:2003.11673v1, 2020; Combinatorica 41 (2021). https://arxiv.org/abs/2003.11673
• S. Mohanty, R. O'Donnell, P. Paredes, Explicit near-Ramanujan graphs of every degree, STOC 2020. https://arxiv.org/abs/1909.06988
• A. Lubotzky, R. Phillips, P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988). https://doi.org/10.1007/BF02126799
• N. Alon, Eigenvalues and expanders, Combinatorica 6 (1986). https://doi.org/10.1007/BF02579166
• A. Nilli, On the second eigenvalue of a graph, Discrete Mathematics 91 (1991). https://doi.org/10.1016/0012-365X(91)90112-F
• N. Kahale, Eigenvalues and expansion of regular graphs, J. ACM 42 (1995). https://doi.org/10.1145/210118.210136

Motivation

A graph is perfect if every induced subgraph has chromatic number equal to its clique number. Berge conjectured in 1961 that a graph is perfect exactly when it contains no odd hole and no odd antihole. Chudnovsky, Robertson, Seymour and Thomas proved this strong perfect graph theorem in 2006 (Ann. of Math. 164 (2006), 51–229). Perfect graphs matter beyond graph theory: for them the stable set polytope is described by clique inequalities, so maximum weight stable set and colouring problems become polynomially solvable linear programs (Grötschel, Lovász and Schrijver).

The proof reduces the theorem to a decomposition statement (1.3 of the paper): every Berge graph is basic or admits one of a few decompositions. That statement is in turn proved in twelve steps, listed as 1.8.1–1.8.12. Each step excludes one kind of configuration from a Berge graph without the decompositions. This mission is step 1.8.5, restated as 13.4: it deals with Berge graphs that contain a long odd prism but no appearance of $K_4$. It is the only step of the proof that needs proper 2-joins in the complement and proper homogeneous pairs.

Setting

All graphs are finite and simple; $\overline{G}$ is the complement of $G$. A path is an induced subgraph which is a path, and its length is its number of edges. An antipath is a path of $\overline{G}$. A hole is an induced cycle of length at least $4$, and an antihole is the complement of a hole of $\overline{G}$. $G$ is Berge if every hole and antihole of $G$ has even length.

A prism consists of two disjoint triangles $\{a_1,a_2,a_3\}$, $\{b_1,b_2,b_3\}$ and three paths $P_i$ from $a_i$ to $b_i$, such that the only edges between different paths are the triangle edges. It is long if some $P_i$ has length $>1$, even if all three lengths are even, and odd otherwise.

A subdivision $H$ of a graph $J$ replaces every edge of $J$ by a track, these tracks being disjoint except at their ends. $J$ appears in $G$ if $L(H)$ is isomorphic to an induced subgraph of $G$ for some bipartite subdivision $H$ of $J$, where $L$ is the line graph.

The decompositions in the conclusion (pp. 53–54):

• A proper 2-join is a partition $(X_1,X_2)$ of $V(G)$, with disjoint nonempty $A_i,B_i\subseteq X_i$, such that the only edges between $X_1$ and $X_2$ are all edges between $A_1$ and $A_2$ and all edges between $B_1$ and $B_2$. Every component of $G|X_i$ meets $A_i$ and $B_i$. If $G|X_i$ is a path between single vertices $A_i$ and $B_i$, it has odd length $\ge 3$.
• A skew partition is a partition $(A,B)$ of $V(G)$ with $A$ not connected and $B$ not anticonnected. It is balanced if no odd path joins two nonadjacent vertices of $B$ through $A$, and no odd antipath joins two adjacent vertices of $A$ through $B$.
• A proper homogeneous pair is a pair $(A,B)$ of disjoint nonempty sets such that every other vertex is complete or anticomplete to $A$, and complete or anticomplete to $B$. All four combinations must occur.

The intermediate objects come from Sections 11–13 of the paper:

• A strip $S=(A,C,B)$: every vertex of $V(S)=A\cup B\cup C$ lies on a rung, a path from $A$ to $B$ with interior in $C$.
• A step: two disjoint rungs joined exactly by an edge at each end.
• A step-connected strip: steps cover $V(S)$ and connect $A$ and $B$.
• Left-stars and right-stars: vertices complete to $A$ (resp. $B$) and anticomplete to the rest of $V(S)$.
• A banister: a path from a left-star to a right-star whose interior sees nothing of $V(S)$.
• A staircase $K=(S,a_0\text{-}R_0\text{-}b_0)$: a step-connected strip with a banister of length $\ge 3$. A staircase can be maximal or strongly maximal.
• Three kinds of breaker: sets around a strip or staircase whose presence forces a balanced skew partition.

Formalization targets

Goal: 13.4

Let $G$ be Berge with no appearance of $K_4$ in $G$ or in $\overline{G}$, and suppose $G$ contains a long odd prism as an induced subgraph. Then

$$G \text{ or } \overline{G} \text{ admits a proper 2-join, or } G \text{ admits a balanced skew partition, or } G \text{ admits a proper homogeneous pair.}$$

Milestones

In the order of the paper's argument:

• 11.3: in a Berge graph with no even prism, every rung of a step-connected strip and every banister has odd length.
• 11.4: under no appearance of $K_4$ and no even prism, no anticonnected set $Q$ has the six properties listed in the statement.
• 11.5: a 1-breaker forces a balanced skew partition.
• 12.1: relative to a maximal staircase, every outside vertex is of exactly one of three types (minor; major; a star with a neighbour on $R_0$).
• 12.3: a connected set containing a left-star and attaching to $B\cup C$ contains a major vertex or a banister.
• 12.4: a 2-breaker forces a balanced skew partition.
• 13.3: a 3-breaker forces a balanced skew partition.

Significance

13.4 removes long prisms from the analysis. Combined with 10.6 (the even prism), it shows that a recalcitrant graph contains no long prism in $G$ or $\overline{G}$, which places it in the class $\mathcal F_5$ (p. 154). The later steps (double diamonds, odd wheels, pseudowheels, wheels) all assume this. The step-connected strip and staircase method developed here is also the paper's model for growing a maximal structure and then classifying how the rest of the graph attaches to it.

The theorem has been proved since 2006; no machine-checked proof of it or of any of its steps is known. The proof of 13.4 also cites these results of the same paper, which are posed in other missions of this series:

• 10.6 (the even-prism step), posed in mission V;
• 7.2 (equal parity of the paths of a prism), posed in mission V;
• 2.1, 2.4, 2.6, 2.7, 4.2, 4.3, 4.5, 4.6 (the Roussel–Rubio lemma and the skew-partition toolkit), posed in mission II.

Difficulty

The difficulty is the volume of case analysis behind every statement. The paper does not prove the exact analogue of the even-prism result 10.6. It warns (p. 127) that it does not know whether that analogue holds, and adds the two extra outcomes instead. The obvious first idea is to take a long odd prism and analyse attachments to it as in Section 10. The paper does not get the result that way (p. 127): it replaces two of the three paths by a maximal step-connected strip. Controlling how every remaining vertex or connected set attaches to such a strip is what the breaker results do. Maximality is also delicate. "Strongly maximal" refers to staircases of the complement, so $G$ and $\overline{G}$ must be handled in one framework.

Formalization scope

Graphs are SimpleGraph V on a Fintype vertex type with decidable equality. $\overline{G}$ is Gᶜ.

• Paths, holes, rungs, banisters. Paths are lists of distinct vertices, adjacent exactly when consecutive (induced). Holes are lists adjacent exactly when cyclically consecutive. Rungs are listed from their end in $A$ to their end in $B$, and banisters from the left-star to the right-star.
• Vertex sets. Connectedness of a vertex set is reachability inside G.induce X, so $\emptyset$ is connected. Anticonnectedness is the same notion in Gᶜ.
• Prisms. A prism is three paths whose cross adjacencies are exactly the two triangles. Each path has length at least $1$, so the triangles are disjoint.
• Appearances. A subdivision of $J$ is an injection of $V(J)$ together with one track per edge. The tracks are internally disjoint and cover every vertex and edge. An appearance is a graph embedding of $L(H)$ into $G$, and embeddings reflect adjacency.
• Staircases and breakers. A staircase is a quadruple $(A,C,B,R_0)$. Maximality quantifies over all staircases of $G$, strong maximality also over staircases of $\overline{G}$. The breakers are predicates on these data.

Every hypothesis of the paper is kept. "No appearance of $K_4$" is in $G$ and in $\overline{G}$ for the goal, and in $G$ for the milestones. The goal also keeps "Berge", "no even prism" and "no 1-/2-breaker" where the page has them. 12.1's "exactly one" is an exclusive disjunction. 11.4 is a non-existence statement.

A formalization with non-induced paths, with the complement dropped from "one of $G,\overline{G}$", or with a strip, staircase or breaker predicate that no graph satisfies would make the targets empty or false. The definitions here are checked against a concrete graph: the 8-vertex prism with path lengths $1,1,3$ is a long odd prism, and it carries a staircase. Contributions are welcome: proofs of the milestones, and reusable material on induced paths, holes and line graphs of subdivisions.

Selected references

• M. Chudnovsky, N. Robertson, P. Seymour, R. Thomas, The strong perfect graph theorem, Annals of Mathematics 164 (2006), 51–229. https://doi.org/10.4007/annals.2006.164.51
• C. Berge, Färbung von Graphen, deren sämtliche bzw. deren ungerade Kreise starr sind, Wiss. Z. Martin-Luther-Univ. Halle-Wittenberg 10 (1961), 114–115.
• V. Chvátal, Star-cutsets and perfect graphs, J. Combin. Theory Ser. B 39 (1985), 189–199. https://doi.org/10.1016/0095-8956(85)90049-8
• V. Chvátal, N. Sbihi, Bull-free Berge graphs are perfect, Graphs and Combinatorics 3 (1987), 127–139. https://doi.org/10.1007/BF01788536
• G. Cornuéjols, W. H. Cunningham, Compositions for perfect graphs, Discrete Mathematics 55 (1985), 245–254. https://doi.org/10.1016/0012-365X(85)90051-7
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

Motivation

Sparse graphs whose adjacency spectrum is concentrated near zero, expanders, are used throughout theoretical computer science: in error-correcting codes, derandomization, sorting and routing networks, and the construction of pseudorandom objects (Hoory, Linial and Wigderson, survey). The best possible spectral expansion for a $d$-regular graph is governed by the Alon–Boppana bound $2\sqrt{d-1}$, and graphs attaining it, Ramanujan graphs, were constructed explicitly by Lubotzky, Phillips and Sarnak (LPS 1988) and by Margulis. These constructions exist only for special degrees ($d = p+1$ with $p$ prime) and special numbers of vertices (orders of $PSL(2,\mathbb F_q)$ or $SL(2,\mathbb F_q)$). Applications often need a graph of a prescribed size $n$.

N. Alon's paper Explicit expanders of every degree and size (arXiv:2003.11673v1; Combinatorica 41, 2021) shows how to obtain explicit near-Ramanujan graphs on exactly $n$ vertices. This mission formalizes the spectral core of its Theorem 1.2: a Ramanujan graph on $m$ vertices can be enlarged to $n = m + r$ vertices, with degree raised by one, while the nontrivial eigenvalues stay within a constant factor of optimal.

Setting

Let $V$ be a finite set of $m \ge 1$ vertices. A $(n,d,\lambda)$-graph is a $d$-regular graph on $n$ vertices whose adjacency matrix $A$ satisfies $|\mu| \le \lambda$ for every nontrivial eigenvalue $\mu$, that is, every eigenvalue other than the top eigenvalue $d$ of the constant vector $\mathbf 1$. For a symmetric $A$ with $A\mathbf 1 = d\,\mathbf 1$, the nontrivial eigenvalues are those with an eigenvector $f \ne 0$ satisfying $\sum_v f(v) = 0$. Graphs may carry loops, at most one per vertex, and a loop adds one to the degree: it is a diagonal entry $1$ of $A$.

Fix an integer $p \ge 0$ and let $H$ be an $(m, p+1, 2\sqrt p)$-graph on $V$, a $(p+1)$-regular Ramanujan graph. Let $R = \{u_1, \dots, u_r\}$ be $r$ new vertices and let $W_1, \dots, W_r \subseteq V$ be pairwise disjoint sets of $p+2$ vertices each. Put $W = \bigcup_i W_i$ and $L = V \setminus W$. The graph $G$ on $U = V \cup R$ is obtained from $H$ by joining each $u_i$ to every vertex of $W_i$ and adding one loop at each vertex of $L$. Its adjacency matrix is

$$A_G = A_H + A_R + A_L,$$

where $A_H$ is the adjacency matrix of $H$ (zero on $R$), $A_R$ that of the stars joining $u_i$ to $W_i$, and $A_L$ the diagonal matrix of the loops. Every vertex of $G$ has degree $p+2$.

Formalization targets

Goal: Theorem 1.2, spectral core

$$A_G \text{ is an } \Big(m+r,\; p+2,\; \sqrt{2(p+1)} + \sqrt p + \frac{(p+1)\,r}{m}\Big)\text{ matrix.}$$

The paper states $\lambda \le \sqrt{2(d-1)} + \sqrt{d-1} + o(1)$ for $d = p+2$; its proof gives $\sqrt{2(p+1)} + \sqrt p + o(1)$, which is stronger, and the error term it produces is $(p+1)r/m$. The goal is parametrised by $H$, $r$ and the sets $W_i$, so it does not depend on how $m$ and $r$ are chosen.

Milestones

1. The variational characterization of the nontrivial eigenvalues: for a symmetric matrix with constant row sums and $\lambda \ge 0$, $|\mu| \le \lambda$ for every nontrivial eigenvalue if and only if $|f^tAf| \le \lambda\|f\|^2$ whenever $\sum f = 0$.
2. The Cauchy–Schwarz display: $\sum_U f = 0$ implies $|\sum_V f|^2 = |\sum_R f|^2 \le |R| \sum_R f^2$.
3. Inequality (3): $|f^tA_Hf| \le b^2(p+1) + c^2\, 2\sqrt p$ with $b^2 = (\sum_V f)^2/m$ and $c^2 = \sum_V f^2 - b^2$.
4. Display (4): $f^tA_Lf = \sum_{v\in L} f^2(v)$.
5. Inequality (5): $|f^tA_Rf| \le \frac{p+2}{x}\sum_R f^2 + x\sum_W f^2$ for every $x > 0$.
6. Inequality (6): for $\sum_U f = 0$ and $x > 0$,

$$|f^tA_Gf| \le (2\sqrt p+1)\sum_L f^2 + (2\sqrt p+x)\sum_W f^2 + \frac{p+2}{x}\sum_R f^2 + (p+1)\frac rm \sum_R f^2.$$

Significance

With $H$ the Lubotzky–Phillips–Sarnak graph on $m = |SL(2,\mathbb F_q)|$ vertices for the largest suitable prime $q$ with $m \le n$, and $r = n - m$, the distribution of primes in arithmetic progressions gives $r = o(m)$, and the goal yields an explicit $(n, p+2, \lambda)$-graph with $\lambda \le (1+\sqrt2)\sqrt{d-1} + o(1)$ for every sufficiently large $n$. This is within a factor of about $1.21$ of the Ramanujan bound $2\sqrt{d-1}$, for every number of vertices, by an elementary modification of an existing graph. The statement is useful independently of LPS: any Ramanujan graph, or any graph with a bound on its nontrivial eigenvalues, can be padded to a nearby size in the same way.

The result is proved in the paper. No formalization of it, of the $(n,d,\lambda)$ notion, or of the variational characterization of nontrivial eigenvalues for regular graphs exists on the platform. The mission produces a checked version of the spectral argument, and the variational characterization (milestone 1) is a general fact about symmetric matrices with constant row sums that applies to any spectral expander argument.

Difficulty

The vertices of $W$ and $L$ lie in the old graph $H$, whose spectrum is controlled, but the new vertices of $R$ are not; and a vector orthogonal to $\mathbf 1$ on $U$ need not be orthogonal to the constant vector on $V$. Bounding $f^tA_Gf$ by applying the Ramanujan bound for $H$ to $f$ restricted to $V$ therefore fails: the restriction has a component along the trivial eigenvector of $H$, whose eigenvalue $p+1$ is large. The argument must show that this component is small, of order $r/m$, and must balance the star edges between $R$ and $W$ against the loops on $L$ so that every vertex class gets the same coefficient. The naive bound $|f^tA_Rf| \le \|A_R\|\,\|f\|^2 = \sqrt{p+2}\,\|f\|^2$ added to $2\sqrt p$ for $H$ and $1$ for $L$ gives a constant larger than $\sqrt{2(p+1)}+\sqrt p$; the stated constant needs the weighted estimate.

On the Lean side, milestone 1 concerns the spectrum of a symmetric matrix on the invariant subspace $\mathbf 1^\perp$, while Mathlib states the spectral theorem for the whole space.

Formalization scope

• Vertices of $G$ are the disjoint union $V \oplus \mathrm{Fin}\, r$. $G$ is represented by its real adjacency matrix, since it has loops; $H$ is a Mathlib SimpleGraph with adjMatrix.
• The $(n,d,\lambda)$ predicate is stated for matrices: $|V| = n$, symmetry, $A\mathbf 1 = d\,\mathbf 1$, and $|\mu| \le \lambda$ for every eigenpair $(\mu, f)$ with $f \ne 0$ and $\sum f = 0$. For simple graphs, $d$-regularity is added.
• The paper's $o(1)$ terms are replaced by the explicit quantities its proof produces: $(p+1)r/m$ in the goal, and $(p+1)\frac rm\sum_R f^2$ in (6). Inequality (3) is stated with the corrected relation $b^2 + c^2 = \sum_V f^2$; the paper's "$b^2 + c^2 = 1$" holds only for unit restrictions.
• The bound uses $\sqrt p = \sqrt{d-2}$, as in the proof and the abstract, which implies the printed $\sqrt{d-1}$.
• $p$ is any natural number. The hypothesis "$p$ prime, $p \equiv 1 \pmod 4$" serves only to obtain $H$ from LPS, and $H$ is a hypothesis here. The sets $W_i$ are arbitrary pairwise disjoint sets of size $p+2$, not the paper's consecutive blocks of a numbering of $SL(2,\mathbb F_q)$.
• Out of scope: the existence of the prime $q$ and the estimate $n - m = o(m)$; the numbering of $SL(2,\mathbb F_q)$; the "strongly explicit" and polynomial-time claims; the LPS construction (Theorem 2.1, cited); the variant that replaces loops by a matching for even $n$.
• The goal cannot be satisfied trivially: dropping the condition $\sum f = 0$ makes it false, since $p+2$ is always an eigenvalue, and for $p \ge 2$ and small $r/m$ the bound is below $p + 2$ (for $p = 5$ it is about $5.70 + 6r/m$). At $p = 1$ the bound $3 + 2r/m$ is at least the degree $3$, so that case holds trivially; it is the paper's statement there as well.
• Contributions welcome: proofs of each milestone, especially the variational characterization, which is reusable for mission 3 of this series and for any regular-graph spectral argument.

Selected references

• N. Alon, Explicit expanders of every degree and size, arXiv:2003.11673v1, 2020; Combinatorica 41 (2021). https://arxiv.org/abs/2003.11673
• A. Lubotzky, R. Phillips, P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988) 261–277. https://doi.org/10.1007/BF02126799
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bull. AMS 43 (2006) 439–561. https://doi.org/10.1090/S0273-0979-06-01126-8

Perfect graphs and the decomposition of Berge graphs

A graph is perfect if every induced subgraph has chromatic number equal to its clique number. Perfect graphs are the graphs for which colouring and clique problems behave as linear programs do: the stable-set polytope of a perfect graph is described by its clique inequalities, so maximum weight stable sets and minimum colourings can be computed in polynomial time (Grötschel, Lovász & Schrijver 1988). In 1961 Berge conjectured that a graph is perfect exactly when it has no odd hole and no odd antihole. Chudnovsky, Robertson, Seymour and Thomas proved this, the strong perfect graph theorem, in Ann. of Math. 164 (2006).

The proof is a decomposition theorem: every Berge graph is basic or admits one of a few decompositions. The paper reaches it through twelve steps, 1.8.1–1.8.12 (p. 59), each handling graphs that contain a certain configuration. This mission poses step 1.8.3, Theorem 9.6. It handles Berge graphs that contain the line graph of a bipartite subdivision of $K_4$, all such line graphs being degenerate.

Setting

All graphs are finite and simple. $\overline{G}$ denotes the complement of $G$. A hole is an induced cycle of length at least $4$, an antihole is a hole of $\overline{G}$, and $G$ is Berge if all its holes and antiholes have even length. A path is always an induced path, and an antipath is a path of $\overline{G}$. The length of either is its number of edges.

Line graphs and appearances. The line graph $L(H)$ has vertex set $E(H)$, two edges adjacent when they share an end. $H$ is a subdivision of $J$ if it arises from $J$ by replacing every edge by a track (a path, not necessarily induced), these tracks disjoint except for their ends. $J$ appears in $G$ if, for some bipartite subdivision $H$ of $J$, $L(H)$ is isomorphic to an induced subgraph of $G$; $L(H)$ is then an appearance of $J$. For $J = K_4$ the appearance is degenerate if some 4-cycle of $H$ contains the four vertices of degree three. A $K_4$-enlargement is a 3-connected graph with a proper subgraph isomorphic to a subdivision of $K_4$. An appearance $L(H)$ is overshadowed if some branch of $H$ of odd length $\ge 3$, with ends $b_1, b_2$, has a vertex of $G$ nonadjacent to at most one edge at $b_1$ and at most one edge at $b_2$.

Knots and striations. A knot $(P_1, P_2, Q_1, Q_2)$ is formed by two paths $P_i$ with ends $a_i, b_i$ and two antipaths $Q_j$ with ends $x_j, y_j$. They are pairwise disjoint and of length $\ge 1$, $P_1$ is anticomplete to $P_2$, $Q_1$ is complete to $Q_2$, and the ends are joined in a prescribed twisted pattern (pp. 107–108). A degenerate appearance of $K_4$ is a knot. A strip $(A, C, B)$ is a family of paths ("rungs") from $A$ to $B$ through $C$; an antistrip is a strip of $\overline{G}$. A striation $L$ is made of $m \ge 2$ strips and $n \ge 2$ antistrips. All rungs and antirungs are odd, the strips are pairwise anticomplete, the antistrips pairwise complete, and every strip is parallel or co-parallel to every antistrip, with enough "twists" between them (p. 112). A striation is maximal if no striation has a strictly larger vertex set. The paper defines when a set of vertices is local for a knot or striation and when it resolves one.

Outcomes. A double split graph has its vertices partitioned into $\{a_i\}, \{b_i\}$ ($m \ge 2$) and $\{c_j\}, \{d_j\}$ ($n \ge 2$). Each $a_ib_i$ is an edge and each $c_jd_j$ a nonedge, distinct pairs $\{a_i,b_i\}$ are anticomplete and distinct pairs $\{c_j,d_j\}$ complete to each other, and every $\{a_i,b_i\}$ and $\{c_j,d_j\}$ are joined by exactly two disjoint edges. A skew partition $(A, B)$ of $V(G)$ has $G|A$ disconnected and $\overline{G}|B$ disconnected. It is balanced if no odd path joins nonadjacent vertices of $B$ through $A$ and no odd antipath joins adjacent vertices of $A$ through $B$. A proper 2-join is a partition $(X_1, X_2)$ of $V(G)$ whose only cross edges are complete joins $A_1$–$A_2$ and $B_1$–$B_2$, with the side conditions of p. 53.

Formalization targets

Goal: Theorem 9.6 (p. 116)

Let $G$ be Berge, with every appearance of $K_4$ in $G$ and in $\overline{G}$ degenerate and no induced subgraph of $G$ isomorphic to $L(K_{3,3})$. Then

$$G \text{ is double split} \ \lor\ G \text{ admits a balanced skew partition} \ \lor\ G \text{ or } \overline{G} \text{ admits a proper 2-join} \ \lor\ K_4 \text{ appears in neither } G \text{ nor } \overline{G}.$$

Milestones

1. 9.1 (p. 108): in a knot of a Berge graph all four paths and antipaths are odd, and either both paths or both antipaths have length one.
2. 9.3 (p. 109): a connected set $F$ whose attachments to a knot are not local either contains a vertex whose neighbourhood resolves the knot, or attaches in one of three special ways ("up to symmetry").
3. 9.4 (p. 112): the neighbourhood in $V(L)$ of a vertex outside a maximal striation $L$ is local or resolves $L$.
4. 9.5 (p. 113): if every vertex of a connected set $F$ outside $V(L)$ has a local neighbourhood, then the attachments of $F$ in $V(L)$ are local.

9.3–9.5 assume that no $K_4$-enlargement appears in $G$ or $\overline{G}$ and that no appearance of $K_4$ in $G$ or $\overline{G}$ is overshadowed. An optional, non-milestone item poses 9.7 (p. 118): a Berge graph with an appearance of $K_4$ is a line graph or the complement of one, a double split graph, or admits a proper 2-join (in $G$ or $\overline{G}$) or a balanced skew partition.

Significance

9.6 is the step of the proof that produces double split graphs, one of the five basic classes. In the main argument it follows step 1.8.1 (5.1, nondegenerate appearances of $K_4$) and is combined with it in 9.7. Through 9.7 it gives the first half of 13.5: every recalcitrant graph belongs to the class $\mathcal{F}_5$ and so contains no appearance of $K_4$ in $G$ or $\overline{G}$.

The theorem has been proved since 2006. We know of no machine-checked proof of the strong perfect graph theorem or of any of its steps. Mathlib has line graphs and graph embeddings but no subdivisions, appearances or decompositions of Berge graphs. This mission produces a faithful Lean statement of step 1.8.3 and of the four lemmas its proof rests on, together with Lean definitions of knots, strips and striations.

Difficulty

The obvious approach would take a degenerate appearance of $K_4$ and study how each remaining vertex attaches to it, as §§5–6 do for nondegenerate appearances. This does not close. A degenerate appearance can be read as a line graph or as its complement, so the analysis of a vertex in $G$ and in $\overline{G}$ has to be run at once. Single vertices can also be absorbed into larger structures that the line-graph analysis does not see. The proof grows the appearance to a maximal striation and classifies attachments to it, and the hard steps are 9.4 and 9.5. Their proofs need 9.3 in every case, and they use maximality to refute configurations that would let the striation grow.

Formalization scope

Graphs are SimpleGraph V on a Fintype with decidable equality. Every object is defined as on the page, in the namespace StrongPerfectGraph.DoubleSplit.

• Paths and antipaths are induced and given as vertex lists. A list fixes the labelling of the ends: $a_i, b_i$ are the first and last vertices of $P_i$, and $x_j, y_j$ those of $Q_j$.
• The empty set is connected (p. 54).
• Line graphs are Mathlib's SimpleGraph.lineGraph; "isomorphic to an induced subgraph" is an induced embedding ↪g. Subdivisions $H$ and enlargements $J'$ range over graphs on Fin k.
• "Every appearance of $K_4$ is degenerate" is the absence of a nondegenerate appearance. The hypothesis on $L(K_{3,3})$ concerns $G$ only. Every other hypothesis concerns both $G$ and $\overline{G}$, as on the page.
• A striation is a structure with $m$ strips and $n$ antistrips indexed by Fin m, Fin n.
• "Up to symmetry" in 9.3 is the paper's exchange of $P_1, P_2$ and $Q_1, Q_2$ with the ends renamed so that the result is again a knot. Both compatible renamings are allowed, and so is their composite, the reversal of all four.

Dropping the bars of the complement would make the theorem false or vacuous. So would reading "path" as a non-induced path, or encoding a decomposition so that it always exists. The statements use the complement explicitly, induced paths throughout, and the full definitions of p. 53–54.

The proof of 9.6 also uses results of the same paper that are posed in other missions of this series. These are 2.1, 2.2, 4.1 and 4.2, posed in mission II (skew partitions), and 5.3, 5.8, 6.1 and 7.5, posed in mission III (line graphs). They are not posed again here. The bridge 9.2 between knots and line graphs, whose proof the paper omits as obvious, is not posed either. Proofs of 9.1, of 9.3, and reusable lemmas about knots and striations are welcome.

Selected references

• M. Chudnovsky, N. Robertson, P. Seymour, R. Thomas, The strong perfect graph theorem, Annals of Mathematics 164 (2006), 51–229. https://doi.org/10.4007/annals.2006.164.51
• C. Berge, Färbung von Graphen, deren sämtliche bzw. deren ungerade Kreise starr sind, Wiss. Z. Martin-Luther-Univ. Halle-Wittenberg Math.-Natur. Reihe 10 (1961), 114.
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4