CubicPathwidth.CorePruning

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

import CubicPathwidth.CoreCounting

/-!
# Pruning leaves without losing the core count

`ClosedIn G U S` says S is a union of components of the graph induced by U.
`NonnegativeComponentExcess` is its arithmetic no-tree-component condition:
every such union has at least as many edges as vertices. We prove directly
that this condition survives deleting a leaf. No graph-search oracle or
unproved extraction routine is used.
-/

noncomputable section
namespace CubicPathwidth

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

def ClosedIn (U S : Finset (Fin n)) : Prop :=
  ∀ v ∈ S, ∀ w ∈ U, G.Adj v w → w ∈ S

def NonnegativeComponentExcess (U : Finset (Fin n)) : Prop :=
  ∀ S : Finset (Fin n), S ⊆ U → ClosedIn G U S → 0 ≤ degreeExcess G S

theorem nonnegativeComponentExcess_degree_pos {U : Finset (Fin n)}
    (h : NonnegativeComponentExcess G U) {v : Fin n} (hv : v ∈ U) :
    0 < (sectionNeighbors G U v).card := by
  classical
  by_contra hn
  have hz : sectionNeighbors G U v = ∅ := Finset.card_eq_zero.mp (by omega)
  have hclosed : ClosedIn G U {v} := by
    intro a ha w hw hadj
    have hav : a = v := Finset.mem_singleton.mp ha
    subst a
    have hmem : w ∈ sectionNeighbors G U v := mem_sectionNeighbors.mpr ⟨hw, hadj⟩
    rw [hz] at hmem
    exact False.elim (Finset.notMem_empty w hmem)
  have he := h {v} (Finset.singleton_subset_iff.mpr hv) hclosed
  simp [degreeExcess, incidence_singleton] at he

