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

import FormalConjecturesUtil

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

*References:*
- [E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
- [O. Favaron, M. Mahéo, J.-F. Saclé, On the residue of a graph](https://doi.org/10.1002/jgt.3190150107)
-/

namespace WrittenOnTheWallII.GraphConjecture109

open Classical SimpleGraph

/-- An induced subgraph is bipartite exactly when its vertices admit a two-coloring. -/
@[category API, AMS 5]
theorem induce_isBipartite_iff_exists_coloring {α : Type*} [DecidableEq α]
    (G : SimpleGraph α) (s : Finset α) :
    (G.induce s).IsBipartite ↔
      ∃ c : α → Fin 2, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v := by
  constructor
  · rintro ⟨c⟩
    refine ⟨fun v => if hv : v ∈ s then c ⟨v, hv⟩ else 0, ?_⟩
    intro u hu v hv huv
    simp only [dif_pos hu, dif_pos hv]
    exact c.valid huv
  · rintro ⟨c, hc⟩
    exact ⟨Coloring.mk (fun v => c v) fun {u v} huv => hc u u.prop v v.prop huv⟩

/--
The thirteen-vertex counterexample $\overline K_7 \vee (K_3 \sqcup K_3)$.
Vertices below seven form an independent set, vertices seven through nine and
vertices ten through twelve form two disjoint triangles, and every vertex of
the independent set is adjacent to every vertex in either triangle.
-/
abbrev wowii109Counterexample : SimpleGraph (Fin 13) :=
  SimpleGraph.fromRel fun u v =>
    (u.val < 7 ∧ 7 ≤ v.val) ∨
    (v.val < 7 ∧ 7 ≤ u.val) ∨
    (7 ≤ u.val ∧ u.val < 10 ∧ 7 ≤ v.val ∧ v.val < 10) ∨
    (10 ≤ u.val ∧ 10 ≤ v.val)

instance : DecidableRel wowii109Counterexample.Adj := by
  unfold wowii109Counterexample
  infer_instance

/-- The counterexample is connected. -/
@[category test, AMS 5]
theorem wowii109Counterexample_connected : wowii109Counterexample.Connected := by
  decide +native

/-- The counterexample has independence number seven. -/
@[category test, AMS 5]
theorem wowii109Counterexample_indepNum : wowii109Counterexample.indepNum = 7 := by
  rw [indep_num_eq_computable]
  decide +native

/-- The largest induced bipartite subgraph of the counterexample has nine vertices. -/
@[category test, AMS 5]
theorem wowii109Counterexample_bipartiteSize :
    wowii109Counterexample.largestInducedBipartiteSubgraphSize = 9 := by
  have htriangle :
      ∀ s : Finset (Fin 13), 9 < s.card →
        ∃ u ∈ s, ∃ v ∈ s, ∃ w ∈ s,
          wowii109Counterexample.Adj u v ∧
          wowii109Counterexample.Adj v w ∧
          wowii109Counterexample.Adj w u := by
    decide +native
  unfold SimpleGraph.largestInducedBipartiteSubgraphSize
  apply le_antisymm
  · apply csSup_le
    · refine ⟨0, ∅, ?_, rfl⟩
      rw [induce_isBipartite_iff_exists_coloring]
      exact ⟨fun _ => 0, by simp⟩
    · rintro n ⟨s, hs, rfl⟩
      by_contra hle
      obtain ⟨u, hu, v, hv, w, hw, huv, hvw, hwu⟩ :=
        htriangle s (Nat.lt_of_not_ge hle)
      obtain ⟨c, hc⟩ := (induce_isBipartite_iff_exists_coloring _ _).mp hs
      have noTriangle :
          ∀ first second third : Fin 2,
            first ≠ second → second ≠ third → third ≠ first → False := by
        decide
      exact noTriangle (c u) (c v) (c w)
        (hc u hu v hv huv) (hc v hv w hw hvw) (hc w hw u hu hwu)
  · apply le_csSup
    · exact ⟨Fintype.card (Fin 13), fun n ⟨s, _, hs⟩ => hs ▸ s.card_le_univ⟩
    · refine ⟨{0, 1, 2, 3, 4, 5, 6, 7, 10}, ?_, by decide⟩
      rw [induce_isBipartite_iff_exists_coloring]
      refine ⟨fun v => if v.val < 7 then 0 else 1, ?_⟩
      decide +native

/-- The counterexample has Havel--Hakimi residue two. -/
@[category test, AMS 5]
theorem wowii109Counterexample_residue : residue wowii109Counterexample = 2 := by
  unfold residue
  decide +native

/--
WOWII [Conjecture 109](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)

For a simple connected graph $G$, the independence number $\alpha(G)$ satisfies
$\alpha(G) \le \lfloor (\mathrm{residue}(G) + 2 \cdot b(G)) / 3 \rfloor$, where
$\mathrm{residue}(G)$ is the Havel-Hakimi residue and $b(G)$ is the size of a
largest induced bipartite subgraph.

See: Favaron, Mahéo, Saclé (1991) for the residue; DeLaVina's Graffiti.pc for the conjecture.

This conjecture is false. The graph `wowii109Counterexample` has independence
number $7$, largest induced bipartite subgraph size $9$, and residue $2$, so the
proposed upper bound is $\lfloor(2 + 2 \cdot 9) / 3\rfloor = 6$.
-/
@[category research solved, AMS 5, formal_proof using formal_conjectures at
  "https://github.com/chelokot/wowii-109-counterexample/blob/543a66ee78565b553f4ba6dc7fd32b5610557913/lean/GraphConjecture109.lean#L29-L139"]
theorem conjecture109 : answer(False) ↔
    ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj] (_h : G.Connected),
      (G.indepNum : ℝ) ≤ ⌊((residue G : ℝ) + 2 * b G) / 3⌋ := by
  show False ↔ _
  rw [false_iff]
  intro h
  have hbad := h (Fin 13) wowii109Counterexample wowii109Counterexample_connected
  rw [wowii109Counterexample_indepNum, b, wowii109Counterexample_bipartiteSize,
    wowii109Counterexample_residue] at hbad
  norm_num at hbad

-- Sanity checks

/-- The invariant `b G` is nonneg (cast of a natural number). -/
@[category test, AMS 5]
example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _

/-- The residue of $K_2$ equals $1$: degree sequence is $[1, 1]$; one Havel-Hakimi
step gives $[0]$, leaving a single zero. -/
@[category test, AMS 5]
example : residue (⊤ : SimpleGraph (Fin 2)) = 1 := by
  unfold residue; decide +native

end WrittenOnTheWallII.GraphConjecture109