Combinatorics

Motivation

In online selection, useful items arrive one at a time and must be accepted or rejected before the next arrival. A knapsack constraint limits the total size of accepted items to one unit. When the order may depend on all of the random outcomes, an algorithm needs a guarantee that survives every such order. Feldman, Svensson, and Zenklusen introduced online contention resolution schemes (OCRSs) to provide this guarantee for fractional relaxations of selection problems. Their knapsack theorem gives an explicit guarantee for a randomized greedy scheme and contrasts with a size-dependent obstruction for deterministic greedy schemes (Feldman–Svensson–Zenklusen, §2.3).

The knapsack result is one of the three concrete existence results summarized in Theorem 1.8 of the paper. The surrounding framework is designed to convert fractional solutions into feasible online selections under an almighty adversary, who knows the active items and the scheme's random choices before choosing their arrival order. This makes the selectability requirement stronger than a performance claim for one fixed order (Feldman–Svensson–Zenklusen, Definitions 1.3–1.5).

Setting

Let $N$ be a finite ground set. Each element $e\in N$ has a size $s_e\in[0,1]$. A subset $I\subseteq N$ is feasible when its total size is at most one. The natural fractional polytope is

$$P=\left\{x\in[0,1]^N:\sum_{e\in N}s_ex_e\le1\right\}.$$

For a vector $x\in[0,1]^N$, the random active set $R(x)$ includes each element $e$ independently with probability $x_e$. A greedy family $F_x$ is a downward-closed family of feasible subsets. The online rule accepts an active arriving element when adding it to the accepted set keeps that set inside $F_x$. A randomized greedy OCRS chooses the family at random, independently of $R(x)$. The paper studies the probability that an element $e$ is selectable: for every possible accepted set $I\subseteq R(x)$ with $I\in F_x$, the enlarged set $I\cup\{e\}$ still belongs to $F_x$. Such an event makes $e$ acceptable regardless of the arrival order (Feldman–Svensson–Zenklusen, §1.1).

Write $bP=\{bp:p\in P\}$. An OCRS is $(b,c)$-selectable when, for every $x\in bP$ and every $e\in N$, the probability that $e$ is selectable is at least $c$. The paper divides elements at size $1/2$: $N_{\mathrm{big}}=\{e:s_e>1/2\}$, while equality belongs to the small elements. Its construction randomly chooses between the feasible subsets using only big elements and those using only small elements (Feldman–Svensson–Zenklusen, proof of Theorem 2.9).

Formalization targets

Main theorem

Theorem 2.9 asserts that for every $b\in[0,1/2]$ and every such knapsack polytope, a randomized greedy OCRS exists with

$$c=\frac{1-2b}{2-2b}.$$

The goal quantifies over every finite ground set and every allowed size vector. At the endpoint $b=1/2$, the claimed lower bound is zero; at $b=0$, it is $1/2$. The denominator remains positive throughout the stated interval. The goal is an existence statement; its witnesses are arbitrary randomized greedy families meeting the definition, so the paper's particular construction is named separately in the supporting definitions (Feldman–Svensson–Zenklusen, Theorem 2.9, p. 14).

Supporting targets

The milestones include the paper's bound $0\le b_{\mathrm{big}}\le b$ for $b_{\mathrm{big}}=\sum_{e\in N_{\mathrm{big}}}s_ex_e$, the big and small element selectability bounds for the paper's construction, and Proposition 2.8. That proposition says that, for every ground-set size $n\ge1$, some knapsack constraint defeats every deterministic greedy OCRS whenever $c>(1-b)^{n-1}$ for $b\in[0,1]$ (Feldman–Svensson–Zenklusen, §2.3, pp. 14–15).

Significance

The theorem supplies a concrete selectable OCRS for the natural fractional knapsack relaxation. Its guarantee applies to every element and every fractional point in $bP$, under the paper's strongest arrival-order adversary. Proposition 2.8 explains why randomization matters here: a deterministic greedy scheme cannot retain an analogous positive constant independent of the number of elements on every knapsack instance. These results serve as the knapsack component in the paper's broader OCRS framework and can be combined with schemes for other constraints in the paper's later combination result (Feldman–Svensson–Zenklusen, Theorem 1.9).