theorem nonnegativeComponentExcess_erase_leaf {U : Finset (Fin n)}
    (h : NonnegativeComponentExcess G U) {v : Fin n} (hv : v ∈ U)
    (hdeg : (sectionNeighbors G U v).card = 1) :
    NonnegativeComponentExcess G (U.erase v) := by
  classical
  obtain ⟨u, hu⟩ := Finset.card_eq_one.mp hdeg
  have hun : u ∈ sectionNeighbors G U v := by rw [hu]; simp
  obtain ⟨huU, hvu⟩ := mem_sectionNeighbors.mp hun
  have unique : ∀ w ∈ U, G.Adj v w → w = u := by
    intro w hw hadj
    have hn : w ∈ sectionNeighbors G U v := mem_sectionNeighbors.mpr ⟨hw, hadj⟩
    rw [hu] at hn
    exact Finset.mem_singleton.mp hn
  intro S hS hclosed
  have hvS : v ∉ S := by
    intro hv'
    exact Finset.notMem_erase v U (hS hv')
  have hSU : S ⊆ U := hS.trans (Finset.erase_subset _ _)
  by_cases huS : u ∈ S
  · have hsub : insert v S ⊆ U := Finset.insert_subset hv hSU
    have hc : ClosedIn G U (insert v S) := by
      intro a ha w hw hadj
      by_cases hwv : w = v
      · subst w
        exact Finset.mem_insert_self _ _
      · rcases Finset.mem_insert.mp ha with rfl | haS
        · rw [unique w hw hadj]
          exact Finset.mem_insert_of_mem huS
        · exact Finset.mem_insert_of_mem
            (hclosed a haS w (Finset.mem_erase.mpr ⟨hwv, hw⟩) hadj)
    have hneigh : sectionNeighbors G S v = {u} := by
      ext w
      constructor
      · intro hw
        obtain ⟨hwS, hvw⟩ := mem_sectionNeighbors.mp hw
        exact Finset.mem_singleton.mpr (unique w (hSU hwS) hvw)
      · intro hw
        have hwu := Finset.mem_singleton.mp hw
        subst w
        exact mem_sectionNeighbors.mpr ⟨huS, hvu⟩
    have he := h (insert v S) hsub hc
    rw [degreeExcess_insert G hvS, hneigh] at he
    simpa using he
  · apply h S hSU
    intro a ha w hw hadj
    have hwv : w ≠ v := by
      intro heq
      subst w
      have hau := unique a (hSU ha) hadj.symm
      exact huS (hau ▸ ha)
    exact hclosed a ha w (Finset.mem_erase.mpr ⟨hwv, hw⟩) hadj

/-- A certificate retaining every vertex except a sequence of degree-one
vertices. Isolated vertices are deliberately not removed by this relation. -/
inductive LeafPrunes : Finset (Fin n) → Finset (Fin n) → Prop
  | refl (U) : LeafPrunes U U
  | step {U C} (v : Fin n) (hv : v ∈ U)
      (hdeg : (sectionNeighbors G U v).card = 1)
      (rest : LeafPrunes (U.erase v) C) : LeafPrunes U C

theorem LeafPrunes.subset {U C : Finset (Fin n)} (h : LeafPrunes G U C) : C ⊆ U := by
  induction h with
  | refl U => exact Finset.Subset.refl U
  | step v hv hdeg rest ih => exact ih.trans (Finset.erase_subset _ _)

theorem LeafPrunes.excess_eq {U C : Finset (Fin n)} (h : LeafPrunes G U C) :
    degreeExcess G C = degreeExcess G U := by
  induction h with
  | refl U => rfl
  | step v hv hdeg rest ih => exact ih.trans (degreeExcess_erase_leaf G hv hdeg)

/-- Actual finite core extraction under the arithmetic no-tree condition. -/
theorem exists_leafPrunes_minDegree_two (U : Finset (Fin n))
    (h : NonnegativeComponentExcess G U) :
    ∃ C : Finset (Fin n), LeafPrunes G U C ∧
      ∀ v ∈ C, 2 ≤ (sectionNeighbors G C v).card := by
  classical
  have go : ∀ m : ℕ, ∀ U : Finset (Fin n), U.card = m →
      NonnegativeComponentExcess G U →
      ∃ C : Finset (Fin n), LeafPrunes G U C ∧
        ∀ v ∈ C, 2 ≤ (sectionNeighbors G C v).card := by
    intro m
    induction m using Nat.strong_induction_on with
    | h m ih =>
      intro V hV hgood
      by_cases hmin : ∀ v ∈ V, 2 ≤ (sectionNeighbors G V v).card
      · exact ⟨V, LeafPrunes.refl V, hmin⟩
      · obtain ⟨v, hv, hsmall⟩ : ∃ v ∈ V, (sectionNeighbors G V v).card < 2 := by
          simpa only [not_forall, not_le, exists_prop] using hmin
        have hpos := nonnegativeComponentExcess_degree_pos G hgood hv
        have hone : (sectionNeighbors G V v).card = 1 := by omega
        have hlt : (V.erase v).card < m := by
          rw [← hV]
          exact Finset.card_erase_lt_of_mem hv
        obtain ⟨C, hprune, hC⟩ := ih _ hlt (V.erase v) rfl
          (nonnegativeComponentExcess_erase_leaf G hgood hv hone)
        exact ⟨C, LeafPrunes.step v hv hone hprune, hC⟩
  exact go U.card U rfl h

/-- A stable boundary with no tree component outside it has a core whose
number q of degree-three vertices satisfies q + 3|X| ≤ |U|. -/
theorem exists_core_branch_bound (hG : IsSubcubic G)
    {U X : Finset (Fin n)} (hX : X ⊆ U) (hs : StableBoundary G U X)
    (hgood : NonnegativeComponentExcess G (U \ X)) :
    ∃ C : Finset (Fin n), LeafPrunes G (U \ X) C ∧
      (∀ v ∈ C, 2 ≤ (sectionNeighbors G C v).card) ∧
      (C.filter (fun v => (sectionNeighbors G C v).card = 3)).card + 3 * X.card ≤ U.card := by
  classical
  obtain ⟨C, hp, hm⟩ := exists_leafPrunes_minDegree_two G (U \ X) hgood
  refine ⟨C, hp, hm, ?_⟩
  have hbound := stable_degreeExcess_bound G hG hX hs
  have he := hp.excess_eq
  have hc := degreeExcess_eq_branch_card G hG C hm
  omega

end CubicPathwidth