# An infinite family of counterexamples to WOWII Conjecture 109

[![Verify certificates](https://github.com/chelokot/wowii-109-counterexample/actions/workflows/verify.yml/badge.svg)](https://github.com/chelokot/wowii-109-counterexample/actions/workflows/verify.yml)

> [!IMPORTANT]
> **AI provenance:** Essentially all technical work in this repository—the search, counterexample family, proof, Lean formalization, verification code, and write-up—was produced by **GPT-5.6 Sol Max in Codex**. [Andrii Vlasenko](https://github.com/chelokot) initiated and directed the investigation and publishes the repository.

Written on the Wall II Conjecture 109 proposes that every finite simple connected graph $G$ satisfies

$$
\alpha(G)\le
\left\lfloor\frac{\mathrm{res}(G)+2b(G)}{3}\right\rfloor,
$$

where $\alpha(G)$ is the independence number, $b(G)$ is the largest order of an induced bipartite subgraph, and $\mathrm{res}(G)$ is the Havel--Hakimi residue.

The conjecture is false. For every $r\ge3$, let

$$
G_r=\overline K_{2r+1}\vee(K_r\sqcup K_r).
$$

Then

$$
\alpha(G_r)=2r+1,\qquad b(G_r)=2r+3,\qquad \mathrm{res}(G_r)=2,
$$

and therefore

$$
\left\lfloor\frac{\mathrm{res}(G_r)+2b(G_r)}3\right\rfloor
=\left\lfloor\frac{4r+8}{3}\right\rfloor
<2r+1=\alpha(G_r).
$$

The smallest member of this family is

$$
G_3=\overline K_7\vee(K_3\sqcup K_3)
=\overline{K_7\sqcup K_{3,3}}.
$$

It has 13 vertices, 48 edges, graph6 encoding `L???F~~~~{^p~b`, and exact invariants

| invariant | value |
|---|---:|
| $\alpha(G_3)$ | 7 |
| $b(G_3)$ | 9 |
| $\mathrm{res}(G_3)$ | 2 |
| proposed upper bound | 6 |

The complete mathematical argument, including the symbolic residue calculation for the infinite family, is in [PROOF.md](PROOF.md).

## Verification

The self-contained Python verifier exhaustively checks all $2^{13}$ vertex subsets:

```sh
python3 verify_counterexample.py
```

The independent C++20 verifier performs the same exact calculation:

```sh
c++ -std=c++20 -O2 -Wall -Wextra -Wpedantic verify_counterexample.cpp -o verify_counterexample
./verify_counterexample
```

The family/minimality audit checks the formulas through $r=100$ and exhausts every cluster-join graph
$\overline K_a\vee\left(\bigsqcup_iK_{r_i}\right)$ of order at most 13:

```sh
python3 verify_family.py
```

The Lean 4 certificate is [lean/GraphConjecture109.lean](lean/GraphConjecture109.lean). It was checked against `google-deepmind/formal-conjectures` at commit `b8b5208` with Lean 4.27.0:

```sh
cp lean/GraphConjecture109.lean \
  /path/to/formal-conjectures/FormalConjectures/WrittenOnTheWallII/
cd /path/to/formal-conjectures
lake --wfail build FormalConjectures/WrittenOnTheWallII/GraphConjecture109.lean
```

## Status and novelty

As of 21 July 2026, the [official WOWII list](http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html) still marks Conjecture 109 open, and the [formal-conjectures entry](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/WrittenOnTheWallII/GraphConjecture109.lean) is tagged `research open`. Searches of the official page, GitHub, and the literature found no earlier resolution of this exact conjecture. That is an evidence-based novelty check, not a guarantee that no unpublished or unindexed observation exists.

## Scope

The 13-vertex example is the unique counterexample, up to ordering of the clique blocks, among graphs
$\overline K_a\vee\left(\bigsqcup_iK_{r_i}\right)$ on at most 13 vertices. This repository does not claim that 13 is globally minimal among all connected graphs.