A short proof candidate for Graffiti.pc Conjecture 143

graffiti-pc-conjecture-143.md

A Short Proof of Graffiti.pc Conjecture 143

Status: Proof candidate pending independent expert review. No claim of publication priority is made.

Abstract

Graffiti.pc Conjecture 143 asserts that if $G$ is a finite simple connected graph that is not a tree, then

t(G) ≥ (g(G) + 1) / σ(G).

where $t(G)$ is the maximum order of an induced tree, $g(G)$ is the girth, and $\sigma(G)$ is the second entry of the nondecreasing degree sequence. We give an elementary proof. The only non-immediate case is $\sigma(G)=1$. For that case, we prove that every connected cyclic graph with at least two leaves has an induced tree on at least $g(G)+1$ vertices.

1. Statement and definitions

All graphs in this note are finite and simple. Let $G$ be connected and contain a cycle. Write its degree sequence, with multiplicity, as

d₁ ≤ d₂ ≤ ⋯ ≤ dₙ,

and define

σ(G) = d₂.

Thus $\sigma(G)$ is the second-smallest degree, counting repeated degrees. Let $g(G)$ be the length of a shortest cycle in $G$, and let $t(G)$ be the maximum number of vertices in a vertex-induced subgraph of $G$ that is a tree.

The conjecture is equivalently the denominator-free inequality

t(G) σ(G) ≥ g(G) + 1.   (1)

The historical statement and definitions appear in Douglas West's Graffiti.pc registry and Ermelinda DeLaViña's Written on the Wall II registry. The original WOWII definition list defines tree(G) as the number of vertices in a largest induced tree and $\sigma(G)$ as the second entry in the ordered degree sequence.¹

2. A non-cut-vertex lemma

We use the following elementary observation.

Lemma 1. Every connected graph containing a cycle has at least three vertices that are not cut vertices.

Proof. Consider the block-cut tree of the graph. If it consists of a single block, that block is cyclic and has at least three vertices, and none of its vertices is a cut vertex.

Otherwise, every leaf block contains at most one cut vertex and therefore contains at least one vertex that is not a cut vertex of the graph. If the block-cut tree has at least three leaf blocks, these give three distinct non-cut vertices.

It remains to consider the case of exactly two leaf blocks. The block-cut tree is then a path. Since the graph contains a cycle, one of its blocks, say $B$, is cyclic and hence has at least three vertices. If $B$ is internal in the block-cut path, it contains at most two cut vertices. It therefore supplies a non-cut vertex in addition to one from each leaf block. If $B$ is itself a leaf block, it contains at most one cut vertex and consequently supplies at least two non-cut vertices; the other leaf block supplies a third. $\square$

3. The two-leaf lemma

Lemma 2. Let $G$ be connected and contain a cycle. If $G$ has at least two leaves, then

t(G) ≥ g(G) + 1.

Proof. Choose two distinct leaves $a$ and $b$. Among all subsets $X\subseteq V(G)$ such that

1. $a,b\in X$;
2. the induced subgraph $G[X]$ is connected; and
3. $G[X]$ contains a cycle,

choose one that is inclusion-minimal. Such a set exists because $X=V(G)$ is eligible. Put $H=G[X]$.

The vertices $a$ and $b$ are leaves of $H$, so neither is a cut vertex of $H$. By Lemma 1, $H$ has at least three non-cut vertices. Hence there is a non-cut vertex

w ∉ {a, b}.

Because $w$ is not a cut vertex, $H-w$ is connected. It cannot contain a cycle: otherwise $X\setminus{w}$ would be a smaller eligible set, contradicting the minimality of $X$. Therefore $H-w$ is connected and acyclic. It is induced in $G$, so it is an induced tree.

The graph $H$ contains a cycle of length at least $g(G)$. Neither $a$ nor $b$ lies on a cycle, because both have degree one in $H$. Consequently

|V(H)| ≥ g(G) + 2,

and the induced tree $H-w$ has order at least $g(G)+1$. Thus $t(G)\geq g(G)+1$. $\square$

4. Proof of the conjecture

Theorem. If $G$ is a finite simple connected graph containing a cycle, then

