Combinatorics

Motivation

Makespan minimization on identical parallel machines, $P\|C_{\max}$, asks to assign $n$ jobs with processing times to $m$ machines so that the largest machine load is as small as possible. It is strongly NP-hard, and the question has long been how fast a $(1+\varepsilon)$-approximate schedule can be found. After rounding and scaling, a guess $T$ of the optimal makespan becomes a constant, the job sizes take only $d = O((1/\varepsilon)\log(1/\varepsilon))$ distinct values, and the problem becomes an integer program over machine packings: the configuration IP.

A short history of the running times for this problem:

• Hochbaum and Shmoys (1987) gave the first PTAS, with running time $(n/\varepsilon)^{O(1/\varepsilon^2)}$.
• Alon, Azar, Woeginger and Yadid (1997/1998), and Hochbaum and Shmoys, obtained an EPTAS with running time $2^{(1/\varepsilon)^{\mathrm{poly}(1/\varepsilon)}} + O(n\log n)$.
• Jansen (2010) used the support bound of Eisenbrand and Shmonin (2006) to reach $2^{O((1/\varepsilon)^2\log^3(1/\varepsilon))} + O(n\log n)$.
• Chen, Jansen and Zhang (2014) showed that, under the Exponential Time Hypothesis, no PTAS runs in time $2^{(1/\varepsilon)^{1-\delta}}\mathrm{poly}(n)$.
• Jansen, Klein and Verschae (arXiv 2016; Mathematics of Operations Research 2020) reached $2^{O((1/\varepsilon)\log^4(1/\varepsilon))} + O(n\log n)$, matching that lower bound up to polylogarithmic factors in the exponent. Their key ingredient is a structural theorem on the configuration IP, which this mission formalizes.

Setting

Fix $d \in \mathbb{N}$, a vector of job sizes $\pi \in \mathbb{Z}^d_{>0}$ and a capacity $T \in \mathbb{Z}_{>0}$. The knapsack polytope is $\mathcal{P} = \{c \in \mathbb{R}^d_{\ge 0} : \pi\cdot c \le T\}$, and a configuration is an integral point of it:

$$Q = \mathbb{Z}^d \cap \mathcal{P}, \qquad c \in Q \iff c \in \mathbb{Z}^d_{\ge 0},\ \ \sum_{k} \pi_k c_k \le T.$$

A configuration describes one machine: $c_k$ jobs of size $\pi_k$, of total load at most $T$. The support of a vector is the set of its nonzero coordinates, $\operatorname{supp}(c) = \{k : c_k \ne 0\}$. Throughout, $\log = \log_2$. A configuration is simple if $|\operatorname{supp}(c)| \le \log(T+1)$ and complex otherwise; $Q_c$ is the set of complex configurations.

Given the number $b_k$ of jobs of each size and the number $m$ of machines, the configuration IP [conf-IP] asks for multiplicities $x_c \in \mathbb{Z}_{\ge 0}$, one per configuration, with

$$\sum_{c\in Q} c\, x_c = b, \qquad \sum_{c \in Q} x_c = m.$$

Its LP relaxation [conf-LP] replaces $x_c \in \mathbb{Z}_{\ge 0}$ by $x_c \ge 0$. The support of a solution is $\operatorname{supp}(x) = \{c \in Q : x_c \neq 0\}$.

Formalization targets

Goal: thin solutions (Theorem 1)

If [conf-IP] is feasible, it has a feasible solution $x$ with

$$x_c > 1 \Rightarrow c \text{ simple}, \qquad |\operatorname{supp}(x)| \le 4(d+1)\log(4(d+1)T), \qquad \sum_{c\in Q_c} x_c \le 2(d+1)\log(4(d+1)T).$$

A solution with these three properties is called thin.

Milestones

1. Lemma 2 (Eisenbrand–Shmonin): if $|\operatorname{supp}(x)| > 2(d+1)\log(4(d+1)T)$ for a nonnegative integer vector $x$ on $Q$, there are disjoint nonempty $A, B \subseteq \operatorname{supp}(x)$ with $\sum_{c \in A} c = \sum_{c\in B} c$ and $|A| = |B|$.
2. Lemma 3 (Eisenbrand–Shmonin): a feasible [conf-IP] has a solution with $|\operatorname{supp}(x)| \le 2(d+1)\log(4(d+1)T)$.
3. Lemma 4 (Sparsification Lemma): every complex $c \in Q$ satisfies $2c = c_1 + c_2$ for configurations $c_1, c_2$ with $\pi\cdot c_1 = \pi\cdot c_2 = \pi\cdot c$ and $\operatorname{supp}(c_i) \subsetneq \operatorname{supp}(c)$.
4. P1: a feasible solution minimizing the potential $\Phi(x) = \sum_{c \text{ complex}} x_c|\operatorname{supp}(c)|$ uses each complex configuration at most once.
5. P2: such a solution has at most $2(d+1)\log(4(d+1)T)$ complex configurations in its support.

Companion results

• Corollary 5: every vertex of $\operatorname{conv.hull}(Q)$ is a simple configuration; and, from its proof, the number of simple configurations is at most $(L+1)d^{L}(T+1)^{L}$ with $L = \log(T+1)$, for $d \ge 1$.
• Corollary 6: a feasible [conf-LP] has a solution supported on simple configurations only.

Significance

The result. Theorem 1 says that, up to $O(d\log(dT))$ machines, every feasible configuration IP can be solved using simple configurations only. There are $2^{O(\log^2 d + \log^2 T)}$ simple configurations, far fewer than configurations in general, so an algorithm can guess the support of a solution among a much smaller family. This is what yields the $2^{O((1/\varepsilon)\log^4(1/\varepsilon))} + O(n\log n)$ EPTAS for $P\|C_{\max}$, and through the same structure PTASs for $Q\|C_{\max}$ and for $L_p$-norm and max–min objectives. Corollaries 5 and 6 are structural facts about knapsack polytopes in their own right: the integer hull has only simple vertices, and the configuration LP can be restricted to simple configurations.

