Erdős problem 944

/-
Submission body for Erdős 944. The checker supplies the imports and outer
Bounty namespace. Submit this entire file as the proof body.

Authors of the accompanying manuscript: Liam Kruer and Jensen Kohlmeyer.
OpenAI Codex assisted with proof development and Lean formalization.
-/

namespace Erdos944Proof

/-- Allowed differences in a punctured cyclic three-coloring. -/
def NormalDifference (n s : Nat) : Prop :=
  s = 1 ∨ s = n - 1 ∨ s % 3 = 2

theorem normalDifference_ne_color
    {n x y s : Nat} (hn : n % 3 = 1)
    (hx : 0 < x) (hxn : x < n) (hy : 0 < y) (hyn : y < n)
    (hs : NormalDifference n s) (hxy : y = x + s ∨ y + n = x + s) :
    x % 3 ≠ y % 3 := by
  rcases hs with hs | hs | hs <;> rcases hxy with hxy | hxy <;> omega

theorem normalDifference_neg {n s : Nat} (hn : n % 3 = 1)
    (_hs0 : 0 < s) (hsn : s < n) (hs : NormalDifference n s) :
    NormalDifference n (n - s) := by
  rcases hs with hs | hs | hs
  · exact Or.inr (Or.inl (by omega))
  · exact Or.inl (by omega)
  · exact Or.inr (Or.inr (by omega))

/-- The largest odd lift in {-1,1,3} of the color difference modulo three. -/
def maxStep (a b : Fin 3) : Int :=
  if a = b then 3 else if ((b.val : Int) - a.val) % 3 = 1 then 1 else -1

theorem maxStep_cases (a b : Fin 3) :
    maxStep a b = 3 ∨ maxStep a b = 1 ∨ maxStep a b = -1 := by
  unfold maxStep
  split <;> simp_all
  split <;> simp_all

theorem maxStep_eq_three (a : Fin 3) : maxStep a a = 3 := by
  simp [maxStep]

theorem maxStep_of_ne {a b : Fin 3} (h : a ≠ b) :
    maxStep a b = 1 ∨ maxStep a b = -1 := by
  simp only [maxStep, if_neg h]
  split <;> simp

theorem maxStep_mod_three (a b : Fin 3) :
    maxStep a b % 3 = ((b.val : Int) - a.val) % 3 := by
  have ha := a.isLt
  have hb := b.isLt
  by_cases hab : a = b
  · subst b
    simp [maxStep]
  · have hv : a.val ≠ b.val := fun h => hab (Fin.ext h)
    unfold maxStep
    simp only [if_neg hab]
    split <;> omega

theorem maxStep_reverse {a b : Fin 3} (h : a ≠ b) :
    maxStep a b + maxStep b a = 0 := by
  have h₁ := maxStep_of_ne h
  have h₂ := maxStep_of_ne (Ne.symm h)
  have h₃ := maxStep_mod_three a b
  have h₄ := maxStep_mod_three b a
  omega

theorem proper_square_sum_zero {a b c d : Fin 3}
    (hab : a ≠ b) (hbc : b ≠ c) (hcd : c ≠ d) (hda : d ≠ a) :
    maxStep a b + maxStep b c + maxStep c d + maxStep d a = 0 := by
  have h₁ := maxStep_of_ne hab
  have h₂ := maxStep_of_ne hbc
  have h₃ := maxStep_of_ne hcd
  have h₄ := maxStep_of_ne hda
  have m₁ := maxStep_mod_three a b
  have m₂ := maxStep_mod_three b c
  have m₃ := maxStep_mod_three c d
  have m₄ := maxStep_mod_three d a
  omega

theorem four_step_shortcut {a b c d : Fin 3}
    (hab : a ≠ b) (hbc : b ≠ c) (hcd : c ≠ d) :
    3 + maxStep a b + maxStep b c + maxStep c d - maxStep a d ≤ 3 := by
  have h₁ := maxStep_of_ne hab
  have h₂ := maxStep_of_ne hbc
  have h₃ := maxStep_of_ne hcd
  have h₄ := maxStep_cases a d
  have m₁ := maxStep_mod_three a b
  have m₂ := maxStep_mod_three b c
  have m₃ := maxStep_mod_three c d
  have m₄ := maxStep_mod_three a d
  omega

