Written on the Wall II - Conjecture 133

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.