Formalizing it. The results are proved in the paper; none of them has a machine-checked proof that this mission knows of. The development produces a reusable formal model of configurations and of the configuration IP and LP, a formal Eisenbrand–Shmonin support bound for this IP (a Carathéodory-type statement for integer cones that recurs across integer programming), and the sparsification lemma with its potential-function argument. The constants $4(d+1)$ and $2(d+1)$ are the paper's and are stated exactly.

Difficulty

The obvious argument applies the sparsification lemma repeatedly, replacing any complex configuration used twice by two configurations of smaller support, and then shrinks the support with the Eisenbrand–Shmonin exchange. The second step can undo the first: the exchange moves weight between configurations and may raise the multiplicity of a complex configuration above one again, so alternating the two steps has no evident termination measure. A proof has to control both properties at once. The counting behind the support bound needs the explicit inequality $(sT+1)^{d+1} < 2^s$ for every $s > 2(d+1)\log(4(d+1)T)$, which must be carried out with the exact constants rather than up to $O(\cdot)$.

Formalization scope

• Configurations are functions Fin d → ℕ with $\sum_k \pi_k c_k \le T$; solutions of [conf-IP] are finitely supported functions (Fin d → ℕ) →₀ ℕ vanishing outside $Q$, and solutions of [conf-LP] are finitely supported real-valued functions, nonnegative and vanishing outside $Q$.
• The standing assumptions of §2 are binders of every statement: $\pi_k > 0$ for all $k$ and $T > 0$. Lemma 4 does not need $T > 0$ and omits it.
• The paper writes $b \in \mathbb{R}^d$ for [conf-IP]; feasibility forces $b \in \mathbb{N}^d$, so $b$ and $m$ are natural numbers. For [conf-LP] they are real.
• $\log$ is Real.logb 2 and every bound is a real inequality; no floor is taken.
• In Lemma 2, $Mx^A = Mx^B$ is stated row by row: the sum of the configurations in $A$ equals that in $B$, and $|A| = |B|$.
• "Minimum potential" in P1 and P2 means $\Phi(x) \le \Phi(y)$ for every feasible solution $y$ of the same instance.
• A vertex of $\operatorname{conv.hull}(Q)$ is an extreme point (Mathlib's Set.extremePoints). The asymptotic count of Corollary 5 is replaced by the explicit bound of its proof, with the added hypothesis $d \ge 1$ (at $d = 0$ the explicit bound is $0$ while $Q = \{0\}$).

The goal theorem refers only to [conf-IP], its solutions, supports and the simple/complex split; it does not mention the potential, the matrix $M$ or a minimality assumption, so it cannot be discharged by choosing a special solution in the hypotheses.

Needed infrastructure: finite sums over Finsupp, the pigeonhole principle on finsets, elementary bounds on Real.logb, and, for Corollaries 5 and 6, convex hulls and extreme points of finite sets in $\mathbb{R}^d$. The definitions of configurations and of the configuration IP/LP are reusable for other configuration-IP papers (bin packing, cutting stock, scheduling). Contributions of auxiliary lemmas on supports of integer conic combinations are welcome.

Selected references

• K. Jansen, K.-M. Klein, J. Verschae, Closing the Gap for Makespan Scheduling via Sparsification Techniques, ICALP 2016; Mathematics of Operations Research, 2020. https://arxiv.org/abs/1604.07153 (version v1, the basis of every citation in this mission)
• F. Eisenbrand, G. Shmonin, Carathéodory bounds for integer cones, Operations Research Letters 34, 564–568, 2006. https://doi.org/10.1016/j.orl.2005.09.008
• K. Jansen, An EPTAS for scheduling jobs on uniform processors: using an MILP relaxation with a constant number of integral variables, SIAM Journal on Discrete Mathematics 24, 457–485, 2010.
• N. Alon, Y. Azar, G. J. Woeginger, T. Yadid, Approximation schemes for scheduling on parallel machines, Journal of Scheduling 1, 55–66, 1998.
• D. S. Hochbaum, D. B. Shmoys, Using dual approximation algorithms for scheduling problems: theoretical and practical results, Journal of the ACM 34, 144–162, 1987. https://doi.org/10.1145/7531.7535
• L. Chen, K. Jansen, G. Zhang, On the optimality of approximation schemes for the classical scheduling problem, Proceedings of the 25th ACM-SIAM Symposium on Discrete Algorithms (SODA), 657–668, 2014.

Motivation

The generalized Turán number $\mathrm{ex}(n,H,\mathcal F)$ is the largest number of copies of a graph $H$ in an $n$-vertex graph containing no member of a family $\mathcal F$. With $H=K_2$ it is the classical Turán number; the systematic study of general $H$ began with Alon and Shikhelman (2016), and cycles are its most studied case: Bollobás and Győri bounded $\mathrm{ex}(n,C_3,C_5)$, and Gerbner and Palmer determined $\mathrm{ex}(n,C_l,K_{2,t})$.

Gerbner, Győri, Methuku and Vizer, Generalized Turán problems for even cycles (J. Combin. Theory Ser. B, 2020; arXiv:1712.07079), count copies of one cycle in graphs avoiding another. For even cycles they show $\mathrm{ex}(n,C_{2l},C_{2k})=\Theta(n^l)$. Most extremal constructions there are bipartite, so they also study the bipartite generalized Turán number. For the first non-trivial pair, six-cycles in a graph avoiding eight-cycles, they determine its leading term exactly. This mission formalizes that result, Theorem 12 of the paper.

Setting

All graphs are finite and simple. A $k$-cycle $C_k$ is a cycle with $k$ vertices. A copy of $C_k$ in $G$ is a subgraph of $G$ isomorphic to $C_k$; $\mathcal N(C_k,G)$ is the number of copies, so a cycle is counted once regardless of its starting point and direction. A graph is $C_8$-free if no subgraph of it is isomorphic to $C_8$ (induced or not). A graph is bipartite if its vertices can be split into two classes $A$ and $B$ with every edge joining $A$ to $B$.

$$\mathrm{ex}_{bip}(n,C_6,C_8)=\max\{\mathcal N(C_6,G) : G \text{ bipartite},\ C_8\text{-free},\ |V(G)|=n\}.$$

The proof works with a fixed bipartition $(A,B)$ of a $C_8$-free graph $G$ and uses the following notions.

• $N(u,v)$ is the set of common neighbours of $u$ and $v$.
• A pair $\{u,v\}$ is fat if $|N(u,v)|\ge 4$.
• A 6-cycle is fat if it contains a fat pair from each class.
• A pair is marked if it has exactly three common neighbours.
• A 4-set $F\subseteq A$ is nice if its four vertices have three common neighbours in $B$, i.e. they span a $K_{4,3}$.
• For $x,y,z\in A$, $h(x,y,z)$ is the number of 6-cycles through all three. The triple is good if $h\le 6$ and bad otherwise.
• A hypergraph is Berge-$C_4$-free if it has no distinct vertices $x,y,z,w$ and distinct hyperedges $h_1,\dots,h_4$ with $\{x,y\}\subseteq h_1$, $\{y,z\}\subseteq h_2$, $\{z,w\}\subseteq h_3$, $\{w,x\}\subseteq h_4$.

In Lean, $\mathrm{ex}_{bip}(n,C_6,C_8)$ is exBip n (cycleGraph 6) {8}, and $\mathcal N$ is Mathlib's copyCount.

Formalization targets

Goal: Theorem 12

$$\mathrm{ex}_{bip}(n,C_6,C_8)=n^3+O\bigl(n^{5/2}\bigr)\qquad(n\to\infty).$$

This is two-sided: $|\mathrm{ex}_{bip}(n,C_6,C_8)-n^3|\le Cn^{5/2}$ for some constant $C$ and all large $n$.

Milestones

1. Lower bound. $K_{3,n-3}$ is bipartite, $C_8$-free, and has exactly $6\binom{n-3}{3}=n^3-O(n^2)$ six-cycles. This is Theorem 10's construction with $k=4$, $l=3$, and Remark 2 notes that it is bipartite.
2. Shape of fat 6-cycles.
   • Claim 3: a fat pair $\{v_1,v_3\}$ on $v_1\cdots v_6$ excludes the fat pairs $\{v_2,v_4\}$ and $\{v_2,v_6\}$.
   • Claim 4: fat 6-cycles through one fat pair have pairwise intersecting fat pairs in the other class.
   • Claim 5: distinct fat pairs of fat 6-cycles in $A$ have $|N\cap N'|\le 1$.
   • Observation 1: a disjointness statement for fat pairs sharing a vertex.
3. Claim 6. For a fat pair $\{v_1,v_3\}\subseteq A$, the sum $g(v_1,v_3)$ of $|N(v_4,v_6)|$ over the fat pairs $\{v_4,v_6\}\subseteq B$ on a common fat 6-cycle with $v_1,v_3$ is at most $4n$.
4. Corollary 7 (from Győri–Lemons). A Berge-$C_4$-free hypergraph on $n$ vertices has $\sum_e|e|=O(n^{3/2})$.
5. Claim 7. The hypergraph on $B$ whose hyperedges are the sets $N(v_1,v_3)$, over the fat pairs of $A$ that lie on a fat 6-cycle, is Berge-$C_4$-free.
6. Claim 8. There are $O(n^{5/2})$ fat 6-cycles.
7. Non-fat cycles.
   • Claim 9: a marked pair inside a nice set gives good triples.
   • Claim 10: $O(|A|^{3/2})$ marked pairs lie in no nice set.
   • Claim 11: $O(|A|^2)$ bad triples contain neither a fat nor a marked pair.
8. One-sided count. At most $6\binom{|A|}{3}+O(|A|^{5/2})$ six-cycles contain no fat pair from $A$.

Significance

Theorem 12 is the only case of the paper where a bipartite generalized Turán number of two even cycles is determined up to a lower-order term. Theorem 10 gives the order $n^l$ in general, and Remark 2 gives bipartite upper and lower bounds whose ratio tends to 1 only as $k\to\infty$. Theorem 12 settles $(l,k)=(3,4)$ exactly. The authors conjecture that the non-bipartite number $\mathrm{ex}(n,C_6,C_8)$ has the same asymptotics, but this is open. The argument also links graph counting to Berge hypergraphs: Claim 7 reduces the fat 6-cycles to a Berge-$C_4$-free hypergraph, whose total edge size is controlled by Corollary 7.

Theorem 12 is proved in the paper. As far as a search of the Prove2Me catalogue shows, neither it nor any of its claims has a machine-checked proof. Formalizing it means:

• formalizing the case analysis of §4.2;
• formalizing Corollary 7, which depends on the Győri–Lemons theorems (Theorems 5 and 6), proved outside the paper;
• formalizing the elementary but tedious count of 6-cycles in $K_{3,n-3}$.

Difficulty

The obvious bound fails. Every 6-cycle in a bipartite graph has three vertices in each class, and each pair of them has some common neighbours. If no pair had more than three common neighbours, each triple in $A$ would lie on at most $27$ six-cycles, giving roughly $27\binom{n}{3}$ cycles, not $n^3$. The leading constant $1$ needs two refinements. First, triples on more than $6$ cycles must be shown to be rare. Second, cycles through pairs with many common neighbours (fat pairs) must be bounded separately, by $O(n^{5/2})$. That second bound is the main obstacle. A fat pair alone can lie on many cycles, so counting fat pairs is not enough. What makes the bound work is the near-disjointness of the common neighbourhoods (Claims 4–6) together with a hypergraph Turán estimate.

Formalization scope

• Vertices and copies. Graphs are SimpleGraph (Fin n), or a general finite type in milestones about a single graph. Copies are unlabelled (copyCount, the number of subgraphs isomorphic to $C_6$): $K_{3,3}$ has $6$ copies of $C_6$, not $72$.

• Bipartiteness. In $\mathrm{ex}_{bip}$ it is Colorable 2. In the milestones it is an explicit bipartition $(A,B)$ that excludes edges inside a class. $C_8$-freeness is (cycleGraph 8).Free G.

• The maximum. $\mathrm{ex}_{bip}$ is a supremum of natural numbers over a nonempty finite set, since the empty graph is admissible. It is therefore a true maximum; a sanity file proves this.

• Cycles inside the proof. Labelled 6-cycles are injective maps from $\mathbb Z/6$ with consecutive images adjacent. Claim 8 counts fat 6-cycles labelled, which changes only the constant.

• Landau terms. Every $O(\cdot)$ is an explicit constant, quantified before $n$ and the graph. The goal uses Mathlib's IsBigO of $\mathrm{ex}_{bip}(n,C_6,C_8)-n^3$ against $n^{5/2}$.

• Corrections to the printed text.

  • Observation 1's conclusion is stated with $N(v_4,v_6')$, as in its proof, rather than the printed $N(v_4',v_6')$.
  • Claim 6's $g$ is the displayed sum, not "the cardinality of the union".
  • Claim 4 drops the hypothesis "different cycles", which only excludes a trivial case. It also drops "these are the other fat pairs", which follows from Claim 3.

