Formalize the disproof of WOWII Conjecture 176

## Summary

WOWII Conjecture 176 is currently listed as open. Under the source-faithful reading

`Ls(G) + b(G) ≥ n(G) + dist_min(G, M(G²))`,

where `M(G²)` is selected in the square but `dist_min` is measured back in
`G`, the conjecture is false.

## Counterexample

Let `D₇` consist of two triangles whose distinguished vertices are joined by
a path of seven edges. The formally certified bounds and values are:

- `n(D₇) = 12`;
- `Ls(D₇) ≤ 4`;
- `b(D₇) = 10`;
- `M(D₇²) = {p₁,p₆}`;
- `dist_D₇(p₁,p₆) = 5`.

Thus the proposed inequality would imply `14 ≥ 17`.

This witness is independent of the main notation ambiguity. Measuring the
distance in `D₇²` instead gives `3`, and hence the still-false inequality
`14 ≥ 15`.

## Relationship to the C₅[K₄] campaign

This is a direct follow-up to the tightness/invariant-separation pattern
exposed by `C₅[K₄]`. On the original diameter-two carrier family,
Conjecture 176 repeatedly sits at equality because it collapses to the known
`Ls+b ≥ n+1` wall. The obstruction was removed by leaving diameter two while
keeping `Ls` pinned and forcing the maximum-degree vertices of the square far
apart.

The derivation and exact computational audit are recorded immutably here:

https://github.com/Kuberwastaken/c5-k4/blob/9bfc0586e7afcf3708aea5fe878346d72e266196/results/expansion/wowii_176_disproof.md#L1-L39

The broader structural-transfer account is:

https://github.com/Kuberwastaken/c5-k4/blob/37f93e1504d8bb732007a04a00add00749c7b3f5/README.md#L157-L184

## Complete formal certificate

The no-`sorry` Lean 4 certificate is available at:

https://github.com/Kuberwastaken/c5-k4/blob/b0ba2b9206176b4fc30bd633de206ac230b4e01f/lean/GraphConjecture176.lean#L1-L377

It compiles warning-clean. `#print axioms` reports `propext`,
`Classical.choice`, `Lean.ofReduceBool`, `Lean.trustCompiler`, and `Quot.sound`;
there is no `sorryAx` or project-specific axiom.

## Reading note

The source defines `dist_min(S)` using distances in `G`. Accordingly, the
declaration selects `M(G²)` by square degree and then evaluates `distMin G`
on that set. The alternative all-in-`G²` reading is not submitted as the
historical statement, but `D₇` refutes it too.

## AI assistance disclosure

OpenAI Codex and delegated coding agents assisted with source interpretation,
proof development, independent verification, and submission preparation. The
submitter reviewed the mathematical statement, counterexample, and Lean
artifact and takes responsibility for the submission.

Read the formal conjecture declaration in the repository and compare its distance convention with the D₇ counterexample. Then inspect the linked results/expansion/wowii_176_disproof.md and lean/GraphConjecture176.lean artifacts, and run the cited Lean certificate. Done means the repository records the disproof or corrects the conjecture with a verified, warning-clean formalization.

Written by the indexing model from the issue text.