Graph Theory

Motivation

Minimum-cost flow is a standard model for routing a quantity through a network while paying a cost on each arc. Unit capacities arise when each input arc can carry at most one unit; they include flow formulations of several matching and assignment problems. Goldberg, Kaplan, Hed and Tarjan analyze a cost-scaling algorithm for this setting. Their second-phase argument depends on a bound on the excess left in a pseudoflow when every excess vertex has undergone enough potential increases. This mission formalizes that bound, Lemma 5 of their STACS 2015 paper. The published paper gives an $O(\min\{m^{1/2},n^{2/3}\}\,m\log(nC))$ running-time bound for its unit-capacity algorithm; the running-time statement itself is outside this mission.

Setting

A network has a finite vertex set $V$ and an arc set $E$ that contains both orientations of each input arc. Write $n=|V|$. Every input arc has capacity one; its reverse has capacity zero and opposite cost. Write $m$ for the number of input arcs, so $|E|=2m$. The paper assumes no parallel or antiparallel input arcs, allowing an arc to be identified by its ordered endpoints. Costs are antisymmetric between orientations.

A pseudoflow $f$ assigns an antisymmetric quantity to each arc and respects its capacity. Its excess at $v$ is the sum $e_f(v)$ of incoming flow. Positive excess means that $v$ has flow to discharge; negative excess is a deficit. A circulation is a pseudoflow with zero excess at every vertex. An arc is residual for $f$ when its residual capacity $u_f(v,w)=u(v,w)-f(v,w)$ is positive. For vertex prices $p$, its reduced cost is $c_p(v,w)=c(v,w)-p(v)+p(w)$. A pseudoflow is $\varepsilon$-optimal at $p$ when every residual arc has reduced cost at least $-\varepsilon$. These are the paper's conventions on p. 408.

