Complete formal certification for the disproof of WOWII Conjecture 59

## Summary

WOWII Graph Conjecture 59 (`f(G) ≥ ⌈√(residue(G) · b(G))⌉` for connected graphs) is false, and
this issue tracks a **complete in-file Lean certification** of that fact via an 18-vertex
counterexample, in the style of #4482 / #4542: every invariant of the witness is machine-checked,
with no informal steps.

## Relationship to existing work

#4573 / #4574 (@QDKStorm) publicly reported a counterexample to this conjecture earlier today,
via a 123-vertex construction with an infinite family. This issue makes **no priority claim on
the mathematical disproof** — that public claim came first. The PR attached here is offered as a
complementary completion of the formal record:

- the witness here is independent and smaller (18 vertices), found by a separate search;
- **all five certified facts live in Lean**: connectedness, `residue = 10`, `b = 17`
(both directions), `largestInducedForestSize = 13` (both directions), and the final
`⌈√170⌉ = 14 > 13` contradiction — including the two invariants (`b`, `f`) that are
infeasible to certify by decision procedures at 123 vertices;
- the proof follows the reviewed #4482 / #4542 shape: `answer(False) ↔ ∀ …`,
`@[category research solved]`, explicit checked counterexample lemmas, complete in-file proof.

If maintainers prefer to resolve the conjecture through #4574, this certification can equally
serve as supporting reference material; the two are not in conflict about the mathematics.

## Certified statement

The 18-vertex witness: a bipartite chain-graph core on `{0, …, 9}` (parts `{0, …, 4}`,
`{5, …, 9}`), a universal hub `10`, and seven pendant leaves at the hub. Then
`residue = 10`, `b = 17`, `f = 13`, and `10 · 17 = 170 = 13² + 1`, so
`⌈√170⌉ = 14 > 13`.

`#print axioms` for the final theorem and every invariant lemma:
`[propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound]` — no `sorryAx`,
no custom axioms. (`Lean.ofReduceBool`/`Lean.trustCompiler` come from `native_decide`, as in
the reviewed #4482 pattern.)

## AI assistance disclosure

Claude (Anthropic) carried out the counterexample search, invariant verification, Lean proof
engineering, and drafting under my direction; I reviewed the mathematical argument and the
reproducible outputs.

Locate the existing WOWII Conjecture 59 declaration and compare its proof structure with #4482 and #4542. Formalize the stated 18-vertex witness and check connectedness, residue = 10, b = 17, largestInducedForestSize = 13, and the final ceiling-square-root contradiction in Lean. Done means the complete in-file certification has no informal steps or sorryAx and the listed axioms are reported.

Written by the indexing model from the issue text.