The mathematical theorem and proposition have proofs in the cited paper. This mission asks for machine-checked proofs of their formal statements and of the stated intermediate bounds. The current draft declarations contain proof placeholders; compilation establishes only that their statements and definitions are well formed. A completed development would also leave reusable finite active-set probabilities, greedy-family predicates, and explicit knapsack constructions for later online-rounding work.

Difficulty

A family that contains every feasible subset is not automatically useful for online selection: one active set may contain several subsets whose accepted elements block the tested element. The requirement quantifies over every feasible accepted subset of the realized active set, reflecting the almighty adversary rather than a fixed order. In a knapsack, elements larger than one half behave differently from smaller ones, and a single deterministic family cannot give a ground-set-independent selectability guarantee on all instances. The randomized construction must assign valid probabilities to its two families and obtain the same lower bound in both size regimes (Feldman–Svensson–Zenklusen, Proposition 2.8 and Theorem 2.9).

Formalization scope

The Lean ground set is a finite type, and subsets are Finsets. The polytope is the set of real vectors satisfying both the box inequalities and the unit-capacity inequality. The feasible family uses the same sizes and unit capacity. Active-set and family-choice probabilities are finite sums, with independent Bernoulli factors for $R(x)$. The scaling $bP$ is pointwise set scalar multiplication, so the case $b=0$ retains its intended meaning. The size assumptions $s_e\in[0,1]$ and the ranges of $b$ are explicit theorem hypotheses. No nonemptiness assumption is added to the ground set; the statements include the empty case.

The greedy-family definition requires the empty set, making it impossible to satisfy selectability by using an empty family. Every family chosen with positive probability is downward closed and consists of feasible sets. The polytope's box constraints keep every active-set weight a probability. The construction's mixing probability is used exactly on $x\in bP$; on other vectors its totalized value chooses the small family, where the paper makes no performance claim. The two branch weights are added if their families coincide, as they can on an empty ground set.

One display on page 15 includes the tested element in a load sum, while the next displayed equality treats that element as excluded. The pointwise supporting item uses the excluded-element form needed for the stated argument; the printed display is preserved in the milestone quotation and the discrepancy is detailed in MODERATION_NOTES.md. Contributions toward either size regime, the finite probability bounds, or the deterministic obstruction are welcome. The finite probability and greedy-family definitions are the parts most directly reusable beyond knapsack.

Selected references

• Moran Feldman, Ola Svensson, and Rico Zenklusen, Online Contention Resolution Schemes, arXiv:1508.00142v2, 2015, §1.1 and §2.3, pp. 2–4 and 14–15. arXiv.

Motivation

Social networks exhibit triadic closure: two people with a common friend are more likely to be friends themselves than two people chosen at random, and the more common friends they have, the more likely they are to be connected. The principle goes back to sociology (Granovetter 1973) and is documented on large network data sets (see the Enron e-mail graph in Figure 1 of Fox, Roughgarden, Seshadhri, Wei and Wein).

A common computational task on such networks is to list all maximal cliques, the groups of mutually connected vertices that cannot be enlarged. On an arbitrary graph this is hopeless in the worst case: Moon and Moser showed in 1965 that an $n$-vertex graph can have $3^{n/3}$ maximal cliques, and that no graph has more (Moon and Moser 1965). Yet clique enumeration on real social networks runs quickly. Fox, Roughgarden, Seshadhri, Wei and Wein proposed a distribution-free graph class, defined by a coarse form of triadic closure, on which the worst case is provably polynomial. This mission formalizes their first bound, for the class of weakly $c$-closed graphs (Theorem 2.2 of the paper, also stated as Theorem 1.5), together with the peeling argument that proves it.

Setting

All graphs are finite, simple and undirected. For a graph $G$ with vertex set $V$ and a vertex $v$, $N(v)$ is the set of neighbours of $v$; for $W \subseteq V$, $G[W]$ is the subgraph induced by $W$. The common neighbours of two vertices $u, v$ are the vertices of $N(u) \cap N(v)$.