• Ruled-out encodings. Some encodings would make the statements trivial or wrong, and none of them is used:

  • a one-sided goal (only the upper bound, or only the lower bound);
  • a junk supremum;
  • labelled copies in place of unlabelled ones;
  • constants allowed to depend on $n$ or on the graph;
  • a bipartition that allows edges inside a class.

• Infrastructure. A complete development needs:

  • counting of cycle copies in complete bipartite graphs;
  • Hall's theorem (in Mathlib), used in Claims 7 and 10;
  • the Kővári–Sós–Turán bound $\mathrm{ex}(m,C_4)=O(m^{3/2})$ for Claim 10;
  • the Győri–Lemons theorems for Corollary 7.

  The Berge-cycle and $C_4$-free bounds can be reused beyond this mission. Contributions are welcome at any level: proofs of individual claims, of Corollary 7, or the final assembly.

Selected references

• D. Gerbner, E. Győri, A. Methuku, M. Vizer, Generalized Turán problems for even cycles, J. Combin. Theory Ser. B 145 (2020); arXiv:1712.07079v3. https://arxiv.org/abs/1712.07079, https://doi.org/10.1016/j.jctb.2020.05.005
• N. Alon, C. Shikhelman, Many $T$ copies in $H$-free graphs, J. Combin. Theory Ser. B 121 (2016). https://doi.org/10.1016/j.jctb.2016.03.004
• E. Győri, N. Lemons, Hypergraphs with no cycle of a given length, Combin. Probab. Comput. 21 (2012). https://doi.org/10.1017/S0963548311000691
• B. Bollobás, E. Győri, Pentagons vs. triangles, Discrete Math. 308 (2008). https://doi.org/10.1016/j.disc.2007.08.041
• D. Gerbner, C. Palmer, Counting copies of a fixed subgraph in $F$-free graphs, European J. Combin. 82 (2019). https://doi.org/10.1016/j.ejc.2019.07.004

