FormalConjectures/WrittenOnTheWallII/GraphConjecture63.lean

GitHub source file

2 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 63

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

Counterexample

The conjecture is false for the lexicographic product $C_5[K_4]$. This graph has minimum even-distance count $9$, while its largest induced forest and largest induced bipartite subgraph both have order $4$. The conjectured lower bound is therefore $\lceil(9 + 4 + 1)/3\rceil = 5 > 4$.

Imports (1)
  1. theorem WrittenOnTheWallII.GraphConjecture63.conjecture63 sorry line 48 source

    depends on sorry what this means

    Statement uses: Iff, False, Fintype, DecidableEq, Nontrivial, SimpleGraph, SimpleGraph.Connected, Nat, Finset.min', Finset.image, SimpleGraph.distEven, Finset.univ, LE.le, Real, Int.ceil, HDiv.hDiv, HAdd.hAdd, SimpleGraph.b, OfNat.ofNat, SimpleGraph.largestInducedForestSize

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

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  2. example WrittenOnTheWallII.GraphConjecture63.(example at line 57) line 57 source

    Source documentation

    Every vertex is counted among the vertices at even distance from itself.

    example (G : SimpleGraph (Fin 3)) (v : Fin 3) : 0 < G.distEven v := by
…