/-- A discrete antiderivative, with value zero at the initial vertex. -/
def partialSum (f : Nat → Int) : Nat → Int
  | 0 => 0
  | n + 1 => partialSum f n + f n

theorem prefix_add (f g : Nat → Int) (n : Nat) :
    partialSum (fun j => f j + g j) n = partialSum f n + partialSum g n := by
  induction n with
  | zero => rfl
  | succ n ih => simp only [partialSum, ih]; omega

theorem prefix_const (a : Int) (n : Nat) :
    partialSum (fun _ => a) n = (n : Int) * a := by
  induction n with
  | zero => simp [partialSum]
  | succ n ih => simp [partialSum, ih, Int.add_mul]

theorem prefix_mod_three (c : Nat → Fin 3) (f : Nat → Int)
    (hf : ∀ j, f j % 3 = ((c (j + 1)).val - (c j).val : Int) % 3) (n : Nat) :
    partialSum f n % 3 = ((c n).val - (c 0).val : Int) % 3 := by
  induction n with
  | zero => simp [partialSum]
  | succ n ih => have hj := hf n; simp only [partialSum]; omega

theorem prefix_mod_two (f : Nat → Int) (hf : ∀ j, f j % 2 = 1) (n : Nat) :
    partialSum f n % 2 = (n : Int) % 2 := by
  induction n with
  | zero => simp [partialSum]
  | succ n ih => have hj := hf n; simp only [partialSum]; omega

theorem cycle_flux_mod_six (c : Nat → Fin 3) (f : Nat → Int)
    (hf₃ : ∀ j, f j % 3 = ((c (j + 1)).val - (c j).val : Int) % 3)
    (hf₂ : ∀ j, f j % 2 = 1) {n : Nat} (hn : c n = c 0) :
    (partialSum f n - 3 * (n : Int)) % 6 = 0 := by
  have h₃ := prefix_mod_three c f hf₃ n
  have h₂ := prefix_mod_two f hf₂ n
  rw [hn] at h₃
  omega

/-- Sum of `s` consecutive increments starting at `v`. -/
def windowSum (f : Nat → Int) (v s : Nat) : Int :=
  partialSum (fun j => f (v + j)) s

theorem windowSum_succ (f : Nat → Int) (v s : Nat) :
    windowSum f v (s + 1) = windowSum f v s + f (v + s) := rfl

theorem windowSum_shift (f : Nat → Int) (v s : Nat) :
    windowSum f (v + 1) s - windowSum f v s = f (v + s) - f v := by
  induction s with
  | zero => simp [windowSum, partialSum]
  | succ s ih =>
    simp only [windowSum_succ]
    have hv : v + 1 + s = v + (s + 1) := by omega
    rw [hv]
    omega

theorem windowSum_period (f : Nat → Int) {n : Nat}
    (hf : ∀ v, f (v + n) = f v) (s : Nat) :
    windowSum f s n = partialSum f n := by
  induction s with
  | zero => simp [windowSum]
  | succ s ih =>
    have hs := windowSum_shift f s n
    rw [hf s, ih] at hs
    omega

theorem windowSum_flux (f : Nat → Int) {n : Nat}
    (hf : ∀ v, f (v + n) = f v) (s : Nat) :
    partialSum (fun v => windowSum f v s) n = (s : Int) * partialSum f n := by
  induction s with
  | zero => simp [windowSum, partialSum, prefix_const]
  | succ s ih =>
    have heq : (fun v => windowSum f v (s + 1)) =
        (fun v => windowSum f v s + f (v + s)) := by funext v; rfl
    rw [heq, prefix_add, ih]
    have hs : partialSum (fun v => f (v + s)) n = partialSum f n := by
      have hp := windowSum_period f hf s
      simpa only [windowSum, Nat.add_comm] using hp
    rw [hs]
    simp [Int.add_mul]