Motivation

The Turán number $\mathrm{ex}(n,F)$ is the largest number of edges in an $n$-vertex graph with no copy of $F$. Its generalized version, introduced systematically by Alon and Shikhelman (JCTB 2016), replaces edges by copies of a second graph $H$: $\mathrm{ex}(n,H,\mathcal F)$ is the largest number of copies of $H$ in an $n$-vertex graph containing no member of the family $\mathcal F$. When both $H$ and the forbidden graphs are cycles, these numbers measure how many long cycles a graph can carry while some cycle lengths are excluded and they refine the Bondy–Simonovits even-cycle theorem (JCTB 1974), which bounds the number of edges of a $C_{2k}$-free graph by $O(n^{1+1/k})$.

Gerbner, Győri, Methuku and Vizer (arXiv:1712.07079, J. Combin. Theory Ser. B 2020, DOI 10.1016/j.jctb.2020.05.005) study $\mathrm{ex}(n,C_a,\mathcal C_A)$ for cycles. Their Theorem 10 gives $\mathrm{ex}(n,C_{2l},C_{2k})=\Theta(n^l)$; Theorem 14, the subject of this mission, adds a girth condition: when all cycles of length $3,\dots,2l-1$ are forbidden together with $C_{2k}$, the order of magnitude of the number of $C_{ml}$'s is $n^m$. The case $m=2$ answers the question of how many $C_{2l}$'s a $C_{2k}$-free graph of girth $2l$ can have.

Setting

All graphs are finite and simple. A copy of a graph $H$ in $G$ is a subgraph of $G$ isomorphic to $H$, and $\mathcal N(H,G)$ is the number of copies. $C_a$ is the cycle of length $a\ge3$; $P_l$ is the path on $l$ vertices (of length $l-1$).

For a set $A$ of integers, each at least $3$, let $\mathcal C_A=\{C_a:a\in A\}$; a graph is $\mathcal C_A$-free if it contains none of these cycles as a subgraph. Write $\mathcal C_{2l-1}=\{C_3,C_4,\dots,C_{2l-1}\}$. The generalized Turán number is

$$\mathrm{ex}(n,H,\mathcal C_A)=\max\{\mathcal N(H,G): G\text{ is a }\mathcal C_A\text{-free graph on }n\text{ vertices}\}.$$

For vertices $a\neq b$, $f_l(a,b)$ is the number of paths with $l$ edges between $a$ and $b$. A pair $\{u,v\}$ is fat if $f_l(u,v)\ge 4l^2$, and a copy of $C_{2l}$ is fat if all $l$ of its pairs of opposite vertices are fat.

The $(l,t)$-theta graph joins two vertices by $t$ internally disjoint paths of length $l$. For a graph $F$, the theta-$(n,F,l)$ graph replaces each edge of $F$ by an $(l,t)$-theta graph with $t=\lfloor (n-|V(F)|)/(|E(F)|(l-1))\rfloor$ and adds isolated vertices up to $n$; here $F=C_m$ for $m\ge3$ and $F=K_2$ for $m=2$.

Formalization targets

Goal: Theorem 14

