WOWII/GraphConjecture34: statement uses maxEccentricityVertices (B) instead of max-degree vertices (M)

[henrykmichalewski]

Problem

FormalConjectures/WrittenOnTheWallII/GraphConjecture34.lean formalizes Conjecture 34 of WOWII incorrectly:

WOWII source

The WOWII website states Conjecture 34 as:

If G is a simple connected graph, then path(G) ≥ CEIL[dist_avg(C,V) + dist_avg(M,V)]

Where

• C = centers (min-eccentricity vertices) — already graphCenter in the project
• M = max-degree vertices — this is the set intended
• path(G) = size of the longest induced path (largestInducedPath / path in the project)

Current Lean

theorem conjecture34 [Nontrivial α] (G : SimpleGraph α) (h_conn : G.Connected) :
    Int.ceil (distavg G (graphCenter G) + distavg G (maxEccentricityVertices G)) ≤ (path G : ℤ) := by
  sorry

The statement uses maxEccentricityVertices G — this is the boundary set B (vertices achieving max eccentricity), not M (vertices of max degree). These are different vertex sets in general.

The docstring also contains a subtle misstatement:

"Let path(G) be the floor of the average distance of a connected graph G."

path(G) in WOWII is the longest induced path, not the floor of the average distance.

Suggested fix

Replace maxEccentricityVertices G with the set of max-degree vertices. A minimal fix:

/--
WOWII [Conjecture 34](http://cms.uhd.edu/faculty/delavinae/research/wowII/)

Let `path(G)` be the size of the longest induced path of a connected graph `G`,
and let `C` be the set of centers (minimum-eccentricity vertices) and `M` the
set of vertices of maximum degree. Then
`path(G) ≥ CEIL[ distavg(C,V) + distavg(M,V) ]`.
-/
@[category research open, AMS 5]
theorem conjecture34 [Nontrivial α] (G : SimpleGraph α) (h_conn : G.Connected) :
    let M : Finset α := Finset.univ.filter (fun v => G.degree v = G.maxDegree)
    Int.ceil (distavg G (graphCenter G) + distavg G (↑M : Set α)) ≤ (path G : ℤ) := by
  sorry

(Or add maxDegreeVertices G to Invariants.lean alongside maxEccentricityVertices.)

Origin

I discovered this while auditing my own PRs (#3795, #3796, and a staging branch) — we had a similar off-by-one / vertex-set-confusion pattern. The upstream file appears to have the same root cause.

Happy to submit a PR if this fix looks right.