FormalConjectures/WrittenOnTheWallII/GraphConjecture194.lean

GitHub source file

3 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 194

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

Counterexample

The conjecture is false. Take a clique on vertices 0, ..., 10, four additional vertices 11, ..., 14 adjacent to every clique vertex, and three leaves attached at 11, 12, and 14. This connected graph has independence number 4, while the sum of the independence numbers of its vertex neighbourhoods is 54, so their average is 3. Thus it satisfies the conjecture's hypothesis with equality. However, its three leaves would all have to be endpoints of a Hamiltonian path, which is impossible.

Imports (1)
  1. theorem WrittenOnTheWallII.GraphConjecture194.conjecture194 sorry line 57 source

    depends on sorry what this means

    Statement uses: Iff, False, Fintype, DecidableEq, Nontrivial, SimpleGraph, SimpleGraph.Connected, LE.le, Real, SimpleGraph.indepNum, HAdd.hAdd, OfNat.ofNat, SimpleGraph.averageIndepNeighbors, Exists, SimpleGraph.Walk, SimpleGraph.Walk.IsHamiltonian

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

  2. example WrittenOnTheWallII.GraphConjecture194.(example at line 68) line 68 source

    Source documentation

    The average indep-neighbors invariant l G is nonneg.

    example (G : SimpleGraph (Fin 3)) : 0 ≤ averageIndepNeighbors G := by
…
  3. example WrittenOnTheWallII.GraphConjecture194.(example at line 77) line 77 source

    Source documentation

    The edgeless graph on 2 vertices has 2 vertices.

    example : Fintype.card (Fin 2) = 2 := by decide
…