/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Written on the Wall II - Conjecture 200

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Counterexample

For every integer $q \geq 5$, let $C = {a,b} \cup D$ have $q$ vertices and induce $K_q$ minus the edge $ab$. Add two nonadjacent vertices $x,y$, each complete to $C$; a vertex $z$ adjacent exactly to $a,b$; and, for every $d \in D$, a pendant vertex $p_d$ adjacent exactly to $d$.

The local-neighbourhood independence numbers are $2$ at $x,y,z$, $1$ at each $p_d$, and $3$ at every vertex of $C$. Their sum is $4q+4$, while the graph has $2q+1$ vertices, so $$\left\lceil 1 + l_{\mathrm{avg}}(G)\right\rceil = 4.$$ The vertices ${a,x,y,z}$ induce a claw, and a case split on the number of vertices from $C$ shows that no induced tree has more than four vertices. Thus $\operatorname{tree}(G)=4$. Finally, the graph has $q-2 \geq 3$ pendant vertices, but a Hamiltonian path has only two endpoints.

The smallest member of this family has 11 vertices and graph6 encoding J??FFBRq}N_. This is a smallest counterexample overall: an exhaustive search over all 11,989,760 connected graphs on 4 ≤ n ≤ 10 vertices (via nauty's geng; graphs on at most 3 vertices are trivially traceable) found no graph satisfying the premise without a Hamiltonian path.

namespace WrittenOnTheWallII.GraphConjecture200open SimpleGraph

WOWII Conjecture 200

For a simple connected graph G, if tree(G) = ⌈1 + l_avg(G)⌉, then G has a Hamiltonian path. Here tree(G) is the number of vertices of a largest induced tree subgraph, and l_avg(G) = averageIndepNeighbors G is the average over all vertices of the independence number of the neighbourhood. A Hamiltonian path is a walk visiting every vertex exactly once.

This conjecture is false. The counterexample family in the module docstring satisfies the equality hypothesis and has no Hamiltonian path.

@[category research solved, AMS 5, formal_proof using formal_conjectures at "https://github.com/infinityscroll/formal-conjectures/blob/9dd290db402c49922fa42793e4a7cfb802daf5c1/FormalConjectures/WrittenOnTheWallII/GraphConjecture200Counterexample.lean#L24-L195"] theorem conjecture200 : answer(False) (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) (_h : G.Connected), (largestInducedTreeSize G : ) = 1 + averageIndepNeighbors G a b : α, p : G.Walk a b, p.IsHamiltonian := False (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α), G.Connected G.largestInducedTreeSize = 1 + G.averageIndepNeighbors a b p, p.IsHamiltonian All goals completed! 🐙-- Sanity checks

The largestInducedTreeSize is nonneg.

@[category test, AMS 5] example (G : SimpleGraph (Fin 3)) : 0 largestInducedTreeSize G := Nat.zero_le _

The average indep-neighbors is nonneg.

@[category test, AMS 5] example (G : SimpleGraph (Fin 3)) : 0 averageIndepNeighbors G := G:SimpleGraph (Fin 3)0 G.averageIndepNeighbors G:SimpleGraph (Fin 3)0 (∑ v, G.indepNeighbors v) / (Fintype.card (Fin 3)) G:SimpleGraph (Fin 3)0 v, G.indepNeighbors vG:SimpleGraph (Fin 3)0 (Fintype.card (Fin 3)) G:SimpleGraph (Fin 3)0 v, G.indepNeighbors v G:SimpleGraph (Fin 3) i Finset.univ, 0 G.indepNeighbors i; G:SimpleGraph (Fin 3)v:Fin 3a✝:v Finset.univ0 G.indepNeighbors v; All goals completed! 🐙 G:SimpleGraph (Fin 3)0 (Fintype.card (Fin 3)) All goals completed! 🐙end WrittenOnTheWallII.GraphConjecture200