Proposed proof of source-corrected WOWII Conjecture 160

## Summary

I am submitting an AI-assisted candidate proof of the **source-corrected**
Written on the Wall II Graph Conjecture 160 for independent mathematical
review and possible Lean formalization.

The source correction is tracked in #4423 and PR #4443. In that corrected
statement, $\chi_{C_4}(G)$ is the binary $C_4$-free characteristic: it is
$1$ when $G$ contains no 4-cycle as a subgraph and $0$ otherwise. The
cycle need not be induced.

The candidate theorem is

$$
L_s(G)\ge \max_v\lambda(v)+\max_vT(v)\,\chi_{C_4}(G),
$$

where $\lambda(v)=\alpha(G[N(v)])$.

## Permanent proof package

The proof and verifier are published at permanent commit
[`42878d6c04ec2115e31c01c8e7433da0c07070b4`](https://github.com/vulnix0x4/wowii-conjecture-160/tree/42878d6c04ec2115e31c01c8e7433da0c07070b4):

- [Proof PDF](https://github.com/vulnix0x4/wowii-conjecture-160/blob/42878d6c04ec2115e31c01c8e7433da0c07070b4/proof/WOWII_Conjecture_160_proof.pdf)
- [Proof in Markdown](https://github.com/vulnix0x4/wowii-conjecture-160/blob/42878d6c04ec2115e31c01c8e7433da0c07070b4/proof/WOWII_Conjecture_160_proof.md)
- [LaTeX source](https://github.com/vulnix0x4/wowii-conjecture-160/blob/42878d6c04ec2115e31c01c8e7433da0c07070b4/proof/WOWII_Conjecture_160_proof.tex)
- [Constructive verifier](https://github.com/vulnix0x4/wowii-conjecture-160/blob/42878d6c04ec2115e31c01c8e7433da0c07070b4/verification/verify_wowii160.py)
- [Recorded verification output](https://github.com/vulnix0x4/wowii-conjecture-160/blob/42878d6c04ec2115e31c01c8e7433da0c07070b4/verification/verification_output.txt)

## Proof outline

The proof is constructive.

1. Any tree subgraph of a connected graph can be extended to a spanning tree
without decreasing its number of leaves.
2. If $G$ is $C_4$-free, every open neighborhood is a matching together
with isolated vertices. Consequently,
$d(v)=\lambda(v)+T(v)$ and $\lambda(v)\ge T(v)$.
3. Choose $x$ maximizing $\lambda$ and $y$ maximizing $T$. Two full
stars joined by a geodesic give the required number of leaves in the
general case. The adjacent cases and one exceptional degree-two triangle
case are handled separately.
4. If $G$ contains a 4-cycle, the characteristic term vanishes and a star
formed from a maximum independent set in $G[N(x)]$ gives the bound.

## Computational audit

The accompanying Python program implements the proof's construction; it does
not optimize $L_s$. I reran it independently with NetworkX 3.6.1. It passed:

- all 995 connected unlabeled graphs of orders 2 through 7 in the NetworkX
graph atlas;
- 4,997 deterministic random connected graphs of orders up to 20.

All construction cases in the proof were exercised. This audit is supporting
evidence, not a substitute for proof review.

## Review requested

Could maintainers or graph theorists review the mathematical argument and
confirm that it matches the intended source-corrected invariant? I would also
appreciate guidance on whether a Lean formalization should be completed before
proposing that Conjecture 160 be marked `research solved`.

I am **not** asking to change the status in this issue, and I am not claiming
that the result has been accepted or that historical priority has been
established.

## AI assistance disclosure

OpenAI models assisted with proof search, case analysis, computational
verification, and preparation of the write-up and submission. The proof
package should receive normal independent mathematical and formal review.

Read proof/WOWII_Conjecture_160.md and proof/WOWII_Conjecture_160.tex first, then run verification/verify_wowii160.py and inspect verification/verification_output.txt. Compare the source-corrected invariant and proof cases against the requested independent review; done means a mathematical review is provided or guidance is given on completing Lean formalization.

Written by the indexing model from the issue text.