• $c$-closed graph (Definition 1.1). For a positive integer $c$, $G$ is $c$-closed if every two distinct vertices with at least $c$ common neighbours are adjacent. A 1-closed graph is a disjoint union of cliques; every graph on $n$ vertices is $(n-1)$-closed.
• Bad pair (Definition 1.2). Given $c$, a bad pair of a graph is a pair of distinct, non-adjacent vertices with at least $c$ common neighbours. A graph is $c$-closed exactly when it has no bad pair.
• Weakly $c$-closed graph (Definition 1.3). A graph on $n$ vertices is weakly $c$-closed if its vertices can be ordered $v_1, \dots, v_n$ so that for every $i$, the vertex $v_i$ is in no bad pair of the induced subgraph $G[\{v_i, v_{i+1}, \dots, v_n\}]$. Common neighbours are counted inside that subgraph.
• Maximal clique. A clique is a set of pairwise adjacent vertices. It is maximal if no other vertex can be added to it. Write $\mathrm{mc}(G)$ for the number of maximal cliques of $G$ and $\mathrm{mc}(G[W])$ for that of an induced subgraph. The paper writes $F(n,c)$ for the largest value of $\mathrm{mc}(G)$ over $c$-closed graphs $G$ on $n$ vertices.

Every $c$-closed graph is weakly $c$-closed, but not conversely. The paper's example: a clique on $k$ vertices with one edge $\{u,v\}$ removed is not $c$-closed for any $c < k-2$, but it is weakly 1-closed (order $u$ and $v$ last).

In the Lean development these objects are IsCClosed, IsBadPairIn, IsWeaklyCClosed, maxCliquesIn, numMaxCliquesIn and numMaxCliques, in the namespace CClosedGraphs.Peeling.

Formalization targets

Goal: Theorem 2.2

For all positive integers $c$ and $n$, every weakly $c$-closed graph $G$ on $n$ vertices satisfies

$$\mathrm{mc}(G) \le 3^{(c-1)/3}\, n^2 .$$

Milestones

The milestones follow the proof of Theorem 2.1 in §2.1 and the remark that extends it to Theorem 2.2. Fix a graph, an induced subgraph $G[W]$ and a vertex $v \in W$. A maximal clique $K$ of $G[W]$ is of type 1 if $v \notin K$, of type 2 if $v \in K$ and $K \setminus \{v\}$ is maximal in $G[W \setminus \{v\}]$, and of type 3 otherwise.

1. Moon–Moser bound (cited as [45], p. 7): $\mathrm{mc}(G[W]) \le 3^{|W|/3}$.
2. Types 1 and 2 (p. 6): there are at most $\mathrm{mc}(G[W \setminus \{v\}])$ of them.
3. Type-3 structure (p. 7, properties A–C): for a type-3 clique $K$ there is $u \in W \setminus (N(v) \cup \{v\})$ such that $K \setminus \{v\}$ is a maximal clique of $G[W \cap N(v) \cap N(u)]$.
4. Inequality (1) (p. 7): the number of type-3 cliques is at most $\sum_{u \in W \setminus (N(v)\cup\{v\})} \mathrm{mc}(G[W \cap N(u) \cap N(v)])$.
5. One-vertex recursion (pp. 7–8): if $v$ is in no bad pair of $G[W]$, then $\mathrm{mc}(G[W]) \le \mathrm{mc}(G[W \setminus \{v\}]) + 3^{(c-1)/3}|W|$.
6. Theorem 2.1 (p. 6): every $c$-closed graph on $n \ge 1$ vertices has $\mathrm{mc}(G) \le 3^{(c-1)/3} n^2$.

Significance

For fixed $c$, the theorem makes the number of maximal cliques of a weakly $c$-closed graph polynomial in $n$, against $3^{n/3}$ for general graphs. Since all maximal cliques can be listed in polynomial time per clique, this makes maximal-clique enumeration fixed-parameter tractable in $c$ on the class. The paper's Theorem 2.3 turns the proof into an enumeration algorithm. Weak $c$-closure is the version that matters in practice: Table 1 of the paper reports social networks with thousands of vertices that are weakly $c$-closed for modest $c$ while being $c$-closed only for much larger $c$. The bound is the starting point of the paper's sharper Theorem 3.1 ($4^{(c+4)(c-1)/2} n^{2-2^{1-c}}$) and its lower bound Theorem 4.1, which are separate missions of this series.

The result is proved in the paper, and the proof is short. No machine-checked proof of it or of the Moon–Moser bound exists in Mathlib at the pinned revision or on Prove2Me. This mission produces both, together with a reusable vocabulary for counting maximal cliques of induced subgraphs. Proofs of the sharp Moon–Moser values, or of the sharper $|W|-1$ in the recursion, are welcome as further contributions but are not milestones.

Difficulty

