Formalize the counterexample to WOWII Conjecture 36

WOWII Conjecture 36 is already marked `research solved`; its docstring credits
Waller (October 2003) and records a counterexample with path number `5`, radius
`3`, and one diametrical pair. The theorem itself is still closed by `sorry`,
however, and the file does not give an explicit graph.

I have an explicit 10-vertex graph with those invariants. Its eight-vertex core
is a subdivided triangle together with two vertices adjacent to all three
triangle vertices; attaching one leaf to each of those two vertices gives the
counterexample. A finite Lean check establishes connectedness, radius `3`, a
unique diametrical pair, and largest induced-path order `5`, reducing the
proposed inequality to `6 ≤ 5`.

This is a formalization of a previously known disproof, not a claim of a new
mathematical disproof or of reproducing Waller's exact original graph.

## AI assistance disclosure

OpenAI Codex assisted with the finite graph search, independent invariant
checks, Lean proof development, and preparation of the contribution.

## Planned contribution

- [x] I plan to submit the follow-up pull request.
- [ ] This issue is up for grabs.

Start with the existing WOWII Conjecture 36 theorem and its docstring, then inspect the proposed finite Lean check for the explicit graph. Done means the graph is represented formally, its connectedness, radius, unique diametrical pair, and path order are checked, and the theorem no longer uses `sorry`.

Written by the indexing model from the issue text.