theorem flat_offset_constant (f e : Nat → Int) {s : Nat}
    (hflat : ∀ v, e (v + 1) - e v = f (v + s) - f v) (v : Nat) :
    e v - windowSum f v s = e 0 - partialSum f s := by
  induction v with
  | zero => simp [windowSum]
  | succ v ih =>
    have h₁ := hflat v
    have h₂ := windowSum_shift f v s
    omega

theorem flat_flux (f e : Nat → Int) {n s : Nat}
    (hf : ∀ v, f (v + n) = f v)
    (hflat : ∀ v, e (v + 1) - e v = f (v + s) - f v) :
    partialSum e n = (s : Int) * partialSum f n + (n : Int) * (e 0 - partialSum f s) := by
  have heq : e = (fun v => windowSum f v s + (e 0 - partialSum f s)) := by
    funext v
    have hv := flat_offset_constant f e hflat v
    omega
  calc
    partialSum e n = partialSum (fun v => windowSum f v s + (e 0 - partialSum f s)) n :=
      congrArg (fun g => partialSum g n) heq
    _ = _ := by rw [prefix_add, prefix_const, windowSum_flux f hf s]

theorem flat_offset_mod_six (c : Nat → Fin 3) (f e : Nat → Int) {s : Nat}
    (hf₃ : ∀ j, f j % 3 = ((c (j + 1)).val - (c j).val : Int) % 3)
    (hf₂ : ∀ j, f j % 2 = 1)
    (he₃ : e 0 % 3 = ((c s).val - (c 0).val : Int) % 3)
    (he₂ : e 0 % 2 = 1) :
    (e 0 - partialSum f s - 3 * (1 - (s : Int))) % 6 = 0 := by
  have h₃ := prefix_mod_three c f hf₃ s
  have h₂ := prefix_mod_two f hf₂ s
  omega

theorem exists_flux_character (c : Nat → Fin 3) (f : Nat → Int) {n : Nat}
    (hcn : c n = c 0) (hperiod : ∀ v, f (v + n) = f v)
    (hf₃ : ∀ j, f j % 3 = ((c (j + 1)).val - (c j).val : Int) % 3)
    (hf₂ : ∀ j, f j % 2 = 1) :
    ∃ K : Int, ∀ (s : Nat) (e : Nat → Int),
      (∀ v, e (v + 1) - e v = f (v + s) - f v) →
      e 0 % 3 = ((c s).val - (c 0).val : Int) % 3 →
      e 0 % 2 = 1 →
      ∃ z : Int, partialSum e n = 3 * (n : Int) + 6 * K * s + 6 * n * z := by
  let K : Int := (partialSum f n - 3 * n) / 6
  have hm := cycle_flux_mod_six c f hf₃ hf₂ hcn
  have hK : partialSum f n = 3 * (n : Int) + 6 * K := by dsimp [K]; omega
  refine ⟨K, fun s e hflat he₃ he₂ => ?_⟩
  let z : Int := (e 0 - partialSum f s - 3 * (1 - (s : Int))) / 6
  have hm' := flat_offset_mod_six c f e hf₃ hf₂ he₃ he₂
  have hz : e 0 - partialSum f s = 3 * (1 - (s : Int)) + 6 * z := by
    dsimp [z]
    omega
  refine ⟨z, ?_⟩
  rw [flat_flux f e hperiod hflat, hK, hz]
  grind

theorem maxStep_mod_two (a b : Fin 3) : maxStep a b % 2 = 1 := by
  have h := maxStep_cases a b
  omega

theorem partialSum_le (f : Nat → Int) (bound : Int) (n : Nat)
    (hf : ∀ j < n, f j ≤ bound) : partialSum f n ≤ (n : Int) * bound := by
  induction n with
  | zero => simp [partialSum]
  | succ n ih =>
    have hp := ih (fun j hj => hf j (by omega))
    have hn := hf n (by omega)
    simp only [partialSum, Int.natCast_succ, Int.add_mul, Int.one_mul]
    omega