t(G) σ(G) ≥ g(G) + 1.

Proof. Since $G$ is connected and has at least three vertices, $\sigma(G)\geq1$. We divide into two cases.

Suppose first that $\sigma(G)=1$. The second entry of the degree sequence is one, so $G$ has at least two leaves. Lemma 2 yields

t(G) σ(G) = t(G) ≥ g(G) + 1.

Now suppose that $\sigma(G)\geq2$. Let $C$ be a cycle of minimum length $g=g(G)$. The cycle $C$ has no chord, since a chord would produce a shorter cycle. Hence $C$ is induced. Deleting one vertex of $C$ leaves an induced path on $g-1$ vertices, and therefore

t(G) ≥ g − 1.

Every cycle in a simple graph has length at least three, so

t(G) σ(G) ≥ 2(g − 1) ≥ g + 1.

This proves (1), and division by the positive integer $\sigma(G)$ gives the original form of the conjecture. $\square$

5. Sharpness

Both cases of the proof are sharp.

For the $\sigma(G)=1$ case, begin with the cycle $C_g$ and attach two pendant vertices to one cycle vertex. The resulting graph has

σ(G) = 1 and t(G) = g + 1.

Indeed, an induced tree must omit at least one cycle vertex, while omitting a cycle vertex other than the attachment vertex produces an induced tree on $g+1$ vertices.

For the $\sigma(G)\geq2$ case, the triangle $C_3$ has

g(C₃) = 3,   σ(C₃) = 2,   t(C₃) = 2,

so equality again holds.

6. Relation to the Formal Conjectures statement

The current GraphConjecture143.lean uses Mathlib's convention that an acyclic graph has girth zero, and its theorem does not exclude trees. Thus the Lean declaration is slightly stronger in scope than the historical statement.

The additional tree case is immediate. If $G$ is a tree, then $G$ itself is an induced tree, while $g(G)=0$. Under the Lean theorem's hypothesis $\sigma(G)>0$, we have

g(G) + 1 = 1 ≤ t(G) σ(G).

Together with the theorem above, this proves the mathematical statement of the Lean declaration as well.

7. Independent finite check

As a supplementary check, the inequality and Lemma 2 were tested on every connected unlabeled graph with two through seven vertices in NetworkX's graph atlas. There are 995 such graphs, of which 971 contain a cycle. No counterexample was found. This computation is not used in the proof.

The following script reproduces the check with a current NetworkX release:

import itertools

import networkx as nx


def largest_induced_tree_size(graph):
    vertices = list(graph)
    for size in range(len(vertices), 0, -1):
        for subset in itertools.combinations(vertices, size):
            if nx.is_tree(graph.subgraph(subset)):
                return size
    return 0


graphs = [
    graph
    for graph in nx.graph_atlas_g()
    if len(graph) >= 2 and nx.is_connected(graph)
]
cyclic_graphs = [graph for graph in graphs if not nx.is_tree(graph)]

for graph in cyclic_graphs:
    girth = nx.girth(graph)
    sigma = sorted(dict(graph.degree()).values())[1]
    tree_number = largest_induced_tree_size(graph)

    assert tree_number * sigma >= girth + 1

    number_of_leaves = sum(degree == 1 for _, degree in graph.degree())
    if number_of_leaves >= 2:
        assert tree_number >= girth + 1

print(len(graphs), len(cyclic_graphs))  # 995 971

AI-assistance disclosure

This proof candidate and write-up were prepared and checked with assistance from OpenAI Codex, using the model identified by the Codex interface as GPT-5.6 Sol. The argument was audited line by line and independently checked on the finite graph atlas, but it should still receive independent human expert review before being described as an established or novel published result.

References

1. E. DeLaViña, Written on the Wall II: Conjectures of Graffiti.pc, historical registry.
2. D. B. West, Some Conjectures of Graffiti.pc (2004–07), REGS 2009 registry.
3. Google DeepMind, Formal Conjectures, GraphConjecture143.lean.

Footnotes

1. See entries 43, 48, and 65 in the original WOWII definition script. Entry 48 defines the tree number, and entry 65 defines the second-smallest degree. ↩