The counting argument is elementary. The work lies in two places. First, the Moon–Moser bound $3^{k/3}$ is not in Mathlib and needs its own proof, and its exponential bound must be handled with real powers. Second, the type decomposition must be handled exactly: a type-3 clique $K$ is charged to a pair $(u, K \setminus \{v\})$, and the charge has to be injective while $u$ ranges over all vertices outside $N(v) \cup \{v\}$. The degenerate cases are real. When $v$ is isolated in $G[W]$ and $W \ne \{v\}$, the clique $\{v\}$ is of type 3 and $K \setminus \{v\} = \varnothing$. The peeling for weakly $c$-closed graphs must also follow the given vertex ordering, with closure checked in the shrinking induced subgraphs rather than in $G$.

Formalization scope

• Graphs on $n$ vertices are SimpleGraph (Fin n). Auxiliary statements are generic over a finite type with decidable equality.
• The weakly closed ordering is a permutation $\sigma$ of Fin n with $v_i = \sigma(i)$. The set $\{v_i, \dots, v_n\}$ is $\{x : i \le \sigma^{-1}(x)\}$.
• Common-neighbour counts are Set.ncard, which is exact on a finite type. "At least $c$" is $c \le |\cdot|$, not $c < |\cdot|$.
• Maximal cliques of $G[W]$ are counted as finite vertex sets $K \subseteq W$ of the ambient type that are maximal among cliques contained in $W$. Removing $v$ from the current graph $G[W]$ is $G[W \setminus \{v\}]$, and $G[N(v) \cap N(u)]$ is $G[W \cap N(v) \cap N(u)]$.
• All bounds are real numbers: $3^{(c-1)/3}$ and $3^{|W|/3}$ are real powers.
• The hypotheses $c \ge 1$ and $n \ge 1$ are on the page. The second is needed, since the graph with no vertices has one maximal clique, the empty one.
• No hypothesis is added relative to the paper. In property C, "$u \notin N(v)$" is read as $u \notin N(v) \cup \{v\}$, as in Figure 2 and in (1).
• The paper's $F(\cdot, c)$ is a maximum over graphs. The milestones use the actual count of the relevant induced subgraph instead, which is at most $F$; the goals bound the count for every graph in the class, which is the same content.

Three trivializing readings are ruled out. The count is of maximal cliques, not of all cliques or of cliques of a given size. A bad pair needs at least $c$ common neighbours, not more than $c$. In the weakly closed definition, common neighbours are counted inside $\{v_i, \dots, v_n\}$, not in $G$; counting them in $G$ would make the hypothesis stronger and the theorem weaker.

A complete development needs a Moon–Moser lemma for induced subgraphs, the injections behind milestones 2 and 4, and a peeling induction over a vertex ordering. The first two are reusable for any maximal-clique counting argument. The induced-subgraph counts numMaxCliquesIn are also used by the later missions of this series, which repeat the definitions in their own namespaces.

Selected references

• J. Fox, T. Roughgarden, C. Seshadhri, F. Wei, N. Wein, Finding cliques in social networks: a new distribution-free model, arXiv:1804.07431v1, 2018; SIAM Journal on Computing 49(2), 2020. https://arxiv.org/abs/1804.07431v1, https://doi.org/10.1137/18M1210459
• J. W. Moon, L. Moser, On cliques in graphs, Israel Journal of Mathematics 3, 23–28, 1965. https://doi.org/10.1007/BF02760024
• M. S. Granovetter, The strength of weak ties, American Journal of Sociology 78(6), 1360–1380, 1973. https://doi.org/10.1086/225469
• E. Tomita, A. Tanaka, H. Takahashi, The worst-case time complexity for generating all maximal cliques and computational experiments, Theoretical Computer Science 363(1), 28–42, 2006. https://doi.org/10.1016/j.tcs.2006.06.015

Motivation

In online selection, items reveal information one at a time, and each decision to accept an item is irrevocable. A matroid constraint permits some subsets and excludes others; it covers choices such as selecting linearly independent vectors or acyclic edges. A fractional solution can assign an acceptance probability to each item, but independent activations can produce a set that violates the constraint. An online contention resolution scheme (OCRS) turns these activations into a feasible selection while respecting the order in which items arrive. The matroid result of Feldman, Svensson and Zenklusen gives a guarantee that survives even when an adversary knows all random outcomes before choosing the arrival order.