For integers $k>l\ge2$ and $m\ge2$ with $2k\neq ml$,

$$\mathrm{ex}\big(n,C_{ml},\mathcal C_{2l-1}\cup\{C_{2k}\}\big)=\Theta(n^m)\qquad(n\to\infty).$$

Both bounds are part of the goal; the constants depend on $k,l,m$ only.

Milestones

1. Lemmas 25 and 26: forbidding additional odd cycles (Lemma 25) or shorter odd cycles (Lemma 26) does not change the order of magnitude of $\mathrm{ex}(n,C_{2k},\mathcal C_A)$ or $\mathrm{ex}(n,C_{2k+1},\mathcal C_A)$.
2. Lemma 27: a partition $V_1,\dots,V_s$ with no $P_3$ inside $V_i$ ($i<s$), no $P_{p+1}$ joining different parts and $V_s$ independent forces $|E(G)|\le p\,n$.
3. The lower bound: the theta graph has only cycles of lengths $2l$ and $ml$, hence avoids the forbidden family, and has $\Omega(n^m)$ cycles of length $ml$.
4. Claims 12 and 13: the structure of two $2l$-cycles through a common path, and short detours between fat pairs, in graphs of girth at least $2l$.
5. Counting $C_{2l}$'s in girth at least $2l$: at most $\binom{4l^2-1}{2}\binom n2$ non-fat ones; Claim 14 on the greedy multiplicities; at most $\frac{2k(k-l)}{l-2}\binom n2$ fat ones.
6. The case $m\ge3$: display (5), $\tfrac12\sum_{a\ne b}\binom{f_l(a,b)}{2}=O(n^2)$, and Claim 15, $\sum_{b\neq a}f_l(a,b)=O(n)$.

Significance

Theorem 14 locates $\mathrm{ex}(n,C_{ml},\mathcal C_{2l-1}\cup\{C_{2k}\})$ at $n^m$ for every admissible triple, so in graphs of girth $2l$ forbidding one further even cycle $C_{2k}$ (with $2k\neq ml$) caps the number of $ml$-cycles at the count achieved by a blown-up $m$-cycle of long paths. The paper uses it to settle the order of magnitude of $\mathrm{ex}(n,C_6,\mathcal C_A)$ for every family $A$ with $4\in A$, $6\notin A$ and $|A_e|\ge2$ (Theorem 20), and its case $l=2$ recovers Theorem 10.

The result is proved in the paper; nothing here is open mathematically. To the best of a platform search (2026-10-08), no part of it is formalized: Mathlib has copyCount, cycleGraph and pathGraph, but no generalized Turán numbers, no theta graphs and no counting of paths between two vertices. The mission produces a machine-checked proof of the theorem and of the counting lemmas of §5, which are reusable for other generalized Turán problems with cycles.

Difficulty

The lower bound is an explicit construction, and its difficulty is bookkeeping: proving that a subdivided multigraph has no cycles other than those of lengths $2l$ and $ml$, and counting the $ml$-cycles. The upper bound is the substance. A direct count of $C_{2l}$'s through codegrees, which works for $C_4$, fails here because paths of length $l$ between a pair are not controlled by a single neighbourhood. The paper's route separates fat from non-fat cycles and runs a greedy multiplicity procedure; Claim 14 then grows a $C_{2k}$ by an induction on the cycle length in steps of $l-1$, which needs the precise intersection pattern of Claim 12 and the detour paths of Claim 13. For $m\ge3$ the argument goes through layered neighbourhoods and Lemma 27. The $m=2$ argument divides by $l-2$, so for $l=2$ a different route (Theorems 10 and 11 of the paper) is needed.

Formalization scope

Graphs are SimpleGraph (Fin n) for the extremal function and graphs on an arbitrary finite type for the lemmas. Copies are unlabelled (copyCount, subgraphs isomorphic to the pattern); $C_a$ and $P_l$ are Mathlib's cycleGraph a and pathGraph l. exCyc n H A is the supremum, over $\mathcal C_A$-free graphs on Fin n, of the copy count; the set is finite and contains the empty graph's count whenever every length in $A$ is at least $3$, so it is a maximum. The forbidden family of the goal is Set.Icc 3 (2 * l - 1) ∪ {2 * k}, every length from $3$ to $2l-1$ together with $2k$. $\Theta$, $O$ and $\Omega$ are Mathlib's asymptotic relations along atTop, with constants fixed before $n$ and the graph. $f_l(a,b)$ counts injective vertex sequences (paths, not walks). The theta graph thetaCycle n m l is an explicit graph on Fin n.

Added or pinned hypotheses, all disclosed in the items: $l\ge2$ in the goal (the page writes only $k>l$; at $l=1$ the family $\mathcal C_{2l-1}$ is empty and the statement fails); $C\neq C'$ in Claim 12; $l\ge3$ where the page divides by $l-2$; Lemma 27 with the explicit bound $p\,n$ of its proof, which is uniform in $s$; Claim 15 under the full family $\mathcal C_{2l-1}\cup\{C_{2k}\}$, which its proof needs. Claim 14 assumes only girth $\ge 2l$, not $C_{2k}$-freeness, since on the page its conclusion at $r=k$ is the contradiction.

The statements rule out the trivializing readings: the goal is two-sided, so an upper bound alone does not close it; exCyc is a genuine maximum, not a junk supremum; copies are unlabelled; the constants come before $n$ and the graph; the forbidden family contains all short cycles, not only $C_{2l-1}$.

A complete development needs path counting in graphs of large girth (uniqueness of short paths), layered neighbourhoods, the degeneracy argument of Lemma 27, a random bipartition argument for Lemma 25, and cycle structure in theta graphs. Contributions of any milestone, and of general-purpose lemmas on paths and cycles in SimpleGraph, are welcome.

Selected references

