module

public import Papers.OaiPairedStatesHamiltonian.Helpers.RootComponents
public import Papers.OaiPairedStatesHamiltonian.Helpers.Duality
public import Papers.OaiPairedStatesHamiltonian.Helpers.ForestGraph
public import Papers.OaiPairedStatesHamiltonian.Helpers.SpokeEdges

/-! Deleted spokes, the white-face tree, and the prescribed selected edges. -/

@[expose] public section

namespace OaiPairedStatesHamiltonian

set_option linter.style.openClassical false
set_option linter.style.longLine false
set_option linter.unusedVariables false
set_option backward.isDefEq.respectTransparency false
open Classical
attribute [local instance] propDecidable


section FaceRepresentatives

variable (T : SphereMap) (faces : Finset T.Face)
  (hfaces : ∀ d, ¬ (T.faceOf d ∈ faces ∧ T.faceOf (T.edgeInv d) ∈ faces))

-- @node: spokePieceOutside
/-- For [a sphere map](hyp:T) and [a set of selected faces](hyp:faces) such that
[no edge has selected faces on both sides](hyp:hfaces), the [outside-face assignment](goal)
[leaves an unselected face unchanged](step:1) and [sends a selected sector to the unselected
face across its supplying edge](step:2). -/
noncomputable def spokePieceOutside : SpokePiece T faces → {f : T.Face // f ∉ faces}
  | Sum.inl f => f
  | Sum.inr d => ⟨T.faceOf (T.edgeInv d.val), fun h => hfaces d.val ⟨d.property, h⟩⟩

-- @node: spokePieceOutside_across
/-- If no edge has selected faces on both sides and [every edge has a selected
face on at least one side](hyp:hcover), then [the pieces on the two sides of any directed
edge have the same outside face](goal). -/
lemma spokePieceOutside_across
    (hcover : ∀ d, T.faceOf d ∈ faces ∨ T.faceOf (T.edgeInv d) ∈ faces) (d : T.Dart) :
    spokePieceOutside T faces hfaces (spokePieceAt T faces d) =
      spokePieceOutside T faces hfaces (spokePieceAt T faces (T.edgeInv d)) := by
  by_cases hd : T.faceOf d ∈ faces
  · have hi : T.faceOf (T.edgeInv d) ∉ faces := fun h => hfaces d ⟨hd, h⟩
    simp only [spokePieceAt, dif_pos hd, dif_neg hi, spokePieceOutside]
  · have hi := (hcover d).resolve_left hd
    apply Subtype.ext
    simp only [spokePieceAt, dif_neg hd, dif_pos hi, spokePieceOutside]
    exact congrArg T.faceOf (T.edgeInv_involutive d).symm

-- @node: spokePieceOutside_eq_of_glued
/-- If no edge has selected faces on both sides, [every edge has a selected
face on at least one side](hyp:hcover), and [two pieces are identified by the equivalence
relation generated by gluing across edges](hyp:h), then [their outside faces agree](goal). -/
lemma spokePieceOutside_eq_of_glued
    (hcover : ∀ d, T.faceOf d ∈ faces ∨ T.faceOf (T.edgeInv d) ∈ faces)
    (a b : SpokePiece T faces)
    (h : Relation.EqvGen (spokePieceRelation T faces) a b) :
    spokePieceOutside T faces hfaces a = spokePieceOutside T faces hfaces b := by
  induction h with
  | rel a b h =>
    obtain ⟨d, rfl, rfl⟩ := h
    exact spokePieceOutside_across T faces hfaces hcover d
  | refl => rfl
  | symm _ _ _ ih => exact ih.symm
  | trans _ _ _ _ _ hab hbc => exact hab.trans hbc

-- @node: spokeFaceClass_outside
/-- If no edge has selected faces on both sides, then [each piece represents
the same glued face as its assigned unselected outside face](goal). -/
lemma spokeFaceClass_outside (a : SpokePiece T faces) :
    spokeFaceClass T faces a =
      spokeFaceClass T faces (Sum.inl (spokePieceOutside T faces hfaces a)) := by
  cases a with
  | inl f => rfl
  | inr d =>
    apply Quotient.sound
    apply Relation.EqvGen.rel
    refine ⟨d.val, ?_, ?_⟩
    · simp only [spokePieceAt, dif_pos d.property]
    · have hi : T.faceOf (T.edgeInv d.val) ∉ faces :=
        fun h => hfaces d.val ⟨d.property, h⟩
      simp only [spokePieceAt, dif_neg hi, spokePieceOutside]

-- @node: spokeFaceEquivOutside
/-- For [a sphere map](hyp:T) and [selected faces](hyp:faces), assuming [no edge has two
selected sides](hyp:hfaces) and [every edge has at least one selected side](hyp:hcover),
the [bijection between glued spoke faces and unselected original faces](goal) assigns
each glued face its outside face. -/
noncomputable def spokeFaceEquivOutside
    (hcover : ∀ d, T.faceOf d ∈ faces ∨ T.faceOf (T.edgeInv d) ∈ faces) :
    SpokeFace T faces ≃ {f : T.Face // f ∉ faces} where
  toFun := Quotient.lift (spokePieceOutside T faces hfaces)
    (spokePieceOutside_eq_of_glued T faces hfaces hcover)
  invFun f := spokeFaceClass T faces (Sum.inl f)
  left_inv := by
    intro f
    induction f using Quotient.inductionOn with
    | h a => exact (spokeFaceClass_outside T faces hfaces a).symm
  right_inv _ := rfl

end FaceRepresentatives

variable (T : SphereMap) (hT : IsSphereTriangulation T) (col : T.Face → Bool)
  (hcol : PartitionColoring T col) (t0 : T.Face)

-- @node: spokeAll_connected
/-- If the map is a sphere triangulation and adjacent faces have opposite
colors, then [the graph containing all black-face spokes is connected](goal). -/
lemma spokeAll_connected : (spokeGraphAll T col t0 hT hcol).IsConnectedMap := by
  let N := spokeRotation T hT (blackFaces T col t0) (black_faces_disjoint T col t0 hcol)
  change N.toSimpleGraph.Connected
  let : Nonempty T.Vertex := hT.props.1.nonempty
  let v0 : T.Vertex := Classical.choice inferInstance
  obtain ⟨d0, hd0⟩ := triangulation_has_dart_at_vertex T hT v0
  let : Nonempty T.Dart := ⟨d0⟩
  let : Nonempty N.Vertex := ⟨Sum.inl v0⟩
  have edge (d : T.Dart) :
      N.toSimpleGraph.connectedComponentMk (Sum.inl (T.vert d)) =
        N.toSimpleGraph.connectedComponentMk (Sum.inl (T.head d)) := by
    by_cases hb : normalizedColoring T col t0 (T.faceOf d) = true
    · exact spoke_side_component T hT _ _ d (Finset.mem_filter.mpr ⟨Finset.mem_univ _, hb⟩)
    · have hi : normalizedColoring T col t0 (T.faceOf (T.edgeInv d)) = true := by
        have hop := normalizedColoring_partition T col hcol t0 d
        cases he : normalizedColoring T col t0 (T.faceOf (T.edgeInv d)) <;>
          cases hf : normalizedColoring T col t0 (T.faceOf d) <;> simp_all
      have h := spoke_side_component T hT (blackFaces T col t0)
        (black_faces_disjoint T col t0 hcol) (T.edgeInv d)
        (Finset.mem_filter.mpr ⟨Finset.mem_univ _, hi⟩)
      have hh : T.head (T.edgeInv d) = T.vert d :=
        congrArg T.vert (T.edgeInv_involutive d)
      rw [hh] at h
      exact h.symm
  have originals (u v : T.Vertex) :
      N.toSimpleGraph.connectedComponentMk (Sum.inl u) =
        N.toSimpleGraph.connectedComponentMk (Sum.inl v) := by
    obtain ⟨p⟩ := hT.props.1.preconnected u v
    induction p with
    | nil => rfl
    | @cons u w v h p ih =>
      obtain ⟨hne, d, hu, hw⟩ := h
      have heq : N.toSimpleGraph.connectedComponentMk (Sum.inl u) =
          N.toSimpleGraph.connectedComponentMk (Sum.inl w) := by
        simpa only [hu, hw] using edge d
      exact heq.trans ih
  have all_vertices (v : N.Vertex) :
      N.toSimpleGraph.connectedComponentMk v =
        N.toSimpleGraph.connectedComponentMk (Sum.inl v0) := by
    cases v with
    | inl v => exact originals v v0
    | inr f =>
      obtain ⟨d, hd⟩ := T.faceOf_surjective hT.props.1 f.val
      have hf : T.faceOf d ∈ blackFaces T col t0 := hd.symm ▸ f.property
      have hc := spoke_corner_component T hT (blackFaces T col t0)
        (black_faces_disjoint T col t0 hcol) ⟨d, hf⟩
      have he : (⟨T.faceOf d, hf⟩ : blackFaces T col t0) = f := Subtype.ext hd
      rw [he] at hc
      exact hc.symm.trans (originals _ v0)
  refine ⟨?_⟩
  intro u v
  exact SimpleGraph.ConnectedComponent.exact ((all_vertices u).trans (all_vertices v).symm)
/-- For [a sphere map](hyp:T), [a face coloring](hyp:col), and [a designated outer
face](hyp:t0), the [white faces](goal) are the faces colored white after normalizing
the coloring so that the outer face is black. -/
abbrev WhiteFace := {f : T.Face // normalizedColoring T col t0 f = false}

-- @node: exists_whiteFaceEquiv
/-- If the map is a sphere triangulation and adjacent faces have opposite
colors, then [there is a bijection from all-spoke graph faces to white original
faces that sends the face incident to each black-face corner's outward spoke to the
original face across that corner's edge](goal). -/
lemma exists_whiteFaceEquiv :
    ∃ q : (spokeGraphAll T col t0 hT hcol).Face ≃ WhiteFace T col t0,
      ∀ d : SpokeCorner T (blackFaces T col t0),
        (q ((spokeGraphAll T col t0 hT hcol).faceOf (d, false))).val = T.faceOf (T.edgeInv d.val) := by
  have hwhite (f : T.Face) : f ∉ blackFaces T col t0 ↔
      normalizedColoring T col t0 f = false := by
    simp only [blackFaces, Finset.mem_filter, Finset.mem_univ, true_and, Bool.not_eq_true]
  have hcover (d : T.Dart) : T.faceOf d ∈ blackFaces T col t0 ∨
      T.faceOf (T.edgeInv d) ∈ blackFaces T col t0 := by
    by_cases hd : normalizedColoring T col t0 (T.faceOf d) = true
    · exact Or.inl (Finset.mem_filter.mpr ⟨Finset.mem_univ _, hd⟩)
    · apply Or.inr
      apply Finset.mem_filter.mpr
      refine ⟨Finset.mem_univ _, ?_⟩
      have hop := normalizedColoring_partition T col hcol t0 d
      cases h : normalizedColoring T col t0 (T.faceOf (T.edgeInv d)) <;>
        cases h' : normalizedColoring T col t0 (T.faceOf d) <;> simp_all
  let e : {f : T.Face // f ∉ blackFaces T col t0} ≃ WhiteFace T col t0 :=
    { toFun := fun f => ⟨f.val, (hwhite f.val).mp f.property⟩
      invFun := fun f => ⟨f.val, (hwhite f.val).mpr f.property⟩
      left_inv := fun _ => rfl
      right_inv := fun _ => rfl }
  let q := (spokeFaceEquivOutside T (blackFaces T col t0)
    (black_faces_disjoint T col t0 hcol) hcover).trans e
  refine ⟨q, ?_⟩
  intro d
  have hd := (Classical.choose_spec (exists_spokeBoundaryFace T hT
    (blackFaces T col t0) (black_faces_disjoint T col t0 hcol))).1 (d, false)
  exact (congrArg (fun f => (q f).val) hd).trans rfl

/-- For [a sphere map](hyp:T) that [is a sphere triangulation](hyp:hT), [a face
coloring](hyp:col) with [opposite colors across every edge](hyp:hcol), and [an outer
face](hyp:t0), the [white-face bijection](goal) identifies all-spoke graph faces with
original white faces, sending each outward spoke's incident face to the face across
the corresponding black-face edge. -/
noncomputable def whiteFaceEquiv : (spokeGraphAll T col t0 hT hcol).Face ≃ WhiteFace T col t0 :=
  Classical.choose (exists_whiteFaceEquiv T hT col hcol t0)

include hT in
-- @node: exists_stateCorner
/-- If the map is a sphere triangulation, then for [a state](hyp:s) and
[a nonouter black face](hyp:t), [there is a black-face spoke corner belonging to that
face whose vertex is the vertex assigned to it by the state](goal). -/
lemma exists_stateCorner (s : State T col t0) (t : blackNonOuter T col t0) :
    ∃ d : SpokeCorner T (blackFaces T col t0), T.faceOf d.val = t.val ∧ T.vert d.val = (s.val t).val := by
  have hv := s.property.incident t
  rw [triangulation_faceVertices_eq_image T hT] at hv
  obtain ⟨d, hd, hv⟩ := Finset.mem_image.mp hv
  have hf : T.faceOf d = t.val := (Finset.mem_filter.mp hd).2
  have ht : normalizedColoring T col t0 t.val = true :=
    (Finset.mem_filter.mp t.property).2.1
  exact ⟨⟨d, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hf ▸ ht⟩⟩, hf, hv⟩

include hT in
-- @node: stateCorner
/-- For [a sphere map](hyp:T) that [is a sphere triangulation](hyp:hT), [a face
coloring](hyp:col), [an outer face](hyp:t0), [a state](hyp:s), and [a nonouter black
face](hyp:t), the [state corner](goal) is a chosen corner of that face at the vertex
assigned to it by the state. -/
noncomputable def stateCorner (s : State T col t0) (t : blackNonOuter T col t0) :
    SpokeCorner T (blackFaces T col t0) := Classical.choose (exists_stateCorner T hT col t0 s t)

-- @node: def:white-tree
/-- For [a sphere map](hyp:T) that [is a sphere triangulation](hyp:hT), [a face
coloring](hyp:col) with [opposite colors across every edge](hyp:hcol), [an outer
face](hyp:t0), and [a state](hyp:s), the [deleted spokes](goal) are the spoke edges
at the state's assigned corners, one for each nonouter black face. -/
noncomputable def deletedSpokes (s : State T col t0) : Set (spokeGraphAll T col t0 hT hcol).Edge :=
  {e | ∃ t : blackNonOuter T col t0,
    e = (spokeGraphAll T col t0 hT hcol).edgeOf (stateCorner T hT col t0 s t, false)}

/-- For [a sphere map](hyp:T) that [is a sphere triangulation](hyp:hT), [a face
coloring](hyp:col) with [opposite colors across every edge](hyp:hcol), [an outer
face](hyp:t0), and [a state](hyp:s), the [white-face graph](goal) is the spanning
subgraph of the all-spoke graph's dual consisting of the state's deleted spoke edges. -/
noncomputable def whiteFaceGraph (s : State T col t0) : SimpleGraph (spokeGraphAll T col t0 hT hcol).Face :=
  ((spokeGraphAll T col t0 hT hcol).dual (spokeAll_connected T hT col hcol t0)).spanningGraph
    (deletedSpokes T hT col hcol t0 s)

/-- If the map is a sphere triangulation, then for [a state](hyp:s) and
[a nonouter black face](hyp:t), [the chosen state corner lies on that face and has
the vertex assigned to that face by the state](goal). -/
lemma stateCorner_spec (s : State T col t0) (t : blackNonOuter T col t0) :
    T.faceOf (stateCorner T hT col t0 s t).val = t.val ∧
      T.vert (stateCorner T hT col t0 s t).val = (s.val t).val :=
  Classical.choose_spec (exists_stateCorner T hT col t0 s t)

-- @node: deletedSpokes_corner_iff
/-- If the map is a sphere triangulation and adjacent faces have opposite
colors, then for [a state](hyp:s) and [a black-face corner](hyp:c),
[the corner's spoke is deleted exactly when its face is a nonouter black face and
its vertex is the vertex assigned to that face by the state](goal). -/
lemma deletedSpokes_corner_iff (s : State T col t0) (c : SpokeCorner T (blackFaces T col t0)) :
    (spokeGraphAll T col t0 hT hcol).edgeOf (c, false) ∈ deletedSpokes T hT col hcol t0 s ↔
      ∃ t : blackNonOuter T col t0,
        T.faceOf c.val = t.val ∧ T.vert c.val = (s.val t).val := by
  constructor
  · rintro ⟨t, he⟩
    have hc : c = stateCorner T hT col t0 s t :=
      congrArg (spokeEdgeEquiv T hT (blackFaces T col t0)
        (black_faces_disjoint T col t0 hcol)) he
    exact ⟨t, hc ▸ stateCorner_spec T hT col t0 s t⟩
  · rintro ⟨t, hf, hv⟩
    have hc : c = stateCorner T hT col t0 s t :=
      spoke_corner_eq_of_face_tail T hT _ c _
        (hf.trans (stateCorner_spec T hT col t0 s t).1.symm)
        (hv.trans (stateCorner_spec T hT col t0 s t).2.symm)
    exact ⟨t, by rw [hc]⟩

-- @node: retainedSpokes_connected
/-- If the map is a sphere triangulation, adjacent faces have opposite
colors, [the two states assign distinct vertices to every nonouter black
face](hyp:hpair), [the second state's opposite-edge graph is a forest](hyp:hforest),
and [the map has no separating triangle](hyp:hsep), then [the graph of spokes retained
after deleting the second state's spokes is connected](goal). -/
lemma retainedSpokes_connected (r s : State T col t0) (hpair : IsPair T col t0 r s)
    (hforest : QsForest T col t0 s) (hsep : TreesNoSeparatingTriangle T) :
    ((spokeGraphAll T col t0 hT hcol).spanningGraph
      (deletedSpokes T hT col hcol t0 s)ᶜ).Connected := by
  let N := spokeGraphAll T col t0 hT hcol
  let G := N.spanningGraph (deletedSpokes T hT col hcol t0 s)ᶜ
  let outer : blackFaces T col t0 := ⟨t0, by simp [blackFaces, normalizedColoring_self]⟩
  have link (f : blackFaces T col t0) (v : T.Vertex) (hv : v ∈ T.faceVertices f.val)
      (hret : ∀ t : blackNonOuter T col t0, t.val = f.val → v ≠ (s.val t).val) :
      G.connectedComponentMk (Sum.inr f) = G.connectedComponentMk (Sum.inl v) := by
    rw [triangulation_faceVertices_eq_image T hT] at hv
    obtain ⟨d, hd, hdv⟩ := Finset.mem_image.mp hv
    have hdf : T.faceOf d = f.val := (Finset.mem_filter.mp hd).2
    let c : SpokeCorner T (blackFaces T col t0) := ⟨d, hdf.symm ▸ f.property⟩
    have hk : N.edgeOf (c, false) ∉ deletedSpokes T hT col hcol t0 s := by
      intro he
      obtain ⟨t, ht, htv⟩ := (deletedSpokes_corner_iff T hT col hcol t0 s c).mp he
      exact hret t (ht.symm.trans hdf) (hdv.symm.trans htv)
    apply SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj
    refine ⟨by simp, (c, false), hk, ?_, ?_⟩
    · exact congrArg Sum.inr (Subtype.ext hdf)
    · change (spokeRotation T hT _ _).vert ((spokeRotation T hT _ _).edgeInv (c, false)) = _
      rw [spokeRotation_edgeInv]
      exact congrArg Sum.inl hdv
  have outer_link (v : T.Vertex) (hv : v ∈ roots T t0) :
      G.connectedComponentMk (Sum.inr outer) = G.connectedComponentMk (Sum.inl v) := by
    apply link outer v hv
    intro t ht
    exact False.elim ((Finset.mem_filter.mp t.property).2.2 ht)
  have edge {u v : T.Vertex} (huv : (Qs T col t0 s).Adj u v) :
      G.connectedComponentMk (Sum.inl u) = G.connectedComponentMk (Sum.inl v) := by
    rw [Qs, SimpleGraph.fromEdgeSet_adj] at huv
    obtain ⟨⟨t, d, hdf, hdu, hdv, he⟩, hne⟩ := huv
    rcases Sym2.eq_iff.mp he with ⟨hu, hv⟩ | ⟨hv, hu⟩
    all_goals
      let f : blackFaces T col t0 := ⟨t.val, by
        exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, (Finset.mem_filter.mp t.property).2.1⟩⟩
      have hends := faceDart_endpoints_incident T hT d
      rw [hdf] at hends
      have ha := link f (T.vert d) hends.1 (by
        intro a ha
        have hat : a = t := Subtype.ext ha
        simpa only [hat] using hdu)
      have hb := link f (T.head d) hends.2 (by
        intro a ha
        have hat : a = t := Subtype.ext ha
        simpa only [hat] using hdv)
    · simpa only [hu, hv] using ha.symm.trans hb
    · simpa only [hu, hv] using hb.symm.trans ha
  have walk {u v : T.Vertex} (p : (Qs T col t0 s).Walk u v) :
      G.connectedComponentMk (Sum.inl u) = G.connectedComponentMk (Sum.inl v) := by
    induction p with
    | nil => rfl
    | cons h p ih => exact (edge h).trans ih
  have original (v : T.Vertex) :
      G.connectedComponentMk (Sum.inl v) = G.connectedComponentMk (Sum.inr outer) := by
    obtain ⟨w, hw, _⟩ := qs_component_contains_unique_root T hT col hcol t0 r s
      hpair hforest hsep ((Qs T col t0 s).connectedComponentMk v)
    obtain ⟨p⟩ := SimpleGraph.ConnectedComponent.exact hw.2.symm
    exact (walk p).trans (outer_link w hw.1).symm
  have all_vertices (v : N.Vertex) :
      G.connectedComponentMk v = G.connectedComponentMk (Sum.inr outer) := by
    cases v with
    | inl v => exact original v
    | inr f =>
      by_cases hf : f.val = t0
      · have he : f = outer := Subtype.ext hf
        rw [he]
      · let t : blackNonOuter T col t0 := ⟨f.val,
          Finset.mem_filter.mpr ⟨Finset.mem_univ _, (Finset.mem_filter.mp f.property).2, hf⟩⟩
        have hl := link f (r.val t).val (r.property.incident t) (by
          intro a ha
          have hat : a = t := Subtype.ext ha
          simpa only [hat] using pair_vertex_ne T col t0 r s hpair t)
        exact hl.trans (original _)
  let : Nonempty N.Vertex := ⟨Sum.inr outer⟩
  refine ⟨?_⟩
  intro u v
  exact SimpleGraph.ConnectedComponent.exact ((all_vertices u).trans (all_vertices v).symm)

-- @node: deletedSpokes_card
/-- If the map is a sphere triangulation and adjacent faces have opposite
colors, then for [any state](hyp:s), [the number of deleted spokes equals
the number of nonouter black faces](goal). -/
lemma deletedSpokes_card (s : State T col t0) :
    (Finset.univ.filter (fun e => e ∈ deletedSpokes T hT col hcol t0 s)).card =
      (blackNonOuter T col t0).card := by
  let f (t : blackNonOuter T col t0) :=
    (spokeGraphAll T col t0 hT hcol).edgeOf (stateCorner T hT col t0 s t, false)
  have hinj : Function.Injective f := by
    intro a b h
    have hc : stateCorner T hT col t0 s a = stateCorner T hT col t0 s b :=
      congrArg (spokeEdgeEquiv T hT (blackFaces T col t0)
        (black_faces_disjoint T col t0 hcol)) h
    apply Subtype.ext
    exact (stateCorner_spec T hT col t0 s a).1.symm.trans
      ((congrArg (fun c => T.faceOf c.val) hc).trans (stateCorner_spec T hT col t0 s b).1)
  have heq : Finset.univ.filter (fun e => e ∈ deletedSpokes T hT col hcol t0 s) =
      Finset.univ.image f := by
    ext e
    simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_image,
      deletedSpokes, Set.mem_setOf_eq]
    exact ⟨fun ⟨t, ht⟩ => ⟨t, ht.symm⟩,
      fun ⟨t, ht⟩ => ⟨t, ht.symm⟩⟩
  rw [heq, Finset.card_image_of_injective _ hinj, Finset.card_univ, Fintype.card_coe]

-- @node: retainedSpokes_edge_card
/-- If the map is a sphere triangulation and adjacent faces have opposite
colors, then for [any state](hyp:s), [the number of retained spoke edges
plus one equals the number of vertices of the all-spoke graph](goal). -/
lemma retainedSpokes_edge_card (s : State T col t0) :
    (Finset.univ.filter (fun e => e ∈ (deletedSpokes T hT col hcol t0 s)ᶜ)).card + 1 =
      Fintype.card (spokeGraphAll T col t0 hT hcol).Vertex := by
  have hsplit := Finset.card_filter_add_card_filter_not (s := Finset.univ)
    (fun e => e ∈ deletedSpokes T hT col hcol t0 s)
  rw [deletedSpokes_card T hT col hcol t0 s, Finset.card_univ] at hsplit
  have he := spoke_edge_card T hT (blackFaces T col t0) (black_faces_disjoint T col t0 hcol)
  have hs := (stateSetsCard_of_triangulation T hT col hcol t0).1
  have hv := (standingCounts_of_triangulation T hT (normalizedColoring T col t0)
    (normalizedColoring_partition T col hcol t0)).2.2
  have hb : (blackFaces T col t0).card = blackFaceCount T (normalizedColoring T col t0) := rfl
  have hp : 0 < (blackFaces T col t0).card := Finset.card_pos.mpr
    ⟨t0, by simp [blackFaces, normalizedColoring_self]⟩
  change _ + 1 = Fintype.card (T.Vertex ⊕ blackFaces T col t0)
  rw [Fintype.card_sum, Fintype.card_coe]
  change (blackNonOuter T col t0).card + _ =
    Fintype.card (spokeRotation T hT (blackFaces T col t0) (black_faces_disjoint T col t0 hcol)).Edge at hsplit
  simp only [Set.mem_compl_iff]
  omega

-- @node: deletedSpokes_dual_isTree
/-- If the map is a sphere triangulation, adjacent faces have opposite
colors, [the two states assign distinct vertices to every nonouter black
face](hyp:hpair), [the second state's opposite-edge graph is a forest](hyp:hforest),
and [there is no separating triangle](hyp:hsep), then [the second state's deleted
spokes form a spanning tree in the dual of the all-spoke graph](goal). -/
lemma deletedSpokes_dual_isTree (r s : State T col t0) (hpair : IsPair T col t0 r s)
    (hforest : QsForest T col t0 s) (hsep : TreesNoSeparatingTriangle T) :
    ((spokeGraphAll T col t0 hT hcol).dual (spokeAll_connected T hT col hcol t0)).IsSpanningTree
      (deletedSpokes T hT col hcol t0 s) := by
  let N := spokeGraphAll T col t0 hT hcol
  have htree : N.IsSpanningTree (deletedSpokes T hT col hcol t0 s)ᶜ :=
    N.isSpanningTree_of_connected_card _
      (retainedSpokes_connected T hT col hcol t0 r s hpair hforest hsep)
      (by simpa only [N, spokeGraphAll, buildSpokes, spokeRotation] using
        retainedSpokes_edge_card T hT col hcol t0 s)
  have hdual := (N.dual_compl_spanning (spokeAll_connected T hT col hcol t0)
    ⟨inferInstance, inferInstance⟩).1 _ htree
  simpa only [compl_compl] using hdual

-- @node: whiteFaceGraph_isTree
/-- If the map is a sphere triangulation, adjacent faces have opposite
colors, [the two states assign distinct vertices to every nonouter black
face](hyp:hpair), [the second state's opposite-edge graph is a forest](hyp:hforest),
and [there is no separating triangle](hyp:hsep), then [the second state's white-face
graph is a tree](goal). -/
lemma whiteFaceGraph_isTree (r s : State T col t0) (hpair : IsPair T col t0 r s)
    (hforest : QsForest T col t0 s) (hsep : TreesNoSeparatingTriangle T) :
    (whiteFaceGraph T hT col hcol t0 s).IsTree := by
  exact SphereMap.IsSpanningTree.isTree _ _
    (deletedSpokes_dual_isTree T hT col hcol t0 r s hpair hforest hsep)

-- @node: exists_outerEdgeDart
/-- For [an edge](hyp:e0) that [lies on the outer face](hyp:he0), [there is a directed
edge representing it with the outer face on its incident side](goal). -/
lemma exists_outerEdgeDart (e0 : T.Edge) (he0 : T.edgeOnFace e0 t0) :
    ∃ d : T.Dart, T.edgeOf d = e0 ∧ T.faceOf d = t0 := by
  exact he0

/-- For [a sphere map](hyp:T), [an outer face](hyp:t0), and [an edge](hyp:e0) that
[lies on that face](hyp:he0), the [outer-edge orientation](goal) is a chosen directed
representative of the edge whose incident face is the outer face. -/
noncomputable def outerEdgeDart (e0 : T.Edge) (he0 : T.edgeOnFace e0 t0) : T.Dart :=
  Classical.choose (exists_outerEdgeDart T t0 e0 he0)

-- @node: across_isWhite
/-- If [adjacent faces have opposite colors](hyp:hcol), [a face is black in the
normalized coloring](hyp:ht), and [a directed edge has that face on one of its two
sides](hyp:hd), then [the face on the other side is white](goal). -/
lemma across_isWhite (hcol : PartitionColoring T col) (t : T.Face) (ht : normalizedColoring T col t0 t = true)
    (d : T.Dart) (hd : T.faceOf d = t ∨ T.faceOf (T.edgeInv d) = t) :
    normalizedColoring T col t0 (if T.faceOf d = t then T.faceOf (T.edgeInv d) else T.faceOf d) = false := by
  have hop := normalizedColoring_partition T col hcol t0 d
  by_cases hf : T.faceOf d = t
  · rw [if_pos hf]
    rw [hf, ht] at hop
    exact Bool.eq_false_iff.mpr (Ne.symm hop)
  · rw [if_neg hf]
    have hi := hd.resolve_left hf
    rw [hi, ht] at hop
    exact Bool.eq_false_iff.mpr hop

/-- For [a sphere map](hyp:T) that [is a sphere triangulation](hyp:hT), [a face
coloring](hyp:col) with [opposite colors across every edge](hyp:hcol), [an outer
face](hyp:t0), [a face](hyp:t) that [is black after normalization](hyp:ht), and
[a directed edge](hyp:d) with [that face on one side](hyp:hd), the [white face across
the edge, represented as a face of the all-spoke graph](goal) is obtained by transporting
the original face on the other side through the white-face bijection. -/
noncomputable def whiteAcross (t : T.Face) (ht : normalizedColoring T col t0 t = true)
    (d : T.Dart) (hd : T.faceOf d = t ∨ T.faceOf (T.edgeInv d) = t) :
    (spokeGraphAll T col t0 hT hcol).Face :=
  (whiteFaceEquiv T hT col hcol t0).symm
    ⟨if T.faceOf d = t then T.faceOf (T.edgeInv d) else T.faceOf d,
      across_isWhite T col t0 hcol t ht d hd⟩

-- @node: normalized_outer_black
/-- [The outer face is black in the normalized coloring](goal). -/
lemma normalized_outer_black : normalizedColoring T col t0 t0 = true := by
  exact normalizedColoring_self T col t0
-- @node: outerEdgeDart_face
/-- For [an edge](hyp:e0) that [lies on the outer face](hyp:he0), [the chosen
outer-edge orientation has the outer face as its incident face](goal). -/
lemma outerEdgeDart_face (e0 : T.Edge) (he0 : T.edgeOnFace e0 t0) :
    T.faceOf (outerEdgeDart T t0 e0 he0) = t0 := by
  exact (Classical.choose_spec (exists_outerEdgeDart T t0 e0 he0)).2

/-- For [a sphere map](hyp:T) that [is a sphere triangulation](hyp:hT), [a face
coloring](hyp:col) with [opposite colors across every edge](hyp:hcol), [an outer
face](hyp:t0), and [a prescribed edge](hyp:e0) that [lies on the outer face](hyp:he0),
the [white root](goal) is the white face across the prescribed edge from the outer
face, represented as a face of the all-spoke graph. -/
noncomputable def whiteRoot (e0 : T.Edge) (he0 : T.edgeOnFace e0 t0) :
    (spokeGraphAll T col t0 hT hcol).Face :=
  whiteAcross T hT col hcol t0 t0 (normalized_outer_black T col t0)
    (outerEdgeDart T t0 e0 he0) (Or.inl (outerEdgeDart_face T t0 e0 he0))
  -- @realizes y_0(white triangle across e0, transported to a face of H)
  -- @realizes e_0(prescribed edge on the outer facial triangle)

-- @node: nonOuter_black
/-- [Every nonouter black face is black in the normalized coloring](goal). -/
lemma nonOuter_black (t : blackNonOuter T col t0) : normalizedColoring T col t0 t.val = true := by
  exact (Finset.mem_filter.mp t.property).2.1
/-- For [a sphere map](hyp:T), [a face coloring](hyp:col), [an outer face](hyp:t0),
[a state](hyp:s), and [a nonouter black face](hyp:t), the [selection candidates](goal)
are directed edges whose tail is the vertex assigned to that face by the state and
which have that face on one side. -/
abbrev SelectionCandidate (s : State T col t0) (t : blackNonOuter T col t0) :=
  {d : T.Dart // T.vert d = (s.val t).val ∧ (T.faceOf d = t.val ∨ T.faceOf (T.edgeInv d) = t.val)}

/-- For [a sphere map](hyp:T) that [is a sphere triangulation](hyp:hT), [a face
coloring](hyp:col) with [opposite colors across every edge](hyp:hcol), [an outer
face](hyp:t0), [a state](hyp:s), [a nonouter black face](hyp:t), and [a candidate
directed edge at its assigned vertex](hyp:d), the [candidate's white face](goal) is
the face across that edge from the black face, represented in the all-spoke graph. -/
noncomputable def candidateWhite (s : State T col t0) (t : blackNonOuter T col t0)
    (d : SelectionCandidate T col t0 s t) : (spokeGraphAll T col t0 hT hcol).Face :=
  whiteAcross T hT col hcol t0 t.val (nonOuter_black T col t0 t) d.val d.property.2

-- @node: exists_farthestCandidate
/-- If the map is a sphere triangulation and adjacent faces have opposite
colors, then for [a state](hyp:s), [a prescribed edge](hyp:e0) that
[lies on the outer face](hyp:he0), and [a nonouter black face](hyp:t), [there is a
candidate directed edge whose white face maximizes distance from the white root in
the state's white-face graph among all candidates for that black face](goal). -/
lemma exists_farthestCandidate (s : State T col t0) (e0 : T.Edge) (he0 : T.edgeOnFace e0 t0)
    (t : blackNonOuter T col t0) :
    ∃ d : SelectionCandidate T col t0 s t,
      ∀ d' : SelectionCandidate T col t0 s t,
        (whiteFaceGraph T hT col hcol t0 s).dist (whiteRoot T hT col hcol t0 e0 he0)
            (candidateWhite T hT col hcol t0 s t d') ≤
          (whiteFaceGraph T hT col hcol t0 s).dist (whiteRoot T hT col hcol t0 e0 he0)
            (candidateWhite T hT col hcol t0 s t d) := by
  have hv := s.property.incident t
  rw [triangulation_faceVertices_eq_image T hT] at hv
  obtain ⟨d, hd, hv⟩ := Finset.mem_image.mp hv
  have hf : T.faceOf d = t.val := (Finset.mem_filter.mp hd).2
  let c : SelectionCandidate T col t0 s t := ⟨d, hv, Or.inl hf⟩
  let : Nonempty (SelectionCandidate T col t0 s t) := ⟨c⟩
  obtain ⟨a, _, ha⟩ := Finset.exists_max_image Finset.univ
    (fun d : SelectionCandidate T col t0 s t =>
      (whiteFaceGraph T hT col hcol t0 s).dist (whiteRoot T hT col hcol t0 e0 he0)
        (candidateWhite T hT col hcol t0 s t d)) Finset.univ_nonempty
  exact ⟨a, fun d' => ha d' (Finset.mem_univ _)⟩

/-- For [a sphere map](hyp:T) that [is a sphere triangulation](hyp:hT), [a face
coloring](hyp:col) with [opposite colors across every edge](hyp:hcol), [an outer
face](hyp:t0), [a state](hyp:s), [a prescribed edge](hyp:e0) that [lies on the outer
face](hyp:he0), and [a nonouter black face](hyp:t), the [selected directed edge](goal)
is a chosen candidate whose white face has maximal distance from the white root in
the state's white-face graph. -/
noncomputable def selectedDart (s : State T col t0) (e0 : T.Edge) (he0 : T.edgeOnFace e0 t0)
    (t : blackNonOuter T col t0) : T.Dart :=
  (Classical.choose (exists_farthestCandidate T hT col hcol t0 s e0 he0 t)).val

-- @node: selectedDart_spec
/-- If the map is a sphere triangulation and adjacent faces have opposite
colors, then for [a state](hyp:s), [a prescribed edge](hyp:e0) that
[lies on the outer face](hyp:he0), and [a nonouter black face](hyp:t), [the selected
directed edge starts at the vertex assigned to that face by the state and has that
face on one of its two sides](goal). -/
lemma selectedDart_spec (s : State T col t0) (e0 : T.Edge) (he0 : T.edgeOnFace e0 t0)
    (t : blackNonOuter T col t0) :
    T.vert (selectedDart T hT col hcol t0 s e0 he0 t) = (s.val t).val ∧
      (T.faceOf (selectedDart T hT col hcol t0 s e0 he0 t) = t.val ∨
        T.faceOf (T.edgeInv (selectedDart T hT col hcol t0 s e0 he0 t)) = t.val) := by
  exact (Classical.choose (exists_farthestCandidate T hT col hcol t0 s e0 he0 t)).property

-- @node: selectedDart_eq_of_tail_eq
/-- If the map is a sphere triangulation and adjacent faces have opposite
colors, then for [a state](hyp:s) and [a prescribed edge](hyp:e0) that
[lies on the outer face](hyp:he0), whenever [the directed edges selected for two
nonouter black faces have equal tails](hyp:h), [those selected directed edges are
equal](goal). -/
lemma selectedDart_eq_of_tail_eq (s : State T col t0) (e0 : T.Edge)
    (he0 : T.edgeOnFace e0 t0) (t u : blackNonOuter T col t0)
    (h : T.vert (selectedDart T hT col hcol t0 s e0 he0 t) =
      T.vert (selectedDart T hT col hcol t0 s e0 he0 u)) :
    selectedDart T hT col hcol t0 s e0 he0 t =
      selectedDart T hT col hcol t0 s e0 he0 u := by
  rw [(selectedDart_spec T hT col hcol t0 s e0 he0 t).1,
    (selectedDart_spec T hT col hcol t0 s e0 he0 u).1] at h
  have htu : t = u := s.property.bijective.1 (Subtype.ext h)
  exact congrArg (selectedDart T hT col hcol t0 s e0 he0) htu

-- @node: def:p
/-- For [a sphere map](hyp:T) that [is a sphere triangulation](hyp:hT), [a face
coloring](hyp:col) with [opposite colors across every edge](hyp:hcol), [an outer
face](hyp:t0), [a state](hyp:s), and [a prescribed edge](hyp:e0) that [lies on the
outer face](hyp:he0), the [selected edge set](goal) consists of the prescribed edge
together with the underlying edges selected for all nonouter black faces by maximizing
white-face distance from the white root.

Ties between maximizing candidates are settled by classical choice. -/
noncomputable def selectedSet (s : State T col t0) (e0 : T.Edge) (he0 : T.edgeOnFace e0 t0) : Finset T.Edge :=
  insert e0 (Finset.univ.image (fun t => T.edgeOf (selectedDart T hT col hcol t0 s e0 he0 t)))
  -- @realizes P(edges at the farther white endpoints, together with e0)

/-- For [a sphere map](hyp:T) that [is a sphere triangulation](hyp:hT), [a face
coloring](hyp:col) with [opposite colors across every edge](hyp:hcol), [an outer
face](hyp:t0), [a state](hyp:s), and [a prescribed edge](hyp:e0) that [lies on the
outer face](hyp:he0), the [reduced selected edge set](goal) is the selected edge set
with the prescribed edge removed. -/
noncomputable def selectedSet0 (s : State T col t0) (e0 : T.Edge) (he0 : T.edgeOnFace e0 t0) : Finset T.Edge :=
  (selectedSet T hT col hcol t0 s e0 he0).erase e0 -- @realizes P_0(P with the outer edge removed)

-- @node: def:p0-orientation
/-- For [a sphere map](hyp:T) that [is a sphere triangulation](hyp:hT), [a face
coloring](hyp:col) with [opposite colors across every edge](hyp:hcol), [an outer
face](hyp:t0), [a state](hyp:s), and [a prescribed edge](hyp:e0) that [lies on the
outer face](hyp:he0), the [oriented reduced selection](goal) consists of the directed
edges selected for nonouter black faces, excluding those whose underlying edge is
the prescribed edge. -/
noncomputable def orientedP0 (s : State T col t0) (e0 : T.Edge) (he0 : T.edgeOnFace e0 t0) : Finset T.Dart :=
  (Finset.univ.image (selectedDart T hT col hcol t0 s e0 he0)).filter (fun d => T.edgeOf d ≠ e0)


-- @node: orientedP0_tail_injective
/-- If the map is a sphere triangulation, adjacent faces have opposite
colors, and [the prescribed edge lies on the outer face](hyp:he0), then
any [first directed edge in the state's oriented reduced selection](hyp:hd) and
[second directed edge in that selection](hyp:he) that [have equal tails](hyp:h)
[are equal as directed edges](goal). -/
lemma orientedP0_tail_injective (s : State T col t0) (e0 : T.Edge)
    (he0 : T.edgeOnFace e0 t0) (d e : T.Dart)
    (hd : d ∈ orientedP0 T hT col hcol t0 s e0 he0)
    (he : e ∈ orientedP0 T hT col hcol t0 s e0 he0)
    (h : T.vert d = T.vert e) : d = e := by
  obtain ⟨t, _, rfl⟩ := Finset.mem_image.mp (Finset.mem_filter.mp hd).1
  obtain ⟨u, _, rfl⟩ := Finset.mem_image.mp (Finset.mem_filter.mp he).1
  exact selectedDart_eq_of_tail_eq T hT col hcol t0 s e0 he0 t u h

-- @node: orientedP0_tail_nonRoot
/-- If the map is a sphere triangulation, adjacent faces have opposite
colors, [the prescribed edge lies on the outer face](hyp:he0), and
[a directed edge belongs to the state's oriented reduced selection](hyp:hd), then
[its tail is a nonroot vertex, outside the outer face's vertices](goal). -/
lemma orientedP0_tail_nonRoot (s : State T col t0) (e0 : T.Edge)
    (he0 : T.edgeOnFace e0 t0) (d : T.Dart)
    (hd : d ∈ orientedP0 T hT col hcol t0 s e0 he0) : T.vert d ∈ nonRoot T t0 := by
  obtain ⟨t, _, rfl⟩ := Finset.mem_image.mp (Finset.mem_filter.mp hd).1
  rw [(selectedDart_spec T hT col hcol t0 s e0 he0 t).1]
  exact (s.val t).property


end OaiPairedStatesHamiltonian