GraphConjecture31.lean`

3 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 31

The WOWII page records this as Chung's theorem. This radius bound is proved in Section 2 of P. Erdős, M. Saks, and V. T. Sós, Maximum Induced Trees in Graphs, J. Combin. Theory Ser. B 41 (1986), 61–79; the authors credit Fan Chung for the proof. We state it here as a theorem; the formal proof is left as sorry pending a Lean port of the argument.

Here $\mathrm{path}(G)$ is the maximum number of vertices in an induced path, and $\mathrm{rad}(G)$ is the graph radius.

References:

Imports (1)

FormalConjecturesUtil

theorem WrittenOnTheWallII.GraphConjecture31.conjecture31 sorry line 57 source
depends on sorry what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Int, HSub.hSub, HMul.hMul, OfNat.ofNat, ENat.toNat, SimpleGraph.radius, SimpleGraph.path
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
17 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
example WrittenOnTheWallII.GraphConjecture31.(example at line 65) line 65 source
Source documentation
The path G invariant cast to ℤ is nonneg.
```
example (G : SimpleGraph (Fin 3)) : 0 ≤ (path G : ℤ) := Int.natCast_nonneg _
…
```
example WrittenOnTheWallII.GraphConjecture31.(example at line 69) line 69 source
Source documentation
The radius cast to ℤ is nonneg.
```
example (G : SimpleGraph (Fin 3)) : 0 ≤ (G.radius.toNat : ℤ) := Int.natCast_nonneg _
…
```