theorem proper_cycle_winding (c : Nat → Fin 3) (t : Nat)
    (hcyc : c (3 * t + 2) = c 0)
    (hproper : ∀ j < 3 * t + 2, c j ≠ c (j + 1)) :
    partialSum (fun j => maxStep (c j) (c (j + 1))) (3 * t + 2) ≤ 3 * (t : Int) := by
  let f := fun j => maxStep (c j) (c (j + 1))
  have hb := partialSum_le f 1 (3 * t + 2) (fun j hj => by
    have h := maxStep_of_ne (hproper j hj)
    dsimp [f]
    omega)
  have hm := cycle_flux_mod_six c f (fun j => maxStep_mod_three _ _)
    (fun j => maxStep_mod_two _ _) hcyc
  dsimp [f] at hb hm
  omega

/-- The increment assigned to an oriented cyclic connection. -/
def directionStep (c : Nat → Fin 3) (s v : Nat) : Int :=
  maxStep (c v) (c (v + s))

theorem directionStep_flat (c : Nat → Fin 3) {s : Nat}
    (hunit : ∀ v, c v ≠ c (v + 1)) (hs : ∀ v, c v ≠ c (v + s)) (v : Nat) :
    directionStep c s (v + 1) - directionStep c s v =
      directionStep c 1 (v + s) - directionStep c 1 v := by
  have hi : v + 1 + s = v + s + 1 := by omega
  have hsq := proper_square_sum_zero (hunit v) (hs (v + 1))
    (by simpa only [hi] using Ne.symm (hunit (v + s))) (Ne.symm (hs v))
  have hr₁ := maxStep_reverse (hunit (v + s))
  have hr₂ := maxStep_reverse (hs v)
  simp only [hi] at hsq
  simp only [directionStep, hi]
  omega

/-- The height gain along a word of three proper connections. -/
def wordStep (c : Nat → Fin 3) (a b d v : Nat) : Int :=
  directionStep c a v + directionStep c b (v + a) +
    directionStep c d (v + a + b)

theorem wordStep_flat (c : Nat → Fin 3) {a b d : Nat}
    (hunit : ∀ v, c v ≠ c (v + 1))
    (ha : ∀ v, c v ≠ c (v + a)) (hb : ∀ v, c v ≠ c (v + b))
    (hd : ∀ v, c v ≠ c (v + d)) (v : Nat) :
    wordStep c a b d (v + 1) - wordStep c a b d v =
      directionStep c 1 (v + (a + b + d)) - directionStep c 1 v := by
  have h₁ := directionStep_flat c hunit ha v
  have h₂ := directionStep_flat c hunit hb (v + a)
  have h₃ := directionStep_flat c hunit hd (v + a + b)
  simp only [wordStep]
  simp only [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] at h₁ h₂ h₃ ⊢
  omega

theorem wordStep_cases (c : Nat → Fin 3) {a b d : Nat}
    (ha : ∀ v, c v ≠ c (v + a)) (hb : ∀ v, c v ≠ c (v + b))
    (hd : ∀ v, c v ≠ c (v + d)) (v : Nat) :
    wordStep c a b d v = -3 ∨ wordStep c a b d v = -1 ∨
      wordStep c a b d v = 1 ∨ wordStep c a b d v = 3 := by
  have h₁ := maxStep_of_ne (ha v)
  have h₂ := maxStep_of_ne (hb (v + a))
  have h₃ := maxStep_of_ne (hd (v + a + b))
  dsimp [wordStep, directionStep]
  omega

theorem wordStep_mod_three (c : Nat → Fin 3) (a b d v : Nat) :
    wordStep c a b d v % 3 = ((c (v + (a + b + d))).val - (c v).val : Int) % 3 := by
  have h₁ := maxStep_mod_three (c v) (c (v + a))
  have h₂ := maxStep_mod_three (c (v + a)) (c (v + a + b))
  have h₃ := maxStep_mod_three (c (v + a + b)) (c (v + a + b + d))
  have hi : v + (a + b + d) = v + a + b + d := by omega
  simp only [hi, wordStep, directionStep]
  omega

