Written on the Wall II - Conjecture 133

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

theorem WrittenOnTheWallII.GraphConjecture133.conjecture133 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) : have rad := G.radius.toNat; let hasC4 := ∃ (a : α) (b : α) (c : α) (d : α), a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d ∧ G.Adj a b ∧ G.Adj b c ∧ G.Adj c d ∧ G.Adj d a; have cC4 := if hasC4 then 0 else 1; ↑rad + ↑⌊G.l⌋ ^ cC4 ≤ ↑G.path

WOWII Conjecture 133:

For a simple connected graph $G$, $\operatorname{path}(G) \ge \operatorname{rad}(G) + \lfloor \mathrm{avg}_v\, l(v) \rfloor^{cC_4(G)}$, where $\operatorname{path}(G)$ is the path number of the graph (number of vertices of a largest induced path), $\operatorname{rad}(G)$ is the radius (minimum eccentricity, as a natural number), $\mathrm{avg}_v\, l(v) = l(G)$ is the average independence number of vertex neighbourhoods, and $cC_4(G)$ is the $C_4$-free characteristic function (1 if $G$ is $C_4$-free, not necessarily induced, and 0 otherwise).

We read DeLaVina's bracket notation [average of λ(v)] in the source as the floor (a standard Graffiti.pc convention), hence ⌊l G⌋ in Lean.