GraphConjecture58.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 58

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

Counterexample

The conjecture is false. A counterexample is given by taking $K_{3,3}$ (with bipartition $\{0,1,2\}$, $\{3,4,5\}$) and $K_{73}$ (on vertices $\{6,\ldots,78\}$), then adding edges between vertex $0$ and every vertex of $K_{73}$.

This graph $G$ has $n = 79$ vertices and satisfies:

$b(G) \ge 7$: the set $\{0,1,2,3,4,5,6\}$ induces a bipartite subgraph
$f(G) \le 6$: the largest induced forest has at most 6 vertices
$l_{\mathrm{avg}}(G) = 92/79$
$\lceil b(G) / l_{\mathrm{avg}}(G) \rceil \ge 7 > 6 \ge f(G)$

Imports (1)

FormalConjecturesUtil

theorem WrittenOnTheWallII.GraphConjecture58.conjecture58 sorry line 62 source
depends on sorry what this means
Statement uses: Iff, False, Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Nat, Nat.ceil, Real, HDiv.hDiv, SimpleGraph.b, SimpleGraph.l_avg, SimpleGraph.largestInducedForestSize
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
21 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.