• D. Gerbner, E. Győri, A. Methuku, M. Vizer, Generalized Turán problems for even cycles, J. Combin. Theory Ser. B (2020); arXiv:1712.07079v3 (2018). https://arxiv.org/abs/1712.07079, https://doi.org/10.1016/j.jctb.2020.05.005
• N. Alon, C. Shikhelman, Many T copies in H-free graphs, J. Combin. Theory Ser. B 121 (2016). https://doi.org/10.1016/j.jctb.2016.03.004
• J. A. Bondy, M. Simonovits, Cycles of even length in graphs, J. Combin. Theory Ser. B 16 (1974). https://doi.org/10.1016/0095-8956(74)90052-5

Motivation

An extremal graph problem asks how many copies of a chosen small graph can occur when a different graph is forbidden. The usual Turán problem counts edges; counting paths or cycles gives a more detailed view of the structure that can survive a forbidden subgraph. Gerbner, Győri, Methuku and Vizer study these generalized Turán numbers for paths and cycles in their paper on even-cycle problems. Their Theorem 23 asks for the leading number of paths when a specified odd cycle is absent. The answer has the same leading term as a balanced complete bipartite graph, despite the fact that excluding one odd cycle is weaker than requiring a graph to be bipartite. Gerbner et al., Theorem 23

The spectral theorem cited by the authors gives a useful threshold for this setting. For a graph with no cycle of length $2k+1$, it bounds the adjacency spectral radius once the vertex count exceeds $320(2k+1)$. This threshold is explicit and stays visible in the finite-size milestone. Gerbner et al., Theorem 32, citing Nikiforov (2008).

Setting

A simple graph $G$ has finitely many vertices and no loops or parallel edges. For $a\ge3$, $C_a$ is the cycle on $a$ vertices, and $P_l$ is the path on $l$ vertices. Thus $P_l$ has $l-1$ edges, following the paper's convention. A copy of $H$ in $G$ is a subgraph of $G$ isomorphic to $H$; copies are unlabelled, so reversing a path does not create a second copy. Write $\mathcal N(H,G)$ for their number. Gerbner et al., pp. 2–3

For a set $A$ of lengths, a graph is $\mathcal C_A$-free if it has no subgraph isomorphic to $C_a$ for any $a\in A$. The mission mainly uses $A=\{2k+1\}$: exactly one odd cycle length is forbidden, while shorter and longer cycles may still occur. The generalized Turán number is the maximum

$$\operatorname{ex}(n,H,\mathcal C_A) =\max_{\substack{|V(G)|=n\\G\text{ is }\mathcal C_A\text{-free}}}\mathcal N(H,G).$$

The adjacency matrix $A_G$ records whether each pair of vertices is adjacent. Because the graph is undirected, this is a real symmetric matrix. Its spectral radius $\mu(G)$ is the largest absolute value of an eigenvalue of $A_G$. The graph $B_{n,a}$ is the complete bipartite graph with parts of sizes $a$ and $n-a$; the balanced choice uses $a=\lfloor n/2\rfloor$. Gerbner et al., §§7.1–7.2

Formalization targets

Main result: Theorem 23

For each fixed $k\ge1$ and $l\ge2$, as $n\to\infty$,

$$\operatorname{ex}(n,P_l,\mathcal C_{\{2k+1\}}) =(1+o(1))\left(\frac n2\right)^l.$$

The equality gives both sides of the asymptotic estimate. The $o(1)$ term may depend on the fixed parameters $k,l$ and tends to zero as the number of vertices grows. Gerbner et al., Theorem 23, p. 8

Supporting targets

The milestone list records the balanced complete bipartite lower bound, the comparison between paths and walks in equation (7), a spectral bound on the walk sum, Nikiforov's stated spectral estimate, and the resulting finite-size upper bound. In particular, the last two targets retain the paper's constants:

$$n>320(2k+1),\qquad \mu(G)\le\sqrt{n^2/4},\qquad \mathcal N(P_l,G)\le(n/2)^l.$$

The milestone statements identify which assertions concern every graph and which require the forbidden-cycle condition. Gerbner et al., pp. 30, 32

Companion: even cycles (Theorem 24)

For fixed $k\ge1$ and $l\ge2$,

$$\operatorname{ex}(n,C_{2l},\mathcal C_{\{2k+1\}})=(1+o(1))\,\frac{1}{2l}\left(\frac{n^2}{4}\right)^{l},$$

and Remark 3 records the inequality $\mathcal N(P_{2l},G)\ge 2l\,\mathcal N(C_{2l},G)$ for every graph $G$, which links this count to Theorem 23. Gerbner et al., Theorem 24, p. 11; Remark 3, p. 32

Significance

Theorem 23 fixes the leading coefficient for the maximum path count for every fixed path length and forbidden odd-cycle length in its range. A balanced complete bipartite graph reaches that coefficient asymptotically, so the result identifies an extremal construction at first order. The lower-bound milestone formalizes this construction with balanced parts, including the one-vertex rounding needed when $n$ is odd. The matrix and spectral milestones can also be reused when counting walks or paths under different graph restrictions. Gerbner et al., §7.2

The paper proves these results on paper. In this mission, the definitions and theorem statements are checked by Lean, while proofs of the draft theorems remain to be supplied. A completed development would make the path-count theorem and its stated spectral dependency machine checked in the pinned Mathlib environment. It would also expose where a general graph identity suffices and where the odd-cycle prohibition matters.

Difficulty

Counting paths directly is difficult because the available information about a graph with one forbidden odd-cycle length does not control each vertex degree tightly enough to determine a sharp path count. Counting walks is easier algebraically, but walks may revisit vertices, so their number is generally larger than the number of paths. A graph-wide spectral bound is needed to control the walk total sharply, and the cited Nikiforov estimate has to be carried with its forbidden-cycle hypothesis and vertex threshold. A generic bound based only on the maximum degree would not yield the coefficient in Theorem 23. Gerbner et al., §§7.1–7.2

Formalization scope

Graphs on $n$ vertices are represented as SimpleGraph (Fin n). Mathlib's cycleGraph a and pathGraph l represent $C_a$ and the path on $l$ vertices, and copyCount counts unlabelled subgraph copies. The finite set of real adjacency eigenvalues defines $\mu(G)$ through a maximum of absolute values. On an empty vertex type this value is zero. The extremal number is a natural-number supremum over feasible graphs; for the odd-cycle family the feasible set is nonempty and finite, so this supremum is attained.