This mission concerns the paper's matroid theorem, Theorem 2.1. The same paper develops schemes for matching and knapsack constraints and a rule for combining schemes for intersecting constraints. Those results are separate missions in this series. Here the central question is how much of a fractional matroid point can be retained by a deterministic greedy rule as each active item is revealed.

Setting

Let $N$ be a finite ground set and let $M$ be a matroid on $N$. Its independent subsets form a down-closed family $\mathcal F$: if $I$ is independent, every subset of $I$ is independent. The rank $r(S)$ of $S\subseteq N$ is the maximum size of an independent subset of $S$. The matroid independence polytope is

$$P_{\mathcal F}=\left\{x\in\mathbb R^N_{\ge0}:x(S):=\sum_{e\in S}x_e\le r(S)\text{ for all }S\subseteq N\right\}.$$

Its points have $0\le x_e\le1$. For a point $x$, the active set $R(x)$ contains each $e$ independently with probability $x_e$. A deterministic greedy OCRS assigns a down-closed family $\mathcal F_x\subseteq\mathcal F$ to $x$ and accepts an active element when adding it to the already accepted set stays in $\mathcal F_x$. The empty set belongs to every $\mathcal F_x$. The rule depends on $x$ before the active set and arrival order are revealed.

An element $e$ is selectable for an active set $A$ if $I\cup\{e\}\in\mathcal F_x$ for every $I\subseteq A$ with $I\in\mathcal F_x$. A greedy OCRS is $(b,c)$-selectable if this event has probability at least $c$ for every $x\in bP_{\mathcal F}$ and every $e\in N$. The event implies that $e$ can be added regardless of which eligible active elements arrived first. These definitions are from §1.1 of the paper.

Formalization targets

Matroid OCRS

For every $b\in[0,1]$ and every finite loopless matroid $M$, the target is a deterministic greedy OCRS with

$$\Pr\left[I\cup\{e\}\in\mathcal F_x\text{ for all }I\subseteq R(x),\ I\in\mathcal F_x\right]\ge 1-b \quad\text{for every }x\in bP_{\mathcal F},\ e\in N.$$

The loopless condition is a disclosed correction to the printed Theorem 2.1: a loop cannot belong to any independent singleton, so its selectability is zero. The printed bound would demand positive selectability for that loop whenever $b<1$. The theorem keeps the paper's constant $1-b$ exactly.

Supporting targets

The milestones reproduce six statements from §2.1–2.1.1, in attack order: validity of a family defined by a chain $\varnothing=N_\ell\subsetneq\cdots\subsetneq N_0=N$ of matroid minors (independence of the union of layer-wise independent sets is Soto, Theorem 5.1); a characterization of selectability through span in one layer; monotonicity of the first chain set as coordinates of $x$ increase; the description of the base polytope $P_{\mathcal B}=\{x\in P_{\mathcal F}:x(N)=r(N)\}$ as the set of maximal vectors of $P_{\mathcal F}$; the weighted span bound of Lemma 2.4,

$$\sum_{e\in N}x_e\Pr[e\in\operatorname{span}(R(x)\cup S)]\le b\cdot\bigl(x(N)+(1-b)\,r(S)\bigr),$$

strict when $S\neq\varnothing$; and the proper-inclusion conclusion $S\subsetneq N$ of Corollary 2.5. They expose the distinct matroid and probability claims on which the main theorem rests.

Significance

The theorem gives a fixed greedy family for each fractional point, with a per-element probability guarantee that is independent of the arrival order. Offline contention resolution schemes for matroids were introduced by Chekuri, Vondrák and Zenklusen; the online, almighty-adversary version here is stronger. A solver can use that guarantee as the matroid component in larger online selection problems. In the source paper it feeds the intersection and application results; those applications require further models and statements beyond this mission. The factor $1-b$ makes the tradeoff explicit: using a more heavily scaled fractional point raises the risk of contention.

The result is proved in the cited paper. This mission asks for a machine-checked Lean proof of its corrected statement and the source's supporting claims. A successful development would add reusable finite representations of independent activation, matroid polytope inequalities, span probabilities, and chain families. It would also make the loop boundary explicit, preventing a formally false version of the printed theorem from being published as a target.

Difficulty

