Written on the Wall II - Conjecture 100

Verbatim statement (WOWII #100, status O):

If G is a simple connected graph, then α(G) ≤ CEIL[(maximum of λ(v) + 0.5*length(Ḡ))/2]

Source: http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj100

The WOWII HTML uses length(Ḡ) (the bar denotes graph complement); the extracted JSON in our private repo previously dropped the overline. The formal statement below uses the diameter of Gᶜ.

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

Definitional choice

DeLaVina does not give a stand-alone definition for length(H) on the WOWII page. We interpret it as the diameter of H (the maximum eccentricity, i.e. H.ediam), which is the most natural graph-theoretic notion of "length" of a graph. Combined with the overline above, the inequality reads: α(G) ≤ ⌈(max_v l(v) + 0.5 · diam(Gᶜ)) / 2⌉ where l(v) = indepNeighbors G v and diam(Gᶜ) = Gᶜ.ediam.toNat.

Connectedness of the complement

When Gᶜ is disconnected, Gᶜ.ediam = ⊤ and Gᶜ.ediam.toNat = 0, so the right-hand side silently degenerates to ⌈max_v l(v) / 2⌉ — a much weaker (and often vacuously false) statement than the conjecture intends. We therefore add the hypothesis hGc : Gᶜ.Connected so the inequality is genuinely about a finite length(Ḡ) = diam(Gᶜ).

theorem WrittenOnTheWallII.GraphConjecture100.conjecture100 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) (hGc : Gᶜ.Connected) : have maxL := (Finset.image G.indepNeighborsCard Finset.univ).max' ⋯; ↑G.indepNum ≤ ↑⌈(↑maxL + 1 / 2 * Gᶜ.degreeL2Norm) / 2⌉

WOWII Conjecture 100 (status O):

For a simple connected graph G, α(G) ≤ ⌈(max_v l(v) + 0.5 · diam(Gᶜ)) / 2⌉ where α(G) = G.indepNum is the independence number, max_v l(v) is the maximum over all vertices of the independence number of the neighbourhood (in G), and diam(Gᶜ) is the diameter of the complement Gᶜ.

Note: length(Ḡ) in DeLaVina's original is interpreted here as the diameter of the complement. The hypothesis hGc : Gᶜ.Connected is added so that diam(Gᶜ) is finite (otherwise Gᶜ.ediam = ⊤ and Gᶜ.ediam.toNat collapses silently to 0); see the module docstring above.