CubicPathwidth.T4.DeletionXKey

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

import CubicPathwidth.T4.DeletionXLoc
import CubicPathwidth.T4.DeletionXArith

/-!
# One round of the deletion process (helper for `DeletionX`)

`key_step`: in a good state with torso minimum degree at least `3`, for a torso
component `C` that is not basic there is a deletion of a core vertex `w ∈ C`, followed
by a maximal sequence of reductions, which pays for itself: `1 + ψ⁻' ≤ ψ⁻`.
This is the "connected and not basic" case of the proof of Proposition 9.10 (`prop:deletion`).
-/

noncomputable section

namespace CubicPathwidth
namespace T4
namespace DelX

open T2 SectionDecomposition

variable {n : ℕ}

/-- The quantity `J₄` of the manuscript, in global form: the drop of `ψ` caused by the
reductions, plus the gain in the sum of the `H`-terms of the other components. -/
def Jval (b : ℕ → ℝ) (G : SimpleGraph (Fin n)) (F B C : Finset (Fin n)) (w : Fin n)
    (B' : Finset (Fin n)) : ℝ :=
  (psi b G (F.erase w) (B.erase w) - psi b G (F.erase w) B') +
    (∑ D ∈ tcomps G (F.erase w) B', runMin b (cmin G (F.erase w) B' D) -
      ∑ D ∈ (tcomps G F B).erase C, runMin b (cmin G F B D))

/-- Choosing a centre: a vertex of maximum degree which has a neighbour of smaller
degree, if there is one (so that a non-regular `C` gives such a vertex). -/
theorem choose_center {H : SimpleGraph (Fin n)} {C : Finset (Fin n)}
    (hconn : SectionConnected H C) (d : Fin n → ℕ) {Δ : ℕ}
    (hmax : ∀ v ∈ C, d v ≤ Δ) (hex : ∃ w ∈ C, d w = Δ) :
    ∃ w ∈ C, d w = Δ ∧ ((∀ v ∈ C, d v = Δ) ∨ ∃ x, H.Adj w x ∧ d x < Δ) := by
  classical
  by_cases h : ∃ w ∈ C, d w = Δ ∧ ∃ x, H.Adj w x ∧ d x < Δ
  · obtain ⟨w, hwC, hwd, hx⟩ := h
    exact ⟨w, hwC, hwd, Or.inr hx⟩
  · obtain ⟨w₀, hw₀C, hw₀d⟩ := hex
    refine ⟨w₀, hw₀C, hw₀d, Or.inl ?_⟩
    by_contra hnreg
    push Not at hnreg
    obtain ⟨v, hvC, hvne⟩ := hnreg
    have hmem : w₀ ∈ C.filter (fun x => d x = Δ) := Finset.mem_filter.mpr ⟨hw₀C, hw₀d⟩
    obtain ⟨u, hu, v', hv', huv'⟩ := connected_cross_edge H hconn (S := C.filter (fun x => d x = Δ))
      (Finset.filter_subset _ _) ⟨w₀, hmem⟩ (by
        intro heq
        have : v ∈ C.filter (fun x => d x = Δ) := by rw [heq]; exact hvC
        exact hvne (Finset.mem_filter.mp this).2)
    obtain ⟨huC, hud⟩ := Finset.mem_filter.mp hu
    obtain ⟨hv'C, hv'n⟩ := Finset.mem_sdiff.mp hv'
    have hv'd : d v' ≠ Δ := fun h' => hv'n (Finset.mem_filter.mpr ⟨hv'C, h'⟩)
    exact h ⟨u, huC, hud, v', huv', lt_of_le_of_ne (hmax v' hv'C) hv'd⟩

/-- The `H`-terms: components other than `C` survive, and a surviving vertex `u` of `C`
contributes a new component inside `C`. -/
theorem comp_sum_ge (hdyn : TorsoDynamics) {b : ℕ → ℝ} (hb : BootProps b)
    {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)} (hg : Good G F B)
    (hmin : ∀ v ∈ B, 3 ≤ tdeg G F B v) {C : Finset (Fin n)} (hC : C ∈ tcomps G F B)
    {w : Fin n} (hwC : w ∈ C) {B' : Finset (Fin n)}
    (hR : Reach G (F, B) (F.erase w, B')) :
    (∑ D ∈ (tcomps G F B).erase C, runMin b (cmin G F B D) ≤
      ∑ D ∈ tcomps G (F.erase w) B', runMin b (cmin G (F.erase w) B' D)) ∧
    (∀ u ∈ C, u ∈ B' →
      runMin b (tdeg G (F.erase w) B' u) +
        ∑ D ∈ (tcomps G F B).erase C, runMin b (cmin G F B D) ≤
      ∑ D ∈ tcomps G (F.erase w) B', runMin b (cmin G (F.erase w) B' D)) := by
  classical
  have hFB : B ⊆ F := hg.subset
  have hpres : ∀ C' ∈ (tcomps G F B).erase C,
      C' ∈ tcomps G (F.erase w) B' ∧ cmin G (F.erase w) B' C' = cmin G F B C' := by
    intro C' hC'
    obtain ⟨hne, hC'm⟩ := Finset.mem_erase.mp hC'
    have hdisj := components_disjoint (tgraph G F B) hC'm hC (hne)
    have hwC' : w ∉ C' := fun h => Finset.disjoint_left.mp hdisj h hwC
    have hC'B := (mem_components (tgraph G F B) hC'm).1
    exact tcomp_preserve hdyn hg hmin hR hC'm (fun x hx =>
      Finset.mem_erase.mpr ⟨fun h => hwC' (h ▸ hx), hFB (hC'B hx)⟩)
  have hsub : (tcomps G F B).erase C ⊆ tcomps G (F.erase w) B' := fun C' hC' =>
    (hpres C' hC').1
  have heqsum : ∑ D ∈ (tcomps G F B).erase C, runMin b (cmin G (F.erase w) B' D) =
      ∑ D ∈ (tcomps G F B).erase C, runMin b (cmin G F B D) :=
    Finset.sum_congr rfl fun D hD => by rw [(hpres D hD).2]
  refine ⟨?_, ?_⟩
  · rw [← heqsum]
    exact Finset.sum_le_sum_of_subset_of_nonneg hsub (fun D _ _ => runMin_nonneg hb _)
  · intro u huC huB'
    have hDu : component (tgraph G (F.erase w) B') B' u ∈ tcomps G (F.erase w) B' :=
      component_mem_tcomps huB'
    have hDuC := reach_component_subset hdyn hg hR hC huC huB'
    have huDu : u ∈ component (tgraph G (F.erase w) B') B' u := mem_component_self _ huB'
    have hnot : component (tgraph G (F.erase w) B') B' u ∉ (tcomps G F B).erase C := by
      intro hmem
      obtain ⟨hne, hm⟩ := Finset.mem_erase.mp hmem
      have hdisj := components_disjoint (tgraph G F B) hm hC hne
      exact Finset.disjoint_left.mp hdisj huDu huC
    have hsub2 : insert (component (tgraph G (F.erase w) B') B' u) ((tcomps G F B).erase C) ⊆
        tcomps G (F.erase w) B' := by
      intro D hD
      rcases Finset.mem_insert.mp hD with rfl | hD
      · exact hDu
      · exact hsub hD
    have h1 := Finset.sum_le_sum_of_subset_of_nonneg
      (f := fun D => runMin b (cmin G (F.erase w) B' D)) hsub2
      (fun D _ _ => runMin_nonneg hb _)
    rw [Finset.sum_insert hnot, heqsum] at h1
    have hle : cmin G (F.erase w) B' (component (tgraph G (F.erase w) B') B' u) ≤
        tdeg G (F.erase w) B' u := by
      unfold cmin
      have hne : (component (tgraph G (F.erase w) B') B' u).Nonempty := ⟨u, huDu⟩
      simp only [hne, dite_true]
      exact Finset.inf'_le _ huDu
    have h2 := runMin_anti b hle
    linarith

/-- The Claim of the manuscript: if `u ∈ C - w` has degree `j ≥ 3` after the deletion
of `w`, then `J₄ ≥ H_j`. -/
theorem claim_J (hdyn : TorsoDynamics) {b : ℕ → ℝ} (hb : BootProps b)
    {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)} (hg : Good G F B)
    (hmin : ∀ v ∈ B, 3 ≤ tdeg G F B v) {C : Finset (Fin n)} (hC : C ∈ tcomps G F B)
    {w : Fin n} (hwC : w ∈ C) {B' : Finset (Fin n)} (hB'sub : B' ⊆ B.erase w)
    (hR : Reach G (F, B) (F.erase w, B'))
    (hdeg' : ∀ v ∈ B', tdeg G (F.erase w) B' v ≤ tdeg G (F.erase w) (B.erase w) v) :
    ∀ u ∈ C.erase w, 3 ≤ tdeg G (F.erase w) (B.erase w) u →
      runMin b (tdeg G (F.erase w) (B.erase w) u) ≤ Jval b G F B C w B' := by
  classical
  intro u hu hu3
  have huC := Finset.mem_of_mem_erase hu
  obtain ⟨hs1, hs2⟩ := comp_sum_ge hdyn hb hg hmin hC hwC hR
  have hpsi : psi b G (F.erase w) B' ≤ psi b G (F.erase w) (B.erase w) :=
    psi_le_psi hb hB'sub hdeg'
  unfold Jval
  by_cases huB' : u ∈ B'
  · have h1 := hs2 u huC huB'
    have h2 := runMin_anti b (hdeg' u huB')
    linarith
  · have huBw : u ∈ B.erase w := Finset.mem_erase.mpr ⟨Finset.ne_of_mem_erase hu, 
      (mem_components (tgraph G F B) (show C ∈ components (tgraph G F B) B from hC)).1 huC⟩
    have hsd := Finset.sum_sdiff (f := fun v => b (tdeg G (F.erase w) (B.erase w) v)) hB'sub
    have hmono : ∑ v ∈ B', b (tdeg G (F.erase w) B' v) ≤
        ∑ v ∈ B', b (tdeg G (F.erase w) (B.erase w) v) :=
      Finset.sum_le_sum fun v hv => hb.monotone (hdeg' v hv)
    have hsingle : b (tdeg G (F.erase w) (B.erase w) u) ≤
        ∑ v ∈ (B.erase w) \ B', b (tdeg G (F.erase w) (B.erase w) v) :=
      Finset.single_le_sum (f := fun v => b (tdeg G (F.erase w) (B.erase w) v))
        (fun v _ => hb.nonneg _) (Finset.mem_sdiff.mpr ⟨huBw, huB'⟩)
    have h3 := runMin_le_b hb hu3
    unfold psi at *
    linarith

/-- One round of the process on a non-basic torso component. -/
theorem key_step (hdyn : TorsoDynamics) {b : ℕ → ℝ} (hb : BootProps b)
    {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)} (hg : Good G F B)
    (hmin : ∀ v ∈ B, 3 ≤ tdeg G F B v) {C : Finset (Fin n)} (hC : C ∈ tcomps G F B)
    (hnb : ¬ Basic G F B C) :
    ∃ w ∈ B, ∃ B' ⊆ B.erase w, Reach G (F, B) (F.erase w, B') ∧
      (∀ v ∈ B', 3 ≤ tdeg G (F.erase w) B' v) ∧
      1 + psiMinus b G (F.erase w) B' ≤ psiMinus b G F B := by
  classical
  obtain ⟨hCB, hcl, hconn⟩ := mem_components (tgraph G F B) hC
  have hCne : C.Nonempty := hconn.1
  -- non-basic: unpack
  have hbig : ∃ v ∈ C, 5 < tdeg G F B v := by
    by_contra h
    apply hnb
    left
    intro v hv
    by_contra h'
    exact h ⟨v, hv, by omega⟩
  have hnodel : ∀ v ∈ C, ∀ B'' : Finset (Fin n), Reach G (F, B) (F.erase v, B'') →
      ¬ Disjoint B'' C := fun v hv B'' hr hd => hnb (Or.inr ⟨v, hv, B'', hr, hd⟩)
  -- the maximum degree
  obtain ⟨w₀, hw₀C, hw₀max⟩ := Finset.exists_max_image C (tdeg G F B) hCne
  set Δ := tdeg G F B w₀ with hΔdef
  have hΔ : 6 ≤ Δ := by
    obtain ⟨v, hv, h5⟩ := hbig
    have := hw₀max v hv
    omega
  obtain ⟨w, hwC, hwd, hreg0⟩ := choose_center hconn (tdeg G F B) hw₀max ⟨w₀, hw₀C, rfl⟩
  have hwB : w ∈ B := hCB hwC
  -- the deletion and the maximal reduction
  have hstep : Step G (F, B) (F.erase w, B.erase w) := Step.delete hwB
  have hg1 : Good G (F.erase w) (B.erase w) := hg.reach (Reach.single hstep)
  obtain ⟨B', hB'sub, hRed, hmin', hdeg'⟩ := td_maxred hdyn hg1
  have hR : Reach G (F, B) (F.erase w, B') := (Reach.single hstep).trans hRed
  -- some vertex of C survives
  obtain ⟨u₁, hu₁B', hu₁C⟩ := Finset.not_disjoint_iff.mp (hnodel w hwC B' hR)
  -- the data for the arithmetic lemma
  have hCd : ∀ v ∈ C, 3 ≤ tdeg G F B v ∧ tdeg G F B v ≤ Δ :=
    fun v hv => ⟨hmin v (hCB hv), hw₀max v hv⟩
  have hNC : nbrs G F B w ⊆ C.erase w := by
    intro u hu
    have h := mem_nbrs.mp hu
    refine Finset.mem_erase.mpr ⟨h.1.symm, ?_⟩
    exact hcl w hwC u h.2.2.1 h
  have hNcard : (nbrs G F B w).card = Δ := by
    rw [← tdeg_eq_card_nbrs]; exact hwd
  have hd'N : ∀ v ∈ nbrs G F B w,
      tdeg G (F.erase w) (B.erase w) v + 1 = tdeg G F B v := by
    intro v hv
    have hvw : v ≠ w := Finset.ne_of_mem_erase (nbrs_subset_erase hv)
    have := tdeg_delete hdyn hg hwB hvw
    simpa [hv] using this
  have hd'o : ∀ v ∈ C.erase w, v ∉ nbrs G F B w →
      tdeg G (F.erase w) (B.erase w) v = tdeg G F B v := by
    intro v hv hvn
    have hvw : v ≠ w := Finset.ne_of_mem_erase hv
    have := tdeg_delete hdyn hg hwB hvw
    simpa [hvn] using this
  have hδ : ∀ v ∈ C, cmin G F B C ≤ tdeg G F B v := by
    intro v hv
    unfold cmin
    simp only [hCne, dite_true]
    exact Finset.inf'_le _ hv
  have hδ' : ∃ v ∈ C, tdeg G F B v = cmin G F B C := by
    unfold cmin
    simp only [hCne, dite_true]
    obtain ⟨v, hv, h⟩ := Finset.exists_mem_eq_inf' hCne (tdeg G F B)
    exact ⟨v, hv, h.symm⟩
  have hreg : (∀ v ∈ C, tdeg G F B v = Δ) ∨ ∃ x ∈ nbrs G F B w, tdeg G F B x < Δ := by
    rcases hreg0 with h | ⟨x, hx, hxlt⟩
    · exact Or.inl h
    · exact Or.inr ⟨x, mem_nbrs.mpr hx, hxlt⟩
  have hJ := claim_J hdyn hb hg hmin hC hwC hB'sub hR hdeg'
  have hstar : ∃ u ∈ C.erase w, 3 ≤ tdeg G (F.erase w) (B.erase w) u := by
    have hu₁w : u₁ ≠ w := Finset.ne_of_mem_erase (hB'sub hu₁B')
    exact ⟨u₁, Finset.mem_erase.mpr ⟨hu₁w, hu₁C⟩,
      (hmin' u₁ hu₁B').trans (hdeg' u₁ hu₁B')⟩
  have hcore := deletion_core_ineq hb C (nbrs G F B w) w (tdeg G F B)
    (tdeg G (F.erase w) (B.erase w)) Δ (cmin G F B C)
    (Jval b G F B C w B') hΔ hCd hwd hNC hNcard hd'N hd'o hδ hδ' hreg hJ hstar
  -- assemble
  refine ⟨w, hwB, B', hB'sub, hR, hmin', ?_⟩
  have hid := hb.identity Δ hΔ
  have hpd := psi_delete hdyn b hg hwB
  rw [hwd] at hpd
  have hcsum : ∑ D ∈ tcomps G F B, runMin b (cmin G F B D) =
      runMin b (cmin G F B C) + ∑ D ∈ (tcomps G F B).erase C, runMin b (cmin G F B D) :=
    (Finset.add_sum_erase _ _ hC).symm
  unfold psiMinus
  rw [hcsum]
  unfold Jval at hcore
  have hincr : ∀ v, b (tdeg G F B v) - b (tdeg G F B v - 1) = incr b (tdeg G F B v) :=
    fun v => rfl
  simp only [hincr] at hpd
  linarith

end DelX
end T4
end CubicPathwidth