Independent activation does not itself respect matroid independence. A greedy family that simply contains every independent set can make an element unavailable after earlier active elements are accepted, and the arrival order can expose the worst such history. The central issue is therefore a uniform selectability event: the same element must remain addable after every feasible subset of the active set. The paper measures that obstruction through spans in successive matroid minors. The first chain set must be proper so that the construction can continue, which is why the strict part of the weighted span inequality matters.

Formalization scope

The ground set is a finite Lean type, subsets are Finsets, and Mathlib's Matroid supplies independence, closure, contraction and restriction. Matroid rank is converted from Mathlib's extended natural rank to a real number; finiteness makes this conversion finite on every subset. The independence and base polytopes are defined by the paper's inequalities. The scalar multiple $bP$ is pointwise set scalar multiplication, including $b=0$.

Probabilities are finite sums of product weights over all active sets. In particular, the event in Lemma 2.4 uses $\operatorname{span}(R(x)\cup S)$, whereas the recurrence defining $S$ uses $\operatorname{span}((R(x)\cup S_i)\setminus\{e\})$. These are separate definitions. Every point used for activation lies in $[0,1]^N$, as enforced by the polytope and $b\in[0,1]$. The base-polytope condition on Corollary 2.5 is the standing assumption stated before the lemma in the source.

The loopless condition applies to the goal, to Corollary 2.5, and to the strict clause of Lemma 2.4 only; its non-strict clause, the chain statements and the monotonicity statement hold for every matroid and are stated without it. Three trivializing formalizations are ruled out: every greedy family must contain the empty set, so an empty family cannot satisfy selectability vacuously; every member of a greedy family must be independent in $M$, so $\mathcal F_x=2^N$ is not admissible; and every point used for activation lies in $[0,1]^N$, so $\Pr[R(x)=A]$ is a genuine probability. The quantified scheme depends only on $x$, and its success condition ranges over every feasible subset of the realized active set. Contributions that establish the chain family's independence, finite probability identities, and rank or closure facts are within scope. Polynomial-time implementation and the Monte Carlo estimates of Lemma 2.6 are outside this mission's mathematical target.

Selected references

• Moran Feldman, Ola Svensson and Rico Zenklusen, Online Contention Resolution Schemes, arXiv:1508.00142v2, 2015; published as Online Contention Resolution Schemes with Applications to Bayesian Selection Problems, SIAM Journal on Computing, 2021. Preprint.
• Chandra Chekuri, Jan Vondrák and Rico Zenklusen, Submodular Function Maximization via the Multilinear Relaxation and Contention Resolution Schemes, SIAM Journal on Computing, 2014. arXiv:1105.4593.
• José A. Soto, Matroid Secretary Problem in the Random-Assignment Model, SIAM Journal on Computing, 2013. arXiv:1007.2140.

Motivation

Hypergraph Turán problems ask how many edges a $k$-uniform hypergraph on $n$ vertices can have without containing a fixed sub-hypergraph. For graphs ($k=2$) the theory is well developed; for $k\ge 3$ exact answers are rare and are known mostly for small, dense configurations such as the Fano plane or expanded triangles. Paths are the natural sparse test case. For graphs, Erdős and Gallai (1959) showed that a graph on $n$ vertices without a path of length $\ell$ has at most $\frac12(\ell-1)n$ edges. For hypergraphs there are several notions of path: Berge paths (Győri, Katona and Lemons, 2010), loose paths (Mubayi and Verstraëte, 2007, asymptotic bounds) and the most restrictive notion, linear paths. The case of two edges was solved by Frankl (1977), and the case $\ell<k$ asymptotically by Frankl and Füredi (1987).

Füredi, Jiang and Seiver (arXiv:1108.1247v1, published in Combinatorica 34 (2014), doi:10.1007/s00493-014-2838-4) determined the Turán number of every $k$-uniform linear path exactly, for $k\ge4$ and $n$ large, together with the unique extremal families. It is one of the few exact hypergraph Turán results for an infinite family of forbidden hypergraphs.

Setting

The vertex set is $[n]=\{1,\dots,n\}$. A family $\mathcal F$ is a set of subsets of $[n]$; it is $k$-uniform if $\mathcal F\subseteq\binom{[n]}{k}$, the set of all $k$-element subsets.

A linear path of length $\ell$ is a sequence of distinct sets $F_1,\dots,F_\ell$ such that

$$|F_i\cap F_{i+1}|=1\ \text{ for each } i,\qquad F_i\cap F_j=\emptyset\ \text{ whenever } |i-j|>1.$$

