CubicPathwidth.Alg.Proofs2.TorsoLocal

Source file CubicPathwidth/Alg/Proofs2/TorsoLocal.lean of the Lean project (how it is built).

import CubicPathwidth.Alg.Plan2Deletion
import CubicPathwidth.T4.TorsoDyn

/-!
# Task D6: locality of torsos (`torsoLocal : TorsoLocal`)

Route (from `CubicPathwidth/Alg/Plan2Deletion.lean`): `components G U` and
`attachment G B T` only read `G` on `U` and on `B ∪ T`. Here `B ⊆ F ⊆ F₀`, so the
torso `T4.tgraph S F B` only reads `S` on `F₀`. Reachability is preserved step by step:
the invariant `B ⊆ F ⊆ F₀` is kept by all steps, and each step's torso condition
(`tdeg ≤ 2`) transfers by the torso equality.
-/

noncomputable section

namespace CubicPathwidth.Alg.D6

variable {n : ℕ}

/-- `ClosedIn` on a subset of `U` only reads the graph on `U`. -/
theorem closedIn_congr {S S' : SimpleGraph (Fin n)} {U T : Finset (Fin n)} (hT : T ⊆ U)
    (h : ∀ u ∈ U, ∀ v ∈ U, S.Adj u v ↔ S'.Adj u v) :
    CubicPathwidth.ClosedIn S U T ↔ CubicPathwidth.ClosedIn S' U T := by
  unfold CubicPathwidth.ClosedIn
  constructor
  · intro hc v hv w hw hadj
    exact hc v hv w hw ((h v (hT hv) w hw).mpr hadj)
  · intro hc v hv w hw hadj
    exact hc v hv w hw ((h v (hT hv) w hw).mp hadj)

/-- `component U v` only reads the graph on `U`. -/
theorem component_congr {S S' : SimpleGraph (Fin n)} {U : Finset (Fin n)}
    (h : ∀ u ∈ U, ∀ v ∈ U, S.Adj u v ↔ S'.Adj u v) (v : Fin n) :
    CubicPathwidth.component S U v = CubicPathwidth.component S' U v := by
  ext w
  unfold CubicPathwidth.component
  simp only [Finset.mem_filter]
  constructor
  · rintro ⟨hw, hv, hmin⟩
    exact ⟨hw, hv, fun T hT hc hvT => hmin T hT ((closedIn_congr hT h).mpr hc) hvT⟩
  · rintro ⟨hw, hv, hmin⟩
    exact ⟨hw, hv, fun T hT hc hvT => hmin T hT ((closedIn_congr hT h).mp hc) hvT⟩

/-- `components U` only reads the graph on `U`. -/
theorem components_congr {S S' : SimpleGraph (Fin n)} {U : Finset (Fin n)}
    (h : ∀ u ∈ U, ∀ v ∈ U, S.Adj u v ↔ S'.Adj u v) :
    CubicPathwidth.components S U = CubicPathwidth.components S' U := by
  ext T
  unfold CubicPathwidth.components
  simp only [Finset.mem_image, component_congr h]

/-- `attachment B T` only reads the graph between `B` and `T`. -/
theorem attachment_congr {S S' : SimpleGraph (Fin n)} {B T : Finset (Fin n)}
    (h : ∀ u ∈ B, ∀ v ∈ T, S.Adj u v ↔ S'.Adj u v) :
    CubicPathwidth.attachment S B T = CubicPathwidth.attachment S' B T := by
  ext x
  rw [CubicPathwidth.mem_attachment S, CubicPathwidth.mem_attachment S']
  constructor
  · rintro ⟨hx, u, hu, hxu⟩
    exact ⟨hx, u, hu, (h x hx u hu).mp hxu⟩
  · rintro ⟨hx, u, hu, hxu⟩
    exact ⟨hx, u, hu, (h x hx u hu).mpr hxu⟩

/-- The torso of `(F, B)` only depends on the graph on `F₀`, when `B ⊆ F ⊆ F₀`. -/
theorem tgraph_congr_of {S S' : SimpleGraph (Fin n)} {F₀ : Finset (Fin n)}
    (h : ∀ u ∈ F₀, ∀ v ∈ F₀, S.Adj u v ↔ S'.Adj u v) {F B : Finset (Fin n)}
    (hB : B ⊆ F) (hF : F ⊆ F₀) : CubicPathwidth.T4.tgraph S F B = CubicPathwidth.T4.tgraph S' F B := by
  have hU : F \ B ⊆ F₀ := Finset.sdiff_subset.trans hF
  have hBF₀ : B ⊆ F₀ := hB.trans hF
  have hcomp : CubicPathwidth.components S (F \ B) = CubicPathwidth.components S' (F \ B) :=
    components_congr (fun a ha b hb => h a (hU ha) b (hU hb))
  have hatt : ∀ T ∈ CubicPathwidth.components S (F \ B),
      CubicPathwidth.attachment S B T = CubicPathwidth.attachment S' B T :=
    fun T hT => attachment_congr
      (fun a ha b hb => h a (hBF₀ ha) b (hU ((CubicPathwidth.mem_components S hT).1 hb)))
  ext x y
  rw [CubicPathwidth.T4.tgraph_adj_iff S F B x y, CubicPathwidth.T4.tgraph_adj_iff S' F B x y]
  constructor
  · rintro ⟨hne, hx, hy, hxy | ⟨T, hT, hxT, hyT⟩⟩
    · exact ⟨hne, hx, hy, Or.inl ((h x (hBF₀ hx) y (hBF₀ hy)).mp hxy)⟩
    · have hT' : T ∈ CubicPathwidth.components S' (F \ B) := by rw [← hcomp]; exact hT
      rw [hatt T hT] at hxT hyT
      exact ⟨hne, hx, hy, Or.inr ⟨T, hT', hxT, hyT⟩⟩
  · rintro ⟨hne, hx, hy, hxy | ⟨T, hT, hxT, hyT⟩⟩
    · exact ⟨hne, hx, hy, Or.inl ((h x (hBF₀ hx) y (hBF₀ hy)).mpr hxy)⟩
    · have hT' : T ∈ CubicPathwidth.components S (F \ B) := by rw [hcomp]; exact hT
      rw [← hatt T hT'] at hxT hyT
      exact ⟨hne, hx, hy, Or.inr ⟨T, hT', hxT, hyT⟩⟩

/-- Torso degrees agree when the torsos agree. -/
theorem tdeg_congr_of {S S' : SimpleGraph (Fin n)} {F B : Finset (Fin n)}
    (hg : CubicPathwidth.T4.tgraph S F B = CubicPathwidth.T4.tgraph S' F B) (v : Fin n) :
    CubicPathwidth.T4.tdeg S F B v = CubicPathwidth.T4.tdeg S' F B v := by
  rw [CubicPathwidth.T4.tdeg_eq_card S F B v, CubicPathwidth.T4.tdeg_eq_card S' F B v, hg]

/-- The core stays inside the undeleted set along a reachability. -/
theorem inv_reach {G : SimpleGraph (Fin n)} {s t : Finset (Fin n) × Finset (Fin n)}
    (h : CubicPathwidth.T4.Reach G s t) (hs : s.2 ⊆ s.1) : t.2 ⊆ t.1 := by
  induction h with
  | refl => exact hs
  | tail _ hst ih =>
    cases hst with
    | reduce _ _ => exact (Finset.erase_subset _ _).trans ih
    | delete _ => exact Finset.erase_subset_erase _ ih

/-- Reachability in `S'` from a state inside `F₀` is reachability in `S`. -/
theorem reach_transfer {S S' : SimpleGraph (Fin n)} {F₀ : Finset (Fin n)}
    (h : ∀ u ∈ F₀, ∀ v ∈ F₀, S.Adj u v ↔ S'.Adj u v) {s t : Finset (Fin n) × Finset (Fin n)}
    (hr : CubicPathwidth.T4.Reach S' s t) (hs : s.2 ⊆ s.1) (hF : s.1 ⊆ F₀) :
    CubicPathwidth.T4.Reach S s t := by
  induction hr with
  | refl => exact CubicPathwidth.T4.Reach.refl S _
  | @tail b c hb hst ih =>
    have hbF : b.1 ⊆ F₀ := (CubicPathwidth.T4.Reach.subset hb).1.trans hF
    have hbinv : b.2 ⊆ b.1 := inv_reach hb hs
    cases hst with
    | @reduce F B v hv hdeg =>
      have hBF : B ⊆ F := hbinv
      have hFF₀ : F ⊆ F₀ := hbF
      have hg := tgraph_congr_of h hBF hFF₀
      have hdeg' : CubicPathwidth.T4.tdeg S F B v ≤ 2 := by
        rw [tdeg_congr_of hg v]; exact hdeg
      exact ih.tail (CubicPathwidth.T4.Step.reduce hv hdeg')
    | @delete F B w hw =>
      exact ih.tail (CubicPathwidth.T4.Step.delete hw)

end CubicPathwidth.Alg.D6

namespace CubicPathwidth.Alg

/-- (D6) Locality of torsos: the torso of a state `B ⊆ F ⊆ F₀` and reachability from it
only depend on the graph on `F₀`. -/
theorem torsoLocal : TorsoLocal := by
  unfold TorsoLocal
  intro n S S' F₀ h
  exact ⟨fun F B hB hF => D6.tgraph_congr_of h hB hF,
    fun F B F' B' hB hF hr => D6.reach_transfer h hr hB hF⟩

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.torsoLocal