FormalConjectures/WrittenOnTheWallII/GraphConjecture34.lean

GitHub source file

3 declarations, 1 contain sorry, 0 declared as axioms

1. theorem WrittenOnTheWallII.GraphConjecture34.conjecture34 WOWII Conjecture 34 For a simple connected graph sorry line 52 source

   Source documentation

   WOWII Conjecture 34

   For a simple connected graph $G$, $\operatorname{path}(G) \ge \lceil \operatorname{dist}_{\operatorname{avg}}(C, V)

   • \operatorname{dist}_{\operatorname{avg}}(M, V) \rceil$, where $\operatorname{path}(G)$ is the number of vertices of a largest induced path of $G$, $C$ is the set of center vertices (those with minimum eccentricity), $M$ is the set of maximum-degree vertices, and $\operatorname{dist}\_{\operatorname{avg}}(S, V)$ is the average of all nonzero distances $\operatorname{dist}\_G(s, v)$ with $s \in S$ and $v \in V$.

   The conjecture is false. Let $G$ be the tree on $39$ vertices formed by a vertex with three pendant leaves, joined by a path of five edges to the root of a perfect binary tree of depth four. Then $\operatorname{path}(G) = 11$, while $C$ and $M$ are singletons whose distance sums are $154$ and $266$, so the bound is $\lceil (154 + 266) / 38 \rceil = 12$.

   L4DEL explanation

   WOWII Conjecture 34 For a simple connected graph $G$, $\operatorname{path}(G) \ge \lceil \operatorname{dist}\_{\operatorname{avg}}(C, V) + \operatorname{dist}\_{\operatorname{avg}}(M, V) \rceil$, where $\operatorname{path}(G)$ is the number of vertices of a largest induced path of $G$, $C$ is the set of center vertices (those with minimum eccentricity), $M$ is the set of maximum-degree vertices, and $\operatorname{dist}\_{\operatorname{avg}}(S, V)$ is the average of all nonzero distances $\operatorname{dist}\_G(s, v)$ with $s \in S$ and $v \in V$. The conjecture is false. Let $G$ be the tree on $39$ vertices formed by a vertex with three pendant leaves, joined by a path of five edges to the root of a perfect binary tree of depth four. Then $\operatorname{path}(G) = 11$, while $C$ and $M$ are singletons whose distance sums are $154$ and $266$, so the bound is $\lceil (154 + 266) / 38 \rceil = 12$.

   Sources and attribution: Pinned Lean source (1646ca16afd6)

   depends on sorry what this means

   Statement uses: Iff, False, Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, Set, SimpleGraph.center, Set.ofPred, Eq, Nat, SimpleGraph.degree, Membership.mem, SimpleGraph.neighborSet, SimpleGraph.maxDegree, Real, Finset and 19 more

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

   40 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

   theorem conjecture34 :
     answer(False) ↔
       ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
         (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected),
         let C : Set α := center G
   …

2. example WrittenOnTheWallII.GraphConjecture34.(example at line 69) line 69 source

   Source documentation

   The path G invariant is nonneg when cast to ℤ.

   example (G : SimpleGraph (Fin 3)) : 0 ≤ (path G : ℤ) := Int.natCast_nonneg _
   …

3. example WrittenOnTheWallII.GraphConjecture34.(example at line 73) line 73 source

   Source documentation

   The edgeless graph on 3 vertices has no edges.

   example : (⊥ : SimpleGraph (Fin 3)).edgeFinset.card = 0 := by simp
   …