Erdos Critical Minimum Degree

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