CubicPathwidth.T4.TorsoDyn

Source file CubicPathwidth/T4/TorsoDyn.lean of the Lean project (how it is built).

import CubicPathwidth.T4.ProcessDefs
import CubicPathwidth.T2.Reduction

/-!
# Torso dynamics (`TorsoDynamics`, part of `StateClaim`)

Mirrors invariants (I1), (I2) of Lemma 4.5 (`lem:reduction`).

* Deleting a core vertex `w` does not change the components of the non-core part
  (`erase_sdiff_erase`), and removes `w` from every attachment set
  (`attachment_erase`).
* Removing a core vertex `v` from the core (with `B ⊆ F`): the components of
  `F \ (B.erase v)` are the old components not attached to `v`, and one new component
  `component v` that contains `v` and the old components attached to `v`. Its
  attachment set is the torso neighbourhood of `v`, so the new torso is the old one with
  `v` removed and the torso neighbourhood of `v` made into a clique
  (`tgraph_erase_core_adj`; no bound on the torso degree of `v` is needed for this).
* If the torso degree of `v` is at most two this never increases a torso degree
  (`tdeg_erase_le`), and repeated reduction gives a core of minimum torso degree at
  least three (`exists_reduced`).
* As a by-product, every component of `F \ B` of a good state has at most two
  attachment vertices (`Good.attachment_card_le`); the dynamics do not need it.
-/

noncomputable section

namespace CubicPathwidth
namespace T4

open T2

variable {n : ℕ} (G : SimpleGraph (Fin n))

theorem tgraph_adj_iff (F B : Finset (Fin n)) (x y : Fin n) :
    (tgraph G F B).Adj x y ↔ x ≠ y ∧ x ∈ B ∧ y ∈ B ∧ (G.Adj x y ∨
      ∃ T ∈ components G (F \ B), x ∈ attachment G B T ∧ y ∈ attachment G B T) :=
  Iff.rfl

/-! ## Deletion -/

theorem erase_sdiff_erase {F B : Finset (Fin n)} {w : Fin n} (hw : w ∈ B) :
    F.erase w \ B.erase w = F \ B := by
  ext x
  simp only [Finset.mem_sdiff, Finset.mem_erase]
  constructor
  · rintro ⟨⟨hxw, hxF⟩, h⟩
    exact ⟨hxF, fun hxB => h ⟨hxw, hxB⟩⟩
  · rintro ⟨hxF, hxB⟩
    exact ⟨⟨fun h => hxB (h ▸ hw), hxF⟩, fun h => hxB h.2⟩

theorem attachment_erase (B T : Finset (Fin n)) (w : Fin n) :
    attachment G (B.erase w) T = (attachment G B T).erase w := by
  ext x
  simp only [mem_attachment, Finset.mem_erase]
  tauto

theorem attachment_erase_subset (B T : Finset (Fin n)) (w : Fin n) :
    attachment G (B.erase w) T ⊆ attachment G B T := by
  rw [attachment_erase]
  exact Finset.erase_subset _ _

theorem tgraph_erase_adj {F B : Finset (Fin n)} {w : Fin n} (hw : w ∈ B) (x y : Fin n) :
    (tgraph G (F.erase w) (B.erase w)).Adj x y ↔
      (tgraph G F B).Adj x y ∧ x ≠ w ∧ y ≠ w := by
  rw [tgraph_adj_iff, tgraph_adj_iff, erase_sdiff_erase hw]
  simp only [attachment_erase, Finset.mem_erase]
  constructor
  · rintro ⟨hne, ⟨hxw, hx⟩, ⟨hyw, hy⟩, h⟩
    refine ⟨⟨hne, hx, hy, ?_⟩, hxw, hyw⟩
    rcases h with h | ⟨T, hT, hxT, hyT⟩
    · exact Or.inl h
    · exact Or.inr ⟨T, hT, hxT.2, hyT.2⟩
  · rintro ⟨⟨hne, hx, hy, h⟩, hxw, hyw⟩
    refine ⟨hne, ⟨hxw, hx⟩, ⟨hyw, hy⟩, ?_⟩
    rcases h with h | ⟨T, hT, hxT, hyT⟩
    · exact Or.inl h
    · exact Or.inr ⟨T, hT, ⟨hxw, hxT⟩, ⟨hyw, hyT⟩⟩