The goal has $k\ge1$ and $l\ge2$, exactly as Theorem 23 states. The lower-bound item chooses parts of sizes $\lfloor n/2\rfloor$ and $\lceil n/2\rceil$. Equation (7) requires $l\ge2$: for $l=1$ the claimed factor of two is false. The finite spectral and path bounds require $n>320(2k+1)$. These conditions are explicit in the Lean statements. Natural subtraction appears only in expressions whose hypotheses make the intended quantity meaningful, including $l-1$; the bipartite part size is computed with natural division. The asymptotic statements use real sequences tending to zero and eventual comparisons or equality.

The result must include the lower bound as well as the upper bound. It uses unlabelled path copies, an attained extremal maximum, and a forbidden family consisting of the specified odd cycle. An upper bound alone, labelled copies, or a supremum over an empty class would change the theorem. The needed infrastructure consists of graph-copy counts, adjacency-matrix walk counts, finite-dimensional spectral facts, and the cited odd-cycle spectral theorem. The page states Theorem 24 "for any $k,l$"; the Lean statement and Remark 3 require $k\ge1$ and $l\ge2$, the only values for which $C_{2k+1}$ and $C_{2l}$ are cycles. Contributions proving the milestones or developing reusable interfaces for those objects are within scope.

Selected references

• D. Gerbner, E. Győri, A. Methuku and M. Vizer, Generalized Turán problems for even cycles, Journal of Combinatorial Theory, Series B, 2020. arXiv:1712.07079v3; DOI:10.1016/j.jctb.2020.05.005.
• V. Nikiforov, A spectral condition for odd cycles in graphs, Linear Algebra and its Applications 428 (2008), 1492–1498. Cited as [34] in arXiv:1712.07079v3.

Motivation

A suffix tree of a text $T[1..n]$ answers pattern-matching and string-analysis queries (longest repeats, maximal repeats, matching statistics) in time close to optimal, but it occupies $\Theta(n)$ machine words. For highly repetitive collections, such as many genomes of one species or the versions of a document, this is far more than the information the text contains. A standard measure of that information is $r$, the number of runs (maximal blocks of one repeated symbol) of the Burrows–Wheeler transform of $T$. On repetitive collections $r$ is orders of magnitude smaller than $n$, and indexes using $O(r)$ words are of direct practical interest in bioinformatics and in versioned document stores.

Gagie, Navarro and Prezza (arXiv:1809.02792v2, 2019) build a compressed suffix tree in $O(r\log(n/r))$ words (their Theorem 9, p. 28). A compressed suffix tree in the style of Abeliuk, Cánovas and Navarro (Algorithms 2013) needs the longest common prefix array $LCP$ in compressed form, and stores it differentially, as $DLCP$. The paper's route to compressing $DLCP$ is one exact combinatorial fact: $DLCP$ has a bidirectional macro scheme of size at most $4r+1$ (p. 28). A cited conversion of macro schemes into run-length grammars (Lemma 18, from Gagie, Navarro and Prezza, LATIN 2018) then gives the $O(r\log(n/r))$ grammar. This mission formalizes that combinatorial fact and the lemmas it rests on.

Setting

A text $T[1..n]$, $n\ge 1$, is a string over the alphabet $[1..\sigma]$ whose last symbol T[n]=\=1$is the smallest symbol and occurs nowhere else. The **suffix**$T[i..]$is$T[i]T[i+1]\cdots T[n]$. The **suffix array**$SA[1..n]$is the permutation of$[1..n]$ listing the starting positions of the suffixes in increasing lexicographic order.

The Burrows–Wheeler transform is $BWT[p]=T[SA[p]-1]$ if $SA[p]>1$ and $BWT[p]=T[n]$ if $SA[p]=1$: the symbol preceding the $p$-th smallest suffix, read cyclically. The LF mapping is

$$LF(p)=C[BWT[p]]+\operatorname{rank}[p],$$

where $C[c]$ counts the symbols of $BWT$ smaller than $c$ and $\operatorname{rank}[p]$ counts the occurrences of $BWT[p]$ in $BWT[1..p]$. A position $p$ starts a run if $p=1$ or $BWT[p]\ne BWT[p-1]$; $r$ is the number of run starts, written $p_1<\dots<p_r$.

