/- Maintained source: Replay/Core.lean -/
/-! Shared finite-coloring vocabulary for the reviewed sparse-obstruction proof.
This source is maintained by the lead. The final exporter removes imports and
places these declarations inside the trusted task namespace. -/

namespace Replay

abbrev Colour := Fin 3

abbrev Partial (V : Type*) := V → Option Colour

def LE {V : Type*} (rho sigma : Partial V) : Prop :=
  ∀ v c, rho v = some c → sigma v = some c

def Extends {V : Type*} (rho : Partial V) (f : V → Colour) : Prop :=
  ∀ v c, rho v = some c → f v = c

def Good {V : Type*} (G : SimpleGraph V) (f : V → Colour) : Prop :=
  ∀ v w, G.Adj v w → f v ≠ f w

def GoodOn {V : Type*} (E : Finset (Sym2 V)) (f : V → Colour) : Prop :=
  ∀ v w, s(v, w) ∈ E → f v ≠ f w

def EdgeHolds {V : Type*} (e : Sym2 V) (f : V → Colour) : Prop :=
  ∀ v w, e = s(v, w) → f v ≠ f w

theorem goodOn_iff_forall_edgeHolds {V : Type*}
    (E : Finset (Sym2 V)) (f : V → Colour) :
    GoodOn E f ↔ ∀ e ∈ E, EdgeHolds e f := by
  constructor
  · intro hf e he v w heq
    subst e
    exact hf v w he
  · intro hf v w hmem
    exact hf s(v, w) hmem v w rfl

theorem goodOn_mono {V : Type*} {E F : Finset (Sym2 V)}
    {f : V → Colour} (hEF : E ⊆ F) (hf : GoodOn F f) : GoodOn E f := by
  intro v w hmem
  exact hf v w (hEF hmem)

theorem goodOn_empty {V : Type*} (f : V → Colour) :
    GoodOn (∅ : Finset (Sym2 V)) f := by
  intro v w hmem
  exact False.elim (Finset.notMem_empty _ hmem)

theorem goodOn_union_iff {V : Type*} [DecidableEq V]
    (E F : Finset (Sym2 V)) (f : V → Colour) :
    GoodOn (E ∪ F) f ↔ GoodOn E f ∧ GoodOn F f := by
  constructor
  · intro hf
    exact ⟨goodOn_mono Finset.subset_union_left hf,
      goodOn_mono Finset.subset_union_right hf⟩
  · rintro ⟨hE, hF⟩ v w hmem
    rcases Finset.mem_union.mp hmem with hmem | hmem
    · exact hE v w hmem
    · exact hF v w hmem

theorem goodOn_edgeFinset_iff {V : Type*} (G : SimpleGraph V)
    [Fintype G.edgeSet] (f : V → Colour) :
    GoodOn G.edgeFinset f ↔ Good G f := by
  simp only [GoodOn, Good, SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet]

theorem extends_empty {V : Type*} (f : V → Colour) :
    Extends (fun _ : V => none) f := by
  intro v c h
  cases h

end Replay

/- Maintained source: Replay/TwoCNF.lean -/
namespace Replay.TwoCNF

variable {W : Type*}

abbrev Lit (W : Type*) := W × Bool
abbrev Clause (W : Type*) := Lit W × Lit W
abbrev Formula (W : Type*) := Finset (Clause W)

def neg (l : Lit W) : Lit W := (l.1, !l.2)
def Holds (a : W → Bool) (l : Lit W) : Prop := a l.1 = l.2
def Models (a : W → Bool) (F : Formula W) : Prop :=
  ∀ c ∈ F, Holds a c.1 ∨ Holds a c.2
def Satisfiable (F : Formula W) : Prop := ∃ a, Models a F
def unit (l : Lit W) : Clause W := (l, l)
def withUnits [DecidableEq W] (F : Formula W) (U : Finset (Lit W)) : Formula W :=
  F ∪ U.image unit

def Imp (F : Formula W) (a b : Lit W) : Prop :=
  ∃ c ∈ F, (a = neg c.1 ∧ b = c.2) ∨
    (a = neg c.2 ∧ b = c.1)
def Reach (F : Formula W) : Lit W → Lit W → Prop :=
  Relation.ReflTransGen (Imp F)

theorem neg_neg (l : Lit W) : neg (neg l) = l := by
  rcases l with ⟨v, b⟩
  cases b <;> rfl

theorem holds_neg (a : W → Bool) (l : Lit W) :
    Holds a (neg l) ↔ ¬ Holds a l := by
  rcases l with ⟨v, b⟩
  cases hb : a v <;> cases b <;> simp [Holds, neg, hb]

theorem models_withUnits_iff [DecidableEq W]
    (a : W → Bool) (F : Formula W) (U : Finset (Lit W)) :
    Models a (withUnits F U) ↔ Models a F ∧ ∀ l ∈ U, Holds a l := by
  constructor
  · intro h
    refine ⟨fun c hc => h c (Finset.mem_union_left _ hc), ?_⟩
    intro l hl
    have hu := h (unit l) (Finset.mem_union_right _ (Finset.mem_image.mpr ⟨l, hl, rfl⟩))
    simpa [unit] using hu
  · rintro ⟨hF, hU⟩ c hc
    rcases Finset.mem_union.mp hc with hc | hc
    · exact hF c hc
    · obtain ⟨l, hl, rfl⟩ := Finset.mem_image.mp hc
      exact Or.inl (hU l hl)

theorem imp_contra {F : Formula W} {a b : Lit W} (h : Imp F a b) :
    Imp F (neg b) (neg a) := by
  rcases h with ⟨c, hc, h | h⟩
  · rcases h with ⟨rfl, rfl⟩
    exact ⟨c, hc, Or.inr ⟨rfl, neg_neg _⟩⟩
  · rcases h with ⟨rfl, rfl⟩
    exact ⟨c, hc, Or.inl ⟨rfl, neg_neg _⟩⟩

theorem reach_contra {F : Formula W} {a b : Lit W} (h : Reach F a b) :
    Reach F (neg b) (neg a) := by
  induction h with
  | refl => exact .refl
  | tail _ hbc ih => exact ih.head (imp_contra hbc)

theorem models_imp {F : Formula W} {a : W → Bool} (hF : Models a F)
    {l m : Lit W} (h : Imp F l m) (hl : Holds a l) : Holds a m := by
  rcases h with ⟨c, hc, h | h⟩
  · rcases h with ⟨rfl, rfl⟩
    exact (hF c hc).resolve_left ((holds_neg _ _).mp hl)
  · rcases h with ⟨rfl, rfl⟩
    exact (hF c hc).resolve_right ((holds_neg _ _).mp hl)

theorem models_reach {F : Formula W} {a : W → Bool} (hF : Models a F)
    {l m : Lit W} (h : Reach F l m) (hl : Holds a l) : Holds a m := by
  induction h with
  | refl => exact hl
  | tail _ hbc ih => exact models_imp hF hbc ih

theorem satisfiable_no_cycle {F : Formula W} (hF : Satisfiable F) (l : Lit W) :
    ¬ (Reach F l (neg l) ∧ Reach F (neg l) l) := by
  rintro ⟨h₁, h₂⟩
  obtain ⟨a, ha⟩ := hF
  by_cases hl : Holds a l
  · exact ((holds_neg _ _).mp (models_reach ha h₁ hl)) hl
  · have hn := (holds_neg a l).mpr hl
    exact hl (models_reach ha h₂ hn)

private def Consistent (R : Finset (Lit W)) : Prop :=
  ∀ l ∈ R, neg l ∉ R

private def Closed (F : Formula W) (R : Finset (Lit W)) : Prop :=
  ∀ ⦃a b⦄, a ∈ R → Reach F a b → b ∈ R

private noncomputable def addClosure [Fintype W] [DecidableEq W]
    (F : Formula W) (R : Finset (Lit W)) (a : Lit W) : Finset (Lit W) := by
  classical
  exact R ∪ Finset.univ.filter (Reach F a)

private theorem mem_addClosure [Fintype W] [DecidableEq W]
    (F : Formula W) (R : Finset (Lit W)) (a b : Lit W) :
    b ∈ addClosure F R a ↔ b ∈ R ∨ Reach F a b := by
  classical
  simp [addClosure]

private theorem subset_addClosure [Fintype W] [DecidableEq W]
    (F : Formula W) (R : Finset (Lit W)) (a : Lit W) : R ⊆ addClosure F R a := by
  intro b hb
  exact (mem_addClosure _ _ _ _).mpr (Or.inl hb)

private theorem self_mem_addClosure [Fintype W] [DecidableEq W]
    (F : Formula W) (R : Finset (Lit W)) (a : Lit W) : a ∈ addClosure F R a :=
  (mem_addClosure _ _ _ _).mpr (Or.inr .refl)

private theorem closed_addClosure [Fintype W] [DecidableEq W]
    {F : Formula W} {R : Finset (Lit W)} (hR : Closed F R) (a : Lit W) :
    Closed F (addClosure F R a) := by
  intro b c hb hbc
  rcases (mem_addClosure _ _ _ _).mp hb with hb | hb
  · exact (mem_addClosure _ _ _ _).mpr (Or.inl (hR hb hbc))
  · exact (mem_addClosure _ _ _ _).mpr (Or.inr (hb.trans hbc))

private theorem consistent_addClosure [Fintype W] [DecidableEq W]
    {F : Formula W} {R : Finset (Lit W)} (hR : Consistent R) (hclosed : Closed F R)
    {a : Lit W} (hna : neg a ∉ R) (hcycle : ¬ Reach F a (neg a)) :
    Consistent (addClosure F R a) := by
  intro b hb hnb
  rcases (mem_addClosure _ _ _ _).mp hb with hb | hb
  · rcases (mem_addClosure _ _ _ _).mp hnb with hnb | hnb
    · exact hR b hb hnb
    · have h := reach_contra hnb
      exact hna (hclosed hb (by simpa only [neg_neg] using h))
  · rcases (mem_addClosure _ _ _ _).mp hnb with hnb | hnb
    · exact hna (hclosed hnb (reach_contra hb))
    · have h := reach_contra hnb
      exact hcycle (hb.trans (by simpa only [Reach, neg_neg] using h))

private theorem extend_one [Fintype W] [DecidableEq W]
    {F : Formula W} (hF : ∀ l, ¬ (Reach F l (neg l) ∧ Reach F (neg l) l))
    {R : Finset (Lit W)} (hR : Consistent R) (hclosed : Closed F R)
    {a : Lit W} (ha : a ∉ R) (hna : neg a ∉ R) :
    ∃ S, R ⊆ S ∧ Consistent S ∧ Closed F S ∧ (a ∈ S ∨ neg a ∈ S) := by
  classical
  by_cases h : Reach F a (neg a)
  · refine ⟨addClosure F R (neg a), subset_addClosure _ _ _, ?_,
      closed_addClosure hclosed _, Or.inr (self_mem_addClosure _ _ _)⟩
    apply consistent_addClosure hR hclosed
    · simpa only [neg_neg] using ha
    · simpa only [neg_neg] using fun hr => hF a ⟨h, hr⟩
  · exact ⟨addClosure F R a, subset_addClosure _ _ _,
      consistent_addClosure hR hclosed hna h, closed_addClosure hclosed _,
      Or.inl (self_mem_addClosure _ _ _)⟩

private theorem complete_extension [Fintype W] [DecidableEq W]
    {F : Formula W} (hF : ∀ l, ¬ (Reach F l (neg l) ∧ Reach F (neg l) l))
    {R : Finset (Lit W)} (hR : Consistent R) (hclosed : Closed F R) :
    ∃ S, R ⊆ S ∧ Consistent S ∧ Closed F S ∧
      ∀ v : W, (v, true) ∈ S ∨ (v, false) ∈ S := by
  classical
  let candidates : Finset (Finset (Lit W)) :=
    Finset.univ.filter fun S => R ⊆ S ∧ Consistent S ∧ Closed F S
  have hmem : R ∈ candidates := by simp [candidates, hR, hclosed]
  obtain ⟨S, hS, hmax⟩ := candidates.exists_max_image Finset.card ⟨R, hmem⟩
  obtain ⟨hRS, hcon, hcl⟩ := (Finset.mem_filter.mp hS).2
  refine ⟨S, hRS, hcon, hcl, ?_⟩
  intro v
  by_contra h
  have ht : (v, true) ∉ S := fun hv => h (Or.inl hv)
  have hf : (v, false) ∉ S := fun hv => h (Or.inr hv)
  obtain ⟨T, hST, hTcon, hTcl, hT⟩ := extend_one hF hcon hcl ht (by simpa [neg] using hf)
  have hTcand : T ∈ candidates := by
    simp only [candidates, Finset.mem_filter, Finset.mem_univ, true_and]
    exact ⟨hRS.trans hST, hTcon, hTcl⟩
  have heq : S = T := Finset.eq_of_subset_of_card_le hST (hmax T hTcand)
  apply h
  simpa [← heq, neg] using hT

