Formalize the disproof of WOWII Conjecture 430a

## Summary

WOWII Conjecture 430a is currently listed as open. It asserts that every
connected graph of order greater than three satisfies

`i(G) ≤ α(G[N(C)]) + 2 floor(CW(G)-1)`,

where `C` is the center, `N(C)` is the union of the open neighborhoods of the
vertices in `C`, and `CW(G) = Σ_v 1/(degree(v)+1)`. The conjecture is false.

## Counterexample

Take the nonuniform clique blow-up of `P₇` with blob orders
`(1,4,12,19,12,4,1)`. The formally certified values are:

- `|V| = 53`;
- `i(G) = 3`;
- the center is the middle `K₁₉`;
- `α(G[N(C)]) = 2`;
- `CW(G) = 51123/25585 < 2`, so `floor(CW(G)-1) = 0`.

Thus the conjecture asserts `3 ≤ 2`.

Uniformly scaling all seven blob orders preserves these controlling
invariants, giving an infinite counterexample family.

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

This is a follow-up to the tightness/invariant-separation pattern exposed by
`C₅[K₄]`, now in a substantially different independent-domination cluster.
The regular carrier was tight because its center was all of `V`. The
nonuniform path blow-up separates the controlling invariants: eccentricity
asymmetry pins the center to one middle clique, while the blob weights keep
the Caro--Wei sum immediately below its integer cliff at `2`.

This is the second clean instance of the discovery pattern

`tight wall → identify obstruction → separate invariant → cross`.

The derivation and exact audit are recorded immutably here:

https://github.com/Kuberwastaken/c5-k4/blob/8d48fbdf45301afb57f9d4d5627f5b984f385089/results/expansion/wowii_430a_disproof.md#L1-L69

The broader structural-transfer account is:

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

## Complete formal certificate

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

https://github.com/Kuberwastaken/c5-k4/blob/85fff48cdd7cc1f743802320fdc94db14d1f841e/lean/GraphConjecture430a.lean#L1-L390

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.

## Neighborhood convention

DeLaViña defines `N(S)` as the union of the open vertex neighborhoods, not
the external boundary `N(S) \ S`. Because the center here is a clique, center
vertices themselves belong to `N(C)`. The formalization preserves this convention.

## 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.

Start by reading the linked expansion/wowii_430a_disproof.md audit and lean/GraphConjecture430a.lean certificate, then inspect how formal-conjectures records and validates conjectures. Done means the disproof is represented and verified in the repository's expected Lean structure, with the certificate compiling cleanly and no unsupported gaps.

Written by the indexing model from the issue text.