Written on the Wall II - Conjecture 314

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

noncomputable def WrittenOnTheWallII.GraphConjecture314.largestInducedPathSize {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ

The size of a largest induced path of $G$, as a natural number.

A subset $s \subseteq V(G)$ is an induced path when the induced subgraph G.induce s is a tree in which every vertex has degree at most $2$ (equivalently: a tree that is itself a path graph). We define largestInducedPathSize G as the supremum of s.card over all such subsets.

Disambiguation. This is not the SimpleGraph.path invariant, which is the floor of the average distance — that one is the wrong tool for WOWII Conjecture 314, where $\mathrm{path}(G)$ denotes the size of a largest induced path.

TODO: it would probably be clearer to rename the SimpleGraph.path invariant to something like pathBound / floorAvgDist to avoid this naming collision.

Equations

• One or more equations did not get rendered due to their size.

theorem WrittenOnTheWallII.GraphConjecture314.conjecture314 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Connected) (hTriFree : ∀ (a b c : α), G.Adj a b → G.Adj b c → G.Adj c a → False) (hPath : largestInducedPathSize G ≤ 4) : G.IsWellTotallyDominated

WOWII Conjecture 314:

For every finite simple connected graph $G$ with $n > 1$ vertices, if $G$ is triangle-free and $\mathrm{path}(G) \le 4$, then $G$ is well totally dominated.

Here $\mathrm{path}(G) = \mathrm{largestInducedPathSize}\, G$ is the size of a largest induced path in $G$, defined locally above.

Disambiguation. Earlier revisions of this file used the SimpleGraph.path invariant, but that is the floor of the average distance, not the size of a largest induced path — a different quantity that makes Conjecture 314 vacuous in many cases.