The $k$-uniform linear path of length $\ell$ is written $\mathbb P^{(k)}_\ell$; a family contains it if some $\ell$ of its members form a linear path. The Turán number $\mathbf{ex}_k(n,\mathbb P^{(k)}_\ell)$ is the maximum size of a $k$-uniform family on $[n]$ that does not contain $\mathbb P^{(k)}_\ell$.

Two counting functions describe the answer:

$$f(n,k,t)=\sum_{i=1}^{t}\binom{n-i}{k-1},\qquad g(n,k,t)=f(n,k,t)+\binom{n-t-2}{k-2}.$$

For a set $S\subseteq[n]$ of $t$ elements, $f(n,k,t)$ is the number of $k$-sets meeting $S$ (the star family of $S$), and $g(n,k,t)$ adds the $k$-sets of $[n]\setminus S$ that contain two fixed vertices $u,v$ (the even family).

The proof is phrased in the language of the delta-system method: $s$-stars (sets pairwise meeting in a common kernel), the kernel degree $\deg^*_{\mathcal F}(W)$ (the largest $s$ for which an $s$-star with kernel $W$ exists), $(k,s)$-homogeneous families (k-partite families whose intersections follow a single intersection-closed pattern $\mathcal J$ of subsets of $[k]$, each intersection being the kernel of an $s$-star), the rank of $\mathcal J$, the kernel graph of $\mathcal F$, and the $k$-blowup $H^{(k)}$ of a graph $H$.

Formalization targets

Goal: Theorem 2.4

For every $k\ge 4$ and $t\ge1$ there is $n_0$ such that for all $n\ge n_0$:

$$\mathbf{ex}_k(n,\mathbb P^{(k)}_{2t+1})=f(n,k,t),\qquad \mathbf{ex}_k(n,\mathbb P^{(k)}_{2t+2})=g(n,k,t),$$

and in each case a $k$-uniform, path-free family of that size is exactly the star family of some $t$-set $S$ (odd case), respectively the even family of some $t$-set $S$ and two distinct vertices $u,v\notin S$ (even case).

Milestones

In the order the proof uses them:

