Formalize the proof of WOWII Conjecture 438b

## Summary

WOWII Conjecture 438b is currently marked open. It asks whether every connected graph of order greater than three satisfies

`α₂(G) ≤ α(G) + α(G[V − H₂]) + |E(G[H₂])|`,

where `H₂` is the set of vertices of degree at most two and `α₂` is the maximum order of an induced subgraph of maximum degree at most one.

The conjecture is true. The formal certificate proves the stronger inequality

`α₂(G) ≤ α(G) + α(G[V − H]) + |E(G[H])|`

for every finite simple graph and every vertex subset `H`.

## Proof idea

A 2-independent set induces a matching plus isolated vertices. Removing one endpoint from each matching edge leaves an independent set, paying at most `α(G)`.

Partition the matching edges into those wholly inside `H` and all remaining edges. The first class is bounded by `|E(G[H])|`. From every remaining edge choose an endpoint in `V − H`; because the matching is induced, the chosen endpoints form an independent set in `G[V − H]`. This pays at most `α(G[V − H])`.

Taking `H = H₂` proves the source statement. Connectivity, order, and the special degree definition of `H₂` are unnecessary.

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

This is a follow-up to the tightness/invariant-separation pattern exposed by `C₅[K₄]`. The carrier and several related graphs repeatedly attain equality in 438b. A preregistered attempt to cross the wall with low-degree false-twin layers instead exposed the edge-by-edge compensation above, turning a failed construction direction into a proof.

The derivation and exact computational audit are recorded immutably here:

https://github.com/Kuberwastaken/c5-k4/blob/57eda7b3895ed8c64971c352311df029bf86e9ed/results/expansion/method_v02_438b.md

The versioned wall-navigation method is:

https://github.com/Kuberwastaken/c5-k4/blob/020a0d18c0f4388f32aacd0e16168f89d99c4b2e/METHOD.md

## Complete formal certificate

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

https://github.com/Kuberwastaken/c5-k4/blob/e62f216625438bc099707e466d2825ab483717a4/lean/GraphConjecture438b.lean

It compiles warning-clean. Its trust assumptions are `propext`, `Classical.choice`, and `Quot.sound`; there is no `sorryAx`, native-decision trust, or project-specific axiom.

## Source/status note

The current primary WOWII page contains one 438b entry under upper bounds on 2-independence and marks it `O`. The `α₂`, `α`, and `H₂` notation in the formalization matches the source definitions.

The stronger arbitrary-`H` inequality is also an immediate consequence of the published 2022 bound `diss(G) ≤ α(G) + ν_s(G)` by splitting an induced matching across `H`. Accordingly, this submission claims a complete Lean proof/formalization of a source-listed-open entry, not a novel mathematical theorem or first-ever solution. The full source/status/priority audit is:

https://github.com/Kuberwastaken/c5-k4/blob/841ab2078e37c0bc8f14ae9696f0e91c1f76f3a1/results/expansion/wowii_438b_status_audit.md

## AI assistance disclosure

OpenAI Codex and delegated coding agents assisted with theorem discovery, source/status research, proof development, independent verification, and submission preparation. The submitter reviewed the mathematical statement, proof, literature qualification, and Lean artifact and takes responsibility for the submission.

Start by reading the referenced lean/GraphConjecture438b.lean certificate and the linked status audit, then inspect how the formal-conjectures repository organizes and verifies comparable formalizations. Confirm the theorem statement and source status, and verify that the submitted certificate compiles without sorry or project-specific axioms.

Written by the indexing model from the issue text.