private theorem model_of_closed [Fintype W] [DecidableEq W]
    {F : Formula W} {S : Finset (Lit W)} (hcon : Consistent S) (hcl : Closed F S)
    (htot : ∀ v : W, (v, true) ∈ S ∨ (v, false) ∈ S) :
    ∃ a, Models a F ∧ ∀ l ∈ S, Holds a l := by
  classical
  let a : W → Bool := fun v => if (v, true) ∈ S then true else false
  have heval : ∀ l : Lit W, Holds a l ↔ l ∈ S := by
    rintro ⟨v, b⟩
    cases b
    · by_cases ht : (v, true) ∈ S
      · have hf : (v, false) ∉ S := by simpa [neg] using hcon (v, true) ht
        simp [Holds, a, ht, hf]
      · have hf : (v, false) ∈ S := (htot v).resolve_left ht
        simp [Holds, a, ht, hf]
    · simp [Holds, a]
  refine ⟨a, ?_, fun l hl => (heval l).mpr hl⟩
  intro c hc
  by_cases h : Holds a c.1
  · exact Or.inl h
  · apply Or.inr
    apply (heval c.2).mpr
    apply hcl ((heval (neg c.1)).mp ((holds_neg _ _).mpr h))
    exact .single ⟨c, hc, Or.inl ⟨rfl, rfl⟩⟩

private theorem consistent_closed_extension [Fintype W] [DecidableEq W]
    {F : Formula W} (hF : ∀ l, ¬ (Reach F l (neg l) ∧ Reach F (neg l) l))
    {R : Finset (Lit W)} (hR : Consistent R) (hclosed : Closed F R) :
    ∃ a, Models a F ∧ ∀ l ∈ R, Holds a l := by
  obtain ⟨S, hRS, hcon, hcl, htot⟩ := complete_extension hF hR hclosed
  obtain ⟨a, ha, hS⟩ := model_of_closed hcon hcl htot
  exact ⟨a, ha, fun l hl => hS l (hRS hl)⟩

theorem satisfiable_iff_no_cycle [Fintype W] [DecidableEq W] (F : Formula W) :
    Satisfiable F ↔ ∀ l : Lit W, ¬ (Reach F l (neg l) ∧ Reach F (neg l) l) := by
  refine ⟨satisfiable_no_cycle, ?_⟩
  intro hF
  have hc : Consistent (∅ : Finset (Lit W)) := by simp [Consistent]
  have hcl : Closed F (∅ : Finset (Lit W)) := by simp [Closed]
  obtain ⟨a, ha, _⟩ := consistent_closed_extension hF hc hcl
  exact ⟨a, ha⟩

private noncomputable def unitClosure [Fintype W] [DecidableEq W]
    (F : Formula W) (U : Finset (Lit W)) : Finset (Lit W) := by
  classical
  exact Finset.univ.filter fun l => ∃ u ∈ U, Reach F u l

private theorem mem_unitClosure [Fintype W] [DecidableEq W]
    (F : Formula W) (U : Finset (Lit W)) (l : Lit W) :
    l ∈ unitClosure F U ↔ ∃ u ∈ U, Reach F u l := by
  classical
  simp [unitClosure]

theorem exists_two_units [Fintype W] [DecidableEq W]
    {F : Formula W} {U : Finset (Lit W)}
    (hF : Satisfiable F) (hU : ¬ Satisfiable (withUnits F U)) :
    ∃ p ∈ U, ∃ q ∈ U, ¬ Satisfiable (withUnits F {p, q}) := by
  classical
  have hcl : Closed F (unitClosure F U) := by
    intro a b ha hab
    obtain ⟨u, hu, hua⟩ := (mem_unitClosure _ _ _).mp ha
    exact (mem_unitClosure _ _ _).mpr ⟨u, hu, hua.trans hab⟩
  have hbad : ¬ Consistent (unitClosure F U) := by
    intro hcon
    obtain ⟨a, ha, hR⟩ := consistent_closed_extension (satisfiable_no_cycle hF) hcon hcl
    apply hU
    refine ⟨a, (models_withUnits_iff _ _ _).mpr ⟨ha, ?_⟩⟩
    intro u hu
    exact hR u ((mem_unitClosure _ _ _).mpr ⟨u, hu, .refl⟩)
  simp only [Consistent, not_forall, not_not] at hbad
  obtain ⟨l, hl, hnl⟩ := hbad
  obtain ⟨p, hp, hpl⟩ := (mem_unitClosure _ _ _).mp hl
  obtain ⟨q, hq, hql⟩ := (mem_unitClosure _ _ _).mp hnl
  refine ⟨p, hp, q, hq, ?_⟩
  rintro ⟨a, ha⟩
  obtain ⟨haF, haU⟩ := (models_withUnits_iff _ _ _).mp ha
  have h₁ := models_reach haF hpl (haU p (by simp))
  have h₂ := models_reach haF hql (haU q (by simp))
  exact ((holds_neg _ _).mp h₂) h₁