1. the star and even families are path-free and have $f$ and $g$ members (lower bound);
2. Lemma 3.1, Füredi's intersection semilattice lemma;
3. Lemma 3.3 and Proposition 3.4, the rank bound $|\mathcal F^*|\le\binom np$;
4. Lemma 3.6 and Corollary 3.7, the structure of patterns of rank $k$ and $k-1$;
5. Theorem 3.8, blowups of trees in homogeneous families of rank $k$ or type 2;
6. Theorem 3.9, the canonical partition of a path-free family;
7. Lemmas 4.2–4.4, from kernel graphs to blowups, the edge count $(k-1)|\mathcal F|\le e(H')\binom{n-2}{k-2}$, and the Erdős–Gallai circumference bound;
8. Theorem 4.5, $\mathbf{ex}_k(n,\mathbb P_{2t+2}^{(k)})\le t\binom{n-1}{k-1}+O(n^{k-2})$;
9. the bound (1), $\mathbf{ex}_k(n,\mathbb P^{(k)}_\ell)\le(k-1)(\ell-1)\binom{n-1}{k-1}$ for every $n$;
10. Erdős' matching theorem for large $n$ (Theorem 1.1) and the $r$-intersecting Erdős–Ko–Rado theorem;
11. Claims 2–3 of §5: a near-extremal family has a $t$-set joined in the kernel graph to all but $O(\sqrt n)$ vertices.

Significance

The theorem gives the exact extremal number and the unique extremal configuration for every linear path when $k\ge4$, and its proof yields a stability statement (Theorem 5.1 of the paper): a path-free family of nearly extremal size is close to a star family. The method is the standard template for exact results on sparse hypergraphs: delta-system decomposition, an asymptotic bound from a graph theorem applied to a kernel graph, then stability and cleaning.

The result is proved in the paper. As far as the platform's catalog shows, none of it is formalized: Mathlib has the intersecting Erdős–Ko–Rado theorem ($r=1$) but not the $r$-intersecting version with uniqueness for large $n$, not Erdős' matching theorem, not the Erdős–Gallai circumference theorem, and no delta-system machinery. A formalization would produce reusable libraries for each of these, and the first machine-checked exact hypergraph Turán number for an infinite family.

Difficulty

The obvious argument — bound the number of members through each vertex and sum — gives only $O(n^{k-1})$ with a wrong leading constant, because a path-free family can have $t$ vertices of almost full degree. Exactness needs three layers that do not reduce to one another. First, the intersection semilattice lemma (Lemma 3.1) is a deep structural theorem with a doubly exponential constant; it is cited, not proved, in the paper. Second, the asymptotic bound passes through the Erdős–Gallai circumference theorem, itself a nontrivial graph result. Third, the exact value requires a stability argument with several error terms ($O(n^{k-3/2})$, $O(\sqrt n)$) that must be balanced, followed by Erdős' matching theorem and the 2-intersecting Erdős–Ko–Rado theorem for large $n$, both with uniqueness. The structural lemmas of §§3–4 are elementary but involve greedy embeddings in which disjointness of the new vertices has to be maintained carefully.

Formalization scope

Vertices are Fin n; families are Finset (Finset (Fin n)); $k$-uniformity is 𝓕 ⊆ univ.powersetCard k. A linear path is an injective map Fin ℓ → Finset (Fin n) into the family with consecutive members meeting in exactly one vertex and non-consecutive members disjoint. The Turán number is a Finset.sup of cardinalities over all path-free $k$-uniform subfamilies, a finite attained maximum for $\ell\ge1$; at $\ell=0$ the feasible set is empty and Lean returns zero, which no theorem here uses. Partitions into $k$ parts are part maps Fin n → Fin k; stars are finsets of distinct petals; the rank is a minimum computed with sInf, exact because intersection patterns consist of proper subsets of $[k]$. "Sufficiently large $n$" and every $O(\cdot)$ are explicit existential constants chosen before $n$ and the family.

Hypotheses added relative to the page: Theorem 3.8 assumes the homogeneous family is nonempty (the empty family is homogeneous for every pattern, and the proof starts from a member). Lemma 4.2 states $k\ge2$, implicit in the paper's definition of a blowup using $k-2$ new vertices; it excludes a false zero-threshold case at $k=0$. Lemma 4.3 is stated for an arbitrary choice of a vertex $c(F)\in F$ in each member, a generalization of the printed lemma, whose proof uses only $c(F)\in F$. Bound (1) is posed for $k\ge2$. Claims 2–3 are stated stand-alone with the $t$-set $S$ existentially quantified.

Trivializing formalizations are ruled out: the goal asserts the value and the uniqueness of the extremal family, the Turán number is a true maximum rather than a junk supremum, the linear path requires intersections of size exactly one and disjointness of non-consecutive members, and all constants are quantified before $n$.

Needed infrastructure: the delta-system method (Lemma 3.1), Erdős–Gallai for circumference, Erdős' matching theorem and $r$-intersecting Erdős–Ko–Rado for large $n$. Each is reusable well beyond this mission, and contributions of any of them are welcome.

Selected references

• Z. Füredi, T. Jiang, R. Seiver, Exact solution of the hypergraph Turán problem for k-uniform linear paths, Combinatorica 34 (2014). arXiv:1108.1247, doi:10.1007/s00493-014-2838-4
• Z. Füredi, On finite set-systems whose every intersection is a kernel of a star, Discrete Math. 47 (1983) 129–132. doi:10.1016/0012-365X(83)90081-X
• P. Erdős, T. Gallai, On maximal paths and circuits of graphs, Acta Math. Acad. Sci. Hungar. 10 (1959) 337–356. doi:10.1007/BF02024498
• P. Erdős, A problem on independent r-tuples, Ann. Univ. Sci. Budapest. Eötvös Sect. Math. 8 (1965) 93–95.
• P. Erdős, C. Ko, R. Rado, Intersection theorems for systems of finite sets, Quart. J. Math. Oxford 12 (1961) 313–320. doi:10.1093/qmath/12.1.313
• P. Frankl, Z. Füredi, Exact solution of some Turán-type problems, J. Combin. Theory Ser. A 45 (1987) 226–262. doi:10.1016/0097-3165(87)90016-7
• D. Mubayi, J. Verstraëte, Minimal paths and cycles in set systems, European J. Combin. 28 (2007) 1681–1693. doi:10.1016/j.ejc.2006.07.008

Motivation

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

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

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

Setting

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

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

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

Formalization targets

Goal: Theorem 2 with the paper's bound

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

A 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