At the start of a cost scale, let $f'$ be a circulation that is $2\varepsilon$-optimal at prices $p'$. During the scale, $f$ is a pseudoflow that is $\varepsilon$-optimal at prices $p$. The potential increase in scale units is $d(v)=(p(v)-p'(v))/\varepsilon$. Put $\lambda=\min\{\sqrt m,n^{2/3}\}$. The second phase begins when every excess vertex has $d(v)\ge\lambda$; the paper also states that every deficit then has $d(v)=0$ and that the levels $d(v)$ are integral. The remaining excess is $X(f)=\sum_{v:e_f(v)>0}e_f(v)$.

The comparison graph has arcs $E^+=\{(v,w)\in E:f'(v,w)>f(v,w)\}$ and vertices $V$. An excess–deficit cut $Y\subseteq E^+$ meets every path in this graph from an excess vertex to a deficit vertex. Thus a cut is measured among comparison arcs, not among arbitrary arcs of the original network. Lemmas 3 and 4 of the paper establish the level and cut bounds on which the excess estimate rests.

Formalization targets

The goal is Lemma 5 on p. 410, stated with both constants obtained in its proof. Under the cost-scale conditions above, and the divisibility conventions in footnotes 5–6, its two cases are

$$\lambda=\sqrt m\quad\Longrightarrow\quad X(f)\le 3\lambda,$$ $$\lambda=n^{2/3}\quad\Longrightarrow\quad X(f)\le36\lambda.$$

The second case also assumes that six divides the integer $\lambda$; the first uses divisibility by three. The goal keeps the two conclusions separate so that the stronger $3\lambda$ bound is retained when $\sqrt m$ determines the scale. Its milestone list follows the paper: Lemma 3 bounds $d(v)-d(w)$ by three on an arc of $E^+$; Lemma 4 bounds total excess by a cut; and the proof of Lemma 5 supplies the cut bands and the two size estimates. The bands use the exact three-level and six-level ranges printed on p. 410.

Significance

The result connects a condition on price increases to a numerical bound on the amount of flow still needing discharge. Combined with the paper's time per unit of remaining excess, this is the bound needed for its second-phase running-time estimate. The two regimes show how the same cost-scale state can be controlled by either the number of input arcs or the number of vertices. Without the excess bound, the paper's argument gives no comparable limit on the remaining work at the phase transition.

The paper proves Lemma 5, but this particular unit-capacity excess argument has no matching theorem in the platform catalog checked for this mission. The network, circulation and pseudoflow interfaces are already published as reusable definitions from earlier cost-scaling work. A completed machine-checked development would add the cut argument and band counts to those interfaces. Those facts can also support other analyses that compare an entry circulation with an intermediate pseudoflow; this mission does not claim to formalize the algorithm's entire execution or its running-time model.

Difficulty

The main obstacle is linking local price inequalities to a global bound on excess. A reduced-cost inequality controls a single residual arc, while excess may move through a path and is measured over many vertices. The comparison graph $G^+$ is essential: on a residual arc outside $E^+$, the level difference used by Lemma 3 is not available. Counting all residual arcs as if they were comparison arcs would therefore not justify the cut bound. There is a separate counting issue: the represented network has both directions of each input arc, so using $|E|$ for $m$ changes the constant in the square-root case.

Formalization scope

Lean represents the network by a finite symmetric arc set with real capacities and antisymmetric real costs. A local unit-capacity predicate marks each reverse pair as capacities $(1,0)$ or $(0,1)$; $m$ counts the capacity-one orientations. Flows are real valued as on p. 408. Integer costs on that page are generalized to real costs because Lemmas 3–5 use only antisymmetry and reduced-cost inequalities. No result here depends on cost integrality.

The formalization takes the cost-scale state as hypotheses: $\varepsilon>0$, entry circulation and $2\varepsilon$-optimality, current $\varepsilon$-optimality, integral levels, level at least $\lambda$ at excess vertices, and zero level at deficits. It takes $\lambda$ as a natural number equal to $\min\{\sqrt m,n^{2/3}\}$ and records the paper's divisibility simplifications. The indexed pigeonhole milestones also require $\lambda>0$ so their index ranges are nonempty; the goal includes the zero-arc boundary without requiring an index. Cuts use reachability after deleting a subset of $E^+$, equivalent to meeting every excess-to-deficit path. The proof of Lemma 5 prints “cut in $G_f$”; the formalized claim uses $G^+$, the graph for which Lemma 3 gives the required level control and Lemma 4 states its bound.

The definition layer, path-cut lemma and finite counting arguments are the reusable infrastructure. Contributions that establish these exact statements, their necessary elementary flow identities, or a machine-checked goal proof are in scope. Counting $m$ with reverse arcs, allowing cuts outside $E^+$, using arbitrary real levels in place of integral ones, or replacing both cases by the weaker $36\lambda$ bound does not express this target.

Selected references

• A. V. Goldberg, H. Kaplan, S. Hed and R. E. Tarjan, Minimum Cost Flows in Graphs with Unit Capacities, 32nd International Symposium on Theoretical Aspects of Computer Science, LIPIcs 30, pp. 406–419, 2015. doi:10.4230/LIPIcs.STACS.2015.406.

Motivation

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

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

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

Setting

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

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

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

Formalization targets

Goal: Theorem 2 with the paper's bound

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

The adjacency matrix of an Erdős–Rényi random graph contains a large deterministic mean as well as random fluctuations. The mean affects the largest eigenvalue, while the centered fluctuations determine much of the remaining spectrum. A local spectral law must describe both pieces at a resolution fine enough to distinguish eigenvalues within a narrow energy window. Erdős, Knowles, Yau and Yin established such estimates for a broader class of sparse symmetric matrices and their noncentered rank-one deformations in Spectral statistics of Erdős–Rényi graphs I. This mission formalizes the paper's Theorem 2.9, with the centered-matrix law and eleven intermediate results of the paper as milestones.

The paper treats the graph matrix through a model that also allows other sparse distributions. Its parameters $q_N$ and $f_N$ separate sparsity from the size of the deterministic mean. That separation matters: the normalized resolvent trace can obey a local semicircle law even when the deformation produces a distinguished top eigenvalue. The formal target therefore concerns the deformed matrix itself, rather than replacing it with the centered matrix.

Setting

For each size $N$, let $H_N=(h_{ij})$ be a real symmetric random matrix. Entries indexed by the upper triangle are independent, centered, and have variance $1/N$. Their higher moments obey

$$\mathbf E|h_{ij}|^p\le\frac{C^p}{Nq_N^{p-2}},\qquad 3\le p\le(\log N)^{A_0\log\log N}.$$

The sparsity parameter $q_N$ lies between $(\log N)^{3\xi_N}$ and $C\sqrt N$, and the logarithmic parameter satisfies $1+a_0\le\xi_N\le A_0\log\log N$, with $a_0>0$ and $A_0\ge10$. Define $e_N=N^{-1/2}(1,\ldots,1)$ and the noncentered matrix $A_N=H_N+f_N|e_N\rangle\langle e_N|$, where $0\le f_N\le N^C$. The projection $|e_N\rangle\langle e_N|$ has every entry equal to $1/N$. These are Definitions 2.1 and 2.2 of the source paper, pp. 5–6.

For a complex number $z=E+i\eta$ with $\eta>0$, the resolvents are $G(z)=(H_N-zI)^{-1}$ and $\widetilde G(z)=(A_N-zI)^{-1}$. Their normalized traces are $m(z)=N^{-1}\operatorname{Tr}G(z)$ and $\widetilde m(z)=N^{-1}\operatorname{Tr}\widetilde G(z)$. The comparison object is the semicircle density $\rho_{\mathrm{sc}}(x)=(2\pi)^{-1}\sqrt{[4-x^2]_+}$ and its Stieltjes transform $m_{\mathrm{sc}}(z)=\int_{\mathbb R}\rho_{\mathrm{sc}}(x)/(x-z)\,dx$. Put $\kappa_E=\bigl||E|-2\bigr|$ and $D=\{E+i\eta:|E|\le\Sigma,\ 0<\eta\le3\}$ for a fixed $\Sigma\ge3$. These definitions appear in Section 2, pp. 7–9.

An $N$-dependent event has $(\xi,\nu)$-high probability when its failure probability is at most $\exp[-\nu(\log N)^{\xi_N}]$ for all sufficiently large $N$. The spectral estimates below refer to single events on which the claimed bound holds at every $z\in D$ simultaneously.

Formalization targets

Main goal: the local law for A

Theorem 2.9 assumes $\xi_N\sim(A_0/2)\log\log N$ and $q_N\ge(\log N)^{C_1\xi_N}$. Its first conclusion is that, with $(\xi,\nu)$-high probability, every $z=E+i\eta\in D$ satisfies

$$|\widetilde m(z)-m_{\mathrm{sc}}(z)|\le(\log N)^{C_2\xi_N}\left(\min\left\{\frac1{q_N^2\sqrt{\kappa_E+\eta}},\frac1{q_N}\right\}+\frac1{N\eta}\right).$$

Under the additional bound $f_N\le C_0\sqrt N$, its second conclusion controls every entry at every $z\in D$:

$$|\widetilde G_{ij}(z)-\delta_{ij}m_{\mathrm{sc}}(z)|\le(\log N)^{C_2\xi_N}\left(\frac1{q_N}+\sqrt{\frac{\operatorname{Im}m_{\mathrm{sc}}(z)}{N\eta}}+\frac1{N\eta}\right).$$

The constants $C_1,C_2$ are universal and positive. The probability exponent $\nu>0$ may depend on the fixed parameters named in the theorem. Both conclusions, including the extra condition on $f_N$ in the second, are retained from Theorem 2.9, pp. 9–10.

Milestones

The milestones follow the paper's own sequence of numbered results.

1. Properties of $m_{\mathrm{sc}}$ (Lemma 3.2): $|m_{\mathrm{sc}}|\sim1$, $|1-m_{\mathrm{sc}}^2|\sim\sqrt{\kappa_E+\eta}$, and the size of $\operatorname{Im}m_{\mathrm{sc}}$ inside and outside the spectrum.
2. Resolvent identities for minors (Lemma 3.4) and the self-consistent equation $G_{ii}=1/(-z-m_{\mathrm{sc}}-([v]-\Upsilon_i))$ (Lemma 3.10); both are deterministic.
3. Large deviation bounds for linear and quadratic forms in independent variables with the sparse moment decay (Lemma 3.8 (ii)).
4. The weak local semicircle law for $H$ (Theorem 3.1) on $D_L=\{|E|\le\Sigma,\ (\log N)^LN^{-1}\le\eta\le3\}$, $L\ge8\xi$.
5. Fluctuation averaging (Lemma 4.1 (4.2)): the average $[Z]=N^{-1}\sum_iZ_i$ of the fluctuation terms is much smaller than each $Z_i$.
6. The a priori norm bound $\|H\|\le2+(\log N)^\xi q^{-1/2}$ (Lemma 4.3) and the strong local law for $H$ (Theorem 2.8, the analogue of the goal for $f=0$).
7. Interlacing of the eigenvalues of $H$ and $A$ (Lemma 6.1) and the near-orthogonality $\sum_{\alpha\ne N}|\langle v_\alpha,e\rangle|^2=O(f^{-2})$ of $e$ to the non-top eigenvectors of $A$ (Corollary 6.7).
8. The trace comparison $|\widetilde\Lambda-\Lambda|\le\pi/(N\eta)$ (Lemma 7.1), which yields the first conclusion of the goal from Theorem 2.8.
9. Entrywise control of $\widetilde G$ on the event $\widetilde\Omega(\eta)$ that $\widetilde\Lambda_d+\widetilde\Lambda_o\le(\log N)^{-\xi}$ on the line $\operatorname{Im}z=\eta$: the off-diagonal bound $\widetilde\Lambda_o\le C\Phi$ (Proposition 7.6 (7.14)) and the diagonal bounds of Lemma 7.7, with $\Phi=(\log N)^\xi/q+(\log N)^{2\xi}(\sqrt{\operatorname{Im}\widetilde m/(N\eta)}+1/(N\eta))$.

Significance

The trace estimate gives quantitative control over spectral mass at local scales, including near the edges $E=\pm2$. The entrywise estimate says more: each resolvent entry is close to the diagonal semicircle approximation with an error that records both sparsity and finite-size effects. The paper's later results derive density-of-states and eigenvector statements from these local controls. Those consequences are outside this mission's goal.

The intended formal development supplies reusable definitions of sparse symmetric ensembles, high-probability events, semicircle transforms, and complex resolvents, followed by exact statements of the paper's estimates. Mathlib contains no local semicircle law, for Wigner or for sparse matrices, and no Stieltjes transform of the semicircle distribution; the local law, the large deviation bounds and the interlacing lemma are each reusable beyond this paper.

Difficulty

The deterministic rank-one comparison controls the normalized trace but does not by itself control each entry of $\widetilde G$. The entrywise estimate must account for the deformation and for fluctuations caused by sparse entries. Near the spectral edges, the stability scale of the semicircle transform changes with $\kappa_E+\eta$; a bound that is uniform in the bulk does not automatically retain the paper's edge behavior. The theorem also asks for one event covering a continuum of $z$ values, so a collection of separate fixed-$z$ probability bounds has the wrong quantifier order. These are substantive parts of Sections 3–7, beyond algebraic manipulation of resolvents.

Formalization scope

Lean represents all $H_N$ on one probability space and takes their entries to be real, symmetric, measurable random variables, independent in the upper triangle. Conditions involving $\log\log N$ and the moments hold for all sufficiently large $N$; this avoids impossible small-$N$ parameter bounds and matches the asymptotic theorem. The moment order $p$ is real, as in the paper. Each finite expectation has an explicit integrability condition. A single positive constant $C$ is used for the moment, sparsity, and deformation bounds: replacing several fixed constants by their maximum preserves all three inequalities.

Matrix indices use Fin N rather than the paper's $1,\ldots,N$. The resolvent is a complex matrix formed by coercing the real matrix before subtracting $zI$. Every result that uses it restricts $\eta>0$ eventually or explicitly; its inverse at a singular input is never used to make a claim. The semicircle transform is defined by the paper's integral, and $\sqrt{4-x^2}$ uses Lean's nonnegative square root, implementing the positive part. The high-probability predicate evaluates the measure of arbitrary sets, so it can state the intersection over all $z$ without a separate measurability assumption on that intersection. Positive $q_N$ and positive square-root arguments follow eventually from the model and $z\in D$.

The deterministic Lemmas 3.2, 3.4, 3.10, 6.1 and 7.1 are stated for every real symmetric matrix and every $z$ with $\eta>0$ (Lemma 3.2 on $D$); the paper's $D_L$ is contained there. Minors keep the original index names, and $G^{(\mathbb T)}_{kl}$ is only used for $k,l\notin\mathbb T$. $Z_i$ is the explicit expression of (3.15). Ordered eigenvalues are the sorted roots of the characteristic polynomial. Statements the paper makes "for fixed $z$" (Lemmas 4.1, 7.7, Proposition 7.6) are uniform in $z$: one threshold $N_0$ serves every $z$. The unnamed constants $C$, $\nu$, $K$ are chosen after the fixed parameters and before the random matrices; the universal $C_1,C_2$ come first.

Trivializing encodings are ruled out: every resolvent is taken at $\eta>0$, so the junk inverse of a singular matrix never enters; the model is satisfiable (independent Rademacher signs divided by $\sqrt N$ with $q_N=\sqrt N$ and $\xi_N=(A_0/2)\log\log N$ satisfy it for large $N$); each event of the goal is one intersection over all $z\in D$, not a family of pointwise bounds; the constants appear in the paper's order; and the goal is about $A=H+f|e\rangle\langle e|$ with $f$ allowed to be large, so it does not reduce to Theorem 2.8.

Part (iii) of Lemma 3.8 is not a milestone: the printed (3.22) omits the diagonal variance term $(N^{-2}\sum_i|B_{ii}|^2)^{1/2}$, without which it fails for Rademacher variables with $q\asymp\sqrt N$. Contributions of proofs of any milestone, and of the missing groundwork (Stieltjes transforms of measures, Schur complements of resolvents, moment bounds for sums of independent variables), are welcome.

Selected references

• L. Erdős, A. Knowles, H.-T. Yau and J. Yin, Spectral statistics of Erdős–Rényi graphs I: Local semicircle law, Annals of Probability 41(3B), 2013, pp. 2279–2375. arXiv:1103.1919v5; DOI:10.1214/11-AOP734.

Motivation

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

Setting

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

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

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

Formalization targets

Queue bound for planar graphs

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

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

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

Layered partition and transfer bounds

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

The characteristic polynomial of an ordinary graph records spectral information in coefficients that can also be described by finite graph configurations. The classical Harary–Sachs theorem is an instance of this connection. For a uniform hypergraph, the adjacency object is a tensor rather than a matrix, and its characteristic polynomial is defined through a multivariate resultant. Clark and Cooper's hypergraph theorem gives a corresponding coefficient formula. It identifies the configurations that replace the elementary subgraphs of the graph case and assigns them weights determined by directed Eulerian structures. The result makes a tensor spectral invariant accessible through finite combinatorial objects.

The article appeared as Gregory J. Clark and Joshua N. Cooper, A Harary-Sachs theorem for hypergraphs, Journal of Combinatorial Theory, Series B (2021), DOI 10.1016/j.jctb.2021.01.002. This mission follows the pinned arXiv version 2, whose page and theorem numbers are used below.

Setting

A simple $k$-graph $\mathcal H=([n],E)$ has a fixed vertex set of $n$ labeled vertices and a set $E$ of distinct edges, each containing exactly $k$ vertices. Isolated vertices remain part of $[n]$. The normalized adjacency hypermatrix $\mathcal A_{\mathcal H}$ gives an ordered $k$-tuple the value $1/(k-1)!$ when its underlying set is an edge, and zero otherwise. This normalization makes every ordering of the other $k-1$ vertices contribute the intended total weight.

The characteristic polynomial $\phi(\mathcal H)$ is the multivariate resultant of the coordinates of $(\lambda\mathcal I-\mathcal A_{\mathcal H})x^{k-1}$. The resultant is characterized by three conditions: it vanishes exactly when homogeneous coordinate polynomials have a nonzero common complex root, it evaluates to one on the coordinate monomials, and it is irreducible over the complex coefficient field. Its degree in $\lambda$ is $t=n(k-1)^{n-1}$. The codegree-$d$ coefficient $\phi_d(\mathcal H)$ is the coefficient of $\lambda^{t-d}$; this degree is fixed from the source theorem and is not read from an implementation of $\phi$.

A multi-hypergraph $S$ is a multiset of $k$-element edges. It is Veblen when the degree of every vertex is divisible by $k$. Its flattening discards repeated edges, so $S$ is an infragraph of $\mathcal H$ when every edge of its flattening belongs to $E$. Components use only vertices covered by edges; a labeled object may still sit in a larger ambient vertex set with unused vertices.

A rooting of $S$ is a sequence of its edges, each assigned a root vertex in that edge, with roots in nondecreasing order. An edge rooted at $u$ contributes a directed arc $u\to v$ to every other vertex $v$ of the edge. Summing these arcs with multiplicity produces a directed multigraph $D_R$. An Euler rooting has balanced in- and out-degrees and connected positive-degree vertices. Its arborescence number $\tau(D_R)$ counts spanning trees of these active vertices directed toward a specified root, with parallel arcs distinguished. For connected $S$, its associated coefficient is

$$C_S=\sum_{R:\,D_R\text{ Eulerian}}\frac{\tau(D_R)}{\prod_{v\in V(D_R)}\deg^-(v)}.$$

For disconnected $S$, $C_S$ is the product of the coefficients of its connected components. These conventions follow Definitions 6–10 in the source.

Formalization targets

Differential trace and Euler rootings

The supporting targets identify when a monomial differential operator contributes to a matrix trace, and show that an Euler rooting determines a connected Veblen multi-hypergraph. The operator identity is counted by Euler tours with distinguishable parallel arcs. The resultant-to-trace identity quoted in the paper is also a milestone:

$$\phi_d(\mathcal H)=P_d\left(-\operatorname{Tr}_1(\mathcal H)/1,\ldots,-\operatorname{Tr}_d(\mathcal H)/d\right).$$

Here $P_d$ is the paper's sum over positive compositions of $d$, and $\operatorname{Tr}_j$ is its differential trace from Equation (1).

Harary–Sachs coefficient formula

The goal uses the labeled form of Theorem 14. Let $\mathscr T_m(d,\mathcal H)$ be the set of ordered $m$-tuples $(S_1,\ldots,S_m)$ of connected labeled Veblen infragraphs whose edge counts sum to $d$. Then

$$\phi_d(\mathcal H)=\sum_{m=1}^{d}\frac{\bigl(-(k-1)^n\bigr)^m}{m!}\sum_{(S_1,\ldots,S_m)\in\mathscr T_m(d,\mathcal H)}\prod_{i=1}^{m}C_{S_i}.$$

The paper prints the equivalent sum over isomorphism classes, using automorphism groups and the copy weight $(\#H\subseteq\mathcal H)$. The labeled expression is the result before that grouping. The isomorphism-class statement is outside this mission's Lean target and remains a separate formalization task.

Significance

The theorem expresses a coefficient of a resultant, defined algebraically over complex common roots, as a finite rational weighted sum over hypergraph configurations. It extends the graph case while preserving the exact normalization, sign, component count, and coefficient index. The formula can be used to study low codegree coefficients by enumerating finite Veblen infragraphs and their Euler rootings. Clark and Cooper also use associated coefficients to compare different hypergraph structures in the paper.

The formal development separates the resultant, the differential trace, and the combinatorial counts into reusable definitions. It would provide machine-checked statements of the paper's main equality and several links between those definitions. The Lean theorems in this draft are open targets with sorry placeholders; compiling their statements does not constitute a machine-checked proof of the paper's claims.

Difficulty

The ordinary matrix determinant has a direct expansion by permutations. A tensor characteristic polynomial is a multivariate resultant, so that expansion does not directly reveal which hypergraphs contribute to a coefficient. The trace side uses repeated partial derivatives, and repeated hyperedges can create several distinct rootings with the same directed arc multiplicities. Counting only a multiset of root assignments loses those orderings and changes the coefficient. The Eulerian condition, arborescence multiplicities, and factorial factors must agree simultaneously for the algebraic and combinatorial expressions to match.

Formalization scope

The Lean representation uses Fin n vertices, finite sets of simple edges, multisets of repeated edges, rational adjacency weights, and complex polynomials only for the resultant criterion. It assumes $k\ge2$, $n\ge1$, and $1\le d\le n(k-1)^{n-1}$. The source fixes $k\ge2$, and the latter two bounds expose the domain in which the printed coefficient expansion and its proof use $d$. An isolated vertex of $\mathcal H$ counts in $n$ and in $(k-1)^n$, while isolated vertices do not pad a multi-hypergraph component.

The formalization takes a polynomial satisfying the resultant's common-root, normalization, and irreducibility properties as an input. Separate sanity proofs give witnesses in the one-variable degree-zero and degree-one cases; degree one covers the first goal-domain degree when $k=2$. The characteristic polynomial is evaluated from this polynomial, never defined by the trace identity. Rootings are sequences, arborescences are directed toward the least positive-degree vertex, and the associated coefficient is calculated on covered vertices. The goal uses the labeled sum, so no automorphism is computed on an ambient padded vertex set. Contributions formalizing the omitted isomorphism-class equivalence, the BEST circuit count, and proofs of the stated targets are welcome.

Selected references

• Gregory J. Clark and Joshua N. Cooper, A Harary-Sachs theorem for hypergraphs, Journal of Combinatorial Theory, Series B, 2021. arXiv:1812.00468v2; DOI 10.1016/j.jctb.2021.01.002.

Motivation

A graph may have enough symmetry for every edge to look the same while its vertices still fall into two distinct classes. Such a graph is semisymmetric when it has constant valency, is edge-transitive, and is not vertex-transitive. Conder, Zhou, Feng and Zhang study this phenomenon among bi-Cayley graphs, graphs equipped with a group acting freely on two vertex orbits. Their dihedral case supplies examples related to questions of Marušič and Potočnik about semisymmetric tetracirculants. It also asks how small the valency of a semisymmetric graph with this specific group action can be. The paper states that six is the minimum and that examples occur at every valency $2k$ with odd $k\ge3$ (Conder et al., Theorem 1.5 and its introduction, p. 3).

The authors develop the bi-Cayley setting and the relevant automorphism actions before reaching the dihedral result. The lower bound appears as Theorem 6.1, while Example 6.2 defines a graph family and Proposition 6.4 gives a semisymmetry criterion for its odd-$k$ members (Conder et al., pp. 11–13). This mission targets those claims within a single formal graph model. The final sentence of Theorem 1.5, concerning an edge-regular family, depends on the separate Theorem 6.5 and is outside this goal.

Setting

Let $H$ be a finite group. Choose subsets $R,L,S\subseteq H$ with $R^{-1}=R$, $L^{-1}=L$, $1\notin R\cup L$, and $|R|=|L|$. The graph $\operatorname{BiCay}(H,R,L,S)$ has two labelled copies of each element of $H$, written $h_0$ and $h_1$. For each $h\in H$, it joins $h_0$ to $(xh)_0$ when $x\in R$, joins $h_1$ to $(yh)_1$ when $y\in L$, and joins $h_0$ to $(zh)_1$ when $z\in S$. These are unoriented edges. Right multiplication by $H$ preserves the graph and acts regularly on each of its two vertex copies (Conder et al., pp. 1 and 4).

A bi-dihedrant is a bi-Cayley graph whose group is dihedral. Write $D_n=\langle a,b\mid a^n=b^2=(ab)^2=1\rangle$ for the dihedral group of degree $n\ge3$. Graph valency is the number of neighbours of a vertex. Connectedness is required throughout the paper. For a semisymmetric graph the common valency exists by definition, but the formal statements quantify over every vertex so that the numerical claims refer to the actual graph degree (Conder et al., definitions on p. 4 and Theorem 6.1 on p. 11).

The constructed family $\Gamma(n,\lambda,2k)$ uses $n\ge5$, $k\ge2$, and a residue $\lambda$ of multiplicative order $2k$ modulo $n$ whose even-power sum vanishes: $\sum_{j=0}^{k-1}\lambda^{2j}=0$. For $0\le i<k$, put $c_i=\sum_{j=0}^{i}\lambda^{2j}$ and $d_i=\lambda c_i$. Set $S(n,\lambda,2k)=\{a^{c_i}:0\le i<k\}\cup\{ba^{d_i}:0\le i<k\}$. Then $\Gamma(n,\lambda,2k)=\operatorname{BiCay}(D_n,\varnothing,\varnothing,S(n,\lambda,2k))$ (Conder et al., Example 6.2, pp. 12–13).

Right multiplication $R(g):h_i\mapsto(hg)_i$ gives a subgroup $R(H)\le\operatorname{Aut}(\Gamma)$, and $X=N_{\operatorname{Aut}(\Gamma)}(R(H))$ is its normaliser. For $\alpha\in\operatorname{Aut}(H)$ and $g,x,y\in H$ the paper's permutations are $\sigma_{\alpha,g}:h_0\mapsto(h^\alpha)_0,\ h_1\mapsto(gh^\alpha)_1$ and $\delta_{\alpha,x,y}:h_0\mapsto(xh^\alpha)_1,\ h_1\mapsto(yh^\alpha)_0$; the sets $\mathrm F$ and $\mathrm I$ of (2.2) collect those that preserve the edge rules. A graph is normal edge-transitive when $X$, not merely $\operatorname{Aut}(\Gamma)$, is transitive on edges (Conder et al., pp. 4–5).

Formalization targets

The milestones, in attack order, are Proposition 2.1(b) (one may assume $1\in S$), Proposition 2.2 (the normaliser $X=R(H)(\mathrm F\cup\mathrm I)$), the opening step of the proof of Theorem 6.1 ($R=L=\varnothing$ for a semisymmetric graph), Theorem 6.1, the claims of Example 6.2, and Proposition 6.4.

Minimum valency

For every connected semisymmetric bi-dihedrant over $D_n$, $n\ge3$, and every vertex $v$,

$$\deg_{\Gamma}(v)\ge6.$$

This is Theorem 6.1 and the first claim of Theorem 1.5. The milestone for the proof's opening step records that semisymmetry forces $R=L=\varnothing$; the theorem itself still ranges over all valid $R,L,S$ (Conder et al., Theorem 6.1, p. 11).

Examples at every odd index

For each odd integer $k\ge3$, there is a connected semisymmetric bi-dihedrant $\Gamma$ such that

$$\deg_{\Gamma}(v)=2k\qquad\text{for every vertex }v.$$

Example 6.2 is the first milestone toward this claim: under its hypotheses $\Gamma(n,\lambda,2k)$ is connected, $|S|=2k$, every vertex has degree $2k$, and $\sigma_{\alpha,b}$ for $\alpha:(a,b)\mapsto(a^\lambda,ba)$ lies in $X$ and permutes the neighbours of $1_0$ cyclically, so the graph is normal edge-transitive (Conder et al., p. 13). Proposition 6.4 is the second: under the defining conditions for $\Gamma(n,\lambda,2k)$, odd $k$ and $\lambda^k=-1$ modulo $n$ imply semisymmetry (Conder et al., Proposition 6.4, p. 13). An auxiliary arithmetic theorem states the parameter existence needed to apply it for every odd $k\ge3$.

Significance

The lower bound excludes semisymmetric bi-dihedrants of valency at most five. The existence assertion says that six is attained and places examples at an infinite sequence of larger valencies. Together these claims distinguish the restrictions imposed by a dihedral bi-Cayley action from edge transitivity alone. The construction also gives a concrete family on which questions about stronger automorphism properties can be posed (Conder et al., §6, pp. 11–14).

The result is proved in the cited paper; this mission seeks a machine-checked version of its first two Theorem 1.5 claims. The definition of a bi-Cayley graph, the precise graph symmetry predicates, and the arithmetic parameter family are reusable beyond this particular lower bound. The statements here are open proof targets in Lean, with their mathematical content fixed before proof development. The edge-regular claim from the theorem's final sentence requires additional source results and remains a separate formalization target.

Difficulty

Edge transitivity alone does not make a graph vertex-transitive: a semisymmetric graph is precisely the regular case where that inference fails. The lower bound therefore cannot be obtained by treating every vertex as lying in one automorphism orbit. In the dihedral case, the proof must account for both the rotations and reflections in the connection set, and for the constraints that connectedness and graph automorphisms impose on low-valency possibilities (Conder et al., proof of Theorem 6.1, pp. 11–12).

The existence statement has a distinct arithmetic requirement. Proposition 6.4 is conditional on $n,\lambda,k$ satisfying Example 6.2 and $\lambda^k=-1$. The paper asserts examples for every odd $k\ge3$ without spelling out parameters for all such $k$. The auxiliary arithmetic statement records that remaining obligation explicitly; a proof of the conditional proposition alone would not establish the quantified existence claim.

Formalization scope

Lean represents the two vertex copies by H ⊕ H and the dihedral group by Mathlib's DihedralGroup n. The graph is a SimpleGraph built from the three edge rules above, with the inverse-closure and loop-exclusion conditions retained in BiCayData. Semisymmetry uses the full graph automorphism group, unoriented edge transitivity, and constant graph degree. The source's standing finite, connected, simple, and undirected conventions are explicit through finite groups, simple graphs, and connectedness hypotheses. The goal and Theorem 6.1 use $n\ge3$, the range of dihedral groups in §6; the existence examples are also required to be connected.

The definitions do not set valency equal to $|S|$, replace a graph degree by a formula, or make an edge-transitivity claim true by ranging over an empty edge set. The setting requires valid inverse-closed side sets rather than silently symmetrising an invalid one. The arithmetic hypothesis uses the multiplicative order in $\mathbb Z/n\mathbb Z$ and enumerates the indices of $\mathbb Z_k$ by $0,\ldots,k-1$. Normal edge-transitivity in Example 6.2 is stated for the subgroup $X$ and semisymmetry for the full group $\operatorname{Aut}(\Gamma)$; the two are not interchanged. The restriction $n\ge3$ in the lower bound is that of Theorem 6.1 and is a disclosed hypothesis of the goal: $D_1$ and $D_2$ are abelian, and the paper treats bi-Cayley graphs over abelian groups separately. The auxiliary parameter statement is not in the paper; it is supplied so that the existence claim has a complete proof path. The third sentence of Theorem 1.5 is not formalized. Contributions establishing the structural lower bound, the family criterion, or the arithmetic existence statement are all within scope.

Selected references

• Marston Conder, Jin-Xin Zhou, Yan-Quan Feng and Mi-Mi Zhang, Edge-transitive bi-Cayley graphs, preprint arXiv:1606.04625v1, 2016; published in Journal of Combinatorial Theory, Series B, 2020. Preprint · DOI.

Motivation

A graph is symmetric when its automorphism group moves any vertex, edge or arc to any other, and $s$-arc-transitive when it moves any walk of length $s$ without immediate backtracking to any other. Tutte's work on cubic graphs made $s$-arc-transitivity a central measure of symmetry in algebraic graph theory, and most constructions of highly symmetric graphs start from a group acting regularly on vertices (Cayley graphs) or semiregularly with a few orbits.

Bi-Cayley graphs are the case of two orbits: a group $H$ acts semiregularly by right multiplication with exactly two vertex orbits. The Petersen graph, the Gray graph (the smallest cubic semisymmetric graph) and the smallest member of Bouwer's family of half-arc-transitive graphs are all bi-Cayley graphs, and all of them are edge-transitive. Deciding edge-transitivity of a bi-Cayley graph is hard in general, but the subgroup of automorphisms that normalise the semiregular group $R(H)$ is explicitly known, which makes the "normal" version of the question tractable.

C. H. Li asked whether 3-arc-transitive bi-normal Cayley graphs exist and asked for a description of the 2-arc-transitive ones (Li, Proc. Amer. Math. Soc. 133, Question 1.2(a) and Problem 1.3(b), as cited in the paper, p. 2). M. Conder, J.-X. Zhou, Y.-Q. Feng and M.-M. Zhang answered both through their Theorem 1.1 (arXiv:1606.04625v1; J. Combin. Theory Ser. B, 2020). This mission formalizes that theorem and the lemmas its proof uses.

Setting

Let $H$ be a finite group with identity $1$. Let $R, L, S \subseteq H$ with $|R| = |L|$, $1 \notin R = R^{-1}$ and $1 \notin L = L^{-1}$. The bi-Cayley graph $\Gamma = \mathrm{BiCay}(H,R,L,S)$ has vertex set $H_0 \cup H_1$, two disjoint copies of $H$ (the copy of $h$ in $H_i$ is $h_i$), and edges $\{h_0,(xh)_0\}$, $\{h_1,(yh)_1\}$ and $\{h_0,(zh)_1\}$ for $h \in H$, $x \in R$, $y \in L$, $z \in S$. The main theorem concerns $R = L = \emptyset$, where $\Gamma$ is bipartite with parts $H_0$, $H_1$ and every vertex has $|S|$ neighbours.

For $g \in H$, $R(g) : h_i \mapsto (hg)_i$ is an automorphism of $\Gamma$; these form the subgroup $R(H) \le \mathrm{Aut}(\Gamma)$, and

$$X = N_{\mathrm{Aut}(\Gamma)}(R(H))$$

is its normaliser. For $\alpha \in \mathrm{Aut}(H)$ (written as an exponent, $h \mapsto h^\alpha$) and $x, y, g \in H$ the paper defines the permutations

$$\delta_{\alpha,x,y} : h_0 \mapsto (xh^\alpha)_1,\ h_1 \mapsto (yh^\alpha)_0, \qquad \sigma_{\alpha,g} : h_0 \mapsto (h^\alpha)_0,\ h_1 \mapsto (gh^\alpha)_1,$$

and the sets $\mathrm{I}$ of those $\delta_{\alpha,x,y}$ with $R^\alpha = x^{-1}Lx$, $L^\alpha = y^{-1}Ry$, $S^\alpha = y^{-1}S^{-1}x$, and $\mathrm{F}$ of those $\sigma_{\alpha,g}$ with $R^\alpha = R$, $L^\alpha = g^{-1}Lg$, $S^\alpha = g^{-1}S$.

An $s$-arc is a sequence $(v_0,\dots,v_s)$ of vertices in which consecutive vertices are adjacent and $v_{i-1} \ne v_{i+1}$. A subgroup $K \le \mathrm{Aut}(\Gamma)$ is transitive on $s$-arcs if any $s$-arc can be mapped to any other by an element of $K$; 1-arcs are arcs. $\Gamma$ is normal edge-transitive if $X$ is transitive on edges, and normal locally arc-transitive if the stabiliser $X_{1_0}$ is transitive on the neighbourhood $\Gamma(1_0)$. $K$ acts semisymmetrically if it is edge-transitive but not vertex-transitive. $\mathrm{Aut}(H,\Delta)$ is the setwise stabiliser of $\Delta \subseteq H$ in $\mathrm{Aut}(H)$.

Formalization targets

Goal: Theorem 1.1

Let $\Gamma = \mathrm{BiCay}(H,\emptyset,\emptyset,S)$ be connected, with $1 \in S$ and $|S| \ge 2$. Then

$$X \text{ is transitive on the 2-arcs of } \Gamma \iff \text{(a)} \wedge \text{(b)} \wedge \text{(c)},$$

where (a) $S^\alpha = S^{-1}$ for some $\alpha \in \mathrm{Aut}(H)$; (b) $\mathrm{Aut}(H, S\setminus\{1\})$ is transitive on $S \setminus \{1\}$; (c) $S^\beta = s^{-1}S$ for some $s \in S\setminus\{1\}$ and $\beta \in \mathrm{Aut}(H)$. Furthermore, if $|S| \ge 3$, $X$ is not transitive on the 3-arcs of $\Gamma$.

Milestones

• Proposition 2.2 (cited by the paper from Zhou and Feng): for connected $\Gamma$, every element of $\mathrm{F}$ and of $\mathrm{I}$ is an automorphism in $X$, and $X = R(H)\,(\mathrm{F} \cup \mathrm{I})$.
• Proposition 2.2(a): for $\delta_{\alpha,x,y} \in \mathrm{I}$, $\langle R(H),\delta_{\alpha,x,y}\rangle$ is vertex-transitive.
• Lemma 3.2: $X_{1_01_1} = \{\sigma_{\alpha,1} \mid \alpha \in \mathrm{Aut}(H,S\setminus\{1\})\}$, and, for $|S| \ge 3$, $X$ is not 3-arc-transitive.
• Proposition 3.3: $\Gamma$ is normal locally arc-transitive iff $\Gamma(1_0)$ is an orbit of $\mathrm{F}$; in that case $X$ is arc-transitive iff $S^\alpha = S^{-1}$ for some $\alpha$, and semisymmetric otherwise.

A companion item, Lemma 3.1, shows that a connected normal edge-transitive $\mathrm{BiCay}(H,R,L,S)$ has $R = L = \emptyset$; it explains why the goal is stated for $\mathrm{BiCay}(H,\emptyset,\emptyset,S)$.

Significance

Combined with Lemma 3.1, Theorem 1.1 reduces 2-arc-transitivity of the normaliser of $R(H)$ to three conditions on $\mathrm{Aut}(H)$ and the single set $S$, all checkable in the group without building the graph. Its second part rules out normal 3-arc-transitive bi-Cayley graphs of valency at least 3, which settles Li's question on 3-arc-transitive bi-normal Cayley graphs negatively. Proposition 3.3 is the arc-transitive versus semisymmetric dichotomy for normal locally arc-transitive bi-Cayley graphs, the starting point of the paper's later constructions of semisymmetric and half-arc-transitive examples.

All results are proved in the paper (Proposition 2.2 by citation). None of them has a machine-checked proof that this mission knows of. Mathlib has simple graphs, graph isomorphisms and normalisers, but no bi-Cayley graphs, no $s$-arcs and no transitivity notions for subgroups of $\mathrm{Aut}(\Gamma)$. A formal proof would supply the first verified description of the normaliser of a semiregular group with two orbits, reusable for any bi-Cayley or bi-circulant result.

Difficulty

The bulk of the work is Proposition 2.2. That $\sigma_{\alpha,g}$ and $\delta_{\alpha,x,y}$ preserve edges exactly under the conditions of (2.2) is a direct computation. The converse is harder: every automorphism normalising $R(H)$ must be one of these permutations composed with some $R(h)$. That needs the conjugation action of $X$ on $R(H)$ to induce an automorphism of $H$, and $X$ to preserve the partition $\{H_0, H_1\}$ into $R(H)$-orbits.

The 3-arc clause looks like a stabiliser count, but it holds only once $1_1$ has at least two neighbours besides $1_0$: for $|S| = 2$ the graph is a cycle of length $2|H|$, the normaliser is the whole dihedral automorphism group, and that group is transitive on 3-arcs. Any proof must use $|S| \ge 3$ at exactly this step.

Formalization scope

The vertex set is H ⊕ H (Sum.inl h $= h_0$, Sum.inr h $= h_1$). The data $(R, L, S)$ is a structure of three Finsets carrying the side conditions $R^{-1} = R$, $L^{-1} = L$, $1 \notin R$, $1 \notin L$ and $|R| = |L|$. Adjacency is given directly by the three edge rules. $\mathrm{Aut}(\Gamma)$ is the group Γ ≃g Γ, $R(H)$ is the subgroup generated by the $R(g)$, and $X$ is its Subgroup.normalizer. Automorphisms of $H$ are MulAut H, and $\Delta^\alpha$ is the image of $\Delta$ under $\alpha$. $\sigma_{\alpha,g}$ and $\delta_{\alpha,x,y}$ are permutations of H ⊕ H, and "$\sigma_{\alpha,g} \in X$" means that some element of $X$ has $\sigma_{\alpha,g}$ as its vertex map. Products are written pointwise to avoid the composition-order convention of the group of graph automorphisms. An $s$-arc is a function on Fin (s+1).

The paper assumes throughout that groups and graphs are finite and graphs connected; each theorem carries Fintype H and connectivity. Three hypotheses are added to the printed Theorem 1.1, each needed for the statement to be true or non-vacuous: $1 \in S$ (the paper's normalisation of a bi-Cayley triple, used by conditions (b) and (c) and by the proof); $|S| \ge 2$ (for $|S| = 1$ the graph is $K_2$, which has no 2-arcs, so 2-arc-transitivity would hold vacuously while (c) fails); and $|S| \ge 3$ for the 3-arc clause (false for cycles). Lemma 3.2 carries the same $1 \in S$ and $|S| \ge 3$, and Proposition 3.3 carries $1 \in S$.

Trivializing formalizations are ruled out in four ways. 2-arc-transitivity is never vacuous, since $|S| \ge 2$ guarantees 2-arcs. $R$ and $L$ are never symmetrised silently, since the side conditions are data rather than repairs. Every transitivity statement is about $X$, not the full $\mathrm{Aut}(\Gamma)$. Valency is the degree in the graph, never a formula in $|S|$.

Contributions are welcome at every level: proofs of the milestones, a general library of bi-Cayley graphs and their normalisers, and lemmas on $s$-arcs and stabilisers in SimpleGraph. The definitions are repeated identically in the companion missions on bi-abelian graphs and bi-dihedrants.

Selected references

• M. Conder, J.-X. Zhou, Y.-Q. Feng and M.-M. Zhang, Edge-transitive bi-Cayley graphs, arXiv:1606.04625v1, 2016; J. Combin. Theory Ser. B, 2020. https://arxiv.org/abs/1606.04625v1, https://doi.org/10.1016/j.jctb.2020.05.006
• J.-X. Zhou and Y.-Q. Feng, The automorphisms of bi-Cayley graphs, J. Combin. Theory Ser. B 116 (2016) 504–532 (reference [55] of the paper; source of Proposition 2.2). https://doi.org/10.1016/j.jctb.2015.10.004
• C. H. Li, Finite s-arc transitive Cayley graphs and flag transitive projective planes, Proc. Amer. Math. Soc. 133 (2005) 31–41 (reference [29] of the paper; Question 1.2(a) and Problem 1.3(b)). https://doi.org/10.1090/S0002-9939-04-07549-5

Why bi-Cayley graphs over abelian groups matter

A Cayley graph turns multiplication in a group into adjacency between vertices. Every Cayley graph is vertex transitive: multiplying every vertex by the same group element moves any chosen vertex to any other. A bi-Cayley graph starts with two copies of a group and permits edges both within and between the copies. Its built-in group action is transitive on each copy, but it need not exchange them. This makes bi-Cayley graphs a setting for distinguishing edge, vertex, and arc transitivity. Conder, Zhou, Feng and Zhang study these distinctions and their consequences for graph constructions in Edge-transitive bi-Cayley graphs.

For abelian groups, the paper proves a strong restriction: once a connected bi-Cayley graph is edge transitive, it is also vertex transitive. Its half-arc-transitive examples face additional local restrictions, including a minimum valency of six. The paper exhibits a graph of valency six in Example 4.3, so the numerical bound is attained in its class. The result separates these graphs from semisymmetric graphs, which are edge transitive but not vertex transitive. The claims and example appear in Proposition 1.3 and §4.

Graphs, actions, and terminology

Let $H$ be a finite group and let $R,L,S$ be subsets of $H$. Require $R=R^{-1}$, $L=L^{-1}$, $1\notin R\cup L$, and $|R|=|L|$. The graph $\Gamma=\operatorname{BiCay}(H,R,L,S)$ has vertices $H_0\cup H_1$, two labelled copies of $H$. For $h\in H$, an element $x\in R$ gives an edge from $h_0$ to $(xh)_0$; an element $y\in L$ gives an edge from $h_1$ to $(yh)_1$; and an element $z\in S$ gives an edge from $h_0$ to $(zh)_1$. The inverse closure of $R$ and $L$ makes the within-copy edges undirected. Excluding $1$ from those two sets excludes loops. This is the construction on p. 1.

Every $g\in H$ acts by right multiplication $R(g):h_i\mapsto(hg)_i$. The subgroup $R(H)$ of graph automorphisms has two vertex orbits, $H_0$ and $H_1$. Its normaliser in $\operatorname{Aut}(\Gamma)$ is useful for describing further symmetries. For a group automorphism $\alpha$ and group elements $g,x,y$, the paper defines permutations $\sigma_{\alpha,g}$, which preserve the two copies, and $\delta_{\alpha,x,y}$, which exchange them. Their precise edge-preservation conditions are the sets $F$ and $I$ of equation (2.2). The mission includes those definitions and the relevant part of the normaliser characterization, Proposition 2.2.

A graph is vertex transitive if its full automorphism group can move any vertex to any other, and edge transitive if it can move any undirected edge to any other. Arc transitivity asks the same for ordered adjacent pairs. A graph is half-arc-transitive when it is vertex and edge transitive but not arc transitive. A semisymmetric graph has constant valency, is edge transitive, and is not vertex transitive. These are the paper's definitions on p. 4. Valency means the actual number of neighbours of a vertex.

Formalization targets

The central target is the corrected reading of Proposition 1.3: for connected $\Gamma$ over an abelian $H$,

$$\Gamma\text{ edge transitive}\implies\Gamma\text{ vertex transitive},$$

and, if $\Gamma$ is half-arc-transitive,

$$R\cup L\ne\varnothing,\quad (\forall x\in R\cup L)\ \operatorname{ord}(x)\ne2, \quad |R|=|L|\text{ is even},\quad |S|>2,\quad \deg_{\Gamma}(v)\ge6\quad(v\in V(\Gamma)).$$

The attack path records the normaliser characterization in Proposition 2.2, both parts of Proposition 4.1, its explicit bipartition step, and Proposition 4.2. The companion Corollary 4.4 expresses the absence of connected semisymmetric examples over abelian groups.

What the result establishes

The vertex-transitivity conclusion collapses one apparent possibility in the symmetry classification: an edge-transitive bi-Cayley graph over an abelian group cannot be semisymmetric. For half-arc-transitive graphs, the theorem rules out involutions in the within-copy connection sets, forces even set sizes, and excludes valencies below six. Example 4.3 supplies an attained bound, with $H=C_{28}$ and valency six. These are concrete restrictions on any later classification or construction in this family; they follow from §4.

The mathematical results are proved in the cited paper. The mission asks for machine-checked Lean proofs of their statements and for a reusable finite bi-Cayley graph interface. The setting includes the right regular action, its normaliser, the two families of candidate automorphisms, and the transitivity predicates. The proof obligations are open in this local proposal; a successful development would make the abelian argument and its underlying graph-action lemmas available for later formalizations of bi-Cayley graphs.

The main obstacle

The right multiplication action gives only two known vertex orbits, one for each copy of $H$. Edge transitivity alone does not name an automorphism that swaps them. Inversion is an automorphism of an abelian group, but its induced copy-swapping permutation preserves graph edges directly only in the relevant bipartite case $R=L=\varnothing$. The paper must account for edge-transitive graphs whose connection sets initially allow edges inside the copies. For the valency bound, the absence of arc transitivity restricts how a vertex stabiliser can permute its neighbours; degree counting without those orbit constraints cannot yield $|S|>2$. These are the points at which a proof must use the full automorphism action rather than just the visible right regular subgroup.

Formalization scope

Lean uses the vertex type $H\sqcup H$, with Sum.inl h for $h_0$ and Sum.inr h for $h_1$. The group and graph are finite; the graph is simple and undirected by construction, and every theorem assumes it is connected. The finite sets $R,L,S$ retain the conditions $R=R^{-1}$, $L=L^{-1}$, $1\notin R\cup L$, and $|R|=|L|$. The graph's degree, rather than a separately defined cardinality formula, represents valency. “Involution” means an element of order exactly two. All graph-level transitivity predicates quantify over the full automorphism group; the normaliser appears only in the separate Proposition 2.2 milestone. The paper's exponent notation for group automorphisms is rendered as function application, while $R(g)$ remains right multiplication.

The printed first sentence of Proposition 1.3 says every connected bi-Cayley graph over an abelian group is vertex transitive. That sentence is false: the connected generalized Petersen graph $GP(7,2)$ is a bi-Cayley graph over $C_7$ and is not vertex transitive. Proposition 4.1(b), which the paper uses to establish Proposition 1.3, includes the missing edge-transitivity condition. The Lean goal states that corrected condition explicitly. It does not add an assumption to the half-arc-transitive clause, since half-arc-transitivity already entails edge transitivity. Proposition 4.2 prints two clauses labelled “(a)”; they are treated as distinct clauses while its quotation retains the printed labels.

The definition of the graph keeps $R$ and $L$ inverse closed as data; no graph constructor silently symmetrises arbitrary sets. Transitivity is taken over actual edges or arcs, and the degree bound is checked at every vertex. Contributions to the graph-action lemmas, the normaliser result, Proposition 4.1, and the vertex-stabiliser analysis behind Proposition 4.2 are all within scope. The Cayley-graph isomorphism in Proposition 2.2(b) is outside this mission's stated milestone because it is not used by the target.

Selected references

• M. Conder, J.-X. Zhou, Y.-Q. Feng, and M.-M. Zhang, Edge-transitive bi-Cayley graphs, Journal of Combinatorial Theory, Series B, 2020; arXiv:1606.04625v1; DOI:10.1016/j.jctb.2020.05.006.