theorem wordStep_mod_two (c : Nat → Fin 3) (a b d v : Nat) :
    wordStep c a b d v % 2 = 1 := by
  have h₁ := maxStep_mod_two (c v) (c (v + a))
  have h₂ := maxStep_mod_two (c (v + a)) (c (v + a + b))
  have h₃ := maxStep_mod_two (c (v + a + b)) (c (v + a + b + d))
  dsimp [wordStep, directionStep]
  omega

theorem wordStep_of_ne (c : Nat → Fin 3) {a b d v : Nat}
    (ha : ∀ v, c v ≠ c (v + a)) (hb : ∀ v, c v ≠ c (v + b))
    (hd : ∀ v, c v ≠ c (v + d)) (hv : c v ≠ c (v + (a + b + d))) :
    wordStep c a b d v = 1 ∨ wordStep c a b d v = -1 := by
  have hc := wordStep_cases c ha hb hd v
  have hm := wordStep_mod_three c a b d v
  have hlo := (c v).isLt
  have hhi := (c (v + (a + b + d))).isLt
  have hne : (c v).val ≠ (c (v + (a + b + d))).val := fun h => hv (Fin.ext h)
  omega

theorem directionStep_period (c : Nat → Fin 3) {n : Nat}
    (hc : ∀ v, c (v + n) = c v) (s v : Nat) :
    directionStep c s (v + n) = directionStep c s v := by
  have hi : v + n + s = v + s + n := by omega
  simp only [directionStep, hi, hc]

/-- One character controls both proper directions and all proper three-step words. -/
theorem exists_coloring_flux_character (c : Nat → Fin 3) {n : Nat}
    (hc : ∀ v, c (v + n) = c v) (hunit : ∀ v, c v ≠ c (v + 1)) :
    ∃ K : Int,
      (∀ s, (∀ v, c v ≠ c (v + s)) → ∃ z : Int,
        partialSum (directionStep c s) n = 3 * (n : Int) + 6 * K * s + 6 * n * z) ∧
      (∀ a b d, (∀ v, c v ≠ c (v + a)) → (∀ v, c v ≠ c (v + b)) →
        (∀ v, c v ≠ c (v + d)) → ∃ z : Int,
        partialSum (wordStep c a b d) n =
          3 * (n : Int) + 6 * K * (a + b + d) + 6 * n * z) := by
  obtain ⟨K, hK⟩ := exists_flux_character c (directionStep c 1)
    (by simpa using hc 0) (directionStep_period c hc 1)
    (fun j => maxStep_mod_three _ _) (fun j => maxStep_mod_two _ _)
  refine ⟨K, ?_, ?_⟩
  · intro s hs
    exact hK s (directionStep c s) (directionStep_flat c hunit hs)
      (by simpa [directionStep] using maxStep_mod_three (c 0) (c s))
      (maxStep_mod_two _ _)
  · intro a b d ha hb hd
    have hm := hK (a + b + d) (wordStep c a b d) (wordStep_flat c hunit ha hb hd)
      (by simpa using wordStep_mod_three c a b d 0) (wordStep_mod_two c a b d 0)
    simpa only [Int.natCast_add] using hm

theorem partialSum_mono (f g : Nat → Int) (n : Nat)
    (h : ∀ v < n, f v ≤ g v) : partialSum f n ≤ partialSum g n := by
  induction n with
  | zero => simp [partialSum]
  | succ n ih =>
    have h₁ := ih (fun v hv => h v (by omega))
    have h₂ := h n (by omega)
    simp only [partialSum]
    omega

theorem partialSum_mul (a : Int) (f : Nat → Int) (n : Nat) :
    partialSum (fun v => a * f v) n = a * partialSum f n := by
  induction n with
  | zero => simp [partialSum]
  | succ n ih => simp only [partialSum, ih, Int.mul_add]