/-! ## Removing a core vertex from the core -/

section Reduce

variable {F B : Finset (Fin n)} {v : Fin n}

theorem mem_sdiff_erase_iff (u : Fin n) : u ∈ F \ B.erase v ↔ u ∈ F ∧ (u = v ∨ u ∉ B) := by
  simp only [Finset.mem_sdiff, Finset.mem_erase]
  tauto

theorem sdiff_subset_sdiff_erase : F \ B ⊆ F \ B.erase v := by
  intro u hu
  rw [mem_sdiff_erase_iff]
  exact ⟨(Finset.mem_sdiff.mp hu).1, Or.inr (Finset.mem_sdiff.mp hu).2⟩

theorem mem_components_of_conn {U T : Finset (Fin n)} (hS : T ⊆ U) (hc : ClosedIn G U T)
    (hconn : SectionConnected G T) : T ∈ components G U := by
  obtain ⟨u, hu⟩ := hconn.1
  rw [← component_eq_of_connected G hS hc hconn hu]
  exact mem_components_of_mem G (hS hu)

theorem sub_of_mem {T T' : Finset (Fin n)} (hT : T ∈ components G (F \ B))
    (hT' : T' ∈ components G (F \ B.erase v)) {u : Fin n} (hu : u ∈ T) (hu' : u ∈ T') :
    T ⊆ T' := by
  rcases connected_subset_or_disjoint G
      ((mem_components G hT).1.trans sdiff_subset_sdiff_erase) (mem_components G hT).2.2
      (mem_components G hT').2.1 with h | h
  · exact h
  · exact absurd hu' (Finset.disjoint_left.mp h hu)

theorem vmem_att {T T' : Finset (Fin n)} (hv : v ∈ B) (hT : T ∈ components G (F \ B))
    (hT' : T' ∈ components G (F \ B.erase v)) (hTT' : T ⊆ T') (hvT' : v ∈ T') :
    v ∈ attachment G B T := by
  have hvT : v ∉ T := fun h => (Finset.mem_sdiff.mp ((mem_components G hT).1 h)).2 hv
  obtain ⟨x, hx, y, hy, hxy⟩ := connected_cross_edge G (mem_components G hT').2.2 hTT'
    (mem_components G hT).2.2.1 (fun h => hvT (by rw [h]; exact hvT'))
  obtain ⟨hyT', hyT⟩ := Finset.mem_sdiff.mp hy
  have hyv : y = v := by
    by_contra hyv
    have hyU : y ∈ F \ B := by
      obtain ⟨hF, h⟩ := (mem_sdiff_erase_iff y).mp ((mem_components G hT').1 hyT')
      exact Finset.mem_sdiff.mpr ⟨hF, h.resolve_left hyv⟩
    exact hyT ((mem_components G hT).2.1 x hx y hyU hxy)
  subst hyv
  exact (mem_attachment G).mpr ⟨hv, x, hx, hxy.symm⟩

/-- Attachments of the new component are torso neighbours of `v`. -/
theorem att_erase_adj {T' : Finset (Fin n)} (hv : v ∈ B)
    (hT' : T' ∈ components G (F \ B.erase v)) (hvT' : v ∈ T') {x : Fin n}
    (hx : x ∈ attachment G (B.erase v) T') : (tgraph G F B).Adj x v := by
  obtain ⟨hxB', u, huT', hxu⟩ := (mem_attachment G).mp hx
  obtain ⟨hxv, hxB⟩ := Finset.mem_erase.mp hxB'
  refine (tgraph_adj_iff G F B x v).mpr ⟨hxv, hxB, hv, ?_⟩
  by_cases huv : u = v
  · subst huv
    exact Or.inl hxu
  · right
    have huU : u ∈ F \ B := by
      obtain ⟨hF, h⟩ := (mem_sdiff_erase_iff u).mp ((mem_components G hT').1 huT')
      exact Finset.mem_sdiff.mpr ⟨hF, h.resolve_left huv⟩
    have hTmem := mem_components_of_mem G huU
    have hsub := sub_of_mem G hTmem hT' (mem_component_self G huU) huT'
    exact ⟨_, hTmem,
      (mem_attachment G).mpr ⟨hxB, u, mem_component_self G huU, hxu⟩,
      vmem_att G hv hTmem hT' hsub hvT'⟩

theorem comp_of_not_mem {T' : Finset (Fin n)} (hT' : T' ∈ components G (F \ B.erase v))
    (hvT' : v ∉ T') : T' ∈ components G (F \ B) := by
  obtain ⟨hs, hc, hconn⟩ := mem_components G hT'
  have hsub : T' ⊆ F \ B := by
    intro u hu
    obtain ⟨hF, h⟩ := (mem_sdiff_erase_iff u).mp (hs hu)
    exact Finset.mem_sdiff.mpr ⟨hF, h.resolve_left (fun h => hvT' (h ▸ hu))⟩
  exact mem_components_of_conn G hsub
    (fun a ha w hw hadj => hc a ha w (sdiff_subset_sdiff_erase hw) hadj) hconn

theorem comp_of_not_att {T : Finset (Fin n)} (hv : v ∈ B) (hT : T ∈ components G (F \ B))
    (hvT : v ∉ attachment G B T) : T ∈ components G (F \ B.erase v) := by
  obtain ⟨hs, hc, hconn⟩ := mem_components G hT
  refine mem_components_of_conn G (hs.trans sdiff_subset_sdiff_erase) ?_ hconn
  intro a ha w hw hadj
  obtain ⟨hF, h⟩ := (mem_sdiff_erase_iff w).mp hw
  rcases h with hwv | hwB
  · rw [hwv] at hadj
    exact absurd ((mem_attachment G).mpr ⟨hv, a, ha, hadj.symm⟩) hvT
  · exact hc a ha w (Finset.mem_sdiff.mpr ⟨hF, hwB⟩) hadj

theorem sub_of_att {T : Finset (Fin n)} (hBF : B ⊆ F) (hT : T ∈ components G (F \ B))
    (hvT : v ∈ attachment G B T) : T ⊆ component G (F \ B.erase v) v := by
  have hvB : v ∈ B := attachment_subset G B T hvT
  have hvU' : v ∈ F \ B.erase v := (mem_sdiff_erase_iff v).mpr ⟨hBF hvB, Or.inl rfl⟩
  obtain ⟨_, u0, hu0T, hvu0⟩ := (mem_attachment G).mp hvT
  have hu0U : u0 ∈ F \ B := (mem_components G hT).1 hu0T
  have hu0U' : u0 ∈ F \ B.erase v := sdiff_subset_sdiff_erase hu0U
  have hu0 : u0 ∈ component G (F \ B.erase v) v :=
    component_closed G _ v v (mem_component_self G hvU') u0 hu0U' hvu0
  exact sub_of_mem G hT (mem_components_of_mem G hvU') hu0T hu0

theorem att_Tv_of_att {T : Finset (Fin n)} (hBF : B ⊆ F) (hT : T ∈ components G (F \ B))
    (hvT : v ∈ attachment G B T) {z : Fin n} (hz : z ∈ attachment G B T) (hzv : z ≠ v) :
    z ∈ attachment G (B.erase v) (component G (F \ B.erase v) v) := by
  obtain ⟨hzB, u, huT, hzu⟩ := (mem_attachment G).mp hz
  exact (mem_attachment G).mpr ⟨Finset.mem_erase.mpr ⟨hzv, hzB⟩, u,
    sub_of_att G hBF hT hvT huT, hzu⟩

/-- The torso after removing `v` from the core: `v` disappears and its torso
neighbourhood becomes a clique. -/
theorem tgraph_erase_core_adj (hBF : B ⊆ F) (hv : v ∈ B) (x y : Fin n) :
    (tgraph G F (B.erase v)).Adj x y ↔
      x ≠ v ∧ y ≠ v ∧ ((tgraph G F B).Adj x y ∨
        (x ≠ y ∧ (tgraph G F B).Adj x v ∧ (tgraph G F B).Adj y v)) := by
  have hvU' : v ∈ F \ B.erase v := (mem_sdiff_erase_iff v).mpr ⟨hBF hv, Or.inl rfl⟩
  have hTv := mem_components_of_mem G hvU'
  have hvTv := mem_component_self G hvU'
  have attTv : ∀ z, (tgraph G F B).Adj z v →
      z ∈ attachment G (B.erase v) (component G (F \ B.erase v) v) := by
    intro z hz
    obtain ⟨hzv, hzB, _, h⟩ := (tgraph_adj_iff G F B z v).mp hz
    rcases h with h | ⟨T, hT, hzT, hvT⟩
    · exact (mem_attachment G).mpr ⟨Finset.mem_erase.mpr ⟨hzv, hzB⟩, v, hvTv, h⟩
    · exact att_Tv_of_att G hBF hT hvT hzT hzv
  constructor
  · intro h
    obtain ⟨hne, hxB', hyB', h⟩ := (tgraph_adj_iff G F (B.erase v) x y).mp h
    obtain ⟨hxv, hxB⟩ := Finset.mem_erase.mp hxB'
    obtain ⟨hyv, hyB⟩ := Finset.mem_erase.mp hyB'
    refine ⟨hxv, hyv, ?_⟩
    rcases h with h | ⟨T', hT', hxT, hyT⟩
    · exact Or.inl ((tgraph_adj_iff G F B x y).mpr ⟨hne, hxB, hyB, Or.inl h⟩)
    · by_cases hvT' : v ∈ T'
      · exact Or.inr ⟨hne, att_erase_adj G hv hT' hvT' hxT, att_erase_adj G hv hT' hvT' hyT⟩
      · exact Or.inl ((tgraph_adj_iff G F B x y).mpr ⟨hne, hxB, hyB,
          Or.inr ⟨T', comp_of_not_mem G hT' hvT', attachment_erase_subset G B T' v hxT,
            attachment_erase_subset G B T' v hyT⟩⟩)
  · rintro ⟨hxv, hyv, h | ⟨hne, hxv', hyv'⟩⟩
    · obtain ⟨hne, hxB, hyB, h⟩ := (tgraph_adj_iff G F B x y).mp h
      refine (tgraph_adj_iff G F (B.erase v) x y).mpr ⟨hne, Finset.mem_erase.mpr ⟨hxv, hxB⟩,
        Finset.mem_erase.mpr ⟨hyv, hyB⟩, ?_⟩
      rcases h with h | ⟨T, hT, hxT, hyT⟩
      · exact Or.inl h
      · right
        by_cases hvT : v ∈ attachment G B T
        · exact ⟨_, hTv, att_Tv_of_att G hBF hT hvT hxT hxv, att_Tv_of_att G hBF hT hvT hyT hyv⟩
        · refine ⟨T, comp_of_not_att G hv hT hvT, ?_, ?_⟩
          · obtain ⟨hxB, u, huT, hxu⟩ := (mem_attachment G).mp hxT
            exact (mem_attachment G).mpr ⟨Finset.mem_erase.mpr ⟨hxv, hxB⟩, u, huT, hxu⟩
          · obtain ⟨hyB, u, huT, hyu⟩ := (mem_attachment G).mp hyT
            exact (mem_attachment G).mpr ⟨Finset.mem_erase.mpr ⟨hyv, hyB⟩, u, huT, hyu⟩
    · obtain ⟨_, hxB, _, _⟩ := (tgraph_adj_iff G F B x v).mp hxv'
      obtain ⟨_, hyB, _, _⟩ := (tgraph_adj_iff G F B y v).mp hyv'
      exact (tgraph_adj_iff G F (B.erase v) x y).mpr ⟨hne, Finset.mem_erase.mpr ⟨hxv, hxB⟩,
        Finset.mem_erase.mpr ⟨hyv, hyB⟩, Or.inr ⟨_, hTv, attTv x hxv', attTv y hyv'⟩⟩

end Reduce

/-! ## Torso degrees -/

open Classical in

theorem tdeg_eq_card (F B : Finset (Fin n)) (v : Fin n) :
    tdeg G F B v = (Finset.univ.filter (fun u => (tgraph G F B).Adj v u)).card := by
  unfold tdeg
  rw [← SimpleGraph.card_neighborFinset_eq_degree]
  congr 1
  ext u
  simp

open Classical in

theorem tdeg_erase_le {F B : Finset (Fin n)} {v : Fin n} (hBF : B ⊆ F) (hv : v ∈ B)
    (hdeg : tdeg G F B v ≤ 2) {u : Fin n} (_hu : u ∈ B.erase v) :
    tdeg G F (B.erase v) u ≤ tdeg G F B u := by
  rw [tdeg_eq_card, tdeg_eq_card G F B u]
  rw [tdeg_eq_card] at hdeg
  have hsym : ∀ a b, (tgraph G F B).Adj a b → (tgraph G F B).Adj b a := fun a b h => h.symm
  by_cases huv : (tgraph G F B).Adj u v
  · set N := Finset.univ.filter (fun y => (tgraph G F B).Adj u y) with hN
    set Nv := Finset.univ.filter (fun y => (tgraph G F B).Adj v y) with hNv
    have hsub : Finset.univ.filter (fun y => (tgraph G F (B.erase v)).Adj u y) ⊆
        N.erase v ∪ Nv.erase u := by
      intro y hy
      have hy' := (tgraph_erase_core_adj G hBF hv u y).mp (Finset.mem_filter.mp hy).2
      obtain ⟨_, hyv, h | ⟨hne, _, hyv'⟩⟩ := hy'
      · exact Finset.mem_union_left _ (Finset.mem_erase.mpr ⟨hyv,
          Finset.mem_filter.mpr ⟨Finset.mem_univ _, h⟩⟩)
      · exact Finset.mem_union_right _ (Finset.mem_erase.mpr ⟨hne.symm,
          Finset.mem_filter.mpr ⟨Finset.mem_univ _, hsym _ _ hyv'⟩⟩)
    have hvN : v ∈ N := Finset.mem_filter.mpr ⟨Finset.mem_univ _, huv⟩
    have huNv : u ∈ Nv := Finset.mem_filter.mpr ⟨Finset.mem_univ _, hsym _ _ huv⟩
    have h1 := Finset.card_le_card hsub
    have h2 := Finset.card_union_le (N.erase v) (Nv.erase u)
    have h3 := Finset.card_erase_add_one hvN
    have h4 := Finset.card_erase_add_one huNv
    omega
  · apply Finset.card_le_card
    intro y hy
    have hy' := (tgraph_erase_core_adj G hBF hv u y).mp (Finset.mem_filter.mp hy).2
    obtain ⟨_, _, h | ⟨_, h, _⟩⟩ := hy'
    · exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, h⟩
    · exact absurd h huv

/-- Maximal sequences of reductions. -/
theorem exists_reduced : ∀ (m : ℕ) (F B : Finset (Fin n)), B.card = m → Good G F B →
    ∃ B' ⊆ B, Reach G (F, B) (F, B') ∧ (∀ v ∈ B', 3 ≤ tdeg G F B' v) ∧
      ∀ v ∈ B', tdeg G F B' v ≤ tdeg G F B v := by
  intro m
  induction m using Nat.strong_induction_on with
  | _ m ih =>
    intro F B hm hgood
    by_cases hall : ∀ v ∈ B, 3 ≤ tdeg G F B v
    · exact ⟨B, Finset.Subset.rfl, Reach.refl G _, hall, fun _ _ => le_rfl⟩
    · push Not at hall
      obtain ⟨v, hvB, hlt⟩ := hall
      have hstep : Step G (F, B) (F, B.erase v) := Step.reduce hvB (by omega)
      have hgood' : Good G F (B.erase v) := hgood.reach (Reach.single hstep)
      have hcard : (B.erase v).card < m := hm ▸ Finset.card_erase_lt_of_mem hvB
      obtain ⟨B', hsub, hreach, h3, hle⟩ := ih _ hcard F (B.erase v) rfl hgood'
      refine ⟨B', hsub.trans (Finset.erase_subset _ _), (Reach.single hstep).trans hreach,
        h3, ?_⟩
      intro u hu
      have hu' : u ∈ B.erase v := hsub hu
      exact (hle u hu).trans (tdeg_erase_le G hgood.subset hvB (by omega) hu')

/-! ## Attachments of good states -/

/-- In a good state every component of the non-core part has at most two attachment
vertices. -/
theorem Good.attachment_card_le {F B : Finset (Fin n)} (h : Good G F B) :
    ∀ T ∈ components G (F \ B), (attachment G B T).card ≤ 2 := by
  have key : ∀ t : Finset (Fin n) × Finset (Fin n),
      Reach G (Finset.univ, Finset.univ) t →
        t.2 ⊆ t.1 ∧ ∀ T ∈ components G (t.1 \ t.2), (attachment G t.2 T).card ≤ 2 := by
    intro t ht
    induction ht with
    | refl =>
      refine ⟨Finset.Subset.rfl, ?_⟩
      intro T hT
      obtain ⟨u, hu⟩ := (mem_components G hT).2.2.1
      have := (mem_components G hT).1 hu
      simp at this
    | @tail s t _ hs ih =>
      obtain ⟨F, B⟩ := s
      obtain ⟨ihsub, ihatt⟩ := ih
      cases hs with
      | @reduce F B v hvB hdeg =>
        classical
        refine ⟨(Finset.erase_subset _ _).trans ihsub, ?_⟩
        intro T' hT'
        change (attachment G (B.erase v) T').card ≤ 2
        by_cases hvT' : v ∈ T'
        · have hsub : attachment G (B.erase v) T' ⊆
              Finset.univ.filter (fun u => (tgraph G F B).Adj v u) := by
            intro z hz
            exact Finset.mem_filter.mpr ⟨Finset.mem_univ _,
              (att_erase_adj G hvB hT' hvT' hz).symm⟩
          have h1 := Finset.card_le_card hsub
          have h2 := tdeg_eq_card G F B v
          have h3 : (Finset.univ.filter (fun u => (tgraph G F B).Adj v u)).card ≤ 2 := by
            rw [← tdeg_eq_card]; exact hdeg
          omega
        · exact (Finset.card_le_card (attachment_erase_subset G B T' v)).trans
            (ihatt T' (comp_of_not_mem G hT' hvT'))
      | @delete F B w hwB =>
        refine ⟨Finset.erase_subset_erase _ ihsub, ?_⟩
        intro T hT
        rw [erase_sdiff_erase hwB] at hT
        rw [attachment_erase]
        exact (Finset.card_erase_le).trans (ihatt T hT)
  exact (key _ h).2

end T4
end CubicPathwidth

namespace CubicPathwidth
namespace T4

theorem torsoDynamics : TorsoDynamics := by
  intro n G F B hgood
  refine ⟨fun w hw x y => tgraph_erase_adj G hw x y, ?_, ?_⟩
  · intro v hv _ x y
    exact tgraph_erase_core_adj G hgood.subset hv x y
  · exact exists_reduced G _ F B rfl hgood

end T4
end CubicPathwidth

#print axioms CubicPathwidth.T4.torsoDynamics
#print axioms CubicPathwidth.T4.Good.attachment_card_le