theorem imp_mono {F F' : Formula W} (hFF' : F ⊆ F') {a b : Lit W}
    (h : Imp F a b) : Imp F' a b := by
  obtain ⟨c, hc, hab⟩ := h
  exact ⟨c, hFF' hc, hab⟩

theorem reach_mono {F F' : Formula W} (hFF' : F ⊆ F') {a b : Lit W}
    (h : Reach F a b) : Reach F' a b := by
  induction h with
  | refl => exact .refl
  | tail _ hbc ih => exact ih.tail (imp_mono hFF' hbc)

private def Walk (F : Formula W) : ℕ → Lit W → Lit W → Prop
  | 0, a, b => a = b
  | n + 1, a, b => ∃ c, Walk F n a c ∧ Imp F c b

private theorem walk_reach {F : Formula W} {n : ℕ} {a b : Lit W}
    (h : Walk F n a b) : Reach F a b := by
  induction n generalizing b with
  | zero => obtain rfl := h; exact .refl
  | succ n ih =>
    obtain ⟨c, hac, hcb⟩ := h
    exact (ih hac).tail hcb

private theorem reach_walk {F : Formula W} {a b : Lit W} (h : Reach F a b) :
    ∃ n, Walk F n a b := by
  induction h with
  | refl => exact ⟨0, rfl⟩
  | tail _ hbc ih =>
    obtain ⟨n, hn⟩ := ih
    exact ⟨n + 1, _, hn, hbc⟩

private noncomputable def depth (F : Formula W) (a b : Lit W) : ℕ := by
  classical
  exact if h : Reach F a b then Nat.find (reach_walk h) else 0

private theorem walk_depth {F : Formula W} {a b : Lit W} (h : Reach F a b) :
    Walk F (depth F a b) a b := by
  classical
  simpa [depth, h] using Nat.find_spec (reach_walk h)

private theorem depth_le {F : Formula W} {n : ℕ} {a b : Lit W}
    (h : Walk F n a b) : depth F a b ≤ n := by
  classical
  have hr := walk_reach h
  simpa [depth, hr] using Nat.find_min' (reach_walk hr) h

private theorem predecessor_clause {F : Formula W} {a b : Lit W}
    (h : Reach F a b) (hne : b ≠ a) :
    ∃ d ∈ F, ∃ c, Reach F a c ∧ depth F a c < depth F a b ∧
      ((c = neg d.1 ∧ b = d.2) ∨ (c = neg d.2 ∧ b = d.1)) := by
  have hw := walk_depth h
  cases hn : depth F a b with
  | zero =>
    rw [hn] at hw
    exact (hne hw.symm).elim
  | succ n =>
    rw [hn] at hw
    obtain ⟨c, hac, d, hd, hcd⟩ := hw
    refine ⟨d, hd, c, walk_reach hac, ?_, hcd⟩
    have hle := depth_le hac
    omega

private theorem exists_reach_support [Fintype W] [DecidableEq W]
    (F : Formula W) (a : Lit W) :
    ∃ C : Formula W, C ⊆ F ∧ C.card ≤ Fintype.card (Lit W) ∧
      ∀ b, Reach F a b → Reach C a b := by
  classical
  let B := {b : Lit W // Reach F a b ∧ b ≠ a}
  let chooseClause : B → Clause W := fun b =>
    Classical.choose (predecessor_clause b.2.1 b.2.2)
  have hClause : ∀ b : B, chooseClause b ∈ F ∧
      ∃ c, Reach F a c ∧ depth F a c < depth F a b.1 ∧
        ((c = neg (chooseClause b).1 ∧ b.1 = (chooseClause b).2) ∨
          (c = neg (chooseClause b).2 ∧ b.1 = (chooseClause b).1)) := by
    intro b
    exact Classical.choose_spec (predecessor_clause b.2.1 b.2.2)
  let C : Formula W := Finset.univ.image chooseClause
  have hCF : C ⊆ F := by
    intro c hc
    obtain ⟨b, _, rfl⟩ := Finset.mem_image.mp hc
    exact (hClause b).1
  have hcard : C.card ≤ Fintype.card (Lit W) := by
    calc
      C.card ≤ (Finset.univ : Finset B).card := Finset.card_image_le
      _ = Fintype.card B := Finset.card_univ
      _ ≤ Fintype.card (Lit W) := Fintype.card_subtype_le _
  refine ⟨C, hCF, hcard, ?_⟩
  have hretained : ∀ n, ∀ b, depth F a b = n → Reach F a b → Reach C a b := by
    intro n
    induction n using Nat.strong_induction_on with
    | h n ih =>
      intro b hbn hab
      by_cases hba : b = a
      · subst b
        exact .refl
      · let b' : B := ⟨b, hab, hba⟩
        obtain ⟨c, hac, hlt, hcb⟩ := (hClause b').2
        change depth F a c < depth F a b at hlt
        have hacC : Reach C a c := ih (depth F a c) (by omega) c rfl hac
        apply hacC.tail
        refine ⟨chooseClause b', ?_, hcb⟩
        exact Finset.mem_image.mpr ⟨b', Finset.mem_univ _, rfl⟩
  exact fun b hb => hretained (depth F a b) b rfl hb

theorem exists_small_unsat_core [Fintype W] [DecidableEq W]
    {F : Formula W} (hF : ¬ Satisfiable F) :
    ∃ F' : Formula W, F' ⊆ F ∧ ¬ Satisfiable F' ∧
      F'.card ≤ 4 * Fintype.card W := by
  classical
  have hcycle : ¬ ∀ l : Lit W, ¬ (Reach F l (neg l) ∧ Reach F (neg l) l) :=
    fun h => hF ((satisfiable_iff_no_cycle F).mpr h)
  push Not at hcycle
  obtain ⟨l, h₁, h₂⟩ := hcycle
  obtain ⟨C₁, hC₁F, hcard₁, hreach₁⟩ := exists_reach_support F l
  obtain ⟨C₂, hC₂F, hcard₂, hreach₂⟩ := exists_reach_support F (neg l)
  refine ⟨C₁ ∪ C₂, Finset.union_subset hC₁F hC₂F, ?_, ?_⟩
  · intro hsat
    apply satisfiable_no_cycle hsat l
    exact ⟨reach_mono Finset.subset_union_left (hreach₁ _ h₁),
      reach_mono Finset.subset_union_right (hreach₂ _ h₂)⟩
  · calc
      (C₁ ∪ C₂).card ≤ C₁.card + C₂.card := Finset.card_union_le _ _
      _ ≤ Fintype.card (Lit W) + Fintype.card (Lit W) := Nat.add_le_add hcard₁ hcard₂
      _ = 4 * Fintype.card W := by simp [Lit, Fintype.card_prod]; omega

end Replay.TwoCNF

/- Maintained source: Replay/Lists.lean -/
namespace Replay

/-! Two-list graph coloring as a two-clause formula, with graph-edge support.

The choice family is separate from partial coloring states. Every retained
binary clause has its canonical edge; selected units retain their own external
edge. This module contains no implication-graph arguments.
-/

variable {V W : Type*}

structure TwoLists (G : SimpleGraph V) (W : Type*) where
  vert : W → V
  vert_injective : Function.Injective vert
  choice : W → Bool → Colour
  choice_injective : ∀ w, Function.Injective (choice w)

namespace TwoLists

private theorem exists_bool_choice (L : Finset Colour) (hL : L.card = 2) :
    ∃ c : Bool → Colour, Function.Injective c ∧
      ∀ x, x ∈ L ↔ ∃ b, x = c b := by
  classical
  obtain ⟨x, y, hxy, rfl⟩ := Finset.card_eq_two.mp hL
  refine ⟨(fun b => if b then y else x), ?_, ?_⟩
  · intro a b hab
    cases a <;> cases b <;> simp_all
  · intro z
    constructor
    · intro hz
      rcases Finset.mem_insert.mp hz with hz | hz
      · exact ⟨false, hz⟩
      · exact ⟨true, Finset.mem_singleton.mp hz⟩
    · rintro ⟨b, rfl⟩
      cases b <;> simp

/-- Choose Boolean names for each exact two-element list. -/
noncomputable def ofFinset (G : SimpleGraph V) (vert : W → V)
    (hinj : Function.Injective vert) (L : W → Finset Colour)
    (hL : ∀ w, (L w).card = 2) : TwoLists G W where
  vert := vert
  vert_injective := hinj
  choice w := Classical.choose (exists_bool_choice (L w) (hL w))
  choice_injective w := (Classical.choose_spec
    (exists_bool_choice (L w) (hL w))).1

theorem ofFinset_vert (G : SimpleGraph V) (vert : W → V)
    (hinj : Function.Injective vert) (L : W → Finset Colour)
    (hL : ∀ w, (L w).card = 2) (w : W) :
    (ofFinset G vert hinj L hL).vert w = vert w := rfl

theorem ofFinset_mem_iff (G : SimpleGraph V) (vert : W → V)
    (hinj : Function.Injective vert) (L : W → Finset Colour)
    (hL : ∀ w, (L w).card = 2) (w : W) (c : Colour) :
    c ∈ L w ↔ ∃ b, c = (ofFinset G vert hinj L hL).choice w b := by
  exact (Classical.choose_spec (exists_bool_choice (L w) (hL w))).2 c

variable {G : SimpleGraph V} (T : TwoLists G W)

private theorem bool_eq_not_of_ne {a b : Bool} (h : a ≠ b) : a = !b := by
  cases a <;> cases b <;> simp_all

private theorem bool_eq_of_ne_not {a b : Bool} (h : a ≠ !b) : a = b := by
  cases a <;> cases b <;> simp_all

/-- The clause signs are the allowed values, so their complements name the
forbidden common color. Clauses have a canonical originating graph edge. -/
noncomputable def graphFormula [Fintype W] : TwoCNF.Formula W := by
  classical
  exact Finset.univ.filter fun c =>
    G.Adj (T.vert c.1.1) (T.vert c.2.1) ∧
      T.choice c.1.1 (!c.1.2) = T.choice c.2.1 (!c.2.2)

theorem mem_graphFormula [Fintype W] (c : TwoCNF.Clause W) :
    c ∈ graphFormula T ↔
      G.Adj (T.vert c.1.1) (T.vert c.2.1) ∧
        T.choice c.1.1 (!c.1.2) = T.choice c.2.1 (!c.2.2) := by
  classical
  simp [graphFormula]

theorem models_graphFormula_iff [Fintype W] (a : W → Bool) :
    TwoCNF.Models a (graphFormula T) ↔
      ∀ v w, G.Adj (T.vert v) (T.vert w) →
        T.choice v (a v) ≠ T.choice w (a w) := by
  classical
  constructor
  · intro h v w hvw hcolor
    let c : TwoCNF.Clause W := ((v, !(a v)), (w, !(a w)))
    have hc : c ∈ graphFormula T := by
      apply (mem_graphFormula T c).2
      simpa [c] using And.intro hvw hcolor
    rcases h c hc with hbad | hbad
    · cases ha : a v <;> simp [TwoCNF.Holds, c, ha] at hbad
    · cases ha : a w <;> simp [TwoCNF.Holds, c, ha] at hbad
  · intro h c hc
    obtain ⟨hadj, hcolor⟩ := (mem_graphFormula T c).1 hc
    by_cases h₁ : TwoCNF.Holds a c.1
    · exact Or.inl h₁
    by_cases h₂ : TwoCNF.Holds a c.2
    · exact Or.inr h₂
    have hb₁ : a c.1.1 = !c.1.2 := bool_eq_not_of_ne h₁
    have hb₂ : a c.2.1 = !c.2.2 := bool_eq_not_of_ne h₂
    exact False.elim (h c.1.1 c.2.1 hadj (by simpa [hb₁, hb₂] using hcolor))

/-- Finite graph-edge support of a retained graph-clause family. -/
noncomputable def graphSupport (F : TwoCNF.Formula W) : Finset (Sym2 V) := by
  classical
  exact F.image fun c => s(T.vert c.1.1, T.vert c.2.1)

theorem graphSupport_card (F : TwoCNF.Formula W) :
    (graphSupport T F).card ≤ F.card := by
  classical
  exact Finset.card_image_le

theorem graphSupport_sub_edges [Fintype V] [DecidableEq V]
    [DecidableRel G.Adj] [Fintype W]
    {F : TwoCNF.Formula W} (hF : F ⊆ graphFormula T) :
    graphSupport T F ⊆ G.edgeFinset := by
  classical
  intro e he
  have hex : ∃ c ∈ F, s(T.vert c.1.1, T.vert c.2.1) = e := by
    letI : DecidableEq V := Classical.decEq V
    exact Finset.mem_image.mp he
  obtain ⟨c, hc, hce⟩ := hex
  have hcG : s(T.vert c.1.1, T.vert c.2.1) ∈ G.edgeFinset := by
    simpa only [SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet] using
      ((mem_graphFormula T c).1 (hF hc)).1
  exact hce ▸ hcG

theorem models_of_goodOn_graphSupport [Fintype W]
    {F : TwoCNF.Formula W} (hF : F ⊆ graphFormula T)
    (a : W → Bool) (f : V → Colour)
    (hchoice : ∀ w, f (T.vert w) = T.choice w (a w))
    (hgood : GoodOn (graphSupport T F) f) : TwoCNF.Models a F := by
  classical
  intro c hc
  obtain ⟨_, hcolor⟩ := (mem_graphFormula T c).1 (hF hc)
  by_cases h₁ : TwoCNF.Holds a c.1
  · exact Or.inl h₁
  by_cases h₂ : TwoCNF.Holds a c.2
  · exact Or.inr h₂
  have hb₁ : a c.1.1 = !c.1.2 := bool_eq_not_of_ne h₁
  have hb₂ : a c.2.1 = !c.2.2 := bool_eq_not_of_ne h₂
  have he : s(T.vert c.1.1, T.vert c.2.1) ∈ graphSupport T F :=
    Finset.mem_image_of_mem _ hc
  apply False.elim
  apply hgood _ _ he
  rw [hchoice, hchoice, hb₁, hb₂]
  exact hcolor

theorem sparse_list_obstruction [Fintype V] [DecidableEq V]
    [DecidableRel G.Adj] [Fintype W]
    (h : ¬ TwoCNF.Satisfiable (graphFormula T)) :
    ∃ E : Finset (Sym2 V), E ⊆ G.edgeFinset ∧
      E.card ≤ 4 * Fintype.card W ∧
      ∀ f : V → Colour, GoodOn E f →
        (∀ w, ∃ b, f (T.vert w) = T.choice w b) → False := by
  classical
  obtain ⟨F, hF, hunsat, hcard⟩ := TwoCNF.exists_small_unsat_core h
  refine ⟨graphSupport T F, graphSupport_sub_edges T hF,
    (graphSupport_card T F).trans hcard, ?_⟩
  intro f hgood hlist
  let a : W → Bool := fun w => Classical.choose (hlist w)
  have hchoice : ∀ w, f (T.vert w) = T.choice w (a w) :=
    fun w => Classical.choose_spec (hlist w)
  exact hunsat ⟨a, models_of_goodOn_graphSupport T hF a f hchoice hgood⟩

/-- Units imposed by fixing all vertices in S to their prescribed defaults. -/
noncomputable def defaultUnits [Fintype W]
    (S : Finset V) (default : V → Colour) : Finset (TwoCNF.Lit W) := by
  classical
  exact Finset.univ.filter fun l =>
    ∃ s ∈ S, G.Adj s (T.vert l.1) ∧
      default s = T.choice l.1 (!l.2)

theorem mem_defaultUnits [Fintype W]
    (S : Finset V) (default : V → Colour) (l : TwoCNF.Lit W) :
    l ∈ defaultUnits T S default ↔
      ∃ s ∈ S, G.Adj s (T.vert l.1) ∧
        default s = T.choice l.1 (!l.2) := by
  classical
  simp [defaultUnits]

theorem models_withDefaultUnits_iff [Fintype W] [DecidableEq W]
    (S : Finset V) (default : V → Colour) (a : W → Bool) :
    TwoCNF.Models a
        (TwoCNF.withUnits (graphFormula T) (defaultUnits T S default)) ↔
      (∀ v w, G.Adj (T.vert v) (T.vert w) →
        T.choice v (a v) ≠ T.choice w (a w)) ∧
      (∀ s ∈ S, ∀ w, G.Adj s (T.vert w) →
        default s ≠ T.choice w (a w)) := by
  classical
  rw [TwoCNF.models_withUnits_iff, models_graphFormula_iff]
  constructor
  · rintro ⟨hgraph, hunits⟩
    refine ⟨hgraph, ?_⟩
    intro s hs w hadj hcolor
    let l : TwoCNF.Lit W := (w, !(a w))
    have hl : l ∈ defaultUnits T S default := by
      apply (mem_defaultUnits T S default l).2
      exact ⟨s, hs, hadj, by simpa [l] using hcolor⟩
    have hbad := hunits l hl
    cases ha : a w <;> simp [TwoCNF.Holds, l, ha] at hbad
  · rintro ⟨hgraph, hcross⟩
    refine ⟨hgraph, ?_⟩
    intro l hl
    obtain ⟨s, hs, hadj, hcolor⟩ := (mem_defaultUnits T S default l).1 hl
    by_contra hbad
    have hb : a l.1 = !l.2 := bool_eq_not_of_ne hbad
    apply hcross s hs l.1 hadj
    simpa [hb] using hcolor

private theorem holds_of_goodOn_origin
    (default : V → Colour) (a : W → Bool) (f : V → Colour)
    (hchoice : ∀ w, f (T.vert w) = T.choice w (a w))
    {E : Finset (Sym2 V)} (hgood : GoodOn E f)
    (l : TwoCNF.Lit W) (s : V)
    (he : s(s, T.vert l.1) ∈ E)
    (hdefault : f s = default s)
    (horigin : default s = T.choice l.1 (!l.2)) : TwoCNF.Holds a l := by
  apply bool_eq_of_ne_not
  intro hb
  apply hgood s (T.vert l.1) he
  rw [hdefault, horigin, hchoice, hb]

/-- A contradiction caused by all defaults is already witnessed by defaults
at one or two originating external vertices. The retained binary support uses
at most four edges per variable; the selected unit origins add two edges. -/
theorem sparse_default_obstruction [Fintype V] [DecidableEq V]
    [DecidableRel G.Adj] [Fintype W] [DecidableEq W]
    (S : Finset V) (default : V → Colour)
    (hF : TwoCNF.Satisfiable (graphFormula T))
    (hU : ¬ TwoCNF.Satisfiable
      (TwoCNF.withUnits (graphFormula T) (defaultUnits T S default))) :
    ∃ s ∈ S, ∃ t ∈ S, ∃ E : Finset (Sym2 V),
      E ⊆ G.edgeFinset ∧ E.card ≤ 4 * Fintype.card W + 2 ∧
      ∀ f : V → Colour, GoodOn E f →
        (∀ w, ∃ b, f (T.vert w) = T.choice w b) →
        f s = default s → f t = default t → False := by
  classical
  obtain ⟨p, hp, q, hq, hpq⟩ := TwoCNF.exists_two_units hF hU
  obtain ⟨s, hs, hsp, hpc⟩ := (mem_defaultUnits T S default p).1 hp
  obtain ⟨t, ht, htq, hqc⟩ := (mem_defaultUnits T S default q).1 hq
  obtain ⟨K, hK, hKunsat, hKcard⟩ := TwoCNF.exists_small_unsat_core hpq
  let F : TwoCNF.Formula W := K ∩ graphFormula T
  have hFsub : F ⊆ graphFormula T := Finset.inter_subset_right
  have hFcard : F.card ≤ 4 * Fintype.card W :=
    (Finset.card_le_card (Finset.inter_subset_left : F ⊆ K)).trans hKcard
  have hKsub : K ⊆ TwoCNF.withUnits F {p, q} := by
    intro c hc
    have hc' := hK hc
    rcases Finset.mem_union.mp hc' with hcG | hcU
    · exact Finset.mem_union.mpr (Or.inl (Finset.mem_inter.mpr ⟨hc, hcG⟩))
    · exact Finset.mem_union.mpr (Or.inr hcU)
  have hsmall : ¬ TwoCNF.Satisfiable (TwoCNF.withUnits F {p, q}) := by
    rintro ⟨a, ha⟩
    exact hKunsat ⟨a, fun c hc => ha c (hKsub hc)⟩
  let E := graphSupport T F ∪ {s(s, T.vert p.1), s(t, T.vert q.1)}
  refine ⟨s, hs, t, ht, E, ?_, ?_, ?_⟩
  · intro e he
    rcases Finset.mem_union.mp he with he | he
    · exact graphSupport_sub_edges T hFsub he
    · rcases Finset.mem_insert.mp he with rfl | he
      · simpa only [SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet] using hsp
      · have he' := Finset.mem_singleton.mp he
        subst e
        simpa only [SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet] using htq
  · calc
      E.card ≤ (graphSupport T F).card +
          ({s(s, T.vert p.1), s(t, T.vert q.1)} : Finset (Sym2 V)).card :=
        Finset.card_union_le _ _
      _ ≤ F.card + 2 := Nat.add_le_add (graphSupport_card T F) Finset.card_le_two
      _ ≤ 4 * Fintype.card W + 2 := Nat.add_le_add_right hFcard 2
  · intro f hgood hlist hfs hft
    let a : W → Bool := fun w => Classical.choose (hlist w)
    have hchoice : ∀ w, f (T.vert w) = T.choice w (a w) :=
      fun w => Classical.choose_spec (hlist w)
    have hgoodF : GoodOn (graphSupport T F) f := by
      intro v w he
      exact hgood v w (Finset.mem_union.mpr (Or.inl he))
    have haF : TwoCNF.Models a F :=
      models_of_goodOn_graphSupport T hFsub a f hchoice hgoodF
    have hap : TwoCNF.Holds a p :=
      holds_of_goodOn_origin T default a f hchoice hgood p s
        (by simp [E]) hfs hpc
    have haq : TwoCNF.Holds a q :=
      holds_of_goodOn_origin T default a f hchoice hgood q t
        (by simp [E]) hft hqc
    apply hsmall
    refine ⟨a, (TwoCNF.models_withUnits_iff a F {p, q}).2 ⟨haF, ?_⟩⟩
    intro l hl
    rcases Finset.mem_insert.mp hl with rfl | hl
    · exact hap
    · have hlq : l = q := Finset.mem_singleton.mp hl
      subst l
      exact haq

end TwoLists

end Replay

/- Maintained source: Replay/State.lean -/
open scoped BigOperators

noncomputable section

namespace Replay

variable {V : Type*} [Fintype V] [DecidableEq V]
variable (G : SimpleGraph V) [DecidableRel G.Adj]

def available (rho : Partial V) (v : V) : Finset Colour := by
  classical
  exact Finset.univ.filter fun c => ∀ w, G.Adj v w → rho w ≠ some c

def domain (rho : Partial V) (v : V) : Finset Colour :=
  match rho v with
  | some c => {c}
  | none => available G rho v

def rankWeight (rho : Partial V) (v : V) : ℕ :=
  (domain G rho v).card - 1

def rank (rho : Partial V) : ℕ := ∑ v, rankWeight G rho v

def unassignedCount (rho : Partial V) : ℕ := by
  classical
  exact (Finset.univ.filter fun v => rho v = none).card

def put (rho : Partial V) (v : V) (c : Colour) : Partial V :=
  Function.update rho v (some c)

def Conflict (rho : Partial V) : Prop :=
  (∃ v w c, G.Adj v w ∧ rho v = some c ∧ rho w = some c) ∨
  ∃ v, rho v = none ∧ available G rho v = ∅

structure Closed (rho : Partial V) : Prop where
  proper : ∀ v w c, G.Adj v w → rho v = some c → rho w ≠ some c
  lists : ∀ v, rho v = none → 2 ≤ (available G rho v).card

def IsThree (rho : Partial V) (v : V) : Prop :=
  rho v = none ∧ available G rho v = Finset.univ

variable {G} {rho sigma : Partial V} {v w : V} {c : Colour}

theorem le_refl (rho : Partial V) : LE rho rho := by
  intro v c h
  exact h

theorem le_trans {tau : Partial V} (hab : LE rho sigma) (hbc : LE sigma tau) :
    LE rho tau := by
  intro v c h
  exact hbc v c (hab v c h)

theorem extends_of_le (h : LE rho sigma) {f : V → Colour}
    (hf : Extends sigma f) : Extends rho f := by
  intro v c hv
  exact hf v c (h v c hv)

theorem mem_available_iff :
    c ∈ available G rho v ↔ ∀ w, G.Adj v w → rho w ≠ some c := by
  classical
  simp [available]

theorem not_mem_available_iff :
    c ∉ available G rho v ↔ ∃ w, G.Adj v w ∧ rho w = some c := by
  classical
  constructor
  · intro hc
    by_contra h
    apply hc
    rw [mem_available_iff]
    intro w hw heq
    exact h ⟨w, hw, heq⟩
  · rintro ⟨w, hw, heq⟩ hc
    exact (mem_available_iff.mp hc) w hw heq

theorem available_mono (h : LE rho sigma) :
    available G sigma v ⊆ available G rho v := by
  intro c hc
  rw [mem_available_iff] at hc ⊢
  intro w hw heq
  exact hc w hw (h w c heq)

theorem available_card_le : (available G rho v).card ≤ 3 := by
  classical
  have h := Finset.card_le_card (Finset.subset_univ (available G rho v))
  simpa [Colour] using h

theorem available_eq_univ_iff :
    available G rho v = Finset.univ ↔
      ∀ w, G.Adj v w → rho w = none := by
  classical
  constructor
  · intro h w hw
    cases hval : rho w with
    | none => rfl
    | some c =>
        have hc : c ∈ available G rho v := by rw [h]; exact Finset.mem_univ c
        exact False.elim ((mem_available_iff.mp hc) w hw hval)
  · intro h
    apply Finset.eq_univ_of_forall
    intro c
    rw [mem_available_iff]
    intro w hw
    simp [h w hw]

theorem available_card_eq_three_iff :
    (available G rho v).card = 3 ↔ available G rho v = Finset.univ := by
  classical
  constructor
  · intro h
    apply Finset.eq_of_subset_of_card_le (Finset.subset_univ _)
    simpa [Colour] using h.ge
  · intro h
    simp [h, Colour]

theorem domain_eq_of_some (h : rho v = some c) : domain G rho v = {c} := by
  simp [domain, h]

theorem domain_eq_of_none (h : rho v = none) :
    domain G rho v = available G rho v := by
  simp [domain, h]

theorem domain_mono_of_unassigned (h : LE rho sigma) (hv : sigma v = none) :
    domain G sigma v ⊆ domain G rho v := by
  have hr : rho v = none := by
    cases heq : rho v with
    | none => rfl
    | some c =>
        have hs := h v c heq
        rw [hv] at hs
        contradiction
  rw [domain_eq_of_none hv, domain_eq_of_none hr]
  exact available_mono h

theorem rankWeight_mono (h : LE rho sigma) (v : V) :
    rankWeight G sigma v ≤ rankWeight G rho v := by
  cases hv : sigma v with
  | none =>
      exact Nat.sub_le_sub_right
        (Finset.card_le_card (domain_mono_of_unassigned h hv)) 1
  | some c => simp [rankWeight, domain, hv]

theorem rank_mono (h : LE rho sigma) : rank G sigma ≤ rank G rho := by
  exact Finset.sum_le_sum fun v _ => rankWeight_mono h v

theorem rank_empty : rank G (fun _ => none) = 2 * Fintype.card V := by
  classical
  simp [rank, rankWeight, domain, available, Colour, Nat.mul_comm]

theorem closed_not_conflict (h : Closed G rho) : ¬ Conflict G rho := by
  rintro (⟨v, w, c, hvw, hv, hw⟩ | ⟨v, hv, hempty⟩)
  · exact h.proper v w c hvw hv hw
  · have hc := h.lists v hv
    simp [hempty] at hc

theorem closed_domain_card_ge (h : Closed G rho) (hv : rho v = none) :
    2 ≤ (domain G rho v).card := by
  rw [domain_eq_of_none hv]
  exact h.lists v hv

theorem isThree_neighbors_unassigned (h : IsThree G rho v) :
    ∀ w, G.Adj v w → rho w = none :=
  available_eq_univ_iff.mp h.2

theorem closed_three_neighbors_unassigned
    (_h : Closed G rho) (_hv : rho v = none)
    (hcard : (available G rho v).card = 3) :
    ∀ w, G.Adj v w → rho w = none :=
  available_eq_univ_iff.mp (available_card_eq_three_iff.mp hcard)

theorem le_put (hv : rho v = none) : LE rho (put rho v c) := by
  intro w d hw
  by_cases h : w = v
  · subst w
    rw [hv] at hw
    contradiction
  · simp [put, Function.update_of_ne h, hw]

theorem put_self : put rho v c v = some c := by simp [put]

theorem put_of_ne (h : w ≠ v) : put rho v c w = rho w := by
  simp [put, h]

theorem unassignedCount_le (rho : Partial V) :
    unassignedCount rho ≤ Fintype.card V := by
  classical
  exact (Finset.card_filter_le _ _).trans_eq (Finset.card_univ)

theorem unassignedCount_put (hv : rho v = none) :
    unassignedCount (put rho v c) + 1 = unassignedCount rho := by
  classical
  have hset : (Finset.univ.filter fun w => put rho v c w = none) =
      (Finset.univ.filter fun w => rho w = none).erase v := by
    ext w
    rw [Finset.mem_filter, Finset.mem_erase, Finset.mem_filter]
    simp only [Finset.mem_univ, true_and]
    by_cases hw : w = v
    · subst w
      rw [put_self]
      simp
    · rw [put_of_ne hw]
      simp [hw]
  have hmem : v ∈ Finset.univ.filter fun w => rho w = none := by simp [hv]
  simpa only [unassignedCount, hset] using Finset.card_erase_add_one hmem

theorem forbidden_support (rho : Partial V) (v : V) (A : Finset Colour)
    (hA : ∀ c ∈ A, c ∉ available G rho v) :
    ∃ E : Finset (Sym2 V), E ⊆ G.edgeFinset ∧ E.card ≤ A.card ∧
      ∀ f, GoodOn E f → Extends rho f → f v ∉ A := by
  classical
  have hex : ∀ a : {c // c ∈ A}, ∃ w, G.Adj v w ∧ rho w = some a.1 := by
    intro a
    exact not_mem_available_iff.mp (hA a.1 a.2)
  choose reason hadj hcolor using hex
  let E : Finset (Sym2 V) := A.attach.image fun a => s(v, reason a)
  refine ⟨E, ?_, ?_, ?_⟩
  · intro e he
    obtain ⟨a, _, rfl⟩ := Finset.mem_image.mp he
    simpa only [SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet] using hadj a
  · simpa only [Finset.card_attach] using
      (Finset.card_image_le (s := A.attach) (f := fun a => s(v, reason a)))
  · intro f hgood hf hmem
    let a : {c // c ∈ A} := ⟨f v, hmem⟩
    have he : s(v, reason a) ∈ E :=
      Finset.mem_image.mpr ⟨a, Finset.mem_attach _ _, rfl⟩
    exact hgood v (reason a) he (hf (reason a) a.1 (hcolor a)).symm

theorem singleton_force_support
    (_hv : rho v = none) (hc : available G rho v = {c}) :
    ∃ E : Finset (Sym2 V), E ⊆ G.edgeFinset ∧ E.card ≤ 2 ∧
      ∀ f, GoodOn E f → Extends rho f → Extends (put rho v c) f := by
  classical
  have hA : ∀ d ∈ (Finset.univ.erase c : Finset Colour),
      d ∉ available G rho v := by
    intro d hd
    simpa [hc] using (Finset.mem_erase.mp hd).1
  obtain ⟨E, hE, hcard, hforce⟩ :=
    forbidden_support rho v (Finset.univ.erase c) hA
  refine ⟨E, hE, ?_, ?_⟩
  · simpa [Colour] using hcard
  · intro f hgood hf
    have hfc : f v = c := by
      have hnot := hforce f hgood hf
      simpa using hnot
    intro w d hw
    by_cases h : w = v
    · subst w
      have hcd : c = d := by simpa [put] using hw
      exact hfc.trans hcd
    · exact hf w d (by simpa [put, h] using hw)

theorem conflict_support (hc : Conflict G rho) :
    ∃ E : Finset (Sym2 V), E ⊆ G.edgeFinset ∧ E.card ≤ 3 ∧
      ∀ f, GoodOn E f → Extends rho f → False := by
  classical
  rcases hc with ⟨v, w, c, hvw, hv, hw⟩ | ⟨v, _hv, hempty⟩
  · refine ⟨{s(v, w)}, ?_, by simp, ?_⟩
    · intro e he
      have heq : e = s(v, w) := Finset.mem_singleton.mp he
      subst e
      simpa only [SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet] using hvw
    · intro f hgood hf
      exact hgood v w (by simp) ((hf v c hv).trans (hf w c hw).symm)
  · have hA : ∀ c ∈ (Finset.univ : Finset Colour), c ∉ available G rho v := by
      simp [hempty]
    obtain ⟨E, hE, hcard, hforce⟩ := forbidden_support rho v Finset.univ hA
    refine ⟨E, hE, ?_, ?_⟩
    · simpa [Colour] using hcard
    · intro f hgood hf
      exact hforce f hgood hf (Finset.mem_univ _)

theorem two_list_missing (hcard : (available G rho v).card = 2) :
    ∃ c, c ∉ available G rho v ∧ available G rho v = Finset.univ.erase c := by
  classical
  have hcompl : (Finset.univ \ available G rho v).card = 1 := by
    rw [Finset.card_sdiff_of_subset (Finset.subset_univ _)]
    simp [hcard, Colour]
  obtain ⟨c, hc⟩ := Finset.card_eq_one.mp hcompl
  have hcnot : c ∉ available G rho v := by
    have hmem : c ∈ Finset.univ \ available G rho v := by rw [hc]; simp
    exact (Finset.mem_sdiff.mp hmem).2
  refine ⟨c, hcnot, ?_⟩
  apply Finset.eq_of_subset_of_card_le
  · intro d hd
    exact Finset.mem_erase.mpr ⟨fun heq => hcnot (heq ▸ hd), Finset.mem_univ _⟩
  · simp [hcard, Colour]

theorem list_reasons (rho : Partial V) :
    ∃ E : Finset (Sym2 V), E ⊆ G.edgeFinset ∧ E.card ≤ Fintype.card V ∧
      ∀ f, GoodOn E f → Extends rho f →
        ∀ v, rho v = none → (available G rho v).card = 2 →
          f v ∈ available G rho v := by
  classical
  let R : Finset V := Finset.univ.filter fun v =>
    rho v = none ∧ (available G rho v).card = 2
  have hex : ∀ x : {v // v ∈ R}, ∃ c w,
      G.Adj x.1 w ∧ rho w = some c ∧ available G rho x.1 = Finset.univ.erase c := by
    intro x
    have hcard : (available G rho x.1).card = 2 :=
      (Finset.mem_filter.mp x.2).2.2
    obtain ⟨c, hcnot, hc⟩ := two_list_missing hcard
    obtain ⟨w, hw, hcolor⟩ := not_mem_available_iff.mp hcnot
    exact ⟨c, w, hw, hcolor, hc⟩
  choose missing reason hadj hcolor havail using hex
  let E : Finset (Sym2 V) := R.attach.image fun x => s(x.1, reason x)
  refine ⟨E, ?_, ?_, ?_⟩
  · intro e he
    obtain ⟨x, _, rfl⟩ := Finset.mem_image.mp he
    simpa only [SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet] using hadj x
  · calc
      E.card ≤ R.attach.card := Finset.card_image_le
      _ = R.card := Finset.card_attach
      _ ≤ Fintype.card V := by
        exact (Finset.card_filter_le _ _).trans_eq Finset.card_univ
  · intro f hgood hf v hv hcard
    have hvmem : v ∈ R := by simp [R, hv, hcard]
    let x : {v // v ∈ R} := ⟨v, hvmem⟩
    have he : s(v, reason x) ∈ E :=
      Finset.mem_image.mpr ⟨x, Finset.mem_attach _ _, rfl⟩
    have hneq : f v ≠ missing x := by
      intro hsame
      exact hgood v (reason x) he (hsame.trans (hf (reason x) _ (hcolor x)).symm)
    rw [havail x]
    exact Finset.mem_erase.mpr ⟨hneq, Finset.mem_univ _⟩

theorem propagate_aux (rho : Partial V) :
    ∃ sigma : Partial V, ∃ E : Finset (Sym2 V),
      LE rho sigma ∧ E ⊆ G.edgeFinset ∧
      E.card + 2 * unassignedCount sigma ≤ 2 * unassignedCount rho ∧
      (∀ f, GoodOn E f → Extends rho f → Extends sigma f) ∧
      (Conflict G sigma ∨ Closed G sigma) := by
  classical
  have general : ∀ m : ℕ, ∀ rho : Partial V, unassignedCount rho = m →
      ∃ sigma : Partial V, ∃ E : Finset (Sym2 V),
        LE rho sigma ∧ E ⊆ G.edgeFinset ∧
        E.card + 2 * unassignedCount sigma ≤ 2 * unassignedCount rho ∧
        (∀ f, GoodOn E f → Extends rho f → Extends sigma f) ∧
        (Conflict G sigma ∨ Closed G sigma) := by
    intro m
    induction m using Nat.strong_induction_on with
    | h m ih =>
      intro rho hcount
      by_cases hc : Conflict G rho
      · refine ⟨rho, ∅, le_refl rho, Finset.empty_subset _, ?_, ?_, Or.inl hc⟩
        · simp
        · intro f _ hf
          exact hf
      · by_cases hs : ∃ v c, rho v = none ∧ available G rho v = {c}
        · obtain ⟨v, c, hv, havail⟩ := hs
          have hcountput := unassignedCount_put (c := c) hv
          have hlt : unassignedCount (put rho v c) < m := by omega
          obtain ⟨sigma, E₂, hle₂, hE₂, hcard₂, hforce₂, hterm⟩ :=
            ih (unassignedCount (put rho v c)) hlt (put rho v c) rfl
          obtain ⟨E₁, hE₁, hcard₁, hforce₁⟩ := singleton_force_support hv havail
          refine ⟨sigma, E₁ ∪ E₂, le_trans (le_put hv) hle₂,
            Finset.union_subset hE₁ hE₂, ?_, ?_, hterm⟩
          · have hcardu := Finset.card_union_le E₁ E₂
            omega
          · intro f hgood hf
            obtain ⟨hgood₁, hgood₂⟩ := (goodOn_union_iff E₁ E₂ f).mp hgood
            exact hforce₂ f hgood₂ (hforce₁ f hgood₁ hf)
        · have hclosed : Closed G rho := by
            constructor
            · intro v w c hvw hv hw
              exact hc (Or.inl ⟨v, w, c, hvw, hv, hw⟩)
            · intro v hv
              have hzero : (available G rho v).card ≠ 0 := by
                intro hz
                exact hc (Or.inr ⟨v, hv, Finset.card_eq_zero.mp hz⟩)
              have hone : (available G rho v).card ≠ 1 := by
                intro ho
                obtain ⟨c, hsingleton⟩ := Finset.card_eq_one.mp ho
                exact hs ⟨v, c, hv, hsingleton⟩
              omega
          refine ⟨rho, ∅, le_refl rho, Finset.empty_subset _, ?_, ?_, Or.inr hclosed⟩
          · simp
          · intro f _ hf
            exact hf
  exact general (unassignedCount rho) rho rfl

theorem propagate (rho : Partial V) :
    ∃ sigma : Partial V, ∃ E : Finset (Sym2 V),
      LE rho sigma ∧ E ⊆ G.edgeFinset ∧ E.card ≤ 2 * Fintype.card V ∧
      (∀ f, GoodOn E f → Extends rho f → Extends sigma f) ∧
      (Conflict G sigma ∨ Closed G sigma) := by
  obtain ⟨sigma, E, hle, hE, hcard, hforce, hterm⟩ := propagate_aux (G := G) rho
  refine ⟨sigma, E, hle, hE, ?_, hforce, hterm⟩
  have hn := unassignedCount_le rho
  omega

end Replay

end

/- Maintained source: Replay/Hard.lean -/
open scoped BigOperators

noncomputable section

namespace Replay

variable {V : Type*} [Fintype V] [DecidableEq V]
variable (G : SimpleGraph V) [DecidableRel G.Adj]

def freqSet (rho : Partial V) (v : V) (c : Colour) : Finset V := by
  classical
  exact Finset.univ.filter fun w => G.Adj v w ∧ c ∈ domain G rho w

def freq (rho : Partial V) (v : V) (c : Colour) : ℕ :=
  (freqSet G rho v c).card

def Hard (rho : Partial V) (k : ℕ) (v : V) (c : Colour) : Prop :=
  k ≤ freq G rho v c

variable {G} {rho sigma : Partial V} {v w : V} {c c' : Colour} {d k : ℕ}

theorem mem_freqSet_iff :
    w ∈ freqSet G rho v c ↔ G.Adj v w ∧ c ∈ domain G rho w := by
  classical
  simp [freqSet]

theorem colour_mem_or_mem (s : Finset Colour) (hs : 2 ≤ s.card)
    (hne : c ≠ c') : c ∈ s ∨ c' ∈ s := by
  classical
  by_contra h
  have hc : c ∉ s := fun hc => h (Or.inl hc)
  have hc' : c' ∉ s := fun hc' => h (Or.inr hc')
  have hpair : ({c, c'} : Finset Colour) ⊆ Finset.univ \ s := by
    intro a ha
    rcases Finset.mem_insert.mp ha with ha | ha
    · subst a
      simp [hc]
    · have ha' : a = c' := Finset.mem_singleton.mp ha
      subst a
      simp [hc']
  have hpaircard := Finset.card_le_card hpair
  have hcc' : c ∉ ({c'} : Finset Colour) := by simpa using hne
  rw [Finset.card_insert_of_notMem hcc', Finset.card_singleton] at hpaircard
  have hdiff := Finset.card_sdiff_add_card_eq_card (Finset.subset_univ s)
  have hthree : (Finset.univ : Finset Colour).card = 3 := by simp [Colour]
  omega

theorem freq_pair_ge_degree (hclosed : Closed G rho)
    (hv : IsThree G rho v) (hne : c ≠ c') :
    G.degree v ≤ freq G rho v c + freq G rho v c' := by
  classical
  have hcover : G.neighborFinset v ⊆ freqSet G rho v c ∪ freqSet G rho v c' := by
    intro w hw
    have hadj : G.Adj v w := by simpa using hw
    have hun : rho w = none := isThree_neighbors_unassigned hv w hadj
    have hcard := closed_domain_card_ge hclosed hun
    rcases colour_mem_or_mem (domain G rho w) hcard hne with hc | hc'
    · exact Finset.mem_union.mpr (Or.inl (mem_freqSet_iff.mpr ⟨hadj, hc⟩))
    · exact Finset.mem_union.mpr (Or.inr (mem_freqSet_iff.mpr ⟨hadj, hc'⟩))
  calc
    G.degree v = (G.neighborFinset v).card := rfl
    _ ≤ (freqSet G rho v c ∪ freqSet G rho v c').card := Finset.card_le_card hcover
    _ ≤ freq G rho v c + freq G rho v c' := Finset.card_union_le _ _

theorem nonhard_unique (hclosed : Closed G rho)
    (hv : IsThree G rho v) (hdegree : d ≤ G.degree v)
    (hc : freq G rho v c < d / 2)
    (hc' : freq G rho v c' < d / 2) : c = c' := by
  by_contra hne
  have hpair := freq_pair_ge_degree hclosed hv hne
  have hhalf := Nat.div_mul_le_self d 2
  omega

theorem hard_of_ne_nonhard (hclosed : Closed G rho)
    (hv : IsThree G rho v) (hdegree : d ≤ G.degree v)
    (hdefault : freq G rho v c' < d / 2) (hne : c ≠ c') :
    Hard G rho (d / 2) v c := by
  by_contra h
  have hc : freq G rho v c < d / 2 := Nat.lt_of_not_ge h
  exact hne (nonhard_unique hclosed hv hdegree hc hdefault)

theorem hard_ne_default (hclosed : Closed G rho)
    (hv : IsThree G rho v) (hdegree : d ≤ G.degree v)
    (hdefault : ¬ Hard G rho (d / 2) v c') (hne : c ≠ c') :
    Hard G rho (d / 2) v c :=
  hard_of_ne_nonhard hclosed hv hdegree (Nat.lt_of_not_ge hdefault) hne

theorem all_hard_or_unique_default (hclosed : Closed G rho)
    (hv : IsThree G rho v) (hdegree : d ≤ G.degree v) :
    (∀ c, Hard G rho (d / 2) v c) ∨
      ∃ default, ¬ Hard G rho (d / 2) v default ∧
        ∀ c, c ≠ default → Hard G rho (d / 2) v c := by
  classical
  by_cases h : ∀ c, Hard G rho (d / 2) v c
  · exact Or.inl h
  · obtain ⟨default, hdefault⟩ := not_forall.mp h
    exact Or.inr ⟨default, hdefault,
      fun c hne => hard_ne_default hclosed hv hdegree hdefault hne⟩

theorem half_pos (hd : 2 ≤ d) : 0 < d / 2 := by omega

theorem le_three_mul_half (hd : 2 ≤ d) : d ≤ 3 * (d / 2) := by omega

theorem rankWeight_drop_on_freq (hLE : LE rho sigma)
    (hclosed : Closed G rho) (hv : IsThree G rho v)
    (hsv : sigma v = some c) (hw : w ∈ freqSet G rho v c) :
    rankWeight G sigma w + 1 ≤ rankWeight G rho w := by
  classical
  obtain ⟨hadj, hc⟩ := mem_freqSet_iff.mp hw
  have hun : rho w = none := isThree_neighbors_unassigned hv w hadj
  have htwo := closed_domain_card_ge hclosed hun
  cases hsw : sigma w with
  | some a =>
      simp only [rankWeight, domain_eq_of_some hsw, Finset.card_singleton,
        Nat.sub_self, zero_add]
      omega
  | none =>
      have hnot : c ∉ domain G sigma w := by
        rw [domain_eq_of_none hsw]
        intro hnew
        exact (mem_available_iff.mp hnew) v (G.adj_symm hadj) hsv
      have hsub : domain G sigma w ⊆ domain G rho w :=
        domain_mono_of_unassigned hLE hsw
      have hins : insert c (domain G sigma w) ⊆ domain G rho w := by
        intro a ha
        rcases Finset.mem_insert.mp ha with ha | ha
        · simpa only [ha] using hc
        · exact hsub ha
      have hcard := Finset.card_le_card hins
      rw [Finset.card_insert_of_notMem hnot] at hcard
      unfold rankWeight
      omega

theorem rank_drop_of_assignment (hLE : LE rho sigma)
    (hclosed : Closed G rho) (hv : IsThree G rho v)
    (hsv : sigma v = some c) :
    rank G sigma + freq G rho v c ≤ rank G rho := by
  classical
  have hpoint : ∀ w ∈ (Finset.univ : Finset V),
      rankWeight G sigma w + (if w ∈ freqSet G rho v c then 1 else 0) ≤
        rankWeight G rho w := by
    intro w _
    by_cases hw : w ∈ freqSet G rho v c
    · simpa only [if_pos hw] using rankWeight_drop_on_freq hLE hclosed hv hsv hw
    · simpa only [if_neg hw, add_zero] using rankWeight_mono hLE w
  have hsum := Finset.sum_le_sum hpoint
  have hcount : (∑ w : V, if w ∈ freqSet G rho v c then 1 else 0) =
      freq G rho v c := by
    exact (Finset.card_eq_sum_ite (Finset.subset_univ (freqSet G rho v c))).symm
  simpa only [rank, Finset.sum_add_distrib, hcount] using hsum

theorem rank_drop_of_hard (hLE : LE rho sigma)
    (hclosed : Closed G rho) (hv : IsThree G rho v)
    (hsv : sigma v = some c) (hhard : Hard G rho k v c) :
    rank G sigma + k ≤ rank G rho := by
  exact (Nat.add_le_add_left hhard _).trans
    (rank_drop_of_assignment hLE hclosed hv hsv)

end Replay

end

/- Maintained source: Replay/Tree.lean -/
universe u v w

namespace Replay.Tree

def Satisfies {Edge : Type u} {Model : Type w}
    (Holds : Edge → Model → Prop) (E : Finset Edge) (m : Model) : Prop :=
  ∀ e, e ∈ E → Holds e m

def nodes : ℕ → ℕ
  | 0 => 0
  | b + 1 => 1 + 9 * nodes b

structure LocalStep {Edge : Type u} {State : Type v} {Model : Type w}
    (rank : State → ℕ) (Holds : Edge → Model → Prop)
    (Extends : State → Model → Prop) (allowed : Finset Edge)
    (k L : ℕ) (s : State) where
  support : Finset Edge
  support_allowed : ∀ e, e ∈ support → e ∈ allowed
  support_card : support.card ≤ L
  count : ℕ
  count_le : count ≤ 9
  child : Fin count → State
  rank_decrease : ∀ i, rank (child i) + k ≤ rank s
  route : ∀ m, Extends s m → Satisfies Holds support m →
    ∃ i, Extends (child i) m

theorem bounded_certificate {Edge : Type u} {State : Type v} {Model : Type w}
    (rank : State → ℕ) (Holds : Edge → Model → Prop)
    (Extends : State → Model → Prop) (allowed : Finset Edge)
    (k L : ℕ)
    (step : ∀ s, Nonempty (LocalStep rank Holds Extends allowed k L s))
    (b : ℕ) (s : State) (hbudget : rank s < b * k) :
    ∃ E : Finset Edge,
      (∀ e, e ∈ E → e ∈ allowed) ∧
      E.card ≤ L * nodes b ∧
      ∀ m, Extends s m → ¬ Satisfies Holds E m := by
  classical
  induction b generalizing s with
  | zero =>
      simp only [Nat.zero_mul, Nat.not_lt_zero] at hbudget
  | succ b ih =>
      let T := Classical.choice (step s)
      have hchild : ∀ i : Fin T.count, rank (T.child i) < b * k := by
        intro i
        have hdecrease := T.rank_decrease i
        have hparent : rank s < b * k + k := by
          simpa only [Nat.succ_mul] using hbudget
        omega
      have hcert : ∀ i : Fin T.count, ∃ E : Finset Edge,
          (∀ e, e ∈ E → e ∈ allowed) ∧
          E.card ≤ L * nodes b ∧
          ∀ m, Extends (T.child i) m → ¬ Satisfies Holds E m := by
        intro i
        exact ih (T.child i) (hchild i)
      let childSupport (i : Fin T.count) : Finset Edge :=
        Classical.choose (hcert i)
      have hchildSupport : ∀ i : Fin T.count,
          (∀ e, e ∈ childSupport i → e ∈ allowed) ∧
          (childSupport i).card ≤ L * nodes b ∧
          ∀ m, Extends (T.child i) m →
            ¬ Satisfies Holds (childSupport i) m := by
        intro i
        exact Classical.choose_spec (hcert i)
      let E := T.support ∪ Finset.univ.biUnion childSupport
      refine ⟨E, ?_, ?_, ?_⟩
      · intro e he
        rcases Finset.mem_union.mp he with he | he
        · exact T.support_allowed e he
        · obtain ⟨i, _, hei⟩ := Finset.mem_biUnion.mp he
          exact (hchildSupport i).1 e hei
      · have hcardChildren : (Finset.univ.biUnion childSupport).card ≤
            T.count * (L * nodes b) := by
          simpa only [Finset.card_univ, Fintype.card_fin] using
            (Finset.card_biUnion_le_card_mul
              (Finset.univ : Finset (Fin T.count)) childSupport (L * nodes b)
              (fun i _ => (hchildSupport i).2.1))
        calc
          E.card ≤ T.support.card + (Finset.univ.biUnion childSupport).card :=
            Finset.card_union_le _ _
          _ ≤ L + T.count * (L * nodes b) :=
            Nat.add_le_add T.support_card hcardChildren
          _ ≤ L + 9 * (L * nodes b) :=
            Nat.add_le_add_left
              (Nat.mul_le_mul_right (L * nodes b) T.count_le) L
          _ = L * nodes (b + 1) := by
            rw [nodes]
            ring
      · intro m hstate hE
        have hlocal : Satisfies Holds T.support m := by
          intro e he
          exact hE e (Finset.mem_union_left _ he)
        obtain ⟨i, hmodel⟩ := T.route m hstate hlocal
        apply (hchildSupport i).2.2 m hmodel
        intro e he
        apply hE e
        exact Finset.mem_union_right _
          (Finset.mem_biUnion.mpr ⟨i, Finset.mem_univ i, he⟩)

end Replay.Tree

/- Maintained source: Replay/Step.lean -/
namespace Replay
namespace Step

variable {V : Type*} [Fintype V] [DecidableEq V]

/-- A raw branch assignment. Equal selected vertices require compatible colors. -/
def assign2 (rho : Partial V) (a : V) (ca : Colour)
    (b : V) (cb : Colour) : Partial V :=
  Function.update (Function.update rho a (some ca)) b (some cb)

theorem assign2_le (rho : Partial V) (a b : V) (ca cb : Colour)
    (ha : rho a = none) (hb : rho b = none) :
    LE rho (assign2 rho a ca b cb) := by
  intro v c hc
  have hva : v ≠ a := by
    intro h
    subst v
    rw [ha] at hc
    contradiction
  have hvb : v ≠ b := by
    intro h
    subst v
    rw [hb] at hc
    contradiction
  simpa [assign2, Function.update_apply, hva, hvb] using hc

theorem assign2_left (rho : Partial V) (a b : V) (ca cb : Colour)
    (hcompat : a = b → ca = cb) :
    assign2 rho a ca b cb a = some ca := by
  by_cases hab : a = b
  · subst b
    simp [assign2, Function.update_apply, hcompat rfl]
  · simp [assign2, Function.update_apply, hab]

theorem assign2_right (rho : Partial V) (a b : V) (ca cb : Colour) :
    assign2 rho a ca b cb b = some cb := by
  simp [assign2, Function.update_apply]

theorem extends_assign2 (rho : Partial V) (a b : V) (f : V → Colour)
    (hf : Extends rho f) :
    Extends (assign2 rho a (f a) b (f b)) f := by
  intro v c hc
  by_cases hvb : v = b
  · subst v
    simpa [assign2, Function.update_apply] using hc
  · by_cases hva : v = a
    · subst v
      simpa [assign2, Function.update_apply, hvb] using hc
    · apply hf v c
      simpa [assign2, Function.update_apply, hva, hvb] using hc

noncomputable def pairs (a b : V) (allowed : Colour → Colour → Prop) :
    Finset (Colour × Colour) := by
  classical
  exact Finset.univ.filter fun p => (a = b → p.1 = p.2) ∧ allowed p.1 p.2

theorem mem_pairs_iff (a b : V) (allowed : Colour → Colour → Prop)
    (p : Colour × Colour) :
    p ∈ pairs a b allowed ↔
      (a = b → p.1 = p.2) ∧ allowed p.1 p.2 := by
  classical
  simp [pairs]

theorem pairs_card_le (a b : V) (allowed : Colour → Colour → Prop) :
    (pairs a b allowed).card ≤ 9 := by
  classical
  calc
    (pairs a b allowed).card ≤
        (Finset.univ : Finset (Colour × Colour)).card :=
      Finset.card_filter_le _ _
    _ = 9 := by simp [Colour]

theorem pair_of_coloring (a b : V) (allowed : Colour → Colour → Prop)
    (f : V → Colour) (hf : allowed (f a) (f b)) :
    (f a, f b) ∈ pairs a b allowed := by
  rw [mem_pairs_iff]
  exact ⟨fun h => congrArg f h, hf⟩

variable (G : SimpleGraph V) [DecidableRel G.Adj]

/-- A local contradiction is a split with no children. -/
theorem terminal_step (k L : ℕ) (rho : Partial V)
    (E : Finset (Sym2 V)) (hE : E ⊆ G.edgeFinset)
    (hcard : E.card ≤ L)
    (hfalse : ∀ f, GoodOn E f → Extends rho f → False) :
    Nonempty (Tree.LocalStep (rank G) EdgeHolds Extends G.edgeFinset k L rho) := by
  refine ⟨{
    support := E
    support_allowed := fun e he => hE he
    support_card := hcard
    count := 0
    count_le := by omega
    child := Fin.elim0
    rank_decrease := ?_
    route := ?_ }⟩
  · intro i
    exact Fin.elim0 i
  · intro f hf hgood
    exact False.elim (hfalse f
      ((goodOn_iff_forall_edgeHolds E f).2 hgood) hf)

/-- The finite pair branch, independent of the source of its local blocker. -/
theorem pair_step (k L : ℕ) (rho sigma : Partial V)
    (hLE : LE rho sigma) (hclosed : Closed G sigma)
    (E : Finset (Sym2 V)) (hE : E ⊆ G.edgeFinset)
    (hcard : E.card ≤ L) (a b : V)
    (ha : IsThree G sigma a) (hb : IsThree G sigma b)
    (allowed : Colour → Colour → Prop)
    (hhard : ∀ ca cb, (a = b → ca = cb) → allowed ca cb →
      Hard G sigma k a ca ∨ Hard G sigma k b cb)
    (hroute : ∀ f, GoodOn E f → Extends rho f →
      Extends sigma f ∧ allowed (f a) (f b)) :
    Nonempty (Tree.LocalStep (rank G) EdgeHolds Extends G.edgeFinset k L rho) := by
  classical
  let P := pairs a b allowed
  let A := { p : Colour × Colour // p ∈ P }
  let e : A ≃ Fin (Fintype.card A) := Fintype.equivFin A
  let child (i : Fin (Fintype.card A)) : Partial V :=
    assign2 sigma a (e.symm i).val.1 b (e.symm i).val.2
  have hcount : Fintype.card A ≤ 9 := by
    simpa only [A, P, Fintype.card_coe] using pairs_card_le a b allowed
  refine ⟨{
    support := E
    support_allowed := fun z hz => hE hz
    support_card := hcard
    count := Fintype.card A
    count_le := hcount
    child := child
    rank_decrease := ?_
    route := ?_ }⟩
  · intro i
    let p : A := e.symm i
    have hp : (a = b → p.val.1 = p.val.2) ∧ allowed p.val.1 p.val.2 :=
      (mem_pairs_iff a b allowed p.val).1 p.property
    have hchildLE : LE sigma (assign2 sigma a p.val.1 b p.val.2) :=
      assign2_le sigma a b p.val.1 p.val.2 ha.1 hb.1
    have hdrop : rank G (assign2 sigma a p.val.1 b p.val.2) + k ≤
        rank G sigma := by
      rcases hhard p.val.1 p.val.2 hp.1 hp.2 with hh | hh
      · exact rank_drop_of_hard hchildLE hclosed ha
          (assign2_left sigma a b p.val.1 p.val.2 hp.1) hh
      · exact rank_drop_of_hard hchildLE hclosed hb
          (assign2_right sigma a b p.val.1 p.val.2) hh
    exact hdrop.trans (rank_mono hLE)
  · intro f hf hgood
    obtain ⟨hsigma, hallowed⟩ := hroute f
      ((goodOn_iff_forall_edgeHolds E f).2 hgood) hf
    let p : A := ⟨(f a, f b), pair_of_coloring a b allowed f hallowed⟩
    refine ⟨e p, ?_⟩
    change Extends (assign2 sigma a (e.symm (e p)).val.1
      b (e.symm (e p)).val.2) f
    rw [e.symm_apply_apply]
    exact extends_assign2 sigma a b f hsigma

noncomputable def twoVertices (rho : Partial V) : Finset V := by
  classical
  exact Finset.univ.filter fun v =>
    rho v = none ∧ (available G rho v).card = 2

noncomputable def threeVertices (rho : Partial V) : Finset V := by
  classical
  exact Finset.univ.filter fun v => IsThree G rho v

theorem mem_twoVertices (rho : Partial V) (v : V) :
    v ∈ twoVertices G rho ↔ rho v = none ∧ (available G rho v).card = 2 := by
  classical
  simp [twoVertices]

theorem mem_threeVertices (rho : Partial V) (v : V) :
    v ∈ threeVertices G rho ↔ IsThree G rho v := by
  classical
  simp [threeVertices]

theorem isThree_of_not_two (rho : Partial V) (hclosed : Closed G rho)
    (v : V) (hv : rho v = none) (hnot : v ∉ twoVertices G rho) :
    IsThree G rho v := by
  have hlow := hclosed.lists v hv
  have hupp : (available G rho v).card ≤ 3 := available_card_le
  have hne : (available G rho v).card ≠ 2 := by
    intro hc
    exact hnot ((mem_twoVertices G rho v).2 ⟨hv, hc⟩)
  exact ⟨hv, available_card_eq_three_iff.mp (by omega)⟩

theorem isThree_not_two (rho : Partial V) (v : V)
    (hv : IsThree G rho v) : v ∉ twoVertices G rho := by
  intro htwo
  have hc := ((mem_twoVertices G rho v).1 htwo).2
  simp [hv.2, Colour] at hc

noncomputable def twoListFamily (rho : Partial V) :
    TwoLists G { v : V // v ∈ twoVertices G rho } :=
  TwoLists.ofFinset G Subtype.val Subtype.val_injective
    (fun v => available G rho v.val)
    (fun v => ((mem_twoVertices G rho v.val).1 v.property).2)

theorem twoListFamily_vert (rho : Partial V)
    (v : { v : V // v ∈ twoVertices G rho }) :
    (twoListFamily G rho).vert v = v.val := rfl

theorem twoListFamily_mem_iff (rho : Partial V)
    (v : { v : V // v ∈ twoVertices G rho }) (c : Colour) :
    c ∈ available G rho v.val ↔
      ∃ b, c = (twoListFamily G rho).choice v b := by
  exact TwoLists.ofFinset_mem_iff G Subtype.val Subtype.val_injective
    (fun v => available G rho v.val)
    (fun v => ((mem_twoVertices G rho v.val).1 v.property).2) v c

theorem twoListFamily_card (rho : Partial V) :
    Fintype.card { v : V // v ∈ twoVertices G rho } ≤ Fintype.card V := by
  classical
  simpa only [Fintype.card_coe] using Finset.card_le_univ (twoVertices G rho)

/-- Fill the unassigned positions of a partial state. -/
def fill (rho : Partial V) (g : V → Colour) (v : V) : Colour :=
  (rho v).getD (g v)

theorem fill_extends (rho : Partial V) (g : V → Colour) :
    Extends rho (fill rho g) := by
  intro v c hv
  simp [fill, hv]

theorem good_fill (rho : Partial V) (hclosed : Closed G rho)
    (g : V → Colour)
    (hmem : ∀ v, rho v = none → g v ∈ available G rho v)
    (hrest : ∀ v w, rho v = none → rho w = none →
      G.Adj v w → g v ≠ g w) : Good G (fill rho g) := by
  intro v w hvw
  cases hv : rho v with
  | none =>
      cases hw : rho w with
      | none => simpa [fill, hv, hw] using hrest v w hv hw hvw
      | some c =>
          simp only [fill, hv, hw, Option.getD_none, Option.getD_some]
          intro heq
          apply (mem_available_iff.mp (hmem v hv)) w hvw
          simpa [hw, heq]
  | some c =>
      cases hw : rho w with
      | none =>
          simp only [fill, hv, hw, Option.getD_none, Option.getD_some]
          intro heq
          apply (mem_available_iff.mp (hmem w hw)) v hvw.symm
          simpa [hv, heq]
      | some d =>
          simp only [fill, hv, hw, Option.getD_some]
          intro heq
          apply hclosed.proper v w c hvw hv
          simpa [heq] using hw

/-- A model of the two-list formula with all default units colors the graph. -/
theorem good_of_default_model (rho : Partial V) (hclosed : Closed G rho)
    (default : V → Colour)
    (hdefault : ∀ v ∈ threeVertices G rho, ∀ w ∈ threeVertices G rho,
      G.Adj v w → default v ≠ default w)
    (a : { v : V // v ∈ twoVertices G rho } → Bool)
    (ha : TwoCNF.Models a (TwoCNF.withUnits
      (TwoLists.graphFormula (twoListFamily G rho))
      (TwoLists.defaultUnits (twoListFamily G rho)
        (threeVertices G rho) default))) :
    ∃ f : V → Colour, Good G f := by
  classical
  let T := twoListFamily G rho
  obtain ⟨hrr, hsr⟩ := (TwoLists.models_withDefaultUnits_iff T
    (threeVertices G rho) default a).1 ha
  let g : V → Colour := fun v =>
    if h : v ∈ twoVertices G rho then T.choice ⟨v, h⟩ (a ⟨v, h⟩)
    else default v
  have hR (v : V) (hv : v ∈ twoVertices G rho) :
      g v = T.choice ⟨v, hv⟩ (a ⟨v, hv⟩) := by simp [g, hv]
  have hS (v : V) (hv : v ∉ twoVertices G rho) : g v = default v := by
    simp [g, hv]
  refine ⟨fill rho g, good_fill G rho hclosed g ?_ ?_⟩
  · intro v hv
    by_cases hvR : v ∈ twoVertices G rho
    · rw [hR v hvR]
      exact (twoListFamily_mem_iff G rho ⟨v, hvR⟩ _).2 ⟨a ⟨v, hvR⟩, rfl⟩
    · have hvS := isThree_of_not_two G rho hclosed v hv hvR
      rw [hvS.2]
      exact Finset.mem_univ _
  · intro v w hv hw hvw
    by_cases hvR : v ∈ twoVertices G rho
    · by_cases hwR : w ∈ twoVertices G rho
      · rw [hR v hvR, hR w hwR]
        exact hrr ⟨v, hvR⟩ ⟨w, hwR⟩ hvw
      · have hwS : w ∈ threeVertices G rho :=
          (mem_threeVertices G rho w).2
            (isThree_of_not_two G rho hclosed w hw hwR)
        rw [hR v hvR, hS w hwR]
        exact (hsr w hwS ⟨v, hvR⟩ hvw.symm).symm
    · have hvS : v ∈ threeVertices G rho :=
        (mem_threeVertices G rho v).2
          (isThree_of_not_two G rho hclosed v hv hvR)
      by_cases hwR : w ∈ twoVertices G rho
      · rw [hS v hvR, hR w hwR]
        exact hsr v hvS ⟨w, hwR⟩ hvw
      · have hwS : w ∈ threeVertices G rho :=
          (mem_threeVertices G rho w).2
            (isThree_of_not_two G rho hclosed w hw hwR)
        rw [hS v hvR, hS w hwR]
        exact hdefault v hvS w hwS hvw

/-- The globally noncolorable graph forces a contradiction among default units. -/
theorem unsat_default_units (rho : Partial V) (hclosed : Closed G rho)
    (hnon : ¬ ∃ f : V → Colour, Good G f)
    (default : V → Colour)
    (hdefault : ∀ v ∈ threeVertices G rho, ∀ w ∈ threeVertices G rho,
      G.Adj v w → default v ≠ default w) :
    ¬ TwoCNF.Satisfiable (TwoCNF.withUnits
      (TwoLists.graphFormula (twoListFamily G rho))
      (TwoLists.defaultUnits (twoListFamily G rho)
        (threeVertices G rho) default)) := by
  rintro ⟨a, ha⟩
  exact hnon (good_of_default_model G rho hclosed default hdefault a ha)

/-- One or two default vertices whose joint default assignment is excluded. -/
theorem default_blocker (rho : Partial V) (hclosed : Closed G rho)
    (hnon : ¬ ∃ f : V → Colour, Good G f) (default : V → Colour)
    (hsat : TwoCNF.Satisfiable (TwoLists.graphFormula (twoListFamily G rho))) :
    ∃ a b : V, ∃ B : Finset (Sym2 V),
      IsThree G rho a ∧ IsThree G rho b ∧ B ⊆ G.edgeFinset ∧
      B.card ≤ 4 * Fintype.card V + 2 ∧
      ∀ f, GoodOn B f →
        (∀ w, ∃ c, f ((twoListFamily G rho).vert w) =
          (twoListFamily G rho).choice w c) →
        f a ≠ default a ∨ f b ≠ default b := by
  classical
  let S := threeVertices G rho
  by_cases hbad : ∃ a ∈ S, ∃ b ∈ S,
      G.Adj a b ∧ default a = default b
  · obtain ⟨a, ha, b, hb, hab, hcolor⟩ := hbad
    refine ⟨a, b, {s(a, b)}, (mem_threeVertices G rho a).1 ha,
      (mem_threeVertices G rho b).1 hb, ?_, ?_, ?_⟩
    · intro e he
      have heq := Finset.mem_singleton.mp he
      subst e
      simpa only [SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet] using hab
    · simp only [Finset.card_singleton]
      omega
    · intro f hf _
      by_cases hfa : f a = default a
      · right
        intro hfb
        apply hf a b (Finset.mem_singleton_self _)
        rw [hfa, hfb, hcolor]
      · exact Or.inl hfa
  · have hproper : ∀ a ∈ threeVertices G rho, ∀ b ∈ threeVertices G rho,
        G.Adj a b → default a ≠ default b := by
      intro a ha b hb hab hcolor
      exact hbad ⟨a, ha, b, hb, hab, hcolor⟩
    have hunsat := unsat_default_units G rho hclosed hnon default hproper
    obtain ⟨a, ha, b, hb, B, hB, hcard, hblock⟩ :=
      TwoLists.sparse_default_obstruction (twoListFamily G rho)
        (threeVertices G rho) default hsat hunsat
    refine ⟨a, b, B, (mem_threeVertices G rho a).1 ha,
      (mem_threeVertices G rho b).1 hb, hB, ?_, ?_⟩
    · exact hcard.trans (Nat.add_le_add_right
        (Nat.mul_le_mul_left 4 (twoListFamily_card G rho)) 2)
    · intro f hf hlist
      by_cases hfa : f a = default a
      · right
        exact fun hfb => hblock f hf hlist hfa hfb
      · exact Or.inl hfa

theorem card_union3_le (A B C : Finset (Sym2 V)) :
    ((A ∪ B) ∪ C).card ≤ A.card + B.card + C.card := by
  classical
  exact (Finset.card_union_le (A ∪ B) C).trans
    (Nat.add_le_add_right (Finset.card_union_le A B) C.card)

/-- The sparse local split used by the abstract finite-branch certificate theorem. -/
theorem local_split (d : ℕ) (hd : 2 ≤ d)
    (hdegree : ∀ v, d ≤ G.degree v)
    (hnon : ¬ ∃ f : V → Colour, Good G f) (rho : Partial V) :
    Nonempty (Tree.LocalStep (rank G) EdgeHolds Extends G.edgeFinset
      (d / 2) (10 * Fintype.card V) rho) := by
  classical
  have hn : 0 < Fintype.card V := by
    by_contra hpos
    have hzero : Fintype.card V = 0 := by omega
    letI : IsEmpty V := Fintype.card_eq_zero_iff.mp hzero
    apply hnon
    exact ⟨fun _ => 0, fun v => isEmptyElim v⟩
  obtain ⟨sigma, F, hLE, hF, hFcard, hforce, hstate⟩ :=
    propagate (G := G) rho
  rcases hstate with hconflict | hclosed
  · obtain ⟨B, hB, hBcard, hblock⟩ := conflict_support hconflict
    apply terminal_step G (d / 2) (10 * Fintype.card V) rho (F ∪ B)
    · exact Finset.union_subset hF hB
    · have hu := Finset.card_union_le F B
      omega
    · intro f hf hext
      obtain ⟨hfF, hfB⟩ := (goodOn_union_iff F B f).1 hf
      exact hblock f hfB (hforce f hfF hext)
  · obtain ⟨Q, hQ, hQcard, hQlist⟩ := list_reasons (G := G) sigma
    let T := twoListFamily G sigma
    have hlist : ∀ f, GoodOn Q f → Extends sigma f →
        ∀ w, ∃ c, f (T.vert w) = T.choice w c := by
      intro f hf hext w
      change ∃ c, f w.val = (twoListFamily G sigma).choice w c
      apply (twoListFamily_mem_iff G sigma w (f w.val)).1
      obtain ⟨hw, hcard⟩ := (mem_twoVertices G sigma w.val).1 w.property
      exact hQlist f hf hext w.val hw hcard
    by_cases hsat : TwoCNF.Satisfiable (TwoLists.graphFormula T)
    · by_cases hall : ∃ v, IsThree G sigma v ∧
          ∀ c, Hard G sigma (d / 2) v c
      · obtain ⟨v, hv, hhard⟩ := hall
        apply pair_step G (d / 2) (10 * Fintype.card V) rho sigma hLE hclosed
          F hF (by omega) v v hv hv (fun _ _ => True)
        · intro ca cb _ _
          exact Or.inl (hhard ca)
        · intro f hf hext
          exact ⟨hforce f hf hext, True.intro⟩
      · have hdefaults : ∀ v : V, ∃ c : Colour,
            IsThree G sigma v →
              ¬ Hard G sigma (d / 2) v c ∧
              ∀ c', c' ≠ c → Hard G sigma (d / 2) v c' := by
          intro v
          by_cases hv : IsThree G sigma v
          · rcases all_hard_or_unique_default hclosed hv (hdegree v) with
              hhard | ⟨c, hnonhard, hhard⟩
            · exact False.elim (hall ⟨v, hv, hhard⟩)
            · exact ⟨c, fun _ => ⟨hnonhard, hhard⟩⟩
          · exact ⟨0, fun h => False.elim (hv h)⟩
        choose default hdefault using hdefaults
        obtain ⟨a, b, B, ha, hb, hB, hBcard, hblock⟩ :=
          default_blocker G sigma hclosed hnon default hsat
        let E := (F ∪ Q) ∪ B
        have hE : E ⊆ G.edgeFinset :=
          Finset.union_subset (Finset.union_subset hF hQ) hB
        have hEcard : E.card ≤ 10 * Fintype.card V := by
          change ((F ∪ Q) ∪ B).card ≤ 10 * Fintype.card V
          have hu := card_union3_le F Q B
          omega
        apply pair_step G (d / 2) (10 * Fintype.card V) rho sigma hLE hclosed
          E hE hEcard a b ha hb
          (fun ca cb => ca ≠ default a ∨ cb ≠ default b)
        · intro ca cb _ hchoice
          rcases hchoice with hca | hcb
          · exact Or.inl ((hdefault a ha).2 ca hca)
          · exact Or.inr ((hdefault b hb).2 cb hcb)
        · intro f hf hext
          obtain ⟨hfFQ, hfB⟩ := (goodOn_union_iff (F ∪ Q) B f).1 hf
          obtain ⟨hfF, hfQ⟩ := (goodOn_union_iff F Q f).1 hfFQ
          have hsigma := hforce f hfF hext
          exact ⟨hsigma, hblock f hfB (hlist f hfQ hsigma)⟩
    · obtain ⟨B, hB, hBcard, hblock⟩ := TwoLists.sparse_list_obstruction T hsat
      have hBcard' : B.card ≤ 4 * Fintype.card V :=
        hBcard.trans (Nat.mul_le_mul_left 4 (twoListFamily_card G sigma))
      apply terminal_step G (d / 2) (10 * Fintype.card V) rho ((F ∪ Q) ∪ B)
      · exact Finset.union_subset (Finset.union_subset hF hQ) hB
      · have hu := card_union3_le F Q B
        omega
      · intro f hf hext
        obtain ⟨hfFQ, hfB⟩ := (goodOn_union_iff (F ∪ Q) B f).1 hf
        obtain ⟨hfF, hfQ⟩ := (goodOn_union_iff F Q f).1 hfFQ
        exact hblock f hfB (hlist f hfQ (hforce f hfF hext))

end Step
end Replay

/- Maintained source: Replay/Sparse.lean -/
namespace Replay.Sparse

def coefficient (b : ℕ) : ℕ := 10 * Tree.nodes b

theorem sparse_obstruction {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (d b : ℕ)
    (hd : 2 ≤ d) (hdegree : ∀ v, d ≤ G.degree v)
    (hbudget : 2 * Fintype.card V < b * (d / 2))
    (hnon : ¬ ∃ f : V → Colour, Good G f) :
    ∃ E : Finset (Sym2 V),
      E ⊆ G.edgeFinset ∧
      E.card ≤ coefficient b * Fintype.card V ∧
      ¬ ∃ f : V → Colour, GoodOn E f := by
  classical
  let root : Partial V := fun _ => none
  have hroot : rank G root < b * (d / 2) := by
    simpa only [root, rank_empty] using hbudget
  obtain ⟨E, hE, hcard, hno⟩ :=
    Tree.bounded_certificate (rank G) EdgeHolds Extends G.edgeFinset
      (d / 2) (10 * Fintype.card V)
      (fun rho => Step.local_split G d hd hdegree hnon rho) b root hroot
  refine ⟨E, hE, ?_, ?_⟩
  · calc
      E.card ≤ (10 * Fintype.card V) * Tree.nodes b := hcard
      _ = coefficient b * Fintype.card V := by
        unfold coefficient
        ring
  · rintro ⟨f, hf⟩
    apply hno f (extends_empty f)
    exact (goodOn_iff_forall_edgeHolds E f).mp hf

end Replay.Sparse

/- Maintained source: Replay/Final.lean -/
open scoped BigOperators

namespace Replay

theorem good_iff_colorable {V : Type*} (G : SimpleGraph V) :
    (∃ f : V → Colour, Good G f) ↔ G.Colorable 3 := by
  constructor
  · rintro ⟨f, hf⟩
    exact ⟨SimpleGraph.Coloring.mk f (fun {v w} h => hf v w h)⟩
  · rintro ⟨f⟩
    exact ⟨f, fun v w h => f.valid h⟩

theorem critical_support_eq {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (hcritical : ∀ e ∈ G.edgeSet, (G.deleteEdges {e}).Colorable 3)
    (E : Finset (Sym2 V)) (hE : E ⊆ G.edgeFinset)
    (hno : ¬ ∃ f : V → Colour, GoodOn E f) : E = G.edgeFinset := by
  classical
  apply Finset.Subset.antisymm hE
  intro e he
  by_contra heE
  obtain ⟨f⟩ := hcritical e (SimpleGraph.mem_edgeFinset.mp he)
  apply hno
  refine ⟨f, ?_⟩
  intro v w hvw
  have hGvw : G.Adj v w :=
    (SimpleGraph.mem_edgeSet G).mp (SimpleGraph.mem_edgeFinset.mp (hE hvw))
  have hne : s(v, w) ≠ e := by
    intro h
    apply heE
    simpa only [h] using hvw
  apply f.valid
  exact SimpleGraph.deleteEdges_adj.mpr
    ⟨hGvw, by simpa only [Set.mem_singleton_iff] using hne⟩

theorem degree_bound_of_edge_bound {n d C : ℕ}
    (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    (hn : 0 < n) (hdegree : ∀ v, d ≤ G.degree v)
    (hedges : G.edgeFinset.card ≤ C * n) : d ≤ 2 * C := by
  classical
  have hsum : n * d ≤ 2 * (C * n) := by
    calc
      n * d = ∑ _v : Fin n, d := by simp
      _ ≤ ∑ v : Fin n, G.degree v :=
        Finset.sum_le_sum (fun v _ => hdegree v)
      _ = 2 * G.edgeFinset.card := G.sum_degrees_eq_twice_card_edges
      _ ≤ 2 * (C * n) := Nat.mul_le_mul_left 2 hedges
  have hmul : n * d ≤ n * (2 * C) := by
    simpa only [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using hsum
  exact Nat.le_of_mul_le_mul_left hmul hn

theorem natural_degree_budget (ε : ℝ) {n d b : ℕ}
    (hn : 0 < n) (hd : 2 ≤ d)
    (hdegree : ε * (n : ℝ) ≤ (d : ℝ))
    (hb : 6 < ε * (b : ℝ)) : 2 * n < b * (d / 2) := by
  have hdhalfNat : d ≤ 3 * (d / 2) := by omega
  have hdhalf : (d : ℝ) ≤ 3 * ((d / 2 : ℕ) : ℝ) := by
    exact_mod_cast hdhalfNat
  have hnreal : 0 < (n : ℝ) := by exact_mod_cast hn
  have hcalc : 6 * (n : ℝ) < 3 * ((b : ℝ) * ((d / 2 : ℕ) : ℝ)) := by
    calc
      6 * (n : ℝ) < (ε * (b : ℝ)) * (n : ℝ) :=
        mul_lt_mul_of_pos_right hb hnreal
      _ = (ε * (n : ℝ)) * (b : ℝ) := by ring
      _ ≤ (d : ℝ) * (b : ℝ) :=
        mul_le_mul_of_nonneg_right hdegree (Nat.cast_nonneg b)
      _ ≤ (3 * ((d / 2 : ℕ) : ℝ)) * (b : ℝ) :=
        mul_le_mul_of_nonneg_right hdhalf (Nat.cast_nonneg b)
      _ = 3 * ((b : ℝ) * ((d / 2 : ℕ) : ℝ)) := by ring
  have hreal : (2 : ℝ) * (n : ℝ) < (b : ℝ) * ((d / 2 : ℕ) : ℝ) := by
    linarith
  exact_mod_cast hreal

theorem not_erdosCriticalMinimumDegree_of_sparse (C : ℕ → ℕ)
    (hSparse : ∀ {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
      (d b : ℕ),
      2 ≤ d →
      (∀ v, d ≤ G.degree v) →
      2 * n < b * (d / 2) →
      (¬ ∃ f : Fin n → Colour, Good G f) →
      ∃ E : Finset (Sym2 (Fin n)),
        E ⊆ G.edgeFinset ∧ E.card ≤ C b * n ∧
          ¬ ∃ f : Fin n → Colour, GoodOn E f) :
    ¬ FullOldProblems.ErdosCriticalMinimumDegree := by
  classical
  rintro ⟨ε, hε, harb⟩
  obtain ⟨b, hb⟩ := exists_nat_gt (6 / ε)
  have hb' : 6 < ε * (b : ℝ) := by
    simpa only [mul_comm] using (div_lt_iff₀ hε).mp hb
  obtain ⟨N, hN⟩ := exists_nat_gt ((3 + 2 * (C b : ℝ)) / ε)
  have hN' : (3 : ℝ) + 2 * (C b : ℝ) < ε * (N : ℝ) := by
    simpa only [mul_comm] using (div_lt_iff₀ hε).mp hN
  obtain ⟨n, hnN, G, hcritical, hdegree⟩ := harb (N + 1)
  have hn : 0 < n := by omega
  have hNn : (N : ℝ) ≤ (n : ℝ) := by
    exact_mod_cast (show N ≤ n by omega)
  have hlarge : (3 : ℝ) + 2 * (C b : ℝ) < ε * (n : ℝ) :=
    hN'.trans_le (mul_le_mul_of_nonneg_left hNn hε.le)
  haveI : Nonempty (Fin n) := ⟨⟨0, hn⟩⟩
  let d := G.minDegree
  obtain ⟨v, hv⟩ := G.exists_minimal_degree_vertex
  have hdreal : ε * (n : ℝ) ≤ (d : ℝ) := by
    change ε * (n : ℝ) ≤ (G.minDegree : ℝ)
    rw [hv]
    simpa only [SimpleGraph.ncard_neighborSet] using hdegree v
  have hdgt : (3 : ℝ) < (d : ℝ) := by
    have hC : (0 : ℝ) ≤ (C b : ℝ) := Nat.cast_nonneg _
    linarith
  have hd : 2 ≤ d := by
    have hdNat : 3 < d := by exact_mod_cast hdgt
    omega
  have halldegree : ∀ v, d ≤ G.degree v := fun v => G.minDegree_le_degree v
  have hbudget : 2 * n < b * (d / 2) :=
    natural_degree_budget ε hn hd hdreal hb'
  have hno : ¬ ∃ f : Fin n → Colour, Good G f := by
    intro hf
    have hc := (good_iff_colorable G).mp hf
    have hle := hc.chromaticNumber_le
    rw [hcritical.1] at hle
    norm_num at hle
  obtain ⟨E, hE, hEcard, hEno⟩ :=
    hSparse G d b hd halldegree hbudget hno
  have hdeletions : ∀ e ∈ G.edgeSet, (G.deleteEdges {e}).Colorable 3 := by
    intro e he
    exact SimpleGraph.chromaticNumber_le_iff_colorable.mp
      (le_of_eq (hcritical.2 e he))
  have hEq : E = G.edgeFinset := critical_support_eq G hdeletions E hE hEno
  have hfullcard : G.edgeFinset.card ≤ C b * n := by
    simpa only [hEq] using hEcard
  have hdUpper : d ≤ 2 * C b :=
    degree_bound_of_edge_bound G hn halldegree hfullcard
  have hdUpperReal : (d : ℝ) ≤ 2 * (C b : ℝ) := by exact_mod_cast hdUpper
  linarith

end Replay

/- Maintained source: Replay/Target.lean -/
theorem target : ¬ FullOldProblems.ErdosCriticalMinimumDegree := by
  apply Replay.not_erdosCriticalMinimumDegree_of_sparse Replay.Sparse.coefficient
  intro n G hdec d b hd hdegree hbudget hnon
  simpa only [Fintype.card_fin] using
    (Replay.Sparse.sparse_obstruction G d b hd hdegree
      (by simpa only [Fintype.card_fin] using hbudget) hnon)