Formalize the disproof of WOWII Conjecture 172

## Summary

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

`Ls(G) ≥ -1 + Δ(B(G)) + dist_min(G, M(G²))`,

where `B(G)` is the periphery, `Δ(B(G))` measures the original-graph degrees
of its vertices, and `M(G²)` is selected in the square while `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 nine edges. The formally certified bounds and values are:

- `Ls(D₉) ≤ 4`;
- the peripheral vertices have maximum original-graph degree `2`;
- `M(D₉²) = {p₁, p₈}`;
- `dist_D₉(p₁,p₈) = 7`.

Thus the conjecture would imply `4 ≥ -1 + 2 + 7 = 8`.

The same witness removes the natural notation ambiguity: measuring the last
distance in `D₉²` gives distance `4`, and the still-false inequality
`4 ≥ -1 + 2 + 4 = 5`.

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

This is a follow-up to the tightness/invariant-separation pattern exposed by
`C₅[K₄]`. Exploration of the carrier's exact `Ls` walls led first to the
two-triangles-and-a-path family for Conjecture 176; evaluating the adjacent
wall then produced this disproof of 172.

The derivation and exact computational audit are recorded immutably here:

https://github.com/Kuberwastaken/c5-k4/blob/bf10abe232b96d98db895a879d25a1343ccd5c77/results/expansion/wowii_172_disproof.md#L1-L30

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/a948106ad2d2a5d291b6b99575fe78bf373e7e02/lean/GraphConjecture172.lean#L1-L384

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

`Δ(B)` is formalized as the maximum degree in `G` among the
maximum-eccentricity vertices of `G`; it is not the maximum degree of an
induced periphery graph. Likewise, the source definition of `dist_min`
measures distance in `G`, even though the selected set is `M(G²)`.

## 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 Lean certificate at lean/GraphConjecture172.lean and the disproof derivation in results/expansion/wowii_172_disproof.md. Verify how the certificate relates to this repository's formal conjecture, then identify the repository change needed to record the disproof; done means the formal statement is updated with a warning-clean, no-sorry verification.

Written by the indexing model from the issue text.