Let $\operatorname{lcp}(S,S')$ be the length of the longest common prefix of two strings. Then

$$LCP[1]=0,\quad LCP[p]=\operatorname{lcp}(T[SA[p-1]..],T[SA[p]..]),\qquad DLCP[1]=LCP[1],\quad DLCP[i]=LCP[i]-LCP[i-1].$$

The differential suffix array is $DSA[1]=SA[1]$, $DSA[p]=SA[p]-SA[p-1]$.

A bidirectional macro scheme (BMS) of size $b$ on a sequence $S[1..n]$ of any symbol type (Definition 6, p. 28, after Storer and Szymanski) is a partition $S=S_1\cdots S_b$ into consecutive blocks, each either an explicit symbol (a block of length 1) or a pointer to another occurrence $S[j..j']$ of the same content. The source map sends a position at offset $i'$ inside a pointer block to $f(i)=j+i'-1$. The scheme is correct if, from every position $i$, some iterate $f^k(i)$, $k\ge0$, is an explicit symbol.

Formalization targets

Goal: a macro scheme of size at most $4r+1$

$$\exists\ \text{a correct BMS of } DLCP[1..n] \text{ of size } b\le 4r+1.$$

This is the sentence following Lemma 16 on p. 28, proved by Lemma 17. It fixes no constant beyond the paper's own count, and it is the exact input Lemma 18 needs.

Milestones

1. LF is a single cycle (§2.3, p. 8): $LF$ permutes $[1..n]$ and the orbit of position 1 visits every position in fewer than $n$ steps.
2. $LF$ walks the text backwards (§2.4, p. 9): $SA[LF(p)]=SA[p]-1$ whenever $SA[p]>1$.
3. Lemma 12 (p. 20): if $BWT[p-1]=BWT[p]$ then $LF(p-1)=LF(p)-1$ and $DSA[LF(p)]=DSA[p]$.
4. Lemma 16 (p. 28): if $BWT[p-2]=BWT[p-1]=BWT[p]$ then $LF(p-1)=LF(p)-1$ and $DLCP[LF(p)]=DLCP[p]$.
5. Lemma 17 (p. 28): the partition of $DLCP$ into the explicit symbols $DLCP[p_i+k]$, $k\in\{0,1,2\}$, and the regions $DLCP[p_i+3..p_{i+1}-1]$ pointing to $DLCP[LF(p_i+3)..LF(p_{i+1}-1)]$, is a BMS.

Significance

The result. The bound $4r+1$ ties the compressibility of the $LCP$ array, a structure of size $n$ that does not obviously inherit the repetitiveness of the BWT, to the number of BWT runs. Through Lemma 18 it yields a run-length grammar of size $O(r\log(n/r))$ for $DLCP$ (Lemma 19, p. 29), and the paper's compressed suffix tree supports its navigation primitives on that grammar. The same pattern, runs of the BWT inducing copies in a differential array, drives the paper's $O(r\log(n/r))$-word access to $SA$ and $ISA$ (§5), of which Lemma 12 is the first step.

Formalizing it. The result is proved in the paper; to our knowledge none of it, nor the basic theory of suffix arrays and the Burrows–Wheeler transform, has a machine-checked proof on this platform. The mission produces a self-contained Lean development of the BWT and LF mapping from their counting definitions, of the $LCP$ and $DLCP$ arrays, and of macro schemes with their correctness condition. The single-cycle property of $LF$ and the identity $SA[LF(p)]=SA[p]-1$ are folklore results that underlie every FM-index; they are formalized here from the counting formula, not assumed.

Difficulty

The obvious proof of the goal counts blocks: at most $3r$ explicit symbols and at most $r+1$ regions. The counting is easy; the content lies in the two properties the count presupposes. First, the copies must be correct: a whole region $DLCP[p_i+3..p_{i+1}-1]$ must coincide with the stretch starting at $LF(p_i+3)$, which needs $LF$ to map a run onto consecutive positions and $LCP$ differences to be preserved, and it needs three consecutive equal BWT symbols, not two, because $DLCP[p]$ involves the suffixes in cells $p-2$, $p-1$ and $p$. Second, the scheme must be correct as a whole: following pointers must never cycle. A scheme in which two regions point at each other satisfies every local condition and still fails. Ruling this out requires the global fact that $LF$ is one cycle through all of $[1..n]$, which in turn rests on the lexicographic order of suffixes and the uniqueness of the terminator \$$. Connecting the counting definition of LF$to the backward step$SA[LF(p)]=SA[p]-1$ is itself a nontrivial argument about ranks of symbols among sorted suffixes.

Formalization scope

Positions are 1-based natural numbers, as in the paper. The text and the suffix array are functions $\mathbb N\to\mathbb N$ read only on $[1..n]$, symbols are natural numbers, and \=1$. The suffix array is a hypothesis (`IsSuffixArray`: a permutation of$[1..n]$sorting the suffixes strictly), never a construction;$BWT$and$LF$are the counting formulas of p. 8, with$T[0]$read as$T[n]$.$LCP$is computed from a recursive$\operatorname{lcp}$on suffix lists;$DLCP$and$DSA$are integer-valued. A macro scheme is defined for any symbol type as a list of blocks laid out consecutively from position 1, each with a length and an optional source start; its size is the list length. Explicit blocks have length 1; a pointer block starting at$i$has a source$j\ne i$inside$[1..n]$, possibly overlapping the block. The value of$f$on explicit symbols, arbitrary on the page, is the identity. The explicit cells$p_i+k$of Lemma 17 are taken only where they exist ($\le n$), and coinciding cells of short runs are counted once; the convention$p_0=-2$only empties the region before$p_1=1$. Lemma 17 is stated as a characterisation of the scheme: explicit blocks exactly at explicit cells, pointer blocks exactly the maximal stretches of the remaining cells, each pointing to$LF$of its first cell with$LF$mapping every cell in the block to the corresponding source cell. The identity$SA[LF(p)]=SA[p]-1$carries the guard$SA[p]>1$, since for$SA[p]=1$ it holds only cyclically.

The paper's $O(\cdot)$ space and time claims (Theorem 9, Lemma 19) and the cited grammar conversion (Lemma 18) are out of scope; the goal is their explicit combinatorial content.

Every sequence has a macro scheme of size $n$ (all symbols explicit), and a set of pointers that only point at each other satisfies every local condition, so a formalization that bounds the size of an arbitrary partition, or that drops the condition that every chain of copies reaches an explicit symbol, would be empty or false; both are excluded by the definition used. $SA$, $BWT$ and $LF$ are not defined through the properties the milestones assert.

Contributions welcome: proofs of the milestones, and reusable lemmas about the LF mapping and lexicographic order of suffixes, which the paper's other missions (locating with sampled phrases, counting distinct substrings) also use.

Selected references

• T. Gagie, G. Navarro, N. Prezza, Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space, arXiv preprint, 2019 (v2). https://arxiv.org/abs/1809.02792
• J. A. Storer, T. G. Szymanski, Data compression via textual substitution, Journal of the ACM 29(4):928–951, 1982. https://doi.org/10.1145/322344.322346
• A. Abeliuk, R. Cánovas, G. Navarro, Practical compressed suffix trees, Algorithms 6(2):319–351, 2013. https://doi.org/10.3390/a6020319
• T. Gagie, G. Navarro, N. Prezza, On the approximation ratio of Lempel-Ziv parsing, Proc. LATIN 2018, LNCS 10807, pp. 490–503.
• M. Burrows, D. Wheeler, A block sorting lossless data compression algorithm, Technical Report 124, Digital Equipment Corporation, 1994.
• V. Mäkinen, G. Navarro, Succinct suffix arrays based on run-length encoding, Nordic Journal of Computing 12(1):40–66, 2005.