/-- Number of monochromatic oriented edges of a fixed connection in one period. -/
def badCount (c : Nat → Fin 3) (s n : Nat) : Int :=
  partialSum (fun v => if c v = c (v + s) then 1 else 0) n

theorem badCount_nonneg (c : Nat → Fin 3) (s n : Nat) : 0 ≤ badCount c s n := by
  have h := partialSum_mono (fun _ => 0)
    (fun v => if c v = c (v + s) then 1 else 0) n (fun _ _ => by split <;> omega)
  simpa only [badCount, prefix_const, Int.mul_zero] using h

theorem wordStep_bounds (c : Nat → Fin 3) {a b d : Nat}
    (ha : ∀ v, c v ≠ c (v + a)) (hb : ∀ v, c v ≠ c (v + b))
    (hd : ∀ v, c v ≠ c (v + d)) (v : Nat) :
    -1 - 2 * (if c v = c (v + (a + b + d)) then 1 else 0) ≤ wordStep c a b d v ∧
    wordStep c a b d v ≤ 1 + 2 * (if c v = c (v + (a + b + d)) then 1 else 0) := by
  by_cases hv : c v = c (v + (a + b + d))
  · have h := wordStep_cases c ha hb hd v
    simp only [if_pos hv]
    omega
  · have h := wordStep_of_ne c ha hb hd hv
    simp only [if_neg hv]
    omega

theorem wordStep_flux_bounds (c : Nat → Fin 3) {a b d : Nat}
    (ha : ∀ v, c v ≠ c (v + a)) (hb : ∀ v, c v ≠ c (v + b))
    (hd : ∀ v, c v ≠ c (v + d)) (n : Nat) :
    -(n : Int) - 2 * badCount c (a + b + d) n ≤ partialSum (wordStep c a b d) n ∧
    partialSum (wordStep c a b d) n ≤ (n : Int) + 2 * badCount c (a + b + d) n := by
  have hlo := partialSum_mono
    (fun v => -1 + -2 * (if c v = c (v + (a + b + d)) then 1 else 0))
    (wordStep c a b d) n (fun v _ => by have h := (wordStep_bounds c ha hb hd v).1; omega)
  have hhi := partialSum_mono (wordStep c a b d)
    (fun v => 1 + 2 * (if c v = c (v + (a + b + d)) then 1 else 0))
    n (fun v _ => (wordStep_bounds c ha hb hd v).2)
  simp only [prefix_add, prefix_const, partialSum_mul] at hlo hhi
  dsimp [badCount]
  omega

/-- The integral shortfall of a character from the middle third. -/
def characterDeficit (n : Nat) (x : Int) : Int :=
  max 0 ((n : Int) - 3 * min (x % n) ((n : Int) - x % n))

theorem characterDeficit_le_of_flux {n : Nat} (hn : 0 < n) {x z W β : Int}
    (hβ : 0 ≤ β) (hW : W = 3 * (n : Int) + 6 * x + 6 * n * z)
    (hlo : -(n : Int) - 2 * β ≤ W) (hhi : W ≤ (n : Int) + 2 * β) :
    characterDeficit n x ≤ β := by
  let m : Int := x % n
  let q : Int := x / n + z
  have hn' : 0 < (n : Int) := by omega
  have hm₀ : 0 ≤ m := Int.emod_nonneg _ (by omega)
  have hm₁ : m < n := Int.emod_lt_of_pos _ hn'
  have he := Int.emod_add_mul_ediv x n
  have hW' : W = 3 * (n : Int) + 6 * m + 6 * n * q := by
    dsimp [m, q]
    grind
  have hbounds : (n : Int) - 3 * m ≤ β ∧ (n : Int) - 3 * ((n : Int) - m) ≤ β := by
    by_cases hq₀ : 0 ≤ q
    · have hp := Int.mul_nonneg (show 0 ≤ 6 * (n : Int) by omega) hq₀
      omega
    · by_cases hq₁ : q = -1
      · rw [hq₁] at hW'
        omega
      · have hq₂ : q ≤ -2 := by omega
        have hp := Int.mul_le_mul_of_nonneg_left hq₂ (show 0 ≤ 6 * (n : Int) by omega)
        omega
  have hm : (n : Int) - 3 * min m ((n : Int) - m) ≤ β := by
    rw [Int.min_def]
    split <;> omega
  change max 0 ((n : Int) - 3 * min m ((n : Int) - m)) ≤ β
  rw [Int.max_def]
  split <;> omega

