FormalConjectures/WrittenOnTheWallII/GraphConjecture85.lean

GitHub source file

2 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 85

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$ and largest induced-tree order $4$. The conjectured lower bound is therefore $\lceil\sqrt{1 + 2 \cdot 9}\rceil = \lceil\sqrt{19}\rceil = 5 > 4$.

Imports (1)
  1. theorem WrittenOnTheWallII.GraphConjecture85.conjecture85 sorry line 49 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, Real.sqrt, HAdd.hAdd, OfNat.ofNat, HMul.hMul, SimpleGraph.largestInducedTreeSize

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

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. example WrittenOnTheWallII.GraphConjecture85.(example at line 59) line 59 source

    Source documentation

    The largest induced-tree order is a natural number.

    example (G : SimpleGraph (Fin 3)) : 0 ≤ G.largestInducedTreeSize := Nat.zero_le _
…