theorem wordStep_deficit_bound (c : Nat → Fin 3) {n a b d : Nat} (hn : 0 < n)
    (ha : ∀ v, c v ≠ c (v + a)) (hb : ∀ v, c v ≠ c (v + b))
    (hd : ∀ v, c v ≠ c (v + d)) {K z : Int}
    (hflux : partialSum (wordStep c a b d) n =
      3 * (n : Int) + 6 * K * (a + b + d) + 6 * n * z) :
    characterDeficit n (K * (a + b + d)) ≤ badCount c (a + b + d) n := by
  have hbds := wordStep_flux_bounds c ha hb hd n
  exact characterDeficit_le_of_flux hn (badCount_nonneg c _ _)
    (by simpa only [Int.mul_assoc] using hflux) hbds.1 hbds.2

/-- The undirected monochromatic edges of a vertex assignment. -/
def badEdges {V : Type*} (G : SimpleGraph V) {k : Nat} (c : V → Fin k) : Set (Sym2 V) :=
  {e | ∃ v w, e = s(v, w) ∧ G.Adj v w ∧ c v = c w}

theorem badEdges_eq_empty_iff {V : Type*} (G : SimpleGraph V) {k : Nat} (c : V → Fin k) :
    badEdges G c = ∅ ↔ ∀ v w, G.Adj v w → c v ≠ c w := by
  constructor
  · intro h v w hadj heq
    have he : s(v, w) ∈ badEdges G c := ⟨v, w, rfl, hadj, heq⟩
    rw [h] at he
    exact he
  · intro h
    apply Set.eq_empty_iff_forall_notMem.mpr
    rintro e ⟨v, w, rfl, hadj, heq⟩
    exact h v w hadj heq

theorem badEdges_subset_of_deleted {V : Type*} (G : SimpleGraph V) {k : Nat}
    (edges : Set (Sym2 V)) (c : (G.deleteEdges edges).Coloring (Fin k)) :
    badEdges G c ⊆ edges := by
  rintro e ⟨v, w, rfl, hadj, heq⟩
  by_contra hnot
  exact c.valid (SimpleGraph.deleteEdges_adj.mpr ⟨hadj, hnot⟩) heq

theorem not_colorable_of_badEdges_bound {V : Type*} (G : SimpleGraph V) {k r : Nat}
    (hbad : ∀ c : V → Fin k, r < (badEdges G c).ncard) : ¬ G.Colorable k := by
  rintro ⟨c⟩
  have hc := hbad c
  have he := (badEdges_eq_empty_iff G c).mpr (fun _ _ => c.valid)
  simp only [he, Set.ncard_empty, Nat.not_lt_zero] at hc

theorem colorable_succ_of_punctured {V : Type*} (G : SimpleGraph V) {k : Nat}
    (v : V) (c : V → Fin k)
    (hc : ∀ u w, u ≠ v → w ≠ v → G.Adj u w → c u ≠ c w) : G.Colorable (k + 1) := by
  classical
  refine ⟨SimpleGraph.Coloring.mk (fun u => if u = v then 0 else (c u).succ) ?_⟩
  intro u w hadj
  by_cases hu : u = v
  · subst u
    by_cases hw : w = v
    · subst w
      exact False.elim (G.ne_of_adj hadj rfl)
    · simpa only [if_pos rfl, if_neg hw, ite_true] using (Fin.succ_ne_zero (c w)).symm
  · by_cases hw : w = v